Theory Example_TypeSystem

(*
Title: Value-Dependent SIFUM-Type-Systems
Authors: Toby Murray, Robert Sison, Edward Pierzchalski, Christine Rizkallah
(Based on the SIFUM-Type-Systems AFP entry, whose authors
 are: Sylvia Grewe, Heiko Mantel, Daniel Schoepe)
*)
theory Example_TypeSystem
imports 
  "../TypeSystem" 
  TypeSystemTactics
begin

datatype addr = low_var | high_var | control_var | buffer | temp
type_synonym val = nat
type_synonym mem = "addr ⇒ val"

datatype aexp = Load "addr"

fun 
  ev⇩A :: "mem ⇒ aexp ⇒ val"
where
  "ev⇩A mem (Load x) = mem x"
 
fun
  aexp_vars :: "aexp ⇒ addr set"
where
  "aexp_vars (Load x) = {x}"
  
datatype bexp = Same "addr" "addr" |
                NotSame "addr" "addr" |
                Eq "addr" "val" |
                Neq "addr" "val" |
                TT | FF

fun
  ev⇩B :: "mem ⇒ bexp ⇒ bool"
where
  "ev⇩B mem (Same x y) = ((mem x) = (mem y))" | 
  "ev⇩B mem (NotSame x y) = ((mem x) ≠ (mem y))" |
  "ev⇩B mem (Eq x c) = ((mem x) = c)" | 
  "ev⇩B mem (Neq x c) = ((mem x) ≠ c)" |
  "ev⇩B mem TT = True" |
  "ev⇩B mem FF = False"

fun
  bexp_vars :: "bexp ⇒ addr set"
where
  "bexp_vars (Neq x c) = {x}" |
  "bexp_vars (Eq x c) = {x}" |
  "bexp_vars (Same x y) = {x,y}" |
  "bexp_vars (NotSame x y) = {x,y}" |
  "bexp_vars _ = {}"
  
fun
  bexp_neg :: "bexp ⇒ bexp"
where
  "bexp_neg (Neq x y) = (Eq x y)" |
  "bexp_neg (Eq x y) = (Neq x y)" |
  "bexp_neg (Same x y) = (NotSame x y)" |
  "bexp_neg (NotSame x y) = (Same x y)" |
  "bexp_neg TT = FF" |
  "bexp_neg FF = TT"
  
fun
   bexp_assign :: "addr ⇒ aexp ⇒ bexp"
where
  "bexp_assign x (Load y)  = (Same x y)"
    
definition
  dma_control_var :: "val ⇒ Sec"
where
  "dma_control_var v ≡ if v = 0 then Low else High"

definition
  dma :: "mem ⇒ addr ⇒ Sec"
where
  "dma m x ≡ if x = buffer then dma_control_var (m control_var) else if x = high_var then High else Low"

definition
  𝒞_vars :: "addr ⇒ addr set"
where
  "𝒞_vars x ≡ if x = buffer then {control_var} else {}"

definition
  mds⇩s :: "Mode ⇒ 'Var set"
where 
  "mds⇩s ≡ λ_. {}"

locale sifum_example =
  sifum_lang_no_dma ev⇩A ev⇩B aexp_vars bexp_vars +
  assumes eval_det: "(lc, lc') ∈ sifum_lang_no_dma.eval⇩w ev⇩A ev⇩B ⟹ (lc, lc'') ∈ sifum_lang_no_dma.eval⇩w ev⇩A ev⇩B ⟹ lc' = lc''"

definition
  𝒞 :: "addr set"
where
  "𝒞 ≡ ⋃x. 𝒞_vars x"

fun
  dma_type :: "addr ⇒ bexp set"
where
  "dma_type high_var = {FF}" |
  "dma_type buffer = {Eq control_var 0}" |
  "dma_type _ = {}"

sublocale sifum_example ⊆ sifum_types_assign ev⇩A ev⇩B aexp_vars bexp_vars dma 𝒞_vars 𝒞 bexp_neg dma_type FF bexp_assign
  apply(unfold_locales)
              apply(blast intro: eval_det)
             apply(rule Var_finite)
            apply(auto simp: 𝒞_vars_def dma_def 𝒞_def split: if_splits)[3]
         apply(rename_tac mem e, case_tac e, auto)[1]
        apply(case_tac x, auto simp: dma_def dma_control_var_def)[1]
       apply(case_tac x, auto simp: 𝒞_vars_def)[1]
      apply(simp+)[2]
    apply(case_tac e, auto)[1]
   apply(case_tac e, simp)
  apply(auto simp: 𝒞_def)
  done

