Theory Definitions

(*  Title:       Extension of Stateful Intransitive Noninterference with Inputs, Outputs, and Nondeterminism in Language IMP
    Author:      Pasquale Noce
                 Senior Staff Firmware Engineer at HID Global, Italy
                 pasquale dot noce dot lavoro at gmail dot com
                 pasquale dot noce at hidglobal dot com
*)

section "Underlying concepts and formal definitions"

theory Definitions
  imports Small_Step
begin


subsection "Global context definitions"

text ‹
As compared with my previous paper \<^cite>‹"Noce24"›:

  ▪ Type @{text flow}, which models any potential program execution flow as a list of instructions,
occurring in their order of execution, is extended with two additional instructions, namely an input
instruction @{text "IN x"} and an output instruction @{text "OUT x"} standing for the respective
additional commands of the considered extension of language IMP.

  ▪ Function @{text run_flow}, which used to map a pair formed by such a program execution flow
@{text cs} and a starting program state @{text s} to the resulting program state, here takes two
additional parameters, namely a starting trace of inputs @{text vs} and a stream of input values
@{text f}, since they are required as well for computing the resulting program state according to
the semantics of the considered extension of language IMP.

\null
›

declare [[syntax_ambiguity_warning = false]]


datatype com_flow =
  Assign vname aexp  (‹_ ::= _› [1000, 61] 70) |
  Input vname  (‹(IN _)› [61] 70) |
  Output vname  (‹(OUT _)› [61] 70) |
  Observe "vname set"  (‹⟨_⟩› [61] 70)

type_synonym flow = "com_flow list"
type_synonym tag = "vname × nat"
type_synonym config = "state set × vname set"
type_synonym scope = "config set × bool"
type_synonym state_upd = "vname × val option"


definition eq_streams ::
 "stream ⇒ stream ⇒ inputs ⇒ inputs ⇒ tag set ⇒ bool"
  (‹(_ = _ '(⊆ _, _, _'))› [51, 51] 50) where
"f = f' (⊆ vs, vs', T) ≡ ∀(x, n) ∈ T.
  f x (length [p←vs. fst p = x] + n) =
  f' x (length [p←vs'. fst p = x] + n)"

abbreviation eq_states :: "state ⇒ state ⇒ vname set ⇒ bool"
  (‹(_ = _ '(⊆ _'))› [51, 51] 50) where
"s = t (⊆ X) ≡ ∀x ∈ X. s x = t x"

abbreviation univ_states :: "state set ⇒ vname set ⇒ state set"
  (‹(Univ _ '(⊆ _'))› [51] 75) where
"Univ A (⊆ X) ≡ {s. ∃t ∈ A. s = t (⊆ X)}"

abbreviation univ_vars_if :: "state set ⇒ vname set ⇒ vname set"
  (‹(Univ?? _ _)› [51, 75] 75) where
"Univ?? A X ≡ if A = {} then UNIV else X"

abbreviation "tl2 xs ≡ tl (tl xs)"


primrec avars :: "aexp ⇒ vname set" where
"avars (N i) = {}" |
"avars (V x) = {x}" |
"avars (Plus a⇩1 a⇩2) = avars a⇩1 ∪ avars a⇩2"

primrec bvars :: "bexp ⇒ vname set" where
"bvars (Bc v) = {}" |
"bvars (Not b) = bvars b" |
"bvars (And b⇩1 b⇩2) = bvars b⇩1 ∪ bvars b⇩2" |
"bvars (Less a⇩1 a⇩2) = avars a⇩1 ∪ avars a⇩2"

fun no_upd :: "flow ⇒ vname set ⇒ bool" where
"no_upd (x ::= _ # cs) X = (x ∉ X ∧ no_upd cs X)" |
"no_upd (IN x # cs) X = (x ∉ X ∧ no_upd cs X)" |
"no_upd (OUT x # cs) X = (x ∉ X ∧ no_upd cs X)" |
"no_upd (_ # cs) X = no_upd cs X" |
"no_upd _ _ = True"


fun flow_aux :: "com list ⇒ flow" where
"flow_aux (x ::= a # cs) = (x ::= a) # flow_aux cs" |
"flow_aux (IN x # cs) = IN x # flow_aux cs" |
"flow_aux (OUT x # cs) = OUT x # flow_aux cs" |
"flow_aux (IF b THEN _ ELSE _ # cs) = ⟨bvars b⟩ # flow_aux cs" |
"flow_aux (WHILE b DO _ # cs) = ⟨bvars b⟩ # flow_aux cs" |
"flow_aux (c;; _ # cs) = flow_aux (c # cs)" |
"flow_aux (_ # cs) = flow_aux cs" |
"flow_aux [] = []"

definition flow :: "(com × stage) list ⇒ flow" where
"flow cfs = flow_aux (map fst cfs)"


function in_flow :: "flow ⇒ inputs ⇒ stream ⇒ inputs" where
"in_flow (cs @ [_ ::= _]) vs f = in_flow cs vs f" |
"in_flow (cs @ [IN x]) vs f = in_flow cs vs f @ (let
  n = length [p←vs. fst p = x] + length [c←cs. c = IN x]
  in [(x, f x n)])" |
"in_flow (cs @ [OUT _]) vs f = in_flow cs vs f" |
"in_flow (cs @ [⟨_⟩]) vs f = in_flow cs vs f" |
"in_flow [] _ _ = []"

proof atomize_elim
  fix p :: "flow × inputs × stream"
  show
   "(∃cs x a vs f. p = (cs @ [x ::= a], vs, f)) ∨
    (∃cs x vs f. p = (cs @ [IN x], vs, f)) ∨
    (∃cs x vs f. p = (cs @ [OUT x], vs, f)) ∨
    (∃cs X vs f. p = (cs @ [⟨X⟩], vs, f)) ∨
    (∃vs f. p = ([], vs, f))"
    by (cases p, metis com_flow.exhaust rev_exhaust)
