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 [pvs. fst p = x] + n) =
  f' x (length [pvs'. 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 a1 a2) = avars a1  avars a2"

primrec bvars :: "bexp  vname set" where
"bvars (Bc v) = {}" |
"bvars (Not b) = bvars b" |
"bvars (And b1 b2) = bvars b1  bvars b2" |
"bvars (Less a1 a2) = avars a1  avars a2"

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 [pvs. fst p = x] + length [ccs. 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 [pvs. fst p = x] + length [ccs. 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 "csn+1"},
@{term "csn @ [cn]"}, ..., @{term "cs1 @ [c1]"} of @{text cs} and a sequence of variables
@{text "yn+1"}, ..., @{text y1}, where $n \ge 1$, @{text "csn+1 = cs"}, @{text "yn+1 = x"}, and
@{text "y1 = y"}, satisfying the following conditions.

   For each positive integer $i \le n$, the instruction @{text "ci"} is an assignment
@{text "yi+1 ::= ai"} such that:

     @{prop "yi  avars ai"},

     @{text "run_flow csi vs s f: dom yi ↝ dom yi+1"}, and

     the right sublist of @{text "csi+1"} complementary to @{term "csi @ [ci]"} does not comprise
any assignment or input instruction setting variable @{text "yi+1"} (as the assignment @{text "ci"}
would otherwise be irrelevant),

  or else an observation @{term "Xi"} such that:

     @{prop "yi  Xi"} and

     @{text "run_flow csi vs s f: dom yi ↝ dom yi+1"}.

   The program execution flow @{text "cs1"} 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 csi vs s f xi"}, where @{term "csi @ [ci]"} is any left sublist
of @{text cs} such that the instruction @{text "ci"} is an output instruction @{text "OUT x"}, in
which case @{text "xi = x"}, or else an observation @{term "Xi"} such that:

   @{prop "xi  Xi"} and

   @{text "run_flow csi vs s f: dom xi ↝ 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 "csn+1"}, @{term "csn @ [cn]"}, ...,
@{term "cs1 @ [c1]"} of @{text cs} and a sequence of variables @{text "yn+1"}, ..., @{text y1}, where
$n \ge 1$, @{text "csn+1 = cs"}, @{text "yn+1 = x"}, @{text "y1 = 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 "ci"} is an
assignment @{text "yi+1 ::= ai"} such that:

     @{prop "yi  avars ai"},

     @{text "run_flow csi vs s f: dom yi ↝ dom yi+1"}, and

     the right sublist of @{text "csi+1"} complementary to @{term "csi @ [ci]"} does not comprise
any assignment or input instruction setting variable @{text "yi+1"} (as the assignment @{text "ci"}
would otherwise be irrelevant),

  or else an observation @{term "Xi"} such that:

     @{prop "yi  Xi"} and

     @{text "run_flow csi vs s f: dom yi ↝ dom yi+1"}.

   The instruction @{text "c1"} is the @{text m}-th input instruction @{text "IN y"} within flow
@{text cs}.

   The right sublist of @{text "cs2"} complementary to @{term "cs1 @ [c1]"} does not comprise any
assignment or input instruction setting variable @{text y} (as the input instruction @{text "c1"}
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 [ccs. 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 csi vs s f xi"}, where @{term "csi @ [ci]"} is any left sublist of @{text cs} such
that the instruction @{text "ci"} is an output instruction @{text "OUT x"}, in which case
@{text "xi = x"}, or else an observation @{term "Xi"} such that:

   @{prop "xi  Xi"} and

   @{text "run_flow csi vs s f: dom xi ↝ 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 "c1"} and a program execution stage @{text "(s1, f, vs1, ws1)"}, and

   the command @{text c1} and the program execution stage @{text "(s1, f, vs1, ws1)"} into a command
@{text "c2"} and a program execution stage @{text "(s2, f, vs2, ws2)"}.

Furthermore, let:

   @{text cs} be the program execution flow leading from @{text "(c1, s1, f, vs1, ws1)"} to
@{text "(c2, s2, f, vs2, ws2)"}, and

   @{text "(t1, f', vs1', ws1')"} 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 "t1"} agrees with @{text "s1"} on the value of each variable contained in
@{term "sources cs vs1 s1 f x"}.

   For each variable @{text x} contained in @{text S}, and each tag @{text "(y, n)"} contained in
@{term "tags cs vs1 s1 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 vs1'} and @{text "vs1"}, respectively.

Then, the information flow is correct only if the small-step semantics turns the command
@{text "c1"} and the program execution stage @{text "(t1, f', vs1', ws1')"} into a command
@{text "c2'"} and a program execution stage @{text "(t2, f', vs2', ws2')"} satisfying the following
correctness conditions.

   @{prop "c2' = SKIP"} just in case @{prop "c2 = 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 "t2"} and @{text "s2"} 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 c1 c2 c2' s1 s2 t1 t2 f f' vs1 vs1' vs2 vs2' ws1' ws2' cs 
  S  {x. s1 = t1 (⊆ sources cs vs1 s1 f x)}.
    S  {} 
    f = f' (⊆ vs1, vs1',  {tags cs vs1 s1 f x | x. x  S}) 
      (c1, t1, f', vs1', ws1') →* (c2', t2, f', vs2', ws2') 
      (c2 = SKIP) = (c2' = SKIP) 
      map fst [pdrop (length vs1) vs2. fst p  S] =
        map fst [pdrop (length vs1') vs2'. fst p  S] 
      s2 = t2 (⊆ S)"

abbreviation ok_flow_2 where
"ok_flow_2 c1 c2 c2' s1 t1 t2 f f' vs1 vs1' vs2 vs2' ws1 ws1' ws2 ws2' cs 
  S  {x. s1 = t1 (⊆ sources_out cs vs1 s1 f x)}.
    S  {} 
    f = f' (⊆ vs1, vs1',  {tags_out cs vs1 s1 f x | x. x  S}) 
      (c1, t1, f', vs1', ws1') →* (c2', t2, f', vs2', ws2') 
      (c2 = SKIP) = (c2' = SKIP) 
      map fst [pdrop (length vs1) vs2. fst p  S] =
        map fst [pdrop (length vs1') vs2'. fst p  S] 
      [pdrop (length ws1) ws2. fst p  S] =
        [pdrop (length ws1') ws2'. fst p  S]"

abbreviation ok_flow where
"ok_flow c1 c2 s1 s2 f vs1 vs2 ws1 ws2 cs 
  t1 f' vs1' ws1'. c2' t2 vs2' ws2'.
    ok_flow_1 c1 c2 c2' s1 s2 t1 t2 f f' vs1 vs1' vs2 vs2' ws1' ws2' cs 
    ok_flow_2 c1 c2 c2' s1 t1 t2 f f' vs1 vs1' vs2 vs2' ws1 ws1' ws2 ws2' cs"

definition correct :: "com  state set  vname set  bool" where
"correct c A X 
  s  Univ A (⊆ state  X). c1 c2 s1 s2 f vs vs1 vs2 ws ws1 ws2 cfs.
    (c, s, f, vs, ws) →* (c1, s1, f, vs1, ws1) 
    (c1, s1, f, vs1, ws1) →*{cfs} (c2, s2, f, vs2, ws2) 
      ok_flow c1 c2 s1 s2 f vs1 vs2 ws1 ws2 (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 c1 c2 c2' s1 t1 t2 f f' vs1 vs1' vs2 vs2' ws1' ws2' cs 
  S  {x. s1 = t1 (⊆ sources_aux cs vs1 s1 f x)}.
    S  {} 
    f = f' (⊆ vs1, vs1',  {tags_aux cs vs1 s1 f x | x. x  S}) 
      (c1, t1, f', vs1', ws1') →* (c2', t2, f', vs2', ws2') 
      (c2 = SKIP) = (c2' = SKIP) 
      map fst [pdrop (length vs1) vs2. fst p  S] =
        map fst [pdrop (length vs1') vs2'. fst p  S]"

abbreviation ok_flow_aux_2 where
"ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' cs 
  S  {x. s1 = t1 (⊆ sources cs vs1 s1 f x)}.
    S  {} 
    f = f' (⊆ vs1, vs1',  {tags cs vs1 s1 f x | x. x  S}) 
      s2 = t2 (⊆ S)"

abbreviation ok_flow_aux_3 where
"ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' cs 
  S  {x. s1 = t1 (⊆ sources_out cs vs1 s1 f x)}.
    S  {} 
    f = f' (⊆ vs1, vs1',  {tags_out cs vs1 s1 f x | x. x  S}) 
      [pdrop (length ws1) ws2. fst p  S] =
        [pdrop (length ws1') ws2'. 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 c1 c2 s1 s2 f vs1 vs2 ws1 ws2 cs 
  (t1 f' vs1' ws1'. c2' t2 vs2' ws2'.
    ok_flow_aux_1 c1 c2 c2' s1 t1 t2 f f' vs1 vs1' vs2 vs2' ws1' ws2' cs 
    ok_flow_aux_2 s1 s2 t1 t2 f f' vs1 vs1' cs 
    ok_flow_aux_3 s1 t1 f f' vs1 vs1' ws1 ws1' ws2 ws2' 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 "c1 OR c2"} sets the returned value to
@{text "⊢ c1 ⊔ ⊢ c2"}, in the same way as the equation for a conditional statement
@{term "IF b THEN c1 ELSE c2"} 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 b1 b2 = (case ( b1,  b2) of
  (Some v1, Some v2)  Some (v1  v2) | _  None)" |

" Less a1 a2 = (if avars a1  avars a2 = {}
  then Some (aval a1 (λx. 0) < aval a2 (λ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 = {[]}" |

" c1;; c2 =  c1 @  c2" |

" c1 OR c2 =  c1   c2" |

" IF b THEN c1 ELSE c2 = (let f =  b in
  (if f  {Some True, None} then  c1 else {}) 
  (if f  {Some False, None} then  c2 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. [yys. 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 "c1 OR c2"} 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 c1 ELSE c2"} 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 b1 b2 (⊆ A, X) = (case ( b1 (⊆ A, X),  b2 (⊆ A, X)) of
  (Some B1, Some B2)  Some (B1  B2) | _  None)" |

" Less a1 a2 (⊆ A, X) = (if avars a1  avars a2  state  X
  then Some {s. s  A  aval a1 s < aval a2 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)  c1;; c2 (⊆ A, X) =
 (case (U, v)  c1 (⊆ A, X) of
    Some (B, Y)  (U, v)  c2 (⊆ B, Y) | _  None)" |

"(U, v)  c1 OR c2 (⊆ A, X) =
 (case ((U, v)  c1 (⊆ A, X), (U, v)  c2 (⊆ A, X)) of
    (Some (C1, Y1), Some (C2, Y2))  Some (C1  C2, Y1  Y2) |
    _  None)" |

"(U, v)  IF b THEN c1 ELSE c2 (⊆ A, X) =
 (case (insert (Univ? A X, bvars b) U,  b (⊆ A, X)) of (U', B1, B2) 
    case ((U', v)  c1 (⊆ B1, X), (U', v)  c2 (⊆ B2, X)) of
      (Some (C1, Y1), Some (C2, Y2))  Some (C1  C2, Y1  Y2) |
      _  None)" |

"(U, v)  WHILE b DO c (⊆ A, X) = (case  b (⊆ A, X) of (B1, B2) 
  case  c (⊆ B1, X) of (C, Y)  case  b (⊆ C, Y) of (B1', B2') 
    if (B, W)  insert (Univ? A X  Univ? C Y, bvars b) U. B: W  UNIV
    then case (({}, False)  c (⊆ B1, X), ({}, False)  c (⊆ B1', Y)) of
      (Some _, Some _)  Some (B2  B2', Univ?? B2 X  Y) |
      _  None
    else None)"

end

end