

@2756

9 years 
sacerdot 
WARNING: this commit breaks things, sorry, Paolo is going to fix …



@2755

9 years 
tranquil 
* changed primitives of abstract status (with stuf that is probably …



@2751

9 years 
mckinna 
Added
 AssemblyTooLarge? : ErrorMessage?
to complete compiler.ma



@2727

9 years 
campbell 
Remove a couple of redundant hypotheses.



@2726

9 years 
campbell 
Show max stack preserved in FEMeasurable.



@2725

9 years 
campbell 
Add observables to FEMeasurable proof; fix silly typo.



@2724

9 years 
campbell 
Add RTLabs cost labelling checks to compiler.ma.



@2722

9 years 
campbell 
It's easier to keep the real function identifier in frontend …



@2720

9 years 
tranquil 
implemented back end ops that were still axioms



@2703

9 years 
mckinna 
now includes defn of costlabel_map



@2690

9 years 
campbell 
Most of the measurable subtrace preservation proof done.



@2685

9 years 
campbell 
Progress on measurable trace preservation: prefix preserves observable …



@2682

9 years 
campbell 
Don't apply inv in after_n_steps to last state.



@2678

9 years 
campbell 
Switch to single source step simulations for frontend measurable …



@2673

9 years 
tranquil 
corrected some compilation errors (that might depend on some matita update)



@2670

9 years 
campbell 
Clean up from recent commits.



@2669

9 years 
campbell 
Tweak exec_steps output; show that simulations extend to measurable …



@2668

9 years 
campbell 
Intermediate measurable proof checkin before I change its traces again.



@2646

9 years 
sacerdot 
A tag was classified as an error message. Fixed.



@2645

9 years 
sacerdot 
1. some broken backend files repaires, several still to go
2. the …



@2644

9 years 
campbell 
Commit some work on FEMeasurable before trying to do something nicer …



@2641

9 years 
piccolo 
defined dummy block code equals to 0



@2624

9 years 
campbell 
Properly evict unused and axiomatised Floats.



@2618

9 years 
campbell 
Tidy up measurable a little.



@2617

9 years 
campbell 
Trivial simplification on split_trace.



@2608

9 years 
garnier 
Regions are no more stored in blocks. block_region now tests the id, …



@2604

9 years 
piccolo 
ERTLtoERTLptr in place.



@2603

9 years 
piccolo 
Dead code commented out.



@2601

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



@2599

9 years 
tranquil 
* map_opt and map on positive maps are now clean (erase empty …



@2597

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



@2596

9 years 
campbell 
Use a simpler stack cost map, and then specialise to each semantics.



@2590

9 years 
piccolo 
added monad machineary for ERTL to ERTLptr translation
eval_seq_no_pc …



@2582

9 years 
garnier 
Some progress on CL to CM.



@2570

9 years 
piccolo 
ERTLtoERTLptr in place



@2569

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



@2553

9 years 
tranquil 
as_classify changed to a partial function
added a status for tailcalls



@2548

9 years 
tranquil 
in BackEndOps?, cleaner def of be_op2
new statement of …



@2541

9 years 
tranquil 
adapted size notation to last matita lib update (01/12/2012)
that …



@2540

9 years 
tranquil 
cl_jump case now provides a proof of costedness of the following state



@2539

9 years 
tranquil 
added cl_jump case to trace_any_any_free



@2534

9 years 
campbell 
Tweak measurable definition to stop at the return from a function.



@2533

9 years 
campbell 
Some fall out from removing floats.



@2531

9 years 
mckinna 
Trivial tweaks.



@2530

9 years 
tranquil 
temporary switch to cl_jump treated as cl_other
fixed script for new …



@2511

9 years 
campbell 
Conjecture main Cminor/RTLabs simulation results.
Add a few notes …



@2508

9 years 
mckinna 
more tweaks. compiler and correctness still build.



@2503

9 years 
mckinna 
tidied up, with new auxiliary defns, some refactoring, some code …



@2502

9 years 
campbell 
Sketch a little about how measurable traces might work with RTLabs and …



@2500

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



@2496

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



@2487

9 years 
campbell 
Set up "after_n_steps" to enforce an invariant on states.



@2486

9 years 
campbell 
First go at a generalised version of measurable.



@2478

9 years 
tranquil 
unified is_internal_function_of_program and is_internal_function



@2477

9 years 
tranquil 
status_simulation reformulated
definition of joint_classify split up …



@2476

9 years 
piccolo 
fixed commutation lemmas in lineariseProof
started proof of main …



@2474

9 years 
tranquil 
changed form of a statement



@2473

9 years 
tranquil 
put some generic stuff we need in the back end in extraGlobalenvs …



@2471

9 years 
campbell 
Tame global environments a little.



@2470

9 years 
tranquil 
completely separated program counters from code pointers in joint …



@2468

9 years 
garnier 
Floats are gone from the frontend. Some trace amount might remain in …



@2463

9 years 
tranquil 
swapped back call_rel and ret_rel…



@2462

9 years 
tranquil 
separated in back end values program counters from code pointers …



@2459

9 years 
campbell 
Syntax update



@2457

9 years 
tranquil 
rewritten function handling in joint
swapped call_rel with ret_rel in …



@2453

9 years 
tranquil 
come changes in monad notation to
* avoid pretty printed monsters
* …



@2444

9 years 
campbell 
Some inversion lemmas for after_n_steps for dealing with >1 source …



@2443

9 years 
tranquil 
changed joint's stack pointer and internal stack



@2439

9 years 
campbell 
Get a proper reverse mapping of function blocks to identifiers by …



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


