source: src/ASM @ 2261

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
Char.ma 76 bytes 697   9 years campbell Merge Clight branch of vectors and friends. Start making stuff build.
String.ma 90 bytes 1599   8 years sacerdot Start of merging of stuff into the standard library of Matita.
I8051bis.ma 125 bytes 1415   8 years sacerdot 1. hwreg_store/retrieve no longer returns a res (but it is still …
README 641 bytes 431   9 years mulligan - README updated - Test and DoTest? fixed to work on assembly_program - …
FoldStuff.ma 1.7 KB 1600   8 years sacerdot utilities and ASM ported to the new standard library
AbstractStatus.ma 2.0 KB 1944   8 years sacerdot common/StructuredTraces no longer depends on ASM/AbstractStatus (again)
UtilBranch.ma 2.2 KB 1946   8 years sacerdot \snd half_add => add everywhere
Interpret2.ma 2.4 KB 1996   8 years campbell Work on correctness from yesterday.
Erase.ma 3.5 KB 1600   8 years sacerdot utilities and ASM ported to the new standard library
BitVectorZ.ma 4.3 KB 2200   7 years tranquil * updated joint semantics: generation of linear and graph semantics * …
I8051.ma 6.9 KB 1987   8 years campbell Move BEValues to common to reflect their use in the memory model for …
WellLabeled.ma 6.9 KB 2032   8 years sacerdot !! BEWARE: major commit !! 1) [affects everybody] split for …
BitVector.ma 7.7 KB 2126   7 years sacerdot Proof improved (for case 3) + new proof (for case 11)
ASMCostsSplit.ma 12.1 KB 2001   8 years campbell Get the compiler to output more.
StatusProofs.ma 13.3 KB 2172   7 years mulligan Moved new versions of get_ / set_arg_* into Status.ma. Commented out …
AssemblyProofSplitSplit.ma 16.7 KB 2140   7 years mulligan Done the hardest cases in the main theorem. Just got a few daemons to …
Arithmetic.ma 24.3 KB 2192   7 years sacerdot Shuffling around.
Vector.ma 24.6 KB 2124   7 years sacerdot Much more shuffling around to proper places
Fetch.ma 25.6 KB 2124   7 years sacerdot Much more shuffling around to proper places
BitVectorTrie.ma 25.7 KB 2028   8 years boender - bugfix to Assembly (forgotten sigma) - added …
StatusProofsSplit.ma 28.6 KB 2172   7 years mulligan Moved new versions of get_ / set_arg_* into Status.ma. Commented out …
ASM.ma 31.3 KB 2143   7 years mulligan Changes to the subaddressing mode elim functions moved into their …
PolicyFront.ma 31.9 KB 2235   7 years sacerdot Towards smaller proofs.
CostsProof.ma 32.4 KB 2057   7 years sacerdot Repaired (was broken by fetch_pseudo_instruction now taking a proof …
Policy.ma 34.4 KB 2230   7 years sacerdot Glue proof maximally simplified or sort of.
ASMCosts.ma 35.4 KB 1964   8 years tranquil introduced as_label_of_cost and adapted accordingly. Equality of cost …
Status.ma 40.2 KB 2247   7 years mulligan Work on the MOV instruction from today and bug fixes in set_arg_1.
Util.ma 41.2 KB 2211   7 years boender - finished proof of sigma specification - added some stuff to Util, as …
Assembly.ma 51.3 KB 2221   7 years boender - removed cases daemon from PolicyFront?
AssemblyProof.ma 52.3 KB 2256   7 years mulligan MOV and MOVX cases complete
Test.ma 55.1 KB 2258   7 years sacerdot 1. lemma generalized 2. automation replaced with expansion to make …
PolicyStep.ma 58.6 KB 2248   7 years sacerdot Final changes. All daemons removed, but the real one (open goal).
Interpret.ma 59.5 KB 2212   7 years mulligan More work on the INC case
AssemblyProofSplit.ma 136.7 KB 2261   7 years mulligan Resolved conflict
Note: See TracBrowser for help on using the repository browser.