Timeline



Dec 15, 2010:

11:35 PM Changeset [437] by sacerdot
1. new function assembly_unlabelled_program 2. the new function is now …
11:20 PM Changeset [436] by sacerdot
11:19 PM Changeset [435] by sacerdot
logic/pts.ma is now used in place of Universes.ma
7:50 PM Changeset [434] by mulligan
Types added.
7:42 PM Changeset [433] by mulligan
Most things added, just need to fill in types in table.
7:21 PM Changeset [432] by mulligan
Removed Plogic/
6:38 PM Changeset [431] by mulligan
- README updated - Test and DoTest? fixed to work on assembly_program - …
5:42 PM Changeset [430] by mulligan
- ToMatita? now generates a list of labelled_instructions (used to be a …
5:16 PM Changeset [429] by mulligan
1) README upated 2) executable now reads the name of the HEX file from argv
5:04 PM Changeset [428] by mulligan
Changed instr. to labelled_instr.
5:01 PM Changeset [427] by mulligan
Removed interpret.ma from ToMatita?
5:00 PM Changeset [426] by mulligan
Changes to ocaml code and makefile.

Dec 14, 2010:

4:55 PM Changeset [425] by mulligan
Removed Map.ma as no longer needed. Everything else seems to build …
4:51 PM Changeset [424] by mulligan
Tidied up English in last addition.
4:49 PM Changeset [423] by mulligan
Discussed partiality in the case of assembly: use of Maybe monad.
4:38 PM Changeset [422] by mulligan
Tweaks to the report.
4:13 PM Changeset [421] by mulligan
Removed duplicate "assembly1" function. Removed Ocaml code from file.
4:12 PM Changeset [420] by mulligan
All proof obligations closed.
2:13 PM Changeset [419] by mulligan
Type errors fixed, need to close additional proof obligations.
12:08 PM Changeset [418] by mulligan
Fixed type error in Mov instruction implementation.

Dec 13, 2010:

6:48 PM Changeset [417] by campbell
Minor typo.
6:38 PM Changeset [416] by campbell
Fix printing of switch statements as matita terms.
6:35 PM Changeset [415] by campbell
A couple of amusing examples.
6:03 PM Changeset [414] by mulligan
Got a few more cases working.
5:52 PM Changeset [413] by campbell
Add example of executing C semantics.
5:52 PM Changeset [412] by campbell
Add example of animation.
5:11 PM Changeset [411] by campbell
Note associativity of IOMonad, subject to extensionality.
5:00 PM Changeset [410] by mulligan
Using bitvectortries for a dictionary doesn't work even if we …
3:58 PM Changeset [409] by campbell
Update a couple of examples; put support for animation in its own file.
1:04 PM Changeset [408] by campbell
Add missing diagram.
12:43 PM Changeset [407] by campbell
Mention version of compcert used.
12:12 PM Changeset [406] by campbell
Move description of 8051 memory model out of C semantics.
11:47 AM Changeset [405] by campbell
Move C semantics to the appropriate deliverable directory.
11:43 AM Changeset [404] by campbell
Update C-semantics README.
11:13 AM Changeset [403] by mulligan
Removed stray ncheck so that files will now compile.
12:02 AM Changeset [402] by campbell
Revise D3.1, add notes on files.

Dec 11, 2010:

4:16 PM Changeset [401] by campbell
Keep a depends file in the repository for the C-semantics.
4:16 PM Changeset [400] by campbell
Minor changes for the new version of matita.

Dec 10, 2010:

5:05 PM Changeset [399] by campbell
Rearrange executable semantics a little.

Dec 9, 2010:

8:35 PM Changeset [398] by campbell
This time actually prove the result I intended.
4:48 PM Changeset [397] by mulligan
Changed layout of document title.
4:47 PM Changeset [396] by mulligan
More changes.
3:33 PM Changeset [395] by mulligan
Lots added from this afternoon to report. Implemented nearly all …
11:55 AM Changeset [394] by mulligan
Commit of what I did this morning.

Dec 8, 2010:

6:08 PM Changeset [393] by campbell
A few more details in D3.1.
4:56 PM Changeset [392] by campbell
Work around cofixpoint unfolding problem. We only use axioms in …
4:56 PM Changeset [391] by campbell
Comment out daemon and its uses - we don't need the properties of the …
3:14 PM Changeset [390] by mulligan
Implemented some of the changes suggested by CSC.
12:18 PM Changeset [389] by campbell
Sort out minor inconsistency between semantics.
11:40 AM Changeset [388] by campbell
Tidy up some decidability functions.

