Timeline
Dec 1, 2011:
- 5:24 PM Changeset [1582] by
- more added to the proof of execute_1_preinstruction --- ~260 cases now …
- 3:15 PM Changeset [1581] by
- Dangling de Bruijn pointer when trying to propagate russell to set_arg_1
- 2:50 PM Changeset [1580] by
- implemented constant propagation in LTL cleaned up translations in …
- 2:11 PM Changeset [1579] by
- Finished proof with simpler statement, making everything a lot nicer
- 1:12 PM Changeset [1578] by
- - proof of termination of policy completed (needs some clean-up work …
Nov 30, 2011:
- 5:32 PM Changeset [1577] by
- A lot more cases added to the proof at the bottom of …
Nov 29, 2011:
- 5:22 PM Changeset [1576] by
- big changes to proofs, just two small cases remain and a few …
- 2:21 PM Changeset [1575] by
- Changes to specifications on execute functions
Nov 28, 2011:
- 5:57 PM Changeset [1574] by
- A little more progress on traces on RTLabs.
- 5:13 PM Changeset [1573] by
- more complicated than it appears :(
- 3:13 PM Changeset [1572] by
- * corrected previous bug * finished propagating immediates
- 1:39 PM Changeset [1571] by
- small changes
Nov 25, 2011:
- 8:48 PM Changeset [1570] by
- Dependent type crazyness.
- 7:46 PM Changeset [1569] by
- * added in repository some missing files…
- 7:43 PM Changeset [1568] by
- * Immediates introduced (but not fully used yet in RTLabs to RTL pass) …
- 6:17 PM Changeset [1567] by
- more work on big proof, 2.5 cases left
- 6:12 PM Changeset [1566] by
- Pacify changes to destruct tactic.
- 5:30 PM Changeset [1565] by
- Note that RTLabs ought to classify branches as "jumps" (in the …
- 3:31 PM Changeset [1564] by
- Commit where we use a dependently typed version of bigops. I am now …
- 1:49 PM Changeset [1563] by
- A little progress on constructing RTLabs structured traces.
- 1:20 PM Changeset [1562] by
- new version of assembly, fixed conflict in positivemap.ma, changed …
- 1:13 PM Changeset [1561] by
- More dependent types to accomodate the statement.
Nov 24, 2011:
- 7:22 PM Changeset [1560] by
- Complete re-implementation that: 1) assumes no code before the first …
- 6:49 PM Changeset [1559] by
- Add a notion of flat traces with evidence for RTLabs.
- 6:47 PM Changeset [1558] by
- Snapshot before moving things to ASMCosts.ma.
- 6:09 PM Changeset [1557] by
- Byte => costlabel
- 5:24 PM Changeset [1556] by
- submitting to avoid conflicts
- 5:19 PM Changeset [1555] by
- - changes to assembly - added lookup to PositiveMap? - lightly changed …
- 4:49 PM Changeset [1554] by
- Major progress in the proof.
- 12:26 PM Changeset [1553] by
- - added lookup_opt_lookup lemma
- 12:12 PM Changeset [1552] by
- Update RTLabs structured trace definition.
- 11:52 AM Changeset [1551] by
- Functions to translate between back-end and front-end values.
- 11:44 AM Changeset [1550] by
- Repaired after use of Russell for execute_1.
- 11:11 AM Changeset [1549] by
- removed cruft from costsproof.ma file so claudio can work in parallel
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 …
Note: See TracTimeline
for information about the timeline view.
