|
|
|
@2398
|
8 years |
boender |
- committed start of stacksize
|
|
|
|
@2299
|
8 years |
campbell |
Soundly labelled RTLabs structured traces are "unrepeating".
|
|
|
|
@2186
|
9 years |
tranquil |
updated joint semantics
|
|
|
|
@2129
|
9 years |
mulligan |
Large changes from today trying to complete the main theorem. Again :(
|
|
|
|
@2044
|
9 years |
campbell |
PCs for RTLabs structured traces.
|
|
|
|
@1976
|
9 years |
tranquil |
* monads: just changed some defs, which had to be propagated in some …
|
|
|
|
@1964
|
9 years |
tranquil |
introduced as_label_of_cost and adapted accordingly. Equality of cost …
|
|
|
|
@1949
|
9 years |
tranquil |
* lemma trace rel to eq flatten trace
* some more properties of …
|
|
|
|
@1944
|
9 years |
sacerdot |
common/StructuredTraces no longer depends on ASM/AbstractStatus (again)
|
|
|
|
@1939
|
9 years |
mulligan |
Changes to get things to compile and to avoid the dependency …
|
|
|
|
@1938
|
9 years |
sacerdot |
Definitions moved to the right places, now everything compiles again.
|
|
|
|
@1935
|
9 years |
mulligan |
Generalized some lemma in ASM/CostsProof.ma to work on abstract …
|
|
|
|
@1927
|
9 years |
mulligan |
Reduced complexity of good_program predicate, ported to new notion of …
|
|
|
|
@1926
|
9 years |
tranquil |
* added as_label to abstract status, with as_costed defined with it. …
|
|
|
|
@1921
|
9 years |
mulligan |
Horror proof mostly finished (compiles all way until end of CostsProof?.ma).
|
|
|
|
@1918
|
9 years |
tranquil |
using listb.ma now
|
|
|
|
@1917
|
9 years |
tranquil |
predicate for unrepeating traces, fused final_abstract_status with …
|
|
|
|
@1902
|
9 years |
mulligan |
Reverted needless changes to StructuredTraces?
|
|
|
|
@1901
|
9 years |
mulligan |
Slight changes to StructuredTraces?: should not change too much
|
|
|
|
@1880
|
9 years |
campbell |
Show that RTLabs flat traces are determined by their starting state, …
|
|
|
|
@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 …
|
|
|
|
@1783
|
9 years |
campbell |
Remove junk from non-terminating structured traces.
|
|
|
|
@1709
|
9 years |
mulligan |
Changes to the execution of the MOVC instruction
|
|
|
|
@1658
|
9 years |
mulligan |
asm costs changes from today
|
|
|
|
@1654
|
9 years |
campbell |
Corrections to structured trace definitions (see the mailing list). …
|
|
|
|
@1652
|
9 years |
campbell |
Forgot to apply 1583 to non-terminating case.
|
|
|
|
@1601
|
9 years |
sacerdot |
Files ported to new version of the standard library.
|
|
|
|
@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.
|
|
|
|
@1544
|
9 years |
sacerdot |
StructuredTraces? inhabited for object code.
|
|
|
|
@1536
|
9 years |
campbell |
Use predicates throughout the structured traces.
|
|
|
|
@1532
|
9 years |
campbell |
Remove jump classification from structured traces.
|
|
|
|
@1531
|
9 years |
campbell |
A notion of abstract structured traces.
|
