|
|
@1711
|
9 years |
mulligan |
finished block_cost' proof: 1.5 minutes to typecheck qed.
|
|
|
@1710
|
9 years |
mulligan |
changes from friday afternoon
|
|
|
@1709
|
9 years |
mulligan |
Changes to the execution of the MOVC instruction
|
|
|
@1697
|
9 years |
mulligan |
important bug found
|
|
|
@1696
|
9 years |
mulligan |
finished adding russell types to the traverse_cost_* functions
|
|
|
@1695
|
9 years |
mulligan |
Progress on CostsProof?.ma file.
|
|
|
@1693
|
9 years |
mulligan |
Changes to ASMCosts and CostsProofs? files to get everything working again.
|
|
|
@1692
|
9 years |
mulligan |
resolved conflict in asm costs this morning
|
|
|
@1691
|
9 years |
sacerdot |
Some progress in the proof: less daemons, less hypotheses in lemmas.
|
|
|
@1684
|
9 years |
mulligan |
changes from the past week
|
|
|
@1669
|
9 years |
mulligan |
Commit for claudio
|
|
|
@1668
|
9 years |
boender |
- split build_maps into build_maps and build_maps_ok
- work with CSC …
|
|
|
@1667
|
9 years |
sacerdot |
Main lemma for the main_thm of AssemblyProof? re-declared as an axiom …
|
|
|
@1666
|
9 years |
sacerdot |
PreStatus? datatype change: the code_memory field is not a left …
|
|
|
@1665
|
9 years |
mulligan |
progress on closing holes in block_cost' proof
|
|
|
@1663
|
9 years |
mulligan |
old cases working again, work on new ones
|
|
|
@1658
|
9 years |
mulligan |
asm costs changes from today
|
|
|
@1650
|
9 years |
mulligan |
changes over the last couple of days: stuck due to matita producing …
|
|
|
@1649
|
9 years |
boender |
- changes to Assembly for integration with Policy and easier use of …
|
|
|
@1648
|
9 years |
mulligan |
new version of utilities/monad.ma with typecheck command comented out
|
|
|
@1646
|
9 years |
mulligan |
finished the block_costs computation, and propagated the changes …
|
|
|
@1645
|
9 years |
mulligan |
more progress on the ASMCosts work: block_costs is now complete …
|
|
|
@1642
|
9 years |
mulligan |
finished big proof in all but two cases
|
|
|
@1639
|
9 years |
mulligan |
changes from today
|
|
|
@1635
|
9 years |
tranquil |
* lists with binders and monads
* Joint.ma and other temprarily …
|
|
|
@1632
|
9 years |
boender |
- strengthened insert_lookup_opt
|
|
|
@1625
|
9 years |
mulligan |
before christmas
|
|
|
@1624
|
9 years |
mulligan |
commit for claudio
|
|
|
@1623
|
9 years |
mulligan |
strange matita issue
|
|
|
@1622
|
9 years |
mulligan |
to avoid conflicts, bug in typechecker?
|
|
|
@1621
|
9 years |
mulligan |
to prevent conflicts
|
|
|
@1620
|
9 years |
sacerdot |
One of the mutual cases of the open proof is practically finished.
|
|
|
@1619
|
9 years |
sacerdot |
Major advancement.
|
|
|
@1616
|
9 years |
sacerdot |
Partially ported to new Matita syntax.
Because of some changes in …
|
|
|
@1615
|
9 years |
sacerdot |
Policy now depends on Assembly and not the other way around.
|
|
|
@1614
|
9 years |
boender |
- split policy from assembly
|
|
|
@1613
|
9 years |
sacerdot |
Coercion moved to Matita standard lib.
|
|
|
@1609
|
9 years |
boender |
- added alias to ASM/BitVectorTrie
- removed double include from …
|
|
|
@1607
|
9 years |
sacerdot |
Porting to new library.
|
|
|
@1606
|
9 years |
sacerdot |
Porting to last library of Matita.
|
|
|
@1604
|
9 years |
mulligan |
for jaap
|
|
|
@1602
|
9 years |
mulligan |
giving up on fetch proofs for time being
|
|
|
@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
|
|
|
@1597
|
9 years |
mulligan |
fixed fetch for jaap
|
|
|
@1593
|
9 years |
boender |
- cleaned up Assembly, moved some definitions elsewhere
|
|
|
@1592
|
9 years |
boender |
- updated definitions to work with programs of maximum 216 instructions
|
|
|
@1591
|
9 years |
mulligan |
work from today
|
|
|
@1588
|
9 years |
sacerdot |
All goals generated by Russell for execute_1* are now closed, mostly …
|
|
|
@1587
|
9 years |
mulligan |
changes from today, including removing indexing of problematic …
|
|
|
@1582
|
9 years |
mulligan |
more added to the proof of execute_1_preinstruction --- ~260 cases now …
|
|
|
@1581
|
9 years |
mulligan |
Dangling de Bruijn pointer when trying to propagate russell to set_arg_1
|
|
|
@1579
|
9 years |
mulligan |
Finished proof with simpler statement, making everything a lot nicer
|
|
|
@1578
|
9 years |
boender |
- proof of termination of policy completed (needs some clean-up work …
|
|
|
@1577
|
9 years |
mulligan |
A lot more cases added to the proof at the bottom of …
|
|
|
@1576
|
9 years |
mulligan |
big changes to proofs, just two small cases remain and a few …
|
|
|
@1575
|
9 years |
mulligan |
Changes to specifications on execute functions
|
|
|
@1573
|
9 years |
mulligan |
more complicated than it appears :(
|
|
|
@1571
|
9 years |
mulligan |
small changes
|
|
|
@1570
|
9 years |
sacerdot |
Dependent type crazyness.
|
|
|
@1567
|
9 years |
mulligan |
more work on big proof, 2.5 cases left
|
|
|
@1564
|
9 years |
sacerdot |
Commit where we use a dependently typed version of bigops.
I am now …
|
|
|
@1562
|
9 years |
mulligan |
new version of assembly, fixed conflict in positivemap.ma, changed …
|
|
|
@1561
|
9 years |
sacerdot |
More dependent types to accomodate the statement.
|
|
|
@1560
|
9 years |
sacerdot |
Complete re-implementation that:
1) assumes no code before the first …
|
|
|
@1558
|
9 years |
sacerdot |
Snapshot before moving things to ASMCosts.ma.
|
|
|
@1557
|
9 years |
sacerdot |
Byte => costlabel
|
|
|
@1556
|
9 years |
mulligan |
submitting to avoid conflicts
|
|
|
@1555
|
9 years |
boender |
- changes to assembly
- added lookup to PositiveMap?
- lightly changed …
|
|
|
@1554
|
9 years |
sacerdot |
Major progress in the proof.
|
|
|
@1553
|
9 years |
boender |
- added lookup_opt_lookup lemma
|
|
|
@1550
|
9 years |
sacerdot |
Repaired after use of Russell for execute_1.
|
|
|
@1549
|
9 years |
mulligan |
removed cruft from costsproof.ma file so claudio can work in parallel
|
|
|
@1548
|
9 years |
sacerdot |
…
|
|
|
@1547
|
9 years |
sacerdot |
Invariant on cost of one execution step strengthened.
|
|
|
@1544
|
9 years |
sacerdot |
StructuredTraces? inhabited for object code.
|
|
|
@1541
|
9 years |
mulligan |
interpret.ma now compiles
|
|
|
@1540
|
9 years |
mulligan |
changes to proof in interrupt.ma
|
|
|
@1538
|
9 years |
mulligan |
changes to execute_1_0 proof
|
|
|
@1534
|
9 years |
mulligan |
committing my changes to interpret to prevent any further conflicts
|
|
|
@1533
|
9 years |
sacerdot |
Proof of execute_1 with Russell completed (up to some daemon used before).
|
|
|
@1530
|
9 years |
campbell |
Update due to Russell changes.
|
|
|
@1528
|
9 years |
campbell |
Update most of Assembly.ma with new syntax and identifier maps.
Change …
|
|
|
@1527
|
9 years |
sacerdot |
More on Russell.
|
|
|
@1526
|
9 years |
sacerdot |
Using Russell to prove some properties.
|
|
|
@1524
|
9 years |
boender |
- adapted files to new Matita syntax
|
|
|
@1522
|
9 years |
mulligan |
changes to preamble and lin to asm pass, resolved conflict in interpret
|
|
|
@1521
|
9 years |
sacerdot |
Syntax change in Matita: change what where => change where what.
|
|
|
@1519
|
9 years |
campbell |
More syntax updates.
|
|
|
@1518
|
9 years |
campbell |
Update to new syntax.
|
|
|
@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 …
|
|
|
@1514
|
9 years |
mulligan |
changes from today. matita keeps dieing
|
|
|
@1511
|
9 years |
mulligan |
proofs, added, changes to execute_1_0 function therefore required to …
|
|
|
@1509
|
9 years |
mulligan |
i hate subtraction over the nats
|
|
|
@1506
|
9 years |
mulligan |
changes to costs proof over weekend
|
|
|
@1503
|
9 years |
mulligan |
inductive type complete
|
|
|
@1502
|
9 years |
mulligan |
changes to inductive defn
|
|
|
@1501
|
9 years |
sacerdot |
We must take in account the labelled_p predicate.
|
|
|