Timeline
Dec 14, 2010:
- 4:55 PM Changeset [425] by
- Removed Map.ma as no longer needed. Everything else seems to build …
- 4:51 PM Changeset [424] by
- Tidied up English in last addition.
- 4:49 PM Changeset [423] by
- Discussed partiality in the case of assembly: use of Maybe monad.
- 4:38 PM Changeset [422] by
- Tweaks to the report.
- 4:13 PM Changeset [421] by
- Removed duplicate "assembly1" function. Removed Ocaml code from file.
- 4:12 PM Changeset [420] by
- All proof obligations closed.
- 2:13 PM Changeset [419] by
- Type errors fixed, need to close additional proof obligations.
- 12:08 PM Changeset [418] by
- Fixed type error in Mov instruction implementation.
Dec 13, 2010:
- 6:48 PM Changeset [417] by
- Minor typo.
- 6:38 PM Changeset [416] by
- Fix printing of switch statements as matita terms.
- 6:35 PM Changeset [415] by
- A couple of amusing examples.
- 6:03 PM Changeset [414] by
- Got a few more cases working.
- 5:52 PM Changeset [413] by
- Add example of executing C semantics.
- 5:52 PM Changeset [412] by
- Add example of animation.
- 5:11 PM Changeset [411] by
- Note associativity of IOMonad, subject to extensionality.
- 5:00 PM Changeset [410] by
- Using bitvectortries for a dictionary doesn't work even if we …
- 3:58 PM Changeset [409] by
- Update a couple of examples; put support for animation in its own file.
- 1:04 PM Changeset [408] by
- Add missing diagram.
- 12:43 PM Changeset [407] by
- Mention version of compcert used.
- 12:12 PM Changeset [406] by
- Move description of 8051 memory model out of C semantics.
- 11:47 AM Changeset [405] by
- Move C semantics to the appropriate deliverable directory.
- 11:43 AM Changeset [404] by
- Update C-semantics README.
- 11:13 AM Changeset [403] by
- Removed stray ncheck so that files will now compile.
- 12:02 AM Changeset [402] by
- Revise D3.1, add notes on files.
Dec 11, 2010:
- 4:16 PM Changeset [401] by
- Keep a depends file in the repository for the C-semantics.
- 4:16 PM Changeset [400] by
- Minor changes for the new version of matita.
Dec 10, 2010:
- 5:05 PM Changeset [399] by
- Rearrange executable semantics a little.
Dec 9, 2010:
- 8:35 PM Changeset [398] by
- This time actually prove the result I intended.
- 4:48 PM Changeset [397] by
- Changed layout of document title.
- 4:47 PM Changeset [396] by
- More changes.
- 3:33 PM Changeset [395] by
- Lots added from this afternoon to report. Implemented nearly all …
- 11:55 AM Changeset [394] by
- Commit of what I did this morning.
Dec 8, 2010:
- 6:08 PM Changeset [393] by
- A few more details in D3.1.
- 4:56 PM Changeset [392] by
- Work around cofixpoint unfolding problem. We only use axioms in …
- 4:56 PM Changeset [391] by
- Comment out daemon and its uses - we don't need the properties of the …
- 3:14 PM Changeset [390] by
- Implemented some of the changes suggested by CSC.
- 12:18 PM Changeset [389] by
- Sort out minor inconsistency between semantics.
- 11:40 AM Changeset [388] by
- Tidy up some decidability functions.
Dec 7, 2010:
- 7:06 PM Changeset [387] by
- Sort out equality checking of types.
- 5:23 PM Changeset [386] by
- Whole program equivalence result for the Clight executable and …
- 5:22 PM Changeset [385] by
- Almost finished whole program equivalence.
- 4:22 PM Changeset [384] by
- Fixed problem in Abstract.
- 4:12 PM Changeset [383] by
- First draft of report finished.
- 11:23 AM Changeset [382] by
- Changes from this morning.
Dec 6, 2010:
- 5:17 PM Changeset [381] by
- Some d3.1 work.
- 5:14 PM Changeset [380] by
- More added on subtyping stuff, etc.
- 4:03 PM Changeset [379] by
- More whole execution equivalence - need ability to unfold cofixpoints …
- 11:49 AM Changeset [378] by
- More work on equivalence of whole executions.
- 11:44 AM Changeset [377] by
- Description of techniques related to validation of O'Caml emulator.
- 10:19 AM Changeset [376] by
- Work on describing sparse bitvector tries.
- 10:03 AM Changeset [375] by
- More work on report.
Dec 5, 2010:
- 11:54 PM Changeset [374] by
- 1) notation for cast fixed 2) ambiguity reduced: Empty => VEmpty, Cons …
- 9:55 PM Changeset [373] by
- Order of declaration of notations changed to put more precise …
Dec 3, 2010:
- 11:52 PM Changeset [372] by
- No more axioms! All proofs completed. (Interrupts, I/O and timers not …
- 4:47 PM Changeset [371] by
- Report started. Background/introduction finished (first draft). …
- 4:47 PM Changeset [370] by
- Most of critical lemma done. Hole remaining that I can't coax matita …
- 10:33 AM Changeset [369] by
- Proof of missing lemma seems to be done, but won't Qed. My version of …
Dec 2, 2010:
- 6:27 PM Changeset [368] by
- All 450 proof obligations closed.
- 5:13 PM Changeset [367] by
- Added decidable equality for addressing_mode_tags.
- 4:41 PM Changeset [366] by
- Make I/O type safe, removing a discrepancy between the executable and …
- 4:40 PM Changeset [365] by
- Soundness (really completeness) of Wrong executions.
- 4:36 PM Changeset [364] by
- Added subvector_with function.
- 2:03 PM Changeset [363] by
- Resolved conflicts. Added new get_index' which hides the proof …
- 11:53 AM Changeset [362] by
- Less ambiguous definitions.
- 10:52 AM Changeset [361] by
- …
- 10:43 AM Changeset [360] by
- Missing include added.
- 10:25 AM Changeset [359] by
- add_n_with_carry and sub_n_with_carry now both return bitvectors of …
- 10:15 AM Changeset [358] by
- Added \bot to all absd cases in execute_1 to get rid of as many open …
Dec 1, 2010:
- 11:27 PM Changeset [357] by
- - stupid bug fixed in BitVectorTrie? - dependencies minimized, dead …
- 10:29 PM Changeset [356] by
- Bug fixed: fold_left_i was actually a sort of fold_right_i :-)
- 10:19 PM Changeset [355] by
- …
- 6:49 PM Changeset [354] by
- Everything compiles. Doesn't jump correctly still.
- 6:40 PM Changeset [353] by
- - pc was initialized to 7 in place of sp - bitvector_of_nat was …
- 6:03 PM Changeset [352] by
- Do not use ndestruct for injectivity since it introduces StreickerK …
- 4:30 PM Changeset [351] by
- No more axioms but the paralogisms.
- 1:10 PM Changeset [350] by
- less axioms
- 11:18 AM Changeset [349] by
- Added fold_right_i (with dependent type) to List file.
- 10:31 AM Changeset [348] by
- Added skeleton files for report.
Nov 30, 2010:
- 6:13 PM Changeset [347] by
- Work on main execution loop. All cases covered. Need to close open …
- 5:07 PM Changeset [346] by
- An example of execution.
- 5:07 PM Changeset [345] by
- load implemented
- 5:01 PM Changeset [344] by
- Removed stray ncheck in Status.ma.
- 4:56 PM Changeset [343] by
- Fixed Status.ma so that it compiles.
- 4:46 PM Changeset [342] by
- fold_lefti
- 3:06 PM Changeset [341] by
- A simple version of assembly (no labels) implemented.
- 2:36 PM Changeset [340] by
- ::: is now used in place of :: for vectors to reduce ambiguity
- 2:35 PM Changeset [339] by
- New: pretty printer from HEX files to .ma files.
- 2:35 PM Changeset [338] by
- Most jumps finished. Only CJNE to do.
- 12:26 PM Changeset [337] by
- Changes to execute_1 file. Changes to get everything type checking.
- 12:21 PM Changeset [336] by
- check removed.
Nov 29, 2010:
- 6:42 PM Changeset [335] by
- Quick pass through 3.1 text.
- 5:34 PM Changeset [334] by
- More added.
- 4:12 PM Changeset [333] by
- Work on execute_1 function.
- 3:53 PM Changeset [332] by
- Code of fetch greatly simplified because of better behaviour of Matita.
- 2:32 PM Changeset [331] by
- More changes to get everything to typecheck.
- 2:08 PM Changeset [330] by
- Fixed segmentation fault in Nat.ma, added get_index and renamed …
- 1:42 PM Changeset [329] by
- Commit to restore deleted file.
- 11:17 AM Changeset [328] by
- Got fold_right_i to type check. Moved eq_rect_Type0 into …
- 1:26 AM Changeset [327] by
- Completed!
- 1:08 AM Changeset [326] by
- Almost compiling.
Nov 26, 2010:
- 10:36 PM Changeset [325] by
- Almost finished.
- 10:29 PM Changeset [324] by
- It starts working…
- 10:14 PM Changeset [323] by
- …
- 9:35 PM Changeset [322] by
- More work on fetch.
- 7:00 PM Changeset [321] by
- Soundness for reactive executions.
- 6:13 PM Changeset [320] by
- Added fold_right_i, equivalent of O'Caml's fold_right2.
- 6:12 PM Changeset [319] by
- …
- 5:54 PM Changeset [318] by
- First version: to be debugged.
- 5:45 PM Changeset [317] by
- Fixed problems with arguments of register change.
- 5:38 PM Changeset [316] by
- REGISTER now takes a BitVector? 3
- 5:32 PM Changeset [315] by
- Decidable equality on vectors and its specialisation to bitvectors.
- 4:53 PM Changeset [314] by
- Finished all get_ and set_arg_* functions.
- 3:33 PM Changeset [313] by
- Added axioms for addition for claudio.
- 3:24 PM Changeset [312] by
- arguments of split reversed
- 1:28 PM Changeset [311] by
- get_arg_16 complete.
- 11:26 AM Changeset [310] by
- Most of get_arg_16 done.
- 1:12 AM Changeset [309] by
- assembly1 is finally compiling in about 37s!
- 12:49 AM Changeset [308] by
- More explicit typing solves one of the points.
- 12:25 AM Changeset [307] by
- assembly1 completed, but two cases commented out since they require …
- 12:19 AM Changeset [306] by
- …
- 12:10 AM Changeset [305] by
- …
- 12:06 AM Changeset [304] by
- …
Nov 25, 2010:
- 11:41 PM Changeset [303] by
- …
- 11:30 PM Changeset [302] by
- …
- 11:19 PM Changeset [301] by
- …
- 11:12 PM Changeset [300] by
- …
- 10:55 PM Changeset [299] by
- …
- 10:44 PM Changeset [298] by
- …
- 10:36 PM Changeset [297] by
- …
- 10:17 PM Changeset [296] by
- …
- 6:15 PM Changeset [295] by
- Soundness of terminating whole program execution.
- 3:51 PM Changeset [294] by
- get and set_arg_16 implemented.
- 3:09 PM Changeset [293] by
- …
- 2:54 PM Changeset [292] by
- Update acc 8051 syntax extension patch. Adds memory spaces to Clight …
- 12:54 PM Changeset [291] by
- Soundness of behaviour of exec_inf_aux on finite number of steps.
- 12:48 PM Changeset [290] by
- Moved definitions around so related are grouped together.
- 12:47 PM Changeset [289] by
- Writing at stack pointer implemented.
- 12:28 PM Changeset [288] by
- Set flags implemented.
- 11:49 AM Changeset [287] by
- Reading at stack pointer added.
- 11:18 AM Changeset [286] by
- Added bit address lookup for registers.
- 10:53 AM Changeset [285] by
- Get and set for bitaddressable SFRs now completed.
Nov 24, 2010:
- 11:15 PM Changeset [284] by
- …
- 11:01 PM Changeset [283] by
- Bug fixed in type declaration of BIT/N_BIT.
- 7:11 PM Changeset [282] by
- …
- 6:29 PM Changeset [281] by
- Resolved conflicts.
- 5:26 PM Changeset [280] by
- Bug fixed in assemblying AJMP.
- 5:19 PM Changeset [279] by
- Notation moved to Cartesian.
- 5:18 PM Changeset [278] by
- More curryfication.
- 5:06 PM Changeset [277] by
- Bugs fixed in definition of sub8_with_carrier.
- 4:16 PM Changeset [276] by
- Messed up a file.
- 3:40 PM Changeset [275] by
- Removed all axioms from Arithmetic.ma and replaced them with …
- 3:28 PM Changeset [274] by
- First attempt at sub8_with_c complete.
- 2:28 PM Changeset [273] by
- Some fault functions were rewritten.
- 1:43 PM Changeset [272] by
- Changes from this morning.
- 1:00 AM Changeset [271] by
- assembly1 defined on ACALL and ADD: it seems it will become too slow…
Nov 23, 2010:
- 6:12 PM Changeset [270] by
- More added.
- 6:11 PM Changeset [269] by
- - …
- 5:44 PM Changeset [268] by
- - notation moved to proper places - new function split on Vectors
- 5:42 PM Changeset [267] by
- Renamed Interpret to Status.
- 5:10 PM Changeset [266] by
- Changes to bitvector.
- 5:05 PM Changeset [265] by
- Test commit.
- 5:05 PM Changeset [264] by
- - new axiomatic data type for Strings - new file for Assembly
- 4:43 PM Changeset [263] by
- - use standard notation for exponential - Bit is now Bool
- 4:39 PM Changeset [262] by
- - new notation ...? for vectors to reduce ambiguity - …
- 3:50 PM Changeset [261] by
- Strengthened typings of get_ and set_index in Vector file.
- 2:30 PM Changeset [260] by
- - Minimal changes to make it compile with the standard distribution of …
- 12:56 PM Changeset [259] by
- Need stronger set_ and get_index functions on vectors (current ones …
- 11:43 AM Changeset [258] by
- Forgotten files.
- 11:43 AM Changeset [257] by
- Added exponential functions for nats. Working on operational …
Nov 22, 2010:
- 7:25 PM Changeset [256] by
- Work on ASM.ma file.
- 3:57 PM Changeset [255] by
- Really restore matita root.
- 2:40 PM Changeset [254] by
- Reset matita root.
- 2:40 PM Changeset [253] by
- Update completeness proof for executable semantics with separate …
- 2:40 PM Changeset [252] by
- Separate out soundness of exec_step from definition.
- 2:40 PM Changeset [251] by
- Separate out soundness of exec_expr from definition.
- 2:40 PM Changeset [250] by
- Begin separating soundness from executable semantics.
- 1:55 PM Changeset [249] by
- More work on defining fundamental datatypes.
- 11:43 AM Changeset [248] by
- More changes. Added datatype for addressing modes.
- 11:12 AM Changeset [247] by
- Changes to get directory to compile.
- 10:05 AM Changeset [246] by
- Added physical file (Arithmetic) for arithmetic on bit vectors, and …
Nov 16, 2010:
- 1:42 PM Changeset [245] by
- Some progress on whole-execution soundness.
Nov 15, 2010:
- 10:42 AM Changeset [244] by
- Vector.ma now compiles.
- 10:41 AM Changeset [243] by
- Updated Util.ma too.
- 10:28 AM Changeset [242] by
- Got List to compile.
- 10:26 AM Changeset [241] by
- Also needed an updated List.ma.
- 10:22 AM Changeset [240] by
- Updated Vector / BitVector? files taken from my Matita library.
Note: See TracTimeline
for information about the timeline view.
