source: src/ASM/AssemblyProofSplit.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(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) @2301   8 years mulligan Trying to get the big proof working again
(edit) @2285   8 years sacerdot 1. duplicated code erased 2. POP case finished up to lemmas on …
(edit) @2284   8 years sacerdot PUSH finished
(edit) @2283   8 years mulligan Work from today.
(edit) @2282   8 years sacerdot PUSH case almost finished
(edit) @2279   8 years sacerdot 1. Bug fixed in the semantics of PUSH (no indirection performed) 2. …
(edit) @2278   8 years mulligan Half of JC case complete
(edit) @2276   8 years sacerdot …
(edit) @2273   8 years sacerdot 1. lemmas moved from all files to Test.ma 2. most of the lemmas in …
(edit) @2272   8 years mulligan Changed proof strategy for main lemma after noticed that the current …
(edit) @2265   9 years sacerdot Commented out code removed.
(edit) @2262   9 years mulligan Changes from today.
(edit) @2261   9 years mulligan Resolved conflict
(edit) @2260   9 years sacerdot Now we use the efficient lookup_address.
(edit) @2259   9 years mulligan For Claudio
(edit) @2258   9 years sacerdot 1. lemma generalized 2. automation replaced with expansion to make …
(edit) @2257   9 years mulligan Daemon in SETB case closed.
(edit) @2256   9 years mulligan MOV and MOVX cases complete
(edit) @2247   9 years mulligan Work on the MOV instruction from today and bug fixes in set_arg_1.
(edit) @2216   9 years mulligan More work on the big lemma. Nearly there now.
(edit) @2212   9 years mulligan More work on the INC case
(edit) @2210   9 years mulligan XOR case completely finished.
(edit) @2209   9 years mulligan Closed major daemons in the supporting lemmas of the main lemma.
(edit) @2207   9 years mulligan Improvements and corrections to the main lemma proof in …
(edit) @2204   9 years sacerdot Shuffling around, suggestions, improvements.
(edit) @2198   9 years mulligan Work from today.
(edit) @2187   9 years mulligan Work from today on the big proof.
(edit) @2183   9 years mulligan More progress on main lemma proof.
(edit) @2181   9 years mulligan Work from the last week on the new formulation of the main lemma for …
(edit) @2173   9 years mulligan MUL case of main lemma nearly complete (subject to two small holes …
(edit) @2172   9 years mulligan Moved new versions of get_ / set_arg_* into Status.ma. Commented out …
(edit) @2160   9 years mulligan Added a new scratch file Test.ma for working on lemmas that are needed …
(edit) @2143   9 years mulligan Changes to the subaddressing mode elim functions moved into their …
(edit) @2140   9 years mulligan Done the hardest cases in the main theorem. Just got a few daemons to …
(edit) @2139   9 years mulligan Changes to get the main lemma compiling again. Changes pushed into …
(edit) @2131   9 years sacerdot No more need for functional extensionality.
(edit) @2129   9 years mulligan Large changes from today trying to complete the main theorem. Again :(
(edit) @2124   9 years sacerdot Much more shuffling around to proper places
(edit) @2122   9 years sacerdot More stuff moved around in proper places
(edit) @2121   9 years sacerdot More functions moved to the places they belong to
(edit) @2114   9 years sacerdot Proof repaired
(edit) @2109   9 years mulligan Finished porting the large, main lemma to the new notion of jump …
(edit) @2108   9 years mulligan Various axioms closed and others moved around. Uncommented main lemma …
(edit) @2047   9 years mulligan Big bugs in policy calculations found. Waiting for Jaap's commit.
(edit) @2039   9 years sacerdot New, better interface for subaddressing_mode_elim
(edit) @2032   9 years sacerdot !! BEWARE: major commit !! 1) [affects everybody] split for …
(edit) @2026   9 years mulligan Added a new file to house the main theorem as the type checking time …
(edit) @2024   9 years mulligan Updated AssemblyProof? to fix mismatch in definition of lookup_labels …
(edit) @2023   9 years mulligan Closed main lemma modulo closing trivial subgoals about commutations …
(edit) @2020   9 years mulligan CJNE case complete, DJNZ case almost complete
(edit) @2018   9 years mulligan CJNE case a complete mess.
(edit) @2017   9 years mulligan Large swathes of proof of main lemma added.
(edit) @1985   9 years mulligan A single `false' case for unconditional jumps completed.
(edit) @1984   9 years mulligan Most proof obligations closed in main_lemma apart from those of the …
(edit) @1983   9 years mulligan Changes to simplify the simpler cases of the main_lemma.
(edit) @1979   9 years sacerdot Very very very tricky lemma closed. A dreadful mix of JM equality …
(edit) @1978   9 years sacerdot Two more cases completed.
(edit) @1977   9 years sacerdot Unblocked: let ... as hides two different terms, one that uses Leibniz …
(edit) @1975   9 years mulligan Work from today on closing main_thm.
(edit) @1971   9 years sacerdot 1. Interpret.ma: we need to prove \sigma (execute_preinstruction …
(edit) @1969   9 years sacerdot Some more progress, but now we must prove something on a Russell …
(edit) @1967   9 years sacerdot Mov case completed.
(edit) @1966   9 years mulligan Progress made on main_thm proof: trying to find a pattern to use …
(edit) @1963   9 years sacerdot More progress in restoring the original proof.
(edit) @1958   9 years mulligan Marked divergence in StatusProofs?.ma
(add) @1952   9 years sacerdot AssemblyProof? splitted.
Note: See TracRevisionLog for help on using the revision log.