|
../
|
|
CPP2011
|
|
1033
|
9 years
|
sacerdot |
ispelled & submitted
|
|
CPP2012-asm
|
|
2095
|
8 years
|
mulligan |
Added reference to CompCert? and CompCertTSO.
|
|
CPP2012-policy
|
|
2099
|
8 years
|
boender |
- added reference to Intel dev manual
|
|
AbstractStatus.ma
|
2.0 KB
|
1944
|
8 years
|
sacerdot |
common/StructuredTraces no longer depends on ASM/AbstractStatus (again)
|
|
Arithmetic.ma
|
24.3 KB
|
2192
|
8 years
|
sacerdot |
Shuffling around.
|
|
ASM.ma
|
31.3 KB
|
2143
|
8 years
|
mulligan |
Changes to the subaddressing mode elim functions moved into their …
|
|
ASMCosts.ma
|
35.4 KB
|
1964
|
8 years
|
tranquil |
introduced as_label_of_cost and adapted accordingly. Equality of cost …
|
|
ASMCostsSplit.ma
|
12.1 KB
|
2001
|
8 years
|
campbell |
Get the compiler to output more.
|
|
Assembly.ma
|
51.3 KB
|
2221
|
8 years
|
boender |
- removed cases daemon from PolicyFront?
|
|
AssemblyProof.ma
|
49.5 KB
|
2209
|
8 years
|
mulligan |
Closed major daemons in the supporting lemmas of the main lemma.
|
|
AssemblyProofSplit.ma
|
116.9 KB
|
2216
|
8 years
|
mulligan |
More work on the big lemma. Nearly there now.
|
|
AssemblyProofSplitSplit.ma
|
16.7 KB
|
2140
|
8 years
|
mulligan |
Done the hardest cases in the main theorem. Just got a few daemons to …
|
|
BitVector.ma
|
7.7 KB
|
2126
|
8 years
|
sacerdot |
Proof improved (for case 3) + new proof (for case 11)
|
|
BitVectorTrie.ma
|
25.7 KB
|
2028
|
8 years
|
boender |
- bugfix to Assembly (forgotten sigma)
- added …
|
|
BitVectorZ.ma
|
4.3 KB
|
2200
|
8 years
|
tranquil |
* updated joint semantics: generation of linear and graph semantics
* …
|
|
Char.ma
|
76 bytes
|
697
|
9 years
|
campbell |
Merge Clight branch of vectors and friends.
Start making stuff build.
|
|
CostsProof.ma
|
32.4 KB
|
2057
|
8 years
|
sacerdot |
Repaired (was broken by fetch_pseudo_instruction now taking a proof …
|
|
Erase.ma
|
3.5 KB
|
1600
|
8 years
|
sacerdot |
utilities and ASM ported to the new standard library
|
|
Fetch.ma
|
25.6 KB
|
2124
|
8 years
|
sacerdot |
Much more shuffling around to proper places
|
|
FoldStuff.ma
|
1.7 KB
|
1600
|
8 years
|
sacerdot |
utilities and ASM ported to the new standard library
|
|
I8051.ma
|
6.9 KB
|
1987
|
8 years
|
campbell |
Move BEValues to common to reflect their use in the memory model for …
|
|
I8051bis.ma
|
125 bytes
|
1415
|
9 years
|
sacerdot |
1. hwreg_store/retrieve no longer returns a res (but it is still …
|
|
Interpret2.ma
|
2.4 KB
|
1996
|
8 years
|
campbell |
Work on correctness from yesterday.
|
|
Interpret.ma
|
59.5 KB
|
2212
|
8 years
|
mulligan |
More work on the INC case
|
|
Policy.ma
|
34.4 KB
|
2230
|
8 years
|
sacerdot |
Glue proof maximally simplified or sort of.
|
|
PolicyFront.ma
|
31.9 KB
|
2235
|
8 years
|
sacerdot |
Towards smaller proofs.
|
|
PolicyStep.ma
|
59.0 KB
|
2239
|
8 years
|
sacerdot |
One more lemma polished.
|
|
README
|
641 bytes
|
431
|
9 years
|
mulligan |
- README updated
- Test and DoTest? fixed to work on assembly_program
- …
|
|
Status.ma
|
40.2 KB
|
2172
|
8 years
|
mulligan |
Moved new versions of get_ / set_arg_* into Status.ma. Commented out …
|
|
StatusProofs.ma
|
13.3 KB
|
2172
|
8 years
|
mulligan |
Moved new versions of get_ / set_arg_* into Status.ma. Commented out …
|
|
StatusProofsSplit.ma
|
28.6 KB
|
2172
|
8 years
|
mulligan |
Moved new versions of get_ / set_arg_* into Status.ma. Commented out …
|
|
String.ma
|
90 bytes
|
1599
|
8 years
|
sacerdot |
Start of merging of stuff into the standard library of Matita.
|
|
Test.ma
|
55.2 KB
|
2207
|
8 years
|
mulligan |
Improvements and corrections to the main lemma proof in …
|
|
Util.ma
|
41.2 KB
|
2211
|
8 years
|
boender |
- finished proof of sigma specification
- added some stuff to Util, as …
|
|
UtilBranch.ma
|
2.2 KB
|
1946
|
8 years
|
sacerdot |
\snd half_add => add everywhere
|
|
Vector.ma
|
24.6 KB
|
2124
|
8 years
|
sacerdot |
Much more shuffling around to proper places
|
|
WellLabeled.ma
|
6.9 KB
|
2032
|
8 years
|
sacerdot |
!! BEWARE: major commit !!
1) [affects everybody]
split for …
|
