source: src/ASM/AssemblyProofSplit.ma

Revision Log Mode:


Legend:

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