Commit 99126c39 authored by Lennard Gäher's avatar Lennard Gäher
Browse files

hoare

parent 29e3bf97
......@@ -81,6 +81,25 @@ theories/systemf_mu_state/mutbit.v
# Program logic library
theories/axiomatic/program_logic/notation.v
theories/axiomatic/program_logic/sequential_wp.v
theories/axiomatic/program_logic/lifting.v
theories/axiomatic/program_logic/ectx_lifting.v
theories/axiomatic/heap_lang/primitive_laws.v
theories/axiomatic/heap_lang/derived_laws.v
theories/axiomatic/heap_lang/proofmode.v
theories/axiomatic/heap_lang/adequacy.v
theories/axiomatic/heap_lang/primitive_laws_nolater.v
# Program logic chapter
theories/axiomatic/hoare_lib.v
theories/axiomatic/hoare.v
# By removing the # below, you can add the exercise sheets to make
......
From iris.algebra Require Import auth.
From iris.proofmode Require Import proofmode.
From semantics.axiomatic.program_logic Require Export sequential_wp.
From iris.heap_lang Require Import notation.
From semantics.axiomatic.heap_lang Require Export proofmode.
From iris.prelude Require Import options.
Class heapGpreS Σ := HeapGpreS {
heapGpreS_iris :> invGpreS Σ;
heapGpreS_heap :> gen_heapGpreS loc (option val) Σ;
}.
Definition heapΣ : gFunctors :=
#[invΣ; gen_heapΣ loc (option val)].
Global Instance subG_heapGpreS {Σ} : subG heapΣ Σ heapGpreS Σ.
Proof. solve_inG. Qed.
(** This file extends the HeapLang program logic with some derived laws (not
using the lifting lemmas) about arrays and prophecies.
For utility functions on arrays (e.g., freeing/copying an array), see
[heap_lang.lib.array]. *)
From stdpp Require Import fin_maps.
From iris.bi Require Import lib.fractional.
From iris.proofmode Require Import proofmode.
From iris.heap_lang Require Import tactics notation.
From semantics.axiomatic.heap_lang Require Export primitive_laws.
From iris.prelude Require Import options.
(** The [array] connective is a version of [mapsto] that works
with lists of values. *)
Definition array `{!heapGS Σ} (l : loc) (dq : dfrac) (vs : list val) : iProp Σ :=
[ list] i v vs, (l + i) {dq} v.
(** FIXME: Refactor these notations using custom entries once Coq bug #13654
has been fixed. *)
Notation "l ↦∗{ dq } vs" := (array l dq vs)
(at level 20, format "l ↦∗{ dq } vs") : bi_scope.
Notation "l ↦∗□ vs" := (array l DfracDiscarded vs)
(at level 20, format "l ↦∗□ vs") : bi_scope.
Notation "l ↦∗{# q } vs" := (array l (DfracOwn q) vs)
(at level 20, format "l ↦∗{# q } vs") : bi_scope.
Notation "l ↦∗ vs" := (array l (DfracOwn 1) vs)
(at level 20, format "l ↦∗ vs") : bi_scope.
(** We have [FromSep] and [IntoSep] instances to split the fraction (via the
[AsFractional] instance below), but not for splitting the list, as that would
lead to overlapping instances. *)
Section lifting.
Context `{!heapGS Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ.
Implicit Types σ : state.
Implicit Types v : val.
Implicit Types vs : list val.
Implicit Types l : loc.
Implicit Types sz off : nat.
Global Instance array_timeless l q vs : Timeless (array l q vs) := _.
Global Instance array_fractional l vs : Fractional (λ q, l ↦∗{#q} vs)%I := _.
Global Instance array_as_fractional l q vs :
AsFractional (l ↦∗{#q} vs) (λ q, l ↦∗{#q} vs)%I q.
Proof. split; done || apply _. Qed.
Lemma array_nil l dq : l ↦∗{dq} [] emp.
Proof. by rewrite /array. Qed.
Lemma array_singleton l dq v : l ↦∗{dq} [v] l {dq} v.
Proof. by rewrite /array /= right_id loc_add_0. Qed.
Lemma array_app l dq vs ws :
l ↦∗{dq} (vs ++ ws) l ↦∗{dq} vs (l + length vs) ↦∗{dq} ws.
Proof.
rewrite /array big_sepL_app.
setoid_rewrite Nat2Z.inj_add.
by setoid_rewrite loc_add_assoc.
Qed.
Lemma array_cons l dq v vs : l ↦∗{dq} (v :: vs) l {dq} v (l + 1) ↦∗{dq} vs.
Proof.
rewrite /array big_sepL_cons loc_add_0.
setoid_rewrite loc_add_assoc.
setoid_rewrite Nat2Z.inj_succ.
by setoid_rewrite Z.add_1_l.
Qed.
Global Instance array_cons_frame l dq v vs R Q :
Frame false R (l {dq} v (l + 1) ↦∗{dq} vs) Q
Frame false R (l ↦∗{dq} (v :: vs)) Q | 2.
Proof. by rewrite /Frame array_cons. Qed.
Lemma update_array l dq vs off v :
vs !! off = Some v
l ↦∗{dq} vs - ((l + off) {dq} v v', (l + off) {dq} v' - l ↦∗{dq} <[off:=v']>vs).
Proof.
iIntros (Hlookup) "Hl".
rewrite -[X in (l ↦∗{_} X)%I](take_drop_middle _ off v); last done.
iDestruct (array_app with "Hl") as "[Hl1 Hl]".
iDestruct (array_cons with "Hl") as "[Hl2 Hl3]".
assert (off < length vs) as H by (apply lookup_lt_is_Some; by eexists).
rewrite take_length min_l; last by lia. iFrame "Hl2".
iIntros (w) "Hl2".
clear Hlookup. assert (<[off:=w]> vs !! off = Some w) as Hlookup.
{ apply list_lookup_insert. lia. }
rewrite -[in (l ↦∗{_} <[off:=w]> vs)%I](take_drop_middle (<[off:=w]> vs) off w Hlookup).
iApply array_app. rewrite take_insert; last by lia. iFrame.
iApply array_cons. rewrite take_length min_l; last by lia. iFrame.
rewrite drop_insert_gt; last by lia. done.
Qed.
(** * Rules for allocation *)
Lemma mapsto_seq_array l dq v n :
([ list] i seq 0 n, (l + (i : nat)) {dq} v) -
l ↦∗{dq} replicate n v.
Proof.
rewrite /array. iInduction n as [|n'] "IH" forall (l); simpl.
{ done. }
iIntros "[$ Hl]". rewrite -fmap_S_seq big_sepL_fmap.
setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
setoid_rewrite <-loc_add_assoc. iApply "IH". done.
Qed.
Lemma wp_allocN s E v n Φ :
(0 < n)%Z
( l, l ↦∗ replicate (Z.to_nat n) v - Φ (LitV $ LitLoc l)) -
WP AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E; E {{ Φ }}.
Proof.
iIntros (Hzs) "HΦ". iApply wp_allocN_seq; [done..|].
iNext. iIntros (l) "Hlm". iApply "HΦ".
by iApply mapsto_seq_array.
Qed.
Lemma wp_allocN_vec s E v n Φ :
(0 < n)%Z
( l, l ↦∗ vreplicate (Z.to_nat n) v - Φ (#l)) -
WP AllocN #n v @ s ; E; E {{ Φ }}.
Proof.
iIntros (Hzs) "HΦ". iApply wp_allocN; [ lia | .. ].
iNext. iIntros (l) "Hl". iApply "HΦ". rewrite vec_to_list_replicate. iFrame.
Qed.
(** * Rules for accessing array elements *)
Lemma wp_load_offset s E l dq off vs v Φ :
vs !! off = Some v
l ↦∗{dq} vs -
(l ↦∗{dq} vs - Φ v) -
WP ! #(l + off) @ s; E; E {{ Φ }}.
Proof.
iIntros (Hlookup) "Hl HΦ".
iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
iApply (wp_load with "Hl1"). iIntros "!> Hl1". iApply "HΦ".
iDestruct ("Hl2" $! v) as "Hl2". rewrite list_insert_id; last done.
iApply "Hl2". iApply "Hl1".
Qed.
Lemma wp_load_offset_vec s E l dq sz (off : fin sz) (vs : vec val sz) Φ :
l ↦∗{dq} vs -
(l ↦∗{dq} vs - Φ (vs !!! off)) -
WP ! #(l + off) @ s; E; E {{ Φ }}.
Proof. apply wp_load_offset. by apply vlookup_lookup. Qed.
Lemma wp_store_offset s E l off vs v Φ :
is_Some (vs !! off)
l ↦∗ vs -
(l ↦∗ <[off:=v]> vs - Φ #()) -
WP #(l + off) <- v @ s; E; E {{ Φ }}.
Proof.
iIntros ([w Hlookup]) "Hl HΦ".
iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
iApply (wp_store with "Hl1"). iIntros "!> Hl1".
iApply "HΦ". iApply "Hl2". iApply "Hl1".
Qed.
Lemma wp_store_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v Φ :
l ↦∗ vs -
(l ↦∗ vinsert off v vs - Φ #()) -
WP #(l + off) <- v @ s; E; E {{ Φ }}.
Proof.
setoid_rewrite vec_to_list_insert. apply wp_store_offset.
eexists. by apply vlookup_lookup.
Qed.
End lifting.
Typeclasses Opaque array.
(** This file proves the basic laws of the HeapLang program logic by applying
the Iris lifting lemmas. *)
From iris.proofmode Require Import proofmode.
From iris.bi.lib Require Import fractional.
From iris.base_logic.lib Require Export gen_heap gen_inv_heap.
From semantics.axiomatic.program_logic Require Export sequential_wp.
From semantics.axiomatic.program_logic Require Import ectx_lifting.
From iris.heap_lang Require Export class_instances.
From iris.heap_lang Require Import tactics notation.
From iris.prelude Require Import options.
Class heapGS Σ := HeapGS {
heapGS_invGS : invGS Σ;
heapGS_gen_heapGS :> gen_heapGS loc (option val) Σ;
}.
Global Instance heapGS_irisGS `{!heapGS Σ} : irisGS heap_lang Σ := {
iris_invGS := heapGS_invGS;
state_interp σ := (gen_heap_interp σ.(heap))%I;
}.
(** Since we use an [option val] instance of [gen_heap], we need to overwrite
the notations. That also helps for scopes and coercions. *)
(** FIXME: Refactor these notations using custom entries once Coq bug #13654
has been fixed. *)
Notation "l ↦{ dq } v" := (mapsto (L:=loc) (V:=option val) l dq (Some v%V))
(at level 20, format "l ↦{ dq } v") : bi_scope.
Notation "l ↦□ v" := (mapsto (L:=loc) (V:=option val) l DfracDiscarded (Some v%V))
(at level 20, format "l ↦□ v") : bi_scope.
Notation "l ↦{# q } v" := (mapsto (L:=loc) (V:=option val) l (DfracOwn q) (Some v%V))
(at level 20, format "l ↦{# q } v") : bi_scope.
Notation "l ↦ v" := (mapsto (L:=loc) (V:=option val) l (DfracOwn 1) (Some v%V))
(at level 20, format "l ↦ v") : bi_scope.
Section lifting.
Context `{!heapGS Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ Ψ : val iProp Σ.
Implicit Types efs : list expr.
Implicit Types σ : state.
Implicit Types v : val.
Implicit Types l : loc.
(** Recursive functions: we do not use this lemmas as it is easier to use Löb
induction directly, but this demonstrates that we can state the expected
reasoning principle for recursive functions, without any visible ▷. *)
Lemma wp_rec_löb s E1 E2 f x e Φ Ψ :
( ( v, Ψ v - WP (rec: f x := e)%V v @ s; E1; E2 {{ Φ }}) -
v, Ψ v - WP (subst' x v (subst' f (rec: f x := e) e)) @ s; E1; E2 {{ Φ }}) -
v, Ψ v - WP (rec: f x := e)%V v @ s; E1; E2 {{ Φ }}.
Proof.
iIntros "#Hrec". iLöb as "IH". iIntros (v) "HΨ".
iApply lifting.wp_pure_step_later; first done.
iNext. iApply ("Hrec" with "[] HΨ"). iIntros "!>" (w) "HΨ".
iApply ("IH" with "HΨ").
Qed.
(** Heap *)
(** We need to adjust the [gen_heap] and [gen_inv_heap] lemmas because of our
value type being [option val]. *)
Lemma mapsto_valid l dq v : l {dq} v - ⌜✓ dq.
Proof. apply mapsto_valid. Qed.
Lemma mapsto_valid_2 l dq1 dq2 v1 v2 :
l {dq1} v1 - l {dq2} v2 - ⌜✓ (dq1 dq2) v1 = v2.
Proof.
iIntros "H1 H2". iDestruct (mapsto_valid_2 with "H1 H2") as %[? [=?]]. done.
Qed.
Lemma mapsto_agree l dq1 dq2 v1 v2 : l {dq1} v1 - l {dq2} v2 - v1 = v2.
Proof. iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %[=?]. done. Qed.
Lemma mapsto_combine l dq1 dq2 v1 v2 :
l {dq1} v1 - l {dq2} v2 - l {dq1 dq2} v1 v1 = v2.
Proof.
iIntros "Hl1 Hl2". iDestruct (mapsto_combine with "Hl1 Hl2") as "[$ Heq]".
by iDestruct "Heq" as %[= ->].
Qed.
Lemma mapsto_frac_ne l1 l2 dq1 dq2 v1 v2 :
¬ (dq1 dq2) l1 {dq1} v1 - l2 {dq2} v2 - l1 l2.
Proof. apply mapsto_frac_ne. Qed.
Lemma mapsto_ne l1 l2 dq2 v1 v2 : l1 v1 - l2 {dq2} v2 - l1 l2.
Proof. apply mapsto_ne. Qed.
Lemma mapsto_persist l dq v : l {dq} v == l ↦□ v.
Proof. apply mapsto_persist. Qed.
Lemma heap_array_to_seq_mapsto l v (n : nat) :
([ map] l' ov heap_array l (replicate n v), gen_heap.mapsto l' (DfracOwn 1) ov) -
[ list] i seq 0 n, (l + (i : nat)) v.
Proof.
iIntros "Hvs". iInduction n as [|n] "IH" forall (l); simpl.
{ done. }
rewrite big_opM_union; last first.
{ apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
intros (j&w&?&Hjl&_)%heap_array_lookup.
rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl. simplify_eq; lia. }
rewrite loc_add_0 -fmap_S_seq big_sepL_fmap.
setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
setoid_rewrite <-loc_add_assoc.
rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]". by iApply "IH".
Qed.
Lemma wp_allocN_seq s E v n Φ :
(0 < n)%Z
( l, ([ list] i seq 0 (Z.to_nat n), (l + (i : nat)) v) - Φ (LitV $ LitLoc l)) -
WP AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E; E {{ Φ }}.
Proof.
iIntros (Hn) "HΦ".
iApply wp_lift_head_step_fupd_nomask; first done.
iIntros (σ1) "Hσ !>"; iSplit; first by destruct n; auto with lia head_step.
iIntros (e2 σ2 κ efs Hstep); inv_head_step.
iMod (gen_heap_alloc_big _ (heap_array _ (replicate (Z.to_nat n) v)) with "Hσ")
as "(Hσ & Hl & Hm)".
{ apply heap_array_map_disjoint.
rewrite replicate_length Z2Nat.id; auto with lia. }
iApply step_fupd_intro; first done.
iModIntro. iFrame "Hσ". do 2 (iSplit; first done).
iApply wp_value_fupd. iApply "HΦ".
by iApply heap_array_to_seq_mapsto.
Qed.
Lemma wp_alloc s E v Φ :
( l, l v - Φ (LitV $ LitLoc l)) -
WP Alloc (Val v) @ s; E; E {{ Φ }}.
Proof.
iIntros "HΦ". iApply wp_allocN_seq; [auto with lia..|].
iIntros "!>" (l) "/= (? & _)". rewrite loc_add_0. iApply "HΦ"; iFrame.
Qed.
Lemma wp_free s E l v Φ :
l v -
( Φ (LitV LitUnit)) -
WP Free (Val $ LitV $ LitLoc l) @ s; E; E {{ Φ }}.
Proof.
iIntros ">Hl HΦ". iApply wp_lift_head_step_fupd_nomask; first done.
iIntros (σ1) "Hσ !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto with head_step.
iIntros (e2 σ2 κ efs Hstep); inv_head_step.
iMod (gen_heap_update with "Hσ Hl") as "[$ Hl]".
iIntros "!>!>!>". iSplit; first done. iSplit; first done.
iApply wp_value. by iApply "HΦ".
Qed.
Lemma wp_load s E l dq v Φ :
l {dq} v -
(l {dq} v - Φ v) -
WP Load (Val $ LitV $ LitLoc l) @ s; E; E {{ Φ }}.
Proof.
iIntros ">Hl HΦ". iApply wp_lift_head_step_fupd_nomask; first done.
iIntros (σ1) "Hσ !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto with head_step.
iIntros (e2 σ2 κ efs Hstep); inv_head_step.
iApply step_fupd_intro; first done. iNext. iFrame.
iSplitR; first done. iSplitR; first done. iApply wp_value. by iApply "HΦ".
Qed.
Lemma wp_store s E l v' v Φ :
l v' -
(l v - Φ (LitV LitUnit)) -
WP Store (Val $ LitV $ LitLoc l) (Val v) @ s; E; E {{ Φ }}.
Proof.
iIntros ">Hl HΦ". iApply wp_lift_head_step_fupd_nomask; first done.
iIntros (σ1) "Hσ !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto with head_step.
iIntros (e2 σ2 κ efs Hstep); inv_head_step.
iMod (gen_heap_update with "Hσ Hl") as "[$ Hl]".
iApply step_fupd_intro; first done. iNext.
iSplit; first done. iSplit; first done.
iApply wp_value. by iApply "HΦ".
Qed.
End lifting.
From stdpp Require Import fin_maps.
From iris.proofmode Require Import proofmode.
From iris.bi.lib Require Import fractional.
From semantics.axiomatic.heap_lang Require Export primitive_laws derived_laws.
From iris.base_logic.lib Require Export gen_heap gen_inv_heap.
From semantics.axiomatic.program_logic Require Export sequential_wp.
From semantics.axiomatic.program_logic Require Import ectx_lifting.
From iris.heap_lang Require Export class_instances.
From iris.heap_lang Require Import tactics notation.
From iris.prelude Require Import options.
Section lifting.
Context `{!heapGS Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ Ψ : val iProp Σ.
Implicit Types efs : list expr.
Implicit Types σ : state.
Implicit Types v : val.
Implicit Types l : loc.
(** Heap *)
Lemma wp_allocN_seq s E v n Φ :
(0 < n)%Z
( l, ([ list] i seq 0 (Z.to_nat n), (l + (i : nat)) v) - Φ (LitV $ LitLoc l)) -
WP AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E; E {{ Φ }}.
Proof.
iIntros (Hn) "HΦ". iApply wp_allocN_seq; done.
Qed.
Lemma wp_alloc s E v Φ :
( l, l v - Φ (LitV $ LitLoc l)) -
WP Alloc (Val v) @ s; E; E {{ Φ }}.
Proof.
iIntros "HΦ". by iApply wp_alloc.
Qed.
Lemma wp_free s E l v Φ :
l v -
(Φ (LitV LitUnit)) -
WP Free (Val $ LitV $ LitLoc l) @ s; E; E {{ Φ }}.
Proof.
iIntros "Hl HΦ". iApply (wp_free with "Hl HΦ").
Qed.
Lemma wp_load s E l dq v Φ :
l {dq} v -
(l {dq} v - Φ v) -
WP Load (Val $ LitV $ LitLoc l) @ s; E; E {{ Φ }}.
Proof.
iIntros "Hl HΦ". iApply (wp_load with "Hl HΦ").
Qed.
Lemma wp_store s E l v' v Φ :
l v' -
(l v - Φ (LitV LitUnit)) -
WP Store (Val $ LitV $ LitLoc l) (Val v) @ s; E; E {{ Φ }}.
Proof.
iIntros "Hl HΦ".
iApply (wp_store with "Hl HΦ").
Qed.
(*** Derived *)
Lemma wp_allocN s E v n Φ :
(0 < n)%Z
( l, l ↦∗ replicate (Z.to_nat n) v - Φ (LitV $ LitLoc l)) -
WP AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E; E {{ Φ }}.
Proof.
iIntros. by iApply wp_allocN.
Qed.
Lemma wp_allocN_vec s E v n Φ :
(0 < n)%Z
( l, l ↦∗ vreplicate (Z.to_nat n) v - Φ (#l)) -
WP AllocN #n v @ s ; E; E {{ Φ }}.
Proof.
iIntros. by iApply wp_allocN_vec.
Qed.
(** * Rules for accessing array elements *)
Lemma wp_load_offset s E l dq (off : nat) vs v Φ :
vs !! off = Some v
l ↦∗{dq} vs -
(l ↦∗{dq} vs - Φ v) -
WP ! #(l + off) @ s; E; E {{ Φ }}.
Proof.
iIntros (?) "Hl HΦ". by iApply (wp_load_offset with "Hl HΦ").
Qed.
Lemma wp_load_offset_vec s E l dq sz (off : fin sz) (vs : vec val sz) Φ :
l ↦∗{dq} vs -
(l ↦∗{dq} vs - Φ (vs !!! off)) -
WP ! #(l + off) @ s; E; E {{ Φ }}.
Proof. apply wp_load_offset. by apply vlookup_lookup. Qed.
Lemma wp_store_offset s E l (off : nat) vs v Φ :
is_Some (vs !! off)
l ↦∗ vs -
(l ↦∗ <[off:=v]> vs - Φ #()) -
WP #(l + off) <- v @ s; E; E {{ Φ }}.
Proof.
iIntros (?) "Hl HΦ". by iApply (wp_store_offset with "Hl HΦ").
Qed.
Lemma wp_store_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v Φ :
l ↦∗ vs -
(l ↦∗ vinsert off v vs - Φ #()) -
WP #(l + off) <- v @ s; E; E {{ Φ }}.
Proof.
iIntros "Hl HΦ". by iApply (wp_store_offset_vec with "Hl HΦ").
Qed.
End lifting.
<
From iris.proofmode Require Import coq_tactics reduction spec_patterns.
From iris.proofmode Require Export tactics.
From iris.heap_lang Require Export tactics.
From iris.heap_lang Require Import notation.
From semantics.axiomatic.heap_lang Require Export derived_laws.
From semantics.axiomatic.program_logic Require Export notation.
From iris.prelude Require Import options.
Import uPred.
Lemma tac_wp_expr_eval `{!heapGS Σ} Δ s E1 E2 Φ e e' :
( (e'':=e'), e = e'')
envs_entails Δ (WP e' @ s; E1; E2 {{ Φ }}) envs_entails Δ (WP e @ s; E1; E2 {{ Φ }}).
Proof. by intros ->. Qed.
Tactic Notation "wp_expr_eval" tactic3(t) :=
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp ?s ?E1 ?E2 ?e ?Q) =>
notypeclasses refine (tac_wp_expr_eval _ _ _ _ _ e _ _ _);
[let x := fresh in intros x; t; unfold x; notypeclasses refine eq_refl|]
| _ => fail "wp_expr_eval: not a 'wp'"