Preliminary support: conditional sub as primitive

Things to be done:
- Fill in Axiom conditional_subtract_modulus in
  src/ModularArithmetic/ModularBaseSystemListZOperations.v (jadep)
- Refactor code to make GF25519.freeze use
  ModularBaseSystemListZOperations.conditional_subtract_modulus in a
  non-unfolded form (jadep)
- Check that the bounds I defined in conditional_subtract' in
  src/Reflection/Z/Interpretations.v are correct (jadep)
- Fill in bounds checking in conditional_subtract_o in
  src/Reflection/Z/Interpretations.v (jgross or jadep)
- Integrate boundedness lemma about conditional_subtract_modulus into
  BoundedWord64.conditional_subtract in src/Reflection/Z/Interpretations.v
  (jadep and jgross?)
- Prove BoundedWord64.invert_conditional_subtract (depends on some bits
  of the above bullet point, but could be done by jgross)
- Fill in the three admits in
  src/Reflection/Z/Interpretations/Relations.v (jadep or jgross?)
- Verify that everything works

(cc @jadephilipoom @andres-erbsen)

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.