

@2436

9 years 
tranquil 
small changes



@2435

9 years 
tranquil 
new back end operations



@2432

9 years 
campbell 
Remove offtheend pointers from front end ops.



@2429

9 years 
garnier 
Restrict semantics of pointer comparison to what CompCert? does  i.e. …



@2428

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



@2426

9 years 
boender 
 updated stacksize to reflect new developments, completed proof
 …



@2423

9 years 
tranquil 
as_classifier predicate → as_classify function
as_call predicate from …



@2421

9 years 
tranquil 
added simulation of flat prefix, and comments to explain the code



@2420

9 years 
campbell 
Tidy away generic results about folds on positive/identifier maps.



@2418

9 years 
campbell 
Add a checking function for the uniqueness of cost labels in RTLabs …



@2417

9 years 
boender 
 reverted changes to StructuredTraces? (shouldn't have been committed …



@2415

9 years 
campbell 
Add the ability to map blocks to symbols in preparation for stack space.



@2413

9 years 
tranquil 
* tal_rel corrected to include cases where tal_base_call \approx …



@2398

9 years 
boender 
 committed start of stacksize



@2395

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



@2338

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



@2335

9 years 
campbell 
Deal with goto labels in RTLabs to Cminor by fixing up goto statements …



@2332

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



@2319

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



@2314

9 years 
campbell 
Move generic definitions from recent commit to appropriate places.



@2307

9 years 
campbell 
Half the proofs for sound cost labelling check.



@2305

9 years 
campbell 
RTLabs cost spec checking function implemented (lacks proof, or much …



@2303

9 years 
campbell 
Some preliminary checking of cost labelling properties in RTLabs.



@2299

9 years 
campbell 
Soundly labelled RTLabs structured traces are "unrepeating".



@2296

9 years 
campbell 
Tidy up some illplaced definitions.



@2286

9 years 
tranquil 
Big update!
* merge of all _paolo variants
* reorganised some depends …



@2277

9 years 
tranquil 
* replaced incorrect use of subvector_with



@2275

9 years 
tranquil 
* moved around some code (I8051.ma does not depend on ByteValues?.ma …



@2226

9 years 
campbell 
Whole program proof.



@2222

9 years 
sacerdot 
More robust to possible future changes to the "in match" semantics …



@2218

9 years 
campbell 
Separate out cost properties required of RTLabs programs from the …



@2206

9 years 
campbell 
Add note about cost maps to simulation definition.



@2203

9 years 
campbell 
A general result about simulations of executions.



@2202

9 years 
campbell 
Start defining equivalent executions.



@2186

9 years 
tranquil 
updated joint semantics



@2185

9 years 
campbell 
Use bitvectors for offsets.



@2182

9 years 
tranquil 
updated linearisation pass



@2180

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



@2177

9 years 
campbell 
Tidy up multiplication.



@2176

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



@2155

9 years 
tranquil 
updates to blocks and RTLabs to RTL translation (which sidesteps …



@2145

9 years 
campbell 
Cost labelling doesn't affect interaction.



@2133

9 years 
boender 
 moved does_not_occur_occur_absurd



@2129

9 years 
mulligan 
Large changes from today trying to complete the main theorem. Again :(



@2118

9 years 
campbell 
Labelling preserves behaviour.



@2117

9 years 
campbell 
Workaround for bug in Matita.



@2111

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



@2107

9 years 
campbell 
Memory initialisation and program transformations.



@2105

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



@2104

9 years 
campbell 
Fill in misc axiom.



@2103

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



@2044

9 years 
campbell 
PCs for RTLabs structured traces.



@2032

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



@2010

9 years 
campbell 
Make globalenvs use proper maps.



@1999

9 years 
campbell 
Make backend use the main global envs.



@1994

9 years 
campbell 
Remove redundant allocation definition in Globalenvs.



@1993

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



@1988

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



@1987

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



@1986

9 years 
campbell 
Get rid of unused abstraction of Globalenvs.



@1976

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



@1964

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



@1954

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



@1949

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



@1944

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



@1939

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



@1938

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



@1935

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



@1930

9 years 
campbell 
Tidy up labelling simulation stuff a bit.



@1928

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



@1927

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



@1926

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



@1921

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



@1920

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



@1918

9 years 
tranquil 
using listb.ma now



@1917

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



@1908

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



@1902

9 years 
mulligan 
Reverted needless changes to StructuredTraces?



@1901

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



@1882

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



@1881

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



@1880

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



@1878

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



@1876

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



@1874

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



@1873

10 years 
campbell 
Fix up earlier frontend value conversion work.



@1872

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



@1812

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



@1808

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



@1806

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



@1783

10 years 
campbell 
Remove junk from nonterminating structured traces.



@1709

10 years 
mulligan 
Changes to the execution of the MOVC instruction



@1658

10 years 
mulligan 
asm costs changes from today



@1654

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



@1652

10 years 
campbell 
Forgot to apply 1583 to nonterminating case.



@1647

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



@1640

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



@1635

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



@1631

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



@1627

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


