From 0069611d31c4a3390ff31098d4c582c86fbf848d Mon Sep 17 00:00:00 2001 From: jadep Date: Tue, 19 Feb 2019 14:34:24 -0500 Subject: finish porting barrett and montgomery code to new glue style --- src/Fancy/Barrett256.v | 38 +++++++++++++------------------------- src/Fancy/Montgomery256.v | 36 ++++++++++++------------------------ 2 files changed, 25 insertions(+), 49 deletions(-) (limited to 'src') 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. } -- cgit v1.2.3