aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/GiblePargen.v
Commit message (Expand)AuthorAgeFilesLines
* Finished the propert version of from_predicated_sem_pred_expr2Yann Herklotz2023-06-021-2/+11
* Prove evaluable_pred_expr_exists_RBsetpredYann Herklotz2023-05-211-10/+0
* Work on scheduling proofYann Herklotz2023-05-161-0/+7
* Add example computation to update functionYann Herklotz2023-05-151-0/+11
* Add function to reason about executable constraintsYann Herklotz2023-05-151-1/+11
* Split proof up into more filesYann Herklotz2023-05-091-0/+27
* Continue proofs about Abstr.vYann Herklotz2023-05-041-1/+1
* Finish sem_update_instr finallyYann Herklotz2023-02-121-0/+19
* Change evaluation of predicates and remove forest_evaluableYann Herklotz2023-02-111-4/+7
* Switch to half lazy evaluationYann Herklotz2023-02-051-1/+1
* Work on simplifying seq_app evaluation lemmaYann Herklotz2023-01-021-0/+2
* Clean up proofsYann Herklotz2022-10-111-52/+24
* [sched] Remove some unprovable lemmasYann Herklotz2022-10-061-38/+3
* Add global monad notation using InstancesYann Herklotz2022-09-261-4/+4
* Update and fix the transformationYann Herklotz2022-08-051-7/+17
* Add back changes to AbstrYann Herklotz2022-08-041-61/+65
* Add current changesYann Herklotz2022-07-311-1/+1
* Work on implementing abstract predicatesYann Herklotz2022-07-191-69/+131
* Add work on abstract predicatesYann Herklotz2022-07-141-9/+5
* Add work on schedulingYann Herklotz2022-07-031-23/+23
* Update documentation for GibleYann Herklotz2022-06-241-3/+3
* Fix update function for control-flowYann Herklotz2022-05-311-1/+12
* Fix code generation in partitioning and schedulingYann Herklotz2022-05-271-2/+3
* Rewrite a lot fixing scheduling of GibleYann Herklotz2022-05-271-0/+296