|
|
@1635
|
9 years |
tranquil |
* lists with binders and monads
* Joint.ma and other temprarily …
|
|
|
@1634
|
9 years |
campbell |
Update memory model examples syntax.
|
|
|
@1633
|
9 years |
campbell |
Update Cminor pretty printer and examples.
|
|
|
@1632
|
9 years |
boender |
- strengthened insert_lookup_opt
|
|
|
@1631
|
9 years |
campbell |
Use fact that type environments in Cminor have distinct variables to …
|
|
|
@1630
|
9 years |
campbell |
Remainder of freshness in Clight to Cminor pass.
|
|
|
@1629
|
9 years |
campbell |
Sort out most of the fresh names stuff in Clight to Cminor.
|
|
|
@1628
|
9 years |
campbell |
Show that the universe generated by Clight/fresh.ma is good.
|
|
|
@1627
|
9 years |
campbell |
Add some notions of freshness, and start using them for temporary …
|
|
|
@1626
|
9 years |
campbell |
Add extra type safety in front end. NB: critical freshness parts …
|
|
|
@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.
|
|
|
@1618
|
9 years |
campbell |
Minor updates due to recent changes.
|
|
|
@1617
|
9 years |
campbell |
Note stuff to do on structured traces.
|
|
|
@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.
|
|
|
@1612
|
9 years |
sacerdot |
All library ported to new Matita lib (finally).
|
|
|
@1611
|
9 years |
sacerdot |
All of Cminor now compiles with the latest lib of Matita.
|
|
|
@1610
|
9 years |
sacerdot |
Ported to new lib.
|
|
|
@1609
|
9 years |
boender |
- added alias to ASM/BitVectorTrie
- removed double include from …
|
|
|
@1608
|
9 years |
sacerdot |
Porting to new library still in progress.
|
|
|
@1607
|
9 years |
sacerdot |
Porting to new library.
|
|
|
@1606
|
9 years |
sacerdot |
Porting to last library of Matita.
|
|
|
@1605
|
9 years |
sacerdot |
Porting to last standard library of Matita.
|
|
|
@1604
|
9 years |
mulligan |
for jaap
|
|
|
@1603
|
9 years |
sacerdot |
More proofs ported to new lib.
|
|
|
@1602
|
9 years |
mulligan |
giving up on fetch proofs for time being
|
|
|
@1601
|
9 years |
sacerdot |
Files ported to new version of the standard library.
|
|
|
@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
|
|
|
@1596
|
9 years |
campbell |
RTLabs structured traces: sort out passing of termination proofs around.
|
|
|
@1595
|
9 years |
campbell |
We don't need an explicit termination count when building traces.
|
|
|
@1594
|
9 years |
campbell |
Rework handling of termination information in RTLabs structured traces …
|
|
|
@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
|
|
|
@1590
|
9 years |
tranquil |
* got back to previous implementation of multiplication in RTLabs -> …
|
|
|
@1589
|
9 years |
tranquil |
* turned to argument-less return statements for RTLabs and RTL (there …
|
|
|
@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 …
|
|
|
@1586
|
9 years |
campbell |
RTLabs structured traces: cost labels after jumps.
|
|
|
@1585
|
9 years |
tranquil |
fighting with a bug of the translation from RTL to ERTL
|
|
|
@1584
|
9 years |
tranquil |
* new form of translation written in graphUtilites (mainly as a test …
|
|
|
@1583
|
9 years |
campbell |
More on RTLabs structured traces.
Fixed mistake in structure trace …
|
|
|
@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
|
|
|
@1580
|
9 years |
tranquil |
implemented constant propagation in LTL
cleaned up translations in …
|
|
|
@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
|
|
|
@1574
|
9 years |
campbell |
A little more progress on traces on RTLabs.
|
|
|
@1573
|
9 years |
mulligan |
more complicated than it appears :(
|
|
|
@1572
|
9 years |
tranquil |
* corrected previous bug
* finished propagating immediates
|
|
|
@1571
|
9 years |
mulligan |
small changes
|
|
|
@1570
|
9 years |
sacerdot |
Dependent type crazyness.
|
|
|
@1569
|
9 years |
tranquil |
* added in repository some missing files…
|
|
|
@1568
|
9 years |
tranquil |
* Immediates introduced (but not fully used yet in RTLabs to RTL pass) …
|
|
|
@1567
|
9 years |
mulligan |
more work on big proof, 2.5 cases left
|
|
|
@1566
|
9 years |
campbell |
Pacify changes to destruct tactic.
|
|
|
@1565
|
9 years |
campbell |
Note that RTLabs ought to classify branches as "jumps" (in the …
|
|
|
@1564
|
9 years |
sacerdot |
Commit where we use a dependently typed version of bigops.
I am now …
|
|
|
@1563
|
9 years |
campbell |
A little progress on constructing RTLabs structured traces.
|
|
|
@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 …
|
|
|
@1559
|
9 years |
campbell |
Add a notion of flat traces with evidence for RTLabs.
|
|
|
@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
|
|
|
@1552
|
9 years |
campbell |
Update RTLabs structured trace definition.
|
|
|
@1551
|
9 years |
campbell |
Functions to translate between back-end and front-end values.
|
|
|
@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.
|
|
|
@1546
|
9 years |
tranquil |
added an option to prevent reindexing transformations from taking …
|
|
|
@1545
|
9 years |
campbell |
Use pointer record in front-end.
|
|
|
@1544
|
9 years |
sacerdot |
StructuredTraces? inhabited for object code.
|
|
|
@1543
|
9 years |
tranquil |
deletion of indexed labels branch
|
|
|
@1542
|
9 years |
tranquil |
merge of indexed labels branch
|
|
|
@1541
|
9 years |
mulligan |
interpret.ma now compiles
|
|
|
@1540
|
9 years |
mulligan |
changes to proof in interrupt.ma
|
|
|
@1539
|
9 years |
tranquil |
branch up to date
|
|
|
@1538
|
9 years |
mulligan |
changes to execute_1_0 proof
|
|
|
@1537
|
9 years |
campbell |
A preliminary definition of the abstract status record for RTLabs.
|
|
|
@1536
|
9 years |
campbell |
Use predicates throughout the structured traces.
|
|
|