Skip to content

GitLab

R
ReLoC-v1
Commit 9dc6e3a8 authored by Dan Frumin's avatar Dan Frumin
Browse files
Options

Merge branch 'master' of bitbucket.org:Danya/iris-logrel

parents 545272f2 c7f5f4cc
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 290 additions and 289 deletions
README.md
View file @ 9dc6e3a8
......@@ -5,8 +5,8 @@ This version is known to compile with:
- Coq 8.6.1
- Ssreflect 1.6
- Autosubst branch [coq86-devel](https://github.com/uds-psl/autosubst/tree/coq86-devel)
- std++ version [fa6ff9d18aefb29e839e815aa170262d330bd108](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/tree/fa6ff9d18aefb29e839e815aa170262d330bd108)
- Iris version [d85fdb0ea89edebcd10056e073ab9c7edc6c2050](https://gitlab.mpi-sws.org/FP/iris-coq/tree/d85fdb0ea89edebcd10056e073ab9c7edc6c2050)
- std++ version [24aef2fea9481e65d1f6658005ddde25ae9a64ee](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/tree/24aef2fea9481e65d1f6658005ddde25ae9a64ee)
- Iris version [f96a894b14fe7095bb5ac5b937abd31e40316858](https://gitlab.mpi-sws.org/FP/iris-coq/tree/f96a894b14fe7095bb5ac5b937abd31e40316858)
# Compilation
......
theories/F_mu_ref_conc/binder.v
View file @ 9dc6e3a8
......@@ -153,8 +153,8 @@ Proof.
by rewrite fmap_insert.
Qed.
Lemma delete_idem_binder {A} (x : binder) (m : stringmap A) :
Lemma delete_idemp_binder {A} (x : binder) (m : stringmap A) :
delete x (delete x m) = delete x m.
Proof.
destruct x; cbn; eauto. apply delete_idem.
destruct x; cbn; eauto. apply delete_idemp.
Qed.
theories/F_mu_ref_conc/lang.v
View file @ 9dc6e3a8
......@@ -55,11 +55,6 @@ Module lang.
| CAS (e0 : expr) (e1 : expr) (e2 : expr).
Bind Scope expr_scope with expr.
(* Notation for bool and nat *)
Notation "#♭ b" := (Lit (Bool b)) (at level 20).
Notation "#n n" := (Lit (Nat n)) (at level 20).
Notation "#l l" := (Lit (Loc l)) (at level 20).
Instance literal_dec_eq (l l' : literal) : Decision (l = l').
Proof. solve_decision. Defined.
......@@ -108,18 +103,15 @@ Module lang.
Bind Scope val_scope with val.
(* Notation for bool and nat *)
Notation "'#♭v' b" := (LitV (Bool b)) (at level 20).
Notation "'#nv' n" := (LitV (Nat n)) (at level 20).
Fixpoint binop_eval (op : binop) (v1 v2 : val) : option val :=
match op,v1,v2 with
| Add,#nv a,#nv b => Some $ #nv(a + b)
| Sub,#nv a,#nv b => Some $ #nv(a - b)
| Eq,#nv a,#nv b => Some $ if (eq_nat_dec a b) then #♭v true else #♭v false
| Eq,#♭v a,#♭v b => Some $ #♭v(eqb a b)
| Le,#nv a,#nv b => Some $ if (le_dec a b) then #♭v true else #♭v false
| Lt,#nv a,#nv b => Some $ if (lt_dec a b) then #♭v true else #♭v false
| Xor,#♭v a,#♭v b => Some $ #♭v(xorb a b)
| Add, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a + b))
| Sub, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a - b))
| Eq, LitV (Nat a), LitV (Nat b) => Some $ if eq_nat_dec a b then LitV (Bool true) else LitV (Bool false)
| Eq, LitV (Bool a), LitV (Bool b) => Some $ LitV (Bool (eqb a b))
| Le, LitV (Nat a), LitV (Nat b) => Some $ if le_dec a b then LitV (Bool true) else LitV (Bool false)
| Lt, LitV (Nat a), LitV (Nat b) => Some $ if lt_dec a b then LitV (Bool true) else LitV (Bool false)
| Xor, LitV (Bool a), LitV (Bool b) => Some $ LitV (Bool (xorb a b))
| _,_,_ => None
end.
Instance val_inh : Inhabited val := populate (LitV Unit).
......@@ -300,9 +292,9 @@ Module lang.
head_step (BinOp op e1 e2) σ (of_val v) σ []
(* If then else *)
| IfFalse e1 e2 σ :
head_step (If (#♭ false) e1 e2) σ e2 σ []
head_step (If (Lit (Bool false)) e1 e2) σ e2 σ []
| IfTrue e1 e2 σ :
head_step (If (#♭ true) e1 e2) σ e1 σ []
head_step (If (Lit (Bool true)) e1 e2) σ e1 σ []
(* Recursive Types *)
| Unfold_Fold e v σ :
to_val e = Some v →
......@@ -333,11 +325,11 @@ Module lang.
| CasFailS l e1 v1 e2 v2 vl σ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
σ !! l = Some vl → vl ≠ v1 →
head_step (CAS (Lit (Loc l)) e1 e2) σ (#♭ false) σ []
head_step (CAS (Lit (Loc l)) e1 e2) σ (Lit (Bool false)) σ []
| CasSucS l e1 v1 e2 v2 σ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
σ !! l = Some v1 →
head_step (CAS (Lit (Loc l)) e1 e2) σ (#♭ true) (<[l:=v2]>σ) [].
head_step (CAS (Lit (Loc l)) e1 e2) σ (Lit (Bool true)) (<[l:=v2]>σ) [].
Definition is_atomic (e : expr) : Prop :=
match e with
......
theories/F_mu_ref_conc/notation.v
View file @ 9dc6e3a8
......@@ -12,7 +12,6 @@ Coercion of_val : val >-> expr.
Coercion Nat : nat >-> literal.
Coercion Bool : bool >-> literal.
Coercion Loc : loc >-> literal.
Notation "'tt'" := lang.Unit.
Notation "()" := lang.Unit : val_scope.
(* No scope for the values, does not conflict and scope is often not inferred
......@@ -36,15 +35,11 @@ Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)).
Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
(Match e0 x1%bind e1 x2%bind e2)
(e0, x1, e1, x2, e2 at level 200,
format "'[' 'match:' e0 'with' '/' '[hv' 'InjL' x1 => '[' e1 ']' '/' | 'InjR' x2 => '[' e2 ']' '/' 'end' ']' ']'") : expr_scope.
format "'[hv' 'match:' e0 'with' '/ ' '[' 'InjL' x1 => '/ ' e1 ']' '/' '[' | 'InjR' x2 => '/ ' e2 ']' '/' 'end' ']'") : expr_scope.
Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" :=
(Match e0 x2%bind e2 x1%bind e1)
(e0, x1, e1, x2, e2 at level 200, only parsing) : expr_scope.
Notation "'case:' e0 'of' 'InjL' => e1 | 'InjR' => e2 'end'" :=
(Case e0 e1 e2)
(e0, e1, e2 at level 200) : expr_scope.
Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope.
Notation "'ref' e" := (Alloc e%E)
(at level 30, right associativity) : expr_scope.
......@@ -60,19 +55,33 @@ Notation "e1 ⊕ e2" := (BinOp Xor e1%E e2%E) (at level 70) : expr_scope.
(* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope.
Notation "'rec:' f x := e" := (Rec f%bind x%bind e%E)
(at level 102, f at level 1, x at level 1, e at level 200) : expr_scope.
(at level 102, f at level 1, x at level 1, e at level 200,
format "'[' 'rec:' f x := '/ ' e ']'") : expr_scope.
Notation "'rec:' f x := e" := (locked (RecV f%bind x%bind e%E))
(at level 102, f at level 1, x at level 1, e at level 200) : val_scope.
(at level 102, f at level 1, x at level 1, e at level 200,
format "'[' 'rec:' f x := '/ ' e ']'") : val_scope.
Notation "'rec:' f x y .. z := e" := (Rec f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
(at level 102, f, x, y, z at level 1, e at level 200,
format "'[' 'rec:' f x y .. z := '/ ' e ']'") : expr_scope.
Notation "'rec:' f x y .. z := e" := (locked (RecV f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..)))
(at level 102, f, x, y, z at level 1, e at level 200,
format "'[' 'rec:' f x y .. z := '/ ' e ']'") : val_scope.
Notation "λ: x , e" := (Lam x%bind e%E)
(at level 102, x at level 1, e at level 200) : expr_scope.
(at level 102, x at level 1, e at level 200,
format "'[' 'λ:' x , '/ ' e ']'") : expr_scope.
Notation "λ: x y .. z , e" := (Lam x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
(at level 102, x, y, z at level 1, e at level 200) : expr_scope.
(at level 102, x, y, z at level 1, e at level 200,
format "'[' 'λ:' x y .. z , '/ ' e ']'") : expr_scope.
Notation "λ: x , e" := (locked (LamV x%bind e%E))
(at level 102, x at level 1, e at level 200) : val_scope.
(at level 102, x at level 1, e at level 200,
format "'[' 'λ:' x , '/ ' e ']'") : val_scope.
Notation "λ: x y .. z , e" := (locked (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. )))
(at level 102, x, y, z at level 1, e at level 200) : val_scope.
(at level 102, x, y, z at level 1, e at level 200,
format "'[' 'λ:' x y .. z , '/ ' e ']'") : val_scope.
Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
(at level 200, e1, e2, e3 at level 200) : expr_scope.
......@@ -86,7 +95,8 @@ Notation "'Λ:' e" := (TLamV e%E)
Notation "'let:' x := e1 'in' e2" := (Lam x%bind e2%E e1%E)
(at level 102, x at level 1, e1, e2 at level 200,
format "'[' '[hv' 'let:' x := '[' e1 ']' 'in' ']' '/' e2 ']'") : expr_scope.
format "'[' 'let:' x := '[' e1 ']' 'in' '/' e2 ']'") : expr_scope.
Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
(at level 100, e2 at level 200, format "e1 ;; e2") : expr_scope.
(at level 100, e2 at level 200,
format "'[' '[' e1 ']' ;; '/' e2 ']'") : expr_scope.
theories/F_mu_ref_conc/rules.v
View file @ 9dc6e3a8
......@@ -40,7 +40,7 @@ Section lang_rules.
(** Base axioms for core primitives of the language: Stateful reductions. *)
Lemma wp_alloc E e v :
to_val e = Some v →
{{{ True }}} Alloc e @ E {{{ l, RET (LitV (Loc l))%E; l ↦ᵢ v }}}.
{{{ True }}} Alloc e @ E {{{ l, RET #l; l ↦ᵢ v }}}.
Proof.
iIntros (<-%of_to_val Φ) "HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>"; iSplit; first by auto.
......@@ -50,7 +50,7 @@ Section lang_rules.
Qed.
Lemma wp_load E l q v :
{{{ ▷ l ↦ᵢ{q} v }}} (! # l)%E @ E {{{ RET v; l ↦ᵢ{q} v }}}.
{{{ ▷ l ↦ᵢ{q} v }}} ! #l @ E {{{ RET v; l ↦ᵢ{q} v }}}.
Proof.
iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
......@@ -58,11 +58,11 @@ Section lang_rules.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
Lemma wp_store E l v' e v :
to_val e = Some v →
{{{ ▷ l ↦ᵢ v' }}} # l <- e @ E
{{{ RET (LitV tt); l ↦ᵢ v }}}.
{{{ ▷ l ↦ᵢ v' }}} #l <- e @ E
{{{ RET #(); l ↦ᵢ v }}}.
Proof.
iIntros (<-%of_to_val Φ) ">Hl HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
......@@ -74,8 +74,8 @@ Section lang_rules.
Lemma wp_cas_fail E l q v' e1 v1 e2 v2 :
to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 →
{{{ ▷ l ↦ᵢ{q} v' }}} CAS (# l) e1 e2 @ E
{{{ RET (LitV false); l ↦ᵢ{q} v' }}}.
{{{ ▷ l ↦ᵢ{q} v' }}} CAS #l e1 e2 @ E
{{{ RET #false; l ↦ᵢ{q} v' }}}.
Proof.
iIntros (<-%of_to_val <-%of_to_val ? Φ) ">Hl HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
......@@ -87,8 +87,8 @@ Section lang_rules.
Lemma wp_cas_suc E l e1 v1 e2 v2 :
to_val e1 = Some v1 → to_val e2 = Some v2 →
{{{ ▷ l ↦ᵢ v1 }}} CAS (# l) e1 e2 @ E
{{{ RET (LitV true); l ↦ᵢ v2 }}}.
{{{ ▷ l ↦ᵢ v1 }}} CAS #l e1 e2 @ E
{{{ RET #true; l ↦ᵢ v2 }}}.
Proof.
iIntros (<-%of_to_val <-%of_to_val Φ) ">Hl HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
......@@ -172,7 +172,7 @@ Section lang_rules.
Lemma wp_case_inl E e0 v0 e1 e2 Φ :
to_val e0 = Some v0 →
▷ WP (App e1 e0) @ E {{ Φ }} ⊢ WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
▷ WP App e1 e0 @ E {{ Φ }} ⊢ WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_head_step_no_fork (Case _ _ _) _); eauto.
intros; inv_head_step; eauto.
......@@ -180,17 +180,17 @@ Section lang_rules.
Lemma wp_case_inr E e0 v0 e1 e2 Φ :
to_val e0 = Some v0 →
▷ WP (App e2 e0) @ E {{ Φ }} ⊢ WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
▷ WP App e2 e0 @ E {{ Φ }} ⊢ WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_head_step_no_fork (Case _ _ _)); eauto.
intros; inv_head_step; eauto.
Qed.
Lemma wp_fork E e Φ :
▷ (|={E}=> Φ (LitV tt)) ∗ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
▷ (|={E}=> Φ #()) ∗ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
Proof.
rewrite -(wp_lift_pure_det_head_step (Fork e) #tt [e]) //=; eauto.
- rewrite -(wp_value_fupd _ _ (Lit tt)); auto.
rewrite -(wp_lift_pure_det_head_step (Fork e) #() [e]) //=; eauto.
- rewrite -(wp_value_fupd _ _ #()); auto.
by rewrite -step_fupd_intro // right_id later_sep.
- intros; inv_head_step; eauto.
Qed.
......
theories/F_mu_ref_conc/subst.v
View file @ 9dc6e3a8
......@@ -384,8 +384,8 @@ Proof.
by rewrite (delete_commute_binder _ f (BNamed x)).
+ apply not_and_l in H0 as [<-%dec_stable|<-%dec_stable].
* rewrite (delete_commute_binder _ x0 (BNamed x)).
by rewrite delete_idem_binder.
* by rewrite delete_idem_binder.
by rewrite delete_idemp_binder.
* by rewrite delete_idemp_binder.
Qed.
Lemma subst_p_rec (x1 x2 : binder) v1 v2 e :
......
theories/F_mu_ref_conc/typing.v
View file @ 9dc6e3a8
......@@ -44,10 +44,10 @@ Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level).
Inductive typed (Γ : stringmap type) : expr → type → Prop :=
| Var_typed x τ : Γ !! x = Some τ → Γ ⊢ₜ Var x : τ
| Unit_typed : Γ ⊢ₜ #tt : TUnit
| Nat_typed (n : nat) : Γ ⊢ₜ #n n : TNat
| Bool_typed (b : bool) : Γ ⊢ₜ #♭ b : TBool
| BinOp_typed_nat op e1 e2 τ :
| Unit_typed : Γ ⊢ₜ #() : TUnit
| Nat_typed (n : nat) : Γ ⊢ₜ # n : TNat
| Bool_typed (b : bool) : Γ ⊢ₜ # b : TBool
| BinOp_typed_nat op e1 e2 τ :
Γ ⊢ₜ e1 : TNat → Γ ⊢ₜ e2 : TNat →
binop_nat_res_type op = Some τ →
Γ ⊢ₜ BinOp op e1 e2 : τ
......@@ -133,14 +133,14 @@ Tactic Notation "solve_typed" := solve_typed 50.
(** Typeability of binops *)
Lemma binop_nat_typed_safe (op : binop) (n1 n2 : nat) τ :
binop_nat_res_type op = Some τ → is_Some (binop_eval op (#nv n1) (#nv n2)).
binop_nat_res_type op = Some τ → is_Some (binop_eval op #n1 #n2).
Proof.
destruct op; simpl; eauto.
inversion 1.
Qed.
Lemma binop_bool_typed_safe (op : binop) (b1 b2 : bool) τ :
binop_bool_res_type op = Some τ → is_Some (binop_eval op (#♭v b1) (#♭v b2)).
binop_bool_res_type op = Some τ → is_Some (binop_eval op #b1 #b2).
Proof.
destruct op; simpl; eauto; try by inversion 1.
Qed.
......
theories/examples/bit.v
View file @ 9dc6e3a8
From iris.proofmode Require Import tactics.
From iris.algebra Require Import agree (* TODO: Why do we need to import this? *).
From iris_logrel Require Import logrel.
Definition bitτ : type :=
......@@ -54,7 +53,7 @@ Section bit_refinement.
(* This is the graph of the `bitf` function *)
Program Definition bitτi : prodC valC valC -n> iProp Σ := λne vv,
(∃ b, ⌜vv.1 = #♭v b⌝ ∗ ⌜vv.2 = #nv (bitf b)⌝)%I.
(∃ b : bool, ⌜vv.1 = #b⌝ ∗ ⌜vv.2 = #(bitf b)⌝)%I.
Next Obligation. solve_proper. Qed.
Instance bitτi_persistent ww : PersistentP (bitτi ww).
......
theories/examples/counter.v
View file @ 9dc6e3a8
......@@ -27,8 +27,7 @@ Definition FG_counter : val := λ: <>,
Section CG_Counter.
Context `{logrelG Σ}.
Variable (Δ : list (prodC valC valC -n> iProp Σ)).
Open Scope expr_scope.
(* Coarse-grained increment *)
Lemma CG_increment_type Γ :
typed Γ CG_increment (TArrow (Tref TNat) (TArrow LockType (TArrow TUnit TUnit))).
......@@ -38,10 +37,10 @@ Section CG_Counter.
Lemma bin_log_related_CG_increment_r Γ K E1 E2 t τ (x l : loc) (n : nat) :
nclose specN ⊆ E1 →
(x ↦ₛ (#nv n) -∗ l ↦ₛ (#♭v false) -∗
(x ↦ₛ (#nv S n) -∗ l ↦ₛ (#♭v false) -∗
({E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (Lit tt) : τ)) -∗
{E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((CG_increment $/ (LitV (Loc x)) $/ LitV (Loc l)) #())%E : τ)%I.
(x ↦ₛ # n -∗ l ↦ₛ #false -∗
(x ↦ₛ # (S n) -∗ l ↦ₛ #false -∗
({E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K #() : τ)) -∗
{E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((CG_increment $/ (LitV (Loc x)) $/ LitV (Loc l)) #()) : τ)%I.
Proof.
iIntros (?) "Hx Hl Hlog".
unfold CG_increment. unlock. simpl_subst/=.
......@@ -76,9 +75,9 @@ Section CG_Counter.
Hint Resolve FG_increment_type : typeable.
Lemma bin_log_FG_increment_l Γ K E x n t τ :
x ↦ᵢ (#nv n) -∗
(x ↦ᵢ (#nv (S n)) -∗ {E,E;Δ;Γ} ⊨ fill K (Lit tt) ≤log≤ t : τ) -∗
Lemma bin_log_FG_increment_l Γ K E x (n : nat) t τ :
x ↦ᵢ #n -∗
(x ↦ᵢ # (S n) -∗ {E,E;Δ;Γ} ⊨ fill K #() ≤log≤ t : τ) -∗
{E,E;Δ;Γ} ⊨ fill K (FG_increment #x #()) ≤log≤ t : τ.
Proof.
iIntros "Hx Hlog".
......@@ -114,14 +113,13 @@ Section CG_Counter.
Definition counterN : namespace := nroot .@ "counter".
Definition counter_inv l cnt cnt' : iProp Σ :=
(∃ n, l ↦ₛ (#♭v false) ∗ cnt ↦ᵢ (#nv n) ∗ cnt' ↦ₛ (#nv n))%I.
(∃ n : nat, l ↦ₛ #false ∗ cnt ↦ᵢ #n ∗ cnt' ↦ₛ #n)%I.
Lemma bin_log_counter_read_r Γ E1 E2 K x n t τ
Lemma bin_log_counter_read_r Γ E1 E2 K x (n : nat) t τ
(Hspec : nclose specN ⊆ E1) :
x ↦ₛ (#nv n)
-∗ (x ↦ₛ (#nv n)
-∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (#n n)%E : τ)%I
-∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((counter_read $/ LitV (Loc x)) #())%E : τ.
x ↦ₛ #n -∗
(x ↦ₛ #n -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K #n : τ) -∗
{E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K ((counter_read $/ LitV (Loc x)) #()) : τ.
Proof.
iIntros "Hx Hlog".
unfold counter_read. unlock. simpl.
......@@ -134,20 +132,20 @@ Section CG_Counter.
a fine-grained increment with a baked in frame. *)
(* Unfortunately, the precondition is not baked in the rule so you can only use it when your spatial context is empty *)
Lemma bin_log_FG_increment_logatomic R Γ E1 E2 K x t τ :
□ (|={E1,E2}=> ∃ n, x ↦ᵢ (#nv n) ∗ R(n) ∗
((∃ n, x ↦ᵢ (#nv n) ∗ R(n)) ={E2,E1}=∗ True) ∧
(∀ m, x ↦ᵢ (#nv (S m)) ∗ R(m) -∗
{E2,E1;Δ;Γ} ⊨ fill K (Lit tt) ≤log≤ t : τ))
-∗ ({E1,E1;Δ;Γ} ⊨ fill K ((FG_increment $/ LitV (Loc x)) #())%E ≤log≤ t : τ).
□ (|={E1,E2}=> ∃ n : nat, x ↦ᵢ #n ∗ R n ∗
((∃ n : nat, x ↦ᵢ #n ∗ R n) ={E2,E1}=∗ True) ∧
(∀ m, x ↦ᵢ # (S m) ∗ R m -∗
{E2,E1;Δ;Γ} ⊨ fill K #() ≤log≤ t : τ))
-∗ ({E1,E1;Δ;Γ} ⊨ fill K ((FG_increment $/ LitV (Loc x)) #()) ≤log≤ t : τ).
Proof.
iIntros "#H".
unfold FG_increment. unlock. simpl.
iLöb as "IH".
rewrite {2}/FG_increment. unlock. simpl.
rel_rec_l.
iPoseProof "H" as "H2". (* lolwhat *)
rel_load_l_atomic.
iMod "H" as (n) "[Hx [HR Hrev]]". iModIntro.
iExists (#nv n). iFrame. iNext. iIntros "Hx".
iExists #n. iFrame. iNext. iIntros "Hx".
iDestruct "Hrev" as "[Hrev _]".
iApply fupd_logrel.
iMod ("Hrev" with "[HR Hx]").
......@@ -157,13 +155,13 @@ Section CG_Counter.
rel_cas_l_atomic.
iMod "H2" as (n') "[Hx [HR HQ]]". iModIntro. simpl.
destruct (decide (n = n')); subst.
- iExists (#nv n'). iFrame.
- iExists #n'. iFrame.
iSplitR; eauto. { iDestruct 1 as %Hfoo. exfalso. done. }
iIntros "_ !> Hx". simpl.
iDestruct "HQ" as "[_ HQ]".
iSpecialize ("HQ" $! n' with "[Hx HR]"). { iFrame. }
rel_if_true_l. done.
- iExists (#nv n'). iFrame.
- iExists #n'. iFrame.
iSplitL; eauto; last first.
{ iDestruct 1 as %Hfoo. exfalso. simplify_eq. }
iIntros "_ !> Hx". simpl.
......@@ -171,16 +169,17 @@ Section CG_Counter.
iDestruct "HQ" as "[HQ _]".
iMod ("HQ" with "[Hx HR]").
{ iExists _; iFrame. }
rewrite /FG_increment. unlock. simpl.
iApply "IH".
Qed.
(* A similar atomic specification for the counter_read fn *)
Lemma bin_log_counter_read_atomic_l R Γ E1 E2 K x t τ :
□ (|={E1,E2}=> ∃ n, x ↦ᵢ (#nv n) ∗ R(n) ∗
((∃ n, x ↦ᵢ (#nv n) ∗ R(n)) ={E2,E1}=∗ True) ∧
(∀ m, x ↦ᵢ (#nv m) ∗ R(m) -∗
{E2,E1;Δ;Γ} ⊨ fill K (#n m) ≤log≤ t : τ))
-∗ {E1,E1;Δ;Γ} ⊨ fill K ((counter_read $/ LitV (Loc x)) #())%E ≤log≤ t : τ.
□ (|={E1,E2}=> ∃ n : nat, x ↦ᵢ #n ∗ R n ∗
((∃ n : nat, x ↦ᵢ #n ∗ R n) ={E2,E1}=∗ True) ∧
(∀ m : nat, x ↦ᵢ #m ∗ R m -∗
{E2,E1;Δ;Γ} ⊨ fill K #m ≤log≤ t : τ))
-∗ {E1,E1;Δ;Γ} ⊨ fill K ((counter_read $/ LitV (Loc x)) #()) ≤log≤ t : τ.
Proof.
iIntros "#H".
unfold counter_read. unlock. simpl.
......@@ -206,7 +205,7 @@ Section CG_Counter.
{ unfold CG_increment. unlock; simpl_subst/=. solve_closed. }
iAlways. iIntros (v v') "[% %]"; simpl in *; subst.
iApply (bin_log_FG_increment_logatomic (fun n => (l ↦ₛ (#♭v false)) ∗ cnt' ↦ₛ #nv n)%I _ _ _ [] cnt with "[Hinv]").
iApply (bin_log_FG_increment_logatomic (fun n => (l ↦ₛ #false) ∗ cnt' ↦ₛ #n)%I _ _ _ [] cnt with "[Hinv]").
iAlways.
iInv counterN as ">Hcnt" "Hcl". iModIntro.
iDestruct "Hcnt" as (n) "[Hl [Hcnt Hcnt']]".
......@@ -236,7 +235,7 @@ Section CG_Counter.
{ unfold counter_read. unlock. simpl. solve_closed. }
{ unfold counter_read. unlock. simpl. solve_closed. }
iAlways. iIntros (v v') "[% %]"; simpl in *; subst.
iApply (bin_log_counter_read_atomic_l (fun n => (l ↦ₛ (#♭v false)) ∗ cnt' ↦ₛ #nv n)%I _ _ _ [] cnt with "[Hinv]").
iApply (bin_log_counter_read_atomic_l (fun n => (l ↦ₛ #false) ∗ cnt' ↦ₛ #n)%I _ _ _ [] cnt with "[Hinv]").
iAlways. iInv counterN as (n) "[>Hl [>Hcnt >Hcnt']]" "Hclose".
iModIntro.
iExists n. iFrame "Hcnt Hcnt' Hl". clear n.
......
theories/examples/lateearlychoice.v
View file @ 9dc6e3a8
......@@ -17,16 +17,15 @@ Section Refinement.
Definition choiceN : namespace := nroot .@ "choice".
Definition choice_inv y y' : iProp Σ :=
(∃ f, y ↦ᵢ (#♭v f) ∗ y' ↦ₛ (#♭v f))%I.
(∃ f : bool, y ↦ᵢ #f ∗ y' ↦ₛ #f)%I.
Lemma wp_rand :
(WP rand #() {{ v, ⌜v = #♭v true⌝ ∨ ⌜v = #♭v false⌝}})%I.
(WP rand #() {{ v, ⌜v = #true⌝ ∨ ⌜v = #false⌝}})%I.
Proof.
iStartProof.
unfold rand. unlock.
iApply wp_rec; eauto. iNext. simpl.
wp_bind (Alloc _). iApply wp_alloc; auto. iNext. iIntros (y) "Hy".
iMod (inv_alloc choiceN _ (y ↦ᵢ (#♭v false) ∨ y ↦ᵢ (#♭v true))%I with "[Hy]") as "#Hinv"; eauto.
iMod (inv_alloc choiceN _ (y ↦ᵢ #false ∨ y ↦ᵢ #true)%I with "[Hy]") as "#Hinv"; eauto.
iApply wp_rec; eauto. iNext. simpl.
wp_bind (Fork _). iApply wp_fork. iNext.
iSplitL.
......@@ -39,15 +38,15 @@ Section Refinement.
Lemma rand_l Δ Γ E1 K ρ t τ :
↑choiceN ⊆ E1 →
spec_ctx ρ -∗ (∀ b, {E1,E1;Δ;Γ} ⊨ fill K (#♭ b) ≤log≤ t : τ)
-∗ {E1,E1;Δ;Γ} ⊨ fill K (rand #())%E ≤log≤ t : τ.
spec_ctx ρ -∗ (∀ b : bool, {E1,E1;Δ;Γ} ⊨ fill K #b ≤log≤ t : τ) -∗
{E1,E1;Δ;Γ} ⊨ fill K (rand #()) ≤log≤ t : τ.
Proof.
iIntros (?) "#Hs Hlog".
unfold rand. unlock. simpl.
rel_rec_l.
rel_alloc_l as y "Hy". simpl.
rel_rec_l.
iMod (inv_alloc choiceN _ (∃ b, y ↦ᵢ (#♭v b))%I with "[Hy]") as "#Hinv".
iMod (inv_alloc choiceN _ (∃ b : bool, y ↦ᵢ #b)%I with "[Hy]") as "#Hinv".
{ iNext. eauto. }
rel_fork_l. iModIntro.
iSplitR.
......@@ -61,19 +60,19 @@ Section Refinement.
rel_rec_l.
rel_load_l_atomic.
iInv choiceN as (b) "Hy" "Hcl".
iExists (#♭v b). iFrame.
iExists #b. iFrame.
iModIntro. iNext. iIntros "Hy".
iMod ("Hcl" with "[Hy]").
{ iNext. iExists b. iFrame. }
done.
Qed.
Lemma rand_r b Δ Γ E1 E2 K ρ t τ :
Lemma rand_r (b : bool) Δ Γ E1 E2 K ρ t τ :
↑specN ⊆ E1 →
↑choiceN ⊆ E1 →
spec_ctx ρ -∗
{E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (#♭ b) : τ -∗
{E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (rand #())%E : τ.
{E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K #b : τ -∗
{E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (rand #()) : τ.
Proof.
iIntros (??) "#Hs Hlog".
unfold rand. unlock.
......@@ -90,7 +89,7 @@ Section Refinement.
Lemma lateChoice_l Δ Γ x v ρ t :
spec_ctx ρ -∗ x ↦ᵢ v -∗
(x ↦ᵢ (#nv 0) -∗ ∀ b, {⊤,⊤;Δ;Γ} ⊨ #♭ b ≤log≤ t : TBool) -∗
(x ↦ᵢ #0 -∗ ∀ b : bool, {⊤,⊤;Δ;Γ} ⊨ #b ≤log≤ t : TBool) -∗
{⊤,⊤;Δ;Γ} ⊨ lateChoice #x ≤log≤ t : TBool.
Proof.
iIntros "#Hs Hx Hlog".
......@@ -103,8 +102,8 @@ Section Refinement.
Qed.
Lemma prerefinement Δ Γ x x' n ρ :
(spec_ctx ρ -∗ x ↦ᵢ (#nv n) -∗ x' ↦ₛ (#nv n) -∗
{⊤,⊤;Δ;Γ} ⊨ lateChoice #x ≤log≤ earlyChoice #x' : TBool)%I.
spec_ctx ρ -∗ x ↦ᵢ #n -∗ x' ↦ₛ #n -∗
{⊤,⊤;Δ;Γ} ⊨ lateChoice #x ≤log≤ earlyChoice #x' : TBool.
Proof.
iIntros "#Hspec Hx Hx'".
iApply (lateChoice_l with "Hspec Hx"). iIntros "Hx".
......@@ -120,8 +119,8 @@ Section Refinement.
Qed.
Lemma prerefinement2 Δ Γ x x' n ρ :
(spec_ctx ρ -∗ x ↦ᵢ (#nv n) -∗ x' ↦ₛ (#nv n) -∗
{⊤,⊤;Δ;Γ} ⊨ earlyChoice #x ≤log≤ lateChoice #x' : TBool)%I.
spec_ctx ρ -∗ x ↦ᵢ #n -∗ x' ↦ₛ #n -∗
{⊤,⊤;Δ;Γ} ⊨ earlyChoice #x ≤log≤ lateChoice #x' : TBool.
Proof.
iIntros "#Hspec Hx Hx'".
unfold earlyChoice. unlock.
......
theories/examples/lock.v
View file @ 9dc6e3a8
......@@ -45,8 +45,8 @@ Section proof.
Lemma steps_newlock ρ j K
(Hcl : nclose specN ⊆ E1) :
spec_ctx ρ -∗ j ⤇ fill K (newlock #())%E
={E1}=∗ ∃ l : loc, j ⤇ fill K (of_val (# l)) ∗ l ↦ₛ (#♭v false).
spec_ctx ρ -∗ j ⤇ fill K (newlock #())
={E1}=∗ ∃ l : loc, j ⤇ fill K (of_val #l) ∗ l ↦ₛ #false.
Proof.
iIntros "#Hspec Hj".
unfold newlock. unlock.
......@@ -57,8 +57,8 @@ Section proof.
Lemma bin_log_related_newlock_r Γ K t τ
(Hcl : nclose specN ⊆ E1) :
(∀ l : loc, l ↦ₛ (#♭v false) -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (Lit (Loc l)) :