Timeline


and

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

Jul 3, 2012:

6:12 PM Changeset [2151] by sacerdot
1. Lemmas from AssemblyProof? anticipated to Assembly.ma 2. Jaap's …
11:30 AM Changeset [2150] by campbell
Add labelling result to the correctness file.
4:19 AM Changeset [2149] by sacerdot
Code shuffling to proper places.
4:14 AM Changeset [2148] by sacerdot
1. specification made more user-friendly for AssemblyProof? 2. no more …
3:53 AM Changeset [2147] by sacerdot
Theorem closed (up to one more lemma on overflow), but new proof …
3:09 AM Changeset [2146] by sacerdot
1. specification fixed again 2. the proof in AssemblyProof? is now …

Jul 2, 2012:

4:12 PM Changeset [2145] by campbell
Cost labelling doesn't affect interaction.
3:59 PM Changeset [2144] by sacerdot
1. Policy specification fixed 2. Proof of monotonicity of sigma
11:37 AM Changeset [2143] by mulligan
Changes to the subaddressing mode elim functions moved into their …

Jun 29, 2012:

10:09 AM Changeset [2142] by sacerdot
Down to one daemon that requires one lemma (monotonicity of sigma).

Jun 28, 2012:

8:08 PM Changeset [2141] by boender
- committed working version
6:47 PM Changeset [2140] by mulligan
Done the hardest cases in the main theorem. Just got a few daemons to …
5:42 PM Changeset [2139] by mulligan
Changes to get the main lemma compiling again. Changes pushed into …
4:47 PM Changeset [2138] by sacerdot
Invariant exported from proof of assembly_ok.
3:00 PM Changeset [2137] by sacerdot
Bug fixed in specification.
2:58 PM Changeset [2136] by sacerdot
2:34 PM Changeset [2135] by sacerdot
One complex daemon changed to two simpler ones.
12:37 PM Changeset [2134] by campbell
Split out behavioural equivalence spec for labelling.
10:59 AM Changeset [2133] by boender
- moved does_not_occur_occur_absurd
10:41 AM Changeset [2132] by sacerdot
Two more daemons closed, one left.
12:55 AM Changeset [2131] by sacerdot
No more need for functional extensionality.

Jun 27, 2012:

10:19 PM Changeset [2130] by sacerdot
Proof repaired after Dominic's bug fix.
7:14 PM Changeset [2129] by mulligan
Large changes from today trying to complete the main theorem. Again :(
5:05 PM Changeset [2128] by sacerdot
Final shuffling around
4:59 PM Changeset [2127] by sacerdot
Last daemon closed
4:56 PM Changeset [2126] by sacerdot
Proof improved (for case 3) + new proof (for case 11)
4:28 PM Changeset [2125] by boender
- some more displacement from Policy to Util
4:23 PM Changeset [2124] by sacerdot
Much more shuffling around to proper places
4:04 PM Changeset [2123] by boender
- moved is_well_labeled_p to Status and instruction_is_label to ASM …
3:36 PM Changeset [2122] by sacerdot
More stuff moved around in proper places
3:30 PM Changeset [2121] by sacerdot
More functions moved to the places they belong to
12:59 PM Changeset [2120] by campbell
Fix victim of alloc unfolding.
12:09 PM Changeset [2119] by sacerdot
load_code_memory moved to Fetch.ma and proved correct w.r.t. next …
12:04 PM Changeset [2118] by campbell
Labelling preserves behaviour.
12:04 PM Changeset [2117] by campbell
Workaround for bug in Matita.
11:46 AM Changeset [2116] by sacerdot
load_code_memory will be moved into Fetch.ma in the next commit. This …
1:59 AM Changeset [2115] by sacerdot
Old commented out code removed
1:40 AM Changeset [2114] by sacerdot
Proof repaired
12:49 AM Changeset [2113] by sacerdot
Proof by cases repaired; dead code removed.

Jun 26, 2012:

11:47 PM Changeset [2112] by sacerdot
WARNING: this commit may break some code. - dead/useless code removed
5:30 PM Changeset [2111] by sacerdot
Cleanup: lemmas/theorems/axioms moved to the right places.
4:05 PM Changeset [2110] by sacerdot
2:47 PM Changeset [2109] by mulligan
Finished porting the large, main lemma to the new notion of jump …

Jun 25, 2012:

2:39 PM Changeset [2108] by mulligan
Various axioms closed and others moved around. Uncommented main lemma …

Jun 22, 2012:

2:07 PM Changeset [2107] by campbell
Memory initialisation and program transformations.

Jun 21, 2012:

5:21 PM Changeset [2106] by campbell
Fix up a couple of proofs broken by recent changes.
5:21 PM Changeset [2105] by campbell
Show some results about globalenvs and program transformations.
5:21 PM Changeset [2104] by campbell
Fill in misc axiom.
5:21 PM Changeset [2103] by campbell
Make transform_*program take a more general transformation to make …

Jun 20, 2012:

4:51 PM Changeset [2102] by boender
- some small changes

Jun 19, 2012:

4:43 PM Changeset [2101] by boender
- renamed medium to absolute jump - revised proofs of policy, some …
Note: See TracTimeline for information about the timeline view.