aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/CondElimproof.v
Commit message (Expand)AuthorAgeFilesLines
* Annonimize submissiondev/asplosYann Herklotz2023-08-101-1/+1
* 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