context sifum_example begin

definition
  read_buffer :: "(addr, aexp, bexp) Stmt"
where
  "read_buffer ≡ 
     ModeDecl Skip (Acq control_var AsmNoWrite) ;; 
     ModeDecl Skip (Acq temp AsmNoReadOrWrite) ;;
     Assign temp (Load buffer) ;;
     If (Eq control_var 0) (Assign low_var (Load temp)) (Assign high_var (Load temp))"


lemma 𝒞_simp[simp]:
  "𝒞 = {control_var}"
  by(auto simp: 𝒞_def 𝒞_vars_def split: if_splits)

  
lemma type_aexpr_Load:
  "v ∉ dom Γ ⟹ type_aexpr Γ (Load v) (dma_type v)"
  apply(insert type_aexpr[of Γ "Load v", simplified])
  apply(simp add: to_total_def)
  done

lemma type_aexpr_Load':
  "v ∈ dom Γ ⟹ t = (the (Γ v)) ⟹ type_aexpr Γ (Load v) t"
  apply(insert type_aexpr[of Γ "Load v", simplified])
  apply(simp add: to_total_def)
  done


declare restrict_preds_to_vars_def [simp]
declare add_pred_def [simp]
declare stable_def [simp]
declare to_total_def [simp]
declare 𝒞_vars_def [simp]
declare anno_type_stable_def [simp]
declare anno_type_sec_def [simp]
declare assign_post_def [simp]

lemma [simp]: "pred_entailment P {}" by(simp add: pred_entailment_def pred_def)
lemma [simp]: "e ∈ P ⟹ pred_entailment P {e}" by(blast intro: subset_entailment)
lemma [simp]: "FF ∈ P ⟹ pred_entailment P Q" by(auto simp: pred_entailment_def pred_def)

