|
|
@1607
|
8 years |
sacerdot |
Porting to new library.
|
|
|
@1606
|
8 years |
sacerdot |
Porting to last library of Matita.
|
|
|
@1605
|
8 years |
sacerdot |
Porting to last standard library of Matita.
|
|
|
@1604
|
8 years |
mulligan |
for jaap
|
|
|
@1603
|
8 years |
sacerdot |
More proofs ported to new lib.
|
|
|
@1602
|
8 years |
mulligan |
giving up on fetch proofs for time being
|
|
|
@1601
|
8 years |
sacerdot |
Files ported to new version of the standard library.
|
|
|
@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
|
|
|
@1596
|
8 years |
campbell |
RTLabs structured traces: sort out passing of termination proofs around.
|
|
|
@1595
|
8 years |
campbell |
We don't need an explicit termination count when building traces.
|
|
|
@1594
|
8 years |
campbell |
Rework handling of termination information in RTLabs structured traces …
|
|
|
@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
|
|
|
@1590
|
8 years |
tranquil |
* got back to previous implementation of multiplication in RTLabs -> …
|
|
|
@1589
|
8 years |
tranquil |
* turned to argument-less return statements for RTLabs and RTL (there …
|
|
|
@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 …
|
|
|
@1586
|
8 years |
campbell |
RTLabs structured traces: cost labels after jumps.
|
|
|
@1585
|
8 years |
tranquil |
fighting with a bug of the translation from RTL to ERTL
|
|
|
@1584
|
8 years |
tranquil |
* new form of translation written in graphUtilites (mainly as a test …
|
|
|
@1583
|
8 years |
campbell |
More on RTLabs structured traces.
Fixed mistake in structure trace …
|
|
|
@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
|
|
|
@1580
|
8 years |
tranquil |
implemented constant propagation in LTL
cleaned up translations in …
|
|
|
@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
|
|
|
@1574
|
8 years |
campbell |
A little more progress on traces on RTLabs.
|
|
|
@1573
|
8 years |
mulligan |
more complicated than it appears :(
|
|
|
@1572
|
8 years |
tranquil |
* corrected previous bug
* finished propagating immediates
|
|
|
@1571
|
8 years |
mulligan |
small changes
|
|
|
@1570
|
8 years |
sacerdot |
Dependent type crazyness.
|
|
|
@1569
|
8 years |
tranquil |
* added in repository some missing files…
|
|
|
@1568
|
8 years |
tranquil |
* Immediates introduced (but not fully used yet in RTLabs to RTL pass) …
|
|
|
@1567
|
8 years |
mulligan |
more work on big proof, 2.5 cases left
|
|
|
@1566
|
8 years |
campbell |
Pacify changes to destruct tactic.
|
|
|
@1565
|
8 years |
campbell |
Note that RTLabs ought to classify branches as "jumps" (in the …
|
|
|
@1564
|
8 years |
sacerdot |
Commit where we use a dependently typed version of bigops.
I am now …
|
|
|
@1563
|
8 years |
campbell |
A little progress on constructing RTLabs structured traces.
|
|
|
@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 …
|
|
|
@1559
|
8 years |
campbell |
Add a notion of flat traces with evidence for RTLabs.
|
|
|
@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
|
|
|
@1552
|
8 years |
campbell |
Update RTLabs structured trace definition.
|
|
|
@1551
|
8 years |
campbell |
Functions to translate between back-end and front-end values.
|
|
|
@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.
|
|
|
@1546
|
8 years |
tranquil |
added an option to prevent reindexing transformations from taking …
|
|
|
@1545
|
8 years |
campbell |
Use pointer record in front-end.
|
|
|
@1544
|
8 years |
sacerdot |
StructuredTraces? inhabited for object code.
|
|
|
@1543
|
8 years |
tranquil |
deletion of indexed labels branch
|
|
|
@1542
|
8 years |
tranquil |
merge of indexed labels branch
|
|
|
@1541
|
8 years |
mulligan |
interpret.ma now compiles
|
|
|
@1540
|
8 years |
mulligan |
changes to proof in interrupt.ma
|
|
|
@1539
|
8 years |
tranquil |
branch up to date
|
|
|
@1538
|
8 years |
mulligan |
changes to execute_1_0 proof
|
|
|
@1537
|
8 years |
campbell |
A preliminary definition of the abstract status record for RTLabs.
|
|
|
@1536
|
8 years |
campbell |
Use predicates throughout the structured traces.
|
|
|
@1535
|
8 years |
campbell |
Make RTLabs semantics use knowledge that the next instruction always …
|
|
|
@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).
|
|
|
@1532
|
8 years |
campbell |
Remove jump classification from structured traces.
|
|
|
@1531
|
8 years |
campbell |
A notion of abstract structured traces.
|
|
|
@1530
|
8 years |
campbell |
Update due to Russell changes.
|
|
|
@1529
|
8 years |
campbell |
Update RTLabs to RTL with unary operation types.
|
|
|
@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.
|
|
|
@1525
|
8 years |
ayache |
D2.2: function pointers using JMP.
|
|
|
@1524
|
8 years |
boender |
- adapted files to new Matita syntax
|
|
|
@1523
|
8 years |
campbell |
Separate out positive and Z definitions from extralib.ma.
Minor 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.
|
|
|
@1520
|
8 years |
campbell |
Generate cost labels with correct type.
|
|
|
@1519
|
8 years |
campbell |
More syntax updates.
|
|
|
@1518
|
8 years |
campbell |
Update to new syntax.
|
|
|
@1517
|
8 years |
sacerdot |
Ported to syntax of Matita 0.99.1.
|
|
|
@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
|
|
|
@1513
|
8 years |
campbell |
Fix up Clight examples.
|
|
|
@1512
|
8 years |
campbell |
Shorten proof of goal that solves now.
|
|
|
@1511
|
8 years |
mulligan |
proofs, added, changes to execute_1_0 function therefore required to …
|
|
|
@1510
|
8 years |
sacerdot |
All files ported to new dependent inversion.
|
|
|
@1509
|
8 years |
mulligan |
i hate subtraction over the nats
|
|
|
@1508
|
8 years |
tranquil |
branched a version of the plug-in that is compatible with the indexed …
|
|
|