Update bounds things with prefreeze

17 files changed, 553 insertions, 222 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v b/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v
index 5d9e64901..6163650e4 100644
--- a/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v
@@ -16,3 +16,13 @@ Proof.
   unfold neg; intros; break_match; auto with zarith.
 Qed.
 Hint Resolve neg_upperbound : zarith.
+
+Lemma neg_range : forall x y, 0 <= x ->
+  0 <= neg x y < 2 ^ x.
+Proof.
+  intros.
+  split; auto using neg_nonneg.
+  eapply Z.le_lt_trans; eauto using neg_upperbound.
+  rewrite Z.ones_equiv.
+  omega.
+Qed.
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.
diff --git a/src/SpecificGen/GF2213_32.v b/src/SpecificGen/GF2213_32.v
index 4108ba2b0..58d9f2559 100644
--- a/src/SpecificGen/GF2213_32.v
+++ b/src/SpecificGen/GF2213_32.v
@@ -22,8 +22,8 @@ Local Open Scope Z.
 
 Definition modulus : Z := Eval compute in 2^221 - 3.
 Lemma prime_modulus : prime modulus. Admitted.
+Definition int_width := Eval compute in (2 * 32)%Z.
 Definition freeze_input_bound := 32%Z.
-Definition int_width := 32%Z.
 
 Instance params2213_32 : PseudoMersenneBaseParams modulus.
   construct_params prime_modulus 8%nat 221.
@@ -498,8 +498,37 @@ Proof.
   assumption.
 Defined.
 
-Definition freeze_sig (f : fe2213_32) :
-  { f' : fe2213_32 | f' = from_list_default 0 8 (freeze_opt (int_width := int_width) c_ (to_list 8 f)) }.
+Definition prefreeze_sig (f : fe2213_32) :
+  { f' : fe2213_32 | f' = from_list_default 0 8 (carry_full_3_opt c_ (to_list 8 f)) }.
+Proof.
+  cbv [fe2213_32] in *.
+  repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
+  eexists.
+  cbv - [from_list_default].
+  (* TODO(jgross,jadep): use Reflective linearization here? *)
+  repeat (
+       set_evars; rewrite app_Let_In_nd; subst_evars;
+       eapply Proper_Let_In_nd_changebody; [reflexivity|intro]).
+  cbv [from_list_default from_list_default'].
+  reflexivity.
+Defined.
+
+Definition prefreeze (f : fe2213_32) : fe2213_32 :=
+  Eval cbv beta iota delta [proj1_sig prefreeze_sig] in
+    let '(f0, f1, f2, f3, f4, f5, f6, f7) := f in
+    proj1_sig (prefreeze_sig (f0, f1, f2, f3, f4, f5, f6, f7)).
+
+Definition prefreeze_correct (f : fe2213_32)
+  : prefreeze f = from_list_default 0 8 (carry_full_3_opt c_ (to_list 8 f)).
+Proof.
+  pose proof (proj2_sig (prefreeze_sig f)).
+  cbv [fe2213_32] in *.
+  repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
+  assumption.
+Defined.
+
+Definition postfreeze_sig (f : fe2213_32) :
+  { f' : fe2213_32 | f' = from_list_default 0 8 (conditional_subtract_modulus_opt (int_width := int_width) (to_list 8 f)) }.
 Proof.
   cbv [fe2213_32] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
@@ -516,20 +545,40 @@ Proof.
   reflexivity.
 Defined.
 
-Definition freeze (f : fe2213_32) : fe2213_32 :=
-  Eval cbv beta iota delta [proj1_sig freeze_sig] in
+Definition postfreeze (f : fe2213_32) : fe2213_32 :=
+  Eval cbv beta iota delta [proj1_sig postfreeze_sig] in
     let '(f0, f1, f2, f3, f4, f5, f6, f7) := f in
-    proj1_sig (freeze_sig (f0, f1, f2, f3, f4, f5, f6, f7)).
+    proj1_sig (postfreeze_sig (f0, f1, f2, f3, f4, f5, f6, f7)).
 
-Definition freeze_correct (f : fe2213_32)
-  : freeze f = from_list_default 0 8 (freeze_opt (int_width := int_width) c_ (to_list 8 f)).
+Definition postfreeze_correct (f : fe2213_32)
+  : postfreeze f = from_list_default 0 8 (conditional_subtract_modulus_opt (int_width := int_width) (to_list 8 f)).
 Proof.
-  pose proof (proj2_sig (freeze_sig f)).
+  pose proof (proj2_sig (postfreeze_sig f)).
   cbv [fe2213_32] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
   assumption.
 Defined.
 
+Definition freeze (f : fe2213_32) : fe2213_32 :=
+  dlet x := prefreeze f in
+  postfreeze x.
+
+Local Transparent Let_In.
+Definition freeze_correct (f : fe2213_32)
+  : freeze f = from_list_default 0 8 (freeze_opt (int_width := int_width) c_ (to_list 8 f)).
+Proof.
+  cbv [freeze_opt freeze Let_In].
+  rewrite prefreeze_correct.
+  rewrite postfreeze_correct.
+  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.
+  { rewrite carry_full_3_opt_correct; repeat rewrite ModularBaseSystemListProofs.length_carry_full; auto using length_to_list. }
+  rewrite to_list_from_list.
+  reflexivity.
+Qed.
+Local Opaque Let_In.
+
 Definition fieldwiseb_sig (f g : fe2213_32) :
   { b | b = @fieldwiseb Z Z 8 Z.eqb f g }.
 Proof.
diff --git a/src/SpecificGen/GF2213_32Bounded.v b/src/SpecificGen/GF2213_32Bounded.v
index f304eb648..eeb871b73 100644
--- a/src/SpecificGen/GF2213_32Bounded.v
+++ b/src/SpecificGen/GF2213_32Bounded.v
@@ -10,6 +10,7 @@ Require Import Crypto.SpecificGen.GF2213_32BoundedCommon.
 Require Import Crypto.SpecificGen.GF2213_32Reflective.
 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 : fe2213_32W) : word64 := Eval simpl in interp_rge_mod
 Definition packW (f : fe2213_32W) : wire_digitsW := Eval simpl in interp_rpack f.
 Definition unpackW (f : wire_digitsW) : fe2213_32W := 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 GF2213_32.modulus_digits_)).
