aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments
Commit message (Expand)AuthorAge
* Add dead code elimination via inliningGravatar Jason Gross2018-01-29
* Have reification run delta on unknown identsGravatar Jason Gross2018-01-29
* Remove useless dletGravatar Jason Gross2018-01-29
* Change reduction behavior of let-bound listsGravatar Jason Gross2018-01-29
* 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
* 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
* 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
* Partial work on fixing partial reductionGravatar Jason Gross2018-01-29
* Partial work on implementing partial reductionGravatar Jason Gross2018-01-29
* Montgomery.XZ, Loops: montladder proof scaffoldingGravatar Andres Erbsen2017-12-22
* add non-cps version of chained_carries (resolves #283 again)Gravatar jadep2017-12-14
* add non-cps carry to experimental pipeline (this resolves #283)Gravatar jadep2017-12-14
* Loops (trying again) (#259)Gravatar Andres Erbsen2017-12-11
* [demo] Add reification in src/Experiments/SimplyTypedArithmetic.v (#275)Gravatar Jason Gross2017-11-26
* [demo] Replace (max (length a) (length b)) with explicit nat argGravatar Jason Gross2017-11-24
* [Demo] Define [place] in terms of nat_rectGravatar Jason Gross2017-11-24
* [demo] Use [List.repeat] rather than [List.map]Gravatar Jason Gross2017-11-24
* [demo] Pass in a [nat] for list lengthGravatar Jason Gross2017-11-24
* Remove tuple from src/DemoWithReification.vGravatar Jason Gross2017-11-24
* Move DemoWithReification.v => Experiments/SimplyTypedArithmetic.vGravatar Jason Gross2017-11-24
* automate some proofs; also remove trace-based reasoning in favor of induction...Gravatar jadep2017-10-26
* invariants don't need to know the fuelGravatar jadep2017-10-26
* WIP: loopsGravatar jadep2017-10-26
* remove unused filesGravatar Andres Erbsen2017-04-06
* Add [Proof using] to most proofsGravatar Jason Gross2017-04-04
* More fine-grained tactic importsGravatar Jason Gross2017-04-03
* Remove everything after the individual reified opsGravatar Jason Gross2017-04-03
* remove undeclared lines from Ed25519Extraction.vGravatar Andres Erbsen2017-03-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 20:01:25 +0000