Theory compUCisRC

theory compUCisRC
  imports
    RobustCompilation
    UC
    Utils
    HOL.Fun
begin

context compUC
begin

section "Computational UC"

abbreviation comp_emulates:: "'uc prgm ⇒ 'uc prgm ⇒ bool" (infixl "computationally-emulates" 45)
  where
  "comp_emulates P F ≡ ∀ A . ∃ (S::'uc ctxt) . ∀ Z ∈ ZClass.
   PrExec Z A P True ≈ PrExec Z S F True"

fun tprob :: "('t×real×nat) ⇒ real"
  where "tprob (t,p,n) = p" 

fun ttrace :: "('t×real×nat) ⇒ 't"
  where "ttrace (t,p,n) = t" 

lemma sum_reindex:
  assumes "bij_betw f A B"
    shows "sum (g ∘ f) A = sum g B"
by (simp add: assms sum.reindex_bij_betw)

(* interpret T for a fixed Z and n as a random variable *)
fun RV :: "('t×real×nat) set ⇒ 'env ⇒ nat ⇒ real"
  where "RV T Z n = (case (csum2 tprob {(t,p,n') ∈ T . n'=n ∧ prefix t ∧ β(t) ∧ possible Z t n})
    of  None ⇒ -1 | Some x ⇒ x)"

lemma RV_Behav:
  fixes A:: "'uc ctxt"
  fixes P:: "'uc prgm"
  fixes Z:: "'env"
  assumes Znonprob: "nonprobabilistic Z"
  shows "RV (Behav (A >< P)) Z = PrExec Z A P True"
proof -
  let ?T = "Behav (A >< P)"
  have "∀ n .( (RV(?T) Z n) = (PrExec Z A P True n))" 
  proof
    fix n
    let ?S0 = "{(t,p,n') ∈ ?T . n'=n ∧ prefix t ∧ β(t) ∧ possible Z t n}"
    have L1: "RV ?T Z n  = (case (csum2 tprob ?S0) of  None ⇒ -1 | Some x ⇒ x)" by simp
    
    let ?S1 = "{(t,p,n') .  PrExecT (Zcan t) A P t n' = p ∧ p>0 ∧ n'=n ∧ prefix t ∧ β(t) ∧ possible Z t n}"
    let ?S2 = "{t . PrExecT (Zcan t) A P t n >0  ∧ prefix t ∧ β(t) ∧ possible Z t n}"
    let ?S2' = "{t . PrExecT (Zcan t) A P t n ≠ 0  ∧ prefix t ∧ β(t) ∧ possible Z t n}"
    let ?S3 = "{t .  prefix t ∧ β(t) ∧ possible Z t n}" 
    let ?S4 = "{t .  prefix t ∧ β(t)}" 

    have "?S0 = ?S1" using relation_uc by simp
    hence "csum2 tprob ?S0 = csum2 tprob ?S1" by auto
    moreover have
       "... = csum (λ t . PrExecT (Zcan t) A P t n) ?S2"
     proof-
        let ?f = "ttrace"
        let ?g = "λ t . PrExecT (Zcan t) A P t n"
        have "bij_betw ?f ?S1 ?S2" 
          proof -
            have A: "inj_on ?f ?S1" by (simp add: inj_on_def) 
            have B: "?f ` ?S1 ⊆ ?S2" by force 
            have C: "?f ` ?S1 ⊇ ?S2" by force            
            from A B C show ?thesis by (simp add: bij_betw_def)        
          qed
        from this csum_reindex have "csum2 (?g ∘ ?f) ?S1 = csum ?g ?S2" by auto
        thus ?thesis using csum2_cong by (smt (z3) case_prodE comp_apply mem_Collect_eq tprob.simps ttrace.simps)  
      qed    
    moreover have "... = csum (λ t . PrExecT (Zcan t) A P t n) ?S3 "
      using Zcan_possible possible2 by force     
    moreover have "... = csum (λ t . PrExecT Z A P t n) ?S3"
      using Znonprob Zcan_nonprob Zcan_possible env_fixes_io by presburger 
    moreover have "... = csum (λ t . PrExecT Z A P t n) ?S4 "
    proof -
      from possible PrExecT_unit_interval_min
        have "∀ t. ¬ (possible Z t n) ⟶ PrExecT Z A P t n = 0" 
          by (metis order_less_le)
        thus ?thesis
          by (metis (mono_tags, opaque_lifting) Zcan_nonprob Zcan_possible assms env_fixes_io possible possible2) 
      qed
    ultimately have "csum2 tprob ?S0 = csum (λ t . PrExecT Z A P t n) ?S4 " by auto
    thus "RV ?T Z n = PrExec Z A P True n"  using L1 prefixes_contain_final_bit by simp  
  qed
  hence "RV(?T) Z = PrExec Z A P True " by blast
  thus ?thesis by simp
qed

fun compindstep
  where "compindstep T' =  { T . (∀ Z . nonprobabilistic Z ⟶ RV T Z ≈ RV T' Z )}"

lemma compindstep_mono:
  "T ∈ compindstep T"
