Theory Preliminaries

(*
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)
*)
section ‹Preliminaries›
theory Preliminaries
imports Main
begin

text ‹Possible modes for variables:›
datatype Mode = AsmNoReadOrWrite | AsmNoWrite | GuarNoReadOrWrite | GuarNoWrite

text ‹We consider a two-element security lattice:›
datatype Sec = High | Low


text ‹@{term Sec} forms a (complete) lattice:›
instantiation Sec :: complete_lattice
begin

definition top_Sec_def: "top = High"
definition sup_Sec_def: "sup d1 d2 = (if (d1 = High ∨ d2 = High) then High else Low)"
definition inf_Sec_def: "inf d1 d2 = (if (d1 = Low ∨ d2 = Low) then Low else High)"
definition bot_Sec_def: "bot = Low"
definition less_eq_Sec_def: "d1 ≤ d2 = (d1 = d2 ∨ d1 = Low)"
definition less_Sec_def: "d1 < d2 = (d1 = Low ∧ d2 = High)"
definition Sup_Sec_def: "Sup S = (if (High ∈ S) then High else Low)"
definition Inf_Sec_def: "Inf S = (if (Low ∈ S) then Low else High)"

instance
  apply (intro_classes)
                 using Sec.exhaust less_Sec_def less_eq_Sec_def inf_Sec_def sup_Sec_def apply auto[10]
       apply (metis Inf_Sec_def Sec.exhaust less_eq_Sec_def)
      apply (metis Inf_Sec_def Sec.exhaust less_eq_Sec_def)
     using Sec.exhaust less_Sec_def less_eq_Sec_def inf_Sec_def sup_Sec_def Inf_Sec_def Sup_Sec_def top_Sec_def bot_Sec_def 
     by auto
end

text ‹Memories are mappings from variables to values›
type_synonym ('var, 'val) Mem = "'var ⇒ 'val"

text ‹A mode state maps modes to the set of variables for which the
  given mode is set.›
type_synonym 'var Mds = "Mode ⇒ 'var set"

text ‹Local configurations:›
type_synonym ('com, 'var, 'val) LocalConf = "('com × 'var Mds) × ('var, 'val) Mem"

text ‹Global configurations:›
type_synonym ('com, 'var, 'val) GlobalConf = "('com × 'var Mds) list × ('var, 'val) Mem"

text ‹A locale to fix various parametric components in Mantel et. al, and assumptions
  about them:›
locale sifum_security_init =
  fixes dma :: "('Var,'Val) Mem ⇒ 'Var ⇒ Sec"
  fixes 𝒞_vars :: "'Var ⇒ 'Var set"
  fixes 𝒞 :: "'Var set" (* classification control variables *)
  fixes eval :: "('Com, 'Var, 'Val) LocalConf rel"
  fixes some_val :: "'Val"
  fixes INIT :: "('Var,'Val) Mem ⇒ bool"
  assumes deterministic: "⟦ (lc, lc') ∈ eval; (lc, lc'') ∈ eval ⟧ ⟹ lc' = lc''"
  assumes finite_memory: "finite {(x::'Var). True}"
  defines "𝒞 ≡ ⋃x. 𝒞_vars x"
  assumes 𝒞_vars_𝒞: "x ∈ 𝒞 ⟹ 𝒞_vars x = {}"
  assumes dma_𝒞_vars: "∀x∈𝒞_vars y. mem⇩1 x = mem⇩2 x ⟹ dma mem⇩1 y = dma mem⇩2 y"
  assumes 𝒞_Low: "∀x∈𝒞. dma mem x = Low"

locale sifum_security = sifum_security_init dma 𝒞_vars 𝒞 eval some_val "λ_.True"
  for dma :: "('Var,'Val) Mem ⇒ 'Var ⇒ Sec"
  and 𝒞_vars :: "'Var ⇒ 'Var set"
  and 𝒞 :: "'Var set" (* classification control variables *)
  and eval :: "('Com, 'Var, 'Val) LocalConf rel"
  and some_val :: "'Val"

context sifum_security_init begin

lemma 𝒞_vars_subset_𝒞:
  "𝒞_vars x ⊆ 𝒞"
  by(force simp: 𝒞_def)

lemma dma_𝒞:
  "∀x∈𝒞. mem⇩1 x = mem⇩2 x ⟹ dma mem⇩1 = dma mem⇩2"
  proof
    fix y
    assume "∀x∈𝒞. mem⇩1 x = mem⇩2 x"
    hence "∀x∈𝒞_vars y. mem⇩1 x = mem⇩2 x"
      using 𝒞_vars_subset_𝒞 by blast
    thus "dma mem⇩1 y = dma mem⇩2 y"
      by(rule dma_𝒞_vars)
  qed

end

(* induction tools, moved up as far as possible *)

lemma my_trancl_induct [consumes 1, case_names base step]:
  "⟦(a, b) ∈ r⇧+; 
    P a ; 
   ⋀x y. ⟦(x, y) ∈ r; P x⟧ ⟹ P y⟧ ⟹ P b"
  by (induct rule: trancl.induct, blast+)
  
lemma my_trancl_step_induct [consumes 1, case_names base step]:
  "⟦(a, b) ∈ r⇧+; 
   ⋀x y. (x, y) ∈ r ⟹ P x y;
   ⋀x y z. P x y ⟹ (y, z) ∈ r ⟹ P x z⟧ ⟹ P a b"
  by (induct rule: trancl_induct, blast+)
  
lemma my_trancl_big_step_induct [consumes 1, case_names base step]:
  "⟦(a, b) ∈ r⇧+; 
   ⋀x y. (x, y) ∈ r ⟹ P x y;
   ⋀x y z. (x, y) ∈ r⇧+ ⟹ P x y ⟹ (y, z) ∈ r ⟹ P y z ⟹ P x z⟧ ⟹ P a b"
  by (induct rule: trancl.induct, blast+)
  
lemmas my_trancl_step_induct3 = 
  my_trancl_step_induct[of "((ax,ay), az)" "((bx,by), bz)", split_format (complete),
                 consumes 1, case_names step]
  
lemmas my_trancl_big_step_induct3 = 
  my_trancl_big_step_induct[of "((ax,ay), az)" "((bx,by), bz)", split_format (complete),
                 consumes 1, case_names base step]

end