Timeline


and

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 …

Jun 11, 2011:

11:37 PM Changeset [941] by sacerdot
Jmp case finished up to arithmetical properties.

Jun 10, 2011:

6:49 PM Changeset [940] by mulligan
more changes to inc case of main theorem
6:42 PM Changeset [939] by sacerdot
Long Jmp case finished.
6:36 PM Changeset [938] by sacerdot
4:48 PM Changeset [937] by mulligan
resolved conflict in assembly_proof, more lemmas added
4:20 PM Changeset [936] by sacerdot
Ticks are now handled correctly everywhere and the main proof takes …
1:15 PM Changeset [935] by mulligan
changes to status and assembly proof
3:25 AM Changeset [934] by sacerdot
3:20 AM Changeset [933] by sacerdot
New proof strategy.
3:10 AM Changeset [932] by sacerdot
2:53 AM Changeset [931] by sacerdot
2:19 AM Changeset [930] by sacerdot
Comment, Cost, ADD, ADC cases done.

Jun 9, 2011:

6:40 PM Changeset [929] by mulligan
added ticks_of function
6:07 PM Changeset [928] by sacerdot
Technical splitting.
5:06 PM Changeset [927] by mulligan
changes
5:06 PM Changeset [926] by sacerdot
Main theorem false because of ticks :-(
4:42 PM Changeset [925] by sacerdot
4:14 PM Changeset [924] by sacerdot
3:51 PM Changeset [923] by sacerdot
Main theorem made nice... but unprovable at the moment.
3:38 PM Changeset [922] by mulligan
changes to get assemblyproof to compile
3:21 PM Changeset [921] by mulligan
resolved conflict, fixed bugs
2:52 PM Changeset [920] by boender
- corrected mov instruction
2:15 PM Changeset [919] by sacerdot
Back to a readable statement.
1:13 PM Changeset [918] by mulligan
headers added, etc.
1:10 PM Changeset [917] by mulligan
outline of cpp paper committed
11:56 AM Changeset [916] by sacerdot
Fix for jump_expansion_policy.
11:30 AM Changeset [915] by mulligan
finished changes to fetch_assembly_pseudo2
11:10 AM Changeset [914] by boender
- complete.
10:50 AM Changeset [913] by boender
- temporary commit s.t. Assembly compiles
10:45 AM Changeset [912] by sacerdot
Readable main theorem statement.
10:38 AM Changeset [911] by sacerdot
Type of set_code_memory generalized.
10:36 AM Changeset [910] by mulligan
removed bug in execute_1_pseudoinstruction
1:27 AM Changeset [909] by sacerdot
Back to the main theorem.
1:22 AM Changeset [908] by sacerdot
Next big lemma proved!

Jun 8, 2011:

6:15 PM Changeset [907] by boender
- added quadruples to Util - start of implementation of new jump …
6:12 PM Changeset [906] by sacerdot
6:07 PM Changeset [905] by mulligan
work from today
5:53 PM Changeset [904] by sacerdot
Cleanup.
5:53 PM Changeset [903] by sacerdot
Statement of new main lemma (as axiom).
5:28 PM Changeset [902] by sacerdot
Cleanup.
5:27 PM Changeset [901] by sacerdot
Second main lemma proved.
2:24 PM Changeset [900] by sacerdot
New implementation of flatten was bugged: fixed.
2:17 PM Changeset [899] by mulligan
changed defn. of flatten
1:14 PM Changeset [898] by campbell
Update pretty printers and examples.
10:59 AM Changeset [897] by sacerdot
Proof completed, fetch and assembly are mutual inverses.
10:38 AM Changeset [896] by sacerdot
Proof finished (but ugly) :-)
10:30 AM Changeset [895] by sacerdot
Fetch function fixed: alla AJMPS were ACALL (and the other way around) …
10:09 AM Changeset [894] by sacerdot
Bug more evident.
9:46 AM PublicationVenues edited by mulligan
(diff)

Jun 7, 2011:

5:32 PM Changeset [893] by sacerdot
Cleanup.
5:28 PM Changeset [892] by sacerdot
First fundamental lemma almost finished.
4:53 PM Changeset [891] by campbell
Revise proofs affected by recent matita change.
2:56 AM Changeset [890] by sacerdot
Better statement, begin of uniform proof.

Jun 6, 2011:

11:07 PM Changeset [889] by sacerdot
Minor changes because of the new, weaker (but much faster) delift.
4:28 PM Changeset [888] by campbell
Use simplified conditionals in RTLabs, following the prototype.
3:55 PM Changeset [887] by campbell
Start bringing RTLabs into line with the prototype compiler: - a …
1:27 PM Changeset [886] by campbell
Put types into parameter and variable lists in Cminor. Temporarily …

Jun 5, 2011:

2:04 AM Changeset [885] by sacerdot
Proof almost finished, but rewritings are extremely slow.

Jun 4, 2011:

6:16 PM Changeset [884] by sacerdot

Jun 3, 2011:

6:36 PM Changeset [883] by sacerdot
Merged done well.
5:35 PM Changeset [882] by campbell
Fix up fragile proofs for current version of matita.
5:35 PM Changeset [881] by campbell
Sort out regions in Cminor to fix Clight to Cminor translation of Ederef.
5:35 PM Changeset [880] by campbell
Add type information into Cminor. As a result, the Clight to Cminor …
5:35 PM Changeset [879] by campbell
Refine "AST" types to include size/signedness information.
5:35 PM Changeset [878] by campbell
Removal of manually inserted record projections.
4:11 PM Changeset [877] by mulligan
work from today
4:03 PM Changeset [876] by sacerdot
11:21 AM Changeset [875] by sacerdot
10:13 AM Changeset [874] by sacerdot
Tactics no longer works.

Jun 2, 2011:

5:47 PM Changeset [873] by sacerdot
Script improved. Maybe this requires an svn up of Matita.

Jun 1, 2011:

5:32 PM Changeset [872] by mulligan
changes from today, need investigation of reduction machine

May 31, 2011:

6:05 PM Changeset [871] by sacerdot
5:54 PM Changeset [870] by mulligan
more changes
5:28 PM Changeset [869] by sacerdot
More progress.
5:28 PM Changeset [868] by mulligan
more changes
5:01 PM Changeset [867] by mulligan
changes to assembly proof
3:03 PM Changeset [866] by sacerdot
Significant improvement in the proof.
11:45 AM Changeset [865] by sacerdot
Renaming.
11:27 AM Changeset [864] by mulligan
resolved conflict
2:56 AM Changeset [863] by sacerdot
Yet another fix to the statement.
2:33 AM Changeset [862] by sacerdot
1:39 AM Changeset [861] by sacerdot
Statement of the lemma fixed (again!) Some preliminary work on …

May 30, 2011:

6:43 PM Changeset [860] by sacerdot
Progress in the proof.
6:38 PM Changeset [859] by mulligan
more added
4:43 PM Changeset [858] by sacerdot
If then else notation improved.
4:37 PM Changeset [857] by sacerdot
Notations.
1:44 PM Changeset [856] by sacerdot
1. if_then_else is now a notation for match with (to allow Russell to …
Note: See TracTimeline for information about the timeline view.