Update bounds things with prefreeze

2 files changed, 13 insertions, 24 deletions

diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index b69d4224e..790fa4571 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -571,7 +571,6 @@ Proof.
   cbv [freeze_opt freeze Let_In].
   rewrite prefreeze_correct.
   rewrite postfreeze_correct.
-  Check from_list_default_eq.
   match goal with
     |- appcontext [to_list _ (from_list_default _ ?n ?xs)] =>
     assert (length xs = n) as pf; [ | rewrite from_list_default_eq with (pf0 := pf) ] end.
@@ -755,7 +754,7 @@ Print edwards_extended_add_coordinates.
 
 Local Existing Instance field25519.
 Create HintDb edwards_extended_add_coordinates_correct discriminated.
-Hint Rewrite 
+Hint Rewrite
      (Ring.homomorphism_mul(is_homomorphism:=homomorphism_F25519_decode))
      (Ring.homomorphism_add(H1             :=homomorphism_F25519_decode))
      (Ring.homomorphism_sub(H1             :=homomorphism_F25519_decode))
@@ -770,4 +769,4 @@ Proof.
   simpl.
   rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
   reflexivity.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/src/Specific/GF25519Bounded.v b/src/Specific/GF25519Bounded.v
index 66de326b2..2b9c824ed 100644
--- a/src/Specific/GF25519Bounded.v
+++ b/src/Specific/GF25519Bounded.v
@@ -10,6 +10,7 @@ Require Import Crypto.Specific.GF25519BoundedCommon.
 Require Import Crypto.Specific.GF25519Reflective.
 Require Import Bedrock.Word Crypto.Util.WordUtil.
 Require Import Coq.Lists.List Crypto.Util.ListUtil.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemWord.
 Require Import Crypto.Tactics.VerdiTactics.
 Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tuple.
@@ -63,18 +64,18 @@ Definition ge_modulusW (f : fe25519W) : word64 := Eval simpl in interp_rge_modul
 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_)).
+  Eval cbv - [ZToWord64] in (Tuple.map ZToWord64 (Tuple.from_list_default 0%Z length_fe25519 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.
+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)
+         (num_limbs := length_fe25519)
          modulusW
          ge_modulusW
          (Interpretations.Word64.neg GF25519.int_width)
@@ -111,17 +112,6 @@ Proof. port_correct_and_bounded interp_rpack_correct packW interp_rpack rpack_co
 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.
-
 Ltac lower_bound_minus_ge_modulus :=
   apply Z.le_0_sub;
   cbv [ge_modulus Let_In ModularBaseSystemListZOperations.cmovl ModularBaseSystemListZOperations.cmovne ModularBaseSystemListZOperations.neg];
@@ -165,14 +155,14 @@ Proof.
   rewrite !Interpretations.Word64.word64ToZ_land;
   rewrite !Interpretations.Word64.word64ToZ_ZToWord64;
   try match goal with
-         | |- 0 <=  ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply neg_range; omega
+         | |- 0 <=  ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.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; instantiate; try match goal with |- ?G => not has_evar G; vm_compute; discriminate end; reflexivity];
+  eapply Z.le_lt_trans; try apply Z.land_upper_bound_r; try apply ModularBaseSystemListZOperationsProofs.neg_range; instantiate; try match goal with |- ?G => not has_evar G; vm_compute; discriminate end; reflexivity];
   match goal with
   | |- 0 <= _ - _ => lower_bound_minus_ge_modulus
   | |- Z.log2 (_ - _) < _ => upper_bound_minus_ge_modulus
@@ -186,21 +176,21 @@ Proof.
   rewrite !Interpretations.Word64.word64ToZ_ZToWord64;
   repeat match goal with |- _ /\ _ => split; Z.ltb_to_lt end;
   try match goal with
-         | |- 0 <=  ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply neg_range; omega
+         | |- 0 <=  ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.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
       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; instantiate; try match goal with |- ?G => not has_evar G; vm_compute; discriminate end; reflexivity];
+  eapply Z.le_lt_trans; try apply Z.land_upper_bound_r; try apply ModularBaseSystemListZOperationsProofs.neg_range; instantiate; try match goal with |- ?G => not has_evar G; vm_compute; discriminate end; reflexivity];
   try match goal with
   | |- 0 <= _ - _ => lower_bound_minus_ge_modulus
   | |- Z.log2 (_ - _) < _ => upper_bound_minus_ge_modulus
   | |- _ - _ <= _ => etransitivity; [ apply Z.le_sub_nonneg; apply Z.land_nonneg; right; omega | instantiate; assumption ]
   | |- 0 <= ModularBaseSystemListZOperations.neg _ _ =>
-    apply neg_range; vm_compute; discriminate
+    apply ModularBaseSystemListZOperationsProofs.neg_range; vm_compute; discriminate
   | |- ModularBaseSystemListZOperations.neg _ _ < _ =>
-    apply neg_range; vm_compute; discriminate
+    apply ModularBaseSystemListZOperationsProofs.neg_range; vm_compute; discriminate
   | |- _ => vm_compute; (discriminate || reflexivity)
       end.
 Qed.