qed auto

termination by lexicographic_order


function run_flow :: "flow ⇒ inputs ⇒ state ⇒ stream ⇒ state" where
"run_flow (cs @ [x ::= a]) vs s f = (let t = run_flow cs vs s f
  in t(x := aval a t))" |
"run_flow (cs @ [IN x]) vs s f = (let t = run_flow cs vs s f;
  n = length [p←vs. fst p = x] + length [c←cs. c = IN x]
  in t(x := f x n))" |
"run_flow (cs @ [OUT _]) vs s f = run_flow cs vs s f" |
"run_flow (cs @ [⟨_⟩]) vs s f = run_flow cs vs s f" |
"run_flow [] vs s _ = s"

proof atomize_elim
  fix p :: "flow × inputs × state × stream"
  show
   "(∃cs x a vs s f. p = (cs @ [x ::= a], vs, s, f)) ∨
    (∃cs x vs s f. p = (cs @ [IN x], vs, s, f)) ∨
    (∃cs x vs s f. p = (cs @ [OUT x], vs, s, f)) ∨
    (∃cs X vs s f. p = (cs @ [⟨X⟩], vs, s, f)) ∨
    (∃vs s f. p = ([], vs, s, f))"
    by (cases p, metis com_flow.exhaust rev_exhaust)
qed auto

termination by lexicographic_order


function out_flow :: "flow ⇒ inputs ⇒ state ⇒ stream ⇒ outputs" where
"out_flow (cs @ [_ ::= _]) vs s f = out_flow cs vs s f" |
"out_flow (cs @ [IN _]) vs s f = out_flow cs vs s f" |
"out_flow (cs @ [OUT x]) vs s f = (let t = run_flow cs vs s f
  in out_flow cs vs s f @ [(x, t x)])" |
"out_flow (cs @ [⟨_⟩]) vs s f = out_flow cs vs s f" |
"out_flow [] _ _ _ = []"

proof atomize_elim
  fix p :: "flow × inputs × state × stream"
  show
   "(∃cs x a vs s f. p = (cs @ [x ::= a], vs, s, f)) ∨
    (∃cs x vs s f. p = (cs @ [IN x], vs, s, f)) ∨
    (∃cs x vs s f. p = (cs @ [OUT x], vs, s, f)) ∨
    (∃cs X vs s f. p = (cs @ [⟨X⟩], vs, s, f)) ∨
    (∃vs s f. p = ([], vs, s, f))"
    by (cases p, metis com_flow.exhaust rev_exhaust)
qed auto

termination by lexicographic_order


subsection "Local context definitions"

locale noninterf =
  fixes
    interf :: "state ⇒ 'd ⇒ 'd ⇒ bool"
      (‹(_: _ ↝ _)› [51, 51, 51] 50) and
    dom :: "vname ⇒ 'd" and
    state :: "vname set"
  assumes
    interf_state: "s = t (⊆ state) ⟹ interf s = interf t"


context noninterf
begin

text ‹
\null

As in my previous paper \<^cite>‹"Noce24"›, function @{text sources} is defined along with an auxiliary
function @{text sources_aux} by means of mutual recursion. According to this definition, the set of
variables @{text "sources cs vs s f x"}, where:

  ▪ @{text cs} is a program execution flow,

  ▪ @{text vs} is a trace of inputs,

  ▪ @{text s} is a program state,

  ▪ @{text f} is a stream of input values, and

  ▪ @{text x} is a variable,

contains a variable @{text y} if there exist a descending sequence of left sublists @{text "cs⇩n⇩+⇩1"},
@{term "cs⇩n @ [c⇩n]"}, ..., @{term "cs⇩1 @ [c⇩1]"} of @{text cs} and a sequence of variables
@{text "y⇩n⇩+⇩1"}, ..., @{text y⇩1}, where $n \ge 1$, @{text "cs⇩n⇩+⇩1 = cs"}, @{text "y⇩n⇩+⇩1 = x"}, and
@{text "y⇩1 = y"}, satisfying the following conditions.

  ▪ For each positive integer $i \le n$, the instruction @{text "c⇩i"} is an assignment
@{text "y⇩i⇩+⇩1 ::= a⇩i"} such that:

    ▪ @{prop "y⇩i ∈ avars a⇩i"},

    ▪ @{text "run_flow cs⇩i vs s f: dom y⇩i ↝ dom y⇩i⇩+⇩1"}, and

    ▪ the right sublist of @{text "cs⇩i⇩+⇩1"} complementary to @{term "cs⇩i @ [c⇩i]"} does not comprise
any assignment or input instruction setting variable @{text "y⇩i⇩+⇩1"} (as the assignment @{text "c⇩i"}
would otherwise be irrelevant),

  or else an observation @{term "⟨X⇩i⟩"} such that:

    ▪ @{prop "y⇩i ∈ X⇩i"} and

    ▪ @{text "run_flow cs⇩i vs s f: dom y⇩i ↝ dom y⇩i⇩+⇩1"}.

  ▪ The program execution flow @{text "cs⇩1"} does not comprise any assignment or input instruction
setting variable @{text y}.

In addition, @{text "sources cs vs s f x"} contains variable @{text x} also if the program execution
flow @{text cs} does not comprise any assignment or input instruction setting variable @{text x}.

\null
›

function
  sources :: "flow ⇒ inputs ⇒ state ⇒ stream ⇒ vname ⇒ vname set" and
  sources_aux :: "flow ⇒ inputs ⇒ state ⇒ stream ⇒ vname ⇒ vname set"
where

