Reversible coercion from choice_type

theories/Crypt/choice_type.v

@@ -53,37 +53,73 @@ Inductive choice_type :=
 Derive NoConfusion NoConfusionHom for choice_type.
 
 
-Fixpoint chElement_ordType (U : choice_type) : ordType :=
-  match U with
-  | chUnit => Datatypes.unit
-  | chNat => nat
-  | chInt => BinInt.Z
-  | chBool => bool
-  | chProd U1 U2 => chElement_ordType U1 * chElement_ordType U2
-  | chMap U1 U2 => {fmap chElement_ordType U1 → chElement_ordType U2}
-  | chOption U => option(chElement_ordType U)
-  | chFin n => ordinal n.(pos)
-  | chWord nbits => word nbits
-  | chList U => list (chElement_ordType U)
-  | chSum U1 U2 => chElement_ordType U1 + chElement_ordType U2
-  end.
+(* Types T that may be represented by the interpretation of
+   a choice_type A are given an instance of hasInterp.  *)
+HB.mixin Record hasInterp (A : choice_type) T := { }.
+
+HB.structure Definition Crypt (A : choice_type)
+  := { T of Countable T & Ord.Ord T & hasInterp A T }.
+
+HB.instance Definition _
+  := hasInterp.Build chUnit unit.
+
+HB.instance Definition _
+  := hasInterp.Build chNat nat.
+
+HB.instance Definition _
+  := hasInterp.Build chInt BinInt.Z.
+
+HB.instance Definition _
+  := hasInterp.Build chBool bool.
+
+HB.instance Definition _ (A B : choice_type)
+  (T : Crypt.type A) (S : Crypt.type B)
+  := hasInterp.Build (chProd A B) (T * S)%type.
+
+HB.instance Definition _ (A B : choice_type)
+  (T : Crypt.type A) (S : Crypt.type B) :=
+  @CanIsCountable _ {fmap T → S} _ _ (@fmvalK T S).
+
+HB.instance Definition _ (A B : choice_type)
+  (T : Crypt.type A) (S : Crypt.type B)
+  := hasInterp.Build (chMap A B) {fmap T → S}.
+
+HB.instance Definition _ (A : choice_type) (T : Crypt.type A)
+  := hasInterp.Build (chOption A) (option T).
+
+HB.instance Definition _ n
+  := hasInterp.Build (chFin n) (ordinal n.(pos)).
 
-Fixpoint chElement (U : choice_type) : choiceType :=
+#[non_forgetful_inheritance]
+HB.instance Definition _ nbits
+  := hasInterp.Build (chWord nbits) (word nbits).
+
+HB.instance Definition _ (A : choice_type) (T : Crypt.type A)
+  := hasInterp.Build (chList A) (list T).
+
+HB.instance Definition _ (A B : choice_type)
+  (T : Crypt.type A) (S : Crypt.type B)
+  := hasInterp.Build (chSum A B) (T + S)%type.
+
+Fixpoint chInterp (U : choice_type) : Crypt.type U :=
   match U with
-  | chUnit => Datatypes.unit
+  | chUnit => unit
   | chNat => nat
   | chInt => BinInt.Z
   | chBool => bool
-  | chProd U1 U2 => chElement U1 * chElement U2
-  | chMap U1 U2 => {fmap chElement_ordType U1 → chElement U2}
-  | chOption U => option (chElement U)
+  | chProd u v => (chInterp u * chInterp v)%type
+  | chMap u v => {fmap chInterp u → chInterp v}
+  | chOption u => option (chInterp u)
   | chFin n => ordinal n.(pos)
   | chWord nbits => word nbits
-  | chList U => list (chElement U)
-  | chSum U1 U2 => chElement U1 + chElement U2
+  | chList u => list (chInterp u)
+  | chSum u v => (chInterp u + chInterp v)%type
   end.
 
-Coercion chElement : choice_type >-> choiceType.
+(* When a Crypt.type is found for an arbitrary type, the
+   parameter U remembers how to construct a corresponding
+   choice_type. This allows us to use this coercion in reverse. *)
+#[reversible] Coercion chInterp : choice_type >-> Crypt.type.
 
 (* Canonical element in a type of the choice_type *)
 #[program] Fixpoint chCanonical (T : choice_type) : T :=
@@ -101,162 +137,8 @@ Coercion chElement : choice_type >-> choiceType.
   | chSum A B => inl (chCanonical A)
   end.
 
