aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls
Commit message (Expand)AuthorAgeFilesLines
* Update to Coq 8.17 and CompCert 3.12Yann Herklotz2023-04-275-109/+5
* Change nat to positive in Sat proofYann Herklotz2023-04-278-68/+202
* Work on finishing the SAT decidability proofsYann Herklotz2023-04-241-26/+44
* Added lemmas about decidability of SatYann Herklotz2023-04-243-117/+293
* Add temp filesYann Herklotz2023-03-122-10/+24
* Work on proof of norm_expressionYann Herklotz2023-02-223-57/+261
* 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-124-3/+352
* Change evaluation of predicates and remove forest_evaluableYann Herklotz2023-02-114-100/+125
* Switch to half lazy evaluationYann Herklotz2023-02-053-52/+113
* Work on intermediate lemma for evaluationYann Herklotz2023-01-291-5/+12
* Prove abstr_fold_correct top-downYann Herklotz2023-01-292-41/+99
* Add documentation and continue on top-down proofYann Herklotz2023-01-281-6/+54
* Work on simplifying seq_app evaluation lemmaYann Herklotz2023-01-022-6/+13
* 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-152-43/+344
* 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-118-143/+145
* [sched] Remove some unprovable lemmasYann Herklotz2022-10-064-899/+178
* Add new if-conversion pass with top-level foldYann Herklotz2022-09-292-64/+67
* Add proof using to ifconversionproofYann Herklotz2022-09-292-24/+30
* Add global monad notation using InstancesYann Herklotz2022-09-265-93/+88
* Update and fix the transformationYann Herklotz2022-08-054-272/+313
* Add back changes to AbstrYann Herklotz2022-08-042-246/+362
* Add forest typeYann Herklotz2022-08-011-3/+8
* Merge remote-tracking branch 'origin/dev/scheduling' into dev/schedulingYann Herklotz2022-07-312-112/+5
|\
| * Add current changesYann Herklotz2022-07-312-112/+5
* | Start refactor in AbstrYann Herklotz2022-07-311-14/+29
|/
* 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-1912-340/+515
* Add work on abstract predicatesYann Herklotz2022-07-145-95/+376
* Working on scheduling proofYann Herklotz2022-07-044-55/+224
* Try and fix pargenproofYann Herklotz2022-07-041-8/+7
* Add work on schedulingYann Herklotz2022-07-033-56/+63
* Update ifconversion definitionYann Herklotz2022-07-012-65/+73
* Finish DeadBlocksproofYann Herklotz2022-07-013-101/+158
* Merge remote-tracking branch 'origin/dev/scheduling' into dev/schedulingYann Herklotz2022-07-012-75/+466
|\
| * Working on extending ifconversion proofYann Herklotz2022-06-302-0/+20
generated by cgit (git 2.34.1) at 2024-06-30 21:55:34 +0000