

@3081

7 years 
campbell 
Tidy up recent work a little.



@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 checkin 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

8 years 
campbell 
A general result about simulations of executions.



@2202

8 years 
campbell 
Start defining equivalent executions.



@2145

8 years 
campbell 
Cost labelling doesn't affect interaction.



@2118

8 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 backends
…



@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 smallstep 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.