-Section Cucumber.
-  (* Cucumber is a replacement for pickle until a
-     countType for each choice_type can be given directly
-     or until the inductive choice_type is removed entirely.
-     The functions cucumber and uncucumber correspond to pickle
-     and unpickle respectively.
-   *)
-
-  Fixpoint cucumber' {U : choice_type} : chElement_ordType U → nat :=
-    match U with
-    | chUnit => pickle
-    | chNat => pickle
-    | chInt => pickle
-    | chBool => pickle
-    | chProd _ _ => λ '(x, y), pickle (cucumber' x, cucumber' y)
-    | chMap _ _ =>
-        λ x, pickle (map (λ '(x, y), (cucumber' x, cucumber' y)) (\val x))
-    | chOption _ => λ x, pickle (omap cucumber' x)
-    | chFin _ => pickle
-    | chWord _ => pickle
-    | chList _ => λ x, pickle (map cucumber' x)
-    | chSum _ _ => λ x,
-      match x with
-      | inl y => pickle (true, cucumber' y)
-      | inr y => pickle (false, cucumber' y)
-      end
-    end.
-
-  Fixpoint cucumber {U : choice_type} : U → nat :=
-    match U with
-    | chUnit => pickle
-    | chNat => pickle
-    | chInt => pickle
-    | chBool => pickle
-    | chProd _ _ => λ '(x, y), pickle (cucumber x, cucumber y)
-    | chMap _ _ =>
-        λ x, pickle (map (λ '(x, y), (cucumber' x, cucumber y)) (\val x))
-    | chOption _ => λ x, pickle (omap cucumber x)
-    | chFin _ => pickle
-    | chWord _ => pickle
-    | chList _ => λ x, pickle (map cucumber x)
-    | chSum _ _ => λ x,
-      match x with
-      | inl y => pickle (true, cucumber y)
-      | inr y => pickle (false, cucumber y)
-      end
-    end.
-
-  Definition helper {U : countType} (x : U) : nat → U
-    := λ n, locked (odflt x (unpickle n)).
-
-  Lemma helperK U x : cancel (@pickle U) (helper x).
-  Proof.
-    intros y.
-    rewrite /helper -lock pickleK //=.
-  Qed.
-
-
-  Fixpoint uncucumber'' {U : choice_type}
-    : nat → chElement_ordType U :=
-    match U with
-    | chUnit => λ x, helper tt x
-    | chNat => λ x, helper 0 x
-    | chInt => λ x, helper BinInt.Z0 x
-    | chBool => λ x, helper false x
-    | chProd _ _ => λ x,
-        let (y, z) := helper (0,0) x in (uncucumber'' y, uncucumber'' z)
-    | chMap _ _ =>
-        λ x, mkfmap (map (λ '(x, y), (uncucumber'' x, uncucumber'' y))
-          (helper [::] x))
-    | chOption _ =>
-        λ x, omap uncucumber'' (helper None x)
-    | chFin n => λ x, helper (Ordinal n.(cond_pos)) x
-    | chWord _ => λ x, helper word0 x
-    | chList _ => λ x,
-        map uncucumber'' (helper [::] x)
-    | chSum _ _ => λ x,
-        let (b, n) := helper (true,0) x in
-        if b then inl (uncucumber'' n) else inr (uncucumber'' n)
-    end.
-
-  Fixpoint uncucumber' {U : choice_type} : nat → U :=
-    match U with
-    | chUnit => λ x, helper tt x
-    | chNat => λ x, helper 0 x
-    | chInt => λ x, helper BinInt.Z0 x
-    | chBool => λ x, helper false x
-    | chProd _ _ => λ x,
-        let (y, z) := helper (0,0) x in (uncucumber' y, uncucumber' z)
-    | chMap _ _ =>
-        λ x, mkfmap (map (λ '(x, y), (uncucumber'' x, uncucumber' y))
-          (helper [::] x))
-    | chOption _ =>
-        λ x, omap uncucumber' (helper None x)
-    | chFin n => λ x, helper (Ordinal n.(cond_pos)) x
-    | chWord _ => λ x, helper word0 x
-    | chList _ => λ x,
-        map uncucumber' (helper [::] x)
-    | chSum _ _ => λ x,
-        let (b, n) := helper (true,0) x in
-        if b then inl (uncucumber' n) else inr (uncucumber' n)
-    end.
-
-  Definition uncucumber {U : choice_type} : nat → option U :=
-    λ n, locked (Some (uncucumber' n)).
-
-  Lemma cucumber''K (U : choice_type) : cancel (@cucumber' U) uncucumber''.
-  Proof.
-    induction U => //=.
-    all: intros x.
-    all: try rewrite helperK //.
-    + destruct x => //=.
-      rewrite helperK IHU1 IHU2 //.
-    + rewrite -map_comp //=.
-      rewrite (@map_ext _ _ _ id).
-      2: intros [a b] _; simpl.
-      2: rewrite IHU1 IHU2 //.
-      rewrite map_id.
-      apply fmvalK.
-    + apply omapK, IHU.
-    + rewrite -map_comp.
-      rewrite (@map_ext _ _ _ id).
-      2: intros a _; rewrite //= IHU //.
-      by rewrite map_id.
-    + destruct x; rewrite helperK ?IHU1 ?IHU2 //.
-  Qed.
-
-  Lemma cucumber'K (U : choice_type) : cancel (@cucumber U) uncucumber'.
-  Proof.
-    induction U => //=.
-    all: intros x.
-    all: try rewrite helperK //.
-    + destruct x => //=.
-      rewrite helperK IHU1 IHU2 //.
-    + rewrite -map_comp //=.
-      rewrite (@map_ext _ _ _ id).
-      2: intros [a b] _; simpl.
-      2: rewrite cucumber''K IHU2 //.
-      rewrite map_id.
-      apply fmvalK.
-    + apply omapK, IHU.
-    + rewrite -map_comp.
-      rewrite (@map_ext _ _ _ id).
-      2: intros a _; rewrite //= IHU //.
-      by rewrite map_id.
-    + destruct x; rewrite helperK ?IHU1 ?IHU2 //.
-  Qed.
-
-  Lemma cucumberK U : pcancel (@cucumber U) uncucumber.
-  Proof. intros x. rewrite /uncucumber -lock. f_equal. apply cucumber'K. Qed.
-
-End Cucumber.
-
-
 Definition coerce {A B : choice_type} : A → B
-  := λ x, odflt (chCanonical B) (uncucumber (cucumber x)).
+  := λ x, odflt (chCanonical B) (unpickle (pickle x)).
 
 Lemma coerceE {A : choice_type} (a : A) : coerce a = a.
-Proof. rewrite /coerce cucumberK //. Qed.
+Proof. rewrite /coerce pickleK //. Qed.

theories/Crypt/examples/KEMDEM.v

@@ -233,18 +233,18 @@ Section KEMDEM.
         #assert (k == None) ;;
         k ← sample keyD ;;
         #put k_loc := Some k ;;
-        @ret 'unit tt
+        ret tt
       } ;
       #def #[ SET ] (k : 'key) : 'unit {
         k' ← get k_loc ;;
         #assert (k' == None) ;;
         #put k_loc := Some k ;;
-        @ret 'unit tt
+        ret tt
       } ;
       #def #[ GET ] (_ : 'unit) : 'key {
         k ← get k_loc ;;
         #assert (isSome k) as kSome ;;
-        @ret 'key (getSome k kSome)
+        ret (getSome k kSome)
       }
     ].
 
@@ -296,7 +296,7 @@ Section KEMDEM.
         '(pk, sk) ← η.(KEM_kgen) ;;
         #put pk_loc := Some pk ;;
         #put sk_loc := Some sk ;;
-        @ret 'pkey pk
+        ret pk
       } ;
       #def #[ ENCAP ] (_ : 'unit) : 'ekey {
         #import {sig #[ SET ] : 'key → 'unit } as SET ;;
@@ -420,7 +420,7 @@ Section KEMDEM.
         '(pk, sk) ← ζ.(PKE_kgen) ;;
         #put pk_loc := Some pk ;;
         #put sk_loc := Some sk ;;
-        @ret 'pkey pk
+        ret pk
       } ;
       #def #[ PKENC ] (m : 'plain) : 'ekey × 'cipher {
         pk ← get pk_loc ;;
@@ -433,7 +433,7 @@ Section KEMDEM.
         '(ek, c) ← ζ.(PKE_enc) pk (if b then m else nullPlain) ;;
         #put ek_loc := Some ek ;;
         #put c_loc := Some c ;;
-        @ret (chProd 'ekey 'cipher) (ek, c)
+        ret (ek, c)
       } ;
       #def #[ PKDEC ] (c' : 'ekey × 'cipher) : 'plain {
         sk ← get sk_loc ;;
@@ -487,7 +487,7 @@ Section KEMDEM.
         #put ek_loc := Some ek ;;
         c ← ENC m ;;
         #put c_loc := Some c ;;
-        @ret (chProd 'ekey 'cipher) (ek, c)
+        ret (ek, c)
       } ;
       #def #[ PKDEC ] ('(ek', c') : 'ekey × 'cipher) : 'plain {
         #import {sig #[ DECAP ] : 'ekey → 'key } as DECAP ;;

