Freeze stubs

19 files changed, 130 insertions, 54 deletions

diff --git a/_CoqProject b/_CoqProject
index cf46abd60..140b4716a 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -157,11 +157,11 @@ src/Specific/GF25519Reflective/Reified/Add.v
 src/Specific/GF25519Reflective/Reified/CarryAdd.v
 src/Specific/GF25519Reflective/Reified/CarryOpp.v
 src/Specific/GF25519Reflective/Reified/CarrySub.v
-src/Specific/GF25519Reflective/Reified/Freeze.v
 src/Specific/GF25519Reflective/Reified/GeModulus.v
 src/Specific/GF25519Reflective/Reified/Mul.v
 src/Specific/GF25519Reflective/Reified/Opp.v
 src/Specific/GF25519Reflective/Reified/Pack.v
+src/Specific/GF25519Reflective/Reified/PreFreeze.v
 src/Specific/GF25519Reflective/Reified/Sub.v
 src/Specific/GF25519Reflective/Reified/Unpack.v
 src/Tactics/VerdiTactics.v
diff --git a/src/Specific/GF25519Bounded.v b/src/Specific/GF25519Bounded.v
index 2d83b8dbd..f09b843f0 100644
--- a/src/Specific/GF25519Bounded.v
+++ b/src/Specific/GF25519Bounded.v
@@ -50,7 +50,7 @@ Local Arguments interp_radd / _ _.
 Local Arguments interp_rsub / _ _.
 Local Arguments interp_rmul / _ _.
 Local Arguments interp_ropp / _.
-Local Arguments interp_rfreeze / _.
+Local Arguments interp_rprefreeze / _.
 Local Arguments interp_rge_modulus / _.
 Local Arguments interp_rpack / _.
 Local Arguments interp_runpack / _.
@@ -58,10 +58,11 @@ Definition addW (f g : fe25519W) : fe25519W := Eval simpl in interp_radd f g.
 Definition subW (f g : fe25519W) : fe25519W := Eval simpl in interp_rsub f g.
 Definition mulW (f g : fe25519W) : fe25519W := Eval simpl in interp_rmul f g.
 Definition oppW (f : fe25519W) : fe25519W := Eval simpl in interp_ropp f.
-Definition freezeW (f : fe25519W) : fe25519W := Eval simpl in interp_rfreeze f.
+Definition prefreezeW (f : fe25519W) : fe25519W := Eval simpl in interp_rprefreeze f.
 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.
+Definition freezeW (f : fe25519W) : fe25519W := Eval cbv beta delta [prefreezeW postfreezeW] in postfreezeW (prefreezeW f).
 
 Local Transparent Let_In.
 Definition powW (f : fe25519W) chain := fold_chain_opt (proj1_fe25519W one) mulW chain [f].
@@ -81,14 +82,22 @@ Lemma mulW_correct_and_bounded : ibinop_correct_and_bounded mulW mul.
 Proof. port_correct_and_bounded interp_rmul_correct mulW interp_rmul rmul_correct_and_bounded. Qed.
 Lemma oppW_correct_and_bounded : iunop_correct_and_bounded oppW carry_opp.
 Proof. port_correct_and_bounded interp_ropp_correct oppW interp_ropp ropp_correct_and_bounded. Qed.
-Lemma freezeW_correct_and_bounded : iunop_correct_and_bounded freezeW freeze.
-Proof. port_correct_and_bounded interp_rfreeze_correct freezeW interp_rfreeze rfreeze_correct_and_bounded. Qed.
+Lemma prefreezeW_correct_and_bounded : iunop_correct_and_bounded prefreezeW prefreeze.
+Proof. port_correct_and_bounded interp_rprefreeze_correct prefreezeW interp_rprefreeze rprefreeze_correct_and_bounded. Qed.
 Lemma ge_modulusW_correct : iunop_FEToZ_correct ge_modulusW ge_modulus.
 Proof. port_correct_and_bounded interp_rge_modulus_correct ge_modulusW interp_rge_modulus rge_modulus_correct_and_bounded. Qed.
 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.
