fact: Definition PKE_CCA_pkg (ζ : PKE_scheme) b : package PKE_CCA_loc [interface] PKE_CCA_out := [package #def #[ PKGEN ] (_ : 'unit) : 'pkey { sk ← get sk_loc ;; #assert (sk == None) ;; '(pk, sk) ← ζ.(PKE_kgen) ;; #put pk_loc := Some pk ;; #put sk_loc := Some sk ;; @ret 'pkey pk } ; #def #[ PKENC ] (m : 'plain) : 'ekey × 'cipher { pk ← get pk_loc ;; #assert (isSome pk) as pkSome ;; let pk := getSome pk pkSome in ek ← get ek_loc ;; #assert (ek == None) ;; c ← get c_loc ;; #assert (c == None) ;; '(ek, c) ← ζ.(PKE_enc) pk (if b then m else nullPlain) ;; #put ek_loc := Some ek ;; #put c_loc := Some c ;; @ret (chProd 'ekey 'cipher) (ek, c) } ; #def #[ PKDEC ] (c' : 'ekey × 'cipher) : 'plain { sk ← get sk_loc ;; #assert (isSome sk) as skSome ;; let sk := getSome sk skSome in ek ← get ek_loc ;; c ← get c_loc ;; #assert ((ek, c) != (Some c'.1, Some c'.2)) ;; ret (ζ.(PKE_dec) sk c') } ].
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr fingroup.fingroup realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb Package Prelude pkg_composition) Coq(Utf8 Lia) extructures(ord fset fmap) Equations(Equations)