Theory perfUCisRC

theory perfUCisRC
  imports
    HOL.Real
    HOL.Option
    "HOL-Library.Monad_Syntax"
begin

section "Requirements for UC-style compositionality"

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

partial_function (tailrec) oddity :: "nat => nat"
where "oddity arg = (case arg of (Suc (Suc n)) => n | 0 => 0 )"

consts 
  call:: "'blue prgm ⇒ 'red prgm ⇒ 'blue prgm" (infixr "∘∘"  60)
  bigcall:: "'blue whle ⇒ 'red whle ⇒ 'blue whle" (infixr "∘∘∘" 52)
  par:: "'blue ctxt ⇒ 'red ctxt ⇒ 'blue ctxt" (infixl "∥" 60)
  link:: "'b ctxt ⇒ 'b prgm ⇒ 'b whle" (infixl "><" 55) 
  ple :: "'c whle ⇒ 'd whle ⇒ bool" (infixl "≲" 50)

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"


locale composition =
  assumes par_decomp: (* parallel decomposition (for pink programs using red programs) *)
  "∀ (A::'p ctxt) (P1::'p prgm) (P2::'r prgm) .
             ∃ (A1::'p ctxt) (A2::'r ctxt).
      A >< P1 ∘∘ P2 ≲ A1 ∥ A2 >< P1 ∘∘ P2"
  and inter_comp: (* intertwined composition (dito) *)
  "∀ (P1::'p prgm) (P2::'r prgm) 
              (A1::'p ctxt) (A2::'r ctxt).
       A1 ∥ A2 >< P1 ∘∘ P2 ≲ A1 >< P1 ∘∘∘ A2 >< P2"
  and inter_decomp: (* intertwined composition (for pink programs using blue programs) *)
  "∀ (P1::'p prgm) (P2::'b prgm) A1 A2 .
    A1 >< P1 ∘∘∘ A2 >< P2  ≲   A1 ∥ A2 >< P1 ∘∘ P2 "
  and  const_elim: (* constant elimination (for plugging substituting red with blue in pink contexts*)
  "∀ (redW::'r whle) (blueW::'b whle) (pinkW::'p whle) .
       ( (redW ≲ blueW) ⟶ ( pinkW ∘∘∘ redW ≲ pinkW ∘∘∘ blueW))"
  and transitivity [simp,trans]: (* transitivity of trace relation for pink programs *)
  "(W1::'p whle) ≲ (W2::'p whle)
    ⟹  W2 ≲ (W3::'p whle)  ⟹ W1 ≲ W3"

(* new axioms for dummy adversary theorem *)
locale dummy =
 (* dummy context and program *)
 fixes Pd::"'r prgm" (* Z→Pd ⇒ Z→Psub, A→Pd⇒ undefined  , Psub→Pd⇒ Psub⇒Z, *)
 fixes Ad::"'r ctxt" (* Z→Ad ⇒ Z→P,    P→ Ad ⇒ P→Z *)
 assumes adv_split:
 "∀ A (P::'r prgm) . ∃ A' . A >< Pd∘∘P ≲ (A' ∥ Ad) >< Pd∘∘P" 
 and prog_unsplit: 
 "∀(A::'r ctxt) (P::'b prgm) . ∃ (A'::'b ctxt) . A >< (Pd ∘∘ P) ≲ A' >< P"  
 and prog_split:
 "∀(A::'r ctxt) (P::'r prgm) . ∃ (A'::'r ctxt) . A >< P ≲  A' >< (Pd ∘∘ P)"  
 and  const_elim2: (* constant elimination for red contexts *)
 "∀(redW::'r whle) (blueW::'b whle) (W::'r whle) .
       ( (redW ≲ blueW) ⟶ ( W ∘∘∘ redW ≲ W ∘∘∘ blueW))"
 and inter_comp2: (* intertwined composition (for red  programs) *)
 "∀(P1::'r prgm) (P2::'r prgm) 
              (A1::'r ctxt) (A2::'r ctxt).
       A1 ∥ A2 >< P1 ∘∘ P2 ≲ A1 >< P1 ∘∘∘ A2 >< P2"
 and inter_decomp2: (* intertwined composition (for pink programs using blue programs) *)
 "∀ (P1::'r prgm) (P2::'b prgm) A1 A2.
    A1 >< P1 ∘∘∘ A2 >< P2  ≲  A1 ∥ A2 >< P1 ∘∘ P2 "
 and transitivity2 [trans]: (* transitivity of trace relation for red programs *)
 "⟦(W1::'r whle) ≲ (W2::'r whle); W2 ≲ (W3::'r whle)⟧ ⟹ W1 ≲ W3"
 and transitivity3 [trans]: (* transitivity of trace relation from red-to-red to red-to-blue  *)
 "⟦(W1'::'r whle) ≲ (W2'::'r whle); W2' ≲ (W3'::'b whle)⟧ ⟹ W1' ≲ W3'" 
context dummy
begin

theorem dummy:
  fixes P::"'r prgm"
  fixes F::"'b prgm"
  assumes A: " ∃ (S::'b ctxt) . Ad >< P ≲ S >< F"
shows "∀ (A::'r ctxt). ∃ (S::'b ctxt) . A >< P ≲ S >< F"
proof
  fix A 
  from prog_split obtain A' where "A >< P ≲ A' >< (Pd ∘∘ P)" by auto
  also obtain  A'' where "... ≲ A'' ∥ Ad >< Pd ∘∘ P" using adv_split by auto 
  also have "... ≲ (A'' >< Pd) ∘∘∘ (Ad >< P)" using inter_comp2 by blast
  also obtain S where "... ≲ (A'' >< Pd) ∘∘∘ (S >< F)" using A const_elim2 by blast
  also have "... ≲ ((A'' ∥ S) >< (Pd ∘∘ F))" using inter_decomp2 by blast
  also obtain S' where "... ≲ S' >< F" using prog_unsplit by blast
  finally have Almost:"A >< P ≲ S' >< F".
  thus "∃ (S::'b ctxt) . A >< P ≲ S >< F" by auto
 qed
end

context composition
begin

theorem composition:
  fixes P::"'r prgm"
  fixes F::"'b prgm"
  fixes R::"'p prgm"
  assumes A: "P robustly-refines F"
  shows "R ∘∘ P robustly-refines R ∘∘ F"
proof
  fix A
  from par_decomp obtain A1 A2 where "(A >< R ∘∘ P) ≲ ((A1::'p ctxt) ∥ (A2:: 'r ctxt) >< R ∘∘ P)" by presburger
  also have  "... ≲  (A1 >< R ∘∘∘ A2 >< P)" by (simp add:inter_comp)
  finally have OK:"(A >< R ∘∘ P) ≲  (A1 >< R ∘∘∘ A2 >< P)".
  
  from A obtain S2 where "(A2 >< P) ≲ (S2 >< F)" by auto
  hence "(A1 >< R) ∘∘∘ (A2 >< P) ≲ (A1 >< R) ∘∘∘ (S2 >< F)" by (simp add:const_elim)
  also have "... ≲ (A1 ∥ S2) >< (R ∘∘ F)" by (simp add:inter_decomp)
  finally have  "(A1 >< R) ∘∘∘ (A2 >< P) ≲ (A1 ∥ S2) >< (R ∘∘ F)".
  from this OK have "(A >< R ∘∘ P) ≲ (A1 ∥ S2) >< (R ∘∘ F)" by (meson transitivity)   
  then show "∃ S . (A >< R ∘∘ P) ≲ S >< (R ∘∘ F)" by metis
qed

end

section "Relating UC to RSCP"

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

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

(* We instantiate RSCHP from RRgen above for modularity. *)
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. (case C P of 
              Some CP ⇒  RRgen (RSCHPrel (t:: 't itself)) (CP) P
              | None ⇒ True 
            )"


locale UC = 
  fixes PrExec  :: "'env ⇒ 'uc ctxt ⇒ 'uc prgm ⇒ bool ⇒ real"
  fixes PrExecT :: "'env ⇒ 'uc ctxt ⇒ 'uc prgm ⇒ 't ⇒ real"
    (* Note: PrExec and PrExecT are total function. Hence, when the random vars Exec or ExecT are
       undefined, we give them probability zero.  *)
  fixes β :: "'t ⇒ bool" (* extracts final bit from trace *) 
  fixes Zcan :: "'t ⇒ 'env" (* canonical Z: produces messages to A and P as specified by t *)
  fixes nonprobabilistic :: "'env ⇒ bool"
  
  (* assumptions needed in both directions *)
  assumes relation_uc: (* We can define a semantic's from UC's semantics. *)
    "prefix t ⟶  (A >< P) ↝ (t,p) ≡ (PrExecT (Zcan t) A P t) = p ∧ p > 0"
  and prefix_iff_trace_is_prefix: (* PL-level trace (i.e., tuple) is prefix is the UC trace in it is. *)
    "prefix (t::'t,p::real) ≡ prefix t"

  (* only needed in RSCHPtoUC *)
  and prefixes_contain_final_bit: (* every finite trace contains the final bit *)
    "PrExec Z A P b = (∑ t ∈ {t. prefix t ∧ β t = b}  . PrExecT Z A P t)"
  and nonprobabilistic_envs_are_complete:
    "(∃ Z b. PrExec Z A P b ≠ PrExec Z S F b) ⟶ (∃ Z' . PrExec Z' A P True ≠ PrExec Z' S F True ∧ nonprobabilistic Z')"  
  and construct_canonical_env:
    "⟦nonprobabilistic Z;  prefix t; (∃ A' P' . PrExecT Z A' P' t > 0) ⟧ ⟹ PrExecT Z A P t = PrExecT (Zcan t) A P t"

  (* only needed in UCtoRSCHP *)
  and construct_canonical_env2:
    "⟦prefix t ⟧ ⟹ PrExecT (Zcan t) A P t = PrExec (Zcan t) A P True"

  (* axioms of probabilities *)
  and unit_interval: "PrExec Z A P True = 1- PrExec Z A P False"
  and unit_interval_min: "PrExec Z A P b ≥ 0"
  and PrExecT_unit_interval_min: "PrExecT Z A P t ≥ 0"

context UC
begin

abbreviation UCemulates:: "'uc prgm ⇒ 'uc prgm ⇒ bool" (infixl "UC-emulates" 45)
  where
  "UCemulates P F ≡ ∀ A . ∃ (S::'uc ctxt) . ∀ (Z::'env). 
    (PrExec Z A P True = PrExec Z S F True)"

lemma UCemulates_reflexive:
  fixes P::"'uc prgm"
  shows "P UC-emulates P"
  by metis

lemma difference_in_sum' :
  fixes f:: "'a ⇒ real"
  fixes g:: "'a ⇒ real"
  assumes A:" (∑ x∈ P . f x) > (∑x ∈ P . g x)"
  shows "∃ x∈P . f x > g x "
proof (rule ccontr)
  assume CF: "¬(∃ x∈P . f x > g x)"
  then show "False" 
  proof -
    from CF have "∀ x∈ P.  f x ≤  g x" by auto
    hence "∀x.  (x∈P ⟶ f x ≤ g x)" by simp
    from this sum_mono have "(∑x∈P. f x) ≤ (∑x∈P. g x)" by metis
    thus "False" using A by arith 
  qed
qed

lemma distinguishingZ_differentTrace:
  assumes A: "PrExecT Z A P t ≠ PrExecT Z S F t"
  and  B: "PrExecT Z A P t > 0"
  and Z : "nonprobabilistic Z"
  and T : "prefix t"
  shows "∃ p ::real .(A >< P) ↝ (t,p) ∧ ¬((S >< F) ↝ (t,p))"
proof -
  from B have t_possible_in_Z: "∃ A' P' . PrExecT Z A' P' t > 0" by auto
  from Z construct_canonical_env A T t_possible_in_Z have A':"PrExecT (Zcan t) A P t ≠ PrExecT (Zcan t) S F t" by fastforce
  from Z construct_canonical_env B T have B': "PrExecT (Zcan t) A P t > 0" by fastforce

  let ?p = "PrExecT (Zcan t) A P t"
  from relation_uc B' have Yes: "(A >< P) ↝ (t,?p)" by blast
  have No: "¬((S >< F) ↝ (t,?p))"
  proof (rule ccontr)
    assume C:"¬¬(S >< F) ↝ (t,?p)"
    show "False"
    proof -
      from C relation_uc T have "(PrExecT (Zcan t) S F t) = ?p ∧ ?p > 0" by metis
      hence "PrExecT (Zcan t) S F t = ?p" by auto
      from this A' show "False" by simp
    qed
  qed
  from Yes No show ?thesis by auto
qed

lemma greater_to_unequal_and_nonzero:
  assumes Greater: "PrExecT Z A P t > PrExecT Z S F t"
  shows "PrExecT Z A P t ≠ PrExecT Z S F t ∧ PrExecT Z A P t > 0"
proof -
  from PrExecT_unit_interval_min have "PrExecT Z S F t ≥  0" by simp
  from this Greater have B:"PrExecT Z A P t > 0" by fastforce 
  from this Greater show ?thesis by auto
qed

lemma PrExec_bit_selects_inequality:
  assumes "PrExec Z A P True ≠ PrExec Z' A' P' True"
  shows "∃ b. PrExec Z A P b > PrExec Z' A' P' b"
proof -
  consider 
        (A) "PrExec Z A P True > PrExec Z' A' P' True" 
      | (B) "PrExec Z A P True < PrExec Z' A' P' True"
     using assms by fastforce 
  then show ?thesis 
  proof cases
    case A then show ?thesis by auto
  next
    case B then show ?thesis using unit_interval by auto
  qed
qed

theorem RSCHPtoUC':
  fixes C ::"('uc,'uc) comp"
  fixes ttype :: "('t × real) itself"
  fixes P::"'uc prgm"
  fixes CP::"'uc prgm"
  assumes CP: "C P = Some CP"
  assumes A: "∀ A:: 'uc ctxt . ∃ S::'uc ctxt.
                 ∀ (m:: ('t × real)). prefix m ⟶  A >< CP ↝ m ⟶ S >< P ↝ m"
  shows " CP UC-emulates P"
proof (rule ccontr)
  assume CF: "¬ CP UC-emulates P"
  then show "False" 
  proof -
     from CF obtain A::"'uc ctxt" where CF1:"∀ (S::'uc ctxt) . ∃ (Z::'env).
       PrExec Z A (CP) True ≠ PrExec Z S P True" by auto

    from A obtain S::"'uc ctxt" where
      A1: "∀ (m:: ('t × real)). prefix m ⟶  A >< CP ↝ m ⟶ S >< P ↝ m" by blast

    from CF1 have "∃ Z . PrExec Z A CP True ≠ PrExec Z S P True"
      by auto
    hence 
       "∃ Z . PrExec Z A CP True ≠ PrExec Z S P True ∧ nonprobabilistic Z" 
      using nonprobabilistic_envs_are_complete by metis
    then obtain Z::"'env" 
      where "PrExec Z A (CP) True ≠ PrExec Z S P True"
      and Prob: "nonprobabilistic Z"
      by auto

    (* Need to select a bit here so that one is larger than the other.*)
    then obtain b::"bool" where "PrExec Z A (CP) b > PrExec Z S P b"
        using PrExec_bit_selects_inequality by metis
      hence "(∑ t∈ {t. prefix t ∧ β t= b} . 
        PrExecT Z A (CP) t) > (∑ t∈{t . prefix t ∧ β t = b} . PrExecT Z S P t)" 
      using prefixes_contain_final_bit by simp
    then obtain t::"'t" 
        where "PrExecT Z A (CP) t > PrExecT Z S P t"
        and Prefix: "prefix t" using difference_in_sum' by fastforce
    then have "PrExecT Z A (CP) t ≠ PrExecT Z S P t"
         and  "PrExecT Z A (CP) t > 0"
         using greater_to_unequal_and_nonzero by auto
    then obtain p::"real" where "A >< (CP) ↝ (t,p) ∧ ¬((S >< P) ↝ (t,p)) "
         using Prob Prefix distinguishingZ_differentTrace by metis
    moreover have "prefix (t,p)" using Prefix prefix_iff_trace_is_prefix by auto
    ultimately show False using A1 by fastforce
qed 
qed


theorem RSCHPtoUC:
  fixes C ::"('uc,'uc) comp"
  fixes ttype :: "('t × real) itself"
  assumes A: "RSCHP C ttype"
  shows "∀ (P::'uc prgm) . case C P of Some CP ⇒ CP UC-emulates P | None ⇒ True"
proof
  fix P
  show "case C P of Some CP ⇒ CP UC-emulates P | None ⇒ True"
  proof (cases "C P")
    case None
    then show ?thesis by simp
  next
    case A1: (Some CP)
    hence A2:"
         ∀A. ∃S. ∀m. prefix (m::('t × real)) ⟶
                           A >< CP ↝ m ⟶ S >< P ↝ m
         " by (smt (verit, best) A1 assms option.simps(5))  
    then show ?thesis using RSCHPtoUC' A1 A2 by simp 
  qed
qed

theorem UCtoRSCHP:
  fixes C ::"('uc,'uc) comp"
  fixes ttype :: "('t × real) itself"
  assumes A1: "∀ (P::'uc prgm) . case C P of Some CP ⇒ CP UC-emulates P | None ⇒ True"
  shows "RSCHP C ttype"
proof (rule ccontr)
  assume CF: "¬ (RSCHP C ttype)"
  then show "False" 
  proof -
    from CF obtain P  where  CF':"
          ¬( case C P of None ⇒ True
          | Some CP ⇒
              ∀A. ∃S. ∀m :: ('t × real). prefix m ⟶
                          A >< CP ↝ m ⟶ S >< P ↝ m)" by auto
    hence "∃ CP . C P = Some CP"   using option.simps(4) by fastforce
    then obtain CP where SomeCP: "C P  = Some (CP::'uc prgm)" by auto
    from CF' SomeCP have "¬(∀A. ∃S. ∀m :: ('t × real). prefix m ⟶
                          A >< CP ↝ m ⟶ S >< P ↝ m)" by auto
    then obtain A where  NotRSCHP: "∀ (S::'uc ctxt).
      (∃ m :: ('t × real) . prefix m ∧ (A >< (CP::'uc prgm) ↝ m) ∧ ¬(S >< P ↝ m))" by auto
    from A1 SomeCP have "CP UC-emulates P "  by (smt (verit, del_insts) option.simps(5)) 
    then obtain S where Eq: "∀ (Z::'env) . (PrExec Z A (CP) True = PrExec Z S P True)" by blast
    from NotRSCHP have
      "(∃  (t::'t) (p::real) . prefix (t,p) ∧ (A >< (CP) ↝ (t,p)) ∧ ¬(S >< P ↝ (t,p)))"
      by auto 
    then obtain  t :: "'t" and p :: "real"
      where prefix_full: "prefix (t,p)" 
      and Yes:"A >< (CP) ↝ (t,p)"
      and No: "¬(S >< P ↝ (t,p))" by auto
    from prefix_full prefix_iff_trace_is_prefix have prefix: "prefix t" by simp

    let ?Z = "Zcan t"
    from Yes relation_uc prefix have PrEx1: "PrExecT ?Z A (CP) t = p" by metis
    from Yes relation_uc prefix have p_nonzero: "p> 0" by metis
    from PrEx1 prefix construct_canonical_env2  prefix 
      have LHS: "PrExec ?Z A (CP) True = p" by auto
    
    from No relation_uc p_nonzero prefix have "p ≠ PrExecT ?Z S P t" by blast
    moreover have "PrExecT ?Z S P t = PrExec ?Z S P True"
      using construct_canonical_env2 prefix   by simp
    ultimately have RHS: "PrExec ?Z S P True ≠ p" by simp

    from LHS RHS  have "PrExec ?Z A (CP) True ≠ PrExec ?Z S P True" by arith
    from this Eq show "False" by blast
  qed
qed

end

section "Relating UC to 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 . case (C P) of (Some CP) ⇒  RRgen (RHPrel (t:: 't itself)) (CP) P
                                          | None ⇒ True                                  
"

context UC 
begin

theorem RHPtoUC:
  fixes C ::"('uc,'uc) comp"
  fixes ttype :: "('t × real) itself"
  assumes A: "RHP C ttype"
  shows "∀ (P::'uc prgm) . case (C P) of (Some CP) ⇒ CP UC-emulates P | None ⇒ True"
using RSCHPtoUC assms 
  by (smt (z3) UC.relation_uc not_Some_eq option.simps(4) option.simps(5)) 

theorem UCtoRHP:
  fixes C ::"('uc,'uc) comp"
  fixes ttype :: "('t × real) itself"
  assumes A1: "∀ (P::'uc prgm) . case (C P) of (Some CP) ⇒ CP UC-emulates P | None ⇒ True"
  shows "RHP C ttype"
proof (rule ccontr)
  assume CF: "¬ (RHP C ttype)"
  then show "False" 
  proof -
    from CF obtain P  where  CF':"
          ¬( case C P of None ⇒ True
          | Some CP ⇒
              ∀A. ∃S. ∀m :: ('t × real). prefix m ⟶
                          A >< CP ↝ m = S >< P ↝ m)" by auto
    hence "∃ CP . C P = Some CP"   using option.simps(4) by fastforce
    then obtain CP where SomeCP: "C P  = Some (CP::'uc prgm)" by auto
    from CF' SomeCP have "¬(∀A. ∃S. ∀m :: ('t × real). prefix m ⟶
                          A >< CP ↝ m = S >< P ↝ m)" by auto
    then obtain A where  NotRSCHP: "∀ (S::'uc ctxt).
      (∃ m :: ('t × real) . prefix m ∧  (A >< CP ↝ m) ≠ (S >< P ↝ m))" by auto

    from A1 SomeCP have "CP UC-emulates P "  by (smt (verit, del_insts) option.simps(5)) 
    then obtain S where Eq: "∀ (Z::'env) . (PrExec Z A (CP) True = PrExec Z S P True)" by blast
    from NotRSCHP have "(∃  (t::'t) (p::real) . prefix (t,p) ∧ ((A >< (CP) ↝ (t,p)) ≠ (S >< P ↝ (t,p))))" by auto 
    then obtain  t :: "'t" and p :: "real" and AY and AN and PY and PN
      where prefix_full: "prefix (t,p)" 
      and Yes:"AY >< PY ↝ (t,p)"
      and No: "¬(AN >< PN ↝ (t,p))"
      and Dunno: "(AY  = A ∧ PY = CP ∧ AN = S ∧ PN = P)
                 ∨(AN  = A ∧ PN = CP ∧ AY = S ∧ PY = P)"
      by metis
    from prefix_full prefix_iff_trace_is_prefix have prefix: "prefix t" by simp

    let ?Z = "Zcan t"
    from Yes relation_uc prefix have PrEx1: "PrExecT ?Z AY PY t = p" by metis
    from Yes relation_uc prefix have p_nonzero: "p> 0" by metis
    from PrEx1 prefix construct_canonical_env2  prefix 
      have LHS: "PrExec ?Z AY PY True = p" by auto
    
    from No relation_uc p_nonzero prefix have "p ≠ PrExecT ?Z AN PN t" by blast
    moreover have "PrExecT ?Z AN PN t = PrExec ?Z AN PN True"
      using construct_canonical_env2 prefix   by simp
    ultimately have RHS: "PrExec ?Z AN PN True ≠ p" by simp

    from LHS RHS  have "PrExec ?Z AY PY True ≠ PrExec ?Z AN PN True" by arith
    from this Eq Dunno show "False" by fastforce 
  qed
qed

end

section "Translating UC results to programming languages"

lemma RRGen_is_transitive [simp,trans]:
  fixes P1::"('b) prgm"
  fixes P2::"('i) prgm"
  fixes P3::"('r) prgm"
  assumes trans: "∀ a b c . rel12 a b ∧ rel23 b c ⟶ rel13 a c"
  assumes A: "RRgen rel12 P1 P2"
  assumes B: "RRgen rel23 P2 P3"
 shows  "RRgen rel13 P1 P3"
proof
  fix A
  from A obtain S2 where R1: "rel12 (A >< P1) (S2 >< P2)" by auto
  from B obtain S3 where R2: "rel23 (S2 >< P2) (S3 >< P3)" by auto
  from R1 R2 trans have R3: "rel13 (A >< P1) (S3 >< P3)" by simp
  then show  "∃ S. rel13 (A >< P1) (S >< P3)" by auto
qed

(* First, we need transitivity for RSCHPrel. *)
lemma RHPrel [simp,trans]:
  fixes ttype :: "('t × real) itself" 
  assumes A1:"RHPrel ttype a b"
  assumes A2:"RHPrel ttype b c"
  shows "RHPrel ttype a c"
using A1 A2 by blast   

(* Second, for RHP compilers. *)
lemma RHPbind_trans [simp,trans]:
  fixes ttype :: "('t × real) itself" 
  fixes C1 ::"('a, 'b) comp"  
  fixes C2 ::"('b, 'c) comp"   
  assumes A1:"RHP C1 ttype "
  assumes A2:"RHP C2 ttype "
  shows "RHP ((λ x. ( C1 x) >>= C2)::('a, 'c) comp)  ttype"
(*
shows "RHP (λ x. bind (C1 x) C2)  ttype" *)
proof
  fix P
  show "case bind (C1 P) C2 of None ⇒ True
         | Some CP ⇒
             ∀A. ∃S. ∀m::('t × real). prefix m ⟶
                         A >< CP ↝ m = S >< P ↝ m" 
  
  proof (cases "bind (C1 P) C2")
    case None
    then show ?thesis by simp
  next
    case SomeC1P:(Some C2P)
    then have "∃ C1P . (C1 P) = Some C1P ∧ (C2 C1P) = Some C2P" by (meson bind_eq_Some_conv) 
    then obtain C1P where 
        C1P: "C1 P = Some C1P"
      and  C2P: "C2 C1P = Some C2P"   
      by auto
    from C1P A1 have "∀A. ∃S. ∀m::('t × real). prefix m ⟶
                         A >< C1P ↝ m = S >< P ↝ m"  by (smt (verit, best) option.simps(5)) 
    from this C2P A2 have "∀A. ∃S. ∀m::('t × real). prefix m ⟶
                         A >< C2P ↝ m = S >< P ↝ m"  by (smt (verit, best) option.simps(5))
    thus ?thesis using C1P C2P by (smt (verit, best) SomeC1P option.simps(5)) 
  qed 
qed


context UC
begin

theorem implementUC:
  fixes UCC::"('uc,'uc) comp" (* This can be seen as one for more UC results. *)
  fixes C1 ::"('b ,'uc) comp"  
  fixes C2 ::"('uc,'r ) comp"  
  fixes ttype :: "('t × real) itself"  
  assumes AUCC: "∀ (P::'uc prgm) . case UCC P of (Some UCCP) ⇒ (UCCP) UC-emulates P | None ⇒ True"
  assumes AC1:  "RHP C1 ttype"
  assumes AC2:  "RHP C2 ttype"
  shows "RHP (λ x. C1 x ⤜ UCC ⤜ C2)   ttype"
proof-
  from UCtoRHP AUCC have ACUCC: "RHP UCC ttype" by simp
  from RHPbind_trans AC1 ACUCC have CM: "RHP (λ x. C1 x ⤜ UCC) ttype" by simp
  let ?C1UCC = "(λ x. C1 x ⤜ UCC)"
  from CM AC2 RHPbind_trans[of ?C1UCC C2] have "RHP (λ y . ?C1UCC y ⤜ C2) ttype" by simp
  thus "RHP (λ x. C1 x ⤜ UCC ⤜ C2)   ttype" by auto  
qed


end

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

abbreviation program_agree
  where
 "program_agree P1 P2 (ttype:: 't itself) ≡ 
     ∀ T::'t set. ((∃ A1 . Behav(A1 >< P1) = T) = (∃ A2 . Behav(A2 >< P2) = T))
"
*)

abbreviation program_agree
  where
  "program_agree P1 P2 ttype ≡ ∃ C . (C P1) = Some P2 ∧ RHP C ttype"


theorem (in UC) UCcompiler1:
  fixes ttype :: "('t × real) itself"  
  fixes Pb::"'b prgm"
  fixes Pr::"'r prgm"
  fixes pi::"'uc prgm"
  fixes F ::"'uc prgm"  
  fixes C:: "('b,'r) comp"
  assumes FuncAgree: "program_agree Pb F ttype"
  assumes ProtAgree: "program_agree pi Pr ttype" 
  assumes Cdef1: "C Pb = Some Pr"
  assumes Cdef2: "∀ x. x ≠ Pb ⟶ C x = None" 
  (* Direction ⟹ *)
  assumes AUCC': "pi UC-emulates F"
  shows "RHP C ttype"
proof -
  fix P A 
  obtain C1 where C1agree: "(C1 Pb) = Some F" and
                  C1RHP: "RHP (C1::('b,'uc) comp) ttype" using FuncAgree by blast  
  obtain C2 where C2agree: "(C2 pi) = Some Pr" and
                  C2RHP: "RHP (C2::('uc,'r) comp) ttype" using ProtAgree by blast
  define UCC where UCCdef: "UCC ≡ λx ::'uc prgm . if x = F then Some (pi::'uc prgm) else None"  
  have AUCC:
    "∀ (P::'uc prgm) . case UCC P of (Some UCCP) ⇒ (UCCP) UC-emulates P | None ⇒ True"
    using AUCC' UCemulates_reflexive UCCdef by auto
  let ?bigC= " (λ (x::'b prgm). C1 x ⤜ UCC ⤜ C2) :: ('b,'r) comp"
  have RHP: "RHP (?bigC) ttype" using
        implementUC AUCC C1RHP C2RHP 
    by blast
  let ?smallC = "λ x. if x = Pb then ?bigC x else None"
  have CisSmallC: "∀ x . C x = ?smallC x"
  proof 
    fix x
    have "C x = ?bigC x" when X: "x=Pb" 
      using C1agree C2agree UCCdef Cdef1 X  by auto 
    moreover
    have "C x = None" when notX: "x≠Pb"
      using Cdef2 notX by auto
    ultimately
    show "C x = ?smallC x" by simp   
  qed
  then have "RHP ?smallC ttype"  using RHP by simp
  from this CisSmallC show ?thesis by auto
qed

(*
theorem(in UC) CompRCimplCompUC :
  fixes tt::"('t×real) itself"
  fixes C::"('p,'r) comp"
  assumes RHCC:"RHP C ttype"
  fixes P::"'p prgm"
  fixes pi::"'uc prgm"
  fixes F ::"'uc prgm"
  assumes FuncAgree: "program_agree P F ttype"
  assumes ProtAgree: "program_agree pi (C P) ttype"
  shows "pi UC-emulates F"
proof
  fix A::"'uc ctxt"
  show "∃ S . (∀ Z . PrExec Z A pi True = PrExec Z S F True)" proof
    have "∃ A' . (Behav(A' >< C P)) = (Behav(A >< pi)::('t×real) set)"
      using ProtAgree by auto
    then obtain A' where
      ProtBehavEq:"Behav(A' >< C P) = (Behav(A >< pi)::('t×real) set)" by auto
    then obtain S' where  BehavInd:"Behav(A' >< C P) = Behav(S' >< P)"
      using RHCC by blast
    hence "∃ S . poly_time S F ∧ (Behav(S >< F)) = (Behav(S' >< P)::('t×real×nat) set)"
      using FuncAgree prog_agree_one_dir by auto
    then obtain S where PolyS:"poly_time S F"
        and FuncBehavEq:"Behav(S' >< P) = (Behav(S >< F)::('t×real×nat) set)" by auto
    hence "Behav(A >< pi) ≅ Behav(S >< F)" using ProtBehavEq BehavInd by metis
    hence "∀ Z ∈ ZClass . PrExec Z A pi True ≈ PrExec Z S F True" using PolyA PolyS Behav_PrExec by auto
    thus "∃ S . poly_time S F ∧ (∀ Z ∈ ZClass . PrExec Z A pi True ≈ PrExec Z S F True)"
      using PolyS by auto
  qed
qed
*)

lemma (in UC) noUCnoRHP:
  fixes ttype :: "('t × real) itself"  
  assumes A1: "¬ (CF) UC-emulates F"
  assumes A2: "C F = Some CF"
  shows "¬ RHP C ttype"
using A1 A2 RHPtoUC 
  by (smt (verit, del_insts) option.simps(5)) 

theorem (in UC) UCcompiler2:
  fixes ttype :: "('t × real) itself"  
  fixes Pb::"'b prgm"
  fixes Pr::"'r prgm"
  fixes pi::"'uc prgm"
  fixes F ::"'uc prgm"  
  assumes AA2: "program_agree pi Pr ttype"
  assumes AA3: "program_agree F Pb ttype"
  assumes AA4: "program_agree Pr pi ttype"
  fixes C:: "('b,'r) comp"
  assumes AC1: "C Pb = Some Pr"
  (* Direction ⟹ *)
  assumes ARHP: "RHP C ttype"
  shows "pi UC-emulates F"
proof(rule ccontr)
  assume notUC: "¬ pi UC-emulates F"
  then show False
  proof-
  obtain C1b where C1bagree: "(C1b F) = Some Pb" and
                  C1bRHP: "RHP C1b ttype" using AA3 by blast
  obtain C2 where C2agree: "(C2 pi) = Some Pr" and
                  C2RHP: "RHP C2 ttype" using AA2 by blast
  obtain C2b where C2bagree: "(C2b Pr) = Some pi" and
                  C2bRHP: "RHP C2b ttype" using AA4 by blast

  define UCC where "UCC ≡ λx ::'uc prgm . if x = F then Some (pi::'uc prgm) else None" (* Note was x before *)
  
  from notUC UCC_def have "¬ pi UC-emulates F" by presburger
  from this UCC_def RSCHPtoUC' obtain A where  " ∀ S . ∃m::'t × real.
               prefix m ∧ 
               A >< pi ↝m  ≠  S >< F ↝ m" by metis
  from this UCC_def obtain A where  Last: " ∀ S . ∃m::'t × real.
               prefix m ∧ 
               A >< pi ↝m  ≠  S >< F ↝ m" by metis

  have "∃ Cr . ∀ S . ∃m::'t × real. prefix m ∧ 
               Cr >< Pr ↝ m  ≠  S >< F ↝ m" 
  proof-
    from C2bRHP C2bagree have
      Side1: "∀A. ∃S. ∀m::'t × real . prefix m ⟶ A >< pi ↝ m = S >< Pr ↝ m" by (smt (verit, del_insts) option.simps(5)) 
    from C2RHP C2agree have
      Side2: "∀A. ∃S. ∀m::'t × real . prefix m ⟶ A >< Pr ↝ m = S >< pi ↝ m" by (smt (verit, del_insts) option.simps(5)) 
    from Side1 Side2 Last show ?thesis  by meson
  qed
  then obtain Cr where  "∀ S . ∃m::'t × real. prefix m ∧ Cr >< Pr ↝ m  ≠  S >< F ↝ m" 
    by meson
    
  hence NoSim: "∀ S . ∃m::'t × real.
               prefix m ∧ 
               Cr >< Pr ↝ m  ≠  S >< F ↝ m" using C2agree by blast

  from ARHP AC1 obtain Cb where 
    Bla1:"∀ m::'t × real. prefix m ⟶ Cr >< Pr ↝ m = Cb >< Pb ↝ m" by (smt (verit, del_insts) option.simps(5))
  from C1bRHP C1bagree obtain S where 
    Bla2:"∀ m::'t × real. prefix m ⟶ S >< F ↝ m = Cb >< Pb ↝ m" by (smt (verit, del_insts) option.simps(5))
  from NoSim obtain m::"'t × real" where "prefix m" 
      and "Cr >< Pr ↝ m  ≠  S >< F ↝ m"  by blast
  from this Bla1 Bla2 show "False" by blast
qed
qed

end