stdpp:fc78a6baa572579f33fe82344077424aaf205c0e commitshttps://gitlab.mpi-sws.org/iris/stdpp/-/commits/fc78a6baa572579f33fe82344077424aaf205c0e2016-04-07T19:09:20+02:00https://gitlab.mpi-sws.org/iris/stdpp/-/commit/fc78a6baa572579f33fe82344077424aaf205c0eMake atomic a boolean predicate.2016-04-07T19:09:20+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/2f42e9103160b1305420374972747c5528d72f6dMake naive_solver deal with some Boolean connectives.2016-03-03T14:00:33+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/7dd32d7d13355459a3f3095508bb8b80981241bcUse new Import/Export syntax everywhere.2016-02-13T12:39:54+01:00Robbert Krebbersmail@robbertkrebbers.nl
Also, make our redefinition of done more robust under different
orders of Importing modules.https://gitlab.mpi-sws.org/iris/stdpp/-/commit/44b18f4df008fefa1d9618d6725a63689942552dShorter names for common math notions.2016-02-11T22:48:51+01:00Robbert Krebbersmail@robbertkrebbers.nl
Also do some minor clean up.https://gitlab.mpi-sws.org/iris/stdpp/-/commit/dcff8ded2b64738c838a552487ae9e4d4630015bUse qualified module names and coqc -Q instead of -R.2015-11-16T11:38:22+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/02f213ce883755c487150fcd89cededc8ea7e8c8Port to Coq 8.5 beta 2.2017-02-01T19:55:16+01:00Robbert Krebbersmail@robbertkrebbers.nl
The port makes the following notable changes:
* The carrier types of separation algebras and integer environments are no
longer in Set. Now they have a type at a fixed type level above Set. This
both works better in 8.5 and makes the formalization more general.
I have tried putting them at polymorphic type levels, but that increased the
compilation time by an order of magnitude.
* I am using a custom f_equal tactic written in Ltac to circumvent bug #4069.
That bug has been fixed, so this custom tactic can be removed when the next
beta of 8.5 is out.https://gitlab.mpi-sws.org/iris/stdpp/-/commit/5a73c4edfb423c4cbead774d288d97cabf71e049Update copyright headers.2015-02-08T19:38:19+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/914f32eec7693c255088060e6f52811f2bd760d8More lenient pointer equality.2014-12-23T20:12:23+01:00Robbert Krebbersmail@robbertkrebbers.nl
Pointer equality is now defined using absolute object offsets. The treatment
is similar to CompCert:
* Equality of pointers in the same object is defined provided the object has
not been deallocated.
* Equality of pointers in different objects is defined provided both pointers
have not been deallocated and both are strict (i.e. not end-of-array).
Thus, pointer equality is defined for all pointers that are not-end-of-array
and have not been deallocated. The following examples have defined behavior:
int x, y;
printf("%d\n", &x == &y);
int *p = malloc(sizeof(int)), *q = malloc(sizeof(int));
printf("%d\n", p == q);
struct S { int a; int b; } s, *r = &s;
printf("%d\n", &s.a + 1 == &(r->b));
The following not:
int x, y;
printf("%d\n", &x + 1 == &y);https://gitlab.mpi-sws.org/iris/stdpp/-/commit/7f9c5994dddd04acb2f8bf4253cf4383453a096bModify typing judgments to depend on a description of the types of objects in2014-08-22T10:10:16+02:00Robbert Krebbersmail@robbertkrebbers.nlmemory instead of the whole memory itself.
This has the following advantages:
* Avoid parametrization in {addresses,pointers,pointer_bits,bits}.v
* Make {base_values,values}.v independent of the memory, this makes better
parallelized compilation possible.
* Allow small memories (e.g. singletons as used in separation logic) with
addresses to objects in another part to be typed.
* Some proofs become easier, because the memory environments are preserved
under many operations (insert, force, lock, unlock).
It also as the following disadvantages:
* At all kinds of places we now have explicit casts from memories to memory
environments. This is kind of ugly. Note, we cannot declare memenv_of as a
Coercion because it is non-uniform.
* It is a bit inefficient with respect to the interpreter, because memory
environments are finite functions instead of proper functions, so calling
memenv_of often (which we do) is not too good.https://gitlab.mpi-sws.org/iris/stdpp/-/commit/bb9d75d9f83c0d250c6267c015dc86adb484bae5Various changes.2014-05-22T10:31:18+02:00Robbert Krebbersmail@robbertkrebbers.nl
* Parametrize refinements with memories. This way, refinements imply typing,
for example [w1 ⊑{Γ,f@m1↦m2} w2 : τ → (Γ,m1) ⊢ w1 : τ]. This relieves us from
various hacks.
* Use addresses instead of index/references pairs for lookup and alter
operations on memories.
* Prove various disjointness properties.https://gitlab.mpi-sws.org/iris/stdpp/-/commit/83f05bf19970b5e75f9e23a80d7229f185b74adeUpdate copyright headers.2014-05-02T22:40:17+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/716f554d652e6865a5dd013a636e8472da630ad3Start integrating memory model with sequence point semantics.2014-05-02T22:35:34+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/64bedf4ca9583aa486805cd24450cb60c273bc6dTwo basic De Morgan like laws for decidable propositions.2013-08-21T14:46:37+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/46304c52633a2bf6c159efb8bc9a6e57e2182c49Misc prelude changes.2013-06-24T10:42:47+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/1f545953461773101d430dec00fb8df1d7d694fdAdd "as ident(H)" to the "case_bool_decide" tactic.2013-05-21T11:26:23+02:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/361308c7b173f353afd99499e8bfcf168fdab1caLots of refactoring. and new results on permutations and list containment.2013-05-07T17:01:37+02:00Robbert Krebbersmail@robbertkrebbers.nl
The refactoring includes:
* Use infix notations for the various list relations
* More consistent naming
* Put lemmas on one line whenever possible
* Change proofs into one-liners when possible
* Make better use of the "Implicit Types" command
* Improve the order of the list module by placing all definitions at the start,
then the proofs, and finally the tactics.
Besides, there is some new machinery for proofs by reflection on lists. It is
used for a decision procedure for permutations and list containment.https://gitlab.mpi-sws.org/iris/stdpp/-/commit/c490d8581c3cefa0dbae505ed465feaf1fbd077bAn axiomatization and implementation of machine integers.2013-03-14T20:13:29+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/415a4f1ca2bf510240bb6a2ec0366a04b17be36fSupport sequence point, add permissions, and update prelude.2013-02-19T13:32:10+01:00Robbert Krebbersmail@robbertkrebbers.nl
Both the operational and axiomatic semantics are extended with sequence points
and a permission system based on fractional permissions. In order to achieve
this, the memory model has been completely revised, and is now built on top
of an abstract interface for permissions.
Apart from these changed, the library on lists and sets has been heavily
extended, and minor changed have been made to other parts of the prelude.https://gitlab.mpi-sws.org/iris/stdpp/-/commit/487cdeadf8fb6850bd209dd4f1f6530e61bae710Some minor cleanup, and more lemmas on prefix/postfixes of lists.2013-02-01T13:28:42+01:00Robbert Krebbersmail@robbertkrebbers.nlhttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/3f3ca628ac094cfe070281905ffab59d6bf1d5ceUpdate to match the article.2013-01-09T20:46:54+01:00Robbert Krebbersmail@robbertkrebbers.nl
The development now corresponds exactly to the FoSSaCS 2013 paper.
Also, the prelude is updated to the one of the master branch.https://gitlab.mpi-sws.org/iris/stdpp/-/commit/507a150aa88377eb834191600f4214cd3379be61Various small changes.2013-01-05T01:28:59+01:00Robbert Krebbersmail@robbertkrebbers.nl
* Define the standard strict order on pre orders.
* Prove that this strict order is well founded for finite sets and finite maps.
We also provide some utilities to compute with well founded recursion.
* Improve the "simplify_option_equality" tactic to handle more cases.
* Axiomatize finiteness of finite maps by translation to lists, instead of by
them having a finite domain.
* Prove many additional properties of finite maps.
* Add many functions and theorems on lists, including: permutations, resize,
filter, ...https://gitlab.mpi-sws.org/iris/stdpp/-/commit/50dfc1488f5f92bfde5dd20cd0d119ce61f5fb63Many relatively small changes.2012-11-12T13:44:48+01:00Robbert Krebbersmail@robbertkrebbers.nl
Most interestingly:
* Use [lia] instead of [omega] everywhere
* More many generic lemmas on the memory to the theory on finite maps.
* Many additional list lemmas.
* A new interface for a monad for collections, which is now also used by the
collection tactics.
* Provide an additional finite collection implementation using unordered lists
without duplicates removed. This implementation forms a monad (just the list
monad in disguise).https://gitlab.mpi-sws.org/iris/stdpp/-/commit/e82cda6cd47ca4a55fa6c203aa1a93e9540c8c3fAdd non-deterministic expressions with side-effects.2012-10-19T14:46:47+02:00Robbert Krebbersmail@robbertkrebbers.nl
The following things have been changed in this revision:
* We now give a small step semantics for expressions. The denotational semantics
only works for side-effect free expressions.
* Dynamically allocated memory through alloc and free is now supported.
* The following expressions are added: assignment, function call, unary
operators, conditional, alloc, and free.
* Some customary induction schemes for expressions are proven.
* The axiomatic semantics (and its interpretation) have been changed in order
to deal with non-deterministic expressions.
* We have added inversion schemes based on small inversions for the operational
semantics. Inversions using these schemes are much faster.
* We improved the statement preservation proof of the operational semantics.
* We now use a variant of SsReflect's [by] and [done], instead of Coq's [now]
and [easy]. The [done] tactic is much faster as it does not perform
inversions.
* Add theory, definitions and notations on vectors.
* Separate theory on contexts.
* Change [Arguments] declarations to ensure better unfolding.https://gitlab.mpi-sws.org/iris/stdpp/-/commit/e79e91f757d9f2ffa7724e843adb9249fc827ae8Add documentation, add license, simplify build process, some reorganization,2012-08-29T21:29:37+02:00Robbert Krebbersmail@robbertkrebbers.nlimprove some definitions, simplify some proofs.https://gitlab.mpi-sws.org/iris/stdpp/-/commit/18669b9259e8eacbf6dcaed25db562008ef3f13cMajor revision of the whole development.2012-08-21T10:50:53+02:00Robbert Krebbersmail@robbertkrebbers.nl
The main changes are:
* Function calls in the operational semantics
* Mutually recursive function calls in the axiomatic semantics
* A general definition of the interpretation of the axiomatic semantics so as
to improve reusability (useful for function calls, and also for expressions
in future versions)
* Type classes for stack independent, memory independent, and memory extensible
assertions, and a lot of instances to automatically derive these properties.
* Many additional lemmas on the memory and more robust tactics to simplify
goals involving is_free and mem_disjoint
* Proof of preservation of statements in the smallstep semantics
* Some new tactics: feed, feed destruct, feed inversion, etc...
* More robust tactic scripts using bullets and structured scripts
* Truncate most lines at 80 charactershttps://gitlab.mpi-sws.org/iris/stdpp/-/commit/5446fba3ac18b0e479269b76675acd6a6e6b3042Initial commit2012-06-11T19:33:56+02:00Robbert Krebbersmail@robbertkrebbers.nl