aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/RTLPargen.v
Commit message (Expand)AuthorAgeFilesLines
* Add list of bb to semanticsYann Herklotz2022-03-311-1/+1
* Remove literal files againYann Herklotz2022-03-261-27/+77
* Add more documentationYann Herklotz2022-03-241-36/+14
* Change origin of tangled filesYann Herklotz2022-03-231-1/+1
* Add comments to allow for literate detanglingYann Herklotz2022-03-221-1/+3
* Fix up some more documentationYann Herklotz2022-02-251-19/+11
* Start converting commentsYann Herklotz2022-02-251-15/+5
* Simplify the RTLPargen update functionYann Herklotz2021-11-131-11/+21
* Add documentation to RTLPargenYann Herklotz2021-11-111-18/+72
* Uncomment many more proofsYann Herklotz2021-11-021-917/+1
* Merge remote-tracking branch 'origin/dev/scheduling' into dev/schedulingYann Herklotz2021-11-021-8/+6
|\
| * Merge remote-tracking branch 'origin/dev/scheduling' into dev/schedulingYann Herklotz2021-11-011-129/+153
| |\
| * | [sched] Simplify some of the Lemma statementsYann Herklotz2021-11-011-8/+6
* | | No admitted theorems in RTLPargenproof.vYann Herklotz2021-11-021-2/+2
| |/ |/|
* | Add work on RTLPargenproof.vYann Herklotz2021-11-011-129/+153
|/
* Fix compilation issues with new typesYann Herklotz2021-10-301-28/+12
* [sched] Fix passes with new predicatesYann Herklotz2021-10-141-0/+1
* Add abstract intermediate language to RTLPargenYann Herklotz2021-10-081-17/+49
* RTLPargen now uses Abstr as symbolic execution targetYann Herklotz2021-10-071-705/+1
* Fix equivalence checkingYann Herklotz2021-10-011-4/+2
* Improve equivalence checking using SATYann Herklotz2021-10-011-15/+22
* Fix scopingYann Herklotz2021-09-241-12/+10
* Add back top-level functionsYann Herklotz2021-09-241-40/+157
* RTLpargen passes compilation againYann Herklotz2021-09-221-8/+16
* Fix the comparison of predicated expressionsYann Herklotz2021-09-221-138/+174
* Start adding hashing to RTLPargenYann Herklotz2021-09-201-5/+49
* Merge branch 'master' into developYann Herklotz2021-09-181-4/+6
|\
| * Remove unnecessary files and proofsYann Herklotz2021-07-111-3/+4
* | Add predicate semantics to abstractYann Herklotz2021-05-261-69/+296
* | Finish top-level of proofYann Herklotz2021-05-211-9/+1
* | Finish up step_cf_instr_correct againYann Herklotz2021-05-161-0/+18
* | Fix the top-level proofs with new state_matchYann Herklotz2021-05-151-8/+101
* | Finish abstract interpretationYann Herklotz2021-05-121-75/+199
* | Fix admitted in first proof of sem. preservationYann Herklotz2021-05-101-19/+68
* | Finish correctness of semantics wrt. RTBlockYann Herklotz2021-05-061-84/+327
* | Add admitted proof of translations in RTLPargenYann Herklotz2021-05-031-27/+177
|/
* Fix RTLPar to use instr list list listYann Herklotz2021-02-161-7/+1
* Add temporary fixes to get everything to compileYann Herklotz2021-02-121-1/+9
* Add Vrange and predicatesYann Herklotz2021-02-021-4/+5
* Fix proofs with better defined equalityYann Herklotz2021-01-301-11/+6
* Fix definitions of proofs some moreYann Herklotz2021-01-291-47/+51
* Fix HTLPargen and RTLPargenYann Herklotz2021-01-291-51/+173
* Add more proofs for RTLPargen correctnessYann Herklotz2021-01-271-6/+22
* Remove the schedule oracleYann Herklotz2021-01-261-3/+515
* Share code between RTLBlock and ParYann Herklotz2021-01-211-44/+7
* Correct translation of scheduling with oracle checkYann Herklotz2021-01-131-4/+53
* Add RTLPargen.vYann Herklotz2021-01-131-0/+27
generated by cgit (git 2.34.1) at 2024-06-28 21:59:02 +0000