fact: Definition DEM (b : bool) : package DEM_loc DEM_in DEM_out := [package #def #[ ENC ] (m : 'plain) : 'cipher { #import {sig #[ GET ] : 'unit → 'key } as GET ;; c ← get c_loc ;; #assert (c == None) ;; k ← GET Datatypes.tt ;; let c := θ.(DEM_enc) k (if b then m else nullPlain) in #put c_loc := Some c ;; ret c } ; #def #[ DEC ] (c' : 'cipher) : 'plain { #import {sig #[ GET ] : 'unit → 'key } as GET ;; c ← get c_loc ;; #assert (c != Some c') ;; k ← GET Datatypes.tt ;; ret (θ.(DEM_dec) k 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)