diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-05 18:52:29 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-05 18:53:53 -0400 |
| commit | b7fcef091fe3f73bc0eb36098bbaab6f1a493c55 (patch) | |
| tree | 0ec85c521d6c28f6387f82c034d466b82063f7d5 /src/Specific/GF25519Reflective/Reified/CarrySub.v | |
| parent | dcc55ed8d1b6afced5ccdfb9e86b6a9c516b4bd6 (diff) | |
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.
Diffstat (limited to 'src/Specific/GF25519Reflective/Reified/CarrySub.v')
| -rw-r--r-- | src/Specific/GF25519Reflective/Reified/CarrySub.v | 1 |
1 files changed, 1 insertions, 0 deletions
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).*) |