Drop CSE from Fancy Machine

By being careful about building the expressions in the first place, we
no longer need it, and can rely on dead code elimination.

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.