|
|
@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 …
|
|
|
@1507
|
8 years |
tranquil |
* added an option to not use ternary expressions in costs, to …
|
|
|
@1506
|
8 years |
mulligan |
changes to costs proof over weekend
|
|
|
@1505
|
8 years |
ayache |
D2.2: addendum on 16 and 32 bits integer and function pointers support.
|
|
|
@1504
|
8 years |
ayache |
8051 ocaml: bug fix in the labelling of do-whiles.
|
|
|
@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
|
|
|
@1492
|
8 years |
ayache |
Comment in D2.2 -> LINToASM about function pointers.
|
|
|
@1491
|
8 years |
ayache |
Function pointers good and working.
|
|
|
@1490
|
8 years |
ayache |
Function pointers fixed.
|
|
|
@1489
|
8 years |
campbell |
Fix up a couple of lemmas affected by the change to add_with_carries.
|
|
|
@1488
|
8 years |
ayache |
Function pointers in D2.2/8051. Bugged for now.
|
|
|
@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 |
…
|
|
|
@1483
|
8 years |
tranquil |
* implemented a first draft of loop unrolling
* correced bugs in CostExpr?
|
|
|
@1482
|
8 years |
sacerdot |
1. very long standing conflict committed (but don't ask me what the …
|
|
|
@1481
|
8 years |
sacerdot |
Proof fixed. The new standard library does not index any longer the …
|
|
|
@1480
|
8 years |
sacerdot |
Proof changed (to use new automation).
BUG FOUND: automation fails if …
|
|
|
@1479
|
8 years |
boender |
- added insert_lookup_opt
- assembly compiles now
|
|
|
@1478
|
8 years |
sacerdot |
Almost completed (up to is_finals).
|
|
|
@1477
|
8 years |
tranquil |
* corrected a bug
* implemented copy propagation
* enhanced constant …
|
|
|
@1476
|
8 years |
sacerdot |
…
|
|
|
@1475
|
8 years |
sacerdot |
Towards the two fullexec transition systems that represent …
|
|
|