+  Eval cbv - [ZToWord64] in (Tuple.map ZToWord64 (Tuple.from_list_default 0%Z length_fe2213_32 GF2213_32.modulus_digits_)).
 
 Definition postfreeze : GF2213_32.fe2213_32 -> GF2213_32.fe2213_32 :=
   GF2213_32.postfreeze.
 
-Lemma freeze_prepost_freeze : forall x, postfreeze (prefreeze x) = GF2213_32.freeze x. Proof. reflexivity. Qed.
+Lemma freeze_prepost_freeze : forall x, postfreeze (prefreeze x) = GF2213_32.freeze x.
+Proof. reflexivity. Qed.
 
 Definition postfreezeW : fe2213_32W -> fe2213_32W :=
       (conditional_subtract_modulusW
-         (num_limbs := 10)
+         (num_limbs := length_fe2213_32)
          modulusW
          ge_modulusW
          (Interpretations.Word64.neg GF2213_32.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.
diff --git a/src/SpecificGen/GF2519_32.v b/src/SpecificGen/GF2519_32.v
index 9c350a04f..084e5ec57 100644
--- a/src/SpecificGen/GF2519_32.v
+++ b/src/SpecificGen/GF2519_32.v
@@ -22,8 +22,8 @@ Local Open Scope Z.
 
 Definition modulus : Z := Eval compute in 2^251 - 9.
 Lemma prime_modulus : prime modulus. Admitted.
+Definition int_width := Eval compute in (2 * 32)%Z.
 Definition freeze_input_bound := 32%Z.
-Definition int_width := 32%Z.
 
 Instance params2519_32 : PseudoMersenneBaseParams modulus.
   construct_params prime_modulus 10%nat 251.
@@ -481,8 +481,37 @@ Proof.
   assumption.
 Defined.
 
-Definition freeze_sig (f : fe2519_32) :
-  { f' : fe2519_32 | f' = from_list_default 0 10 (freeze_opt (int_width := int_width) c_ (to_list 10 f)) }.
+Definition prefreeze_sig (f : fe2519_32) :
+  { f' : fe2519_32 | f' = from_list_default 0 10 (carry_full_3_opt c_ (to_list 10 f)) }.
+Proof.
+  cbv [fe2519_32] in *.
+  repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
+  eexists.
+  cbv - [from_list_default].
+  (* TODO(jgross,jadep): use Reflective linearization here? *)
+  repeat (
+       set_evars; rewrite app_Let_In_nd; subst_evars;
+       eapply Proper_Let_In_nd_changebody; [reflexivity|intro]).
+  cbv [from_list_default from_list_default'].
+  reflexivity.
+Defined.
+
+Definition prefreeze (f : fe2519_32) : fe2519_32 :=
+  Eval cbv beta iota delta [proj1_sig prefreeze_sig] in
+    let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in
+    proj1_sig (prefreeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9)).
+
+Definition prefreeze_correct (f : fe2519_32)
+  : prefreeze f = from_list_default 0 10 (carry_full_3_opt c_ (to_list 10 f)).
+Proof.
+  pose proof (proj2_sig (prefreeze_sig f)).
+  cbv [fe2519_32] in *.
+  repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
+  assumption.
+Defined.
+
+Definition postfreeze_sig (f : fe2519_32) :
+  { f' : fe2519_32 | f' = from_list_default 0 10 (conditional_subtract_modulus_opt (int_width := int_width) (to_list 10 f)) }.
 Proof.
   cbv [fe2519_32] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
@@ -499,20 +528,40 @@ Proof.
   reflexivity.
 Defined.
 
-Definition freeze (f : fe2519_32) : fe2519_32 :=
-  Eval cbv beta iota delta [proj1_sig freeze_sig] in
+Definition postfreeze (f : fe2519_32) : fe2519_32 :=
+  Eval cbv beta iota delta [proj1_sig postfreeze_sig] in
     let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in
-    proj1_sig (freeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9)).
+    proj1_sig (postfreeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9)).
 
-Definition freeze_correct (f : fe2519_32)
-  : freeze f = from_list_default 0 10 (freeze_opt (int_width := int_width) c_ (to_list 10 f)).
+Definition postfreeze_correct (f : fe2519_32)
+  : postfreeze f = from_list_default 0 10 (conditional_subtract_modulus_opt (int_width := int_width) (to_list 10 f)).
 Proof.
-  pose proof (proj2_sig (freeze_sig f)).
+  pose proof (proj2_sig (postfreeze_sig f)).
   cbv [fe2519_32] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
   assumption.
 Defined.
 
+Definition freeze (f : fe2519_32) : fe2519_32 :=
+  dlet x := prefreeze f in
+  postfreeze x.
+
+Local Transparent Let_In.
+Definition freeze_correct (f : fe2519_32)
+  : freeze f = from_list_default 0 10 (freeze_opt (int_width := int_width) c_ (to_list 10 f)).
+Proof.
+  cbv [freeze_opt freeze Let_In].
+  rewrite prefreeze_correct.
+  rewrite postfreeze_correct.
+  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.
+  { rewrite carry_full_3_opt_correct; repeat rewrite ModularBaseSystemListProofs.length_carry_full; auto using length_to_list. }
+  rewrite to_list_from_list.
+  reflexivity.
+Qed.
+Local Opaque Let_In.
+
 Definition fieldwiseb_sig (f g : fe2519_32) :
   { b | b = @fieldwiseb Z Z 10 Z.eqb f g }.
 Proof.
diff --git a/src/SpecificGen/GF2519_32Bounded.v b/src/SpecificGen/GF2519_32Bounded.v
index a878292a2..bc907bdf1 100644
--- a/src/SpecificGen/GF2519_32Bounded.v
+++ b/src/SpecificGen/GF2519_32Bounded.v
@@ -10,6 +10,7 @@ Require Import Crypto.SpecificGen.GF2519_32BoundedCommon.
 Require Import Crypto.SpecificGen.GF2519_32Reflective.
 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 : fe2519_32W) : word64 := Eval simpl in interp_rge_mod
 Definition packW (f : fe2519_32W) : wire_digitsW := Eval simpl in interp_rpack f.
 Definition unpackW (f : wire_digitsW) : fe2519_32W := 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 GF2519_32.modulus_digits_)).
