|
|
@1495
|
8 years |
mulligan |
proper calculation of costs
|
|
|
@1494
|
8 years |
mulligan |
changes to get everything compiling again
|
|
|
@1493
|
8 years |
mulligan |
finished well labeled check, up to injectivity of the label map
|
|
|
@1487
|
8 years |
mulligan |
committing some code for well labelling
|
|
|
@1486
|
8 years |
mulligan |
finished asm costs
|
|
|
@1485
|
8 years |
sacerdot |
Less nice definitiion of add_with_carries that avoids a quadratic …
|
|
|
@1484
|
8 years |
sacerdot |
…
|
|
|
@1482
|
8 years |
sacerdot |
1. very long standing conflict committed (but don't ask me what the …
|
|
|
@1479
|
8 years |
boender |
- added insert_lookup_opt
- assembly compiles now
|
|
|
@1478
|
8 years |
sacerdot |
Almost completed (up to is_finals).
|
|
|
@1476
|
8 years |
sacerdot |
…
|
|
|
@1475
|
8 years |
sacerdot |
Towards the two fullexec transition systems that represent …
|
|
|
@1474
|
8 years |
mulligan |
adding missing asmcosts file for computing the costs of an assembly …
|
|
|
@1463
|
8 years |
mulligan |
added erasure for lin
|
|
|
@1461
|
8 years |
mulligan |
rewrote erasure for assembly programs
|
|
|
@1460
|
8 years |
mulligan |
most of cost label erasure for assembly language complete, with one …
|
|
|
@1459
|
8 years |
boender |
- moved stronger occurs_exactly_once lemma to its proper place in …
|
|
|
@1426
|
8 years |
boender |
removed axiom
|
|
|
@1424
|
8 years |
sacerdot |
1. fold function over BitVectorTries? moved from ERTLToLTL to …
|
|
|
@1417
|
8 years |
boender |
- proved that jumps always increase - this should make termination easy
|
|
|
@1416
|
8 years |
sacerdot |
Maps from hardware registers to beval now implemented in ASM/I8051 (in …
|
|
|
@1415
|
8 years |
sacerdot |
1. hwreg_store/retrieve no longer returns a res (but it is still …
|
|
|
@1404
|
8 years |
boender |
- reworked + added
- added an axiom to arithmetic, but should be provable
|
|
|
@1393
|
8 years |
boender |
- added invariant for policy trie to assembly
- change (syntax only) …
|
|
|
@1363
|
8 years |
boender |
- done stuff with create_label_trie
|
|
|
@1335
|
8 years |
sacerdot |
Ported to new Matita stdlib.
|
|
|
@1333
|
8 years |
sacerdot |
Avoid using the name of the construction of jmeq.
|
|
|
@1330
|
8 years |
campbell |
Evict obsolete file.
|
|
|
@1323
|
8 years |
campbell |
Reduce number of notations for destructive let on pairs to one.
|
|
|
@1316
|
8 years |
campbell |
Merge in id-lookup-branch to trunk.
|
|
|
@1309
|
8 years |
boender |
- refounded JEP
|
|
|
@1279
|
8 years |
sacerdot |
Bug fixed in definition of ltb.
|
|
|
@1207
|
8 years |
campbell |
Second part of fixing temporaries in Clight to Cminor stage.
|
|
|
@1193
|
8 years |
mulligan |
work on colouring algorithm halted as it can be axiomatised. now …
|
|
|
@1187
|
8 years |
mulligan |
fixed build.ma
|
|
|
@1161
|
8 years |
mulligan |
changes from today: merged ertl, ltl and lin into one datatype to …
|
|
|
@1159
|
8 years |
boender |
- added 'nth' theorems
- moved up \bot a bit
|
|
|
@1145
|
8 years |
mulligan |
changed naming in i8051 of classes of registers to make them consistent
|
|
|
@1119
|
8 years |
sacerdot |
Type for evaluation of opaccs fixed (maybe wrongly: should it return …
|
|
|
@1112
|
8 years |
mulligan |
got lin > asm stuff working
|
|
|
@1103
|
8 years |
boender |
- reverted to old policy
|
|
|
@1094
|
8 years |
mulligan |
some changes from today to do with liveness analyses
|
|
|
@1089
|
8 years |
mulligan |
more changes from earlier in the week
|
|
|
@1075
|
8 years |
mulligan |
nearly completed rtl -> ertl pass removing all option types with dep. types
|
|
|
@1074
|
8 years |
boender |
- added lookup lemma
|
|
|
@1071
|
8 years |
mulligan |
changes the specific form that the added proofs take to use None, not …
|
|
|
@1070
|
8 years |
campbell |
Show that entry and exit labels are in the RTLabs graph.
|
|
|
@1069
|
8 years |
campbell |
Change odd proof obligation problem back.
|
|
|
@1066
|
8 years |
mulligan |
changes from today
|
|
|
@1064
|
8 years |
mulligan |
changes from today, nearly complete rtlabs translation pass
|
|
|
@1063
|
8 years |
mulligan |
changes from today
|
|
|
@1062
|
8 years |
mulligan |
separated jmeq and coercions from foldstuff.ma in order to fix the …
|
|
|
@1061
|
8 years |
mulligan |
more work, bug found, ridiculous map3 function with dep. types added
|
|
|
@1060
|
8 years |
mulligan |
work from this morning and yesterday
|
|
|
@1059
|
8 years |
mulligan |
work from today, bit of a mess at the moment
|
|
|
@1057
|
8 years |
mulligan |
changes from today
|
|
|
@1054
|
8 years |
boender |
- proven policy safe
|
|
|
@1052
|
8 years |
mulligan |
removed offsets after reading cerco mailing list
|
|
|
@1045
|
8 years |
mulligan |
resolved conflict in rtlabs
|
|
|
@1044
|
8 years |
boender |
- more fold/forall stuff
|
|
|
@1043
|
8 years |
sacerdot |
Axiom commented out.
|
|
|
@1042
|
8 years |
sacerdot |
Dead code removed.
Slow code uncommented.
|
|
|
@1041
|
8 years |
sacerdot |
fetch_assembly is still working after bug fix
|
|
|
@1040
|
8 years |
sacerdot |
Bug fixed in assembly.
|
|
|
@1039
|
8 years |
sacerdot |
fetch_assembly_pseudo2 repaired from dependent type madness
|
|
|
@1038
|
8 years |
boender |
- some more BVT improvements
|
|
|
@1037
|
8 years |
sacerdot |
Main theorem: comments are working again.
|
|
|
@1036
|
8 years |
sacerdot |
…
|
|
|
@1035
|
8 years |
sacerdot |
Main theorem (broken because of dependent types) almost restored.
|
|
|
@1034
|
8 years |
boender |
various & sundry fold/forall lemmas
|
|
|
@1033
|
8 years |
sacerdot |
ispelled & submitted
|
|
|
@1032
|
8 years |
sacerdot |
Final version.
|
|
|
@1031
|
8 years |
sacerdot |
..
|
|
|
@1030
|
8 years |
sacerdot |
…
|
|
|
@1029
|
8 years |
sacerdot |
…
|
|
|
@1028
|
8 years |
sacerdot |
One more sentence restored and fitted in.
|
|
|
@1027
|
8 years |
sacerdot |
Bug fixed in figure.
|
|
|
@1026
|
8 years |
mulligan |
final version? under 16 pages
|
|
|
@1025
|
8 years |
mulligan |
removing stray single words to reduce page usage
|
|
|
@1024
|
8 years |
mulligan |
tidied explanation of proof
|
|
|
@1023
|
8 years |
mulligan |
changes to english in matita section, shrunk diagrams in introduction …
|
|
|
@1022
|
8 years |
sacerdot |
…
|
|
|
@1021
|
8 years |
mulligan |
tidied english in sect 3
|
|
|
@1020
|
8 years |
sacerdot |
More on Matita.
|
|
|
@1019
|
8 years |
sacerdot |
Finished rewriting of Section 3.
|
|
|
@1018
|
8 years |
mulligan |
tidying
|
|
|
@1017
|
8 years |
mulligan |
complete, just under 16 pages
|
|
|
@1016
|
8 years |
sacerdot |
Many fixes to the code snippets.
|
|
|
@1015
|
8 years |
sacerdot |
One intermediate version of main_thm0 close to be repaired.
|
|
|
@1014
|
8 years |
sacerdot |
The main theorem is completely broken (again).
|
|
|
@1013
|
8 years |
mulligan |
more added
|
|
|
@1012
|
8 years |
mulligan |
just a few things left to change
|
|
|
@1011
|
8 years |
mulligan |
…
|
|
|
@1010
|
8 years |
mulligan |
more added, finished up to end of subsect 3.2
|
|
|
@1009
|
8 years |
mulligan |
added line number counts, etc.
|
|
|
@1008
|
8 years |
mulligan |
…
|
|
|
@1007
|
8 years |
mulligan |
added explanation of sdcc
|
|
|
@1006
|
8 years |
boender |
- added fold + lemmas on fold
|
|
|
@1005
|
8 years |
sacerdot |
…
|
|
|
@1004
|
8 years |
mulligan |
changes to typesetting
|
|
|