aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/GiblePargenproofBackward.v
Commit message (Collapse)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