lifting.v 1.34 KB
Newer Older
Dan Frumin's avatar
Dan Frumin committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40
From iris.heap_lang Require Export proofmode notation.
From iris.algebra Require Import frac auth.
From iris.base_logic.lib Require Import fractional.
From iris_c.lib Require Export locking_heap mset flock.
From iris_c.c_translation Require Export monad.

Section lifting.
  Context `{locking_heapG Σ, heapG Σ, flockG Σ}.

  Lemma awp_value (ve : expr) (v : val) R Φ :
    IntoVal ve v 
    Φ v -
    awp (λ: <> <>, ve) R Φ.
  Proof.
    intros ?. rewrite -(of_to_val ve v); last done.
    iIntros "HΦ". rewrite /awp.
    iIntros (γ π env lk) "Hfl Hunfl".
    do 2 wp_rec. by iFrame.
  Qed.

  Lemma awp_pure K φ e1 e2 R Φ :
    PureExec φ e1 e2 
    φ 
     awp (fill K e2) R Φ -
    awp (fill K e1) R Φ.
  Proof.
    iIntros (? Hφ) "Hawp".
    rewrite /awp. iIntros (γ π env l) "#Hflock Hunfl".
    replace ((fill K e1) env l) with (fill (K++[AppLCtx (of_val env);AppLCtx (of_val l)]) e1); last first.
    { by rewrite fill_app. }
    iApply (wp_bind (fill (K++[AppLCtx (of_val env);AppLCtx (of_val l)]))).
    wp_pure e1.
    iSpecialize ("Hawp" with "Hflock Hunfl").
    replace ((fill K e2) env l) with (fill (K++[AppLCtx (of_val env);AppLCtx (of_val l)]) e2); last first.
    { by rewrite fill_app. }
    rewrite (wp_bind_inv (fill (K++[AppLCtx (of_val env);AppLCtx (of_val l)]))).
    by iApply "Hawp".
  Qed.

End lifting.