Don't inline everything in Montgomery and Barrett

We still use CSE in fancy machine, because we want to lift the ldi's
above the rest of the code.  However, on a quick inspection, the
algorithm no longer needs CSE to be duplicate-free.

4 files changed, 51 insertions, 11 deletions

diff --git a/src/BoundedArithmetic/ArchitectureToZLike.v b/src/BoundedArithmetic/ArchitectureToZLike.v
index 3388ece78..80f0d9803 100644
--- a/src/BoundedArithmetic/ArchitectureToZLike.v
+++ b/src/BoundedArithmetic/ArchitectureToZLike.v
@@ -4,6 +4,7 @@ Require Import Crypto.BoundedArithmetic.Interface.
 Require Import Crypto.BoundedArithmetic.DoubleBounded.
 Require Import Crypto.ModularArithmetic.ZBounded.
 Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.LockedLet.
 
 Local Open Scope Z_scope.
 
@@ -23,7 +24,7 @@ Section fancy_machine_p256_montgomery_foundation.
       DivBy_SmallBound v := snd v;
       DivBy_SmallerBound v := if smaller_bound_exp =? n
                               then snd v
-                              else shrd (snd v) (fst v) smaller_bound_exp;
+                              else llet v := v in shrd (snd v) (fst v) smaller_bound_exp;
       Mul x y := muldw x y;
       CarryAdd x y := adc x y false;
       CarrySubSmall x y := subc x y false;
diff --git a/src/BoundedArithmetic/ArchitectureToZLikeProofs.v b/src/BoundedArithmetic/ArchitectureToZLikeProofs.v
index 804296374..243ecb064 100644
--- a/src/BoundedArithmetic/ArchitectureToZLikeProofs.v
+++ b/src/BoundedArithmetic/ArchitectureToZLikeProofs.v
@@ -8,6 +8,7 @@ Require Import Crypto.BoundedArithmetic.ArchitectureToZLike.
 Require Import Crypto.ModularArithmetic.ZBounded.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.ZUtil Crypto.Util.Tactics.
+Require Import Crypto.Util.LockedLet.
 
 Local Open Scope nat_scope.
 Local Open Scope Z_scope.
@@ -53,6 +54,7 @@ Section fancy_machine_p256_montgomery_foundation.
   Local Ltac post_t_step :=
     match goal with
     | _ => reflexivity
+    | _ => rewrite !unlock_let
     | _ => progress autorewrite with zsimplify_const
     | [ |- fst ?x = (?a <=? ?b) :> bool ]
       => cut (((if fst x then 1 else 0) = (if a <=? b then 1 else 0))%Z);
diff --git a/src/BoundedArithmetic/DoubleBounded.v b/src/BoundedArithmetic/DoubleBounded.v
index b624c5082..b6aa858ff 100644
--- a/src/BoundedArithmetic/DoubleBounded.v
+++ b/src/BoundedArithmetic/DoubleBounded.v
@@ -6,6 +6,7 @@ Require Import Crypto.ModularArithmetic.Pow2Base.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.Notations.
+Require Import Crypto.Util.LockedLet.
 
 Local Open Scope nat_scope.
 Local Open Scope Z_scope.
