Use sigma types to fix extraction

This should get rid of the extra data being carried around after
extraction.

(cc @andres-erbsen)

2 files changed, 119 insertions, 37 deletions

diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v
index e2e4b25ea..629a2e576 100644
--- a/src/Experiments/Ed25519.v
+++ b/src/Experiments/Ed25519.v
@@ -241,7 +241,7 @@ Proof.
     unfold ModularBaseSystem.rep in Hencode; rewrite !Hencode in H.
   assumption.
 Qed.
-      
+
 Module N.
   Lemma size_le a b : (a <= b -> N.size a <= N.size b)%N.
   Proof.
@@ -364,10 +364,10 @@ Proof.
   replace (Z.of_nat 2) with 2%Z by reflexivity.
   omega.
 Qed.
-  
+
 Lemma combine_ZNWord : forall sz1 sz2 z1 z2,
-  (0 <= Z.of_nat sz1)%Z -> 
-  (0 <= Z.of_nat sz2)%Z -> 
+  (0 <= Z.of_nat sz1)%Z ->
+  (0 <= Z.of_nat sz2)%Z ->
   (0 <= z1 < 2 ^ (Z.of_nat sz1))%Z ->
   (0 <= z2 < 2 ^ (Z.of_nat sz2))%Z ->
   Word.combine (ZNWord sz1 z1) (ZNWord sz2 z2) =
