Timeline
Dec 19, 2011:
- 2:48 PM Changeset [1631] by
- Use fact that type environments in Cminor have distinct variables to …
- 2:48 PM Changeset [1630] by
- Remainder of freshness in Clight to Cminor pass.
- 2:48 PM Changeset [1629] by
- Sort out most of the fresh names stuff in Clight to Cminor.
- 2:48 PM Changeset [1628] by
- Show that the universe generated by Clight/fresh.ma is good.
- 2:48 PM Changeset [1627] by
- Add some notions of freshness, and start using them for temporary …
- 2:48 PM Changeset [1626] by
- Add extra type safety in front end. NB: critical freshness parts …
Dec 16, 2011:
- 6:35 PM Changeset [1625] by
- before christmas
- 3:44 PM Changeset [1624] by
- commit for claudio
- 2:07 PM Changeset [1623] by
- strange matita issue
- 10:09 AM Changeset [1622] by
- to avoid conflicts, bug in typechecker?
Dec 15, 2011:
- 10:22 AM Changeset [1621] by
- to prevent conflicts
- 12:23 AM Changeset [1620] by
- One of the mutual cases of the open proof is practically finished.
- 12:02 AM Changeset [1619] by
- Major advancement.
Dec 14, 2011:
- 6:17 PM Changeset [1618] by
- Minor updates due to recent changes.
- 6:17 PM Changeset [1617] by
- Note stuff to do on structured traces.
- 5:57 PM Changeset [1616] by
- Partially ported to new Matita syntax. Because of some changes in …
- 5:28 PM Changeset [1615] by
- Policy now depends on Assembly and not the other way around.
- 5:00 PM Changeset [1614] by
- - split policy from assembly
- 4:41 PM Changeset [1613] by
- Coercion moved to Matita standard lib.
- 3:58 PM Changeset [1612] by
- All library ported to new Matita lib (finally).
- 3:35 PM Changeset [1611] by
- All of Cminor now compiles with the latest lib of Matita.
- 3:33 PM Changeset [1610] by
- Ported to new lib.
- 2:44 PM Changeset [1609] by
- - added alias to ASM/BitVectorTrie - removed double include from …
- 2:30 PM Changeset [1608] by
- Porting to new library still in progress.
- 1:50 PM Changeset [1607] by
- Porting to new library.
- 1:40 PM Changeset [1606] by
- Porting to last library of Matita.
- 1:18 PM Changeset [1605] by
- Porting to last standard library of Matita.
- 11:52 AM Changeset [1604] by
- for jaap
Dec 13, 2011:
- 5:37 PM Changeset [1603] by
- More proofs ported to new lib.
- 4:23 PM Changeset [1602] by
- giving up on fetch proofs for time being
- 2:49 PM Changeset [1601] by
- Files ported to new version of the standard library.
- 1:41 PM Changeset [1600] by
- utilities and ASM ported to the new standard library
- 1:34 AM Changeset [1599] by
- Start of merging of stuff into the standard library of Matita.
Dec 12, 2011:
- 5:53 PM Changeset [1598] by
- changes over the last couple of days
- 9:51 AM Changeset [1597] by
- fixed fetch for jaap
Dec 7, 2011:
- 4:24 PM Changeset [1596] by
- RTLabs structured traces: sort out passing of termination proofs around.
- 4:24 PM Changeset [1595] by
- We don't need an explicit termination count when building traces.
- 4:24 PM Changeset [1594] by
- Rework handling of termination information in RTLabs structured traces …
- 3:48 PM Changeset [1593] by
- - cleaned up Assembly, moved some definitions elsewhere
- 2:50 PM Changeset [1592] by
- - updated definitions to work with programs of maximum 216 instructions
Dec 6, 2011:
- 5:24 PM Changeset [1591] by
- work from today
- 5:13 PM Changeset [1590] by
- * got back to previous implementation of multiplication in RTLabs -> …
- 5:04 PM Changeset [1589] by
- * turned to argument-less return statements for RTLabs and RTL (there …
- 11:21 AM Changeset [1588] by
- All goals generated by Russell for execute_1* are now closed, mostly …
Dec 5, 2011:
- 5:16 PM Changeset [1587] by
- changes from today, including removing indexing of problematic …
- 1:11 PM Changeset [1586] by
- RTLabs structured traces: cost labels after jumps.
Dec 2, 2011:
- 7:49 PM Changeset [1585] by
- fighting with a bug of the translation from RTL to ERTL
- 3:13 PM Changeset [1584] by
- * new form of translation written in graphUtilites (mainly as a test …
- 1:02 PM Changeset [1583] by
- More on RTLabs structured traces. Fixed mistake in structure trace …
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.
Note: See TracTimeline
for information about the timeline view.
