

@2536

8 years 
piccolo 
finished eval_seq_no_pc_sigma_commute lemma



@2532

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



@2529

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



@2528

8 years 
piccolo 
added cases PUSH, C_ADDRESS and COPACCS



@2507

8 years 
piccolo 
finished pop case in commutation eval_Seq_no_pc



@2501

8 years 
piccolo 
working on lineariseProof. Not yet finished.



@2495

8 years 
piccolo 
continuing lineariseProof



@2491

8 years 
tranquil 
fixed wrt change of list member definition



@2490

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



@2484

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



@2481

8 years 
piccolo 
corrected some inconsistencies
fixed some of lineariseProof



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



@2470

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



@2467

8 years 
piccolo 
LINEARISE PROOF MODIFIED NOT YED FIXED



@2464

8 years 
piccolo 
adapted lineariseProof to new semantics



@2462

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



@2457

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



@2456

8 years 
boender 
 added simple proof



@2452

8 years 
piccolo 
Completed commutation lemmas of fetch_statement



@2447

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



@2446

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



@2445

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



@2443

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



@2442

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



@2440

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



@2437

8 years 
tranquil 
generalised calls to calls with pointers



@2426

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



@2422

8 years 
tranquil 
adapted joint to cl_call f



@2417

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



@2398

8 years 
boender 
 committed start of stacksize



@2324

8 years 
tranquil 
semantics of blocks: function to produce trace from execution of …



@2286

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



@2233

8 years 
tranquil 
* completed update of ERTL semantics
* some minor changes in joint …



@2217

8 years 
tranquil 
* collapsed step_params, unserialized_params, funct_params and …



@2214

8 years 
tranquil 
* changed order of parameters of joint_internal_function and genv in …



@2208

8 years 
tranquil 
* moving some code around
* changed immediates to hold beval in …



@2200

8 years 
tranquil 
* updated joint semantics: generation of linear and graph semantics
* …



@2186

8 years 
tranquil 
updated joint semantics



@2185

8 years 
campbell 
Use bitvectors for offsets.



@2182

8 years 
tranquil 
updated linearisation pass



@2176

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



@2162

8 years 
tranquil 
* yet another correction to joint
* added functions adding prologues …



@2155

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



@2103

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



@2043

8 years 
sacerdot 
Broken code commented out.



@2042

8 years 
sacerdot 
Repaired (Type => DeqSet?)



@1999

8 years 
campbell 
Make backend use the main global envs.



@1995

8 years 
campbell 
Overall compiler definition; bits and pieces to
make everything happy(ish).



@1993

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



@1988

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



@1987

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



@1976

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



@1949

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



@1908

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



@1882

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



@1874

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



@1709

9 years 
mulligan 
Changes to the execution of the MOVC instruction



@1644

9 years 
tranquil 
minor changes



@1643

9 years 
tranquil 
* some changes in everything
* separated extensions in sequential and …



@1641

9 years 
tranquil 
* semanticsUtils_paolo.ma contains code to generate both graph and …



@1640

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



@1635

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



@1601

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



@1599

9 years 
sacerdot 
Start of merging of stuff into the standard library of Matita.



@1521

9 years 
sacerdot 
Syntax change in Matita: change what where => change where what.



@1516

9 years 
sacerdot 
Ported to syntax of Matita 0.99.1.



@1515

9 years 
campbell 
Add type of maps on positive binary numbers, and use them for …



@1472

9 years 
mulligan 
moved proof utils to erasure.ma



@1471

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



@1470

9 years 
mulligan 
finished, pretty ugly though as matita's disambiguation is a …



@1469

9 years 
mulligan 
finished new relabelling for graphs subject to one axiom closed



@1467

9 years 
mulligan 
small change, adding entry and exit labels into the internal function, …



@1466

9 years 
mulligan 
erasure for graph based joint languages almost complete



@1463

9 years 
mulligan 
added erasure for lin



@1458

9 years 
mulligan 
added skeleton file for erasure function for joint languages



@1457

9 years 
sacerdot 
Bug fixed: when calling an internal function, the pc block is now set …



@1452

9 years 
sacerdot 
Bug fixed: labels MUST be represented as pointers whose block is the …



@1451

9 years 
sacerdot 
1. All axioms in LIN/semantics.ma closed
2. succ_pc and …



@1430

9 years 
sacerdot 
Bug fixed: push/pop must work on the isp (now added).
Note: the sp is …



@1419

9 years 
sacerdot 
All axioms closed.



@1416

9 years 
sacerdot 
Maps from hardware registers to beval now implemented in ASM/I8051 (in …



@1415

9 years 
sacerdot 
1. hwreg_store/retrieve no longer returns a res (but it is still …



@1411

9 years 
sacerdot 
1. sem_params2 splitted into sem_params1 + sem_params2 to take out the …



@1408

9 years 
sacerdot 
1. Added joint/BEGlobalenvs that is a modification of …



@1395

9 years 
sacerdot 
1) New versions of pointer_of_beval/beval_of_pointer with a stricter …



@1390

9 years 
sacerdot 
All fetch_result implementations have been factorized out, leaving …



@1387

9 years 
sacerdot 
Further simplification *params1 no longer used.



@1386

9 years 
sacerdot 
Structure of semantic parameters simplified.



@1385

9 years 
sacerdot 
1. fetch_result and pop_frame now takes the genv in input
2. …



@1384

9 years 
sacerdot 
* fetch_ra taken out of pop_frame again since it is used uniformly and …



@1383

9 years 
sacerdot 
Potential bug fixed and bug found: the way pointers and labels are put …



@1382

9 years 
sacerdot 
 succ_pc generalized to return a res (necessary for LIN semantics)
 …



@1380

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



@1377

9 years 
sacerdot 
pop_frame now incorporates the fetch_result (that made sense only for …



@1376

9 years 
sacerdot 
Stack deallocation for RTL implemented in pop_frame.



@1372

9 years 
sacerdot 
save_frame now takes the stacksize to allow RTL to allocate the stack frame



@1371

9 years 
sacerdot 
save_frame changed to accept also the formal/actual argument pairs, …