"sources (cs @ [c]) vs s f x = (case c of
  z ::= a ⇒ if z = x
    then sources_aux cs vs s f x ∪ ⋃ {sources cs vs s f y | y.
      run_flow cs vs s f: dom y ↝ dom x ∧ y ∈ avars a}
    else sources cs vs s f x |
  IN z ⇒ if z = x
    then sources_aux cs vs s f x
    else sources cs vs s f x |
  ⟨X⟩ ⇒
    sources cs vs s f x ∪ ⋃ {sources cs vs s f y | y.
      run_flow cs vs s f: dom y ↝ dom x ∧ y ∈ X} |
  _ ⇒
    sources cs vs s f x)" |

"sources [] _ _ _ x = {x}" |

"sources_aux (cs @ [c]) vs s f x = (case c of
  ⟨X⟩ ⇒
    sources_aux cs vs s f x ∪ ⋃ {sources cs vs s f y | y.
      run_flow cs vs s f: dom y ↝ dom x ∧ y ∈ X} |
  _ ⇒
    sources_aux cs vs s f x)" |

"sources_aux [] _ _ _ _ = {}"

proof atomize_elim
  fix a :: "flow × inputs × state × stream × vname +
    flow × inputs × state × stream × vname"
  show
   "(∃cs c vs s f x. a = Inl (cs @ [c], vs, s, f, x)) ∨
    (∃vs s f x. a = Inl ([], vs, s, f, x)) ∨
    (∃cs c vs s f x. a = Inr (cs @ [c], vs, s, f, x)) ∨
    (∃vs s f x. a = Inr ([], vs, s, f, x))"
    by (metis obj_sumE prod_cases3 rev_exhaust)
qed auto

termination by lexicographic_order

lemmas sources_induct = sources_sources_aux.induct

text ‹
\null

Function @{text sources_out}, defined here below, takes the same parameters @{text cs}, @{text vs},
@{text s}, @{text f}, and @{text x} as function @{const sources}, and returns the set of the
variables whose values in the program state @{text s} are allowed to affect the outputs of variable
@{text x} possibly occurring as a result of the execution of flow @{text cs} if it starts from the
initial state @{text s} and the initial trace of inputs @{text vs}, and takes place according to the
stream of input values @{text f}.

In more detail, the set of variables @{text "sources_out cs vs s f x"} is defined as the union of
any set of variables @{text "sources cs⇩i vs s f x⇩i"}, where @{term "cs⇩i @ [c⇩i]"} is any left sublist
of @{text cs} such that the instruction @{text "c⇩i"} is an output instruction @{text "OUT x"}, in
which case @{text "x⇩i = x"}, or else an observation @{term "⟨X⇩i⟩"} such that:

  ▪ @{prop "x⇩i ∈ X⇩i"} and

  ▪ @{text "run_flow cs⇩i vs s f: dom x⇩i ↝ dom x"}.

\null
›

function
  sources_out :: "flow ⇒ inputs ⇒ state ⇒ stream ⇒ vname ⇒ vname set"
where

"sources_out (cs @ [c]) vs s f x = (case c of
  OUT z ⇒
    sources_out cs vs s f x ∪ (if z = x then sources cs vs s f x else {}) |
  ⟨X⟩ ⇒
    sources_out cs vs s f x ∪ ⋃ {sources cs vs s f y | y.
      run_flow cs vs s f: dom y ↝ dom x ∧ y ∈ X} |
  _ ⇒
    sources_out cs vs s f x)" |

"sources_out [] _ _ _ _ = {}"

by (atomize_elim, auto intro: rev_cases)
termination by lexicographic_order

text ‹
\null

Function @{text tags}, defined here below, takes the same parameters @{text cs}, @{text vs},
@{text s}, @{text f}, and @{text x} as the previous functions, and returns the set of the
\emph{tags}, namely of the pairs @{text "(y, m)"} where @{text y} is a variable and @{text m} is a
natural number, such that the @{text m}-th input instruction @{text "IN y"} within flow @{text cs}
is allowed to affect the value of variable @{text x} resulting from the execution of @{text cs} if
it starts from the initial state @{text s} and the initial trace of inputs @{text vs}, and takes
place according to the stream of input values @{text f}.

In more detail, the set of tags @{text "tags cs vs s f x"} contains a tag @{text "(y, m)"} just in
case there exist a descending sequence of left sublists @{text "cs⇩n⇩+⇩1"}, @{term "cs⇩n @ [c⇩n]"}, ...,
@{term "cs⇩1 @ [c⇩1]"} of @{text cs} and a sequence of variables @{text "y⇩n⇩+⇩1"}, ..., @{text y⇩1}, where
$n \ge 1$, @{text "cs⇩n⇩+⇩1 = cs"}, @{text "y⇩n⇩+⇩1 = x"}, @{text "y⇩1 = y"}, and @{text "y = x"} if $n = 1$,
satisfying the following conditions.

  ▪ For each integer $i$, if any, such that $1 < i \le n$, the instruction @{text "c⇩i"} is an
assignment @{text "y⇩i⇩+⇩1 ::= a⇩i"} such that:

    ▪ @{prop "y⇩i ∈ avars a⇩i"},

    ▪ @{text "run_flow cs⇩i vs s f: dom y⇩i ↝ dom y⇩i⇩+⇩1"}, and

    ▪ the right sublist of @{text "cs⇩i⇩+⇩1"} complementary to @{term "cs⇩i @ [c⇩i]"} does not comprise
any assignment or input instruction setting variable @{text "y⇩i⇩+⇩1"} (as the assignment @{text "c⇩i"}
would otherwise be irrelevant),

  or else an observation @{term "⟨X⇩i⟩"} such that:

    ▪ @{prop "y⇩i ∈ X⇩i"} and

    ▪ @{text "run_flow cs⇩i vs s f: dom y⇩i ↝ dom y⇩i⇩+⇩1"}.

  ▪ The instruction @{text "c⇩1"} is the @{text m}-th input instruction @{text "IN y"} within flow
