Timeline
Nov 23, 2011:
- 11:15 PM Changeset [1548] by
- …
- 11:08 PM Changeset [1547] by
- Invariant on cost of one execution step strengthened.
- 6:39 PM Changeset [1546] by
- added an option to prevent reindexing transformations from taking …
- 6:03 PM Changeset [1545] by
- Use pointer record in front-end.
- 6:01 PM Changeset [1544] by
- StructuredTraces? inhabited for object code.
- 5:46 PM Changeset [1543] by
- deletion of indexed labels branch
- 5:43 PM Changeset [1542] by
- merge of indexed labels branch
- 4:31 PM Changeset [1541] by
- interpret.ma now compiles
- 4:03 PM Changeset [1540] by
- changes to proof in interrupt.ma
- 1:55 PM Changeset [1539] by
- branch up to date
- 12:28 PM Changeset [1538] by
- changes to execute_1_0 proof
- 12:27 PM Changeset [1537] by
- A preliminary definition of the abstract status record for RTLabs.
- 12:07 PM Changeset [1536] by
- Use predicates throughout the structured traces.
- 12:07 PM Changeset [1535] by
- Make RTLabs semantics use knowledge that the next instruction always …
- 10:36 AM Changeset [1534] by
- committing my changes to interpret to prevent any further conflicts
Nov 22, 2011:
- 7:24 PM Changeset [1533] by
- Proof of execute_1 with Russell completed (up to some daemon used before).
- 4:18 PM Changeset [1532] by
- Remove jump classification from structured traces.
- 4:18 PM Changeset [1531] by
- A notion of abstract structured traces.
- 12:37 PM Changeset [1530] by
- Update due to Russell changes.
- 12:28 PM Changeset [1529] by
- Update RTLabs to RTL with unary operation types.
- 11:58 AM Changeset [1528] by
- Update most of Assembly.ma with new syntax and identifier maps. Change …
- 11:50 AM Changeset [1527] by
- More on Russell.
- 10:43 AM Changeset [1526] by
- Using Russell to prove some properties.
Nov 21, 2011:
- 6:17 PM Changeset [1525] by
- D2.2: function pointers using JMP.
- 5:51 PM Changeset [1524] by
- - adapted files to new Matita syntax
- 4:29 PM Changeset [1523] by
- Separate out positive and Z definitions from extralib.ma. Minor syntax …
- 3:49 PM Changeset [1522] by
- changes to preamble and lin to asm pass, resolved conflict in interpret
- 1:06 PM Changeset [1521] by
- Syntax change in Matita: change what where => change where what.
- 12:23 PM Changeset [1520] by
- Generate cost labels with correct type.
- 12:10 PM Changeset [1519] by
- More syntax updates.
- 11:15 AM Changeset [1518] by
- Update to new syntax.
Nov 19, 2011:
- 12:38 AM Changeset [1517] by
- Ported to syntax of Matita 0.99.1.
- 12:38 AM Changeset [1516] by
- Ported to syntax of Matita 0.99.1.
Nov 18, 2011:
- 1:03 PM Changeset [1515] by
- Add type of maps on positive binary numbers, and use them for …
Nov 17, 2011:
- 5:41 PM Changeset [1514] by
- changes from today. matita keeps dieing
- 4:50 PM Changeset [1513] by
- Fix up Clight examples.
- 4:11 PM Changeset [1512] by
- Shorten proof of goal that solves now.
Nov 16, 2011:
- 5:35 PM Changeset [1511] by
- proofs, added, changes to execute_1_0 function therefore required to …
- 4:38 PM Changeset [1510] by
- All files ported to new dependent inversion.
Nov 15, 2011:
- 5:21 PM Changeset [1509] by
- i hate subtraction over the nats
- 5:12 PM Changeset [1508] by
- branched a version of the plug-in that is compatible with the indexed …
- 5:11 PM Changeset [1507] by
- * added an option to not use ternary expressions in costs, to …
- 10:05 AM Changeset [1506] by
- changes to costs proof over weekend
Nov 14, 2011:
- 1:22 PM Changeset [1505] by
- D2.2: addendum on 16 and 32 bits integer and function pointers support.
Nov 10, 2011:
- 3:39 PM Changeset [1504] by
- 8051 ocaml: bug fix in the labelling of do-whiles.
Nov 9, 2011:
- 11:14 AM Changeset [1503] by
- inductive type complete
Nov 8, 2011:
- 5:26 PM Changeset [1502] by
- changes to inductive defn
- 1:41 PM Changeset [1501] by
- We must take in account the labelled_p predicate.
- 1:34 PM Changeset [1500] by
- Proof sketch for one of the two main proofs.
Nov 7, 2011:
- 5:06 PM Changeset [1499] by
- part way through main statement transcription
- 4:56 PM Changeset [1498] by
- added new file for proof that costs are preserved at asm level
- 4:51 PM Changeset [1497] by
- a bit of tidying up, removing dead code, etc.
- 4:01 PM Changeset [1496] by
- problem fixed with tactics missing a semicolon to stop greedy parsing
- 3:45 PM Changeset [1495] by
- proper calculation of costs
- 10:56 AM Changeset [1494] by
- changes to get everything compiling again
Nov 4, 2011:
- 5:01 PM Changeset [1493] by
- finished well labeled check, up to injectivity of the label map
- 2:49 PM Changeset [1492] by
- Comment in D2.2 -> LINToASM about function pointers.
- 1:39 PM Changeset [1491] by
- Function pointers good and working.
- 1:25 PM Changeset [1490] by
- Function pointers fixed.
- 12:39 PM Changeset [1489] by
- Fix up a couple of lemmas affected by the change to add_with_carries.
- 12:22 PM Changeset [1488] by
- Function pointers in D2.2/8051. Bugged for now.
Nov 3, 2011:
- 5:24 PM Changeset [1487] by
- committing some code for well labelling
- 2:36 PM Changeset [1486] by
- finished asm costs
Nov 2, 2011:
- 6:58 PM Changeset [1485] by
- Less nice definitiion of add_with_carries that avoids a quadratic …
- 2:46 PM Changeset [1484] by
- …
- 2:40 PM Changeset [1483] by
- * implemented a first draft of loop unrolling * correced bugs in CostExpr?
- 2:26 PM Changeset [1482] by
- 1. very long standing conflict committed (but don't ask me what the …
- 2:00 PM Changeset [1481] by
- Proof fixed. The new standard library does not index any longer the …
- 1:59 PM Changeset [1480] by
- Proof changed (to use new automation). BUG FOUND: automation fails if …
- 8:27 AM Changeset [1479] by
- - added insert_lookup_opt - assembly compiles now
Nov 1, 2011:
- 9:39 PM Changeset [1478] by
- Almost completed (up to is_finals).
- 6:31 PM Changeset [1477] by
- * corrected a bug * implemented copy propagation * enhanced constant …
- 5:04 PM Changeset [1476] by
- …
- 3:14 PM Changeset [1475] by
- Towards the two fullexec transition systems that represent …
Oct 31, 2011:
- 10:18 AM Changeset [1474] by
- adding missing asmcosts file for computing the costs of an assembly …
Oct 28, 2011:
- 4:45 PM Changeset [1473] by
- * implemented partial redundancy elimination * added some tools for …
- 3:05 PM Changeset [1472] by
- moved proof utils to erasure.ma
- 3:05 PM Changeset [1471] by
- finished erasure and generalised so as to work on arbitrary joint programs
Oct 27, 2011:
- 5:29 PM Changeset [1470] by
- finished, pretty ugly though as matita's disambiguation is a …
- 3:36 PM Changeset [1469] by
- finished new relabelling for graphs subject to one axiom closed
Oct 26, 2011:
- 7:45 PM Changeset [1468] by
- * implemented constant propagation * implementing partial redundancy …
- 5:25 PM Changeset [1467] by
- small change, adding entry and exit labels into the internal function, …
- 5:08 PM Changeset [1466] by
- erasure for graph based joint languages almost complete
- 2:07 PM Changeset [1465] by
- Dead code removed.
Oct 25, 2011:
- 7:12 PM Changeset [1464] by
- Use unification hints to simplify the graph monotonicity proofs.
- 5:33 PM Changeset [1463] by
- added erasure for lin
- 4:11 PM Changeset [1462] by
- Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been …
Oct 24, 2011:
- 5:56 PM Changeset [1461] by
- rewrote erasure for assembly programs
- 4:53 PM Changeset [1460] by
- most of cost label erasure for assembly language complete, with one …
- 2:34 PM Changeset [1459] by
- - moved stronger occurs_exactly_once lemma to its proper place in …
- 11:44 AM Changeset [1458] by
- added skeleton file for erasure function for joint languages
Note: See TracTimeline
for information about the timeline view.
