source: src/ASM/AssemblyProof.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @2284   7 years sacerdot PUSH finished
(edit) @2282   7 years sacerdot PUSH case almost finished
(edit) @2279   7 years sacerdot 1. Bug fixed in the semantics of PUSH (no indirection performed) 2. …
(edit) @2276   7 years sacerdot
(edit) @2272   7 years mulligan Changed proof strategy for main lemma after noticed that the current …
(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) @2209   7 years mulligan Closed major daemons in the supporting lemmas of the main lemma.
(edit) @2197   7 years sacerdot Main lemmas all closed.
(edit) @2195   7 years mulligan Got AssemblyProof?.ma compiling again using daemons.
(edit) @2194   7 years sacerdot 1. monotone moved to Assembly 2. some easier daemons, one shows an …
(edit) @2160   7 years mulligan Added a new scratch file Test.ma for working on lemmas that are needed …
(edit) @2157   7 years sacerdot Anticipating a proof needed before.
(edit) @2151   7 years sacerdot 1. Lemmas from AssemblyProof? anticipated to Assembly.ma 2. Jaap's …
(edit) @2149   7 years sacerdot Code shuffling to proper places.
(edit) @2148   7 years sacerdot 1. specification made more user-friendly for AssemblyProof? 2. no more …
(edit) @2147   7 years sacerdot Theorem closed (up to one more lemma on overflow), but new proof …
(edit) @2146   7 years sacerdot 1. specification fixed again 2. the proof in AssemblyProof? is now …
(edit) @2144   7 years sacerdot 1. Policy specification fixed 2. Proof of monotonicity of sigma
(edit) @2143   7 years mulligan Changes to the subaddressing mode elim functions moved into their …
(edit) @2142   7 years sacerdot Down to one daemon that requires one lemma (monotonicity of sigma).
(edit) @2138   7 years sacerdot Invariant exported from proof of assembly_ok.
(edit) @2136   7 years sacerdot
(edit) @2135   7 years sacerdot One complex daemon changed to two simpler ones.
(edit) @2132   7 years sacerdot Two more daemons closed, one left.
(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) @2128   7 years sacerdot Final shuffling around
(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) @2119   7 years sacerdot load_code_memory moved to Fetch.ma and proved correct w.r.t. next …
(edit) @2115   7 years sacerdot Old commented out code removed
(edit) @2113   7 years sacerdot Proof by cases repaired; dead code removed.
(edit) @2112   7 years sacerdot WARNING: this commit may break some code. - dead/useless code removed
(edit) @2111   7 years sacerdot Cleanup: lemmas/theorems/axioms moved to the right places.
(edit) @2110   7 years sacerdot
(edit) @2108   7 years mulligan Various axioms closed and others moved around. Uncommented main lemma …
(edit) @2078   7 years sacerdot sigma_policy_specification has been 1) strengthened 2) made nicer to …
(edit) @2075   7 years mulligan Solved conflict in AssemblyProof?
(edit) @2057   7 years sacerdot Repaired (was broken by fetch_pseudo_instruction now taking a proof …
(edit) @2032   7 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   8 years boender - split build_maps into build_maps and build_maps_ok - work with CSC …
(edit) @1667   8 years sacerdot Main lemma for the main_thm of AssemblyProof? re-declared as an axiom …
(edit) @1666   8 years sacerdot PreStatus? datatype change: the code_memory field is not a left …
(edit) @1649   8 years boender - changes to Assembly for integration with Policy and easier use of …
(edit) @1616   8 years sacerdot Partially ported to new Matita syntax. Because of some changes in …
(edit) @1607   8 years sacerdot Porting to new library.
(edit) @1484   8 years sacerdot
(edit) @1333   8 years sacerdot Avoid using the name of the construction of jmeq.
(edit) @1045   8 years mulligan resolved conflict in rtlabs
(edit) @1043   8 years sacerdot Axiom commented out.
(edit) @1042   8 years sacerdot Dead code removed. Slow code uncommented.
(edit) @1041   8 years sacerdot fetch_assembly is still working after bug fix
(edit) @1039   8 years sacerdot fetch_assembly_pseudo2 repaired from dependent type madness
(edit) @1037   8 years sacerdot Main theorem: comments are working again.
(edit) @1036   8 years sacerdot
(edit) @1035   8 years sacerdot Main theorem (broken because of dependent types) almost restored.
(edit) @1015   8 years sacerdot One intermediate version of main_thm0 close to be repaired.
(edit) @1014   8 years sacerdot The main theorem is completely broken (again).
(edit) @998   8 years sacerdot Half repaired, half broken. Most functions no longer return option …
(edit) @994   8 years mulligan small changes
(edit) @993   8 years sacerdot More Russell everywhere; getting closer to the goal.
(edit) @992   8 years mulligan a few more axioms closed
(edit) @991   8 years mulligan loads of axioms related to equality on instructions closed
(edit) @989   8 years sacerdot Type of build_maps strengthened.
(edit) @988   8 years sacerdot Proof restored.
(edit) @987   8 years sacerdot Real parameterization over the policy.
(edit) @985   8 years sacerdot 1) Major refactoring: proofs moved where they should be. 2) New …
(edit) @982   8 years boender - this should work (see previous commit)
(edit) @979   8 years sacerdot
(edit) @977   8 years sacerdot #$%@#$@#$
(edit) @975   8 years sacerdot
(edit) @972   8 years sacerdot
(edit) @971   8 years sacerdot
(edit) @959   8 years sacerdot
(edit) @951   8 years sacerdot long call case completed
(edit) @950   8 years sacerdot Horrible sub-proof finished :-)
(edit) @949   8 years mulligan resolved conflict, work from today
(edit) @948   8 years sacerdot Some progress on the Call case.
(edit) @946   8 years sacerdot Jmp case repaired after addition of MAP hypothesis.
(edit) @945   8 years mulligan more small changes to proof of main thrm
Note: See TracRevisionLog for help on using the revision log.