Timeline



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 …

Nov 17, 2011:

5:41 PM Changeset [1514] by mulligan
changes from today. matita keeps dieing
4:50 PM Changeset [1513] by campbell
Fix up Clight examples.
4:11 PM Changeset [1512] by campbell
Shorten proof of goal that solves now.

Nov 16, 2011:

5:35 PM Changeset [1511] by mulligan
proofs, added, changes to execute_1_0 function therefore required to …
4:38 PM Changeset [1510] by sacerdot
All files ported to new dependent inversion.

Nov 15, 2011:

5:21 PM Changeset [1509] by mulligan
i hate subtraction over the nats
5:12 PM Changeset [1508] by tranquil
branched a version of the plug-in that is compatible with the indexed …
5:11 PM Changeset [1507] by tranquil
* added an option to not use ternary expressions in costs, to …
10:05 AM Changeset [1506] by mulligan
changes to costs proof over weekend

Nov 14, 2011:

1:22 PM Changeset [1505] by ayache
D2.2: addendum on 16 and 32 bits integer and function pointers support.

Nov 10, 2011:

3:39 PM Changeset [1504] by ayache
8051 ocaml: bug fix in the labelling of do-whiles.

Nov 9, 2011:

11:14 AM Changeset [1503] by mulligan
inductive type complete

Nov 8, 2011:

5:26 PM Changeset [1502] by mulligan
changes to inductive defn
1:41 PM Changeset [1501] by sacerdot
We must take in account the labelled_p predicate.
1:34 PM Changeset [1500] by sacerdot
Proof sketch for one of the two main proofs.

Nov 7, 2011:

5:06 PM Changeset [1499] by mulligan
part way through main statement transcription
4:56 PM Changeset [1498] by mulligan
added new file for proof that costs are preserved at asm level
4:51 PM Changeset [1497] by mulligan
a bit of tidying up, removing dead code, etc.
4:01 PM Changeset [1496] by mulligan
problem fixed with tactics missing a semicolon to stop greedy parsing
3:45 PM Changeset [1495] by mulligan
proper calculation of costs
10:56 AM Changeset [1494] by mulligan
changes to get everything compiling again

Nov 4, 2011:

5:01 PM Changeset [1493] by mulligan
finished well labeled check, up to injectivity of the label map
2:49 PM Changeset [1492] by ayache
Comment in D2.2 -> LINToASM about function pointers.
1:39 PM Changeset [1491] by ayache
Function pointers good and working.
1:25 PM Changeset [1490] by ayache
Function pointers fixed.
12:39 PM Changeset [1489] by campbell
Fix up a couple of lemmas affected by the change to add_with_carries.
12:22 PM Changeset [1488] by ayache
Function pointers in D2.2/8051. Bugged for now.

Nov 3, 2011:

5:24 PM Changeset [1487] by mulligan
committing some code for well labelling
2:36 PM Changeset [1486] by mulligan
finished asm costs

Nov 2, 2011:

6:58 PM Changeset [1485] by sacerdot
Less nice definitiion of add_with_carries that avoids a quadratic …
2:46 PM Changeset [1484] by sacerdot
2:40 PM Changeset [1483] by tranquil
* implemented a first draft of loop unrolling * correced bugs in CostExpr?
2:26 PM Changeset [1482] by sacerdot
1. very long standing conflict committed (but don't ask me what the …
2:00 PM Changeset [1481] by sacerdot
Proof fixed. The new standard library does not index any longer the …
1:59 PM Changeset [1480] by sacerdot
Proof changed (to use new automation). BUG FOUND: automation fails if …
8:27 AM Changeset [1479] by boender
- added insert_lookup_opt - assembly compiles now

Nov 1, 2011:

9:39 PM Changeset [1478] by sacerdot
Almost completed (up to is_finals).
6:31 PM Changeset [1477] by tranquil
* corrected a bug * implemented copy propagation * enhanced constant …
5:04 PM Changeset [1476] by sacerdot
3:14 PM Changeset [1475] by sacerdot
Towards the two fullexec transition systems that represent …

Oct 31, 2011:

10:18 AM Changeset [1474] by mulligan
adding missing asmcosts file for computing the costs of an assembly …

Oct 28, 2011:

4:45 PM Changeset [1473] by tranquil
* implemented partial redundancy elimination * added some tools for …
3:05 PM Changeset [1472] by mulligan
moved proof utils to erasure.ma
3:05 PM Changeset [1471] by mulligan
finished erasure and generalised so as to work on arbitrary joint programs

Oct 27, 2011:

5:29 PM Changeset [1470] by mulligan
finished, pretty ugly though as matita's disambiguation is a …
3:36 PM Changeset [1469] by mulligan
finished new relabelling for graphs subject to one axiom closed

Oct 26, 2011:

7:45 PM Changeset [1468] by tranquil
* implemented constant propagation * implementing partial redundancy …
5:25 PM Changeset [1467] by mulligan
small change, adding entry and exit labels into the internal function, …
5:08 PM Changeset [1466] by mulligan
erasure for graph based joint languages almost complete
2:07 PM Changeset [1465] by sacerdot
Dead code removed.

Oct 25, 2011:

7:12 PM Changeset [1464] by campbell
Use unification hints to simplify the graph monotonicity proofs.
5:33 PM Changeset [1463] by mulligan
added erasure for lin
4:11 PM Changeset [1462] by ayache
Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been …

Oct 24, 2011:

5:56 PM Changeset [1461] by mulligan
rewrote erasure for assembly programs
4:53 PM Changeset [1460] by mulligan
most of cost label erasure for assembly language complete, with one …
2:34 PM Changeset [1459] by boender
- moved stronger occurs_exactly_once lemma to its proper place in …
11:44 AM Changeset [1458] by mulligan
added skeleton file for erasure function for joint languages

Oct 23, 2011:

10:15 PM Changeset [1457] by sacerdot
Bug fixed: when calling an internal function, the pc block is now set …
6:37 PM Changeset [1456] by mulligan
changed type of pointer_of_label in report
5:51 PM Changeset [1455] by mulligan
ratios changed
4:28 PM Changeset [1454] by mulligan
removed mention of axiomatised code in LIN/semantics.ma
Note: See TracTimeline for information about the timeline view.