source: src/ASM @ 2005

Name Size Rev Age Author Last Change
../
CPP2011 1033   8 years sacerdot ispelled & submitted
SEFM2012 1889   7 years boender - some pages of article
AbstractStatus.ma 2.0 KB 1944   7 years sacerdot common/StructuredTraces no longer depends on ASM/AbstractStatus (again)
Arithmetic.ma 17.8 KB 1963   7 years sacerdot More progress in restoring the original proof.
ASM.ma 9.0 KB 1882   8 years tranquil big update, alas incomplete: joint changed a bit, and all BE languages …
ASMCosts.ma 35.4 KB 1964   7 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 56.3 KB 2005   7 years boender - minor changes to make things compile with a clean checkout
AssemblyProof.ma 76.4 KB 1984   7 years mulligan Most proof obligations closed in main_lemma apart from those of the …
AssemblyProofSplit.ma 69.9 KB 1985   7 years mulligan A single `false' case for unconditional jumps completed.
BitVector.ma 6.7 KB 1928   7 years mulligan Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should …
BitVectorTrie.ma 24.3 KB 1931   7 years boender - added latest bvt alias - temporary "cases daemon" commit of new …
BitVectorZ.ma 4.0 KB 1516   8 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 33.0 KB 2001   7 years campbell Get the compiler to output more.
Erase.ma 3.5 KB 1600   8 years sacerdot utilities and ASM ported to the new standard library
Fetch.ma 23.6 KB 1961   7 years sacerdot No more interaction required.
FoldStuff.ma 1.7 KB 1600   8 years sacerdot utilities and ASM ported to the new standard library
I8051.ma 6.9 KB 1987   7 years campbell Move BEValues to common to reflect their use in the memory model for …
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 69.9 KB 1971   7 years sacerdot 1. Interpret.ma: we need to prove \sigma (execute_preinstruction …
Policy.ma 66.6 KB 1973   7 years boender - removed superfluous match - displaced 'cases daemon'
README 641 bytes 431   9 years mulligan - README updated - Test and DoTest? fixed to work on assembly_program - …
Status.ma 40.3 KB 1946   7 years sacerdot \snd half_add => add everywhere
StatusProofs.ma 13.4 KB 1962   7 years sacerdot More examples are now indexed.
String.ma 90 bytes 1599   8 years sacerdot Start of merging of stuff into the standard library of Matita.
Util.ma 33.1 KB 2005   7 years boender - minor changes to make things compile with a clean checkout
UtilBranch.ma 2.2 KB 1946   7 years sacerdot \snd half_add => add everywhere
Vector.ma 17.8 KB 1908   7 years fguidi notation fixup following last commit of matita we shifted the levels …
WellLabeled.ma 6.9 KB 1494   8 years mulligan changes to get everything compiling again
Note: See TracBrowser for help on using the repository browser.