Theory Step_Basic

section "Basic Semantics"

theory Step_Basic
imports Language_Syntax
begin


text ‹This theory introduces a standard semantics for the commands defined›

subsection "Well-formed programs"
text ‹A well-formed program is a nonempty list of commands where the head of the list is the "Start" command›

type_synonym prog = "com list"

locale Prog = 
fixes prog :: prog
assumes (* well-formed programs begin with a "Start" command: *) 
wf_prog: "prog  []  hd prog = Start"
begin

text "This is the program counter signifying the end of the program:"
definition "endPC  length prog"

text "And some sanity checks for a well formed program..."

lemma lenth_prog_gt_0: "length prog > 0"
using wf_prog by auto

lemma lenth_prog_not_0: "length prog  0"
using wf_prog by auto

lemma endPC_gt_0: "endPC > 0"
unfolding endPC_def using lenth_prog_gt_0 by blast

lemma endPC_not_0: "endPC  0"
unfolding endPC_def using lenth_prog_not_0 by blast


lemma hd_prog_Start: "hd prog = Start" 
using wf_prog by auto

lemma prog_0: "prog ! 0 = Start"
by (metis hd_conv_nth wf_prog)

subsection "Basic Semantics of Commands"
text ‹The basic small step semantics of the language, parameterised by a fixed program. 
The semantics operate on input streams and memories which are consumed and updated while the program counter moves through the list of commands.
This emulates standard (and expected) execution of the commands defined. Since no speculation is captured in this basic semantics, the Fence command the same as SKIP›

inductive
stepB :: "config × val llist × val llist  config × val llist × val llist  bool" (infix →B 55)
where
Seq_Start_Skip_Fence: 
"pc < endPC  prog!pc  {Start, Skip, Fence}  
 (Config pc s, ibT, ibUT) →B (Config (Suc pc) s, ibT, ibUT)"
|
Assign:  
"pc < endPC  prog!pc = (x ::= a)  
 s = State (Vstore vs) avst h p  
 (Config pc s, ibT, ibUT) 
 →B 
 (Config (Suc pc) (State (Vstore (vs(x := aval a s))) avst h p), ibT, ibUT)" 
|
ArrAssign:  
"pc < endPC  prog!pc = (arr[index] ::= a)   
 v = aval index s  w = aval a s  
 0  v  v < int (array_bound arr avst) 
 l = array_loc arr (nat v) avst 
 s = State vst avst (Heap h) p
  
 (Config pc s, ibT, ibUT) 
 →B 
 (Config (Suc pc) (State vst avst (Heap (h(l := w))) p), ibT, ibUT)"
|
getTrustedInput: 
"pc < endPC  prog!pc = Input T x 
 (Config pc (State (Vstore vs) avst h p), LCons i ibT, ibUT) 
 →B 
 (Config (Suc pc) (State (Vstore (vs(x := i))) avst h p), ibT, ibUT)"
|
getUntrustedInput: 
"pc < endPC  prog!pc = Input U x 
 (Config pc (State (Vstore vs) avst h p), ibT, LCons i ibUT) 
 →B 
 (Config (Suc pc) (State (Vstore (vs(x := i))) avst h p), ibT, ibUT)"
|
Output: 
"pc < endPC  prog!pc = Output t aexp 
 (Config pc s, ibT, ibUT) 
 →B 
 (Config (Suc pc) s, ibT, ibUT)"
|
Jump: 
"pc < endPC  prog!pc = Jump pc1  
 (Config pc s, ibT, ibUT) →B (Config pc1 s, ibT, ibUT)" 
|
IfTrue: 
"pc < endPC  prog!pc = IfJump b pc1 pc2  
 bval b s  
 (Config pc s, ibT, ibUT) →B (Config pc1 s, ibT, ibUT)" 
|
IfFalse: 
"pc < endPC  prog!pc = IfJump b pc1 pc2  
 ¬ bval b s  
 (Config pc s, ibT, ibUT) →B (Config pc2 s, ibT, ibUT)" 
|
MaskTrue:  
"pc < endPC  prog!pc = (M x I b T a1 E a2 )  
 bval b s 
 s = State (Vstore vs) avst h p 
 (Config pc s, ibT, ibUT) 
 →B 
 (Config (Suc pc) (State (Vstore (vs(x := aval a1 s))) avst h p), ibT, ibUT)" 