+  Eval cbv - [ZToWord64] in (Tuple.map ZToWord64 (Tuple.from_list_default 0%Z length_fe2519_32 GF2519_32.modulus_digits_)).
 
 Definition postfreeze : GF2519_32.fe2519_32 -> GF2519_32.fe2519_32 :=
   GF2519_32.postfreeze.
 
-Lemma freeze_prepost_freeze : forall x, postfreeze (prefreeze x) = GF2519_32.freeze x. Proof. reflexivity. Qed.
+Lemma freeze_prepost_freeze : forall x, postfreeze (prefreeze x) = GF2519_32.freeze x.
+Proof. reflexivity. Qed.
 
 Definition postfreezeW : fe2519_32W -> fe2519_32W :=
       (conditional_subtract_modulusW
-         (num_limbs := 10)
+         (num_limbs := length_fe2519_32)
          modulusW
          ge_modulusW
          (Interpretations.Word64.neg GF2519_32.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.
diff --git a/src/SpecificGen/GF25519_32.v b/src/SpecificGen/GF25519_32.v
index ba2e76a0b..920da6dde 100644
--- a/src/SpecificGen/GF25519_32.v
+++ b/src/SpecificGen/GF25519_32.v
@@ -22,8 +22,8 @@ Local Open Scope Z.
 
 Definition modulus : Z := Eval compute in 2^255 - 19.
 Lemma prime_modulus : prime modulus. Admitted.
+Definition int_width := Eval compute in (2 * 32)%Z.
 Definition freeze_input_bound := 32%Z.
-Definition int_width := 32%Z.
 
 Instance params25519_32 : PseudoMersenneBaseParams modulus.
   construct_params prime_modulus 10%nat 255.
@@ -498,8 +498,37 @@ Proof.
   assumption.
 Defined.
 
-Definition freeze_sig (f : fe25519_32) :
-  { f' : fe25519_32 | f' = from_list_default 0 10 (freeze_opt (int_width := int_width) c_ (to_list 10 f)) }.
+Definition prefreeze_sig (f : fe25519_32) :
+  { f' : fe25519_32 | f' = from_list_default 0 10 (carry_full_3_opt c_ (to_list 10 f)) }.
+Proof.
+  cbv [fe25519_32] in *.
+  repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
+  eexists.
+  cbv - [from_list_default].
+  (* TODO(jgross,jadep): use Reflective linearization here? *)
+  repeat (
+       set_evars; rewrite app_Let_In_nd; subst_evars;
+       eapply Proper_Let_In_nd_changebody; [reflexivity|intro]).
+  cbv [from_list_default from_list_default'].
+  reflexivity.
+Defined.
+
+Definition prefreeze (f : fe25519_32) : fe25519_32 :=
+  Eval cbv beta iota delta [proj1_sig prefreeze_sig] in
+    let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in
+    proj1_sig (prefreeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9)).
+
+Definition prefreeze_correct (f : fe25519_32)
+  : prefreeze f = from_list_default 0 10 (carry_full_3_opt c_ (to_list 10 f)).
+Proof.
+  pose proof (proj2_sig (prefreeze_sig f)).
+  cbv [fe25519_32] in *.
+  repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
+  assumption.
+Defined.
+
+Definition postfreeze_sig (f : fe25519_32) :
+  { f' : fe25519_32 | f' = from_list_default 0 10 (conditional_subtract_modulus_opt (int_width := int_width) (to_list 10 f)) }.
 Proof.
   cbv [fe25519_32] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
@@ -516,20 +545,40 @@ Proof.
   reflexivity.
 Defined.
 
-Definition freeze (f : fe25519_32) : fe25519_32 :=
-  Eval cbv beta iota delta [proj1_sig freeze_sig] in
+Definition postfreeze (f : fe25519_32) : fe25519_32 :=
+  Eval cbv beta iota delta [proj1_sig postfreeze_sig] in
     let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in
-    proj1_sig (freeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9)).
+    proj1_sig (postfreeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9)).
 
-Definition freeze_correct (f : fe25519_32)
-  : freeze f = from_list_default 0 10 (freeze_opt (int_width := int_width) c_ (to_list 10 f)).
+Definition postfreeze_correct (f : fe25519_32)
+  : postfreeze f = from_list_default 0 10 (conditional_subtract_modulus_opt (int_width := int_width) (to_list 10 f)).
 Proof.
-  pose proof (proj2_sig (freeze_sig f)).
+  pose proof (proj2_sig (postfreeze_sig f)).
   cbv [fe25519_32] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
   assumption.
 Defined.
 
+Definition freeze (f : fe25519_32) : fe25519_32 :=
+  dlet x := prefreeze f in
+  postfreeze x.
+
+Local Transparent Let_In.
+Definition freeze_correct (f : fe25519_32)
+  : freeze f = from_list_default 0 10 (freeze_opt (int_width := int_width) c_ (to_list 10 f)).
+Proof.
+  cbv [freeze_opt freeze Let_In].
+  rewrite prefreeze_correct.
+  rewrite postfreeze_correct.
+  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.
+  { rewrite carry_full_3_opt_correct; repeat rewrite ModularBaseSystemListProofs.length_carry_full; auto using length_to_list. }
+  rewrite to_list_from_list.
+  reflexivity.
+Qed.
+Local Opaque Let_In.
+
 Definition fieldwiseb_sig (f g : fe25519_32) :
   { b | b = @fieldwiseb Z Z 10 Z.eqb f g }.
 Proof.
