12 files changed, 12 insertions, 0 deletions
diff --git a/src/Specific/GF25519Reflective/Reified/Add.v b/src/Specific/GF25519Reflective/Reified/Add.v
index 96fe51ab2..36357fcb7 100644
--- a/src/Specific/GF25519Reflective/Reified/Add.v
+++ b/src/Specific/GF25519Reflective/Reified/Add.v
@@ -8,3 +8,4 @@ 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).*)
diff --git a/src/Specific/GF25519Reflective/Reified/CarryAdd.v b/src/Specific/GF25519Reflective/Reified/CarryAdd.v
index 8df627632..cc93a5bef 100644
--- a/src/Specific/GF25519Reflective/Reified/CarryAdd.v
+++ b/src/Specific/GF25519Reflective/Reified/CarryAdd.v
@@ -8,3 +8,4 @@ Definition rcarry_add_output_bounds := Eval vm_compute in compute_bounds rcarry_
 
 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).*)
diff --git a/src/Specific/GF25519Reflective/Reified/CarryOpp.v b/src/Specific/GF25519Reflective/Reified/CarryOpp.v
index 79e6e29a1..130e55329 100644
--- a/src/Specific/GF25519Reflective/Reified/CarryOpp.v
+++ b/src/Specific/GF25519Reflective/Reified/CarryOpp.v
@@ -8,3 +8,4 @@ Definition rcarry_opp_output_bounds := Eval vm_compute in compute_bounds rcarry_
 
 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).*)
diff --git a/src/Specific/GF25519Reflective/Reified/CarrySub.v b/src/Specific/GF25519Reflective/Reified/CarrySub.v
index e7c2c53ab..b09960a18 100644
--- a/src/Specific/GF25519Reflective/Reified/CarrySub.v
+++ b/src/Specific/GF25519Reflective/Reified/CarrySub.v
@@ -8,3 +8,4 @@ Definition rcarry_sub_output_bounds := Eval vm_compute in compute_bounds rcarry_
 
 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).*)
diff --git a/src/Specific/GF25519Reflective/Reified/Freeze.v b/src/Specific/GF25519Reflective/Reified/Freeze.v
index 72032bb36..4158a5277 100644
--- a/src/Specific/GF25519Reflective/Reified/Freeze.v
+++ b/src/Specific/GF25519Reflective/Reified/Freeze.v
@@ -8,3 +8,4 @@ Definition rfreeze_output_bounds := Eval vm_compute in compute_bounds rfreezeW E
 
 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 75ff2bfdc..776219f96 100644
--- a/src/Specific/GF25519Reflective/Reified/GeModulus.v
+++ b/src/Specific/GF25519Reflective/Reified/GeModulus.v
@@ -8,3 +8,4 @@ Definition rge_modulus_output_bounds := Eval vm_compute in compute_bounds rge_mo
 
 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).*)
diff --git a/src/Specific/GF25519Reflective/Reified/Mul.v b/src/Specific/GF25519Reflective/Reified/Mul.v
index f1b775754..1643a6610 100644
--- a/src/Specific/GF25519Reflective/Reified/Mul.v
+++ b/src/Specific/GF25519Reflective/Reified/Mul.v
@@ -8,3 +8,4 @@ Definition rmul_output_bounds := Eval vm_compute in compute_bounds rmulW ExprBin
 
 Local Open Scope string_scope.
 Compute ("Mul", compute_bounds_for_display rmulW ExprBinOp_bounds).
+(*Compute ("Mul overflows? ", sanity_check rmulW ExprBinOp_bounds).*)
diff --git a/src/Specific/GF25519Reflective/Reified/Opp.v b/src/Specific/GF25519Reflective/Reified/Opp.v
index c561f5bf0..907771b14 100644
--- a/src/Specific/GF25519Reflective/Reified/Opp.v
+++ b/src/Specific/GF25519Reflective/Reified/Opp.v
@@ -8,3 +8,4 @@ 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).*)
diff --git a/src/Specific/GF25519Reflective/Reified/Pack.v b/src/Specific/GF25519Reflective/Reified/Pack.v
index 8e943649d..7f0f46494 100644
--- a/src/Specific/GF25519Reflective/Reified/Pack.v
+++ b/src/Specific/GF25519Reflective/Reified/Pack.v
@@ -8,3 +8,4 @@ Definition rpack_output_bounds := Eval vm_compute in compute_bounds rpackW ExprU
 
 Local Open Scope string_scope.
 Compute ("Pack", compute_bounds_for_display rpackW ExprUnOpFEToWire_bounds).
+(*Compute ("Pack overflows? ", sanity_check rpackW ExprUnOpFEToWire_bounds).*)
diff --git a/src/Specific/GF25519Reflective/Reified/Sub.v b/src/Specific/GF25519Reflective/Reified/Sub.v
index 334d1db7e..9b684248d 100644
--- a/src/Specific/GF25519Reflective/Reified/Sub.v
+++ b/src/Specific/GF25519Reflective/Reified/Sub.v
@@ -8,3 +8,4 @@ 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).*)
diff --git a/src/Specific/GF25519Reflective/Reified/Unpack.v b/src/Specific/GF25519Reflective/Reified/Unpack.v
index 7caa18c54..701115388 100644
--- a/src/Specific/GF25519Reflective/Reified/Unpack.v
+++ b/src/Specific/GF25519Reflective/Reified/Unpack.v
@@ -8,3 +8,4 @@ Definition runpack_output_bounds := Eval vm_compute in compute_bounds runpackW E
 
 Local Open Scope string_scope.
 Compute ("Unpack", compute_bounds_for_display runpackW ExprUnOpWireToFE_bounds).
+(*Compute ("Unpack overflows? ", sanity_check runpackW ExprUnOpWireToFE_bounds).*)
diff --git a/src/Specific/GF25519Reflective/Reified/rebuild-reified.py b/src/Specific/GF25519Reflective/Reified/rebuild-reified.py
index e1c090105..992bc7a7e 100755
--- a/src/Specific/GF25519Reflective/Reified/rebuild-reified.py
+++ b/src/Specific/GF25519Reflective/Reified/rebuild-reified.py
@@ -18,4 +18,5 @@ Definition r%(lname)s_output_bounds := Eval vm_compute in compute_bounds r%(lnam
 
 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).*)
 """ % locals())