Commit 8111cab0 authored by Robbert Krebbers's avatar Robbert Krebbers

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).
parent e35004b0
Pipeline #2625 passed with stage
in 8 minutes and 52 seconds
......@@ -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.
......@@ -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 *)
......
......@@ -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".
......
......@@ -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 Φ :
......
......@@ -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.
......
......@@ -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
  • do_head_step fails in the first example because the RHS of the goal does not contain an of_val, unlike the rule for binary operators.

    I could not be bothered to fix this, because I do not think these tests are useful any longer now that heap_lang is widely used throughout the Iris development.

    @jung (since you wrote these tests a long time ago) do you agree and shall we remove these?

    Edited by Robbert
  • These tests served their purpose, we have enough other tests of the reductions now I think. ;)

    This seems to indicate that do_head_step has a fairly narrow use case. Could you document its limitations?

  • Done, see 266e82fe

Please register or sign in to reply
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 Σ}.
......
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