diff --git a/src/SpecificGen/GF25519_32Bounded.v b/src/SpecificGen/GF25519_32Bounded.v
index 8a978fc6f..41e20b6e6 100644
--- a/src/SpecificGen/GF25519_32Bounded.v
+++ b/src/SpecificGen/GF25519_32Bounded.v
@@ -10,6 +10,7 @@ Require Import Crypto.SpecificGen.GF25519_32BoundedCommon.
 Require Import Crypto.SpecificGen.GF25519_32Reflective.
 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 : fe25519_32W) : word64 := Eval simpl in interp_rge_mo
 Definition packW (f : fe25519_32W) : wire_digitsW := Eval simpl in interp_rpack f.
 Definition unpackW (f : wire_digitsW) : fe25519_32W := 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_32.modulus_digits_)).
+  Eval cbv - [ZToWord64] in (Tuple.map ZToWord64 (Tuple.from_list_default 0%Z length_fe25519_32 GF25519_32.modulus_digits_)).
 
 Definition postfreeze : GF25519_32.fe25519_32 -> GF25519_32.fe25519_32 :=
   GF25519_32.postfreeze.
 
-Lemma freeze_prepost_freeze : forall x, postfreeze (prefreeze x) = GF25519_32.freeze x. Proof. reflexivity. Qed.
+Lemma freeze_prepost_freeze : forall x, postfreeze (prefreeze x) = GF25519_32.freeze x.
+Proof. reflexivity. Qed.
 
 Definition postfreezeW : fe25519_32W -> fe25519_32W :=
       (conditional_subtract_modulusW
-         (num_limbs := 10)
+         (num_limbs := length_fe25519_32)
          modulusW
          ge_modulusW
          (Interpretations.Word64.neg GF25519_32.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.
diff --git a/src/SpecificGen/GF25519_64.v b/src/SpecificGen/GF25519_64.v
index d5970edea..f68c52382 100644
--- a/src/SpecificGen/GF25519_64.v
+++ b/src/SpecificGen/GF25519_64.v
@@ -22,8 +22,8 @@ Local Open Scope Z.
 
 Definition modulus : Z := Eval compute in 2^255 - 19.
 Lemma prime_modulus : prime modulus. Admitted.
+Definition int_width := Eval compute in (2 * 64)%Z.
 Definition freeze_input_bound := 64%Z.
-Definition int_width := 64%Z.
 
 Instance params25519_64 : PseudoMersenneBaseParams modulus.
   construct_params prime_modulus 5%nat 255.
@@ -498,8 +498,37 @@ Proof.
   assumption.
 Defined.
 
-Definition freeze_sig (f : fe25519_64) :
-  { f' : fe25519_64 | f' = from_list_default 0 5 (freeze_opt (int_width := int_width) c_ (to_list 5 f)) }.
+Definition prefreeze_sig (f : fe25519_64) :
+  { f' : fe25519_64 | f' = from_list_default 0 5 (carry_full_3_opt c_ (to_list 5 f)) }.
+Proof.
+  cbv [fe25519_64] in *.
+  repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
+  eexists.
+  cbv - [from_list_default].
+  (* TODO(jgross,jadep): use Reflective linearization here? *)
+  repeat (
+       set_evars; rewrite app_Let_In_nd; subst_evars;
+       eapply Proper_Let_In_nd_changebody; [reflexivity|intro]).
+  cbv [from_list_default from_list_default'].
+  reflexivity.
+Defined.
+
+Definition prefreeze (f : fe25519_64) : fe25519_64 :=
+  Eval cbv beta iota delta [proj1_sig prefreeze_sig] in
+    let '(f0, f1, f2, f3, f4) := f in
+    proj1_sig (prefreeze_sig (f0, f1, f2, f3, f4)).
+
+Definition prefreeze_correct (f : fe25519_64)
+  : prefreeze f = from_list_default 0 5 (carry_full_3_opt c_ (to_list 5 f)).
+Proof.
+  pose proof (proj2_sig (prefreeze_sig f)).
+  cbv [fe25519_64] in *.
+  repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
+  assumption.
+Defined.
+
+Definition postfreeze_sig (f : fe25519_64) :
+  { f' : fe25519_64 | f' = from_list_default 0 5 (conditional_subtract_modulus_opt (int_width := int_width) (to_list 5 f)) }.
 Proof.
   cbv [fe25519_64] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
@@ -516,20 +545,40 @@ Proof.
   reflexivity.
 Defined.
 
-Definition freeze (f : fe25519_64) : fe25519_64 :=
-  Eval cbv beta iota delta [proj1_sig freeze_sig] in
+Definition postfreeze (f : fe25519_64) : fe25519_64 :=
+  Eval cbv beta iota delta [proj1_sig postfreeze_sig] in
     let '(f0, f1, f2, f3, f4) := f in
-    proj1_sig (freeze_sig (f0, f1, f2, f3, f4)).
+    proj1_sig (postfreeze_sig (f0, f1, f2, f3, f4)).
 
-Definition freeze_correct (f : fe25519_64)
-  : freeze f = from_list_default 0 5 (freeze_opt (int_width := int_width) c_ (to_list 5 f)).
+Definition postfreeze_correct (f : fe25519_64)
+  : postfreeze f = from_list_default 0 5 (conditional_subtract_modulus_opt (int_width := int_width) (to_list 5 f)).
 Proof.
-  pose proof (proj2_sig (freeze_sig f)).
+  pose proof (proj2_sig (postfreeze_sig f)).
   cbv [fe25519_64] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
   assumption.
 Defined.
 
+Definition freeze (f : fe25519_64) : fe25519_64 :=
+  dlet x := prefreeze f in
+  postfreeze x.
+
+Local Transparent Let_In.
+Definition freeze_correct (f : fe25519_64)
+  : freeze f = from_list_default 0 5 (freeze_opt (int_width := int_width) c_ (to_list 5 f)).
+Proof.
+  cbv [freeze_opt freeze Let_In].
+  rewrite prefreeze_correct.
+  rewrite postfreeze_correct.
+  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.
+  { rewrite carry_full_3_opt_correct; repeat rewrite ModularBaseSystemListProofs.length_carry_full; auto using length_to_list. }
+  rewrite to_list_from_list.
+  reflexivity.
+Qed.
+Local Opaque Let_In.
+
 Definition fieldwiseb_sig (f g : fe25519_64) :
   { b | b = @fieldwiseb Z Z 5 Z.eqb f g }.
 Proof.
diff --git a/src/SpecificGen/GF25519_64Bounded.v b/src/SpecificGen/GF25519_64Bounded.v
index 528e536a0..8a6ef8eb7 100644
--- a/src/SpecificGen/GF25519_64Bounded.v
+++ b/src/SpecificGen/GF25519_64Bounded.v
@@ -10,6 +10,7 @@ Require Import Crypto.SpecificGen.GF25519_64BoundedCommon.
 Require Import Crypto.SpecificGen.GF25519_64Reflective.
 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 : fe25519_64W) : word64 := Eval simpl in interp_rge_mo
 Definition packW (f : fe25519_64W) : wire_digitsW := Eval simpl in interp_rpack f.
 Definition unpackW (f : wire_digitsW) : fe25519_64W := 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_64.modulus_digits_)).
