Timeline
Jul 24, 2012:
- 8:12 PM Changeset [2255] by
- Had to modify the definition of memory injections to prove that …
- 7:40 PM Changeset [2254] by
- Fix up invariants in Cminor semantics.
- 7:40 PM Changeset [2253] by
- Cminor to RTLabs is now a total function.
- 7:40 PM Changeset [2252] by
- Use the return statement invariant. Restructure the invariants for …
- 7:40 PM Changeset [2251] by
- Add new invariant to Cminor that return typs should be respected.
- 7:40 PM Changeset [2250] by
- Tidy up Clight to Cminor pass a bit.
- 7:40 PM Changeset [2249] by
- Tweak Cminor invariant to be slightly more readable/extendable.
- 7:15 PM Changeset [2248] by
- Final changes. All daemons removed, but the real one (open goal).
- 6:00 PM Changeset [2247] by
- Work on the MOV instruction from today and bug fixes in set_arg_1.
- 5:51 PM Changeset [2246] by
- Final technical lemma streamlined. Maybe it can be streamlined even more.
- 4:50 PM Changeset [2245] by
- Temporary commit to have a backtracking point. Yes, I know this breaks …
- 2:47 PM Changeset [2244] by
- Technical lemma used.
- 2:31 PM Changeset [2243] by
- One more lemma streamlined, one to go + one to be completed.
- 1:01 PM Changeset [2242] by
- jump_expansion_step3 streamlined
- 11:51 AM Changeset [2241] by
- - merged changes by Claudio
- 11:40 AM Changeset [2240] by
- All "interesting" technical lemmas singled out, proofs to be uncommented.
- 11:09 AM Changeset [2239] by
- One more lemma polished.
Jul 23, 2012:
- 11:31 PM Changeset [2238] by
- Taken out lemma integrated.
- 11:11 PM Changeset [2237] by
- Even shorter version.
- 10:46 PM Changeset [2236] by
- One subproof made shorter.
- 9:22 PM Changeset [2235] by
- Towards smaller proofs.
- 7:31 PM Changeset [2234] by
- Progress on proving semantics preservation under memory injections.
- 4:51 PM Changeset [2233] by
- * completed update of ERTL semantics * some minor changes in joint …
- 2:05 PM Changeset [2232] by
- Remove unused block structure in Cminor.
- 12:44 PM Changeset [2231] by
- Various tiny lemmas used in at least two files in the fornt-end.
- 10:35 AM Changeset [2230] by
- Glue proof maximally simplified or sort of.
Jul 20, 2012:
- 9:38 PM Changeset [2229] by
- More cleaning up, ready for more aggressive factorization.
- 9:10 PM Changeset [2228] by
- Further proof reduction.
- 8:28 PM Changeset [2227] by
- * New version of the switch removal algorithm, described at the top of …
- 6:36 PM Changeset [2226] by
- Whole program proof.
- 6:15 PM Changeset [2225] by
- Minor and major improvements everywhere, shortened proofs.
- 4:29 PM Changeset [2224] by
- Proper whole program result in RTLabs/Traces
- 4:29 PM Changeset [2223] by
- Simplify RTLabs structure traces proofs by getting rid of wrong …
- 10:58 AM Changeset [2222] by
- More robust to possible future changes to the "in match" semantics …
- 10:46 AM Changeset [2221] by
- - removed cases daemon from PolicyFront?
- 2:05 AM Changeset [2220] by
- Some minor speed up and daemon-uncommenting.
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 …
Note: See TracTimeline
for information about the timeline view.
