Timeline



Jul 13, 2011:

5:37 PM Changeset [1067] by mulligan
more smaller changes
5:12 PM Changeset [1066] by mulligan
changes from today
4:02 PM Changeset [1065] by campbell
Note a couple of deviations from the prototype.

Jul 12, 2011:

5:52 PM Changeset [1064] by mulligan
changes from today, nearly complete rtlabs translation pass

Jul 11, 2011:

5:52 PM Changeset [1063] by mulligan
changes from today
2:09 PM Changeset [1062] by mulligan
separated jmeq and coercions from foldstuff.ma in order to fix the …

Jul 8, 2011:

5:49 PM Changeset [1061] by mulligan
more work, bug found, ridiculous map3 function with dep. types added
12:17 PM Changeset [1060] by mulligan
work from this morning and yesterday

Jul 6, 2011:

6:09 PM Changeset [1059] by mulligan
work from today, bit of a mess at the moment
1:29 PM Changeset [1058] by campbell
Evict CompCert? Maps interface in favour of BitVectorTries?.

Jul 5, 2011:

5:53 PM Changeset [1057] by mulligan
changes from today
4:25 PM Changeset [1056] by campbell
Switch to delayed identifier error scheme.
12:15 PM Changeset [1055] by mulligan
changes to how identifiers are generated
9:51 AM Changeset [1054] by boender
- proven policy safe

Jul 4, 2011:

6:20 PM Changeset [1053] by mulligan
changes
3:31 PM Changeset [1052] by mulligan
removed offsets after reading cerco mailing list
1:49 PM Changeset [1051] by mulligan
removed superfluous addressing mode code from RTLabs/syntax.ma
10:43 AM Changeset [1050] by mulligan
adding dependent types to map datastructure to remove all option …

Jul 1, 2011:

5:45 PM Changeset [1049] by mulligan
more stuff added
5:11 PM Changeset [1048] by mulligan
added implementation of haskell associative maps to clean up the mess …

Jun 29, 2011:

5:38 PM Changeset [1047] by mulligan
more work from today
12:15 PM Changeset [1046] by mulligan
syntax of rtlabs was wrong: cast not const. more added to rtlabs --> …
10:47 AM Changeset [1045] by mulligan
resolved conflict in rtlabs

Jun 27, 2011:

2:17 PM Changeset [1044] by boender
- more fold/forall stuff
12:28 PM AssemblerFormalisation edited by mulligan
(diff)
12:27 PM AssemblerFormalisation edited by mulligan
(diff)
12:27 PM AssemblerFormalisation edited by mulligan
(diff)
12:26 PM AssemblerFormalisation edited by mulligan
(diff)
12:25 PM AssemblerFormalisation edited by mulligan
(diff)
12:24 PM latest.tar.bz2 attached to AssemblerFormalisation by mulligan
Latest bundle of development files.
12:24 PM AssemblerFormalisation created by mulligan
12:05 PM WikiStart edited by mulligan
(diff)

Jun 25, 2011:

2:32 AM Changeset [1043] by sacerdot
Axiom commented out.
2:30 AM Changeset [1042] by sacerdot
Dead code removed. Slow code uncommented.

Jun 24, 2011:

5:05 PM Changeset [1041] by sacerdot
fetch_assembly is still working after bug fix
4:54 PM Changeset [1040] by sacerdot
Bug fixed in assembly.
2:11 PM Changeset [1039] by sacerdot
fetch_assembly_pseudo2 repaired from dependent type madness

Jun 23, 2011:

5:40 PM Changeset [1038] by boender
- some more BVT improvements
2:56 AM Changeset [1037] by sacerdot
Main theorem: comments are working again.

Jun 22, 2011:

11:38 PM Changeset [1036] by sacerdot
11:06 PM Changeset [1035] by sacerdot
Main theorem (broken because of dependent types) almost restored.
5:37 PM WikiStart edited by mulligan
(diff)
5:36 PM WikiStart edited by mulligan
(diff)
5:36 PM WikiStart edited by mulligan
(diff)
5:30 PM WikiStart edited by mulligan
(diff)
5:30 PM WikiStart edited by mulligan
(diff)
5:29 PM WikiStart edited by mulligan
(diff)
5:29 PM WikiStart edited by mulligan
(diff)
5:23 PM WikiStart edited by mulligan
(diff)
4:03 PM Changeset [1034] by boender
various & sundry fold/forall lemmas

Jun 21, 2011:

3:08 PM Changeset [1033] by sacerdot
ispelled & submitted
3:04 PM Changeset [1032] by sacerdot
Final version.
2:25 PM Changeset [1031] by sacerdot
..
2:24 PM Changeset [1030] by sacerdot
2:23 PM Changeset [1029] by sacerdot
2:08 PM Changeset [1028] by sacerdot
One more sentence restored and fitted in.
2:02 PM Changeset [1027] by sacerdot
Bug fixed in figure.
12:47 PM Changeset [1026] by mulligan
final version? under 16 pages
12:35 PM Changeset [1025] by mulligan
removing stray single words to reduce page usage
12:27 PM Changeset [1024] by mulligan
tidied explanation of proof
12:23 PM Changeset [1023] by mulligan
changes to english in matita section, shrunk diagrams in introduction …
12:18 PM Changeset [1022] by sacerdot
12:15 PM Changeset [1021] by mulligan
tidied english in sect 3
12:09 PM Changeset [1020] by sacerdot
More on Matita.
11:39 AM Changeset [1019] by sacerdot
Finished rewriting of Section 3.
11:21 AM Changeset [1018] by mulligan
tidying
11:15 AM Changeset [1017] by mulligan
complete, just under 16 pages
10:20 AM Changeset [1016] by sacerdot
Many fixes to the code snippets.
4:27 AM Changeset [1015] by sacerdot
One intermediate version of main_thm0 close to be repaired.
2:02 AM Changeset [1014] by sacerdot
The main theorem is completely broken (again).
1:52 AM Changeset [1013] by mulligan
more added
12:33 AM Changeset [1012] by mulligan
just a few things left to change