Dec 7, 2010:

7:06 PM Changeset [387] by campbell
Sort out equality checking of types.
5:23 PM Changeset [386] by campbell
Whole program equivalence result for the Clight executable and …
5:22 PM Changeset [385] by campbell
Almost finished whole program equivalence.
4:22 PM Changeset [384] by mulligan
Fixed problem in Abstract.
4:12 PM Changeset [383] by mulligan
First draft of report finished.
11:23 AM Changeset [382] by mulligan
Changes from this morning.

Dec 6, 2010:

5:17 PM Changeset [381] by campbell
Some d3.1 work.
5:14 PM Changeset [380] by mulligan
More added on subtyping stuff, etc.
4:03 PM Changeset [379] by campbell
More whole execution equivalence - need ability to unfold cofixpoints …
11:49 AM Changeset [378] by campbell
More work on equivalence of whole executions.
11:44 AM Changeset [377] by mulligan
Description of techniques related to validation of O'Caml emulator.
10:19 AM Changeset [376] by mulligan
Work on describing sparse bitvector tries.
10:03 AM Changeset [375] by mulligan
More work on report.

Dec 5, 2010:

11:54 PM Changeset [374] by sacerdot
1) notation for cast fixed 2) ambiguity reduced: Empty => VEmpty, Cons …
9:55 PM Changeset [373] by sacerdot
Order of declaration of notations changed to put more precise …

Dec 3, 2010:

11:52 PM Changeset [372] by sacerdot
No more axioms! All proofs completed. (Interrupts, I/O and timers not …
4:47 PM Changeset [371] by mulligan
Report started. Background/introduction finished (first draft). …
4:47 PM Changeset [370] by mulligan
Most of critical lemma done. Hole remaining that I can't coax matita …
10:33 AM Changeset [369] by mulligan
Proof of missing lemma seems to be done, but won't Qed. My version of …

Dec 2, 2010:

6:27 PM Changeset [368] by mulligan
All 450 proof obligations closed.
5:13 PM Changeset [367] by mulligan
Added decidable equality for addressing_mode_tags.
4:41 PM Changeset [366] by campbell
Make I/O type safe, removing a discrepancy between the executable and …
4:40 PM Changeset [365] by campbell
Soundness (really completeness) of Wrong executions.
4:36 PM Changeset [364] by mulligan
Added subvector_with function.
2:03 PM Changeset [363] by mulligan
Resolved conflicts. Added new get_index' which hides the proof …
11:53 AM Changeset [362] by sacerdot
Less ambiguous definitions.
10:52 AM Changeset [361] by sacerdot
10:43 AM Changeset [360] by sacerdot
Missing include added.
10:25 AM Changeset [359] by mulligan
add_n_with_carry and sub_n_with_carry now both return bitvectors of …
10:15 AM Changeset [358] by mulligan
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 sacerdot
- stupid bug fixed in BitVectorTrie? - dependencies minimized, dead …
10:29 PM Changeset [356] by sacerdot
Bug fixed: fold_left_i was actually a sort of fold_right_i :-)
10:19 PM Changeset [355] by sacerdot
6:49 PM Changeset [354] by mulligan
Everything compiles. Doesn't jump correctly still.
6:40 PM Changeset [353] by mulligan
- pc was initialized to 7 in place of sp - bitvector_of_nat was …
6:03 PM Changeset [352] by mulligan
Do not use ndestruct for injectivity since it introduces StreickerK …
4:30 PM Changeset [351] by mulligan
No more axioms but the paralogisms.
1:10 PM Changeset [350] by mulligan
less axioms
11:18 AM Changeset [349] by mulligan
Added fold_right_i (with dependent type) to List file.
10:31 AM Changeset [348] by mulligan
Added skeleton files for report.

Nov 30, 2010:

