aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/GiblePargenproofBackward.v
Commit message (Expand)AuthorAgeFilesLines
* Finish evaluability proof of RBopYann Herklotz2023-05-191-17/+43
* Add new proofs about semantic identityYann Herklotz2023-05-181-14/+138
* Work on scheduling proofYann Herklotz2023-05-161-25/+120
* Add start of backward proofYann Herklotz2023-05-161-3/+39
* Add function to reason about executable constraintsYann Herklotz2023-05-151-4/+5
* Split correctness lemma into twoYann Herklotz2023-05-141-2/+19
* Rename backwards proofYann Herklotz2023-05-121-0/+96