@@ -395,7 +395,7 @@ Lemma nth_default_B_compat : forall i,
    GF25519.int_width)%Z.
 Proof.
     assert (@ModularBaseSystemProofs.FreezePreconditions
-                 GF25519.modulus GF25519.params25519 
+                 GF25519.modulus GF25519.params25519
                  GF25519.int_width) by
      (let A := fresh "H" in
             pose proof GF25519.freezePreconditions25519 as A;
@@ -428,7 +428,7 @@ Lemma minrep_freeze : forall x,
             0%Z.
 Proof.
     assert (@ModularBaseSystemProofs.FreezePreconditions
-                 GF25519.modulus GF25519.params25519 
+                 GF25519.modulus GF25519.params25519
                  GF25519.int_width)
       by (let A := fresh "H" in
             pose proof GF25519.freezePreconditions25519 as A;
@@ -473,7 +473,7 @@ Qed.
 Lemma convert_freezes: forall x,
   (ModularBaseSystemList.freeze GF25519.int_width
        (Tuple.to_list
-          (length PseudoMersenneBaseParams.limb_widths) x)) = 
+          (length PseudoMersenneBaseParams.limb_widths) x)) =
               (Tuple.to_list
                  (length
                     PseudoMersenneBaseParams.limb_widths)
@@ -738,7 +738,7 @@ Proof.
   cbv [GF25519.wire_widths length Tuple.fieldwise Tuple.fieldwise' fst snd] in *;
     intuition subst; reflexivity.
 Qed.
-  
+
 Lemma Proper_feEnc : Proper (GF25519BoundedCommon.eq ==> eq) feEnc.
 Proof.
   pose proof freezePre.
@@ -993,7 +993,7 @@ Proof.
          | |- _ => rewrite ModularArithmeticTheorems.F.of_Z_to_Z in *
          | |- _ => rewrite @ModularArithmeticTheorems.F.to_Z_of_Z in *
          | |- _ => reflexivity
-         | |- _ => omega 
+         | |- _ => omega
          end.
 Qed.
 
@@ -1029,7 +1029,7 @@ Let ERepDec :=
 
 Axiom ERepDec_correct : forall w : Word.word b, ERepDec w = @option_map E Erep EToRep (Edec w).
 
-Lemma Fsqrt_minus1_correct : 
+Lemma Fsqrt_minus1_correct :
  ModularArithmetic.F.mul Fsqrt_minus1 Fsqrt_minus1 =
  ModularArithmetic.F.opp
    (ModularArithmetic.F.of_Z GF25519.modulus 1).
@@ -1054,7 +1054,7 @@ Proof.
   apply (@PrimeFieldTheorems.F.sqrt_5mod8_correct GF25519.modulus _ eq_refl Fsqrt_minus1 Fsqrt_minus1_correct).
   eexists.
   symmetry; eassumption.
-Qed.  
+Qed.
 
 Let verify_correct :
   forall {mlen : nat} (msg : Word.word mlen) (pk : Word.word b)
@@ -1357,6 +1357,7 @@ Extraction Inline Crypto.Util.IterAssocOp.iter_op Crypto.Util.IterAssocOp.test_a
 Extraction Inline PointEncoding.Kencode_point.
 Extraction Inline ExtendedCoordinates.Extended.point ExtendedCoordinates.Extended.coordinates ExtendedCoordinates.Extended.to_twisted  ExtendedCoordinates.Extended.from_twisted ExtendedCoordinates.Extended.add_coordinates ExtendedCoordinates.Extended.add ExtendedCoordinates.Extended.opp ExtendedCoordinates.Extended.zero. (* ExtendedCoordinates.Extended.zero could be precomputed *)
 Extraction Inline CompleteEdwardsCurve.E.coordinates CompleteEdwardsCurve.E.zero.
+Extraction Inline GF25519BoundedCommon.proj_word GF25519BoundedCommon.Build_bounded_word GF25519BoundedCommon.Build_bounded_word'.
 
 (* Recursive Extraction sign. *)
   (* most of the code we want seems to be below [eq_dec1] and there is other stuff above that *)
diff --git a/src/Specific/GF25519BoundedCommon.v b/src/Specific/GF25519BoundedCommon.v
index 511370c63..900b2d564 100644
--- a/src/Specific/GF25519BoundedCommon.v
+++ b/src/Specific/GF25519BoundedCommon.v
@@ -46,10 +46,32 @@ Qed.
 
 (* BEGIN precomputation. *)
 Local Notation b_of exp := (0, 2^exp + 2^(exp-3))%Z (only parsing). (* max is [(0, 2^(exp+2) + 2^exp + 2^(exp-1) + 2^(exp-3) + 2^(exp-4) + 2^(exp-5) + 2^(exp-6) + 2^(exp-10) + 2^(exp-12) + 2^(exp-13) + 2^(exp-14) + 2^(exp-15) + 2^(exp-17) + 2^(exp-23) + 2^(exp-24))%Z] *)
-Record bounded_word (lower upper : Z) :=
-  Build_bounded_word'
-    { proj_word :> word64;
-      word_bounded : andb (lower <=? proj_word)%Z (proj_word <=? upper)%Z = true }.
+Module Type WordIsBounded.
+  Parameter is_boundedT : forall (lower upper : Z), word64 -> bool.
+  Parameter Build_is_boundedT : forall {lower upper} {proj_word : word64},
+      andb (lower <=? proj_word)%Z (proj_word <=? upper)%Z = true -> is_boundedT lower upper proj_word = true.
+  Parameter project_is_boundedT : forall {lower upper} {proj_word : word64},
+      is_boundedT lower upper proj_word = true -> andb (lower <=? proj_word)%Z (proj_word <=? upper)%Z = true.
+End WordIsBounded.
+
+Module Import WordIsBoundedDefault : WordIsBounded.
+  Definition is_boundedT : forall (lower upper : Z), word64 -> bool
+    := fun lower upper proj_word => andb (lower <=? proj_word)%Z (proj_word <=? upper)%Z.
+  Definition Build_is_boundedT {lower upper} {proj_word : word64}
+    : andb (lower <=? proj_word)%Z (proj_word <=? upper)%Z = true -> is_boundedT lower upper proj_word = true
+    := fun x => x.
+  Definition project_is_boundedT {lower upper} {proj_word : word64}
+    : is_boundedT lower upper proj_word = true -> andb (lower <=? proj_word)%Z (proj_word <=? upper)%Z = true
+    := fun x => x.
+End WordIsBoundedDefault.
+
+Definition bounded_word (lower upper : Z) := { proj_word : word64 | is_boundedT lower upper proj_word = true }.
+Definition proj_word {lower upper} (v : bounded_word lower upper) := Eval cbv [proj1_sig] in proj1_sig v.
+Definition word_bounded {lower upper} (v : bounded_word lower upper)
+  : andb (lower <=? proj_word v)%Z (proj_word v <=? upper)%Z = true
+  := project_is_boundedT (proj2_sig v).
+Definition Build_bounded_word' {lower upper} proj_word word_bounded : bounded_word lower upper
+  := exist _ proj_word (Build_is_boundedT word_bounded).
 Arguments proj_word {_ _} _.
 Arguments word_bounded {_ _} _.
 Arguments Build_bounded_word' {_ _} _ _.
@@ -69,7 +91,7 @@ Proof.
   rewrite Z.pow_Zpow; simpl Z.of_nat.
   intros H H'.
   assert (2^Z.of_nat e <= 2^64) by auto with zarith.
-  rewrite !ZToWord64ToZ by omega.
+  rewrite ?ZToWord64ToZ by omega.
   match goal with
   | [ |- context[andb ?x ?y] ]
     => destruct x eqn:?, y eqn:?; try reflexivity; Z.ltb_to_lt
@@ -107,6 +129,65 @@ Definition wire_digitsWToZ (x : wire_digitsW) : Specific.GF25519.wire_digits
 Definition wire_digitsZToW (x : Specific.GF25519.wire_digits) : wire_digitsW
   := let '(x0, x1, x2, x3, x4, x5, x6, x7) := x in
      (x0 : word64, x1 : word64, x2 : word64, x3 : word64, x4 : word64, x5 : word64, x6 : word64, x7 : word64).
+
+Definition app_7 {T} (f : wire_digitsW) (P : wire_digitsW -> T) : T.
+Proof.
+  cbv [wire_digitsW] in *.
+  set (f0 := f).
+  repeat (let g := fresh "g" in destruct f as [f g]).
+  apply P.
+  apply f0.
+Defined.
+
+Definition app_7_correct {T} f (P : wire_digitsW -> T) : app_7 f P = P f.
+Proof.
+  intros.
+  cbv [wire_digitsW] in *.
+  destruct_head' prod.
+  reflexivity.
+Qed.
+
+Definition app_10 {T} (f : fe25519W) (P : fe25519W -> T) : T.
+Proof.
+  cbv [fe25519W] in *.
+  set (f0 := f).
+  repeat (let g := fresh "g" in destruct f as [f g]).
+  apply P.
+  apply f0.
+Defined.
+
+Definition app_10_correct {T} f (P : fe25519W -> T) : app_10 f P = P f.
+Proof.
+  intros.
+  cbv [fe25519W] in *.
+  destruct_head' prod.
+  reflexivity.
+Qed.
+
+Definition appify2 {T} (op : fe25519W -> fe25519W -> T) (f g : fe25519W) :=
+  app_10 f (fun f0 => (app_10 g (fun g0 => op f0 g0))).
+
+Lemma appify2_correct : forall {T} op f g, @appify2 T op f g = op f g.
+Proof.
+  intros. cbv [appify2].
+  etransitivity; apply app_10_correct.
+Qed.
+
+Definition uncurry_unop_fe25519W {T} (op : fe25519W -> T)
+  := Eval cbv (*-[word64]*) in Tuple.uncurry (n:=length_fe25519) op.
+Definition curry_unop_fe25519W {T} op : fe25519W -> T
+  := Eval cbv (*-[word64]*) in fun f => app_10 f (Tuple.curry (n:=length_fe25519) op).
+Definition uncurry_binop_fe25519W {T} (op : fe25519W -> fe25519W -> T)
+  := Eval cbv (*-[word64]*) in uncurry_unop_fe25519W (fun f => uncurry_unop_fe25519W (op f)).
+Definition curry_binop_fe25519W {T} op : fe25519W -> fe25519W -> T
+  := Eval cbv (*-[word64]*) in appify2 (fun f => curry_unop_fe25519W (curry_unop_fe25519W op f)).
+
+Definition uncurry_unop_wire_digitsW {T} (op : wire_digitsW -> T)
+  := Eval cbv (*-[word64]*) in Tuple.uncurry (n:=length wire_widths) op.
+Definition curry_unop_wire_digitsW {T} op : wire_digitsW -> T
+  := Eval cbv (*-[word64]*) in fun f => app_7 f (Tuple.curry (n:=length wire_widths) op).
+
+
 Definition fe25519 :=
   Eval cbv [fst snd] in
     let sanity := eq_refl : length bounds = length limb_widths in
@@ -131,15 +212,15 @@ Definition is_bounded (x : Specific.GF25519.fe25519) : bool
 
 Lemma is_bounded_proj1_fe25519 (x : fe25519) : is_bounded (proj1_fe25519 x) = true.
 Proof.
-  refine (let '(Build_bounded_word' x0 p0, Build_bounded_word' x1 p1, Build_bounded_word' x2 p2, Build_bounded_word' x3 p3, Build_bounded_word' x4 p4,
-                Build_bounded_word' x5 p5, Build_bounded_word' x6 p6, Build_bounded_word' x7 p7, Build_bounded_word' x8 p8, Build_bounded_word' x9 p9)
+  refine (let '(exist x0 p0, exist x1 p1, exist x2 p2, exist x3 p3, exist x4 p4,
+                exist x5 p5, exist x6 p6, exist x7 p7, exist x8 p8, exist x9 p9)
             as x := x return is_bounded (proj1_fe25519 x) = true in
           _).
   cbv [is_bounded proj1_fe25519 proj1_fe25519W fe25519WToZ to_list length bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map List.rev List.app proj_word].
   apply fold_right_andb_true_iff_fold_right_and_True.
   cbv [fold_right List.map].
   cbv beta in *.
-  repeat split; assumption.
+  repeat split; auto using project_is_boundedT.
 Qed.
 
 Definition proj1_wire_digitsW (x : wire_digits) : wire_digitsW
@@ -158,15 +239,15 @@ Definition wire_digits_is_bounded (x : Specific.GF25519.wire_digits) : bool
 
 Lemma is_bounded_proj1_wire_digits (x : wire_digits) : wire_digits_is_bounded (proj1_wire_digits x) = true.
 Proof.
-  refine (let '(Build_bounded_word' x0 p0, Build_bounded_word' x1 p1, Build_bounded_word' x2 p2, Build_bounded_word' x3 p3, Build_bounded_word' x4 p4,
-                Build_bounded_word' x5 p5, Build_bounded_word' x6 p6, Build_bounded_word' x7 p7)
+  refine (let '(exist x0 p0, exist x1 p1, exist x2 p2, exist x3 p3, exist x4 p4,
+                exist x5 p5, exist x6 p6, exist x7 p7)
             as x := x return wire_digits_is_bounded (proj1_wire_digits x) = true in
           _).
   cbv [wire_digits_is_bounded proj1_wire_digits proj1_wire_digitsW wire_digitsWToZ to_list length wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map List.rev List.app proj_word].
   apply fold_right_andb_true_iff_fold_right_and_True.
   cbv [fold_right List.map].
   cbv beta in *.
-  repeat split; assumption.
+  repeat split; auto using project_is_boundedT.
 Qed.
 
 (** TODO: Turn this into a lemma to speed up proofs *)
@@ -190,7 +271,7 @@ Proof.
     | clearbody H'; clear H x;
       unfold_is_bounded_in H';
       exact H' ];
-    destruct_head and; auto;
+    destruct_head' and; simpl in *; auto;
       rewrite_hyp !*; reflexivity.
 Defined.
 
@@ -198,10 +279,10 @@ Definition exist_fe25519' (x : Specific.GF25519.fe25519) : is_bounded x = true -
 Proof.
   intro H; apply (exist_fe25519W (fe25519ZToW x)).
   abstract (
-      hnf in x; destruct_head prod;
+      hnf in x; destruct_head' prod;
       pose proof H as H';
       unfold_is_bounded_in H;
-      destruct_head and;
+      destruct_head' and; simpl in *;
       Z.ltb_to_lt;
       rewrite ?ZToWord64ToZ by (simpl; omega);
       assumption
@@ -214,9 +295,9 @@ Proof.
           fun H => _).
   let v := constr:(exist_fe25519' (x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) H) in
   let rec do_refine v :=
-      first [ let v' := (eval cbv [exist_fe25519W fe25519ZToW exist_fe25519' proj_word Build_bounded_word snd fst] in (proj_word v)) in
+      first [ let v' := (eval cbv [exist_fe25519W fe25519ZToW exist_fe25519' proj_word Build_bounded_word Build_bounded_word' snd fst] in (proj_word v)) in
               refine (Build_bounded_word v' _); abstract exact (word_bounded v)
-            | let v' := (eval cbv [exist_fe25519W fe25519ZToW exist_fe25519' proj_word Build_bounded_word snd fst] in (proj_word (snd v))) in
+            | let v' := (eval cbv [exist_fe25519W fe25519ZToW exist_fe25519' proj_word Build_bounded_word Build_bounded_word' snd fst] in (proj_word (snd v))) in
               refine (_, Build_bounded_word v' _);
               [ do_refine (fst v) | abstract exact (word_bounded (snd v)) ] ] in
   do_refine v.
@@ -241,9 +322,9 @@ Proof.
   revert pf.
   refine (let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) as x := x return forall pf : is_bounded x = true, proj1_fe25519 (exist_fe25519 x pf) = x in
           fun pf => _).
-  cbv [proj1_fe25519 exist_fe25519 proj1_fe25519W fe25519WToZ proj_word Build_bounded_word].
+  cbv [proj1_fe25519 exist_fe25519 proj1_fe25519W fe25519WToZ proj_word Build_bounded_word Build_bounded_word'].
   unfold_is_bounded_in pf.
-  destruct_head and.
+  destruct_head' and.
   Z.ltb_to_lt.
   rewrite ?ZToWord64ToZ by (rewrite unfold_Pow2_64; cbv [Pow2_64]; omega).
   reflexivity.
@@ -261,7 +342,7 @@ Proof.
     | clearbody H'; clear H x;
       unfold_is_bounded_in H';
       exact H' ];
-    destruct_head and; auto;
+    destruct_head' and; simpl in *; auto;
       rewrite_hyp !*; reflexivity.
 Defined.
 
@@ -269,10 +350,10 @@ Definition exist_wire_digits' (x : Specific.GF25519.wire_digits) : wire_digits_i
 Proof.
   intro H; apply (exist_wire_digitsW (wire_digitsZToW x)).
   abstract (
-      hnf in x; destruct_head prod;
+      hnf in x; destruct_head' prod;
       pose proof H as H';
       unfold_is_bounded_in H;
-      destruct_head and;
+      destruct_head' and; simpl in *;
       Z.ltb_to_lt;
       rewrite ?ZToWord64ToZ by (simpl; omega);
       assumption
@@ -285,9 +366,9 @@ Proof.
           fun H => _).
   let v := constr:(exist_wire_digits' (x0, x1, x2, x3, x4, x5, x6, x7) H) in
   let rec do_refine v :=
-      first [ let v' := (eval cbv [exist_wire_digitsW wire_digitsZToW exist_wire_digits' proj_word Build_bounded_word snd fst] in (proj_word v)) in
+      first [ let v' := (eval cbv [exist_wire_digitsW wire_digitsZToW exist_wire_digits' proj_word Build_bounded_word Build_bounded_word' snd fst] in (proj_word v)) in
               refine (Build_bounded_word v' _); abstract exact (word_bounded v)
-            | let v' := (eval cbv [exist_wire_digitsW wire_digitsZToW exist_wire_digits' proj_word Build_bounded_word snd fst] in (proj_word (snd v))) in
+            | let v' := (eval cbv [exist_wire_digitsW wire_digitsZToW exist_wire_digits' proj_word Build_bounded_word Build_bounded_word' snd fst] in (proj_word (snd v))) in
               refine (_, Build_bounded_word v' _);
               [ do_refine (fst v) | abstract exact (word_bounded (snd v)) ] ] in
   do_refine v.
@@ -312,9 +393,9 @@ Proof.
   revert pf.
   refine (let '(x0, x1, x2, x3, x4, x5, x6, x7) as x := x return forall pf : wire_digits_is_bounded x = true, proj1_wire_digits (exist_wire_digits x pf) = x in
           fun pf => _).
-  cbv [proj1_wire_digits exist_wire_digits proj1_wire_digitsW wire_digitsWToZ proj_word Build_bounded_word].
+  cbv [proj1_wire_digits exist_wire_digits proj1_wire_digitsW wire_digitsWToZ proj_word Build_bounded_word Build_bounded_word'].
   unfold_is_bounded_in pf.
-  destruct_head and.
+  destruct_head' and.
   Z.ltb_to_lt.
   rewrite ?ZToWord64ToZ by (rewrite unfold_Pow2_64; cbv [Pow2_64]; omega).
   reflexivity.
@@ -365,7 +446,7 @@ Proof.
   pose proof (bounded_encode x).
   generalize dependent (encode x).
   intro t; compute in t; intros.
-  destruct_head prod.
+  destruct_head' prod.
   unfold Pow2Base.bounded in H.
   pose proof (H 0%nat); pose proof (H 1%nat); pose proof (H 2%nat);
     pose proof (H 3%nat); pose proof (H 4%nat); pose proof (H 5%nat);