Timeline



Dec 16, 2011:

6:35 PM Changeset [1625] by mulligan
before christmas
3:44 PM Changeset [1624] by mulligan
commit for claudio
2:07 PM Changeset [1623] by mulligan
strange matita issue
10:09 AM Changeset [1622] by mulligan
to avoid conflicts, bug in typechecker?

Dec 15, 2011:

10:22 AM Changeset [1621] by mulligan
to prevent conflicts
12:23 AM Changeset [1620] by sacerdot
One of the mutual cases of the open proof is practically finished.
12:02 AM Changeset [1619] by sacerdot
Major advancement.

Dec 14, 2011:

6:17 PM Changeset [1618] by campbell
Minor updates due to recent changes.
6:17 PM Changeset [1617] by campbell
Note stuff to do on structured traces.
5:57 PM Changeset [1616] by sacerdot
Partially ported to new Matita syntax. Because of some changes in …
5:28 PM Changeset [1615] by sacerdot
Policy now depends on Assembly and not the other way around.
5:00 PM Changeset [1614] by boender
- split policy from assembly
4:41 PM Changeset [1613] by sacerdot
Coercion moved to Matita standard lib.
3:58 PM Changeset [1612] by sacerdot
All library ported to new Matita lib (finally).
3:35 PM Changeset [1611] by sacerdot
All of Cminor now compiles with the latest lib of Matita.
3:33 PM Changeset [1610] by sacerdot
Ported to new lib.
2:44 PM Changeset [1609] by boender
- added alias to ASM/BitVectorTrie - removed double include from …
2:30 PM Changeset [1608] by sacerdot
Porting to new library still in progress.
1:50 PM Changeset [1607] by sacerdot
Porting to new library.
1:40 PM Changeset [1606] by sacerdot
Porting to last library of Matita.
1:18 PM Changeset [1605] by sacerdot
Porting to last standard library of Matita.
11:52 AM Changeset [1604] by mulligan
for jaap

Dec 13, 2011:

5:37 PM Changeset [1603] by sacerdot
More proofs ported to new lib.
4:23 PM Changeset [1602] by mulligan
giving up on fetch proofs for time being
2:49 PM Changeset [1601] by sacerdot
Files ported to new version of the standard library.
1:41 PM Changeset [1600] by sacerdot
utilities and ASM ported to the new standard library
1:34 AM Changeset [1599] by sacerdot
Start of merging of stuff into the standard library of Matita.

Dec 12, 2011:

5:53 PM Changeset [1598] by mulligan
changes over the last couple of days
9:51 AM Changeset [1597] by mulligan
fixed fetch for jaap

Dec 7, 2011:

4:24 PM Changeset [1596] by campbell
RTLabs structured traces: sort out passing of termination proofs around.
4:24 PM Changeset [1595] by campbell
We don't need an explicit termination count when building traces.
4:24 PM Changeset [1594] by campbell
Rework handling of termination information in RTLabs structured traces …
3:48 PM Changeset [1593] by boender
- cleaned up Assembly, moved some definitions elsewhere
2:50 PM Changeset [1592] by boender
- updated definitions to work with programs of maximum 216 instructions

Dec 6, 2011:

