From bfcbbc60273f78ad6b8fe4fd5cb101e21f5fbf49 Mon Sep 17 00:00:00 2001
From: June Rousseau <june.rousseau@cs.au.dk>
Date: Tue, 7 Jan 2025 12:45:53 +0100
Subject: [PATCH] Squashed commit of the following: WIP trusted compute enclave

commit b899cd2b0898aad6d75add394b52345cb7928a9a
Author: June Rousseau <june.rousseau@cs.au.dk>
Date:   Wed Dec 25 22:56:06 2024 +0100

    WIP setup for custom enclave contract

commit 40b7568fea37220cd83fefc6854fd61969b50bc8
Author: June Rousseau <june.rousseau@cs.au.dk>
Date:   Tue Dec 24 11:25:29 2024 +0100

    WIP proof TC example: setup for custom enclave predicates

commit 731e84bca3441042f19c9e827371b821a64245ff
Author: June Rousseau <june.rousseau@cs.au.dk>
Date:   Tue Dec 24 02:50:31 2024 +0100

    WIP proof TC example

commit c4c3755a9a603e9b7ff65270e7882dc8fd62d57b
Author: June Rousseau <june.rousseau@cs.au.dk>
Date:   Tue Dec 24 02:50:10 2024 +0100

    New WP rule for UnSeal

commit 8a5b904a1874cd16ec2311bf6e088d52028abfbb
Author: June Rousseau <june.rousseau@cs.au.dk>
Date:   Tue Dec 24 02:50:01 2024 +0100

    Generalise spec macros

commit b57a5d2cf846129967805dfb26bb602dbcbefac4
Author: June Rousseau <june.rousseau@cs.au.dk>
Date:   Mon Dec 23 21:47:14 2024 +0100

    WIP proof callback trusted compute example

commit 0292d5b0be1a52a5df0c52915d0f1fc68f6ab7b5
Author: June Rousseau <june.rousseau@cs.au.dk>
Date:   Mon Dec 23 21:46:35 2024 +0100

    Fix code trusted compute example

commit 7836df21a84699433ddbd45f7135b8b57633a8b8
Author: June Rousseau <june.rousseau@cs.au.dk>
Date:   Mon Dec 23 18:04:49 2024 +0100

    Simplification WP rule is_unique
---
 theories/examples/enclaves/trusted_compute.v | 433 +++++++++++++++----
 theories/examples/macros_new.v               | 128 +++---
 theories/logical_mapsto.v                    |  27 ++
 theories/rules/rules_IsUnique.v              |   9 +-
 theories/rules/rules_UnSeal.v                |  24 +
 5 files changed, 461 insertions(+), 160 deletions(-)

diff --git a/theories/examples/enclaves/trusted_compute.v b/theories/examples/enclaves/trusted_compute.v
index 78fd3431..0fe6929a 100644
--- a/theories/examples/enclaves/trusted_compute.v
+++ b/theories/examples/enclaves/trusted_compute.v
@@ -7,15 +7,90 @@ From cap_machine Require Import proofmode.
 From cap_machine Require Import macros_new.
 Open Scope Z_scope.
 
+(* This section redefines useful definitions from `arch_sealing` along with further explanations. *)
+Section invariants.
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealsg: sealStoreG Σ}
+          {nainv: logrel_na_invs Σ} `{MP: MachineParameters}.
+
+  (* `seal_pred` denotes that the sealed satisfies a predicate `Φ`, for a specific `τ` OType. *)
+  (* Note: `seal_pred` does not need to be put inside an invariant, because it is `Persistent`. *)
+  (* Definition seal_pred τ Φ {Hpers : ∀ w, Persistent (Φ w)} := seal_store.seal_pred τ Φ. *)
+
+  (* Note: `arch_sealing.seal_state` is the combination of `seal_pred` and a invariant. *)
+  (* > This invariant pins `WSealRange` in memory to retrieve an access to it. *)
+  (* For simplicity, `WSealRange` will be easily accessible (hidden in front of our instructions). *)
+
+  (* Fact that the value `w`, if `interp w`, has been validly sealed satisfying a `Φ` predicate. *)
+  Definition valid_sealed w o (Φ : LWord -> iProp Σ) :=
+    (∃ sb, ⌜w = LWSealed o sb⌝ ∗  ⌜∀ w : leibnizO LWord, Persistent (Φ w)⌝
+                                                         ∗ seal_pred o Φ ∗ Φ (LWSealable sb))%I.
+
+  (* Lemma: If something is sealed, it is sufficient to know that the sealed satisfies a predicate `Φ`. *)
+  Lemma interp_valid_sealed sb o:
+    interp (LWSealed o sb) -∗ ∃ Φ, ▷ valid_sealed (LWSealed o sb) o Φ.
+  Proof.
+    iIntros "Hsl /=". rewrite fixpoint_interp1_eq /= /valid_sealed.
+    iDestruct "Hsl" as (P) "(%Hpers & Hpred & HP)".
+    iExists P, sb; repeat iSplit; [auto | auto | iFrame.. ].
+  Qed.
+
+  (* Lemma: Concludes that `Φ ≡ Φ'` if `seal_pred τ Φ` and `valid_sealed w τ Φ` have the same `τ` OType. *)
+  (* Note: This is a more generic version of `arch_sealing.sealLL_valid_sealed_pred_eq` *)
+  Lemma seal_pred_valid_sealed_eq τ w Φ Φ' {Hpers : ∀ w, Persistent (Φ w)} :
+    seal_pred τ Φ -∗ valid_sealed w τ Φ' -∗ (∀ w, ▷ (Φ w ≡ Φ' w)).
+  Proof.
+    iIntros "Hsp Hvs".
+    iDestruct "Hvs" as (sb) "(_ & _ & Hsp' & _)".
+    iApply (seal_pred_agree with "Hsp Hsp'").
+  Qed.
+
+End invariants.
+
+(* The proof guideline for accessing the sealed predicate is as follows: *)
+
+(* We assume: *)
+(*  - `seal_pred τ φ`, for some known `φ` (e.g: `sealed_cap`) *)
+(*  - `interp w`, where `w = WSealed τ scap` for any given `scap` *)
+
+(* 1. Using `interp_valid_sealed`, we can get `▷ valid_sealed (WSealed τ scap) τ Φ`. *)
+(* 2. `Φ` is currently unknown, we have to use `seal_pred_valid_sealed_eq` to retrieve `φ`. *)
+
+Section invariants_cap.
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealsg: sealStoreG Σ}
+          {nainv: logrel_na_invs Σ} `{MP: MachineParameters}.
+
+
+  Definition seal_capN : namespace := nroot .@ "seal_cap".
+
+  (* `sealed_cap` is the sealed predicate of a sealed buffer containing a capability. *)
+  (* The capability must be `interp`. *)
+  Program Definition f42 : Addr := (finz.FinZ 42 eq_refl eq_refl).
+  Definition sealed_42 : LWord → iProp Σ :=
+    λ w, (∃ b e v, ⌜w = LCap O b e f42 v⌝)%I.
+
+
+  (* Note: `sealed_cap` is not `Timeless` because of the use of the non-atomic invariant. *)
+  (* > In our case, any later can be stripped at time. *)
+  (* One could use `a_cap ↦ₐ{DFracDiscarded} w` to avoid using the non-atomic invariant. *)
+  (* > However, this denies the right to write to `a_cap` making it read-only. *)
+
+  (* Required by `seal_pred`: `sealed_cap` is `Persistent`. *)
+  Instance sealed_42_persistent w : Persistent (sealed_42 w).
+  Proof. apply _. Qed.
+
+  (* Capability-specific redefinitions *)
+  Definition seal_pred_42 τ := seal_pred τ sealed_42.
+  Definition valid_sealed_cap w τ := valid_sealed w τ sealed_42.
+
+End invariants_cap.
+
+
 Section trusted_compute_example.
   Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealsg : sealStoreG Σ} `{MP: MachineParameters}.
 
   (* Data part, following the directly the main code *)
   Definition trusted_compute_data (linking_table_cap : LWord) : list LWord :=
