aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments
Commit message (Expand)AuthorAge
...
* fix commentGravatar Jade Philipoom2018-04-30
* Fix bounds analysis for saturated ops and remove unneeded commentGravatar Jade Philipoom2018-04-30
* first stab at reifying barrettGravatar Jade Philipoom2018-04-30
* fix definitions of saturated operations to avoid unnecessary work, and make M...Gravatar Jade Philipoom2018-04-30
* tweak definition of flatten to use an index rather than check the length of t...Gravatar Jade Philipoom2018-04-30
* fix the placement of a dlet to make more senseGravatar Jade Philipoom2018-04-30
* In reassocation, don't reassociate additionsGravatar Jason Gross2018-04-26
* Fix a printoutGravatar Jason Gross2018-04-26
* Revert most of "Make reassociation optional"Gravatar Jason Gross2018-04-26
* Make reassociation optionalGravatar Jason Gross2018-04-26
* Compute tight bounds in a different wayGravatar Jason Gross2018-04-26
* Don't introduce extra lambdas and apps in uncurryGravatar Jason Gross2018-04-26
* Add some Positional Hint RewritesGravatar Jason Gross2018-04-26
* pass-through after Jason's reviewGravatar Jade Philipoom2018-04-19
* add instructions cc_m, rshi, and sub_with_get_borrow to pipeline in preparati...Gravatar Jade Philipoom2018-04-19
* Also include argument bounds in bounds-analysis-failure messageGravatar Jason Gross2018-04-18
* Merge pull request #335 from mit-plv/cpsloopsGravatar Andres Erbsen2018-04-18
|\
* | Actually display the error messages from pipeline failuresGravatar Jason Gross2018-04-18
* | Add a Z.cast2 case to bounds extractionGravatar Jason Gross2018-04-18
* | Also include the syntax tree in bounds analysis errorsGravatar Jason Gross2018-04-18
* | move requires to top of fileGravatar Jade Philipoom2018-04-11
* | barrett reduction definition and proofGravatar Jade Philipoom2018-04-11
* | fix trashed carry flagGravatar Jade Philipoom2018-04-11
* | package properties of weight functions into a recordGravatar Jade Philipoom2018-04-09
* | relocate and prove an admitGravatar Jade Philipoom2018-04-09
* | reorganization: move more things into BaseConversionGravatar Jade Philipoom2018-04-09
* | better factoring-out of mul_converted stuff, define saturated arith operationsGravatar Jade Philipoom2018-04-06
* | Use a simpler form of UncurryingGravatar Jason Gross2018-04-04
* | Stick an uncurry pass in the pipelineGravatar Jason Gross2018-04-04
* | Add UncurryGravatar Jason Gross2018-04-04
* | pass-through after Jason's reviewGravatar Jade Philipoom2018-04-03
* | 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 th...Gravatar Jade Philipoom2018-04-03
* | rename w_half to w_mulGravatar Jade Philipoom2018-04-03
* | make a more general kind of mul_converted_halve that produces the correct car...Gravatar Jade Philipoom2018-04-03
* | 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 add_g...Gravatar Jade Philipoom2018-04-03
* | inline shifts for Montgomery exampleGravatar Jade Philipoom2018-04-03