

@3030

8 years 
campbell 
Break up frontend for correctness proof.
Use let rec to prevent …



@2722

8 years 
campbell 
It's easier to keep the real function identifier in frontend …



@2682

8 years 
campbell 
Don't apply inv in after_n_steps to last state.



@2677

8 years 
campbell 
Retain the pointer for the function called in frontend call states
so …



@2588

8 years 
garnier 
modified Cexec/Csem? semantics:
. force andbool and orbool types to be …



@2574

8 years 
campbell 
Update labelling simulation proofs due to some changes elsewhere.



@2487

8 years 
campbell 
Set up "after_n_steps" to enforce an invariant on states.



@2468

8 years 
garnier 
Floats are gone from the frontend. Some trace amount might remain in …



@2428

8 years 
campbell 
Tighten requirements on switch statements in Clight to only give …



@2392

8 years 
campbell 
Labelling translations of && and  need a lot of cost labelling to …



@2391

8 years 
campbell 
Revert "Put the postloop cost label into the Clight while statement …



@2353

8 years 
campbell 
Put the postloop cost label into the Clight while statement to get …



@2338

8 years 
campbell 
Use much nicer definition for making several steps in the labelling …



@2319

8 years 
campbell 
Generate perprogram cost labels rather than perfunction ones, and …



@2203

9 years 
campbell 
A general result about simulations of executions.



@2202

9 years 
campbell 
Start defining equivalent executions.



@2176

9 years 
campbell 
Remove memory spaces other than XData and Code; simplify pointers as a …



@2145

9 years 
campbell 
Cost labelling doesn't affect interaction.



@2134

9 years 
campbell 
Split out behavioural equivalence spec for labelling.



@2118

9 years 
campbell 
Labelling preserves behaviour.



@2107

9 years 
campbell 
Memory initialisation and program transformations.



@2105

9 years 
campbell 
Show some results about globalenvs and program transformations.



@2103

9 years 
campbell 
Make transform_*program take a more general transformation to make …



@2050

9 years 
campbell 
Limit some normalization that doesn't seem to like.



@2019

9 years 
campbell 
Split out special induction principle for Clight from soundness file. …



@2011

9 years 
garnier 
Minor cleanup.



@2000

9 years 
campbell 
Fix g.e. glitch in label simulation.



@1986

9 years 
campbell 
Get rid of unused abstraction of Globalenvs.



@1954

9 years 
campbell 
Initial state is in the labelling simulation
(modulo global envs results).



@1930

9 years 
campbell 
Tidy up labelling simulation stuff a bit.



@1922

9 years 
campbell 
Main labelling simulation proof complete.



@1920

9 years 
campbell 
Most of the labelling simulation. Still need to sort out switch …



@1893

9 years 
campbell 
Show stronger result about labelling of expressions.



@1888

9 years 
campbell 
Show that labelling of expressions works ...
after fixing it to match …
