source: src/ASM @ 2121

Name Size Rev Age Author Last Change
../
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 21.7 KB ​ 2111   8 years sacerdot Cleanup: lemmas/theorems/axioms moved to the right places.
ASM.ma 16.1 KB ​ 2032   8 years sacerdot !! BEWARE: major commit !! 1) [affects everybody] split for …
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 41.4 KB ​ 2111   8 years sacerdot Cleanup: lemmas/theorems/axioms moved to the right places.
AssemblyProof.ma 57.6 KB ​ 2121   8 years sacerdot More functions moved to the places they belong to
AssemblyProofSplit.ma 54.6 KB ​ 2121   8 years sacerdot More functions moved to the places they belong to
AssemblyProofSplitSplit.ma 13.1 KB ​ 2110   8 years sacerdot …
BitVector.ma 6.8 KB ​ 2121   8 years sacerdot More functions moved to the places they belong to
BitVectorTrie.ma 25.7 KB ​ 2028   8 years boender - bugfix to Assembly (forgotten sigma) - added …
BitVectorZ.ma 4.0 KB ​ 1516   9 years sacerdot Ported to syntax of Matita 0.99.1.
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   9 years sacerdot utilities and ASM ported to the new standard library
Fetch.ma 25.8 KB ​ 2119   8 years sacerdot load_code_memory moved to Fetch.ma and proved correct w.r.t. next …
FoldStuff.ma 1.7 KB ​ 1600   9 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.3 KB ​ 2108   8 years mulligan Various axioms closed and others moved around. Uncommented main lemma …
Policy.ma 30.0 KB ​ 2101   8 years boender - renamed medium to absolute jump - revised proofs of policy, some …
PolicyFront.ma 30.6 KB ​ 2102   8 years boender - some small changes
PolicyStep.ma 42.8 KB ​ 2102   8 years boender - some small changes
README 641 bytes ​ 431   10 years mulligan - README updated - Test and DoTest? fixed to work on assembly_program - …
Status.ma 41.4 KB ​ 2119   8 years sacerdot load_code_memory moved to Fetch.ma and proved correct w.r.t. next …
StatusProofs.ma 13.4 KB ​ 2032   8 years sacerdot !! BEWARE: major commit !! 1) [affects everybody] split for …
String.ma 90 bytes ​ 1599   9 years sacerdot Start of merging of stuff into the standard library of Matita.
Util.ma 34.5 KB ​ 2111   8 years sacerdot Cleanup: lemmas/theorems/axioms moved to the right places.
UtilBranch.ma 2.2 KB ​ 1946   8 years sacerdot \snd half_add => add everywhere
Vector.ma 24.4 KB ​ 2121   8 years sacerdot More functions moved to the places they belong to
WellLabeled.ma 6.9 KB ​ 2032   8 years sacerdot !! BEWARE: major commit !! 1) [affects everybody] split for …
Note: See TracBrowser for help on using the repository browser.