From 4bc6702e87ec22603353bad92471b1af31bf919b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 6 Nov 2016 13:46:59 -0500 Subject: 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) --- src/ModularArithmetic/ModularBaseSystemListZOperations.v | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'src/ModularArithmetic') 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. -- cgit v1.2.3