From 1d81cfca6ac9d761741d84572164aebf61e327db Mon Sep 17 00:00:00 2001 From: JuneRousseau Date: Sat, 14 Sep 2024 23:32:04 +0000 Subject: [PATCH] deploy: d31966ccde5aa5aa7c0ca7b9e61b7373f11bed77 --- .../cap_machine.ftlr.IsUnique.html | 758 +++++++++--------- .../attestation_refactor_ftlr/indexpage.html | 298 +++---- 2 files changed, 547 insertions(+), 509 deletions(-) diff --git a/branch/june/attestation_refactor_ftlr/cap_machine.ftlr.IsUnique.html b/branch/june/attestation_refactor_ftlr/cap_machine.ftlr.IsUnique.html index d310d213..1ac00779 100644 --- a/branch/june/attestation_refactor_ftlr/cap_machine.ftlr.IsUnique.html +++ b/branch/june/attestation_refactor_ftlr/cap_machine.ftlr.IsUnique.html @@ -355,7 +355,6 @@

cap_machine.ftlr.IsUnique

      decide (reg_allows_sweep lregs r p b e a v /\ (r = PC \/ pc_a ∉ (finz.seq_between b e)))
    in

-
    length la = length Ps ->
    allow_sweep_mem lregs r pc_a pc_v pc_lw p b e a v lmem Ps false
    -∗ ([∗ map] la↦lw ∈ lmem, la ↦ₐ lw)
@@ -385,234 +384,173 @@

cap_machine.ftlr.IsUnique

  Unshelve. Fail idtac. Admitted.

-  (* TODO @June redo the proof in the same style as Load or Store *)
-  Lemma isunique_case (lregs : leibnizO LReg)
-    (ppc : Perm) (bpc epc apc : Addr) (vpc : Version)
-    (lwpc : LWord) (dst src : RegName) (P : D):
-    ftlr_instr lregs ppc bpc epc apc vpc lwpc (IsUnique dst src) P.
+  Lemma cond_open_contra
+    ppc bpc epc apc vpc lregs src psrc bsrc esrc asrc vsrc :
+    psrc ≠ machine_base.E ->
+    <[PC:=LCap ppc bpc epc apc vpc]> lregs !! src = Some (LCap psrc bsrc esrc asrc vsrc) ->
+    unique_in_registersL (<[PC:=LCap ppc bpc epc apc vpc]> lregs) src
+      (LCap psrc bsrc esrc asrc vsrc) ->
+    (bpc <= apc < epc)%a ->
+    ¬ (reg_allows_sweep
+         (<[PC:=LCap ppc bpc epc apc vpc]> lregs) src psrc bsrc
+         esrc asrc vsrc ∧ (src = PC ∨ apc ∉ finz.seq_between bsrc esrc))
+    -> psrc = O.
  Proof.
