aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/GiblePargenproofBackward.v
Commit message (Expand)AuthorAgeFilesLines
* Finish mutual exclusivity checkYann Herklotz2023-06-251-2/+2
* Add proof outline for evaluabilityYann Herklotz2023-06-081-2/+0
* Work towards proving evaluabilityYann Herklotz2023-06-051-28/+28
* Move around generating functionsYann Herklotz2023-06-031-64/+0
* Fix proof of predicates completelyYann Herklotz2023-06-021-7/+23
* Fix top-level proof with Isetpred missingYann Herklotz2023-06-021-12/+55
* Finished the propert version of from_predicated_sem_pred_expr2Yann Herklotz2023-06-021-2/+19
* Finish proofs in GiblePargenproofBackward.vYann Herklotz2023-05-271-26/+101
* Add proofs of gather_predicatesYann Herklotz2023-05-261-25/+196
* Finish predicate inclusion proofsYann Herklotz2023-05-251-48/+99
* Finish gather_predicate proofsYann Herklotz2023-05-241-17/+502
* Prove evaluability of predicates throughoutYann Herklotz2023-05-221-61/+126
* Work on smaller evaluability proofYann Herklotz2023-05-221-49/+88
* Finish abstr_seq_reverse_correct_foldYann Herklotz2023-05-211-35/+87
* Add proof about preds_emptyYann Herklotz2023-05-211-3/+12
* Add proofs about RBexitYann Herklotz2023-05-211-2/+63
* Prove evaluable_pred_expr_exists_RBsetpredYann Herklotz2023-05-211-83/+474
* Work on evaluability proofYann Herklotz2023-05-191-0/+37
* Prepare work on evaluability of instructionsYann Herklotz2023-05-191-23/+34
* 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
generated by cgit (git 2.34.1) at 2024-06-26 02:50:30 +0000