Theory RobustCompilation

theory RobustCompilation
  imports
    HOL.Real
begin

section "Basic Notions"

datatype ('color) prgm = Prgrm 'color
datatype ('color) ctxt = Ctxt 'color
datatype ('color) whle = Whle 'color

type_synonym ('b,'r) comp = "'b prgm ⇒ 'r prgm"

(* TODO see if we can get rid of this *)
partial_function (tailrec) oddity :: "nat => nat"
where "oddity arg = (case arg of (Suc (Suc n)) => n | 0 => 0 )"

consts 
  link:: "'b ctxt ⇒ 'b prgm ⇒ 'b whle" (infixl "><" 55) 
  ple :: "'c whle ⇒ 'd whle ⇒ bool" (infixl "≲" 50)

section "Refinement"

abbreviation RRgen:: "('r whle ⇒ 'b whle ⇒ bool) ⇒ 'r prgm ⇒ 'b prgm ⇒ bool" 
  where
  "RRgen rel (p::'r prgm) (f::'b prgm) ≡ 
    ∀ (A::'r ctxt). ∃ (S::'b ctxt). rel (A >< p) (S >< f)"

abbreviation RR:: "'r prgm ⇒ 'b prgm ⇒ bool" ("_ robustly-refines _" [20,20] 17)
  where
  "RR p f ≡ RRgen ple p f"

text "Refinement by trace inclusion"

consts
  leadsto :: "'a whle ⇒ 't ⇒ bool" (infixr "↝" 51)
  prefix :: "'t ⇒ bool"

fun Behav :: "'a whle ⇒ 't set"
  where
    "Behav(W) = { t . W ↝ t}"

section "RSCHP"

abbreviation RSCHPrel
  where
  "RSCHPrel (t:: 't itself) W W' ≡ 
        (∀ m :: 't . prefix m ⟶  W ↝ m ⟶  W' ↝ m)"

abbreviation RSCHP
  where
  "RSCHP C (t:: 't itself) ≡ ∀ P . RRgen (RSCHPrel (t:: 't itself)) (C P) P"

(*
abbreviation RSCHPXrel 
  where
  "RSCHPXrel (t:: 't itself) T (W::'r whle) (W'::'b whle) ≡
         Behav(W)⊆ T ⟶ Behav(W')⊆T"


abbreviation RSCHPX (* Equivalent to other definition of RSCHPX *)
  where
  "RSCHPX (X:: 't set set set) C (t:: 't itself) ≡ ∀ T ∈ X . ∀ P . RRgen (RSCHPXrel (t:: 't itself) T) (C P) P"
*)

section "RHP"

abbreviation RHPrel
  where
  "RHPrel (t:: 't itself) W W' ≡ 
        (∀ m :: 't . prefix m ⟶  (W ↝ m ⟷ W' ↝ m))"

abbreviation RHP
  where
  "RHP C (t:: 't itself) ≡ ∀ P . RRgen (RHPrel (t:: 't itself)) (C P) P"


section "RHP(X), for computational UC"

type_synonym ('t) traceprop = "('t) set"
type_synonym ('t) hyperprop = "('t set) set"

abbreviation RHPXj (* definition of RHP(X) from journey paper, to prove equivalence *)
  where
  "RHPXj (t:: 't itself) (X:: ('t hyperprop) set) C  ≡
   ∀ H ∈ X . ∀ P . 
      (∀ S . Behav(S >< P)∈H) ⟶ (∀ A . Behav(A >< C P)∈H)"

abbreviation RHPXrel 
  where
  "RHPXrel (t:: 't itself) H (W::'r whle) (W'::'b whle) ≡
         Behav(W')∈ H ⟶ Behav(W)∈H"

abbreviation RHPX (* definition of RHP(X) that uses RRgen for uniform structure here *)
  where
  "RHPX (t:: 't itself) (X:: ('t hyperprop) set) C ≡
    ∀ H∈X . ∀P . RRgen (RHPXrel t H) (C P) P"

lemma "RHPXj t X C = RHPX t X C"
proof -
  fix t
  have "RHPXj t X C = (∀H∈X. ∀P A. 
        (∀S. Behav (S >< P)∈ H) ⟶ Behav (A >< C P) ∈ H)" by auto
  moreover have "... = 
  (∀H∈X. ∀P A. ∃ S .(Behav (S >< P)∈ H) ⟶ Behav (A >< C P) ∈ H)" by auto
  ultimately show ?thesis by auto
qed

text "Generalized robust preservation properties"

abbreviation RRHCrel
  where
  "RRHCrel (R :: 't set ⇒ 't set ⇒ bool) W W' ≡ R (Behav W) (Behav W')"

abbreviation RRHC
  where
  "RRHC R C ≡ ∀ P . RRgen (RRHCrel R) (C P) P"

fun r_hyper
  where "r_hyper (R::'t set ⇒ 't set ⇒ bool) F = {T . ∃ S . R T (Behav(S >< F))}"

fun r_hyperSet
  where "r_hyperSet (lang::'l itself) (R::'t set ⇒ 't set ⇒ bool) = {H . ∃ (F::'l prgm) . H = r_hyper R F}"

fun r_emul
  where "r_emul R (P::'p prgm) (ft::'f itself) = {F::'f prgm . ∀ A . Behav(A >< P) ∈ r_hyper R F}"

text "Prove these properties are equivalent to each other"

declare [[show_types ]]

locale GenRC =
  fixes R :: "'t set ⇒ 't set ⇒ bool"
  assumes r_refl : "∀ T . R T T"
  assumes r_trans : "∀ T0 T1 T2 . R T0 T1 ⟶ R T1 T2 ⟶ R T0 T2"
  fixes C :: "('f,'p) comp"

begin

lemma EmulSet_contain_subset:
  fixes P :: "'p prgm"
  fixes F :: "'f prgm"
  fixes ft :: "'f itself"
  shows "F ∈ r_emul R P ft ⟷ (r_emul R F ft) ⊆ (r_emul R P ft)"
  using r_refl r_trans by fastforce

theorem RHPXeqEmul:
  fixes tt::"'t itself"
  fixes ft :: "'f itself"
  shows "RHPX tt (r_hyperSet ft R) C = (∀ P . P ∈ r_emul R (C P) ft)"
proof-
  have "RHPX tt (r_hyperSet ft R) C
      = (∀ H. (∃ (F::'f prgm). H = r_hyper R F) ⟶ (∀ P A. ∃S. Behav (S >< P) ∈ H ⟶ Behav (A >< C P) ∈ H))"
    by simp
  also have "... =  (∀ P (F::'f prgm) A. ∃S. Behav (S >< P) ∈ r_hyper R F ⟶ Behav (A >< C P) ∈ r_hyper R F)"
    by blast
  also have "... = (∀ P (F::'f prgm). (F ∈ r_emul R P ft) ⟶ (F ∈ r_emul R (C P) ft))"
    by simp
  also have "... = (∀ P . r_emul R P ft ⊆ r_emul R (C P) ft)" by auto
  also have "... = (∀ P . P ∈ r_emul R (C P) ft)"
    using r_refl r_trans EmulSet_contain_subset by (metis (mono_tags, lifting))
  finally show ?thesis by auto
qed

theorem RHCeqEmul:
  fixes ft :: "'f itself"
  shows "RRHC R C = (∀P. P ∈ r_emul R (C P) ft)"
proof-
  have "RRHC R C = (∀P A . ∃ (S::'f ctxt) . R (Behav(A >< C P)) (Behav(S >< P)))"
    by simp
  also have "... = (∀P . P ∈ r_emul R (C P) ft)" by simp
  finally show ?thesis by auto
qed

theorem RHPXeqRRHC:
  fixes tt::"'t itself"
  fixes ft :: "'f itself"
  shows "RHPX tt (r_hyperSet ft R) C = RRHC R C"
proof-
  have "RHPX tt (r_hyperSet ft R) C = (∀ P . P ∈ r_emul R (C P) ft)"
    using r_refl r_trans RHPXeqEmul by auto
  also have "... = RRHC R C" using RHCeqEmul by auto
  finally show ?thesis by auto
qed

end

lemma RRHC_multiRel:
  fixes R0 R1 :: "'t set ⇒ 't set ⇒ bool"
  assumes Strength: "∀ T0 T1 . R0 T0 T1 ⟶ R1 T0 T1"
  fixes C :: "('f,'p) comp"
  assumes RHC_R0: "RRHC R0 C"
  shows "RRHC R1 C"
  using RHC_R0 Strength by blast

end