Timeline



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 …

Jun 18, 2012:

5:16 PM Changeset [2100] by tranquil
temporary solution to a bug where operations on spilled registers …
2:07 PM WikiStart edited by mulligan
(diff)
2:05 PM Matita-18-06-2012.tar.gz attached to WikiStart by mulligan
Matita snapshot for typechecking CPP submissions
2:02 PM WikiStart edited by mulligan
(diff)
2:00 PM WikiStart edited by mulligan
(diff)

Jun 15, 2012:

5:56 PM Changeset [2099] by boender
- added reference to Intel dev manual
5:29 PM Changeset [2098] by boender
- updates & changes
3:25 PM Changeset [2097] by mulligan
Consistency change (institution)
3:25 PM Changeset [2096] by mulligan
Changes to the English for Jaap, and some tidying up and making …
1:58 PM Changeset [2095] by mulligan
Added reference to CompCert? and CompCertTSO.
1:56 PM Changeset [2094] by boender
- oops
1:55 PM Changeset [2093] by boender
- added reference to CompCertTSO
1:38 PM Changeset [2092] by mulligan
Jaap noticed it's Randall Hyde not Holmes.
1:35 PM Changeset [2091] by boender
- systematically changed 'jump' to 'branch'
12:57 PM Changeset [2090] by mulligan
Fixed mistaken reference to RISC instead of CISC architectures.
11:54 AM Changeset [2089] by mulligan
Harmonised institution name to that used by Jaap
11:52 AM Changeset [2088] by mulligan
Added list of keywords as is required. Other minor changes.
11:40 AM Changeset [2087] by mulligan
Tidied up the paper, added a few more things, tidied and expanded …
11:39 AM Changeset [2086] by boender
- spell-check
11:36 AM Changeset [2085] by boender
- rewrote introduction - changed 'medium' to 'absolute' - added a bit …
1:17 AM Changeset [2084] by boender
- changed bibliography style - added CerCo? thanks - some words of …

Jun 14, 2012:

5:32 PM Changeset [2083] by mulligan
More work on paper from today.
4:26 PM Changeset [2082] by boender
- reworked and extended presentation of invariants
12:04 PM Changeset [2081] by sacerdot
Type of assembly fixed to be compatible with the old one and to take …
11:57 AM Changeset [2080] by boender
- added references to SDCC and gcc (thanks, Dominic) - updated sigma …
11:45 AM Changeset [2079] by sacerdot
sigma_policy_specification restyled
11:44 AM Changeset [2078] by sacerdot
sigma_policy_specification has been 1) strengthened 2) made nicer to …
10:45 AM Changeset [2077] by boender
- committed actual file instead of link
10:30 AM Changeset [2076] by garnier
First steps towards a simulation proof for switch removal.
10:25 AM Changeset [2075] by mulligan
Solved conflict in AssemblyProof?
10:23 AM Changeset [2074] by garnier
Prophylactic renaming of a relation
4:10 AM Changeset [2073] by sacerdot
All false daemons removed.
4:03 AM Changeset [2072] by sacerdot
We need to import Jaap's invariants now.
3:25 AM Changeset [2071] by sacerdot
More daemons closed, but one is suspect now.
2:18 AM Changeset [2070] by sacerdot
More daemons closed.

Jun 13, 2012:

7:58 PM Changeset [2069] by sacerdot
7:54 PM Changeset [2068] by sacerdot
7:50 PM Changeset [2067] by sacerdot
6:46 PM Changeset [2066] by mulligan
Finished for the day.
5:54 PM Changeset [2065] by boender
- committed another draft
5:29 PM Changeset [2064] by boender
- more progress
5:05 PM Changeset [2063] by mulligan
Minor fixes
5:00 PM Changeset [2062] by sacerdot
Everything repaired (broken because of new proof obligation for fetch).
4:59 PM Changeset [2061] by mulligan
Added Randall Holmes' Usenet post on branch displacement optimisation …
4:26 PM Changeset [2060] by mulligan
More work on paper.
3:44 PM Changeset [2059] by boender
- updated Policy to work better
3:17 PM Changeset [2058] by mulligan
First draft of changes to main sections (i.e. those describing the …
1:30 PM Changeset [2057] by sacerdot
Repaired (was broken by fetch_pseudo_instruction now taking a proof …
1:01 PM Changeset [2056] by sacerdot
Repaired, ported to new fetch_pseudo_assembly. The execute_n is …
12:11 PM Changeset [2055] by sacerdot
Warning: this commit adds an hypothesis that breaks all of assembly stuff.
11:58 AM Changeset [2054] by boender
- progress
11:02 AM Changeset [2053] by mulligan
Introduction changed, with many paragraphs deleted.
10:04 AM Changeset [2052] by mulligan
Initial commit of proposed CPP 2012 paper on the proof of correctness …

Jun 12, 2012:

5:49 PM Changeset [2051] by mulligan
Finished the Jmp case in the main theorem.
4:01 PM Changeset [2050] by campbell
Limit some normalization that doesn't seem to like.
3:49 PM Changeset [2049] by boender
- progress
2:46 PM Changeset [2048] by boender
- factorised jump decisions
2:18 PM Changeset [2047] by mulligan
Big bugs in policy calculations found. Waiting for Jaap's commit.
1:36 PM Changeset [2046] by boender
- removed old paper directory
1:35 PM Changeset [2045] by boender
- renamed paper directory
10:52 AM Changeset [2044] by campbell
PCs for RTLabs structured traces.
Note: See TracTimeline for information about the timeline view.