@{text cs}.

  ▪ The right sublist of @{text "cs⇩2"} complementary to @{term "cs⇩1 @ [c⇩1]"} does not comprise any
assignment or input instruction setting variable @{text y} (as the input instruction @{text "c⇩1"}
would otherwise be irrelevant).

\null
›

function
  tags :: "flow ⇒ inputs ⇒ state ⇒ stream ⇒ vname ⇒ tag set" and
  tags_aux :: "flow ⇒ inputs ⇒ state ⇒ stream ⇒ vname ⇒ tag set"
where

"tags (cs @ [c]) vs s f x = (case c of
  z ::= a ⇒ if z = x
    then tags_aux cs vs s f x ∪ ⋃ {tags cs vs s f y | y.
      run_flow cs vs s f: dom y ↝ dom x ∧ y ∈ avars a}
    else tags cs vs s f x |
  IN z ⇒ if z = x
    then insert (x, length [c←cs. c = IN x]) (tags_aux cs vs s f x)
    else tags cs vs s f x |
  ⟨X⟩ ⇒
    tags cs vs s f x ∪ ⋃ {tags cs vs s f y | y.
      run_flow cs vs s f: dom y ↝ dom x ∧ y ∈ X} |
  _ ⇒
    tags cs vs s f x)" |

"tags [] _ _ _ _ = {}" |

"tags_aux (cs @ [c]) vs s f x = (case c of
  ⟨X⟩ ⇒
    tags_aux cs vs s f x ∪ ⋃ {tags cs vs s f y | y.
      run_flow cs vs s f: dom y ↝ dom x ∧ y ∈ X} |
  _ ⇒
    tags_aux cs vs s f x)" |

"tags_aux [] _ _ _ _ = {}"

proof atomize_elim
  fix a :: "flow × inputs × state × stream × vname +
    flow × inputs × state × stream × vname"
  show
   "(∃cs c vs s f x. a = Inl (cs @ [c], vs, s, f, x)) ∨
    (∃vs s f x. a = Inl ([], vs, s, f, x)) ∨
    (∃cs c vs s f x. a = Inr (cs @ [c], vs, s, f, x)) ∨
    (∃vs s f x. a = Inr ([], vs, s, f, x))"
    by (metis obj_sumE prod_cases3 rev_exhaust)
qed auto

termination by lexicographic_order

lemmas tags_induct = tags_tags_aux.induct

text ‹
\null

Finally, function @{text tags_out}, defined here below, takes the same parameters @{text cs},
@{text vs}, @{text s}, @{text f}, and @{text x} as the previous functions, and returns the set of
the tags @{text "(y, m)"} such that the @{text m}-th input instruction @{text "IN y"} within flow
@{text cs} is allowed to affect the outputs of variable @{text x} possibly occurring as a result of
the execution of flow @{text cs} if it starts from the initial state @{text s} and the initial trace
of inputs @{text vs}, and takes place according to the stream of input values @{text f}.

In more detail, the set of tags @{text "tags_out cs vs s f x"} is defined as the union of any set of
tags @{text "tags cs⇩i vs s f x⇩i"}, where @{term "cs⇩i @ [c⇩i]"} is any left sublist of @{text cs} such
that the instruction @{text "c⇩i"} is an output instruction @{text "OUT x"}, in which case
@{text "x⇩i = x"}, or else an observation @{term "⟨X⇩i⟩"} such that:

  ▪ @{prop "x⇩i ∈ X⇩i"} and

  ▪ @{text "run_flow cs⇩i vs s f: dom x⇩i ↝ dom x"}.

\null
›

function
  tags_out :: "flow ⇒ inputs ⇒ state ⇒ stream ⇒ vname ⇒ tag set"
where

"tags_out (cs @ [c]) vs s f x = (case c of
  OUT z ⇒
    tags_out cs vs s f x ∪ (if z = x then tags cs vs s f x else {}) |
  ⟨X⟩ ⇒
    tags_out cs vs s f x ∪ ⋃ {tags cs vs s f y | y.
      run_flow cs vs s f: dom y ↝ dom x ∧ y ∈ X} |
  _ ⇒
    tags_out cs vs s f x)" |

"tags_out [] _ _ _ _ = {}"

by (atomize_elim, auto intro: rev_cases)
termination by lexicographic_order

text ‹
\null

Predicate @{text correct}, defined here below, formalizes the extended termination-sensitive
information flow correctness criterion. As in my previous paper \<^cite>‹"Noce24"›, its parameters
consist of a program @{text c}, a set of program states @{text A}, and a set of variables @{text X}.

In more detail, for any state @{text s} agreeing with a state in @{text A} on the value of each
state variable contained in @{text X}, let the small-step semantics turn:

  ▪ the command @{text c} and the program execution stage @{text "(s, f, vs, ws)"} into a command
@{text "c⇩1"} and a program execution stage @{text "(s⇩1, f, vs⇩1, ws⇩1)"}, and

  ▪ the command @{text c⇩1} and the program execution stage @{text "(s⇩1, f, vs⇩1, ws⇩1)"} into a command
@{text "c⇩2"} and a program execution stage @{text "(s⇩2, f, vs⇩2, ws⇩2)"}.

Furthermore, let:

  ▪ @{text cs} be the program execution flow leading from @{text "(c⇩1, s⇩1, f, vs⇩1, ws⇩1)"} to
@{text "(c⇩2, s⇩2, f, vs⇩2, ws⇩2)"}, and

  ▪ @{text "(t⇩1, f', vs⇩1', ws⇩1')"} be any program execution stage,

and assume that the following conditions hold.

  ▪ @{text S} is a nonempty subset of the set of the variables @{text x} such that state