+  Eval cbv - [ZToWord64] in (Tuple.map ZToWord64 (Tuple.from_list_default 0%Z length_fe25519_64 GF25519_64.modulus_digits_)).
 
 Definition postfreeze : GF25519_64.fe25519_64 -> GF25519_64.fe25519_64 :=
   GF25519_64.postfreeze.
 
-Lemma freeze_prepost_freeze : forall x, postfreeze (prefreeze x) = GF25519_64.freeze x. Proof. reflexivity. Qed.
+Lemma freeze_prepost_freeze : forall x, postfreeze (prefreeze x) = GF25519_64.freeze x.
+Proof. reflexivity. Qed.
 
 Definition postfreezeW : fe25519_64W -> fe25519_64W :=
       (conditional_subtract_modulusW
-         (num_limbs := 10)
+         (num_limbs := length_fe25519_64)
          modulusW
          ge_modulusW
          (Interpretations.Word64.neg GF25519_64.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.
diff --git a/src/SpecificGen/GF41417_32.v b/src/SpecificGen/GF41417_32.v
index 345f4b7b0..03590bf8c 100644
--- a/src/SpecificGen/GF41417_32.v
+++ b/src/SpecificGen/GF41417_32.v
@@ -22,8 +22,8 @@ Local Open Scope Z.
 
 Definition modulus : Z := Eval compute in 2^414 - 17.
 Lemma prime_modulus : prime modulus. Admitted.
+Definition int_width := Eval compute in (2 * 32)%Z.
 Definition freeze_input_bound := 32%Z.
-Definition int_width := 32%Z.
 
 Instance params41417_32 : PseudoMersenneBaseParams modulus.
   construct_params prime_modulus 18%nat 414.
@@ -481,8 +481,37 @@ Proof.
   assumption.
 Defined.
 
-Definition freeze_sig (f : fe41417_32) :
-  { f' : fe41417_32 | f' = from_list_default 0 18 (freeze_opt (int_width := int_width) c_ (to_list 18 f)) }.
+Definition prefreeze_sig (f : fe41417_32) :
+  { f' : fe41417_32 | f' = from_list_default 0 18 (carry_full_3_opt c_ (to_list 18 f)) }.
+Proof.
+  cbv [fe41417_32] in *.
+  repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
+  eexists.
+  cbv - [from_list_default].
+  (* TODO(jgross,jadep): use Reflective linearization here? *)
+  repeat (
+       set_evars; rewrite app_Let_In_nd; subst_evars;
+       eapply Proper_Let_In_nd_changebody; [reflexivity|intro]).
+  cbv [from_list_default from_list_default'].
+  reflexivity.
+Defined.
+
+Definition prefreeze (f : fe41417_32) : fe41417_32 :=
+  Eval cbv beta iota delta [proj1_sig prefreeze_sig] in
+    let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17) := f in
+    proj1_sig (prefreeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17)).
+
+Definition prefreeze_correct (f : fe41417_32)
+  : prefreeze f = from_list_default 0 18 (carry_full_3_opt c_ (to_list 18 f)).
+Proof.
+  pose proof (proj2_sig (prefreeze_sig f)).
+  cbv [fe41417_32] in *.
+  repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
+  assumption.
+Defined.
+
+Definition postfreeze_sig (f : fe41417_32) :
+  { f' : fe41417_32 | f' = from_list_default 0 18 (conditional_subtract_modulus_opt (int_width := int_width) (to_list 18 f)) }.
 Proof.
   cbv [fe41417_32] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
@@ -499,20 +528,40 @@ Proof.
   reflexivity.
 Defined.
 
-Definition freeze (f : fe41417_32) : fe41417_32 :=
-  Eval cbv beta iota delta [proj1_sig freeze_sig] in
+Definition postfreeze (f : fe41417_32) : fe41417_32 :=
+  Eval cbv beta iota delta [proj1_sig postfreeze_sig] in
     let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17) := f in
-    proj1_sig (freeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17)).
+    proj1_sig (postfreeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17)).
 
-Definition freeze_correct (f : fe41417_32)
-  : freeze f = from_list_default 0 18 (freeze_opt (int_width := int_width) c_ (to_list 18 f)).
+Definition postfreeze_correct (f : fe41417_32)
+  : postfreeze f = from_list_default 0 18 (conditional_subtract_modulus_opt (int_width := int_width) (to_list 18 f)).
 Proof.
-  pose proof (proj2_sig (freeze_sig f)).
+  pose proof (proj2_sig (postfreeze_sig f)).
   cbv [fe41417_32] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
   assumption.
 Defined.
 
+Definition freeze (f : fe41417_32) : fe41417_32 :=
+  dlet x := prefreeze f in
+  postfreeze x.
+
+Local Transparent Let_In.
+Definition freeze_correct (f : fe41417_32)
+  : freeze f = from_list_default 0 18 (freeze_opt (int_width := int_width) c_ (to_list 18 f)).
+Proof.
+  cbv [freeze_opt freeze Let_In].
+  rewrite prefreeze_correct.
+  rewrite postfreeze_correct.
+  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.
+  { rewrite carry_full_3_opt_correct; repeat rewrite ModularBaseSystemListProofs.length_carry_full; auto using length_to_list. }
+  rewrite to_list_from_list.
+  reflexivity.
+Qed.
+Local Opaque Let_In.
+
 Definition fieldwiseb_sig (f g : fe41417_32) :
   { b | b = @fieldwiseb Z Z 18 Z.eqb f g }.
 Proof.
