Add code for overflow check (disabled bc freeze)

Currently freeze overflows; Jade says this is because the carry chain
got reversed, and that she'll work on fixing this.  We should enable the
sanity checks at some point after this is fixed, to fail early if things
overflow.

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