

@3263

6 years 
tranquil 
moved callee saved saving and restoring to ERTL > LTL pass (untrusted …



@3145

7 years 
tranquil 
* removed sigma types from traces of intensional events
* completed …



@3037

7 years 
tranquil 
* ADDRESS joint instruction now has also an offset
* corrected call to …



@2946

7 years 
tranquil 
main novelties:
* there is an inbuilt stack_usage nat in joint …



@2865

7 years 
sacerdot 
…



@2863

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



@2843

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



@2824

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



@2823

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



@2808

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



@2783

7 years 
piccolo 
modified joint_closed_internal_function definition (added condition on …



@2774

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



@2712

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



@2688

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



@2681

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



@2655

7 years 
tranquil 
new step in code semantic lemma



@2645

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



@2595

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



@2562

7 years 
piccolo 
linearise modified



@2561

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



@2547

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



@2537

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



@2532

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



@2490

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



@2462

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



@2457

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



@2437

7 years 
tranquil 
generalised calls to calls with pointers



@2422

7 years 
tranquil 
adapted joint to cl_call f



@2286

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



@1601

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



@1471

8 years 
mulligan 
finished erasure and generalised so as to work on arbitrary joint programs



@1380

8 years 
sacerdot 
LTL and LIN semantics factorized out in joint_LTL_LIN_semantics.ma. …



@1282

8 years 
sacerdot 
Cosmetic change: names of joint statements/instructions shortened and …



@1280

8 years 
sacerdot 
Some progress in the porting of RTLAbstoRTL to the joint syntax:
1) …



@1275

8 years 
sacerdot 
RTL ported to joint syntax, but:
1. bug discovered: opaccs should …



@1271

8 years 
mulligan 
finished, kind of



@1270

8 years 
sacerdot 
Making RTL syntax an instance of Joint.



@1260

8 years 
mulligan 
commit for csc



@1255

8 years 
sacerdot 
Major mistake fixed: op1 and op2 were assuming the source and dest …



@1254

8 years 
sacerdot 
More progress towards porting of RTLtoERTL to joint syntax.



@1252

8 years 
sacerdot 
graph_params added to joint/Joint.ma, together with useful common …



@1250

8 years 
sacerdot 
1. Sigma types projections moved to utilities/extralib.ma
2. Extended …



@1246

8 years 
sacerdot 
Yet another change to Joint.ma to accomodate all passes.
The concrete …



@1245

8 years 
sacerdot 
RTLtoERTL and LINToASM: porting to new Joint data type in progress. …



@1236

8 years 
sacerdot 
LTLToLin.ma completed (up to a couple of daemons used to provide dead …



@1233

8 years 
sacerdot 
1) Ported to Brian's new dependent type for fullexec
2) Universe level …



@1228

8 years 
mulligan 
some more changes



@1220

8 years 
sacerdot 
ERTL ported to the new joint syntax.



@1182

8 years 
mulligan 
changes to semantics: removing parameterised "next" element in joint …



@1176

8 years 
sacerdot 
…



@1171

8 years 
mulligan 
changes made on claudio's request: changed order of nesting in the …



@1169

8 years 
sacerdot 
JointRTLtoLIN moved to Joint



@1167

8 years 
mulligan 
…


copied from src/joint/JointLTLLIN.ma:



@1166

8 years 
mulligan 
moved joint ltl lin files into their own directory. more changes to …
