aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAge
* Inline weight into *mod, remove rweightGravatar Jason Gross2018-03-28
|
* Move mod_ops out of PositionalGravatar Jason Gross2018-03-28
|
* Move cps out of cache part of the pipelineGravatar Jason Gross2018-03-27
| | | | | | | | | | Most of the changes are due to the fact that the PrePipeline (cache) part no longer errors, and the pre-check post-cache part of the pipeline can now error. Note that this slows rcarry_mul down from about 0.3 s to about 2.6 s (some of which is probably counter-balanced by the fact that caching is probably now faster).
* Add Zdiv_0_l to zsimplify dbsGravatar Jason Gross2018-03-27
|
* Add a test for hd and tlGravatar Jason Gross2018-03-27
|
* Add support for handling match on listGravatar Jason Gross2018-03-27
| | | | | | As per https://github.com/mit-plv/fiat-crypto/pull/334/files#r177112883 Currently untested
* Add list_case, a definition for match on listGravatar Jason Gross2018-03-27
|
* Response to code review commentGravatar Jason Gross2018-03-23
| | | | https://github.com/mit-plv/fiat-crypto/pull/330#discussion_r176406316
* Be more explicit about reductionGravatar Jason Gross2018-03-23
| | | | | We were using `lazy` to substitute an evar context variable when the right hand side was `Pipeline.Success rv`; now we use `subst_evars`.
* s/nobrainer1/subst01/Gravatar Jason Gross2018-03-23
| | | | | As per https://github.com/mit-plv/fiat-crypto/pull/332#discussion_r176415846
* Remove spurious indentationGravatar Jason Gross2018-03-23
|
* Added input var type for clarityGravatar Jason Gross2018-03-23
| | | | As per https://github.com/mit-plv/fiat-crypto/pull/332/files#r176417396
* Make the ERROR definition opaque to vm_computeGravatar Jason Gross2018-03-23
|
* Add GeneralizeVar explanatory commentGravatar Jason Gross2018-03-23
| | | | As per https://github.com/mit-plv/fiat-crypto/pull/332/files#r176417542
* Flip the meaning of a boolean testGravatar Jason Gross2018-03-23
| | | | As per https://github.com/mit-plv/fiat-crypto/pull/332/files#r176414627
* Add a comment explaining default inhabitantsGravatar Jason Gross2018-03-23
| | | | As per https://github.com/mit-plv/fiat-crypto/pull/332/files#r176422391
* Use nobrainer1 in the pipelineGravatar Jason Gross2018-03-23
| | | | | | By passing through a type of expression trees without any Gallina functions in the AST, we achieve good performance (even faster than before) on the pipeline with a cbv strategy.
* Add NoBrainer1Gravatar Jason Gross2018-03-23
|
* Thunk let-bound default values, unfold bool_rectGravatar Jason Gross2018-03-23
| | | | | This makes the pipeline faster to run under vm_compute than under lazy. I suspect mainly because I've replaced [bool_rect] with [if].
* Update output of montred from the dlet place changeGravatar Jason Gross2018-03-22
|
* [experiments] Remove dead code, inline some thingsGravatar Jason Gross2018-03-22
|
* Add another reserved notation for App_fstGravatar Jason Gross2018-03-21
|
* s/partial reduction/partial evaluation/Gravatar Jason Gross2018-03-21
|
* Don't inline var nodes on the first pass through partial evaluationGravatar Jason Gross2018-03-21
|
* Let-bind placeGravatar Jason Gross2018-03-21
| | | | | This allows vm_compute to run in 300 seconds on the from_associational pipeline.
* [experiments] Thunk the eliminator casesGravatar Jason Gross2018-03-20
| | | | | This allows us to remove the special case for `bool_rect`, and is a step towards targeting `vm_compute` rather than `lazy`.
* Remove some dead codeGravatar Jason Gross2018-03-19
|
* Fix for Coq <= 8.7Gravatar Jason Gross2018-03-19
|
* Add support for Z*Z casts, get montred workingGravatar Jason Gross2018-03-19
|
* Split up the two calls to `lazy`Gravatar Jason Gross2018-03-19
| | | | It was too slow to do `lazy -[Let_In]` in montgomery reduction.
* Fix some bugs in cachingGravatar Jason Gross2018-03-19
| | | | Also adapt to the lack of `'` notation in master for `Z.pos`.
* Add comments explaining the various [interp] functionsGravatar Jason Gross2018-03-19
|
* Add commented out example of using the full end-to-end lemma inlineGravatar Jason Gross2018-03-19
|
* Add end-to-end correctness lemmaGravatar Jason Gross2018-03-19
|
* Unify cache and nocacheGravatar Jason Gross2018-03-19
|
* Add alternate tactics for handling the all-in-one-derive caseGravatar Jason Gross2018-03-19
|
* Clean and simplify some codeGravatar Jason Gross2018-03-19
|
* WIP with Andres on cleaning boilerplateGravatar Jason Gross2018-03-19
|
* Partial fix for montredGravatar Jason Gross2018-03-19
| | | | Still need to insert casts for operations returning two values
* Speed up the final pipeline by about 2xGravatar Jason Gross2018-03-19
| | | | | | | | | | | | | | | | | As the comment says, doing `lazy` is twice as slow as doing `lazy -[Let_In]; lazy`. This is because the bounds pipeline does `dlet E : Expr := (reduced thing) in let b := extract_bounds E in ...`. If we allow `lazy` to unfold `Let_In` before it fully reduces the function (function, because `Expr := forall var, @expr var`), then there is no sharing between the partial reduction in bounds extraction and the partial reduction in the return value. So we force `lazy` to fully reduce the argument first, and only then permit `lazy` to inline it. This is slightly slower than doing bounds analysis in a non-PHOAS representation; we spend about 3%-5% of the overall time doing bounds extraction, and fully reducing the bounds extraction expression before plugging in arguments costs a bit more. However, it's still reasonably fast, and the code is much simpler when `Interp` always succeeds rather than returning `option`.
* Insert missing commentGravatar Jason Gross2018-03-19
|
* Remove dead bounds analysis codeGravatar Jason Gross2018-03-19
|
* Move the ring goal upGravatar Jason Gross2018-03-19
|
* Add shiftl notationGravatar Jason Gross2018-03-19
|
* Update printingGravatar Jason Gross2018-03-19
|
* Move relax_zrange to a separate phaseGravatar Jason Gross2018-03-19
|
* WIP castGravatar Jason Gross2018-03-19
|
* Update montred to newish pipeline, revive DCEGravatar Jason Gross2018-03-19
| | | | | | | | | - Update the style of montred snythesis to match the changes in the pipeline - Bring back non-quadratic dead code elimination and make use of it for montgomery reduction - Update partial reduction to inline "var-like" things (fst, snd, pair applied to var)
* Add a ring goalGravatar Jason Gross2018-03-19
| | | | Unfortunately, the ring proofs are a bit messy.
* subsetoid_ring: don't ask for false thingsGravatar Jason Gross2018-03-12
| | | | | We can't actually prove the previous okness lemmas in SimplyTypedArithmetic, so we instead ask for exactly what we need.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 23:50:01 +0000