6:13 PM Changeset [347] by mulligan
Work on main execution loop. All cases covered. Need to close open …
5:07 PM Changeset [346] by sacerdot
An example of execution.
5:07 PM Changeset [345] by sacerdot
load implemented
5:01 PM Changeset [344] by mulligan
Removed stray ncheck in Status.ma.
4:56 PM Changeset [343] by mulligan
Fixed Status.ma so that it compiles.
4:46 PM Changeset [342] by sacerdot
fold_lefti
3:06 PM Changeset [341] by sacerdot
A simple version of assembly (no labels) implemented.
2:36 PM Changeset [340] by sacerdot
::: is now used in place of :: for vectors to reduce ambiguity
2:35 PM Changeset [339] by sacerdot
New: pretty printer from HEX files to .ma files.
2:35 PM Changeset [338] by mulligan
Most jumps finished. Only CJNE to do.
12:26 PM Changeset [337] by mulligan
Changes to execute_1 file. Changes to get everything type checking.
12:21 PM Changeset [336] by sacerdot
check removed.

Nov 29, 2010:

6:42 PM Changeset [335] by campbell
Quick pass through 3.1 text.
5:34 PM Changeset [334] by mulligan
More added.
4:12 PM Changeset [333] by mulligan
Work on execute_1 function.
3:53 PM Changeset [332] by sacerdot
Code of fetch greatly simplified because of better behaviour of Matita.
2:32 PM Changeset [331] by mulligan
More changes to get everything to typecheck.
2:08 PM Changeset [330] by mulligan
Fixed segmentation fault in Nat.ma, added get_index and renamed …
1:42 PM Changeset [329] by mulligan
Commit to restore deleted file.
11:17 AM Changeset [328] by mulligan
Got fold_right_i to type check. Moved eq_rect_Type0 into …
1:26 AM Changeset [327] by sacerdot
Completed!
1:08 AM Changeset [326] by sacerdot
Almost compiling.

Nov 26, 2010:

10:36 PM Changeset [325] by sacerdot
Almost finished.
10:29 PM Changeset [324] by sacerdot
It starts working…
10:14 PM Changeset [323] by sacerdot
9:35 PM Changeset [322] by sacerdot
More work on fetch.
7:00 PM Changeset [321] by campbell
Soundness for reactive executions.
6:13 PM Changeset [320] by mulligan
Added fold_right_i, equivalent of O'Caml's fold_right2.
6:12 PM Changeset [319] by sacerdot
5:54 PM Changeset [318] by sacerdot
First version: to be debugged.
5:45 PM Changeset [317] by mulligan
Fixed problems with arguments of register change.
5:38 PM Changeset [316] by sacerdot
REGISTER now takes a BitVector? 3
5:32 PM Changeset [315] by mulligan
Decidable equality on vectors and its specialisation to bitvectors.
4:53 PM Changeset [314] by mulligan
Finished all get_ and set_arg_* functions.
3:33 PM Changeset [313] by mulligan
Added axioms for addition for claudio.
3:24 PM Changeset [312] by sacerdot
arguments of split reversed
1:28 PM Changeset [311] by mulligan
get_arg_16 complete.
11:26 AM Changeset [310] by mulligan
Most of get_arg_16 done.
1:12 AM Changeset [309] by sacerdot
assembly1 is finally compiling in about 37s!
12:49 AM Changeset [308] by sacerdot
More explicit typing solves one of the points.
12:25 AM Changeset [307] by sacerdot
assembly1 completed, but two cases commented out since they require …
12:19 AM Changeset [306] by sacerdot
12:10 AM Changeset [305] by sacerdot
12:06 AM Changeset [304] by sacerdot

Nov 25, 2010:

11:41 PM Changeset [303] by sacerdot
11:30 PM Changeset [302] by sacerdot
11:19 PM Changeset [301] by sacerdot
11:12 PM Changeset [300] by sacerdot
10:55 PM Changeset [299] by sacerdot
10:44 PM Changeset [298] by sacerdot
10:36 PM Changeset [297] by sacerdot
10:17 PM Changeset [296] by sacerdot
6:15 PM Changeset [295] by campbell
Soundness of terminating whole program execution.
3:51 PM Changeset [294] by mulligan
get and set_arg_16 implemented.
3:09 PM Changeset [293] by sacerdot
2:54 PM Changeset [292] by campbell
Update acc 8051 syntax extension patch. Adds memory spaces to Clight …
12:54 PM Changeset [291] by campbell
Soundness of behaviour of exec_inf_aux on finite number of steps.
12:48 PM Changeset [290] by mulligan
Moved definitions around so related are grouped together.
12:47 PM Changeset [289] by mulligan
Writing at stack pointer implemented.
12:28 PM Changeset [288] by mulligan
Set flags implemented.
11:49 AM Changeset [287] by mulligan
Reading at stack pointer added.
11:18 AM Changeset [286] by mulligan
Added bit address lookup for registers.
10:53 AM Changeset [285] by mulligan
Get and set for bitaddressable SFRs now completed.

