source: src/ASM/AssemblyProof.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @2151   8 years sacerdot 1. Lemmas from AssemblyProof? anticipated to Assembly.ma 2. Jaap's …
(edit) @2149   8 years sacerdot Code shuffling to proper places.
(edit) @2148   8 years sacerdot 1. specification made more user-friendly for AssemblyProof? 2. no more …
(edit) @2147   8 years sacerdot Theorem closed (up to one more lemma on overflow), but new proof …
(edit) @2146   8 years sacerdot 1. specification fixed again 2. the proof in AssemblyProof? is now …
(edit) @2144   8 years sacerdot 1. Policy specification fixed 2. Proof of monotonicity of sigma
(edit) @2143   8 years mulligan Changes to the subaddressing mode elim functions moved into their …
(edit) @2142   8 years sacerdot Down to one daemon that requires one lemma (monotonicity of sigma).
(edit) @2138   8 years sacerdot Invariant exported from proof of assembly_ok.
(edit) @2136   8 years sacerdot …
(edit) @2135   8 years sacerdot One complex daemon changed to two simpler ones.
(edit) @2132   8 years sacerdot Two more daemons closed, one left.
(edit) @2131   8 years sacerdot No more need for functional extensionality.
(edit) @2129   8 years mulligan Large changes from today trying to complete the main theorem. Again :(
(edit) @2128   8 years sacerdot Final shuffling around
(edit) @2124   8 years sacerdot Much more shuffling around to proper places
(edit) @2122   8 years sacerdot More stuff moved around in proper places
(edit) @2121   8 years sacerdot More functions moved to the places they belong to
(edit) @2119   8 years sacerdot load_code_memory moved to Fetch.ma and proved correct w.r.t. next …
(edit) @2115   8 years sacerdot Old commented out code removed
(edit) @2113   8 years sacerdot Proof by cases repaired; dead code removed.
(edit) @2112   8 years sacerdot WARNING: this commit may break some code. - dead/useless code removed
(edit) @2111   8 years sacerdot Cleanup: lemmas/theorems/axioms moved to the right places.
(edit) @2110   8 years sacerdot …
(edit) @2108   8 years mulligan Various axioms closed and others moved around. Uncommented main lemma …
(edit) @2078   8 years sacerdot sigma_policy_specification has been 1) strengthened 2) made nicer to …
(edit) @2075   8 years mulligan Solved conflict in AssemblyProof?
(edit) @2057   8 years sacerdot Repaired (was broken by fetch_pseudo_instruction now taking a proof …
(edit) @2032   8 years sacerdot !! BEWARE: major commit !! 1) [affects everybody] split for …
(edit) @2024   8 years mulligan Updated AssemblyProof? to fix mismatch in definition of lookup_labels …
(edit) @2021   8 years sacerdot Proof skeleton in place. Several daemons to be closed adding invariants.
(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) @1975   8 years mulligan Work from today on closing main_thm.
(edit) @1972   8 years mulligan Simple lemma with strangely complex proof complete.
(edit) @1966   8 years mulligan Progress made on main_thm proof: trying to find a pattern to use …
(edit) @1957   8 years mulligan Stitching proofs back together after slight change in statement of …
(edit) @1955   8 years mulligan Completed proof of snd_assembly_1_pseudoinstruction_ok, modulo some …
(edit) @1953   8 years mulligan Commit to avoid conflicts.
(edit) @1952   8 years sacerdot AssemblyProof? splitted.
(edit) @1948   8 years mulligan Weakened statements of ASM/Assembly.ma and ASM/AssemblyProof.ma, so …
(edit) @1947   8 years sacerdot Failure of automation/demod investigated a little bit.
(edit) @1946   8 years sacerdot \snd half_add => add everywhere
(edit) @1945   8 years sacerdot All proof statements repaired.
(edit) @1941   8 years mulligan Changes to the AssemblyProof? with a few more (large) axioms closed.
(edit) @1939   8 years mulligan Changes to get things to compile and to avoid the dependency …
(edit) @1936   8 years mulligan Some holes filled in AssemblyProof?.ma.
(edit) @1668   9 years boender - split build_maps into build_maps and build_maps_ok - work with CSC …
(edit) @1667   9 years sacerdot Main lemma for the main_thm of AssemblyProof? re-declared as an axiom …
(edit) @1666   9 years sacerdot PreStatus? datatype change: the code_memory field is not a left …
(edit) @1649   9 years boender - changes to Assembly for integration with Policy and easier use of …
(edit) @1616   9 years sacerdot Partially ported to new Matita syntax. Because of some changes in …
(edit) @1607   9 years sacerdot Porting to new library.
(edit) @1484   9 years sacerdot …
(edit) @1333   9 years sacerdot Avoid using the name of the construction of jmeq.
(edit) @1045   9 years mulligan resolved conflict in rtlabs
(edit) @1043   9 years sacerdot Axiom commented out.
(edit) @1042   9 years sacerdot Dead code removed. Slow code uncommented.
(edit) @1041   9 years sacerdot fetch_assembly is still working after bug fix
(edit) @1039   9 years sacerdot fetch_assembly_pseudo2 repaired from dependent type madness
(edit) @1037   9 years sacerdot Main theorem: comments are working again.
(edit) @1036   9 years sacerdot …
(edit) @1035   9 years sacerdot Main theorem (broken because of dependent types) almost restored.
(edit) @1015   9 years sacerdot One intermediate version of main_thm0 close to be repaired.
(edit) @1014   9 years sacerdot The main theorem is completely broken (again).
(edit) @998   9 years sacerdot Half repaired, half broken. Most functions no longer return option …
(edit) @994   9 years mulligan small changes
(edit) @993   9 years sacerdot More Russell everywhere; getting closer to the goal.
(edit) @992   9 years mulligan a few more axioms closed
(edit) @991   9 years mulligan loads of axioms related to equality on instructions closed
(edit) @989   9 years sacerdot Type of build_maps strengthened.
(edit) @988   9 years sacerdot Proof restored.
(edit) @987   9 years sacerdot Real parameterization over the policy.
(edit) @985   9 years sacerdot 1) Major refactoring: proofs moved where they should be. 2) New …
(edit) @982   9 years boender - this should work (see previous commit)
(edit) @979   9 years sacerdot …
(edit) @977   9 years sacerdot #$%@#$@#$
(edit) @975   9 years sacerdot …
(edit) @972   9 years sacerdot …
(edit) @971   9 years sacerdot …
(edit) @959   9 years sacerdot …
(edit) @951   9 years sacerdot long call case completed
(edit) @950   9 years sacerdot Horrible sub-proof finished :-)
(edit) @949   9 years mulligan resolved conflict, work from today
(edit) @948   9 years sacerdot Some progress on the Call case.
(edit) @946   9 years sacerdot Jmp case repaired after addition of MAP hypothesis.
(edit) @945   9 years mulligan more small changes to proof of main thrm
(edit) @944   9 years mulligan split definition
(edit) @943   9 years sacerdot …
(edit) @942   9 years sacerdot New invariant for the main theorem. The new invariant is much more …
(edit) @941   9 years sacerdot Jmp case finished up to arithmetical properties.
(edit) @940   9 years mulligan more changes to inc case of main theorem
(edit) @939   9 years sacerdot Long Jmp case finished.
(edit) @938   9 years sacerdot …
(edit) @937   9 years mulligan resolved conflict in assembly_proof, more lemmas added
(edit) @936   9 years sacerdot Ticks are now handled correctly everywhere and the main proof takes …
(edit) @935   9 years mulligan changes to status and assembly proof
(edit) @934   9 years sacerdot …
(edit) @933   9 years sacerdot New proof strategy.
(edit) @932   9 years sacerdot …
Note: See TracRevisionLog for help on using the revision log.