Add a stronger rule for a_load_spec, which quantifies existentially over the fraction 'q'.

theories/c_translation/translation.v

@@ -133,14 +133,16 @@ Section proofs.
       iPureIntro. apply lvl_included. destruct b'; eauto.
   Qed.
 
-  Lemma a_load_spec R Φ q e :
-    awp e R (λ v, ∃ (l : loc) (w : val), ⌜v = #l⌝ ∗ l ↦U{q} w ∗ (l ↦U{q} w -∗ Φ w)) -∗
+
+  Lemma a_load_spec_exists_frac R Φ e :
+    awp e R (λ v, ∃ (l : loc) (q: frac) (w : val), ⌜v = #l⌝ ∗ l ↦U{q} w ∗ (l ↦U{q} w -∗ Φ w)) -∗
     awp (a_load e) R Φ.
   Proof.
-    iIntros "H". awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam.
+    iIntros "H".
+    awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam.
     iApply awp_bind.
     iApply (awp_wand with "H"). clear v.
-    iIntros (v). iDestruct 1 as (l w) "(% & Hl & HΦ)". subst.
+    iIntros (v). iDestruct 1 as (l q w) "(% & Hl & HΦ)". subst.
     awp_lam.
     iApply awp_atomic_env.
     iIntros (env) "Henv HR".
@@ -165,6 +167,17 @@ Section proofs.
     - iApply "HΦ". iExists b'. iSplit; eauto.
   Qed.
 
+  Lemma a_load_spec R Φ q e :
+    awp e R (λ v, ∃ (l : loc) (w : val), ⌜v = #l⌝ ∗ l ↦U{q} w ∗ (l ↦U{q} w -∗ Φ w)) -∗
+    awp (a_load e) R Φ.
+  Proof.
+    iIntros "H".
+    iApply a_load_spec_exists_frac.
+    awp_apply (awp_wand with "H").
+    iIntros (v) "H". iDestruct "H" as (l w ->) "[H1 H2]".
+    eauto with iFrame.
+  Qed.
+
   Lemma a_un_op_spec R Φ e op:
     awp e R (λ v, ∃ w, ⌜un_op_eval op v = Some w⌝ ∧ Φ w) -∗
     awp (a_un_op op e) R Φ.