finish porting barrett and montgomery code to new glue style

2 files changed, 25 insertions, 49 deletions

diff --git a/src/Fancy/Barrett256.v b/src/Fancy/Barrett256.v
index 58a9efd2d..21da40aa7 100644
--- a/src/Fancy/Barrett256.v
+++ b/src/Fancy/Barrett256.v
@@ -3,6 +3,7 @@ Require Import Coq.derive.Derive.
 Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
 Require Import Coq.Lists.List. Import ListNotations.
 Require Import Crypto.Arithmetic.
+Require Import Crypto.COperationSpecifications. Import COperationSpecifications.BarrettReduction.
 Require Import Crypto.Fancy.Compiler.
 Require Import Crypto.Fancy.Prod.
 Require Import Crypto.Fancy.Spec.
@@ -21,9 +22,17 @@ Module Barrett256.
   Definition machine_wordsize := 256.
 
   Derive barrett_red256
-         SuchThat (BarrettReduction.rbarrett_red_correctT M machine_wordsize barrett_red256)
-         As barrett_red256_correct.
-  Proof. Time solve_rbarrett_red_nocache machine_wordsize. Time Qed.
+         SuchThat (barrett_red M machine_wordsize = ErrorT.Success barrett_red256)
+         As barrett_red256_eq.
+  Proof. lazy; reflexivity. Qed.
+
+  Lemma barrett_red256_correct :
+    COperationSpecifications.BarrettReduction.barrett_red_correct machine_wordsize M (expr.Interp (@ident.gen_interp cast_oor) barrett_red256).
+  Proof.
+    apply barrett_red_correct with (n:=2%nat) (nout:=2%nat) (machine_wordsize:=machine_wordsize).
+    { lazy. reflexivity. }
+    { apply barrett_red256_eq. }
+  Qed.
 
   Definition muLow := Eval lazy in (2 ^ (2 * machine_wordsize) / M) mod (2^machine_wordsize).
 
@@ -41,26 +50,6 @@ Module Barrett256.
           end; lazy; try split; congruence.
   Qed.
 
-  Strategy -100 [type.app_curried].
-  Local Arguments ZRange.is_bounded_by_bool / .
-  Lemma barrett_red256_correct_full  :
-    forall (xLow xHigh : Z),
-      0 <= xLow < 2 ^ machine_wordsize ->
-      0 <= xHigh < M ->
-      expr.Interp (@ident.gen_interp cast_oor) barrett_red256 xLow xHigh = (xLow + 2 ^ machine_wordsize * xHigh) mod M.
-  Proof.
-    intros.
-    rewrite <-barrett_reduce_correct_specialized by assumption.
-    destruct (proj1 barrett_red256_correct (xLow, (xHigh, tt)) (xLow, (xHigh, tt))) as [H1 H2].
-    { repeat split. }
-    { cbn -[Z.pow].
-      rewrite !andb_true_iff.
-      assert (M < 2^machine_wordsize) by (vm_compute; reflexivity).
-      repeat apply conj; Z.ltb_to_lt; trivial; omega. }
-    { etransitivity; [ eapply H2 | ]. (* need Strategy -100 [type.app_curried]. for this to be fast *)
-      generalize BarrettReduction.barrett_reduce; vm_compute; reflexivity. }
-  Qed.
-
   Definition barrett_red256_fancy' (xLow xHigh RegMuLow RegMod RegZero error : positive) :=
     of_Expr 6%positive
             (make_consts [(RegMuLow, muLow); (RegMod, M); (RegZero, 0)])
