Library zoo.program_logic.state_interp
From iris.base_logic Require Import
lib.invariants.
From zoo Require Import
prelude.
From zoo.iris Require Import
diaframe.
From zoo.language Require Import
notations.
From zoo.program_logic Require Export
ghost_state.
From zoo Require Import
options.
Implicit Types cnt ns nt : nat.
Implicit Type pid : prophet_id.
Implicit Types tid : thread_id.
Implicit Types l : location.
Implicit Types v : val.
Implicit Types vs : list val.
Implicit Types hdr : header.
Implicit Types hdrs : gmap location header.
Implicit Types σ : state.
Implicit Type proph : val × val.
Implicit Type prophs : list (val × val).
Implicit Type prophets : gmap prophet_id (list (val × val)).
Implicit Types κ κs : list observation.
Record state_wf σ v :=
{ state_wf_locals :
σ.(state_locals) = [v]
; state_wf_counter :
σ.(state_heap) !! zoo_counter = Some 0%V
}.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Definition state_interp ns nt σ κs : iProp Σ :=
headers_auth σ.(state_headers) ∗
heap_auth σ.(state_heap) ∗
prophets_auth κs σ.(state_prophets) ∗
steps_auth ns ∗
locals_auth σ.(state_locals) ∗
⌜length σ.(state_locals) = nt⌝ ∗
zoo_counter_inv.
Definition fork_post (_ : val) : iProp Σ :=
True.
End zoo_G.
#[local] Instance : CustomIpat "state_interp" :=
" ( Hheaders_auth & Hheap_auth & Hprophets_auth & Hsteps_auth & Hlocals_auth & %Hlocals & Hcounter_inv ) ".
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Lemma state_interp_mono ns nt σ κs :
state_interp ns nt σ κs ⊢ |==>
state_interp (S ns) nt σ κs.
Lemma state_interp_counter_inv ns nt σ κs :
state_interp ns nt σ κs ⊢
zoo_counter_inv.
End zoo_G.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
#[local] Lemma big_sepM_chunk {A} (Φ : location → A → iProp Σ) l xs :
([∗ map] l ↦ x ∈ chunk l xs, Φ l x) ⊢
[∗ list] i ↦ x ∈ xs, Φ (l +ₗ i) x.
Lemma state_interp_alloc {ns nt σ κs} l tag vs :
σ.(state_headers) !! l = None →
( ∀ i,
i < length vs →
σ.(state_heap) !! (l +ₗ i) = None
) →
state_interp ns nt σ κs ⊢ |==>
let hdr := Header tag (length vs) in
state_interp ns nt (state_alloc l hdr vs σ) κs ∗
l ↦ₕ hdr ∗
meta_token l ⊤ ∗
l ↦∗ vs.
Lemma state_interp_headers_at_valid ns nt σ κs l hdr :
state_interp ns nt σ κs -∗
l ↦ₕ hdr -∗
⌜σ.(state_headers) !! l = Some hdr⌝.
Lemma state_interp_pointsto_valid ns nt σ κs l dq v :
state_interp ns nt σ κs -∗
l ↦{dq} v -∗
⌜σ.(state_heap) !! l = Some v⌝.
Lemma state_interp_pointstos_valid ns nt σ κs l dq vs :
state_interp ns nt σ κs -∗
l ↦∗{dq} vs -∗
⌜ ∀ (i : nat) v,
vs !! i = Some v →
σ.(state_heap) !! (l +ₗ i) = Some v
⌝.
Lemma state_interp_pointsto_update {ns nt σ κs l w} v :
state_interp ns nt σ κs -∗
l ↦ w ==∗
state_interp ns nt (state_set_location l v σ) κs ∗
l ↦ v.
Lemma state_interp_steps_lb_get ns nt σ κs :
state_interp ns nt σ κs ⊢
⧖ ns.
Lemma state_interp_steps_lb_valid ns1 nt σ κs ns2 :
state_interp ns1 nt σ κs -∗
⧖ ns2 -∗
⌜ns2 ≤ ns1⌝.
Lemma state_interp_local_pointsto_valid ns nt σ κs tid dq v :
state_interp ns nt σ κs -∗
tid ↦ₗ{dq} v -∗
⌜σ.(state_locals) !! tid = Some v⌝.
Lemma state_interp_fork {ns nt σ κs} v :
state_interp ns nt σ κs ⊢ |==>
state_interp ns (nt + 1) (state_add_local v σ) κs ∗
nt ↦ₗ v.
Lemma state_interp_local_pointsto_update {ns nt σ κs tid w} v :
state_interp ns nt σ κs -∗
tid ↦ₗ w ==∗
state_interp ns nt (state_set_local tid v σ) κs ∗
tid ↦ₗ v.
Lemma state_interp_prophet_new {ns nt σ κs} pid :
pid ∉ σ.(state_prophets) →
state_interp ns nt σ κs ⊢ |==>
∃ prophs,
state_interp ns nt (state_add_prophet pid σ) κs ∗
prophet_model pid prophs.
Lemma state_interp_prophet_resolve ns nt σ κs pid proph prophs :
state_interp ns nt σ ((pid, proph) :: κs) -∗
prophet_model pid prophs ==∗
∃ prophs',
⌜prophs = proph :: prophs'⌝ ∗
state_interp ns nt σ κs ∗
prophet_model pid prophs'.
End zoo_G.
Definition state_heap_initial σ :=
delete zoo_counter σ.(state_heap).
Lemma state_interp_init `{zoo_Gpre : !ZooGpre Σ} `{inv_G : !invGS Σ} σ v κs :
state_wf σ v →
⊢ |={⊤}=>
∃ zoo_G : ZooG Σ,
⌜zoo_G.(zoo_G_inv_G) = inv_G⌝ ∗
state_interp 0 1 σ κs ∗
([∗ map] l ↦ v ∈ state_heap_initial σ, l ↦ v) ∗
0 ↦ₗ v.
#[global] Opaque state_interp.
lib.invariants.
From zoo Require Import
prelude.
From zoo.iris Require Import
diaframe.
From zoo.language Require Import
notations.
From zoo.program_logic Require Export
ghost_state.
From zoo Require Import
options.
Implicit Types cnt ns nt : nat.
Implicit Type pid : prophet_id.
Implicit Types tid : thread_id.
Implicit Types l : location.
Implicit Types v : val.
Implicit Types vs : list val.
Implicit Types hdr : header.
Implicit Types hdrs : gmap location header.
Implicit Types σ : state.
Implicit Type proph : val × val.
Implicit Type prophs : list (val × val).
Implicit Type prophets : gmap prophet_id (list (val × val)).
Implicit Types κ κs : list observation.
Record state_wf σ v :=
{ state_wf_locals :
σ.(state_locals) = [v]
; state_wf_counter :
σ.(state_heap) !! zoo_counter = Some 0%V
}.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Definition state_interp ns nt σ κs : iProp Σ :=
headers_auth σ.(state_headers) ∗
heap_auth σ.(state_heap) ∗
prophets_auth κs σ.(state_prophets) ∗
steps_auth ns ∗
locals_auth σ.(state_locals) ∗
⌜length σ.(state_locals) = nt⌝ ∗
zoo_counter_inv.
Definition fork_post (_ : val) : iProp Σ :=
True.
End zoo_G.
#[local] Instance : CustomIpat "state_interp" :=
" ( Hheaders_auth & Hheap_auth & Hprophets_auth & Hsteps_auth & Hlocals_auth & %Hlocals & Hcounter_inv ) ".
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Lemma state_interp_mono ns nt σ κs :
state_interp ns nt σ κs ⊢ |==>
state_interp (S ns) nt σ κs.
Lemma state_interp_counter_inv ns nt σ κs :
state_interp ns nt σ κs ⊢
zoo_counter_inv.
End zoo_G.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
#[local] Lemma big_sepM_chunk {A} (Φ : location → A → iProp Σ) l xs :
([∗ map] l ↦ x ∈ chunk l xs, Φ l x) ⊢
[∗ list] i ↦ x ∈ xs, Φ (l +ₗ i) x.
Lemma state_interp_alloc {ns nt σ κs} l tag vs :
σ.(state_headers) !! l = None →
( ∀ i,
i < length vs →
σ.(state_heap) !! (l +ₗ i) = None
) →
state_interp ns nt σ κs ⊢ |==>
let hdr := Header tag (length vs) in
state_interp ns nt (state_alloc l hdr vs σ) κs ∗
l ↦ₕ hdr ∗
meta_token l ⊤ ∗
l ↦∗ vs.
Lemma state_interp_headers_at_valid ns nt σ κs l hdr :
state_interp ns nt σ κs -∗
l ↦ₕ hdr -∗
⌜σ.(state_headers) !! l = Some hdr⌝.
Lemma state_interp_pointsto_valid ns nt σ κs l dq v :
state_interp ns nt σ κs -∗
l ↦{dq} v -∗
⌜σ.(state_heap) !! l = Some v⌝.
Lemma state_interp_pointstos_valid ns nt σ κs l dq vs :
state_interp ns nt σ κs -∗
l ↦∗{dq} vs -∗
⌜ ∀ (i : nat) v,
vs !! i = Some v →
σ.(state_heap) !! (l +ₗ i) = Some v
⌝.
Lemma state_interp_pointsto_update {ns nt σ κs l w} v :
state_interp ns nt σ κs -∗
l ↦ w ==∗
state_interp ns nt (state_set_location l v σ) κs ∗
l ↦ v.
Lemma state_interp_steps_lb_get ns nt σ κs :
state_interp ns nt σ κs ⊢
⧖ ns.
Lemma state_interp_steps_lb_valid ns1 nt σ κs ns2 :
state_interp ns1 nt σ κs -∗
⧖ ns2 -∗
⌜ns2 ≤ ns1⌝.
Lemma state_interp_local_pointsto_valid ns nt σ κs tid dq v :
state_interp ns nt σ κs -∗
tid ↦ₗ{dq} v -∗
⌜σ.(state_locals) !! tid = Some v⌝.
Lemma state_interp_fork {ns nt σ κs} v :
state_interp ns nt σ κs ⊢ |==>
state_interp ns (nt + 1) (state_add_local v σ) κs ∗
nt ↦ₗ v.
Lemma state_interp_local_pointsto_update {ns nt σ κs tid w} v :
state_interp ns nt σ κs -∗
tid ↦ₗ w ==∗
state_interp ns nt (state_set_local tid v σ) κs ∗
tid ↦ₗ v.
Lemma state_interp_prophet_new {ns nt σ κs} pid :
pid ∉ σ.(state_prophets) →
state_interp ns nt σ κs ⊢ |==>
∃ prophs,
state_interp ns nt (state_add_prophet pid σ) κs ∗
prophet_model pid prophs.
Lemma state_interp_prophet_resolve ns nt σ κs pid proph prophs :
state_interp ns nt σ ((pid, proph) :: κs) -∗
prophet_model pid prophs ==∗
∃ prophs',
⌜prophs = proph :: prophs'⌝ ∗
state_interp ns nt σ κs ∗
prophet_model pid prophs'.
End zoo_G.
Definition state_heap_initial σ :=
delete zoo_counter σ.(state_heap).
Lemma state_interp_init `{zoo_Gpre : !ZooGpre Σ} `{inv_G : !invGS Σ} σ v κs :
state_wf σ v →
⊢ |={⊤}=>
∃ zoo_G : ZooG Σ,
⌜zoo_G.(zoo_G_inv_G) = inv_G⌝ ∗
state_interp 0 1 σ κs ∗
([∗ map] l ↦ v ∈ state_heap_initial σ, l ↦ v) ∗
0 ↦ₗ v.
#[global] Opaque state_interp.