|
MaskFalse:  
"pc < endPC  prog!pc = (M x I b T a1 E a2 ) 
 ¬bval b s 
 s = State (Vstore vs) avst h p 
 (Config pc s, ibT, ibUT) 
 →B 
 (Config (Suc pc) (State (Vstore (vs(x := aval a2 s))) avst h p), ibT, ibUT)" 

lemmas stepB_induct = stepB.induct[split_format(complete)]
(* thm stepB_induct *)

abbreviation
  stepsB :: "config × val llist × val llist  config × val llist × val llist  bool" (infix →B* 55)
  where "x →B* y == star stepB x y"

declare stepB.intros[simp,intro]
(*

*)

(* *)
subsection "State Transitions"
text ‹Useful lemmas regarding valid transitions of the semantics along with conditions for termination (finalB)›

definition "finalB = final stepB"
lemmas finalB_defs  = final_def finalB_def


lemma finalB_iff_aux:  
"pc < endPC  
 (x i a. prog!pc = (x[i] ::= a)  aval i s  0  
          aval i s < int (array_bound x (getAvstore s)))  
 (y. prog!pc = Input T y  ibT  LNil) 
 (y. prog!pc = Input U y  ibUT  LNil)
  
 (cfg'. (Config pc s, ibT, ibUT) →B cfg')"
apply (cases s) subgoal for vst avst h p 
apply(cases vst) apply(cases h) subgoal for vs hh apply clarsimp 
(* apply safe subgoal *)
apply (cases "prog!pc")
  subgoal by (auto elim: stepB.cases, blast)
  subgoal by (auto elim: stepB.cases, blast)
  subgoal for t apply(cases t)
     subgoal by(cases ibT, auto elim: stepB.cases, blast) 
     subgoal by(cases ibUT, auto elim: stepB.cases, blast) .
   subgoal for t apply(cases t) 
     subgoal by (auto elim: stepB.cases, blast)
     subgoal by (auto elim: stepB.cases, blast) .
  subgoal by (auto elim: stepB.cases, blast)
  subgoal by (auto elim: stepB.cases, blast)   
  subgoal by (auto elim: stepB.cases, blast)
  subgoal by (auto elim: stepB.cases, blast)
  subgoal by (auto elim: stepB.cases, blast)
  subgoal by (auto elim: stepB.cases,meson IfFalse IfTrue) . . .

lemma finalB_iff: 
"finalB (Config pc s, ibT, ibUT) 
 
 (pc  endPC 
  (x i a. prog!pc = (x[i] ::= a)  
       (¬ aval i s  0  ¬ aval i s < int (array_bound x (getAvstore s)))))  
  (y. prog!pc = Input T y  ibT = LNil)  
  (y. prog!pc = Input U y  ibUT = LNil)"
using finalB_iff_aux[of pc s ibT ibUT] unfolding finalB_def final_def 
using verit_comp_simplify1(3) by blast


(* *)

lemma stepB_determ:
"cfg_ib →B cfg_ib'  cfg_ib →B cfg_ib''  cfg_ib'' = cfg_ib'"
apply(induction arbitrary: cfg_ib'' rule: stepB.induct)
by (auto elim: stepB.cases)
 
definition nextB :: "config × val llist × val llist  config × val llist × val llist" where 
"nextB cfg_ib  SOME cfg'_ib'. cfg_ib →B cfg'_ib'"
 
lemma nextB_stepB: "¬ finalB cfg_ib  cfg_ib →B (nextB cfg_ib)"
unfolding nextB_def apply(rule someI_ex) 
unfolding finalB_def final_def by auto

lemma stepB_nextB: "cfg_ib →B cfg'_ib'  cfg'_ib' = nextB cfg_ib"
unfolding nextB_def apply(rule sym) apply(rule some_equality)
using stepB_determ by auto

lemma nextB_iff_stepB: "¬ finalB cfg_ib  nextB cfg_ib  = cfg'_ib'  cfg_ib →B cfg'_ib'"
using nextB_stepB stepB_nextB by blast

lemma stepB_iff_nextB: "cfg_ib →B cfg'_ib'  ¬ finalB cfg_ib  nextB cfg_ib  = cfg'_ib'"
by (metis finalB_def final_def stepB_nextB)

(* *)
subsubsection "Simplification Rules"
text ‹Sufficient conditions for a given command to "execute" transit to the next state›

lemma nextB_Start_Skip_Fence[simp]:  
"pc < endPC  prog!pc  {Start, Skip, Fence} 
 nextB (Config pc s, ibT, ibUT) = (Config (Suc pc) s, ibT, ibUT)"