diff --git a/src/SpecificGen/GF41417_32Bounded.v b/src/SpecificGen/GF41417_32Bounded.v
index d44c722b2..9e1cec774 100644
--- a/src/SpecificGen/GF41417_32Bounded.v
+++ b/src/SpecificGen/GF41417_32Bounded.v
@@ -10,6 +10,7 @@ Require Import Crypto.SpecificGen.GF41417_32BoundedCommon.
 Require Import Crypto.SpecificGen.GF41417_32Reflective.
 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 : fe41417_32W) : word64 := Eval simpl in interp_rge_mo
 Definition packW (f : fe41417_32W) : wire_digitsW := Eval simpl in interp_rpack f.
 Definition unpackW (f : wire_digitsW) : fe41417_32W := 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 GF41417_32.modulus_digits_)).
+  Eval cbv - [ZToWord64] in (Tuple.map ZToWord64 (Tuple.from_list_default 0%Z length_fe41417_32 GF41417_32.modulus_digits_)).
 
 Definition postfreeze : GF41417_32.fe41417_32 -> GF41417_32.fe41417_32 :=
   GF41417_32.postfreeze.
 
-Lemma freeze_prepost_freeze : forall x, postfreeze (prefreeze x) = GF41417_32.freeze x. Proof. reflexivity. Qed.
+Lemma freeze_prepost_freeze : forall x, postfreeze (prefreeze x) = GF41417_32.freeze x.
+Proof. reflexivity. Qed.
 
 Definition postfreezeW : fe41417_32W -> fe41417_32W :=
       (conditional_subtract_modulusW
-         (num_limbs := 10)
+         (num_limbs := length_fe41417_32)
          modulusW
          ge_modulusW
          (Interpretations.Word64.neg GF41417_32.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.
diff --git a/src/SpecificGen/GF5211_32.v b/src/SpecificGen/GF5211_32.v
index c2272aa1a..bca4d1050 100644
--- a/src/SpecificGen/GF5211_32.v
+++ b/src/SpecificGen/GF5211_32.v
@@ -22,8 +22,8 @@ Local Open Scope Z.
 
 Definition modulus : Z := Eval compute in 2^521 - 1.
 Lemma prime_modulus : prime modulus. Admitted.
+Definition int_width := Eval compute in (2 * 32)%Z.
 Definition freeze_input_bound := 32%Z.
-Definition int_width := 32%Z.
 
 Instance params5211_32 : PseudoMersenneBaseParams modulus.
   construct_params prime_modulus 20%nat 521.
@@ -481,8 +481,37 @@ Proof.
   assumption.
 Defined.
 
-Definition freeze_sig (f : fe5211_32) :
-  { f' : fe5211_32 | f' = from_list_default 0 20 (freeze_opt (int_width := int_width) c_ (to_list 20 f)) }.
+Definition prefreeze_sig (f : fe5211_32) :
+  { f' : fe5211_32 | f' = from_list_default 0 20 (carry_full_3_opt c_ (to_list 20 f)) }.
+Proof.
+  cbv [fe5211_32] in *.
+  repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
+  eexists.
+  cbv - [from_list_default].
+  (* TODO(jgross,jadep): use Reflective linearization here? *)
+  repeat (
+       set_evars; rewrite app_Let_In_nd; subst_evars;
+       eapply Proper_Let_In_nd_changebody; [reflexivity|intro]).
+  cbv [from_list_default from_list_default'].
+  reflexivity.
+Defined.
+
+Definition prefreeze (f : fe5211_32) : fe5211_32 :=
+  Eval cbv beta iota delta [proj1_sig prefreeze_sig] in
+    let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17, f18, f19) := f in
+    proj1_sig (prefreeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17, f18, f19)).
+
+Definition prefreeze_correct (f : fe5211_32)
+  : prefreeze f = from_list_default 0 20 (carry_full_3_opt c_ (to_list 20 f)).
+Proof.
+  pose proof (proj2_sig (prefreeze_sig f)).
+  cbv [fe5211_32] in *.
+  repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
+  assumption.
+Defined.
+
+Definition postfreeze_sig (f : fe5211_32) :
+  { f' : fe5211_32 | f' = from_list_default 0 20 (conditional_subtract_modulus_opt (int_width := int_width) (to_list 20 f)) }.
 Proof.
   cbv [fe5211_32] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
@@ -499,20 +528,40 @@ Proof.
   reflexivity.
 Defined.
 
-Definition freeze (f : fe5211_32) : fe5211_32 :=
-  Eval cbv beta iota delta [proj1_sig freeze_sig] in
+Definition postfreeze (f : fe5211_32) : fe5211_32 :=
+  Eval cbv beta iota delta [proj1_sig postfreeze_sig] in
     let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17, f18, f19) := f in
-    proj1_sig (freeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17, f18, f19)).
+    proj1_sig (postfreeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12, f13, f14, f15, f16, f17, f18, f19)).
 
-Definition freeze_correct (f : fe5211_32)
-  : freeze f = from_list_default 0 20 (freeze_opt (int_width := int_width) c_ (to_list 20 f)).
+Definition postfreeze_correct (f : fe5211_32)
+  : postfreeze f = from_list_default 0 20 (conditional_subtract_modulus_opt (int_width := int_width) (to_list 20 f)).
 Proof.
-  pose proof (proj2_sig (freeze_sig f)).
+  pose proof (proj2_sig (postfreeze_sig f)).
   cbv [fe5211_32] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
   assumption.
 Defined.
 
