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)" 

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) . . .

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 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 _ _ = {}"

context Prog
begin

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

end (* context Prog *)


end