Theory Type_System_example

(*
Title: Strong-Security
Authors: Sylvia Grewe, Alexander Lux, Heiko Mantel, Jens Sauer
*)
theory Type_System_example
imports Type_System Expr Domain_example 
begin

― ‹When interpreting, we have to instantiate the type for domains.› 
― ‹As an example, we take a type containing 'low' and 'high' as domains.›


consts DA :: "('id,Dom) DomainAssignment"
consts BMap :: "'val ⇒ bool"

abbreviation d_indistinguishable' :: "('id,'val) Expr ⇒ Dom
  ⇒ ('id,'val) Expr ⇒ bool"
( "(_ ≡⇘_⇙ _)" )
where 
"e1 ≡⇘d⇙ e2 
  ≡ Strongly_Secure_Programs.d_indistinguishable ExprEval DA d e1 e2"

abbreviation relatedbyUSdB' :: "(('id,'val) Expr, 'id) MWLfCom list 
  ⇒ Dom ⇒ (('id,'val) Expr, 'id) MWLfCom list ⇒ bool" (infixr "≈⇘_⇙" 65)
where "V ≈⇘d⇙ V' ≡ (V,V') ∈ Strong_Security.USdB 
  (MWLf_semantics.MWLfSteps_det ExprEval BMap) DA d"

― ‹Security typing rules for expressions - will be part of a side condition›
inductive 
ExprSecTyping :: "('id, 'val) Expr ⇒ Dom set ⇒ bool"
("⊢⇘ℰ⇙ _ : _")
where 
Consts: "⊢⇘ℰ⇙ (Const v) : {d}" |
Vars: "⊢⇘ℰ⇙ (Var x) : {DA x}" |
Ops: "∀i < length arglist. ⊢⇘ℰ⇙ (arglist!i) : (dl!i)
  ⟹ ⊢⇘ℰ⇙ (Op f arglist) : (⋃{d. (∃i < length arglist. d = (dl!i))})"

definition synAssignSC :: "'id ⇒ ('id, 'val) Expr ⇒ bool"
where
"synAssignSC x e ≡ ∃D. (⊢⇘ℰ⇙ e : D ∧ (∀d ∈ D. (d ≤ DA x)))"

definition synWhileSC :: "('id, 'val) Expr ⇒ bool"
where
"synWhileSC e ≡ ∃D. (⊢⇘ℰ⇙ e : D ∧ (∀d∈D. ∀d'. d ≤ d'))"

definition synIfSC :: "('id, 'val) Expr ⇒ (('id, 'val) Expr, 'id) MWLfCom 
  ⇒ (('id, 'val) Expr, 'id) MWLfCom ⇒ bool" 
where
"synIfSC e c1 c2 ≡ 
 ∀d. (¬ (e ≡⇘d⇙ e) ⟶ [c1] ≈⇘d⇙ [c2])"

lemma ExprTypable_with_smallerD_implies_d_indistinguishable:
"⟦ ⊢⇘ℰ⇙ e : D'; ∀d' ∈ D'. d' ≤ d ⟧ ⟹ e ≡⇘d⇙ e" 
proof (induct rule: ExprSecTyping.induct, 
    simp_all add: Strongly_Secure_Programs.d_indistinguishable_def 
    Strong_Security.d_equal_def, auto)
  fix dl and arglist::"(('id, 'val) Expr) list" and f::"'val list ⇒ 'val" 
    and m1::"('id,'val) State" and m2::"('id,'val) State"
  assume main: "∀i < length arglist. ⊢⇘ℰ⇙ arglist!i : dl!i ∧
    ((∀d' ∈ (dl!i). d' ≤ d) ⟶ 
    (∀m m'. (∀x. DA x ≤ d ⟶ m x = m' x) 
    ⟶ ExprEval (arglist!i) m = ExprEval (arglist!i) m'))"
  assume smaller: "∀D. (∃i < length arglist. D = (dl!i)) 
    ⟶ (∀d'∈D. d' ≤ d)"
  assume eqstate: "∀x. DA x ≤ d ⟶ m1 x = m2 x"
  
  from smaller have irangesubst: 
    "∀i < length arglist. ∀d' ∈ (dl!i). d' ≤ d"
    by auto
        
  with eqstate main have 
    "∀i < length arglist. ExprEval (arglist!i) m1 
    = ExprEval (arglist!i) m2"
    by force
 
  hence substmap: "(ExprEvalL arglist m1) = (ExprEvalL arglist m2)" 
    by (induct arglist, auto, force)
    
  show "f (ExprEvalL arglist m1) = f (ExprEvalL arglist m2)"
    by (subst substmap, auto)
qed

interpretation Type_System_example: Type_System ExprEval BMap DA
  synAssignSC synWhileSC synIfSC
by (unfold_locales, simp add: synAssignSC_def,
  metis ExprTypable_with_smallerD_implies_d_indistinguishable,
  simp add: synWhileSC_def,
  metis ExprTypable_with_smallerD_implies_d_indistinguishable,
  simp add: synIfSC_def, metis)

end