aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls
Commit message (Expand)AuthorAgeFilesLines
...
* 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-214-100/+493
* Work on evaluability proofYann Herklotz2023-05-191-0/+37
* Prepare work on evaluability of instructionsYann Herklotz2023-05-193-71/+133
* Finish evaluability proof of RBopYann Herklotz2023-05-195-210/+338
* Add new proofs about semantic identityYann Herklotz2023-05-184-599/+868
* Work on scheduling proofYann Herklotz2023-05-164-25/+154
* Add start of backward proofYann Herklotz2023-05-161-3/+39
* Add example computation to update functionYann Herklotz2023-05-151-0/+11
* Add function to reason about executable constraintsYann Herklotz2023-05-152-5/+16
* Split correctness lemma into twoYann Herklotz2023-05-141-2/+19
* Rename backwards proofYann Herklotz2023-05-123-30/+55
* Split proof up into more filesYann Herklotz2023-05-098-3766/+3924
* Add assumption and prove assumption that preds are evaluableYann Herklotz2023-05-062-43/+50
* Add check for mutexcl and fix top-level proofYann Herklotz2023-05-062-342/+80
* Finished proof of beq_pred_expr in both directionsYann Herklotz2023-05-051-12/+108
* Finish forward and backward proofs for predicated proofYann Herklotz2023-05-053-287/+499
* Try and prove equivalence of predicated thingsYann Herklotz2023-05-052-167/+196
* Continue proofs about Abstr.vYann Herklotz2023-05-043-279/+330
* Add IfConversionOracle.mlYann Herklotz2023-05-041-0/+43
* Add structural equality for predicatesYann Herklotz2023-05-021-0/+29
* Fix warnings introduced by Coq 8.17Yann Herklotz2023-05-021-8/+14
* Fix definitions of structural equalityYann Herklotz2023-05-021-18/+125
* Update Sat.v namesYann Herklotz2023-04-282-300/+280
* Finish decidability proof of SATYann Herklotz2023-04-281-39/+219
* 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
generated by cgit (git 2.34.1) at 2024-06-28 19:38:18 +0000