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
/
lib
Commit message (
Expand
)
Author
Age
Files
Lines
*
fixing the move of the verified prepass scheduler into scheduling/ directory
Sylvain Boulmé
2020-10-17
1
-872
/
+0
*
Merge remote-tracking branch 'origin/kvx-test-prepass' into mppa-RTLpathSE-verif
Cyril SIX
2020-10-16
15
-7426
/
+98
|
\
|
*
simpl -> cbn
David Monniaux
2020-09-29
4
-98
/
+98
*
|
removing useless opt_simu
Sylvain Boulmé
2020-10-13
3
-36
/
+25
*
|
refactoring of RTLpathSE_impl.v (split with _simu_specs)
Sylvain Boulmé
2020-10-13
5
-3911
/
+2086
*
|
remove the last tiny issue!
Sylvain Boulmé
2020-10-12
1
-10
/
+3
*
|
simpl hsstate_simu_core_correct
Sylvain Boulmé
2020-10-12
1
-3
/
+1
*
|
fix one issue by generalizing RTLpathSE_theory.sstate_simu
Sylvain Boulmé
2020-10-12
2
-9
/
+18
*
|
move issue from hsexec_correct to hsstate_simu_core_correct
Sylvain Boulmé
2020-10-12
1
-14
/
+19
*
|
most of the proof is done ! two (small ?) issues remain...
Sylvain Boulmé
2020-10-12
1
-30
/
+83
*
|
oops: forget to save before compile/commit/push
Sylvain Boulmé
2020-10-12
1
-2
/
+5
*
|
end of merge with Cyril's proof
Sylvain Boulmé
2020-10-12
2
-59
/
+227
*
|
starting to merge with Cyril's proof
Sylvain Boulmé
2020-10-11
1
-48
/
+773
*
|
hconsing: full proof of hsiexec_path_correct
Sylvain Boulmé
2020-10-10
2
-42
/
+71
*
|
progress on hslocal_set_sreg_correct
Sylvain Boulmé
2020-10-10
1
-37
/
+53
*
|
progress on hsexec_inst_correct_dyn
Sylvain Boulmé
2020-10-10
1
-39
/
+140
*
|
hconsing: red_PTree_set_correct
Sylvain Boulmé
2020-10-09
1
-0
/
+11
*
|
hconsing: root_happly_correct + simplify_correct DONE
Sylvain Boulmé
2020-10-09
4
-15
/
+145
*
|
prove the kvx-test-prepass fix (commit 0e4186b8f)
Sylvain Boulmé
2020-10-08
1
-14
/
+58
*
|
Merge branch 'mppa-RTLpathSE-verif_Op_mem-irrel' into mppa-RTLpathSE-xverif
Sylvain Boulmé
2020-10-08
1
-30
/
+29
|
\
\
|
*
|
prove the trick of simplify (as implemented in RTLpathSE_impl_junk)
Sylvain Boulmé
2020-08-27
1
-18
/
+6
|
*
|
prove that Mem.valid is preserved by symbolic execution of RTLpath
Sylvain Boulmé
2020-08-27
1
-12
/
+22
*
|
|
Restart the proof with cherry-pick from Cyril and commit 0e4186b8f
Sylvain Boulmé
2020-10-08
2
-1795
/
+433
*
|
|
Some theorem was wrong
Cyril SIX
2020-09-30
1
-4
/
+18
*
|
|
Proof of hsok_local_set_sreg
Cyril SIX
2020-09-30
1
-4
/
+25
*
|
|
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
|
/
/
[next]