Timeline



Aug 2, 2012:

6:40 PM Changeset [2292] by campbell
More RTLabs invariants.
5:04 PM Changeset [2291] by campbell
Disable switch removal in compiler.ma for now.
5:04 PM Changeset [2290] by campbell
Remove jump tables from RTLabs -> RTL.
5:04 PM Changeset [2289] by campbell
Update alias
5:04 PM Changeset [2288] by campbell
Remove jumptables from RTLabs. :(
5:04 PM Changeset [2287] by campbell
RTLabs typing for loads and stores.
3:18 PM Changeset [2286] by tranquil
Big update! * merge of all _paolo variants * reorganised some depends …
1:58 PM Changeset [2285] by sacerdot
1. duplicated code erased 2. POP case finished up to lemmas on …

Aug 1, 2012:

4:56 PM Changeset [2284] by sacerdot
PUSH finished

Jul 31, 2012:

6:11 PM Changeset [2283] by mulligan
Work from today.
6:08 PM Changeset [2282] by sacerdot
PUSH case almost finished
2:22 AM Changeset [2281] by sacerdot
12:10 AM Changeset [2280] by sacerdot
Proof repaired.

Jul 30, 2012:

11:44 PM Changeset [2279] by sacerdot
1. Bug fixed in the semantics of PUSH (no indirection performed) 2. …
6:33 PM Changeset [2278] by mulligan
Half of JC case complete
4:54 PM Changeset [2277] by tranquil
* replaced incorrect use of subvector_with
2:36 PM Changeset [2276] by sacerdot
1:05 PM Changeset [2275] by tranquil
* moved around some code (I8051.ma does not depend on ByteValues?.ma …
1:14 AM Changeset [2274] by sacerdot
Dead code commented out and code out of place moved to Test.ma.
12:46 AM Changeset [2273] by sacerdot
1. lemmas moved from all files to Test.ma 2. most of the lemmas in …

Jul 27, 2012:

5:53 PM Changeset [2272] by mulligan
Changed proof strategy for main lemma after noticed that the current …

Jul 26, 2012:

5:02 PM Changeset [2271] by garnier
Proof of correction for the semantics of expressions under memory …
3:57 PM Changeset [2270] by mulligan
Bug spotted and fixed in write_at_stack_pointer
3:29 PM Changeset [2269] by sacerdot
Proof completely repaired up to …
2:56 PM Changeset [2268] by mulligan
Bug spotted in instruction_size (lookup_datalabels cannot just be a …
12:05 PM Changeset [2267] by sacerdot
Call is now proved using the new strategy.
10:43 AM Changeset [2266] by sacerdot
All daemons closed in Jmp case.
3:48 AM Changeset [2265] by sacerdot
Commented out code removed.
12:38 AM Changeset [2264] by sacerdot
1) Major change: we now always use the efficient way of resolving …

Jul 25, 2012:

6:55 PM Changeset [2263] by garnier
Finished proving semantics preservation under memory injections for …
5:54 PM Changeset [2262] by mulligan
Changes from today.
5:04 PM Changeset [2261] by mulligan
Resolved conflict
4:52 PM Changeset [2260] by sacerdot
Now we use the efficient lookup_address.
4:37 PM Changeset [2259] by mulligan
For Claudio
1:47 PM Changeset [2258] by sacerdot
1. lemma generalized 2. automation replaced with expansion to make …
1:13 PM Changeset [2257] by mulligan
Daemon in SETB case closed.
12:12 PM Changeset [2256] by mulligan
MOV and MOVX cases complete

Jul 24, 2012:

8:12 PM Changeset [2255] by garnier
Had to modify the definition of memory injections to prove that …
7:40 PM Changeset [2254] by campbell
Fix up invariants in Cminor semantics.
7:40 PM Changeset [2253] by campbell
Cminor to RTLabs is now a total function.
7:40 PM Changeset [2252] by campbell
Use the return statement invariant. Restructure the invariants for …
7:40 PM Changeset [2251] by campbell
Add new invariant to Cminor that return typs should be respected.
7:40 PM Changeset [2250] by campbell
Tidy up Clight to Cminor pass a bit.
7:40 PM Changeset [2249] by campbell
Tweak Cminor invariant to be slightly more readable/extendable.
7:15 PM Changeset [2248] by sacerdot
Final changes. All daemons removed, but the real one (open goal).
6:00 PM Changeset [2247] by mulligan
Work on the MOV instruction from today and bug fixes in set_arg_1.
5:51 PM Changeset [2246] by sacerdot
Final technical lemma streamlined. Maybe it can be streamlined even more.
4:50 PM Changeset [2245] by sacerdot
Temporary commit to have a backtracking point. Yes, I know this breaks …
2:47 PM Changeset [2244] by sacerdot
Technical lemma used.
2:31 PM Changeset [2243] by sacerdot
One more lemma streamlined, one to go + one to be completed.
1:01 PM Changeset [2242] by sacerdot
jump_expansion_step3 streamlined
11:51 AM Changeset [2241] by boender
- merged changes by Claudio
11:40 AM Changeset [2240] by sacerdot
All "interesting" technical lemmas singled out, proofs to be uncommented.
11:09 AM Changeset [2239] by sacerdot
One more lemma polished.

Jul 23, 2012:

11:31 PM Changeset [2238] by sacerdot
Taken out lemma integrated.
11:11 PM Changeset [2237] by sacerdot
Even shorter version.
10:46 PM Changeset [2236] by sacerdot
One subproof made shorter.
9:22 PM Changeset [2235] by sacerdot
Towards smaller proofs.
7:31 PM Changeset [2234] by garnier
Progress on proving semantics preservation under memory injections.
4:51 PM Changeset [2233] by tranquil
* completed update of ERTL semantics * some minor changes in joint …
2:05 PM Changeset [2232] by campbell
Remove unused block structure in Cminor.
12:44 PM Changeset [2231] by garnier
Various tiny lemmas used in at least two files in the fornt-end.
10:35 AM Changeset [2230] by sacerdot
Glue proof maximally simplified or sort of.

Jul 20, 2012:

9:38 PM Changeset [2229] by sacerdot
More cleaning up, ready for more aggressive factorization.
9:10 PM Changeset [2228] by sacerdot
Further proof reduction.
8:28 PM Changeset [2227] by garnier
* New version of the switch removal algorithm, described at the top of …
6:36 PM Changeset [2226] by campbell
Whole program proof.
6:15 PM Changeset [2225] by sacerdot
Minor and major improvements everywhere, shortened proofs.
4:29 PM Changeset [2224] by campbell
Proper whole program result in RTLabs/Traces
4:29 PM Changeset [2223] by campbell
Simplify RTLabs structure traces proofs by getting rid of wrong …
10:58 AM Changeset [2222] by sacerdot
More robust to possible future changes to the "in match" semantics …
10:46 AM Changeset [2221] by boender
- removed cases daemon from PolicyFront?
2:05 AM Changeset [2220] by sacerdot
Some minor speed up and daemon-uncommenting.

Jul 19, 2012:

6:45 PM Changeset [2219] by campbell
Speed up cast simplification proof checking a bit.
6:45 PM Changeset [2218] by campbell
Separate out cost properties required of RTLabs programs from the …
6:13 PM Changeset [2217] by tranquil
* collapsed step_params, unserialized_params, funct_params and …
5:33 PM Changeset [2216] by mulligan
More work on the big lemma. Nearly there now.
5:12 PM Changeset [2215] by sacerdot
Some speed up.
2:42 PM Changeset [2214] by tranquil
* changed order of parameters of joint_internal_function and genv in …
10:08 AM CPP2012.tar.gz attached to WikiStart by mulligan
Latest snapshot of CerCo? proof.

Jul 18, 2012:

5:57 PM Changeset [2213] by boender
- removed one cases daemon
5:30 PM Changeset [2212] by mulligan
More work on the INC case
3:57 PM Changeset [2211] by boender
- finished proof of sigma specification - added some stuff to Util, as …
3:03 PM Changeset [2210] by mulligan
XOR case completely finished.
2:56 PM Changeset [2209] by mulligan
Closed major daemons in the supporting lemmas of the main lemma.
1:26 PM Changeset [2208] by tranquil
* moving some code around * changed immediates to hold beval in …
12:29 PM Changeset [2207] by mulligan
Improvements and corrections to the main lemma proof in …
12:27 PM Changeset [2206] by campbell
Add note about cost maps to simulation definition.
12:27 PM Changeset [2205] by campbell
Get correctness.ma type checking again.
10:08 AM Changeset [2204] by sacerdot
Shuffling around, suggestions, improvements.

Jul 17, 2012:

6:57 PM Changeset [2203] by campbell
A general result about simulations of executions.
6:57 PM Changeset [2202] by campbell
Start defining equivalent executions.
6:57 PM Changeset [2201] by campbell
Forgotten comment update.
6:00 PM Changeset [2200] by tranquil
* updated joint semantics: generation of linear and graph semantics * …
5:40 PM Changeset [2199] by sacerdot
No longer used lemma containing the last daemon removed. The proof is …
4:27 PM Changeset [2198] by mulligan
Work from today.
3:23 PM Changeset [2197] by sacerdot
Main lemmas all closed.
2:19 PM Changeset [2196] by sacerdot
Speed up using patterns.
10:48 AM Changeset [2195] by mulligan
Got AssemblyProof?.ma compiling again using daemons.
10:18 AM Changeset [2194] by sacerdot
1. monotone moved to Assembly 2. some easier daemons, one shows an …
2:12 AM Changeset [2193] by sacerdot
Statement clean-up.
2:06 AM Changeset [2192] by sacerdot
Shuffling around.
2:01 AM Changeset [2191] by sacerdot
Only one daemon left.
1:41 AM Changeset [2190] by sacerdot
Two daemons left.
1:03 AM Changeset [2189] by sacerdot
Proof very close to completion.

Jul 16, 2012:

11:28 PM Changeset [2188] by sacerdot
1. Policy specification generalized 2. All invariants but the main one …
5:19 PM Changeset [2187] by mulligan
Work from today on the big proof.
4:59 PM Changeset [2186] by tranquil
updated joint semantics

Jul 13, 2012:

7:59 PM Changeset [2185] by campbell
Use bitvectors for offsets.
7:59 PM Changeset [2184] by campbell
Minor fix ups.
5:03 PM Changeset [2183] by mulligan
More progress on main lemma proof.
11:20 AM Changeset [2182] by tranquil
updated linearisation pass
11:00 AM Changeset [2181] by mulligan
Work from the last week on the new formulation of the main lemma for …

Jul 12, 2012:

4:46 PM Changeset [2180] by campbell
Fix off-by-one error in GenMem?.ma.
2:56 PM Changeset [2179] by campbell
Dependent pair monad binding notation.
2:56 PM Changeset [2178] by campbell
Shift some notation into utilities.
2:56 PM Changeset [2177] by campbell
Tidy up multiplication.
1:28 PM Changeset [2176] by campbell
Remove memory spaces other than XData and Code; simplify pointers as a …

Jul 10, 2012:

6:08 PM Changeset [2175] by tranquil
corrected small bug
5:37 PM Changeset [2174] by tranquil
* factored out script for (axiomatised) fixpoint computation * ERTL → …
5:29 PM Changeset [2173] by mulligan
MUL case of main lemma nearly complete (subject to two small holes …
2:39 PM Changeset [2172] by mulligan
Moved new versions of get_ / set_arg_* into Status.ma. Commented out …
11:54 AM Changeset [2171] by mulligan
Finished the commutations
10:44 AM Changeset [2170] by sacerdot
Splitted from AssemblyProofSplit?.ma

Jul 9, 2012:

2:08 PM Changeset [2169] by tranquil
corrected bug where definition of carry bit by MUL and DIV (which …

Jul 8, 2012:

4:34 PM Changeset [2168] by sacerdot
No more daemons left! All axioms are real axioms.
4:24 PM Changeset [2167] by sacerdot
Only one daemon left.
3:59 PM Changeset [2166] by sacerdot
1. less daemons 2. more easily usable statement

Jul 7, 2012:

3:23 AM Changeset [2165] by sacerdot
Only three daemons left.
3:00 AM Changeset [2164] by sacerdot
More steady progress.

Jul 6, 2012:

11:04 PM Changeset [2163] by sacerdot
Steady progress.
5:53 PM Changeset [2162] by tranquil
* yet another correction to joint * added functions adding prologues …
5:35 PM Changeset [2161] by sacerdot
Most of the old proof restored.
5:26 PM Changeset [2160] by mulligan
Added a new scratch file Test.ma for working on lemmas that are needed …
12:05 PM Changeset [2159] by sacerdot
One daemon left, back to original proof.
11:41 AM Changeset [2158] by sacerdot
One less daemon.
11:34 AM Changeset [2157] by sacerdot
Anticipating a proof needed before.
11:30 AM Changeset [2156] by sacerdot
One more invariant, one less daemon.
11:25 AM Changeset [2155] by tranquil
updates to blocks and RTLabs to RTL translation (which sidesteps …

Jul 5, 2012:

2:22 PM Changeset [2154] by sacerdot
Code shuffled around.

Jul 4, 2012:

3:38 PM Changeset [2153] by boender
- updated the proof some more
1:23 PM Changeset [2152] by boender
- this should compile
Note: See TracTimeline for information about the timeline view.