by(intro stepB_nextB[THEN sym] stepB.intros)

lemma nextB_Assign[simp]:  
"pc < endPC  prog!pc = (x ::= a) 
 s = State (Vstore vs) avst h p  
 nextB (Config pc s, ibT, ibUT) 
 = 
 (Config (Suc pc) (State (Vstore (vs(x := aval a s))) avst h p), 
    ibT, ibUT)" 
by(intro stepB_nextB[THEN sym] stepB.intros)

lemma nextB_ArrAssign[simp]:  
"pc < endPC  prog!pc = (arr[index] ::= a) 
 ls' = readLocs a vst avst (Heap h)  
 v = aval index s  w = aval a s  
 0  v  v < int (array_bound arr avst)  
 l = array_loc arr (nat v) avst 
 s = State vst avst (Heap h) p 
  
 nextB (Config pc s, ibT, ibUT) 
 =
 (Config (Suc pc) (State vst avst (Heap (h(l := w))) p), ibT, ibUT)"
by(intro stepB_nextB[THEN sym] stepB.intros)

lemma nextB_getTrustedInput[simp]: 
"pc < endPC  prog!pc = (Input T x) 
 nextB (Config pc (State (Vstore vs) avst h p), LCons i ibT, ibUT) 
 = 
 (Config (Suc pc) (State (Vstore (vs(x := i))) avst h p), ibT, ibUT)"  
  by(intro stepB_nextB[THEN sym] stepB.intros)

lemma nextB_getUntrustedInput[simp]: 
"pc < endPC  prog!pc = (Input U x) 
 nextB (Config pc (State (Vstore vs) avst h p), ibT, LCons i ibUT) 
 = 
 (Config (Suc pc) (State (Vstore (vs(x := i))) avst h p), ibT, ibUT)"  
by(intro stepB_nextB[THEN sym] stepB.intros)

lemma nextB_getTrustedInput'[simp]: 
"pc < endPC  prog!pc = Input T x 
 ibT  LNil  
 nextB (Config pc (State (Vstore vs) avst h p), ibT, ibUT) 
 = 
 (Config (Suc pc) (State (Vstore (vs(x := lhd ibT))) avst h p), ltl ibT, ibUT)"  
  by(cases ibT, auto)

lemma nextB_getUntrustedInput'[simp]: 
"pc < endPC  prog!pc = Input U x 
 ibUT  LNil  
 nextB (Config pc (State (Vstore vs) avst h p), ibT, ibUT) 
 = 
 (Config (Suc pc) (State (Vstore (vs(x := lhd ibUT))) avst h p), ibT, ltl ibUT)"  
by(cases ibUT, auto)

lemma nextB_Output[simp]: 
"pc < endPC  prog!pc = Output t aexp 
 nextB (Config pc s, ibT, ibUT) 
 = 
 (Config (Suc pc) s, ibT, ibUT)"
by(intro stepB_nextB[THEN sym] stepB.intros)

lemma nextB_Jump[simp]:  
"pc < endPC  prog!pc = Jump pc1  
 nextB (Config pc s, ibT, ibUT) = (Config pc1 s, ibT, ibUT)" 
  by(intro stepB_nextB[THEN sym] stepB.intros, simp_all+)

lemma nextB_IfTrue[simp]:  
"pc < endPC  prog!pc = IfJump b pc1 pc2  
 bval b s  
 nextB (Config pc s, ibT, ibUT) = (Config pc1 s, ibT, ibUT)" 
by(intro stepB_nextB[THEN sym] stepB.intros)

lemma nextB_IfFalse[simp]:  
"pc < endPC  prog!pc = IfJump b pc1 pc2  
 ¬ bval b s  
 nextB (Config pc s, ibT, ibUT) = (Config pc2 s, ibT, ibUT)" 
by(intro stepB_nextB[THEN sym] stepB.intros)


lemma nextB_MaskTrue[simp]:  
"pc < endPC  prog!pc = (M x I b T a1 E a2)  
 bval b (State (Vstore vs) avst h p)  
 nextB (Config pc (State (Vstore vs) avst h p), ibT, ibUT) = 
       (Config (Suc pc) (State (Vstore (vs(x := aval a1 (State (Vstore vs) avst h p)))) avst h p), ibT, ibUT)" 
apply(intro stepB_nextB[THEN sym])
  using MaskTrue by simp