@{text "t⇩1"} agrees with @{text "s⇩1"} on the value of each variable contained in
@{term "sources cs vs⇩1 s⇩1 f x"}.

  ▪ For each variable @{text x} contained in @{text S}, and each tag @{text "(y, n)"} contained in
@{term "tags cs vs⇩1 s⇩1 f x"}, the stream of input values @{text f'} agrees with @{text f} on the
input value assigned to variable @{text y} by an input instruction @{text "IN y"} after @{text n}
previous such assignments to @{text y} following any one tracked by the starting trace of inputs
@{text vs⇩1'} and @{text "vs⇩1"}, respectively.

Then, the information flow is correct only if the small-step semantics turns the command
@{text "c⇩1"} and the program execution stage @{text "(t⇩1, f', vs⇩1', ws⇩1')"} into a command
@{text "c⇩2'"} and a program execution stage @{text "(t⇩2, f', vs⇩2', ws⇩2')"} satisfying the following
correctness conditions.

  ▪ @{prop "c⇩2' = SKIP"} just in case @{prop "c⇩2 = SKIP"}; namely, program execution terminates just
in case it terminates as a result of the execution of flow @{text cs}, so that the two program
executions cannot be distinguished based on program termination.

  ▪ The resulting sequence of input requests @{text "IN x"} being prompted, where @{text x} is any
variable contained in @{text S}, matches the one triggered by the execution of flow @{text cs}, so
that the two program executions cannot be distinguished based on those sequences.

  ▪ States @{text "t⇩2"} and @{text "s⇩2"} agree on the value of each variable contained in @{text S},
so that the two program executions cannot be distinguished based on the resulting program states.

Likewise, if the above assumptions hold for functions @{const sources_out} and @{const tags_out}
in place of functions @{const sources} and @{const tags}, respectively, then the information flow
correctness requires the first two correctness conditions listed above to hold as well, plus the
following one.

  ▪ The resulting sequence of outputs of any variable contained in @{text S} matches the one
produced by the execution of flow @{text cs}, so that the two program executions cannot be
distinguished based on those sequences.

\null
›

abbreviation ok_flow_1 where
"ok_flow_1 c⇩1 c⇩2 c⇩2' s⇩1 s⇩2 t⇩1 t⇩2 f f' vs⇩1 vs⇩1' vs⇩2 vs⇩2' ws⇩1' ws⇩2' cs ≡
  ∀S ⊆ {x. s⇩1 = t⇩1 (⊆ sources cs vs⇩1 s⇩1 f x)}.
    S ≠ {} ⟶
    f = f' (⊆ vs⇩1, vs⇩1', ⋃ {tags cs vs⇩1 s⇩1 f x | x. x ∈ S}) ⟶
      (c⇩1, t⇩1, f', vs⇩1', ws⇩1') →* (c⇩2', t⇩2, f', vs⇩2', ws⇩2') ∧
      (c⇩2 = SKIP) = (c⇩2' = SKIP) ∧
      map fst [p←drop (length vs⇩1) vs⇩2. fst p ∈ S] =
        map fst [p←drop (length vs⇩1') vs⇩2'. fst p ∈ S] ∧
      s⇩2 = t⇩2 (⊆ S)"

abbreviation ok_flow_2 where
"ok_flow_2 c⇩1 c⇩2 c⇩2' s⇩1 t⇩1 t⇩2 f f' vs⇩1 vs⇩1' vs⇩2 vs⇩2' ws⇩1 ws⇩1' ws⇩2 ws⇩2' cs ≡
  ∀S ⊆ {x. s⇩1 = t⇩1 (⊆ sources_out cs vs⇩1 s⇩1 f x)}.
    S ≠ {} ⟶
    f = f' (⊆ vs⇩1, vs⇩1', ⋃ {tags_out cs vs⇩1 s⇩1 f x | x. x ∈ S}) ⟶
      (c⇩1, t⇩1, f', vs⇩1', ws⇩1') →* (c⇩2', t⇩2, f', vs⇩2', ws⇩2') ∧
      (c⇩2 = SKIP) = (c⇩2' = SKIP) ∧
      map fst [p←drop (length vs⇩1) vs⇩2. fst p ∈ S] =
        map fst [p←drop (length vs⇩1') vs⇩2'. fst p ∈ S] ∧
      [p←drop (length ws⇩1) ws⇩2. fst p ∈ S] =
        [p←drop (length ws⇩1') ws⇩2'. fst p ∈ S]"

abbreviation ok_flow where
"ok_flow c⇩1 c⇩2 s⇩1 s⇩2 f vs⇩1 vs⇩2 ws⇩1 ws⇩2 cs ≡
  ∀t⇩1 f' vs⇩1' ws⇩1'. ∃c⇩2' t⇩2 vs⇩2' ws⇩2'.
    ok_flow_1 c⇩1 c⇩2 c⇩2' s⇩1 s⇩2 t⇩1 t⇩2 f f' vs⇩1 vs⇩1' vs⇩2 vs⇩2' ws⇩1' ws⇩2' cs ∧
    ok_flow_2 c⇩1 c⇩2 c⇩2' s⇩1 t⇩1 t⇩2 f f' vs⇩1 vs⇩1' vs⇩2 vs⇩2' ws⇩1 ws⇩1' ws⇩2 ws⇩2' cs"

definition correct :: "com ⇒ state set ⇒ vname set ⇒ bool" where
"correct c A X ≡
  ∀s ∈ Univ A (⊆ state ∩ X). ∀c⇩1 c⇩2 s⇩1 s⇩2 f vs vs⇩1 vs⇩2 ws ws⇩1 ws⇩2 cfs.
    (c, s, f, vs, ws) →* (c⇩1, s⇩1, f, vs⇩1, ws⇩1) ∧
    (c⇩1, s⇩1, f, vs⇩1, ws⇩1) →*{cfs} (c⇩2, s⇩2, f, vs⇩2, ws⇩2) ⟶
      ok_flow c⇩1 c⇩2 s⇩1 s⇩2 f vs⇩1 vs⇩2 ws⇩1 ws⇩2 (flow cfs)"


abbreviation noninterf_set :: "state set ⇒ vname set ⇒ vname set ⇒ bool"
  (‹(_: _ ↝| _)› [51, 51, 51] 50) where
"A: X ↝| Y ≡ ∀y ∈ Y. ∃s ∈ A. ∃x ∈ X. ¬ s: dom x ↝ dom y"

abbreviation ok_flow_aux_1 where
"ok_flow_aux_1 c⇩1 c⇩2 c⇩2' s⇩1 t⇩1 t⇩2 f f' vs⇩1 vs⇩1' vs⇩2 vs⇩2' ws⇩1' ws⇩2' cs ≡
  ∀S ⊆ {x. s⇩1 = t⇩1 (⊆ sources_aux cs vs⇩1 s⇩1 f x)}.
    S ≠ {} ⟶
    f = f' (⊆ vs⇩1, vs⇩1', ⋃ {tags_aux cs vs⇩1 s⇩1 f x | x. x ∈ S}) ⟶
      (c⇩1, t⇩1, f', vs⇩1', ws⇩1') →* (c⇩2', t⇩2, f', vs⇩2', ws⇩2') ∧
      (c⇩2 = SKIP) = (c⇩2' = SKIP) ∧
      map fst [p←drop (length vs⇩1) vs⇩2. fst p ∈ S] =
        map fst [p←drop (length vs⇩1') vs⇩2'. fst p ∈ S]"

abbreviation ok_flow_aux_2 where
"ok_flow_aux_2 s⇩1 s⇩2 t⇩1 t⇩2 f f' vs⇩1 vs⇩1' cs ≡
  ∀S ⊆ {x. s⇩1 = t⇩1 (⊆ sources cs vs⇩1 s⇩1 f x)}.
    S ≠ {} ⟶
    f = f' (⊆ vs⇩1, vs⇩1', ⋃ {tags cs vs⇩1 s⇩1 f x | x. x ∈ S}) ⟶
      s⇩2 = t⇩2 (⊆ S)"

abbreviation ok_flow_aux_3 where
"ok_flow_aux_3 s⇩1 t⇩1 f f' vs⇩1 vs⇩1' ws⇩1 ws⇩1' ws⇩2 ws⇩2' cs ≡
  ∀S ⊆ {x. s⇩1 = t⇩1 (⊆ sources_out cs vs⇩1 s⇩1 f x)}.
    S ≠ {} ⟶
    f = f' (⊆ vs⇩1, vs⇩1', ⋃ {tags_out cs vs⇩1 s⇩1 f x | x. x ∈ S}) ⟶
      [p←drop (length ws⇩1) ws⇩2. fst p ∈ S] =
        [p←drop (length ws⇩1') ws⇩2'. fst p ∈ S]"

abbreviation ok_flow_aux :: "config set ⇒ com ⇒ com ⇒ state ⇒ state ⇒
  stream ⇒ inputs ⇒ inputs ⇒ outputs ⇒ outputs ⇒ flow ⇒ bool"
where
"ok_flow_aux U c⇩1 c⇩2 s⇩1 s⇩2 f vs⇩1 vs⇩2 ws⇩1 ws⇩2 cs ≡
  (∀t⇩1 f' vs⇩1' ws⇩1'. ∃c⇩2' t⇩2 vs⇩2' ws⇩2'.
    ok_flow_aux_1 c⇩1 c⇩2 c⇩2' s⇩1 t⇩1 t⇩2 f f' vs⇩1 vs⇩1' vs⇩2 vs⇩2' ws⇩1' ws⇩2' cs ∧
    ok_flow_aux_2 s⇩1 s⇩2 t⇩1 t⇩2 f f' vs⇩1 vs⇩1' cs ∧
    ok_flow_aux_3 s⇩1 t⇩1 f f' vs⇩1 vs⇩1' ws⇩1 ws⇩1' ws⇩2 ws⇩2' cs) ∧
  (∀Y. (∃(A, X) ∈ U. A: X ↝| Y) ⟶ no_upd cs Y)"

text ‹
\null

In addition to the equations handling the further constructs of the considered extension of language
IMP, the auxiliary recursive function @{text ctyping1_aux} used to define the idempotent type system
@{text ctyping1} differs from its counterpart used in my previous paper \<^cite>‹"Noce24"› also in that
it records any update of a state variable using a pair of type @{typ "vname × val option"}, where
the first component is the state variable being updated, and the latter one matches @{term "Some i"}
or @{const None} depending on whether its new value can be evaluated to an integer @{text i} at
compile time or not.

Apart from the aforesaid type change, the equations for the constructs included in the original
language IMP are the same as in my previous paper \<^cite>‹"Noce24"›, whereas the equations for the
additional constructs of the considered language extension are as follows.

  ▪ The equation for an input instruction @{text "IN x"}, like the one handling assignments, records
the update of variable @{text x} just in case it is a state variable (as otherwise its update cannot
change the applying interference relation). If so, its update is recorded with @{term "(x, None)"},
since input values cannot be evaluated at compile time.

  ▪ The equation for an output instruction @{text "OUT x"} does not record any update, since output
instructions leave the program state unchanged.

  ▪ The equation for a nondeterministic choice @{term "c⇩1 OR c⇩2"} sets the returned value to
@{text "⊢ c⇩1 ⊔ ⊢ c⇩2"}, in the same way as the equation for a conditional statement
@{term "IF b THEN c⇩1 ELSE c⇩2"} whose boolean condition @{text b} cannot be evaluated at compile time.

As in my previous paper \<^cite>‹"Noce24"›, the @{typ "state set"} returned by @{text ctyping1} is
defined so that any \emph{indeterminate} state variable (namely, any state variable @{text x} with a
latest recorded update @{term "(x, None)"}) may take an arbitrary value. Of course, a real-world
implementation of this type system would not need to actually return a distinct state for any such
value, but rather just to mark any indeterminate state variable in each returned state with some
special value standing for \emph{arbitrary}.

\null
›

primrec btyping1 :: "bexp ⇒ bool option" (‹(⊢ _)› [51] 55) where

"⊢ Bc v = Some v" |

"⊢ Not b = (case ⊢ b of
  Some v ⇒ Some (¬ v) | _ ⇒ None)" |

"⊢ And b⇩1 b⇩2 = (case (⊢ b⇩1, ⊢ b⇩2) of
  (Some v⇩1, Some v⇩2) ⇒ Some (v⇩1 ∧ v⇩2) | _ ⇒ None)" |

"⊢ Less a⇩1 a⇩2 = (if avars a⇩1 ∪ avars a⇩2 = {}
  then Some (aval a⇩1 (λx. 0) < aval a⇩2 (λx. 0)) else None)"


inductive_set ctyping1_merge_aux :: "state_upd list set ⇒
  state_upd list set ⇒ (state_upd list × bool) list set"
  (infix ‹⨆› 55) for A and B where

 "xs ∈ A ⟹ [(xs, True)] ∈ A ⨆ B" |

 "ys ∈ B ⟹ [(ys, False)] ∈ A ⨆ B" |

 "⟦ws ∈ A ⨆ B; ¬ snd (hd ws); xs ∈ A; (xs, True) ∉ set ws⟧ ⟹
    (xs, True) # ws ∈ A ⨆ B" |

 "⟦ws ∈ A ⨆ B; snd (hd ws); ys ∈ B; (ys, False) ∉ set ws⟧ ⟹
    (ys, False) # ws ∈ A ⨆ B"

declare ctyping1_merge_aux.intros [intro]

definition ctyping1_append ::
 "state_upd list set ⇒ state_upd list set ⇒ state_upd list set"
  (infixl ‹@› 55) where
"A @ B ≡ {xs @ ys | xs ys. xs ∈ A ∧ ys ∈ B}"

definition ctyping1_merge ::
 "state_upd list set ⇒ state_upd list set ⇒ state_upd list set"
  (infixl ‹⊔› 55) where
"A ⊔ B ≡ {concat (map fst ws) | ws. ws ∈ A ⨆ B}"

definition ctyping1_merge_append ::
 "state_upd list set ⇒ state_upd list set ⇒ state_upd list set"
  (infixl ‹⊔⇩@› 55) where
"A ⊔⇩@ B ≡ (if card B = Suc 0 then A else A ⊔ B) @ B"


primrec ctyping1_aux :: "com ⇒ state_upd list set"
  (‹(⊢ _)› [51] 60) where

"⊢ SKIP = {[]}" |

"⊢ x ::= a = (if x ∈ state
  then {[(x, if avars a = {} then Some (aval a (λx. 0)) else None)]}
  else {[]})" |

"⊢ IN x = (if x ∈ state then {[(x, None)]} else {[]})" |

"⊢ OUT x = {[]}" |

"⊢ c⇩1;; c⇩2 = ⊢ c⇩1 ⊔⇩@ ⊢ c⇩2" |

"⊢ c⇩1 OR c⇩2 = ⊢ c⇩1 ⊔ ⊢ c⇩2" |

"⊢ IF b THEN c⇩1 ELSE c⇩2 = (let f = ⊢ b in
  (if f ∈ {Some True, None} then ⊢ c⇩1 else {}) ⊔
  (if f ∈ {Some False, None} then ⊢ c⇩2 else {}))" |

"⊢ WHILE b DO c = (let f = ⊢ b in
  (if f ∈ {Some False, None} then {[]} else {}) ∪
  (if f ∈ {Some True, None} then ⊢ c else {}))"

definition ctyping1 :: "com ⇒ state set ⇒ vname set ⇒ config"
  (‹(⊢ _ '(⊆ _, _'))› [51] 55) where
"⊢ c (⊆ A, X) ≡ let F = {λx. [y←ys. fst y = x] | ys. ys ∈ ⊢ c} in
  ({λx. if f x = []
     then s x else case snd (last (f x)) of None ⇒ t x | Some i ⇒ i |
       f s t. f ∈ F ∧ s ∈ A},
   Univ?? A {x. ∀f ∈ F. if f x = []
     then x ∈ X else snd (last (f x)) ≠ None})"

text ‹
\null

Finally, in the recursive definition of the main type system @{text ctyping2}, the equations dealing
with the constructs included in the original language IMP are the same as in my previous paper
\<^cite>‹"Noce24"›, whereas the equations for the additional constructs of the considered language
extension are as follows.

  ▪ The equation for an input instruction @{text "IN x"} sets the returned value to a \emph{pass}
verdict @{term "Some (B, Y)"} just in case each set of variables in the current scope is allowed to
affect variable @{text x} in the associated set of program states. If so, then the sets @{text B}
and @{text Y} are computed in the same way as with an assignment whose right-hand expression cannot
be evaluated at compile time, since input values cannot be evaluated at compile time, too.

  ▪ The equation for an output instruction @{text "OUT x"} sets the returned value to a \emph{pass}
verdict @{term "Some (B, Y)"} just in case each set of variables in the current scope is allowed to
affect variable @{text x} in the associated set of program states. If so, then the sets @{text B}
and @{text Y} are computed in the same way as with a @{const SKIP} command, as output instructions
leave the program state unchanged, too.

  ▪ The equation for a nondeterministic choice @{term "c⇩1 OR c⇩2"} sets the returned value to a
\emph{pass} verdict @{term "Some (B, Y)"} just in case \emph{pass} verdicts are returned for both
branches. If so, then the sets @{text B} and @{text Y} are computed in the same way as with a
conditional statement @{term "IF b THEN c⇩1 ELSE c⇩2"} whose boolean condition @{text b} cannot be
evaluated at compile time.

\null
›

primrec btyping2_aux :: "bexp ⇒ state set ⇒ vname set ⇒ state set option"
  (‹(⊫ _ '(⊆ _, _'))› [51] 55) where

