Relax the `load` rules

Allow to read the location if you have a fractional (non 1)
permission.

theories/F_mu_ref_conc/rules.v

 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import ectx_lifting.
-From iris.base_logic Require Export invariants big_op.
+From iris.base_logic Require Export invariants big_op fractional.
 From iris.algebra Require Import auth frac agree gmap.
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Export gen_heap.
@@ -24,6 +24,30 @@ Notation "l ↦ᵢ{ q } v" := (mapsto (L:=loc) (V:=val) l q v)
   (at level 20, q at level 50, format "l  ↦ᵢ{ q }  v") : uPred_scope.
 Notation "l ↦ᵢ v" := (mapsto (L:=loc) (V:=val) l 1 v) (at level 20) : uPred_scope.
 
+Section mapsto.
+  Context `{heapG Σ}.
+
+  Global Instance mapsto_timeless l q v : TimelessP (l ↦ᵢ{q} v).
+  Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed.
+  Global Instance mapsto_fractional l v : Fractional (λ q, l ↦ᵢ{q} v)%I.
+  Proof.
+    intros p q. by rewrite mapsto_eq -own_op -auth_frag_op
+      op_singleton pair_op agree_idemp.
+  Qed.
+  Global Instance mapsto_as_fractional l q v :
+    AsFractional (l ↦ᵢ{q} v) (λ q, l ↦ᵢ{q} v)%I q.
+  Proof. split. done. apply _. Qed.
+
+  Lemma mapsto_agree l q1 q2 v1 v2 : l ↦ᵢ{q1} v1 -∗ l ↦ᵢ{q2} v2 -∗ ⌜v1 = v2⌝.
+  Proof.
+    apply wand_intro_r.
+    rewrite mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
+    f_equiv=> /auth_own_valid /=. rewrite op_singleton singleton_valid pair_op.
+    by intros [_ ?%agree_op_invL'].
+  Qed.
+
+End mapsto.
+
 Section lang_rules.
   Context `{heapG Σ}.
   Implicit Types P Q : iProp Σ.

theories/logrel/proofmode/tactics_rel.v

@@ -319,10 +319,10 @@ Tactic Notation "rel_alloc_r" :=
 (* Load *)
 Tactic Notation "rel_load_l_atomic" := rel_apply_l bin_log_related_load_l.
 
