Changes to sqrt for easier bounds proofs; currently blocked on broken proof in GF25519Bounded

3 files changed, 42 insertions, 52 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v
index d8303d1a7..6df49173e 100644
--- a/src/ModularArithmetic/ModularBaseSystem.v
+++ b/src/ModularArithmetic/ModularBaseSystem.v
@@ -95,13 +95,10 @@ Section ModularBaseSystem.
                   (chain_correct : fold_chain 0%N N.add chain (1%N :: nil) = Z.to_N (modulus / 4 + 1))
                   (x : digits) : digits := pow x chain.
 
-  (* sqrt_5mod8 is parameterized over implementation of [mul] and [pow] because it relies on bounds-checking
-     for these two functions, which is much easier for simplified implementations than the more generalized
-     ones defined here. *)
-  Definition sqrt_5mod8 B mul_ pow_ (chain : list (nat * nat))
+  Definition sqrt_5mod8 B powx powx_squared (chain : list (nat * nat))
                   (chain_correct : fold_chain 0%N N.add chain (1%N :: nil) = Z.to_N (modulus / 8 + 1))
                   (sqrt_minus1 x : digits) : digits :=
-    let b := pow_ x chain in if eqb B (mul_ b b) x then b else mul_ sqrt_minus1 b.
+    if eqb B powx_squared x then powx else mul sqrt_minus1 powx.
 
   Import Morphisms.
   Global Instance eq_Equivalence : Equivalence eq.
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index f7f6efad7..d302f83a8 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -1069,32 +1069,41 @@ Section SquareRoots.
 
   End SquareRoot3mod4.
 
-  Import Morphisms.
-  Global Instance eqb_Proper : Proper (Logic.eq ==> eq ==> eq ==> Logic.eq) ModularBaseSystem.eqb. Admitted.
-
   Section SquareRoot5mod8.
   Context {ec : ExponentiationChain (modulus / 8 + 1)}.
   Context (sqrt_m1 : digits) (sqrt_m1_correct : rep (mul sqrt_m1 sqrt_m1) (F.opp 1%F)).
   Context {int_width} (preconditions : freezePreconditions prm int_width).
 
-  Definition sqrt_5mod8_opt_sig (us : digits) :
+  Definition sqrt_5mod8_opt_sig (powx powx_squared us : digits) :
     { vs : digits |
-      eq vs (sqrt_5mod8 int_width (carry_mul_opt k_ c_) (pow_opt k_ c_ one_) chain chain_correct sqrt_m1 us)}.
+      eq vs (sqrt_5mod8 int_width powx powx_squared chain chain_correct sqrt_m1 us)}.
   Proof.
-    eexists; cbv [sqrt_5mod8].
-    let LHS := match goal with |- eq ?LHS ?RHS => LHS end in
-    let RHS := match goal with |- eq ?LHS ?RHS => RHS end in
-    let RHSf := match (eval pattern (pow_opt k_ c_ one_ us chain) in RHS) with ?RHSf _ => RHSf end in
-    change (eq LHS (Let_In (pow_opt k_ c_ one_ us chain) RHSf)).
-    reflexivity.
+    cbv [sqrt_5mod8].
+    match goal with
+      |- appcontext[(if ?P then ?t else mul ?a ?b)] =>
+      assert (eq (carry_mul_opt k_ c_ a b) (mul a b))
+        by (rewrite carry_mul_opt_correct by auto;
+           cbv [eq]; rewrite carry_mul_rep, mul_rep; reflexivity)
+    end.
+    let RHS := match goal with |- {vs | eq ?vs ?RHS} => RHS end in
+    let RHSf := match (eval pattern powx in RHS) with ?RHSf _ => RHSf end in
+    change ({vs | eq vs (Let_In powx RHSf)}).
+    match goal with
+    | H : eq (?g powx) (?f powx)
+    |- {vs | eq vs (Let_In powx (fun x => if ?P then x else ?f x))} =>
+      exists (Let_In powx (fun x => if P then x else g x))
+    end.
+    break_if; try reflexivity.
+    cbv [Let_In].
+    auto.
   Defined.
 
-  Definition sqrt_5mod8_opt us := Eval cbv [proj1_sig sqrt_5mod8_opt_sig] in
-    proj1_sig (sqrt_5mod8_opt_sig us).
+  Definition sqrt_5mod8_opt powx powx_squared us := Eval cbv [proj1_sig sqrt_5mod8_opt_sig] in
+    proj1_sig (sqrt_5mod8_opt_sig powx powx_squared us).
 
