source: src/ASM/AssemblyProof.ma

Revision Log Mode:


Legend:

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