Commit 982e612e authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Silly tweaks while reading the code: white space, order of quantifiers, ...

parent 76d85093
......@@ -48,11 +48,10 @@ Section vcg.
Definition mapsto_wand_list (E: known_locs) (m : denv) (Φ : iProp Σ ) : iProp Σ :=
mapsto_wand_list_aux E m Φ O.
Definition popstack (mOut : list denv) : option (list denv * denv) :=
match mOut with
Definition popstack (ms : list denv) : option (list denv * denv) :=
match ms with
| [] => None
| m::ms => Some (ms, m)
| m :: ms => Some (ms, m)
end.
Fixpoint vcg_sp (E: known_locs) (ms : list denv) (de : dcexpr)
......@@ -121,8 +120,10 @@ Section vcg.
(dloc_interp E (dLoc i) C[ULvl]{q} dval_interp E (dValUnknown v) -
Φ [] (dValUnknown v)))
end
| _ => mapsto_wand_list E m ( l : loc, dval_interp E dv = #l
( q v, l C{q} v (l C{q} v - Φ [] (dValUnknown v))))%I
| _ =>
mapsto_wand_list E m ( (l : loc) q v,
dval_interp E dv = #l
l C{q} v (l C{q} v - Φ [] (dValUnknown v)))%I
end%I.
Definition vcg_wp_store (E : known_locs) (dv1 dv2 : dval) (m : denv)
......@@ -137,10 +138,10 @@ Section vcg.
(dloc_interp E (dLoc i) C[LLvl] dval_interp E dv2 - Φ [] dv2))
end
| _ =>
mapsto_wand_list E m ( l : loc,
dval_interp E dv1 = #l v : val,
dloc_interp E (dLocUnknown l) C v
(dloc_interp E (dLocUnknown l) C[LLvl] dval_interp E dv2 - Φ [] dv2))%I
mapsto_wand_list E m ( (l : loc) (v : val),
dval_interp E dv1 = #l
dloc_interp E (dLocUnknown l) C v
(dloc_interp E (dLocUnknown l) C[LLvl] dval_interp E dv2 - Φ [] dv2))%I
end%I.
Definition vcg_wp_bin_op (E : known_locs) (op : bin_op) (dv1 dv2 : dval)
......@@ -205,15 +206,12 @@ Section vcg_spec.
(λ '{| denv_level := lv; denv_frac := q; denv_dval := dv |},
default 1%positive (E !! (k + n)%nat) C[lv]{q} dval_interp E dv) True dio) - Φ.
Proof.
generalize dependent k.
induction m; simpl. eauto.
iIntros (k) "H1 [Hl H2]".
destruct a as [[x q dv]|]; simpl.
- rewrite -plus_n_O. iSpecialize ("H1" with "Hl").
iApply (IHm with "H1 [H2]"). iApply (big_sepL_mono with "H2").
intros n y ?. simpl. assert ((k + S n)%nat = (S k + n)%nat) as -> by omega. done.
- iApply (IHm with "H1 [H2]"). iApply (big_sepL_mono with "H2").
intros n y ?. simpl. assert ((k + S n)%nat = (S k + n)%nat) as -> by omega. done.
iIntros "H". iInduction m as [|[[x q dv]|]] "IH" forall (k); simpl; first auto.
- iIntros "[H1 H2]". rewrite -plus_n_O. iSpecialize ("H" with "H1").
iApply ("IH" with "H [H2]"). iApply (big_sepL_impl with "H2").
iIntros "!>" (n y ?) "/= H". by replace (k + S n)%nat with (S k + n)%nat by omega.
- iIntros "[_ H2]". iApply ("IH" with "H [H2]"). iApply (big_sepL_impl with "H2").
iIntros "!>" (n y ?) "/= H". by replace (k + S n)%nat with (S k + n)%nat by omega.
Qed.
Lemma mapsto_wand_list_spec E m Φ :
......@@ -248,9 +246,7 @@ Section vcg_spec.
- destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
destruct (dbin_op_eval E b dv1 dv2) eqn:Hboe; simplify_eq/=.
transitivity (length ms1).
+ by eapply IHde1.
+ by eapply IHde2.
transitivity (length ms1); eauto.
- destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hde; simplify_eq/=.
destruct (dun_op_eval E u dv1); simplify_eq/=.
by eapply IHde.
......@@ -476,9 +472,11 @@ Section vcg_spec.
denv_wf E m
denv_interp E m -
vcg_wp_load E dv m (Φ E) -
(l:loc) q w, dval_interp E dv = #l l C{q} w (l C{q} w -
E' dv' m', E `prefix_of` E' dval_interp E' dv' = w dval_wf E' dv'
denv_wf E' m' denv_interp E' m' Φ E' m' dv').
(l : loc) q w,
dval_interp E dv = #l
l C{q} w (l C{q} w - E' dv' m',
E `prefix_of` E' dval_interp E' dv' = w dval_wf E' dv'
denv_wf E' m' denv_interp E' m' Φ E' m' dv').
Proof.
rewrite /vcg_wp_load. destruct (is_dloc E dv) as [i|] eqn:Hdloc.
+ destruct (denv_lookup i m) as [[q dv'] |] eqn:Hlkp; simpl; simplify_eq /=.
......@@ -498,7 +496,7 @@ Section vcg_spec.
unfold denv_interp, denv_wf. eauto.
+ rewrite mapsto_wand_list_spec. iIntros (Hmwf) "Hm Hwp".
iSpecialize ("Hwp" with "Hm"); simpl.
iDestruct "Hwp" as (l) "(-> & Hwp)". iDestruct "Hwp" as (q v') "[Hl Hwp]".
iDestruct "Hwp" as (l q v' ->) "[Hl Hwp]".
iExists l, q, v'. iSplit; first done.
iFrame. iIntros "Hl". iSpecialize ("Hwp" with "Hl").
iExists E, (dValUnknown v'), []; iSplit; first done.
......@@ -511,34 +509,34 @@ Section vcg_spec.
denv_interp E m -
vcg_wp_bin_op E b dv1 dv2 (denv_merge mOut m) (Φ E) -
denv_interp E mOut -
w : val, bin_op_eval b (dval_interp E dv1) (dval_interp E dv2) = Some w
( E' dv m', E0 `prefix_of` E' dval_interp E' dv = w dval_wf E' dv
denv_wf E' m' denv_interp E' m' Φ E' m' dv).
w E' dv m',
bin_op_eval b (dval_interp E dv1) (dval_interp E dv2) = Some w
E0 `prefix_of` E' dval_interp E' dv = w dval_wf E' dv
denv_wf E' m' denv_interp E' m' Φ E' m' dv.
Proof.
iIntros (Hpre Hwf1 Hwf2 Hwf3) "Hm Hwp HmOut". rewrite /vcg_wp_bin_op.
destruct (dbin_op_eval E b dv1 dv2) as [ | dw | dw ] eqn:Hbin; first done.
* iExists (dval_interp E dw); iSplit.
* iExists (dval_interp E dw), E, dw, (denv_merge mOut m); iSplit.
{ iPureIntro. apply dbin_op_eval_correct. by rewrite Hbin. }
iExists E, dw, (denv_merge mOut m).
apply dbin_op_eval_dSome_wf in Hbin; try done.
rewrite -denv_merge_interp //. eauto with iFrame.
* destruct dw as [dw1|] eqn:Hdw; last done.
iExists (dval_interp E dw1); iSplit.
iExists (dval_interp E dw1), E, dw1, (denv_merge mOut m); iSplit.
iPureIntro. apply dbin_op_eval_correct. by rewrite Hbin.
iExists E, dw1, (denv_merge mOut m).
rewrite -denv_merge_interp.
apply dbin_op_eval_dUnknown_wf in Hbin; try done. eauto with iFrame.
Qed.
Lemma vcg_wp_store_correct E0 E m dv1 dv2 Φ :
E0 `prefix_of` E
denv_wf E m
dval_wf E dv2
denv_interp E m -
vcg_wp_store E dv1 dv2 m (Φ E) -
(l : loc) (w : val), dval_interp E dv1 = #l
l C w (l C[LLvl] dval_interp E dv2 -
E' dv m', E0 `prefix_of` E' dval_interp E' dv = dval_interp E dv2
E0 `prefix_of` E
denv_wf E m
dval_wf E dv2
denv_interp E m -
vcg_wp_store E dv1 dv2 m (Φ E) -
(l : loc) (w : val),
dval_interp E dv1 = #l
l C w (l C[LLvl] dval_interp E dv2 - E' dv m',
E0 `prefix_of` E' dval_interp E' dv = dval_interp E dv2
dval_wf E' dv denv_wf E' m' denv_interp E' m' Φ E' m' dv).
Proof.
iIntros (Hpre Hwf Hwf2) "Hm Hwp". rewrite{1} /vcg_wp_store; fold vcg_wp.
......@@ -560,8 +558,7 @@ Section vcg_spec.
iExists E, dv2, []; repeat (iSplit; first done). unfold denv_interp. by iFrame.
- rewrite mapsto_wand_list_spec.
iSpecialize ("Hwp" with "[Hm]"); iFrame.
iDestruct "Hwp" as (l ->) "Hwp";
iDestruct "Hwp" as (v) "[Hdv Hwp]";
iDestruct "Hwp" as (l v ->) "[Hdv Hwp]".
iExists l,v ; iSplit; first done. iFrame.
iIntros "Hl". iSpecialize ("Hwp" with "Hl").
iExists E, dv2, []; repeat (iSplit; first done). unfold denv_interp. by iFrame.
......@@ -633,8 +630,8 @@ Section vcg_spec.
iDestruct "Hex" as (E' dv1 m1 Hpre <- Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=.
rewrite (dval_interp_mono E E' dv2); eauto.
iPoseProof (denv_interp_mono with "Hm'") as "Hm'"; [done | done |].
iApply (vcg_wp_bin_op_correct with "Hm' Hwp [HmNew]");
eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
iDestruct (vcg_wp_bin_op_correct with "Hm' Hwp [HmNew]") as (w E'' dv m'' ?) "?";
eauto 10 using dval_wf_mono, denv_wf_merge, denv_wf_mono.
iApply (denv_interp_mono with "HmNew"); eauto.
+ iPoseProof (vcg_sp'_correct) as "Hsp"; first eassumption.
specialize (vcg_sp'_wf _ _ _ _ _ _ Hmwf Hwf1 Heqsp) as (?&?&?).
......@@ -646,8 +643,8 @@ Section vcg_spec.
iDestruct "Hex" as (E' dv2 m2 Hpre <- Hm'wf) "(% & Hm' & Hwp)"; simplify_eq /=.
rewrite (dval_interp_mono E E' dv1); eauto.
iPoseProof (denv_interp_mono with "Hm'") as "Hm'"; [done | done |].
iApply (vcg_wp_bin_op_correct with "Hm' Hwp [HmNew]");
eauto using dval_wf_mono, denv_wf_merge, denv_wf_mono.
iDestruct (vcg_wp_bin_op_correct with "Hm' Hwp [HmNew]") as (w E'' dv m'' ?) "?";
eauto 10 using dval_wf_mono, denv_wf_merge, denv_wf_mono.
iApply (denv_interp_mono with "HmNew"); eauto.
- rewrite IHde //. iApply a_un_op_spec. iSpecialize ("Hm" with "Hwp").
iApply (awp_wand with "Hm"). iIntros (v) "Hex".
......
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