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
/
aarch64
/
Asmblockdeps.v
Commit message (
Expand
)
Author
Age
Files
Lines
*
Adding fp stores pair
Léo Gourdin
2021-01-20
1
-6
/
+12
*
Adding fp loads pair
Léo Gourdin
2021-01-20
1
-13
/
+30
*
Val_cmp* -> Val.mxcmp*
Sylvain Boulmé
2021-01-07
1
-6
/
+6
*
Fix the Asmblock/Asm proof
Léo Gourdin
2020-12-20
1
-7
/
+7
*
Merge branch 'kvx-work' into aarch64-peephole
Sylvain Boulmé
2020-12-17
1
-1
/
+3
*
Big improvment in peephole, changing LDP/STP semantics
Léo Gourdin
2020-12-10
1
-92
/
+110
*
Asmgen proof completely proved with ldp/stp
Léo Gourdin
2020-12-06
1
-2
/
+3
*
a first working draft on ldp/stp peephole
Léo Gourdin
2020-12-04
1
-52
/
+227
*
Adding semantics for Pldp
Léo Gourdin
2020-12-02
1
-33
/
+38
*
Some optimizations again
Léo Gourdin
2020-11-28
1
-27
/
+30
*
Optimizing Asmblockdeps proof
Léo Gourdin
2020-11-28
1
-58
/
+92
*
Proof of Pfmovimm fine tuned OK, moving float checks in Asm
Léo Gourdin
2020-11-26
1
-240
/
+96
*
Fine tuning for Pfmovimm
Léo Gourdin
2020-11-26
1
-3
/
+5
*
Main part of postpasssch proof now completed
Léo Gourdin
2020-11-24
1
-1
/
+1
*
Asmblockdeps is now finished
Léo Gourdin
2020-11-24
1
-226
/
+42
*
Start of the postpasschedproof, redefining verify schedule lemmas
Léo Gourdin
2020-11-23
1
-36
/
+42
*
a step forward in bblock_simu_reduce
Sylvain Boulmé
2020-11-23
1
-40
/
+34
*
Trying to finish the bisimu reduce proof for builtin (last case admitted)
Léo Gourdin
2020-11-20
1
-29
/
+76
*
draft of the exec_bblock Asmblockdeps proof
Léo Gourdin
2020-11-20
1
-29
/
+116
*
Postpass scheduling OK
Léo Gourdin
2020-11-18
1
-164
/
+29
*
Merge remote-tracking branch 'origin/aarch64-postpass' into aarch64-postpass
Léo Gourdin
2020-11-17
1
-7
/
+56
|
\
|
*
extend the aarch64 scheduling verifier to check builtins.
Sylvain Boulmé
2020-11-17
1
-7
/
+56
*
|
Builtin mem spec in scheduler and some needed proof in Postpasssch.v
Léo Gourdin
2020-11-17
1
-2
/
+2
|
/
*
Remaining ctl insts except Pbuiltin (maps to error)
Léo Gourdin
2020-11-16
1
-369
/
+493
*
Lemma for bisimu with potential builtins, alloc and constant
Léo Gourdin
2020-11-13
1
-65
/
+132
*
Loads and stores op
Léo Gourdin
2020-11-13
1
-5
/
+203
*
Arith inst OK for the verifier
Léo Gourdin
2020-11-12
1
-61
/
+191
*
Finishing PArith cases in abb, and linking the pass to compile
Léo Gourdin
2020-11-11
1
-387
/
+479
*
PArithCmpR0R in checker
Léo Gourdin
2020-11-11
1
-36
/
+130
*
PArithComparison special lemmas and adaptations
Léo Gourdin
2020-11-10
1
-17
/
+315
*
Simplifications using ltacs and XZR special case
Léo Gourdin
2020-11-10
1
-33
/
+150
*
First version of the oracle checker, does not compile yet
Léo Gourdin
2020-11-09
1
-832
/
+576
*
Preparation for postpass in aarch64 and refactoring
Léo Gourdin
2020-11-02
1
-0
/
+1841