-Lemma tac_rel_load_l_simp `{logrelG Σ} ℶ1 ℶ2 i1 E1 Δ Γ (l : loc) v K e t eres τ :
+Lemma tac_rel_load_l_simp `{logrelG Σ} ℶ1 ℶ2 i1 E1 Δ Γ (l : loc) q v K e t eres τ :
   e = fill K (Load (# l)) →
   IntoLaterNEnvs 1 ℶ1 ℶ2 →
-  envs_lookup i1 ℶ2 = Some (false, l ↦ᵢ v)%I →
+  envs_lookup i1 ℶ2 = Some (false, l ↦ᵢ{q} v)%I →
   eres = fill K (of_val v) →
   (ℶ2 ⊢ bin_log_related E1 E1 Δ Γ eres t τ) →
   (ℶ1 ⊢ bin_log_related E1 E1 Δ Γ e t τ).
@@ -341,16 +341,16 @@ Tactic Notation "rel_load_l" :=
   eapply (tac_rel_load_l_simp);
     [tac_bind_helper (* e = fill K' .. *)
     |apply _  (* IntoLaterNenvs _ Δ1 Δ2 *)
-    |iAssumptionCore || fail 3 "rel_load_l: cannot find ? ↦ᵢ ?"
+    |iAssumptionCore || fail 3 "rel_load_l: cannot find ? ↦ᵢ{?} ?"
     |simpl; reflexivity  (* eres = fill K (of_val v) *)
     |simpl (* new goal *)].
 
-Lemma tac_rel_load_r `{logrelG Σ} ℶ1 ℶ2 E1 E2 Δ Γ K i1 (l : loc) e t tres τ v :
+Lemma tac_rel_load_r `{logrelG Σ} ℶ1 ℶ2 E1 E2 Δ Γ K i1 (l : loc) q e t tres τ v :
   nclose specN ⊆ E1 →
   t = fill K (Load (# l)) →
-  envs_lookup i1 ℶ1 = Some (false, l ↦ₛ v)%I →
+  envs_lookup i1 ℶ1 = Some (false, l ↦ₛ{q} v)%I →
   envs_simple_replace i1 false
-    (Esnoc Enil i1 (l ↦ₛ v)%I) ℶ1 = Some ℶ2 →
+    (Esnoc Enil i1 (l ↦ₛ{q} v)%I) ℶ1 = Some ℶ2 →
   tres = fill K (of_val v) →
   (ℶ2 ⊢ bin_log_related E1 E2 Δ Γ e tres τ) →
   (ℶ1 ⊢ bin_log_related E1 E2 Δ Γ e t τ).
@@ -369,7 +369,7 @@ Tactic Notation "rel_load_r" :=
   eapply (tac_rel_load_r);
     [solve_ndisj || fail "rel_load_r: cannot prove 'nclose specN ⊆ ?'"
     |tac_bind_helper (* e = fill K (Store (# l) e') *)
-    |iAssumptionCore || fail "rel_load_r: cannot find ? ↦ₛ ?"
+    |iAssumptionCore || fail "rel_load_r: cannot find ? ↦ₛ{?} ?"
     |env_cbv; reflexivity || fail "rel_load_r: this should not happen"
     |simpl; reflexivity  (* tres = fill K (of_val v) *)
     |simpl (* new goal *)].

theories/logrel/rules.v

@@ -420,10 +420,10 @@ Section properties.
     iApply (bin_log_related_alloc_l); auto. assumption.
   Qed.
 
-  Lemma bin_log_related_load_l Δ Γ E1 E2 K l t τ :
+  Lemma bin_log_related_load_l Δ Γ E1 E2 K l q t τ :
     (|={E1,E2}=> ∃ v',
-      ▷(l ↦ᵢ v') ∗
-      ▷(l ↦ᵢ v' -∗ ({ E2,E1;Δ;Γ } ⊨ fill K (of_val v') ≤log≤ t : τ)))%I
+      ▷(l ↦ᵢ{q} v') ∗
+      ▷(l ↦ᵢ{q} v' -∗ ({ E2,E1;Δ;Γ } ⊨ fill K (of_val v') ≤log≤ t : τ)))%I
     -∗ {E1,E1;Δ;Γ} ⊨ fill K (! #l) ≤log≤ t : τ.
   Proof.
     iIntros "Hlog".
@@ -432,9 +432,9 @@ Section properties.
     iApply (wp_load with "Hl"); auto.
   Qed.
 
-  Lemma bin_log_related_load_l' Δ Γ E1 K l v' t τ :
-    ▷ l ↦ᵢ v' -∗
-    ▷ (l ↦ᵢ v' -∗ ({E1,E1;Δ;Γ} ⊨ fill K (of_val v') ≤log≤ t : τ))
+  Lemma bin_log_related_load_l' Δ Γ E1 K l q v' t τ :
+    ▷ l ↦ᵢ{q} v' -∗
+    ▷ (l ↦ᵢ{q} v' -∗ ({E1,E1;Δ;Γ} ⊨ fill K (of_val v') ≤log≤ t : τ))
     -∗ {E1,E1;Δ;Γ} ⊨ fill K !#l ≤log≤ t : τ.
   Proof.
     iIntros "Hl Hlog".
@@ -759,14 +759,14 @@ Section properties.
     done.
   Qed.
 
-  Lemma bin_log_related_load_r Δ Γ E1 E2 K l v' t τ
+  Lemma bin_log_related_load_r Δ Γ E1 E2 K l q v' t τ
     (Hmasked : nclose specN ⊆ E1) :
-    l ↦ₛ v' -∗
-    (l ↦ₛ v' -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (of_val v') : τ)
+    l ↦ₛ{q} v' -∗
+    (l ↦ₛ{q} v' -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (of_val v') : τ)
     -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (Load (# l)) : τ.
   Proof.
     iIntros "Hl Hlog".
-    pose (Φ := (fun w => ⌜w = v'⌝ ∗ l ↦ₛ v')%I).
+    pose (Φ := (fun w => ⌜w = v'⌝ ∗ l ↦ₛ{q} v')%I).
     iApply (bin_log_related_step_r Φ with "[Hl]"); eauto.
     { cbv[Φ].
       iIntros (ρ j K') "#Hs Hj /=". iExists v'.

theories/logrel/threadpool.v

 (* The threadpool RA *)
 From iris.algebra Require Import auth gmap agree list.
-From iris.base_logic Require Export gen_heap invariants.
+From iris.base_logic Require Export gen_heap invariants fractional.
 From iris_logrel.F_mu_ref_conc Require Import lang.
 Import uPred.
 
@@ -117,3 +117,28 @@ Section conversions.
     {[j := Excl e]} ≼ to_tpool tp → to_tpool tp !! j = Excl' e.
   Proof. rewrite tpool_lookup. by move=> /tpool_singleton_included=> ->. Qed.
 End conversions.
+
+Section mapsto.
+  Context `{cfgSG Σ}.
+
+  Global Instance mapsto_fractional l v : Fractional (λ q, l ↦ₛ{q} v)%I.
+  Proof.
+    intros p q. rewrite heapS_mapsto_eq -own_op -auth_frag_op.
+    by rewrite pair_op op_singleton pair_op agree_idemp right_id.
+  Qed.
+  Global Instance mapsto_as_fractional l q v :
+    AsFractional (l ↦ₛ{q} v) (λ q, l ↦ₛ{q} v)%I q.
+  Proof. split. done. apply _. Qed.
+
+  Lemma mapsto_agree l q1 q2 v1 v2 : l ↦ₛ{q1} v1 -∗ l ↦ₛ{q2} v2 -∗ ⌜v1 = v2⌝.
+  Proof.
+    apply uPred.wand_intro_r.
+    rewrite heapS_mapsto_eq -own_op -auth_frag_op own_valid uPred.discrete_valid.
+    f_equiv=> /auth_own_valid /=.
+    rewrite pair_op op_singleton right_id pair_op.
+    move=> [_ Hv]. move:Hv => /=.
+    rewrite singleton_valid.
+    by intros [_ ?%agree_op_invL'].
+  Qed.
+
+End mapsto.