source: src/ASM @ 2745

Name Size Rev Age Author Last Change
../
CPP2011 1033   10 years sacerdot ispelled & submitted
CPP2012-asm 2327   8 years mulligan Fixed typos in paper highlighted by referees. More substantial …
CPP2012-policy 2099   9 years boender - added reference to Intel dev manual
AbstractStatus.ma 2.0 KB ​ 2705   8 years sacerdot More progress in ASM towards implementing the new pseudoinstructions.
Arithmetic.ma 37.4 KB ​ 2700   8 years sacerdot 1. exponential function dropped in favour of standard library 2. …
ASM.ma 32.7 KB ​ 2708   8 years tranquil fixed linearise and LINToASM LINToASM has now correct transformation …
ASMCosts.ma 37.0 KB ​ 2710   8 years sacerdot ASMCosts.ma repaired
ASMCostsSplit.ma 12.1 KB ​ 2665   8 years sacerdot …
Assembly.ma 49.6 KB ​ 2707   8 years sacerdot Assembly repaired.
AssemblyProof.ma 62.0 KB ​ 2516   8 years mckinna removed typedefs; restored older versions; moved typedefs to …
AssemblyProofSplit.ma 119.7 KB ​ 2516   8 years mckinna removed typedefs; restored older versions; moved typedefs to …
AssemblyProofSplitSplit.ma 15.5 KB ​ 2278   8 years mulligan Half of JC case complete
BitVector.ma 7.6 KB ​ 2645   8 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
BitVectorTrie.ma 25.7 KB ​ 2028   9 years boender - bugfix to Assembly (forgotten sigma) - added …
BitVectorZ.ma 4.3 KB ​ 2200   9 years tranquil * updated joint semantics: generation of linear and graph semantics * …
CostsProof.ma 34.6 KB ​ 2671   8 years sacerdot simplification
Fetch.ma 32.4 KB ​ 2516   8 years mckinna removed typedefs; restored older versions; moved typedefs to …
FoldStuff.ma 1.7 KB ​ 1600   9 years sacerdot utilities and ASM ported to the new standard library
I8051.ma 4.6 KB ​ 2645   8 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
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 ​ 2516   8 years mckinna removed typedefs; restored older versions; moved typedefs to …
Interpret.ma 60.1 KB ​ 2705   8 years sacerdot More progress in ASM towards implementing the new pseudoinstructions.
Policy.ma 35.6 KB ​ 2745   8 years sacerdot 1. Complexity of policy computation lowered from O(n2) to O(n) 2. …
PolicyFront.ma 33.4 KB ​ 2713   8 years sacerdot PolicyFront?.ma repaired
PolicyStep.ma 59.8 KB ​ 2714   8 years sacerdot PolicyStep?.ma repaired
README 641 bytes ​ 431   10 years mulligan - README updated - Test and DoTest? fixed to work on assembly_program - …
Status.ma 38.4 KB ​ 2710   8 years sacerdot ASMCosts.ma repaired
StatusProofs.ma 13.5 KB ​ 2285   8 years sacerdot 1. duplicated code erased 2. POP case finished up to lemmas on …
StatusProofsSplit.ma 20.3 KB ​ 2285   8 years sacerdot 1. duplicated code erased 2. POP case finished up to lemmas on …
Test.ma 92.8 KB ​ 2284   8 years sacerdot PUSH finished
Util.ma 41.5 KB ​ 2700   8 years sacerdot 1. exponential function dropped in favour of standard library 2. …
UtilBranch.ma 2.4 KB ​ 2702   8 years sacerdot 1. proof closed in ASM/UtilBranch 2. more passes integrated in the …
Vector.ma 34.9 KB ​ 2286   8 years tranquil Big update! * merge of all _paolo variants * reorganised some depends …
WellLabeled.ma 6.8 KB ​ 2710   8 years sacerdot ASMCosts.ma repaired
Note: See TracBrowser for help on using the repository browser.