-    [
-      linking_table_cap ;
-      (LWInt 0%Z) (* placeholder for storing identity of the enclave *)
-    ].
+    [ linking_table_cap ].
 
   (* Expect:
      - PC := (RWX, main, main_end, main)
@@ -30,21 +105,14 @@ Section trusted_compute_example.
         Lea r_t1 (callback - main)%Z;       (* rt1 := (RWX, main, main_end, callback) *)
         Restrict r_t1 (encodePerm E);       (* rt1 := (E, main, main_end, callback) *)
 
-        (* Store writable capability into data*)
-        Lea r_t2 (data - main)%Z;           (* rt2 := (RWX, main, main_end, data) *)
-        Mov r_t3 r_t2;                      (* rt3 := (RWX, main, main_end, data) *)
-        Lea r_t3 1%Z;                       (* rt3 := (RWX, main, main_end, data + 1) *)
-        Store r_t3 r_t2;                    (* mem[data + 1] := (RWX, main, main_end, data) *)
-
         (* Jump to adversary *)
         Mov r_t2 0;
-        Mov r_t3 0;
         Jmp r_t0
       ].
 
   (* Expect PC := (RWX, main, main_end, callback) *)
   Definition trusted_compute_main_code_callback0
-    (callback fails data : Z)
+    (callback fails : Z)
     (hash_enclave : Z)
     (assert_lt_offset : Z)
     : list LWord :=
@@ -55,12 +123,6 @@ Section trusted_compute_example.
         Mov r_t4 r_t3 ;               (* r_t4 :=  (RX, main, main_end, callback) *)
         Lea r_t3 (fails-callback)%Z;  (* r_t3 :=  (RX, main, main_end, fails) *)
 
-        (* get a writable capability for storing identity *)
-        Lea r_t4 (data + 1 - callback)%Z; (* r_t4 := (RX, main, main_end, data + 1) *)
-        Load r_t4 r_t4;                   (* r_t4 := (RWX, main, main_end, data) *)
-        Load r_t5 r_t4 ;                  (* r_t5 := (RO, b_lt, e_lt, b_lt) *)
-        Lea r_t4 1;                       (* r_t4 := (RWX, main, main_end, data + 1) *)
-
         (* sanity check: w_res is a sealed capability *)
         GetOType r_t2 r_t0;
         Sub r_t2 r_t2 (-1)%Z;
@@ -69,33 +131,31 @@ Section trusted_compute_example.
         Jnz r_t5 r_t2;
         Jmp r_t3;
 
-        (* check otype(w_res) against identity of the enclave *)
+        (*  attestation *)
         GetOType r_t2 r_t0;
-        EStoreId r_t2 r_t2 r_t4;
-        Sub r_t2 r_t2 1;
-        Jnz r_t3 r_t2;
-        Load r_t4 r_t4;
+        EStoreId r_t4 r_t2;
+        (* check otype(w_res) against identity of the enclave *)
         Sub r_t4 r_t4 hash_enclave;
-        Mov r_t5 PC ;
-        Lea r_t5 4 ;
-        Jnz r_t5 r_t4;
-        Jmp r_t3;
+        Jnz r_t3 r_t4;
 
         (* get returned value and assert it to be 42 *)
-        UnSeal r_t0 r_t0 r_t1;
-        Mov r_t1 r_t5;
-        GetA r_t4 r_t0;
-        Mov r_t5 42%Z
+        UnSeal r_t1 r_t1 r_t0;
+        Mov r_t0 r_t5;
+        GetA r_t4 r_t1;
+        Mov r_t5 42%Z;
+        Mov r_t1 r_t3%Z;
+        Lea r_t1 1;
+        Load r_t1 r_t1
       ]
       ++ assert_reg_instrs assert_lt_offset r_t1
-      ++ encodeInstrsLW [Halt]
+      ++ encodeInstrsLW [Mov r_t0 0 ; Mov r_t3 0 ; Halt]
       ++ (* fails: *) encodeInstrsLW [Fail].
 
   Definition trusted_compute_main_init_len : Z :=
     Eval cbv in (length (trusted_compute_main_code_init0 0%Z 0%Z 0%Z)).
 
   Definition trusted_compute_main_callback_len : Z :=
-    Eval cbv in (length (trusted_compute_main_code_callback0 0%Z 0%Z 0%Z 0%Z 0%Z)).
+    Eval cbv in (length (trusted_compute_main_code_callback0 0%Z 0%Z 0%Z 0%Z)).
 
   Definition trusted_compute_main_data_len : Z :=
     Eval cbv in (length (trusted_compute_data (LInt 0%Z))).
@@ -133,7 +193,7 @@ Section trusted_compute_example.
     let data     := trusted_compute_main_init_len + trusted_compute_main_callback_len in
     let fails    := (data - 1)%Z in
     (trusted_compute_main_code_init0 init callback data) ++
-    (trusted_compute_main_code_callback0 callback fails data hash_trusted_compute_enclave assert_lt_offset).
+    (trusted_compute_main_code_callback0 callback fails hash_trusted_compute_enclave assert_lt_offset).
 
   Definition trusted_compute_main_code_len : Z :=
     Eval cbv in trusted_compute_main_init_len + trusted_compute_main_callback_len.
@@ -144,10 +204,10 @@ Section trusted_compute_example.
 
   (** Specification init code *)
   Lemma trusted_compute_main_init_spec
-    (b_main adv adv_end: Addr)
+    (b_main : Addr)
     (pc_v adv_v : Version)
     (assert_lt_offset : Z)
-    (w0 w1 w2 w3 w4 : LWord)
+    (w0 w1 w2 w3 w4 wadv : LWord)
     φ :
 
     let e_main := (b_main ^+ trusted_compute_main_len)%a in
@@ -158,21 +218,17 @@ Section trusted_compute_example.
     ContiguousRegion b_main trusted_compute_main_len ->
     ⊢ ((
           codefrag b_main pc_v trusted_compute_main
-          ∗ ((a_data ^+ 1)%a, pc_v) ↦ₐ (LWInt 0%Z)
 
           ∗ PC ↦ᵣ LCap RWX b_main e_main b_main pc_v
-          ∗ r_t0 ↦ᵣ LCap RWX adv adv_end adv adv_v
+          ∗ r_t0 ↦ᵣ wadv
           ∗ r_t1 ↦ᵣ w1
           ∗ r_t2 ↦ᵣ w2
-          ∗ r_t3 ↦ᵣ w3
           (* NOTE this post-condition stops after jumping to the adversary *)
           ∗ ▷ ( codefrag b_main pc_v trusted_compute_main
-                ∗ ((a_data ^+ 1)%a, pc_v) ↦ₐ (LCap RWX b_main e_main a_data pc_v)
-                ∗ PC ↦ᵣ (LCap RWX adv adv_end adv adv_v)
-                ∗ r_t0 ↦ᵣ (LCap RWX adv adv_end adv adv_v)
+                ∗ PC ↦ᵣ updatePcPermL wadv
+                ∗ r_t0 ↦ᵣ wadv
                 ∗ r_t1 ↦ᵣ (LCap E b_main e_main a_callback pc_v)
                 ∗ r_t2 ↦ᵣ LInt 0
-                ∗ r_t3 ↦ᵣ LInt 0
                   -∗ WP Seq (Instr Executable) {{ φ }}))
          -∗ WP Seq (Instr Executable) {{ λ v, φ v ∨ ⌜v = FailedV⌝ }})%I.
   Proof.
