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, 9 insertions, 4 deletions

diff --git a/src/BoundedArithmetic/ArchitectureToZLike.v b/src/BoundedArithmetic/ArchitectureToZLike.v
index e37932192..939265c1e 100644
--- a/src/BoundedArithmetic/ArchitectureToZLike.v
+++ b/src/BoundedArithmetic/ArchitectureToZLike.v
@@ -13,11 +13,12 @@ Section fancy_machine_p256_montgomery_foundation.
   Local Notation n := (2 * n_over_two).
   Context (ops : fancy_machine.instructions n) (modulus : Z).
 
-  Global Instance ZLikeOps_of_ArchitectureBoundedOps (smaller_bound_exp : Z)
+  Local Instance ZLikeOps_of_ArchitectureBoundedOps_Factored (smaller_bound_exp : Z)
+         ldi_modulus ldi_0
     : ZLikeOps (2^n) (2^smaller_bound_exp) modulus :=
     { LargeT := tuple fancy_machine.W 2;
       SmallT := fancy_machine.W;
-      modulus_digits := ldi modulus;
+      modulus_digits := ldi_modulus;
       decode_large := decode;
       decode_small := decode;
       Mod_SmallBound v := fst v;
@@ -28,6 +29,10 @@ Section fancy_machine_p256_montgomery_foundation.
       Mul x y := muldw x y;
       CarryAdd x y := adc x y false;
       CarrySubSmall x y := subc x y false;
-      ConditionalSubtract b x := let v := selc b (ldi modulus) (ldi 0) in snd (subc x v false);
-      ConditionalSubtractModulus y := addm y (ldi 0) (ldi modulus) }.
+      ConditionalSubtract b x := let v := selc b (ldi_modulus) (ldi_0) in snd (subc x v false);
+      ConditionalSubtractModulus y := addm y (ldi_0) (ldi_modulus) }.
+
+  Global Instance ZLikeOps_of_ArchitectureBoundedOps (smaller_bound_exp : Z)
+    : ZLikeOps (2^n) (2^smaller_bound_exp) modulus :=
+    @ZLikeOps_of_ArchitectureBoundedOps_Factored smaller_bound_exp (ldi modulus) (ldi 0).
 End fancy_machine_p256_montgomery_foundation.