Timeline
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 …
May 27, 2011:
- 6:11 PM Changeset [855] by
- changes from today
- 5:13 PM Changeset [854] by
- commit to avoid conflicts
- 1:58 PM Changeset [853] by
- …
- 1:26 PM Changeset [852] by
- foldl_strong outer definition
- 12:40 PM Changeset [851] by
- strong foldl added
- 12:58 AM Changeset [850] by
- More informative foldl: foldll.
May 26, 2011:
- 6:41 PM Changeset [849] by
- …
- 6:26 PM Changeset [848] by
- …
- 2:16 PM Changeset [847] by
- Several bugs fixed in Matita.
May 25, 2011:
- 6:10 PM Changeset [846] by
- changes
- 6:09 PM Changeset [845] by
- Nightmare…
- 4:26 PM Changeset [844] by
- Useless code removed.
- 3:57 PM Changeset [843] by
- Function moved from Interpret to Status.
- 3:57 PM Changeset [842] by
- Bug fixed.
- 2:33 PM Changeset [841] by
- Minor changes.
- 1:57 PM Changeset [840] by
- sigma defined
- 1:31 PM Changeset [839] by
- More experiments.
- 12:08 PM Changeset [838] by
- Restored.
- 11:49 AM Changeset [837] by
- changes complete
- 11:43 AM Changeset [836] by
- changes to assembly functions
- 11:06 AM Changeset [835] by
- Old experiments removed.
- 12:10 AM Changeset [834] by
- Russell at work.
May 24, 2011:
- 11:19 PM Changeset [833] by
- Bug fixed to make the file compile. But the type of the assembly …
- 6:40 PM Changeset [832] by
- work from today
- 4:01 PM Changeset [831] by
- Progress in proofs.
- 2:27 PM Changeset [830] by
- Move files that accidentally ended up in the root of the repository.
- 2:06 PM Changeset [829] by
- …
- 1:32 PM Changeset [828] by
- Proof statement.
- 1:26 PM Changeset [827] by
- The preamble is now part of the PseudoStatus?.
May 23, 2011:
- 6:39 PM Changeset [826] by
- start of proof
- 6:12 PM Changeset [825] by
- lots of refactoring, finally got something to prove
- 5:39 PM Changeset [824] by
- Some work on showing that casts around integer operations can be removed.
- 4:24 PM Changeset [823] by
- added new file for proof of correctness of pseudo-assembly translation
- 4:22 PM Changeset [822] by
- removed all axioms
- 3:23 PM Changeset [821] by
- changes to introduce pseudostatus
May 20, 2011:
- 6:09 PM Changeset [820] by
- changes to get the semantics of pseudoassembly working
May 19, 2011:
- 4:45 PM Changeset [819] by
- Final changes. Under 8 pages.
- 4:03 PM Changeset [818] by
- 32 and 16 bits operations support in D2.2/8051
- 3:16 PM Changeset [817] by
- final changes, now to get under 8 pages
- 3:06 PM Changeset [816] by
- Clight to Cminor compilation, modulo switch statements, temporary …
- 12:24 PM Changeset [815] by
- some changes
May 18, 2011:
- 3:33 PM Changeset [814] by
- changes with claudio
May 16, 2011:
- 6:07 PM Changeset [813] by
- added boxing of matita code to distinguish from o'caml
- 5:43 PM Changeset [812] by
- small change
- 5:35 PM Changeset [811] by
- small typo fixed
- 5:12 PM Changeset [810] by
- More added.
- 4:32 PM Changeset [809] by
- more changes to get everything to fit correctly. gone past 8 pg limit
- 10:44 AM Changeset [808] by
- Changes to paper to get it ready for FMCAD
May 13, 2011:
- 6:31 PM Changeset [807] by
- small change
- 6:29 PM Changeset [806] by
- more changes to language used
- 6:21 PM Changeset [805] by
- …
- 6:18 PM Changeset [804] by
- …
- 6:07 PM Changeset [803] by
- more changes
- 5:55 PM Changeset [802] by
- …
- 5:50 PM Changeset [801] by
- Changes to english in letter.
- 5:36 PM Changeset [800] by
- Half finished.
- 5:35 PM Changeset [799] by
- more changes.
- 1:10 PM Changeset [798] by
- Fix usual matita tactic mistake.
- 1:10 PM Changeset [797] by
- Add error messages wherever the error monad is used. Sticks to …
- 1:10 PM Changeset [796] by
- Put correct type on cost label expressions in the prototype.
- 12:29 PM Changeset [795] by
- Changes from this morning.
May 12, 2011:
- 7:19 PM Changeset [794] by
- Some content for addendum
- 5:33 PM Changeset [793] by
- Work from today on rtlabs -> rtl pass.
May 11, 2011:
- 5:06 PM Changeset [792] by
- Deliverable D2.1 with addendum
- 2:01 PM Changeset [791] by
- Empty addendum
- 11:44 AM PublicationVenues edited by
- (diff)
May 10, 2011:
- 5:50 PM Changeset [790] by
- A little tidying: get rid of requirement for jmeq in Mem.ma, remove …
- 5:36 PM Changeset [789] by
- More work on rtlabs -> rtl pass.
Note: See TracTimeline
for information about the timeline view.
