Timeline
Jul 19, 2012:
- 6:45 PM Changeset [2219] by
- Speed up cast simplification proof checking a bit.
- 6:45 PM Changeset [2218] by
- Separate out cost properties required of RTLabs programs from the …
- 6:13 PM Changeset [2217] by
- * collapsed step_params, unserialized_params, funct_params and …
- 5:33 PM Changeset [2216] by
- More work on the big lemma. Nearly there now.
- 5:12 PM Changeset [2215] by
- Some speed up.
- 2:42 PM Changeset [2214] by
- * changed order of parameters of joint_internal_function and genv in …
Jul 18, 2012:
- 5:57 PM Changeset [2213] by
- - removed one cases daemon
- 5:30 PM Changeset [2212] by
- More work on the INC case
- 3:57 PM Changeset [2211] by
- - finished proof of sigma specification - added some stuff to Util, as …
- 3:03 PM Changeset [2210] by
- XOR case completely finished.
- 2:56 PM Changeset [2209] by
- Closed major daemons in the supporting lemmas of the main lemma.
- 1:26 PM Changeset [2208] by
- * moving some code around * changed immediates to hold beval in …
- 12:29 PM Changeset [2207] by
- Improvements and corrections to the main lemma proof in …
- 12:27 PM Changeset [2206] by
- Add note about cost maps to simulation definition.
- 12:27 PM Changeset [2205] by
- Get correctness.ma type checking again.
- 10:08 AM Changeset [2204] by
- Shuffling around, suggestions, improvements.
Jul 17, 2012:
- 6:57 PM Changeset [2203] by
- A general result about simulations of executions.
- 6:57 PM Changeset [2202] by
- Start defining equivalent executions.
- 6:57 PM Changeset [2201] by
- Forgotten comment update.
- 6:00 PM Changeset [2200] by
- * updated joint semantics: generation of linear and graph semantics * …
- 5:40 PM Changeset [2199] by
- No longer used lemma containing the last daemon removed. The proof is …
- 4:27 PM Changeset [2198] by
- Work from today.
- 3:23 PM Changeset [2197] by
- Main lemmas all closed.
- 2:19 PM Changeset [2196] by
- Speed up using patterns.
- 10:48 AM Changeset [2195] by
- Got AssemblyProof?.ma compiling again using daemons.
- 10:18 AM Changeset [2194] by
- 1. monotone moved to Assembly 2. some easier daemons, one shows an …
- 2:12 AM Changeset [2193] by
- Statement clean-up.
- 2:06 AM Changeset [2192] by
- Shuffling around.
- 2:01 AM Changeset [2191] by
- Only one daemon left.
- 1:41 AM Changeset [2190] by
- Two daemons left.
- 1:03 AM Changeset [2189] by
- Proof very close to completion.
Jul 16, 2012:
- 11:28 PM Changeset [2188] by
- 1. Policy specification generalized 2. All invariants but the main one …
- 5:19 PM Changeset [2187] by
- Work from today on the big proof.
- 4:59 PM Changeset [2186] by
- updated joint semantics
Jul 13, 2012:
- 7:59 PM Changeset [2185] by
- Use bitvectors for offsets.
- 7:59 PM Changeset [2184] by
- Minor fix ups.
- 5:03 PM Changeset [2183] by
- More progress on main lemma proof.
- 11:20 AM Changeset [2182] by
- updated linearisation pass
- 11:00 AM Changeset [2181] by
- Work from the last week on the new formulation of the main lemma for …
Jul 12, 2012:
- 4:46 PM Changeset [2180] by
- Fix off-by-one error in GenMem?.ma.
- 2:56 PM Changeset [2179] by
- Dependent pair monad binding notation.
- 2:56 PM Changeset [2178] by
- Shift some notation into utilities.
- 2:56 PM Changeset [2177] by
- Tidy up multiplication.
- 1:28 PM Changeset [2176] by
- Remove memory spaces other than XData and Code; simplify pointers as a …
Jul 10, 2012:
- 6:08 PM Changeset [2175] by
- corrected small bug
- 5:37 PM Changeset [2174] by
- * factored out script for (axiomatised) fixpoint computation * ERTL → …
- 5:29 PM Changeset [2173] by
- MUL case of main lemma nearly complete (subject to two small holes …
- 2:39 PM Changeset [2172] by
- Moved new versions of get_ / set_arg_* into Status.ma. Commented out …
- 11:54 AM Changeset [2171] by
- Finished the commutations
- 10:44 AM Changeset [2170] by
- Splitted from AssemblyProofSplit?.ma
Jul 9, 2012:
- 2:08 PM Changeset [2169] by
- corrected bug where definition of carry bit by MUL and DIV (which …
Jul 8, 2012:
- 4:34 PM Changeset [2168] by
- No more daemons left! All axioms are real axioms.
- 4:24 PM Changeset [2167] by
- Only one daemon left.
- 3:59 PM Changeset [2166] by
- 1. less daemons 2. more easily usable statement
Jul 7, 2012:
- 3:23 AM Changeset [2165] by
- Only three daemons left.
- 3:00 AM Changeset [2164] by
- More steady progress.
Jul 6, 2012:
- 11:04 PM Changeset [2163] by
- Steady progress.
- 5:53 PM Changeset [2162] by
- * yet another correction to joint * added functions adding prologues …
- 5:35 PM Changeset [2161] by
- Most of the old proof restored.
- 5:26 PM Changeset [2160] by
- Added a new scratch file Test.ma for working on lemmas that are needed …
- 12:05 PM Changeset [2159] by
- One daemon left, back to original proof.
- 11:41 AM Changeset [2158] by
- One less daemon.
- 11:34 AM Changeset [2157] by
- Anticipating a proof needed before.
- 11:30 AM Changeset [2156] by
- One more invariant, one less daemon.
- 11:25 AM Changeset [2155] by
- updates to blocks and RTLabs to RTL translation (which sidesteps …
Jul 5, 2012:
- 2:22 PM Changeset [2154] by
- Code shuffled around.
Jul 4, 2012:
- 3:38 PM Changeset [2153] by
- - updated the proof some more
- 1:23 PM Changeset [2152] by
- - this should compile
Jul 3, 2012:
- 6:12 PM Changeset [2151] by
- 1. Lemmas from AssemblyProof? anticipated to Assembly.ma 2. Jaap's …
- 11:30 AM Changeset [2150] by
- Add labelling result to the correctness file.
- 4:19 AM Changeset [2149] by
- Code shuffling to proper places.
- 4:14 AM Changeset [2148] by
- 1. specification made more user-friendly for AssemblyProof? 2. no more …
- 3:53 AM Changeset [2147] by
- Theorem closed (up to one more lemma on overflow), but new proof …
- 3:09 AM Changeset [2146] by
- 1. specification fixed again 2. the proof in AssemblyProof? is now …
Jul 2, 2012:
- 4:12 PM Changeset [2145] by
- Cost labelling doesn't affect interaction.
- 3:59 PM Changeset [2144] by
- 1. Policy specification fixed 2. Proof of monotonicity of sigma
- 11:37 AM Changeset [2143] by
- Changes to the subaddressing mode elim functions moved into their …
Jun 29, 2012:
- 10:09 AM Changeset [2142] by
- Down to one daemon that requires one lemma (monotonicity of sigma).
Jun 28, 2012:
- 8:08 PM Changeset [2141] by
- - committed working version
- 6:47 PM Changeset [2140] by
- Done the hardest cases in the main theorem. Just got a few daemons to …
- 5:42 PM Changeset [2139] by
- Changes to get the main lemma compiling again. Changes pushed into …
- 4:47 PM Changeset [2138] by
- Invariant exported from proof of assembly_ok.
- 3:00 PM Changeset [2137] by
- Bug fixed in specification.
- 2:58 PM Changeset [2136] by
- …
- 2:34 PM Changeset [2135] by
- One complex daemon changed to two simpler ones.
- 12:37 PM Changeset [2134] by
- Split out behavioural equivalence spec for labelling.
- 10:59 AM Changeset [2133] by
- - moved does_not_occur_occur_absurd
- 10:41 AM Changeset [2132] by
- Two more daemons closed, one left.
- 12:55 AM Changeset [2131] by
- No more need for functional extensionality.
Jun 27, 2012:
- 10:19 PM Changeset [2130] by
- Proof repaired after Dominic's bug fix.
- 7:14 PM Changeset [2129] by
- Large changes from today trying to complete the main theorem. Again :(
- 5:05 PM Changeset [2128] by
- Final shuffling around
- 4:59 PM Changeset [2127] by
- Last daemon closed
- 4:56 PM Changeset [2126] by
- Proof improved (for case 3) + new proof (for case 11)
- 4:28 PM Changeset [2125] by
- - some more displacement from Policy to Util
- 4:23 PM Changeset [2124] by
- Much more shuffling around to proper places
- 4:04 PM Changeset [2123] by
- - moved is_well_labeled_p to Status and instruction_is_label to ASM …
- 3:36 PM Changeset [2122] by
- More stuff moved around in proper places
- 3:30 PM Changeset [2121] by
- More functions moved to the places they belong to
- 12:59 PM Changeset [2120] by
- Fix victim of alloc unfolding.
- 12:09 PM Changeset [2119] by
- load_code_memory moved to Fetch.ma and proved correct w.r.t. next …
- 12:04 PM Changeset [2118] by
- Labelling preserves behaviour.
- 12:04 PM Changeset [2117] by
- Workaround for bug in Matita.
- 11:46 AM Changeset [2116] by
- load_code_memory will be moved into Fetch.ma in the next commit. This …
- 1:59 AM Changeset [2115] by
- Old commented out code removed
- 1:40 AM Changeset [2114] by
- Proof repaired
- 12:49 AM Changeset [2113] by
- Proof by cases repaired; dead code removed.
Jun 26, 2012:
- 11:47 PM Changeset [2112] by
- WARNING: this commit may break some code. - dead/useless code removed
- 5:30 PM Changeset [2111] by
- Cleanup: lemmas/theorems/axioms moved to the right places.
- 4:05 PM Changeset [2110] by
- …
- 2:47 PM Changeset [2109] by
- Finished porting the large, main lemma to the new notion of jump …
Jun 25, 2012:
- 2:39 PM Changeset [2108] by
- Various axioms closed and others moved around. Uncommented main lemma …
Jun 22, 2012:
- 2:07 PM Changeset [2107] by
- Memory initialisation and program transformations.
Jun 21, 2012:
- 5:21 PM Changeset [2106] by
- Fix up a couple of proofs broken by recent changes.
- 5:21 PM Changeset [2105] by
- Show some results about globalenvs and program transformations.
- 5:21 PM Changeset [2104] by
- Fill in misc axiom.
- 5:21 PM Changeset [2103] by
- Make transform_*program take a more general transformation to make …
Jun 20, 2012:
- 4:51 PM Changeset [2102] by
- - some small changes
Jun 19, 2012:
- 4:43 PM Changeset [2101] by
- - renamed medium to absolute jump - revised proofs of policy, some …
Note: See TracTimeline
for information about the timeline view.
