index
:
compcert-kvx
CPP22_if_lifting
CPP22_main
master
patched_for_velus
riscV-cmov
ssa
vericert
vericert-kvx
Unnamed repository; edit this file 'description' to name the repository.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
path:
root
/
kvx
Commit message (
Expand
)
Author
Age
Files
Lines
*
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
|
|
*
|
|
Merge branch 'mppa-RTLpathSE-oracle' of gricad-gitlab.univ-grenoble-alpes.fr:...
David Monniaux
2020-07-13
1
-1
/
+6
|
|
|
\
|
|
|
|
|
*
|
Fix Icond bug
Cyril SIX
2020-07-13
1
-1
/
+6
[next]