aboutsummaryrefslogtreecommitdiffstats
path: root/kvx/lib
Commit message (Expand)AuthorAgeFilesLines
* progress on hsexec_inst_correct_dynSylvain Boulmé2020-10-101-39/+140
* hconsing: red_PTree_set_correctSylvain Boulmé2020-10-091-0/+11
* hconsing: root_happly_correct + simplify_correct DONESylvain Boulmé2020-10-094-15/+145
* prove the kvx-test-prepass fix (commit 0e4186b8f)Sylvain Boulmé2020-10-081-14/+58
* Merge branch 'mppa-RTLpathSE-verif_Op_mem-irrel' into mppa-RTLpathSE-xverifSylvain Boulmé2020-10-081-30/+29
|\
| * prove the trick of simplify (as implemented in RTLpathSE_impl_junk)Sylvain Boulmé2020-08-271-18/+6
| * prove that Mem.valid is preserved by symbolic execution of RTLpathSylvain Boulmé2020-08-271-12/+22
* | Restart the proof with cherry-pick from Cyril and commit 0e4186b8fSylvain Boulmé2020-10-082-1795/+433
* | Some theorem was wrongCyril SIX2020-09-301-4/+18
* | Proof of hsok_local_set_sregCyril SIX2020-09-301-4/+25
* | Some more progressCyril SIX2020-09-291-2/+33
* | Bit of progressCyril SIX2020-09-291-6/+40
* | Proof of simplify_correctCyril SIX2020-09-281-45/+101
* | A bit of new Ltac and renamingCyril SIX2020-09-211-23/+70
* | More avancementCyril SIX2020-09-181-3/+29
* | hsiexec_inst_correct_dyn proof of IopCyril SIX2020-09-181-1/+42
* | AvancementCyril SIX2020-09-181-29/+83
* | Some renamingCyril SIX2020-09-181-129/+230
* | Proof of sfval_simu_check_correctCyril SIX2020-09-151-14/+132
* | CleanupCyril SIX2020-09-091-4/+1
* | exec_final_correct provedCyril SIX2020-09-091-22/+122
* | Proving the last admit of ssem_final_simuCyril SIX2020-09-081-2/+24
* | hsexec_final_correct progressCyril SIX2020-09-071-2/+30
* | Proof of hfinal_simu_core_correctCyril SIX2020-09-074-35/+21
* | Proof of barg_proj_refines_eqCyril SIX2020-09-071-5/+43
* | Updates from _impl.v to _impl_junk.vCyril SIX2020-09-031-55/+102
* | Proof of hsilocal_simu_core_correct junkCyril SIX2020-09-031-14/+16
* | More proofsCyril SIX2020-09-031-8/+32
* | Proof of may_trap_correctCyril SIX2020-09-011-2/+15
* | Simplificating hsiexit_refines_statCyril SIX2020-09-011-7/+4
* | Proof of hsistate_simu_core_correctCyril SIX2020-09-011-6/+30
* | SUCCESS: prouve 1 des admit de hsistate_simu_core_correct.Sylvain Boulmé2020-08-281-14/+13
* | add nested_sok in hsistate_refines_dynSylvain Boulmé2020-08-281-35/+63
* | more realistic ok_allexit.Sylvain Boulmé2020-08-271-5/+5
* | reduction de la preuve de raffinement du exit à ok_allexitSylvain Boulmé2020-08-272-54/+81
|/
* proof of lemma hslocal_set_sreg_correctSylvain Boulmé2020-08-261-46/+64
* simplification of hsilocal_refinesSylvain Boulmé2020-08-261-20/+15
* starting hslocal_set_sreg_correctSylvain Boulmé2020-08-261-9/+31
* Comment changeCyril SIX2020-08-261-1/+1
* Merge branch 'mppa-RTLpathSE-verif' of gricad-gitlab.univ-grenoble-alpes.fr:s...Sylvain Boulmé2020-08-264-34/+183
|\
| * Avancement diversCyril SIX2020-08-264-34/+183
* | fix statement of hslocal_set_sreg_correct ?Sylvain Boulmé2020-08-261-6/+7
|/
* simplify hsi_lsmem into hsi_smemSylvain Boulmé2020-08-261-67/+57
* Start of hfinal_simu_core_correctCyril SIX2020-08-251-18/+48
* hfinal_refines depend on ge, sp, rs0, m0Cyril SIX2020-08-251-17/+81
* Down to hsexec_final_correctCyril SIX2020-08-241-47/+116
* Simpler hypothesisCyril SIX2020-08-241-13/+10
* Avancement sur simu_check_single_correctCyril SIX2020-08-241-1/+50
* AvancementCyril SIX2020-08-211-11/+508
* Started to port the properties from RTLpathSE_impl.vCyril SIX2020-08-201-10/+230
generated by cgit (git 2.34.1) at 2024-07-12 03:45:18 +0000