 16 Nov, 2018 2 commits


Robbert authored
Update the link to std++ See merge request FP/iriscoq!189

Dan Frumin authored

 12 Nov, 2018 1 commit


Robbert Krebbers authored

 11 Nov, 2018 1 commit


Robbert Krebbers authored

 09 Nov, 2018 1 commit


Robbert Krebbers authored

 08 Nov, 2018 3 commits


Ralf Jung authored

Ralf Jung authored

Robbert Krebbers authored

 06 Nov, 2018 1 commit


Robbert Krebbers authored

 01 Nov, 2018 5 commits


Robbert Krebbers authored

Robbert authored
Add `big_opM_union` and `big_sepM_union`. See merge request FP/iriscoq!188

Dan Frumin authored

Ralf Jung authored

Robbert Krebbers authored

 31 Oct, 2018 21 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert authored
Finegrained postconditions for forkedoff threads See merge request FP/iriscoq!182

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
This commit extends the state interpretation with an additional parameter to talk about the number of forkedoff threads, and a fixed postcondition for each forkedoff thread: state_interp : Λstate → list Λobservation → nat → iProp Σ; fork_post : iProp Σ; This way, instead of having `True` as the postcondition of `Fork`, one can have any postcondition, which is then recorded in the state interpretation. The point of keeping track of the postconditions of forkedoff threads, is that we get an (additional) stronger adequacy theorem: Theorem wp_strong_all_adequacy Σ Λ `{invPreG Σ} s e σ1 v vs σ2 φ : (∀ `{Hinv : invG Σ} κs, (={⊤}=> ∃ (stateI : state Λ → list (observation Λ) → nat → iProp Σ) (fork_post : iProp Σ), let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI fork_post in stateI σ1 κs 0 ∗ WP e @ s; ⊤ {{ v, let m := length vs in stateI σ2 [] m ∗ [∗] replicate m fork_post ={⊤,∅}=∗ ⌜ φ v ⌝ }})%I) → rtc erased_step ([e], σ1) (of_val <$> v :: vs, σ2) → φ v. The difference with the ordinary adequacy theorem is that this one only applies once all threads terminated. In this case, one gets back the postconditions `[∗] replicate m fork_post` of all forkedoff threads. In Iron we showed that we can use this mechanism to make sure that all resources are disposed of properly in the presence of forkbased concurrency.

Robbert authored
More principled set of axioms for fancy updates and plainly Closes #164 See merge request FP/iriscoq!184

JacquesHenri Jourdan authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

JacquesHenri Jourdan authored
A specific constructor for injecting values in expressions See merge request FP/iriscoq!175

JacquesHenri Jourdan authored

JacquesHenri Jourdan authored

 29 Oct, 2018 4 commits


JacquesHenri Jourdan authored

Robbert Krebbers authored
Other heap_lang related instances in that file too. Now, the tactics file only contains stuff related to actual tactics.

Robbert Krebbers authored

JacquesHenri Jourdan authored
We add a specific constructor to the type of expressions for injecting values in expressions. The advantage are :  Values can be assumed to be always closed when performing substitutions (even though they could contain free variables, but it turns out it does not cause any problem in the proofs in practice). This means that we no longer need the `Closed` typeclass and everything that comes with it (all the reflectionbased machinery contained in tactics.v is no longer necessary). I have not measured anything, but I guess this would have a significant performance impact.  There is only one constructor for values. As a result, the AsVal and IntoVal typeclasses are no longer necessary: an expression which is a value will always unify with `Val _`, and therefore lemmas can be stated using this constructor. Of course, this means that there are two ways of writing such a thing as "The pair of integers 1 and 2": Either by using the value constructor applied to the pair represented as a value, or by using the expression pair constructor. So we add reduction rules that transform reduced pair, injection and closure expressions into values. At first, this seems weird, because of the redundancy. But in fact, this has some meaning, since the machine migth actually be doing something to e.g., allocate the pair or the closure. These additional steps of computation show up in the proofs, and some additional wp_* tactics need to be called.

 27 Oct, 2018 1 commit


Robbert Krebbers authored
