Theory Eg2

theory Eg2
imports Dependent_SIFUM_Type_Systems.Language
begin

datatype varC = control_varC | bufferC | high_varC | low_varC | tempC | regC

type_synonym addrC = varC
type_synonym val = nat
type_synonym memC = "addrC ⇒ val"

(* Address expression evaluation *)
datatype aexpC = Const "val" |
                 Load "addrC"

fun 
  evAC :: "memC ⇒ aexpC ⇒ val"
where
  "evAC mem (Const v) = v" |
  "evAC mem (Load x) = mem x"

(* Boolean expression evaluation *)
datatype bexpC = Eq "addrC" "val"

fun
  evBC :: "memC ⇒ bexpC ⇒ bool"
where
  "evBC mem (Eq x v) = ((mem x) = v)"

(* NB: dma ~ "domain assignment"
 * Domain assignment function based on the value of a control variable,
 * Low if 0, High otherwise. *)
definition
  dma_control_varC :: "val ⇒ Sec"
where
  "dma_control_varC v ≡ if v = 0 then Low else High"

(* buffer's security level is controlled by control_var.
 * high_var's is High.
 * All other memory's security level is Low. *)
definition
  dmaC :: "memC ⇒ addrC ⇒ Sec"
where
  "dmaC m x ≡ if x = bufferC then dma_control_varC (m control_varC) else if x = high_varC then High else Low"

(* Function that gives the control variables of a given variable.
 * Only buffer is controlled by a control variable, control_var *)
definition
  𝒞_varsC :: "addrC ⇒ addrC set"
where
  "𝒞_varsC x ≡ if x = bufferC then {control_varC} else {}"

primrec
  aexp_varsC :: "aexpC ⇒ varC set"
where
  "aexp_varsC (Const _) = {}" |
  "aexp_varsC (Load v) = {v}"
  
primrec
  bexp_varsC :: "bexpC ⇒ varC set"
where
  "bexp_varsC (Eq v w) = {v}"

locale sifum_example2 =
  sifum_lang_no_dma evAC evBC aexp_varsC bexp_varsC +
  assumes eval_det: "(lc, lc') ∈ sifum_lang_no_dma.evalw evAC evBC ⟹ (lc, lc'') ∈ sifum_lang_no_dma.evalw evAC evBC ⟹ lc' = lc''"

definition
  𝒞C :: "addrC set"
where
  "𝒞C ≡ ⋃x. 𝒞_varsC x"

context sifum_example2 begin

definition
  read_bufferC :: "(varC, aexpC, bexpC) Stmt"
where
  "read_bufferC ≡ 
     ModeDecl Skip (Acq control_varC AsmNoWrite) ;; 
     ModeDecl Skip (Acq tempC AsmNoReadOrWrite) ;;
     Assign tempC (Load bufferC) ;;
     Assign regC (Load control_varC);;
     If (Eq regC 0) (Assign low_varC (Load tempC)) (Assign high_varC (Load tempC)) ;;
     Assign tempC (Const 0) ;;
     ModeDecl Skip (Rel tempC AsmNoReadOrWrite)"

end

end