source: src/ASM @ 1487

Name Size Rev Age Author Last Change
../
CPP2011 1033   10 years sacerdot ispelled & submitted
Arithmetic.ma 12.1 KB ​ 1485   10 years sacerdot Less nice definitiion of add_with_carries that avoids a quadratic …
ASM.ma 8.7 KB ​ 1112   10 years mulligan got lin > asm stuff working
ASMCosts.ma 9.9 KB ​ 1486   10 years mulligan finished asm costs
Assembly.ma 66.0 KB ​ 1482   10 years sacerdot 1. very long standing conflict committed (but don't ask me what the …
AssemblyProof.ma 88.7 KB ​ 1484   10 years sacerdot …
BitVector.ma 6.1 KB ​ 990   10 years sacerdot Do no longer use the daemon automatically :-)
BitVectorTrie.ma 23.5 KB ​ 1479   10 years boender - added insert_lookup_opt - assembly compiles now
BitVectorZ.ma 4.0 KB ​ 891   10 years campbell Revise proofs affected by recent matita change.
Char.ma 76 bytes ​ 697   11 years campbell Merge Clight branch of vectors and friends. Start making stuff build.
Erase.ma 3.5 KB ​ 1463   10 years mulligan added erasure for lin
Fetch.ma 22.0 KB ​ 895   10 years sacerdot Fetch function fixed: alla AJMPS were ACALL (and the other way around) …
FoldStuff.ma 1.7 KB ​ 1062   10 years mulligan separated jmeq and coercions from foldstuff.ma in order to fix the …
I8051.ma 7.2 KB ​ 1416   10 years sacerdot Maps from hardware registers to beval now implemented in ASM/I8051 (in …
I8051bis.ma 125 bytes ​ 1415   10 years sacerdot 1. hwreg_store/retrieve no longer returns a res (but it is still …
Interpret2.ma 2.4 KB ​ 1478   10 years sacerdot Almost completed (up to is_finals).
Interpret.ma 30.5 KB ​ 1037   10 years sacerdot Main theorem: comments are working again.
JMCoercions.ma 823 bytes ​ 1335   10 years sacerdot Ported to new Matita stdlib.
README 641 bytes ​ 431   11 years mulligan - README updated - Test and DoTest? fixed to work on assembly_program - …
Status.ma 45.3 KB ​ 1459   10 years boender - moved stronger occurs_exactly_once lemma to its proper place in …
StatusProofs.ma 9.1 KB ​ 1014   10 years sacerdot The main theorem is completely broken (again).
String.ma 84 bytes ​ 698   11 years mulligan Commit with changes to files to get our files to typecheck.
Util.ma 22.4 KB ​ 1323   10 years campbell Reduce number of notations for destructive let on pairs to one.
Vector.ma 17.7 KB ​ 1330   10 years campbell Evict obsolete file.
WellLabeled.ma 1.9 KB ​ 1487   10 years mulligan committing some code for well labelling
Note: See TracBrowser for help on using the repository browser.