Theory Pseudo_Random_Permutation

(* Title: Pseudo_Random_Permutation.thy
  Author: Andreas Lochbihler, ETH Zurich *)

subsection ‹Random permutation›

theory Pseudo_Random_Permutation imports
  CryptHOL.Computational_Model
begin

locale random_permutation =
  fixes A :: "'b set"
begin

definition random_permutation :: "('a ⇀ 'b) ⇒ 'a ⇒ ('b × ('a ⇀ 'b)) spmf"
where
  "random_permutation σ x =
  (case σ x of Some y ⇒ return_spmf (y, σ)
   | None ⇒ spmf_of_set (A - ran σ) ⤜ (λy. return_spmf (y, σ(x ↦ y))))"

lemma weight_random_oracle [simp]:
  "⟦ finite A; A - ran σ ≠ {} ⟧ ⟹ weight_spmf (random_permutation σ x) = 1"
by(simp add: random_permutation_def weight_bind_spmf o_def split: option.split)

lemma lossless_random_oracle [simp]:
  "⟦ finite A; A - ran σ ≠ {} ⟧ ⟹ lossless_spmf (random_permutation σ x)"
by(simp add: lossless_spmf_def)

sublocale finite: callee_invariant_on random_permutation "λσ. finite (dom σ)" ℐ_full
by(unfold_locales)(auto simp add: random_permutation_def split: option.splits)

lemma card_dom_random_oracle:
  assumes "interaction_any_bounded_by 𝒜 q"
  and "(y, σ') ∈ set_spmf (exec_gpv random_permutation 𝒜 σ)"
  and fin: "finite (dom σ)"
  shows "card (dom σ') ≤ q + card (dom σ)"
by(rule finite.interaction_bounded_by'_exec_gpv_count[OF assms(1-2)])
  (auto simp add: random_permutation_def fin card_insert_if simp del: fun_upd_apply split: option.split_asm)

end

end