diff options
author | Jason Gross <jgross@mit.edu> | 2017-10-06 01:50:59 -0400 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2017-10-18 23:01:29 -0400 |
commit | 28359fcb5be530da65d5049846927a84a880b919 (patch) | |
tree | 8f0d8b6fc8ea4f109a9540c35869fd1d2adf759e /src/Specific/IntegrationTestLadderstep130.v | |
parent | a3a6eb12e7652e40b573372217f0771368ad50cb (diff) |
Build curve-specific files from json
The X25519 curves are now generated from `.json` files. This code
only works in >= 8.7, because it makes use of the
recently-merged-from-fiat `transparent_abstract` tactic to allow
defining things in tactics without massive slowdown. The structure is
as follows:
0. The module types and tactic definitions that set up the
infrastructure live in `src/Specific/Framework/`
1. There are `.json` files in `src/Specific/CurveParameters/` that
specify curve characteristics. A simple example is `x2555_130.json`,
which is:
```json
{
"modulus" : "2^255-5",
"base" : "130",
"a24" : "121665 (* XXX TODO(andreser) FIXME? Is this right for this curve? *)",
"sz" : "3",
"bitwidth" : "128",
"carry_chain1" : "default",
"carry_chain2" : ["0", "1"],
"coef_div_modulus" : "2",
"operations" : ["ladderstep"]
}
```
A more complicated example is `x25519_c64.json`:
```json
{
"modulus" : "2^255-19",
"base" : "51",
"a24" : "121665",
"sz" : "5",
"bitwidth" : "64",
"carry_chain1" : "default",
"carry_chain2" : ["0", "1"],
"coef_div_modulus" : "2",
"operations" : ["femul", "fesquare", "freeze", "ladderstep"],
"extra_files" : ["X25519_C64/scalarmult.c"],
"compiler" : "gcc -march=native -mtune=native -std=gnu11 -O3 -flto -fomit-frame-pointer -fwrapv -Wno-attributes",
"mul_header" : "(* Micro-optimized form from curve25519-donna-c64 by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)",
"mul_code"
:
"
uint128_t t[5];
limb r0,r1,r2,r3,r4,s0,s1,s2,s3,s4,c;
r0 = in[0];
r1 = in[1];
r2 = in[2];
r3 = in[3];
r4 = in[4];
s0 = in2[0];
s1 = in2[1];
s2 = in2[2];
s3 = in2[3];
s4 = in2[4];
t[0] = ((uint128_t) r0) * s0;
t[1] = ((uint128_t) r0) * s1 + ((uint128_t) r1) * s0;
t[2] = ((uint128_t) r0) * s2 + ((uint128_t) r2) * s0 + ((uint128_t) r1) * s1;
t[3] = ((uint128_t) r0) * s3 + ((uint128_t) r3) * s0 + ((uint128_t) r1) * s2 + ((uint128_t) r2) * s1;
t[4] = ((uint128_t) r0) * s4 + ((uint128_t) r4) * s0 + ((uint128_t) r3) * s1 + ((uint128_t) r1) * s3 + ((uint128_t) r2) * s2;
r4 *= 19;
r1 *= 19;
r2 *= 19;
r3 *= 19;
t[0] += ((uint128_t) r4) * s1 + ((uint128_t) r1) * s4 + ((uint128_t) r2) * s3 + ((uint128_t) r3) * s2;
t[1] += ((uint128_t) r4) * s2 + ((uint128_t) r2) * s4 + ((uint128_t) r3) * s3;
t[2] += ((uint128_t) r4) * s3 + ((uint128_t) r3) * s4;
t[3] += ((uint128_t) r4) * s4;
",
"square_header" : "(* Micro-optimized form from curve25519-donna-c64 by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *)",
"square_code"
:
"
uint128_t t[5];
limb r0,r1,r2,r3,r4,c;
limb d0,d1,d2,d4,d419;
r0 = in[0];
r1 = in[1];
r2 = in[2];
r3 = in[3];
r4 = in[4];
do {
d0 = r0 * 2;
d1 = r1 * 2;
d2 = r2 * 2 * 19;
d419 = r4 * 19;
d4 = d419 * 2;
t[0] = ((uint128_t) r0) * r0 + ((uint128_t) d4) * r1 + (((uint128_t) d2) * (r3 ));
t[1] = ((uint128_t) d0) * r1 + ((uint128_t) d4) * r2 + (((uint128_t) r3) * (r3 * 19));
t[2] = ((uint128_t) d0) * r2 + ((uint128_t) r1) * r1 + (((uint128_t) d4) * (r3 ));
t[3] = ((uint128_t) d0) * r3 + ((uint128_t) d1) * r2 + (((uint128_t) r4) * (d419 ));
t[4] = ((uint128_t) d0) * r4 + ((uint128_t) d1) * r3 + (((uint128_t) r2) * (r2 ));
"
}
```
3. The `src/Specific/CurveParameters/remake_curves.sh` script holds a
list of curves to be made, what directories they should end up living
in, and it invokes `src/Specific/Framework/make_curve.py` to transform
these files into outputs. The Python script fills in a few defaults
(such as computing `s` and `c` from the modulus, if you don't pass
them explicitly), and does a lot of processing on the C code that is
pasted verbatim from donna to get it to be in the right format for
Coq.
This Python script creates the files:
- `CurveParameters.v` (the Coq-ified version of the json file, which
instantiates an appropriate module type);
- `Synthesis.v`, which instantiates a `MakeSynthesisTactics` with the
curve parameter modules, invokes a tactic from the applied module
functor to synthesize all of the relevant non-reflective bits
(basically, what used to live in @jadephilipoom 's
`ArithmeticSynthesisTest.v`), and then instantiates another module
functor `PackageSynthesis` which defines notations via tactics in
terms to access the names of the various fields defined by the
synthesis tactic;
- any other files you ask it for, such as `compiler.sh`, `femul.v`,
`femulDisplay.v`. All of the `*Display.v` files are simple, and all
the the operation synthesis files have a single `Definition` (with the
appropriate type), and solve the definition by invoking a single
tactic defined in `PackageSynthesis`, e.g., `synthesize_mul` or
`synthesize_ladderstep`.
Diffstat (limited to 'src/Specific/IntegrationTestLadderstep130.v')
-rw-r--r-- | src/Specific/IntegrationTestLadderstep130.v | 131 |
1 files changed, 0 insertions, 131 deletions
diff --git a/src/Specific/IntegrationTestLadderstep130.v b/src/Specific/IntegrationTestLadderstep130.v deleted file mode 100644 index aba794f4b..000000000 --- a/src/Specific/IntegrationTestLadderstep130.v +++ /dev/null @@ -1,131 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Coq.Lists.List. -Require Import Coq.Classes.Morphisms. -Local Open Scope Z_scope. - -Require Import Crypto.Arithmetic.Core. -Require Import Crypto.Util.FixedWordSizes. -Require Import Crypto.Specific.ArithmeticSynthesisTest130. -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord. -Require Import Crypto.Util.LetIn. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Tactics.MoveLetIn. -Require Import Crypto.Util.Tactics.SetEvars. -Require Import Crypto.Util.Tactics.SubstEvars. -Require Import Crypto.Curves.Montgomery.XZ. -Import ListNotations. - -Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. - -Require Import Crypto.Compilers.Z.Bounds.Pipeline. - -Section BoundedField25p5. - 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 := 2^exp + 2^(exp-3) |}%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 - := Eval compute in - Tuple.from_list length_lw limb_widths eq_refl. - Let bounds : Tuple.tuple zrange length_lw - := 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. - Let feW : Type := tuple (wordT lgbitwidth) sz. - Let feW_bounded : feW -> Prop - := fun w => is_bounded_by None bounds (map wordToZ w). - Let feBW : Type := BoundedWord sz bitwidth bounds. - Let phi : feW -> F m := - fun x => B.Positional.Fdecode wt (Tuple.map wordToZ x). - - (** TODO(jadep,andreser): Move to NewBaseSystemTest? *) - Definition FMxzladderstep := @M.xzladderstep (F m) F.add F.sub F.mul. - - (** TODO(jadep,andreser): Move to NewBaseSystemTest? *) - Definition Mxzladderstep_sig - : { xzladderstep : tuple Z sz -> tuple Z sz -> tuple Z sz * tuple Z sz -> tuple Z sz * tuple Z sz -> tuple Z sz * tuple Z sz * (tuple Z sz * tuple Z sz) - | forall a24 x1 Q Q', let eval := B.Positional.Fdecode wt in Tuple.map (n:=2) (Tuple.map (n:=2) eval) (xzladderstep a24 x1 Q Q') = FMxzladderstep (eval a24) (eval x1) (Tuple.map (n:=2) eval Q) (Tuple.map (n:=2) eval Q') }. - Proof. - exists (@M.xzladderstep _ (proj1_sig add_sig) (proj1_sig sub_sig) (fun x y => proj1_sig carry_sig (proj1_sig mul_sig x y))). - intros a24 x1 Q Q' eval. - cbv [FMxzladderstep M.xzladderstep]. - destruct Q, Q'; cbv [map map' fst snd Let_In eval]. - repeat rewrite ?(proj2_sig add_sig), ?(proj2_sig mul_sig), ?(proj2_sig sub_sig), ?(proj2_sig carry_sig). - reflexivity. - Defined. - - (* TODO : change this to field once field isomorphism happens *) - Definition xzladderstep : - { xzladderstep : feW -> feW * feW -> feW * feW -> feW * feW * (feW * feW) - | forall x1 Q Q', - let xz := xzladderstep x1 Q Q' in - let eval := B.Positional.Fdecode wt in - feW_bounded x1 - -> feW_bounded (fst Q) /\ feW_bounded (snd Q) - -> 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') }. - Proof. - apply_lift_sig. - intros a b c; cbv beta iota zeta. - lazymatch goal with - | [ |- { e | ?A -> ?B -> ?C -> @?E e } ] - => refine (proj2_sig_map (P:=fun e => A -> B -> C -> (_:Prop)) _ _) - end. - { intros ? FINAL. - repeat let H := fresh in intro H; specialize (FINAL H). - cbv [phi]. - split; [ refine (proj1 FINAL); shelve | ]. - do 4 match goal with - | [ |- context[Tuple.map (n:=?N) (fun x : ?T => ?f (?g x))] ] - => rewrite <- (Tuple.map_map (n:=N) f g - : pointwise_relation _ eq _ (Tuple.map (n:=N) (fun x : T => f (g x)))) - end. - rewrite <- (proj2_sig Mxzladderstep_sig). - apply f_equal. - cbv [proj1_sig]; cbv [Mxzladderstep_sig]. - context_to_dlet_in_rhs (@M.xzladderstep _ _ _ _ _). - cbv [M.xzladderstep a24_sig]. - repeat lazymatch goal with - | [ |- context[@proj1_sig ?a ?b ?f_sig _] ] - => context_to_dlet_in_rhs (@proj1_sig a b f_sig) - end. - cbv beta iota delta [proj1_sig mul_sig add_sig sub_sig carry_sig]. - cbv_runtime. - refine (proj2 FINAL). } - subst feW feW_bounded; cbv beta. - (* jgross start here! *) - Set Ltac Profiling. - (* - Time Glue.refine_to_reflective_glue (128::256::nil)%nat%list. - Time ReflectiveTactics.refine_with_pipeline_correct default. - { Time ReflectiveTactics.do_reify. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_rhs_reflexivity. } - { Time ReflectiveTactics.unify_abstract_renamify_rhs_reflexivity. } - { Time SubstLet.subst_let; clear; abstract vm_cast_no_check (eq_refl true). } - { Time SubstLet.subst_let; clear; vm_compute; reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_compute_rhs_reflexivity. } - { Time ReflectiveTactics.unify_abstract_cbv_interp_rhs_reflexivity. } - { Time abstract ReflectiveTactics.handle_bounds_from_hyps. } - *) - Time refine_reflectively128. - Show Ltac Profile. - Time Defined. - -Time End BoundedField25p5. |