Theory UC

theory UC
  imports 
  RobustCompilation
begin

text "Note that we axiomatise some properties about probabilities and sums, for different reasons.

We axiomatize probabilities because HOL.Probability is difficult to use and may be to heavy-weight for simple probabilistic
languages that only have discrete probabilities. This makes it easier to plug them in, and the axioms are few and uncontroversial.

We axiomatise sums because HOL's builtin sum function guarantees (lemma infinite) to give 1 for infinite sets. This is unsuited, e.g., if a subset only consists
of zero probability traces or of traces with rapidly lowering probabilities. HOL does not yet include a sum function over infinite sets. 
Countable_Set provides function to map to naturals and lemmas for closure properties, e.g., to show subsets are countable,
 and perhaps this could be combined with infinite series to define such a sum and prove the necessary properties. Alas, we list those as
axioms here and proved them on paper. 
"

locale UC =
  fixes PrExec  :: "'env ⇒ 'uc ctxt ⇒ 'uc prgm ⇒ bool ⇒ nat ⇒ real"
  fixes PrExecT :: "'env ⇒ 'uc ctxt ⇒ 'uc prgm ⇒  't  ⇒ nat ⇒ 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"
  fixes possible :: "'env ⇒ 't ⇒ nat ⇒ bool" (* for a (non-deterministic Z? ) is this the (a) trace the environment computes *)

  (* sums over countable sets (two because cannot have polymorphism within locale) *)
  fixes csum ::  "('t ⇒ real) ⇒ ('t set) ⇒ real option"
  fixes csum2 ::  "(('t×real×nat) ⇒ real) ⇒ (('t×real×nat) set) ⇒ real option"

  (* assumptions needed in both directions *)
  assumes relation_uc: (* We can define a semantic's from UC's semantics. *)
    "(A >< P) ↝ (t,p,n) ≡ (PrExecT (Zcan t) A P t n) = 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,n::int) ≡ prefix t"

  (* only needed in RSCHPtoUC *)
  assumes prefixes_contain_final_bit: (* every finite trace contains the final bit *)
    "PrExec Z A P b n = (case 
          (csum (λt. PrExecT Z A P t n) {t. prefix t ∧ β t = b}) of
           None ⇒ -1 | Some x ⇒ x)"
  and nonprobabilistic_envs_are_complete:
    "(∃ Z b. PrExec Z A P b n ≠ PrExec Z S F b n) ⟶ (∃ Z' . PrExec Z' A P True n ≠ PrExec Z' S F True n ∧ nonprobabilistic Z')"  
  and construct_canonical_env:
    "⟦nonprobabilistic Z;  prefix t; possible Z t n ⟧ ⟹ PrExecT Z A P t n = PrExecT (Zcan t) A P t n"

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

  (* axioms for sums *)
  and csum_reindex: (* lemma sum_reindex but for infinite sets *)
    "∀ f g A B . bij_betw f A B ⟶  csum2 (g ∘ f) A = csum g B"
  and csum2_cong: (* sum.cong but for infinite sets *)
    "∀ A f g . (∀ x ∈ A :: ('t×real×nat) set  . f x = g x) ⟶ (csum2 f A = csum2 g A)"
  and csum_mono: (* sum.mono but for infinite sets *)
    "∀ A f g fx gx . (∀ x ∈ A :: 't set  . f x ≤ g x) ⟶ 
     (csum f A = Some fx) ⟶ (csum g A = Some gx) ⟶ fx ≤ gx"

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

  and possible: "⟦ PrExecT (Z::'env) (A::'uc ctxt) (P::'uc prgm) (t::'t) n > 0 ⟧ ⟹ possible Z t n"
  and possible2: "⟦ possible Z t n ⟧ ⟹  PrExecT Z A P t n > 0 " (* TODO try to get rid of possible by introducing as abbreviation *)

(* Standard cryptographic definition of computational indistinguishability *)
abbreviation comp_ind :: "(nat ⇒ real) ⇒ (nat ⇒ real) ⇒ bool" (infix "≈" 46)
  where "f ≈ g ≡ (∀ (k::nat) . ∃ (N::nat) . ∀ (n::nat) > N . abs((f n) - (g n)) < 1/(n^k))"

locale compUC = UC +
  fixes uct::"'uc itself"
  fixes ZClass :: "'env set"

  assumes env_fixes_io: "⟦nonprobabilistic Z; nonprobabilistic Z'; possible Z t n; possible Z t n⟧ ⟹
     PrExecT (Z::'env) (A::'uc ctxt) (P::'uc prgm) (t::'t) n = PrExecT Z' A P t n" (* remember, trace contains final bit *)
  and Zcan_nonprob: "nonprobabilistic (Zcan t)" 
  and Zcan_possible: "possible (Zcan t) t n"

  and nonprobabilistic_envs_are_complete_comp:
    "(∃ Z∈ZClass . ∃ b. PrExec Z A P b ≈ PrExec Z S F b) ⟶ (∃ Z'∈ZClass . PrExec Z' A P True ≈ PrExec Z' S F True ∧ nonprobabilistic Z')"
  and nonprobabilistic_envs_are_sound_comp:
    "(∃ Z∈ZClass . ∃ b. ¬(PrExec Z A P b ≈ PrExec Z S F b)) ⟶ (∃ Z'∈ZClass . ¬(PrExec Z' A P True ≈ PrExec Z' S F True) ∧ nonprobabilistic Z')"

(* Create a locale that includes a compiler so Isabelle
   recognizes the proofs as using the same compiler. *)
locale compUCisRC = compUC +
  fixes C :: "('uc,'uc) comp"
  assumes "uct = (uct'::'uc itself)"

end