aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/Abstr.v
Commit message (Expand)AuthorAgeFilesLines
* Work on scheduling proofYann Herklotz2023-05-161-0/+4
* Split proof up into more filesYann Herklotz2023-05-091-1760/+64
* Add assumption and prove assumption that preds are evaluableYann Herklotz2023-05-061-43/+49
* Add check for mutexcl and fix top-level proofYann Herklotz2023-05-061-324/+47
* Finished proof of beq_pred_expr in both directionsYann Herklotz2023-05-051-12/+108
* Finish forward and backward proofs for predicated proofYann Herklotz2023-05-051-189/+499
* Try and prove equivalence of predicated thingsYann Herklotz2023-05-051-167/+188
* Continue proofs about Abstr.vYann Herklotz2023-05-041-247/+311
* Fix definitions of structural equalityYann Herklotz2023-05-021-18/+125
* Change nat to positive in Sat proofYann Herklotz2023-04-271-15/+12
* Added lemmas about decidability of SatYann Herklotz2023-04-241-54/+189
* Add temp filesYann Herklotz2023-03-121-4/+6
* Work on proof of norm_expressionYann Herklotz2023-02-221-0/+178
* Change evaluation of predicates and remove forest_evaluableYann Herklotz2023-02-111-12/+16
* Switch to half lazy evaluationYann Herklotz2023-02-051-8/+28
* Prove top level theorems with evaluabilityYann Herklotz2022-11-151-0/+11
* Clean up proofsYann Herklotz2022-10-111-0/+10
* [sched] Remove some unprovable lemmasYann Herklotz2022-10-061-19/+42
* Update and fix the transformationYann Herklotz2022-08-051-3/+3
* Add back changes to AbstrYann Herklotz2022-08-041-185/+297
* Add forest typeYann Herklotz2022-08-011-3/+8
* Merge remote-tracking branch 'origin/dev/scheduling' into dev/schedulingYann Herklotz2022-07-311-111/+4
|\
| * Add current changesYann Herklotz2022-07-311-111/+4
* | Start refactor in AbstrYann Herklotz2022-07-311-14/+29
|/
* Work on implementing abstract predicatesYann Herklotz2022-07-191-99/+103
* Add work on abstract predicatesYann Herklotz2022-07-141-44/+141
* Add work on schedulingYann Herklotz2022-07-031-18/+29
* Work on CondElim proofYann Herklotz2022-06-031-5/+5
* Rewrite a lot fixing scheduling of GibleYann Herklotz2022-05-271-120/+6
* Remove literal files againYann Herklotz2022-03-261-18/+36
* Move forall_ptree into commonYann Herklotz2022-03-221-42/+0
* Add back proof of beq2_correctYann Herklotz2022-03-031-23/+76
* Fix AbstrYann Herklotz2022-03-031-30/+17
* Fix up some more documentationYann Herklotz2022-02-251-26/+13
* Add the tseytin transformation insteadYann Herklotz2021-11-141-9/+0
* Add Admitted theorems for existence proofsYann Herklotz2021-11-011-9/+2
* Add construction of state in semYann Herklotz2021-10-311-23/+147
* Make Abstr pass with admitted to check top-levelYann Herklotz2021-10-301-45/+110
* Remove admitted from subproofYann Herklotz2021-10-291-6/+57
* Add intermediate step in proof of sem presYann Herklotz2021-10-271-24/+82
* Work more on equivalence of SATYann Herklotz2021-10-261-33/+121
* Continue on semantics preservation proofYann Herklotz2021-10-241-198/+178
* Add setoid typeclassYann Herklotz2021-10-211-15/+21
* Add work towards decidability of SAT solverYann Herklotz2021-10-211-29/+98
* Start to prove termination of SATYann Herklotz2021-10-201-8/+0
* Continuations on proof of predicatesYann Herklotz2021-10-191-98/+151
* [sched] Add combination of equivalent expressionsYann Herklotz2021-10-141-10/+40
* [sched] Finish det proofs of basic Abstr semanticsYann Herklotz2021-10-131-27/+44
* [sched] Add more proof to sem_pred_detYann Herklotz2021-10-131-1/+6
* [sched] Add proofs of sem_pred_detYann Herklotz2021-10-131-8/+44
generated by cgit (git 2.34.1) at 2024-06-26 00:46:01 +0000