fact: Definition CTXT_HYB_pkg_3: package CTXT_HYB_locs_2 [interface] [interface #val #[ctxt]: 'word → 'ciph ; #val #[decrypt]: 'ciph → 'word ] := [package #def #[ctxt] (m: 'word): 'ciph { r <$ uniform Key_N ;; let mr := mkciph m r in T ← get T_loc ;; c <$ uniform Ciph_N ;; Tinv ← get Tinv_loc ;; S ← get S_loc ;; #put T_loc := setm T mr c ;; #put Tinv_loc := setm Tinv c mr ;; #put S_loc := setm S c tt ;; ret c } ; #def #[decrypt] (c: 'ciph): 'word { S ← get S_loc ;; #assert (c \notin domm S) ;; Tinv ← get Tinv_loc ;; Tinv' ← get Tinv'_loc ;; mr ← match getm Tinv' c with | None => mr <$ uniform Ciph_N ;; T ← get T_loc ;; #put T_loc := setm T mr c ;; #put Tinv_loc := setm Tinv c mr ;; #put Tinv'_loc := setm Tinv' c mr ;; ret mr | Some mr => ret mr end ;; let (m, r) := ciph_to_pair mr in ret m } ].
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Mon(SPropBase) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude) extructures(ord fset fmap) Equations(Equations)