 25 Oct, 2017 4 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
I have reimplemented the tactic for introduction of ∀s/pures using type classes, which directly made it much more modular.

Robbert Krebbers authored
The advantage is that we can directly use a Coq introduction pattern `cpat` to perform actions to the pure assertion. Before, this had to be done in several steps: iDestruct ... as "[Htmp ...]"; iDestruct "Htmp" as %cpat. That is, one had to introduce a temporary name. I expect this to be quite useful in various developments as many of e.g. our invariants are written as: ∃ x1 .. x2, ⌜ pure stuff ⌝ ∗ spacial stuff.

 19 Oct, 2017 3 commits
 10 Oct, 2017 4 commits


Robbert Krebbers authored

Ralf Jung authored

Dan Frumin authored

Ralf Jung authored

 09 Oct, 2017 1 commit


Ralf Jung authored

 05 Oct, 2017 1 commit


Robbert Krebbers authored

 04 Oct, 2017 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 28 Sep, 2017 1 commit


Robbert Krebbers authored

 27 Sep, 2017 4 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
This causes a bit of backwards incompatibility: it may now succeed with later stripping below unlocked/TC transparent definitions. This problem actually occured for `wsat`.

Ralf Jung authored

 26 Sep, 2017 3 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
We used to normalize the goal, and then checked whether it was of a certain shape. Since `uPred_valid P` normalized to `True ⊢ P`, there was no way of making a distinction between the two, hence `True ⊢ P` was treated as `uPred_valid P`. In this commit, I use type classes to check whether the goal is of a certain shape. Since we declared `uPred_valid` as `Typeclasses Opaque`, we can now make a distinction between `True ⊢ P` and `uPred_valid P`.

 25 Sep, 2017 13 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
This problem has been reported by Léon Gondelman. Before, when using, for example wp_alloc, in an expression like: ref (ref v) It would apply `tac_wp_alloc` to the outermost ref, after which it fails to establish that the argument `ref v` is a value. In this commit, other evaluation positions will be tried whenever it turn out that the argument of the construct is not a value. The same applies to store/cas/... I have implemented this by making use of the new `IntoVal` class.

Dan Frumin authored

Dan Frumin authored
Expression `e` such that `to_val e = Some v` is in the context gets reflected into value `v` together with the proof that `to_val e = Some v`. This is helpful for substitution and for `solve_to_val` operating on the reflected syntax.

Dan Frumin authored

Dan Frumin authored
This way `IntoLaterNEnvs` is ought to be computed less frequently

Dan Frumin authored

Robbert Krebbers authored
The tactic was doing something weird and only once used.

Robbert Krebbers authored
 Get rid of wp_finish, which was a hack.  Write the wp_ tactics for stateful steps in the same style as wp_pure, i.e. by taking the context into account.  Make use of the context K in wp_pure.

Dan Frumin authored

Dan Frumin authored
Instead of writing a separate tactic lemma for each pure reduction, there is a single tactic lemma for performing all of them. The instances of PureExec can be shared between WP tactics and, e.g. symbolic execution in the ghost threadpool

Robbert Krebbers authored
Typeclass search gets less confused when this version is used, also, we had the same for `wp_bind` already.

 24 Sep, 2017 1 commit


Robbert Krebbers authored

 21 Sep, 2017 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 20 Sep, 2017 1 commit


Robbert Krebbers authored
