aboutsummaryrefslogtreecommitdiff
path: root/src/NewBaseSystem.v
Commit message (Collapse)AuthorAge
* More extensive comment in NewBaseSystemGravatar Jason Gross2017-04-02
| | | | As per Andres' request on #138.
* Work around bug #5434Gravatar Jason Gross2017-04-02
| | | | | | | This is https://coq.inria.fr/bugs/show_bug.cgi?id=5434, [vm_compute] breaks an invariant asserted on line 115 of pretyping/constr_matching.ml. This was triggering whenever we tried to reify one of the operations.
* Remove trailing whitespace in NewBaseSystemGravatar Jason Gross2017-04-01
|
* insert a reduce step in the correct place of the carry chainGravatar jadep2017-04-01
|
* rewrite zeros to use tuple [repeat]Gravatar jadep2017-03-30
|
* Add lemmas needed for saturated arithmetic [compact]Gravatar jadep2017-03-24
|
* Fixes #127Gravatar jadep2017-03-06
|
* Remove assert_preconditions; prove ring-ness of basesystem operations for ↵Gravatar jadep2017-03-04
| | | | base 2^25.5
* Separated out specific test cases for new base systemGravatar jadep2017-03-04
|
* Fixed admit left from fsatz portGravatar jadep2017-03-02
|
* fixup NewBasesystemGravatar Andres Erbsen2017-03-02
|
* make assert_preconditions way more sane; use vm_decide to kill most subgoalsGravatar jadep2017-03-02
|
* Separated out [carry] from other operations.Gravatar jadep2017-03-02
|
* Modify/add to NewBaseSystem to match with what is needed for proof of ring ↵Gravatar jadep2017-03-01
| | | | isomorphism to F
* Fixed carry bugs (indexes need to be reversed, and we need to convert ↵Gravatar jadep2017-03-01
| | | | to/from Positional every time we carry) and added an [encode] function
* Defined [div] and [mod]; removed liftn_sig lemmas because they were actually ↵Gravatar jadep2017-03-01
| | | | no longer needed
* Defined zero and one for NewBaseSystemGravatar jadep2017-02-27
|
* Added operation (including creating )Gravatar jadep2017-02-27
|
* Added subtractionGravatar jadep2017-02-27
|
* added Positional wrappers for Associational operations, added correctness ↵Gravatar jadep2017-02-27
| | | | proof of
* changed names of ops in NewBaseSystem to reflect that they are sig and not sigTGravatar jadep2017-02-27
|
* Modified lemma and created tactic to handle it; added reduce step to ↵Gravatar jadep2017-02-26
| | | | multiplication operation; introduced modular equality to NewBaseSystem
* removed leftover saturated stuff (will probably end up in a separate file ↵Gravatar jadep2017-02-26
| | | | someday)
* speed up NewBaseystem synthesisGravatar Andres Erbsen2017-02-23
| | | | | | Use a vm_compute hack fromhttps://arxiv.org/pdf/1305.6543.pdf section 5.5: pattern terms over what to keep opaque, then reduce the lambda using vm_compute.
* added explanation of why CPS is usefulGravatar jadep2017-02-23
|
* NewBaseSystem: less verboseGravatar Andres Erbsen2017-02-22
|
* Merge new base system (#112)Gravatar jadephilipoom2017-02-22
* Added sketch of new low-level base system code * Implemented and proved addition * Implemented carrying, which requires defining over Z rather than arbitrary ring * Proved carry and proved ring-ness of base system ops * Implemented split operation * Started implementing modular reduction * NewBaseSystem: prettify some proofs * andres base * improve andresbase * new base * first draft of goldilocks karatsuba * Factored out goldilocks karatsuba * Implement and prove karatsuba * goldilocks cleanup remodularize * merge karatsuba and goldilocs karatsuba parameter blocks * carry impl and proofs (not yet synthesis-ready) * newbasesystem: use rewrite databases * carry index range fix (TODO: allow for carry-then-reduce) * simpler carry implementation * Added compact operation for saturated base systems (this handles carries after multiplying or adding) * debugging reduction for compact_rows * rewrote compact * Converted saturated section to CPS * some progress on cps conversion for non-saturated stuff * Converted associational non-saturated code to CPS, temporarily commented out examples * pushed cps conversion through Positional * moved list/tuple stuff to top of file * proved lingering lemma * worked on generic-style goal for simplified operations * finished proving the generic-form example goal, revising a couple earlier lemmas * revised previous lemmas * finished revising previous lemmas * removed commented-out code * fixed non-terminating string in comment * fix for 8.5 * removed old file * better automation part 1 * better automation part 2 (goodbye proofs) * better automation part 3/3 * some work on freeze * remove saturated code and clean up exported-operations code * Move helper lemmas for list/tuple CPS stuff to new CPSUtil file * qualified imports * fix runtime notations and module-level Let as per comments * moved push_id to CPSUtil and cancel_pair lemmas to Prod * fixed typo * correctly generalized and moved lift_tuple2 (now called lift2_sig) and converted chained_carries into a fold * moved karatsuba section to new file * rename lemmas and definitions (now cps definitions are consistently <name>_cps and non-cps equivalents have no suffix) * updated timing on mulT * renamed push_eval to push_basesystem_eval
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 06:37:17 +0000