Commit 3454e5c0 authored by David Swasey's avatar David Swasey

Verify the symbol ADT.

parent ff7eaf61
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth.
From iris_examples.logrel.F_mu_ref_conc Require Import rules typing.
From iris_examples.logrel.F_mu_ref_conc Require Import fundamental_unary.
(** Syntactic sugar. *)
Definition Lam (e : {bind expr}) := Rec e.[ren(+1)].
Definition LamV (e : {bind expr}) := RecV e.[ren(+1)].
Definition Let (e1 : expr) (e2: {bind expr}) := App (Lam e2) e1.
Definition LetCtx (e2 : expr) := AppRCtx (LamV e2).
(** Simple bind tactics. *)
(* These tactics are a bit *too* simple. They render the following
proof scripts more cluttered than they need to be wrt values and
evaluation contexts. For an approach that scales better, see the
heap language bundled with Iris. *)
Local Tactic Notation "wp_bind" uconstr(ctx) :=
iApply (wp_bind (fill ctx)).
Local Tactic Notation "wp_pure" :=
iApply wp_pure_step_later; first done; iNext.
Local Tactic Notation "use_bind_pure" uconstr(ctx) :=
wp_bind ctx; wp_pure; rewrite ?[fill _ _]/=.
Local Tactic Notation "use_bind" uconstr(ctx) uconstr(Hp) ident(v) constr(Hv) :=
wp_bind ctx; iApply Hp; first done; iNext; iIntros (v) Hv;
rewrite ?[fill _ _]/=.
(** Symbol ADT *)
Definition τinc : type := TArrow TUnit (TVar 0).
Definition inc : expr := Lam $ FAI $ Var 1.
Definition τcheck : type := TArrow (TVar 0) TUnit.
Definition check : expr := Lam $ Assert $ BinOp Lt (Var 0) $ Load $ Var 1.
Definition τsymbol : type := TExist $ TProd τinc τcheck.
Definition symbol : expr := Pack $ Let (Alloc $ #n 0) $ Pair inc check.
(** Ghost theory *)
Class symbolG Σ := SymbolG { symbol_inG :> inG Σ (authR mnatUR) }.
Definition symbolΣ : gFunctors := #[GFunctor (authR mnatUR)].
Instance subG_symbolΣ {Σ} : subG symbolΣ Σ symbolG Σ.
Proof. solve_inG. Qed.
Section symbol_ghosts.
Context `{!symbolG Σ}.
Definition Counter (γ : gname) (n : nat) : iProp Σ :=
(own γ ( (n : mnat)))%I.
Definition Symbol (γ : gname) (n : nat) : iProp Σ :=
(own γ ( (S n : mnat)))%I.
Global Instance Counter_timeless γ n : Timeless (Counter γ n).
Proof. apply _. Qed.
Global Instance Symbol_timeless γ n : Timeless (Symbol γ n).
Proof. apply _. Qed.
Lemma Counter_exclusive γ n1 n2 : Counter γ n1 Counter γ n2 False.
Proof. by rewrite -own_op own_valid auth_validI. Qed.
Global Instance Symbol_persistent γ n : Persistent (Symbol γ n).
Proof. apply _. Qed.
Lemma Counter_alloc n : (|==> γ, Counter γ n)%I.
Proof.
iMod (own_alloc ( (n:mnat) (n:mnat))) as (γ) "[Hγ Hγf]";
first done.
iExists γ. by iFrame.
Qed.
Lemma Counter_inc γ n :
Counter γ n == Counter γ (S n) Symbol γ n.
Proof.
rewrite -own_op.
apply own_update, auth_update_alloc, mnat_local_update.
omega.
Qed.
Lemma Symbol_obs γ s n : Counter γ n Symbol γ s s < n.
Proof.
iIntros "(Hc & Hs)".
iDestruct (own_valid_2 with "Hc Hs")
as %[?%mnat_included _]%auth_valid_discrete_2.
iPureIntro. omega.
Qed.
End symbol_ghosts.
Typeclasses Opaque Counter Symbol.
(** The symbol ADT can be semantically typed *)
Section symbol_proof.
Context `{heapIG Σ, symbolG Σ} (N : namespace).
Definition symbol_inv (γ : gname) (l : loc) : iProp Σ :=
( n, l ↦ᵢ (#nv n) Counter γ n)%I.
Definition symbol_ctx (γ : gname) (l : loc) : iProp Σ :=
(inv N (symbol_inv γ l)).
Definition SymbolV (γ : gname) : valC -n> iProp Σ := λne w,
( n, w = #nv n Symbol γ n)%I.
(* under our invariant, [(λ_. l++) V[τinc](Δ, Symbol)]. *)
Lemma type_inc Δ γ l :
symbol_ctx γ l τinc (SymbolV γ :: Δ) (LamV (FAI (Loc l))).
Proof.
iIntros "#Hctx /=". iAlways. iIntros (v) "->".
wp_pure. asimpl.
iInv N as (n) ">[Hl Hc]" "Hclose".
iApply (wp_fai with "Hl"). iIntros "!> Hl".
iMod (Counter_inc with "Hc") as "[Hc Hs]".
iMod ("Hclose" with "[Hl Hc]"); last by auto.
iExists (S n). by iFrame.
Qed.
(* under our invariant, [(λs. assert(s < *l)) V[τcheck](Δ, Symbol)]. *)
Lemma type_check Δ γ l :
symbol_ctx γ l τcheck (SymbolV γ :: Δ) $
LamV $ Assert $ BinOp Lt (Var 0) (Load (Loc l)).
Proof.
iIntros "#Hctx /=". iAlways. iIntros (v) "Hv".
iDestruct "Hv" as (s) "[-> Hs]". asimpl.
wp_pure. asimpl. rewrite -(of_to_val (#n s) (#nv s)) //.
wp_bind [BinOpRCtx _ _; AssertCtx]; simpl.
iInv N as (n) ">[Hl Hc]" "Hclose".
iDestruct (Symbol_obs with "[$Hc $Hs]") as "%".
iApply (wp_load with "Hl"). iIntros "!> Hl".
iMod ("Hclose" with "[Hl Hc]"). { iExists n. by iFrame. }
iModIntro. use_bind_pure [AssertCtx]; simpl.
destruct (lt_dec _ _); last done.
iApply wp_value. wp_pure. by iApply wp_value.
Qed.
Lemma type_symbol Γ : Γ symbol : τsymbol.
Proof.
iIntros (Δ vs _) "_". rewrite/symbol.
use_bind [LetCtx (Pair inc check); PackCtx] wp_alloc l "Hl".
iMod (Counter_alloc 0) as (γ) "Hc".
iMod (inv_alloc N _ (symbol_inv γ l) with "[Hl Hc]") as "#Hctx".
{ iNext. iExists 0. by iFrame. }
use_bind_pure [PackCtx]; asimpl.
iApply wp_value. iApply wp_value. iAlways.
iExists _, (SymbolV γ); iSplit; auto.
iSplit; first by iPureIntro; apply _.
iExists _, _; iSplit; auto. iSplit.
- by iApply (type_inc [] with "Hctx").
- by iApply (type_check [] with "Hctx").
Qed.
End symbol_proof.
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