| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Initial work
* Respond to code review comments
* Add x25519_32, commented out for speed
* Remove outdated comment
* Add another unfolding thing to make 2^127-1 with (_ + 1/3)%Q work
* Use vm_compute in one place where it's faster
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
removing lemma wordToNat_wzero is ok because it's already in bbv
|
| | |
|
| |
|
|
| |
This allows us to remove some manual unfolding
|
| | |
|
| |
|
|
|
|
|
|
| |
Rather than always inline, we now introduce one let-bound node per
non-var list element.
Not sure this is the right thing to do, so maybe we should revert this
commit.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Needed for carry
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
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).
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
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?
|
Jason Gross
Jason Gross
Samuel Gruetter
Andres Erbsen
Andres Erbsen
David Benjamin