Begin filling in @JasonGross's stubs

3 files changed, 81 insertions, 49 deletions

diff --git a/src/Specific/GF25519Bounded.v b/src/Specific/GF25519Bounded.v
index f09b843f0..b7949bff8 100644
--- a/src/Specific/GF25519Bounded.v
+++ b/src/Specific/GF25519Bounded.v
@@ -62,6 +62,24 @@ Definition prefreezeW (f : fe25519W) : fe25519W := Eval simpl in interp_rprefree
 Definition ge_modulusW (f : fe25519W) : word64 := Eval simpl in interp_rge_modulus f.
 Definition packW (f : fe25519W) : wire_digitsW := Eval simpl in interp_rpack f.
 Definition unpackW (f : wire_digitsW) : fe25519W := Eval simpl in interp_runpack f.
+
+Require Import ModularBaseSystemWord.
+Definition modulusW :=
+  Eval cbv - [ZToWord64] in (Tuple.map ZToWord64 (Tuple.from_list_default 0%Z 10 GF25519.modulus_digits_)).
+
+Definition postfreeze : GF25519.fe25519 -> GF25519.fe25519 :=
+  GF25519.postfreeze.
+  
+Lemma freeze_prepost_freeze : forall x, postfreeze (prefreeze x) = GF25519.freeze x. Proof. reflexivity. Qed.
+
+Definition postfreezeW : fe25519W -> fe25519W :=
+      (conditional_subtract_modulusW
+         (num_limbs := 10)
+         modulusW
+         ge_modulusW
+         (Interpretations.Word64.neg GF25519.int_width)
+      ).
+
 Definition freezeW (f : fe25519W) : fe25519W := Eval cbv beta delta [prefreezeW postfreezeW] in postfreezeW (prefreezeW f).
 
 Local Transparent Let_In.
@@ -90,6 +108,64 @@ Lemma packW_correct_and_bounded : iunop_FEToWire_correct_and_bounded packW pack.
 Proof. port_correct_and_bounded interp_rpack_correct packW interp_rpack rpack_correct_and_bounded. Qed.
 Lemma unpackW_correct_and_bounded : iunop_WireToFE_correct_and_bounded unpackW unpack.
 Proof. port_correct_and_bounded interp_runpack_correct unpackW interp_runpack runpack_correct_and_bounded. Qed.
+
+(* TODO : move *)
+Lemma neg_range : forall x y, 0 <= x ->
+  0 <= ModularBaseSystemListZOperations.neg x y < 2 ^ x.
+Proof.
+  intros.
+  split; auto using ModularBaseSystemListZOperationsProofs.neg_nonneg.
+  eapply Z.le_lt_trans; eauto using ModularBaseSystemListZOperationsProofs.neg_upperbound.
+  rewrite Z.ones_equiv.
+  omega.
+Qed.
+  
+Lemma postfreezeW_correct_and_bounded : iunop_correct_and_bounded postfreezeW postfreeze.
+Proof.
+  intros x H.
+  pose proof (ge_modulusW_correct x H) as Hgm.
+  destruct_head_hnf' prod.
+  unfold_is_bounded_in H.
+  destruct_head' and.
+  Z.ltb_to_lt.
+  cbv [postfreezeW].
+  cbv [conditional_subtract_modulusW Interpretations.Word64.neg].
+  change word64ToZ with Interpretations.Word64.word64ToZ in *.
+  rewrite Hgm.
+
+  split.
+  
+  cbv [modulusW Tuple.map].
+  cbv [on_tuple List.map to_list to_list' from_list from_list'
+                Tuple.map2 on_tuple2 ListUtil.map2 fe25519WToZ].
+  cbv [postfreeze GF25519.postfreeze].
+  cbv [Let_In].
+  match goal with
+    |- (_,word64ToZ (_ ^- (Interpretations.Word64.ZToWord64 ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end.
+
+  change ZToWord64 with Interpretations.Word64.ZToWord64 in *.
+  rewrite !Interpretations.Word64.word64ToZ_sub;
+  rewrite !Interpretations.Word64.word64ToZ_land;
+  rewrite !Interpretations.Word64.word64ToZ_ZToWord64;
+  try match goal with
+         | |- 0 <=  ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply neg_range; omega
+         | |- 0 <= _ < 2 ^ Z.of_nat _ => vm_compute; split; [refine (fun x => match x with eq_refl => I end) | reflexivity]
+         | |- 0 <= _ &' _ => apply Z.land_nonneg; right; omega
+         | |- (_,_) = (_,_) => reflexivity
+      end;
+  try solve [
+  (apply Z.log2_lt_pow2_alt; [ vm_compute; reflexivity | ]);
+  eapply Z.le_lt_trans; try apply Z.land_upper_bound_r; try apply neg_range; try (vm_compute; discriminate); reflexivity].
+
+  { 
+  apply Z.le_0_sub.
+  cbv [ge_modulus Let_In ModularBaseSystemListZOperations.cmovl ModularBaseSystemListZOperations.cmovne ModularBaseSystemListZOperations.neg].
+  repeat break_if; Z.ltb_to_lt; subst; try omega;
+    rewrite ?Z.land_0_l; auto. }
+  
+
+Admitted.
+
 Lemma freezeW_correct_and_bounded : iunop_correct_and_bounded freezeW freeze.
 Proof.
   intros f H; rewrite <- freeze_prepost_freeze.
@@ -99,6 +175,8 @@ Proof.
   rewrite H1', H0', H0; split; reflexivity.
 Qed.
 
+
+
 Lemma powW_correct_and_bounded chain : iunop_correct_and_bounded (fun x => powW x chain) (fun x => pow x chain).
 Proof.
   cbv [powW pow].
diff --git a/src/Specific/GF25519BoundedCommon.v b/src/Specific/GF25519BoundedCommon.v
index d006e58af..cc864606a 100644
--- a/src/Specific/GF25519BoundedCommon.v
+++ b/src/Specific/GF25519BoundedCommon.v
@@ -23,7 +23,7 @@ Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.
 Local Open Scope Z.
 
 (* BEGIN common curve-specific definitions *)
-Definition bit_width : nat := 64%nat.
+Definition bit_width : nat := Eval compute in Z.to_nat (GF25519.int_width).
 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] *)
 Definition bounds_exp : tuple Z length_fe25519
   := Eval compute in
@@ -690,50 +690,4 @@ Notation iunop_WireToFE_correct_and_bounded irop op
          -> fe25519WToZ (irop x) = op (wire_digitsWToZ x)
             /\ is_bounded (fe25519WToZ (irop x)) = true) (only parsing).
 