Nov 24, 2010:

11:15 PM Changeset [284] by sacerdot
11:01 PM Changeset [283] by sacerdot
Bug fixed in type declaration of BIT/N_BIT.
7:11 PM Changeset [282] by sacerdot
6:29 PM Changeset [281] by mulligan
Resolved conflicts.
5:26 PM Changeset [280] by sacerdot
Bug fixed in assemblying AJMP.
5:19 PM Changeset [279] by sacerdot
Notation moved to Cartesian.
5:18 PM Changeset [278] by sacerdot
More curryfication.
5:06 PM Changeset [277] by sacerdot
Bugs fixed in definition of sub8_with_carrier.
4:16 PM Changeset [276] by mulligan
Messed up a file.
3:40 PM Changeset [275] by mulligan
Removed all axioms from Arithmetic.ma and replaced them with …
3:28 PM Changeset [274] by mulligan
First attempt at sub8_with_c complete.
2:28 PM Changeset [273] by mulligan
Some fault functions were rewritten.
1:43 PM Changeset [272] by mulligan
Changes from this morning.
1:00 AM Changeset [271] by sacerdot
assembly1 defined on ACALL and ADD: it seems it will become too slow…

Nov 23, 2010:

6:12 PM Changeset [270] by mulligan
More added.
6:11 PM Changeset [269] by sacerdot
- …
5:44 PM Changeset [268] by sacerdot
- notation moved to proper places - new function split on Vectors
5:42 PM Changeset [267] by mulligan
Renamed Interpret to Status.
5:10 PM Changeset [266] by mulligan
Changes to bitvector.
5:05 PM Changeset [265] by mulligan
Test commit.
5:05 PM Changeset [264] by sacerdot
- new axiomatic data type for Strings - new file for Assembly
4:43 PM Changeset [263] by sacerdot
- use standard notation for exponential - Bit is now Bool
4:39 PM Changeset [262] by sacerdot
- new notation ...? for vectors to reduce ambiguity - …
3:50 PM Changeset [261] by mulligan
Strengthened typings of get_ and set_index in Vector file.
2:30 PM Changeset [260] by sacerdot
- Minimal changes to make it compile with the standard distribution of …
12:56 PM Changeset [259] by mulligan
Need stronger set_ and get_index functions on vectors (current ones …
11:43 AM Changeset [258] by mulligan
Forgotten files.
11:43 AM Changeset [257] by mulligan
Added exponential functions for nats. Working on operational …

Nov 22, 2010:

7:25 PM Changeset [256] by mulligan
Work on ASM.ma file.
3:57 PM Changeset [255] by campbell
Really restore matita root.
2:40 PM Changeset [254] by campbell
Reset matita root.
2:40 PM Changeset [253] by campbell
Update completeness proof for executable semantics with separate …
2:40 PM Changeset [252] by campbell
Separate out soundness of exec_step from definition.
2:40 PM Changeset [251] by campbell
Separate out soundness of exec_expr from definition.
2:40 PM Changeset [250] by campbell
Begin separating soundness from executable semantics.
1:55 PM Changeset [249] by mulligan
More work on defining fundamental datatypes.
11:43 AM Changeset [248] by mulligan
More changes. Added datatype for addressing modes.
11:12 AM Changeset [247] by mulligan
Changes to get directory to compile.
10:05 AM Changeset [246] by mulligan
Added physical file (Arithmetic) for arithmetic on bit vectors, and …

Nov 16, 2010:

1:42 PM Changeset [245] by campbell
Some progress on whole-execution soundness.

Nov 15, 2010:

10:42 AM Changeset [244] by mulligan
Vector.ma now compiles.
10:41 AM Changeset [243] by mulligan
Updated Util.ma too.
10:28 AM Changeset [242] by mulligan
Got List to compile.
10:26 AM Changeset [241] by mulligan
Also needed an updated List.ma.
10:22 AM Changeset [240] by mulligan
Updated Vector / BitVector? files taken from my Matita library.
Note: See TracTimeline for information about the timeline view.