@@ -188,23 +244,19 @@ Section trusted_compute_example.
           /trusted_compute_main_init_len /trusted_compute_main_callback_len
       ; solve_addr.
 
-    intros * Hregion.
-    iIntros "(Hcode & Hdata & HPC & Hr0 & Hr1 & Hr2 & Hr3 & Hφ)".
+    intros ???? Hregion.
+    iIntros "(Hcode & HPC & Hr0 & Hr1 & Hr2 & Hφ)".
     codefrag_facts "Hcode".
     iGo "Hcode".
     rewrite decode_encode_perm_inv; by cbn.
     rewrite decode_encode_perm_inv.
     iGo "Hcode".
-    (* FIXME: not sure why I need to rewrite this *)
-    replace (a_data ^+ 1)%a with (b_main ^+ 50)%a by solve_addr'.
-    iGo "Hcode".
     iApply (wp_wand with "[-]"); last (iIntros (v) "H"; by iLeft).
     iApply "Hφ".
     iFrame.
   Qed.
 
   (** Specification callback code *)
-  (** ------ TODO ------ *)
 
   Context {nainv: logrel_na_invs Σ} .
   (* Define all the invariants *)
@@ -213,13 +265,9 @@ Section trusted_compute_example.
   (* Linking table invariant *)
   Definition link_tableN := (trusted_computeN.@"link_table").
   Definition link_table_inv
-    (* table_addr v_table_addr *)
-    (* b_link e_link a_link v_link *)
     v_link
     assert_entry b_assert e_assert v_assert :=
     na_inv logrel_nais link_tableN
-      (* ((table_addr, v_table_addr) ↦ₐ LCap RO b_link e_link a_link v_link *)
-       (* ∗ *)
          ((assert_entry, v_link) ↦ₐ LCap E b_assert e_assert b_assert v_assert)%I.
 
   (* Assert invariant *)
@@ -229,7 +277,122 @@ Section trusted_compute_example.
 
   Definition flag_assertN := (trusted_computeN.@"flag_assert").
   Definition flag_inv a_flag v_flag :=
-    inv flag_assertN ((a_flag,v_flag) ↦ₐ LInt 0%Z) .
+    inv flag_assertN ((a_flag,v_flag) ↦ₐ LInt 0%Z).
+
+  (* TODO: move somewhere else, this is not specific to trusted compute *)
+  Record CustomEnclave :=
+    MkCustomEnclave {
+        code : list LWord;
+        code_region : Addr;
+        Penc : LWord -> iProp Σ;
+        Psign : LWord -> iProp Σ;
+      }.
+
+  Definition custom_enclaves_map : Type :=
+    gmap EIdentity CustomEnclave.
+
+  Definition custom_enclaves_map_wf (cenclaves : custom_enclaves_map) :=
+    map_Forall
+      (fun I ce => I = hash_concat (hash (code_region ce)) (hash (code ce)))
+      cenclaves.
+
+  Definition custom_enclaveN := (trusted_computeN.@"custom_enclave").
+  Definition custom_enclave_inv (cenclaves : custom_enclaves_map) :=
+    inv custom_enclaveN
+      (
+        ⌜ custom_enclaves_map_wf cenclaves ⌝ -∗
+        □ ∀ (I : EIdentity) (tid : TIndex) (ot : OType) (ce : CustomEnclave),
+          enclave_all tid I
+          ∗ ⌜ cenclaves !! I = Some ce ⌝
+          ∗ ⌜ has_seal ot tid ⌝ -∗
+          seal_pred ot (Penc ce)
+          ∗ seal_pred (ot ^+ 1)%ot (Psign ce)
+      ).
+
+  (* Trusted Compute Custom Predicates *)
+  Definition tc_enclave_pred tc_data_cap tc_addr : CustomEnclave :=
+   MkCustomEnclave
+     (trusted_compute_enclave_code tc_data_cap)
+     tc_addr
+     sealed_42 (* TODO: should be false ! *)
+     sealed_42.
+
+  Definition tcenclaves_map tc_data_cap tc_addr : custom_enclaves_map :=
+   {[hash_trusted_compute_enclave := tc_enclave_pred tc_data_cap tc_addr]}.
+
+  Definition sealable_to_lsealable (sb : Sealable) (v : Version) :=
+    match sb with
+    | SCap p b e a => LSCap p b e a v
+    | SSealRange p b e a => LSSealRange p b e a
+    end.
+
+  Definition word_to_lword (w : Word) (v : Version) :=
+    match w with
+    | WInt z => LInt z
+    | WSealable sb => LWSealable (sealable_to_lsealable sb v)
+    | WSealed ot sb => LWSealed ot (sealable_to_lsealable sb v)
+    end.
+
+  Definition custom_enclave_contract
+    (cenclaves : custom_enclaves_map)
+    :=
+    forall
+    (I : EIdentity)
+    (b e a : Addr) (v : Version)
+    (b' e' a' : Addr) (v' : Version)
+    (enclave_data : list LWord)
+    (ot : OType)
+    (ce : CustomEnclave),
+    custom_enclaves_map_wf cenclaves ->
+    cenclaves !! I = Some ce ->
+    (code ce) !! 0%nat = Some (LCap RW b' e' a' v') ->
+    enclave_data !! 0%nat = Some (LSealRange (true,true) ot (ot^+1)%ot ot) ->
+    I = hash_concat (hash b) (hash (tail (code ce))) ->
+    b = (code_region ce) ->
+    (* tid_of_otype ot = tid -> *)
+    (* TODO: either points-to in invariant, or upd modality in implication *)
+    na_inv logrel_nais (trusted_computeN.@I)
+      ([[ b , e ]] ↦ₐ{ v } [[ (code ce) ]]  ∗
+       [[ b' , e' ]] ↦ₐ{ v } [[ enclave_data ]])
+    ∗ seal_pred ot (Penc ce)
+    ∗ seal_pred (ot^+1)%ot (Psign ce) -∗
+    (*  TODO either record a in hash ; or always pick (b+1) *)
+    interp (LCap E b e (b^+1)%a v).
+
+
+  Lemma tc_contract tc_data_cap tc_addr :
+    custom_enclave_contract (tcenclaves_map tc_data_cap tc_addr).
+  Proof.
+    rewrite /custom_enclave_contract.
+    iIntros (I b e a v b' e' a' v' enclave_data ot ce
+      Hwf_cemap Hcode_ce Hdatacap Hdata_seal HIhash Hb)
+      "(#Htc_inv & #HPenc & #HPsign)".
+    rewrite /tcenclaves_map in Hwf_cemap,Hcode_ce.
+    rewrite /custom_enclaves_map_wf in Hwf_cemap.
+    rewrite map_Forall_insert in Hwf_cemap; last by simplify_map_eq.
+    destruct Hwf_cemap as [ Hwf_hash _ ].
+    cbn in Hwf_hash.
+    destruct (decide (I = hash_trusted_compute_enclave)) as [->|] ; last by simplify_map_eq.
+    clear HIhash Hwf_hash.
+    rewrite fixpoint_interp1_eq /=.
+    iIntros (lregs); iNext ; iModIntro.
+    iIntros "([%Hfullmap Hinterp_map] & Hrmap & Hna)".
+    simplify_map_eq.
+    rewrite /interp_conf.
+    iMod (na_inv_acc with "Htc_inv Hna") as "(>[Htc_code Htc_data]  & Hna & Hclose)"; [solve_ndisj ..|].
+    rewrite /registers_mapsto.
+    iExtractList "Hrmap" [PC] as ["HPC"].
+
+    (* iAssert (codefrag tc_addr v (trusted_compute_enclave_code (LCap RW b' e' a' v'))) *)
+    (*   with "[Htc_code]" as "Htc_code". *)
+    (* { *)
+    (*   rewrite /codefrag. *)
+    (* } *)
+
+
+
+  Admitted.
+
 
 
   Lemma trusted_compute_callback_code_spec
@@ -240,6 +403,7 @@ Section trusted_compute_example.
     (assert_lt_offset : Z)
     (b_assert e_assert a_flag : Addr) (v_assert : Version) (* assert *)
     (w0 w1 w2 w3 w4 w5 : LWord)
+    tc_data_cap tc_addr
     φ :
 
     let v_link := pc_v in
@@ -254,18 +418,19 @@ Section trusted_compute_example.
 
 
     (a_link + assert_lt_offset)%a = Some assert_entry →
-    (* TODO assume that, between 'main_end' and 'end_adv',
-       there is only integers (for simplicity) *)
-    (* main_end < end_adv -> *)
+    withinBounds b_link e_link assert_entry = true ->
+
+    (* TODO: should be proved *)
+    custom_enclaves_map_wf (tcenclaves_map tc_data_cap tc_addr) ->
 
-    (* TODO not needed for this part of the spec, but will be required for the full proof *)
     (link_table_inv
-       (* link_addr v_link *)
-       (* b_link e_link a_link *)
        v_link
        assert_entry b_assert e_assert v_assert
     ∗ assert_inv b_assert a_flag e_assert v_assert
     ∗ flag_inv a_flag v_assert)
+    ∗ custom_enclave_inv (tcenclaves_map tc_data_cap tc_addr)
+    ∗ interp w1
+    ∗ interp w0
 
     ⊢ ((
           codefrag b_main pc_v trusted_compute_main
@@ -279,19 +444,23 @@ Section trusted_compute_example.
           ∗ r_t3 ↦ᵣ w3
           ∗ r_t4 ↦ᵣ w4
           ∗ r_t5 ↦ᵣ w5
+          ∗ na_own logrel_nais ⊤
+
           (* NOTE this post-condition stops after jumping to the adversary *)
           ∗ ▷ ( codefrag b_main pc_v trusted_compute_main
                 ∗ ((a_data)%a, pc_v) ↦ₐ link_cap
-                ∗ ((a_data ^+ 1)%a, pc_v) ↦ₐ (LWInt 0%Z)
+                ∗ ((a_data ^+ 1)%a, pc_v) ↦ₐ (LCap RWX b_main e_main a_data pc_v)
 
-                ∗ PC ↦ᵣ LCap RWX b_main e_main a_data pc_v
+                ∗ PC ↦ᵣ LCap RX b_main e_main (a_data ^+ (-2))%a pc_v
                 ∗ r_t0 ↦ᵣ LInt 0
                 ∗ r_t1 ↦ᵣ LInt 0
                 ∗ r_t2 ↦ᵣ LInt 0
                 ∗ r_t3 ↦ᵣ LInt 0
                 ∗ r_t4 ↦ᵣ LInt 0
                 ∗ r_t5 ↦ᵣ LInt 0
-                  -∗ WP Seq (Instr Executable) {{ φ }}))
+                ∗ na_own logrel_nais ⊤
+
+                  -∗ WP (Instr Halted) {{ φ }}))
          -∗ WP Seq (Instr Executable) {{ λ v, φ v ∨ ⌜v = FailedV⌝ }})%I.
   Proof.
 
