| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| |
|
|
| |
This reverts commit 0687a75d075d37ab36ef06b5f3228df801bd80e7.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
The names are terrible and the code organization isn't great, and I
don't like the long list of [Let] statements which are morally doing
very similar things, but, it works.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
I've mostly fused partial_reduce' with arguments.expr.interp. This
fixes some things, but it doesn't fix everything. In particular, the
algorithm is set up incorrectly to run in a single pass. I think the
correct fusing treats the [arguments] metadata as something like
types-in-bidirectional-typechecking. That is, we need to drive the
evalutation by expected [arguments], except at operation nodes, where
we feed the expected output [arguments] to the rewriter and it tells us
what sort of [arguments] we need to use to drive the partial evaluation
of the op-arguments.
Arrows are kind-of wonky, though. What's the right argument annotation
for something like [@List.map A B]? The simplest thing is [λ '(list b),
(A -> b) * list A], i.e., if you want it to produce [list b] for some
description [b], you need to give it a function from a generic
expression for [A] to a thing with as much info as is in [b], and you
need to give it a list of generic [A]s. But that's not accurate,
because it actually works fine for any consistent detail on [A]. So we
want something like [λ '(list b), ∃ a, (a -> b) * list a], but I don't
know how to express that. This is where we do want something like
bidirectional typechecking: we drive the evaluation of [List.map f x] by
the description [list b] of the output. Then we drive the evaluation of
[f] with the description [?a -> b], and we want to get out [?a]. Not
sure how this all fits together though....
|
| | |
|
| |
|
|
|
| |
This will hopefully fix the issue where travis gcc complains about not
being able to inline mulx. I hope.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Hopefully this will lead to overall faster builds
Also:
- try to allow failures
- Version-specific vo caches
- Make archives stage-specific
This way, if multiple branches are running stages at the same time, they
don't have as much a chance of clobbering each others builds.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
This required tending to montladder not being proved Feq-preserving
(sidestepped by proving for all P = 0), and then some wrestling with
scalarmult to show the right-hand side was indeed zero when x is (0, 0).
|
| | |
|
| |
|
|
| |
https://github.com/travis-ci/travis-ci/issues/8507
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
This is a one-line change in generate_parameters.py (plus some
whitespace trimming), and running `make regenerate-curves`
This handles part of #294
|
| |
|
|
|
|
|
|
|
| |
After | File Name | Before || Change | % Change
-------------------------------------------------------------------------
1m11.42s | Total | 1m53.75s || -0m42.33s | -37.21%
-------------------------------------------------------------------------
1m06.02s | Curves/Weierstrass/Jacobian | 1m53.76s || -0m47.73s | -41.96%
0m05.40s | Util/FsatzAutoLemmas | N/A || +0m05.40s | ∞
|
| |
|
|
| |
We no longer seem to need the stronger hypothesis.
|
| |
|
|
|
|
|
|
| |
After | File Name | Before || Change | % Change
---------------------------------------------------------------------------
1m52.31s | Total | 13m36.75s || -11m44.44s | -86.24%
---------------------------------------------------------------------------
1m52.31s | Curves/Weierstrass/Jacobian | 13m36.75s || -11m44.44s | -86.24%
|
| |
|
|
|
|
| |
This reverts commit d33d8be154dbce048ac10d82bc0b39468abd5fdb.
Hmm, apparently there's an error on Qed... maybe a bug in fsatz?
|
| |
|
|
| |
We no longer seem to need the stronger hypothesis.
|
| | |
|
| | |
|
| |
|
|
|
| |
We have about 15 minutes to spare on the curves-proofs travis job, so we
move Jacobian.vo from no-curves-proofs-non-specific to there.
|
| | |
|
| | |
|
| |
|
|
|
| |
Also refresh things after PR#289. This too just updated the comments, as
expected.
|
| | |
|
| | |
|
| |
|
|
|
| |
Refresh things after PR#289, though that just updated the comments, as
expected.
|
| |
|
|
|
|
|
| |
This notation system is fragile and kludgy.
This discovered from @davidben's
https://github.com/mit-plv/fiat-crypto/pull/289/commits/ff0fb38346dde67abef982d6305595216d18519b#r159793723
|
| |
|
|
|
| |
We do this by adding notations for addcarryx and subborrow for all of
the smaller-than-max-bitwidth sizes of arguments.
|
| |
|
|
| |
This handles bullet 3 of #288
|
| |
|
|
| |
This handles bullet point 1 of #288
|
| |
|
|
| |
This handles bullet 2 of #288
|
| |
|
|
| |
This handles bullet 2 of #288
|
| |
|
|
|
|
|
|
|
|
|
| |
This closes #286
This is actually a +1,-1 diff in the python script generating the
notations, plus running it and rebuilding:
```diff
-ADD_CARRY_SUB_BORROW_SIZES = (32, 64, 128, 51)
+ADD_CARRY_SUB_BORROW_SIZES = (32, 64, 128, 25, 26, 51)
```
|
| |
|
|
|
|
| |
This makes it easier to add support for more kinds of addcarryx, etc,
and also add `: expr_scope` to work around changes from
https://github.com/coq/coq/pull/873
|
| | |
|
| | |
|
Jason Gross
David Benjamin
Andres Erbsen
Andres Erbsen