aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmblock.v
Commit message (Expand)AuthorAgeFilesLines
* Déterminisme prouvé -> Tout est prouvéCyril SIX2018-11-081-1/+59
* Proved non_empty_bblock_refl (was Admitted)Cyril SIX2018-11-081-4/+4
* Changing exec_straight to allow all instructions (prepare for MBtailcall proof)Cyril SIX2018-10-261-0/+35
* Adding "proof irrelevance" to bblocksCyril SIX2018-10-251-15/+49
* MBsetstack done!Cyril SIX2018-10-241-2/+2
* step_simulation_bblock is back!Cyril SIX2018-10-241-1/+1
* ajoute un axiom a virer plus tardSylvain Boulmé2018-10-231-1/+7
* Un peu d'avancement dans exec_straight_control et cieCyril SIX2018-10-081-13/+12
* Fini le cas du step_simu_control où il n'y a pas de exitCyril SIX2018-10-041-14/+9
* Schéma de simulation + les Pnop sont maintenant implicitesCyril SIX2018-10-031-8/+22
* Removed the bundle attemptCyril SIX2018-09-281-47/+7
* Enlèvement du "no_builtin" condition; exec_control sur les option control; e...Cyril SIX2018-09-261-12/+25
* AB: removing bregsCyril SIX2018-09-261-68/+37
* MB2AB - un peu d'avancement sur internal functionCyril SIX2018-09-251-8/+6
* MB2AB - Proof of external function stepCyril SIX2018-09-251-7/+7
* relectureSylvain Boulmé2018-09-241-1/+3
* a few stubs for bundlingSylvain Boulmé2018-09-241-194/+0
* one step toward "bundle_step"Sylvain Boulmé2018-09-241-6/+55
* Asmblock -> Asm presque fini.. erreur sur driver/Compiler.vCyril SIX2018-09-061-249/+259
* Asmblockgen: Added Pnop and Program DefinitionsCyril SIX2018-09-061-38/+7
* Example of Program use...Sylvain Boulmé2018-09-061-0/+16
* Asmblock: Adding forward_simulation and determinism as axiomsCyril SIX2018-09-061-0/+2
* Asmblockgen.v finished (no proof yet)Cyril SIX2018-09-061-15/+46
* Changements mineurs Asmblock.v + draft de Asmblockgen.v à compléterCyril SIX2018-09-061-12/+42
* deplacement allocframe/freeframe/loadsymbolSylvain Boulmé2018-09-061-41/+37
* Name changing + introducing Pbuiltin (alone in a block)Cyril SIX2018-09-061-91/+67
* Some renaming on asmblockCyril SIX2018-09-061-11/+11
* add comments (TODO/FIXME)Sylvain Boulmé2018-09-061-11/+28
* notation changeSylvain Boulmé2018-09-061-21/+21
* a version of Asmblock syntax and semanticsSylvain Boulmé2018-09-061-0/+1376
generated by cgit (git 2.34.1) at 2024-07-06 17:21:03 +0000