Jun 20, 2011:

6:39 PM Changeset [1011] by mulligan
6:18 PM Changeset [1010] by mulligan
more added, finished up to end of subsect 3.2
6:01 PM Changeset [1009] by mulligan
added line number counts, etc.
5:58 PM Changeset [1008] by mulligan
5:57 PM Changeset [1007] by mulligan
added explanation of sdcc
5:51 PM Changeset [1006] by boender
- added fold + lemmas on fold
5:41 PM Changeset [1005] by sacerdot
5:32 PM Changeset [1004] by mulligan
changes to typesetting
5:30 PM Changeset [1003] by sacerdot
5:27 PM Changeset [1002] by sacerdot
5:26 PM Changeset [1001] by mulligan
reworded intro
5:25 PM Changeset [1000] by sacerdot
5:07 PM Changeset [999] by mulligan
conclusions
5:05 PM Changeset [998] by sacerdot
Half repaired, half broken. Most functions no longer return option …
3:43 PM Changeset [997] by mulligan
minor linguistic polishing
3:41 PM Changeset [996] by sacerdot
Minor fixes.
3:27 PM Changeset [995] by mulligan
changes

Jun 17, 2011:

6:42 PM Changeset [994] by mulligan
small changes
6:28 PM Changeset [993] by sacerdot
More Russell everywhere; getting closer to the goal.
6:05 PM Changeset [992] by mulligan
a few more axioms closed
5:17 PM Changeset [991] by mulligan
loads of axioms related to equality on instructions closed
1:30 PM Changeset [990] by sacerdot
Do no longer use the daemon automatically :-)
10:28 AM Changeset [989] by sacerdot
Type of build_maps strengthened.

Jun 16, 2011:

11:27 PM Changeset [988] by sacerdot
Proof restored.
6:08 PM Changeset [987] by sacerdot
Real parameterization over the policy.
5:23 PM Changeset [986] by mulligan
changes to paper
4:50 PM Changeset [985] by sacerdot
1) Major refactoring: proofs moved where they should be. 2) New …
4:16 PM Changeset [984] by mulligan
updates
4:00 PM Changeset [983] by mulligan
more work added
2:39 PM Changeset [982] by boender
- this should work (see previous commit)
2:39 PM Changeset [981] by mulligan
added more, worked on conclusions and related work. need just to …
2:37 PM Changeset [980] by boender
- displaced some lemmas (jmeq) from AssemblyProof?
2:26 PM Changeset [979] by sacerdot
1:32 PM Changeset [978] by campbell
Update remaining Clight examples.
12:12 PM Changeset [977] by sacerdot
#$%@#$@#$
12:02 PM Changeset [976] by mulligan
more changes, rearranged paper to put lemmas/defns in correct order, …
11:34 AM Changeset [975] by sacerdot
11:24 AM Changeset [974] by mulligan
more added
10:05 AM Changeset [973] by mulligan
work from yesterday that could not be committed
12:22 AM Changeset [972] by sacerdot
12:07 AM Changeset [971] by sacerdot

Jun 15, 2011:

5:59 PM Changeset [970] by mulligan
commit as i need some money for the communists
5:27 PM Changeset [969] by mulligan
more work on paper, nearly finished policy discussion
4:32 PM Changeset [968] by mulligan
work on paper
4:15 PM Changeset [967] by campbell
Update RTLabs pretty printer and examples.
4:15 PM Changeset [966] by campbell
Update Cminor pretty printer and some examples.
4:15 PM Changeset [965] by campbell
Update some Clight examples.
4:15 PM Changeset [964] by campbell
Rest of cast fix.
4:15 PM Changeset [963] by campbell
Extra debugging aid for animation of semantics.
4:15 PM Changeset [962] by campbell
Casts should use source type's signedness, not the target's.
4:15 PM Changeset [961] by campbell
Use precise bitvector sizes throughout the front end, rather than …
3:39 PM Changeset [960] by mulligan
more work on paper
2:22 PM Changeset [959] by sacerdot
1:33 PM Changeset [958] by sacerdot
1:30 PM Changeset [957] by sacerdot
12:54 PM Changeset [956] by mulligan
changes prior to claudio's editing
12:00 PM Changeset [955] by mulligan
more work on conclusions
11:30 AM Changeset [954] by mulligan
more changes to introduction
10:53 AM Changeset [953] by mulligan
more changes, including additions to the bibliography, and tightening …
10:15 AM Changeset [952] by mulligan
work from yesterday
1:35 AM Changeset [951] by sacerdot
long call case completed

Jun 14, 2011:

5:46 PM Changeset [950] by sacerdot
Horrible sub-proof finished :-)

Jun 13, 2011:

6:42 PM Changeset [949] by mulligan
resolved conflict, work from today
3:28 PM Changeset [948] by sacerdot
Some progress on the Call case.
2:14 PM Changeset [947] by sacerdot
11:37 AM Changeset [946] by sacerdot
Jmp case repaired after addition of MAP hypothesis.
11:15 AM Changeset [945] by mulligan
more small changes to proof of main thrm
10:54 AM Changeset [944] by mulligan
split definition
1:46 AM Changeset [943] by sacerdot
1:14 AM Changeset [942] by sacerdot
New invariant for the main theorem. The new invariant is much more …
Note: See TracTimeline for information about the timeline view.