theories/Crypt/examples/PKE/CyclicGroup.v

@@ -163,14 +163,26 @@ Notation " 'el G " := 'fin #|el G|
 Notation " 'exp G " := 'fin #|exp G|
   (at level 3) : package_scope.
 
-Notation " 'g " := (fto (g _))
-  (at level 3) : package_scope.
+Declare Scope F_scope.
+Delimit Scope F_scope with F.
+
+Notation " 'g " := (fto (g _) : 'el _)
+  (at level 3) : F_scope.
+
+Definition mulf {G} (x y : 'el G) : 'el G
+  := fto (mulg (otf x) (otf y)).
+
+Definition expfn {G} (x : 'el G) (a : 'exp G) : 'el G
+  := fto (expgn (otf x) (otf a)).
+
+Definition expfni {G} (x : 'el G) (a : 'exp G) : 'el G
+  := fto ((otf x) ^- (otf a)).
 
 Notation " x * y " :=
-   (fto (mulg (otf x) (otf y))) : package_scope.
+  (mulf x y) : F_scope.
 
 Notation " x ^ a " :=
-  (fto (otf x ^+ otf a)) : package_scope.
+  (expfn x a) : F_scope.
 
 Notation " x ^- a " :=
-  (fto (otf x ^- otf a)) : package_scope.
+  (expfni x a) : F_scope.