Timeline
Jul 8, 2011:
- 5:49 PM Changeset [1061] by
- more work, bug found, ridiculous map3 function with dep. types added
- 12:17 PM Changeset [1060] by
- work from this morning and yesterday
Jul 6, 2011:
- 6:09 PM Changeset [1059] by
- work from today, bit of a mess at the moment
- 1:29 PM Changeset [1058] by
- Evict CompCert? Maps interface in favour of BitVectorTries?.
Jul 5, 2011:
- 5:53 PM Changeset [1057] by
- changes from today
- 4:25 PM Changeset [1056] by
- Switch to delayed identifier error scheme.
- 12:15 PM Changeset [1055] by
- changes to how identifiers are generated
- 9:51 AM Changeset [1054] by
- - proven policy safe
Jul 4, 2011:
- 6:20 PM Changeset [1053] by
- changes
- 3:31 PM Changeset [1052] by
- removed offsets after reading cerco mailing list
- 1:49 PM Changeset [1051] by
- removed superfluous addressing mode code from RTLabs/syntax.ma
- 10:43 AM Changeset [1050] by
- adding dependent types to map datastructure to remove all option …
Jul 1, 2011:
- 5:45 PM Changeset [1049] by
- more stuff added
- 5:11 PM Changeset [1048] by
- added implementation of haskell associative maps to clean up the mess …
Jun 29, 2011:
- 5:38 PM Changeset [1047] by
- more work from today
- 12:15 PM Changeset [1046] by
- syntax of rtlabs was wrong: cast not const. more added to rtlabs --> …
- 10:47 AM Changeset [1045] by
- resolved conflict in rtlabs
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)
Note: See TracTimeline
for information about the timeline view.
