source: src/ASM/

Revision Log Mode:


Copied or renamed
Diff Rev Age Author Log Message
(edit) @2760   8 years sacerdot 1. Many files repaired. 2. 3 new daemons: 2 in, 1 in …
(edit) @2754   8 years sacerdot 1. WARNING: I commented out one of James's function used in …
(edit) @2671   8 years sacerdot simplification
(edit) @2657   8 years sacerdot Cost proof fully repaired. It was broken by the definitions used in …
(edit) @2656   8 years sacerdot Ported to tailcalls (currently nothing is classified as a tailcall).
(edit) @2516   8 years mckinna removed typedefs; restored older versions; moved typedefs to …
(edit) @2498   8 years mckinna Refactor: Typedefs object_code and costlabel_map lifted out from …
(edit) @2057   8 years sacerdot Repaired (was broken by fetch_pseudo_instruction now taking a proof …
(edit) @2055   8 years sacerdot Warning: this commit adds an hypothesis that breaks all of assembly stuff.
(edit) @2001   9 years campbell Get the compiler to output more.
(edit) @1976   9 years tranquil * monads: just changed some defs, which had to be propagated in some …
(edit) @1964   9 years tranquil introduced as_label_of_cost and adapted accordingly. Equality of cost …
(edit) @1935   9 years mulligan Generalized some lemma in ASM/ to work on abstract …
(edit) @1929   9 years mulligan Simplified proof by removing most of the invariants on the statements …
(edit) @1928   9 years mulligan Moved code from in ASM/ASMCosts*.ma and ASM/ that should …
(edit) @1927   9 years mulligan Reduced complexity of good_program predicate, ported to new notion of …
(edit) @1923   9 years mulligan Small change, closing daemon that went under the RADAR
(edit) @1921   9 years mulligan Horror proof mostly finished (compiles all way until end of CostsProof?.ma).
(edit) @1919   9 years mulligan Fixes to get everything compiling again
(edit) @1910   9 years mulligan Finished proof modulo termination argument
(edit) @1900   9 years mulligan CostProof? complete, modulo some daemons and axioms in earlier files
(edit) @1898   9 years mulligan Ported changes from into CostsProof?.ma and got everything …
(edit) @1695   9 years mulligan Progress on CostsProof?.ma file.
(edit) @1693   9 years mulligan Changes to ASMCosts and CostsProofs? files to get everything working again.
(edit) @1692   9 years mulligan resolved conflict in asm costs this morning
(edit) @1658   9 years mulligan asm costs changes from today
(edit) @1650   9 years mulligan changes over the last couple of days: stuck due to matita producing …
(edit) @1648   9 years mulligan new version of utilities/ with typecheck command comented out
(edit) @1620   9 years sacerdot One of the mutual cases of the open proof is practically finished.
(edit) @1619   9 years sacerdot Major advancement.
(edit) @1587   9 years mulligan changes from today, including removing indexing of problematic …
(edit) @1581   9 years mulligan Dangling de Bruijn pointer when trying to propagate russell to set_arg_1
(edit) @1579   9 years mulligan Finished proof with simpler statement, making everything a lot nicer
(edit) @1577   9 years mulligan A lot more cases added to the proof at the bottom of …
(edit) @1576   9 years mulligan big changes to proofs, just two small cases remain and a few …
(edit) @1575   9 years mulligan Changes to specifications on execute functions
(edit) @1573   9 years mulligan more complicated than it appears :(
(edit) @1571   9 years mulligan small changes
(edit) @1570   9 years sacerdot Dependent type crazyness.
(edit) @1567   9 years mulligan more work on big proof, 2.5 cases left
(edit) @1564   9 years sacerdot Commit where we use a dependently typed version of bigops. I am now …
(edit) @1561   9 years sacerdot More dependent types to accomodate the statement.
(edit) @1558   9 years sacerdot Snapshot before moving things to
(edit) @1556   9 years mulligan submitting to avoid conflicts
(edit) @1554   9 years sacerdot Major progress in the proof.
(edit) @1549   9 years mulligan removed cruft from file so claudio can work in parallel
(edit) @1548   9 years sacerdot
(edit) @1544   9 years sacerdot StructuredTraces? inhabited for object code.
(edit) @1534   9 years mulligan committing my changes to interpret to prevent any further conflicts
(edit) @1522   9 years mulligan changes to preamble and lin to asm pass, resolved conflict in interpret
(edit) @1514   9 years mulligan changes from today. matita keeps dieing
(edit) @1511   9 years mulligan proofs, added, changes to execute_1_0 function therefore required to …
(edit) @1509   9 years mulligan i hate subtraction over the nats
(edit) @1506   9 years mulligan changes to costs proof over weekend
(edit) @1503   9 years mulligan inductive type complete
(edit) @1502   9 years mulligan changes to inductive defn
(edit) @1501   9 years sacerdot We must take in account the labelled_p predicate.
(edit) @1500   9 years sacerdot Proof sketch for one of the two main proofs.
(edit) @1499   9 years mulligan part way through main statement transcription
(add) @1498   9 years mulligan added new file for proof that costs are preserved at asm level
Note: See TracRevisionLog for help on using the revision log.