Theory Instance_Secret_IMem_Inp

section ‹Relative Security Instance: Secret Memory Input›

text ‹ This theory sets up an instance of Relative Security used to prove an Security of a potentially infinite program›

theory Instance_Secret_IMem_Inp
  imports Instance_Common "Relative_Security.Relative_Security"
begin                                                                            

text "Using the following notation to denote an undefined element"
no_notation bot ()

definition ffile :: "vname" where "ffile = ''ffile''"
definition xx :: "vname" where "xx = ''x''"
definition yy :: "vname" where "yy = ''yy''"  
type_synonym secret = "state × val × val"

abbreviation writeSecretOnFile where "writeSecretOnFile  (Output T (Fun (V xx) (V yy)))"
lemma writeOnFile_not_Jump[simp]:"¬is_IfJump writeSecretOnFile" by (simp add: )
lemma writeOnFile_not_Inp[simp]:"¬is_getInput writeSecretOnFile" by (simp add: )
lemma writeOnFile_not_Fence[simp]:"writeSecretOnFile  Fence" by (simp add: )

definition ffileVal where "ffileVal cfg = vstoreOf(cfg) ffile"
lemma ffileVal_vstore[simp]:"ffileVal cfg = vstoreOf(cfg) ffile" by(simp add: ffileVal_def)


context Prog_Mispred
begin

text "The following functions and definitions make up the required components of the Relative Security locale"
fun corrState :: "stateV  stateO  bool" where 
"corrState cfgO cfgA = True"

(* All our programs will have "Start" followed by the rest, with the rest not containing "Start". 
The secret will be "uploaded" at this Start moment. *)
definition isSecV :: "stateV  bool" where 
"isSecV ss  case ss of (cfg,ibT,ibUT,ls)  ¬finalN ss"
(* We consider the entire initial state as a secret: *)
fun getSecV :: "stateV  secret" where 
"getSecV (cfg,ibT,ibUT,ls) = 
 (case prog!(pcOf cfg) of 
    Start  (stateOf cfg, , )
   |Input T _  (, lhd ibT, )
   |Output T _  (,,outOf (prog!(pcOf cfg)) (stateOf cfg))
   |_  (,,))"


lemma isSecV_iff:"isSecV ss  ¬finalN ss" 
  unfolding isSecV_def 
  by (simp add: case_prod_beta)

(* The secrecy infrastructure is similar to that of the "original" semantics: *)
definition isSecO :: "stateO  bool" where 
"isSecO ss  case ss of (pstate,cfg,cfgs,ibT,ibUT,ls)  ¬finalS ss  cfgs = []"
fun getSecO :: "stateO  secret" where 
"getSecO (pstate,cfg,cfgs,ibT,ibUT,ls) = 
 (case prog!(pcOf cfg) of 
    Start  (stateOf cfg, , )
   |Input T _  (, lhd ibT, )
   |Output T _  (,,outOf (prog!(pcOf cfg)) (stateOf cfg))
   |_  (,,))"
end (* context Prog_Mispred *)




sublocale Prog_Mispred_Init < Rel_Sec where 
  validTransV = validTransV and istateV = istateV  
  and finalV = finalN
  and isSecV = isSecV and getSecV = getSecV
  and isIntV = isIntV and getIntV = getIntV  
  (* *)
  and validTransO = validTransO and istateO = istateO
  and finalO = finalS
  and isSecO = isSecO  and getSecO = getSecO
  and isIntO = isIntO and getIntO = getIntO 
  and corrState = corrState 
  apply standard 
  subgoal by (simp add: finalN_defs)
  subgoal for s by (cases s, simp)
  subgoal by(simp add:isSecV_def) 
  subgoal by (simp add: finalS_defs)
  subgoal by (simp add: finalS_defs)  
  subgoal for ss apply(cases ss) subgoal for ps cfg cfgs ib ls apply(cases cfg) subgoal for n s 
  unfolding isSecO_def finalS_def final_def
  using stepS_0[of ps s ib ls] by auto . . .


(* *)


context Prog_Mispred_Init 
begin

lemmas reachV_induct = Van.reach.induct[split_format(complete)]
lemmas reachO_induct = Opt.reach.induct[split_format(complete)]

lemma is_getInputT_getActV[simp]: 
"(prog!(pcOf cfg)) = Input U inp  getActV (cfg,ibT,ibUT,ls) = lhd ibUT"
  by (cases "prog!(pcOf cfg)", auto simp: Van.getAct_def)

lemma is_getInputU_getActV[simp]: 
"(prog!(pcOf cfg)) = Input T inp  getActV (cfg,ibT,ibUT,ls) = lhd ibT"
by (cases "prog!(pcOf cfg)", auto simp: Van.getAct_def)

