source: src/ASM @ 2284

Name Size Rev Age Author Last Change
../
CPP2011 1033   8 years sacerdot ispelled & submitted
CPP2012-asm 2095   7 years mulligan Added reference to CompCert? and CompCertTSO.
CPP2012-policy 2099   7 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   7 years sacerdot Shuffling around.
ASM.ma 31.3 KB ​ 2143   7 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   7 years campbell Get the compiler to output more.
Assembly.ma 48.0 KB ​ 2268   7 years mulligan Bug spotted in instruction_size (lookup_datalabels cannot just be a …
AssemblyProof.ma 62.0 KB ​ 2284   7 years sacerdot PUSH finished
AssemblyProofSplit.ma 117.7 KB ​ 2284   7 years sacerdot PUSH finished
AssemblyProofSplitSplit.ma 15.5 KB ​ 2278   7 years mulligan Half of JC case complete
BitVector.ma 7.7 KB ​ 2126   7 years sacerdot Proof improved (for case 3) + new proof (for case 11)
BitVectorTrie.ma 25.7 KB ​ 2028   7 years boender - bugfix to Assembly (forgotten sigma) - added …
BitVectorZ.ma 4.3 KB ​ 2200   7 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   7 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 32.4 KB ​ 2264   7 years sacerdot 1) Major change: we now always use the efficient way of resolving …
FoldStuff.ma 1.7 KB ​ 1600   8 years sacerdot utilities and ASM ported to the new standard library
I8051.ma 6.4 KB ​ 2275   7 years tranquil * moved around some code (I8051.ma does not depend on ByteValues?.ma …
I8051bis.ma 125 bytes ​ 1415   8 years sacerdot 1. hwreg_store/retrieve no longer returns a res (but it is still …
Interpret2.ma 2.4 KB ​ 1996   7 years campbell Work on correctness from yesterday.
Interpret.ma 58.9 KB ​ 2283   7 years mulligan Work from today.
Policy.ma 34.3 KB ​ 2264   7 years sacerdot 1) Major change: we now always use the efficient way of resolving …
PolicyFront.ma 31.7 KB ​ 2273   7 years sacerdot 1. lemmas moved from all files to Test.ma 2. most of the lemmas in …
PolicyStep.ma 58.6 KB ​ 2264   7 years sacerdot 1) Major change: we now always use the efficient way of resolving …
README 641 bytes ​ 431   9 years mulligan - README updated - Test and DoTest? fixed to work on assembly_program - …
Status.ma 38.3 KB ​ 2272   7 years mulligan Changed proof strategy for main lemma after noticed that the current …
StatusProofs.ma 13.4 KB ​ 2272   7 years mulligan Changed proof strategy for main lemma after noticed that the current …
StatusProofsSplit.ma 20.7 KB ​ 2274   7 years sacerdot Dead code commented out and code out of place moved to Test.ma.
String.ma 90 bytes ​ 1599   8 years sacerdot Start of merging of stuff into the standard library of Matita.
Test.ma 92.8 KB ​ 2284   7 years sacerdot PUSH finished
Util.ma 41.2 KB ​ 2211   7 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   7 years sacerdot Much more shuffling around to proper places
WellLabeled.ma 6.9 KB ​ 2032   7 years sacerdot !! BEWARE: major commit !! 1) [affects everybody] split for …
Note: See TracBrowser for help on using the repository browser.