fact: Definition Hiding_ideal : package fset0 [interface #val #[ COM ] : chChallenge → chMessage ; #val #[ OPEN ] : 'unit → chOpen ; #val #[ VER ] : chTranscript → 'bool ] Hiding_E := [package #def #[ HIDING ] (_ : chHiding) : chMessage { #import {sig #[ COM ] : chChallenge → chMessage } as com ;; e ← sample uniform i_challenge ;; t ← com e ;; ret t } ].
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)