lemma nextB_MaskFalse[simp]:  
"pc < endPC  prog!pc = (M x I b T a1 E a2)  
 ¬bval b (State (Vstore vs) avst h p)  
 nextB (Config pc (State (Vstore vs) avst h p), ibT, ibUT) = 
       (Config (Suc pc) (State (Vstore (vs(x := aval a2 (State (Vstore vs) avst h p)))) avst h p), ibT, ibUT)" 
apply(intro stepB_nextB[THEN sym])
  using MaskFalse by simp
(* *)


lemma finalB_endPC: "pcOf cfg = endPC  finalB (cfg,ibT, ibUT)"
  by (metis finalB_iff config.collapse le_eq_less_or_eq)

lemma stepB_endPC: "pcOf cfg = endPC  ¬ (cfg, ibT, ibUT) →B (cfg', ibT',ibUT')"
  by (simp add: stepB_iff_nextB finalB_endPC)

lemma stepB_imp_le_endPC: assumes "(cfg, ibT, ibUT) →B (cfg', ibT',ibUT')"
  shows "pcOf cfg < endPC"
  using assms by(cases rule: stepB.cases, simp_all)

(* *)

lemma stebB_0: "(Config 0 s, ibT, ibUT) →B (Config 1 s, ibT, ibUT)"
using prog_0 by (simp add: endPC_gt_0)

