P256: Keep around < eval N bounds

This closes #220

The code before the glue part of the pipeline is getting kind-of ugly...

2 files changed, 36 insertions, 19 deletions

diff --git a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256.v b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256.v
index 313b066da..48c4bc549 100644
--- a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256.v
+++ b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256.v
@@ -30,31 +30,45 @@ Section BoundedField25p5.
   Let feZ : Type := tuple Z sz.
   Let feW : Type := tuple (wordT lgbitwidth) sz.
   Let feBW : Type := BoundedWord sz bitwidth bounds.
+  Let eval : feBW -> Z :=
+    fun x => Saturated.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
+  Let feBW_small : Type := { v : feBW | eval v < Saturated.eval (n:=sz) (Z.pos r) p256 }.
+  Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _.
+  Local Coercion feBW_of_feBW_small : feBW_small >-> feBW.
   Let phi : feBW -> F m :=
-    fun x => montgomery_to_F (Saturated.eval (Z.pos r) (BoundedWordToZ _ _ _ x)).
+    fun x => montgomery_to_F (eval x).
 
   (* TODO : change this to field once field isomorphism happens *)
   Definition mul
-    : { mul : feBW -> feBW -> feBW
+    : { mul : feBW_small -> feBW_small -> feBW_small
       | forall A B, phi (mul A B) = F.mul (phi A) (phi B) }.
   Proof.
     lazymatch goal with
-    | [ |- { f | forall a b, ?phi (f a b) = @?rhs a b } ]
-      => apply lift2_sig with (P:=fun a b f => phi f = rhs a b)
+    | [ |- { f | forall a b, ?phi (?proj (f a b)) = @?rhs a b } ]
+      => apply lift2_sig with (P:=fun a b f => phi (proj f) = rhs a b)
     end.
     intros a b.
-    eexists_sig_etransitivity. all:cbv [phi].
-    rewrite <- (proj2_sig mulmod_256)
-      by (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _); destruct_head' feBW; assumption).
-    (*symmetry; rewrite <- (proj2_sig carry_sig); symmetry.
-    set (carry_mulZ := fun a b => proj1_sig carry_sig (proj1_sig mul_sig a b)).
-    change (proj1_sig carry_sig (proj1_sig mul_sig ?a ?b)) with (carry_mulZ a b).*)
+    cbv [feBW_of_feBW_small].
+    eexists_sig_etransitivity. all:cbv [phi eval].
+    rewrite <- (proj1 (proj2_sig mulmod_256))
+      by (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _); destruct_head' feBW_small; destruct_head' feBW; try assumption).
+    reflexivity.
+    apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)).
+    Associativity.sig_sig_assoc.
+    apply sig_conj_by_impl2.
+    { intros ? H; cbv [eval]; rewrite H; clear H.
+      apply (proj2 (proj2_sig mulmod_256)); destruct_head' feBW_small; try assumption;
+        hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _); destruct_head' feBW; assumption. }
+    eexists_sig_etransitivity.
     set (mulmodZ := proj1_sig mulmod_256).
     context_to_dlet_in_rhs mulmodZ; cbv [mulmodZ].
-    cbv beta iota delta [mulmod_256 mulmod_256'' mulmod_256' proj1_sig Saturated.T lift2_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz].
+    cbv beta iota delta [mulmod_256 mulmod_256'' mulmod_256' proj1_sig Saturated.T lift2_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
     reflexivity.
     sig_dlet_in_rhs_to_context.
-    do 2 apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)).
+    apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)).
+    do 2 match goal with
+         | [ H : feBW_small |- _ ] => destruct H as [? _]
+         end.
     (* jgross start here! *)
     Set Ltac Profiling.
     Time refine_reflectively_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *)
diff --git a/src/Specific/NISTP256/AMD64/MontgomeryP256.v b/src/Specific/NISTP256/AMD64/MontgomeryP256.v
index dfc57cfdc..1298c8841 100644
--- a/src/Specific/NISTP256/AMD64/MontgomeryP256.v
+++ b/src/Specific/NISTP256/AMD64/MontgomeryP256.v
@@ -133,18 +133,21 @@ Definition montgomery_to_F (v : Z) : F m
   := (F.of_Z m v * F.of_Z m (r'^Z.of_nat sz)%Z)%F.
 
 Definition mulmod_256 : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-                        | forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
-                                 (B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
-                            let eval := Saturated.eval (Z.pos r) in
-                            montgomery_to_F (eval (f A B))
-                            = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F }.
+                        | let eval := Saturated.eval (Z.pos r) in
+                          (forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
+                                  (B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
+                              montgomery_to_F (eval (f A B))
+                              = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F)
+                          /\ (forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
+                                     (B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
+                                 (eval B < eval p256 -> 0 <= eval (f A B) < eval p256)%Z) }.
 Proof.
   exists (proj1_sig mulmod_256'').
   abstract (
-      intros A Asm B Bsm;
+      split; intros A Asm B Bsm;
       pose proof (proj2_sig mulmod_256'' A B Asm Bsm) as H;
       cbv zeta in *;
-      (*split; try solve [ destruct_head'_and; assumption ];*)
+      try solve [ destruct_head'_and; assumption ];
       rewrite ModularArithmeticTheorems.F.eq_of_Z_iff in H;
       unfold montgomery_to_F;
       destruct H as [H1 [H2 H3]];