|
|
|
@2685
|
7 years |
campbell |
Progress on measurable trace preservation: prefix preserves observable …
|
|
|
|
@2682
|
7 years |
campbell |
Don't apply inv in after_n_steps to last state.
|
|
|
|
@2669
|
7 years |
campbell |
Tweak exec_steps output; show that simulations extend to measurable …
|
|
|
|
@2668
|
7 years |
campbell |
Intermediate measurable proof check-in before I change its traces again.
|
|
|
|
@2618
|
7 years |
campbell |
Tidy up measurable a little.
|
|
|
|
@2487
|
7 years |
campbell |
Set up "after_n_steps" to enforce an invariant on states.
|
|
|
|
@2459
|
7 years |
campbell |
Syntax update
|
|
|
|
@2444
|
7 years |
campbell |
Some inversion lemmas for after_n_steps for dealing with >1 source …
|
|
|
|
@2338
|
7 years |
campbell |
Use much nicer definition for making several steps in the labelling …
|
|
|
|
@2203
|
7 years |
campbell |
A general result about simulations of executions.
|
|
|
|
@2202
|
7 years |
campbell |
Start defining equivalent executions.
|
|
|
|
@2145
|
7 years |
campbell |
Cost labelling doesn't affect interaction.
|
|
|
|
@2118
|
7 years |
campbell |
Labelling preserves behaviour.
|
|
|
|
@1599
|
8 years |
sacerdot |
Start of merging of stuff into the standard library of Matita.
|
|
|
|
@1233
|
8 years |
sacerdot |
1) Ported to Brian's new dependent type for fullexec
2) Universe level …
|
|
|
|
@1231
|
8 years |
campbell |
Change SmallstepExec? so that states can depend on global information. …
|
|
|
|
@1213
|
8 years |
sacerdot |
1) New values (joint/BEValues.ma) and memory model for the back-ends
…
|
|
|
|
@1181
|
8 years |
mulligan |
changed smallstep exec in order to remove matita bug (superposition.ml …
|
|
|
|
@797
|
9 years |
campbell |
Add error messages wherever the error monad is used.
Sticks to …
|
|
|
|
@751
|
9 years |
campbell |
Initial version of the Cminor syntax and semantics.
|
|
|
|
@731
|
9 years |
campbell |
Common definition for animation semantics, and factor out IO definitions.
|
|
|
|
@702
|
9 years |
campbell |
Refine small-step executable semantics abstraction a little.
Some …
|
|
|
|
@700
|
9 years |
campbell |
Get Clight semantics going again (except for problems CexecEquiv? that …
|
|
|
|
@695
|
9 years |
campbell |
Rearrange Clight files a bit - will try to make them work again soon…
|
|
copied from src/Clight/SmallstepExec.ma:
|
|
|
|
@694
|
9 years |
campbell |
Start moving Clight into common directory.
|