"⊫ Bc v (⊆ A, _) = Some (if v then A else {})" |

"⊫ Not b (⊆ A, X) = (case ⊫ b (⊆ A, X) of
  Some B ⇒ Some (A - B) | _ ⇒ None)" |

"⊫ And b⇩1 b⇩2 (⊆ A, X) = (case (⊫ b⇩1 (⊆ A, X), ⊫ b⇩2 (⊆ A, X)) of
  (Some B⇩1, Some B⇩2) ⇒ Some (B⇩1 ∩ B⇩2) | _ ⇒ None)" |

"⊫ Less a⇩1 a⇩2 (⊆ A, X) = (if avars a⇩1 ∪ avars a⇩2 ⊆ state ∩ X
  then Some {s. s ∈ A ∧ aval a⇩1 s < aval a⇩2 s} else None)"

definition btyping2 ::
 "bexp ⇒ state set ⇒ vname set ⇒ state set × state set"
  (‹(⊨ _ '(⊆ _, _'))› [51] 55) where
"⊨ b (⊆ A, X) ≡ case ⊫ b (⊆ A, X) of
  Some A' ⇒ (A', A - A') | _ ⇒ (A, A)"


abbreviation interf_set :: "state set ⇒ vname set ⇒ vname set ⇒ bool"
  (‹(_: _ ↝ _)› [51, 51, 51] 50) where
