aboutsummaryrefslogtreecommitdiffstats
path: root/kvx
Commit message (Expand)AuthorAgeFilesLines
* Characterizing Op dependency on memorySylvain Boulmé2020-07-081-0/+39
* AvancementCyril SIX2020-07-072-88/+290
* ssem_final with less dependenciesCyril SIX2020-07-061-11/+14
* init_hsistate_correctCyril SIX2020-07-061-5/+29
* Version without dependency on rs0, m0, ge and sp ?Cyril SIX2020-07-031-44/+60
* Scope issue..Cyril SIX2020-07-031-11/+12
* Fixing ge, sp, rs, m issueCyril SIX2020-07-031-8/+9
* fix the proof sketchSylvain Boulmé2020-07-031-30/+22
* sketch the proof of symbolic execution of one instructionSylvain Boulmé2020-07-032-35/+68
* slightly simpler codeSylvain Boulmé2020-07-021-64/+88
* Optimization of Iop symbolic executionSylvain Boulmé2020-07-022-35/+107
* Fix hypothesis on environment in hsstate_simuSylvain Boulmé2020-07-021-3/+4
* remove useless (and unprovable) lemmas on completeness of the refinementSylvain Boulmé2020-07-021-47/+66
* Avancement, mais est-ce prouvable ?Cyril SIX2020-07-011-0/+37
* hsexec_completeCyril SIX2020-07-011-37/+36
* AvancementCyril SIX2020-07-012-74/+120
* hsexec_correctCyril SIX2020-07-012-27/+138
* Some renamingCyril SIX2020-07-011-38/+49
* a minor commentSylvain Boulmé2020-06-301-2/+2
* starting refinement of (abstract) symbolic executionsSylvain Boulmé2020-06-301-0/+160
* Must generalize silocal_simub with a list of regsCyril SIX2020-06-291-3/+5
* Only silocal_simub leftCyril SIX2020-06-291-132/+171
* sfval_simub_correctCyril SIX2020-06-291-6/+175
* Going further in sfval_simubCyril SIX2020-06-291-6/+60
* sval_simub + sval_simub_correctCyril SIX2020-06-291-9/+51
* Start of sval_simubCyril SIX2020-06-251-3/+93
* Proving small lemmasCyril SIX2020-06-251-6/+33
* Proof of sistate_simub_correct with smaller admitted lemmasCyril SIX2020-06-241-55/+45
* Some progressCyril SIX2020-06-241-2/+52
* Fixing sistate_simub_correct ; no need for injectionCyril SIX2020-06-233-29/+20
* Reverting injectivity ?Cyril SIX2020-06-231-8/+9
* Modification on istate_simu to go further in the proof of sistate_simub_correctCyril SIX2020-06-223-10/+46
* Start of sistate_simub_correctCyril SIX2020-06-221-5/+54
* Splitting sistate_simubCyril SIX2020-06-221-2/+72
* Proof of sexec_exactCyril SIX2020-06-191-3/+3
* Proof of 2nd admitted of sexec_exactCyril SIX2020-06-191-3/+99
* Fix typoCyril SIX2020-06-181-5/+5
* sfmatch -> sstep_final ; smatch -> ssemCyril SIX2020-06-182-36/+36
* ssem --> ssem_internalCyril SIX2020-06-182-64/+64
* sfstep -> sexec_finalCyril SIX2020-06-181-8/+8
* Renaming sstep -> sexec ; sistep -> siexec_inst ; sisteps -> siexec_pathCyril SIX2020-06-183-92/+92
* fix comments ?Sylvain Boulmé2020-06-181-3/+4
* 1 cas sur 3 (le seul non absurde ?)Sylvain Boulmé2020-06-171-5/+30
* Stuck in sstep_exactCyril SIX2020-06-171-2/+6
* Sbuiltin in sfmatch_simuCyril SIX2020-06-162-4/+44
* sfmatch_simu: Stailcall and SjumptableCyril SIX2020-06-122-3/+49
* Augmenting sfval_simu ; some corrections to do in sfmatch_simuCyril SIX2020-06-122-21/+39
* Beginning of sstate_simubCyril SIX2020-06-122-32/+57
* Proof down to sstate_simub and sstate_simub_correctCyril SIX2020-06-111-5/+25
* Restructuring code to allow tf in simu_check_singleCyril SIX2020-06-111-71/+56
generated by cgit (git 2.34.1) at 2024-06-02 19:12:35 +0000