aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/X25519
diff options
context:
space:
mode:
Diffstat (limited to 'src/Specific/X25519')
-rw-r--r--src/Specific/X25519/C32/ArithmeticSynthesisTest.v2
-rw-r--r--src/Specific/X25519/C32/ReificationTypes.v62
-rw-r--r--src/Specific/X25519/C64/ArithmeticSynthesisTest.v2
-rw-r--r--src/Specific/X25519/C64/ReificationTypes.v62
-rw-r--r--src/Specific/X25519/C64/ladderstepDisplay.log4
5 files changed, 22 insertions, 110 deletions
diff --git a/src/Specific/X25519/C32/ArithmeticSynthesisTest.v b/src/Specific/X25519/C32/ArithmeticSynthesisTest.v
index 6b1d5ee11..c961afd69 100644
--- a/src/Specific/X25519/C32/ArithmeticSynthesisTest.v
+++ b/src/Specific/X25519/C32/ArithmeticSynthesisTest.v
@@ -52,6 +52,8 @@ Section Ops.
Lemma sz_nonzero : sz <> 0%nat. Proof. vm_decide. Qed.
Lemma wt_nonzero i : wt i <> 0.
Proof. eapply pow_ceil_mul_nat_nonzero; vm_decide. Qed.
+ Lemma wt_nonneg i : 0 <= wt i.
+ Proof. apply pow_ceil_mul_nat_nonneg; vm_decide. Qed.
Lemma wt_divides i : wt (S i) / wt i > 0.
Proof. apply pow_ceil_mul_nat_divide; vm_decide. Qed.
Lemma wt_divides' i : wt (S i) / wt i <> 0.
diff --git a/src/Specific/X25519/C32/ReificationTypes.v b/src/Specific/X25519/C32/ReificationTypes.v
index 6b2a47070..c5a9e0fd3 100644
--- a/src/Specific/X25519/C32/ReificationTypes.v
+++ b/src/Specific/X25519/C32/ReificationTypes.v
@@ -1,58 +1,12 @@
-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.
-Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Specific.ReificationTypes.
Require Import Crypto.Specific.X25519.C32.ArithmeticSynthesisTest.
-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)).
-
- 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 sz
- := Eval compute in
- 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.
-
- Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (List.fold_right Z.max 0 limb_widths))).
- Let bitwidth := Eval compute in (2^lgbitwidth)%nat.
- Let feZ : Type := tuple Z sz.
- Definition feW : Type := Eval cbv [lgbitwidth] in tuple (wordT lgbitwidth) sz.
- Definition feW_bounded : feW -> Prop
- := Eval cbv [bounds] in fun w => is_bounded_by None bounds (map wordToZ w).
- Definition feBW : Type := Eval cbv [bitwidth bounds] in BoundedWord sz bitwidth bounds.
+Module RP <: ReificationTypesPrePackage.
+ Definition ReificationTypes_package' : { T : _ & T }.
+ Proof. make_ReificationTypes_package wt sz bounds m wt_nonneg P.upper_bound_of_exponent. Defined.
- Lemma feBW_bounded (a : feBW)
- : 0 <= B.Positional.eval wt (BoundedWordToZ sz bitwidth bounds a) < 2 * Z.pos m.
- Proof.
- destruct a as [a H]; unfold BoundedWordToZ, proj1_sig.
- 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.
- romega.
- Qed.
+ Definition ReificationTypes_package
+ := Eval cbv [ReificationTypes_package' projT2] in projT2 ReificationTypes_package'.
+End RP.
- 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.
+Module Export ReificationTypes := MakeReificationTypes RP.
diff --git a/src/Specific/X25519/C64/ArithmeticSynthesisTest.v b/src/Specific/X25519/C64/ArithmeticSynthesisTest.v
index f4ef43f20..6994e13be 100644
--- a/src/Specific/X25519/C64/ArithmeticSynthesisTest.v
+++ b/src/Specific/X25519/C64/ArithmeticSynthesisTest.v
@@ -52,6 +52,8 @@ Section Ops.
Lemma sz_nonzero : sz <> 0%nat. Proof. vm_decide. Qed.
Lemma wt_nonzero i : wt i <> 0.
Proof. eapply pow_ceil_mul_nat_nonzero; vm_decide. Qed.
+ Lemma wt_nonneg i : 0 <= wt i.
+ Proof. apply pow_ceil_mul_nat_nonneg; vm_decide. Qed.
Lemma wt_divides i : wt (S i) / wt i > 0.
Proof. apply pow_ceil_mul_nat_divide; vm_decide. Qed.
Lemma wt_divides' i : wt (S i) / wt i <> 0.
diff --git a/src/Specific/X25519/C64/ReificationTypes.v b/src/Specific/X25519/C64/ReificationTypes.v
index 009145467..0e999b2fc 100644
--- a/src/Specific/X25519/C64/ReificationTypes.v
+++ b/src/Specific/X25519/C64/ReificationTypes.v
@@ -1,58 +1,12 @@
-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.
-Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Specific.ReificationTypes.
Require Import Crypto.Specific.X25519.C64.ArithmeticSynthesisTest.
-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)).
-
- 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 sz
- := Eval compute in
- 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.
-
- Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (List.fold_right Z.max 0 limb_widths))).
- Let bitwidth := Eval compute in (2^lgbitwidth)%nat.
- Let feZ : Type := tuple Z sz.
- Definition feW : Type := Eval cbv [lgbitwidth] in tuple (wordT lgbitwidth) sz.
- Definition feW_bounded : feW -> Prop
- := Eval cbv [bounds] in fun w => is_bounded_by None bounds (map wordToZ w).
- Definition feBW : Type := Eval cbv [bitwidth bounds] in BoundedWord sz bitwidth bounds.
+Module RP <: ReificationTypesPrePackage.
+ Definition ReificationTypes_package' : { T : _ & T }.
+ Proof. make_ReificationTypes_package wt sz bounds m wt_nonneg P.upper_bound_of_exponent. Defined.
- Lemma feBW_bounded (a : feBW)
- : 0 <= B.Positional.eval wt (BoundedWordToZ sz bitwidth bounds a) < 2 * Z.pos m.
- Proof.
- destruct a as [a H]; unfold BoundedWordToZ, proj1_sig.
- 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.
- romega.
- Qed.
+ Definition ReificationTypes_package
+ := Eval cbv [ReificationTypes_package' projT2] in projT2 ReificationTypes_package'.
+End RP.
- 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.
+Module Export ReificationTypes := MakeReificationTypes RP.
diff --git a/src/Specific/X25519/C64/ladderstepDisplay.log b/src/Specific/X25519/C64/ladderstepDisplay.log
index ca8ba4396..4e22b729f 100644
--- a/src/Specific/X25519/C64/ladderstepDisplay.log
+++ b/src/Specific/X25519/C64/ladderstepDisplay.log
@@ -1,4 +1,4 @@
-λ x x0 x1 x2 x3 : ReificationTypes.feW,
+λ x x0 x1 x2 x3 : ReificationTypes.RP.feW,
let (a, b) := Interp-η
(λ var : Syntax.base_type → Type,
λ '(x15, x16, x14, x12, x10, (x25, x26, x24, x22, x20, (x33, x34, x32, x30, x28)), (x43, x44, x42, x40, x38, (x51, x52, x50, x48, x46)))%core,
@@ -367,4 +367,4 @@ let (a, b) := Interp-η
(let (a0, b0) := a in
(a0, b0), let (a0, b0) := b in
(a0, b0))%core
- : ReificationTypes.feW → ReificationTypes.feW → ReificationTypes.feW → ReificationTypes.feW → ReificationTypes.feW → ReificationTypes.feW * ReificationTypes.feW * (ReificationTypes.feW * ReificationTypes.feW)
+ : ReificationTypes.RP.feW → ReificationTypes.RP.feW → ReificationTypes.RP.feW → ReificationTypes.RP.feW → ReificationTypes.RP.feW → ReificationTypes.RP.feW * ReificationTypes.RP.feW * (ReificationTypes.RP.feW * ReificationTypes.RP.feW)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 02:30:40 +0000