@@ -306,23 +475,15 @@ Section trusted_compute_example.
           /trusted_compute_main_init_len /trusted_compute_main_callback_len
       ; solve_addr.
 
-
-    intros ?????? Hregion Hassert.
-    iIntros "[HlinkInv HassertInv]
-             (Hcode & Hlink_cap & Hdata1 & HPC & Hr0 & Hr1 & Hr2 & Hr3 & Hr4 & Hr5 & Hcont)".
+    intros ?????? Hregion Hassert Hlink Hwf_cemap.
+    iIntros "#[ [HlinkInv [HassertInv HflagInv] ] [ Hcemap_inv [ Hinterp_w1 Hinterp_w0]] ]
+             (Hcode & Hlink_cap & Hdata1 & HPC & Hr0 & Hr1 & Hr2 & Hr3 & Hr4 & Hr5 & Hna & Hcont)".
     codefrag_facts "Hcode".
+
     iInstr "Hcode". (* Mov *)
     iInstr "Hcode". (* Mov *)
     iInstr "Hcode". (* Lea *)
 
-    iInstr "Hcode". (* Lea *)
-    replace (a_data ^+1)%a with (b_main ^+ 50)%a by solve_addr'.
-    iInstr "Hcode". (* Load *)
-    iInstr "Hcode". (* Load *)
-    { admit. (* TODO it's fine *) }
-    iInstr "Hcode". (* Lea *)
-
-
     destruct (is_sealedL w0) eqn:Hsealed_w0 ; cycle 1.
     { (* w0 is not a sealed  *)
       destruct_lword (w0) ; cbn in Hsealed_w0 ; try done.
@@ -339,6 +500,7 @@ Section trusted_compute_example.
 
     destruct w0 as [ ? | ? | o sw0 ]
     ; cbn in Hsealed_w0 ; try done; clear Hsealed_w0.
+
     iInstr "Hcode". (* GetOType *)
     iInstr "Hcode". (* Sub *)
     replace (o - -1) with (o + 1) by lia.
@@ -347,23 +509,112 @@ Section trusted_compute_example.
     iInstr "Hcode". (* Lea *)
     iInstr "Hcode". (* Jnz *)
     iInstr "Hcode". (* GetOType *)
-    (* iInstr "Hcode". (* EStoreId r_t2 r_t2 r_t4 *) *)
-  Admitted.
 
-        (* (* check otype(w_res) against identity of the enclave *) *)
-        (* GetOType r_t2 r_t0; (* r2 := LInt σ *) *)
-        (* EStoreId r_t2 r_t2 r_t4; (* r2 := if etbl[σ] = Some I then 1 else 0 *) *)
-        (* Sub r_t2 r_t2 1; (* r2 := if etbl[σ] = Some I then 0 else -1 *) *)
-        (* Jnz r_t3 r_t2; (* Jumps to `fails` if (etbl[σ] = None)  *) *)
-        (* Load r_t4 r_t4; *)
-        (* Sub r_t4 r_t4 hash_enclave; *)
-        (* Jnz r_t3 r_t4; *)
-
-        (* (* get returned value and assert it to be 42 *) *)
-        (* UnSeal r_t0 r_t0 r_t1; *)
-        (* Mov r_t1 r_t5; *)
-        (* GetA r_t4 r_t0; *)
-        (* Mov r_t5 42%Z *)
+    iInstr_lookup "Hcode" as "Hi" "Hcode".
+    wp_instr.
+    iApply (wp_estoreid_success_unknown with "[HPC Hr2 Hr4 Hi]"); try iFrame; try solve_pure.
+    iNext.
+    iIntros (retv) "H".
+    iDestruct "H" as "(Hi & Hr2 & [(-> & HPC & H)|(-> & HPC & Hr4)])".
+    iDestruct "H" as (I tid) "(Hr4 & #Htc_env & %Hseal)".
+    all: wp_pure; iInstr_close "Hcode".
+    2:{ wp_end; by iRight. }
+
+    iInstr "Hcode". (* Sub *)
+    destruct (decide (I = hash_trusted_compute_enclave)) as [-> | HnI]
+    ; cycle 1.
+    { (* Not the right enclave *)
+      iInstr "Hcode". (* Jnz *)
+      by (injection; intro Hcontra; lia).
+      iInstr "Hcode". (* Fail *)
+      wp_end; by iRight.
+    }
+    replace (hash_trusted_compute_enclave - hash_trusted_compute_enclave)
+      with 0 by lia.
+    iInstr "Hcode". (* Jnz *)
+    iDestruct (interp_valid_sealed with "Hinterp_w0") as (Φ) "Hseal_valid".
+    rewrite /custom_enclave_inv.
+
+
+    (* UnSeal *)
+    wp_instr.
+    iMod (inv_acc with "Hcemap_inv") as "(#Hcemap & Hclose)"; first solve_ndisj.
+
+    iInstr_lookup "Hcode" as "Hi" "Hcode".
+    iDestruct (map_of_regs_3 with "HPC Hr1 Hr0") as "[Hmap _]".
+    iApply (wp_UnSeal with "[$Hmap Hi]"); eauto; simplify_map_eq; eauto;
+    try solve_pure.
+    by unfold regs_of; rewrite !dom_insert; set_solver+.
+    iNext. iIntros (regs' retv) "(#Hspec & Hpc_a & Hmap)". iDestruct "Hspec" as %Hspec.
+    destruct Hspec as [ ? ? ? ? ? ? ? Hps Hbounds Hregs'|]; cycle 1.
+    { iMod ("Hclose" with "Hcemap") as "_". iModIntro.
+      by wp_pure; wp_end; iRight.
+    }
+    iMod ("Hclose" with "Hcemap") as "_"; iModIntro.
+    incrementLPC_inv as (p''&b_main'&e_main'&a_main'&pc_v'& ? & HPC & Z & Hregs'); simplify_map_eq.
+    repeat (rewrite insert_commute //= insert_insert).
+    replace x with (b_main' ^+ 20)%a by solve_addr.
+    clear Z.
+    iDestruct (regs_of_map_3 with "[$Hmap]") as "[HPC [Hr1 Hr0] ]"; eauto; iFrame.
+    wp_pure; iInstr_close "Hcode".
+
+    iAssert (
+        seal_pred a (Penc (tc_enclave_pred tc_data_cap tc_addr))
+        ∗ seal_pred (a ^+ 1)%f (Psign (tc_enclave_pred tc_data_cap tc_addr))
+      )%I as "[Htc_Penc _]".
+    {
+      iApply "Hcemap"; iFrame "%#".
+      iPureIntro.
+      rewrite /tcenclaves_map.
+      by simplify_map_eq.
+    }
+    iEval (cbn) in "Htc_Penc".
+
+    iDestruct (seal_pred_valid_sealed_eq with "[$Htc_Penc] Hseal_valid") as "Heqv".
+    iAssert (▷ sealed_42 (LWSealable sb))%I as (fb fe fv) ">%Hseal42".
+    { iDestruct "Hseal_valid" as (sb') "(%Heq & _ & _ & HΦ)".
+      inversion Heq; subst.
+      iSpecialize ("Heqv" $! (LWSealable sb')).
+      iNext.
+      iRewrite "Heqv".
+      iFrame "HΦ". }
+    destruct sb ; simplify_eq.
+
+    iInstr "Hcode". (* Mov *)
+    iInstr "Hcode". (* GetA *)
+    iInstr "Hcode". (* Mov *)
+    iInstr "Hcode". (* Mov *)
+    iInstr "Hcode". (* Lea *)
+    iInstr "Hcode". (* Load *)
 
+    subst trusted_compute_main.
+    rewrite /trusted_compute_main_code /trusted_compute_main_code_callback0.
+    subst a_callback.
+    rewrite /trusted_compute_main_init_len.
+
+    focus_block 2%nat "Hcode" as addr_block2 Haddr_block2 "Hblock" "Hcode'".
+    cbn in Haddr_block2.
+    iMod (na_inv_acc with "HlinkInv Hna") as "(>Hassert_entry & Hna & Hclose)"; [ solve_ndisj.. |].
+    iApply assert_reg_success; last iFrame "#∗"; try solve_pure ; try solve_addr'.
+    solve_ndisj.
+    iIntros "!> (HPC & Hr0 & Hr1 & Hr2 & Hr4 & Hr5 & Hblock & Hna & Hassert_entry)".
+    iMod ("Hclose" with "[$Hna $Hassert_entry]") as "Hna".
+    iAssert (codefrag addr_block2 pc_v' (assert_reg_instrs assert_lt_offset r_t1)) with "[$Hblock]" as "Hblock".
+    unfocus_block "Hblock" "Hcode'" as "Hcode".
+
+    focus_block 3%nat "Hcode" as addr_block3 Haddr_block3 "Hblock" "Hcode'".
+    cbn in Haddr_block3.
+    iInstr "Hblock". (* Mov *)
+    admit. (* TODO why automation doesn't work here? *)
+    iInstr "Hblock". (* Mov *)
+    admit. (* TODO why automation doesn't work here? *)
+    iInstr "Hblock". (* Halt *)
+    admit. (* TODO why automation doesn't work here? *)
+    unfocus_block "Hblock" "Hcode'" as "Hcode".
+    replace (addr_block3 ^+ 2)%a with (a_data ^+ -2)%a by solve_addr'.
+
+    iApply (wp_wand with "[-]") ; [  | iIntros (?) "H"; iLeft ; iApply "H"].
+    iApply "Hcont"; iFrame.
+    Admitted.
 
 End trusted_compute_example.
diff --git a/theories/examples/macros_new.v b/theories/examples/macros_new.v
index 661fc2a9..cd31b721 100644
--- a/theories/examples/macros_new.v
+++ b/theories/examples/macros_new.v
@@ -28,27 +28,27 @@ Section macros.
       Load r_t1 r_t1
     ].
 
-  Lemma fetch_spec f pc_p pc_b pc_e v a_first b_link e_link a_link entry_a wentry φ w1 w2 w3:
+  Lemma fetch_spec f pc_p pc_b pc_e pc_v a_first b_link e_link a_link v_link entry_a wentry φ w1 w2 w3:
     ExecPCPerm pc_p →
     SubBounds pc_b pc_e a_first (a_first ^+ length (fetch_instrs f))%a →
     withinBounds b_link e_link entry_a = true ->
     (a_link + f)%a = Some entry_a ->
 
-      ▷ codefrag a_first v (fetch_instrs f)
-    ∗ ▷ PC ↦ᵣ LCap pc_p pc_b pc_e a_first v
-    ∗ ▷ (pc_b,v) ↦ₐ LCap RO b_link e_link a_link v
-    ∗ ▷ (entry_a,v) ↦ₐ wentry
+      ▷ codefrag a_first pc_v (fetch_instrs f)
+    ∗ ▷ PC ↦ᵣ LCap pc_p pc_b pc_e a_first pc_v
+    ∗ ▷ (pc_b,pc_v) ↦ₐ LCap RO b_link e_link a_link v_link
+    ∗ ▷ (entry_a,v_link) ↦ₐ wentry
     ∗ ▷ r_t1 ↦ᵣ w1
     ∗ ▷ r_t2 ↦ᵣ w2
     ∗ ▷ r_t3 ↦ᵣ w3
     (* if the capability is global, we want to be able to continue *)
     (* if w is not a global capability, we will fail, and must now show that Phi holds at failV *)
-    ∗ ▷ (PC ↦ᵣ LCap pc_p pc_b pc_e (a_first ^+ length (fetch_instrs f))%a v
-         ∗ codefrag a_first v (fetch_instrs f)
+    ∗ ▷ (PC ↦ᵣ LCap pc_p pc_b pc_e (a_first ^+ length (fetch_instrs f))%a pc_v
+         ∗ codefrag a_first pc_v (fetch_instrs f)
          (* the newly allocated region *)
          ∗ r_t1 ↦ᵣ wentry ∗ r_t2 ↦ᵣ LInt 0%Z ∗ r_t3 ↦ᵣ LInt 0%Z
-         ∗ (pc_b,v) ↦ₐ LCap RO b_link e_link a_link v
-         ∗ (entry_a,v) ↦ₐ wentry
+         ∗ (pc_b,pc_v) ↦ₐ LCap RO b_link e_link a_link v_link
+         ∗ (entry_a,v_link) ↦ₐ wentry
          -∗ WP Seq (Instr Executable) {{ φ }})
     ⊢
       WP Seq (Instr Executable) {{ φ }}.
@@ -70,23 +70,23 @@ Section macros.
         Load r_lt r_lt (* r_lt := mem(b_tbl + f) *)
       ].
 
-  Lemma fetch_reg_spec f r_lt pc_p pc_b pc_e v a_first b_link e_link a_link entry_a wentry φ :
+  Lemma fetch_reg_spec f r_lt pc_p pc_b pc_e pc_v a_first b_link e_link a_link v_link entry_a wentry φ :
     ExecPCPerm pc_p →
     SubBounds pc_b pc_e a_first (a_first ^+ length (fetch_reg_instrs f r_lt))%a →
     withinBounds b_link e_link entry_a = true ->
     (a_link + f)%a = Some entry_a ->
 
-      ▷ codefrag a_first v (fetch_reg_instrs f r_lt)
-    ∗ ▷ PC ↦ᵣ LCap pc_p pc_b pc_e a_first v
-    ∗ ▷ (entry_a,v) ↦ₐ wentry
-    ∗ ▷ r_lt ↦ᵣ LCap RO b_link e_link a_link v
+      ▷ codefrag a_first pc_v (fetch_reg_instrs f r_lt)
+    ∗ ▷ PC ↦ᵣ LCap pc_p pc_b pc_e a_first pc_v
+    ∗ ▷ (entry_a,v_link) ↦ₐ wentry
+    ∗ ▷ r_lt ↦ᵣ LCap RO b_link e_link a_link v_link
     (* if the capability is global, we want to be able to continue *)
     (* if w is not a global capability, we will fail, and must now show that Phi holds at failV *)
-    ∗ ▷ (PC ↦ᵣ LCap pc_p pc_b pc_e (a_first ^+ length (fetch_reg_instrs f r_lt))%a v
-         ∗ codefrag a_first v (fetch_reg_instrs f r_lt)
+    ∗ ▷ (PC ↦ᵣ LCap pc_p pc_b pc_e (a_first ^+ length (fetch_reg_instrs f r_lt))%a pc_v
+         ∗ codefrag a_first pc_v (fetch_reg_instrs f r_lt)
          (* the newly allocated region *)
          ∗ r_lt ↦ᵣ wentry
-         ∗ (entry_a,v) ↦ₐ wentry
+         ∗ (entry_a,v_link) ↦ₐ wentry
          -∗ WP Seq (Instr Executable) {{ φ }})
     ⊢
       WP Seq (Instr Executable) {{ φ }}.
@@ -114,8 +114,8 @@ Section macros.
     ].
 
   (* Spec for assertion success *)
-  Lemma assert_success f_a pc_p pc_b pc_e v a_first
-        b_link e_link a_link a_entry ba a_flag ea w0 w1 w2 w3 assertN EN n1 n2 φ :
+  Lemma assert_success f_a pc_p pc_b pc_e pc_v a_first
+        b_link e_link a_link v_link a_entry ba a_flag ea v_assert w0 w1 w2 w3 assertN EN n1 n2 φ :
     ExecPCPerm pc_p →
     SubBounds pc_b pc_e a_first (a_first ^+ length (assert_instrs f_a))%a →
     (* linking table assumptions *)
@@ -125,26 +125,26 @@ Section macros.
     (* condition for assertion success *)
     (n1 = n2) →
 
-    ▷ codefrag a_first v (assert_instrs f_a)
-    ∗ na_inv logrel_nais assertN (assert_inv ba a_flag ea v)
+    ▷ codefrag a_first pc_v (assert_instrs f_a)
+    ∗ na_inv logrel_nais assertN (assert_inv ba a_flag ea v_assert)
     ∗ na_own logrel_nais EN
-    ∗ ▷ PC ↦ᵣ LCap pc_p pc_b pc_e a_first v
-    ∗ ▷ (pc_b,v) ↦ₐ LCap RO b_link e_link a_link v
-    ∗ ▷ (a_entry,v) ↦ₐ LCap E ba ea ba v
+    ∗ ▷ PC ↦ᵣ LCap pc_p pc_b pc_e a_first pc_v
+    ∗ ▷ (pc_b,pc_v) ↦ₐ LCap RO b_link e_link a_link v_link
+    ∗ ▷ (a_entry,v_link) ↦ₐ LCap E ba ea ba v_assert
     ∗ ▷ r_t0 ↦ᵣ w0
     ∗ ▷ r_t1 ↦ᵣ w1
     ∗ ▷ r_t2 ↦ᵣ w2
     ∗ ▷ r_t3 ↦ᵣ w3
     ∗ ▷ r_t4 ↦ᵣ LInt n1
     ∗ ▷ r_t5 ↦ᵣ LInt n2
-    ∗ ▷ (PC ↦ᵣ LCap pc_p pc_b pc_e (a_first ^+ length (assert_instrs f_a))%a v
+    ∗ ▷ (PC ↦ᵣ LCap pc_p pc_b pc_e (a_first ^+ length (assert_instrs f_a))%a pc_v
          ∗ r_t0 ↦ᵣ w0
          ∗ r_t1 ↦ᵣ LInt 0%Z ∗ r_t2 ↦ᵣ LInt 0%Z ∗ r_t3 ↦ᵣ LInt 0%Z
          ∗ r_t4 ↦ᵣ LInt 0%Z ∗ r_t5 ↦ᵣ LInt 0%Z
-         ∗ codefrag a_first v (assert_instrs f_a)
+         ∗ codefrag a_first pc_v (assert_instrs f_a)
          ∗ na_own logrel_nais EN
-         ∗ (pc_b,v) ↦ₐ LCap RO b_link e_link a_link v
-         ∗ (a_entry,v) ↦ₐ LCap E ba ea ba v
+         ∗ (pc_b,pc_v) ↦ₐ LCap RO b_link e_link a_link v_link
+         ∗ (a_entry,v_link) ↦ₐ LCap E ba ea ba v_assert
          -∗ WP Seq (Instr Executable) {{ φ }})
     ⊢
     WP Seq (Instr Executable) {{ φ }}.
@@ -186,8 +186,8 @@ Section macros.
     ].
 
   (* Spec for assertion success *)
-  Lemma assert_reg_success f_a r_lt pc_p pc_b pc_e v a_first
-        b_link e_link a_link a_entry ba a_flag ea w0 w2 assertN EN n1 n2 φ :
+  Lemma assert_reg_success f_a r_lt pc_p pc_b pc_e pc_v a_first
+        b_link e_link a_link v_link a_entry ba a_flag ea v_assert w0 w2 assertN EN n1 n2 φ :
     ExecPCPerm pc_p →
     SubBounds pc_b pc_e a_first (a_first ^+ length (assert_reg_instrs f_a r_lt))%a →
     (* linking table assumptions *)
@@ -197,23 +197,23 @@ Section macros.
     (* condition for assertion success *)
     (n1 = n2) →
 
-    ▷ codefrag a_first v (assert_reg_instrs f_a r_lt)
-    ∗ na_inv logrel_nais assertN (assert_inv ba a_flag ea v)
+    ▷ codefrag a_first pc_v (assert_reg_instrs f_a r_lt)
+    ∗ na_inv logrel_nais assertN (assert_inv ba a_flag ea v_assert)
     ∗ na_own logrel_nais EN
-    ∗ ▷ PC ↦ᵣ LCap pc_p pc_b pc_e a_first v
-    ∗ ▷ (a_entry,v) ↦ₐ LCap E ba ea ba v
+    ∗ ▷ PC ↦ᵣ LCap pc_p pc_b pc_e a_first pc_v
+    ∗ ▷ (a_entry,v_link) ↦ₐ LCap E ba ea ba v_assert
     ∗ ▷ r_t0 ↦ᵣ w0
-    ∗ ▷ r_lt ↦ᵣ (LCap RO b_link e_link a_link v)
+    ∗ ▷ r_lt ↦ᵣ (LCap RO b_link e_link a_link v_link)
     ∗ ▷ r_t2 ↦ᵣ w2
     ∗ ▷ r_t4 ↦ᵣ LInt n1
     ∗ ▷ r_t5 ↦ᵣ LInt n2
-    ∗ ▷ (PC ↦ᵣ LCap pc_p pc_b pc_e (a_first ^+ length (assert_reg_instrs f_a r_lt))%a v
+    ∗ ▷ (PC ↦ᵣ LCap pc_p pc_b pc_e (a_first ^+ length (assert_reg_instrs f_a r_lt))%a pc_v
          ∗ r_t0 ↦ᵣ w0
          ∗ r_lt ↦ᵣ LInt 0%Z ∗ r_t2 ↦ᵣ LInt 0%Z
          ∗ r_t4 ↦ᵣ LInt 0%Z ∗ r_t5 ↦ᵣ LInt 0%Z
-         ∗ codefrag a_first v (assert_reg_instrs f_a r_lt)
+         ∗ codefrag a_first pc_v (assert_reg_instrs f_a r_lt)
          ∗ na_own logrel_nais EN
-         ∗ (a_entry,v) ↦ₐ LCap E ba ea ba v
+         ∗ (a_entry,v_link) ↦ₐ LCap E ba ea ba v_assert
          -∗ WP Seq (Instr Executable) {{ φ }})
     ⊢
     WP Seq (Instr Executable) {{ φ }}.
@@ -258,8 +258,8 @@ Section macros.
   ].
 
   (* malloc spec *)
-  Lemma malloc_spec_alt φ ψ size cont pc_p pc_b pc_e v a_first
-        b_link e_link a_link f_m a_entry mallocN b_m e_m EN rmap :
+  Lemma malloc_spec_alt φ ψ size cont pc_p pc_b pc_e pc_v a_first
+        b_link e_link a_link v_link f_m a_entry v_malloc mallocN b_m e_m EN rmap :
     ExecPCPerm pc_p →
     SubBounds pc_b pc_e a_first (a_first ^+ length (malloc_instrs f_m size))%a →
     withinBounds b_link e_link a_entry = true →
@@ -269,28 +269,28 @@ Section macros.
     (size > 0)%Z →
 
     (* malloc program and subroutine *)
-    ▷ codefrag a_first v (malloc_instrs f_m size)
-    ∗ na_inv logrel_nais mallocN (malloc_inv b_m e_m v)
+    ▷ codefrag a_first pc_v (malloc_instrs f_m size)
+    ∗ na_inv logrel_nais mallocN (malloc_inv b_m e_m v_malloc)
     ∗ na_own logrel_nais EN
     (* we need to assume that the malloc capability is in the linking table at offset f_m *)
-    ∗ ▷ (pc_b,v) ↦ₐ LCap RO b_link e_link a_link v
-    ∗ ▷ (a_entry,v) ↦ₐ LCap E b_m e_m b_m v
+    ∗ ▷ (pc_b,pc_v) ↦ₐ LCap RO b_link e_link a_link v_link
+    ∗ ▷ (a_entry,v_link) ↦ₐ LCap E b_m e_m b_m v_malloc
     (* register state *)
-    ∗ ▷ PC ↦ᵣ LCap pc_p pc_b pc_e a_first v
+    ∗ ▷ PC ↦ᵣ LCap pc_p pc_b pc_e a_first pc_v
     ∗ ▷ r_t0 ↦ᵣ cont
     ∗ ▷ ([∗ map] r_i↦w_i ∈ rmap, r_i ↦ᵣ w_i)
     (* failure/continuation *)
     ∗ ▷ (∀ v, ψ v -∗ φ v)
     ∗ ▷ (φ FailedV)
-    ∗ ▷ (PC ↦ᵣ LCap pc_p pc_b pc_e (a_first ^+ length (malloc_instrs f_m size))%a v
-         ∗ codefrag a_first v (malloc_instrs f_m size)
-         ∗ (pc_b,v) ↦ₐ LCap RO b_link e_link a_link v
-         ∗ (a_entry,v) ↦ₐ LCap E b_m e_m b_m v
+    ∗ ▷ (PC ↦ᵣ LCap pc_p pc_b pc_e (a_first ^+ length (malloc_instrs f_m size))%a pc_v
+         ∗ codefrag a_first pc_v (malloc_instrs f_m size)
+         ∗ (pc_b,pc_v) ↦ₐ LCap RO b_link e_link a_link v_link
+         ∗ (a_entry,v_link) ↦ₐ LCap E b_m e_m b_m v_malloc
          (* the newly allocated region *)
          ∗ (∃ (b e : Addr),
             ⌜(b + size)%a = Some e⌝
-            ∗ r_t1 ↦ᵣ LCap RWX b e b v
-            ∗ [[b,e]] ↦ₐ{v} [[region_addrs_zeroesL b e v]])
+            ∗ r_t1 ↦ᵣ LCap RWX b e b v_malloc
+            ∗ [[b,e]] ↦ₐ{v_malloc} [[region_addrs_zeroesL b e v_malloc]])
          ∗ r_t0 ↦ᵣ cont
          ∗ na_own logrel_nais EN
          ∗ ([∗ map] r_i↦w_i ∈ (<[r_t2:=LInt 0%Z]>
@@ -360,8 +360,8 @@ Section macros.
   Qed.
 
   (* malloc spec - alternative formulation *)
-  Lemma malloc_spec φ size cont pc_p pc_b pc_e v a_first
-        b_link e_link a_link f_m a_entry mallocN b_m e_m EN rmap :
+  Lemma malloc_spec φ size cont pc_p pc_b pc_e pc_v a_first
+        b_link e_link a_link v_link f_m a_entry v_malloc mallocN b_m e_m EN rmap :
     ExecPCPerm pc_p →
     SubBounds pc_b pc_e a_first (a_first ^+ length (malloc_instrs f_m size))%a →
     withinBounds b_link e_link a_entry = true →
@@ -371,26 +371,26 @@ Section macros.
     (size > 0)%Z →
 
     (* malloc program and subroutine *)
-    ▷ codefrag a_first v (malloc_instrs f_m size)
-    ∗ na_inv logrel_nais mallocN (malloc_inv b_m e_m v)
+    ▷ codefrag a_first pc_v (malloc_instrs f_m size)
+    ∗ na_inv logrel_nais mallocN (malloc_inv b_m e_m v_malloc)
     ∗ na_own logrel_nais EN
     (* we need to assume that the malloc capability is in the linking table at offset f_m *)
-    ∗ ▷ (pc_b,v) ↦ₐ LCap RO b_link e_link a_link v
-    ∗ ▷ (a_entry,v) ↦ₐ LCap E b_m e_m b_m v
+    ∗ ▷ (pc_b,pc_v) ↦ₐ LCap RO b_link e_link a_link v_link
+    ∗ ▷ (a_entry,v_link) ↦ₐ LCap E b_m e_m b_m v_malloc
     (* register state *)
-    ∗ ▷ PC ↦ᵣ LCap pc_p pc_b pc_e a_first v
+    ∗ ▷ PC ↦ᵣ LCap pc_p pc_b pc_e a_first pc_v
     ∗ ▷ r_t0 ↦ᵣ cont
     ∗ ▷ ([∗ map] r_i↦w_i ∈ rmap, r_i ↦ᵣ w_i)
     (* continuation *)
-    ∗ ▷ (PC ↦ᵣ LCap pc_p pc_b pc_e (a_first ^+ length (malloc_instrs f_m size))%a v
-         ∗ codefrag a_first v (malloc_instrs f_m size)
-         ∗ (pc_b,v) ↦ₐ LCap RO b_link e_link a_link v
-         ∗ (a_entry,v) ↦ₐ LCap E b_m e_m b_m v
+    ∗ ▷ (PC ↦ᵣ LCap pc_p pc_b pc_e (a_first ^+ length (malloc_instrs f_m size))%a pc_v
+         ∗ codefrag a_first pc_v (malloc_instrs f_m size)
+         ∗ (pc_b,pc_v) ↦ₐ LCap RO b_link e_link a_link v_link
+         ∗ (a_entry,v_link) ↦ₐ LCap E b_m e_m b_m v_malloc
          (* the newly allocated region *)
          ∗ (∃ (b e : Addr),
             ⌜(b + size)%a = Some e⌝
-            ∗ r_t1 ↦ᵣ LCap RWX b e b v
-            ∗ [[b,e]] ↦ₐ{v} [[region_addrs_zeroesL b e v]])
+            ∗ r_t1 ↦ᵣ LCap RWX b e b v_malloc
+            ∗ [[b,e]] ↦ₐ{v_malloc} [[region_addrs_zeroesL b e v_malloc]])
          ∗ r_t0 ↦ᵣ cont
          ∗ na_own logrel_nais EN
          ∗ ([∗ map] r_i↦w_i ∈ (<[r_t2:=LInt 0%Z]>
diff --git a/theories/logical_mapsto.v b/theories/logical_mapsto.v
index 3abc6e00..5130ec2c 100644
--- a/theories/logical_mapsto.v
+++ b/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 *)
 
diff --git a/theories/rules/rules_IsUnique.v b/theories/rules/rules_IsUnique.v
index f147369c..7c96dc2d 100644
--- a/theories/rules/rules_IsUnique.v
+++ b/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".
@@ -774,8 +772,10 @@ Section cap_lang_rules.
       iClear "Hrmap".
       iFrame.
 
+      assert ( Hpc_a : pc_a ∉ finz.seq_between b0 e0)
+               by (eapply unique_in_registersL_pc_no_overlap; eauto; by simplify_map_eq).
       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. }
 
       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 *)
 
diff --git a/theories/rules/rules_UnSeal.v b/theories/rules/rules_UnSeal.v
index bff8073c..b175754e 100644
--- a/theories/rules/rules_UnSeal.v
+++ b/theories/rules/rules_UnSeal.v
@@ -342,4 +342,28 @@ Section cap_lang_rules.
       destruct (decide (o' = a)) as [->| Hne]; [solve_addr | simplify_map_eq]. }
   Qed.
 
+  Lemma wp_unseal_nomatch_r1 E pc_p pc_b pc_e pc_a pc_v lw r1 r2 o sb lwsealr pc_a' :
+    decodeInstrWL lw = UnSeal r1 r1 r2 →
+    isCorrectLPC (LCap pc_p pc_b pc_e pc_a pc_v) →
+    (pc_a + 1)%a = Some pc_a' →
+    is_sealrL lwsealr = false ->
+
+    {{{ ▷ PC ↦ᵣ LCap pc_p pc_b pc_e pc_a pc_v
+          ∗ ▷ (pc_a, pc_v) ↦ₐ lw
+          ∗ ▷ r1 ↦ᵣ lwsealr
+          ∗ ▷ r2 ↦ᵣ LWSealed o sb }}}
+      Instr Executable @ E
+      {{{ RET FailedV; True }}}.
+  Proof.
+    iIntros (Hinstr Hvpc Hpc_a' Hfalse ϕ) "(>HPC & >Hpc_a & >Hr1 & >Hr2) Hφ".
+
+    iDestruct (map_of_regs_3 with "HPC Hr1 Hr2") as "[Hmap (%&%&%)]".
+    iApply (wp_UnSeal with "[$Hmap Hpc_a]"); eauto; simplify_map_eq; eauto.
+    by unfold regs_of; rewrite !dom_insert; set_solver+.
+    iNext. iIntros (regs' retv) "(#Hspec & Hpc_a & Hmap)". iDestruct "Hspec" as %Hspec.
+
+    destruct Hspec as [ | ]; last by iApply "Hφ".
+    { destruct lwsealr as [| | o' sb']; try by simplify_map_eq. }
+  Qed.
+
 End cap_lang_rules.