"A: X ↝ Y ≡ ∀s ∈ A. ∀x ∈ X. ∀y ∈ Y. s: dom x ↝ dom y"

abbreviation atyping :: "bool ⇒ aexp ⇒ vname set ⇒ bool"
  (‹(_ ⊨ _ '(⊆ _'))› [51, 51] 50) where
"v ⊨ a (⊆ X) ≡ avars a = {} ∨ avars a ⊆ state ∩ X ∧ v"

definition univ_states_if :: "state set ⇒ vname set ⇒ state set"
  (‹(Univ? _ _)› [51, 75] 75) where
"Univ? A X ≡ if state ⊆ X then A else Univ A (⊆ {})"


fun ctyping2 :: "scope ⇒ com ⇒ state set ⇒ vname set ⇒ config option"
  (‹(_ ⊨ _ '(⊆ _, _'))› [51, 51] 55) where

"_ ⊨ SKIP (⊆ A, X) = Some (A, Univ?? A X)" |

"(U, v) ⊨ x ::= a (⊆ A, X) =
 (if ∀(B, Y) ∈ insert (Univ? A X, avars a) U. B: Y ↝ {x}
  then Some (if x ∈ state ∧ A ≠ {}
    then if v ⊨ a (⊆ X)
      then ({s(x := aval a s) | s. s ∈ A}, insert x X) else (A, X - {x})
    else (A, Univ?? A X))
  else None)" |

