Theory Fun1

section "Disproof of Relative Security for fun1"
theory Fun1
imports "../Instance_IMP/Instance_Secret_IMem" 
  "Secret_Directed_Unwinding.SD_Unwinding_fin" 
begin 

subsection "Function definition and Boilerplate"
no_notation bot (‹⊥›)
consts NN :: nat

consts input :: int
definition aa1 :: "avname" where "aa1 = ''a1''" 
definition aa2 :: "avname" where "aa2 = ''a2''" 
definition vv :: "avname" where "vv = ''v''" 
definition xx :: "avname" where "xx = ''i''" 
definition tt :: "avname" where "tt = ''tt''" 

lemma NN_suc[simp]:"nat (NN + 1) = Suc (nat NN)" 
  by force

lemma NN:"NN≥0" by auto


lemmas vvars_defs = aa1_def aa2_def vv_def xx_def tt_def

lemma vvars_dff[simp]: 
"aa1 ≠ aa2" "aa1 ≠ vv" "aa1 ≠ xx" "aa1 ≠ tt"
"aa2 ≠ aa1" "aa2 ≠ vv" "aa2 ≠ xx" "aa2 ≠ tt"
"vv ≠ aa1" "vv ≠ aa2"  "vv ≠ xx" "vv ≠ tt"
"xx ≠ aa1" "xx ≠ aa2" "xx ≠ vv" "xx ≠ tt"
"tt ≠ aa1" "tt ≠ aa2" "tt ≠ vv" "tt ≠ xx"
unfolding vvars_defs by auto


consts size_aa1 :: nat
consts size_aa2 :: nat

definition "s_add = {a. a ≠ nat NN+1}"
fun vs0::"char list ⇒ int" where 
           "vs0 x = 0"

lemma vs0[simp]:"(λx. 0) = vs0"  unfolding vs0.simps by simp

(*avstore*)
fun as:: "char list ⇒ nat × nat" where 
        "as a = (if a = aa1 then (0, nat NN)
                   else (if a = aa2 then (nat NN, nat size_aa2) 
                   else (nat size_aa2,0)))"

definition "avst' ≡ (Avstore as)"

lemmas avst_defs = avst'_def as.simps

lemma avstore_loc[simp]:"Avstore (λa. if a = aa1 then (0, nat NN) else if a = aa2 then (nat NN, nat size_aa2) else (nat size_aa2, 0)) =
    avst'"
  unfolding avst_defs by auto

abbreviation "read_add ≡ {a. a ≠ (nat NN + 1)}"

(* The initial vstore can be anything *)
fun initVstore :: "vstore ⇒ bool" where
"initVstore (Vstore vst) = (vst = vs0)"
(* The initial avstore contains two arrays named aa1 and aa2 located one after the other *)
fun initAvstore :: "avstore ⇒ bool" where
"initAvstore avst  = (avst = avst')"
fun initHeap::"(nat ⇒ int) ⇒ bool" where
"initHeap h = (∀x∈read_add. h x = 0)"

lemma initAvstore_0[intro]:"initAvstore avst' ⟹ array_base aa1 avst' = 0"
  unfolding avst_defs array_base_def
  by (smt (verit, del_insts) avstore.case fstI)

fun istate ::"state ⇒ bool"  where
  "istate s = 
  (initVstore (getVstore s) ∧ 
  initAvstore (getAvstore s) ∧ 
  initHeap (getHheap s))"

definition "prog ≡
[
 ⌦‹0 › Start , 
 ⌦‹1 › Input U xx ,
 ⌦‹2 › tt ::= (N 0),
 ⌦‹3 › IfJump (Less (V xx) (N NN)) 4 5,
 ⌦‹4 ›   tt ::= (VA aa2 (Times (VA aa1 (V xx)) (N 512))) ,
 ⌦‹5 › Output U (V tt) 
]"

(* *)

lemma cases_5: "(i::pcounter) = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 ∨ i = 4 ∨ i = 5 ∨ i > 5"
apply(cases i, simp_all) 
subgoal for i apply(cases i, simp_all)
subgoal for i apply(cases i, simp_all)
subgoal for i apply(cases i, simp_all)
subgoal for i apply(cases i, simp_all)
subgoal for i apply(cases i, simp_all)
  . . . . . . 

lemma xx_NN_cases: "vs xx < (int NN) ∨ vs xx ≥ (int NN)" by auto

