

@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

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



@1647

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



@1634

9 years 
campbell 
Update memory model examples syntax.



@1633

9 years 
campbell 
Update Cminor pretty printer and examples.



@1631

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



@1630

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



@1629

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



@1628

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



@1627

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



@1626

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



@1618

9 years 
campbell 
Minor updates due to recent changes.



@1612

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



@1608

9 years 
sacerdot 
Porting to new library still in progress.



@1605

9 years 
sacerdot 
Porting to last standard library of Matita.



@1603

9 years 
sacerdot 
More proofs ported to new lib.



@1599

9 years 
sacerdot 
Start of merging of stuff into the standard library of Matita.



@1566

9 years 
campbell 
Pacify changes to destruct tactic.



@1545

9 years 
campbell 
Use pointer record in frontend.



@1521

9 years 
sacerdot 
Syntax change in Matita: change what where => change where what.



@1516

9 years 
sacerdot 
Ported to syntax of Matita 0.99.1.



@1515

9 years 
campbell 
Add type of maps on positive binary numbers, and use them for …



@1513

9 years 
campbell 
Fix up Clight examples.



@1510

9 years 
sacerdot 
All files ported to new dependent inversion.



@1489

9 years 
campbell 
Fix up a couple of lemmas affected by the change to add_with_carries.



@1410

9 years 
campbell 
Remove a few old workarounds.



@1401

9 years 
ricciott 
Changes concerning the new behavior of destruct.



@1369

9 years 
campbell 
Put type information into frontend unary ops.
Slight change to …



@1352

9 years 
sacerdot 
This commit is made necessary by the last Matita change.
Inclusion is …



@1351

9 years 
campbell 
Tidy up some loose ends from the invariants branch merge.



@1350

9 years 
sacerdot 
Porting to latest destruct tactic.
Note: the tactics has a few …



@1344

9 years 
sacerdot 
Ported to new destruct.



@1342

9 years 
sacerdot 
The new auto is much more powerful.



@1336

9 years 
sacerdot 
Ported to new Matita destruct/inversion.
One lemma fails at qed. …



@1332

9 years 
campbell 
Summation example updated (needs computational K).



@1316

9 years 
campbell 
Merge in idlookupbranch to trunk.



@1276

9 years 
campbell 
Support for replacing operations with runtime support functions in …



@1244

9 years 
campbell 
Sort out Clight semantics equivalence proof for new SmallstepExec?.



@1238

9 years 
campbell 
Update Cminor and RTLabs to fit SmallstepExec? changes.



@1231

9 years 
campbell 
Change SmallstepExec? so that states can depend on global information. …



@1226

9 years 
campbell 
Adjust pretty printers for change in program records, try a test of each.



@1224

9 years 
sacerdot 
Type of programs in common/AST made more dependent.
In particular, the …



@1216

9 years 
campbell 
Update Clight semantics equivalence proof to match changes in …



@1207

9 years 
campbell 
Second part of fixing temporaries in Clight to Cminor stage.



@1206

9 years 
campbell 
First stage of fixing temporary generation in Clight/toCminor.ma.



@1198

9 years 
campbell 
Clight cast removal (NB: quite different from the prototype).



@1194

9 years 
campbell 
Remove old, commented out code.



@1157

9 years 
campbell 
Update pretty printers and examples.



@1147

9 years 
campbell 
Remove some obsolete commented out code, update a couple of comments.



@1139

9 years 
campbell 
Shift init_data out of generic program record so that it only appears …



@1078

9 years 
campbell 
Implement stack allocation for parameters whose address is taken.



@1058

9 years 
campbell 
Evict CompCert? Maps interface in favour of BitVectorTries?.



@1056

9 years 
campbell 
Switch to delayed identifier error scheme.



@978

9 years 
campbell 
Update remaining Clight examples.



@965

9 years 
campbell 
Update some Clight examples.



@964

9 years 
campbell 
Rest of cast fix.



@962

9 years 
campbell 
Casts should use source type's signedness, not the target's.



@961

9 years 
campbell 
Use precise bitvector sizes throughout the front end, rather than …



@891

9 years 
campbell 
Revise proofs affected by recent matita change.



@886

9 years 
campbell 
Put types into parameter and variable lists in Cminor.
Temporarily …



@882

9 years 
campbell 
Fix up fragile proofs for current version of matita.



@881

9 years 
campbell 
Sort out regions in Cminor to fix Clight to Cminor translation of Ederef.



@880

9 years 
campbell 
Add type information into Cminor.
As a result, the Clight to Cminor …



@879

9 years 
campbell 
Refine "AST" types to include size/signedness information.



@824

9 years 
campbell 
Some work on showing that casts around integer operations can be removed.



@816

9 years 
campbell 
Clight to Cminor compilation, modulo switch statements, temporary …



@798

9 years 
campbell 
Fix usual matita tactic mistake.



@797

9 years 
campbell 
Add error messages wherever the error monad is used.
Sticks to …



@786

9 years 
campbell 
A version of the clight matita term printer for the current prototype.



@781

9 years 
campbell 
Implement labelling pass for Clight.