proof -
  have "∀ Z . RV T Z ≈ RV T Z" by auto
  thus ?thesis by auto
qed

lemma Behav_to_ind:
  fixes A A':: "'uc ctxt"
  fixes P P':: "'uc prgm"
  assumes A: "Behav(A >< P) ∈ compindstep (Behav (A' >< P'))"
  shows "∀ Z . nonprobabilistic Z ⟶ PrExec Z A P True ≈ PrExec Z A' P' True"
proof -
  let ?T="Behav(A >< P)"
  let ?T'="Behav(A' >< P')"
  from A have " ∀ Z . ( nonprobabilistic Z ⟶ RV ?T Z ≈ RV ?T' Z) " by simp
  thus ?thesis using RV_Behav by metis
qed

text "To prove equivalence using the generalizations, define a compeq relation"

fun compeq (infix "≅" 50)
  where
  "T1 ≅ T2 =
     (∀ Z ∈ ZClass . nonprobabilistic Z ⟶ (RV T1 Z) ≈ (RV T2 Z))"

abbreviation compRHC where "compRHC C ≡ RRHC (≅) C"

fun compHyper
  where "compHyper P = {T . ∃ S . ∀ Z ∈ ZClass . nonprobabilistic Z ⟶ (RV T Z) ≈ PrExec Z S P True }"

abbreviation compHyperSet :: "(('t × real × nat) hyperprop set)"
  where "compHyperSet ≡ {H . ∃ F. H = compHyper F}"

lemma compHyperRHyper:
  "compHyper (F::'uc prgm) = r_hyper (≅) F"
proof-
  have "compHyper F = {T . ∃ (S::'uc ctxt) . ∀ Z ∈ ZClass . nonprobabilistic Z ⟶ (RV T Z) ≈ (RV (Behav (S><F)) Z)}" 
    using RV_Behav by simp
  also have " ... = r_hyper (≅) F" by simp
  finally show ?thesis by auto
qed

theorem compHyperRHyper_Sets:
  "compHyperSet = (r_hyperSet (uctype::'uc itself) (≅))"
  using compHyperRHyper by simp

text "Now we show compRHC and RHPX compHyperSet equivalent"

(* Ethan: I wanted to embed this into the proof below,
      but trying to do sub-proofs by contradiction didn't work the way I expected, so I pulled it out. *)
lemma nonprob_env_one:
  fixes A S :: "'uc ctxt"
  assumes Znonprob: " ∀Z ∈ ZClass . nonprobabilistic Z ⟶ PrExec Z A P True ≈ PrExec Z S F True"
  shows "∃ (S'::'uc ctxt) . ∀ Z ∈ ZClass . PrExec Z A P True ≈ PrExec Z S' F True"
proof (rule ccontr)
  assume CF: "∄ (S'::'uc ctxt) . ∀ Z ∈ ZClass . PrExec Z A P True ≈ PrExec Z S' F True"
  thus False
  proof-
    from CF have "∀ (S'::'uc ctxt) . ∃ Z ∈ ZClass . ¬ (PrExec Z A P True ≈ PrExec Z S' F True)" by auto
    hence "∃ Z ∈ ZClass . ¬ (PrExec Z A P True ≈ PrExec Z S F True)" by auto
    then obtain Z :: "'env" where "Z ∈ ZClass ∧ ¬ (PrExec Z A P True ≈ PrExec Z S F True)" by auto
    hence "∃ Z' ∈ ZClass . ¬ (PrExec Z' A P True ≈ PrExec Z' S F True) ∧ nonprobabilistic Z'"
      using nonprobabilistic_envs_are_sound_comp by blast
    then obtain Z' :: "'env" where BadZ : "Z' ∈ ZClass ∧ ¬ (PrExec Z' A P True ≈ PrExec Z' S F True) ∧ nonprobabilistic Z'" by auto
    from this Znonprob have "PrExec Z' A P True ≈ PrExec Z' S F True" by auto
    from this BadZ show False by auto
  qed
qed

lemma nonprob_env:
  fixes P F :: "'uc prgm"
  fixes A :: "'uc ctxt"
  shows "(∃ S . ∀ Z ∈ ZClass . PrExec Z A P True ≈ PrExec Z S F True)
      = (∃ S . ∀ Z ∈ ZClass . nonprobabilistic Z ⟶ PrExec Z A P True ≈ PrExec Z S F True)"
proof
  assume "(∃ S . ∀ Z ∈ ZClass . PrExec Z A P True ≈ PrExec Z S F True)"
  thus "(∃ S . ∀ Z ∈ ZClass . nonprobabilistic Z ⟶ PrExec Z A P True ≈ PrExec Z S F True)" by auto
next
  assume "(∃ S . ∀ Z ∈ ZClass . nonprobabilistic Z ⟶ PrExec Z A P True ≈ PrExec Z S F True)"
  thus "(∃ S . ∀ Z ∈ ZClass . PrExec Z A P True ≈ PrExec Z S F True)" using nonprob_env_one by auto
qed

lemma UCisEmul:
  fixes P F :: "'uc prgm"
  shows "(F ∈ r_emul (≅) P uct) = (P computationally-emulates F)"
proof-
  have "(F ∈ r_emul (≅) P uct) = (∀ A . ∃ (S::'uc ctxt) . ∀ Z ∈ ZClass.
          nonprobabilistic Z ⟶ (RV (Behav(A >< P)) Z) ≈ (RV (Behav(S >< F)) Z))"
    by simp
  also have "... = (∀ A . ∃ (S::'uc ctxt) . ∀ Z ∈ ZClass. nonprobabilistic Z ⟶ PrExec Z A P True ≈ PrExec Z S F True)"
    using RV_Behav by auto
  also have "... = (∀ A . ∃ (S::'uc ctxt) . ∀ Z ∈ ZClass. PrExec Z A P True ≈ PrExec Z S F True)"
    using nonprob_env by auto
  finally show ?thesis by simp