-  Definition sqrt_5mod8_opt_correct us
-    : eq (sqrt_5mod8_opt us) (ModularBaseSystem.sqrt_5mod8 int_width _ _ chain chain_correct sqrt_m1 us)
-    := Eval cbv [proj2_sig sqrt_5mod8_opt_sig] in proj2_sig (sqrt_5mod8_opt_sig us).
+  Definition sqrt_5mod8_opt_correct powx powx_squared us
+    : eq (sqrt_5mod8_opt powx powx_squared us) (ModularBaseSystem.sqrt_5mod8 int_width _ _ chain chain_correct sqrt_m1 us)
+    := Eval cbv [proj2_sig sqrt_5mod8_opt_sig] in proj2_sig (sqrt_5mod8_opt_sig powx powx_squared us).
 
   End SquareRoot5mod8.
 
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index 330dc4e2f..b454daab6 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -1017,7 +1017,7 @@ Section SquareRootProofs.
         then 0
         else (2 ^ B) >> (nth_default 0 limb_widths (pred n)))).
   Definition bounded_by u bounds :=
-      (forall n : nat,
+      (forall n : nat, (n < length limb_widths)%nat ->
           0 <= nth_default 0 (to_list (length limb_widths) u) n < bounds n).
 
   Lemma eqb_true_iff : forall u v x y,
@@ -1063,48 +1063,32 @@ Section SquareRootProofs.
   Context (modulus_5mod8 : modulus mod 8 = 5).
   Context {ec : ExponentiationChain (modulus / 8 + 1)}.
   Context (sqrt_m1 : digits) (sqrt_m1_correct : mul sqrt_m1 sqrt_m1 ~= F.opp 1%F).
-  Context (mul_ : digits -> digits -> digits)
-          (mul_equiv : forall x y, ModularBaseSystem.eq (mul_ x y) (mul x y))
-          {mul_input_bounds : nat -> Z}
-          (mul_bounded : forall x y, bounded_by x mul_input_bounds ->
-                                     bounded_by y mul_input_bounds ->
-                                     bounded_by (mul_ x y) freeze_input_bounds).
-  Context (pow_ : digits -> list (nat * nat) -> digits)
-          (pow_equiv : forall x is, ModularBaseSystem.eq (pow_ x is) (pow x is))
-          {pow_input_bounds : nat -> Z}
-          (pow_bounded : forall x is, bounded_by x pow_input_bounds ->
-                                      bounded_by (pow_ x is) mul_input_bounds).
-
-  Lemma sqrt_5mod8_correct : forall u x, u ~= x ->
-    bounded_by u pow_input_bounds -> bounded_by u freeze_input_bounds ->
-    (sqrt_5mod8 B mul_ pow_ chain chain_correct sqrt_m1 u) ~= F.sqrt_5mod8 (decode sqrt_m1) x.
+
+  Lemma sqrt_5mod8_correct : forall u x powx powx_squared, u ~= x ->
+    bounded_by u freeze_input_bounds ->
+    bounded_by powx_squared freeze_input_bounds ->
+    ModularBaseSystem.eq powx (pow u chain) ->
+    ModularBaseSystem.eq powx_squared (mul powx powx) ->
+    (sqrt_5mod8 B powx powx_squared chain chain_correct sqrt_m1 u) ~= F.sqrt_5mod8 (decode sqrt_m1) x.
   Proof.
     cbv [sqrt_5mod8 F.sqrt_5mod8].
     intros.
     repeat match goal with
            | |- _ => progress (cbv [sqrt_5mod8 F.sqrt_5mod8]; intros)
            | |- _ => rewrite @F.pow_2_r in *
-           | |- _ => rewrite mul_equiv
-           | |- _ => rewrite pow_equiv
            | |- _ => rewrite eqb_correct in * by eassumption
            | |- (if eqb _ ?a ?b then _ else _) ~=
                 (if dec (?c = _) then _ else _) =>
-             assert (a ~= c) by (cbv [rep]; rewrite mul_equiv;
-                                 apply mul_rep; cbv [rep];
-                                 rewrite pow_equiv, <-chain_correct;
-                                 apply pow_rep; auto);
-               cbv [rep]; rewrite ?mul_equiv, ?pow_equiv;
-                 repeat break_if
+             assert (a ~= c) by
+                 (cbv [rep]; rewrite <-chain_correct, <-pow_rep, <-mul_rep;
+                  eassumption); repeat break_if
            | |- _ => apply mul_rep; try reflexivity;
-                       rewrite <-chain_correct; cbv [rep];
-                         rewrite pow_equiv; apply pow_rep; eassumption
-           | |- _ => rewrite <-chain_correct; apply pow_rep; eassumption
+                       rewrite <-chain_correct, <-pow_rep; eassumption
+           | |- _ => rewrite <-chain_correct, <-pow_rep; eassumption
            | H : eqb _ ?a ?b = true, H1 : ?b ~= ?y, H2 : ?a ~= ?x |- _ =>
-             rewrite <-(eqb_true_iff a b x y) in H
-               by (eassumption || apply mul_bounded, pow_bounded; auto)
+             rewrite <-(eqb_true_iff a b x y) in H by eassumption
            | H : eqb _ ?a ?b = false, H1 : ?b ~= ?y, H2 : ?a ~= ?x |- _ =>
-             rewrite <-(eqb_false_iff a b x y) in H
-               by (eassumption || apply mul_bounded, pow_bounded; auto)
+             rewrite <-(eqb_false_iff a b x y) in H by eassumption
            | |- _ => congruence
            end.
   Qed.