aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/CondElimproof.v
Commit message (Collapse)AuthorAgeFilesLines
* Finish final forward simulation correctnessYann Herklotz2023-08-101-0/+6
|
* Change nat to positive in Sat proofYann Herklotz2023-04-271-9/+9
|
* Rearrange definitions and create IfConversion templateYann Herklotz2022-06-061-88/+0
|
* Finish CondElim proof and fix Gible semanticsYann Herklotz2022-06-061-104/+181
|
* Fix many more lemmasYann Herklotz2022-06-051-108/+307
|
* Remove inv H1 from condelim proofYann Herklotz2022-06-051-3/+3
|
* Add condelim proofYann Herklotz2022-06-051-85/+169
|
* work on condelimproofYann Herklotz2022-06-041-66/+72
|
* Add to condelim proofYann Herklotz2022-06-041-2/+111
|
* Working towards ElimCond proofYann Herklotz2022-06-031-34/+82
|
* Work on CondElim proofYann Herklotz2022-06-031-6/+73
|
* Add new translation passes for if-conversionYann Herklotz2022-05-311-0/+179