

@3096

8 years 
tranquil 
preliminary work on closing correctness.ma



@3081

8 years 
campbell 
Tidy up recent work a little.



@3063

8 years 
campbell 
Remove measure function from FEMeasurable because we're not using it …



@3050

8 years 
piccolo 
1) Added general commutation theorem for monads.
2) Added some …



@3032

8 years 
campbell 
Remind myself why ms_rel_normal is reasonable.



@3007

8 years 
campbell 
Sketch out how Cminor to RTLabs correctness would fit into the …



@2991

8 years 
piccolo 
Fixed cond and seq case in StatusSimulationHelper?
Added cost case in …



@2990

8 years 
campbell 
Replace dodgy hypothesis by nice ones, clean up a little.



@2989

8 years 
campbell 
Make frontend measurability preservation proof cope with moving the …



@2975

8 years 
tranquil 
* RTL premain fixed
* fixed bug in back end ops (subtracting to a …



@2959

8 years 
sacerdot 
Typo



@2958

8 years 
sacerdot 
Error message implemented.



@2953

8 years 
campbell 
Fix silly label handling bug I realised was there during my talk…



@2927

8 years 
tranquil 
stupid bug in bool_of_beval



@2926

8 years 
tranquil 
corrected bug in executing Sub



@2914

8 years 
campbell 
Use single definition for stack measurement.



@2896

8 years 
campbell 
Complete part of measurable to structured subtraces proof that
shows …



@2895

8 years 
campbell 
Match up function id from RTLabs Callstate with shadow stack,
use in …



@2871

8 years 
tranquil 
op2 evaluation on beval's rendered oblivious to carry bit when …



@2870

8 years 
sacerdot 
Proof fixed.



@2869

8 years 
tranquil 
some reorganization of definitions, and a new taaf_append_taaf



@2843

8 years 
piccolo 
1) Fixed a litte bug in Joint.ma
2) ERTL to ERTLptr correctness proof …



@2824

8 years 
tranquil 
* moved sum on lists notation to extranat
* used sum on lists to …



@2807

8 years 
mckinna 
Yet another ErrorMessage?
Removed corresponding axiom in …



@2801

8 years 
piccolo 
Partial commit not yet finished



@2800

8 years 
campbell 
Tidy up Measurable.ma a little, get rid of obsolete comments.



@2799

8 years 
tranquil 
* added taaf_to_taa, conversion from trace_any_any_free to …



@2796

8 years 
tranquil 
* added global notation for existence in Type[1] (\exists[1] x.P)
* in …



@2795

8 years 
sacerdot 
Added new function Measurable.observe_all_in_measurable to be used to …



@2783

8 years 
piccolo 
modified joint_closed_internal_function definition (added condition on …



@2769

8 years 
mckinna 
Mistakenly commented out
both as_cost_get_label (needed; OK)
as well …



@2768

8 years 
mckinna 
Nightmare: file no longer typechecks,
because defn as_cost_get_labels …



@2767

8 years 
mckinna 
WARNING: BIG commit, which pushes code_size_opt check into …



@2760

8 years 
sacerdot 
1. Many files repaired.
2. 3 new daemons: 2 in Assembly.ma, 1 in …



@2757

8 years 
tranquil 
many things are still broken, but there is a partial backtrack on …



@2756

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



@2755

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



@2751

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



@2727

8 years 
campbell 
Remove a couple of redundant hypotheses.



@2726

8 years 
campbell 
Show max stack preserved in FEMeasurable.



@2725

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



@2724

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



@2722

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



@2720

8 years 
tranquil 
implemented back end ops that were still axioms



@2703

8 years 
mckinna 
now includes defn of costlabel_map



@2690

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



@2685

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



@2682

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



@2678

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



@2673

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



@2670

8 years 
campbell 
Clean up from recent commits.



@2669

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



@2668

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



@2646

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



@2645

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



@2644

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



@2641

8 years 
piccolo 
defined dummy block code equals to 0



@2624

8 years 
campbell 
Properly evict unused and axiomatised Floats.



@2618

8 years 
campbell 
Tidy up measurable a little.



@2617

8 years 
campbell 
Trivial simplification on split_trace.



@2608

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



@2604

8 years 
piccolo 
ERTLtoERTLptr in place.



@2603

8 years 
piccolo 
Dead code commented out.



@2601

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



@2599

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



@2597

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



@2596

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



@2590

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



@2582

8 years 
garnier 
Some progress on CL to CM.



@2570

8 years 
piccolo 
ERTLtoERTLptr in place



@2569

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



@2553

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



@2548

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



@2541

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



@2540

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



@2539

8 years 
tranquil 
added cl_jump case to trace_any_any_free



@2534

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



@2533

8 years 
campbell 
Some fall out from removing floats.



@2531

8 years 
mckinna 
Trivial tweaks.



@2530

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



@2511

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



@2508

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



@2503

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



@2502

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



@2500

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



@2496

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



@2487

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



@2486

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



@2478

8 years 
tranquil 
unified is_internal_function_of_program and is_internal_function



@2477

8 years 
tranquil 
status_simulation reformulated
definition of joint_classify split up …



@2476

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



@2474

8 years 
tranquil 
changed form of a statement



@2473

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



@2471

8 years 
campbell 
Tame global environments a little.



@2470

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



@2468

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



@2463

8 years 
tranquil 
swapped back call_rel and ret_rel…



@2462

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



@2459

8 years 
campbell 
Syntax update



@2457

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


