|
|
|
@1920
|
9 years |
campbell |
Most of the labelling simulation. Still need to sort out switch …
|
|
|
|
@1882
|
9 years |
tranquil |
big update, alas incomplete:
joint changed a bit, and all BE languages …
|
|
|
|
@1880
|
9 years |
campbell |
Show that RTLabs flat traces are determined by their starting state, …
|
|
|
|
@1878
|
9 years |
campbell |
Enforce typing of constants in front-end, plus binops for RTLabs.
|
|
|
|
@1877
|
9 years |
campbell |
Update RTLabs structured traces for typed binops and new memory model.
|
|
|
|
@1874
|
9 years |
campbell |
First cut at using back-end memory model throughout.
Note the …
|
|
|
|
@1872
|
9 years |
campbell |
Make binary operations in Cminor/RTLabs properly typed.
A few extra …
|
|
|
|
@1812
|
9 years |
campbell |
Provide a combined type for terminating and non-terminating structured …
|
|
|
|
@1808
|
9 years |
campbell |
Create a Prop version of the non-terminating structured traces so that …
|
|
|
|
@1806
|
9 years |
campbell |
Show that we could construct RTLabs non-terminating structured traces …
|
|
|
|
@1805
|
9 years |
campbell |
RTLabs structured traces: package up some of the properties we need …
|
|
|
|
@1784
|
9 years |
campbell |
Start on proof of existence of nonterminating RTLabs structured traces.
|
|
|
|
@1782
|
9 years |
campbell |
Correct bad inversion.
|
|
|
|
@1765
|
9 years |
campbell |
Rule out final states in non-terminating executions chunks (RTLabs …
|
|
|
|
@1764
|
9 years |
campbell |
Terminating function preserve the property that the execution does not …
|
|
|
|
@1736
|
9 years |
campbell |
Show that the bound on the number of instructions until a cost label …
|
|
|
|
@1719
|
9 years |
campbell |
Show that non-termination survives a terminating function call.
|
|
|
|
@1713
|
9 years |
campbell |
Add a distinguished final state to the front-end languages to match up …
|
|
|
|
@1712
|
9 years |
campbell |
Show that constructing an RTLabs structure trace really does use a …
|
|
|
|
@1707
|
9 years |
campbell |
Progress on finite segments of infinite RTLabs structured trace.
|
|
|
|
@1706
|
9 years |
campbell |
Checkpoint RTLabs structured traces.
|
|
|
|
@1705
|
9 years |
campbell |
Checkpoint RTLabs labelling soundness work.
|
|
|
|
@1682
|
9 years |
campbell |
Complete proof for as_after_return for RTLabs.
|
|
|
|
@1681
|
9 years |
campbell |
Checkpoint of stack preservation work in RTLabs.
|
|
|
|
@1680
|
9 years |
campbell |
Comment out unused tailcalls in Cminor and RTLabs.
(They would be a …
|
|
|
|
@1675
|
9 years |
campbell |
Some work on sound labelled for RTLabs.
|
|
|
|
@1671
|
9 years |
campbell |
A little more on RTLabs infinite traces.
|
|
|
|
@1670
|
9 years |
campbell |
Snapshot of non-terminating RTLabs structured traces work.
|
|
|
|
@1656
|
9 years |
campbell |
Minor fixups to RTLabs/Traces due to syntax changes.
|
|
|
|
@1655
|
9 years |
campbell |
Update Cminor and RTLabs semantics to use new monad definitions.
|
|
|
|
@1654
|
9 years |
campbell |
Corrections to structured trace definitions (see the mailing list). …
|
|
|
|
@1653
|
9 years |
campbell |
Start on building finite sections of non-terminating structured traces.
|
|
|
|
@1651
|
9 years |
campbell |
Start looking at non-terminating structured traces by defining …
|
|
|
|
@1644
|
9 years |
tranquil |
minor changes
|
|
|
|
@1643
|
9 years |
tranquil |
* some changes in everything
* separated extensions in sequential and …
|
|
|
|
@1640
|
9 years |
tranquil |
* finished fork of semantics.ma
* unification of Errors under the …
|
|
|
|
@1638
|
9 years |
campbell |
Tidy up RTLabs structured traces code a little.
|
|
|
|
@1637
|
9 years |
campbell |
RTLabs structured traces: Add a termination measure to satisfy …
|
|
|
|
@1636
|
9 years |
tranquil |
* added coercions to arguments (in RTL) and notation for ops (for the …
|
|
|
|
@1635
|
9 years |
tranquil |
* lists with binders and monads
* Joint.ma and other temprarily …
|
|
|
|
@1633
|
9 years |
campbell |
Update Cminor pretty printer and examples.
|
|
|
|
@1626
|
9 years |
campbell |
Add extra type safety in front end. NB: critical freshness parts …
|
|
|
|
@1617
|
9 years |
campbell |
Note stuff to do on structured traces.
|
|
|
|
@1612
|
9 years |
sacerdot |
All library ported to new Matita lib (finally).
|
|
|
|
@1601
|
9 years |
sacerdot |
Files ported to new version of the standard library.
|
|
|
|
@1596
|
9 years |
campbell |
RTLabs structured traces: sort out passing of termination proofs around.
|
|
|
|
@1595
|
9 years |
campbell |
We don't need an explicit termination count when building traces.
|
|
|
|
@1594
|
9 years |
campbell |
Rework handling of termination information in RTLabs structured traces …
|
|
|
|
@1586
|
9 years |
campbell |
RTLabs structured traces: cost labels after jumps.
|
|
|
|
@1583
|
9 years |
campbell |
More on RTLabs structured traces.
Fixed mistake in structure trace …
|
|
|
|
@1574
|
9 years |
campbell |
A little more progress on traces on RTLabs.
|
|
|
|
@1565
|
9 years |
campbell |
Note that RTLabs ought to classify branches as "jumps" (in the …
|
|
|
|
@1563
|
9 years |
campbell |
A little progress on constructing RTLabs structured traces.
|
|
|
|
@1559
|
9 years |
campbell |
Add a notion of flat traces with evidence for RTLabs.
|
|
|
|
@1552
|
9 years |
campbell |
Update RTLabs structured trace definition.
|
|
|
|
@1537
|
9 years |
campbell |
A preliminary definition of the abstract status record for RTLabs.
|
|
|
|
@1535
|
9 years |
campbell |
Make RTLabs semantics use knowledge that the next instruction always …
|
|
|
|
@1529
|
9 years |
campbell |
Update RTLabs to RTL with unary operation types.
|
|
|
|
@1521
|
9 years |
sacerdot |
Syntax change in Matita: change what where => change where what.
|
|
|
|
@1515
|
9 years |
campbell |
Add type of maps on positive binary numbers, and use them for …
|
|
|
|
@1408
|
9 years |
sacerdot |
1. Added joint/BEGlobalenvs that is a modification of …
|
|
|
|
@1369
|
9 years |
campbell |
Put type information into front-end unary ops.
Slight change to …
|
|
|
|
@1358
|
9 years |
mulligan |
got rtlabs to rtl compiling, foldi_strong needs examining
|
|
|
|
@1356
|
9 years |
mulligan |
deleted redundant directory. added outlines for both reports, and …
|
|
|
|
@1354
|
9 years |
sacerdot |
One axiom closed.
|
|
|
|
@1352
|
9 years |
sacerdot |
This commit is made necessary by the last Matita change.
Inclusion is …
|
|
|
|
@1343
|
9 years |
mulligan |
fixed some bugs in the translation
|
|
|
|
@1331
|
9 years |
mulligan |
some changes, but i now have two contradictory proof obligations.
|
|
|
|
@1325
|
9 years |
mulligan |
finished implementing the translate constant function
|
|
|
|
@1316
|
9 years |
campbell |
Merge in id-lookup-branch to trunk.
|
|
|
|
@1315
|
9 years |
mulligan |
another move for the same reason. got rtlabs > rtl compiling again by …
|
|
|
|
@1314
|
9 years |
mulligan |
name changes so that bash tab completion actually works with some …
|
|
|
|
@1308
|
9 years |
mulligan |
changes to translate_cst
|
|
|
|
@1307
|
9 years |
mulligan |
adding translate_cst
|
|
|
|
@1306
|
9 years |
mulligan |
small changes to rtlabs. what axioms remain look hard to close. need …
|
|
|
|
@1296
|
9 years |
mulligan |
changes
|
|
|
|
@1293
|
9 years |
mulligan |
finished rtl abs to rtl transformation subject to closing some axioms …
|
|
|
|
@1292
|
9 years |
mulligan |
more added to rtlabs translation
|
|
|
|
@1290
|
9 years |
sacerdot |
One more function ported to new Joint.
|
|
|
|
@1288
|
9 years |
mulligan |
more added to rtlabs to rtl pass
|
|
|
|
@1287
|
9 years |
mulligan |
about 3/4 of the way through rtlabs to rtl now
|
|
|
|
@1286
|
9 years |
mulligan |
more changes to the rtl abs to rtl pass
|
|
|
|
@1285
|
9 years |
mulligan |
more implementation on maps, final push to get rtl abs to rtl working
|
|
|
|
@1283
|
9 years |
sacerdot |
Bad programming practice removed: change_label is no longer required …
|
|
|
|
@1282
|
9 years |
sacerdot |
Cosmetic change: names of joint statements/instructions shortened and …
|
|
|
|
@1281
|
9 years |
sacerdot |
Porting of all transformation to the joint syntax practically …
|
|
|
|
@1280
|
9 years |
sacerdot |
Some progress in the porting of RTLAbstoRTL to the joint syntax:
1) …
|
|
|
|
@1239
|
9 years |
sacerdot |
RTLAbstoRTL ported to new datatypes.
Note: RTL syntax/semantics is …
|
|
|
|
@1238
|
9 years |
campbell |
Update Cminor and RTLabs to fit SmallstepExec? changes.
|
|
|
|
@1226
|
9 years |
campbell |
Adjust pretty printers for change in program records, try a test of each.
|
|
|
|
@1224
|
9 years |
sacerdot |
Type of programs in common/AST made more dependent.
In particular, the …
|
|
|
|
@1157
|
10 years |
campbell |
Update pretty printers and examples.
|
|
|
|
@1149
|
10 years |
mulligan |
changes to get everything type checking again after changing names of …
|
|
|
|
@1147
|
10 years |
campbell |
Remove some obsolete commented out code, update a couple of comments.
|
|
|
|
@1139
|
10 years |
campbell |
Shift init_data out of generic program record so that it only appears …
|
|
|
|
@1138
|
10 years |
mulligan |
merged ertl_st_opaccs_a and ertl_st_opaccs_b into each other
|
|
|
|
@1123
|
10 years |
sacerdot |
Added comment about missing alignment of data in memory.
|
|
|
|
@1116
|
10 years |
sacerdot |
Some comments.
|
|
|
|
@1077
|
10 years |
mulligan |
ack, dependent types are scary
|
|
|
|
@1073
|
10 years |
mulligan |
more changes from today
|
|
|
|
