

@2118

7 years 
campbell 
Labelling preserves behaviour.



@2117

7 years 
campbell 
Workaround for bug in Matita.



@2111

7 years 
sacerdot 
Cleanup: lemmas/theorems/axioms moved to the right places.



@2107

7 years 
campbell 
Memory initialisation and program transformations.



@2105

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



@2104

7 years 
campbell 
Fill in misc axiom.



@2103

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



@2044

7 years 
campbell 
PCs for RTLabs structured traces.



@2032

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



@2010

7 years 
campbell 
Make globalenvs use proper maps.



@1999

7 years 
campbell 
Make backend use the main global envs.



@1994

7 years 
campbell 
Remove redundant allocation definition in Globalenvs.



@1993

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



@1988

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



@1987

7 years 
campbell 
Move BEValues to common to reflect their use in the memory model for …



@1986

7 years 
campbell 
Get rid of unused abstraction of Globalenvs.



@1976

7 years 
tranquil 
* monads: just changed some defs, which had to be propagated in some …



@1964

7 years 
tranquil 
introduced as_label_of_cost and adapted accordingly. Equality of cost …



@1954

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



@1949

7 years 
tranquil 
* lemma trace rel to eq flatten trace
* some more properties of …



@1944

7 years 
sacerdot 
common/StructuredTraces no longer depends on ASM/AbstractStatus (again)



@1939

7 years 
mulligan 
Changes to get things to compile and to avoid the dependency …



@1938

7 years 
sacerdot 
Definitions moved to the right places, now everything compiles again.



@1935

7 years 
mulligan 
Generalized some lemma in ASM/CostsProof.ma to work on abstract …



@1930

7 years 
campbell 
Tidy up labelling simulation stuff a bit.



@1928

7 years 
mulligan 
Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should …



@1927

7 years 
mulligan 
Reduced complexity of good_program predicate, ported to new notion of …



@1926

7 years 
tranquil 
* added as_label to abstract status, with as_costed defined with it. …



@1921

7 years 
mulligan 
Horror proof mostly finished (compiles all way until end of CostsProof?.ma).



@1920

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



@1918

7 years 
tranquil 
using listb.ma now



@1917

7 years 
tranquil 
predicate for unrepeating traces, fused final_abstract_status with …



@1908

7 years 
fguidi 
notation fixup following last commit of matita
we shifted the levels …



@1902

7 years 
mulligan 
Reverted needless changes to StructuredTraces?



@1901

7 years 
mulligan 
Slight changes to StructuredTraces?: should not change too much



@1882

7 years 
tranquil 
big update, alas incomplete:
joint changed a bit, and all BE languages …



@1881

7 years 
campbell 
Resurrect version of exec_up_to which shows the final state.



@1880

7 years 
campbell 
Show that RTLabs flat traces are determined by their starting state, …



@1878

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



@1876

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



@1874

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



@1873

7 years 
campbell 
Fix up earlier frontend value conversion work.



@1872

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



@1812

8 years 
campbell 
Provide a combined type for terminating and nonterminating structured …



@1808

8 years 
campbell 
Create a Prop version of the nonterminating structured traces so that …



@1806

8 years 
campbell 
Show that we could construct RTLabs nonterminating structured traces …



@1783

8 years 
campbell 
Remove junk from nonterminating structured traces.



@1709

8 years 
mulligan 
Changes to the execution of the MOVC instruction



@1658

8 years 
mulligan 
asm costs changes from today



@1654

8 years 
campbell 
Corrections to structured trace definitions (see the mailing list). …



@1652

8 years 
campbell 
Forgot to apply 1583 to nonterminating case.



@1647

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



@1640

8 years 
tranquil 
* finished fork of semantics.ma
* unification of Errors under the …



@1635

8 years 
tranquil 
* lists with binders and monads
* Joint.ma and other temprarily …



@1631

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



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



@1609

8 years 
boender 
 added alias to ASM/BitVectorTrie
 removed double include from …



@1608

8 years 
sacerdot 
Porting to new library still in progress.



@1601

8 years 
sacerdot 
Files ported to new version of the standard library.



@1599

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



@1598

8 years 
mulligan 
changes over the last couple of days



@1583

8 years 
campbell 
More on RTLabs structured traces.
Fixed mistake in structure trace …



@1574

8 years 
campbell 
A little more progress on traces on RTLabs.



@1566

8 years 
campbell 
Pacify changes to destruct tactic.



@1562

8 years 
mulligan 
new version of assembly, fixed conflict in positivemap.ma, changed …



@1555

8 years 
boender 
 changes to assembly
 added lookup to PositiveMap?
 lightly changed …



@1551

8 years 
campbell 
Functions to translate between backend and frontend values.



@1545

8 years 
campbell 
Use pointer record in frontend.



@1544

8 years 
sacerdot 
StructuredTraces? inhabited for object code.



@1536

8 years 
campbell 
Use predicates throughout the structured traces.



@1535

8 years 
campbell 
Make RTLabs semantics use knowledge that the next instruction always …



@1532

8 years 
campbell 
Remove jump classification from structured traces.



@1531

8 years 
campbell 
A notion of abstract structured traces.



@1523

8 years 
campbell 
Separate out positive and Z definitions from extralib.ma.
Minor syntax …



@1516

8 years 
sacerdot 
Ported to syntax of Matita 0.99.1.



@1515

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



@1512

8 years 
campbell 
Shorten proof of goal that solves now.



@1510

8 years 
sacerdot 
All files ported to new dependent inversion.



@1480

8 years 
sacerdot 
Proof changed (to use new automation).
BUG FOUND: automation fails if …



@1465

8 years 
sacerdot 
Dead code removed.



@1410

8 years 
campbell 
Remove a few old workarounds.



@1401

8 years 
ricciott 
Changes concerning the new behavior of destruct.



@1395

8 years 
sacerdot 
1) New versions of pointer_of_beval/beval_of_pointer with a stricter …



@1369

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



@1368

8 years 
sacerdot 
A bug in the clear tactic makes the previous (correct) commit wrong. …



@1367

8 years 
sacerdot 
Proof improvement, still somehow a bit slow.



@1355

8 years 
sacerdot 
monadic fold_lefti added



@1353

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



@1351

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



@1350

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



@1347

8 years 
campbell 
Remove obsolete definitions.



@1339

8 years 
sacerdot 
Automation is now stronger.



@1316

8 years 
campbell 
Merge in idlookupbranch to trunk.



@1268

8 years 
sacerdot 
1) AST/Identifier.ma no longer used, utilities/IdentifierTools no …



@1253

8 years 
mulligan 
uses.ma finished



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



@1225

8 years 
campbell 
Missing ; in proof



@1224

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


