|
|
|
@2298
|
9 years |
garnier |
WIP: converting switch removal from Z to bitvectors. Does not compile, …
|
|
|
|
@2271
|
9 years |
garnier |
Proof of correction for the semantics of expressions under memory …
|
|
|
|
@2263
|
9 years |
garnier |
Finished proving semantics preservation under memory injections for …
|
|
|
|
@2255
|
9 years |
garnier |
Had to modify the definition of memory injections to prove that …
|
|
|
|
@2253
|
9 years |
campbell |
Cminor to RTLabs is now a total function.
|
|
|
|
@2252
|
9 years |
campbell |
Use the return statement invariant. Restructure the invariants for …
|
|
|
|
@2251
|
9 years |
campbell |
Add new invariant to Cminor that return typs should be respected.
|
|
|
|
@2250
|
9 years |
campbell |
Tidy up Clight to Cminor pass a bit.
|
|
|
|
@2249
|
9 years |
campbell |
Tweak Cminor invariant to be slightly more readable/extendable.
|
|
|
|
@2234
|
9 years |
garnier |
Progress on proving semantics preservation under memory injections.
|
|
|
|
@2232
|
9 years |
campbell |
Remove unused block structure in Cminor.
|
|
|
|
@2231
|
9 years |
garnier |
Various tiny lemmas used in at least two files in the fornt-end.
|
|
|
|
@2227
|
9 years |
garnier |
* New version of the switch removal algorithm, described at the top of …
|
|
|
|
@2219
|
9 years |
campbell |
Speed up cast simplification proof checking a bit.
|
|
|
|
@2203
|
9 years |
campbell |
A general result about simulations of executions.
|
|
|
|
@2202
|
9 years |
campbell |
Start defining equivalent executions.
|
|
|
|
@2201
|
9 years |
campbell |
Forgotten comment update.
|
|
|
|
@2184
|
9 years |
campbell |
Minor fix ups.
|
|
|
|
@2180
|
9 years |
campbell |
Fix off-by-one error in GenMem?.ma.
|
|
|
|
@2177
|
9 years |
campbell |
Tidy up multiplication.
|
|
|
|
@2176
|
9 years |
campbell |
Remove memory spaces other than XData and Code; simplify pointers as a …
|
|
|
|
@2145
|
9 years |
campbell |
Cost labelling doesn't affect interaction.
|
|
|
|
@2134
|
9 years |
campbell |
Split out behavioural equivalence spec for labelling.
|
|
|
|
@2120
|
9 years |
campbell |
Fix victim of alloc unfolding.
|
|
|
|
@2118
|
9 years |
campbell |
Labelling preserves behaviour.
|
|
|
|
@2107
|
9 years |
campbell |
Memory initialisation and program transformations.
|
|
|
|
@2106
|
9 years |
campbell |
Fix up a couple of proofs broken by recent changes.
|
|
|
|
@2105
|
9 years |
campbell |
Show some results about globalenvs and program transformations.
|
|
|
|
@2103
|
9 years |
campbell |
Make transform_*program take a more general transformation to make …
|
|
|
|
@2076
|
9 years |
garnier |
First steps towards a simulation proof for switch removal.
|
|
|
|
@2074
|
9 years |
garnier |
Prophylactic renaming of a relation
|
|
|
|
@2050
|
9 years |
campbell |
Limit some normalization that doesn't seem to like.
|
|
|
|
@2032
|
9 years |
sacerdot |
!! BEWARE: major commit !!
1) [affects everybody]
split for …
|
|
|
|
@2030
|
9 years |
garnier |
Cast simplification was too conservative, now reasonably aggressive.
|
|
|
|
@2019
|
9 years |
campbell |
Split out special induction principle for Clight from soundness file. …
|
|
|
|
@2016
|
9 years |
garnier |
Slight change in simplification strategy to better match the semantics
|
|
|
|
@2011
|
9 years |
garnier |
Minor cleanup.
|
|
|
|
@2009
|
9 years |
garnier |
Proof of simulation completed for singe-step executions.
|
|
|
|
@2000
|
9 years |
campbell |
Fix g.e. glitch in label simulation.
|
|
|
|
@1993
|
9 years |
campbell |
Make front-end memory model only depend on the general definitions by …
|
|
|
|
@1991
|
9 years |
campbell |
Put the front end transformations together and make an example use it.
|
|
|
|
@1988
|
9 years |
campbell |
Abstraction of the memory contents in the memory models is no longer …
|
|
|
|
@1986
|
9 years |
campbell |
Get rid of unused abstraction of Globalenvs.
|
|
|
|
@1974
|
9 years |
garnier |
Progress on the cast simplification proof.
|
|
|
|
@1970
|
9 years |
garnier |
Work-in-progress: correction proof for the cast removal on expressions.
|
|
|
|
@1954
|
9 years |
campbell |
Initial state is in the labelling simulation
(modulo global envs results).
|
|
|
|
@1930
|
9 years |
campbell |
Tidy up labelling simulation stuff a bit.
|
|
|
|
@1922
|
9 years |
campbell |
Main labelling simulation proof complete.
|
|
|
|
@1920
|
9 years |
campbell |
Most of the labelling simulation. Still need to sort out switch …
|
|
|
|
@1915
|
9 years |
garnier |
Correction of a typo in switchRemoval.
|
|
|
|
@1914
|
9 years |
campbell |
Fix bug in Clight semantics that misses goto-labels inside a cost …
|
|
|
|
@1893
|
9 years |
campbell |
Show stronger result about labelling of expressions.
|
|
|
|
@1888
|
9 years |
campbell |
Show that labelling of expressions works ...
after fixing it to match …
|
|
|
|
@1884
|
9 years |
campbell |
Syntax changes to fit Paolo's commit.
|
|
|
|
@1883
|
9 years |
campbell |
Ilias' switch removal code, plus a test.
|
|
|
|
@1878
|
9 years |
campbell |
Enforce typing of constants in front-end, plus binops for RTLabs.
|
|
|
|
@1876
|
9 years |
campbell |
Update Cexec soundness proof.
Change finishes_with predicate to …
|
|
|
|
@1875
|
9 years |
campbell |
Update brief memory model test.
|
|
|
|
@1874
|
9 years |
campbell |
First cut at using back-end memory model throughout.
Note the …
|
|
|
|
@1873
|
9 years |
campbell |
Fix up earlier front-end value conversion work.
|
|
|
|
@1872
|
9 years |
campbell |
Make binary operations in Cminor/RTLabs properly typed.
A few extra …
|
|
|
|
@1871
|
9 years |
campbell |
Change Clight to Cminor compilation to use gotos rather than loops, …
|
|
|
|
@1713
|
9 years |
campbell |
Add a distinguished final state to the front-end languages to match up …
|
|
|
|
@1672
|
9 years |
campbell |
Matita now generates a couple of inversion lemmas that were manually …
|
|
|
|
@1647
|
9 years |
tranquil |
* corrected some notation problems
* adapted Cligth with slight …
|
|
|
|
@1634
|
9 years |
campbell |
Update memory model examples syntax.
|
|
|
|
@1633
|
9 years |
campbell |
Update Cminor pretty printer and examples.
|
|
|
|
@1631
|
10 years |
campbell |
Use fact that type environments in Cminor have distinct variables to …
|
|
|
|
@1630
|
10 years |
campbell |
Remainder of freshness in Clight to Cminor pass.
|
|
|
|
@1629
|
10 years |
campbell |
Sort out most of the fresh names stuff in Clight to Cminor.
|
|
|
|
@1628
|
10 years |
campbell |
Show that the universe generated by Clight/fresh.ma is good.
|
|
|
|
@1627
|
10 years |
campbell |
Add some notions of freshness, and start using them for temporary …
|
|
|
|
@1626
|
10 years |
campbell |
Add extra type safety in front end. NB: critical freshness parts …
|
|
|
|
@1618
|
10 years |
campbell |
Minor updates due to recent changes.
|
|
|
|
@1612
|
10 years |
sacerdot |
All library ported to new Matita lib (finally).
|
|
|
|
@1608
|
10 years |
sacerdot |
Porting to new library still in progress.
|
|
|
|
@1605
|
10 years |
sacerdot |
Porting to last standard library of Matita.
|
|
|
|
@1603
|
10 years |
sacerdot |
More proofs ported to new lib.
|
|
|
|
@1599
|
10 years |
sacerdot |
Start of merging of stuff into the standard library of Matita.
|
|
|
|
@1566
|
10 years |
campbell |
Pacify changes to destruct tactic.
|
|
|
|
@1545
|
10 years |
campbell |
Use pointer record in front-end.
|
|
|
|
@1521
|
10 years |
sacerdot |
Syntax change in Matita: change what where => change where what.
|
|
|
|
@1516
|
10 years |
sacerdot |
Ported to syntax of Matita 0.99.1.
|
|
|
|
@1515
|
10 years |
campbell |
Add type of maps on positive binary numbers, and use them for …
|
|
|
|
@1513
|
10 years |
campbell |
Fix up Clight examples.
|
|
|
|
@1510
|
10 years |
sacerdot |
All files ported to new dependent inversion.
|
|
|
|
@1489
|
10 years |
campbell |
Fix up a couple of lemmas affected by the change to add_with_carries.
|
|
|
|
@1410
|
10 years |
campbell |
Remove a few old workarounds.
|
|
|
|
@1401
|
10 years |
ricciott |
Changes concerning the new behavior of destruct.
|
|
|
|
@1369
|
10 years |
campbell |
Put type information into front-end unary ops.
Slight change to …
|
|
|
|
@1352
|
10 years |
sacerdot |
This commit is made necessary by the last Matita change.
Inclusion is …
|
|
|
|
@1351
|
10 years |
campbell |
Tidy up some loose ends from the invariants branch merge.
|
|
|
|
@1350
|
10 years |
sacerdot |
Porting to latest destruct tactic.
Note: the tactics has a few …
|
|
|
|
@1344
|
10 years |
sacerdot |
Ported to new destruct.
|
|
|
|
@1342
|
10 years |
sacerdot |
The new auto is much more powerful.
|
|
|
|
@1336
|
10 years |
sacerdot |
Ported to new Matita destruct/inversion.
One lemma fails at qed. …
|
|
|
|
@1332
|
10 years |
campbell |
Summation example updated (needs computational K).
|
|
|
|
@1316
|
10 years |
campbell |
Merge in id-lookup-branch to trunk.
|
|
|
|
@1276
|
10 years |
campbell |
Support for replacing operations with runtime support functions in …
|
|
|
|
@1244
|
10 years |
campbell |
Sort out Clight semantics equivalence proof for new SmallstepExec?.
|
|
|
|
