diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-01-17 15:07:47 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-01-18 19:44:48 -0500 |
| commit | cdd5ffb086eb647eabe640c81de9d8af7cd0a1dd (patch) | |
| tree | 4540df27da661c35fdc5246f1692fa124003ff6f /src/Fancy | |
| parent | b99dd6da3b6370bc225d3b501bda07c49fd29c12 (diff) | |
Split up PushButtonSynthesis.v
Closes #497
Diffstat (limited to 'src/Fancy')
| -rw-r--r-- | src/Fancy/Barrett256.v | 8 | ||||
| -rw-r--r-- | src/Fancy/Montgomery256.v | 7 |
2 files changed, 8 insertions, 7 deletions
diff --git a/src/Fancy/Barrett256.v b/src/Fancy/Barrett256.v index 2ee19e6e6..46e8f6f52 100644 --- a/src/Fancy/Barrett256.v +++ b/src/Fancy/Barrett256.v @@ -8,7 +8,7 @@ Require Import Crypto.Fancy.Prod. Require Import Crypto.Fancy.Spec. Require Import Crypto.Language. Import Language.Compilers. Require Import Crypto.LanguageWf. -Require Import Crypto.PushButtonSynthesis. +Require Import Crypto.PushButtonSynthesis.BarrettReduction. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.ZUtil.EquivModulo. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. @@ -144,7 +144,7 @@ Module Barrett256. { cbn. repeat match goal with | _ => apply Compilers.expr.WfLetIn - | _ => progress wf_subgoal + | _ => progress wf_subgoal | _ => econstructor end. } { cbn. cbv [muLow M]. @@ -299,7 +299,7 @@ Module Barrett256. repeat match goal with H : context [start_context] |- _ => rewrite <-H end. - + cbv [barrett_red256_alloc barrett_red256_fancy]. repeat step. reflexivity. @@ -399,4 +399,4 @@ Eval cbv beta iota delta [Barrett256.barrett_red256_alloc] in Barrett256.barrett 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. *) -*)
\ No newline at end of file +*) diff --git a/src/Fancy/Montgomery256.v b/src/Fancy/Montgomery256.v index e5f9c5072..19415ad03 100644 --- a/src/Fancy/Montgomery256.v +++ b/src/Fancy/Montgomery256.v @@ -7,7 +7,8 @@ Require Import Crypto.Fancy.Prod. Require Import Crypto.Fancy.Spec. Require Import Crypto.Language. Import Language.Compilers. Require Import Crypto.LanguageWf. -Require Import Crypto.PushButtonSynthesis. +Require Import Crypto.Arithmetic. (* For the MontgomeryReduction Module *) +Require Import Crypto.PushButtonSynthesis.MontgomeryReduction. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.ZUtil.EquivModulo. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. @@ -140,7 +141,7 @@ Module Montgomery256. { cbn. repeat match goal with | _ => apply Compilers.expr.WfLetIn - | _ => progress wf_subgoal + | _ => progress wf_subgoal | _ => econstructor end. } { cbn. cbv [N' N]. @@ -317,4 +318,4 @@ preconditions. *) (* Check Montgomery256.prod_montred256_correct. Print Assumptions Montgomery256.prod_montred256_correct. -*)
\ No newline at end of file +*) |