+Lemma freezeW_correct_and_bounded : iunop_correct_and_bounded freezeW freeze.
+Proof.
+  intros f H; rewrite <- freeze_prepost_freeze.
+  change (freezeW f) with (postfreezeW (prefreezeW f)).
+  destruct (prefreezeW_correct_and_bounded f H) as [H0 H1].
+  destruct (postfreezeW_correct_and_bounded _ H1) as [H0' H1'].
+  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.
diff --git a/src/Specific/GF25519BoundedCommon.v b/src/Specific/GF25519BoundedCommon.v
index f9ee444dc..4f0c9b4de 100644
--- a/src/Specific/GF25519BoundedCommon.v
+++ b/src/Specific/GF25519BoundedCommon.v
@@ -689,3 +689,51 @@ Notation iunop_WireToFE_correct_and_bounded irop op
          wire_digits_is_bounded (wire_digitsWToZ x) = true
          -> 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 '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) =>
+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.
diff --git a/src/Specific/GF25519Reflective.v b/src/Specific/GF25519Reflective.v
index 4405eefa9..5e306d61d 100644
--- a/src/Specific/GF25519Reflective.v
+++ b/src/Specific/GF25519Reflective.v
@@ -36,7 +36,7 @@ Definition radd : ExprBinOp := Eval vm_compute in rcarry_addW.
 Definition rsub : ExprBinOp := Eval vm_compute in rcarry_subW.
 Definition rmul : ExprBinOp := Eval vm_compute in rmulW.
 Definition ropp : ExprUnOp := Eval vm_compute in rcarry_oppW.
-Definition rfreeze : ExprUnOp := Eval vm_compute in rfreezeW.
+Definition rprefreeze : ExprUnOp := Eval vm_compute in rprefreezeW.
 Definition rge_modulus : ExprUnOpFEToZ := Eval vm_compute in rge_modulusW.
 Definition rpack : ExprUnOpFEToWire := Eval vm_compute in rpackW.
 Definition runpack : ExprUnOpWireToFE := Eval vm_compute in runpackW.
