aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/RTLtoBTLproof.v
Commit message (Expand)AuthorAgeFilesLines
* Porting the BTL non-trap loads approach to RTLLéo Gourdin2021-11-021-3/+7
* ci fix?Léo Gourdin2021-07-281-18/+9
* non trapping loadsLéo Gourdin2021-07-231-6/+9
* finish RTLtoBTL proofLéo Gourdin2021-06-181-2/+18
* End of main scheduling proofLéo Gourdin2021-06-181-5/+4
* some advance, new section to simplify context from symbolic execLéo Gourdin2021-06-171-1/+1
* Preparation for scheduling proof, main lemmas okLéo Gourdin2021-06-141-1/+1
* starting to extend RTLtoBTL with Liveness checking (on BTL side)Sylvain Boulmé2021-05-281-23/+40
* splitting BTL by introducing BTLmatchRTLSylvain Boulmé2021-05-281-34/+10
* fix some merge errorsLéo Gourdin2021-05-281-0/+1
* Merge branch 'BTL_fsem' into BTLLéo Gourdin2021-05-281-5/+5
|\
| * most of the proof BTL.fsem -> BTL.cfgsem.Sylvain Boulmé2021-05-281-2/+2
| * defines fsem (aka functional semantics) of BTLSylvain Boulmé2021-05-201-3/+3
* | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-05-271-258/+301
|\ \
| * | simplification of normRTLSylvain Boulmé2021-05-251-67/+27
| * | tiny simplifications in RTLtoBTLproofSylvain Boulmé2021-05-241-258/+341
* | | [disabled checker] BTL Scheduling and Renumbering OK!Léo Gourdin2021-05-271-2/+2
|/ /
* | splitting is_expand property with a weak version for conditionsLéo Gourdin2021-05-231-56/+58
* | Now supporting Bnop insertion in conditionsLéo Gourdin2021-05-211-92/+59
* | Changing to an opaq record in BTL info, this is a broken commitLéo Gourdin2021-05-201-6/+6
* | Adding a BTL record to help oraclesLéo Gourdin2021-05-191-1/+1
* | todosLéo Gourdin2021-05-181-1/+1
* | preparing compiler passes and ml oraclesLéo Gourdin2021-05-171-6/+5
|/
* finishing RTLtoBTLLéo Gourdin2021-05-171-23/+34
* mib lemmaLéo Gourdin2021-05-171-26/+29
* Lemmas on ISTEPLéo Gourdin2021-05-171-194/+126
* some advanceLéo Gourdin2021-05-161-24/+191
* iblock_istep rec and correct lemmasLéo Gourdin2021-05-131-0/+83
* ascii simuLéo Gourdin2021-05-121-17/+48
* finish proofLéo Gourdin2021-05-111-39/+45
* new lemma definition, some preparations in existing proofsLéo Gourdin2021-05-111-52/+65
* new strong_state predicate and lemmaLéo Gourdin2021-05-101-38/+72
* Some more proof cases, comments and cleanupLéo Gourdin2021-05-101-29/+96
* is_exp and bcond proofLéo Gourdin2021-05-101-18/+35
* Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-05-091-0/+2
|\
| * idee pour simplifier la preuve: restreindre le "right_assoc" en "expand" !Sylvain Boulmé2021-05-081-0/+2
* | mib_exit draftLéo Gourdin2021-05-091-3/+4
* | Some advance in proof and NOTRAP loads fixLéo Gourdin2021-05-071-4/+53
* | intermediate lemma for opt_simu intro caseLéo Gourdin2021-05-071-10/+21
|/
* a draft for the Bnop caseLéo Gourdin2021-05-071-11/+25
* proof OK for Call and Return statesLéo Gourdin2021-05-071-6/+21
* starting RTL->BTL proofLéo Gourdin2021-05-061-4/+46
* fix match_statesSylvain Boulmé2021-05-061-6/+8
* cleaner match_statesSylvain Boulmé2021-05-061-16/+21
* start RTL -> BTLSylvain Boulmé2021-05-061-0/+239
generated by cgit (git 2.34.1) at 2024-05-08 07:45:44 +0000