aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic
diff options
context:
space:
mode:
Diffstat (limited to 'src/ModularArithmetic')
-rw-r--r--src/ModularArithmetic/ModularBaseSystemListZOperations.v5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemListZOperations.v b/src/ModularArithmetic/ModularBaseSystemListZOperations.v
index 1d863abbd..09a252a06 100644
--- a/src/ModularArithmetic/ModularBaseSystemListZOperations.v
+++ b/src/ModularArithmetic/ModularBaseSystemListZOperations.v
@@ -2,6 +2,7 @@
(** We separate these out so that we can depend on them in other files
without waiting for ModularBaseSystemList to build. *)
Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.Tuple.
Definition cmovl (x y r1 r2 : Z) := if Z.leb x y then r1 else r2.
Definition cmovne (x y r1 r2 : Z) := if Z.eqb x y then r1 else r2.
@@ -10,3 +11,7 @@ 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.