

@3237

7 years 
campbell 
Some incomplete work on Clight > Cminor call steps.



@3178

7 years 
campbell 
Some progress on Callstate steps in Clight to Cminor.
Note that some …



@3170

7 years 
mckinna 
removed redundant dependencies



@3165

7 years 
campbell 
A little bit of progress on Callstate case.



@3155

7 years 
campbell 
Now have proof that the initial states are in simulation for clight to …



@3055

7 years 
campbell 
Start getting partial Clight to Cminor proof in shape for …



@3054

7 years 
campbell 
Put missing typ check in; adjust proof because I did it a little …



@3036

7 years 
garnier 
Fixing some problems, progress, etc



@2857

7 years 
garnier 
CL to CM: some invariants strengthened.



@2850

7 years 
garnier 
Progress on CL to CM. Some more cases closed modulo some critical …



@2838

7 years 
garnier 
Closing some more cases



@2825

7 years 
garnier 
Progress, Clight to Cminor



@2822

7 years 
garnier 
A consitent proof state for Clight to Cminor, with some progress (and …



@2737

7 years 
garnier 
Commit of current proof state for Clight to Cminor translation.



@2667

7 years 
garnier 
Clight to Cminor, statements: some cases down. Subset of the …



@2601

7 years 
sacerdot 
Extraction to ocaml is now working, with a couple of bugs left.
One …



@2598

7 years 
garnier 
Tentative, partial draft for the definition of ClightCminor …



@2597

7 years 
campbell 
Some work in progress on measurable subtrace preservation.



@2591

7 years 
garnier 
Moved simulation proof for expressions in toCminorCorrectnessExpr.ma, …



@2588

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



@2582

7 years 
garnier 
Some progress on CL to CM.



@2578

7 years 
garnier 
Progress on CL to CM, fixed some stuff in memory injections.



@2572

7 years 
garnier 
Progress on toCminorCorrectness.



@2569

7 years 
campbell 
Fix Clight semantics for ptr + char. (Compiler works anyway.)



@2568

7 years 
campbell 
Relax some Clight type checks to Cminor type checks to avoid …



@2565

7 years 
garnier 
Cl to Cm progress.



@2554

7 years 
garnier 
Proof of expression translation correctness "mostly" done for CL to …



@2545

7 years 
garnier 
Comitting current progress of CL to CM



@2527

7 years 
garnier 
Progress on CL to CM.



@2510

7 years 
garnier 
Some progress on the Cl > Cm front



@2500

7 years 
garnier 
Continuing work on simulation in Clight/Cminor?



@2496

7 years 
garnier 
Some tentative work on the simulation proof for expressions, in order …



@2489

7 years 
campbell 
Conjecture some Clight/Cminor? simulation results.



@2471

7 years 
campbell 
Tame global environments a little.



@2466

7 years 
campbell 
Show how global environments in clight to cminor pass match up.



@2460

7 years 
campbell 
Rest of variable characterisation.



@2458

7 years 
campbell 
Clight to Cminor allocates stack variables to disjoint regions within …
