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