5:24 PM Changeset [1591] by mulligan
work from today
5:13 PM Changeset [1590] by tranquil
* got back to previous implementation of multiplication in RTLabs -> …
5:04 PM Changeset [1589] by tranquil
* turned to argument-less return statements for RTLabs and RTL (there …
11:21 AM Changeset [1588] by sacerdot
All goals generated by Russell for execute_1* are now closed, mostly …

Dec 5, 2011:

5:16 PM Changeset [1587] by mulligan
changes from today, including removing indexing of problematic …
1:11 PM Changeset [1586] by campbell
RTLabs structured traces: cost labels after jumps.

Dec 2, 2011:

7:49 PM Changeset [1585] by tranquil
fighting with a bug of the translation from RTL to ERTL
3:13 PM Changeset [1584] by tranquil
* new form of translation written in graphUtilites (mainly as a test …
1:02 PM Changeset [1583] by campbell
More on RTLabs structured traces. Fixed mistake in structure trace …

Dec 1, 2011:

5:24 PM Changeset [1582] by mulligan
more added to the proof of execute_1_preinstruction --- ~260 cases now …
3:15 PM Changeset [1581] by mulligan
Dangling de Bruijn pointer when trying to propagate russell to set_arg_1
2:50 PM Changeset [1580] by tranquil
implemented constant propagation in LTL cleaned up translations in …
2:11 PM Changeset [1579] by mulligan
Finished proof with simpler statement, making everything a lot nicer
1:12 PM Changeset [1578] by boender
- proof of termination of policy completed (needs some clean-up work …

Nov 30, 2011:

5:32 PM Changeset [1577] by mulligan
A lot more cases added to the proof at the bottom of …

Nov 29, 2011:

5:22 PM Changeset [1576] by mulligan
big changes to proofs, just two small cases remain and a few …
2:21 PM Changeset [1575] by mulligan
Changes to specifications on execute functions

Nov 28, 2011:

5:57 PM Changeset [1574] by campbell
A little more progress on traces on RTLabs.
5:13 PM Changeset [1573] by mulligan
more complicated than it appears :(
3:13 PM Changeset [1572] by tranquil
* corrected previous bug * finished propagating immediates
1:39 PM Changeset [1571] by mulligan
small changes

Nov 25, 2011:

8:48 PM Changeset [1570] by sacerdot
Dependent type crazyness.
7:46 PM Changeset [1569] by tranquil
* added in repository some missing files…
7:43 PM Changeset [1568] by tranquil
* Immediates introduced (but not fully used yet in RTLabs to RTL pass) …
6:17 PM Changeset [1567] by mulligan
more work on big proof, 2.5 cases left
6:12 PM Changeset [1566] by campbell
Pacify changes to destruct tactic.
5:30 PM Changeset [1565] by campbell
Note that RTLabs ought to classify branches as "jumps" (in the …
3:31 PM Changeset [1564] by sacerdot
Commit where we use a dependently typed version of bigops. I am now …
1:49 PM Changeset [1563] by campbell
A little progress on constructing RTLabs structured traces.
1:20 PM Changeset [1562] by mulligan
new version of assembly, fixed conflict in positivemap.ma, changed …
1:13 PM Changeset [1561] by sacerdot
More dependent types to accomodate the statement.

Nov 24, 2011:

7:22 PM Changeset [1560] by sacerdot
Complete re-implementation that: 1) assumes no code before the first …
6:49 PM Changeset [1559] by campbell
Add a notion of flat traces with evidence for RTLabs.
6:47 PM Changeset [1558] by sacerdot
Snapshot before moving things to ASMCosts.ma.
6:09 PM Changeset [1557] by sacerdot
Byte => costlabel
5:24 PM Changeset [1556] by mulligan
submitting to avoid conflicts
5:19 PM Changeset [1555] by boender
- changes to assembly - added lookup to PositiveMap? - lightly changed …
4:49 PM Changeset [1554] by sacerdot
Major progress in the proof.
12:26 PM Changeset [1553] by boender
- added lookup_opt_lookup lemma
12:12 PM Changeset [1552] by campbell
Update RTLabs structured trace definition.
11:52 AM Changeset [1551] by campbell
Functions to translate between back-end and front-end values.
11:44 AM Changeset [1550] by sacerdot
Repaired after use of Russell for execute_1.
11:11 AM Changeset [1549] by mulligan
removed cruft from costsproof.ma file so claudio can work in parallel

Nov 23, 2011:

11:15 PM Changeset [1548] by sacerdot
11:08 PM Changeset [1547] by sacerdot
Invariant on cost of one execution step strengthened.
6:39 PM Changeset [1546] by tranquil
added an option to prevent reindexing transformations from taking …
6:03 PM Changeset [1545] by campbell
Use pointer record in front-end.
6:01 PM Changeset [1544] by sacerdot
StructuredTraces? inhabited for object code.
5:46 PM Changeset [1543] by tranquil
deletion of indexed labels branch
5:43 PM Changeset [1542] by tranquil
merge of indexed labels branch
4:31 PM Changeset [1541] by mulligan
interpret.ma now compiles
4:03 PM Changeset [1540] by mulligan
changes to proof in interrupt.ma
1:55 PM Changeset [1539] by tranquil
branch up to date
12:28 PM Changeset [1538] by mulligan
changes to execute_1_0 proof
12:27 PM Changeset [1537] by campbell
A preliminary definition of the abstract status record for RTLabs.
12:07 PM Changeset [1536] by campbell
Use predicates throughout the structured traces.
12:07 PM Changeset [1535] by campbell
Make RTLabs semantics use knowledge that the next instruction always …
10:36 AM Changeset [1534] by mulligan
committing my changes to interpret to prevent any further conflicts

Nov 22, 2011:

7:24 PM Changeset [1533] by sacerdot
Proof of execute_1 with Russell completed (up to some daemon used before).
4:18 PM Changeset [1532] by campbell
Remove jump classification from structured traces.
4:18 PM Changeset [1531] by campbell
A notion of abstract structured traces.
12:37 PM Changeset [1530] by campbell
Update due to Russell changes.
12:28 PM Changeset [1529] by campbell
Update RTLabs to RTL with unary operation types.
11:58 AM Changeset [1528] by campbell
Update most of Assembly.ma with new syntax and identifier maps. Change …
11:50 AM Changeset [1527] by sacerdot
More on Russell.
10:43 AM Changeset [1526] by sacerdot
Using Russell to prove some properties.

Nov 21, 2011:

6:17 PM Changeset [1525] by ayache
D2.2: function pointers using JMP.
5:51 PM Changeset [1524] by boender
- adapted files to new Matita syntax
4:29 PM Changeset [1523] by campbell
Separate out positive and Z definitions from extralib.ma. Minor syntax …
3:49 PM Changeset [1522] by mulligan
changes to preamble and lin to asm pass, resolved conflict in interpret
1:06 PM Changeset [1521] by sacerdot
Syntax change in Matita: change what where => change where what.
12:23 PM Changeset [1520] by campbell
Generate cost labels with correct type.
12:10 PM Changeset [1519] by campbell
More syntax updates.
11:15 AM Changeset [1518] by campbell
Update to new syntax.

Nov 19, 2011:

12:38 AM Changeset [1517] by sacerdot
Ported to syntax of Matita 0.99.1.
12:38 AM Changeset [1516] by sacerdot
Ported to syntax of Matita 0.99.1.

Nov 18, 2011:

1:03 PM Changeset [1515] by campbell
Add type of maps on positive binary numbers, and use them for …
Note: See TracTimeline for information about the timeline view.