fact: Definition CTXT_HYB_pkg_1: package CTXT_HYB_locs_1 [interface #val #[samp]: 'set 'key → 'key ] [interface #val #[ctxt]: 'word → 'ciph ; #val #[decrypt]: 'ciph → 'word ] := [package #def #[ctxt] (m: 'word): 'ciph { #import {sig #[samp]: 'set 'key → 'key } as samp ;; R ← get R_loc ;; r ← samp R ;; 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 ;; #put R_loc := setm R r tt ;; ret c } ; #def #[decrypt] (c: 'ciph): 'word { R ← get R_loc ;; S ← get S_loc ;; #assert (c \notin domm S) ;; 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 ;; ret mr | Some mr => ret mr end ;; let (m, r) := ciph_to_pair mr in #put R_loc := setm R r tt ;; 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)