Theory Step_Normal

section "Normal Semantics"

text ‹ This theory augments the basic semantics to include a set of read locations which is a simple representation of a cache›
text ‹The normal semantics is defined by a single rule which involves the basic semantics, extended to accumulate the read locations, which accounts for cache side-channels ›

theory Step_Normal
imports Step_Basic
begin


context Prog 
begin

fun stepN :: "config × val llist × val llist × loc set ⇒ config × val llist × val llist × loc set ⇒ bool" (infix "→N" 55)
where
"(cfg,ibT,ibUT,ls) →N (cfg',ibT',ibUT',ls') =
 ((cfg,ibT,ibUT) →B (cfg',ibT',ibUT') ∧ ls' = ls ∪ readLocs cfg)"

abbreviation
  stepsN :: "config × val llist × val llist × loc set ⇒ config × val llist × val llist × loc set ⇒ bool" (infix "→N*" 55)
  where "x →N* y == star stepN x y"


(* *)

definition "finalN = final stepN"
lemmas finalN_defs  = final_def finalN_def

lemma finalN_iff_finalB[simp]: 
"finalN (cfg, ibT, ibUT, ls) ⟷ finalB (cfg, ibT, ibUT)"
unfolding finalN_def finalB_def final_def by auto

(* *)

subsection "State Transitions"
fun nextN :: "config × val llist × val llist × loc set ⇒ config × val llist × val llist × loc set" where 
"nextN (cfg, ibT, ibUT, ls) = (case nextB (cfg,ibT,ibUT) of (cfg',ibT',ibUT') ⇒ (cfg',ibT',ibUT',ls ∪ readLocs cfg))"
 
lemma nextN_stepN: "¬ finalN cfg_ib_ls ⟹ cfg_ib_ls →N (nextN cfg_ib_ls)"
apply(cases cfg_ib_ls) 
  using Prog.stepB_nextB Prog_axioms finalN_def 
        final_def nextN.simps old.prod.case stepN.elims(2) 
  by force

lemma stepN_nextN: "cfg_ib_ls →N cfg'_ib'_ls' ⟹ cfg'_ib'_ls' = nextN cfg_ib_ls"
apply(cases cfg_ib_ls) apply(cases cfg'_ib'_ls') 
using Prog.stepB_nextB Prog_axioms by auto

lemma nextN_iff_stepN: 
"¬ finalN cfg_ib_ls ⟹ nextN cfg_ib_ls  = cfg'_ib'_ls' ⟷ cfg_ib_ls →N cfg'_ib'_ls'"
using nextN_stepN stepN_nextN by blast

lemma stepN_iff_nextN: "cfg_ib_ls →N cfg'_ib'_ls' ⟷ ¬ finalN cfg_ib_ls ∧ nextN cfg_ib_ls  = cfg'_ib'_ls'"
by (metis finalN_def final_def stepN_nextN)

(* *)

lemma finalN_endPC: "pcOf cfg = endPC ⟹ finalN (cfg,ibT,ibUT)"
  by (metis finalN_iff_finalB finalB_endPC old.prod.exhaust)

lemma stepN_endPC: "pcOf cfg = endPC ⟹ ¬ (cfg,ibT,ibUT) →N (cfg',ibT',ibUT')"
  by (simp add: finalN_endPC stepN_iff_nextN) 

lemma stebN_0: "(Config 0 s, ibT, ibUT, ls) →N (Config 1 s, ibT, ibUT, ls)"
using prog_0 One_nat_def stebB_0 by (auto simp: readLocs_def)


lemma finalB_eq_finalN:"finalB (cfg, ibT,ibUT) ⟷ (∀ls. finalN (cfg, ibT,ibUT, ls))"
  unfolding finalN_defs finalB_def
  apply standard by auto


subsection "Elimination Rules"
(*step2 elims*)
lemma stepN_Assign2E:
  assumes ‹(cfg1, ibT1,ibUT1, ls1) →N (cfg1', ibT1',ibUT1', ls1')› 
      and ‹(cfg2, ibT2,ibUT2, ls2) →N (cfg2', ibT2',ibUT2', ls2')›
      and ‹cfg1 = (Config pc1 (State (Vstore vs1) avst1 h1 p1))› and ‹cfg1' = (Config pc1' (State (Vstore vs1') avst1' h1' p1'))›
      and ‹cfg2 = (Config pc2 (State (Vstore vs2) avst2 h2 p2))› and ‹cfg2' = (Config pc2' (State (Vstore vs2') avst2' h2' p2'))›
      and ‹prog!pc1 = (x ::= a)› and ‹pcOf cfg1 = pcOf cfg2› 
    shows ‹vs1' = (vs1(x := aval a (stateOf cfg1))) ∧ ibT1 = ibT1' ∧ ibUT1 = ibUT1' ∧
           vs2' = (vs2(x := aval a (stateOf cfg2))) ∧ ibT2 = ibT2' ∧ ibUT2 = ibUT2' ∧
           pc1' = Suc pc1 ∧ pc2' = Suc pc2 ∧ ls2' = ls2 ∪ readLocs cfg2 ∧
           avst1' = avst1 ∧ avst2' = avst2 ∧ ls1' = ls1 ∪ readLocs cfg1›
  using assms apply clarsimp
  apply (drule stepB_AssignE[of _ _ _ _ _ _ pc1 vs1 avst1 h1 p1
                                pc1' vs1' avst1' h1' p1' x a], clarify+)
  apply (drule stepB_AssignE[of _ _ _ _ _ _ pc2 vs2 avst2 h2 p2
                                pc2' vs2' avst2' h2' p2' x a], clarify+)
  by auto


lemma stepN_Seq_Start_Skip_Fence2E:
  assumes ‹(cfg1, ibT1,ibUT1, ls1) →N (cfg1', ibT1',ibUT1', ls1')› 
      and ‹(cfg2, ibT2,ibUT2, ls2) →N (cfg2', ibT2',ibUT2', ls2')›
      and ‹cfg1 = (Config pc1 (State (Vstore vs1) avst1 h1 p1))› and ‹cfg1' = (Config pc1' (State (Vstore vs1') avst1' h1' p1'))›
      and ‹cfg2 = (Config pc2 (State (Vstore vs2) avst2 h2 p2))› and ‹cfg2' = (Config pc2' (State (Vstore vs2') avst2' h2' p2'))›
      and ‹prog!pc1 ∈ {Start, Skip, Fence}› and ‹pcOf cfg1 = pcOf cfg2› 
    shows ‹vs1' = vs1 ∧ vs2' = vs2 ∧
           pc1' = Suc pc1 ∧ pc2' = Suc pc2 ∧
           avst1' = avst1 ∧ avst2' = avst2 ∧ 
           ls2' = ls2 ∧ ls1' = ls1›
  using assms apply clarsimp
  apply (drule stepB_Seq_Start_Skip_FenceE[of _ _ _ _ _ _ pc1 vs1 avst1 h1 p1
                                pc1' vs1' avst1' h1' p1'], clarify+)
  apply (drule stepB_Seq_Start_Skip_FenceE[of _ _ _ _ _ _ pc2 vs2 avst2 h2 p2
                                pc2' vs2' avst2' h2' p2'], clarify+)
  by (auto simp add: readLocs_def)

end (* locale Prog *)


end