diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Specific/ReificationTypes.v | 201 | ||||
-rw-r--r-- | src/Specific/X25519/C32/ArithmeticSynthesisTest.v | 2 | ||||
-rw-r--r-- | src/Specific/X25519/C32/ReificationTypes.v | 62 | ||||
-rw-r--r-- | src/Specific/X25519/C64/ArithmeticSynthesisTest.v | 2 | ||||
-rw-r--r-- | src/Specific/X25519/C64/ReificationTypes.v | 62 | ||||
-rw-r--r-- | src/Specific/X25519/C64/ladderstepDisplay.log | 4 |
6 files changed, 223 insertions, 110 deletions
diff --git a/src/Specific/ReificationTypes.v b/src/Specific/ReificationTypes.v new file mode 100644 index 000000000..cc705689b --- /dev/null +++ b/src/Specific/ReificationTypes.v @@ -0,0 +1,201 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.romega.ROmega. +Require Import Coq.micromega.Lia. +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.Util.Decidable. + +Require Import Crypto.Util.Tactics.PoseTermWithName. +Require Import Crypto.Util.Tactics.CacheTerm. + +Ltac pose_limb_widths wt sz limb_widths := + pose_term_with + ltac:(fun _ => (eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 sz)))) + limb_widths. + +Ltac get_b_of upper_bound_of_exponent := + constr:(fun exp => {| lower := 0 ; upper := upper_bound_of_exponent exp |}%Z). (* 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. *) +Ltac pose_bounds_exp sz limb_widths bounds_exp := + pose_term_with_type + (Tuple.tuple Z sz) + ltac:(fun _ => eval compute in + (Tuple.from_list sz limb_widths eq_refl)) + bounds_exp. + +Ltac pose_bounds sz b_of bounds_exp bounds := + pose_term_with_type + (Tuple.tuple zrange sz) + ltac:(fun _ => eval compute in + (Tuple.map (fun e => b_of e) bounds_exp)) + bounds. + +Ltac pose_lgbitwidth limb_widths lgbitwidth := + pose_term_with + ltac:(fun _ => eval compute in (Z.to_nat (Z.log2_up (List.fold_right Z.max 0 limb_widths)))) + lgbitwidth. + +Ltac pose_bitwidth lgbitwidth bitwidth := + pose_term_with + ltac:(fun _ => eval compute in (2^lgbitwidth)%nat) + bitwidth. + +Ltac pose_feZ sz feZ := + pose_term_with + ltac:(fun _ => constr:(tuple Z sz)) + feZ. + +Ltac pose_feW sz lgbitwidth feW := + cache_term_with_type_by + Type + ltac:(let v := eval cbv [lgbitwidth] in (tuple (wordT lgbitwidth) sz) in exact v) + feW. +Ltac pose_feW_bounded feW bounds feW_bounded := + cache_term_with_type_by + (feW -> Prop) + ltac:(let v := eval cbv [bounds] in (fun w : feW => is_bounded_by None bounds (map wordToZ w)) in exact_no_check v) + feW_bounded. +Ltac pose_feBW sz bitwidth bounds feBW := + cache_term_with_type_by + Type + ltac:(let v := eval cbv [bitwidth bounds] in (BoundedWord sz bitwidth bounds) in exact v) + feBW. + +Lemma feBW_bounded_helper' + sz bitwidth bounds + (feBW := BoundedWord sz bitwidth bounds) + (wt : nat -> Z) + (Hwt : forall i, 0 <= wt i) + : forall (a : feBW), + B.Positional.eval wt (map lower bounds) + <= B.Positional.eval wt (BoundedWordToZ sz bitwidth bounds a) + <= B.Positional.eval wt (map upper bounds). +Proof. + let a := fresh "a" in + intro a; + destruct a as [a H]; unfold BoundedWordToZ, proj1_sig. + destruct sz as [|sz]. + { cbv -[Z.le Z.lt Z.mul]; lia. } + { cbn [tuple map] in *. + revert dependent wt; induction sz as [|sz IHsz]; intros. + { cbv -[Z.le Z.lt wordToZ Z.mul Z.pow Z.add lower upper Nat.log2 wordT] in *. + repeat match goal with + | [ |- context[@wordToZ ?n ?x] ] + => generalize dependent (@wordToZ n x); intros + | [ H : forall j, 0 <= wt j |- context[wt ?i] ] + => pose proof (H i); generalize dependent (wt i); intros + end. + nia. } + { pose proof (Hwt 0%nat). + cbn [tuple' map'] in *. + destruct a as [a' a], bounds as [bounds b], H as [H [H' _]]. + cbn [fst snd] in *. + setoid_rewrite (@B.Positional.eval_step (S _)). + specialize (IHsz bounds a' H (fun i => wt (S i)) (fun i => Hwt _)). + nia. } } +Qed. +Lemma feBW_bounded_helper + sz bitwidth bounds + (feBW := BoundedWord sz bitwidth bounds) + (wt : nat -> Z) + (Hwt : forall i, 0 <= wt i) + l u + : l <= B.Positional.eval wt (map lower bounds) + /\ B.Positional.eval wt (map upper bounds) < u + -> forall (a : feBW), + l <= B.Positional.eval wt (BoundedWordToZ sz bitwidth bounds a) < u. +Proof. + intros [Hl Hu] a; split; + [ eapply Z.le_trans | eapply Z.le_lt_trans ]; + [ | eapply feBW_bounded_helper' | eapply feBW_bounded_helper' | ]; + assumption. +Qed. + +Ltac pose_feBW_bounded wt sz feBW bitwidth bounds m wt_nonneg feBW_bounded := + cache_proof_with_type_by + (forall a : feBW, 0 <= B.Positional.eval wt (BoundedWordToZ sz bitwidth bounds a) < 2 * Z.pos m) + ltac:(apply (@feBW_bounded_helper sz bitwidth bounds wt wt_nonneg); + vm_compute; clear; split; congruence) + feBW_bounded. + +Ltac pose_phiW feW m wt phiW := + cache_term_with_type_by + (feW -> F m) + ltac:(exact (fun x : feW => B.Positional.Fdecode wt (Tuple.map wordToZ x))) + phiW. +Ltac pose_phiBW feBW m wt phiBW := + cache_term_with_type_by + (feBW -> F m) + ltac:(exact (fun x : feBW => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x))) + phiBW. + +Ltac get_ReificationTypes_package wt sz bounds m wt_nonneg upper_bound_of_exponent := + let limb_widths := fresh "limb_widths" in + let bounds_exp := fresh "bounds_exp" in + let bounds := fresh "bounds" in + let lgbitwidth := fresh "lgbitwidth" in + let bitwidth := fresh "bitwidth" in + let feZ := fresh "feZ" in + let feW := fresh "feW" in + let feW_bounded := fresh "feW_bounded" in + let feBW := fresh "feBW" in + let feBW_bounded := fresh "feBW_bounded" in + let phiW := fresh "phiW" in + let phiBW := fresh "phiBW" in + let limb_widths := pose_limb_widths wt sz limb_widths in + let b_of := get_b_of upper_bound_of_exponent in + let bounds_exp := pose_bounds_exp sz limb_widths bounds_exp in + let bounds := pose_bounds sz b_of bounds_exp bounds in + let lgbitwidth := pose_lgbitwidth limb_widths lgbitwidth in + let bitwidth := pose_bitwidth lgbitwidth bitwidth in + let feZ := pose_feZ sz feZ in + let feW := pose_feW sz lgbitwidth feW in + let feW_bounded := pose_feW_bounded feW bounds feW_bounded in + let feBW := pose_feBW sz bitwidth bounds feBW in + let feBW_bounded := pose_feBW_bounded wt sz feBW bitwidth bounds m wt_nonneg feBW_bounded in + let phiW := pose_phiW feW m wt phiW in + let phiBW := pose_phiBW feBW m wt phiBW in + constr:((feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW)). +Ltac make_ReificationTypes_package wt sz bounds m wt_nonneg upper_bound_of_exponent := + lazymatch goal with + | [ |- { T : _ & T } ] => eexists + | [ |- _ ] => idtac + end; + let pkg := get_ReificationTypes_package wt sz bounds m wt_nonneg upper_bound_of_exponent in + exact pkg. + +Module Type ReificationTypesPrePackage. + Parameter ReificationTypes_package' : { T : _ & T }. + Parameter ReificationTypes_package : projT1 ReificationTypes_package'. +End ReificationTypesPrePackage. + +Module MakeReificationTypes (RP : ReificationTypesPrePackage). + Definition ReificationTypes_package := RP.ReificationTypes_package. + Ltac reduce_proj x := + let RP_ReificationTypes_package := (eval cbv [ReificationTypes_package] in ReificationTypes_package) in + let v := (eval cbv [ReificationTypes_package RP_ReificationTypes_package] in x) in + exact v. + (** +<< +terms = 'feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW' +for i in terms.split(', '): + print(" Notation %s := (ltac:(reduce_proj (let '(%s) := ReificationTypes_package in %s))) (only parsing)." % (i, terms, i)) +>> *) + Notation feZ := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in feZ))) (only parsing). + Notation feW := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in feW))) (only parsing). + Notation feW_bounded := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in feW_bounded))) (only parsing). + Notation feBW := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in feBW))) (only parsing). + Notation feBW_bounded := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in feBW_bounded))) (only parsing). + Notation phiW := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in phiW))) (only parsing). + Notation phiBW := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in phiBW))) (only parsing). +End MakeReificationTypes. 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) |