"(U, v) ⊨ IN x (⊆ A, X) =
 (if ∀(B, Y) ∈ U. B: Y ↝ {x}
  then Some (if x ∈ state ∧ A ≠ {}
    then (A, X - {x}) else (A, Univ?? A X))
  else None)" |

"(U, v) ⊨ OUT x (⊆ A, X) =
 (if ∀(B, Y) ∈ U. B: Y ↝ {x}
  then Some (A, Univ?? A X)
  else None)" |

"(U, v) ⊨ c⇩1;; c⇩2 (⊆ A, X) =
 (case (U, v) ⊨ c⇩1 (⊆ A, X) of
    Some (B, Y) ⇒ (U, v) ⊨ c⇩2 (⊆ B, Y) | _ ⇒ None)" |

"(U, v) ⊨ c⇩1 OR c⇩2 (⊆ A, X) =
 (case ((U, v) ⊨ c⇩1 (⊆ A, X), (U, v) ⊨ c⇩2 (⊆ A, X)) of
    (Some (C⇩1, Y⇩1), Some (C⇩2, Y⇩2)) ⇒ Some (C⇩1 ∪ C⇩2, Y⇩1 ∩ Y⇩2) |
    _ ⇒ None)" |

"(U, v) ⊨ IF b THEN c⇩1 ELSE c⇩2 (⊆ A, X) =
 (case (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) of (U', B⇩1, B⇩2) ⇒
    case ((U', v) ⊨ c⇩1 (⊆ B⇩1, X), (U', v) ⊨ c⇩2 (⊆ B⇩2, X)) of
      (Some (C⇩1, Y⇩1), Some (C⇩2, Y⇩2)) ⇒ Some (C⇩1 ∪ C⇩2, Y⇩1 ∩ Y⇩2) |
      _ ⇒ None)" |

"(U, v) ⊨ WHILE b DO c (⊆ A, X) = (case ⊨ b (⊆ A, X) of (B⇩1, B⇩2) ⇒
  case ⊢ c (⊆ B⇩1, X) of (C, Y) ⇒ case ⊨ b (⊆ C, Y) of (B⇩1', B⇩2') ⇒
    if ∀(B, W) ∈ insert (Univ? A X ∪ Univ? C Y, bvars b) U. B: W ↝ UNIV
    then case (({}, False) ⊨ c (⊆ B⇩1, X), ({}, False) ⊨ c (⊆ B⇩1', Y)) of
      (Some _, Some _) ⇒ Some (B⇩2 ∪ B⇩2', Univ?? B⇩2 X ∩ Y) |
      _ ⇒ None
    else None)"

end

end