Commit 3d135daa authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'ralf/inv_heap' into 'master'

heap_lang lifting: instantiate inv_heapG and inv_heap_inv

See merge request !429
parents 41400739 48787e36
Pipeline #28343 passed with stage
in 16 minutes and 34 seconds
...@@ -7,20 +7,28 @@ Coq development, but not every API-breaking change is listed. Changes marked ...@@ -7,20 +7,28 @@ Coq development, but not every API-breaking change is listed. Changes marked
**Changes in the theory of Iris itself:** **Changes in the theory of Iris itself:**
* [#] Redefine invariants as "semantic invariants" so that they support * [#] Redefined invariants as "semantic invariants" so that they support
splitting and other forms of weakening. splitting and other forms of weakening.
* Updated the strong variant of the opening lemma for cancellable invariants * Updated the strong variant of the opening lemma for cancellable invariants
to match that of regular invariants, where you can pick the mask at a later time. to match that of regular invariants, where you can pick the mask at a later time.
**Changes in program logic:** **Changes in program logic:**
* In the axiomatization of ectx languages we replace the axiom of positivity of * In the axiomatization of ectx languages we replaced the axiom of positivity of
context composition with an axiom that says if `fill K e` takes a head step, context composition with an axiom that says if `fill K e` takes a head step,
then either `K` is the empty evaluation context or `e` is a value. then either `K` is the empty evaluation context or `e` is a value.
* Added a library for "invariant locations": heap locations that will not be * Added a library for "invariant locations": heap locations that will not be
deallocated (i.e., they are GC-managed) and satisfy some pure, Coq-level deallocated (i.e., they are GC-managed) and satisfy some pure, Coq-level
invariant. See `iris.base_logic.lib.gen_inv_heap` for details. invariant. See `iris.base_logic.lib.gen_inv_heap` for details.
**Changes in heap_lang:**
* Added a fraction to the heap_lang `array` assertion.
* Added array_copy library for copying and cloning arrays.
* Added the ghost state for "invariant locations" to `heapG`. This affects the
statement of `heap_adequacy`, which is now responsible for initializing the
"invariant locations" invariant.
**Changes in Coq:** **Changes in Coq:**
* Added support for Coq 8.10 and Coq 8.11; dropped support for Coq 8.7 and Coq 8.8. * Added support for Coq 8.10 and Coq 8.11; dropped support for Coq 8.7 and Coq 8.8.
...@@ -180,11 +188,6 @@ s/\bauth_both_frac_op\b/auth_both_op/g ...@@ -180,11 +188,6 @@ s/\bauth_both_frac_op\b/auth_both_op/g
' $(find theories -name "*.v") ' $(find theories -name "*.v")
``` ```
**Changes in heap_lang:**
* Added a fraction to the heap_lang `array` assertion.
* Added array_copy library for copying and cloning arrays.
## Iris 3.2.0 (released 2019-08-29) ## Iris 3.2.0 (released 2019-08-29)
The highlight of this release is the completely re-engineered interactive proof The highlight of this release is the completely re-engineered interactive proof
......
...@@ -221,7 +221,7 @@ Section tests. ...@@ -221,7 +221,7 @@ Section tests.
End tests. End tests.
Section notation_tests. Section notation_tests.
Context `{!heapG Σ, inv_heapG loc val Σ}. Context `{!heapG Σ}.
(* Make sure these parse and type-check. *) (* Make sure these parse and type-check. *)
Lemma inv_mapsto_own_test (l : loc) : l _(λ _, True) #5. Abort. Lemma inv_mapsto_own_test (l : loc) : l _(λ _, True) #5. Abort.
...@@ -291,4 +291,4 @@ Section error_tests. ...@@ -291,4 +291,4 @@ Section error_tests.
End error_tests. End error_tests.
Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (λ v _, v = #2). Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (λ v _, v = #2).
Proof. eapply (heap_adequacy heapΣ)=> ?. by apply heap_e_spec. Qed. Proof. eapply (heap_adequacy heapΣ)=> ?. iIntros "_". by iApply heap_e_spec. Qed.
...@@ -124,7 +124,7 @@ Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ]. ...@@ -124,7 +124,7 @@ Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ].
(** This lemma implicitly shows that these functors are enough to meet (** This lemma implicitly shows that these functors are enough to meet
all library assumptions. *) all library assumptions. *)
Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True). Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
Proof. apply (heap_adequacy clientΣ)=> ?. apply client_safe. Qed. Proof. apply (heap_adequacy clientΣ)=> ?. iIntros "_". iApply client_safe. Qed.
(* Since we check the output of the test files, this means (* Since we check the output of the test files, this means
our test suite will fail if we ever accidentally add an axiom our test suite will fail if we ever accidentally add an axiom
......
...@@ -142,4 +142,4 @@ Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ]. ...@@ -142,4 +142,4 @@ Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ].
(** This lemma implicitly shows that these functors are enough to meet (** This lemma implicitly shows that these functors are enough to meet
all library assumptions. *) all library assumptions. *)
Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True). Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
Proof. apply (heap_adequacy clientΣ)=> ?. apply client_safe. Qed. Proof. apply (heap_adequacy clientΣ)=> ?. iIntros "_". iApply client_safe. Qed.
...@@ -113,7 +113,7 @@ Section to_inv_heap. ...@@ -113,7 +113,7 @@ Section to_inv_heap.
Qed. Qed.
End to_inv_heap. End to_inv_heap.
Lemma inv_heap_init {L V : Type} `{Countable L, !invG Σ, !gen_heapG L V Σ, !inv_heapPreG L V Σ} E: Lemma inv_heap_init (L V : Type) `{Countable L, !invG Σ, !gen_heapG L V Σ, !inv_heapPreG L V Σ} E :
|==> _ : inv_heapG L V Σ, |={E}=> inv_heap_inv L V. |==> _ : inv_heapG L V Σ, |={E}=> inv_heap_inv L V.
Proof. Proof.
iMod (own_alloc ( (to_inv_heap ))) as (γ) "H●". iMod (own_alloc ( (to_inv_heap ))) as (γ) "H●".
......
...@@ -7,23 +7,25 @@ Set Default Proof Using "Type". ...@@ -7,23 +7,25 @@ Set Default Proof Using "Type".
Class heapPreG Σ := HeapPreG { Class heapPreG Σ := HeapPreG {
heap_preG_iris :> invPreG Σ; heap_preG_iris :> invPreG Σ;
heap_preG_heap :> gen_heapPreG loc val Σ; heap_preG_heap :> gen_heapPreG loc val Σ;
heap_preG_inv_heap :> inv_heapPreG loc val Σ;
heap_preG_proph :> proph_mapPreG proph_id (val * val) Σ; heap_preG_proph :> proph_mapPreG proph_id (val * val) Σ;
}. }.
Definition heapΣ : gFunctors := Definition heapΣ : gFunctors :=
#[invΣ; gen_heapΣ loc val; proph_mapΣ proph_id (val * val)]. #[invΣ; gen_heapΣ loc val; inv_heapΣ loc val; proph_mapΣ proph_id (val * val)].
Instance subG_heapPreG {Σ} : subG heapΣ Σ heapPreG Σ. Instance subG_heapPreG {Σ} : subG heapΣ Σ heapPreG Σ.
Proof. solve_inG. Qed. Proof. solve_inG. Qed.
Definition heap_adequacy Σ `{!heapPreG Σ} s e σ φ : Definition heap_adequacy Σ `{!heapPreG Σ} s e σ φ :
( `{!heapG Σ}, WP e @ s; {{ v, ⌜φ v }}) ( `{!heapG Σ}, inv_heap_inv - WP e @ s; {{ v, ⌜φ v }})
adequate s e σ (λ v _, φ v). adequate s e σ (λ v _, φ v).
Proof. Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "". intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
iMod (gen_heap_init σ.(heap)) as (?) "Hh". iMod (gen_heap_init σ.(heap)) as (?) "Hh".
iMod (inv_heap_init loc val) as (?) ">Hi".
iMod (proph_map_init κs σ.(used_proph_id)) as (?) "Hp". iMod (proph_map_init κs σ.(used_proph_id)) as (?) "Hp".
iModIntro. iExists iModIntro. iExists
(λ σ κs, (gen_heap_ctx σ.(heap) proph_map_ctx κs σ.(used_proph_id))%I), (λ σ κs, (gen_heap_ctx σ.(heap) proph_map_ctx κs σ.(used_proph_id))%I),
(λ _, True%I). (λ _, True%I).
iFrame. iApply (Hwp (HeapG _ _ _ _)). iFrame. iApply (Hwp (HeapG _ _ _ _ _)). done.
Qed. Qed.
From stdpp Require Import fin_maps. From stdpp Require Import fin_maps.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth gmap. From iris.algebra Require Import auth gmap.
From iris.base_logic.lib Require Export gen_heap proph_map. From iris.base_logic.lib Require Export gen_heap proph_map gen_inv_heap.
From iris.base_logic.lib Require Import gen_inv_heap.
From iris.program_logic Require Export weakestpre total_weakestpre. From iris.program_logic Require Export weakestpre total_weakestpre.
From iris.program_logic Require Import ectx_lifting total_ectx_lifting. From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
...@@ -12,6 +11,7 @@ Set Default Proof Using "Type". ...@@ -12,6 +11,7 @@ Set Default Proof Using "Type".
Class heapG Σ := HeapG { Class heapG Σ := HeapG {
heapG_invG : invG Σ; heapG_invG : invG Σ;
heapG_gen_heapG :> gen_heapG loc val Σ; heapG_gen_heapG :> gen_heapG loc val Σ;
heapG_inv_heapG :> inv_heapG loc val Σ;
heapG_proph_mapG :> proph_mapG proph_id (val * val) Σ; heapG_proph_mapG :> proph_mapG proph_id (val * val) Σ;
}. }.
...@@ -35,6 +35,7 @@ Notation "l ↦□ I" := (inv_mapsto (L:=loc) (V:=val) l I%stdpp%type) ...@@ -35,6 +35,7 @@ Notation "l ↦□ I" := (inv_mapsto (L:=loc) (V:=val) l I%stdpp%type)
(at level 20, format "l ↦□ I") : bi_scope. (at level 20, format "l ↦□ I") : bi_scope.
Notation "l ↦_ I v" := (inv_mapsto_own (L:=loc) (V:=val) l v I%stdpp%type) Notation "l ↦_ I v" := (inv_mapsto_own (L:=loc) (V:=val) l v I%stdpp%type)
(at level 20, I at level 9, format "l ↦_ I v") : bi_scope. (at level 20, I at level 9, format "l ↦_ I v") : bi_scope.
Notation inv_heap_inv := (inv_heap_inv loc val).
(** The tactic [inv_head_step] performs inversion on hypotheses of the shape (** The tactic [inv_head_step] performs inversion on hypotheses of the shape
[head_step]. The tactic will discharge head-reductions starting from values, and [head_step]. The tactic will discharge head-reductions starting from values, and
......
...@@ -5,15 +5,16 @@ From iris.heap_lang Require Import proofmode notation. ...@@ -5,15 +5,16 @@ From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Definition heap_total Σ `{!heapPreG Σ} s e σ φ : Definition heap_total Σ `{!heapPreG Σ} s e σ φ :
( `{!heapG Σ}, WP e @ s; [{ v, ⌜φ v }]) ( `{!heapG Σ}, inv_heap_inv - WP e @ s; [{ v, ⌜φ v }])
sn erased_step ([e], σ). sn erased_step ([e], σ).
Proof. Proof.
intros Hwp; eapply (twp_total _ _); iIntros (?) "". intros Hwp; eapply (twp_total _ _); iIntros (?) "".
iMod (gen_heap_init σ.(heap)) as (?) "Hh". iMod (gen_heap_init σ.(heap)) as (?) "Hh".
iMod (inv_heap_init loc val) as (?) ">Hi".
iMod (proph_map_init [] σ.(used_proph_id)) as (?) "Hp". iMod (proph_map_init [] σ.(used_proph_id)) as (?) "Hp".
iModIntro. iModIntro.
iExists iExists
(λ σ κs _, (gen_heap_ctx σ.(heap) proph_map_ctx κs σ.(used_proph_id))%I), (λ σ κs _, (gen_heap_ctx σ.(heap) proph_map_ctx κs σ.(used_proph_id))%I),
(λ _, True%I); iFrame. (λ _, True%I); iFrame.
iApply (Hwp (HeapG _ _ _ _)). iApply (Hwp (HeapG _ _ _ _ _)). done.
Qed. Qed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment