source: src/ASM @ 2993

Name Size Rev Age Author Last Change
../
CPP2012-policy 2099   7 years boender - added reference to Intel dev manual
CPP2012-asm 2327   7 years mulligan Fixed typos in paper highlighted by referees. More substantial …
CPP2011 1033   8 years sacerdot ispelled & submitted
WellLabeled.ma 6.8 KB 2710   7 years sacerdot ASMCosts.ma repaired
Vector.ma 34.9 KB 2286   7 years tranquil Big update! * merge of all _paolo variants * reorganised some depends …
UtilBranch.ma 2.4 KB 2702   7 years sacerdot 1. proof closed in ASM/UtilBranch 2. more passes integrated in the …
Util.ma 41.5 KB 2700   7 years sacerdot 1. exponential function dropped in favour of standard library 2. …
Test.ma 92.8 KB 2284   7 years sacerdot PUSH finished
StatusProofsSplit.ma 20.3 KB 2285   7 years sacerdot 1. duplicated code erased 2. POP case finished up to lemmas on …
StatusProofs.ma 13.5 KB 2285   7 years sacerdot 1. duplicated code erased 2. POP case finished up to lemmas on …
Status.ma 36.3 KB 2907   7 years sacerdot 1. a few bugs fixed 2. as_return implemented for ASM & OC
README 641 bytes 431   9 years mulligan - README updated - Test and DoTest? fixed to work on assembly_program - …
PolicyStep.ma 59.8 KB 2714   7 years sacerdot PolicyStep?.ma repaired
PolicyFront.ma 33.4 KB 2713   7 years sacerdot PolicyFront?.ma repaired
Policy.ma 35.4 KB 2771   7 years sacerdot Some speed up in Policy.ma.
Interpret.ma 60.3 KB 2906   7 years sacerdot Bug fixed.
Interpret2.ma 5.1 KB 2993   7 years sacerdot 1. performance improved: the type inference was inferring …
I8051bis.ma 125 bytes 1415   8 years sacerdot 1. hwreg_store/retrieve no longer returns a res (but it is still …
I8051.ma 4.6 KB 2645   7 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
FoldStuff.ma 1.7 KB 1600   8 years sacerdot utilities and ASM ported to the new standard library
Fetch.ma 32.5 KB 2770   7 years mckinna WARNING: another big commit, touching many files in ASM/*.ma This …
CostsProof.ma 32.1 KB 2907   7 years sacerdot 1. a few bugs fixed 2. as_return implemented for ASM & OC
CodeMemory.ma 8.5 KB 2767   7 years mckinna WARNING: BIG commit, which pushes code_size_opt check into …
BitVectorZ.ma 4.3 KB 2200   7 years tranquil * updated joint semantics: generation of linear and graph semantics * …
BitVectorTrie.ma 26.6 KB 2767   7 years mckinna WARNING: BIG commit, which pushes code_size_opt check into …
BitVector.ma 7.1 KB 2782   7 years sacerdot 1. Paolo's bv_of_nat/nat_of_bv in BitVector? used to work with the …
AssemblyProofSplitSplit.ma 15.4 KB 2899   7 years sacerdot 1. some renaming ASM_xxx to OC_xxx 2. ASM_pre_classified_system …
AssemblyProofSplit.ma 119.7 KB 2516   7 years mckinna removed typedefs; restored older versions; moved typedefs to …
AssemblyProof.ma 54.1 KB 2899   7 years sacerdot 1. some renaming ASM_xxx to OC_xxx 2. ASM_pre_classified_system …
Assembly.ma 58.5 KB 2899   7 years sacerdot 1. some renaming ASM_xxx to OC_xxx 2. ASM_pre_classified_system …
ASMCostsSplit.ma 11.3 KB 2907   7 years sacerdot 1. a few bugs fixed 2. as_return implemented for ASM & OC
ASMCosts.ma 37.3 KB 2993   7 years sacerdot 1. performance improved: the type inference was inferring …
ASM.ma 36.4 KB 2767   7 years mckinna WARNING: BIG commit, which pushes code_size_opt check into …
Arithmetic.ma 38.3 KB 2796   7 years tranquil * added global notation for existence in Type[1] (\exists[1] x.P) * in …
AbstractStatus.ma 2.0 KB 2899   7 years sacerdot 1. some renaming ASM_xxx to OC_xxx 2. ASM_pre_classified_system …
Note: See TracBrowser for help on using the repository browser.