diff options
author | Jason Gross <jasongross9@gmail.com> | 2016-09-26 13:52:39 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2016-09-26 13:52:39 -0700 |
commit | 5a5ff97e68174e57a0c35a711718885de11367b8 (patch) | |
tree | 9b931f10e40472a7caa13f77acef729e65c07721 /src/ModularArithmetic | |
parent | bba9f9df9f6064f38f1ac6edfe9d5327bd3abfb6 (diff) | |
parent | 275bafc021e6f97cb2bd3dcf6ffd35068594d8fe (diff) |
Merge pull request #69 from JasonGross/scalable-scalars
Scalable Scalars, Dead Code Removal, Register Assignment
Diffstat (limited to 'src/ModularArithmetic')
-rw-r--r-- | src/ModularArithmetic/Montgomery/ZBounded.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/ModularArithmetic/Montgomery/ZBounded.v b/src/ModularArithmetic/Montgomery/ZBounded.v index 2da20ddcf..97bcf87b9 100644 --- a/src/ModularArithmetic/Montgomery/ZBounded.v +++ b/src/ModularArithmetic/Montgomery/ZBounded.v @@ -10,6 +10,7 @@ Require Import Crypto.ModularArithmetic.ZBounded. Require Import Crypto.BaseSystem. Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Notations. Local Open Scope small_zlike_scope. @@ -22,6 +23,19 @@ Section montgomery. (modulus'_valid : small_valid modulus') (modulus_nonzero : modulus <> 0). + (** pull out a common subexpression *) + Local Ltac cse := + let RHS := match goal with |- _ = ?decode ?RHS /\ _ => RHS end in + let v := fresh in + match RHS with + | context[?e] => not is_var e; set (v := e) at 1 2; test clearbody v + end; + revert v; + match goal with + | [ |- let v := ?val in ?LHS = ?decode ?RHS /\ ?P ] + => change (LHS = decode (dlet v := val in RHS) /\ P) + end. + Definition partial_reduce : forall v : LargeT, { partial_reduce : SmallT | large_valid v @@ -38,6 +52,7 @@ Section montgomery. rewrite <- partial_reduce_alt_eq by omega. cbv [Montgomery.Z.partial_reduce Montgomery.Z.partial_reduce_alt Montgomery.Z.prereduce]. pull_zlike_decode. + cse. subst pr; split; [ reflexivity | exact _ ]. Defined. @@ -58,6 +73,7 @@ Section montgomery. rewrite <- partial_reduce_alt_eq by omega. cbv [Montgomery.Z.partial_reduce Montgomery.Z.partial_reduce_alt Montgomery.Z.prereduce]. pull_zlike_decode. + cse. subst pr; split; [ reflexivity | exact _ ]. Defined. |