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)

0 files changed, 0 insertions, 0 deletions