Timeline
Jun 27, 2011:
- 2:17 PM Changeset [1044] by
- - more fold/forall stuff
- 12:28 PM AssemblerFormalisation edited by
- (diff)
- 12:27 PM AssemblerFormalisation edited by
- (diff)
- 12:27 PM AssemblerFormalisation edited by
- (diff)
- 12:26 PM AssemblerFormalisation edited by
- (diff)
- 12:25 PM AssemblerFormalisation edited by
- (diff)
- 12:24 PM AssemblerFormalisation created by
- 12:05 PM WikiStart edited by
- (diff)
Jun 25, 2011:
- 2:32 AM Changeset [1043] by
- Axiom commented out.
- 2:30 AM Changeset [1042] by
- Dead code removed. Slow code uncommented.
Jun 24, 2011:
- 5:05 PM Changeset [1041] by
- fetch_assembly is still working after bug fix
- 4:54 PM Changeset [1040] by
- Bug fixed in assembly.
- 2:11 PM Changeset [1039] by
- fetch_assembly_pseudo2 repaired from dependent type madness
Jun 23, 2011:
- 5:40 PM Changeset [1038] by
- - some more BVT improvements
- 2:56 AM Changeset [1037] by
- Main theorem: comments are working again.
Jun 22, 2011:
- 11:38 PM Changeset [1036] by
- …
- 11:06 PM Changeset [1035] by
- Main theorem (broken because of dependent types) almost restored.
- 5:37 PM WikiStart edited by
- (diff)
- 5:36 PM WikiStart edited by
- (diff)
- 5:36 PM WikiStart edited by
- (diff)
- 5:30 PM WikiStart edited by
- (diff)
- 5:30 PM WikiStart edited by
- (diff)
- 5:29 PM WikiStart edited by
- (diff)
- 5:29 PM WikiStart edited by
- (diff)
- 5:23 PM WikiStart edited by
- (diff)
- 4:03 PM Changeset [1034] by
- various & sundry fold/forall lemmas
Jun 21, 2011:
- 3:08 PM Changeset [1033] by
- ispelled & submitted
- 3:04 PM Changeset [1032] by
- Final version.
- 2:25 PM Changeset [1031] by
- ..
- 2:24 PM Changeset [1030] by
- …
- 2:23 PM Changeset [1029] by
- …
- 2:08 PM Changeset [1028] by
- One more sentence restored and fitted in.
- 2:02 PM Changeset [1027] by
- Bug fixed in figure.
- 12:47 PM Changeset [1026] by
- final version? under 16 pages
- 12:35 PM Changeset [1025] by
- removing stray single words to reduce page usage
- 12:27 PM Changeset [1024] by
- tidied explanation of proof
- 12:23 PM Changeset [1023] by
- changes to english in matita section, shrunk diagrams in introduction …
- 12:18 PM Changeset [1022] by
- …
- 12:15 PM Changeset [1021] by
- tidied english in sect 3
- 12:09 PM Changeset [1020] by
- More on Matita.
- 11:39 AM Changeset [1019] by
- Finished rewriting of Section 3.
- 11:21 AM Changeset [1018] by
- tidying
- 11:15 AM Changeset [1017] by
- complete, just under 16 pages
- 10:20 AM Changeset [1016] by
- Many fixes to the code snippets.
- 4:27 AM Changeset [1015] by
- One intermediate version of main_thm0 close to be repaired.
- 2:02 AM Changeset [1014] by
- The main theorem is completely broken (again).
- 1:52 AM Changeset [1013] by
- more added
- 12:33 AM Changeset [1012] by
- just a few things left to change
Jun 20, 2011:
- 6:39 PM Changeset [1011] by
- …
- 6:18 PM Changeset [1010] by
- more added, finished up to end of subsect 3.2
- 6:01 PM Changeset [1009] by
- added line number counts, etc.
- 5:58 PM Changeset [1008] by
- …
- 5:57 PM Changeset [1007] by
- added explanation of sdcc
- 5:51 PM Changeset [1006] by
- - added fold + lemmas on fold
- 5:41 PM Changeset [1005] by
- …
- 5:32 PM Changeset [1004] by
- changes to typesetting
- 5:30 PM Changeset [1003] by
- …
- 5:27 PM Changeset [1002] by
- …
- 5:26 PM Changeset [1001] by
- reworded intro
- 5:25 PM Changeset [1000] by
- …
- 5:07 PM Changeset [999] by
- conclusions
- 5:05 PM Changeset [998] by
- Half repaired, half broken. Most functions no longer return option …
- 3:43 PM Changeset [997] by
- minor linguistic polishing
- 3:41 PM Changeset [996] by
- Minor fixes.
- 3:27 PM Changeset [995] by
- changes
Jun 17, 2011:
- 6:42 PM Changeset [994] by
- small changes
- 6:28 PM Changeset [993] by
- More Russell everywhere; getting closer to the goal.
- 6:05 PM Changeset [992] by
- a few more axioms closed
- 5:17 PM Changeset [991] by
- loads of axioms related to equality on instructions closed
- 1:30 PM Changeset [990] by
- Do no longer use the daemon automatically :-)
- 10:28 AM Changeset [989] by
- Type of build_maps strengthened.
Jun 16, 2011:
- 11:27 PM Changeset [988] by
- Proof restored.
- 6:08 PM Changeset [987] by
- Real parameterization over the policy.
- 5:23 PM Changeset [986] by
- changes to paper
- 4:50 PM Changeset [985] by
- 1) Major refactoring: proofs moved where they should be. 2) New …
- 4:16 PM Changeset [984] by
- updates
- 4:00 PM Changeset [983] by
- more work added
- 2:39 PM Changeset [982] by
- - this should work (see previous commit)
- 2:39 PM Changeset [981] by
- added more, worked on conclusions and related work. need just to …
- 2:37 PM Changeset [980] by
- - displaced some lemmas (jmeq) from AssemblyProof?
- 2:26 PM Changeset [979] by
- …
- 1:32 PM Changeset [978] by
- Update remaining Clight examples.
- 12:12 PM Changeset [977] by
- #$%@#$@#$
- 12:02 PM Changeset [976] by
- more changes, rearranged paper to put lemmas/defns in correct order, …
- 11:34 AM Changeset [975] by
- …
- 11:24 AM Changeset [974] by
- more added
- 10:05 AM Changeset [973] by
- work from yesterday that could not be committed
- 12:22 AM Changeset [972] by
- …
- 12:07 AM Changeset [971] by
- …
Jun 15, 2011:
- 5:59 PM Changeset [970] by
- commit as i need some money for the communists
- 5:27 PM Changeset [969] by
- more work on paper, nearly finished policy discussion
- 4:32 PM Changeset [968] by
- work on paper
- 4:15 PM Changeset [967] by
- Update RTLabs pretty printer and examples.
- 4:15 PM Changeset [966] by
- Update Cminor pretty printer and some examples.
- 4:15 PM Changeset [965] by
- Update some Clight examples.
- 4:15 PM Changeset [964] by
- Rest of cast fix.
- 4:15 PM Changeset [963] by
- Extra debugging aid for animation of semantics.
- 4:15 PM Changeset [962] by
- Casts should use source type's signedness, not the target's.
- 4:15 PM Changeset [961] by
- Use precise bitvector sizes throughout the front end, rather than …
- 3:39 PM Changeset [960] by
- more work on paper
- 2:22 PM Changeset [959] by
- …
- 1:33 PM Changeset [958] by
- …
- 1:30 PM Changeset [957] by
- …
- 12:54 PM Changeset [956] by
- changes prior to claudio's editing
- 12:00 PM Changeset [955] by
- more work on conclusions
- 11:30 AM Changeset [954] by
- more changes to introduction
- 10:53 AM Changeset [953] by
- more changes, including additions to the bibliography, and tightening …
- 10:15 AM Changeset [952] by
- work from yesterday
- 1:35 AM Changeset [951] by
- long call case completed
Jun 14, 2011:
- 5:46 PM Changeset [950] by
- Horrible sub-proof finished :-)
Jun 13, 2011:
- 6:42 PM Changeset [949] by
- resolved conflict, work from today
- 3:28 PM Changeset [948] by
- Some progress on the Call case.
- 2:14 PM Changeset [947] by
- …
- 11:37 AM Changeset [946] by
- Jmp case repaired after addition of MAP hypothesis.
- 11:15 AM Changeset [945] by
- more small changes to proof of main thrm
- 10:54 AM Changeset [944] by
- split definition
- 1:46 AM Changeset [943] by
- …
- 1:14 AM Changeset [942] by
- New invariant for the main theorem. The new invariant is much more …
Jun 11, 2011:
- 11:37 PM Changeset [941] by
- Jmp case finished up to arithmetical properties.
Jun 10, 2011:
- 6:49 PM Changeset [940] by
- more changes to inc case of main theorem
- 6:42 PM Changeset [939] by
- Long Jmp case finished.
- 6:36 PM Changeset [938] by
- …
- 4:48 PM Changeset [937] by
- resolved conflict in assembly_proof, more lemmas added
- 4:20 PM Changeset [936] by
- Ticks are now handled correctly everywhere and the main proof takes …
- 1:15 PM Changeset [935] by
- changes to status and assembly proof
- 3:25 AM Changeset [934] by
- …
- 3:20 AM Changeset [933] by
- New proof strategy.
- 3:10 AM Changeset [932] by
- …
- 2:53 AM Changeset [931] by
- …
- 2:19 AM Changeset [930] by
- Comment, Cost, ADD, ADC cases done.
Jun 9, 2011:
- 6:40 PM Changeset [929] by
- added ticks_of function
- 6:07 PM Changeset [928] by
- Technical splitting.
- 5:06 PM Changeset [927] by
- changes
- 5:06 PM Changeset [926] by
- Main theorem false because of ticks :-(
- 4:42 PM Changeset [925] by
- …
- 4:14 PM Changeset [924] by
- …
- 3:51 PM Changeset [923] by
- Main theorem made nice... but unprovable at the moment.
- 3:38 PM Changeset [922] by
- changes to get assemblyproof to compile
- 3:21 PM Changeset [921] by
- resolved conflict, fixed bugs
- 2:52 PM Changeset [920] by
- - corrected mov instruction
- 2:15 PM Changeset [919] by
- Back to a readable statement.
- 1:13 PM Changeset [918] by
- headers added, etc.
- 1:10 PM Changeset [917] by
- outline of cpp paper committed
- 11:56 AM Changeset [916] by
- Fix for jump_expansion_policy.
- 11:30 AM Changeset [915] by
- finished changes to fetch_assembly_pseudo2
- 11:10 AM Changeset [914] by
- - complete.
- 10:50 AM Changeset [913] by
- - temporary commit s.t. Assembly compiles
- 10:45 AM Changeset [912] by
- Readable main theorem statement.
- 10:38 AM Changeset [911] by
- Type of set_code_memory generalized.
- 10:36 AM Changeset [910] by
- removed bug in execute_1_pseudoinstruction
- 1:27 AM Changeset [909] by
- Back to the main theorem.
- 1:22 AM Changeset [908] by
- Next big lemma proved!
Jun 8, 2011:
- 6:15 PM Changeset [907] by
- - added quadruples to Util - start of implementation of new jump …
- 6:12 PM Changeset [906] by
- …
- 6:07 PM Changeset [905] by
- work from today
- 5:53 PM Changeset [904] by
- Cleanup.
- 5:53 PM Changeset [903] by
- Statement of new main lemma (as axiom).
- 5:28 PM Changeset [902] by
- Cleanup.
- 5:27 PM Changeset [901] by
- Second main lemma proved.
- 2:24 PM Changeset [900] by
- New implementation of flatten was bugged: fixed.
- 2:17 PM Changeset [899] by
- changed defn. of flatten
- 1:14 PM Changeset [898] by
- Update pretty printers and examples.
- 10:59 AM Changeset [897] by
- Proof completed, fetch and assembly are mutual inverses.
- 10:38 AM Changeset [896] by
- Proof finished (but ugly) :-)
- 10:30 AM Changeset [895] by
- Fetch function fixed: alla AJMPS were ACALL (and the other way around) …
- 10:09 AM Changeset [894] by
- Bug more evident.
- 9:46 AM PublicationVenues edited by
- (diff)
Jun 7, 2011:
- 5:32 PM Changeset [893] by
- Cleanup.
- 5:28 PM Changeset [892] by
- First fundamental lemma almost finished.
- 4:53 PM Changeset [891] by
- Revise proofs affected by recent matita change.
- 2:56 AM Changeset [890] by
- Better statement, begin of uniform proof.
Jun 6, 2011:
- 11:07 PM Changeset [889] by
- Minor changes because of the new, weaker (but much faster) delift.
- 4:28 PM Changeset [888] by
- Use simplified conditionals in RTLabs, following the prototype.
- 3:55 PM Changeset [887] by
- Start bringing RTLabs into line with the prototype compiler: - a …
- 1:27 PM Changeset [886] by
- Put types into parameter and variable lists in Cminor. Temporarily …
Jun 5, 2011:
- 2:04 AM Changeset [885] by
- Proof almost finished, but rewritings are extremely slow.
Jun 4, 2011:
Jun 3, 2011:
- 6:36 PM Changeset [883] by
- Merged done well.
- 5:35 PM Changeset [882] by
- Fix up fragile proofs for current version of matita.
- 5:35 PM Changeset [881] by
- Sort out regions in Cminor to fix Clight to Cminor translation of Ederef.
- 5:35 PM Changeset [880] by
- Add type information into Cminor. As a result, the Clight to Cminor …
- 5:35 PM Changeset [879] by
- Refine "AST" types to include size/signedness information.
- 5:35 PM Changeset [878] by
- Removal of manually inserted record projections.
- 4:11 PM Changeset [877] by
- work from today
- 4:03 PM Changeset [876] by
- …
- 11:21 AM Changeset [875] by
- …
- 10:13 AM Changeset [874] by
- Tactics no longer works.
Jun 2, 2011:
- 5:47 PM Changeset [873] by
- Script improved. Maybe this requires an svn up of Matita.
Jun 1, 2011:
- 5:32 PM Changeset [872] by
- changes from today, need investigation of reduction machine
May 31, 2011:
- 6:05 PM Changeset [871] by
- …
- 5:54 PM Changeset [870] by
- more changes
- 5:28 PM Changeset [869] by
- More progress.
- 5:28 PM Changeset [868] by
- more changes
- 5:01 PM Changeset [867] by
- changes to assembly proof
- 3:03 PM Changeset [866] by
- Significant improvement in the proof.
- 11:45 AM Changeset [865] by
- Renaming.
- 11:27 AM Changeset [864] by
- resolved conflict
- 2:56 AM Changeset [863] by
- Yet another fix to the statement.
- 2:33 AM Changeset [862] by
- …
- 1:39 AM Changeset [861] by
- Statement of the lemma fixed (again!) Some preliminary work on …
May 30, 2011:
- 6:43 PM Changeset [860] by
- Progress in the proof.
- 6:38 PM Changeset [859] by
- more added
- 4:43 PM Changeset [858] by
- If then else notation improved.
- 4:37 PM Changeset [857] by
- Notations.
- 1:44 PM Changeset [856] by
- 1. if_then_else is now a notation for match with (to allow Russell to …
Note: See TracTimeline
for information about the timeline view.