-    intros Hp Hsome i Hbae Hi.
-    iIntros "#IH #Hinv #Hinva #Hreg #(Hread & Hwrite & %HpersP) Hown Ha HP Hcls HPC Hmap".
-    specialize (HpersP lwpc).
-    rewrite delete_insert_delete.
-    iDestruct ((big_sepM_delete _ _ PC) with "[HPC Hmap]") as "Hmap /=";
-      [apply lookup_insert|rewrite delete_insert_delete;iFrame|]. simpl.
- -
-    (* To read out PC's name later, and needed when calling wp_load *)
-    assert(∀ x : RegName, is_Some (<[PC:=LCap ppc bpc epc apc vpc]> lregs !! x)) as Hsome'.
+    intros Hp_neq_E Hlwsrc' Hunique_regs Hbae Hdecide.
+    rewrite /reg_allows_sweep in Hdecide.
+    apply not_and_r in Hdecide.
+    destruct Hdecide as [Hdecide|Hdecide]; cycle 1.
    {
-      intros. destruct (decide (x = PC)) as [Hx|Hx].
-      rewrite Hx lookup_insert; unfold is_Some. by eexists.
-      by rewrite lookup_insert_ne.
+      exfalso.
+      apply Decidable.not_or in Hdecide.
+      destruct Hdecide as [Hsrc_neq_PC Hapc_overlap].
+      apply Decidable.not_not in Hapc_overlap.
+      2: {
+        clear.
+        assert (forall (a : Addr) (la : list Addr), Decision (apc ∈ finz.seq_between bsrc esrc))
+          by (intros; solve_decision).
+        specialize (H apc (finz.seq_between bsrc esrc)).
+        destruct H as [H'|H'] ; [left|right]; done.
+      }
+      clear -Hunique_regs Hapc_overlap Hsrc_neq_PC Hbae.
+      rewrite /unique_in_registersL in Hunique_regs.
+      eapply map_Forall_insert_1_1 in Hunique_regs.
+      rewrite decide_False in Hunique_regs; auto.
+      apply Hunique_regs.
+      rewrite /overlap_wordL /overlap_word //=.
+      apply elem_of_finz_seq_between in Hapc_overlap.
+      destruct (bsrc <? bpc)%a eqn:Hneq; solve_addr.
    }
-
-    (* Initializing the names for the values of Hsrc now, to instantiate the existentials in step 1 *)
-    assert (∃ psrc bsrc esrc asrc vsrc, read_reg_inr (<[PC:=LCap ppc bpc epc apc vpc]> lregs) src psrc bsrc esrc asrc vsrc)
-      as (psrc & bsrc & esrc & asrc & vsrc & HVsrc).
-    {
-      specialize Hsome' with src as Hsrc.
-      destruct Hsrc as [wsrc Hsomesrc].
-      unfold read_reg_inr. rewrite Hsomesrc.
-      destruct wsrc as [|[ psrc bsrc esrc asrc vsrc|] | ]; try done.
-      by repeat eexists.
+    { rewrite /reg_allows_sweep in Hdecide.
+      apply Decidable.not_and in Hdecide; last apply lookup_dec.
+      destruct Hdecide as [Hdecide|Hdecide].
+      + by rewrite Hlwsrc' in Hdecide.
+      + destruct psrc ; try done.
    }
-
-    (* Step 1: open the region, if necessary,
-       and store all the resources obtained from the region in allow_load_res *)
-    iDestruct (create_sweep_res with "[$Hreg] [$Hinv] [%]") as (Ps) "[%Hlen_Ps HSweepRes]"
-    ; [ eassumption
-      | by apply elem_of_finz_seq_between
-      |].
- -
-    (* Step 2: derive the concrete map of memory we need, and any spatial predicates holding over it *)
-    iMod (sweep_res_implies_mem_map with "HSweepRes Ha") as (mem) "[HSweepMem >HMemRes]".
-    set (E := ⊤ ∖ ↑logN.@(apc, vpc)).
-    set (E' := allow_sweep_mask (list_remove_elem apc (finz.seq_between bsrc esrc)) vsrc apc vpc).
-    set (cond_open :=
-           decide
-             (reg_allows_sweep (<[PC:=LCap ppc bpc epc apc vpc]> lregs) src psrc bsrc esrc asrc
-                vsrc ∧ (src = PC ∨ apc ∉ finz.seq_between bsrc esrc))
-        ).
- -
-    (* Step 3:  derive the non-spatial conditions over the memory map*)
-    iDestruct (mem_map_implies_pure_conds with "HSweepMem") as %HReadPC.
- -
-   (* Step 4: move the later outside, so that we can remove it after applying wp_load *)
-     iDestruct (allow_sweep_mem_later with "HSweepMem") as "HSweepMem"; auto.
- -
-    iApply (wp_isunique with "[$Hmap $HMemRes]")
-    ; eauto
-    ; [ by simplify_map_eq
-      | rewrite /subseteq /map_subseteq /set_subseteq_instance
-        ; intros rr _; apply elem_of_dom
-        ; rewrite lookup_insert_is_Some';
-        eauto
-      |].
- -
-    iNext; iIntros (lregs' lmem' retv) "(%Hspec & Hmem & Hmap)".
- -
-    destruct Hspec as
-      [ psrc' bsrc' esrc' asrc' vsrc' Hlwsrc' Hp_neq_E Hupd Hunique_regs Hincr_PC
-      | ? Hlwsrc Hnot_sealed Hunique_regs Hmem' Hincr_PC
-      | lwsrc' psrc' bsrc' esrc' asrc' vsrc' Hlwsrc Hlwsrc' Hmem' Hincr_PC
-      | ? ? Hfail]
-    ; simplify_map_eq
-    ; try (rewrite Hlwsrc' in Hlregs_src; simplify_eq)
-    ; try (rewrite Hlwsrc in Hlregs_src; simplify_eq)
-    ; try (cbn in Hlwsrc' ; simplify_eq).
+  Unshelve. Fail idtac. Admitted.

-    { (* Sweep true cap : update *)
+  Lemma mem_map_recover_res_upd
+    (lregs : leibnizO LReg) (lmem lmem': LMem)
+    (pc_p : Perm) (pc_b pc_e pc_a : Addr) (pc_v : Version) (pc_lw : LWord)
+    (r : RegName)
+    (p : Perm) (b e a : Addr) (v : Version)
+    (Ps : list D) (P : D) :

-      rewrite /allow_sweep_mem.
-      subst cond_open; set (cond_open := decide (_ /\ _)).
-      iDestruct "HSweepMem" as "(_ & HSweepMem)".
-      destruct cond_open as [Hdecide|Hdecide]; cycle 1.
-      + iDestruct "HSweepMem" as "->".
-        iModIntro.
-        rewrite /read_reg_inr Hlwsrc' in HVsrc; simplify_eq.
-        apply not_and_r in Hdecide.
-        destruct Hdecide as [Hdecide|Hdecide]; cycle 1.
-        {
-          exfalso.
-          apply Decidable.not_or in Hdecide.
-          destruct Hdecide as [Hsrc_neq_PC Hapc_overlap].
-          apply Decidable.not_not in Hapc_overlap.
-          2: {
-            clear.
-            assert (forall (a : Addr) (la : list Addr), Decision (apc ∈ la))
-              by (intros; solve_decision).
-            specialize (H apc (finz.seq_between bsrc esrc)).
-            destruct H as [H'|H'] ; [left|right]; done.
-          }
-          clear -Hunique_regs Hapc_overlap Hsrc_neq_PC Hbae.
-          rewrite /unique_in_registersL in Hunique_regs.
-          eapply map_Forall_insert_1_1 in Hunique_regs.
-          rewrite decide_False in Hunique_regs; auto.
-          apply Hunique_regs.
-          rewrite /overlap_wordL /overlap_word //=.
-          apply elem_of_finz_seq_between in Hapc_overlap.
-          destruct (bsrc <? bpc)%a eqn:Hneq; solve_addr.
-        }
-        { rewrite /reg_allows_sweep in Hdecide.
-          apply Decidable.not_and in Hdecide; last apply lookup_dec.
-          destruct Hdecide as [Hdecide|Hdecide].
-          + by rewrite Hlwsrc' in Hdecide.
-          + destruct (decide (psrc = O)) as [->|Hpsrc_O]; last (destruct psrc ; try done).
-            assert (src ≠ PC) as Hsrc_ne_pc.
-            { intro ; subst ; inversion i ; inversion H1 ; cbn in * ; simplify_map_eq.
-              destruct H8 ; done.
-            }
-            assert ( lmem' !! (apc, vpc) = Some lwpc ) as Hmem'_pca.
-            { eapply is_valid_updated_lmemory_preserves_lmem; cycle 1 ; eauto. }
-            rewrite -(insert_id lmem' (apc,vpc) lwpc);auto.
-            iDestruct (big_sepM_insert_delete with "Hmem") as "[Hmem _]".
-            iMod ("Hcls" with "[Hmem HP]");[iExists lwpc;iFrame|iModIntro].
-            iApply wp_pure_step_later; auto.
-            iNext; iIntros "_".
-            incrementLPC_inv; simplify_map_eq.
-            assert (dst ≠ PC) as Hdst_pc by (intro ; simplify_map_eq).
-            simplify_map_eq.
-            do 2 (rewrite (insert_commute _ _ PC) //) ; rewrite insert_insert.
-            iApply ("IH" $! (<[dst := (LInt 1)]> (<[src:=LCap O bsrc esrc asrc (vsrc + 1)]> lregs))
-                     with "[%] [] [Hmap] [$Hown]"); eauto.
-            { intro; by repeat (rewrite lookup_insert_is_Some'; right). }
-            {
-              iIntros (ri ? Hri Hvs).
-              destruct (decide (ri = dst)) ; simplify_map_eq
-              ; first by rewrite !fixpoint_interp1_eq.
-              destruct (decide (ri = src)); simplify_map_eq;
-              first by rewrite !fixpoint_interp1_eq.
-              iDestruct ("Hreg" $! ri _ Hri Hvs) as "Hinterp_dst"; eauto.
-            }
-            rewrite !fixpoint_interp1_eq /=; destruct Hp as [-> | ->]; iFrame "Hinv"; auto.
-        }
-      + destruct Hdecide as [ [Hsrc_lregs Hread_src] Hvalid_sweep].
-        destruct (decide (src = PC)) as [->|Hsrc_ne_pc]; [clear Hvalid_sweep |].
- -
-      - (* src = PC *)
-        incrementLPC_inv
-          as (p_pc' & b_pc' & e_pc' &a_pc' &v_pc' & ? & HPC & Z & Hregs')
-        ; simplify_map_eq.
- +    let la := (list_remove_elem pc_a (finz.seq_between b e)) in
+    let E := ⊤ ∖ ↑logN.@(pc_a, pc_v) in
+    let E' := allow_sweep_mask la v pc_a pc_v in
+    let cond_open :=
+      decide (reg_allows_sweep (<[PC:=LCap pc_p pc_b pc_e pc_a pc_v]> lregs) r p b e a v /\ (r = PC \/ pc_a ∉ (finz.seq_between b e)))
+    in

+    let lregs' := (<[PC:=LCap pc_p pc_b pc_e pc_a pc_v]> lregs) in
+
+    length la = length Ps ->
+    p ≠ machine_base.E ->
+    is_valid_updated_lmemory lmem (finz.seq_between b e) v lmem' ->
+    unique_in_registersL lregs' r (LCap p b e a v) ->
+    lregs' !! r = Some (LCap p b e a v) ->
+    isCorrectLPC (LCap pc_p pc_b pc_e pc_a pc_v) ->
+    Persistent (P pc_lw) ->
+
+    □ (∀ lw : LWord, P lw -∗ fixpoint interp1 lw)
+    -∗ P pc_lw
+    -∗ allow_sweep_mem lregs' r pc_a pc_v pc_lw p b e a v lmem Ps false
+    -∗ ([∗ map] la↦lw ∈ lmem', la ↦ₐ lw)
+    ={(if cond_open then E' else E), E}=∗
+    (pc_a,pc_v) ↦ₐ pc_lw ∗
+    if cond_open
+    then interp (LCap p b e a (v+1))
+    else emp
+  .
+  Proof.
+    intros * Hlen_Ps Hp_ne_E Hvalid_lmem' Hunique_regs Hlwsrc' Hcorrect_pc HpersP
+    ; iIntros "#Hread #HP HSweepMem Hmem".
+    subst lregs'.
+    assert ( (pc_b <= pc_a < pc_e)%a) as Hbae.
+    { inversion Hcorrect_pc ; inversion H1 ; cbn in * ; simplify_map_eq; done. }
+    iDestruct "HSweepMem" as "(%Hread & HSweepMem)".
+    subst cond_open; set (cond_open := decide _).
+    destruct cond_open as [Hdecide|Hdecide]; cycle 1.
+    - iDestruct "HSweepMem" as "->".
+      apply cond_open_contra in Hdecide; auto ; simplify_eq.
+      all: assert (r ≠ PC)
+        as Hr_ne_pc
+             by (intro ; subst ; inversion Hcorrect_pc
+                 ; inversion H1 ; cbn in * ; simplify_map_eq
+                 ; by destruct H8).
+      all: assert ( lmem' !! (pc_a, pc_v) = Some pc_lw )
+        as Hmem'_pca
+             by (eapply is_valid_updated_lmemory_preserves_lmem; cycle 1 ; eauto; by simplify_map_eq).
+      all: rewrite -(insert_id lmem' (pc_a,pc_v) pc_lw);auto.
+      all: iDestruct (big_sepM_insert_delete with "Hmem") as "[Hmem _]"; iFrame.
+      done.
+    - destruct Hdecide as [ [Hsrc_lregs Hread_src] Hvalid_sweep].
+      (* TODO @June: is there any part of the proof that is common
+         and could be refactored beforehand ? *)
+      destruct (decide (r = PC)) as [->|r_ne_pc]
+      ; [clear Hvalid_sweep |]
+      ; simplify_map_eq.
+      + (* r = PC *)
        iDestruct "HSweepMem" as (lws Hlen_lws ->) "HSweepRest".
+        iDestruct "HSweepRest" as "(HPrange & %Hpers & #Hread_cond & Hcls_src)".
        subst E'.
-        rewrite /read_reg_inr in HVsrc; simplify_map_eq.
-        set (la' := (list_remove_elem asrc (finz.seq_between bsrc esrc)) ).
- -
-        assert (dst ≠ PC) as Hdst_pc by (intro ; simplify_map_eq); simplify_map_eq.
-        do 2 (rewrite (insert_commute _ _ PC) //);
-        rewrite !insert_insert.

-        assert (a_pc' ∈ finz.seq_between b_pc' e_pc') as Hapc_in_range.
-        { clear -i.
-          inversion i ; cbn in * ; simplify_eq.
-          inversion H0 ; cbn in * ; simplify_eq.
-          by apply elem_of_finz_seq_between.
+        assert (a ∈ finz.seq_between b e) as Hapc_in_range.
+        { by apply isCorrectLPC_isCorrectPC_iff, isCorrectPC_withinBounds, withinBounds_in_seq
+         in Hcorrect_pc.
        }

-        assert ( a_pc' ∉ la') as Hapc_notin_la'
-          by (by subst la' ; apply not_elemof_list_remove_elem).
+        assert ( a ∉ (list_remove_elem a (finz.seq_between b e)))
+         as Hapc_notin_la' by (by apply not_elemof_list_remove_elem).

-        assert ( lmem' !! (a_pc', vsrc) = Some lwpc ) as Hmem'_pca.
-        { eapply is_valid_updated_lmemory_preserves_lmem; cycle 1 ; eauto.
+        assert ( lmem' !! (a, v) = Some pc_lw ) as Hmem'_pca.
+        { eapply is_valid_updated_lmemory_preserves_lmem ; cycle 1 ; eauto.
          by simplify_map_eq.
        }
-
-        assert ( lmem' !! (a_pc', vsrc+1) = Some lwpc ) as Hmem'_pca_next.
+        assert ( lmem' !! (a, v+1) = Some pc_lw ) as Hmem'_pca_next.
        { eapply is_valid_updated_lmemory_preserves_lmem_next; cycle 1
-          ; eauto
-          ; last by simplify_map_eq.
-          eapply Forall_forall; intros a Ha.
+         ; eauto
+         ; last by simplify_map_eq.
+          eapply Forall_forall; intros a' Ha'.
          rewrite lookup_insert_ne //=; last (intro ; simplify_eq ; lia).
          eapply logical_region_version_neq; eauto ; last lia.
        }

-        assert (logical_region_map la' lws vsrc !! (a_pc', vsrc) = None)
-          as Hasrc_notin_reg_la'.
-        { subst la'. eapply logical_region_notin; eauto. }
+        assert (logical_region_map (list_remove_elem a (finz.seq_between b e)) lws v !! (a, v) = None)
+         as Hasrc_notin_reg_la'.
+        { eapply logical_region_notin; eauto. }


-        assert ( ((logical_region_map la' lws) ) vsrc ⊆ lmem' )
-          as Hmem'_be.
+        assert ( ((logical_region_map (list_remove_elem a (finz.seq_between b e)) lws) ) v ⊆ lmem' )
+         as Hmem'_be.
        {
-          eapply is_valid_updated_lmemory_lmem_incl with (la := (finz.seq_between b_pc' e_pc'))
+         eapply is_valid_updated_lmemory_lmem_incl with (la := (finz.seq_between b e))
          ; eauto.
          eapply is_valid_updated_lmemory_insert'; eauto.
-          subst la'.
-          eapply Forall_forall; intros a Ha.
+          eapply Forall_forall; intros a' Ha'.
          eapply logical_region_version_neq; eauto ; last lia.
        }
-        assert ( ((logical_region_map la' lws) ) (vsrc+1) ⊆ lmem' )
-          as Hmem'_be_next.
+        assert ( ((logical_region_map (list_remove_elem a (finz.seq_between b e)) lws) ) (v+1) ⊆ lmem' )
+         as Hmem'_be_next.
        {
-          eapply map_subseteq_spec; intros [a' v'] lw' Hlw'.
-          assert (v' = vsrc+1 /\ (a' ∈ la'))
-            as [? Ha'_in_be] by (subst la' ; eapply logical_region_map_some_inv; eauto)
+         eapply map_subseteq_spec; intros [a' v'] lw' Hlw'.
+          assert (v' = v+1 /\ (a' ∈ (list_remove_elem a (finz.seq_between b e))))
+         as [? Ha'_in_be] by (eapply logical_region_map_some_inv; eauto)
          ; simplify_eq.
-          destruct Hupd.
+          destruct Hvalid_lmem'.
          eapply lookup_weaken; last eapply H0.
          rewrite update_version_region_preserves_lmem_next; eauto.
          { rewrite lookup_insert_ne.
            erewrite logical_region_map_lookup_versions; eauto.
            clear -Ha'_in_be.
-            intro ; simplify_eq ; subst la'.
-            apply not_elemof_list_remove_elem in Ha'_in_be ; auto.
+            intro ; simplify_eq.
+            apply not_elemof_list_remove_elem in Ha'_in_be ; auto.
          }
-          { subst la'.
-            eapply elem_of_submseteq; eauto.
+          { eapply elem_of_submseteq; eauto.
            eapply list_remove_elem_submsteq.
          }
          { rewrite lookup_insert_ne //=; last (intro ; simplify_eq ; lia).
@@ -620,239 +558,334 @@

cap_machine.ftlr.IsUnique

          }
        }

-        rewrite -(insert_id lmem' (a_pc', vsrc) lwpc); auto.
+        rewrite -(insert_id lmem' (a, v) pc_lw); auto.
        iDestruct (big_sepM_insert_delete with "Hmem") as "[Ha Hmem]".
- -
-        rewrite -(insert_id (_ lmem') (a_pc', vsrc+1) lwpc); auto.
+        rewrite -(insert_id (_ lmem') (a, v+1) pc_lw); auto.
        2: { rewrite lookup_delete_ne ; first by simplify_map_eq. intro ; simplify_eq ; lia. }
        iDestruct (big_sepM_insert_delete with "Hmem") as "[Ha_next Hmem]".
- -
-        eapply delete_subseteq_r with (k := ((a_pc', vsrc) : LAddr)) in Hmem'_be
+        eapply delete_subseteq_r with (k := ((a, v) : LAddr)) in Hmem'_be
        ; last (eapply logical_region_notin; eauto).
-        eapply delete_subseteq_r with (k := ((a_pc', vsrc+1) : LAddr)) in Hmem'_be
+        eapply delete_subseteq_r with (k := ((a, v+1) : LAddr)) in Hmem'_be
        ; last (eapply logical_region_notin; eauto).
        iDestruct (big_sepM_insert_difference with "Hmem") as "[Hrange Hmem]"
        ; first (eapply Hmem'_be).
- -
-        eapply delete_subseteq_r with (k := ((a_pc', vsrc) : LAddr)) in Hmem'_be_next
+        eapply delete_subseteq_r with (k := ((a, v) : LAddr)) in Hmem'_be_next
        ; last (eapply logical_region_notin ; eauto).
-        eapply delete_subseteq_r with (k := ((a_pc', vsrc+1) : LAddr)) in Hmem'_be_next
+        eapply delete_subseteq_r with (k := ((a, v+1) : LAddr)) in Hmem'_be_next
        ; last (eapply logical_region_notin ; eauto).
        eapply delete_subseteq_list_r
-          with (m3 := list_to_map (zip (map (λ a : Addr, (a, vsrc)) la') lws))
-          in Hmem'_be_next
+         with (m3 := list_to_map (zip (map (λ a : Addr, (a, v)) (list_remove_elem a (finz.seq_between b e))) lws))
+         in Hmem'_be_next
        ; eauto
        ; last (by eapply update_logical_memory_region_disjoint).
        iDestruct (big_sepM_insert_difference with "Hmem") as "[Hrange' Hmem]"
        ; first (eapply Hmem'_be_next); iClear "Hmem".
-        iDestruct "HSweepRest" as "(HPrange & %Hpers & #Hread_cond & Hcls_src)".
        iDestruct "HPrange" as "#HPrange".
-        iDestruct "HP" as "#HP".

        iMod ("Hcls_src" with "[Hrange HPrange]") as "_".
        {
-          iNext.
-          iApply region_inv_construct; try done.
-          subst la' ; auto.
-          iExists lws; iSplit ; first done; iFrame "#∗".
+         iNext.
+          iApply region_inv_construct; try done; auto.
        }
-
-
-
-
-
-
-
-
-        iModIntro.
-        iMod ("Hcls" with "[Ha HP]") as "_"; first (iNext ; iExists _ ; iFrame "#∗").
-        iModIntro.
+        iSplitL "Ha"; first by iFrame.

-        iMod (region_valid_alloc' _ b_pc' e_pc' a_pc' (a_pc'::la') (vsrc +1) (lwpc::lws) p_pc'
-               with "[HPrange HP] [Hrange' Ha_next]")
-          as "#Hinterp_src_next".
-        { destruct p_pc' ; cbn in * ; try congruence; done. }
-        { subst la' ; eapply list_remove_list_region ; auto.
+        iMod (region_valid_alloc' _ b e a (a::(list_remove_elem a (finz.seq_between b e))) (v +1) (pc_lw::lws) p
+         with "[HPrange HP] [Hrange' Ha_next]")
+         as "#Hinterp__next"; last done.
+        { destruct p ; cbn in * ; try congruence; done. }
+        { eapply list_remove_list_region ; auto.
          apply list_remove_elem_in in Hapc_in_range.
          by destruct Hapc_in_range as (la' & -> & ->).
        }
-        { iDestruct (big_sepL2_const_sepL_r _ lws with "[Hread_cond]") as "Hread_PSRC".
+        { iDestruct (big_sepL2_const_sepL_r _ lws with "[Hread_cond]") as "Hread_P".
          iSplit ; last iFrame "Hread_cond".
          by rewrite Hlen_lws.
          cbn.
          iDestruct ( big_sepL2_sep_sepL_r with "[$Hread_cond $HPrange]") as "HPs".
          iDestruct (big_sepL2_alt with "HPs") as "[_ HPs']".
          iAssert (
-              (∀ (k : nat) (x0 : leibnizO LWord * D),
-                 ⌜zip lws Ps !! k = Some x0⌝
-                 → x0.2 x0.1 ∗ □ (∀ lw0 : LWord, x0.2 lw0 -∗ fixpoint interp1 lw0) -∗ interp x0.1)
-            )%I as "bla".
+           (∀ (k : nat) (x0 : leibnizO LWord * D),
+         ⌜zip lws Ps !! k = Some x0⌝
+                 → x0.2 x0.1 ∗ □ (∀ lw0 : LWord, x0.2 lw0 -∗ fixpoint interp1 lw0) -∗ interp x0.1)
+         )%I as "bla".
          { iIntros (? ? ?) "[Ha Hpa]"; by iDestruct ("Hpa" with "Ha") as "?". }
-          iDestruct (big_sepL_impl _ (fun _ xy => interp xy.1) with "HPs' bla"
+          iDestruct (big_sepL_impl _ (fun _ xy => interp xy.1) with "HPs' bla"
                    ) as "blaa".
-          iDestruct (big_sepL2_alt (fun _ lw _ => interp lw) lws Ps with "[$blaa]") as "blaaa".
+          iDestruct (big_sepL2_alt (fun _ lw _ => interp lw) lws Ps with "[$blaa]") as "blaaa".
          by rewrite Hlen_lws.
          iSplit.
          by iApply "Hread".
-          by iDestruct (big_sepL2_const_sepL_l (fun _ lw => interp lw) lws Ps with "blaaa") as "[? ?]".
+          by iDestruct (big_sepL2_const_sepL_l (fun _ lw => interp lw) lws Ps with "blaaa") as "[? ?]".
        }
-        { iClear "#". subst la'. clear -Hlen_Ps Hlen_lws.
+        { iClear "#". clear -Hlen_Ps Hlen_lws.
          iApply big_sepL2_alt.
          iSplit; first (iPureIntro; rewrite /= map_length; lia).
          iDestruct (big_sepM_list_to_map with "Hrange'") as "?" ; last iFrame.
          rewrite fst_zip.
          apply NoDup_fmap; auto.
          { by intros x y Heq ; simplify_eq. }
-          rewrite /logical_region map_length ; lia.
+          rewrite /logical_region map_length Hlen_lws ; lia.
        }

-        iApply wp_pure_step_later; auto.
-        iNext; iIntros "_".
+      + (* r ≠ PC *)
+        iDestruct "HSweepMem" as (lws Hlen_lws ->) "HSweepRest".
+        subst E'.
+        destruct Hvalid_sweep as [Hcontra|Hapc_notin_src] ; first done.
+        subst la.
+        rewrite !list_remove_elem_notin in Hvalid_lmem', Hlen_Ps, Hlen_lws |- * ; auto.
+ +
+        assert ( lmem' !! (pc_a, pc_v) = Some pc_lw ) as Hmem'_pca.
+        { eapply is_valid_updated_lmemory_preserves_lmem; eauto; by simplify_map_eq. }
+        assert ( logical_range_map b e lws v ⊆ lmem' )
+          as Hmem'_be.
+        {
+          eapply is_valid_updated_lmemory_lmem_incl with
+            (la := (finz.seq_between b e)) (v := v)
+          ; eauto.
+          eapply is_valid_updated_lmemory_insert; eauto.
+          eapply logical_range_notin; eauto.
+          eapply Forall_forall; intros a' Ha'.
+          eapply logical_range_version_neq; eauto ; last lia.
+        }
+        assert
+          (logical_range_map b e lws (v + 1) ⊆ lmem')
+          as Hmem'_be_next.
+        { clear -Hvalid_lmem' Hlen_lws Hapc_notin_src.
+          eapply map_subseteq_spec; intros [a' v'] lw' Hlw'.
+          assert (v' = v+1 /\ (a' ∈ (finz.seq_between b e)))
+            as [? Ha'_in_be] by (eapply logical_range_map_some_inv; eauto); simplify_eq.
+          destruct Hvalid_lmem'.
+          eapply lookup_weaken; last eauto.
+          rewrite update_version_region_preserves_lmem_next; eauto.
+          all: rewrite lookup_insert_ne //=; last (intro ; set_solver).
+          erewrite logical_region_map_lookup_versions; eauto.
+          eapply logical_region_version_neq; eauto; lia.
+        }
+
+        rewrite -(insert_id lmem' (pc_a, pc_v) pc_lw); auto.
+        iDestruct (big_sepM_insert_delete with "Hmem") as "[Ha_pc Hmem]".
+        eapply delete_subseteq_r with (k := ((pc_a, pc_v) : LAddr)) in Hmem'_be
+        ; last (eapply logical_region_notin; eauto).
+        iDestruct (big_sepM_insert_difference with "Hmem") as "[Hrange Hmem]"
+        ; first (eapply Hmem'_be).
+        eapply delete_subseteq_r with (k := ((pc_a, pc_v) : LAddr)) in Hmem'_be_next
+        ; last (eapply logical_region_notin ; eauto).
+        eapply delete_subseteq_list_r
+          with (m3 := list_to_map (zip (map (λ a : Addr, (a, v)) (finz.seq_between b e)) lws))
+          in Hmem'_be_next
+        ; eauto
+        ; last (by eapply update_logical_memory_region_disjoint).
+        iDestruct (big_sepM_insert_difference with "Hmem") as "[Hrange' Hmem]"
+        ; first (eapply Hmem'_be_next); iClear "Hmem".
+        iDestruct "HSweepRest" as "(HPrange & %Hpers & #Hread_cond & Hcls_src)".
+        iDestruct "HPrange" as "#HPrange".
+        iMod ("Hcls_src" with "[Hrange HPrange]") as "_".
+        {
+          iNext.
+          iApply region_inv_construct; try done; auto.
+        }
+        iSplitL "Ha_pc"; first by iFrame.
+ +
+        iMod (region_valid_alloc _ b e a (v +1) lws p
+               with "[HPrange] [Hrange']")
+          as "#Hinterp__next"; last done.
+        { destruct p ; cbn in * ; try congruence; done. }
+        { iDestruct (big_sepL2_const_sepL_r _ lws with "[Hread_cond]") as "Hread_P".
+          iSplit ; last iFrame "Hread_cond".
+          by rewrite <- Hlen_Ps, Hlen_lws.
+          cbn.
+          iDestruct ( big_sepL2_sep_sepL_r with "[$Hread_cond $HPrange]") as "HPs".
+          iClear "Hread Hread_P HPrange".
+          iDestruct (big_sepL2_alt with "HPs") as "[_ HPs']".
+          iAssert (
+              (∀ (k : nat) (x0 : leibnizO LWord * D),
+                 ⌜zip lws Ps !! k = Some x0⌝
+                 → x0.2 x0.1 ∗ □ (∀ lw0 : LWord, x0.2 lw0 -∗ fixpoint interp1 lw0) -∗ interp x0.1)
+            )%I as "bla".
+          { iIntros (? ? ?) "[Ha Hpa]"; by iDestruct ("Hpa" with "Ha") as "?". }
+          iDestruct (big_sepL_impl _ (fun _ xy => interp xy.1) with "HPs' bla"
+                    ) as "blaa".
+          iDestruct (big_sepL2_alt (fun _ lw _ => interp lw) lws Ps with "[$blaa]") as "blaaa".
+          by rewrite Hlen_lws.
+          by iDestruct (big_sepL2_const_sepL_l (fun _ lw => interp lw) lws Ps with "blaaa") as "[? ?]".
+        }
+        { iClear "#". clear -Hlen_Ps Hlen_lws.
+          iApply big_sepL2_alt.
+          iSplit; first (iPureIntro; rewrite map_length; lia).
+          iDestruct (big_sepM_list_to_map with "Hrange'") as "?" ; last iFrame.
+          rewrite fst_zip; first (apply NoDup_logical_region).
+          rewrite /logical_region map_length Hlen_lws ; lia.
+        }
+  Unshelve. Fail idtac. Admitted.
+ +
+  Local Instance if_Persistent
+    ppc bpc epc apc vpc lregs src psrc bsrc esrc asrc vsrc:
+    Persistent (if decide (reg_allows_sweep (<[PC:=LCap ppc bpc epc apc vpc]> lregs)
+                             src psrc bsrc esrc asrc vsrc
+                           ∧ (src = PC ∨ apc ∉ finz.seq_between bsrc esrc))
+                then interp (LCap psrc bsrc esrc asrc (vsrc + 1))
+                else emp)%I.
+  Proof. intros; case_decide; apply _. Qed.
+ +
+  (* TODO @June redo the proof in the same style as Load or Store *)
+  Lemma isunique_case (lregs : leibnizO LReg)
+    (ppc : Perm) (bpc epc apc : Addr) (vpc : Version)
+    (lwpc : LWord) (dst src : RegName) (P : D):
+    ftlr_instr lregs ppc bpc epc apc vpc lwpc (IsUnique dst src) P.
+  Proof.
+    intros Hp Hsome i Hbae Hi.
+    iIntros "#IH #Hinv #Hinva #Hreg #(Hread & Hwrite & %HpersP) Hown Ha #HP Hcls HPC Hmap".
+    specialize (HpersP lwpc).
+    rewrite delete_insert_delete.
+    iDestruct ((big_sepM_delete _ _ PC) with "[HPC Hmap]") as "Hmap /=";
+      [apply lookup_insert|rewrite delete_insert_delete;iFrame|]. simpl.
+ +
+    (* To read out PC's name later, and needed when calling wp_load *)
+    assert(∀ x : RegName, is_Some (<[PC:=LCap ppc bpc epc apc vpc]> lregs !! x)) as Hsome'.
+    {
+      intros. destruct (decide (x = PC)) as [Hx|Hx].
+      rewrite Hx lookup_insert; unfold is_Some. by eexists.
+      by rewrite lookup_insert_ne.
+    }
+
+    (* Initializing the names for the values of Hsrc now, to instantiate the existentials in step 1 *)
+    assert (∃ psrc bsrc esrc asrc vsrc, read_reg_inr (<[PC:=LCap ppc bpc epc apc vpc]> lregs) src psrc bsrc esrc asrc vsrc)
+      as (psrc & bsrc & esrc & asrc & vsrc & HVsrc).
+    {
+      specialize Hsome' with src as Hsrc.
+      destruct Hsrc as [wsrc Hsomesrc].
+      unfold read_reg_inr. rewrite Hsomesrc.
+      destruct wsrc as [|[ psrc bsrc esrc asrc vsrc|] | ]; try done.
+      by repeat eexists.
+    }
+
+    (* Step 1: open the region, if necessary,
+       and store all the resources obtained from the region in allow_load_res *)
+    iDestruct (create_sweep_res with "[$Hreg] [$Hinv] [%]") as (Ps) "[%Hlen_Ps HSweepRes]"
+    ; [ eassumption
+      | by apply elem_of_finz_seq_between
+      |].
+ +
+    (* Step 2: derive the concrete map of memory we need, and any spatial predicates holding over it *)
+    iMod (sweep_res_implies_mem_map with "HSweepRes Ha") as (mem) "[HSweepMem >HMemRes]".
+    set (E := ⊤ ∖ ↑logN.@(apc, vpc)).
+    set (E' := allow_sweep_mask (list_remove_elem apc (finz.seq_between bsrc esrc)) vsrc apc vpc).
+    set (cond_open :=
+           decide
+             (reg_allows_sweep (<[PC:=LCap ppc bpc epc apc vpc]> lregs) src psrc bsrc esrc asrc
+                vsrc ∧ (src = PC ∨ apc ∉ finz.seq_between bsrc esrc))
+        ).
+ +
+    (* Step 3:  derive the non-spatial conditions over the memory map*)
+    iDestruct (mem_map_implies_pure_conds with "HSweepMem") as %HReadPC.
+ +
+    (* Step 4: move the later outside, so that we can remove it after applying wp_isunique *)
+    iDestruct (allow_sweep_mem_later with "HSweepMem") as "HSweepMem"; auto.
+ +
+    iApply (wp_isunique with "[$Hmap $HMemRes]")
+    ; eauto
+    ; [ by simplify_map_eq
+      | rewrite /subseteq /map_subseteq /set_subseteq_instance
+        ; intros rr _; apply elem_of_dom
+        ; rewrite lookup_insert_is_Some';
+        eauto
+      |].
+    iNext; iIntros (lregs' lmem' retv) "(%Hspec & Hmem & Hmap)".
+    destruct Hspec as
+      [ psrc' bsrc' esrc' asrc' vsrc' Hlwsrc' Hp_neq_E Hupd Hunique_regs Hincr_PC
+      | ? Hlwsrc Hnot_sealed Hunique_regs Hmem' Hincr_PC
+      | lwsrc' psrc' bsrc' esrc' asrc' vsrc' Hlwsrc Hlwsrc' Hmem' Hincr_PC
+      | ? ? Hfail]
+    ; simplify_map_eq
+    ; try (rewrite Hlwsrc' in Hlregs_src; simplify_eq)
+    ; try (rewrite Hlwsrc in Hlregs_src; simplify_eq)
+    ; try (cbn in Hlwsrc' ; simplify_eq).
+ +
+    { (* Sweep true cap : update *)
+      rewrite /read_reg_inr Hlwsrc' in HVsrc ; simplify_eq.
+      iMod (mem_map_recover_res_upd with "Hread HP HSweepMem Hmem") as "[Ha #Hinterp]"; auto.
+ +
+      iModIntro.
+      iMod ("Hcls" with "[Ha HP]") as "_"; first (iNext ; iExists _ ; iFrame "#∗").
+      iModIntro.
+      iApply wp_pure_step_later; auto.
+      iNext; iIntros "_".
+      simplify_map_eq.
+ +
+      incrementLPC_inv
+        as (p_pc' & b_pc' & e_pc' &a_pc' &v_pc' & ? & HPC & Z & Hregs')
+      ; simplify_map_eq.
+      assert (dst ≠ PC) as Hdst_pc by (intro ; simplify_map_eq); simplify_map_eq.
+      clear cond_open; set (cond_open := decide ( _ /\ _ )).
+      destruct cond_open as [Hdecide|Hdecide]; cycle 1.
+      - (* Case (psrc = O) *)
+        apply cond_open_contra in Hdecide; auto ; simplify_eq.
+        assert (src ≠ PC)
+          as Hr_ne_pc
+               by (intro ; subst ; inversion i
+                   ; inversion H1 ; cbn in * ; simplify_map_eq
+                   ; by destruct H8).
+        do 2 (rewrite (insert_commute _ _ PC) //); rewrite !insert_insert.
        simplify_map_eq.
-        iApply ("IH" $! (<[dst := _]> lregs) with "[%] [] [Hmap] [$Hown]")
+        iApply ("IH" $! (<[dst := LInt 1]> (<[src := _]> lregs)) with "[%] [] [Hmap] [$Hown]")
        ; eauto.
        { intro; by repeat (rewrite lookup_insert_is_Some'; right). }
        { iIntros (r1 lw1 Hr1 Hlw1).
          destruct (decide (r1 = dst)) as [ |Hr1_dst]
          ; simplify_map_eq; first (rewrite !fixpoint_interp1_eq //=).
-          iApply "Hreg"; eauto. }
-        { rewrite !fixpoint_interp1_eq //= ; destruct p_pc'; destruct Hp ; done. }
-
-
-        - (* src ≠ PC *)
-          destruct Hvalid_sweep as [Hcontra|Hapc_notin_src] ; first done.
-          incrementLPC_inv
-            as (p_pc' & b_pc' & e_pc' &a_pc' &v_pc' & ? & HPC & Z & Hregs')
-          ; simplify_map_eq.
-          assert (dst ≠ PC) as Hdst_pc by (intro ; simplify_map_eq); simplify_map_eq.
-          do 2 (rewrite (insert_commute _ _ PC) //); rewrite insert_insert.
- -
-          assert ( lmem' !! (a_pc', v_pc') = Some lwpc ) as Hmem'_pca.
-          { eapply is_valid_updated_lmemory_preserves_lmem; eauto. }
-
-          iDestruct "HSweepMem" as (lws Hlen_lws ->) "HSweepRest".
-          subst E'.
-          rewrite /read_reg_inr in HVsrc; simplify_map_eq.
-          rewrite !list_remove_elem_notin in Hupd, Hlen_Ps, Hlen_lws |- * ; auto.
- -
-          assert ( logical_range_map bsrc esrc lws vsrc ⊆ lmem' )
-            as Hmem'_be.
-          {
-            eapply is_valid_updated_lmemory_lmem_incl with
-              (la := (finz.seq_between bsrc esrc)) (v := vsrc)
-            ; eauto.
-            eapply is_valid_updated_lmemory_insert; eauto.
-            eapply logical_range_notin; eauto.
-            eapply Forall_forall; intros a Ha.
-            eapply logical_range_version_neq; eauto ; last lia.
-          }
-
-          assert
-            (logical_range_map bsrc esrc lws (vsrc + 1) ⊆ lmem')
-            as Hmem'_be_next.
-          { clear -Hupd Hlen_lws Hapc_notin_src.
-            eapply map_subseteq_spec; intros [a' v'] lw' Hlw'.
-            assert (v' = vsrc+1 /\ (a' ∈ (finz.seq_between bsrc esrc)))
-              as [? Ha'_in_be] by (eapply logical_range_map_some_inv; eauto); simplify_eq.
-            destruct Hupd.
-            eapply lookup_weaken; last eauto.
-            rewrite update_version_region_preserves_lmem_next; eauto.
-            all: rewrite lookup_insert_ne //=; last (intro ; set_solver).
-            erewrite logical_region_map_lookup_versions; eauto.
-            eapply logical_region_version_neq; eauto; lia.
-          }
-
-          rewrite -(insert_id lmem' (a_pc', v_pc') lwpc); auto.
-          iDestruct (big_sepM_insert_delete with "Hmem") as "[Ha_pc Hmem]".
-          eapply delete_subseteq_r with (k := ((a_pc', v_pc') : LAddr)) in Hmem'_be
-          ; last (eapply logical_region_notin; eauto).
-          iDestruct (big_sepM_insert_difference with "Hmem") as "[Hrange Hmem]"
-          ; first (eapply Hmem'_be).
-          eapply delete_subseteq_r with (k := ((a_pc', v_pc') : LAddr)) in Hmem'_be_next
-          ; last (eapply logical_region_notin ; eauto).
-          eapply delete_subseteq_list_r
-            with (m3 := list_to_map (zip (map (λ a : Addr, (a, vsrc)) (finz.seq_between bsrc esrc)) lws))
-            in Hmem'_be_next
-          ; eauto
-          ; last (by eapply update_logical_memory_region_disjoint).
-          iDestruct (big_sepM_insert_difference with "Hmem") as "[Hrange' Hmem]"
-          ; first (eapply Hmem'_be_next); iClear "Hmem".
-          iDestruct "HSweepRest" as "(HPrange & %Hpers & #Hread_cond & Hcls_src)".
-          iDestruct "HPrange" as "#HPrange".
- -
-          iMod (region_valid_alloc _ bsrc esrc asrc (vsrc +1) lws psrc
-                 with "[HPrange] [Hrange']")
-            as "#Hinterp_src_next".
-          { destruct psrc ; cbn in * ; try congruence; done. }
-          { iDestruct (big_sepL2_const_sepL_r _ lws with "[Hread_cond]") as "Hread_PSRC".
-            iSplit ; last iFrame "Hread_cond".
-            by rewrite Hlen_lws.
-            cbn.
-            iDestruct ( big_sepL2_sep_sepL_r with "[$Hread_cond $HPrange]") as "HPs".
-            iClear "IH Hinv Hinva Hreg Hread Hwrite Hread_PSRC HPrange".
-            iDestruct (big_sepL2_alt with "HPs") as "[_ HPs']".
-            iAssert (
-                (∀ (k : nat) (x0 : leibnizO LWord * D),
-                   ⌜zip lws Ps !! k = Some x0⌝
-                   → x0.2 x0.1 ∗ □ (∀ lw0 : LWord, x0.2 lw0 -∗ fixpoint interp1 lw0) -∗ interp x0.1)
-              )%I as "bla".
-            { iIntros (? ? ?) "[Ha Hpa]"; by iDestruct ("Hpa" with "Ha") as "?". }
-            iDestruct (big_sepL_impl _ (fun _ xy => interp xy.1) with "HPs' bla"
-                      ) as "blaa".
-            iDestruct (big_sepL2_alt (fun _ lw _ => interp lw) lws Ps with "[$blaa]") as "blaaa".
-            by rewrite Hlen_lws.
-            by iDestruct (big_sepL2_const_sepL_l (fun _ lw => interp lw) lws Ps with "blaaa") as "[? ?]".
-          }
-          { iClear "#". clear -Hlen_Ps Hlen_lws.
-            iApply big_sepL2_alt.
-            iSplit; first (iPureIntro; rewrite map_length; lia).
-            iDestruct (big_sepM_list_to_map with "Hrange'") as "?" ; last iFrame.
-            rewrite fst_zip; first (apply NoDup_logical_region).
-            rewrite /logical_region map_length ; lia.
-          }
-
-          iMod ("Hcls_src" with "[Hrange HPrange]") as "_".
-          {
-            iNext.
-            iApply region_inv_construct; auto.
+          destruct (decide (r1 = src)) as [ |Hr1_src]
+          ; simplify_map_eq; first (rewrite !fixpoint_interp1_eq //=).
+          iApply "Hreg"; eauto.
+        }
+        { rewrite !fixpoint_interp1_eq //= ; destruct p_pc'; destruct Hp ; try done. }
+      - destruct Hdecide as [ [Hsrc_lregs Hread_src] Hwf].
+        destruct (decide (src = PC)) as [->|Hsrc_neq_pc]
+        ; [clear Hwf | destruct Hwf ; simplify_eq]
+        ; simplify_map_eq
+        ; do 2 (rewrite (insert_commute _ _ PC) //); rewrite !insert_insert.
+        + (* src = PC *)
+          iApply ("IH" $! (<[dst := LInt 1]> lregs) with "[%] [] [Hmap] [$Hown]")
+          ; eauto.
+          { intro; by repeat (rewrite lookup_insert_is_Some'; right). }
+          { iIntros (r1 lw1 Hr1 Hlw1).
+            destruct (decide (r1 = dst)) as [ |Hr1_dst]
+            ; simplify_map_eq; first (rewrite !fixpoint_interp1_eq //=).
+            iApply "Hreg"; eauto.
          }
-          iModIntro.
-          iMod ("Hcls" with "[Ha_pc HP]") as "_"; first (iNext ; iExists _ ; iFrame).
-          iModIntro.
- -
-          iApply wp_pure_step_later; auto.
-          iNext; iIntros "_".
-          simplify_map_eq.
-          iApply ("IH" $! (<[dst := _]> (<[ src := _ ]> lregs)) with "[%] [] [Hmap] [$Hown]")
+          { rewrite !fixpoint_interp1_eq //= ; destruct p_pc'; destruct Hp ; try done. }
+        + (* src ≠ PC *)
+          iApply ("IH" $! (<[dst := LInt 1]> ( <[src := _ ]> lregs)) with "[%] [] [Hmap] [$Hown]")
          ; eauto.
          { intro; by repeat (rewrite lookup_insert_is_Some'; right). }
          { iIntros (r1 lw1 Hr1 Hlw1).
            destruct (decide (r1 = dst)) as [ |Hr1_dst]
            ; simplify_map_eq; first (rewrite !fixpoint_interp1_eq //=).
            destruct (decide (r1 = src)) as [ |Hr1_src]
-            ; simplify_map_eq; first done.
-            iApply "Hreg"; eauto. }
-          { rewrite !fixpoint_interp1_eq //= ; destruct p_pc'; destruct Hp ; done. }
+            ; simplify_map_eq; first (rewrite !fixpoint_interp1_eq //=).
+            iApply "Hreg"; eauto.
+          }
+          { rewrite !fixpoint_interp1_eq //= ; destruct p_pc'; destruct Hp ; try done. }
    }
-
-
-
-
    { (* Sweep false  *)

      iMod (mem_map_recover_res_noup with "HSweepMem Hmem") as "Ha"; auto.
      subst E.
      iModIntro.
-      iMod ("Hcls" with "[Ha HP]") as "_"; [iNext; iExists lwpc ; iFrame|iModIntro].
+      iMod ("Hcls" with "[Ha HP]") as "_"; [iNext; iExists lwpc ; iFrame|iModIntro]; auto.
      iApply wp_pure_step_later; auto.
      iNext; iIntros "_".
      incrementLPC_inv; simplify_map_eq.
@@ -875,7 +908,7 @@

cap_machine.ftlr.IsUnique

      iMod (mem_map_recover_res_noup with "HSweepMem Hmem") as "Ha"; auto.
      subst E.
      iModIntro.
-      iMod ("Hcls" with "[Ha HP]") as "_"; [iNext; iExists lwpc ; iFrame|iModIntro].
+      iMod ("Hcls" with "[Ha HP]") as "_"; [iNext; iExists lwpc ; iFrame|iModIntro]; auto.
      iApply wp_pure_step_later; auto.
      iNext; iIntros "_".
      incrementLPC_inv; simplify_map_eq.
@@ -898,8 +931,7 @@

cap_machine.ftlr.IsUnique

      iMod (mem_map_recover_res_noup with "HSweepMem Hmem") as "Ha"; auto.
      subst E.
      iModIntro.
-      iMod ("Hcls" with "[Ha HP]") as "_".
-      iNext; iExists lwpc ; iFrame.
+      iMod ("Hcls" with "[Ha HP]") as "_"; auto.
      iModIntro.
      iApply wp_pure_step_later; auto.
      iNext; iIntros "_"; iApply wp_value; auto.
diff --git a/branch/june/attestation_refactor_ftlr/indexpage.html b/branch/june/attestation_refactor_ftlr/indexpage.html index 83ad0608..180a7d1b 100644 --- a/branch/june/attestation_refactor_ftlr/indexpage.html +++ b/branch/june/attestation_refactor_ftlr/indexpage.html @@ -56,7 +56,7 @@ Z _ other -(2298 entries) +(2301 entries) Notation Index @@ -216,7 +216,7 @@ Z _ other -(943 entries) +(945 entries) Constructor Index @@ -315,6 +315,38 @@ (47 entries) +Instance Index +A +B +C +D +E +F +G +H +I +J +K +L +M +N +O +P +Q +R +S +T +U +V +W +X +Y +Z +_ +other +(142 entries) + + Section Index A B @@ -347,38 +379,6 @@ (62 entries) -Instance Index -A -B -C -D -E -F -G -H -I -J -K -L -M -N -O -P -Q -R -S -T -U -V -W -X -Y -Z -_ -other -(141 entries) - - Abbreviation Index A B @@ -667,6 +667,7 @@

Global Index

compute_mask_union [lemma, in cap_machine.logrel]
compute_mask_difference [lemma, in cap_machine.logrel]
compute_mask [definition, in cap_machine.logrel]
+cond_open_contra [lemma, in cap_machine.ftlr.IsUnique]
Conf [definition, in cap_machine.cap_lang]
ConfFlag [inductive, in cap_machine.cap_lang]
ConfFlag_sind [definition, in cap_machine.cap_lang]
@@ -1163,6 +1164,7 @@

Global Index

head_ctx_step_val [lemma, in cap_machine.cap_lang]
helpers [section, in cap_machine.proofmode.tactics_helpers]


I

+if_Persistent [instance, in cap_machine.ftlr.IsUnique]
if_Persistent [instance, in cap_machine.ftlr.Load]
if_persistent [instance, in cap_machine.ftlr.interp_weakening]
IH [definition, in cap_machine.ftlr.interp_weakening]
@@ -1674,6 +1676,7 @@

Global Index

memMap_resource_1 [lemma, in cap_machine.rules.rules_base]
memMap_resource_0 [lemma, in cap_machine.rules.rules_base]
MemNum [definition, in cap_machine.addr_reg]
+mem_map_recover_res_upd [lemma, in cap_machine.ftlr.IsUnique]
mem_map_recover_res_noup [lemma, in cap_machine.ftlr.IsUnique]
mem_map_implies_pure_conds [lemma, in cap_machine.ftlr.IsUnique]
mem_map_recover_res [lemma, in cap_machine.ftlr.Load]
@@ -3052,6 +3055,7 @@

Lemma Index

compute_mask_mono [in cap_machine.logrel]
compute_mask_union [in cap_machine.logrel]
compute_mask_difference [in cap_machine.logrel]
+cond_open_contra [in cap_machine.ftlr.IsUnique]
ContiguousRegion_InCtx [in machine_utils.solve_pure]
contiguous_betweenL_program_split [in cap_machine.proofmode.contiguous]
contiguous_betweenL_contiguous_between [in cap_machine.proofmode.contiguous]
@@ -3477,6 +3481,7 @@

Lemma Index

memMap_resource_1_dq [in cap_machine.rules.rules_base]
memMap_resource_1 [in cap_machine.rules.rules_base]
memMap_resource_0 [in cap_machine.rules.rules_base]
+mem_map_recover_res_upd [in cap_machine.ftlr.IsUnique]
mem_map_recover_res_noup [in cap_machine.ftlr.IsUnique]
mem_map_implies_pure_conds [in cap_machine.ftlr.IsUnique]
mem_map_recover_res [in cap_machine.ftlr.Load]
@@ -4260,84 +4265,6 @@

Projection Index

SG_storedPreds [in cap_machine.seal_store]
SG_sealStore [in cap_machine.seal_store]


-

Section Index

-

A

-Assert [in cap_machine.examples.assert]
-

C

-cap_lang_rules [in cap_machine.rules.rules_IsUnique]
-cap_lang_rules [in cap_machine.rules.rules_Jnz]
-cap_lang_rules [in cap_machine.rules.rules_Subseg]
-cap_lang_rules [in cap_machine.rules.rules_Store]
-cap_lang_rules [in cap_machine.rules.rules_Lea]
-cap_lang_rules [in cap_machine.rules.rules_EStoreId]
-cap_lang_rules [in cap_machine.rules.rules_Seal]
-cap_lang_rules [in cap_machine.rules.rules_EInit]
-cap_lang_rules [in cap_machine.rules.rules_UnSeal]
-cap_lang_rules_opt [in cap_machine.rules.rules_base]
-cap_lang_rules [in cap_machine.rules.rules_base]
-cap_lang_rules [in cap_machine.rules.rules_Jmp]
-cap_lang_rules [in cap_machine.rules.rules_EDeInit]
-cap_lang_rules [in cap_machine.rules.rules_Mov]
-cap_lang_rules [in cap_machine.rules.rules_Load]
-cap_lang_rules [in cap_machine.rules.rules_AddSubLt]
-cap_lang_rules [in cap_machine.rules.rules_Restrict]
-cap_lang_rules [in cap_machine.rules.rules_Get]
-codefrag [in cap_machine.proofmode.region]
-codefrag [in cap_machine.proofmode.proofmode]
-codefrag_subblock [in cap_machine.proofmode.proofmode]
-Contiguous [in cap_machine.proofmode.contiguous]
-ContiguousL [in cap_machine.proofmode.contiguous]
-

D

-denote_domain [in cap_machine.proofmode.register_tactics]
-disjoint_list [in cap_machine.proofmode.disjoint_regions_tactics]
-

F

-finz_lemmas [in machine_utils.finz_base]
-finz.finz [in machine_utils.finz_base]
-fundamental [in cap_machine.ftlr.IsUnique]
-fundamental [in cap_machine.ftlr.Lea]
-fundamental [in cap_machine.ftlr.AddSubLt]
-fundamental [in cap_machine.ftlr.Load]
-fundamental [in cap_machine.ftlr.UnSeal]
-fundamental [in cap_machine.ftlr.Store]
-fundamental [in cap_machine.ftlr.Restrict]
-fundamental [in cap_machine.ftlr.Subseg]
-fundamental [in cap_machine.ftlr.interp_weakening]
-fundamental [in cap_machine.ftlr.ftlr_base]
-fundamental [in cap_machine.ftlr.Seal]
-fundamental [in cap_machine.ftlr.Mov]
-fundamental [in cap_machine.fundamental]
-fundamental [in cap_machine.ftlr.Jmp]
-fundamental [in cap_machine.ftlr.Get]
-fundamental [in cap_machine.ftlr.Jnz]
-

H

-helpers [in cap_machine.proofmode.tactics_helpers]
-

I

-instr_encodings [in cap_machine.examples.addr_reg_sample]
-

L

-lemmas [in machine_utils.finz_interval]
-Linking [in cap_machine.linking]
-logrel [in cap_machine.logrel]
-

M

-machine_param [in cap_machine.logical_mapsto]
-macros [in cap_machine.examples.macros]
-macros [in cap_machine.examples.macros_new]
-monotone [in cap_machine.monotone]
-

N

-named [in cap_machine.proofmode.NamedProp]
-

O

-opsem [in cap_machine.cap_lang]
-

R

-region [in cap_machine.proofmode.region]
-

S

-SimpleMalloc [in cap_machine.examples.malloc]
-SimpleSalloc [in cap_machine.examples.salloc]
-simpl_gmap [in cap_machine.proofmode.map_simpl]
-Store [in cap_machine.seal_store]
-

T

-tests.tests [in cap_machine.proofmode.NamedProp]
-

W

-word_type_encoding [in cap_machine.machine_parameters]
-

Instance Index

A

addr_inhabited [in cap_machine.machine_base]
@@ -4384,6 +4311,7 @@

Instance Index



H

hasValidAddress_dec [in cap_machine.logrel]


I

+if_Persistent [in cap_machine.ftlr.IsUnique]
if_Persistent [in cap_machine.ftlr.Load]
if_persistent [in cap_machine.ftlr.interp_weakening]
IncrFinZ_InCtx [in machine_utils.solve_pure]
@@ -4498,6 +4426,84 @@

Instance Index



Z

ZToFinZ_z_of [in machine_utils.class_instances]


+

Section Index

+

A

+Assert [in cap_machine.examples.assert]
+

C

+cap_lang_rules [in cap_machine.rules.rules_IsUnique]
+cap_lang_rules [in cap_machine.rules.rules_Jnz]
+cap_lang_rules [in cap_machine.rules.rules_Subseg]
+cap_lang_rules [in cap_machine.rules.rules_Store]
+cap_lang_rules [in cap_machine.rules.rules_Lea]
+cap_lang_rules [in cap_machine.rules.rules_EStoreId]
+cap_lang_rules [in cap_machine.rules.rules_Seal]
+cap_lang_rules [in cap_machine.rules.rules_EInit]
+cap_lang_rules [in cap_machine.rules.rules_UnSeal]
+cap_lang_rules_opt [in cap_machine.rules.rules_base]
+cap_lang_rules [in cap_machine.rules.rules_base]
+cap_lang_rules [in cap_machine.rules.rules_Jmp]
+cap_lang_rules [in cap_machine.rules.rules_EDeInit]
+cap_lang_rules [in cap_machine.rules.rules_Mov]
+cap_lang_rules [in cap_machine.rules.rules_Load]
+cap_lang_rules [in cap_machine.rules.rules_AddSubLt]
+cap_lang_rules [in cap_machine.rules.rules_Restrict]
+cap_lang_rules [in cap_machine.rules.rules_Get]
+codefrag [in cap_machine.proofmode.region]
+codefrag [in cap_machine.proofmode.proofmode]
+codefrag_subblock [in cap_machine.proofmode.proofmode]
+Contiguous [in cap_machine.proofmode.contiguous]
+ContiguousL [in cap_machine.proofmode.contiguous]
+

D

+denote_domain [in cap_machine.proofmode.register_tactics]
+disjoint_list [in cap_machine.proofmode.disjoint_regions_tactics]
+

F

+finz_lemmas [in machine_utils.finz_base]
+finz.finz [in machine_utils.finz_base]
+fundamental [in cap_machine.ftlr.IsUnique]
+fundamental [in cap_machine.ftlr.Lea]
+fundamental [in cap_machine.ftlr.AddSubLt]
+fundamental [in cap_machine.ftlr.Load]
+fundamental [in cap_machine.ftlr.UnSeal]
+fundamental [in cap_machine.ftlr.Store]
+fundamental [in cap_machine.ftlr.Restrict]
+fundamental [in cap_machine.ftlr.Subseg]
+fundamental [in cap_machine.ftlr.interp_weakening]
+fundamental [in cap_machine.ftlr.ftlr_base]
+fundamental [in cap_machine.ftlr.Seal]
+fundamental [in cap_machine.ftlr.Mov]
+fundamental [in cap_machine.fundamental]
+fundamental [in cap_machine.ftlr.Jmp]
+fundamental [in cap_machine.ftlr.Get]
+fundamental [in cap_machine.ftlr.Jnz]
+

H

+helpers [in cap_machine.proofmode.tactics_helpers]
+

I

+instr_encodings [in cap_machine.examples.addr_reg_sample]
+

L

+lemmas [in machine_utils.finz_interval]
+Linking [in cap_machine.linking]
+logrel [in cap_machine.logrel]
+

M

+machine_param [in cap_machine.logical_mapsto]
+macros [in cap_machine.examples.macros]
+macros [in cap_machine.examples.macros_new]
+monotone [in cap_machine.monotone]
+

N

+named [in cap_machine.proofmode.NamedProp]
+

O

+opsem [in cap_machine.cap_lang]
+

R

+region [in cap_machine.proofmode.region]
+

S

+SimpleMalloc [in cap_machine.examples.malloc]
+SimpleSalloc [in cap_machine.examples.salloc]
+simpl_gmap [in cap_machine.proofmode.map_simpl]
+Store [in cap_machine.seal_store]
+

T

+tests.tests [in cap_machine.proofmode.NamedProp]
+

W

+word_type_encoding [in cap_machine.machine_parameters]
+

Abbreviation Index

A

Addr [in cap_machine.addr_reg]
@@ -5316,7 +5322,7 @@

Record Index

Z _ other -(2298 entries) +(2301 entries) Notation Index @@ -5476,7 +5482,7 @@

Record Index

Z _ other -(943 entries) +(945 entries) Constructor Index @@ -5575,6 +5581,38 @@

Record Index

(47 entries) +Instance Index +A +B +C +D +E +F +G +H +I +J +K +L +M +N +O +P +Q +R +S +T +U +V +W +X +Y +Z +_ +other +(142 entries) + + Section Index A B @@ -5607,38 +5645,6 @@

Record Index

(62 entries) -Instance Index -A -B -C -D -E -F -G -H -I -J -K -L -M -N -O -P -Q -R -S -T -U -V -W -X -Y -Z -_ -other -(141 entries) - - Abbreviation Index A B