source: src/RTLabs

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @2296   7 years campbell Tidy up some ill-placed definitions.
(edit) @2295   7 years campbell Start on showing unrepeating property of RTLabs structured traces: …
(edit) @2294   7 years campbell Make RTLabs cost spec deterministic.
(edit) @2293   7 years campbell Add instruction pointer for call states in RTLabs.
(edit) @2292   7 years campbell More RTLabs invariants.
(edit) @2290   7 years campbell Remove jump tables from RTLabs -> RTL.
(edit) @2288   7 years campbell Remove jumptables from RTLabs. :(
(edit) @2287   7 years campbell RTLabs typing for loads and stores.
(edit) @2286   7 years tranquil Big update! * merge of all _paolo variants * reorganised some depends …
(edit) @2226   7 years campbell Whole program proof.
(edit) @2224   7 years campbell Proper whole program result in RTLabs/Traces
(edit) @2223   7 years campbell Simplify RTLabs structure traces proofs by getting rid of wrong …
(edit) @2218   7 years campbell Separate out cost properties required of RTLabs programs from the …
(edit) @2217   7 years tranquil * collapsed step_params, unserialized_params, funct_params and …
(edit) @2214   7 years tranquil * changed order of parameters of joint_internal_function and genv in …
(edit) @2208   7 years tranquil * moving some code around * changed immediates to hold beval in …
(edit) @2184   7 years campbell Minor fix ups.
(edit) @2176   7 years campbell Remove memory spaces other than XData and Code; simplify pointers as a …
(edit) @2162   7 years tranquil * yet another correction to joint * added functions adding prologues …
(edit) @2155   7 years tranquil updates to blocks and RTLabs to RTL translation (which sidesteps …
(edit) @2103   7 years campbell Make transform_*program take a more general transformation to make …
(edit) @2044   7 years campbell PCs for RTLabs structured traces.
(edit) @2032   7 years sacerdot !! BEWARE: major commit !! 1) [affects everybody] split for …
(edit) @2025   7 years campbell Silly typo and old comment.
(edit) @1999   7 years campbell Make back-end use the main global envs.
(edit) @1995   7 years campbell Overall compiler definition; bits and pieces to make everything happy(ish).
(edit) @1988   7 years campbell Abstraction of the memory contents in the memory models is no longer …
(edit) @1986   7 years campbell Get rid of unused abstraction of Globalenvs.
(edit) @1960   7 years campbell Update RTLabs structured traces to make minor changes in definitions.
(edit) @1920   7 years campbell Most of the labelling simulation. Still need to sort out switch …
(edit) @1882   8 years tranquil big update, alas incomplete: joint changed a bit, and all BE languages …
(edit) @1880   8 years campbell Show that RTLabs flat traces are determined by their starting state, …
(edit) @1878   8 years campbell Enforce typing of constants in front-end, plus binops for RTLabs.
(edit) @1877   8 years campbell Update RTLabs structured traces for typed binops and new memory model.
(edit) @1874   8 years campbell First cut at using back-end memory model throughout. Note the …
(edit) @1872   8 years campbell Make binary operations in Cminor/RTLabs properly typed. A few extra …
(edit) @1812   8 years campbell Provide a combined type for terminating and non-terminating structured …
(edit) @1808   8 years campbell Create a Prop version of the non-terminating structured traces so that …
(edit) @1806   8 years campbell Show that we could construct RTLabs non-terminating structured traces …
(edit) @1805   8 years campbell RTLabs structured traces: package up some of the properties we need …
(edit) @1784   8 years campbell Start on proof of existence of nonterminating RTLabs structured traces.
(edit) @1782   8 years campbell Correct bad inversion.
(edit) @1765   8 years campbell Rule out final states in non-terminating executions chunks (RTLabs …
(edit) @1764   8 years campbell Terminating function preserve the property that the execution does not …
(edit) @1736   8 years campbell Show that the bound on the number of instructions until a cost label …
(edit) @1719   8 years campbell Show that non-termination survives a terminating function call.
(edit) @1713   8 years campbell Add a distinguished final state to the front-end languages to match up …
(edit) @1712   8 years campbell Show that constructing an RTLabs structure trace really does use a …
(edit) @1707   8 years campbell Progress on finite segments of infinite RTLabs structured trace.
(edit) @1706   8 years campbell Checkpoint RTLabs structured traces.
(edit) @1705   8 years campbell Checkpoint RTLabs labelling soundness work.
(edit) @1682   8 years campbell Complete proof for as_after_return for RTLabs.
(edit) @1681   8 years campbell Checkpoint of stack preservation work in RTLabs.
(edit) @1680   8 years campbell Comment out unused tailcalls in Cminor and RTLabs. (They would be a …
(edit) @1675   8 years campbell Some work on sound labelled for RTLabs.
(edit) @1671   8 years campbell A little more on RTLabs infinite traces.
(edit) @1670   8 years campbell Snapshot of non-terminating RTLabs structured traces work.
(edit) @1656   8 years campbell Minor fixups to RTLabs/Traces due to syntax changes.
(edit) @1655   8 years campbell Update Cminor and RTLabs semantics to use new monad definitions.
(edit) @1654   8 years campbell Corrections to structured trace definitions (see the mailing list). …
(edit) @1653   8 years campbell Start on building finite sections of non-terminating structured traces.
(edit) @1651   8 years campbell Start looking at non-terminating structured traces by defining …
(edit) @1644   8 years tranquil minor changes
(edit) @1643   8 years tranquil * some changes in everything * separated extensions in sequential and …
(edit) @1640   8 years tranquil * finished fork of semantics.ma * unification of Errors under the …
(edit) @1638   8 years campbell Tidy up RTLabs structured traces code a little.
(edit) @1637   8 years campbell RTLabs structured traces: Add a termination measure to satisfy …
(edit) @1636   8 years tranquil * added coercions to arguments (in RTL) and notation for ops (for the …
(edit) @1635   8 years tranquil * lists with binders and monads * Joint.ma and other temprarily …
(edit) @1633   8 years campbell Update Cminor pretty printer and examples.
(edit) @1626   8 years campbell Add extra type safety in front end. NB: critical freshness parts …
(edit) @1617   8 years campbell Note stuff to do on structured traces.
(edit) @1612   8 years sacerdot All library ported to new Matita lib (finally).
(edit) @1601   8 years sacerdot Files ported to new version of the standard library.
(edit) @1596   8 years campbell RTLabs structured traces: sort out passing of termination proofs around.
(edit) @1595   8 years campbell We don't need an explicit termination count when building traces.
(edit) @1594   8 years campbell Rework handling of termination information in RTLabs structured traces …
(edit) @1586   8 years campbell RTLabs structured traces: cost labels after jumps.
(edit) @1583   8 years campbell More on RTLabs structured traces. Fixed mistake in structure trace …
(edit) @1574   8 years campbell A little more progress on traces on RTLabs.
(edit) @1565   8 years campbell Note that RTLabs ought to classify branches as "jumps" (in the …
(edit) @1563   8 years campbell A little progress on constructing RTLabs structured traces.
(edit) @1559   8 years campbell Add a notion of flat traces with evidence for RTLabs.
(edit) @1552   8 years campbell Update RTLabs structured trace definition.
(edit) @1537   8 years campbell A preliminary definition of the abstract status record for RTLabs.
(edit) @1535   8 years campbell Make RTLabs semantics use knowledge that the next instruction always …
(edit) @1529   8 years campbell Update RTLabs to RTL with unary operation types.
(edit) @1521   8 years sacerdot Syntax change in Matita: change what where => change where what.
(edit) @1515   8 years campbell Add type of maps on positive binary numbers, and use them for …
(edit) @1408   8 years sacerdot 1. Added joint/BEGlobalenvs that is a modification of …
(edit) @1369   8 years campbell Put type information into front-end unary ops. Slight change to …
(edit) @1358   8 years mulligan got rtlabs to rtl compiling, foldi_strong needs examining
(edit) @1356   8 years mulligan deleted redundant directory. added outlines for both reports, and …
(edit) @1354   8 years sacerdot One axiom closed.
(edit) @1352   8 years sacerdot This commit is made necessary by the last Matita change. Inclusion is …
(edit) @1343   8 years mulligan fixed some bugs in the translation
(edit) @1331   8 years mulligan some changes, but i now have two contradictory proof obligations.
(edit) @1325   8 years mulligan finished implementing the translate constant function
(edit) @1316   8 years campbell Merge in id-lookup-branch to trunk.
(edit) @1315   8 years mulligan another move for the same reason. got rtlabs > rtl compiling again by …
Note: See TracRevisionLog for help on using the revision log.