

@2883

9 years 
piccolo 
partial commit



@2879

9 years 
tranquil 
changed coercion from list of joint_seq to blocks to a more efficient one



@2878

9 years 
tranquil 
backtracked some changes that were not ready for commit



@2876

9 years 
tranquil 
corrected another endianess bug in joint_semantics. Switched some …



@2869

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



@2865

9 years 
sacerdot 
…



@2863

9 years 
piccolo 
Added new invariant to good_if
Generalized version of cond case for …



@2859

9 years 
sacerdot 
Pretty printing improved (now it always starts the visit from lbl 1).



@2858

9 years 
sacerdot 
Trying to pretty print the code graph in visit order.
Slightly bugged …



@2855

9 years 
piccolo 
little bug fixed in TranslateUtils?.



@2853

9 years 
sacerdot 
Pretty printing of line/label numbers.



@2851

9 years 
piccolo 
partial commit



@2847

9 years 
sacerdot 
…



@2846

9 years 
sacerdot 
Pretty printing of joint programs.



@2843

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



@2824

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



@2823

9 years 
tranquil 
* corrected bug in ERTL semantics (both delframe and newframe did the …



@2821

9 years 
tranquil 
* implemented preclassified system for joint (in joint/joint_fullexec.ma)



@2817

9 years 
sacerdot 
Repaired after Paolo's commit.



@2816

9 years 
sacerdot 
Repaired after Paolo's commit.



@2808

9 years 
tranquil 
added local_stacksize to joint internal functions to accomodate for …



@2806

9 years 
tranquil 
new b_graph_translate obligations



@2796

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



@2785

9 years 
piccolo 
Traces.ma repaired



@2784

9 years 
sacerdot 
Repaired after Mauro's commit.



@2783

9 years 
piccolo 
modified joint_closed_internal_function definition (added condition on …



@2774

9 years 
sacerdot 
1. the compiler now outputs both the stack cost model and the max …



@2760

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



@2757

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



@2755

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



@2723

9 years 
campbell 
Library name typo fixed.



@2716

9 years 
sacerdot 
utilities/deqsets.ma => utilities/deqsets_extra.ma for extraction



@2712

9 years 
tranquil 
changed some fields of joint_internal_function's invariant
fixed linearise



@2708

9 years 
tranquil 
fixed linearise and LINToASM
LINToASM has now correct transformation …



@2702

9 years 
sacerdot 
1. proof closed in ASM/UtilBranch
2. more passes integrated in the …



@2688

9 years 
tranquil 
* in Arithmeticcs.ma: commented include that breaks script in latest …



@2687

9 years 
tranquil 
* polished some interfaces



@2683

9 years 
tranquil 
proof of properties of b_graph_program_transform (with an open axiom)



@2681

9 years 
tranquil 
* improvements to the graph translation function
* fixed passes up to LTL



@2675

9 years 
tranquil 
* a generic graph program transformation



@2674

9 years 
tranquil 
* another change in block definition
* RTLabs > RTL and ERTL > …



@2666

9 years 
piccolo 
bug fixed in blocks.ma



@2661

9 years 
sacerdot 
stacksize "repaired" by "considering" tailcalls
Some daemons added …



@2655

9 years 
tranquil 
new step in code semantic lemma



@2647

9 years 
sacerdot 
Stupid typo fixed.



@2645

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



@2642

9 years 
piccolo 
fixed joint/Traces after having posed block 0 to be Code



@2641

9 years 
piccolo 
defined dummy block code equals to 0



@2639

9 years 
sacerdot 
We are not going to prove erasure. Thus this becomes dead code.



@2638

9 years 
piccolo 
Backend fixes for last Garnier's commit that removes the regions from …



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



@2595

9 years 
tranquil 
* dropped locals and exit from definition of joint_if_function
* new …



@2592

9 years 
piccolo 
main lemma of ERTLptr in place



@2590

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



@2570

9 years 
piccolo 
ERTLtoERTLptr in place



@2564

9 years 
piccolo 
ERTL fully repaired, useless part of return value of pop_ra
removed.



@2562

9 years 
piccolo 
linearise modified



@2561

9 years 
tranquil 
* moved CALL as different case than joint_seq: lots of broken code now …



@2559

9 years 
piccolo 
lineariseProof finished



@2557

9 years 
tranquil 
minor modification of commented (for now) proof of correctness of …



@2556

9 years 
tranquil 
in joint semantics and traces: added a last popped calling address to …



@2555

9 years 
piccolo 
lemma eval_call_ok finished



@2553

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



@2551

9 years 
piccolo 
completed isFinal and fetchStatementSigmaCommute. Fixed exit …



@2548

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



@2547

9 years 
tranquil 
going on in proof of linearise
simplified by use of monadic functional …



@2543

9 years 
piccolo 
finished stmt_at_sigma_commute



@2538

9 years 
tranquil 
fixed Traces.ma after changes in joint/semantics.ma



@2537

9 years 
tranquil 
rolled back changes on calls in joint. Now the save_frame parameter …



@2536

9 years 
piccolo 
finished eval_seq_no_pc_sigma_commute lemma



@2532

9 years 
tranquil 
added FCOND in LIN, and rewritten linearise so that it never adds a …



@2529

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



@2528

9 years 
piccolo 
added cases PUSH, C_ADDRESS and COPACCS



@2507

9 years 
piccolo 
finished pop case in commutation eval_Seq_no_pc



@2501

9 years 
piccolo 
working on lineariseProof. Not yet finished.



@2495

9 years 
piccolo 
continuing lineariseProof



@2491

9 years 
tranquil 
fixed wrt change of list member definition



@2490

9 years 
tranquil 
switched back to Byte immediate (instead of beval ones)
propagated …



@2484

9 years 
piccolo 
fixed Traces and semantics
added commutation record (not yet finished) …



@2481

9 years 
piccolo 
corrected some inconsistencies
fixed some of lineariseProof



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



@2470

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



@2467

9 years 
piccolo 
LINEARISE PROOF MODIFIED NOT YED FIXED



@2464

9 years 
piccolo 
adapted lineariseProof to new semantics



@2462

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



@2457

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



@2456

9 years 
boender 
 added simple proof



@2452

9 years 
piccolo 
Completed commutation lemmas of fetch_statement



@2447

9 years 
piccolo 
All axioms opened so far and that must be closed here have been
closed.



@2446

9 years 
piccolo 
Fetch commutation proof reduced to one simple (?) lemma.



@2445

9 years 
piccolo 
1. sigma function axiomatically defined (together with
its spec). …



@2443

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



@2442

9 years 
piccolo 
Traces repaired. (By Paolo)
Statement of lineariseProof in place.



@2440

9 years 
piccolo 
fixed range_strong and linearise
(commit by Paolo, he's to blame in case)



@2437

9 years 
tranquil 
generalised calls to calls with pointers



@2426

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


