source: src/RTLabs

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @2502   9 years campbell Sketch a little about how measurable traces might work with RTLabs and …
(edit) @2499   9 years campbell Separate out the RTLabs abstract status record from the proofs about …
(edit) @2493   9 years mckinna Change in cst_well_defd to fix previously broken defn of …
(edit) @2490   9 years tranquil switched back to Byte immediate (instead of beval ones) propagated …
(edit) @2475   9 years campbell Get compiler.ma and correctness.ma checking again. Note that the …
(edit) @2439   9 years campbell Get a proper reverse mapping of function blocks to identifiers by …
(edit) @2420   9 years campbell Tidy away generic results about folds on positive/identifier maps.
(edit) @2418   9 years campbell Add a checking function for the uniqueness of cost labels in RTLabs …
(edit) @2395   9 years campbell Proper handling of comparison of pointers off-the-end of an object. We …
(edit) @2384   9 years campbell Move Matita pretty printers into place.
(edit) @2315   9 years campbell Add some more commentary.
(edit) @2314   9 years campbell Move generic definitions from recent commit to appropriate places.
(edit) @2313   9 years campbell RTLabs cost checker correct.
(edit) @2308   9 years campbell More proof (and corrections) on cost checking.
(edit) @2307   9 years campbell Half the proofs for sound cost labelling check.
(edit) @2305   9 years campbell RTLabs cost spec checking function implemented (lacks proof, or much …
(edit) @2303   9 years campbell Some preliminary checking of cost labelling properties in RTLabs.
(edit) @2300   9 years campbell Cut out some dead ends and add some comments to the last commit.
(edit) @2299   9 years campbell Soundly labelled RTLabs structured traces are "unrepeating".
(edit) @2297   9 years campbell Nicer form of steps until cost label bound in RTLabs.
(edit) @2296   9 years campbell Tidy up some ill-placed definitions.
(edit) @2295   9 years campbell Start on showing unrepeating property of RTLabs structured traces: …
(edit) @2294   9 years campbell Make RTLabs cost spec deterministic.
(edit) @2293   9 years campbell Add instruction pointer for call states in RTLabs.
(edit) @2292   9 years campbell More RTLabs invariants.
(edit) @2290   9 years campbell Remove jump tables from RTLabs -> RTL.
(edit) @2288   9 years campbell Remove jumptables from RTLabs. :(
(edit) @2287   9 years campbell RTLabs typing for loads and stores.
(edit) @2286   9 years tranquil Big update! * merge of all _paolo variants * reorganised some depends …
(edit) @2226   9 years campbell Whole program proof.
(edit) @2224   9 years campbell Proper whole program result in RTLabs/Traces
(edit) @2223   9 years campbell Simplify RTLabs structure traces proofs by getting rid of wrong …
(edit) @2218   9 years campbell Separate out cost properties required of RTLabs programs from the …
(edit) @2217   9 years tranquil * collapsed step_params, unserialized_params, funct_params and …
(edit) @2214   9 years tranquil * changed order of parameters of joint_internal_function and genv in …
(edit) @2208   9 years tranquil * moving some code around * changed immediates to hold beval in …
(edit) @2184   9 years campbell Minor fix ups.
(edit) @2176   9 years campbell Remove memory spaces other than XData and Code; simplify pointers as a …
(edit) @2162   9 years tranquil * yet another correction to joint * added functions adding prologues …
(edit) @2155   9 years tranquil updates to blocks and RTLabs to RTL translation (which sidesteps …
(edit) @2103   9 years campbell Make transform_*program take a more general transformation to make …
(edit) @2044   9 years campbell PCs for RTLabs structured traces.
(edit) @2032   9 years sacerdot !! BEWARE: major commit !! 1) [affects everybody] split for …
(edit) @2025   9 years campbell Silly typo and old comment.
(edit) @1999   9 years campbell Make back-end use the main global envs.
(edit) @1995   9 years campbell Overall compiler definition; bits and pieces to make everything happy(ish).
(edit) @1988   9 years campbell Abstraction of the memory contents in the memory models is no longer …
(edit) @1986   9 years campbell Get rid of unused abstraction of Globalenvs.
(edit) @1960   9 years campbell Update RTLabs structured traces to make minor changes in definitions.
(edit) @1920   9 years campbell Most of the labelling simulation. Still need to sort out switch …
(edit) @1882   10 years tranquil big update, alas incomplete: joint changed a bit, and all BE languages …
(edit) @1880   10 years campbell Show that RTLabs flat traces are determined by their starting state, …
(edit) @1878   10 years campbell Enforce typing of constants in front-end, plus binops for RTLabs.
(edit) @1877   10 years campbell Update RTLabs structured traces for typed binops and new memory model.
(edit) @1874   10 years campbell First cut at using back-end memory model throughout. Note the …
(edit) @1872   10 years campbell Make binary operations in Cminor/RTLabs properly typed. A few extra …
(edit) @1812   10 years campbell Provide a combined type for terminating and non-terminating structured …
(edit) @1808   10 years campbell Create a Prop version of the non-terminating structured traces so that …
(edit) @1806   10 years campbell Show that we could construct RTLabs non-terminating structured traces …
(edit) @1805   10 years campbell RTLabs structured traces: package up some of the properties we need …
(edit) @1784   10 years campbell Start on proof of existence of nonterminating RTLabs structured traces.
(edit) @1782   10 years campbell Correct bad inversion.
(edit) @1765   10 years campbell Rule out final states in non-terminating executions chunks (RTLabs …
(edit) @1764   10 years campbell Terminating function preserve the property that the execution does not …
(edit) @1736   10 years campbell Show that the bound on the number of instructions until a cost label …
(edit) @1719   10 years campbell Show that non-termination survives a terminating function call.
(edit) @1713   10 years campbell Add a distinguished final state to the front-end languages to match up …
(edit) @1712   10 years campbell Show that constructing an RTLabs structure trace really does use a …
(edit) @1707   10 years campbell Progress on finite segments of infinite RTLabs structured trace.
(edit) @1706   10 years campbell Checkpoint RTLabs structured traces.
(edit) @1705   10 years campbell Checkpoint RTLabs labelling soundness work.
(edit) @1682   10 years campbell Complete proof for as_after_return for RTLabs.
(edit) @1681   10 years campbell Checkpoint of stack preservation work in RTLabs.
(edit) @1680   10 years campbell Comment out unused tailcalls in Cminor and RTLabs. (They would be a …
(edit) @1675   10 years campbell Some work on sound labelled for RTLabs.
(edit) @1671   10 years campbell A little more on RTLabs infinite traces.
(edit) @1670   10 years campbell Snapshot of non-terminating RTLabs structured traces work.
(edit) @1656   10 years campbell Minor fixups to RTLabs/Traces due to syntax changes.
(edit) @1655   10 years campbell Update Cminor and RTLabs semantics to use new monad definitions.
(edit) @1654   10 years campbell Corrections to structured trace definitions (see the mailing list). …
(edit) @1653   10 years campbell Start on building finite sections of non-terminating structured traces.
(edit) @1651   10 years campbell Start looking at non-terminating structured traces by defining …
(edit) @1644   10 years tranquil minor changes
(edit) @1643   10 years tranquil * some changes in everything * separated extensions in sequential and …
(edit) @1640   10 years tranquil * finished fork of semantics.ma * unification of Errors under the …
(edit) @1638   10 years campbell Tidy up RTLabs structured traces code a little.
(edit) @1637   10 years campbell RTLabs structured traces: Add a termination measure to satisfy …
(edit) @1636   10 years tranquil * added coercions to arguments (in RTL) and notation for ops (for the …
(edit) @1635   10 years tranquil * lists with binders and monads * Joint.ma and other temprarily …
(edit) @1633   10 years campbell Update Cminor pretty printer and examples.
(edit) @1626   10 years campbell Add extra type safety in front end. NB: critical freshness parts …
(edit) @1617   10 years campbell Note stuff to do on structured traces.
(edit) @1612   10 years sacerdot All library ported to new Matita lib (finally).
(edit) @1601   10 years sacerdot Files ported to new version of the standard library.
(edit) @1596   10 years campbell RTLabs structured traces: sort out passing of termination proofs around.
(edit) @1595   10 years campbell We don't need an explicit termination count when building traces.
(edit) @1594   10 years campbell Rework handling of termination information in RTLabs structured traces …
(edit) @1586   10 years campbell RTLabs structured traces: cost labels after jumps.
(edit) @1583   10 years campbell More on RTLabs structured traces. Fixed mistake in structure trace …
(edit) @1574   10 years campbell A little more progress on traces on RTLabs.
Note: See TracRevisionLog for help on using the revision log.