lemma is_If_pcOf[simp]: 
"pcOf cfg < 6 ⟹ is_IfJump (prog ! (pcOf cfg)) ⟷ pcOf cfg = 3"
apply(cases cfg) subgoal for pc s using cases_5[of "pcOf cfg "] 
apply (auto simp: prog_def) . .

lemma is_If_pc[simp]: 
"pc < 6 ⟹ is_IfJump (prog ! pc) ⟷ pc = 3"
using cases_5[of pc] 
by (auto simp: prog_def) 

lemma eq_Fence_pc[simp]: 
"pc < 6 ⟹ prog ! pc ≠ Fence"
using cases_5[of pc] 
  by (auto simp: prog_def)



 
(* *)

fun mispred :: "predState ⇒ pcounter list ⇒ bool" where
  "mispred p pc = (if pc = [3] then True else False)"

fun resolve :: "predState ⇒ pcounter list ⇒ bool" where
  "resolve p pc = (if pc = [5,5] then True else False)"

consts update :: "predState ⇒ pcounter list ⇒ predState"
consts pstate0 :: predState
(* *)
interpretation Prog_Mispred_Init where 
prog = prog and initPstate = pstate0 and 
mispred = mispred and resolve = resolve and update = update and 
istate = istate
  by (standard, simp add: prog_def)
(* *)

(* Restoring the abbreviations: *)
abbreviation
  stepB_abbrev :: "config × val llist × val llist  ⇒ config × val llist × val llist ⇒ bool" (infix ‹→B› 55)
  where "x →B y == stepB x y"

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

abbreviation
  stepM_abbrev :: "config × val llist × val llist ⇒ config × val llist × val llist ⇒ bool" (infix ‹→M› 55)
  where "x →M y == stepM x y"

abbreviation
  stepN_abbrev :: "config × val llist × val llist × loc set ⇒ config × val llist × val llist × loc set ⇒ bool" (infix ‹→N› 55)
  where "x →N y == stepN x y"

abbreviation
  stepsN_abbrev :: "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"

abbreviation
  stepS_abbrev :: "configS ⇒ configS ⇒ bool" (infix ‹→S› 55)
  where "x →S y == stepS x y"

abbreviation
  stepsS_abbrev :: "configS ⇒ configS ⇒ bool" (infix ‹→S*› 55)
  where "x →S* y == star stepS x y"

(* *)

lemma endPC[simp]: "endPC = 6"
unfolding endPC_def unfolding prog_def by auto

(* *)

lemma is_getTrustedInput_pcOf[simp]: "pcOf cfg < 6 ⟹ is_getInput (prog!(pcOf cfg)) ⟷ pcOf cfg = 1"
  using cases_5[of "pcOf cfg"] by (auto simp: prog_def)

lemma getTrustedInput_pcOf[simp]: "(prog!1) = Input U xx"
   by (auto simp: prog_def)


lemma is_Output_pcOf[simp]: "pcOf cfg < 6 ⟹ is_Output (prog!(pcOf cfg)) ⟷ pcOf cfg = 5 ∨ pcOf cfg = 6"
using cases_5[of "pcOf cfg"] by (auto simp: prog_def)


lemma is_Fence_pcOf[simp]: "pcOf cfg < 6 ⟹(prog!(pcOf cfg)) ≠ Fence"
using cases_5[of "pcOf cfg"] by (auto simp: prog_def)

lemma prog0[simp]:"prog ! 0 = Start"
  by (auto simp: prog_def)

lemma prog1[simp]:"prog ! (Suc 0) = Input U xx"
  by (auto simp: prog_def)

lemma prog2[simp]:"prog ! 2 = tt ::= (N 0)"
  by (auto simp: prog_def)

lemma prog3[simp]:"prog ! 3 = IfJump (Less (V xx) (N NN)) 4 5"
  by (auto simp: prog_def)

lemma prog4[simp]:"prog ! 4 = tt ::= (VA aa2 (Times (VA aa1 (V xx)) (N 512)))"
  by (auto simp: prog_def)

lemma prog5[simp]:"prog ! 5 = Output U (V tt)"
  by (auto simp: prog_def)
(* *)

lemma isSecV_pcOf[simp]: 
"isSecV (cfg,ibT, ibUT) ⟷ pcOf cfg = 0"
using isSecV_def by simp

lemma isSecO_pcOf[simp]: 
"isSecO (pstate,cfg,cfgs,ibT,ibUT,ls) ⟷ (pcOf cfg = 0 ∧ cfgs = [])"
using isSecO_def by simp

