aboutsummaryrefslogtreecommitdiff
path: root/src/Specific
Commit message (Expand)AuthorAge
...
* Parameterize bounds analysis over round_upGravatar Jason Gross2017-04-07
* Add Ladderstep130 display logGravatar Jason Gross2017-04-07
* Add display for ladderstep 130-bitGravatar Jason Gross2017-04-07
* Revert "Don't print ladderstep four times"Gravatar Jason Gross2017-04-07
* Add ladderstep display logGravatar Jason Gross2017-04-07
* Don't print ladderstep four timesGravatar Jason Gross2017-04-07
* Add working display of ladderstepGravatar Jason Gross2017-04-07
* Add display logsGravatar Jason Gross2017-04-07
* Display un-interped C codeGravatar Jason Gross2017-04-07
* Add 130-bit 3-register synthesisGravatar Jason Gross2017-04-07
* Add Display files and targetsGravatar Jason Gross2017-04-07
* Use [refine_reflectively] again in ladderstepGravatar Jason Gross2017-04-07
* Use carry_mulGravatar Jason Gross2017-04-07
* Add IntegrationTestLadderstep.vGravatar Jason Gross2017-04-07
* Merge branch 'rename-everything'. Closes #14.Gravatar Andres Erbsen2017-04-06
|\
| * rename-everythingGravatar Andres Erbsen2017-04-06
| * remove unused filesGravatar Andres Erbsen2017-04-06
* | Add IntegrationTest for SubGravatar Jason Gross2017-04-06
* | FIx encoding of [coef]; instead of [encode 2p], it should be [encode p + enco...Gravatar jadep2017-04-06
* | Rename IntegrationTest{=>Mul}.vGravatar Jason Gross2017-04-06
| * start removing BaseSystemGravatar Andres Erbsen2017-04-06
* | Switch to 51-bit limbsGravatar Jason Gross2017-04-06
* | Compute the bitwidth in integration testGravatar Jason Gross2017-04-06
* | don't hardcode number of limbsGravatar jadep2017-04-06
* | Compute weight function from other termsGravatar jadep2017-04-06
|/
* Use tactics from MoveLetIn in integration testGravatar Jason Gross2017-04-05
* Add [Proof using] to most proofsGravatar Jason Gross2017-04-04
* Move sigma MapProjections to a separate fileGravatar Jason Gross2017-04-04
* Use a more robust way of saving context definitions in IntegrationTestGravatar Jason Gross2017-04-03
* More fine-grained tactic importsGravatar Jason Gross2017-04-03
* Split off liftn_sig, add lift{3,4}_sigGravatar Jason Gross2017-04-03
* Synthesize mul instead of addGravatar Jason Gross2017-04-03
* Work around an anomaly in pretyping/constr_matchingGravatar Jason Gross2017-04-03
* Document some tactics from Jade's pipleine sideGravatar Jason Gross2017-04-03
* Finally, a fully working IntegrationTestGravatar Jason Gross2017-04-03
* WIPGravatar Jason Gross2017-04-03
* WIP on integrationGravatar Jason Gross2017-04-03
* An approximately first stab DeBruijn word-size-selGravatar Jason Gross2017-04-03
* Remove old reflective pipeline, making way the newGravatar Jason Gross2017-04-03
* Remove everything after the individual reified opsGravatar Jason Gross2017-04-03
* Remove the bits of the new reflective pipeline in masterGravatar Jason Gross2017-04-02
* Add an initial glue file in the pipeline, no option in boundsGravatar Jason Gross2017-04-01
* Fix definition of BoundedWordGravatar Jason Gross2017-04-01
* Split off BoundedWord.v from IntegrationTest.vGravatar Jason Gross2017-04-01
* insert a reduce step in the correct place of the carry chainGravatar jadep2017-04-01
* Add a comment explaining bounds_expGravatar Jason Gross2017-03-30
* Update IntegrationTest with actual boundsGravatar Jason Gross2017-03-30
* Created test file for newbasesystem/word-size-selection integrationGravatar jadep2017-03-30
* turn [Let]s into [Definition]s so they persist after the sectionGravatar jadep2017-03-30
* change import order to avoid name-clash with [List.repeat] and [Tuple.repeat]Gravatar jadep2017-03-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-16 02:58:56 +0000