subsubsection "Elimination Rules"
text "In the unwinding proofs of relative security it is often the case that two traces will progress in lockstep, when doing so we wish to preserve/update invariants of the current state. T
he following are some useful elimination rules to help simplify reasoning"
(*elims*)
lemma stepB_Seq_Start_Skip_FenceE:
  assumes (cfg, ibT, ibUT) →B (cfg', ibT',ibUT')
      and cfg = (Config pc (State (Vstore vs) avst h p)) 
      and cfg' = (Config pc' (State (Vstore vs') avst' h' p'))
      and prog!pc  {Start, Skip, Fence}
    shows vs' = vs  ibT = ibT'  ibUT = ibUT'  
           pc' = Suc pc  avst' = avst  h' = h 
           p' = p
  using assms apply (cases "(cfg, ibT, ibUT)" "(cfg', ibT',ibUT')" rule: stepB.cases)
  by auto

lemma stepB_AssignE:
  assumes (cfg, ibT, ibUT) →B (cfg', ibT',ibUT')
      and cfg = (Config pc (State (Vstore vs) avst h p)) 
      and cfg' = (Config pc' (State (Vstore vs') avst' h' p'))
      and prog!pc = (x ::= a)
    shows vs' = (vs(x := aval a (stateOf cfg))) 
           ibT = ibT'  ibUT = ibUT'  pc' = Suc pc 
           avst' = avst  h' = h  p' = p
  using assms apply (cases "(cfg, ibT, ibUT)" "(cfg', ibT',ibUT')" rule: stepB.cases)
  by auto

lemma stepB_getTrustedInputE:
  assumes (cfg, ibT, ibUT) →B (cfg', ibT',ibUT')
      and cfg = (Config pc (State (Vstore vs) avst h p)) 
      and cfg' = (Config pc' (State (Vstore vs') avst' h' p'))
      and prog!pc = Input T x
    shows vs' = (vs(x := lhd ibT)) 
           ibT' = ltl ibT  ibUT = ibUT'  pc' = Suc pc 
           avst' = avst  h' = h  p' = p
  using assms apply (cases "(cfg, ibT, ibUT)" "(cfg', ibT',ibUT')" rule: stepB.cases)
  by auto

lemma stepB_getUntrustedInputE:
  assumes (cfg, ibT, ibUT) →B (cfg', ibT',ibUT')
      and cfg = (Config pc (State (Vstore vs) avst h p)) 
      and cfg' = (Config pc' (State (Vstore vs') avst' h' p'))
      and prog!pc = Input U x
    shows vs' = (vs(x := lhd ibUT)) 
           ibT' = ibT  ibUT' = ltl ibUT  pc' = Suc pc 
           avst' = avst  h' = h  p' = p
  using assms apply (cases "(cfg, ibT, ibUT)" "(cfg', ibT',ibUT')" rule: stepB.cases)
  by auto

lemma stepB_OutputE:
  assumes (cfg, ibT, ibUT) →B (cfg', ibT',ibUT')
      and cfg = (Config pc (State (Vstore vs) avst h p)) 
      and cfg' = (Config pc' (State (Vstore vs') avst' h' p'))
      and prog!pc = Output t aexp
    shows vs' = vs  ibT' = ibT  ibUT' = ibUT  
           pc' = Suc pc  avst' = avst  h' = h  p' = p
  using assms apply (cases "(cfg, ibT, ibUT)" "(cfg', ibT',ibUT')" rule: stepB.cases)
  by auto

lemma stepB_JumpE:
  assumes (cfg, ibT, ibUT) →B (cfg', ibT',ibUT')
      and cfg = (Config pc (State (Vstore vs) avst h p)) 
      and cfg' = (Config pc' (State (Vstore vs') avst' h' p'))
      and prog!pc = Jump pc1
    shows vs' = vs  ibT' = ibT  ibUT' = ibUT  
           pc' = pc1  avst' = avst  h' = h  p' = p
  using assms apply (cases "(cfg, ibT, ibUT)" "(cfg', ibT',ibUT')" rule: stepB.cases)
  by auto

lemma stepB_IfTrueE:
  assumes (cfg, ibT, ibUT) →B (cfg', ibT',ibUT')
      and cfg = (Config pc (State (Vstore vs) avst h p)) 
      and cfg' = (Config pc' (State (Vstore vs') avst' h' p'))
      and prog!pc = IfJump b pc1 pc2 and bval b (stateOf cfg)
    shows vs' = vs  ibT' = ibT  ibUT' = ibUT  
           pc' = pc1  avst' = avst  h' = h  p' = p
  using assms apply (cases "(cfg, ibT, ibUT)" "(cfg', ibT',ibUT')" rule: stepB.cases)
  by auto 

lemma stepB_IfFalseE:
  assumes (cfg, ibT, ibUT) →B (cfg', ibT',ibUT')
      and cfg = (Config pc (State (Vstore vs) avst h p)) 
      and cfg' = (Config pc' (State (Vstore vs') avst' h' p'))
      and prog!pc = IfJump b pc1 pc2 and ¬bval b (stateOf cfg)
    shows vs' = vs  ibT' = ibT  ibUT' = ibUT  
           pc' = pc2  avst' = avst  h' = h  p' = p
  using assms apply (cases "(cfg, ibT, ibUT)" "(cfg', ibT',ibUT')" rule: stepB.cases)
  by auto 

end (* context Prog *)

subsection "Read locations"

text ‹For modeling Spectre-like vulnerabilities, we record memory reads (as in \cite{Cheang}),
i.e., accessed for reading during the execution. 
We let readLocs(pc,u) be the (possibly empty) set of locations 
that are read when executing the current command c - computed from all sub-expressions of the form a[e]. i.e. array reads.
For example, if c is the assignment "x = a [b[3]]", then readLocs returns two locations: counting from 0, the 3rd location of b and the b[3]'th location of a.›
(* the locations read by an arithmetic expression: *)
fun readLocsA :: "aexp  state  loc set" and 
readLocsB :: "bexp  state  loc set" where
"readLocsA (N n) s = {}" 
|
"readLocsA (V x) s = {}" 
|
"readLocsA (VA arr index) s = 
 insert (array_loc arr (nat (aval index s)) (getAvstore s)) 
        (readLocsA index s)"
|
"readLocsA (Plus a1 a2) s = readLocsA a1 s  readLocsA a2 s"
|
"readLocsA (Times a1 a2) s = readLocsA a1 s  readLocsA a2 s"
|
"readLocsA (Ite b a1 a2) s = readLocsB b s  readLocsA a1 s  readLocsA a2 s"
|
"readLocsA (Fun a b) s = {}"
|
"readLocsB (Bc c) s= {}" 
|
"readLocsB (Not b) s = readLocsB b s" 
|
"readLocsB (And b1 b2) s = readLocsB b1 s  readLocsB b2 s" 
|
"readLocsB (Less a1 a2) s = readLocsA a1 s  readLocsA a2 s" 

(* the locations read by a command: *)
fun readLocsC :: "com  state  loc set" where
"readLocsC (x ::= a) s = readLocsA a s"
|
"readLocsC (arr[index] ::= a) s = readLocsA a s"
|
"readLocsC (Output t a) s = readLocsA a s"
|
"readLocsC (IfJump b n1 n2) s = readLocsB b s"
|
"readLocsC (M x I b T a1 E a2) s = readLocsB b s  (if (bval b s) then readLocsA a1 s 
                                    else readLocsA a2 s) "
|
"readLocsC _ _ = {}"

context Prog
begin

(* the locations read by a configuration: *)
definition "readLocs cfg  readLocsC (prog!(pcOf cfg)) (stateOf cfg)"

end (* context Prog *)


end