@@ -27,10 +28,14 @@ Section ripple_carry_definitions.
     : forall (xs ys : tuple' T k) (carry : bool), bool * tuple' T k
     := match k return forall (xs ys : tuple' T k) (carry : bool), bool * tuple' T k with
        | O => f
-       | S k' => fun xss yss carry => let '(xs, x) := eta xss in
+       | S k' => fun xss yss carry => llet xss := xss in
+                                      llet yss := yss in
+                                      let '(xs, x) := eta xss in
                                       let '(ys, y) := eta yss in
-                                      let '(carry, zs) := eta (@ripple_carry_tuple' _ f k' xs ys carry) in
-                                      let '(carry, z) := eta (f x y carry) in
+                                      llet addv := (@ripple_carry_tuple' _ f k' xs ys carry) in
+                                      let '(carry, zs) := eta addv in
+                                      llet fxy := (f x y carry) in
+                                      let '(carry, z) := eta fxy in
                                       (carry, (zs, z))
        end.
 
@@ -75,11 +80,16 @@ Section tuple2.
             {ldi : load_immediate W}.
 
     Definition mul_double (a b : W) : tuple W 2
-      := let out : tuple W 2 := (mulhwll a b, mulhwhh a b) in
-         let tmp             := mulhwhl a b in
-         let '(_, out)   := eta (ripple_carry_adc adc out (shl tmp half_n, shr tmp half_n) false) in
-         let tmp             := mulhwhl b a in
-         let '(_, out)   := eta (ripple_carry_adc adc out (shl tmp half_n, shr tmp half_n) false) in
+      := llet a              := a in
+         llet b              := b in
+         let out : tuple W 2 := (mulhwll a b, mulhwhh a b) in
+         llet out            := out in
+         llet tmp            := mulhwhl a b in
+         llet addv           := (ripple_carry_adc adc out (shl tmp half_n, shr tmp half_n) false) in
+         let '(_, out)       := eta addv in
+         llet tmp            := mulhwhl b a in
+         llet addv           := (ripple_carry_adc adc out (shl tmp half_n, shr tmp half_n) false) in
+         let '(_, out)       := eta addv in
          out.
 
     (** Require a dummy [decoder] for these instances to allow
diff --git a/src/BoundedArithmetic/DoubleBoundedProofs.v b/src/BoundedArithmetic/DoubleBoundedProofs.v
index 53ac59d00..95ba35579 100644
--- a/src/BoundedArithmetic/DoubleBoundedProofs.v
+++ b/src/BoundedArithmetic/DoubleBoundedProofs.v
@@ -12,6 +12,7 @@ Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.Notations.
+Require Import Crypto.Util.LockedLet.
 
 Import ListNotations.
 Local Open Scope list_scope.
@@ -235,6 +236,28 @@ Global Instance decode_mul_double
   : forall x y, tuple_decoder (muldw x y) <~=~> (decode x * decode y)%Z
   := proj1 decode_mul_double_iff _.
 
+
+Lemma ripple_carry_tuple_SS' {T} f k xss yss carry
+  : @ripple_carry_tuple T f (S (S k)) xss yss carry
+    = llet xss := xss in
+      llet yss := yss in
+      let '(xs, x) := eta xss in
+      let '(ys, y) := eta yss in
+      llet addv := (@ripple_carry_tuple _ f (S k) xs ys carry) in
+      let '(carry, zs) := eta addv in
+      llet fxy := (f x y carry) in
+      let '(carry, z) := eta fxy in
+      (carry, (zs, z)).
+Proof. reflexivity. Qed.
+
+Local Ltac eta_expand :=
+  repeat match goal with
+         | _ => rewrite !unlock_let
+         | [ |- context[let '(x, y) := ?e in _] ]
+           => rewrite (surjective_pairing e)
+         | _ => rewrite <- !surjective_pairing
+         end.
+
 Lemma ripple_carry_tuple_SS {T} f k xss yss carry
   : @ripple_carry_tuple T f (S (S k)) xss yss carry
     = let '(xs, x) := eta xss in
@@ -242,7 +265,11 @@ Lemma ripple_carry_tuple_SS {T} f k xss yss carry
       let '(carry, zs) := eta (@ripple_carry_tuple _ f (S k) xs ys carry) in
       let '(carry, z) := eta (f x y carry) in
       (carry, (zs, z)).
-Proof. reflexivity. Qed.
+Proof.
+  rewrite ripple_carry_tuple_SS'.
+  eta_expand.
+  reflexivity.
+Qed.
 
 Lemma carry_is_good (n z0 z1 k : Z)
   : 0 <= n ->
@@ -414,7 +441,7 @@ Section tuple2.
     Proof.
       assert (0 <= 2 * half_n) by eauto using decode_exponent_nonnegative.
       assert (0 <= half_n) by omega.
-      unfold mul_double.
+      unfold mul_double; eta_expand.
       push_decode; autorewrite with simpl_tuple_decoder; simplify_projections.
       autorewrite with zsimplify Zshift_to_pow push_Zpow.
       rewrite !spread_left_from_shift_half_correct.