|
|
@1521
|
8 years |
sacerdot |
Syntax change in Matita: change what where => change where what.
|
|
|
@1519
|
8 years |
campbell |
More syntax updates.
|
|
|
@1518
|
8 years |
campbell |
Update to new syntax.
|
|
|
@1516
|
8 years |
sacerdot |
Ported to syntax of Matita 0.99.1.
|
|
|
@1515
|
8 years |
campbell |
Add type of maps on positive binary numbers, and use them for …
|
|
|
@1514
|
8 years |
mulligan |
changes from today. matita keeps dieing
|
|
|
@1511
|
8 years |
mulligan |
proofs, added, changes to execute_1_0 function therefore required to …
|
|
|
@1509
|
8 years |
mulligan |
i hate subtraction over the nats
|
|
|
@1506
|
8 years |
mulligan |
changes to costs proof over weekend
|
|
|
@1503
|
8 years |
mulligan |
inductive type complete
|
|
|
@1502
|
8 years |
mulligan |
changes to inductive defn
|
|
|
@1501
|
8 years |
sacerdot |
We must take in account the labelled_p predicate.
|
|
|
@1500
|
8 years |
sacerdot |
Proof sketch for one of the two main proofs.
|
|
|
@1499
|
8 years |
mulligan |
part way through main statement transcription
|
|
|
@1498
|
8 years |
mulligan |
added new file for proof that costs are preserved at asm level
|
|
|
@1497
|
8 years |
mulligan |
a bit of tidying up, removing dead code, etc.
|
|
|
@1496
|
8 years |
mulligan |
problem fixed with tactics missing a semicolon to stop greedy parsing
|
|
|
@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
|
|
|