aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Specific/IntegrationTestFreeze.v5
-rw-r--r--src/Specific/IntegrationTestSub.v5
-rw-r--r--src/Specific/X25519/C32/ReificationTypes.v23
-rw-r--r--src/Specific/X25519/C32/femul.v5
-rw-r--r--src/Specific/X25519/C32/fesquare.v5
-rw-r--r--src/Specific/X25519/C64/ReificationTypes.v23
-rw-r--r--src/Specific/X25519/C64/femul.v5
-rw-r--r--src/Specific/X25519/C64/fesquare.v5
-rw-r--r--src/Specific/X25519/C64/ladderstep.v5
9 files changed, 37 insertions, 44 deletions
diff --git a/src/Specific/IntegrationTestFreeze.v b/src/Specific/IntegrationTestFreeze.v
index ebfab0c69..79466b8d6 100644
--- a/src/Specific/IntegrationTestFreeze.v
+++ b/src/Specific/IntegrationTestFreeze.v
@@ -6,13 +6,10 @@ Require Import Crypto.Util.BoundedWord.
Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
Require Import Crypto.Compilers.Z.Bounds.Pipeline.
-Local Definition phi : feBW -> F m :=
- fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
-
(* TODO : change this to field once field isomorphism happens *)
Definition freeze :
{ freeze : feBW -> feBW
- | forall a, phi (freeze a) = phi a }.
+ | forall a, phiBW (freeze a) = phiBW a }.
Proof.
start_preglue.
do_rewrite_with_sig_by freeze_sig ltac:(fun _ => apply feBW_bounded); cbv_runtime.
diff --git a/src/Specific/IntegrationTestSub.v b/src/Specific/IntegrationTestSub.v
index f88dc51d9..c40041a1c 100644
--- a/src/Specific/IntegrationTestSub.v
+++ b/src/Specific/IntegrationTestSub.v
@@ -6,13 +6,10 @@ Require Import Crypto.Util.BoundedWord.
Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
Require Import Crypto.Compilers.Z.Bounds.Pipeline.
-Local Definition phi : feBW -> F m :=
- fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
-
(* TODO : change this to field once field isomorphism happens *)
Definition sub :
{ sub : feBW -> feBW -> feBW
- | forall a b, phi (sub a b) = F.sub (phi a) (phi b) }.
+ | forall a b, phiBW (sub a b) = F.sub (phiBW a) (phiBW b) }.
Proof.
start_preglue.
do_rewrite_with_2sig_add_carry sub_sig carry_sig; cbv_runtime.
diff --git a/src/Specific/X25519/C32/ReificationTypes.v b/src/Specific/X25519/C32/ReificationTypes.v
index 83ea345e5..6b2a47070 100644
--- a/src/Specific/X25519/C32/ReificationTypes.v
+++ b/src/Specific/X25519/C32/ReificationTypes.v
@@ -1,8 +1,10 @@
Require Import Coq.ZArith.ZArith.
+Require Import Coq.romega.ROmega.
Require Import Coq.Lists.List.
Local Open Scope Z_scope.
Require Import Crypto.Arithmetic.Core.
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
Require Import Crypto.Util.FixedWordSizes.
Require Import Crypto.Util.Tuple.
Require Import Crypto.Util.ZRange Crypto.Util.BoundedWord.
@@ -13,17 +15,16 @@ Section BoundedField.
Local Coercion Z.of_nat : nat >-> Z.
Let limb_widths := Eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 sz)).
- Let length_lw := Eval compute in List.length limb_widths.
Local Notation b_of exp := {| lower := 0 ; upper := P.upper_bound_of_exponent exp |}%Z (only parsing). (* max is [(0, 2^(exp+2) + 2^exp + 2^(exp-1) + 2^(exp-3) + 2^(exp-4) + 2^(exp-5) + 2^(exp-6) + 2^(exp-10) + 2^(exp-12) + 2^(exp-13) + 2^(exp-14) + 2^(exp-15) + 2^(exp-17) + 2^(exp-23) + 2^(exp-24))%Z] *)
(* The definition [bounds_exp] is a tuple-version of the
limb-widths, which are the [exp] argument in [b_of] above, i.e.,
the approximate base-2 exponent of the bounds on the limb in that
position. *)
- Let bounds_exp : Tuple.tuple Z length_lw
+ Let bounds_exp : Tuple.tuple Z sz
:= Eval compute in
- Tuple.from_list length_lw limb_widths eq_refl.
- Let bounds : Tuple.tuple zrange length_lw
+ Tuple.from_list sz limb_widths eq_refl.
+ Let bounds : Tuple.tuple zrange sz
:= Eval compute in
Tuple.map (fun e => b_of e) bounds_exp.
@@ -39,13 +40,19 @@ Section BoundedField.
: 0 <= B.Positional.eval wt (BoundedWordToZ sz bitwidth bounds a) < 2 * Z.pos m.
Proof.
destruct a as [a H]; unfold BoundedWordToZ, proj1_sig.
- revert H.
- cbv -[Z.le Z.add Z.mul Z.lt fst snd wordToZ wt]; cbn [fst snd].
+ destruct_head_hnf' and.
+ cbv -[Z.le Z.add Z.mul Z.lt fst snd wordToZ wt] in *; cbn [fst snd] in *.
repeat match goal with
+ | [ |- context[@wordToZ ?n ?x] ]
+ => generalize dependent (@wordToZ n x); intros
| [ |- context[wt ?n] ]
=> let v := (eval compute in (wt n)) in change (wt n) with v
end.
- intro; destruct_head'_and.
- omega.
+ romega.
Qed.
+
+ Definition phiW : feW -> F m :=
+ fun x => B.Positional.Fdecode wt (Tuple.map wordToZ x).
+ Definition phiBW : feBW -> F m :=
+ fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
End BoundedField.
diff --git a/src/Specific/X25519/C32/femul.v b/src/Specific/X25519/C32/femul.v
index 9d69dc9f3..9802a372e 100644
--- a/src/Specific/X25519/C32/femul.v
+++ b/src/Specific/X25519/C32/femul.v
@@ -6,13 +6,10 @@ Require Import Crypto.Util.BoundedWord.
Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
Require Import Crypto.Compilers.Z.Bounds.Pipeline.
-Local Definition phi : feBW -> F m :=
- fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
-
(* TODO : change this to field once field isomorphism happens *)
Definition mul :
{ mul : feBW -> feBW -> feBW
- | forall a b, phi (mul a b) = F.mul (phi a) (phi b) }.
+ | forall a b, phiBW (mul a b) = F.mul (phiBW a) (phiBW b) }.
Proof.
start_preglue.
do_rewrite_with_2sig_add_carry mul_sig carry_sig; cbv_runtime.
diff --git a/src/Specific/X25519/C32/fesquare.v b/src/Specific/X25519/C32/fesquare.v
index 32dc4acf9..ff1d0a566 100644
--- a/src/Specific/X25519/C32/fesquare.v
+++ b/src/Specific/X25519/C32/fesquare.v
@@ -6,13 +6,10 @@ Require Import Crypto.Util.BoundedWord.
Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
Require Import Crypto.Compilers.Z.Bounds.Pipeline.
-Local Definition phi : feBW -> F m :=
- fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
-
(* TODO : change this to field once field isomorphism happens *)
Definition square :
{ square : feBW -> feBW
- | forall a, phi (square a) = F.mul (phi a) (phi a) }.
+ | forall a, phiBW (square a) = F.mul (phiBW a) (phiBW a) }.
Proof.
start_preglue.
do_rewrite_with_1sig_add_carry square_sig carry_sig; cbv_runtime.
diff --git a/src/Specific/X25519/C64/ReificationTypes.v b/src/Specific/X25519/C64/ReificationTypes.v
index 6050404c8..009145467 100644
--- a/src/Specific/X25519/C64/ReificationTypes.v
+++ b/src/Specific/X25519/C64/ReificationTypes.v
@@ -1,8 +1,10 @@
Require Import Coq.ZArith.ZArith.
+Require Import Coq.romega.ROmega.
Require Import Coq.Lists.List.
Local Open Scope Z_scope.
Require Import Crypto.Arithmetic.Core.
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
Require Import Crypto.Util.FixedWordSizes.
Require Import Crypto.Util.Tuple.
Require Import Crypto.Util.ZRange Crypto.Util.BoundedWord.
@@ -13,17 +15,16 @@ Section BoundedField.
Local Coercion Z.of_nat : nat >-> Z.
Let limb_widths := Eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 sz)).
- Let length_lw := Eval compute in List.length limb_widths.
Local Notation b_of exp := {| lower := 0 ; upper := P.upper_bound_of_exponent exp |}%Z (only parsing). (* max is [(0, 2^(exp+2) + 2^exp + 2^(exp-1) + 2^(exp-3) + 2^(exp-4) + 2^(exp-5) + 2^(exp-6) + 2^(exp-10) + 2^(exp-12) + 2^(exp-13) + 2^(exp-14) + 2^(exp-15) + 2^(exp-17) + 2^(exp-23) + 2^(exp-24))%Z] *)
(* The definition [bounds_exp] is a tuple-version of the
limb-widths, which are the [exp] argument in [b_of] above, i.e.,
the approximate base-2 exponent of the bounds on the limb in that
position. *)
- Let bounds_exp : Tuple.tuple Z length_lw
+ Let bounds_exp : Tuple.tuple Z sz
:= Eval compute in
- Tuple.from_list length_lw limb_widths eq_refl.
- Let bounds : Tuple.tuple zrange length_lw
+ Tuple.from_list sz limb_widths eq_refl.
+ Let bounds : Tuple.tuple zrange sz
:= Eval compute in
Tuple.map (fun e => b_of e) bounds_exp.
@@ -39,13 +40,19 @@ Section BoundedField.
: 0 <= B.Positional.eval wt (BoundedWordToZ sz bitwidth bounds a) < 2 * Z.pos m.
Proof.
destruct a as [a H]; unfold BoundedWordToZ, proj1_sig.
- revert H.
- cbv -[Z.le Z.add Z.mul Z.lt fst snd wordToZ wt]; cbn [fst snd].
+ destruct_head_hnf' and.
+ cbv -[Z.le Z.add Z.mul Z.lt fst snd wordToZ wt] in *; cbn [fst snd] in *.
repeat match goal with
+ | [ |- context[@wordToZ ?n ?x] ]
+ => generalize dependent (@wordToZ n x); intros
| [ |- context[wt ?n] ]
=> let v := (eval compute in (wt n)) in change (wt n) with v
end.
- intro; destruct_head'_and.
- omega.
+ romega.
Qed.
+
+ Definition phiW : feW -> F m :=
+ fun x => B.Positional.Fdecode wt (Tuple.map wordToZ x).
+ Definition phiBW : feBW -> F m :=
+ fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
End BoundedField.
diff --git a/src/Specific/X25519/C64/femul.v b/src/Specific/X25519/C64/femul.v
index aad541ff6..f0db6c937 100644
--- a/src/Specific/X25519/C64/femul.v
+++ b/src/Specific/X25519/C64/femul.v
@@ -6,13 +6,10 @@ Require Import Crypto.Util.BoundedWord.
Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
Require Import Crypto.Compilers.Z.Bounds.Pipeline.
-Local Definition phi : feBW -> F m :=
- fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
-
(* TODO : change this to field once field isomorphism happens *)
Definition mul :
{ mul : feBW -> feBW -> feBW
- | forall a b, phi (mul a b) = F.mul (phi a) (phi b) }.
+ | forall a b, phiBW (mul a b) = F.mul (phiBW a) (phiBW b) }.
Proof.
start_preglue.
do_rewrite_with_2sig_add_carry mul_sig carry_sig; cbv_runtime.
diff --git a/src/Specific/X25519/C64/fesquare.v b/src/Specific/X25519/C64/fesquare.v
index a88ea6e24..6be0713b6 100644
--- a/src/Specific/X25519/C64/fesquare.v
+++ b/src/Specific/X25519/C64/fesquare.v
@@ -6,13 +6,10 @@ Require Import Crypto.Util.BoundedWord.
Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
Require Import Crypto.Compilers.Z.Bounds.Pipeline.
-Local Definition phi : feBW -> F m :=
- fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
-
(* TODO : change this to field once field isomorphism happens *)
Definition square :
{ square : feBW -> feBW
- | forall a, phi (square a) = F.mul (phi a) (phi a) }.
+ | forall a, phiBW (square a) = F.mul (phiBW a) (phiBW a) }.
Proof.
start_preglue.
do_rewrite_with_1sig_add_carry square_sig carry_sig; cbv_runtime.
diff --git a/src/Specific/X25519/C64/ladderstep.v b/src/Specific/X25519/C64/ladderstep.v
index 62f728dd5..0d7c33588 100644
--- a/src/Specific/X25519/C64/ladderstep.v
+++ b/src/Specific/X25519/C64/ladderstep.v
@@ -20,9 +20,6 @@ Require Import Crypto.Util.Tactics.SubstEvars.
Require Import Crypto.Util.Tactics.ETransitivity.
Require Import Crypto.Util.Notations.
-Local Definition phi : feW -> F m :=
- fun x => B.Positional.Fdecode wt (Tuple.map wordToZ x).
-
(** TODO(jadep,andreser): Move to NewBaseSystemTest? *)
Definition FMxzladderstep := @M.donnaladderstep (F m) F.add F.sub F.mul.
@@ -84,7 +81,7 @@ Definition xzladderstep :
-> feW_bounded (fst Q') /\ feW_bounded (snd Q')
-> ((feW_bounded (fst (fst xz)) /\ feW_bounded (snd (fst xz)))
/\ (feW_bounded (fst (snd xz)) /\ feW_bounded (snd (snd xz))))
- /\ Tuple.map (n:=2) (Tuple.map (n:=2) phi) xz = FMxzladderstep (eval (proj1_sig a24_sig)) (phi x1) (Tuple.map (n:=2) phi Q) (Tuple.map (n:=2) phi Q') }.
+ /\ Tuple.map (n:=2) (Tuple.map (n:=2) phiW) xz = FMxzladderstep (eval (proj1_sig a24_sig)) (phiW x1) (Tuple.map (n:=2) phiW Q) (Tuple.map (n:=2) phiW Q') }.
Proof.
start_preglue.
unmap_map_tuple ().
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-07 06:46:06 +0000