diff options
Diffstat (limited to 'src/Specific/X25519/C64/ReificationTypes.v')
-rw-r--r-- | src/Specific/X25519/C64/ReificationTypes.v | 62 |
1 files changed, 8 insertions, 54 deletions
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. |