aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Fix no-curves-proofs-non-specific targetGravatar Jason Gross2018-02-11
| | | | Previously the vo_reverse_closure logic was not working correctly
* Add notation for option_bindGravatar Jason Gross2018-02-10
|
* Split off ZRange lemmasGravatar Jason Gross2018-02-10
|
* Support older git ls-filesGravatar Jason Gross2018-02-10
| | | | The older ones don't have --recurse-submodules
* Add some ZRange operationsGravatar Jason Gross2018-02-10
|
* make bbv submodule URL relative to origin, so thatGravatar Samuel Gruetter2018-02-05
| | | | developers will clone the submodule via ssh, while travis will clone it via https
* switch to public bbvGravatar Samuel Gruetter2018-02-05
|
* minor updates needed to make it compile with bbvGravatar Samuel Gruetter2018-02-05
| | | | removing lemma wordToNat_wzero is ok because it's already in bbv
* add bedrock bit vectors library (bbv) as a submodule replacing the Bedrock ↵Gravatar Samuel Gruetter2018-02-05
| | | | directory
* Work around travis bugsGravatar Jason Gross2018-01-29
| | | | | | | https://github.com/travis-ci/travis-ci/issues/8507 We use a script and travis_retry to work around "failed to fetch" with launchpad
* Add dead code elimination via inliningGravatar Jason Gross2018-01-29
|
* Have reification run delta on unknown identsGravatar Jason Gross2018-01-29
| | | | This allows us to remove some manual unfolding
* Remove useless dletGravatar Jason Gross2018-01-29
|
* Change reduction behavior of let-bound listsGravatar Jason Gross2018-01-29
| | | | | | | | 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.
* Use Derive plugin, do two passes of partial reductionGravatar Jason Gross2018-01-29
|
* rerunGravatar Andres Erbsen2018-01-29
|
* fix carry chain in exampleGravatar Andres Erbsen2018-01-29
|
* Respond to some CR commentsGravatar Jason Gross2018-01-29
|
* Don't reify [let ... in ...], only [dlet ... in ...]Gravatar Jason Gross2018-01-29
|
* Write ltamer-based CPS transformGravatar Jason Gross2018-01-29
|
* Fix weight to use 51-bit limbsGravatar Jason Gross2018-01-29
|
* Remove use of beta in reification of Let_InGravatar Jason Gross2018-01-29
|
* Rename type.opaque to type.primitiveGravatar Jason Gross2018-01-29
|
* remove outdated commentGravatar Jason Gross2018-01-29
|
* Get cps for carry workingGravatar Jason Gross2018-01-29
|
* Support Let_in with not-fully-reduced second arg in reificationGravatar Jason Gross2018-01-29
| | | | Needed for carry
* More types in type_opaque; restore nth_default notationGravatar Jason Gross2018-01-29
|
* Remove dead codeGravatar Jason Gross2018-01-29
|
* Add a CPS conversion passGravatar Jason Gross2018-01-29
|
* make SimplyTypedArithmetic less "Smart" by giving every expression a normal formGravatar Andres Erbsen2018-01-29
|
* Fix naming partial.interp -> partial.valueGravatar Jason Gross2018-01-29
|
* [demo] Add a list rec canonicalization passGravatar Jason Gross2018-01-29
|
* Revert "Remove the series of Let statements in favor of a fixpoint"Gravatar Jason Gross2018-01-29
| | | | This reverts commit 0687a75d075d37ab36ef06b5f3228df801bd80e7.
* Shorter return statements by using notationsGravatar Jason Gross2018-01-29
|
* Remove the series of Let statements in favor of a fixpointGravatar Jason Gross2018-01-29
|
* Add a reference to a Coq issueGravatar Jason Gross2018-01-29
|
* Update some names in accordance with review commentsGravatar Jason Gross2018-01-29
|
* Remove dead code in commentsGravatar Jason Gross2018-01-29
|
* Finish first working version of partial reductionGravatar Jason Gross2018-01-29
| | | | | | 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.
* Partial work on fixing partial reductionGravatar Jason Gross2018-01-29
| | | | | | | | | | | | | | | | | | | | | | | | | | 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....
* Partial work on implementing partial reductionGravatar Jason Gross2018-01-29
|
* Pass -mbmi2 to gccGravatar Jason Gross2018-01-19
| | | | | This will hopefully fix the issue where travis gcc complains about not being able to inline mulx. I hope.
* Add better levels / printing for bind notationsGravatar Jason Gross2018-01-16
|
* Attempt to build travis in stagesGravatar Jason Gross2018-01-16
| | | | | | | | | | | | 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.
* Add separate targets to build but not run test/benchGravatar Jason Gross2018-01-16
|
* [travis] 8.7.0 -> 8.7.1Gravatar Jason Gross2018-01-15
|
* Fix liblow.h for cmovznz64Gravatar Jason Gross2018-01-15
|
* Update cmovznz to cmovznz64 in the .c fileGravatar Jason Gross2018-01-15
|
* Add .c and .log filesGravatar Jason Gross2018-01-15
|
* Add x25519 donna versions with the new way of generating C codeGravatar Jason Gross2018-01-15
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 00:35:42 +0000