@@ -121,7 +110,7 @@ Module Barrett256.
     intros.
     rewrite barrett_red256_fancy_eq.
     cbv [barrett_red256_fancy'].
-    rewrite <-barrett_red256_correct_full by auto.
+    rewrite <-barrett_red256_correct by auto.
     eapply of_Expr_correct with (x2 := (xLow, (xHigh, tt))).
     { cbn; intros; subst RegZero RegMod RegMuLow RegxHigh RegxLow.
       intuition; Prod.inversion_prod; subst; cbv. break_innermost_match; congruence. }
@@ -330,5 +319,4 @@ Eval cbv beta iota delta [Prod.MulMod Prod.Mul256x256] in Prod.MulMod.
 (*
 Check Barrett256.prod_barrett_red256_correct.
 Print Assumptions Barrett256.prod_barrett_red256_correct.
-(* The equivalence with generated code is admitted as barrett_red256_alloc_equivalent. *)
 *)
diff --git a/src/Fancy/Montgomery256.v b/src/Fancy/Montgomery256.v
index ec4848b0b..078cdd193 100644
--- a/src/Fancy/Montgomery256.v
+++ b/src/Fancy/Montgomery256.v
@@ -24,9 +24,17 @@ Module Montgomery256.
   Definition machine_wordsize := 256.
 
   Derive montred256
-         SuchThat (MontgomeryReduction.rmontred_correctT N R N' machine_wordsize montred256)
-         As montred256_correct.
-  Proof. Time solve_rmontred_nocache machine_wordsize. Time Qed.
+         SuchThat (montred N R N' machine_wordsize = ErrorT.Success montred256)
+         As montred256_eq.
+  Proof. lazy; reflexivity. Qed.
+
+  Lemma montred256_correct :
+    COperationSpecifications.MontgomeryReduction.montred_correct N R R' (expr.Interp (@ident.gen_interp cast_oor) montred256).
+  Proof.
+    apply montred_correct with (n:=2%nat) (nout:=2%nat) (machine_wordsize:=machine_wordsize) (N':=N').
+    { lazy. reflexivity. }
+    { apply montred256_eq. }
+  Qed.
 
   Lemma montred'_correct_specialized R' (R'_correct : Z.equiv_modulo N (R * R') 1) :
     forall (lo hi : Z),
@@ -42,26 +50,6 @@ Module Montgomery256.
           end; lazy; try split; congruence.
   Qed.
 
-  Strategy -100 [type.app_curried].
-  Local Arguments ZRange.is_bounded_by_bool / .
-  Lemma montred256_correct_full  R' (R'_correct : Z.equiv_modulo N (R * R') 1) :
-    forall (lo hi : Z),
-      0 <= lo < R ->
-      0 <= hi < R ->
-      0 <= lo + R * hi < R * N ->
-      expr.Interp (@ident.gen_interp cast_oor) montred256 lo hi = ((lo + R * hi) * R') mod N.
-  Proof.
-    intros.
-    rewrite <-montred'_correct_specialized by assumption.
-    destruct (proj1 montred256_correct (lo, (hi, tt)) (lo, (hi, tt))) as [H2 H3].
-    { repeat split. }
-    { cbn -[Z.pow].
-      rewrite !andb_true_iff.
-      repeat apply conj; Z.ltb_to_lt; trivial; cbv [R N machine_wordsize] in *; lia. }
-    { etransitivity; [ eapply H3 | ]. (* need Strategy -100 [type.app_curried]. for this to be fast *)
-      generalize MontgomeryReduction.montred'; vm_compute; reflexivity. }
-  Qed.
-
   Definition montred256_fancy' (RegMod RegPInv RegZero lo hi error : positive) :=
     of_Expr 6%positive
             (make_consts [(RegMod, N); (RegZero, 0); (RegPInv, N')])
@@ -121,7 +109,7 @@ Module Montgomery256.
     intros.
     rewrite montred256_fancy_eq.
     cbv [montred256_fancy'].
-    rewrite <-montred256_correct_full by (auto; reflexivity).
+    rewrite <-montred256_correct by (auto; reflexivity).
     eapply of_Expr_correct with (x2 := (lo, (hi, tt))).
     { cbn; intros; subst RegZero RegMod RegPInv RegHi RegLo.
       intuition; Prod.inversion_prod; subst; cbv. break_innermost_match; congruence. }