|
|
|
@1993
|
8 years |
campbell |
Make front-end memory model only depend on the general definitions by …
|
|
|
|
@1988
|
8 years |
campbell |
Abstraction of the memory contents in the memory models is no longer …
|
|
|
|
@1987
|
8 years |
campbell |
Move BEValues to common to reflect their use in the memory model for …
|
|
|
|
@1986
|
8 years |
campbell |
Get rid of unused abstraction of Globalenvs.
|
|
|
|
@1976
|
8 years |
tranquil |
* monads: just changed some defs, which had to be propagated in some …
|
|
|
|
@1964
|
8 years |
tranquil |
introduced as_label_of_cost and adapted accordingly. Equality of cost …
|
|
|
|
@1954
|
8 years |
campbell |
Initial state is in the labelling simulation
(modulo global envs results).
|
|
|
|
@1949
|
8 years |
tranquil |
* lemma trace rel to eq flatten trace
* some more properties of …
|
|
|
|
@1944
|
8 years |
sacerdot |
common/StructuredTraces no longer depends on ASM/AbstractStatus (again)
|
|
|
|
@1939
|
8 years |
mulligan |
Changes to get things to compile and to avoid the dependency …
|
|
|
|
@1938
|
8 years |
sacerdot |
Definitions moved to the right places, now everything compiles again.
|
|
|
|
@1935
|
8 years |
mulligan |
Generalized some lemma in ASM/CostsProof.ma to work on abstract …
|
|
|
|
@1930
|
8 years |
campbell |
Tidy up labelling simulation stuff a bit.
|
|
|
|
@1928
|
8 years |
mulligan |
Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should …
|
|
|
|
@1927
|
8 years |
mulligan |
Reduced complexity of good_program predicate, ported to new notion of …
|
|
|
|
@1926
|
8 years |
tranquil |
* added as_label to abstract status, with as_costed defined with it. …
|
|
|
|
@1921
|
8 years |
mulligan |
Horror proof mostly finished (compiles all way until end of CostsProof?.ma).
|
|
|
|
@1920
|
8 years |
campbell |
Most of the labelling simulation. Still need to sort out switch …
|
|
|
|
@1918
|
8 years |
tranquil |
using listb.ma now
|
|
|
|
@1917
|
8 years |
tranquil |
predicate for unrepeating traces, fused final_abstract_status with …
|
|
|
|
@1908
|
8 years |
fguidi |
notation fixup following last commit of matita
we shifted the levels …
|
|
|
|
@1902
|
8 years |
mulligan |
Reverted needless changes to StructuredTraces?
|
|
|
|
@1901
|
8 years |
mulligan |
Slight changes to StructuredTraces?: should not change too much
|
|
|
|
@1882
|
8 years |
tranquil |
big update, alas incomplete:
joint changed a bit, and all BE languages …
|
|
|
|
@1881
|
8 years |
campbell |
Resurrect version of exec_up_to which shows the final state.
|
|
|
|
@1880
|
8 years |
campbell |
Show that RTLabs flat traces are determined by their starting state, …
|
|
|
|
@1878
|
8 years |
campbell |
Enforce typing of constants in front-end, plus binops for RTLabs.
|
|
|
|
@1876
|
8 years |
campbell |
Update Cexec soundness proof.
Change finishes_with predicate to …
|
|
|
|
@1874
|
8 years |
campbell |
First cut at using back-end memory model throughout.
Note the …
|
|
|
|
@1873
|
8 years |
campbell |
Fix up earlier front-end value conversion work.
|
|
|
|
@1872
|
8 years |
campbell |
Make binary operations in Cminor/RTLabs properly typed.
A few extra …
|
|
|
|
@1812
|
8 years |
campbell |
Provide a combined type for terminating and non-terminating structured …
|
|
|
|
@1808
|
8 years |
campbell |
Create a Prop version of the non-terminating structured traces so that …
|
|
|
|
@1806
|
8 years |
campbell |
Show that we could construct RTLabs non-terminating structured traces …
|
|
|
|
@1783
|
8 years |
campbell |
Remove junk from non-terminating structured traces.
|
|
|
|
@1709
|
8 years |
mulligan |
Changes to the execution of the MOVC instruction
|
|
|
|
@1658
|
8 years |
mulligan |
asm costs changes from today
|
|
|
|
@1654
|
8 years |
campbell |
Corrections to structured trace definitions (see the mailing list). …
|
|
|
|
@1652
|
8 years |
campbell |
Forgot to apply 1583 to non-terminating case.
|
|
|
|
@1647
|
8 years |
tranquil |
* corrected some notation problems
* adapted Cligth with slight …
|
|
|
|
@1640
|
8 years |
tranquil |
* finished fork of semantics.ma
* unification of Errors under the …
|
|
|
|
@1635
|
8 years |
tranquil |
* lists with binders and monads
* Joint.ma and other temprarily …
|
|
|
|
@1631
|
8 years |
campbell |
Use fact that type environments in Cminor have distinct variables to …
|
|
|
|
@1627
|
8 years |
campbell |
Add some notions of freshness, and start using them for temporary …
|
|
|
|
@1626
|
8 years |
campbell |
Add extra type safety in front end. NB: critical freshness parts …
|
|
|
|
@1609
|
8 years |
boender |
- added alias to ASM/BitVectorTrie
- removed double include from …
|
|
|
|
@1608
|
8 years |
sacerdot |
Porting to new library still in progress.
|
|
|
|
@1601
|
8 years |
sacerdot |
Files ported to new version of the 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
|
|
|
|
@1583
|
8 years |
campbell |
More on RTLabs structured traces.
Fixed mistake in structure trace …
|
|
|
|
@1574
|
8 years |
campbell |
A little more progress on traces on RTLabs.
|
|
|
|
@1566
|
8 years |
campbell |
Pacify changes to destruct tactic.
|
|
|
|
@1562
|
8 years |
mulligan |
new version of assembly, fixed conflict in positivemap.ma, changed …
|
|
|
|
@1555
|
8 years |
boender |
- changes to assembly
- added lookup to PositiveMap?
- lightly changed …
|
|
|
|
@1551
|
8 years |
campbell |
Functions to translate between back-end and front-end values.
|
|
|
|
@1545
|
8 years |
campbell |
Use pointer record in front-end.
|
|
|
|
@1544
|
8 years |
sacerdot |
StructuredTraces? inhabited for object code.
|
|
|
|
@1536
|
8 years |
campbell |
Use predicates throughout the structured traces.
|
|
|
|
@1535
|
8 years |
campbell |
Make RTLabs semantics use knowledge that the next instruction always …
|
|
|
|
@1532
|
8 years |
campbell |
Remove jump classification from structured traces.
|
|
|
|
@1531
|
8 years |
campbell |
A notion of abstract structured traces.
|
|
|
|
@1523
|
8 years |
campbell |
Separate out positive and Z definitions from extralib.ma.
Minor syntax …
|
|
|
|
@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 …
|
|
|
|
@1512
|
8 years |
campbell |
Shorten proof of goal that solves now.
|
|
|
|
@1510
|
8 years |
sacerdot |
All files ported to new dependent inversion.
|
|
|
|
@1480
|
8 years |
sacerdot |
Proof changed (to use new automation).
BUG FOUND: automation fails if …
|
|
|
|
@1465
|
8 years |
sacerdot |
Dead code removed.
|
|
|
|
@1410
|
8 years |
campbell |
Remove a few old workarounds.
|
|
|
|
@1401
|
8 years |
ricciott |
Changes concerning the new behavior of destruct.
|
|
|
|
@1395
|
8 years |
sacerdot |
1) New versions of pointer_of_beval/beval_of_pointer with a stricter …
|
|
|
|
@1369
|
8 years |
campbell |
Put type information into front-end unary ops.
Slight change to …
|
|
|
|
@1368
|
8 years |
sacerdot |
A bug in the clear tactic makes the previous (correct) commit wrong. …
|
|
|
|
@1367
|
8 years |
sacerdot |
Proof improvement, still somehow a bit slow.
|
|
|
|
@1355
|
8 years |
sacerdot |
monadic fold_lefti added
|
|
|
|
@1353
|
8 years |
sacerdot |
This commit is made necessary by the last Matita change.
Inclusion is …
|
|
|
|
@1351
|
8 years |
campbell |
Tidy up some loose ends from the invariants branch merge.
|
|
|
|
@1350
|
8 years |
sacerdot |
Porting to latest destruct tactic.
Note: the tactics has a few …
|
|
|
|
@1347
|
8 years |
campbell |
Remove obsolete definitions.
|
|
|
|
@1339
|
8 years |
sacerdot |
Automation is now stronger.
|
|
|
|
@1316
|
8 years |
campbell |
Merge in id-lookup-branch to trunk.
|
|
|
|
@1268
|
8 years |
sacerdot |
1) AST/Identifier.ma no longer used, utilities/IdentifierTools no …
|
|
|
|
@1253
|
8 years |
mulligan |
uses.ma finished
|
|
|
|
@1233
|
8 years |
sacerdot |
1) Ported to Brian's new dependent type for fullexec
2) Universe level …
|
|
|
|
@1231
|
8 years |
campbell |
Change SmallstepExec? so that states can depend on global information. …
|
|
|
|
@1225
|
8 years |
campbell |
Missing ; in proof
|
|
|
|
@1224
|
8 years |
sacerdot |
Type of programs in common/AST made more dependent.
In particular, the …
|
|
|
|
@1215
|
8 years |
sacerdot |
1) Added shifting directly on pointers
2) More temporary axioms closed.
|
|
|
|
@1214
|
8 years |
sacerdot |
res_to_opt function added to common/Errors and used in joint/semantics …
|
|
|
|
@1213
|
8 years |
sacerdot |
1) New values (joint/BEValues.ma) and memory model for the back-ends
…
|
|
|
|
@1181
|
8 years |
mulligan |
changed smallstep exec in order to remove matita bug (superposition.ml …
|
|
|
|
@1139
|
8 years |
campbell |
Shift init_data out of generic program record so that it only appears …
|
|
|
|
@1129
|
8 years |
mulligan |
removed conversions between Register and register
|
|
|
|
@1125
|
8 years |
sacerdot |
Monadic mfold_left2 added.
|
|
|
|
@1092
|
8 years |
campbell |
Some minor definitions for identifiers and lists.
|
|
|
|
@1082
|
8 years |
mulligan |
work from today on ertl -> ltl pass
|
|
|
|
@1080
|
8 years |
mulligan |
more added
|
|
|
|
@1077
|
8 years |
mulligan |
ack, dependent types are scary
|
|
|
|
@1072
|
8 years |
campbell |
Use not equals form of showing entry/exit labels.
|
|
|
|
