Commit message (Expand) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
* | | | | | Some more progress | Cyril SIX | 2020-09-29 | 1 | -2/+33 | |
* | | | | | Bit of progress | Cyril SIX | 2020-09-29 | 1 | -6/+40 | |
* | | | | | Proof of simplify_correct | Cyril SIX | 2020-09-28 | 1 | -45/+101 | |
* | | | | | A bit of new Ltac and renaming | Cyril SIX | 2020-09-21 | 1 | -23/+70 | |
* | | | | | More avancement | Cyril SIX | 2020-09-18 | 1 | -3/+29 | |
* | | | | | hsiexec_inst_correct_dyn proof of Iop | Cyril SIX | 2020-09-18 | 1 | -1/+42 | |
* | | | | | Avancement | Cyril SIX | 2020-09-18 | 1 | -29/+83 | |
* | | | | | Some renaming | Cyril SIX | 2020-09-18 | 1 | -129/+230 | |
* | | | | | Proof of sfval_simu_check_correct | Cyril SIX | 2020-09-15 | 1 | -14/+132 | |
* | | | | | Cleanup | Cyril SIX | 2020-09-09 | 1 | -4/+1 | |
* | | | | | exec_final_correct proved | Cyril SIX | 2020-09-09 | 1 | -22/+122 | |
* | | | | | Proving the last admit of ssem_final_simu | Cyril SIX | 2020-09-08 | 1 | -2/+24 | |
* | | | | | hsexec_final_correct progress | Cyril SIX | 2020-09-07 | 1 | -2/+30 | |
* | | | | | Proof of hfinal_simu_core_correct | Cyril SIX | 2020-09-07 | 4 | -35/+21 | |
* | | | | | Proof of barg_proj_refines_eq | Cyril SIX | 2020-09-07 | 1 | -5/+43 | |
* | | | | | Updates from _impl.v to _impl_junk.v | Cyril SIX | 2020-09-03 | 1 | -55/+102 | |
* | | | | | Proof of hsilocal_simu_core_correct junk | Cyril SIX | 2020-09-03 | 1 | -14/+16 | |
* | | | | | More proofs | Cyril SIX | 2020-09-03 | 1 | -8/+32 | |
* | | | | | Proof of may_trap_correct | Cyril SIX | 2020-09-01 | 1 | -2/+15 | |
* | | | | | Simplificating hsiexit_refines_stat | Cyril SIX | 2020-09-01 | 1 | -7/+4 | |
* | | | | | Proof of hsistate_simu_core_correct | Cyril SIX | 2020-09-01 | 1 | -6/+30 | |
* | | | | | SUCCESS: prouve 1 des admit de hsistate_simu_core_correct. | Sylvain Boulmé | 2020-08-28 | 1 | -14/+13 | |
* | | | | | add nested_sok in hsistate_refines_dyn | Sylvain Boulmé | 2020-08-28 | 1 | -35/+63 | |
* | | | | | more realistic ok_allexit. | Sylvain Boulmé | 2020-08-27 | 1 | -5/+5 | |
* | | | | | reduction de la preuve de raffinement du exit à ok_allexit | Sylvain Boulmé | 2020-08-27 | 2 | -54/+81 | |
|/ / / / | ||||||
* | | | | proof of lemma hslocal_set_sreg_correct | Sylvain Boulmé | 2020-08-26 | 1 | -46/+64 | |
* | | | | simplification of hsilocal_refines | Sylvain Boulmé | 2020-08-26 | 1 | -20/+15 | |
* | | | | starting hslocal_set_sreg_correct | Sylvain Boulmé | 2020-08-26 | 1 | -9/+31 | |
* | | | | Comment change | Cyril SIX | 2020-08-26 | 1 | -1/+1 | |
* | | | | Merge branch 'mppa-RTLpathSE-verif' of gricad-gitlab.univ-grenoble-alpes.fr:s... | Sylvain Boulmé | 2020-08-26 | 4 | -34/+183 | |
|\ \ \ \ | ||||||
| * | | | | Avancement divers | Cyril SIX | 2020-08-26 | 4 | -34/+183 | |
* | | | | | fix statement of hslocal_set_sreg_correct ? | Sylvain Boulmé | 2020-08-26 | 1 | -6/+7 | |
|/ / / / | ||||||
* | | | | simplify hsi_lsmem into hsi_smem | Sylvain Boulmé | 2020-08-26 | 1 | -67/+57 | |
* | | | | Start of hfinal_simu_core_correct | Cyril SIX | 2020-08-25 | 1 | -18/+48 | |
* | | | | hfinal_refines depend on ge, sp, rs0, m0 | Cyril SIX | 2020-08-25 | 1 | -17/+81 | |
* | | | | Down to hsexec_final_correct | Cyril SIX | 2020-08-24 | 1 | -47/+116 | |
* | | | | Simpler hypothesis | Cyril SIX | 2020-08-24 | 1 | -13/+10 | |
* | | | | Avancement sur simu_check_single_correct | Cyril SIX | 2020-08-24 | 1 | -1/+50 | |
* | | | | Avancement | Cyril SIX | 2020-08-21 | 1 | -11/+508 | |
* | | | | Started to port the properties from RTLpathSE_impl.v | Cyril SIX | 2020-08-20 | 1 | -10/+230 | |
* | | | | Merge remote-tracking branch 'origin/mppa-RTLpathSE-verif-hash-junk' into mpp... | Cyril SIX | 2020-08-19 | 18 | -213/+1645 | |
|\ \ \ \ | | |/ / | |/| | | ||||||
| * | | | Merge remote-tracking branch 'origin/kvx-work' into mppa-RTLpathSE-verif-hash... | David Monniaux | 2020-07-30 | 7 | -165/+140 | |
| |\ \ \ | | |/ / | |/| / | | |/ | ||||||
| | * | Improving the coqdoc | Sylvain Boulmé | 2020-07-29 | 7 | -165/+140 | |
| * | | trace quand le simulateur est appele | Sylvain Boulmé | 2020-07-24 | 1 | -2/+3 | |
| * | | Merge branch 'mppa-RTLpathSE-oracle' into mppa-RTLpathSE-verif-hash-junk | Cyril SIX | 2020-07-24 | 9 | -47/+768 | |
| |\ \ | ||||||
| | * | | More robust code for changing order of instructions | Cyril SIX | 2020-07-20 | 1 | -43/+118 | |
| | * | | Fixed last instruction not having liveins | Cyril SIX | 2020-07-15 | 1 | -2/+8 | |
| | * | | More debug info | Cyril SIX | 2020-07-15 | 1 | -8/+17 | |
| | * | | Merge branch 'mppa-RTLpathSE-oracle' of gricad-gitlab.univ-grenoble-alpes.fr:... | David Monniaux | 2020-07-13 | 1 | -3/+13 | |
| | |\ \ | ||||||
| | | * | | Fix switching basic instruction with Icond | Cyril SIX | 2020-07-13 | 1 | -3/+13 |