aboutsummaryrefslogtreecommitdiffstats
path: root/kvx
Commit message (Expand)AuthorAgeFilesLines
...
| * | | | | | | | | | 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
| * | | | | | | | | Merge remote-tracking branch 'origin/mppa-RTLpathSE-verif-hash-junk' into mpp...Cyril SIX2020-08-1918-213/+1645
| |\ \ \ \ \ \ \ \ \ | | | |/ / / / / / / | | |/| | | | | | |
| | * | | | | | | | Merge remote-tracking branch 'origin/kvx-work' into mppa-RTLpathSE-verif-hash...David Monniaux2020-07-307-165/+140
| | |\ \ \ \ \ \ \ \ | | | |/ / / / / / / | | |/| | | | | | |
| | * | | | | | | | trace quand le simulateur est appeleSylvain Boulmé2020-07-241-2/+3
| | * | | | | | | | Merge branch 'mppa-RTLpathSE-oracle' into mppa-RTLpathSE-verif-hash-junkCyril SIX2020-07-249-47/+768
| | |\ \ \ \ \ \ \ \
| | | * | | | | | | | More robust code for changing order of instructionsCyril SIX2020-07-201-43/+118
| | | * | | | | | | | Fixed last instruction not having liveinsCyril SIX2020-07-151-2/+8
| | | * | | | | | | | More debug infoCyril SIX2020-07-151-8/+17
| | | * | | | | | | | Merge branch 'mppa-RTLpathSE-oracle' of gricad-gitlab.univ-grenoble-alpes.fr:...David Monniaux2020-07-131-3/+13
| | | |\ \ \ \ \ \ \ \
generated by cgit (git 2.34.1) at 2024-07-04 02:23:31 +0000