(* *)

lemma getInputT_not[simp]: "pcOf cfg < 6 ⟹ 
(prog ! pcOf cfg) ≠ Input T x"
apply(cases cfg) subgoal for pc s using cases_5[of "pcOf cfg "] 
by (auto simp: prog_def) .

lemma getActV_pcOf[simp]: 
"pcOf cfg < 6 ⟹ 
 getActV (cfg,ibT,ibUT,ls) = 
 (if pcOf cfg = 1 then lhd ibUT else ⊥)"
apply(subst getActV_simps) unfolding prog_def 
apply simp  
using getActV_simps not_is_getTrustedInput_getActV prog_def by auto

lemma getObsV_pcOf[simp]: 
"pcOf cfg < 6 ⟹  
 getObsV (cfg,ibT,ibUT,ls) = 
 (if pcOf cfg = 5 then 
  (outOf (prog!(pcOf cfg)) (stateOf cfg), ls)
  else ⊥ 
 )"
apply(subst getObsV_simps) 
unfolding prog_def apply simp  
using getObsV_simps not_is_Output_getObsV is_Output_pcOf prog_def 
  by (metis less_irrefl_nat)

lemma getActO_pcOf[simp]: 
"pcOf cfg < 6 ⟹ 
 getActO (pstate,cfg,cfgs,ibT,ibUT,ls) = 
 (if pcOf cfg = 1 ∧ cfgs = [] then lhd ibUT else ⊥)"
apply(subst getActO_simps)
apply(cases cfgs, auto)
unfolding prog_def 
using getActV_simps getActV_pcOf prog_def by presburger

lemma getObsO_pcOf[simp]: 
"pcOf cfg < 6 ⟹  
 getObsO (pstate,cfg,cfgs,ibT,ibUT,ls) = 
 (if (pcOf cfg = 5 ∧ cfgs = []) then 
  (outOf (prog!(pcOf cfg)) (stateOf cfg), ls)
  else ⊥ 
 )"
apply(subst getObsO_simps) 
apply(cases cfgs, auto)
unfolding prog_def 
using getObsV_simps is_Output_pcOf not_is_Output_getObsV prog_def 
  by (metis getObsV_pcOf)

(* *)

(* nextB, nextM and readLocs behavior 
(for nextM we are only interested at branching points, here only program counter 4): *)

lemma nextB_pc0[simp]: 
"nextB (Config 0 s, ibT, ibUT) = 
 (Config 1 s, ibT, ibUT)"
apply(subst nextB_Start_Skip_Fence)
unfolding endPC_def unfolding prog_def by auto

lemma readLocs_pc0[simp]: 
"readLocs (Config 0 s) = {}"
unfolding endPC_def readLocs_def unfolding prog_def by auto

(* *)
lemma nextB_pc1[simp]: 
"ibUT ≠ LNil ⟹ nextB (Config 1 (State (Vstore vs) avst h p), ibT, ibUT) = 
 (Config 2 (State (Vstore (vs(xx := lhd ibUT))) avst h p), ibT, ltl ibUT)"
