aboutsummaryrefslogtreecommitdiff
path: root/src/NewBaseSystem.v
Commit message (Expand)AuthorAge
* More extensive comment in NewBaseSystemGravatar Jason Gross2017-04-02
* Work around bug #5434Gravatar Jason Gross2017-04-02
* 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 bas...Gravatar jadep2017-03-04
* 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 is...Gravatar jadep2017-03-01
* Fixed carry bugs (indexes need to be reversed, and we need to convert to/from...Gravatar jadep2017-03-01
* Defined [div] and [mod]; removed liftn_sig lemmas because they were actually ...Gravatar jadep2017-03-01
* 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 pro...Gravatar jadep2017-02-27
* 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 multipl...Gravatar jadep2017-02-26
* removed leftover saturated stuff (will probably end up in a separate file som...Gravatar jadep2017-02-26
* speed up NewBaseystem synthesisGravatar Andres Erbsen2017-02-23
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-10 19:05:58 +0000