| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | |
|
| | |
|
| |
|
|
|
|
|
| |
Some of the sizes were too small because python3 generates floats on
division, while python2 rounds down.
Also add better error handling
|
| | |
|
| | |
|
| |
|
|
|
| |
Now there's a version that handles things in Saturated.Core, and in
Wrappers.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
This way, we can reuse it even when we can't fully compute the values
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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_chains" : "default",
"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_chains" : "default",
"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 ));
"
}
```
|
| | |
|
| | |
|
| |
|
|
| |
I'm very confused about how and when it was introduced...
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
This makes it easier to extend the bounds analysis framework.
|
| |
|
|
|
| |
Hopefully this will help with extending the framework. Also remove
[t_map4]; it was unused and didn't match the types of the other [t_mapn]s.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
| |
We now only build selected-test and selected-bench with one version of
Coq (picked 8.7+beta2, because hopefully it'll be faster than 8.6.1).
Previously, some travis builds failed because some travis machines don't
support adc, adcx, mulx, etc.
|
| |
|
|
| |
Also hopefully fix travis
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
Travis was too slow to run all of the coq target, so we split off the
no-curves-proofs and the curves-proofs targets, and, while we're at it,
also add 8.7+beta1 tests.
|
| | |
|
| | |
|
| |
|
|
|
| |
List of dynamically-typed key-value pairs, and some helper definitions
and tactics.
|
| | |
|
| | |
|
| |
|
|
| |
Previously, it was splitting on : and adding extra paths with, e.g., c:/
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
After | File Name | Before || Change
-----------------------------------------------------------------------
3m56.20s | Total | 4m14.86s || -0m18.66s
-----------------------------------------------------------------------
0m02.44s | Specific/X25519/C32/ReificationTypes | 0m19.48s || -0m17.03s
2m00.12s | Specific/X25519/C64/ladderstep | 1m55.72s || +0m04.40s
0m01.16s | Specific/X25519/C64/ReificationTypes | 0m05.17s || -0m04.00s
0m26.27s | Specific/X25519/C32/fesquare | 0m27.76s || -0m01.49s
0m52.60s | Specific/X25519/C32/femul | 0m52.46s || +0m00.14s
0m10.35s | Specific/X25519/C64/femul | 0m10.28s || +0m00.07s
0m08.30s | Specific/IntegrationTestSub | 0m08.69s || -0m00.38s
0m07.97s | Specific/IntegrationTestFreeze | 0m08.00s || -0m00.03s
0m06.99s | Specific/X25519/C64/fesquare | 0m07.31s || -0m00.31s
|
| |
|
|
| |
This will let us call it from Ltac; notations with tactics don't internalize identifiers correctly at tactic definition time
|
Jason Gross
jadep