diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-10 21:24:54 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2016-11-11 16:07:28 -0500 |
| commit | b2e85f8b7983a72390e35c5509127dfabc68fbef (patch) | |
| tree | 23260080c260eac8ad9d09940069695aaad9b264 /src/ModularArithmetic | |
| parent | 8e9b64460ac03810255529b16be49a8a4912d0d5 (diff) | |
Remove special code for reified conditional sub
Diffstat (limited to 'src/ModularArithmetic')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemListZOperations.v | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemListZOperations.v b/src/ModularArithmetic/ModularBaseSystemListZOperations.v index 09a252a06..0c8f3caa0 100644 --- a/src/ModularArithmetic/ModularBaseSystemListZOperations.v +++ b/src/ModularArithmetic/ModularBaseSystemListZOperations.v @@ -11,7 +11,3 @@ Definition cmovne (x y r1 r2 : Z) := if Z.eqb x y then r1 else r2. neg 1 = 2^64 - 1 (on 64-bit; 2^32-1 on 32-bit, etc.) neg 0 = 0 *) Definition neg (int_width : Z) (b : Z) := if Z.eqb b 1 then Z.ones int_width else 0%Z. - -(** TODO(jadep): Fill in this stub *) -Axiom conditional_subtract_modulus - : forall (limb_count : nat) (int_width : Z) (modulus value : Tuple.tuple Z limb_count), Tuple.tuple Z limb_count. |