|
|
@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.
|
|
|
@1500
|
9 years |
sacerdot |
Proof sketch for one of the two main proofs.
|
|
|
@1499
|
9 years |
mulligan |
part way through main statement transcription
|
|
|
@1498
|
9 years |
mulligan |
added new file for proof that costs are preserved at asm level
|
|
|
@1497
|
9 years |
mulligan |
a bit of tidying up, removing dead code, etc.
|
|
|
@1496
|
9 years |
mulligan |
problem fixed with tactics missing a semicolon to stop greedy parsing
|
|
|
@1495
|
9 years |
mulligan |
proper calculation of costs
|
|
|
@1494
|
9 years |
mulligan |
changes to get everything compiling again
|
|
|
@1493
|
9 years |
mulligan |
finished well labeled check, up to injectivity of the label map
|
|
|
@1489
|
9 years |
campbell |
Fix up a couple of lemmas affected by the change to add_with_carries.
|
|
|
@1487
|
9 years |
mulligan |
committing some code for well labelling
|
|
|
@1486
|
9 years |
mulligan |
finished asm costs
|
|
|
@1485
|
9 years |
sacerdot |
Less nice definitiion of add_with_carries that avoids a quadratic …
|
|
|
@1484
|
9 years |
sacerdot |
…
|
|
|
@1482
|
9 years |
sacerdot |
1. very long standing conflict committed (but don't ask me what the …
|
|
|
@1481
|
9 years |
sacerdot |
Proof fixed. The new standard library does not index any longer the …
|
|
|
@1480
|
9 years |
sacerdot |
Proof changed (to use new automation).
BUG FOUND: automation fails if …
|
|
|
@1479
|
9 years |
boender |
- added insert_lookup_opt
- assembly compiles now
|
|
|
@1478
|
9 years |
sacerdot |
Almost completed (up to is_finals).
|
|
|
@1476
|
9 years |
sacerdot |
…
|
|
|
@1475
|
9 years |
sacerdot |
Towards the two fullexec transition systems that represent …
|
|
|
@1474
|
9 years |
mulligan |
adding missing asmcosts file for computing the costs of an assembly …
|
|
|
@1472
|
9 years |
mulligan |
moved proof utils to erasure.ma
|
|
|
@1471
|
9 years |
mulligan |
finished erasure and generalised so as to work on arbitrary joint programs
|
|
|
@1470
|
9 years |
mulligan |
finished, pretty ugly though as matita's disambiguation is a …
|
|
|
@1469
|
9 years |
mulligan |
finished new relabelling for graphs subject to one axiom closed
|
|
|
@1467
|
9 years |
mulligan |
small change, adding entry and exit labels into the internal function, …
|
|
|
@1466
|
9 years |
mulligan |
erasure for graph based joint languages almost complete
|
|
|
@1465
|
9 years |
sacerdot |
Dead code removed.
|
|
|
@1464
|
9 years |
campbell |
Use unification hints to simplify the graph monotonicity proofs.
|
|
|
@1463
|
9 years |
mulligan |
added erasure for lin
|
|
|
@1461
|
9 years |
mulligan |
rewrote erasure for assembly programs
|
|
|
@1460
|
9 years |
mulligan |
most of cost label erasure for assembly language complete, with one …
|
|
|
@1459
|
9 years |
boender |
- moved stronger occurs_exactly_once lemma to its proper place in …
|
|
|
@1458
|
9 years |
mulligan |
added skeleton file for erasure function for joint languages
|
|
|
@1457
|
9 years |
sacerdot |
Bug fixed: when calling an internal function, the pc block is now set …
|
|
|
@1453
|
9 years |
sacerdot |
…
|
|
|
@1452
|
9 years |
sacerdot |
Bug fixed: labels MUST be represented as pointers whose block is the …
|
|
|
@1451
|
9 years |
sacerdot |
1. All axioms in LIN/semantics.ma closed
2. succ_pc and …
|
|
|
@1450
|
9 years |
sacerdot |
Disambiguation problem avoided.
|
|
|
@1431
|
9 years |
sacerdot |
Back-end todo (in Italian only, sorry...)
|
|
|
@1430
|
9 years |
sacerdot |
Bug fixed: push/pop must work on the isp (now added).
Note: the sp is …
|
|
|
@1429
|
9 years |
sacerdot |
Useless and removed.
|
|
|
@1426
|
9 years |
boender |
removed axiom
|
|
|
@1425
|
9 years |
mulligan |
changes to the fixpoint calculation in ertl
|
|
|
@1424
|
9 years |
sacerdot |
1. fold function over BitVectorTries? moved from ERTLToLTL to …
|
|
|
@1423
|
9 years |
sacerdot |
- spill no longer used
- BUG IN Interference: generating the destruct …
|
|
|
@1419
|
9 years |
sacerdot |
All axioms closed.
|
|
|
@1417
|
9 years |
boender |
- proved that jumps always increase - this should make termination easy
|
|
|
@1416
|
9 years |
sacerdot |
Maps from hardware registers to beval now implemented in ASM/I8051 (in …
|
|
|
@1415
|
9 years |
sacerdot |
1. hwreg_store/retrieve no longer returns a res (but it is still …
|
|
|
@1412
|
9 years |
sacerdot |
Tailcalls (via ids or pointers) to internal functions implemented. …
|
|
|
@1411
|
9 years |
sacerdot |
1. sem_params2 splitted into sem_params1 + sem_params2 to take out the …
|
|
|
@1410
|
9 years |
campbell |
Remove a few old workarounds.
|
|
|
@1408
|
9 years |
sacerdot |
1. Added joint/BEGlobalenvs that is a modification of …
|
|
|
@1404
|
9 years |
boender |
- reworked + added
- added an axiom to arithmetic, but should be provable
|
|
|
@1401
|
9 years |
ricciott |
Changes concerning the new behavior of destruct.
|
|
|
@1396
|
9 years |
sacerdot |
Proof obligation closed.
|
|
|
@1395
|
9 years |
sacerdot |
1) New versions of pointer_of_beval/beval_of_pointer with a stricter …
|
|
|
@1393
|
9 years |
boender |
- added invariant for policy trie to assembly
- change (syntax only) …
|
|
|
@1390
|
9 years |
sacerdot |
All fetch_result implementations have been factorized out, leaving …
|
|
|
@1389
|
9 years |
sacerdot |
One more axiom closed.
|
|
|
@1388
|
9 years |
sacerdot |
fetch_result implemented for ERTL. This required a different …
|
|
|
@1387
|
9 years |
sacerdot |
Further simplification *params1 no longer used.
|
|
|
@1386
|
9 years |
sacerdot |
Structure of semantic parameters simplified.
|
|
|
@1385
|
9 years |
sacerdot |
1. fetch_result and pop_frame now takes the genv in input
2. …
|
|
|
@1384
|
9 years |
sacerdot |
* fetch_ra taken out of pop_frame again since it is used uniformly and …
|
|
|
@1383
|
9 years |
sacerdot |
Potential bug fixed and bug found: the way pointers and labels are put …
|
|
|
@1382
|
9 years |
sacerdot |
- succ_pc generalized to return a res (necessary for LIN semantics)
- …
|
|
|
@1381
|
9 years |
sacerdot |
Old commented out code removed.
|
|
|
@1380
|
9 years |
sacerdot |
LTL and LIN semantics factorized out in joint_LTL_LIN_semantics.ma. …
|
|
|
@1379
|
9 years |
sacerdot |
Invariant on LIN code removed. In Paris it was decided that a simpler …
|
|
|
@1378
|
9 years |
sacerdot |
New file LIN/joint_LTL_LIN.ma to factorize out the syntactic …
|
|
|
@1377
|
9 years |
sacerdot |
pop_frame now incorporates the fetch_result (that made sense only for …
|
|
|
@1376
|
9 years |
sacerdot |
Stack deallocation for RTL implemented in pop_frame.
|
|
|
@1372
|
9 years |
sacerdot |
save_frame now takes the stacksize to allow RTL to allocate the stack frame
|
|
|
@1371
|
9 years |
sacerdot |
save_frame changed to accept also the formal/actual argument pairs, …
|
|
|
@1369
|
9 years |
campbell |
Put type information into front-end unary ops.
Slight change to …
|
|
|
@1368
|
9 years |
sacerdot |
A bug in the clear tactic makes the previous (correct) commit wrong. …
|
|
|
@1367
|
9 years |
sacerdot |
Proof improvement, still somehow a bit slow.
|
|
|
@1363
|
9 years |
boender |
- done stuff with create_label_trie
|
|
|
@1359
|
9 years |
sacerdot |
1. more work on the RTL semantics
2. changes to joint/semantics to …
|
|
|
@1358
|
9 years |
mulligan |
got rtlabs to rtl compiling, foldi_strong needs examining
|
|
|
@1356
|
9 years |
mulligan |
deleted redundant directory. added outlines for both reports, and …
|
|
|
@1355
|
9 years |
sacerdot |
monadic fold_lefti added
|
|
|
@1354
|
9 years |
sacerdot |
One axiom closed.
|
|
|
@1353
|
9 years |
sacerdot |
This commit is made necessary by the last Matita change.
Inclusion is …
|
|
|
@1352
|
9 years |
sacerdot |
This commit is made necessary by the last Matita change.
Inclusion is …
|
|
|
@1351
|
9 years |
campbell |
Tidy up some loose ends from the invariants branch merge.
|
|
|
@1350
|
9 years |
sacerdot |
Porting to latest destruct tactic.
Note: the tactics has a few …
|
|
|
@1348
|
9 years |
sacerdot |
…
|
|
|
@1347
|
9 years |
campbell |
Remove obsolete definitions.
|
|
|
@1344
|
9 years |
sacerdot |
Ported to new destruct.
|
|
|
@1343
|
9 years |
mulligan |
fixed some bugs in the translation
|
|
|
@1342
|
9 years |
sacerdot |
The new auto is much more powerful.
|
|
|
@1341
|
9 years |
sacerdot |
Empty directory removed.
|
|
|
@1339
|
9 years |
sacerdot |
Automation is now stronger.
|
|
|