aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/GiblePargen.v
Commit message (Expand)AuthorAgeFilesLines
* Add unhashed functions for comparisonsYann Herklotz2023-09-171-0/+44
* Add beginning to memory generation proofYann Herklotz2023-07-291-4/+4
* Add equivalence classesYann Herklotz2023-07-111-20/+3
* Finish mutual exclusivity checkYann Herklotz2023-06-251-5/+11
* Add SMTCoq solver as dependencyYann Herklotz2023-06-211-5/+8
* Add more to proof of evaluabilityYann Herklotz2023-06-101-1/+5
* Work towards proving evaluabilityYann Herklotz2023-06-051-9/+27
* Move around generating functionsYann Herklotz2023-06-031-4/+68
* Fix proof of predicates completelyYann Herklotz2023-06-021-0/+1
* 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