Commit 075f1b72 authored by Dan Frumin's avatar Dan Frumin
Browse files

Add `wp_quote_store`

parent dd523881
......@@ -42,16 +42,27 @@ Section vcg.
iIntros (?); iDestruct 1 as (l v ->) "[Hl H]".
iDestruct "H" as (k [= ->]) "H /=". wp_load. by iApply "H".
Qed.
Global Instance wp_quote_bin_op op e1 e2 Φ t t' :
( v1, WpQuote e2 (λ v2, IsSome (bin_op_eval op v1 v2) Φ) (t v1))
WpQuote e1 t t'
WpQuote (BinOp op e1 e2) Φ t'.
Global Instance wp_quote_bin_op op e1 e2 Φ Ψ t :
( v1, WpQuote e2 (λ v2, IsSome (bin_op_eval op v1 v2) Φ) (Ψ v1))
WpQuote e1 Ψ t
WpQuote (BinOp op e1 e2) Φ t.
Proof.
rewrite /WpQuote /= => He2 ->. iIntros "H".
wp_apply (wp_wand with "H"); iIntros (v1) "H". rewrite He2.
wp_apply (wp_wand with "H"); iIntros (v2). iDestruct 1 as (v ?) "H".
by wp_op.
Qed.
Global Instance wp_quote_store e1 e2 Φ Ψ t :
( l, WpQuote e2 (λ v2, Inhale l (λ _, Exhale l v2 (Φ #()))) (Ψ l))
WpQuote e1 Ψ t
WpQuote (Store e1 e2) Φ t.
Proof.
rewrite /WpQuote /= => He2 ->. iIntros "H".
wp_apply (wp_wand with "H"); iIntros (v1) "H". rewrite He2.
wp_apply (wp_wand with "H"); iIntros (v2). iDestruct 1 as (l v ->) "[Hl H]".
iDestruct "H" as (?) "[% H]". simplify_eq/=.
wp_store. by iApply "H".
Qed.
Fixpoint vcg (e: expr) (Φ: val wp_expr) : wp_expr :=
match e with
......
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