aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/GiblePargenproof.v
Commit message (Expand)AuthorAgeFilesLines
* Finished painful product proofYann Herklotz2023-05-301-4/+4
* Rename backwards proofYann Herklotz2023-05-121-30/+4
* Split proof up into more filesYann Herklotz2023-05-091-2006/+79
* Add assumption and prove assumption that preds are evaluableYann Herklotz2023-05-061-0/+1
* Add check for mutexcl and fix top-level proofYann Herklotz2023-05-061-18/+33
* Finish forward and backward proofs for predicated proofYann Herklotz2023-05-051-90/+0
* Change nat to positive in Sat proofYann Herklotz2023-04-271-8/+4
* Added lemmas about decidability of SatYann Herklotz2023-04-241-21/+0
* Work on proof of norm_expressionYann Herklotz2023-02-221-48/+0
* Remove aborted evaluable proofsYann Herklotz2023-02-181-96/+4
* Prove abstr_fold_falsy correctYann Herklotz2023-02-121-21/+100
* Prove sem_update_instr_term correctYann Herklotz2023-02-121-8/+19
* Prove abstr_fold_correct inductive case fullyYann Herklotz2023-02-121-12/+15
* Finish eval_predf_update_trueYann Herklotz2023-02-121-3/+6
* Finish sem_update_instr finallyYann Herklotz2023-02-121-3/+247
* Change evaluation of predicates and remove forest_evaluableYann Herklotz2023-02-111-84/+52
* Switch to half lazy evaluationYann Herklotz2023-02-051-43/+84
* Work on intermediate lemma for evaluationYann Herklotz2023-01-291-5/+12
* Prove abstr_fold_correct top-downYann Herklotz2023-01-291-41/+94
* Add documentation and continue on top-down proofYann Herklotz2023-01-281-6/+54
* Work on simplifying seq_app evaluation lemmaYann Herklotz2023-01-021-6/+11
* Add all_evaluable lemma for seq_appYann Herklotz2023-01-011-0/+9
* Add proofs about evaluation of body of expressionsYann Herklotz2022-12-271-7/+59
* Add proofs about evaluability of predicates in the abstract stateYann Herklotz2022-12-241-23/+55
* Add todoYann Herklotz2022-12-011-76/+163
* Prove top level theorems with evaluabilityYann Herklotz2022-11-151-43/+333
* Add proofs about evaluability of predicatesYann Herklotz2022-11-101-18/+132
* Add many more proofs about sem_pred_exprYann Herklotz2022-10-261-36/+311
* Add proofs for sem_pexpr and app_predicatedYann Herklotz2022-10-251-43/+269
* Prove sem_update for load and create lemmaYann Herklotz2022-10-241-3/+51
* Work on abstract lemmas for update functionYann Herklotz2022-10-201-8/+318
* Clean up proofsYann Herklotz2022-10-111-11/+31
* [sched] Remove some unprovable lemmasYann Herklotz2022-10-061-842/+113
* Add global monad notation using InstancesYann Herklotz2022-09-261-83/+75
* Update and fix the transformationYann Herklotz2022-08-051-252/+253
* Update lemmas with new update functionYann Herklotz2022-07-261-35/+128
* Fix main proofYann Herklotz2022-07-201-21/+27
* Work on implementing abstract predicatesYann Herklotz2022-07-191-10/+10
* Add work on abstract predicatesYann Herklotz2022-07-141-35/+223
* Working on scheduling proofYann Herklotz2022-07-041-53/+147
* Try and fix pargenproofYann Herklotz2022-07-041-8/+7
* Add work on schedulingYann Herklotz2022-07-031-15/+11
* Rewrite a lot fixing scheduling of GibleYann Herklotz2022-05-271-0/+1148
generated by cgit (git 2.34.1) at 2024-06-30 22:04:55 +0000