+Definition freeze (f : fe5211_32) : fe5211_32 :=
+  dlet x := prefreeze f in
+  postfreeze x.
+
+Local Transparent Let_In.
+Definition freeze_correct (f : fe5211_32)
+  : freeze f = from_list_default 0 20 (freeze_opt (int_width := int_width) c_ (to_list 20 f)).
+Proof.
+  cbv [freeze_opt freeze Let_In].
+  rewrite prefreeze_correct.
+  rewrite postfreeze_correct.
+  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.
+  { rewrite carry_full_3_opt_correct; repeat rewrite ModularBaseSystemListProofs.length_carry_full; auto using length_to_list. }
+  rewrite to_list_from_list.
+  reflexivity.
+Qed.
+Local Opaque Let_In.
+
 Definition fieldwiseb_sig (f g : fe5211_32) :
   { b | b = @fieldwiseb Z Z 20 Z.eqb f g }.
 Proof.
diff --git a/src/SpecificGen/GF5211_32Bounded.v b/src/SpecificGen/GF5211_32Bounded.v
index d77609534..6456df450 100644
--- a/src/SpecificGen/GF5211_32Bounded.v
+++ b/src/SpecificGen/GF5211_32Bounded.v
@@ -10,6 +10,7 @@ Require Import Crypto.SpecificGen.GF5211_32BoundedCommon.
 Require Import Crypto.SpecificGen.GF5211_32Reflective.
 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 : fe5211_32W) : word64 := Eval simpl in interp_rge_mod
 Definition packW (f : fe5211_32W) : wire_digitsW := Eval simpl in interp_rpack f.
 Definition unpackW (f : wire_digitsW) : fe5211_32W := 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 GF5211_32.modulus_digits_)).
+  Eval cbv - [ZToWord64] in (Tuple.map ZToWord64 (Tuple.from_list_default 0%Z length_fe5211_32 GF5211_32.modulus_digits_)).
 
 Definition postfreeze : GF5211_32.fe5211_32 -> GF5211_32.fe5211_32 :=
   GF5211_32.postfreeze.
 
-Lemma freeze_prepost_freeze : forall x, postfreeze (prefreeze x) = GF5211_32.freeze x. Proof. reflexivity. Qed.
+Lemma freeze_prepost_freeze : forall x, postfreeze (prefreeze x) = GF5211_32.freeze x.
+Proof. reflexivity. Qed.
 
 Definition postfreezeW : fe5211_32W -> fe5211_32W :=
       (conditional_subtract_modulusW
-         (num_limbs := 10)
+         (num_limbs := length_fe5211_32)
          modulusW
          ge_modulusW
          (Interpretations.Word64.neg GF5211_32.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.
diff --git a/src/SpecificGen/GFtemplate3mod4 b/src/SpecificGen/GFtemplate3mod4
index 0ad1a423a..5c78316a1 100644
--- a/src/SpecificGen/GFtemplate3mod4
+++ b/src/SpecificGen/GFtemplate3mod4
@@ -22,8 +22,8 @@ Local Open Scope Z.
 
 Definition modulus : Z := Eval compute in 2^{{{k}}} - {{{c}}}.
 Lemma prime_modulus : prime modulus. Admitted.
+Definition int_width := Eval compute in (2 * {{{w}}})%Z.
 Definition freeze_input_bound := {{{w}}}%Z.
-Definition int_width := {{{w}}}%Z.
 
 Instance params{{{k}}}{{{c}}}_{{{w}}} : PseudoMersenneBaseParams modulus.
   construct_params prime_modulus {{{n}}}%nat {{{k}}}.
@@ -481,8 +481,37 @@ Proof.
   assumption.
 Defined.
 
-Definition freeze_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) :
-  { f' : fe{{{k}}}{{{c}}}_{{{w}}} | f' = from_list_default 0 {{{n}}} (freeze_opt (int_width := int_width) c_ (to_list {{{n}}} f)) }.
+Definition prefreeze_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) :
+  { f' : fe{{{k}}}{{{c}}}_{{{w}}} | f' = from_list_default 0 {{{n}}} (carry_full_3_opt c_ (to_list {{{n}}} f)) }.
+Proof.
+  cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *.
+  repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
+  eexists.
+  cbv - [from_list_default].
+  (* TODO(jgross,jadep): use Reflective linearization here? *)
+  repeat (
+       set_evars; rewrite app_Let_In_nd; subst_evars;
+       eapply Proper_Let_In_nd_changebody; [reflexivity|intro]).
+  cbv [from_list_default from_list_default'].
+  reflexivity.
+Defined.
+
+Definition prefreeze (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} :=
+  Eval cbv beta iota delta [proj1_sig prefreeze_sig] in
+    let '{{{enum f}}} := f in
+    proj1_sig (prefreeze_sig {{{enum f}}}).
+
+Definition prefreeze_correct (f : fe{{{k}}}{{{c}}}_{{{w}}})
+  : prefreeze f = from_list_default 0 {{{n}}} (carry_full_3_opt c_ (to_list {{{n}}} f)).
+Proof.
+  pose proof (proj2_sig (prefreeze_sig f)).
+  cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *.
+  repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
+  assumption.
+Defined.
+
+Definition postfreeze_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) :
+  { f' : fe{{{k}}}{{{c}}}_{{{w}}} | f' = from_list_default 0 {{{n}}} (conditional_subtract_modulus_opt (int_width := int_width) (to_list {{{n}}} f)) }.
 Proof.
   cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
@@ -499,20 +528,40 @@ Proof.
   reflexivity.
 Defined.
 
-Definition freeze (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} :=
-  Eval cbv beta iota delta [proj1_sig freeze_sig] in
+Definition postfreeze (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} :=
+  Eval cbv beta iota delta [proj1_sig postfreeze_sig] in
     let '{{{enum f}}} := f in
-    proj1_sig (freeze_sig {{{enum f}}}).
+    proj1_sig (postfreeze_sig {{{enum f}}}).
 
-Definition freeze_correct (f : fe{{{k}}}{{{c}}}_{{{w}}})
-  : freeze f = from_list_default 0 {{{n}}} (freeze_opt (int_width := int_width) c_ (to_list {{{n}}} f)).
+Definition postfreeze_correct (f : fe{{{k}}}{{{c}}}_{{{w}}})
+  : postfreeze f = from_list_default 0 {{{n}}} (conditional_subtract_modulus_opt (int_width := int_width) (to_list {{{n}}} f)).
 Proof.
