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:"NN0" 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 = (xread_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