Timeline
May 16, 2012:
- 9:12 PM Changeset [1961] by
- No more interaction required.
- 5:24 PM Changeset [1960] by
- Update RTLabs structured traces to make minor changes in definitions.
- 5:12 PM Changeset [1959] by
- Commented out diverging application of demodulation and closed goals …
- 4:47 PM Changeset [1958] by
- Marked divergence in StatusProofs?.ma
- 3:53 PM Changeset [1957] by
- Stitching proofs back together after slight change in statement of …
- 3:10 PM Changeset [1956] by
- - finished proof of lemma (where auto does strange things again)
- 3:03 PM Changeset [1955] by
- Completed proof of snd_assembly_1_pseudoinstruction_ok, modulo some …
- 2:44 PM Changeset [1954] by
- Initial state is in the labelling simulation (modulo global envs results).
- 10:29 AM Changeset [1953] by
- Commit to avoid conflicts.
- 1:29 AM Changeset [1952] by
- AssemblyProof? splitted.
- 1:28 AM Changeset [1951] by
- Bug with overloaded names in the context.
May 15, 2012:
- 6:20 PM Changeset [1950] by
- - advances in policy
- 5:51 PM Changeset [1949] by
- * lemma trace rel to eq flatten trace * some more properties of …
- 11:13 AM Changeset [1948] by
- Weakened statements of ASM/Assembly.ma and ASM/AssemblyProof.ma, so …
- 12:30 AM Changeset [1947] by
- Failure of automation/demod investigated a little bit.
- 12:01 AM Changeset [1946] by
- \snd half_add => add everywhere
May 14, 2012:
- 10:40 PM Changeset [1945] by
- All proof statements repaired.
- 7:56 PM Changeset [1944] by
- common/StructuredTraces no longer depends on ASM/AbstractStatus (again)
- 6:45 PM Changeset [1943] by
- - changed 'labels okay' part of create_label_cost_map
- 6:02 PM Changeset [1942] by
- Work on showing the equivalence of two methods of looking up from the maps.
- 4:33 PM Changeset [1941] by
- Changes to the AssemblyProof? with a few more (large) axioms closed.
- 4:05 PM Changeset [1940] by
- - committed new version of final invariant
- 10:37 AM Changeset [1939] by
- Changes to get things to compile and to avoid the dependency …
- 10:05 AM Changeset [1938] by
- Definitions moved to the right places, now everything compiles again.
May 11, 2012:
- 3:06 PM Changeset [1937] by
- - filled in some of the gaps in the proof of Policy - reverted …
- 2:38 PM Changeset [1936] by
- Some holes filled in AssemblyProof?.ma.
- 1:39 PM WikiStart edited by
- (diff)
May 10, 2012:
- 5:13 PM Changeset [1935] by
- Generalized some lemma in ASM/CostsProof.ma to work on abstract …
- 3:37 PM Changeset [1934] by
- - various & sundry moves of lemmas to better places - integrated …
- 12:00 PM Changeset [1933] by
- - slight revamp
- 10:35 AM Changeset [1932] by
- - added some more dependent types (we love 'em)
May 9, 2012:
- 7:23 PM Changeset [1931] by
- - added latest bvt alias - temporary "cases daemon" commit of new …
- 6:30 PM Changeset [1930] by
- Tidy up labelling simulation stuff a bit.
- 2:44 PM Changeset [1929] by
- Simplified proof by removing most of the invariants on the statements …
- 1:36 PM Changeset [1928] by
- Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should …
- 1:05 PM Changeset [1927] by
- Reduced complexity of good_program predicate, ported to new notion of …
May 8, 2012:
- 6:09 PM Changeset [1926] by
- * added as_label to abstract status, with as_costed defined with it. …
- 6:08 PM Changeset [1925] by
- - re-added jump_lenggh
- 6:04 PM Changeset [1924] by
- Added comment
- 3:43 PM Changeset [1923] by
- Small change, closing daemon that went under the RADAR
- 3:41 PM Changeset [1922] by
- Main labelling simulation proof complete.
- 3:29 PM Changeset [1921] by
- Horror proof mostly finished (compiles all way until end of CostsProof?.ma).
- 11:16 AM Changeset [1920] by
- Most of the labelling simulation. Still need to sort out switch …
May 7, 2012:
- 11:12 AM Changeset [1919] by
- Fixes to get everything compiling again
May 4, 2012:
- 3:40 PM Changeset [1918] by
- using listb.ma now
- 2:21 PM Changeset [1917] by
- predicate for unrepeating traces, fused final_abstract_status with …
- 1:59 PM Changeset [1916] by
- Closed remaining daemons in block_cost'. Rest of file now typechecks …
May 3, 2012:
- 7:13 PM Changeset [1915] by
- Correction of a typo in switchRemoval.
- 5:53 PM Changeset [1914] by
- Fix bug in Clight semantics that misses goto-labels inside a cost …
- 4:20 PM Changeset [1913] by
- Got the rest of the file to typecheck as before.
- 4:11 PM Changeset [1912] by
- Patches to get block_cost' and dependencies working again after change …
Apr 27, 2012:
- 6:45 PM Changeset [1911] by
- Changed statement of block_cost' to start on new termination argument
- 5:48 PM Changeset [1910] by
- Finished proof modulo termination argument
- 10:59 AM Changeset [1909] by
- Ported new statements to remainder of Interpret.ma file.
Apr 26, 2012:
- 5:38 PM Changeset [1908] by
- notation fixup following last commit of matita we shifted the levels …
- 5:37 PM Changeset [1907] by
- Fixes to get file to compile
- 5:20 PM Changeset [1906] by
- Statements simplified in block_cost and dependencies
- 5:15 PM Changeset [1905] by
- - plugging gap in assembly proof
- 5:03 PM Changeset [1904] by
- Problem with proof fixed by noting that problem is actually irrelevant
- 4:49 PM Changeset [1903] by
- Small changes prior to experiment
- 4:20 PM Changeset [1902] by
- Reverted needless changes to StructuredTraces?
- 3:35 PM Changeset [1901] by
- Slight changes to StructuredTraces?: should not change too much
Apr 23, 2012:
- 6:22 PM Changeset [1900] by
- CostProof? complete, modulo some daemons and axioms in earlier files
- 6:10 PM Changeset [1899] by
- Changes to statements of theorems
- 4:36 PM Changeset [1898] by
- Ported changes from ASMCosts.ma into CostsProof?.ma and got everything …
- 3:46 PM Changeset [1897] by
- Changes to proof, and pushed through those changes to rest of the file.
- 3:05 PM Changeset [1896] by
- Finished horror proof
Apr 20, 2012:
- 6:40 PM Changeset [1895] by
- Split the ASMCosts files while working on traverse_code_internal. A …
- 12:52 PM Changeset [1894] by
- Closed a hole in the proof by deriving a contradiction using even_p …
- 11:52 AM Changeset [1893] by
- Show stronger result about labelling of expressions.
Apr 19, 2012:
- 6:09 PM Changeset [1892] by
- Lots of work from today
Apr 18, 2012:
- 2:52 PM Changeset [1891] by
- Nightmarish proofs on bitvectors. Trying to find some way of making …
- 2:01 PM Changeset [1890] by
- - added comment about bitvector translation
Apr 17, 2012:
- 6:05 PM Changeset [1889] by
- - some pages of article
Note: See TracTimeline
for information about the timeline view.
