Simplification WP rule is_unique

theories/logical_mapsto.v

@@ -2354,6 +2354,33 @@ Proof.
   destruct (decide (r1 = r2)); simplify_eq; auto.
 Qed.
 
+Lemma unique_in_registersL_pc_no_overlap
+  (pc_p : Perm) (pc_b pc_e pc_a : Addr) (pc_v : Version)
+  (p : Perm) (b e a : Addr) (v : Version)
+  (src : RegName) (regs : LReg) :
+  PC ≠ src ->
+  isCorrectLPC (LCap pc_p pc_b pc_e pc_a pc_v) ->
+  regs !! PC = Some (LCap pc_p pc_b pc_e pc_a pc_v) ->
+  unique_in_registersL regs src (LCap p b e a v) ->
+  pc_a ∉ finz.seq_between b e.
+Proof.
+  intros Hpc_neq_pc Hvpc Hpc Hunique_regs.
+  assert (pc_a ∈ finz.seq_between pc_b pc_e).
+  { rewrite isCorrectLPC_isCorrectPC_iff /=  in Hvpc.
+    apply isCorrectPC_withinBounds in Hvpc.
+    by apply withinBounds_in_seq.
+  }
+  intro contra.
+  rewrite /unique_in_registersL in Hunique_regs.
+  eapply map_Forall_lookup_1 in Hunique_regs; eauto.
+  destruct (decide (PC = src)); auto.
+  apply Hunique_regs.
+  rewrite /overlap_wordL /overlap_word //=.
+  apply elem_of_finz_seq_between in H,contra.
+  destruct H,contra.
+  destruct (b <? pc_b)%a eqn:Hb; solve_addr.
+Qed.
+
 
 (** Instantiation of the program logic *)
 

theories/rules/rules_IsUnique.v

@@ -699,7 +699,6 @@ Section cap_lang_rules.
 
   Qed.
 
-
   Lemma wp_isunique_success'
     (Ep : coPset)
     (pc_p : Perm) (pc_b pc_e pc_a pc_a' : Addr) (pc_v : Version)
@@ -710,7 +709,6 @@ Section cap_lang_rules.
 
     decodeInstrWL lw = IsUnique dst src →
     isCorrectLPC (LCap pc_p pc_b pc_e pc_a pc_v) →
-    pc_a ∉ finz.seq_between b e -> (* TODO is that necessary ? Or can I derive it ? *)
     (pc_a + 1)%a = Some pc_a' →
     p ≠ E ->
 
@@ -733,7 +731,7 @@ Section cap_lang_rules.
           ∗ (pc_a, pc_v) ↦ₐ lw )
         }}}.
   Proof.
-    iIntros (Hinstr Hvpc Hpca_notin Hpca Hp φ) "(>HPC & >Hsrc & >Hdst & >Hpc_a) Hφ".
+    iIntros (Hinstr Hvpc Hpca Hp φ) "(>HPC & >Hsrc & >Hdst & >Hpc_a) Hφ".
     iDestruct (map_of_regs_3 with "HPC Hsrc Hdst") as "[Hrmap (%&%&%)]".
     rewrite /region_mapsto.
     iDestruct (memMap_resource_1 with "Hpc_a") as "Hmmap".
@@ -775,7 +773,9 @@ Section cap_lang_rules.
       iFrame.
 
       assert ( mem' !! (pc_a, pc_v) = Some lw ) as Hmem'_pca.
-      { eapply is_valid_updated_lmemory_notin_preserves_lmem; eauto; by simplify_map_eq. }
+      { eapply is_valid_updated_lmemory_notin_preserves_lmem; eauto ; last by simplify_map_eq.
+        eapply unique_in_registersL_pc_no_overlap; eauto; by simplify_map_eq.
+      }
 
       assert (
           exists lws,
@@ -798,7 +798,6 @@ Section cap_lang_rules.
       by rewrite map_length.
   Qed.
 
-  (* TODO merge wp_opt from Dominique's branch and use it *)
   (* TODO extend proofmode, which means cases such as:
      dst = PC, src = PC, dst = stc *)