apply(subst nextB_getUntrustedInput')
unfolding endPC_def unfolding prog_def by auto

lemma readLocs_pc1[simp]: 
"readLocs (Config 1 s) = {}"
unfolding endPC_def readLocs_def unfolding prog_def by auto

lemma nextB_pc1'[simp]: 
"ibUT ≠ LNil ⟹ nextB (Config (Suc 0) (State (Vstore vs) avst h p), ibT, ibUT) = 
 (Config 2 (State (Vstore (vs(xx := lhd ibUT))) avst h p), ibT, ltl ibUT)"
apply(subst nextB_getUntrustedInput')
unfolding endPC_def unfolding prog_def by auto

lemma readLocs_pc1'[simp]: 
"readLocs (Config (Suc 0) s) = {}"
unfolding endPC_def readLocs_def unfolding prog_def by auto

(* *)
lemma nextB_pc2[simp]: 
"nextB (Config 2 (State (Vstore vs) avst h p), ibT, ibUT) = 
 ((Config 3 (State (Vstore (vs(tt := 0))) avst h p)), ibT, ibUT)"
apply(subst nextB_Assign)
unfolding endPC_def unfolding prog_def by auto

lemma readLocs_pc2[simp]: 
"readLocs (Config 2 (State (Vstore vs) avst h p)) = {}"
unfolding endPC_def readLocs_def unfolding prog_def by auto

(* *)

lemma nextB_pc3_then[simp]: 
"vs xx < NN ⟹
 nextB (Config 3 (State (Vstore vs) avst h p), ibT, ibUT) = 
 (Config 4 (State (Vstore vs) avst h p), ibT, ibUT)"
apply(subst nextB_IfTrue)
unfolding endPC_def unfolding prog_def by auto

lemma nextB_pc3_else[simp]: 
"vs xx ≥ NN ⟹
 nextB (Config 3 (State (Vstore vs) avst h p), ibT, ibUT) = 
 (Config 5 (State (Vstore vs) avst h p), ibT, ibUT)"
apply(subst nextB_IfFalse)
unfolding endPC_def unfolding prog_def by auto

lemma nextB_pc3: 
"nextB (Config 3 (State (Vstore vs) avst h p), ibT, ibUT) = 
 (Config (if vs xx < NN then 4 else 5) (State (Vstore vs) avst h p), ibT, ibUT)"
  by(cases "vs xx < NN", auto)

lemma nextM_pc3_then[simp]: 
"vs xx ≥ NN ⟹
 nextM (Config 3 (State (Vstore vs) avst h p), ibT, ibUT) = 
 (Config 4 (State (Vstore vs) avst h p), ibT, ibUT)"
apply(subst nextM_IfTrue)
unfolding endPC_def unfolding prog_def by auto

lemma nextM_pc3_else[simp]: 
"vs xx < NN ⟹
 nextM (Config 3 (State (Vstore vs) avst h p), ibT, ibUT) = 
 (Config 5 (State (Vstore vs) avst h p), ibT, ibUT)"
apply(subst nextM_IfFalse)
unfolding endPC_def unfolding prog_def by auto

lemma nextM_pc3: 
"nextM (Config 3 (State (Vstore vs) avst h p), ibT, ibUT) = 
 (Config (if vs xx < NN then 5 else 4) (State (Vstore vs) avst h p), ibT, ibUT)"
by(cases "vs xx < NN", auto)

lemma readLocs_pc3[simp]: 
"readLocs (Config 3 s) = {}"
unfolding endPC_def readLocs_def unfolding prog_def by auto

(* *)

lemma nextB_pc4[simp]: 
"nextB (Config 4 (State (Vstore vs) avst (Heap h) p), ibT, ibUT) = 
 (let i = array_loc aa1 (nat (vs xx)) avst; j = (array_loc aa2 (nat ((h i) * 512)) avst) 
  in (Config 5 (State (Vstore (vs(tt := h j))) avst (Heap h) p)), ibT, ibUT)"
apply(subst nextB_Assign)
  unfolding endPC_def unfolding prog_def by auto

lemma readLocs_pc4[simp]: 
"readLocs (Config 4 (State (Vstore vs) avst (Heap h) p)) = 
(let i = array_loc aa1 (nat (vs xx)) avst; 
     j = (array_loc aa2 (nat ((h i) * 512)) avst)
in {i, j})"
unfolding endPC_def readLocs_def unfolding prog_def by auto

(* *)


lemma nextB_pc5[simp]:
"nextB (Config 5 s, ibT, ibUT) = (Config 6 s, ibT, ibUT)"
apply(subst nextB_Output)
unfolding endPC_def unfolding prog_def by auto

lemma readLocs_pc5[simp]: 
"readLocs (Config 5 (State (Vstore vs) avst (Heap h) p)) = 
 {}"
unfolding endPC_def readLocs_def unfolding prog_def by auto


lemma nextB_stepB_pc: 
"pc < 6 ⟹ (pc = 1 ⟶ ibUT ≠ LNil) ⟹ 
(Config pc s, ibT, ibUT) →B nextB (Config pc s, ibT, ibUT)"
apply(cases s) subgoal for vst avst hh p apply(cases vst, cases avst, cases hh)
subgoal for vs as h
using cases_5[of pc] apply safe
  subgoal by simp 
  subgoal by simp 
  (* *)
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def, metis llist.collapse)

  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def)  
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
  by (simp add: prog_def)
  (* *)
  subgoal by(cases "vs xx < NN", simp_all)  
  subgoal by(cases "vs xx < NN", simp_all)  
  (* *)
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
  by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
  by (simp add: prog_def) 
  (* *)
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
  by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
  by (simp add: prog_def) 
  (* *)
  by simp+ . . 


lemma not_finalB: 
"pc < 6 ⟹ (pc = 1 ⟶ ibUT ≠ LNil) ⟹ 
 ¬ finalB (Config pc s, ibT, ibUT)"