@@ -48,7 +48,7 @@ Declare Reduction asm_interp
   := cbv beta iota delta
          [id
             interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE
-            radd rsub rmul ropp rfreeze rge_modulus rpack runpack
+            radd rsub rmul ropp rprefreeze rge_modulus rpack runpack
             curry_binop_fe25519W curry_unop_fe25519W curry_unop_wire_digitsW
             Word64.interp_op Word64.interp_base_type
             Z.interp_op Z.interp_base_type
@@ -59,7 +59,7 @@ Ltac asm_interp
   := cbv beta iota delta
          [id
             interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE
-            radd rsub rmul ropp rfreeze rge_modulus rpack runpack
+            radd rsub rmul ropp rprefreeze rge_modulus rpack runpack
             curry_binop_fe25519W curry_unop_fe25519W curry_unop_wire_digitsW
             Word64.interp_op Word64.interp_base_type
             Z.interp_op Z.interp_base_type
@@ -84,10 +84,10 @@ Definition interp_ropp : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25
   := Eval asm_interp in interp_uexpr (rword64ize ropp).
 (*Print interp_ropp.*)
 Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl.
-Definition interp_rfreeze : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
-  := Eval asm_interp in interp_uexpr (rword64ize rfreeze).
-(*Print interp_rfreeze.*)
-Definition interp_rfreeze_correct : interp_rfreeze = interp_uexpr rfreeze := eq_refl.
+Definition interp_rprefreeze : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
+  := Eval asm_interp in interp_uexpr (rword64ize rprefreeze).
+(*Print interp_rprefreeze.*)
+Definition interp_rprefreeze_correct : interp_rprefreeze = interp_uexpr rprefreeze := eq_refl.
 
 Definition interp_rge_modulus : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.word64
   := Eval asm_interp in interp_uexpr_FEToZ (rword64ize rge_modulus).
@@ -109,8 +109,8 @@ Lemma rmul_correct_and_bounded : binop_correct_and_bounded rmul mul.
 Proof. exact rmulW_correct_and_bounded. Qed.
 Lemma ropp_correct_and_bounded : unop_correct_and_bounded ropp carry_opp.
 Proof. exact rcarry_oppW_correct_and_bounded. Qed.
-Lemma rfreeze_correct_and_bounded : unop_correct_and_bounded rfreeze freeze.
-Proof. exact rfreezeW_correct_and_bounded. Qed.
+Lemma rprefreeze_correct_and_bounded : unop_correct_and_bounded rprefreeze prefreeze.
+Proof. exact rprefreezeW_correct_and_bounded. Qed.
 Lemma rge_modulus_correct_and_bounded : unop_FEToZ_correct rge_modulus ge_modulus.
 Proof. exact rge_modulusW_correct_and_bounded. Qed.
 Lemma rpack_correct_and_bounded : unop_FEToWire_correct_and_bounded rpack pack.
diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v
index 3d448f97c..c302926d6 100644
--- a/src/Specific/GF25519Reflective/Common.v
+++ b/src/Specific/GF25519Reflective/Common.v
@@ -1,7 +1,7 @@
 Require Export Coq.ZArith.ZArith.
 Require Export Coq.Strings.String.
 Require Export Crypto.Specific.GF25519.
-Require Import Crypto.Specific.GF25519BoundedCommon.
+Require Export Crypto.Specific.GF25519BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Z.Interpretations.
@@ -395,7 +395,11 @@ Notation compute_bounds opW bounds
 
 
 Module Export PrettyPrinting.
-  Inductive bounds_on := overflow | in_range (lower upper : Z).
+  Section bounds_not_set.
+    Let T := let T := Type in let enforce := Set : T in T.
+    Inductive bounds_on : T := overflow | in_range (lower upper : Z).
+  End bounds_not_set.
+  Inductive result := yes | no.
 
   Definition ZBounds_to_bounds_on
     := fun t : base_type
@@ -408,18 +412,23 @@ Module Export PrettyPrinting.
                            end
           end.
 
-  Fixpoint no_overflow {t} : interp_flat_type (fun t => match t with TZ => bounds_on end) t -> bool
-    := match t return interp_flat_type (fun t => match t with TZ => bounds_on end) t -> bool with
+  Fixpoint does_it_overflow {t} : interp_flat_type (fun t => match t with TZ => bounds_on end) t -> result
+    := match t return interp_flat_type (fun t => match t with TZ => bounds_on end) t -> result with
        | Tbase TZ => fun v => match v with
-                              | overflow => false
-                              | in_range _ _ => true
+                              | overflow => yes
+                              | in_range _ _ => no
+                              end
+       | Prod x y => fun v => match @does_it_overflow _ (fst v), @does_it_overflow _ (snd v) with
+                              | no, no => no
+                              | _, _ => yes
                               end
-       | Prod x y => fun v => andb (@no_overflow _ (fst v)) (@no_overflow _ (snd v))
        end.
 
   (** This gives a slightly easier to read version of the bounds *)
   Notation compute_bounds_for_display opW bounds
     := (SmartVarfMap ZBounds_to_bounds_on (compute_bounds opW bounds)) (only parsing).
+  Notation sanity_compute opW bounds
+    := (does_it_overflow (SmartVarfMap ZBounds_to_bounds_on (compute_bounds opW bounds))) (only parsing).
   Notation sanity_check opW bounds
-    := (eq_refl true <: no_overflow (SmartVarfMap ZBounds_to_bounds_on (compute_bounds opW bounds)) = true) (only parsing).
+    := (eq_refl (sanity_compute opW bounds) <: no = no) (only parsing).
 End PrettyPrinting.
diff --git a/src/Specific/GF25519Reflective/Reified.v b/src/Specific/GF25519Reflective/Reified.v
index 98edc1282..aa50ad33f 100644
--- a/src/Specific/GF25519Reflective/Reified.v
+++ b/src/Specific/GF25519Reflective/Reified.v
@@ -7,7 +7,7 @@ Require Export Crypto.Specific.GF25519Reflective.Reified.CarrySub.
 Require Export Crypto.Specific.GF25519Reflective.Reified.Mul.
 Require Export Crypto.Specific.GF25519Reflective.Reified.Opp.
 Require Export Crypto.Specific.GF25519Reflective.Reified.CarryOpp.
-Require Export Crypto.Specific.GF25519Reflective.Reified.Freeze.
+Require Export Crypto.Specific.GF25519Reflective.Reified.PreFreeze.
 Require Export Crypto.Specific.GF25519Reflective.Reified.GeModulus.
 Require Export Crypto.Specific.GF25519Reflective.Reified.Pack.
 Require Export Crypto.Specific.GF25519Reflective.Reified.Unpack.
diff --git a/src/Specific/GF25519Reflective/Reified/Add.v b/src/Specific/GF25519Reflective/Reified/Add.v
index ae3a6a4c6..f2700aca7 100644
--- a/src/Specific/GF25519Reflective/Reified/Add.v
+++ b/src/Specific/GF25519Reflective/Reified/Add.v
@@ -8,4 +8,5 @@ Definition radd_output_bounds := Eval vm_compute in compute_bounds raddW ExprBin
 
 Local Open Scope string_scope.
 Compute ("Add", compute_bounds_for_display raddW ExprBinOp_bounds).
-(*Compute ("Add overflows? ", sanity_check raddW ExprBinOp_bounds).*)
+Compute ("Add overflows? ", sanity_compute raddW ExprBinOp_bounds).
+Compute ("Add overflows (error if it does)? ", sanity_check raddW ExprBinOp_bounds).
diff --git a/src/Specific/GF25519Reflective/Reified/CarryAdd.v b/src/Specific/GF25519Reflective/Reified/CarryAdd.v
index 3051121c0..6e05303e5 100644
--- a/src/Specific/GF25519Reflective/Reified/CarryAdd.v
+++ b/src/Specific/GF25519Reflective/Reified/CarryAdd.v
@@ -13,4 +13,5 @@ Program Definition rcarry_addW_correct_and_bounded
 
 Local Open Scope string_scope.
 Compute ("Carry_Add", compute_bounds_for_display rcarry_addW ExprBinOp_bounds).
-(*Compute ("Carry_Add overflows? ", sanity_check rcarry_addW ExprBinOp_bounds).*)
+Compute ("Carry_Add overflows? ", sanity_compute rcarry_addW ExprBinOp_bounds).
+Compute ("Carry_Add overflows (error if it does)? ", sanity_check rcarry_addW ExprBinOp_bounds).
diff --git a/src/Specific/GF25519Reflective/Reified/CarryOpp.v b/src/Specific/GF25519Reflective/Reified/CarryOpp.v
index 571b9db97..52814dca9 100644
--- a/src/Specific/GF25519Reflective/Reified/CarryOpp.v
+++ b/src/Specific/GF25519Reflective/Reified/CarryOpp.v
@@ -13,4 +13,5 @@ Program Definition rcarry_oppW_correct_and_bounded
 
 Local Open Scope string_scope.
 Compute ("Carry_Opp", compute_bounds_for_display rcarry_oppW ExprUnOp_bounds).
-(*Compute ("Carry_Opp overflows? ", sanity_check rcarry_oppW ExprUnOp_bounds).*)
+Compute ("Carry_Opp overflows? ", sanity_compute rcarry_oppW ExprUnOp_bounds).
+Compute ("Carry_Opp overflows (error if it does)? ", sanity_check rcarry_oppW ExprUnOp_bounds).
diff --git a/src/Specific/GF25519Reflective/Reified/CarrySub.v b/src/Specific/GF25519Reflective/Reified/CarrySub.v
index fda466861..946a4ed67 100644
--- a/src/Specific/GF25519Reflective/Reified/CarrySub.v
+++ b/src/Specific/GF25519Reflective/Reified/CarrySub.v
@@ -13,4 +13,5 @@ Program Definition rcarry_subW_correct_and_bounded
 
 Local Open Scope string_scope.
 Compute ("Carry_Sub", compute_bounds_for_display rcarry_subW ExprBinOp_bounds).
-(*Compute ("Carry_Sub overflows? ", sanity_check rcarry_subW ExprBinOp_bounds).*)
+Compute ("Carry_Sub overflows? ", sanity_compute rcarry_subW ExprBinOp_bounds).
+Compute ("Carry_Sub overflows (error if it does)? ", sanity_check rcarry_subW ExprBinOp_bounds).
diff --git a/src/Specific/GF25519Reflective/Reified/Freeze.v b/src/Specific/GF25519Reflective/Reified/Freeze.v
deleted file mode 100644
index 0dcea29e4..000000000
--- a/src/Specific/GF25519Reflective/Reified/Freeze.v
+++ /dev/null
@@ -1,18 +0,0 @@
-Require Import Crypto.Specific.GF25519Reflective.CommonUnOp.
-
-Definition rfreezeZ_sig : rexpr_unop_sig freeze. Proof. reify_sig. Defined.
-Definition rfreezeW := Eval vm_compute in rword_of_Z rfreezeZ_sig.
-Lemma rfreezeW_correct_and_bounded_gen : correct_and_bounded_genT rfreezeW rfreezeZ_sig.
-Proof. rexpr_correct. Qed.
-Definition rfreeze_output_bounds := Eval vm_compute in compute_bounds rfreezeW ExprUnOp_bounds.
-Local Obligation Tactic := intros; vm_compute; constructor.
-Axiom proof_admitted : False.
-(** XXX TODO: Fix bounds analysis on freeze *)
-Definition rfreezeW_correct_and_bounded
-  := ExprUnOp_correct_and_bounded
-       rfreezeW freeze rfreezeZ_sig rfreezeW_correct_and_bounded_gen
-       match proof_admitted with end match proof_admitted with end.
-
-Local Open Scope string_scope.
-Compute ("Freeze", compute_bounds_for_display rfreezeW ExprUnOp_bounds).
-(*Compute ("Freeze overflows? ", sanity_check rfreezeW ExprUnOp_bounds).*)
diff --git a/src/Specific/GF25519Reflective/Reified/GeModulus.v b/src/Specific/GF25519Reflective/Reified/GeModulus.v
index 69eb3ba41..8bbcf0dc4 100644
--- a/src/Specific/GF25519Reflective/Reified/GeModulus.v
+++ b/src/Specific/GF25519Reflective/Reified/GeModulus.v
@@ -13,4 +13,5 @@ Program Definition rge_modulusW_correct_and_bounded
 
 Local Open Scope string_scope.
 Compute ("Ge_Modulus", compute_bounds_for_display rge_modulusW ExprUnOpFEToZ_bounds).
-(*Compute ("Ge_Modulus overflows? ", sanity_check rge_modulusW ExprUnOpFEToZ_bounds).*)
+Compute ("Ge_Modulus overflows? ", sanity_compute rge_modulusW ExprUnOpFEToZ_bounds).
+Compute ("Ge_Modulus overflows (error if it does)? ", sanity_check rge_modulusW ExprUnOpFEToZ_bounds).
diff --git a/src/Specific/GF25519Reflective/Reified/Mul.v b/src/Specific/GF25519Reflective/Reified/Mul.v
index 0c298134d..0388c626a 100644
--- a/src/Specific/GF25519Reflective/Reified/Mul.v
+++ b/src/Specific/GF25519Reflective/Reified/Mul.v
@@ -13,4 +13,5 @@ Program Definition rmulW_correct_and_bounded
 
 Local Open Scope string_scope.
 Compute ("Mul", compute_bounds_for_display rmulW ExprBinOp_bounds).
-(*Compute ("Mul overflows? ", sanity_check rmulW ExprBinOp_bounds).*)
+Compute ("Mul overflows? ", sanity_compute rmulW ExprBinOp_bounds).
+Compute ("Mul overflows (error if it does)? ", sanity_check rmulW ExprBinOp_bounds).
diff --git a/src/Specific/GF25519Reflective/Reified/Opp.v b/src/Specific/GF25519Reflective/Reified/Opp.v
index 58f2a6fbb..36a0b907e 100644
--- a/src/Specific/GF25519Reflective/Reified/Opp.v
+++ b/src/Specific/GF25519Reflective/Reified/Opp.v
@@ -8,4 +8,5 @@ Definition ropp_output_bounds := Eval vm_compute in compute_bounds roppW ExprUnO
 
 Local Open Scope string_scope.
 Compute ("Opp", compute_bounds_for_display roppW ExprUnOp_bounds).
-(*Compute ("Opp overflows? ", sanity_check roppW ExprUnOp_bounds).*)
+Compute ("Opp overflows? ", sanity_compute roppW ExprUnOp_bounds).
+Compute ("Opp overflows (error if it does)? ", sanity_check roppW ExprUnOp_bounds).
diff --git a/src/Specific/GF25519Reflective/Reified/Pack.v b/src/Specific/GF25519Reflective/Reified/Pack.v
index cd85d0cd7..9645cf24c 100644
--- a/src/Specific/GF25519Reflective/Reified/Pack.v
+++ b/src/Specific/GF25519Reflective/Reified/Pack.v
@@ -13,4 +13,5 @@ Program Definition rpackW_correct_and_bounded
 
 Local Open Scope string_scope.
 Compute ("Pack", compute_bounds_for_display rpackW ExprUnOpFEToWire_bounds).
-(*Compute ("Pack overflows? ", sanity_check rpackW ExprUnOpFEToWire_bounds).*)
+Compute ("Pack overflows? ", sanity_compute rpackW ExprUnOpFEToWire_bounds).
+Compute ("Pack overflows (error if it does)? ", sanity_check rpackW ExprUnOpFEToWire_bounds).
diff --git a/src/Specific/GF25519Reflective/Reified/PreFreeze.v b/src/Specific/GF25519Reflective/Reified/PreFreeze.v
new file mode 100644
index 000000000..6b3bce924
--- /dev/null
+++ b/src/Specific/GF25519Reflective/Reified/PreFreeze.v
@@ -0,0 +1,17 @@
+Require Import Crypto.Specific.GF25519Reflective.CommonUnOp.
+
+Definition rprefreezeZ_sig : rexpr_unop_sig prefreeze. Proof. 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.
+Definition rprefreeze_output_bounds := Eval vm_compute in compute_bounds rprefreezeW ExprUnOp_bounds.
+Local Obligation Tactic := intros; vm_compute; constructor.
+Program Definition rprefreezeW_correct_and_bounded
+  := ExprUnOp_correct_and_bounded
+       rprefreezeW prefreeze rprefreezeZ_sig rprefreezeW_correct_and_bounded_gen
+       _ _.
+
+Local Open Scope string_scope.
+Compute ("PreFreeze", compute_bounds_for_display rprefreezeW ExprUnOp_bounds).
+Compute ("PreFreeze overflows? ", sanity_compute rprefreezeW ExprUnOp_bounds).
+Compute ("PreFreeze overflows (error if it does)? ", sanity_check rprefreezeW ExprUnOp_bounds).
diff --git a/src/Specific/GF25519Reflective/Reified/Sub.v b/src/Specific/GF25519Reflective/Reified/Sub.v
index 03356cd50..aae3af64b 100644
--- a/src/Specific/GF25519Reflective/Reified/Sub.v
+++ b/src/Specific/GF25519Reflective/Reified/Sub.v
@@ -8,4 +8,5 @@ Definition rsub_output_bounds := Eval vm_compute in compute_bounds rsubW ExprBin
 
 Local Open Scope string_scope.
 Compute ("Sub", compute_bounds_for_display rsubW ExprBinOp_bounds).
-(*Compute ("Sub overflows? ", sanity_check rsubW ExprBinOp_bounds).*)
+Compute ("Sub overflows? ", sanity_compute rsubW ExprBinOp_bounds).
+Compute ("Sub overflows (error if it does)? ", sanity_check rsubW ExprBinOp_bounds).
diff --git a/src/Specific/GF25519Reflective/Reified/Unpack.v b/src/Specific/GF25519Reflective/Reified/Unpack.v
index a96f87d96..f8ab40383 100644
--- a/src/Specific/GF25519Reflective/Reified/Unpack.v
+++ b/src/Specific/GF25519Reflective/Reified/Unpack.v
@@ -13,4 +13,5 @@ Program Definition runpackW_correct_and_bounded
 
 Local Open Scope string_scope.
 Compute ("Unpack", compute_bounds_for_display runpackW ExprUnOpWireToFE_bounds).
-(*Compute ("Unpack overflows? ", sanity_check runpackW ExprUnOpWireToFE_bounds).*)
+Compute ("Unpack overflows? ", sanity_compute runpackW ExprUnOpWireToFE_bounds).
+Compute ("Unpack overflows (error if it does)? ", sanity_check runpackW ExprUnOpWireToFE_bounds).
diff --git a/src/Specific/GF25519Reflective/Reified/rebuild-reified.py b/src/Specific/GF25519Reflective/Reified/rebuild-reified.py
index 404afc1ea..8b0da4c35 100755
--- a/src/Specific/GF25519Reflective/Reified/rebuild-reified.py
+++ b/src/Specific/GF25519Reflective/Reified/rebuild-reified.py
@@ -2,13 +2,13 @@
 from __future__ import with_statement
 
 for name, opkind in ([(name, 'BinOp') for name in ('Add', 'Carry_Add', 'Sub', 'Carry_Sub', 'Mul')]
-                     + [(name, 'UnOp') for name in ('Opp', 'Carry_Opp', 'Freeze')]
+                     + [(name, 'UnOp') for name in ('Opp', 'Carry_Opp', 'PreFreeze')]
                      + [('Ge_Modulus', 'UnOp_FEToZ'), ('Pack', 'UnOp_FEToWire'), ('Unpack', 'UnOp_WireToFE')]):
     lname = name.lower()
     lopkind = opkind.replace('UnOp', 'unop').replace('BinOp', 'binop')
     uopkind = opkind.replace('_', '')
     extra = ''
-    if name in ('Carry_Add', 'Carry_Sub', 'Mul', 'Carry_Opp', 'Pack', 'Unpack', 'Ge_Modulus'):
+    if name in ('Carry_Add', 'Carry_Sub', 'Mul', 'Carry_Opp', 'Pack', 'Unpack', 'Ge_Modulus', 'PreFreeze'):
         extra = r"""Local Obligation Tactic := intros; vm_compute; constructor.
 Program Definition r%(lname)sW_correct_and_bounded
   := Expr%(uopkind)s_correct_and_bounded
@@ -35,5 +35,6 @@ Definition r%(lname)s_output_bounds := Eval vm_compute in compute_bounds r%(lnam
 %(extra)s
 Local Open Scope string_scope.
 Compute ("%(name)s", compute_bounds_for_display r%(lname)sW Expr%(uopkind)s_bounds).
-(*Compute ("%(name)s overflows? ", sanity_check r%(lname)sW Expr%(uopkind)s_bounds).*)
+Compute ("%(name)s overflows? ", sanity_compute r%(lname)sW Expr%(uopkind)s_bounds).
+Compute ("%(name)s overflows (error if it does)? ", sanity_check r%(lname)sW Expr%(uopkind)s_bounds).
 """ % locals())