aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAge
* pass-through after Andres's review in #334Gravatar Jade Philipoom2018-04-03
|
* move requires to the top of the fileGravatar Jade Philipoom2018-04-03
|
* make montgomery not depend on intermediate weight for multiplication being ↵Gravatar Jade Philipoom2018-04-03
| | | | the sqrt of the usual weight
* rename w_half to w_mulGravatar Jade Philipoom2018-04-03
|
* make a more general kind of mul_converted_halve that produces the correct ↵Gravatar Jade Philipoom2018-04-03
| | | | carries even in cases where w is not necessarily the square of w', but potentially some other power
* move some lemmas to ZUtil/ListUtilGravatar Jade Philipoom2018-04-03
|
* move some shared lemmas between Columns/Rows into a Saturated moduleGravatar Jade Philipoom2018-04-03
|
* reprint Montgomery output (order of additions in Rows.flatten changed)Gravatar Jade Philipoom2018-04-03
|
* more proof automation in RowsGravatar Jade Philipoom2018-04-03
|
* automate some Rows proofsGravatar Jade Philipoom2018-04-03
|
* organize Rows into sectionsGravatar Jade Philipoom2018-04-03
|
* organize proofs into sectionsGravatar Jade Philipoom2018-04-03
|
* more cleanup of flatten proofsGravatar Jade Philipoom2018-04-03
|
* clean up some [flatten] proofsGravatar Jade Philipoom2018-04-03
|
* move some lemmas/hints to ListUtilGravatar Jade Philipoom2018-04-03
|
* fix typo and add booleans for carriesGravatar Jade Philipoom2018-04-03
|
* changing Montgomery notationsGravatar Jade Philipoom2018-04-03
|
* make add_with_get_carry with a constant zero for the carry translate to ↵Gravatar Jade Philipoom2018-04-03
| | | | add_get_carry
* inline shifts for Montgomery exampleGravatar Jade Philipoom2018-04-03
|
* Make Montgomery example use row-wise flatten (involves adding Nat.max, ↵Gravatar Jade Philipoom2018-04-03
| | | | List.tl, and List.hd to the pipeline)
* add Rows.from_associational and some more length proofs that allow ↵Gravatar Jade Philipoom2018-04-03
| | | | Rows.length_from_associational
* move mul_converted to its own moduleGravatar Jade Philipoom2018-04-03
|
* finish flatten_partitions and slightly change the format of _partitions ↵Gravatar Jade Philipoom2018-04-03
| | | | lemma statements
* proved admits about sum_rowsGravatar Jade Philipoom2018-04-03
|
* finish from_columns proofsGravatar Jade Philipoom2018-04-03
|
* progress on from_columns proofsGravatar Jade Philipoom2018-04-03
|
* clean up proofs a bitGravatar Jade Philipoom2018-04-03
|
* prove sum_rows_div_mod and fix up Rows.from_columns a bitGravatar Jade Philipoom2018-04-03
|
* rowwise flatten (more fleshed-out) and proof outlineGravatar Jade Philipoom2018-04-03
|
* preliminary version of rowwise flattenGravatar Jade Philipoom2018-04-03
|
* some work on rowwise flattenGravatar Jade Philipoom2018-04-03
|
* Add two examples of using the pipeline in a one-linerGravatar Jason Gross2018-04-01
|
* Fix the pipeline to not insert extra castsGravatar Jason Gross2018-03-31
| | | | | | | So long as we have subst01, it must come before bounds analysis (or followed by an extra pass of partial evaluation), because bounds analysis inserts casts at every let-in node, and so inlining some of them results in duplicated cast nodes, which we don't want to have.
* Update printout after change to pipelineGravatar Jason Gross2018-03-31
|
* Do some pipeline consolidation and reorganizationGravatar Jason Gross2018-03-29
| | | | | | | | | | | - Since we pass through a flat representation, we no longer need to invoke `vm_compute` twice, so we don't need to separate out bounds checking from bounds analysis - Only call partial evaluation once, not twice - Remove the call to constant reassociation, as it no longer has a place (it only works post-partial-evaluation pre-bounds-analysis)
* Allow passing in optional bounds to the pipelineGravatar Jason Gross2018-03-28
|
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 09:52:08 +0000