lemma read_buffer_typed:
  "Γ = (λ_. None) ⟹ 𝒮 = ({},{}) ⟹ P = {} ⟹ 
  ∃Γ' 𝒮' P'. has_type Γ 𝒮 P read_buffer Γ' 𝒮' P'"
  apply(intro exI)
  apply(simp add: read_buffer_def)
  apply(rule seq_type)
   apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
       apply clarsimp
       apply(rule skip_type)
      apply simp
     apply simp
    apply simp
   apply simp
  apply(rule seq_type)
   apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
       apply clarsimp
       apply(rule skip_type)
      apply simp
     apply simp
    apply simp
   apply simp
  apply(rule seq_type)
   apply(rule assign⇩2[OF _ _ _ HOL.refl])
      apply simp
     apply(rule type_aexpr_Load)
     apply simp
    apply simp    
   apply simp
  apply(rule if_type')
      apply(rule type_bexprI)
      apply simp
     apply(clarsimp)
    apply(rule assign⇩1)
        apply simp
       apply(simp)
      apply(rule type_aexpr_Load')
       apply simp
      apply simp
     apply(simp add: subtype_def)
    apply(simp)
   apply(rule assign⇩1)
       apply simp
      apply simp
     apply(rule type_aexpr_Load')
      apply simp
     apply simp
    apply(simp add: subtype_def)
   apply(simp)
  apply clarsimp
  apply fastforce
  done

lemma read_buffer_com_sifum_secure:
  "com_sifum_secure (read_buffer,(λ_. {}))"
  apply(insert read_buffer_typed[OF HOL.refl HOL.refl HOL.refl])
  apply clarify
  apply(rule typed_secure)
   apply(fastforce simp: Γ_of_mds_def 𝒮_of_mds_def)
  apply(auto simp: mds_yields_stable_types_def)
  done

definition
  write_buffer :: "(addr, aexp, bexp) Stmt"
where
  "write_buffer ≡ 
     ModeDecl Skip (Acq control_var AsmNoWrite) ;; 
     ModeDecl Skip (Acq temp AsmNoReadOrWrite) ;;
     If (Eq control_var 0) (Assign temp (Load low_var)) (Assign temp (Load high_var)) ;;
     Assign buffer (Load temp)"

lemma restrict_preds_to_vars_empty[simp]:
  "restrict_preds_to_vars {} V = {}"
  apply(simp add: restrict_preds_to_vars_def)
  done

lemma restrict_preds_to_vars_idemp[simp]:
  "restrict_preds_to_vars (restrict_preds_to_vars P V) V = 
   restrict_preds_to_vars P V"
  apply(simp add: restrict_preds_to_vars_def)
  done

lemma restrict_preds_to_vars_insert1[simp]:
  "(∀x∈bexp_vars a. x ∈ V) ⟹ restrict_preds_to_vars (insert a P) V = (insert a (restrict_preds_to_vars P V))"
  apply(simp add: restrict_preds_to_vars_def)
  apply fastforce
  done

lemma restrict_preds_to_vars_insert2[simp]:
  "(∃x∈bexp_vars a. x ∉ V) ⟹ restrict_preds_to_vars (insert a P) V = ((restrict_preds_to_vars P V))"
  apply(simp add: restrict_preds_to_vars_def)
  apply fastforce
  done
  
lemma [simp]:
  "Eq a b ∈ P ⟹ Neq a b ∈ P ⟹ pred_entailment P Q"
  apply(clarsimp simp: pred_entailment_def pred_def)
  apply(frule bspec, assumption)
  apply(drule bspec, assumption, fastforce)
  done
  
declare restrict_preds_to_vars_def[simp del]

lemma write_buffer_typed:
  "Γ = (λ_. None) ⟹ 𝒮 = ({},{}) ⟹ P = {} ⟹ 
  ∃Γ' 𝒮' P'. has_type Γ 𝒮 P write_buffer Γ' 𝒮' P'"
  apply(intro exI)
  apply(simp add: write_buffer_def)
  apply(rule seq_type)
   apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
       apply clarsimp
       apply(rule skip_type)
      apply simp
     apply simp
    apply simp
   apply simp
  apply(rule seq_type)
   apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
       apply clarsimp
       apply(rule skip_type)
      apply simp
     apply simp
    apply simp
   apply simp
  apply(rule seq_type)
   apply(rule if_type[where Γ'''="[temp ↦ dma_type buffer]" and P'''="{}"])
            apply(rule type_bexprI)        
            apply simp
           apply simp
          apply(rule assign⇩2[OF _ _ _ HOL.refl])
             apply simp
            apply(rule type_aexpr_Load)
            apply simp
           apply simp 
          apply simp
         apply(rule assign⇩2[OF _ _ _ HOL.refl])
            apply simp
           apply(rule type_aexpr_Load)
           apply simp
          apply(simp)
         apply simp
        apply(clarsimp simp: context_equiv_def  type_equiv_def subtype_def)
       apply(clarsimp simp: context_equiv_def type_equiv_def subtype_def)
      apply(blast intro: subset_entailment)
     apply(blast intro: subset_entailment)
    (* need to be careful how we unfold here as otherwise the tactics get overwhelmed *)
    apply clarsimp
    apply(subst tyenv_wellformed_def) 
    apply(clarsimp simp: mds_consistent_def types_wellformed_def type_wellformed_def types_stable_def)
    apply(simp add: tyenv_wellformed_def mds_consistent_def)
    apply blast
   apply clarsimp
   apply(subst tyenv_wellformed_def) 
   apply(clarsimp simp: mds_consistent_def types_wellformed_def type_wellformed_def types_stable_def)
   apply(simp add: tyenv_wellformed_def mds_consistent_def)
   apply blast
  apply(rule assign⇩1)
      apply simp+
    apply(rule type_aexpr_Load')
     apply simp
    apply simp
   apply simp
  apply blast
  done


lemma read_buffer_typed':
  "Γ = (λ_. None) ⟹ 𝒮 = ({},{}) ⟹ P = {} ⟹ 
  ∃Γ' 𝒮' P'. has_type Γ 𝒮 P read_buffer Γ' 𝒮' P'"
  by (has_type_tac prog: read_buffer_def 
       aexpr:type_aexpr_Load' type_aexpr_Load 
       bexpr:type_bexprI)
 
 
lemma write_buffer_typed':
  "Γ = (λ_. None) ⟹ 𝒮 = ({},{}) ⟹ P = {} ⟹ 
  ∃Γ' 𝒮' P'. has_type Γ 𝒮 P write_buffer Γ' 𝒮' P'"
  apply (has_type_tac prog: write_buffer_def aexpr:type_aexpr_Load' type_aexpr_Load bexpr:type_bexprI)
  apply (if_type_tac bexpr: type_bexprI
          custom_if: if_type[where Γ'''="[temp ↦ dma_type buffer]" and P'''="{}"])
  apply (has_type_tac' aexpr:type_aexpr_Load' type_aexpr_Load bexpr:type_bexprI)
  done

end

end