

@3081

8 years 
campbell 
Tidy up recent work a little.



@3050

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



@2949

8 years 
sacerdot 
Some advance/repairing in ERTLptrToLTLProof. In particular, we know …



@2897

8 years 
campbell 
Minor tidying.



@2824

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



@2800

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



@2796

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



@2772

8 years 
sacerdot 
Useless code removed.



@2770

8 years 
mckinna 
WARNING: another big commit, touching many files in ASM/*.ma
This …



@2767

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



@2732

8 years 
sacerdot 
Unused code removed.



@2728

8 years 
sacerdot 
listb.ma => listb_extra.ma for extraction



@2716

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



@2708

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



@2700

8 years 
sacerdot 
1. exponential function dropped in favour of standard library
2. …



@2670

8 years 
campbell 
Clean up from recent commits.



@2601

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



@2529

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



@2453

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



@2443

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



@2440

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



@2314

9 years 
campbell 
Move generic definitions from recent commit to appropriate places.



@2310

9 years 
garnier 
Moved a lemma from switchRemoval to positive.



@2309

9 years 
garnier 
Removed the superfluous xorb definition and move some basic properties …



@2306

9 years 
campbell 
An insertion sort for testing purposes.



@2296

9 years 
campbell 
Tidy up some illplaced definitions.



@2292

9 years 
campbell 
More RTLabs invariants.



@2286

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



@2200

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



@2179

9 years 
campbell 
Dependent pair monad binding notation.



@2178

9 years 
campbell 
Shift some notation into utilities.



@2174

9 years 
tranquil 
* factored out script for (axiomatised) fixpoint computation
* ERTL → …



@2155

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



@2101

9 years 
boender 
 renamed medium to absolute jump
 revised proofs of policy, some …



@2006

9 years 
boender 
 added alias for bitvector zero
 changed extralib bounded …



@1976

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



@1949

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



@1930

9 years 
campbell 
Tidy up labelling simulation stuff a bit.



@1908

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



@1882

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



@1648

9 years 
mulligan 
new version of utilities/monad.ma with typecheck command comented out



@1647

9 years 
tranquil 
* corrected some notation problems
* adapted Cligth with slight …



@1640

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



@1636

9 years 
tranquil 
* added coercions to arguments (in RTL) and notation for ops (for the …



@1635

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



@1631

9 years 
campbell 
Use fact that type environments in Cminor have distinct variables to …



@1630

9 years 
campbell 
Remainder of freshness in Clight to Cminor pass.



@1628

9 years 
campbell 
Show that the universe generated by Clight/fresh.ma is good.



@1626

9 years 
campbell 
Add extra type safety in front end. NB: critical freshness parts …



@1600

9 years 
sacerdot 
utilities and ASM ported to the new standard library



@1599

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



@1598

9 years 
mulligan 
changes over the last couple of days



@1593

9 years 
boender 
 cleaned up Assembly, moved some definitions elsewhere



@1587

9 years 
mulligan 
changes from today, including removing indexing of problematic …



@1551

9 years 
campbell 
Functions to translate between backend and frontend values.



@1528

9 years 
campbell 
Update most of Assembly.ma with new syntax and identifier maps.
Change …



@1523

9 years 
campbell 
Separate out positive and Z definitions from extralib.ma.
Minor syntax …



@1521

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



@1517

9 years 
sacerdot 
Ported to syntax of Matita 0.99.1.



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



@1463

9 years 
mulligan 
added erasure for lin



@1451

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



@1351

10 years 
campbell 
Tidy up some loose ends from the invariants branch merge.



@1350

10 years 
sacerdot 
Porting to latest destruct tactic.
Note: the tactics has a few …



@1341

10 years 
sacerdot 
Empty directory removed.



@1338

10 years 
sacerdot 
Automation is now stronger.



@1337

10 years 
sacerdot 
Automation is now stronger.



@1330

10 years 
campbell 
Evict obsolete file.



@1321

10 years 
sacerdot 
No longer/never implemented files removed.



@1316

10 years 
campbell 
Merge in idlookupbranch to trunk.



@1296

10 years 
mulligan 
changes



@1285

10 years 
mulligan 
more implementation on maps, final push to get rtl abs to rtl working



@1274

10 years 
mulligan 
starting removing axioms from adts and giving them proper implementations



@1268

10 years 
sacerdot 
1) AST/Identifier.ma no longer used, utilities/IdentifierTools no …



@1266

10 years 
sacerdot 
Added second projection.



@1260

10 years 
mulligan 
commit for csc



@1250

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



@1248

10 years 
mulligan 
deleted files that do not compile in utilities, changed ertl.ma to use …



@1229

10 years 
mulligan 
changes



@1227

10 years 
mulligan 
changes



@1223

10 years 
mulligan 
changes



@1219

10 years 
mulligan 
a little more added



@1218

10 years 
mulligan 
a lot added to interference graph calculation



@1212

10 years 
mulligan 
more added on interference graphs



@1211

10 years 
mulligan 
fixed interference file



@1210

10 years 
mulligan 
getting rid of typeclasslike records in favour of filelevel axioms. …



@1209

10 years 
mulligan 
more work on int. graphs



@1208

10 years 
mulligan 
added adts for sets, tables and priority sets in order to make life …



@1196

10 years 
mulligan 
some more changes, need some additional datastructures



@1195

10 years 
campbell 
List find function.



@1193

10 years 
mulligan 
work on colouring algorithm halted as it can be axiomatised. now …



@1192

10 years 
mulligan 
some files that were missing / laying dormant on my computer



@1145

10 years 
mulligan 
changed naming in i8051 of classes of registers to make them consistent



@1127

10 years 
mulligan 
interference graphs axiomatised, more added to ertl



@1092

10 years 
campbell 
Some minor definitions for identifiers and lists.



@1075

10 years 
mulligan 
nearly completed rtl > ertl pass removing all option types with dep. types



@1066

10 years 
mulligan 
changes from today



@1052

10 years 
mulligan 
removed offsets after reading cerco mailing list



@1050

10 years 
mulligan 
adding dependent types to map datastructure to remove all option …


