aboutsummaryrefslogtreecommitdiff
path: root/src/BoundedArithmetic
diff options
context:
space:
mode:
Diffstat (limited to 'src/BoundedArithmetic')
-rw-r--r--src/BoundedArithmetic/ArchitectureToZLike.v3
-rw-r--r--src/BoundedArithmetic/ArchitectureToZLikeProofs.v2
-rw-r--r--src/BoundedArithmetic/DoubleBounded.v26
-rw-r--r--src/BoundedArithmetic/DoubleBoundedProofs.v31
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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 04:53:16 +0000