fact: Definition Hiding_real: package fset0 [interface #val #[ COM ] : chChallenge → chMessage ; #val #[ OPEN ] : 'unit → chOpen ; #val #[ VER ] : chTranscript → 'bool ] Hiding_E := [package #def #[ HIDING ] (ms : chHiding) : chMessage { #import {sig #[ COM ] : chChallenge → chMessage } as com ;; let '(m1, m2) := ms in b ← sample uniform 1 ;; if Nat.even b then a ← com m1 ;; ret a else a ← com m2 ;; ret a } ].
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum fingroup.fingroup solvable.cyclic prime ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude RandomOracle) Coq(Utf8) extructures(ord fset fmap) Equations(Equations)