-  pose proof (proj2_sig (freeze_sig f)).
+  pose proof (proj2_sig (postfreeze_sig f)).
   cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
   assumption.
 Defined.
 
+Definition freeze (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} :=
+  dlet x := prefreeze f in
+  postfreeze x.
+
+Local Transparent Let_In.
+Definition freeze_correct (f : fe{{{k}}}{{{c}}}_{{{w}}})
+  : freeze f = from_list_default 0 {{{n}}} (freeze_opt (int_width := int_width) c_ (to_list {{{n}}} f)).
+Proof.
+  cbv [freeze_opt freeze Let_In].
+  rewrite prefreeze_correct.
+  rewrite postfreeze_correct.
+  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.
+  { rewrite carry_full_3_opt_correct; repeat rewrite ModularBaseSystemListProofs.length_carry_full; auto using length_to_list. }
+  rewrite to_list_from_list.
+  reflexivity.
+Qed.
+Local Opaque Let_In.
+
 Definition fieldwiseb_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) :
   { b | b = @fieldwiseb Z Z {{{n}}} Z.eqb f g }.
 Proof.
diff --git a/src/SpecificGen/GFtemplate5mod8 b/src/SpecificGen/GFtemplate5mod8
index 92e25cd18..c5d0d1cfe 100644
--- a/src/SpecificGen/GFtemplate5mod8
+++ b/src/SpecificGen/GFtemplate5mod8
@@ -22,8 +22,8 @@ Local Open Scope Z.
 
 Definition modulus : Z := Eval compute in 2^{{{k}}} - {{{c}}}.
 Lemma prime_modulus : prime modulus. Admitted.
+Definition int_width := Eval compute in (2 * {{{w}}})%Z.
 Definition freeze_input_bound := {{{w}}}%Z.
-Definition int_width := {{{w}}}%Z.
 
 Instance params{{{k}}}{{{c}}}_{{{w}}} : PseudoMersenneBaseParams modulus.
   construct_params prime_modulus {{{n}}}%nat {{{k}}}.
@@ -498,8 +498,37 @@ Proof.
   assumption.
 Defined.
 
-Definition freeze_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) :
-  { f' : fe{{{k}}}{{{c}}}_{{{w}}} | f' = from_list_default 0 {{{n}}} (freeze_opt (int_width := int_width) c_ (to_list {{{n}}} f)) }.
+Definition prefreeze_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) :
+  { f' : fe{{{k}}}{{{c}}}_{{{w}}} | f' = from_list_default 0 {{{n}}} (carry_full_3_opt c_ (to_list {{{n}}} f)) }.
+Proof.
+  cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *.
+  repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
+  eexists.
+  cbv - [from_list_default].
+  (* TODO(jgross,jadep): use Reflective linearization here? *)
+  repeat (
+       set_evars; rewrite app_Let_In_nd; subst_evars;
+       eapply Proper_Let_In_nd_changebody; [reflexivity|intro]).
+  cbv [from_list_default from_list_default'].
+  reflexivity.
+Defined.
+
+Definition prefreeze (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} :=
+  Eval cbv beta iota delta [proj1_sig prefreeze_sig] in
+    let '{{{enum f}}} := f in
+    proj1_sig (prefreeze_sig {{{enum f}}}).
+
+Definition prefreeze_correct (f : fe{{{k}}}{{{c}}}_{{{w}}})
+  : prefreeze f = from_list_default 0 {{{n}}} (carry_full_3_opt c_ (to_list {{{n}}} f)).
+Proof.
+  pose proof (proj2_sig (prefreeze_sig f)).
+  cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *.
+  repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
+  assumption.
+Defined.
+
+Definition postfreeze_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) :
+  { f' : fe{{{k}}}{{{c}}}_{{{w}}} | f' = from_list_default 0 {{{n}}} (conditional_subtract_modulus_opt (int_width := int_width) (to_list {{{n}}} f)) }.
 Proof.
   cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
@@ -516,20 +545,40 @@ Proof.
   reflexivity.
 Defined.
 
-Definition freeze (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} :=
-  Eval cbv beta iota delta [proj1_sig freeze_sig] in
+Definition postfreeze (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} :=
+  Eval cbv beta iota delta [proj1_sig postfreeze_sig] in
     let '{{{enum f}}} := f in
-    proj1_sig (freeze_sig {{{enum f}}}).
+    proj1_sig (postfreeze_sig {{{enum f}}}).
 
-Definition freeze_correct (f : fe{{{k}}}{{{c}}}_{{{w}}})
-  : freeze f = from_list_default 0 {{{n}}} (freeze_opt (int_width := int_width) c_ (to_list {{{n}}} f)).
+Definition postfreeze_correct (f : fe{{{k}}}{{{c}}}_{{{w}}})
+  : postfreeze f = from_list_default 0 {{{n}}} (conditional_subtract_modulus_opt (int_width := int_width) (to_list {{{n}}} f)).
 Proof.
-  pose proof (proj2_sig (freeze_sig f)).
+  pose proof (proj2_sig (postfreeze_sig f)).
   cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
   assumption.
 Defined.
 
+Definition freeze (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} :=
+  dlet x := prefreeze f in
+  postfreeze x.
+
+Local Transparent Let_In.
+Definition freeze_correct (f : fe{{{k}}}{{{c}}}_{{{w}}})
+  : freeze f = from_list_default 0 {{{n}}} (freeze_opt (int_width := int_width) c_ (to_list {{{n}}} f)).
+Proof.
+  cbv [freeze_opt freeze Let_In].
+  rewrite prefreeze_correct.
+  rewrite postfreeze_correct.
+  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.
+  { rewrite carry_full_3_opt_correct; repeat rewrite ModularBaseSystemListProofs.length_carry_full; auto using length_to_list. }
+  rewrite to_list_from_list.
+  reflexivity.
+Qed.
+Local Opaque Let_In.
+
 Definition fieldwiseb_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) :
   { b | b = @fieldwiseb Z Z {{{n}}} Z.eqb f g }.
 Proof.