qed

end

text "Specialize the robust compilation results to computations equivalence"

context compUCisRC
begin

(* Prove that ≈ is an equivalence relation. Transitivity is nontrivial. *)
lemma comp_ind_refl: "f ≈ f" by simp

lemma comp_ind_sym: "f ≈ g ⟶ g ≈ f" by (simp add: abs_minus_commute)

lemma frac_pow_le:
  fixes n k :: "nat"
  assumes nTwo: "n > 1"
  shows "2/(n^(k+1)) ≤ 1/(n^k)"
proof-
  have "0 ≤ 2/n" by auto
  moreover have "2/n ≤ 1" using nTwo by auto
  ultimately have "2/n * 1/(n^k) ≤ 1/(n^k)" using divide_right_mono by fastforce
  thus ?thesis by auto
qed

lemma comp_ind_trans_help:
  fixes f g h :: "nat ⇒ real"
  fixes k N0 N1 :: "nat"
  assumes compFG: "∀ n > N0 . abs((f n) - (g n)) < 1/(n^(k+1))"
  assumes compGH: "∀ n > N1 . abs((g n) - (h n)) < 1/(n^(k+1))"
  shows "∃ (N::nat) . ∀ (n::nat) > N . abs((f n) - (h n)) < 1/(n^k)"
proof
  let ?N = "max 1 (max N0 N1)"
  show "∀ (n::nat) > ?N . abs((f n) - (h n)) < 1/(n^k)"
  proof fix n :: nat show "n > ?N ⟶ abs((f n) - (h n)) < 1/(n^k)"
    proof
      assume nLarge: "n > ?N"
      then have nGt1: "n > 1" by auto
      moreover have "abs((f n) - (g n)) < 1/(n^(k+1))" using nLarge compFG by auto
      moreover have "abs((g n) - (h n)) < 1/(n^(k+1))" using nLarge compGH by auto
      ultimately have "abs((f n) - (h n)) < 2/(n^(k+1))" by fastforce
      thus "abs((f n) - (h n)) < 1/(n^k)" using nGt1 frac_pow_le of_nat_power by (smt (verit))
    qed
  qed
qed

lemma comp_ind_trans:
  assumes compFG: "f ≈ g"
  assumes compGH: "g ≈ h"
  shows "f ≈ h"
proof
  fix k::"nat"
  obtain N0::"nat" where N0bound: "∀ n > N0 . abs((f n) - (g n)) < 1/(n^(k+1))"
    using compFG of_nat_power by metis
  obtain N1::"nat" where N1bound: "∀ n > N1 . abs((g n) - (h n)) < 1/(n^(k+1))"
    using compGH of_nat_power by metis
  show "∃ N . ∀ n > N . abs((f n) - (h n)) < (1::real)/(n^k)"
    using N0bound N1bound comp_ind_trans_help by auto
qed

(* Specialize the general robust compilation result using ≅. *)
interpretation compRC : GenRC "(≅)" C
proof
  show "∀ T . T ≅ T" using comp_ind_refl by simp
next
  show "∀ T0 T1 T2 . T0 ≅ T1 ⟶ T1 ≅ T2 ⟶ T0 ≅ T2" using comp_ind_trans by auto
qed

theorem compRHCeqUC: "compRHC C = (∀ P . (C P) computationally-emulates P)"
proof-
  have "compRHC C = RRHC (≅) C" by simp
  also have "... = (∀ P . P ∈ r_emul (≅) (C P) (uct::'uc itself))" using compRC.RHCeqEmul by auto
  finally show ?thesis using UCisEmul by auto
qed

theorem compRHCisRHPX: "RHPX tt compHyperSet C = compRHC C"
proof-
  have "RHPX tt compHyperSet C = RHPX tt (r_hyperSet uct (≅)) C"
    using compHyperRHyper_Sets by simp
  also have "... = RRHC (≅) C" using compRC.RHPXeqRRHC by auto
  finally show ?thesis by simp
qed

theorem RHPXeqUC:
  "RHPX tt compHyperSet C = (∀ P . (C P) computationally-emulates P)"
  using compRHCisRHPX compRHCeqUC by auto

end

end