-(** TODO(andreser): Remove me in favor of a GF25519.v definition *)
-Definition prefreeze :=
-fun fs => let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := fs in
-dlet a := f9 in
-dlet a0 := (Z.shiftr a 26 + f8)%Z in
-dlet a1 := (Z.shiftr a0 25 + f7)%Z in
-dlet a2 := (Z.shiftr a1 26 + f6)%Z in
-dlet a3 := (Z.shiftr a2 25 + f5)%Z in
-dlet a4 := (Z.shiftr a3 26 + f4)%Z in
-dlet a5 := (Z.shiftr a4 25 + f3)%Z in
-dlet a6 := (Z.shiftr a5 26 + f2)%Z in
-dlet a7 := (Z.shiftr a6 25 + f1)%Z in
-dlet a8 := (Z.shiftr a7 26 + f0)%Z in
-dlet a9 := (19 * Z.shiftr a8 25 + Z.land a 67108863)%Z in
-dlet a10 := (Z.shiftr a9 26 + Z.land a0 33554431)%Z in
-dlet a11 := (Z.shiftr a10 25 + Z.land a1 67108863)%Z in
-dlet a12 := (Z.shiftr a11 26 + Z.land a2 33554431)%Z in
-dlet a13 := (Z.shiftr a12 25 + Z.land a3 67108863)%Z in
-dlet a14 := (Z.shiftr a13 26 + Z.land a4 33554431)%Z in
-dlet a15 := (Z.shiftr a14 25 + Z.land a5 67108863)%Z in
-dlet a16 := (Z.shiftr a15 26 + Z.land a6 33554431)%Z in
-dlet a17 := (Z.shiftr a16 25 + Z.land a7 67108863)%Z in
-dlet a18 := (Z.shiftr a17 26 + Z.land a8 33554431)%Z in
-dlet a19 := (19 * Z.shiftr a18 25 + Z.land a9 67108863)%Z in
-dlet a20 := (Z.shiftr a19 26 + Z.land a10 33554431)%Z in
-dlet a21 := (Z.shiftr a20 25 + Z.land a11 67108863)%Z in
-dlet a22 := (Z.shiftr a21 26 + Z.land a12 33554431)%Z in
-dlet a23 := (Z.shiftr a22 25 + Z.land a13 67108863)%Z in
-dlet a24 := (Z.shiftr a23 26 + Z.land a14 33554431)%Z in
-dlet a25 := (Z.shiftr a24 25 + Z.land a15 67108863)%Z in
-dlet a26 := (Z.shiftr a25 26 + Z.land a16 33554431)%Z in
-dlet a27 := (Z.shiftr a26 25 + Z.land a17 67108863)%Z in
-dlet a28 := (Z.shiftr a27 26 + Z.land a18 33554431)%Z in
-
-((Z.land a28 33554431 )%Z, (Z.land a27 67108863 )%Z,
-(Z.land a26 33554431 )%Z, (Z.land a25 67108863 )%Z,
-(Z.land a24 33554431 )%Z, (Z.land a23 67108863 )%Z,
-(Z.land a22 33554431 )%Z, (Z.land a21 67108863 )%Z,
-(Z.land a20 33554431 )%Z, ( Z.land a19 67108863 )%Z).
-
-Axiom postfreeze : GF25519.fe25519 -> GF25519.fe25519.
-Axiom freeze_prepost_freeze : forall x, postfreeze (prefreeze x) = GF25519.freeze x.
-Axiom proof_admitted : False.
-Tactic Notation "admit" := abstract case proof_admitted.
-Definition postfreezeW : fe25519W -> fe25519W.
-Proof. admit. Defined.
-Axiom postfreezeW_correct_and_bounded : iunop_correct_and_bounded postfreezeW postfreeze.
+Definition prefreeze := GF25519.prefreeze.
diff --git a/src/Specific/GF25519Reflective/Reified/PreFreeze.v b/src/Specific/GF25519Reflective/Reified/PreFreeze.v
index 6b3bce924..9322185e3 100644
--- a/src/Specific/GF25519Reflective/Reified/PreFreeze.v
+++ b/src/Specific/GF25519Reflective/Reified/PreFreeze.v
@@ -1,6 +1,6 @@
 Require Import Crypto.Specific.GF25519Reflective.CommonUnOp.
 
-Definition rprefreezeZ_sig : rexpr_unop_sig prefreeze. Proof. reify_sig. Defined.
+Definition rprefreezeZ_sig : rexpr_unop_sig prefreeze. Proof. cbv [prefreeze GF25519.prefreeze]. reify_sig. Defined.
 Definition rprefreezeW := Eval vm_compute in rword_of_Z rprefreezeZ_sig.
 Lemma rprefreezeW_correct_and_bounded_gen : correct_and_bounded_genT rprefreezeW rprefreezeZ_sig.
 Proof. rexpr_correct. Qed.