diff options
Diffstat (limited to 'src/BoundedArithmetic/DoubleBounded.v')
| -rw-r--r-- | src/BoundedArithmetic/DoubleBounded.v | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/src/BoundedArithmetic/DoubleBounded.v b/src/BoundedArithmetic/DoubleBounded.v index b6aa858ff..5cf48cd3b 100644 --- a/src/BoundedArithmetic/DoubleBounded.v +++ b/src/BoundedArithmetic/DoubleBounded.v @@ -6,7 +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. +Require Import Crypto.Util.LetIn. Local Open Scope nat_scope. Local Open Scope Z_scope. @@ -28,13 +28,13 @@ 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 => llet xss := xss in - llet yss := yss in + | S k' => fun xss yss carry => dlet xss := xss in + dlet yss := yss in let '(xs, x) := eta xss in let '(ys, y) := eta yss in - llet addv := (@ripple_carry_tuple' _ f k' xs ys carry) in + dlet addv := (@ripple_carry_tuple' _ f k' xs ys carry) in let '(carry, zs) := eta addv in - llet fxy := (f x y carry) in + dlet fxy := (f x y carry) in let '(carry, z) := eta fxy in (carry, (zs, z)) end. @@ -80,15 +80,15 @@ Section tuple2. {ldi : load_immediate W}. Definition mul_double (a b : W) : tuple W 2 - := llet a := a in - llet b := b in + := dlet a := a in + dlet 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 + dlet out := out in + dlet tmp := mulhwhl a b in + dlet 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 + dlet tmp := mulhwhl b a in + dlet addv := (ripple_carry_adc adc out (shl tmp half_n, shr tmp half_n) false) in let '(_, out) := eta addv in out. |