

@2407

7 years 
campbell 
Sigh, continue in for loops was broken too.



@2399

7 years 
campbell 
Fill in some details about the statement of correctness.



@2395

7 years 
campbell 
Proper handling of comparison of pointers offtheend of an object.
We …



@2393

7 years 
campbell 
A pointer comparison test case that illustrates a bug.



@2392

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



@2391

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



@2389

8 years 
campbell 
Fix dowhile statements, and carefully arrange the translation so that …



@2388

8 years 
campbell 
Example of each type of control flow statement, plus minor fix to …



@2387

8 years 
garnier 
Revamped memory extensions, proved stuff on freeing blocks and on …



@2386

8 years 
garnier 
Implementation of constructive finite sets based on lists. Various …



@2385

8 years 
campbell 
Minor housekeeping.



@2384

8 years 
campbell 
Move Matita pretty printers into place.



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



@2332

8 years 
garnier 
Some progress on switch removal. Small fix in the definition of free, …



@2328

8 years 
campbell 
Cut down the notion of a Clight labelled state to those where we pick …



@2326

8 years 
campbell 
More accurate notion of labelled states in Clight.



@2325

8 years 
campbell 
Fill out some Clight bits and pieces in correctness.ma.



@2319

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



@2312

8 years 
garnier 
Memory injections, to be revised



@2304

8 years 
garnier 
Strengthened proof of associativity of bitvector addition. Some more …



@2302

8 years 
garnier 
Finally proved associativity of addition on bitvectors. Rejoice.



@2298

8 years 
garnier 
WIP: converting switch removal from Z to bitvectors. Does not compile, …



@2271

8 years 
garnier 
Proof of correction for the semantics of expressions under memory …



@2263

8 years 
garnier 
Finished proving semantics preservation under memory injections for …



@2255

8 years 
garnier 
Had to modify the definition of memory injections to prove that …



@2253

8 years 
campbell 
Cminor to RTLabs is now a total function.



@2252

8 years 
campbell 
Use the return statement invariant. Restructure the invariants for …



@2251

8 years 
campbell 
Add new invariant to Cminor that return typs should be respected.



@2250

8 years 
campbell 
Tidy up Clight to Cminor pass a bit.



@2249

8 years 
campbell 
Tweak Cminor invariant to be slightly more readable/extendable.



@2234

8 years 
garnier 
Progress on proving semantics preservation under memory injections.



@2232

8 years 
campbell 
Remove unused block structure in Cminor.



@2231

8 years 
garnier 
Various tiny lemmas used in at least two files in the forntend.



@2227

8 years 
garnier 
* New version of the switch removal algorithm, described at the top of …



@2219

8 years 
campbell 
Speed up cast simplification proof checking a bit.



@2203

8 years 
campbell 
A general result about simulations of executions.



@2202

8 years 
campbell 
Start defining equivalent executions.



@2201

8 years 
campbell 
Forgotten comment update.



@2184

8 years 
campbell 
Minor fix ups.



@2180

8 years 
campbell 
Fix offbyone error in GenMem?.ma.



@2177

8 years 
campbell 
Tidy up multiplication.



@2176

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



@2145

8 years 
campbell 
Cost labelling doesn't affect interaction.



@2134

8 years 
campbell 
Split out behavioural equivalence spec for labelling.



@2120

8 years 
campbell 
Fix victim of alloc unfolding.



@2118

8 years 
campbell 
Labelling preserves behaviour.



@2107

8 years 
campbell 
Memory initialisation and program transformations.



@2106

8 years 
campbell 
Fix up a couple of proofs broken by recent changes.



@2105

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



@2103

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



@2076

8 years 
garnier 
First steps towards a simulation proof for switch removal.



@2074

8 years 
garnier 
Prophylactic renaming of a relation



@2050

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



@2032

8 years 
sacerdot 
!! BEWARE: major commit !!
1) [affects everybody]
split for …



@2030

8 years 
garnier 
Cast simplification was too conservative, now reasonably aggressive.



@2019

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



@2016

8 years 
garnier 
Slight change in simplification strategy to better match the semantics



@2011

8 years 
garnier 
Minor cleanup.



@2009

8 years 
garnier 
Proof of simulation completed for singestep executions.



@2000

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



@1993

8 years 
campbell 
Make frontend memory model only depend on the general definitions by …



@1991

8 years 
campbell 
Put the front end transformations together and make an example use it.



@1988

8 years 
campbell 
Abstraction of the memory contents in the memory models is no longer …



@1986

8 years 
campbell 
Get rid of unused abstraction of Globalenvs.



@1974

8 years 
garnier 
Progress on the cast simplification proof.



@1970

8 years 
garnier 
Workinprogress: correction proof for the cast removal on expressions.



@1954

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



@1930

8 years 
campbell 
Tidy up labelling simulation stuff a bit.



@1922

8 years 
campbell 
Main labelling simulation proof complete.



@1920

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



@1915

8 years 
garnier 
Correction of a typo in switchRemoval.



@1914

8 years 
campbell 
Fix bug in Clight semantics that misses gotolabels inside a cost …



@1893

8 years 
campbell 
Show stronger result about labelling of expressions.



@1888

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



@1884

8 years 
campbell 
Syntax changes to fit Paolo's commit.



@1883

8 years 
campbell 
Ilias' switch removal code, plus a test.



@1878

8 years 
campbell 
Enforce typing of constants in frontend, plus binops for RTLabs.



@1876

8 years 
campbell 
Update Cexec soundness proof.
Change finishes_with predicate to …



@1875

8 years 
campbell 
Update brief memory model test.



@1874

8 years 
campbell 
First cut at using backend memory model throughout.
Note the …



@1873

8 years 
campbell 
Fix up earlier frontend value conversion work.



@1872

8 years 
campbell 
Make binary operations in Cminor/RTLabs properly typed.
A few extra …



@1871

8 years 
campbell 
Change Clight to Cminor compilation to use gotos rather than loops, …



@1713

8 years 
campbell 
Add a distinguished final state to the frontend languages to match up …



@1672

8 years 
campbell 
Matita now generates a couple of inversion lemmas that were manually …



@1647

8 years 
tranquil 
* corrected some notation problems
* adapted Cligth with slight …



@1634

8 years 
campbell 
Update memory model examples syntax.



@1633

8 years 
campbell 
Update Cminor pretty printer and examples.



@1631

8 years 
campbell 
Use fact that type environments in Cminor have distinct variables to …



@1630

8 years 
campbell 
Remainder of freshness in Clight to Cminor pass.



@1629

8 years 
campbell 
Sort out most of the fresh names stuff in Clight to Cminor.



@1628

8 years 
campbell 
Show that the universe generated by Clight/fresh.ma is good.



@1627

8 years 
campbell 
Add some notions of freshness, and start using them for temporary …



@1626

8 years 
campbell 
Add extra type safety in front end. NB: critical freshness parts …



@1618

8 years 
campbell 
Minor updates due to recent changes.



@1612

8 years 
sacerdot 
All library ported to new Matita lib (finally).



@1608

8 years 
sacerdot 
Porting to new library still in progress.



@1605

8 years 
sacerdot 
Porting to last standard library of Matita.



@1603

8 years 
sacerdot 
More proofs ported to new lib.


