Commit b6b86ac1 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre Committed by Michael Sammler

Operational semantics for intptr casts + CMRA.

Co-authored-by: Michael Sammler's avatarMichael Sammler <msammler@mpi-sws.org>
parent 08d9915b
......@@ -165,6 +165,7 @@ void *fsm_insert(struct fixed_size_map *m, size_t key, void *value) {
[[rc::ensures("m @ &own<{alter (λ _, singleton_place p) key mp, items2, count} @ fixed_size_map>")]]
[[rc::lemmas("fsm_invariant_alter")]]
[[rc::tactics("all: try by erewrite length_filter_insert => //; solve_goal.")]]
[[rc::tactics("all: try by apply inhabitant.")]]
void *fsm_get(struct fixed_size_map *m, size_t key) {
size_t slot_idx = fsm_probe(m, key);
struct item *item = &(*m->items)[slot_idx];
......
......@@ -24,6 +24,7 @@ Section proof_fsm_get.
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
all: try by apply: fsm_invariant_alter; solve_goal.
all: try by erewrite length_filter_insert => //; solve_goal.
all: try by apply inhabitant.
all: print_sidecondition_goal "fsm_get".
Qed.
End proof_fsm_get.
This diff is collapsed.
......@@ -223,7 +223,9 @@ Open Scope loc_scope.
Definition alloc_id := Z.
Definition addr := Z.
Definition loc : Set := alloc_id * addr.
Definition dummy_alloc_id : alloc_id := 0.
Definition loc : Set := option alloc_id * addr.
Bind Scope loc_scope with loc.
Inductive mbyte : Set :=
......@@ -236,7 +238,7 @@ Bind Scope val_scope with val.
Inductive lock_state := WSt | RSt (n : nat).
Definition heap := gmap loc (lock_state * mbyte).
Definition heap := gmap addr (alloc_id * lock_state * mbyte).
Record allocation :=
Allocation {
......@@ -610,24 +612,31 @@ Qed.
allocation that contains [l]. Note that we consider the 1-past-the-end
pointer to be in range of an allocation. *)
Definition heap_loc_in_bounds (l : loc) (n : nat) (st : state) : Prop :=
alloc, st.(st_allocs) !! l.1 = Some alloc
alloc.(alloc_start) l.2
l.2 + n alloc.(alloc_end).
alloc_id alloc,
l.1 = Some alloc_id
st.(st_allocs) !! alloc_id = Some alloc
alloc.(alloc_start) l.2
l.2 + n alloc.(alloc_end).
Fixpoint heap_at_go l v flk h : Prop :=
match v with
| [] => True
| b::v' => ( lk, h !! l = Some (lk, b) flk lk) heap_at_go (l + 1) v' flk h
| b::v' => ( lk, h !! l.2 = Some (default dummy_alloc_id l.1, lk, b) flk lk) heap_at_go (l + 1) v' flk h
end.
Definition heap_at l ly v flk h : Prop :=
l `has_layout_loc` ly v `has_layout_val` ly heap_at_go l v flk h.
is_Some l.1 l `has_layout_loc` ly v `has_layout_val` ly heap_at_go l v flk h.
Definition heap_block_free (h : heap) (aid : alloc_id) : Prop :=
a ha, h !! a = Some ha ha.1.1 aid.
Definition heap_block_free h l : Prop := i, h !! (l + i) = None.
Definition heap_range_free (h : heap) (a : addr) (n : nat) : Prop :=
a', a a' < a + n h !! a' = None.
Fixpoint heap_upd l v flk h : heap :=
Fixpoint heap_upd l v (flk : option lock_state lock_state) (h : heap) : heap :=
match v with
| b::v' => partial_alter (λ m, Some (flk (fst <$> m), b)) l (heap_upd (l + 1) v' flk h)
| b::v' => partial_alter (λ m, Some (default dummy_alloc_id l.1,
flk (snd <$> (fst <$> m)), b)) l.2 (heap_upd (l + 1) v' flk h)
| [] => h
end.
......@@ -640,7 +649,7 @@ Fixpoint heap_upd_list ls vs flk h : heap :=
Fixpoint heap_free l n h : heap :=
match n with
| O => h
| S n' => delete l (heap_free (l + 1) n' h)
| S n' => delete l.2 (heap_free (l + 1) n' h)
end.
Fixpoint heap_free_list ls h : heap :=
......@@ -702,7 +711,13 @@ Definition stmt_of_val (sv : stmt_val) : thread_state :=
(*** Evaluation of operations *)
(** Checks that the location [l] is allocated on the heap [h] *)
Definition valid_ptr l h : Prop :=
is_Some (h !! l).
aid lk b, l.1 = Some aid h !! l.2 = Some (aid, lk, b).
Instance valid_ptr_dec l h : Decision (valid_ptr l h).
Proof.
rewrite /valid_ptr/=. destruct l as [[aid|] a]; [ | right; naive_solver].
destruct (h !! a) as [[[aid' ?]?]|] eqn: Hh; [ | right; naive_solver].
destruct (decide (aid' = aid)); [left | right]; naive_solver.
Qed.
(** Checks whether location [l] is a weak valid pointer in heap [h].
[Some true] means [l] is a valid in bounds pointer, [Some false] means
[l] is a end of block pointer, [None] means [l] is not a valid pointer. *)
......@@ -718,7 +733,7 @@ http://compcert.inria.fr/doc/html/compcert.common.Values.html#Val.cmplu_bool
Definition ptr_eq l1 l2 h : option bool :=
eob1 weak_valid_ptr l1 h;
eob2 weak_valid_ptr l2 h;
if decide (l1.1 = l2.2) then
if decide (l1.1 = l2.1) then
Some (bool_decide (l1 = l2))
else
if eob1 || eob2 then None else Some false.
......@@ -839,12 +854,14 @@ Inductive expr_step : expr → state → list Empty_set → expr → state → l
expr_step (BinOp op ot1 ot2 (Val v1) (Val v2)) σ [] (Val v') σ []
| DerefS o v l ly v' σ:
let start_st st := n, st = if o is Na2Ord then RSt (S n) else RSt n in
let end_st st := match o, st with
| Na1Ord, Some (RSt n) => RSt (S n)
| Na2Ord, Some (RSt (S n)) => RSt n
| ScOrd, Some st => st
(* unreachable *)
| _, _ => WSt end in
let end_st st :=
match o, st with
| Na1Ord, Some (RSt n) => RSt (S n)
| Na2Ord, Some (RSt (S n)) => RSt n
| ScOrd , Some st => st
| _ , _ => WSt (* unreachable *)
end
in
let end_expr := if o is Na1Ord then Deref Na2Ord ly (Val v) else Val v' in
val_to_loc v = Some l
heap_at l ly v' start_st σ.(st_heap)
......@@ -1027,16 +1044,29 @@ Definition subst_function (xs : list var_name) (vs : list val) (f : function) :
f_args := f.(f_args); f_init := f.(f_init); f_local_vars := f.(f_local_vars);
|}.
(*** Allocation semantics *)
(* We reserve 0 for NULL. *)
Definition min_alloc_start : Z := 1.
(* We never allocate the last byte to always have valid one-past pointers. *)
Definition max_alloc_end : Z := 2 ^ (bytes_per_addr * bits_per_byte) - 2.
Definition to_allocation (off : Z) (len : nat) : allocation :=
Allocation off (off + len).
Definition in_range_allocation (a : allocation) : Prop :=
min_alloc_start a.(alloc_start) a.(alloc_end) max_alloc_end.
Inductive alloc_new_block : state loc val state Prop :=
| AllocNewBlock σ l v:
σ.(st_allocs) !! l.1 = None
heap_block_free σ.(st_heap) l
| AllocNewBlock σ l aid v:
l.1 = Some aid
σ.(st_allocs) !! aid = None
heap_block_free σ.(st_heap) aid
in_range_allocation (to_allocation l.2 (length v))
heap_range_free σ.(st_heap) l.2 (length v)
alloc_new_block σ l v {|
st_heap := heap_upd l v (λ _, RSt 0%nat) σ.(st_heap);
st_allocs := <[l.1 := to_allocation l.2 (length v)]> σ.(st_allocs);
st_allocs := <[aid := to_allocation l.2 (length v)]> σ.(st_allocs);
st_fntbl := σ.(st_fntbl); st_alloc_failure := σ.(st_alloc_failure);
|}.
......@@ -1199,13 +1229,6 @@ Proof. rewrite /offset_loc/shift_loc/=. destruct l => /=. f_equal. lia. Qed.
Lemma offset_loc_sz1 ly l n : ly.(ly_size) = 1%nat l offset{ly} n = l + n.
Proof. rewrite /offset_loc => ->. f_equal. lia. Qed.
(*
Lemma stmt_to_val_non_ret ts s :
(if s is Return (Val v) then False else True) →
stmt_to_val (update_stmt ts s) = None.
Proof. destruct s as [|e| | | | | |] => //. by destruct e. Qed.
*)
Lemma stmt_fill_inj Ks1 Ks2 e1 e2 :
to_val e1 = None to_val e2 = None stmt_fill Ks1 e1 = stmt_fill Ks2 e2
Ks1 = Ks2 e1 = e2.
......@@ -1228,43 +1251,41 @@ Lemma heap_at_go_inj_val l h v v' flk1 flk2:
length v = length v'
heap_at_go l v flk1 h heap_at_go l v' flk2 h v = v'.
Proof.
elim: v v' l. by move => [|??] // ? [[]].
move => b v IH [|b' v'] //= l [?] [[?[??]]?] [[?[??]]?]; simplify_eq. f_equal.
by apply: IH.
elim: v v' l; first by move => [|??] // ? [[]].
move => b v IH [|b' v'] //= l [?] [[?[??]]?] [[?[??]]?]; simplify_eq.
f_equal. by apply: IH.
Qed.
Lemma heap_at_go_inj_val' l h v v' flk1 flk2 ly:
v `has_layout_val` ly
heap_at_go l v flk1 h heap_at l ly v' flk2 h v = v'.
Proof. move => ??[_[??]]. apply: heap_at_go_inj_val => //. congruence. Qed.
Proof.
move => ??[_[?[??]]]. apply: heap_at_go_inj_val => //. congruence.
Qed.
Lemma heap_at_inj_val l ly h v v' flk1 flk2:
heap_at l ly v flk1 h heap_at l ly v' flk2 h v = v'.
Proof. move => [_ [Hv1 H1]] [_ [Hv2 H2]]. apply: heap_at_go_inj_val => //. congruence. Qed.
Proof.
move => [_ [Hv1 [H1 ?]]] [_ [Hv2 [H2 ?]]].
apply: heap_at_go_inj_val => //. congruence.
Qed.
Lemma heap_upd_ext h l v f1 f2:
( x, f1 x = f2 x)
heap_upd l v f1 h = heap_upd l v f2 h.
Proof. move => Hext. elim: v l => //= ?? IH ?. rewrite IH. apply: partial_alter_ext => ??. by rewrite Hext. Qed.
Proof.
move => Hext. elim: v l => //= ?? IH ?. rewrite IH.
apply: partial_alter_ext => ??. by rewrite Hext.
Qed.
Lemma heap_upd_lookup_lt l n bl h flk:
n > 0
heap_upd (l + n) bl flk h !! l = h !! l.
heap_upd (l + n) bl flk h !! l.2 = h !! l.2.
Proof.
elim: bl n => // b bl IH /= n Hn. rewrite shift_loc_assoc.
rewrite lookup_partial_alter_ne //.
- apply IH. lia.
- rewrite /shift_loc. destruct l => /= [[]]. lia.
Qed.
Lemma heap_upd_lookup_ne l v h i l' flk:
l'.1 l.1
heap_upd l' v flk h !! (l + i) = h !! (l + i).
Proof.
elim: v l' => // b bl IH l' Hne /=.
rewrite lookup_partial_alter_ne //.
- by apply IH.
- by destruct l, l' => [[]].
- rewrite /shift_loc. destruct l. lia.
Qed.
Lemma heap_upd_heap_at_id l v flk flk' h:
......@@ -1276,27 +1297,8 @@ Proof.
apply: partial_alter_self_alt'. by rewrite Hlk Hflk.
Qed.
Lemma heap_block_free_upd_list ls vs h l flk:
heap_block_free h l l.1 ls.*1
heap_block_free (heap_upd_list ls vs flk h) l.
Proof.
rewrite /heap_block_free.
elim: ls vs => // l' ls IH [|v vs] // Hfree; csimpl => Hl i.
rewrite heap_upd_lookup_ne; set_solver.
Qed.
Lemma heap_block_free_free_list h l ls:
heap_block_free h l
heap_block_free (heap_free_list ls h) l.
Proof.
elim: ls l => // -[l [sz ?]] ls IH l' Hf /= o. unfold ly_size.
elim: sz l. move => ?. by apply IH.
move => sz IH2 l /=. apply lookup_delete_None. naive_solver.
Qed.
Lemma heap_free_delete h l l' n :
delete l (heap_free l' n h) = heap_free l' n (delete l h).
delete l.2 (heap_free l' n h) = heap_free l' n (delete l.2 h).
Proof. revert l'. induction n as [|n IH]=> l' //=. by rewrite delete_commute IH. Qed.
Lemma heap_free_list_app ls1 ls2 h:
......@@ -1312,6 +1314,7 @@ Instance function_inhabited : Inhabited function := populate {| f_args := []; f_
Canonical Structure mbyteO := leibnizO mbyte.
Canonical Structure functionO := leibnizO function.
Canonical Structure locO := leibnizO loc.
Canonical Structure alloc_idO := leibnizO alloc_id.
Canonical Structure layoutO := leibnizO layout.
Canonical Structure valO := leibnizO val.
Canonical Structure exprO := leibnizO expr.
......
......@@ -116,27 +116,27 @@ Proof.
iIntros (Ho Hl Hll Hlv) "Hmt HΦ".
iApply wp_lift_head_step; auto.
iIntros ([h ub fn] ???) "(%&Hhctx&Hfctx)".
iDestruct (heap_mapsto_has_alloc_id with "Hmt") as %Haid.
destruct o; try by destruct Ho.
- iMod (fupd_intro_mask' _ ) as "Hclose"; first set_solver. iModIntro.
iDestruct (heap_mapsto_lookup_q (λ st, n, st = RSt n) with "Hhctx Hmt") as %Hat. naive_solver.
iSplit; first by eauto 7 using DerefS.
iSplit; first by eauto 8 using DerefS.
iIntros "!#" (e2 σ2 efs Hst). inv_expr_step. iMod "Hclose" as "$". iModIntro. unfold end_st, end_expr.
have <- : (v = v') by apply: heap_at_inj_val.
rewrite /heap_fmap/=. erewrite heap_upd_heap_at_id => //.
iFrame. iSplit => //. iApply @wp_value. by iApply "HΦ".
- iMod (heap_read_na with "Hhctx Hmt") as "(% & Hσ & Hσclose)" => //.
iMod (fupd_intro_mask' _ ) as "Hclose"; first set_solver. iModIntro.
iSplit; first by eauto 7 using DerefS.
iSplit; first by eauto 8 using DerefS.
iIntros "!#" (e2 σ2 efs Hst). inv_expr_step. iMod "Hclose" as "$". iModIntro. unfold end_st, end_expr.
have <- : (v = v') by apply: heap_at_inj_val.
iFrame => /=. iSplit; first by eauto 7 using blocks_used_agree_heap_upd.
iFrame => /=. iSplit => //.
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros ([h2 fn2] ???) "(%&Hhctx&Hfctx)". iMod ("Hσclose" with "Hhctx") as (?) "(Hσ & Hv)".
iModIntro; iSplit; first by eauto 7 using DerefS.
iModIntro; iSplit; first by eauto 8 using DerefS.
iIntros "!#" (e2 σ2 efs Hst) "!#". inv_expr_step.
have <- : (v = v'0) by apply: heap_at_inj_val.
iFrame. iSplitR => //=. iSplit; first by eauto 7 using blocks_used_agree_heap_upd.
by iApply "HΦ".
iFrame. iSplitR => //=. by iApply "HΦ".
Qed.
Lemma wp_cas_fail vl1 vl2 vd vo ve z1 z2 Φ l1 l2 it q E:
......@@ -153,19 +153,20 @@ Lemma wp_cas_fail vl1 vl2 vd vo ve z1 z2 Φ l1 l2 it q E:
WP CAS (IntOp it) (Val vl1) (Val vl2) (Val vd) @ E {{ Φ }}.
Proof.
iIntros (Hl1 Hl2 Hly1 Hly2 Hvo Hve Hlen1 Hlen2 Hneq) "Hl1 Hl2 HΦ".
iDestruct (heap_mapsto_has_alloc_id with "Hl1") as %Haid1.
iDestruct (heap_mapsto_has_alloc_id with "Hl2") as %Haid2.
move: (Hvo) (Hve) => /val_to_int_length ? /val_to_int_length ?.
iApply wp_lift_atomic_head_step; auto.
iIntros (σ1 ???) "(%&Hhctx&Hfctx)".
iDestruct (heap_mapsto_lookup_q (λ st : lock_state, n : nat, st = RSt n) with "Hhctx Hl1") as %? => //. { naive_solver. }
iDestruct (heap_mapsto_lookup_1 (λ st : lock_state, st = RSt 0%nat) with "Hhctx Hl2") as %? => //.
iModIntro. iSplit; first by eauto 10 using CasFailS.
iModIntro. iSplit; first by eauto 12 using CasFailS.
iIntros "!#" (e2 σ2 efs Hst). inv_expr_step;
have ? : (vo = vo0) by [apply: heap_at_go_inj_val' => //; congruence];
have ? : (ve = ve0) by [apply: heap_at_go_inj_val' => //; congruence]; simplify_eq.
have ? : (length ve0 = length vo0) by congruence.
iMod (heap_write with "Hhctx Hl2") as "[$ Hl2]" => //.
iFrame. iModIntro. rewrite right_id /=.
iSplit; first by eauto using blocks_used_agree_heap_upd.
by iApply ("HΦ" with "Hl1").
Qed.
......@@ -183,19 +184,20 @@ Lemma wp_cas_suc vl1 vl2 vd vo ve z1 z2 Φ l1 l2 it E q:
WP CAS (IntOp it) (Val vl1) (Val vl2) (Val vd) @ E {{ Φ }}.
Proof.
iIntros (Hl1 Hl2 Hly1 Hly2 Hvo Hve Hlen1 Hlen2 Heq) "Hl1 Hl2 HΦ".
iDestruct (heap_mapsto_has_alloc_id with "Hl1") as %Haid1.
iDestruct (heap_mapsto_has_alloc_id with "Hl2") as %Haid2.
move: (Hvo) (Hve) => /val_to_int_length ? /val_to_int_length ?.
iApply wp_lift_atomic_head_step; auto.
iIntros (σ1 ???) "(%&Hhctx&Hfctx)".
iDestruct (heap_mapsto_lookup_1 (λ st : lock_state, st = RSt 0%nat) with "Hhctx Hl1") as %? => //.
iDestruct (heap_mapsto_lookup_q (λ st : lock_state, n : nat, st = RSt n) with "Hhctx Hl2") as %? => //. { naive_solver. }
iModIntro. iSplit; first by eauto 10 using CasSucS.
iModIntro. iSplit; first by eauto 12 using CasSucS.
iIntros "!#" (e2 σ2 efs Hst). inv_expr_step;
have ? : (ve = ve0) by [apply: heap_at_go_inj_val' => //; congruence];
have ? : (vo = vo0) by [apply: heap_at_go_inj_val' => //; congruence]; simplify_eq.
have ? : (length vo0 = length vd) by congruence.
iMod (heap_write with "Hhctx Hl1") as "[$ Hmt]" => //.
iFrame. iModIntro. rewrite right_id /=.
iSplit; first by eauto using blocks_used_agree_heap_upd.
by iApply ("HΦ" with "Hmt").
Qed.
......@@ -529,13 +531,14 @@ Proof.
iIntros (???? Hstep). inv_stmt_step; last first. {
(* Alloc failure case. *)
iIntros "!> !>". iMod "HE" as "_". iIntros "!>". iSplit; first done.
rewrite /state_ctx. iFrame. iSplit; first done. iIntros (?). done.
rewrite /state_ctx. iFrame. by iIntros (?).
}
iMod (heap_alloc_new_blocks_upd with "[$Hhctx $Hbctx $Hfctx]") as "[Hctx [Hv' Hv]]" => //.
iMod (heap_alloc_new_blocks_upd with "Hctx") as "[Hctx [Ha' Ha]]" => //.
iMod (heap_alloc_new_blocks_upd with "[$Hhctx $Hbctx $Hfctx]") as "[Hctx Hlv]" => //.
iMod (heap_alloc_new_blocks_upd with "Hctx") as "[Hctx Hla]" => //.
iModIntro. iNext.
iDestruct ("HWP" $! lsa lsv with "[//] Ha [Hv]") as (Ψ') "(HQinit & HΨ')". {
rewrite big_sepL2_fmap_r. iApply (big_sepL2_mono with "Hv") => ??? ?? /=.
iDestruct ("HWP" $! lsa lsv with "[//] Hla [Hlv]") as (Ψ') "(HQinit & HΨ')". {
rewrite big_sepL2_fmap_r. iApply (big_sepL2_mono with "Hlv") => ??? ?? /=.
iIntros "?". iExists _. iFrame. iPureIntro. split; first by apply replicate_length.
apply: Forall2_lookup_lr. 2: done. done. rewrite list_lookup_fmap. apply fmap_Some. naive_solver.
}
......@@ -551,9 +554,9 @@ Proof.
iMod "HE" as "$". iFrame. rewrite /heap_fmap/= heap_free_list_app /=.
rewrite -!(big_sepL2_fmap_r snd (λ _ l ly, l|ly|)%I).
iMod (heap_free_list_free with "Hhctx Hv") as "Hhctx".
iMod (heap_free_list_free with "Hhctx Ha") as "$". iModIntro.
iMod (heap_free_list_free with "Hhctx Ha") as "$".
iModIntro.
rewrite stmt_wp_unfold. iSplit => //.
iSplit; first by eauto using blocks_used_agree_heap_free_list.
iIntros "_". iApply "Hs" => //. iIntros (v) "HΨ".
destruct ts1 as [??[]] => //. by iApply "HWP".
Qed.
......@@ -569,37 +572,36 @@ Proof.
iIntros (E Ho Hvl Hly) "HWP". iApply wps_lift_stmt_step. iIntros (ts ? ->).
iSplit; first done. iIntros ([h1 ?]) "(%&Hhctx&Hfctx)". iMod "HWP" as "[Hl HWP]".
iMod (fupd_intro_mask' _ ) as "HE"; first set_solver.
iDestruct "Hl" as (v' ? ?) "Hl". unfold E. case: Ho => ->.
iDestruct "Hl" as (v' ? ?) "Hl".
iDestruct (heap_mapsto_has_alloc_id with "Hl") as %Haid.
unfold E. case: Ho => ->.
- iModIntro.
iDestruct (heap_mapsto_lookup_1 (λ st : lock_state, st = RSt 0%nat) with "Hhctx Hl") as %? => //.
iSplit; first by eauto 11 using AssignS.
iSplit; first by eauto 12 using AssignS.
iIntros (? e2 σ2 efs Hstep). inv_stmt_step. unfold end_val.
have ? : (length v' = length v2) by congruence.
iMod (heap_write with "Hhctx Hl") as "[$ Hl]" => //.
iIntros "!> !>". iMod ("HWP" with "Hl") as "HWP".
iModIntro => /=. iSplit; first done. iFrame.
iSplit; first by eauto 7 using blocks_used_agree_heap_upd. iIntros (?).
iModIntro => /=. iSplit; first done. iFrame. iIntros (?).
rewrite update_stmt_update /=. iApply (wps_wand with "HWP").
iIntros (v) "HΨ HWP". rewrite update_stmt_update. by iApply "HWP".
- iMod (heap_write_na _ _ _ vr with "Hhctx Hl") as (?) "[Hhctx Hc]" => //; first by congruence.
iModIntro. iSplit; first by eauto 11 using AssignS.
iModIntro. iSplit; first by eauto 12 using AssignS.
iIntros (? e2 σ2 efs Hst). inv_stmt_step.
have ? : (v' = v'0) by [apply: heap_at_inj_val]; subst v'0.
iFrame => /=. iModIntro. iNext. iMod "HE" as "_". iModIntro. iSplit; first done.
rewrite update_stmt_update.
iSplit; first by eauto using blocks_used_agree_heap_upd.
iIntros (?). iApply wps_lift_stmt_step. iIntros (???). iSplit; first done.
iIntros ([h2 ?]) "(%&Hhctx&Hfctx)" => /=.
iMod (fupd_intro_mask' _ ) as "HE"; first set_solver.
iMod ("Hc" with "Hhctx") as (?) "[Hhctx Hmt]".
iModIntro. iSplit; first by eauto 11 using AssignS. unfold end_stmt.
iModIntro. iSplit; first by eauto 12 using AssignS. unfold end_stmt.
iIntros (? e2 σ2 efs Hst). inv_stmt_step. iModIntro. iNext. iMod "HE" as "_".
have ? : (v' = v'0) by [apply: heap_at_go_inj_val']; subst v'0.
iFrame => /=. iMod ("HWP" with "Hmt") as "HWP".
iModIntro. rewrite update_stmt_update. iSplit; first done.
have ? : (length v' = length v3) by congruence.
iSplit; first by eauto using blocks_used_agree_heap_upd.
iIntros (?). subst end_stmt0. rewrite H8. iApply (wps_wand with "HWP").
iIntros (v) "HΨ HWP". rewrite update_stmt_update. iApply "HWP".
iIntros "HWP". rewrite update_stmt_update. by iApply "HWP".
......
......@@ -33,10 +33,10 @@ Definition initial_thread_state (main : loc) : thread_state := {|
ts_alloc_failure := false;
|}.
Definition initial_state (fns : gmap loc function) (gs : gmap loc mbyte) (bs : allocs) :=
{| st_heap := (λ b, (RSt 0%nat, b) ) <$> gs;
Definition initial_state (fns : gmap loc function) :=
{| st_heap := ;
st_fntbl := fns;
st_allocs := bs;
st_allocs := ;
st_alloc_failure := false; |}.
Lemma wp_to_typed_stmt `{!typeG Σ} (ts : thread_state) v':
......@@ -58,27 +58,26 @@ Definition main_type `{!typeG Σ} (P : iProp Σ) :=
fn( () : (); P) () : (), int i32; True.
(** * The main adequacy lemma *)
Lemma refinedc_adequacy Σ `{!typePreG Σ} (thread_mains : list loc) (fns : gmap loc function) (gs : gmap loc mbyte) (bs : allocs) n t2 σ2 κs:
blocks_used_agree (initial_state fns gs bs).(st_heap) (initial_state fns gs bs).(st_allocs)
Lemma refinedc_adequacy Σ `{!typePreG Σ} (thread_mains : list loc) (fns : gmap loc function) (gls : list loc) (gvs : list lang.val) n t2 σ2 κs σ:
alloc_new_blocks (initial_state fns) gls gvs σ
( {HtypeG : typeG Σ}, gl gt,
let Hglobals : globalG Σ := {| global_locs := gl; global_initialized_types := gt; |} in
([ map] kqsgs, heap_mapsto_mbyte k 1 qs) -
([ map] kqsbs, allocs_entry k qs) -
([ list] l; v gls; gvs, l v) -
([ map] kqsfns, fntbl_entry k qs) ={}=
[ list] main thread_mains, P, main ◁ᵥ main @ function_ptr (main_type P) P)
nsteps (Λ := stmt_lang) n (initial_thread_state <$> thread_mains, initial_state fns gs bs) κs (t2, σ2)
nsteps (Λ := stmt_lang) n (initial_thread_state <$> thread_mains, σ) κs (t2, σ2)
e2, e2 t2 not_stuck e2 σ2.
Proof.
move => Hvalid Hwp. apply: wp_strong_adequacy. move => ?.
set h := to_heap ((λ b, (RSt 0%nat, b)) <$> gs).
iMod (own_alloc ( h h)) as (γh) "[Hh Hm]" => //.
{ apply auth_both_valid_discrete. split => //. eauto using to_heap_valid. }
move => Hnew Hwp. apply: wp_strong_adequacy. move => ?.
set h := to_heap .
iMod (own_alloc ( h h)) as (γh) "[Hh _]" => //.
{ apply auth_both_valid_discrete. split => //. }
set f := to_fntbl fns.
iMod (own_alloc ( f f)) as (γf) "[Hf Hfm]" => //.
{ apply auth_both_valid_discrete. split => //. eauto using to_fntbl_valid. }
set b := to_allocs bs.
iMod (own_alloc ( b b)) as (γb) "[Hb #Hbm]" => //.
{ apply auth_both_valid_discrete. split => //. eauto using to_allocs_valid. }
set b := to_allocs .
iMod (own_alloc ( b b)) as (γb) "[Hb _]" => //.
{ apply auth_both_valid_discrete. split => //. }
set (HheapG := HeapG _ _ γh _ γb _ γf).
set (HrefinedCG := RefinedCG _ _ HheapG).
......@@ -86,23 +85,9 @@ Proof.
move: (Hwp HtypeG) => {Hwp} [gl [gt]].
set (Hglobals := {| global_locs := gl; global_initialized_types := gt; |}).
move => Hwp.
iMod (Hwp with "[Hm] [] [Hfm]") as "Hmains". {
rewrite /h => {h Hwp Hvalid}.
iInduction (gs) as [|i ????] "IH" using map_ind => //.
iApply big_sepM_insert => //.
rewrite fmap_insert to_heap_insert insert_singleton_op. 2: by apply lookup_to_heap_None; simplify_map_eq.
rewrite heap_mapsto_mbyte_eq /heap_mapsto_mbyte_def /=.
iDestruct "Hm" as "[$ Hm]".
by iApply "IH".
} {
rewrite /b => {b Hwp Hvalid}.
iInduction (bs) as [|??? HNone] "IH" using map_ind => //.
iApply big_sepM_insert => //. rewrite /to_allocs fmap_insert.
rewrite (insert_singleton_op); last by rewrite lookup_fmap HNone.
rewrite allocs_entry_eq. iDestruct "Hbm" as "[$ Hfm]".
by iApply "IH".
} {
rewrite /f => {f Hwp Hvalid}.
iMod (heap_alloc_new_blocks_upd with "[Hh Hf Hb]") as "[Hctx Hmt]" => //. { iFrame. }
iMod (Hwp with "Hmt [Hfm]") as "Hmains". {
rewrite /f => {f Hwp Hnew}.
iInduction (fns) as [] "IH" using map_ind => //.
iApply big_sepM_insert => //. rewrite to_fntbl_insert.
rewrite (insert_singleton_op); last by apply lookup_to_fntbl_None.
......@@ -111,7 +96,7 @@ Proof.
}
iModIntro. iExists NotStuck, _, (replicate (length thread_mains) (λ _, True%I)), _.
iSplitL "Hh Hb Hf"; last first. 1: iSplitL.
iSplitL "Hctx"; last first. 1: iSplitL.
- rewrite big_sepL2_fmap_l. iApply big_sepL2_replicate_2. iApply (big_sepL_impl with "Hmains").
iIntros "!#" (? main ?); iDestruct 1 as (P) "[Hmain HP]".
iApply wp_to_typed_stmt => //.
......@@ -125,84 +110,6 @@ Proof.
Qed.
(** * Helper functions for using the adequacy lemma *)
Definition block_to_loc (l: alloc_id): loc := (l, 0%Z).
Definition block_list_to_loc