using nextB_stepB_pc by (simp add: stepB_iff_nextB)

lemma finalB_pc_iff': 
"pc < 6 ⟹
 finalB (Config pc s, ibT, ibUT) ⟷ 
 (pc = 1 ∧ ibUT = LNil)"
  subgoal apply safe
    subgoal using nextB_stepB_pc[of pc] by (auto simp add: stepB_iff_nextB) 
    subgoal using nextB_stepB_pc[of pc] by (auto simp add: stepB_iff_nextB) 
    subgoal using finalB_iff by auto . .


lemma finalB_pc_iff: 
"pc ≤ 6 ⟹
 finalB (Config pc s, ibT, ibUT) ⟷ 
 (pc = 1 ∧ ibUT = LNil ∨ pc = 6)"
  using cases_5[of pc] apply (elim disjE, simp add: finalB_def)
  subgoal by (meson final_def stebB_0)
  by (simp add: finalB_pc_iff' finalB_endPC)+

lemma finalB_pcOf_iff[simp]:
"pcOf cfg ≤ 6 ⟹ 
 finalB (cfg, ibT, ibUT) ⟷ (pcOf cfg = 1 ∧ ibUT = LNil ∨ pcOf cfg = 6)"
  by (metis config.collapse finalB_pc_iff) 


definition "vsi_t cfg ≡ (vstore (getVstore (stateOf cfg)) xx) < NN"
definition "vsi_f cfg ≡ (vstore (getVstore (stateOf cfg)) xx) ≥ NN"
lemma vs_xx_cases:"vsi_t cfg ∨ vsi_f cfg" unfolding vsi_t_def vsi_f_def by auto

lemmas vsi_defs = vsi_t_def vsi_f_def

lemma bool_invar[simp]:"¬vsi_t (Config 6 s) ⟹ vsi_t (Config 6 s) ⟹ (Config 6 s, ib1) →B (Config 6 s, ib1) ⟹ False"
  unfolding vsi_defs
  by simp
lemma nextB_vs_consistent_aux: 
  "2 ≤ pc ∧ pc < 6 ⟹
   (nextB (Config pc (State (Vstore vs) avst (Heap h) p),ibT, ibUT)) = (Config pc' (State (Vstore vs') avst'' (Heap h') p'),ibT', ibUT') ⟹ 
    avst = avst'' ∧
    vs xx = vs' xx ∧
    h = h'  ∧
    pc < pc'"
  using cases_5[of pc] apply(elim disjE) apply simp_all
  subgoal by auto
  subgoal using xx_NN_cases[of vs] by(elim disjE, simp_all)
  by auto 

lemma nextB_vs_consistent: 
  "2 ≤ pcOf cfg ∧ pcOf cfg < 6 ⟹
   (nextB (cfg, ibT, ibUT)) = (cfg', ibT', ibUT') ⟹ 
    (getAvstore (stateOf cfg)) = (getAvstore (stateOf cfg')) ∧ 
    (getHheap (stateOf cfg)) = (getHheap (stateOf cfg')) ∧ 
    vstore (getVstore (stateOf cfg)) xx = vstore (getVstore (stateOf cfg')) xx"
  apply(cases cfg) subgoal for pc s 
  apply(cases s) subgoal for vstore avst heap_h p 
  apply (cases heap_h, cases vstore, cases avst) subgoal for h vs 
  apply(cases cfg') subgoal for pc' s'
  apply(cases s') subgoal for vstore' avst'' heap_h' p' 
  apply (cases heap_h', cases vstore', cases avst'')  subgoal for h vs 
  using nextB_vs_consistent_aux apply simp 
  by blast . . . . . .


lemma nextB_vsi_t_consistent: 
  "2 ≤ pcOf cfg ∧ pcOf cfg < 6 ⟹
   (nextB (cfg, ibT, ibUT)) = (cfg', ibT', ibUT') ⟹ 
   vsi_t cfg ⟷ vsi_t cfg'"
  unfolding vsi_defs using  nextB_vs_consistent 
  by simp

lemma nextB_vsi_f_consistent: 
  "2 ≤ pcOf cfg ∧ pcOf cfg < 6 ⟹
   (nextB (cfg, ibT, ibUT)) = (cfg', ibT', ibUT') ⟹ 
   vsi_f cfg ⟷ vsi_f cfg'"
  unfolding vsi_defs using  nextB_vs_consistent 
  by simp


end