aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
...
* | remove commentGravatar Jade Philipoom2018-04-11
* | add a comment to rerun buildGravatar Jade Philipoom2018-04-11
* | Automate some proofs a bit moreGravatar Jason Gross2018-04-11
* | try to fix build on coq masterGravatar Jade Philipoom2018-04-11
* | prove stronger bound on quotient error for barrett reductionGravatar Jade Philipoom2018-04-11
* | Update number/string conversionsGravatar Jason Gross2018-04-09
* | 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
* | Make Montgomery example use row-wise flatten (involves adding Nat.max, List.t...Gravatar Jade Philipoom2018-04-03
* | add Rows.from_associational and some more length proofs that allow Rows.lengt...Gravatar Jade Philipoom2018-04-03
* | move mul_converted to its own moduleGravatar Jade Philipoom2018-04-03
* | finish flatten_partitions and slightly change the format of _partitions lemma...Gravatar Jade Philipoom2018-04-03
* | 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
* | Update printout after change to pipelineGravatar Jason Gross2018-03-31
* | Do some pipeline consolidation and reorganizationGravatar Jason Gross2018-03-29
* | Allow passing in optional bounds to the pipelineGravatar Jason Gross2018-03-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 21:30:12 +0000