lemma not_is_getInput_getActV[simp]: 
"¬ is_getInput (prog!(pcOf cfg))  getActV (cfg,ibT,ibUT,ls) = "
apply (cases "prog!(pcOf cfg)", auto simp: Van.getAct_def)
  subgoal for t apply(cases t, simp_all) . .

lemma is_Output_getObsV[simp]: 
"(prog!(pcOf cfg)) = Output U out  getObsV (cfg,ibT,ibUT,ls) = 
 (outOf (prog!(pcOf cfg)) (stateOf cfg), ls)"
by (cases "prog!(pcOf cfg)", auto simp: Van.getObs_def)

lemma not_is_Output_getObsV[simp]: 
"¬ is_Output (prog!(pcOf cfg))  getObsV (cfg,ibT,ibUT,ls) = "
apply (cases "prog!(pcOf cfg)", auto simp: Van.getObs_def)
  subgoal for t apply(cases t, simp_all) . .
(* *)

lemma is_getInputT_Nil_getActO[simp]: 
"(prog!(pcOf cfg)) = Input T inp   getActO (pstate,cfg,[],ibT,ibUT,ls) = lhd ibT"
  by (cases "prog!(pcOf cfg)", auto simp: Opt.getAct_def)

lemma is_getInputU_Nil_getActO[simp]: 
"(prog!(pcOf cfg)) = Input U inp  getActO (pstate,cfg,[],ibT,ibUT,ls) = lhd ibUT"
by (cases "prog!(pcOf cfg)", auto simp: Opt.getAct_def)

lemma not_is_getInput_Nil_getActO[simp]: 
"(¬ is_getInput (prog!(pcOf cfg))) 
 cfgs  []  getActO (pstate,cfg,cfgs,ibT,ibUT,ls) = "
apply (cases cfgs, auto)
   apply (cases "prog!(pcOf cfg)", auto simp: Opt.getAct_def)
  subgoal for t apply(cases t, simp_all) . .

lemma is_Output_Nil_getObsO[simp]: 
"(prog!(pcOf cfg)) = Output U out  
 getObsO (pstate,cfg,[],ibT,ibUT,ls) = (outOf (prog!(pcOf cfg)) (stateOf cfg), ls)"
by (cases "prog!(pcOf cfg)", auto simp: Opt.getObs_def)

lemma not_is_Output_Nil_getObsO[simp]: 
"¬ is_Output (prog!(pcOf cfg))  cfgs  []  getObsO (pstate,cfg,cfgs,ibT,ibUT,ls) = "
apply (cases cfgs, auto)
apply (cases "prog!(pcOf cfg)", auto simp: Opt.getObs_def)
  subgoal for t apply(cases t, simp_all) . .

(* *)



lemma getActV_simps: 
"getActV (cfg,ibT,ibUT,ls) = 
 (case prog!(pcOf cfg) of 
    Input T _    lhd ibT
   |Input U _  lhd ibUT
   |_   
 )"
  unfolding Van.getAct_def 
  apply (simp split: com.splits, safe)
  subgoal for t apply(cases t, simp_all) . 
  subgoal for t apply(cases t, simp_all) . .

lemma getObsV_simps: 
"getObsV (cfg,ibT,ibUT,ls) = 
 (case prog!(pcOf cfg) of 
    Output U _  (outOf (prog!(pcOf cfg)) (stateOf cfg), ls)
   |_   
 )"
  unfolding Van.getObs_def
  apply (simp split: com.splits, safe)
  subgoal for t apply(cases t, simp_all) . 
  subgoal for t apply(cases t, simp_all) . .

lemma getActO_simps: 
"getActO (pstate,cfg,cfgs,ibT,ibUT,ls) = 
 (case (cfgs,prog!(pcOf cfg)) of 
    ([],Input T _)    lhd ibT
   |([],Input U _)  lhd ibUT
   |_   
 )"
  unfolding Van.getAct_def
  apply (simp split: com.splits list.splits, safe)
  subgoal for t apply(cases t, simp_all) . .

lemma getObsO_simps: 
"getObsO (pstate,cfg,cfgs,ibT,ibUT,ls) = 
 (case (cfgs,prog!(pcOf cfg)) of 
    ([],Output U _)  (outOf (prog!(pcOf cfg)) (stateOf cfg), ls)
   |_   
 )"
  unfolding Opt.getObs_def
  apply (simp split: com.splits list.splits, safe)
  subgoal for t apply(cases t, simp_all) . 
  subgoal for t apply(cases t, simp_all) . .


end (* context Prog_Mispred_Init *)


end