Timeline
11/25/11:
- 20:48 Changeset [1570] by
- Dependent type crazyness.
- 19:46 Changeset [1569] by
- * added in repository some missing files…
- 19:43 Changeset [1568] by
- * Immediates introduced (but not fully used yet in RTLabs to RTL pass) * …
- 18:17 Changeset [1567] by
- more work on big proof, 2.5 cases left
- 18:12 Changeset [1566] by
- Pacify changes to destruct tactic.
- 17:30 Changeset [1565] by
- Note that RTLabs ought to classify branches as "jumps" (in the structural …
- 15:31 Changeset [1564] by
- Commit where we use a dependently typed version of bigops. I am now going …
- 13:49 Changeset [1563] by
- A little progress on constructing RTLabs structured traces.
- 13:20 Changeset [1562] by
- new version of assembly, fixed conflict in positivemap.ma, changed …
- 13:13 Changeset [1561] by
- More dependent types to accomodate the statement.
11/24/11:
- 19:22 Changeset [1560] by
- Complete re-implementation that: 1) assumes no code before the first cost …
- 18:49 Changeset [1559] by
- Add a notion of flat traces with evidence for RTLabs.
- 18:47 Changeset [1558] by
- Snapshot before moving things to ASMCosts.ma.
- 18:09 Changeset [1557] by
- Byte => costlabel
- 17:24 Changeset [1556] by
- submitting to avoid conflicts
- 17:19 Changeset [1555] by
- - changes to assembly - added lookup to PositiveMap? - lightly changed …
- 16:49 Changeset [1554] by
- Major progress in the proof.
- 12:26 Changeset [1553] by
- - added lookup_opt_lookup lemma
- 12:12 Changeset [1552] by
- Update RTLabs structured trace definition.
- 11:52 Changeset [1551] by
- Functions to translate between back-end and front-end values.
- 11:44 Changeset [1550] by
- Repaired after use of Russell for execute_1.
- 11:11 Changeset [1549] by
- removed cruft from costsproof.ma file so claudio can work in parallel
11/23/11:
- 23:15 Changeset [1548] by
- …
- 23:08 Changeset [1547] by
- Invariant on cost of one execution step strengthened.
- 18:39 Changeset [1546] by
- added an option to prevent reindexing transformations from taking place, …
- 18:03 Changeset [1545] by
- Use pointer record in front-end.
- 18:01 Changeset [1544] by
- StructuredTraces? inhabited for object code.
- 17:46 Changeset [1543] by
- deletion of indexed labels branch
- 17:43 Changeset [1542] by
- merge of indexed labels branch
- 16:31 Changeset [1541] by
- interpret.ma now compiles
- 16:03 Changeset [1540] by
- changes to proof in interrupt.ma
- 13:55 Changeset [1539] by
- branch up to date
- 12:28 Changeset [1538] by
- changes to execute_1_0 proof
- 12:27 Changeset [1537] by
- A preliminary definition of the abstract status record for RTLabs.
- 12:07 Changeset [1536] by
- Use predicates throughout the structured traces.
- 12:07 Changeset [1535] by
- Make RTLabs semantics use knowledge that the next instruction always …
- 10:36 Changeset [1534] by
- committing my changes to interpret to prevent any further conflicts
11/22/11:
- 19:24 Changeset [1533] by
- Proof of execute_1 with Russell completed (up to some daemon used before).
- 16:18 Changeset [1532] by
- Remove jump classification from structured traces.
- 16:18 Changeset [1531] by
- A notion of abstract structured traces.
- 12:37 Changeset [1530] by
- Update due to Russell changes.
- 12:28 Changeset [1529] by
- Update RTLabs to RTL with unary operation types.
- 11:58 Changeset [1528] by
- Update most of Assembly.ma with new syntax and identifier maps. Change …
- 11:50 Changeset [1527] by
- More on Russell.
- 10:43 Changeset [1526] by
- Using Russell to prove some properties.
11/21/11:
- 18:17 Changeset [1525] by
- D2.2: function pointers using JMP.
- 17:51 Changeset [1524] by
- - adapted files to new Matita syntax
- 16:29 Changeset [1523] by
- Separate out positive and Z definitions from extralib.ma. Minor syntax …
- 15:49 Changeset [1522] by
- changes to preamble and lin to asm pass, resolved conflict in interpret
- 13:06 Changeset [1521] by
- Syntax change in Matita: change what where => change where what.
- 12:23 Changeset [1520] by
- Generate cost labels with correct type.
- 12:10 Changeset [1519] by
- More syntax updates.
- 11:15 Changeset [1518] by
- Update to new syntax.
11/19/11:
- 00:38 Changeset [1517] by
- Ported to syntax of Matita 0.99.1.
- 00:38 Changeset [1516] by
- Ported to syntax of Matita 0.99.1.
11/18/11:
- 13:03 Changeset [1515] by
- Add type of maps on positive binary numbers, and use them for identifers. …
11/17/11:
- 17:41 Changeset [1514] by
- changes from today. matita keeps dieing
- 16:50 Changeset [1513] by
- Fix up Clight examples.
- 16:11 Changeset [1512] by
- Shorten proof of goal that // solves now.
11/16/11:
- 17:35 Changeset [1511] by
- proofs, added, changes to execute_1_0 function therefore required to …
- 16:38 Changeset [1510] by
- All files ported to new dependent inversion.
11/15/11:
- 17:21 Changeset [1509] by
- i hate subtraction over the nats
- 17:12 Changeset [1508] by
- branched a version of the plug-in that is compatible with the indexed …
- 17:11 Changeset [1507] by
- * added an option to not use ternary expressions in costs, to accomodate …
- 10:05 Changeset [1506] by
- changes to costs proof over weekend
11/14/11:
- 13:22 Changeset [1505] by
- D2.2: addendum on 16 and 32 bits integer and function pointers support.
11/10/11:
- 15:39 Changeset [1504] by
- 8051 ocaml: bug fix in the labelling of do-whiles.
11/09/11:
- 11:14 Changeset [1503] by
- inductive type complete
11/08/11:
- 17:26 Changeset [1502] by
- changes to inductive defn
- 13:41 Changeset [1501] by
- We must take in account the labelled_p predicate.
- 13:34 Changeset [1500] by
- Proof sketch for one of the two main proofs.
11/07/11:
- 17:06 Changeset [1499] by
- part way through main statement transcription
- 16:56 Changeset [1498] by
- added new file for proof that costs are preserved at asm level
- 16:51 Changeset [1497] by
- a bit of tidying up, removing dead code, etc.
- 16:01 Changeset [1496] by
- problem fixed with tactics missing a semicolon to stop greedy parsing
- 15:45 Changeset [1495] by
- proper calculation of costs
- 10:56 Changeset [1494] by
- changes to get everything compiling again
11/04/11:
- 17:01 Changeset [1493] by
- finished well labeled check, up to injectivity of the label map
- 14:49 Changeset [1492] by
- Comment in D2.2 -> LINToASM about function pointers.
- 13:39 Changeset [1491] by
- Function pointers good and working.
- 13:25 Changeset [1490] by
- Function pointers fixed.
- 12:39 Changeset [1489] by
- Fix up a couple of lemmas affected by the change to add_with_carries.
- 12:22 Changeset [1488] by
- Function pointers in D2.2/8051. Bugged for now.
11/03/11:
- 17:24 Changeset [1487] by
- committing some code for well labelling
- 14:36 Changeset [1486] by
- finished asm costs
11/02/11:
- 18:58 Changeset [1485] by
- Less nice definitiion of add_with_carries that avoids a quadratic blow-up …
- 14:46 Changeset [1484] by
- …
- 14:40 Changeset [1483] by
- * implemented a first draft of loop unrolling * correced bugs in CostExpr?
- 14:26 Changeset [1482] by
- 1. very long standing conflict committed (but don't ask me what the stuff …
- 14:00 Changeset [1481] by
- Proof fixed. The new standard library does not index any longer the lemma …
- 13:59 Changeset [1480] by
- Proof changed (to use new automation). BUG FOUND: automation fails if run …
- 08:27 Changeset [1479] by
- - added insert_lookup_opt - assembly compiles now
11/01/11:
- 21:39 Changeset [1478] by
- Almost completed (up to is_finals).
- 18:31 Changeset [1477] by
- * corrected a bug * implemented copy propagation * enhanced constant …
- 17:04 Changeset [1476] by
- …
- 15:14 Changeset [1475] by
- Towards the two fullexec transition systems that represent interpretation …
10/31/11:
- 10:18 Changeset [1474] by
- adding missing asmcosts file for computing the costs of an assembly …
10/28/11:
- 16:45 Changeset [1473] by
- * implemented partial redundancy elimination * added some tools for …
- 15:05 Changeset [1472] by
- moved proof utils to erasure.ma
- 15:05 Changeset [1471] by
- finished erasure and generalised so as to work on arbitrary joint programs
10/27/11:
- 17:29 Changeset [1470] by
- finished, pretty ugly though as matita's disambiguation is a nightmare, so …
- 15:36 Changeset [1469] by
- finished new relabelling for graphs subject to one axiom closed
10/26/11:
- 19:45 Changeset [1468] by
- * implemented constant propagation * implementing partial redundancy …
- 17:25 Changeset [1467] by
- small change, adding entry and exit labels into the internal function, as …
- 17:08 Changeset [1466] by
- erasure for graph based joint languages almost complete
- 14:07 Changeset [1465] by
- Dead code removed.
Note: See TracTimeline
for information about the timeline view.
