|
|
@1602
|
8 years |
mulligan |
giving up on fetch proofs for time being
|
|
|
@1600
|
8 years |
sacerdot |
utilities and ASM ported to the new standard library
|
|
|
@1599
|
8 years |
sacerdot |
Start of merging of stuff into the standard library of Matita.
|
|
|
@1598
|
8 years |
mulligan |
changes over the last couple of days
|
|
|
@1597
|
8 years |
mulligan |
fixed fetch for jaap
|
|
|
@1593
|
8 years |
boender |
- cleaned up Assembly, moved some definitions elsewhere
|
|
|
@1592
|
8 years |
boender |
- updated definitions to work with programs of maximum 216 instructions
|
|
|
@1591
|
8 years |
mulligan |
work from today
|
|
|
@1588
|
8 years |
sacerdot |
All goals generated by Russell for execute_1* are now closed, mostly …
|
|
|
@1587
|
8 years |
mulligan |
changes from today, including removing indexing of problematic …
|
|
|
@1582
|
8 years |
mulligan |
more added to the proof of execute_1_preinstruction --- ~260 cases now …
|
|
|
@1581
|
8 years |
mulligan |
Dangling de Bruijn pointer when trying to propagate russell to set_arg_1
|
|
|
@1579
|
8 years |
mulligan |
Finished proof with simpler statement, making everything a lot nicer
|
|
|
@1578
|
8 years |
boender |
- proof of termination of policy completed (needs some clean-up work …
|
|
|
@1577
|
8 years |
mulligan |
A lot more cases added to the proof at the bottom of …
|
|
|
@1576
|
8 years |
mulligan |
big changes to proofs, just two small cases remain and a few …
|
|
|
@1575
|
8 years |
mulligan |
Changes to specifications on execute functions
|
|
|
@1573
|
8 years |
mulligan |
more complicated than it appears :(
|
|
|
@1571
|
8 years |
mulligan |
small changes
|
|
|
@1570
|
8 years |
sacerdot |
Dependent type crazyness.
|
|
|
@1567
|
8 years |
mulligan |
more work on big proof, 2.5 cases left
|
|
|
@1564
|
8 years |
sacerdot |
Commit where we use a dependently typed version of bigops.
I am now …
|
|
|
@1562
|
8 years |
mulligan |
new version of assembly, fixed conflict in positivemap.ma, changed …
|
|
|
@1561
|
8 years |
sacerdot |
More dependent types to accomodate the statement.
|
|
|
@1560
|
8 years |
sacerdot |
Complete re-implementation that:
1) assumes no code before the first …
|
|
|
@1558
|
8 years |
sacerdot |
Snapshot before moving things to ASMCosts.ma.
|
|
|
@1557
|
8 years |
sacerdot |
Byte => costlabel
|
|
|
@1556
|
8 years |
mulligan |
submitting to avoid conflicts
|
|
|
@1555
|
8 years |
boender |
- changes to assembly
- added lookup to PositiveMap?
- lightly changed …
|
|
|
@1554
|
8 years |
sacerdot |
Major progress in the proof.
|
|
|
@1553
|
8 years |
boender |
- added lookup_opt_lookup lemma
|
|
|
@1550
|
8 years |
sacerdot |
Repaired after use of Russell for execute_1.
|
|
|
@1549
|
8 years |
mulligan |
removed cruft from costsproof.ma file so claudio can work in parallel
|
|
|
@1548
|
8 years |
sacerdot |
…
|
|
|
@1547
|
8 years |
sacerdot |
Invariant on cost of one execution step strengthened.
|
|
|
@1544
|
8 years |
sacerdot |
StructuredTraces? inhabited for object code.
|
|
|
@1541
|
8 years |
mulligan |
interpret.ma now compiles
|
|
|
@1540
|
8 years |
mulligan |
changes to proof in interrupt.ma
|
|
|
@1538
|
8 years |
mulligan |
changes to execute_1_0 proof
|
|
|
@1534
|
8 years |
mulligan |
committing my changes to interpret to prevent any further conflicts
|
|
|
@1533
|
8 years |
sacerdot |
Proof of execute_1 with Russell completed (up to some daemon used before).
|
|
|
@1530
|
8 years |
campbell |
Update due to Russell changes.
|
|
|
@1528
|
8 years |
campbell |
Update most of Assembly.ma with new syntax and identifier maps.
Change …
|
|
|
@1527
|
8 years |
sacerdot |
More on Russell.
|
|
|
@1526
|
8 years |
sacerdot |
Using Russell to prove some properties.
|
|
|
@1524
|
8 years |
boender |
- adapted files to new Matita syntax
|
|
|
@1522
|
8 years |
mulligan |
changes to preamble and lin to asm pass, resolved conflict in interpret
|
|
|
@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 …
|
|
|