From 8111cab0de08db91247eea7b0ebecbf4eb56ec0d Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Mon, 22 Aug 2016 23:34:51 +0200 Subject: [PATCH] Generalize equality of heap_lang so it works on any value. This is more consistent with CAS, which also can be used on any value. Note that being able to (atomically) test for equality of any value and being able to CAS on any value is not realistic. See the discussion at https://gitlab.mpi-sws.org/FP/iris-coq/issues/26, and in particular JH Jourdan's observation: I think indeed for heap_lang this is just too complicated. Anyway, the role of heap_lang is not to model any actual programming language, but rather to show that we can do proofs about certain programs. The fact that you can write unrealistic programs is not a problem, IMHO. The only thing which is important is that the program that we write are realistic (i.e., faithfully represents the algorithm we want to p This commit is based on a commit by Zhen Zhang who generalized equality to work on any literal (and not just integers). --- heap_lang/derived.v | 11 ++-- heap_lang/lang.v | 104 ++++++++++++++++++------------------ heap_lang/lib/ticket_lock.v | 10 ++-- heap_lang/lifting.v | 22 ++++---- heap_lang/wp_tactics.v | 9 ++-- tests/heap_lang.v | 3 +- 6 files changed, 83 insertions(+), 76 deletions(-) diff --git a/heap_lang/derived.v b/heap_lang/derived.v index 3783733b5..cd65d6692 100644 --- a/heap_lang/derived.v +++ b/heap_lang/derived.v @@ -63,12 +63,13 @@ Proof. destruct (bool_decide_reflect (n1 < n2)); by eauto with omega. Qed. -Lemma wp_eq E (n1 n2 : Z) P Φ : - (n1 = n2 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool true))) → - (n1 ≠n2 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool false))) → - P ⊢ WP BinOp EqOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}. +Lemma wp_eq E e1 e2 v1 v2 P Φ : + to_val e1 = Some v1 → to_val e2 = Some v2 → + (v1 = v2 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool true))) → + (v1 ≠v2 → P ⊢ ▷ |={E}=> Φ (LitV (LitBool false))) → + P ⊢ WP BinOp EqOp e1 e2 @ E {{ Φ }}. Proof. intros. rewrite -wp_bin_op //; []. - destruct (bool_decide_reflect (n1 = n2)); by eauto with omega. + destruct (bool_decide_reflect (v1 = v2)); by eauto. Qed. End derived. diff --git a/heap_lang/lang.v b/heap_lang/lang.v index 9471d5b04..f850174c4 100644 --- a/heap_lang/lang.v +++ b/heap_lang/lang.v @@ -133,6 +133,40 @@ Fixpoint to_val (e : expr) : option val := (** The state: heaps of vals. *) Definition state := gmap loc val. +(** Equality and other typeclass stuff *) +Lemma to_of_val v : to_val (of_val v) = Some v. +Proof. + by induction v; simplify_option_eq; repeat f_equal; try apply (proof_irrel _). +Qed. + +Lemma of_to_val e v : to_val e = Some v → of_val v = e. +Proof. + revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal. +Qed. + +Instance of_val_inj : Inj (=) (=) of_val. +Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed. + +Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2). +Proof. solve_decision. Defined. +Instance un_op_dec_eq (op1 op2 : un_op) : Decision (op1 = op2). +Proof. solve_decision. Defined. +Instance bin_op_dec_eq (op1 op2 : bin_op) : Decision (op1 = op2). +Proof. solve_decision. Defined. +Instance expr_dec_eq (e1 e2 : expr) : Decision (e1 = e2). +Proof. solve_decision. Defined. +Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2). +Proof. + refine (cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver. +Defined. + +Instance expr_inhabited : Inhabited expr := populate (Lit LitUnit). +Instance val_inhabited : Inhabited val := populate (LitV LitUnit). + +Canonical Structure stateC := leibnizC state. +Canonical Structure valC := leibnizC val. +Canonical Structure exprC := leibnizC expr. + (** Evaluation contexts *) Inductive ectx_item := | AppLCtx (e2 : expr) @@ -208,20 +242,20 @@ Definition subst' (mx : binder) (es : expr) : expr → expr := match mx with BNamed x => subst x es | BAnon => id end. (** The stepping relation *) -Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit := - match op, l with - | NegOp, LitBool b => Some (LitBool (negb b)) - | MinusUnOp, LitInt n => Some (LitInt (- n)) +Definition un_op_eval (op : un_op) (v : val) : option val := + match op, v with + | NegOp, LitV (LitBool b) => Some $ LitV $ LitBool (negb b) + | MinusUnOp, LitV (LitInt n) => Some $ LitV $ LitInt (- n) | _, _ => None end. -Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit := - match op, l1, l2 with - | PlusOp, LitInt n1, LitInt n2 => Some $ LitInt (n1 + n2) - | MinusOp, LitInt n1, LitInt n2 => Some $ LitInt (n1 - n2) - | LeOp, LitInt n1, LitInt n2 => Some $ LitBool $ bool_decide (n1 ≤ n2) - | LtOp, LitInt n1, LitInt n2 => Some $ LitBool $ bool_decide (n1 < n2) - | EqOp, LitInt n1, LitInt n2 => Some $ LitBool $ bool_decide (n1 = n2) +Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val := + match op, v1, v2 with + | PlusOp, LitV (LitInt n1), LitV (LitInt n2) => Some $ LitV $ LitInt (n1 + n2) + | MinusOp, LitV (LitInt n1), LitV (LitInt n2) => Some $ LitV $ LitInt (n1 - n2) + | LeOp, LitV (LitInt n1), LitV (LitInt n2) => Some $ LitV $ LitBool $ bool_decide (n1 ≤ n2) + | LtOp, LitV (LitInt n1), LitV (LitInt n2) => Some $ LitV $ LitBool $ bool_decide (n1 < n2) + | EqOp, v1, v2 => Some $ LitV $ LitBool $ bool_decide (v1 = v2) | _, _, _ => None end. @@ -231,12 +265,14 @@ Inductive head_step : expr → state → expr → state → list (expr) → Prop Closed (f :b: x :b: []) e1 → e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1) → head_step (App (Rec f x e1) e2) σ e' σ [] - | UnOpS op l l' σ : - un_op_eval op l = Some l' → - head_step (UnOp op (Lit l)) σ (Lit l') σ [] - | BinOpS op l1 l2 l' σ : - bin_op_eval op l1 l2 = Some l' → - head_step (BinOp op (Lit l1) (Lit l2)) σ (Lit l') σ [] + | UnOpS op e v v' σ : + to_val e = Some v → + un_op_eval op v = Some v' → + head_step (UnOp op e) σ (of_val v') σ [] + | BinOpS op e1 e2 v1 v2 v' σ : + to_val e1 = Some v1 → to_val e2 = Some v2 → + bin_op_eval op v1 v2 = Some v' → + head_step (BinOp op e1 e2) σ (of_val v') σ [] | IfTrueS e1 e2 σ : head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ [] | IfFalseS e1 e2 σ : @@ -274,19 +310,6 @@ Inductive head_step : expr → state → expr → state → list (expr) → Prop head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) []. (** Basic properties about the language *) -Lemma to_of_val v : to_val (of_val v) = Some v. -Proof. - by induction v; simplify_option_eq; repeat f_equal; try apply (proof_irrel _). -Qed. - -Lemma of_to_val e v : to_val e = Some v → of_val v = e. -Proof. - revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal. -Qed. - -Instance of_val_inj : Inj (=) (=) of_val. -Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed. - Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki). Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed. @@ -334,27 +357,6 @@ Proof. intros. apply is_closed_subst with []; set_solver. Qed. Lemma is_closed_of_val X v : is_closed X (of_val v). Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed. - -(** Equality and other typeclass stuff *) -Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2). -Proof. solve_decision. Defined. -Instance un_op_dec_eq (op1 op2 : un_op) : Decision (op1 = op2). -Proof. solve_decision. Defined. -Instance bin_op_dec_eq (op1 op2 : bin_op) : Decision (op1 = op2). -Proof. solve_decision. Defined. -Instance expr_dec_eq (e1 e2 : expr) : Decision (e1 = e2). -Proof. solve_decision. Defined. -Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2). -Proof. - refine (cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver. -Defined. - -Instance expr_inhabited : Inhabited expr := populate (Lit LitUnit). -Instance val_inhabited : Inhabited val := populate (LitV LitUnit). - -Canonical Structure stateC := leibnizC state. -Canonical Structure valC := leibnizC val. -Canonical Structure exprC := leibnizC expr. End heap_lang. (** Language *) diff --git a/heap_lang/lib/ticket_lock.v b/heap_lang/lib/ticket_lock.v index fdcf90bd0..96bef7eaf 100644 --- a/heap_lang/lib/ticket_lock.v +++ b/heap_lang/lib/ticket_lock.v @@ -116,8 +116,8 @@ Proof. set_solver. - iVs ("Hclose" with "[Hlo Hln Ha]"). { iNext. iExists o, n. by iFrame. } - iVsIntro. wp_let. wp_op=>?; first omega. - wp_if. by iApply ("IH" with "Ht"). + iVsIntro. wp_let. wp_op=>[[/Nat2Z.inj //]|?]. + wp_if. iApply ("IH" with "Ht"). by iExact "HΦ". Qed. Lemma acquire_spec l R (Φ : val → iProp Σ) : @@ -131,8 +131,7 @@ Proof. iVsIntro. wp_let. wp_proj. wp_op. wp_bind (CAS _ _ _). iInv N as (o' n') "[Hlo' [Hln' [Hainv Haown]]]" "Hclose". - destruct (decide (#n' = #n))%V - as [[= ->%Nat2Z.inj] | Hneq]. + destruct (decide (#n' = #n))%V as [[= ->%Nat2Z.inj] | Hneq]. - wp_cas_suc. iDestruct "Hainv" as (s) "[Ho %]"; subst. iVs (own_update with "Ho") as "Ho". @@ -166,8 +165,7 @@ Proof. iVsIntro. wp_let. wp_bind (CAS _ _ _ ). wp_proj. wp_op. iInv N as (o' n') "[Hlo' [Hln' Hr]]" "Hclose". - destruct (decide (#o' = #o))%V - as [[= ->%Nat2Z.inj ] | Hneq]. + destruct (decide (#o' = #o))%V as [[= ->%Nat2Z.inj ] | Hneq]. - wp_cas_suc. iDestruct "Hr" as "[Hainv [[Ho _] | Hown]]". + iExFalso. iCombine "Hγ" "Ho" as "Ho". diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v index 44a1dec26..e12abb660 100644 --- a/heap_lang/lifting.v +++ b/heap_lang/lifting.v @@ -92,20 +92,22 @@ Proof. intros; inv_head_step; eauto. Qed. -Lemma wp_un_op E op l l' Φ : - un_op_eval op l = Some l' → - ▷ (|={E}=> Φ (LitV l')) ⊢ WP UnOp op (Lit l) @ E {{ Φ }}. +Lemma wp_un_op E op e v v' Φ : + to_val e = Some v → + un_op_eval op v = Some v' → + ▷ (|={E}=> Φ v') ⊢ WP UnOp op e @ E {{ Φ }}. Proof. - intros. rewrite -(wp_lift_pure_det_head_step (UnOp op _) (Lit l') []) - ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto. + intros. rewrite -(wp_lift_pure_det_head_step (UnOp op _) (of_val v') []) + ?right_id -?wp_value_pvs' //; intros; inv_head_step; eauto. Qed. -Lemma wp_bin_op E op l1 l2 l' Φ : - bin_op_eval op l1 l2 = Some l' → - ▷ (|={E}=> Φ (LitV l')) ⊢ WP BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}. +Lemma wp_bin_op E op e1 e2 v1 v2 v' Φ : + to_val e1 = Some v1 → to_val e2 = Some v2 → + bin_op_eval op v1 v2 = Some v' → + ▷ (|={E}=> Φ v') ⊢ WP BinOp op e1 e2 @ E {{ Φ }}. Proof. - intros Heval. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (Lit l') []) - ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto. + intros. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (of_val v') []) + ?right_id -?wp_value_pvs' //; intros; inv_head_step; eauto. Qed. Lemma wp_if_true E e1 e2 Φ : diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v index 08a4c4c43..c4bed5297 100644 --- a/heap_lang/wp_tactics.v +++ b/heap_lang/wp_tactics.v @@ -88,11 +88,14 @@ Tactic Notation "wp_op" := lazymatch eval hnf in e' with | BinOp LtOp _ _ => wp_bind_core K; apply wp_lt; wp_finish | BinOp LeOp _ _ => wp_bind_core K; apply wp_le; wp_finish - | BinOp EqOp _ _ => wp_bind_core K; apply wp_eq; wp_finish + | BinOp EqOp _ _ => + wp_bind_core K; eapply wp_eq; [wp_done|wp_done|wp_finish|wp_finish] | BinOp _ _ _ => - wp_bind_core K; etrans; [|eapply wp_bin_op; try fast_done]; wp_finish + wp_bind_core K; etrans; + [|eapply wp_bin_op; [wp_done|wp_done|try fast_done]]; wp_finish | UnOp _ _ => - wp_bind_core K; etrans; [|eapply wp_un_op; try fast_done]; wp_finish + wp_bind_core K; etrans; + [|eapply wp_un_op; [wp_done|try fast_done]]; wp_finish end) || fail "wp_op: cannot find 'BinOp' or 'UnOp' in" e | _ => fail "wp_op: not a 'wp'" end. diff --git a/tests/heap_lang.v b/tests/heap_lang.v index fecf44a34..262779c36 100644 --- a/tests/heap_lang.v +++ b/tests/heap_lang.v @@ -5,6 +5,7 @@ From iris.heap_lang Require Import adequacy. From iris.program_logic Require Import ownership. From iris.heap_lang Require Import proofmode notation. +(* FIXME or remove Section LangTests. Definition add : expr := #21 + #21. Goal ∀ σ, head_step add σ (#42) σ []. @@ -15,7 +16,7 @@ Section LangTests. Definition lam : expr := λ: "x", "x" + #21. Goal ∀ σ, head_step (lam #21)%E σ add σ []. Proof. intros. rewrite /lam. do_head_step done. Qed. -End LangTests. +End LangTests. *) Section LiftingTests. Context `{heapG Σ}. -- GitLab