Freeze stubs

13 files changed, 41 insertions, 31 deletions

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())