fact: Definition KEM (b : bool) : package KEM_loc (KEM_in b) KEM_out := [package #def #[ KEMGEN ] (_ : 'unit) : 'pkey { sk ← get sk_loc ;; #assert (sk == None) ;; '(pk, sk) ← η.(KEM_kgen) ;; #put pk_loc := Some pk ;; #put sk_loc := Some sk ;; @ret 'pkey pk } ; #def #[ ENCAP ] (_ : 'unit) : 'ekey { #import {sig #[ SET ] : 'key → 'unit } as SET ;; #import {sig #[ GEN ] : 'unit → 'unit } as GEN ;; pk ← get pk_loc ;; #assert (isSome pk) as pkSome ;; let pk := getSome pk pkSome in ek ← get ek_loc ;; #assert (ek == None) ;; '(k, ek) ← η.(KEM_encap) pk ;; #put ek_loc := Some ek ;; (if b then SET k else GEN Datatypes.tt) ;; ret ek } ; #def #[ DECAP ] (ek' : 'ekey) : 'key { sk ← get sk_loc ;; #assert (isSome sk) as skSome ;; let sk := getSome sk skSome in ek ← get ek_loc ;; #assert (ek != Some ek') ;; ret (η.(KEM_decap) sk ek') } ].
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)