Commit b07aea79 authored by Dan Frumin's avatar Dan Frumin

Add `awp_ctx_bind`

parent ccd60df8
......@@ -9,3 +9,4 @@ theories/c_translation/monad.v
theories/c_translation/lifting.v
theories/c_translation/proofmode.v
theories/c_translation/translation.v
theories/tests/test1.v
......@@ -37,4 +37,24 @@ Section lifting.
by iApply "Hawp".
Qed.
Lemma awp_ctx_bind (v1 v2 : val) (e1 e2 : expr) R Φ :
IntoVal e1 v1
IntoVal e2 v2
awp e2 R (fun w => awp (e1 w) R Φ) -
awp (a_bind e1 e2) R Φ.
Proof.
intros <-%of_to_val <-%of_to_val.
iIntros "HAWP". rewrite /awp.
iIntros (γ π env l) "#Hflock Hunfl".
rewrite /a_bind. wp_rec. wp_rec. wp_rec. wp_rec.
wp_bind (v2 env l).
iApply (wp_wand with "[HAWP Hunfl]").
{ by iApply "HAWP". }
iIntros (w) "[H Hunfl]".
wp_rec. by iApply "H".
Qed.
End lifting.
Notation "a ;;; b" := (a_bind (λ: <>, b) a)%E (at level 80, right associativity).
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
From iris.algebra Require Import frac auth.
From iris.base_logic.lib Require Import fractional.
From iris_c.lib Require Import locking_heap mset flock U.
From iris_c.c_translation Require Import monad lifting proofmode translation.
Section test.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Lemma test1 (l : loc) :
l L #1 -
awp (a_seq;;; a_load (a_ret #l))%E True (fun v => v = #1).
Proof.
iIntros "Hl".
iApply awp_ctx_bind.
iApply a_seq_spec.
rewrite U_unlock. iRevert "Hl". rewrite -(U_mono (l U #1) (awp _ _ _))%I. eauto.
iIntros "Hl". awp_pure _.
iApply (a_load_spec with "Hl"). iIntros "Hl". eauto.
Qed.
End test.
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