comparison: treat prophecies like unit

tests/heap_lang_proph.v

@@ -25,7 +25,7 @@ Section tests.
   Qed.
 
   Lemma wp_cas_fail_resolve s E (l : loc) (p : proph_id) (vs : list (val * val)) (v' v1 v2 v : val) :
-    v' ≠ v1 → vals_cas_compare_safe v' v1 →
+    val_for_compare v' ≠ val_for_compare v1 → vals_cas_compare_safe v' v1 →
     {{{ proph p vs ∗ ▷ l ↦ v' }}}
       CAS_resolve #l v1 v2 #p v @ s; E
     {{{ RET #false ; ∃ vs', ⌜vs = (#false, v)::vs'⌝ ∗ proph p vs' ∗ l ↦ v' }}}.

theories/heap_lang/lang.v

@@ -159,6 +159,31 @@ Definition val_is_unboxed (v : val) : Prop :=
   | _ => False
   end.
 
+(** CAS just compares the word-sized representation of two values, it cannot
+look into boxed data.  This works out fine if at least one of the to-be-compared
+values is unboxed (exploiting the fact that an unboxed and a boxed value can
+never be equal because these are disjoint sets). *)
+Definition vals_cas_compare_safe (vl v1 : val) : Prop :=
+  val_is_unboxed vl ∨ val_is_unboxed v1.
+Arguments vals_cas_compare_safe !_ !_ /.
+
+(** We don't compare the logical program values, but we first normalize them
+to make sure that prophecies are treated like unit.
+Also all functions become the same, but still distinct from anything else. *)
+Definition lit_for_compare (l : base_lit) : base_lit :=
+  match l with
+  | LitProphecy p => LitUnit
+  | l => l
+  end.
+Fixpoint val_for_compare (v : val) : val :=
+  match v with
+  | LitV l => LitV (lit_for_compare l)
+  | PairV v1 v2 => PairV (val_for_compare v1) (val_for_compare v2)
+  | InjLV v => InjLV (val_for_compare v)
+  | InjRV v => InjRV (val_for_compare v)
+  | RecV f x e => RecV BAnon BAnon (Val $ LitV $ LitUnit)
+  end.
+
 (** The state: heaps of vals. *)
 Record state : Type := {
   heap: gmap loc val;
@@ -492,21 +517,15 @@ Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
   end.
 
 Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
-  if decide (op = EqOp) then Some $ LitV $ LitBool $ bool_decide (v1 = v2) else
-  match v1, v2 with
-  | LitV (LitInt n1), LitV (LitInt n2) => LitV <$> bin_op_eval_int op n1 n2
-  | LitV (LitBool b1), LitV (LitBool b2) => LitV <$> bin_op_eval_bool op b1 b2
-  | LitV (LitLoc l), LitV (LitInt off) => Some $ LitV $ LitLoc (l +ₗ off)
-  | _, _ => None
-  end.
-
-(** CAS just compares the word-sized representation of the two values, it cannot
-look into boxed data.  This works out fine if at least one of the to-be-compared
-values is unboxed (exploiting the fact that an unboxed and a boxed value can
-never be equal because these are disjoint sets).  *)
-Definition vals_cas_compare_safe (vl v1 : val) : Prop :=
-  val_is_unboxed vl ∨ val_is_unboxed v1.
-Arguments vals_cas_compare_safe !_ !_ /.
+  if decide (op = EqOp) then
+    Some $ LitV $ LitBool $ bool_decide (val_for_compare v1 = val_for_compare v2)
+  else
+    match v1, v2 with
+    | LitV (LitInt n1), LitV (LitInt n2) => LitV <$> bin_op_eval_int op n1 n2
+    | LitV (LitBool b1), LitV (LitBool b2) => LitV <$> bin_op_eval_bool op b1 b2
+    | LitV (LitLoc l), LitV (LitInt off) => Some $ LitV $ LitLoc (l +ₗ off)
+    | _, _ => None
+    end.
 
 Definition state_upd_heap (f: gmap loc val → gmap loc val) (σ: state) : state :=
   {| heap := f σ.(heap); used_proph_id := σ.(used_proph_id) |}.
@@ -615,13 +634,15 @@ Inductive head_step : expr → state → list observation → expr → state →
                (Val $ LitV LitUnit) (state_upd_heap <[l:=v]> σ)
                []
   | CasFailS l v1 v2 vl σ :
-     σ.(heap) !! l = Some vl → vl ≠ v1 →
      vals_cas_compare_safe vl v1 →
+     σ.(heap) !! l = Some vl →
+     val_for_compare vl ≠ val_for_compare v1 →
      head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ []
                (Val $ LitV $ LitBool false) σ []
-  | CasSucS l v1 v2 σ :
-     σ.(heap) !! l = Some v1 →
-     vals_cas_compare_safe v1 v1 →
+  | CasSucS l v1 v2 vl σ :
+     vals_cas_compare_safe vl v1 →
+     σ.(heap) !! l = Some vl →
+     val_for_compare vl = val_for_compare v1 →
      head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
                []
                (Val $ LitV $ LitBool true) (state_upd_heap <[l:=v2]> σ)

theories/heap_lang/lib/atomic_heap.v

@@ -35,8 +35,8 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
   cas_spec (l : loc) (w1 w2 : val) :
     val_is_unboxed w1 →
     <<< ∀ v, mapsto l 1 v >>> cas #l w1 w2 @ ⊤
-    <<< if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v,
-        RET #(if decide (v = w1) then true else false) >>>;
+    <<< if decide (val_for_compare v = val_for_compare w1) then mapsto l 1 w2 else mapsto l 1 v,
+        RET #(if decide (val_for_compare v = val_for_compare w1) then true else false) >>>;
 }.
 Arguments atomic_heap _ {_}.
 
@@ -99,12 +99,13 @@ Section proof.
     val_is_unboxed w1 →
     <<< ∀ (v : val), l ↦ v >>>
       primitive_cas #l w1 w2 @ ⊤
-    <<< if decide (v = w1) then l ↦ w2 else l ↦ v,
-        RET #(if decide (v = w1) then true else false) >>>.
+    <<< if decide (val_for_compare v = val_for_compare w1) then l ↦ w2 else l ↦ v,
+        RET #(if decide (val_for_compare v = val_for_compare w1) then true else false) >>>.
   Proof.
     iIntros (? Φ) "AU". wp_lam. wp_let. wp_let.
     iMod "AU" as (v) "[H↦ [_ Hclose]]".
-    destruct (decide (v = w1)) as [<-|Hv]; [wp_cas_suc|wp_cas_fail];
+    destruct (decide (val_for_compare v = val_for_compare w1)) as [Heq|Hne];
+      [wp_cas_suc|wp_cas_fail];
     iMod ("Hclose" with "H↦") as "HΦ"; done.
   Qed.
 End proof.

theories/heap_lang/lib/increment.v

@@ -68,7 +68,7 @@ Section increment.
     rewrite /atomic_acc /=. iMod "AU" as (w) "[Hl Hclose]".
     iModIntro. iExists _. iFrame "Hl". iSplit.
     { (* abort case *) iDestruct "Hclose" as "[? _]". done. }
-    iIntros "Hl". destruct (decide (#w = #v)) as [[= ->]|Hx].
+    iIntros "Hl". simpl. destruct (decide (#w = #v)) as [[= ->]|Hx].
     - iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ".
       iIntros "!>". wp_if. by iApply "HΦ".
     - iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU".
@@ -92,7 +92,7 @@ Section increment.
     iApply (aacc_aupd with "AU"); first done.
     iIntros (x') "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
     iIntros "H↦ !>".
-    destruct (decide (#x' = #x)) as [[= ->]|Hx].
+    simpl. destruct (decide (#x' = #x)) as [[= ->]|Hx].
     - iRight. iFrame. iIntros "HΦ !>".
       wp_if. by iApply "HΦ".
     - iLeft. iFrame. iIntros "AU !>".

theories/heap_lang/lifting.v

@@ -353,7 +353,7 @@ Proof.
 Qed.
 
 Lemma wp_cas_fail s E l q v' v1 v2 :
-  v' ≠ v1 → vals_cas_compare_safe v' v1 →
+  val_for_compare v' ≠ val_for_compare v1 → vals_cas_compare_safe v' v1 →
   {{{ ▷ l ↦{q} v' }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
   {{{ RET LitV (LitBool false); l ↦{q} v' }}}.
 Proof.
@@ -363,7 +363,7 @@ Proof.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 Lemma twp_cas_fail s E l q v' v1 v2 :
-  v' ≠ v1 → vals_cas_compare_safe v' v1 →
+  val_for_compare v' ≠ val_for_compare v1 → vals_cas_compare_safe v' v1 →
   [[{ l ↦{q} v' }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
   [[{ RET LitV (LitBool false); l ↦{q} v' }]].
 Proof.
@@ -373,23 +373,23 @@ Proof.
   iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
 
-Lemma wp_cas_suc s E l v1 v2 :
-  vals_cas_compare_safe v1 v1 →
-  {{{ ▷ l ↦ v1 }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
+Lemma wp_cas_suc s E l v1 v2 v' :
+  val_for_compare v' = val_for_compare v1 → vals_cas_compare_safe v' v1 →
+  {{{ ▷ l ↦ v' }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
   {{{ RET LitV (LitBool true); l ↦ v2 }}}.
 Proof.
-  iIntros (? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
 Qed.
-Lemma twp_cas_suc s E l v1 v2 :
-  vals_cas_compare_safe v1 v1 →
-  [[{ l ↦ v1 }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
+Lemma twp_cas_suc s E l v1 v2 v' :
+  val_for_compare v' = val_for_compare v1 → vals_cas_compare_safe v' v1 →
+  [[{ l ↦ v' }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
   [[{ RET LitV (LitBool true); l ↦ v2 }]].
 Proof.
-  iIntros (? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
+  iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".

theories/heap_lang/proofmode.v

@@ -283,12 +283,16 @@ Lemma tac_wp_cas Δ Δ' Δ'' s E i K l v v1 v2 Φ :
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
   vals_cas_compare_safe v v1 →
-  (v = v1 → envs_entails Δ'' (WP fill K (Val $ LitV true) @ s; E {{ Φ }})) →
-  (v ≠ v1 → envs_entails Δ' (WP fill K (Val $ LitV false) @ s; E {{ Φ }})) →
+  (val_for_compare v = val_for_compare v1 →
+   envs_entails Δ'' (WP fill K (Val $ LitV true) @ s; E {{ Φ }})) →
+  (val_for_compare v ≠ val_for_compare v1 →
+   envs_entails Δ' (WP fill K (Val $ LitV false) @ s; E {{ Φ }})) →
   envs_entails Δ (WP fill K (CAS (LitV l) (Val v1) (Val v2)) @ s; E {{ Φ }}).
 Proof.
-  rewrite envs_entails_eq=> ???? Hsuc Hfail. destruct (decide (v = v1)) as [<-|Hne].
-  - rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
+  rewrite envs_entails_eq=> ???? Hsuc Hfail.
+  destruct (decide (val_for_compare v = val_for_compare v1)) as [Heq|Hne].
+  - rewrite -wp_bind. eapply wand_apply.
+    { eapply wp_cas_suc; eauto. }
     rewrite into_laterN_env_sound -later_sep /= {1}envs_simple_replace_sound //; simpl.
     apply later_mono, sep_mono_r. rewrite right_id. apply wand_mono; auto.
   - rewrite -wp_bind. eapply wand_apply.
@@ -300,12 +304,16 @@ Lemma tac_twp_cas Δ Δ' s E i K l v v1 v2 Φ :
   envs_lookup i Δ = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ = Some Δ' →
   vals_cas_compare_safe v v1 →
-  (v = v1 → envs_entails Δ' (WP fill K (Val $ LitV true) @ s; E [{ Φ }])) →
-  (v ≠ v1 → envs_entails Δ (WP fill K (Val $ LitV false) @ s; E [{ Φ }])) →
+  (val_for_compare v = val_for_compare v1 →
+   envs_entails Δ' (WP fill K (Val $ LitV true) @ s; E [{ Φ }])) →
+  (val_for_compare v ≠ val_for_compare v1 →
+   envs_entails Δ (WP fill K (Val $ LitV false) @ s; E [{ Φ }])) →
   envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
 Proof.
-  rewrite envs_entails_eq=> ??? Hsuc Hfail. destruct (decide (v = v1)) as [<-|Hne].
-  - rewrite -twp_bind. eapply wand_apply; first exact: twp_cas_suc.
+  rewrite envs_entails_eq=> ??? Hsuc Hfail.
+  destruct (decide (val_for_compare v = val_for_compare v1)) as [Heq|Hne].
+  - rewrite -twp_bind. eapply wand_apply.
+    { eapply twp_cas_suc; eauto. }
     rewrite /= {1}envs_simple_replace_sound //; simpl.
     apply sep_mono_r. rewrite right_id. apply wand_mono; auto.
   - rewrite -twp_bind. eapply wand_apply.
@@ -317,7 +325,7 @@ Qed.
 Lemma tac_wp_cas_fail Δ Δ' s E i K l q v v1 v2 Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
-  v ≠ v1 → vals_cas_compare_safe v v1 →
+  val_for_compare v ≠ val_for_compare v1 → vals_cas_compare_safe v v1 →
   envs_entails Δ' (WP fill K (Val $ LitV false) @ s; E {{ Φ }}) →
   envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E {{ Φ }}).
 Proof.
@@ -328,7 +336,7 @@ Proof.
 Qed.
 Lemma tac_twp_cas_fail Δ s E i K l q v v1 v2 Φ :
   envs_lookup i Δ = Some (false, l ↦{q} v)%I →
-  v ≠ v1 → vals_cas_compare_safe v v1 →
+  val_for_compare v ≠ val_for_compare v1 → vals_cas_compare_safe v v1 →
   envs_entails Δ (WP fill K (Val $ LitV false) @ s; E [{ Φ }]) →
   envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
 Proof.
@@ -341,26 +349,26 @@ Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v v1 v2 Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
-  v = v1 → val_is_unboxed v →
+  val_for_compare v = val_for_compare v1 → vals_cas_compare_safe v v1 →
   envs_entails Δ'' (WP fill K (Val $ LitV true) @ s; E {{ Φ }}) →
   envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E {{ Φ }}).
 Proof.
   rewrite envs_entails_eq=> ??????; subst.
   rewrite -wp_bind. eapply wand_apply.
-  { eapply wp_cas_suc; eauto. by left. }
+  { eapply wp_cas_suc; eauto. }
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 Lemma tac_twp_cas_suc Δ Δ' s E i K l v v1 v2 Φ :
   envs_lookup i Δ = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ = Some Δ' →
-  v = v1 → val_is_unboxed v →
+  val_for_compare v = val_for_compare v1 → vals_cas_compare_safe v v1 →
   envs_entails Δ' (WP fill K (Val $ LitV true) @ s; E [{ Φ }]) →
   envs_entails Δ (WP fill K (CAS (LitV l) v1 v2) @ s; E [{ Φ }]).
 Proof.
   rewrite envs_entails_eq=>?????; subst.
   rewrite -twp_bind. eapply wand_apply.
-  { eapply twp_cas_suc; eauto. by left. }
+  { eapply twp_cas_suc; eauto. }
   rewrite envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply sep_mono_r, wand_mono.
 Qed.
@@ -562,7 +570,7 @@ Tactic Notation "wp_cas_fail" :=
       |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
     [iSolveTC
     |solve_mapsto ()
-    |try congruence
+    |try (simpl; congruence) (* value inequality *)
     |try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
     |wp_finish]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
@@ -570,7 +578,7 @@ Tactic Notation "wp_cas_fail" :=
       [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas_fail _ _ _ _ K))
       |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
     [solve_mapsto ()
-    |try congruence
+    |try (simpl; congruence) (* value inequality *)
     |try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
     |wp_finish]
   | _ => fail "wp_cas_fail: not a 'wp'"
@@ -589,8 +597,8 @@ Tactic Notation "wp_cas_suc" :=
     [iSolveTC
     |solve_mapsto ()
     |pm_reflexivity
-    |try congruence
-    |try fast_done (* vals_cas_compare_safe *)
+    |try (simpl; congruence) (* value equality *)
+    |try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
     |wp_finish]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
@@ -598,8 +606,8 @@ Tactic Notation "wp_cas_suc" :=
       |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
     [solve_mapsto ()
     |pm_reflexivity
-    |try congruence
-    |try fast_done (* vals_cas_compare_safe *)
+    |try (simpl; congruence) (* value equality *)
+    |try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
     |wp_finish]
   | _ => fail "wp_cas_suc: not a 'wp'"
   end.