From 981bb1b588ffae98054a40f6840049c32c2aac83 Mon Sep 17 00:00:00 2001
From: June Rousseau <june.rousseau@cs.au.dk>
Date: Thu, 12 Feb 2026 00:25:04 +0100
Subject: [PATCH 1/2] WIP replace readSR/writeSR by specialRW

---
 theories/logrel/ftlr/ReadSR.v                 |  63 ----
 .../logrel/ftlr/{WriteSR.v => SpecialRW.v}    |  13 +-
 theories/logrel/fundamental.v                 |  13 +-
 theories/opsem/assembler.v                    |  29 +-
 theories/opsem/cap_lang.v                     |  14 +-
 theories/opsem/machine_base.v                 |  42 ++-
 theories/program_logic/rules.v                |   2 +-
 theories/program_logic/rules/rules_ReadSR.v   | 194 -----------
 .../program_logic/rules/rules_SpecialRW.v     | 328 ++++++++++++++++++
 theories/program_logic/rules/rules_WriteSR.v  | 196 -----------
 theories/program_logic/rules/rules_base.v     |   6 +-
 .../proofmode/proofmode_instr_rules.v         |  10 +-
 12 files changed, 386 insertions(+), 524 deletions(-)
 delete mode 100644 theories/logrel/ftlr/ReadSR.v
 rename theories/logrel/ftlr/{WriteSR.v => SpecialRW.v} (81%)
 delete mode 100644 theories/program_logic/rules/rules_ReadSR.v
 create mode 100644 theories/program_logic/rules/rules_SpecialRW.v
 delete mode 100644 theories/program_logic/rules/rules_WriteSR.v

diff --git a/theories/logrel/ftlr/ReadSR.v b/theories/logrel/ftlr/ReadSR.v
deleted file mode 100644
index 3df939a0..00000000
--- a/theories/logrel/ftlr/ReadSR.v
+++ /dev/null
@@ -1,63 +0,0 @@
-From cap_machine Require Export logrel.
-From iris.proofmode Require Import proofmode.
-From iris.program_logic Require Import weakestpre adequacy lifting.
-From stdpp Require Import base.
-From cap_machine Require Import ftlr_base interp_weakening.
-From cap_machine Require Import rules_base rules_ReadSR.
-From cap_machine.proofmode Require Import map_simpl register_tactics.
-From cap_machine Require Import stdpp_extra.
-
-Section fundamental.
-  Context
-    {Σ:gFunctors}
-    {ceriseg:ceriseG Σ} {sealsg: sealStoreG Σ}
-    {Cname : CmptNameG}
-    {stsg : STSG Addr region_type Σ} {heapg : heapGS Σ}
-    {cstackg : CSTACKG Σ}
-    {nainv: logrel_na_invs Σ}
-    `{MP: MachineParameters}
-  .
-
-  Implicit Types W : WORLD.
-  Implicit Types C : CmptName.
-
-  Notation D := (WORLD -n> (leibnizO CmptName) -n> (leibnizO Word) -n> iPropO Σ).
-  Notation R := (WORLD -n> (leibnizO CmptName) -n> (leibnizO Reg) -n> iPropO Σ).
-  Implicit Types w : (leibnizO Word).
-  Implicit Types interp : (D).
-
-  Lemma readsr_case (W : WORLD) (C : CmptName) (regs : leibnizO Reg)
-    (p p' : Perm) (g : Locality) (b e a : Addr)
-    (w : Word) (ρ : region_type) (dst : RegName) (src : SRegName) (P:D) (cstk : CSTK) (Ws : list WORLD) (Cs : list CmptName) :
-    ftlr_instr W C regs p p' g b e a w (ReadSR dst src) ρ P cstk Ws Cs.
-  Proof.
-    intros Hp Hsome HcorrectPC Hbae Hfp HO Hpers Hpwl Hregion Hnotrevoked Hi.
-    iIntros "#IH #Hinv_interp #Hreg #Hinva #Hrcond #Hwcond #Hmono #HmonoV Hw Hcont %Hframe Hsts Hown Htframe".
-    iIntros "Hr Hstate Ha HPC Hmap".
-    iInsert "Hmap" PC.
-    destruct (has_sreg_access p) eqn:HpXRS.
-    { iClear "IH Hreg Hinva Hrcond Hwcond Hmono HmonoV Hw Hsts Htframe Hown Hr Hstate Ha Hmap".
-      iEval (rewrite !fixpoint_interp1_eq interp1_eq) in "Hinv_interp".
-      destruct (isO p) eqn: HnO.
-      { destruct Hp as [Hexec _]
-        ; eapply executeAllowed_nonO in Hexec
-        ; congruence.
-      }
-      destruct (has_sreg_access p) eqn:HpXRS'; first done.
-      congruence.
-    }
-
-    iApply (wp_ReadSR with "[$Ha $Hmap]"); eauto.
-    { simplify_map_eq; auto. }
-    { rewrite /subseteq /map_subseteq. intros rr _.
-      apply elem_of_dom. apply lookup_insert_is_Some'; eauto. }
-    { by rewrite HpXRS. }
-
-    iIntros "!>" (regs' retv). iDestruct 1 as (HSpec) "[Ha Hmap]".
-    destruct HSpec; cycle 1.
-    - iApply wp_pure_step_later; auto. iNext; iIntros "_".
-      iApply wp_value; auto.
-    - by simplify_map_eq.
-  Qed.
-
-End fundamental.
diff --git a/theories/logrel/ftlr/WriteSR.v b/theories/logrel/ftlr/SpecialRW.v
similarity index 81%
rename from theories/logrel/ftlr/WriteSR.v
rename to theories/logrel/ftlr/SpecialRW.v
index 78ec2289..53b4f601 100644
--- a/theories/logrel/ftlr/WriteSR.v
+++ b/theories/logrel/ftlr/SpecialRW.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Import weakestpre adequacy lifting.
 From stdpp Require Import base.
 From cap_machine Require Import ftlr_base interp_weakening.
-From cap_machine Require Import rules_base rules_WriteSR.
+From cap_machine Require Import rules_base rules_SpecialRW.
 From cap_machine.proofmode Require Import map_simpl register_tactics.
 From cap_machine Require Import stdpp_extra.
 
@@ -26,10 +26,10 @@ Section fundamental.
   Implicit Types w : (leibnizO Word).
   Implicit Types interp : (D).
 
-  Lemma writesr_case (W : WORLD) (C : CmptName) (regs : leibnizO Reg)
+  Lemma specialrw_case (W : WORLD) (C : CmptName) (regs : leibnizO Reg)
     (p p' : Perm) (g : Locality) (b e a : Addr)
-    (w : Word) (ρ : region_type) (dst : SRegName) (src : RegName) (P:D) (cstk : CSTK) (Ws : list WORLD) (Cs : list CmptName) :
-    ftlr_instr W C regs p p' g b e a w (WriteSR dst src) ρ P cstk Ws Cs.
+    (w : Word) (ρ : region_type) (dst : RegName) (csr : SRegName) (src : RegName) (P:D) (cstk : CSTK) (Ws : list WORLD) (Cs : list CmptName) :
+    ftlr_instr W C regs p p' g b e a w (SpecialRW dst csr src) ρ P cstk Ws Cs.
   Proof.
     intros Hp Hsome HcorrectPC Hbae Hfp HO Hpers Hpwl Hregion Hnotrevoked Hi.
     iIntros "#IH #Hinv_interp #Hreg #Hinva #Hrcond #Hwcond #Hmono #HmonoV Hw Hcont %Hframe Hsts Hown Htframe".
@@ -47,17 +47,18 @@ Section fundamental.
       congruence.
     }
 
-    iApply (wp_WriteSR with "[$Ha $Hmap]"); eauto.
+    iApply (wp_SpecialRW with "[$Ha $Hmap]"); eauto.
     { simplify_map_eq; auto. }
     { rewrite /subseteq /map_subseteq. intros rr _.
       apply elem_of_dom. apply lookup_insert_is_Some'; eauto. }
     { by rewrite HpXRS. }
 
     iIntros "!>" (regs' retv). iDestruct 1 as (HSpec) "[Ha Hmap]".
-    destruct HSpec; cycle 1.
+    destruct HSpec; cycle 2.
     - iApply wp_pure_step_later; auto. iNext; iIntros "_".
       iApply wp_value; auto.
     - simplify_map_eq; congruence.
+    - simplify_map_eq; congruence.
   Qed.
 
 End fundamental.
diff --git a/theories/logrel/fundamental.v b/theories/logrel/fundamental.v
index e0789c3d..5dc7bdc0 100644
--- a/theories/logrel/fundamental.v
+++ b/theories/logrel/fundamental.v
@@ -1,6 +1,6 @@
 From cap_machine Require Export
   Jmp Jnz Jalr Mov Load Store BinOp Restrict
-  Subseg Get Lea Seal UnSeal ReadSR WriteSR.
+  Subseg Get Lea Seal UnSeal SpecialRW.
 From cap_machine Require Export ftlr_base.
 From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Import weakestpre adequacy lifting.
@@ -316,15 +316,8 @@ Section fundamental.
                [$Hw] [$Hcont] [//] [$Hsts] [$Hown] [$Hframe]
                [$Hr] [$Hstate] [$Ha] [$HPC] [Hmreg]")
       ;eauto.
-    + (* ReadSR *)
-      iApply (readsr_case with
-               "[$IH] [$Hinv_interp] [$Hreg] [$Hrela]
-               [$Hrcond] [$Hwcond]  [$HmonoR] [$HmonoV]
-               [$Hw] [$Hcont] [//] [$Hsts] [$Hown] [$Hframe]
-               [$Hr] [$Hstate] [$Ha] [$HPC] [Hmreg]")
-      ;eauto.
-    + (* WriteSR *)
-      iApply (writesr_case with
+    + (* SpecialRW *)
+      iApply (specialrw_case with
                "[$IH] [$Hinv_interp] [$Hreg] [$Hrela]
                [$Hrcond] [$Hwcond]  [$HmonoR] [$HmonoV]
                [$Hw] [$Hcont] [//] [$Hsts] [$Hown] [$Hframe]
diff --git a/theories/opsem/assembler.v b/theories/opsem/assembler.v
index a13eae3b..9ebc8fc7 100644
--- a/theories/opsem/assembler.v
+++ b/theories/opsem/assembler.v
@@ -66,8 +66,7 @@ Module Asm_Griotte.
   | GetOType (dst r: RegName)
   | Seal (dst : RegName) (r1 r2: RegName)
   | UnSeal (dst : RegName) (r1 r2: RegName)
-  | ReadSR (dst: RegName) (src: SRegName)
-  | WriteSR (dst: SRegName) (src: RegName)
+  | SpecialRW (dst: RegName) (csr: SRegName) (src: RegName)
   | Fail
   | Halt.
 
@@ -207,10 +206,8 @@ Module Asm_Griotte.
         Some (Seal dst r1 r2)
     | UnSeal dst r1 r2 =>
         Some (UnSeal dst r1 r2)
-    | ReadSR dst src =>
-        Some (ReadSR dst src)
-    | WriteSR dst src =>
-        Some (WriteSR dst src)
+    | SpecialRW dst csr src =>
+        Some (SpecialRW dst csr src)
     | Fail=>
         Some (Fail)
     | Halt=>
@@ -354,10 +351,8 @@ Module Asm_Griotte.
         Some (machine_base.Seal dst r1 r2)
     | UnSeal dst r1 r2 =>
         Some (machine_base.UnSeal dst r1 r2)
-    | ReadSR dst src =>
-        Some (machine_base.ReadSR dst src)
-    | WriteSR dst src =>
-        Some (machine_base.WriteSR dst src)
+    | SpecialRW dst csr src =>
+        Some (machine_base.SpecialRW dst csr src)
     | Fail=>
         Some (machine_base.Fail)
     | Halt=>
@@ -572,12 +567,10 @@ Module Asm_Griotte.
         let r1 := revert_regs r1 in
         let r2 := revert_regs r2 in
         (machine_base.UnSeal dst r1 r2)
-    | machine_base.ReadSR dst src =>
+    | machine_base.SpecialRW dst csr src =>
         let dst := revert_regs dst in
-        (machine_base.ReadSR dst src)
-    | machine_base.WriteSR dst src =>
         let src := revert_regs src in
-        (machine_base.WriteSR dst src)
+        (machine_base.SpecialRW dst csr src)
     | machine_base.Fail=>
         (machine_base.Fail)
     | machine_base.Halt=>
@@ -638,10 +631,14 @@ Module Asm_Griotte.
   Definition getotype dst src := (ASM_Instr (GetOType dst src)).
   Definition seal dst r1 r2 := (ASM_Instr (Seal dst r1 r2)).
   Definition unseal dst r1 r2 := (ASM_Instr (UnSeal dst r1 r2)).
-  Definition readsr dst src := (ASM_Instr (ReadSR dst src)).
-  Definition writesr dst src := (ASM_Instr (WriteSR dst src)).
+  Definition specialrw dst csr src := (ASM_Instr (SpecialRW dst csr src)).
   Definition fail:= (ASM_Instr Fail).
   Definition halt:= (ASM_Instr Halt).
   Notation "# s" := (ASM_Label s) (at level 50).
 
+  (** Aliases *)
+  Definition readsr dst csr := specialrw dst csr cnull.
+  Definition writesr csr src := specialrw cnull csr src.
+  Definition ret rsrc := jalr cnull rsrc.
+
 End Asm_Griotte.
diff --git a/theories/opsem/cap_lang.v b/theories/opsem/cap_lang.v
index 792893be..9f7051ac 100644
--- a/theories/opsem/cap_lang.v
+++ b/theories/opsem/cap_lang.v
@@ -410,13 +410,15 @@ Section opsem.
         else None
     | _,_ => None
     end
-  | ReadSR dst src =>
+  | SpecialRW dst csr src =>
       if has_sreg_access plevel
-      then tomov ← (sreg φ) !! src; updatePC (update_reg φ dst tomov)
-      else None
-  | WriteSR dst src =>
-      if has_sreg_access plevel
-      then tomov ← (reg φ) !!ᵣ src; updatePC (update_sreg φ dst tomov)
+      then
+        csr_val ← (sreg φ) !! csr;
+        if (decide (src = cnull))
+        then updatePC (update_reg φ dst csr_val)
+        else
+          src_val ← (reg φ) !!ᵣ src;
+          updatePC (update_reg (update_sreg φ csr src_val) dst csr_val)
       else None
   end.
 
diff --git a/theories/opsem/machine_base.v b/theories/opsem/machine_base.v
index 50efe930..ae17aca3 100644
--- a/theories/opsem/machine_base.v
+++ b/theories/opsem/machine_base.v
@@ -146,8 +146,7 @@ Inductive instr: Type :=
 | Seal (dst : RegName) (r1 r2: RegName)
 | UnSeal (dst : RegName) (r1 r2: RegName)
 (* Separate SpecialRW into 2 instructions *)
-| ReadSR (dst: RegName) (src: SRegName)
-| WriteSR (dst: SRegName) (src: RegName)
+| SpecialRW (dst: RegName) (csr : SRegName) (src: RegName)
 | Fail
 | Halt.
 
@@ -1528,16 +1527,15 @@ Proof.
 
       | Seal dst r1 r2 => GenNode 18 [GenLeaf (inl (inl dst)); GenLeaf (inl (inl r1)); GenLeaf (inl (inl r2))]
       | UnSeal dst r1 r2 => GenNode 19 [GenLeaf (inl (inl dst)); GenLeaf (inl (inl r1)); GenLeaf (inl (inl r2))]
-      | ReadSR dst src => GenNode 20 [GenLeaf (inl (inl dst)); GenLeaf (inl (inr src))]
-      | WriteSR dst src => GenNode 21 [GenLeaf (inl (inr dst)); GenLeaf (inl (inl src))]
-      | Fail => GenNode 22 []
-      | Halt => GenNode 23 []
-      | Mul dst r1 r2 => GenNode 24 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)]
-      | LAnd dst r1 r2 => GenNode 25 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)]
-      | LOr dst r1 r2 => GenNode 26 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)]
-      | LShiftL dst r1 r2 => GenNode 27 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)]
-      | LShiftR dst r1 r2 => GenNode 28 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)]
-      | Jalr dst src => GenNode 29 [GenLeaf (inl (inl dst));GenLeaf (inl (inl src))]
+      | SpecialRW dst csr src => GenNode 20 [GenLeaf (inl (inl dst)); GenLeaf (inl (inr csr)); GenLeaf (inl (inl src))]
+      | Fail => GenNode 21 []
+      | Halt => GenNode 22 []
+      | Mul dst r1 r2 => GenNode 23 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)]
+      | LAnd dst r1 r2 => GenNode 24 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)]
+      | LOr dst r1 r2 => GenNode 25 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)]
+      | LShiftL dst r1 r2 => GenNode 26 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)]
+      | LShiftR dst r1 r2 => GenNode 27 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)]
+      | Jalr dst src => GenNode 28 [GenLeaf (inl (inl dst));GenLeaf (inl (inl src))]
       end).
   set (dec := fun e =>
       match e with
@@ -1563,16 +1561,16 @@ Proof.
 
       | GenNode 18 [GenLeaf (inl (inl dst)); GenLeaf (inl (inl r1)); GenLeaf (inl (inl r2))] => Seal dst r1 r2
       | GenNode 19 [GenLeaf (inl (inl dst)); GenLeaf (inl (inl r1)); GenLeaf (inl (inl r2))] => UnSeal dst r1 r2
-      | GenNode 20 [GenLeaf (inl (inl dst)); GenLeaf (inl (inr src))] => ReadSR dst src
-      | GenNode 21 [GenLeaf (inl (inr dst)); GenLeaf (inl (inl src))] => WriteSR dst src
-      | GenNode 22 [] => Fail
-      | GenNode 23 [] => Halt
-      | GenNode 24 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)] => Mul dst r1 r2
-      | GenNode 25 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)] => LAnd dst r1 r2
-      | GenNode 26 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)] => LOr dst r1 r2
-      | GenNode 27 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)] => LShiftL dst r1 r2
-      | GenNode 28 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)] => LShiftR dst r1 r2
-      | GenNode 29 [GenLeaf (inl (inl dst));GenLeaf (inl (inl src))] => Jalr dst src
+      | GenNode 20 [GenLeaf (inl (inl dst)); GenLeaf (inl (inr csr)); GenLeaf (inl (inl src))]
+        => SpecialRW dst csr src
+      | GenNode 21 [] => Fail
+      | GenNode 22 [] => Halt
+      | GenNode 23 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)] => Mul dst r1 r2
+      | GenNode 24 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)] => LAnd dst r1 r2
+      | GenNode 25 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)] => LOr dst r1 r2
+      | GenNode 26 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)] => LShiftL dst r1 r2
+      | GenNode 27 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)] => LShiftR dst r1 r2
+      | GenNode 28 [GenLeaf (inl (inl dst));GenLeaf (inl (inl src))] => Jalr dst src
       | _ => Fail (* dummy *)
       end).
   refine (inj_countable' enc dec _).
diff --git a/theories/program_logic/rules.v b/theories/program_logic/rules.v
index bb0fa529..c3cc9add 100644
--- a/theories/program_logic/rules.v
+++ b/theories/program_logic/rules.v
@@ -5,7 +5,7 @@ From cap_machine Require Export
      rules_Lea rules_Mov rules_Restrict rules_Subseg
      rules_Jmp rules_Jnz rules_Jalr
      rules_Seal rules_UnSeal
-     rules_ReadSR rules_WriteSR.
+     rules_SpecialRW.
 
 (* Program specifications
 
diff --git a/theories/program_logic/rules/rules_ReadSR.v b/theories/program_logic/rules/rules_ReadSR.v
deleted file mode 100644
index f44514c5..00000000
--- a/theories/program_logic/rules/rules_ReadSR.v
+++ /dev/null
@@ -1,194 +0,0 @@
-From iris.base_logic Require Export invariants gen_heap.
-From iris.program_logic Require Export weakestpre ectx_lifting.
-From iris.proofmode Require Import proofmode.
-From iris.algebra Require Import frac.
-From cap_machine Require Export rules_base.
-
-Section cap_lang_rules.
-  Context `{MP: MachineParameters}.
-  Context `{ceriseg: ceriseG Σ}.
-  Implicit Types P Q : iProp Σ.
-  Implicit Types σ : ExecConf.
-  Implicit Types c : cap_lang.expr.
-  Implicit Types a b : Addr.
-  Implicit Types r : RegName.
-  Implicit Types v : cap_lang.val.
-  Implicit Types w : Word.
-  Implicit Types reg : gmap RegName Word.
-  Implicit Types sreg : gmap SRegName Word.
-  Implicit Types ms : gmap Addr Word.
-
-  Inductive ReadSR_failure (regs: Reg) (sregs : SReg) (dst: RegName) (src: SRegName) :=
-  | ReadSR_fail_nonxrs p g b e a:
-      regs !! PC = Some (WCap p g b e a) →
-      has_sreg_access p = false ->
-      ReadSR_failure regs sregs dst src
-  | ReadSR_fail_incrPC p g b e a w:
-      regs !! PC = Some (WCap p g b e a) →
-      sregs !! src = Some w →
-      incrementPC (<[ dst := w ]ᵣ> regs) = None →
-      ReadSR_failure regs sregs dst src
-  .
-
-  Inductive ReadSR_spec
-  (regs: Reg) (sregs: SReg) (dst: RegName) (src: SRegName) (regs': Reg)
-    : cap_lang.val -> Prop :=
-  | ReadSR_spec_success p g b e a w:
-      regs !! PC = Some (WCap p g b e a) →
-      has_sreg_access p = true ->
-      sregs !! src = Some w →
-      incrementPC (<[ dst := w ]ᵣ> regs) = Some regs' →
-      ReadSR_spec regs sregs dst src regs' NextIV
-  | ReadSR_spec_failure:
-      ReadSR_failure regs sregs dst src →
-      ReadSR_spec regs sregs dst src regs' FailedV.
-
-  Lemma wp_ReadSR Ep pc_p pc_g pc_b pc_e pc_a w dst src regs sregs :
-    decodeInstrW w = ReadSR dst src ->
-    isCorrectPC (WCap pc_p pc_g pc_b pc_e pc_a) →
-    regs !! PC = Some (WCap pc_p pc_g pc_b pc_e pc_a) →
-    regs_of (ReadSR dst src) ⊆ dom regs →
-    (if (has_sreg_access pc_p)
-    then sregs_of (ReadSR dst src) ⊆ dom sregs
-    else True) →
-    {{{ ▷ pc_a ↦ₐ w ∗
-        ▷ ([∗ map] k↦y ∈ regs, k ↦ᵣ y) ∗
-        ▷ ([∗ map] k↦y ∈ sregs, k ↦ₛᵣ y)
-    }}}
-      Instr Executable @ Ep
-    {{{ regs' retv, RET retv;
-        ⌜ ReadSR_spec regs sregs dst src regs' retv ⌝ ∗
-        pc_a ↦ₐ w ∗
-        ([∗ map] k↦y ∈ regs', k ↦ᵣ y) ∗
-        ([∗ map] k↦y ∈ sregs, k ↦ₛᵣ y)
-    }}}.
-  Proof.
-    iIntros (Hinstr Hvpc HPC Dregs Dsregs φ) "(>Hpc_a & >Hmap & >Hsmap) Hφ".
-    iApply wp_lift_atomic_base_step_no_fork; auto.
-    iIntros (σ1 ns l1 l2 nt) "[ [Hr Hsr] Hm ] /=". destruct σ1 as [ [r sr] m]; cbn.
-    iDestruct (gen_heap_valid_inclSepM with "Hr Hmap") as %Hregs.
-    iDestruct (gen_heap_valid_inclSepM with "Hsr Hsmap") as %Hsregs.
-    have ? := lookup_weaken _ _ _ _ HPC Hregs.
-    iDestruct (@gen_heap_valid with "Hm Hpc_a") as %Hpc_a; auto.
-    iModIntro. iSplitR; first (by iPureIntro; apply normal_always_base_reducible).
-    iNext. iIntros (e2 σ2 efs Hpstep).
-    apply prim_step_exec_inv in Hpstep as (-> & -> & (c & -> & Hstep)).
-    iIntros "_".
-    iSplitR; auto. eapply step_exec_inv in Hstep; eauto.
-    unfold exec in Hstep.
-
-    specialize (indom_regs_incl _ _ _ Dregs Hregs) as Hri. unfold regs_of in Hri.
-    destruct (Hri dst) as [wdst [H'dst Hdst]]; first by set_solver+.
-
-    destruct (has_sreg_access pc_p) eqn:Hxsr; cycle 1.
-    { cbn in Hstep. rewrite Hxsr in Hstep.
-      simplify_eq.
-      iFailWP "Hφ" ReadSR_fail_nonxrs.
-    }
-
-    specialize (indom_sregs_incl _ _ _ Dsregs Hsregs) as Hsri. unfold sregs_of in Hsri.
-    destruct (Hsri src) as [wsrc [H'src Hsrc]]; first by set_solver+.
-
-    assert (exec_opt (ReadSR dst src) pc_p (r, sr, m) = updatePC (update_reg (r, sr, m) dst wsrc)) as HH.
-    { by cbn; rewrite Hsrc Hxsr /=. }
-    rewrite HH in Hstep. rewrite /update_reg /= in Hstep.
-
-    destruct (incrementPC (<[ dst := wsrc ]ᵣ> regs)) as [regs'|] eqn:Hregs'
-    ; pose proof Hregs' as H'regs'; cycle 1.
-    { apply incrementPC_fail_updatePC with (sregs:=sr) (m:=m) in Hregs'.
-      eapply updatePC_fail_incl with (sregs':=sr) (m':=m) in Hregs'.
-      2: by apply lookup_insert_is_Some'; eauto.
-      2: by apply insert_mono; eauto.
-      rewrite Hregs' in Hstep. simplify_pair_eq.
-      iFailWP "Hφ" ReadSR_fail_incrPC.
-    }
-
-    eapply (incrementPC_success_updatePC _ sr m) in Hregs'
-      as (p' & g' & b' & e' & a'' & a''' & a_pc' & HPC'' & HuPC & ->).
-    eapply updatePC_success_incl with (sregs':=sr) (m':=m) in HuPC. 2: by eapply insert_mono; eauto.
-    rewrite HuPC in Hstep. simplify_pair_eq. iFrame.
-    iMod ((gen_heap_update_inSepM _ _ dst) with "Hr Hmap") as "[Hr Hmap]"; eauto.
-    { apply is_Some_lookup_reg; done. }
-    iMod ((gen_heap_update_inSepM _ _ PC) with "Hr Hmap") as "[Hr Hmap]"; eauto.
-    iFrame. iModIntro. iApply "Hφ". iFrame. iPureIntro. econstructor; eauto.
-  Qed.
-
-  Lemma wp_readsr_success E pc_p pc_g pc_b pc_e pc_a pc_a' w dst wdst src wsrc :
-    decodeInstrW w = ReadSR dst src →
-    isCorrectPC (WCap pc_p pc_g pc_b pc_e pc_a) →
-    has_sreg_access pc_p = true →
-    (pc_a + 1)%a = Some pc_a' →
-    dst ≠ cnull ->
-
-    {{{ ▷ PC ↦ᵣ WCap pc_p pc_g pc_b pc_e pc_a
-        ∗ ▷ pc_a ↦ₐ w
-        ∗ ▷ dst ↦ᵣ wdst
-        ∗ ▷ src ↦ₛᵣ wsrc }}}
-      Instr Executable @ E
-      {{{ RET NextIV;
-          PC ↦ᵣ WCap pc_p pc_g pc_b pc_e pc_a'
-          ∗ pc_a ↦ₐ w
-          ∗ dst ↦ᵣ wsrc
-          ∗ src ↦ₛᵣ wsrc }}}.
-  Proof.
-    iIntros (Hinstr Hvpc Hxsr Hpca' Hcnull ϕ) "(>HPC & >Hpc_a & >Hdst & >Hsrc) Hφ".
-    iDestruct (map_of_regs_2 with "HPC Hdst") as "[Hmap %]".
-    iDestruct (map_of_sregs_1 with "Hsrc") as "Hsmap".
-    iApply (wp_ReadSR with "[$Hmap $Hsmap Hpc_a]"); eauto; simplify_map_eq; eauto.
-    - by unfold regs_of; rewrite !dom_insert; set_solver+.
-    - by unfold sregs_of; rewrite Hxsr !dom_insert; set_solver+.
-    - iNext. iIntros (regs' retv) "(#Hspec & Hpc_a & Hmap & Hsmap)". iDestruct "Hspec" as %Hspec.
-
-    destruct Hspec as [| Hfail].
-    { (* Success *)
-      iApply "Hφ". iFrame. incrementPC_inv; simplify_map_eq.
-      rewrite (insert_commute _ PC dst) // insert_insert (insert_commute _ PC dst) // insert_insert.
-      iDestruct (regs_of_map_2 with "Hmap") as "(?&?&?)"; eauto; iFrame.
-      iDestruct (sregs_of_map_1 with "Hsmap") as "?"; eauto; iFrame.
-    }
-    { (* Failure (contradiction) *)
-      destruct Hfail.
-      - simplify_map_eq; eauto; congruence.
-      - incrementPC_inv; simplify_map_eq; eauto.
-        congruence.
-    }
-  Qed.
-
-  Lemma wp_readsr_success_toPC E pc_p pc_g pc_b pc_e pc_a w src p g b e a a':
-    decodeInstrW w = ReadSR PC src →
-    isCorrectPC (WCap pc_p pc_g pc_b pc_e pc_a) →
-    has_sreg_access pc_p = true →
-    (a + 1)%a = Some a' →
-
-    {{{ ▷ PC ↦ᵣ WCap pc_p pc_g pc_b pc_e pc_a
-        ∗ ▷ pc_a ↦ₐ w
-        ∗ ▷ src ↦ₛᵣ WCap p g b e a }}}
-      Instr Executable @ E
-      {{{ RET NextIV;
-          PC ↦ᵣ WCap p g b e a'
-          ∗ pc_a ↦ₐ w
-          ∗ src ↦ₛᵣ WCap p g b e a }}}.
-  Proof.
-    iIntros (Hinstr Hvpc Hxsr Hpca' ϕ) "(>HPC & >Hpc_a & >Hsrc) Hφ".
-    iDestruct (map_of_regs_1 with "HPC") as "Hmap".
-    iDestruct (map_of_sregs_1 with "Hsrc") as "Hsmap".
-    iApply (wp_ReadSR with "[$Hmap $Hsmap Hpc_a]"); eauto; simplify_map_eq; eauto.
-    { by unfold sregs_of; rewrite Hxsr !dom_insert; set_solver+. }
-    iNext. iIntros (regs' retv) "(#Hspec & Hpc_a & Hmap & Hsmap)". iDestruct "Hspec" as %Hspec.
-
-    destruct Hspec as [|Hfail].
-    { (* Success *)
-      iApply "Hφ". iFrame. incrementPC_inv; simplify_map_eq.
-      rewrite !insert_insert.
-      iDestruct (regs_of_map_1 with "Hmap") as "?"; eauto; iFrame.
-      iDestruct (sregs_of_map_1 with "Hsmap") as "?"; eauto; iFrame.
-    }
-    { (* Failure (contradiction) *)
-      destruct Hfail.
-      - simplify_map_eq; eauto; congruence.
-      - incrementPC_inv; simplify_map_eq; eauto.
-        congruence.
-    }
-  Qed.
-
-End cap_lang_rules.
diff --git a/theories/program_logic/rules/rules_SpecialRW.v b/theories/program_logic/rules/rules_SpecialRW.v
new file mode 100644
index 00000000..2e71cb7d
--- /dev/null
+++ b/theories/program_logic/rules/rules_SpecialRW.v
@@ -0,0 +1,328 @@
+From iris.base_logic Require Export invariants gen_heap.
+From iris.program_logic Require Export weakestpre ectx_lifting.
+From iris.proofmode Require Import proofmode.
+From iris.algebra Require Import frac.
+From cap_machine Require Export rules_base.
+
+Section cap_lang_rules.
+  Context `{MP: MachineParameters}.
+  Context `{ceriseg: ceriseG Σ}.
+  Implicit Types P Q : iProp Σ.
+  Implicit Types σ : ExecConf.
+  Implicit Types c : cap_lang.expr.
+  Implicit Types a b : Addr.
+  Implicit Types r : RegName.
+  Implicit Types v : cap_lang.val.
+  Implicit Types w : Word.
+  Implicit Types reg : gmap RegName Word.
+  Implicit Types sreg : gmap SRegName Word.
+  Implicit Types ms : gmap Addr Word.
+
+  Inductive SpecialRW_failure (regs: Reg) (sregs : SReg) (dst: RegName) (csr: SRegName) (src: RegName) :=
+  | SpecialRW_fail_nonxrs p g b e a:
+      regs !! PC = Some (WCap p g b e a) →
+      has_sreg_access p = false ->
+      SpecialRW_failure regs sregs dst csr src
+  | SpecialRW_fail_incrPC p g b e a w:
+      regs !! PC = Some (WCap p g b e a) →
+      sregs !! csr = Some w →
+      incrementPC (<[ dst := w ]ᵣ> regs) = None →
+      SpecialRW_failure regs sregs dst csr src
+  .
+
+  Inductive SpecialRW_spec
+    (regs regs': Reg) (sregs sregs': SReg) (dst: RegName) (csr: SRegName) (src: RegName)
+    : cap_lang.val -> Prop :=
+  | SpecialRW_spec_success p g b e a w w':
+    regs !! PC = Some (WCap p g b e a) →
+    has_sreg_access p = true ->
+    src ≠ cnull ->
+    regs !!ᵣ src = Some w' →
+    sregs !! csr = Some w →
+    incrementPC (<[ dst := w ]ᵣ> regs) = Some regs' →
+    sregs' = (<[csr := w']> sregs) →
+    SpecialRW_spec regs regs' sregs sregs' dst csr src NextIV
+  | SpecialRW_spec_success' p g b e a w:
+    regs !! PC = Some (WCap p g b e a) →
+    has_sreg_access p = true ->
+    src = cnull ->
+    sregs !! csr = Some w →
+    incrementPC (<[ dst := w ]ᵣ> regs) = Some regs' →
+    sregs' = sregs →
+    SpecialRW_spec regs regs' sregs sregs' dst csr src NextIV
+  | SpecialRW_spec_failure:
+    sregs = sregs' ->
+    SpecialRW_failure regs sregs dst csr src →
+    SpecialRW_spec regs regs' sregs sregs' dst csr src FailedV.
+
+  Lemma wp_SpecialRW Ep pc_p pc_g pc_b pc_e pc_a w dst csr src regs sregs :
+    decodeInstrW w = SpecialRW dst csr src ->
+    isCorrectPC (WCap pc_p pc_g pc_b pc_e pc_a) →
+    regs !! PC = Some (WCap pc_p pc_g pc_b pc_e pc_a) →
+    regs_of (SpecialRW dst csr src) ⊆ dom regs →
+    (if (has_sreg_access pc_p)
+    then sregs_of (SpecialRW dst csr src) ⊆ dom sregs
+    else True) →
+    {{{ ▷ pc_a ↦ₐ w ∗
+        ▷ ([∗ map] k↦y ∈ regs, k ↦ᵣ y) ∗
+        ▷ ([∗ map] k↦y ∈ sregs, k ↦ₛᵣ y)
+    }}}
+      Instr Executable @ Ep
+    {{{ regs' sregs' retv, RET retv;
+        ⌜ SpecialRW_spec regs regs' sregs sregs' dst csr src retv ⌝ ∗
+        pc_a ↦ₐ w ∗
+        ([∗ map] k↦y ∈ regs', k ↦ᵣ y) ∗
+        ([∗ map] k↦y ∈ sregs', k ↦ₛᵣ y)
+    }}}.
+  Proof.
+    iIntros (Hinstr Hvpc HPC Dregs Dsregs φ) "(>Hpc_a & >Hmap & >Hsmap) Hφ".
+    iApply wp_lift_atomic_base_step_no_fork; auto.
+    iIntros (σ1 ns l1 l2 nt) "[ [Hr Hsr] Hm ] /=". destruct σ1 as [ [r sr] m]; cbn.
+    iDestruct (gen_heap_valid_inclSepM with "Hr Hmap") as %Hregs.
+    iDestruct (gen_heap_valid_inclSepM with "Hsr Hsmap") as %Hsregs.
+    have ? := lookup_weaken _ _ _ _ HPC Hregs.
+    iDestruct (@gen_heap_valid with "Hm Hpc_a") as %Hpc_a; auto.
+    iModIntro. iSplitR; first (by iPureIntro; apply normal_always_base_reducible).
+    iNext. iIntros (e2 σ2 efs Hpstep).
+    apply prim_step_exec_inv in Hpstep as (-> & -> & (c & -> & Hstep)).
+    iIntros "_".
+    iSplitR; auto. eapply step_exec_inv in Hstep; eauto.
+    unfold exec in Hstep.
+
+    specialize (indom_regs_incl _ _ _ Dregs Hregs) as Hri. unfold regs_of in Hri.
+    destruct (Hri dst) as [wdst [H'dst Hdst]]; first (by (destruct (decide (src = cnull)); set_solver+)).
+
+    destruct (has_sreg_access pc_p) eqn:Hxsr; cycle 1.
+    { cbn in Hstep.
+      rewrite Hxsr in Hstep; simplify_eq.
+      iFailWP "Hφ" SpecialRW_fail_nonxrs.
+    }
+
+    specialize (indom_sregs_incl _ _ _ Dsregs Hsregs) as Hsri. unfold sregs_of in Hsri.
+    destruct (Hsri csr) as [wcsr [H'csr Hcsr]]; first by set_solver+.
+
+    destruct (decide (src = cnull)) as [Hsrc_cnull|Hsrc_cnull].
+    - assert (exec_opt (SpecialRW dst csr src) pc_p (r, sr, m) = updatePC (update_reg (r, sr, m) dst wcsr)) as HH.
+      { cbn; rewrite Hcsr Hxsr Hsrc_cnull /=; destruct (decide _) as [_|?]; done. }
+      rewrite HH in Hstep. rewrite /update_sreg /= in Hstep.
+
+      destruct (incrementPC (<[ dst := wcsr ]ᵣ> regs)) as [regs'|] eqn:Hregs'
+      ; pose proof Hregs' as H'regs'; cycle 1.
+      { apply incrementPC_fail_updatePC with (sregs:=sr) (m:=m) in Hregs'.
+        eapply updatePC_fail_incl with (sregs':=sr) (m':=m) in Hregs'.
+        2: by apply lookup_insert_is_Some'; eauto.
+        2: by apply insert_mono; eauto.
+        rewrite Hregs' in Hstep. simplify_pair_eq.
+        iFailWP "Hφ" SpecialRW_fail_incrPC.
+      }
+
+      eapply (incrementPC_success_updatePC _ sr m) in Hregs'
+          as (p' & g' & b' & e' & a'' & a''' & a_pc' & HPC'' & HuPC & ->).
+      eapply updatePC_success_incl with (sregs':=sr) (m':=m) in HuPC. 2: by eapply insert_mono; eauto.
+      rewrite HuPC in Hstep. simplify_pair_eq. iFrame.
+      iMod ((gen_heap_update_inSepM _ _ dst) with "Hr Hmap") as "[Hr Hmap]"; eauto.
+      { apply is_Some_lookup_reg; done. }
+      iMod ((gen_heap_update_inSepM _ _ PC) with "Hr Hmap") as "[Hr Hmap]"; eauto.
+      iFrame. iModIntro. iApply "Hφ". iFrame. iPureIntro. econstructor 2; eauto.
+    - destruct (Hri src) as [wsrc [H'src Hsrc]]; first by set_solver+.
+      assert (exec_opt (SpecialRW dst csr src) pc_p (r, sr, m)
+              = updatePC (update_reg (update_sreg (r, sr, m) csr wsrc) dst wcsr)) as HH.
+      { cbn. rewrite Hcsr Hxsr Hsrc /=; destruct (decide _) as [?|?]; done. }
+      rewrite HH in Hstep. rewrite /update_sreg /= in Hstep.
+
+      destruct (incrementPC (<[ dst := wcsr ]ᵣ> regs)) as [regs'|] eqn:Hregs'
+      ; pose proof Hregs' as H'regs'; cycle 1.
+      { apply incrementPC_fail_updatePC with (sregs:=sr) (m:=m) in Hregs'.
+        eapply updatePC_fail_incl with (sregs':= <[csr:=wsrc]>sr) (m':=m) in Hregs'.
+        2: by apply lookup_insert_is_Some'; eauto.
+        2: by apply insert_mono; eauto.
+        rewrite Hregs' in Hstep. simplify_pair_eq.
+        iFailWP "Hφ" SpecialRW_fail_incrPC.
+      }
+
+      eapply (incrementPC_success_updatePC _ (<[csr:=wsrc]> sr) m) in Hregs'
+          as (p' & g' & b' & e' & a'' & a''' & a_pc' & HPC'' & HuPC & ->).
+      eapply updatePC_success_incl with (sregs':=<[csr:=wsrc]>sr) (m':=m) in HuPC.
+      2: by eapply insert_mono; eauto.
+      rewrite HuPC in Hstep. simplify_pair_eq. iFrame.
+      iMod ((gen_heap_update_inSepM _ _ csr) with "Hsr Hsmap") as "[Hsr Hsmap]"; eauto.
+      iMod ((gen_heap_update_inSepM _ _ dst) with "Hr Hmap") as "[Hr Hmap]"; eauto.
+      { apply is_Some_lookup_reg; done. }
+      iMod ((gen_heap_update_inSepM _ _ PC) with "Hr Hmap") as "[Hr Hmap]"; eauto.
+      iFrame. iModIntro. iApply "Hφ". iFrame. iPureIntro. econstructor 1; eauto.
+  Qed.
+
+  Lemma wp_specialrw_success E pc_p pc_g pc_b pc_e pc_a pc_a' w dst wdst csr wcsr src wsrc :
+    decodeInstrW w = SpecialRW dst csr src →
+    isCorrectPC (WCap pc_p pc_g pc_b pc_e pc_a) →
+    has_sreg_access pc_p = true →
+    (pc_a + 1)%a = Some pc_a' →
+    src ≠ cnull ->
+    dst ≠ cnull ->
+
+    {{{ ▷ PC ↦ᵣ WCap pc_p pc_g pc_b pc_e pc_a
+        ∗ ▷ pc_a ↦ₐ w
+        ∗ ▷ dst ↦ᵣ wdst
+        ∗ ▷ csr ↦ₛᵣ wcsr
+        ∗ ▷ src ↦ᵣ wsrc }}}
+      Instr Executable @ E
+      {{{ RET NextIV;
+          PC ↦ᵣ WCap pc_p pc_g pc_b pc_e pc_a'
+          ∗ pc_a ↦ₐ w
+          ∗ dst ↦ᵣ wcsr
+          ∗ csr ↦ₛᵣ wsrc
+          ∗ src ↦ᵣ wsrc }}}.
+  Proof.
+    iIntros (Hinstr Hvpc Hxsr Hpca' ?? ϕ) "(>HPC & >Hpc_a & >Hdst & >Hcsr & >Hsrc) Hφ".
+    iDestruct (map_of_regs_3 with "HPC Hdst Hsrc") as "[Hmap (%&%&%)]".
+    iDestruct (map_of_sregs_1 with "Hcsr") as "Hsmap".
+    iApply (wp_SpecialRW with "[$Hmap $Hsmap Hpc_a]"); eauto; simplify_map_eq; eauto.
+    - by unfold regs_of; rewrite !dom_insert; set_solver+.
+    - by unfold sregs_of; rewrite Hxsr !dom_insert; set_solver+.
+    - iNext. iIntros (regs' sregs' retv) "(#Hspec & Hpc_a & Hmap & Hsmap)". iDestruct "Hspec" as %Hspec.
+
+    destruct Hspec as [| | -> Hfail].
+    { (* Success *)
+      iApply "Hφ". iFrame. incrementPC_inv; simplify_map_eq.
+      rewrite (insert_commute _ PC dst) // insert_insert (insert_commute _ PC dst) // insert_insert.
+      iDestruct (regs_of_map_3 with "Hmap") as "(?&?&?)"; eauto; iFrame.
+      rewrite insert_insert.
+      iDestruct (sregs_of_map_1 with "Hsmap") as "?"; eauto; iFrame.
+    }
+    { (* Success' (contradiction) *) done. }
+    { (* Failure (contradiction) *)
+      destruct Hfail.
+      - simplify_map_eq; eauto; congruence.
+      - incrementPC_inv; simplify_map_eq; eauto.
+        congruence.
+    }
+  Qed.
+
+  Lemma wp_specialrw_readsr E pc_p pc_g pc_b pc_e pc_a pc_a' w dst wdst csr wcsr :
+    decodeInstrW w = SpecialRW dst csr cnull →
+    isCorrectPC (WCap pc_p pc_g pc_b pc_e pc_a) →
+    has_sreg_access pc_p = true →
+    (pc_a + 1)%a = Some pc_a' →
+    dst ≠ cnull ->
+
+    {{{ ▷ PC ↦ᵣ WCap pc_p pc_g pc_b pc_e pc_a
+        ∗ ▷ pc_a ↦ₐ w
+        ∗ ▷ dst ↦ᵣ wdst
+        ∗ ▷ csr ↦ₛᵣ wcsr
+        }}}
+      Instr Executable @ E
+      {{{ RET NextIV;
+          PC ↦ᵣ WCap pc_p pc_g pc_b pc_e pc_a'
+          ∗ pc_a ↦ₐ w
+          ∗ dst ↦ᵣ wcsr
+          ∗ csr ↦ₛᵣ wcsr
+          }}}.
+  Proof.
+    iIntros (Hinstr Hvpc Hxsr Hpca' ? ϕ) "(>HPC & >Hpc_a & >Hdst & >Hcsr) Hφ".
+    iDestruct (map_of_regs_2 with "HPC Hdst") as "[Hmap %]".
+    iDestruct (map_of_sregs_1 with "Hcsr") as "Hsmap".
+    iApply (wp_SpecialRW with "[$Hmap $Hsmap Hpc_a]"); eauto; simplify_map_eq; eauto.
+    - by unfold regs_of; rewrite !dom_insert; set_solver+.
+    - by unfold sregs_of; rewrite Hxsr !dom_insert; set_solver+.
+    - iNext. iIntros (regs' sregs' retv) "(#Hspec & Hpc_a & Hmap & Hsmap)". iDestruct "Hspec" as %Hspec.
+
+    destruct Hspec as [| | -> Hfail].
+    { (* Success (contradiction) *) done. }
+    { (* Success *)
+      iApply "Hφ". iFrame. incrementPC_inv; simplify_map_eq.
+      rewrite (insert_commute _ PC dst) // insert_insert (insert_commute _ PC dst) // insert_insert.
+      iDestruct (regs_of_map_2 with "Hmap") as "(?&?&?)"; eauto; iFrame.
+      iDestruct (sregs_of_map_1 with "Hsmap") as "?"; eauto; iFrame.
+    }
+    { (* Failure (contradiction) *)
+      destruct Hfail.
+      - simplify_map_eq; eauto; congruence.
+      - incrementPC_inv; simplify_map_eq; eauto.
+        congruence.
+    }
+  Qed.
+
+  Lemma wp_specialrw_writesr E pc_p pc_g pc_b pc_e pc_a pc_a' w wcnull csr wcsr src wsrc :
+    decodeInstrW w = SpecialRW cnull csr src →
+    isCorrectPC (WCap pc_p pc_g pc_b pc_e pc_a) →
+    has_sreg_access pc_p = true →
+    (pc_a + 1)%a = Some pc_a' →
+    src ≠ cnull ->
+
+    {{{ ▷ PC ↦ᵣ WCap pc_p pc_g pc_b pc_e pc_a
+        ∗ ▷ pc_a ↦ₐ w
+        ∗ ▷ cnull ↦ᵣ wcnull
+        ∗ ▷ csr ↦ₛᵣ wcsr
+        ∗ ▷ src ↦ᵣ wsrc }}}
+      Instr Executable @ E
+      {{{ RET NextIV;
+          PC ↦ᵣ WCap pc_p pc_g pc_b pc_e pc_a'
+          ∗ pc_a ↦ₐ w
+          ∗ cnull ↦ᵣ WInt 0
+          ∗ csr ↦ₛᵣ wsrc
+          ∗ src ↦ᵣ wsrc }}}.
+  Proof.
+    iIntros (Hinstr Hvpc Hxsr Hpca' ? ϕ) "(>HPC & >Hpc_a & >Hcnull & >Hcsr & >Hsrc) Hφ".
+    iDestruct (map_of_regs_3 with "HPC Hcnull Hsrc") as "[Hmap (%&%&%)]".
+    iDestruct (map_of_sregs_1 with "Hcsr") as "Hsmap".
+    iApply (wp_SpecialRW with "[$Hmap $Hsmap Hpc_a]"); eauto; simplify_map_eq; eauto.
+    - by unfold regs_of; rewrite !dom_insert; set_solver+.
+    - by unfold sregs_of; rewrite Hxsr !dom_insert; set_solver+.
+    - iNext. iIntros (regs' sregs' retv) "(#Hspec & Hpc_a & Hmap & Hsmap)". iDestruct "Hspec" as %Hspec.
+
+    destruct Hspec as [| | -> Hfail].
+    { (* Success *)
+      iApply "Hφ". iFrame. incrementPC_inv; simplify_map_eq.
+      rewrite (insert_commute _ PC cnull) // insert_insert (insert_commute _ PC cnull) // insert_insert.
+      iDestruct (regs_of_map_3 with "Hmap") as "(?&?&?)"; eauto; iFrame.
+      rewrite insert_insert.
+      iDestruct (sregs_of_map_1 with "Hsmap") as "?"; eauto; iFrame.
+    }
+    { (* Success' (contradiction) *) done. }
+    { (* Failure (contradiction) *)
+      destruct Hfail.
+      - simplify_map_eq; eauto; congruence.
+      - incrementPC_inv; simplify_map_eq; eauto.
+        congruence.
+    }
+  Qed.
+
+  (* Lemma wp_specialsr_success_fromPC E pc_p pc_g pc_b pc_e pc_a pc_a' w dst wdst : *)
+  (*   decodeInstrW w = WriteSR dst PC → *)
+  (*   isCorrectPC (WCap pc_p pc_g pc_b pc_e pc_a) → *)
+  (*   has_sreg_access pc_p = true → *)
+  (*   (pc_a + 1)%a = Some pc_a' → *)
+
+  (*   {{{ ▷ PC ↦ᵣ WCap pc_p pc_g pc_b pc_e pc_a *)
+  (*       ∗ ▷ pc_a ↦ₐ w *)
+  (*       ∗ ▷ dst ↦ₛᵣ wdst }}} *)
+  (*     Instr Executable @ E *)
+  (*     {{{ RET NextIV; *)
+  (*         PC ↦ᵣ WCap pc_p pc_g pc_b pc_e pc_a' *)
+  (*         ∗ pc_a ↦ₐ w *)
+  (*         ∗ dst ↦ₛᵣ WCap pc_p pc_g pc_b pc_e pc_a }}}. *)
+  (* Proof. *)
+  (*   iIntros (Hinstr Hvpc Hxsr Hpca' ϕ) "(>HPC & >Hpc_a & >Hdst) Hφ". *)
+  (*   iDestruct (map_of_regs_1 with "HPC") as "Hmap". *)
+  (*   iDestruct (map_of_sregs_1 with "Hdst") as "Hsmap". *)
+  (*   iApply (wp_WriteSR with "[$Hmap $Hsmap Hpc_a]"); eauto; simplify_map_eq; eauto. *)
+  (*   { by unfold sregs_of; rewrite Hxsr !dom_insert; set_solver+. } *)
+  (*   iNext. iIntros (regs' sregs' retv) "(#Hspec & Hpc_a & Hmap & Hsmap)". *)
+  (*   iDestruct "Hspec" as %Hspec. *)
+
+  (*   destruct Hspec as [| -> Hfail]. *)
+  (*   { (* Success *) *)
+  (*     iApply "Hφ". iFrame. incrementPC_inv; simplify_map_eq. *)
+  (*     rewrite !insert_insert. *)
+  (*     iDestruct (regs_of_map_1 with "Hmap") as "?"; eauto; iFrame. *)
+  (*     iDestruct (sregs_of_map_1 with "Hsmap") as "?"; eauto; iFrame. *)
+  (*   } *)
+  (*   { (* Failure (contradiction) *) *)
+  (*     destruct Hfail. *)
+  (*     - simplify_map_eq; eauto; congruence. *)
+  (*     - incrementPC_inv; simplify_map_eq; eauto. *)
+  (*       congruence. *)
+  (*   } *)
+  (* Qed. *)
+
+End cap_lang_rules.
diff --git a/theories/program_logic/rules/rules_WriteSR.v b/theories/program_logic/rules/rules_WriteSR.v
deleted file mode 100644
index 2a117dc3..00000000
--- a/theories/program_logic/rules/rules_WriteSR.v
+++ /dev/null
@@ -1,196 +0,0 @@
-From iris.base_logic Require Export invariants gen_heap.
-From iris.program_logic Require Export weakestpre ectx_lifting.
-From iris.proofmode Require Import proofmode.
-From iris.algebra Require Import frac.
-From cap_machine Require Export rules_base.
-
-Section cap_lang_rules.
-  Context `{MP: MachineParameters}.
-  Context `{ceriseg: ceriseG Σ}.
-  Implicit Types P Q : iProp Σ.
-  Implicit Types σ : ExecConf.
-  Implicit Types c : cap_lang.expr.
-  Implicit Types a b : Addr.
-  Implicit Types r : RegName.
-  Implicit Types v : cap_lang.val.
-  Implicit Types w : Word.
-  Implicit Types reg : gmap RegName Word.
-  Implicit Types sreg : gmap SRegName Word.
-  Implicit Types ms : gmap Addr Word.
-
-  Inductive WriteSR_failure (regs: Reg) (sregs : SReg) (dst: SRegName) (src: RegName) :=
-  | WriteSR_fail_nonxrs p g b e a:
-      regs !! PC = Some (WCap p g b e a) →
-      has_sreg_access p = false ->
-      WriteSR_failure regs sregs dst src
-  | WriteSR_fail_incrPC p g b e a w:
-      regs !! PC = Some (WCap p g b e a) →
-      regs !!ᵣ src = Some w →
-      incrementPC regs = None →
-      WriteSR_failure regs sregs dst src
-  .
-
-  Inductive WriteSR_spec
-    (regs regs': Reg) (sregs sregs': SReg) (dst: SRegName) (src: RegName)
-    : cap_lang.val -> Prop :=
-  | WriteSR_spec_success p g b e a w:
-    regs !! PC = Some (WCap p g b e a) →
-    has_sreg_access p = true ->
-    regs !!ᵣ src = Some w →
-    incrementPC regs = Some regs' →
-    sregs' = (<[dst := w]> sregs) →
-    WriteSR_spec regs regs' sregs sregs' dst src NextIV
-  | WriteSR_spec_failure:
-    sregs = sregs' ->
-    WriteSR_failure regs sregs dst src →
-    WriteSR_spec regs regs' sregs sregs' dst src FailedV.
-
-  Lemma wp_WriteSR Ep pc_p pc_g pc_b pc_e pc_a w dst src regs sregs :
-    decodeInstrW w = WriteSR dst src ->
-    isCorrectPC (WCap pc_p pc_g pc_b pc_e pc_a) →
-    regs !! PC = Some (WCap pc_p pc_g pc_b pc_e pc_a) →
-    regs_of (WriteSR dst src) ⊆ dom regs →
-    (if (has_sreg_access pc_p)
-    then sregs_of (WriteSR dst src) ⊆ dom sregs
-    else True) →
-    {{{ ▷ pc_a ↦ₐ w ∗
-        ▷ ([∗ map] k↦y ∈ regs, k ↦ᵣ y) ∗
-        ▷ ([∗ map] k↦y ∈ sregs, k ↦ₛᵣ y)
-    }}}
-      Instr Executable @ Ep
-    {{{ regs' sregs' retv, RET retv;
-        ⌜ WriteSR_spec regs regs' sregs sregs' dst src retv ⌝ ∗
-        pc_a ↦ₐ w ∗
-        ([∗ map] k↦y ∈ regs', k ↦ᵣ y) ∗
-        ([∗ map] k↦y ∈ sregs', k ↦ₛᵣ y)
-    }}}.
-  Proof.
-    iIntros (Hinstr Hvpc HPC Dregs Dsregs φ) "(>Hpc_a & >Hmap & >Hsmap) Hφ".
-    iApply wp_lift_atomic_base_step_no_fork; auto.
-    iIntros (σ1 ns l1 l2 nt) "[ [Hr Hsr] Hm ] /=". destruct σ1 as [ [r sr] m]; cbn.
-    iDestruct (gen_heap_valid_inclSepM with "Hr Hmap") as %Hregs.
-    iDestruct (gen_heap_valid_inclSepM with "Hsr Hsmap") as %Hsregs.
-    have ? := lookup_weaken _ _ _ _ HPC Hregs.
-    iDestruct (@gen_heap_valid with "Hm Hpc_a") as %Hpc_a; auto.
-    iModIntro. iSplitR; first (by iPureIntro; apply normal_always_base_reducible).
-    iNext. iIntros (e2 σ2 efs Hpstep).
-    apply prim_step_exec_inv in Hpstep as (-> & -> & (c & -> & Hstep)).
-    iIntros "_".
-    iSplitR; auto. eapply step_exec_inv in Hstep; eauto.
-    unfold exec in Hstep.
-
-    specialize (indom_regs_incl _ _ _ Dregs Hregs) as Hri. unfold regs_of in Hri.
-    destruct (Hri src) as [wsrc [H'src Hsrc]]; first by set_solver+.
-
-    destruct (has_sreg_access pc_p) eqn:Hxsr; cycle 1.
-    { cbn in Hstep.
-      rewrite Hxsr in Hstep; simplify_eq.
-      iFailWP "Hφ" WriteSR_fail_nonxrs.
-    }
-
-    specialize (indom_sregs_incl _ _ _ Dsregs Hsregs) as Hsri. unfold sregs_of in Hsri.
-    destruct (Hsri dst) as [wdst [H'dst Hdst]]; first by set_solver+.
-
-    assert (exec_opt (WriteSR dst src) pc_p (r, sr, m) = updatePC (update_sreg (r, sr, m) dst wsrc)) as HH.
-    { by cbn; rewrite Hsrc Hxsr /=. }
-    rewrite HH in Hstep. rewrite /update_sreg /= in Hstep.
-
-    destruct (incrementPC regs) as [regs'|] eqn:Hregs'
-    ; pose proof Hregs' as H'regs'; cycle 1.
-    { apply incrementPC_fail_updatePC with (sregs:=sr) (m:=m) in Hregs'.
-      eapply updatePC_fail_incl with (sregs':= <[dst:=wsrc]>sr) (m':=m) in Hregs'; eauto.
-      rewrite Hregs' in Hstep. simplify_pair_eq.
-      iFailWP "Hφ" WriteSR_fail_incrPC.
-    }
-
-    eapply (incrementPC_success_updatePC _ (<[dst:=wsrc]> sr) m) in Hregs'
-      as (p' & g' & b' & e' & a'' & a''' & HPC'' & a_pc' & HuPC & ->).
-    eapply updatePC_success_incl with (sregs':=<[dst:=wsrc]>sr) (m':=m) in HuPC; eauto.
-    rewrite HuPC in Hstep. simplify_pair_eq. iFrame.
-    iMod ((gen_heap_update_inSepM _ _ PC) with "Hr Hmap") as "[Hr Hmap]"; eauto.
-    iMod ((gen_heap_update_inSepM _ _ dst) with "Hsr Hsmap") as "[Hsr Hsmap]"; eauto.
-    iFrame. iModIntro. iApply "Hφ". iFrame. iPureIntro. econstructor; eauto.
-    rewrite /incrementPC in H'regs'; simplify_map_eq.
-    by rewrite HPC in HPC''; inv HPC''.
-  Qed.
-
-  Lemma wp_writesr_success E pc_p pc_g pc_b pc_e pc_a pc_a' w dst wdst src wsrc :
-    decodeInstrW w = WriteSR dst src →
-    isCorrectPC (WCap pc_p pc_g pc_b pc_e pc_a) →
-    has_sreg_access pc_p = true →
-    (pc_a + 1)%a = Some pc_a' →
-    src ≠ cnull ->
-
-    {{{ ▷ PC ↦ᵣ WCap pc_p pc_g pc_b pc_e pc_a
-        ∗ ▷ pc_a ↦ₐ w
-        ∗ ▷ dst ↦ₛᵣ wdst
-        ∗ ▷ src ↦ᵣ wsrc }}}
-      Instr Executable @ E
-      {{{ RET NextIV;
-          PC ↦ᵣ WCap pc_p pc_g pc_b pc_e pc_a'
-          ∗ pc_a ↦ₐ w
-          ∗ dst ↦ₛᵣ wsrc
-          ∗ src ↦ᵣ wsrc }}}.
-  Proof.
-    iIntros (Hinstr Hvpc Hxsr Hpca' ? ϕ) "(>HPC & >Hpc_a & >Hdst & >Hsrc) Hφ".
-    iDestruct (map_of_regs_2 with "HPC Hsrc") as "[Hmap %]".
-    iDestruct (map_of_sregs_1 with "Hdst") as "Hsmap".
-    iApply (wp_WriteSR with "[$Hmap $Hsmap Hpc_a]"); eauto; simplify_map_eq; eauto.
-    - by unfold regs_of; rewrite !dom_insert; set_solver+.
-    - by unfold sregs_of; rewrite Hxsr !dom_insert; set_solver+.
-    - iNext. iIntros (regs' sregs' retv) "(#Hspec & Hpc_a & Hmap & Hsmap)". iDestruct "Hspec" as %Hspec.
-
-    destruct Hspec as [| -> Hfail].
-    { (* Success *)
-      iApply "Hφ". iFrame. incrementPC_inv; simplify_map_eq.
-      rewrite (insert_commute _ PC src) // insert_insert (insert_commute _ PC src) // insert_insert.
-      iDestruct (regs_of_map_2 with "Hmap") as "(?&?&?)"; eauto; iFrame.
-      iDestruct (sregs_of_map_1 with "Hsmap") as "?"; eauto; iFrame.
-    }
-    { (* Failure (contradiction) *)
-      destruct Hfail.
-      - simplify_map_eq; eauto; congruence.
-      - incrementPC_inv; simplify_map_eq; eauto.
-        congruence.
-    }
-  Qed.
-
-  Lemma wp_writesr_success_fromPC E pc_p pc_g pc_b pc_e pc_a pc_a' w dst wdst :
-    decodeInstrW w = WriteSR dst PC →
-    isCorrectPC (WCap pc_p pc_g pc_b pc_e pc_a) →
-    has_sreg_access pc_p = true →
-    (pc_a + 1)%a = Some pc_a' →
-
-    {{{ ▷ PC ↦ᵣ WCap pc_p pc_g pc_b pc_e pc_a
-        ∗ ▷ pc_a ↦ₐ w
-        ∗ ▷ dst ↦ₛᵣ wdst }}}
-      Instr Executable @ E
-      {{{ RET NextIV;
-          PC ↦ᵣ WCap pc_p pc_g pc_b pc_e pc_a'
-          ∗ pc_a ↦ₐ w
-          ∗ dst ↦ₛᵣ WCap pc_p pc_g pc_b pc_e pc_a }}}.
-  Proof.
-    iIntros (Hinstr Hvpc Hxsr Hpca' ϕ) "(>HPC & >Hpc_a & >Hdst) Hφ".
-    iDestruct (map_of_regs_1 with "HPC") as "Hmap".
-    iDestruct (map_of_sregs_1 with "Hdst") as "Hsmap".
-    iApply (wp_WriteSR with "[$Hmap $Hsmap Hpc_a]"); eauto; simplify_map_eq; eauto.
-    { by unfold sregs_of; rewrite Hxsr !dom_insert; set_solver+. }
-    iNext. iIntros (regs' sregs' retv) "(#Hspec & Hpc_a & Hmap & Hsmap)".
-    iDestruct "Hspec" as %Hspec.
-
-    destruct Hspec as [| -> Hfail].
-    { (* Success *)
-      iApply "Hφ". iFrame. incrementPC_inv; simplify_map_eq.
-      rewrite !insert_insert.
-      iDestruct (regs_of_map_1 with "Hmap") as "?"; eauto; iFrame.
-      iDestruct (sregs_of_map_1 with "Hsmap") as "?"; eauto; iFrame.
-    }
-    { (* Failure (contradiction) *)
-      destruct Hfail.
-      - simplify_map_eq; eauto; congruence.
-      - incrementPC_inv; simplify_map_eq; eauto.
-        congruence.
-    }
-  Qed.
-
-End cap_lang_rules.
diff --git a/theories/program_logic/rules/rules_base.v b/theories/program_logic/rules/rules_base.v
index acd59145..8c929298 100644
--- a/theories/program_logic/rules/rules_base.v
+++ b/theories/program_logic/rules/rules_base.v
@@ -901,8 +901,7 @@ Definition regs_of (i: instr): gset RegName :=
   | Jalr rdst rsrc => {[ rdst; rsrc ]}
   | Seal dst r1 r2 => {[dst; r1; r2]}
   | UnSeal dst r1 r2 => {[dst; r1; r2]}
-  | ReadSR dst _ => {[ dst ]}
-  | WriteSR _ src => {[ src ]}
+  | SpecialRW dst _ src => if (decide (src = cnull)) then {[ dst ]} else {[ dst; src ]}
   | _ => ∅
   end.
 
@@ -921,8 +920,7 @@ Qed.
 
 Definition sregs_of (i: instr): gset SRegName :=
   match i with
-  | ReadSR _ src => {[ src ]}
-  | WriteSR dst _ => {[ dst ]}
+  | SpecialRW _ csr _ => {[ csr ]}
   | _ => ∅
   end.
 
diff --git a/theories/proofmode/proofmode/proofmode_instr_rules.v b/theories/proofmode/proofmode/proofmode_instr_rules.v
index 70eb7ff2..15b9faaf 100644
--- a/theories/proofmode/proofmode/proofmode_instr_rules.v
+++ b/theories/proofmode/proofmode/proofmode_instr_rules.v
@@ -127,12 +127,10 @@ Ltac dispatch_instr_rule instr cont :=
   | UnSeal ?r _ ?r => cont (@wp_unseal_r2)
   | UnSeal ?r ?r _ => cont (@wp_unseal_r1)
   | UnSeal _ _ _ => cont (@wp_unseal_success)
-  (* readsr *)
-  | ReadSR PC _ => cont (@wp_readsr_success_toPC)
-  | ReadSR _ _ => cont (@wp_readsr_success)
-  (* writesr *)
-  | WriteSR _ PC => cont (@wp_writesr_success_fromPC)
-  | WriteSR _ _ => cont (@wp_writesr_success)
+  (* SpecialRW *)
+  | SpecialRW _ _ cnull => cont (@wp_specialrw_readsr)
+  | SpecialRW cnull _ _ => cont (@wp_specialrw_writesr)
+  | SpecialRW _ _ _ => cont (@wp_specialrw_success)
   (* Fail *)
   | Fail => cont (@wp_fail)
   (* Halt *)

From 288dc45894541c5c6f6a7827d34fed1c371647e0 Mon Sep 17 00:00:00 2001
From: June Rousseau <june.rousseau@cs.au.dk>
Date: Thu, 12 Feb 2026 01:35:26 +0100
Subject: [PATCH 2/2] Fix the switcher's proof

---
 theories/switcher/interp_switcher_call.v   | 5 ++++-
 theories/switcher/interp_switcher_return.v | 7 ++++---
 theories/switcher/switcher_spec_call.v     | 3 +++
 theories/switcher/switcher_spec_return.v   | 4 ++++
 4 files changed, 15 insertions(+), 4 deletions(-)

diff --git a/theories/switcher/interp_switcher_call.v b/theories/switcher/interp_switcher_call.v
index 8d350c1f..d78935c7 100644
--- a/theories/switcher/interp_switcher_call.v
+++ b/theories/switcher/interp_switcher_call.v
@@ -714,6 +714,8 @@ Section fundamental.
     { solve_addr. }
 
     (* --- WriteSR mtdc ct2 --- *)
+    specialize (Hfull_rmap cnull) as HH;destruct HH as [? wcnull].
+    iExtract "Hrmap" cnull as "Hcnull".
     iInstr "Hcode".
 
     unfocus_block "Hcode" "Hcls" as "Hcode"; subst hcont.
@@ -937,9 +939,10 @@ Section fundamental.
     ; clear dependent Ha_clear.
 
     rewrite /rmap'. rewrite !map_filter_delete.
+    rewrite (delete_commute _ _ ct1).
     iDestruct (big_sepM_insert with "[$Hrest $Hct1]") as "Hrest"
     ; [clear; by simplify_map_eq|rewrite insert_delete_insert].
-    iInsertList "Hrest" [ctp;ct2;cs1;cs0].
+    iInsertList "Hrest" [cnull;ctp;ct2;cs1;cs0].
 
     iApply (clear_registers_pre_call_spec with "[- $HPC $Hcode $Hrest]"); try solve_pure.
     { clear -Hfull_rmap. apply regmap_full_dom in Hfull_rmap as Heq'.
diff --git a/theories/switcher/interp_switcher_return.v b/theories/switcher/interp_switcher_return.v
index 384316fd..1160c1ff 100644
--- a/theories/switcher/interp_switcher_return.v
+++ b/theories/switcher/interp_switcher_return.v
@@ -100,9 +100,9 @@ Section fundamental.
     (* --- Extract scratch registers ct2 ctp --- *)
     cbn in Hfull_rmap.
 
-    getRegValList [PC;cra;csp;cgp;ca0;ca1;ctp;ca2;cs1;cs0;ct0;ct1].
-    iExtractList "Hrmap" [PC;cra;csp;cgp;ca0;ca1;ctp;ca2;cs1;cs0;ct0;ct1]
-      as ["HPC";"Hcra";"Hcsp";"Hcgp";"Hca0";"Hca1";"Hctp";"Hca2";"Hcs1";"Hcs0";"Hct0";"Hct1"].
+    getRegValList [PC;cra;csp;cgp;ca0;ca1;ctp;ca2;cs1;cs0;ct0;ct1;cnull].
+    iExtractList "Hrmap" [PC;cra;csp;cgp;ca0;ca1;ctp;ca2;cs1;cs0;ct0;ct1;cnull]
+      as ["HPC";"Hcra";"Hcsp";"Hcgp";"Hca0";"Hca1";"Hctp";"Hca2";"Hcs1";"Hcs0";"Hct0";"Hct1";"Hcnull"].
     iAssert (interp W C wcsp) as "#Hinterp_wcsp".
     { iApply "Hrmap_interp"; eauto; done. }
     iAssert (interp W C wcs0) as "#Hinterp_wcs0".
@@ -403,6 +403,7 @@ Section fundamental.
 
     (* We continue the execution *)
     focus_block 13 "Hcode" as a7 Ha7 "Hcode" "Hcont"; iHide "Hcont" as hcont.
+    iInsert "Hrmap" cnull.
     iApply (clear_stack_spec with "[ - $HPC $Hcsp $Hct0 $Hct1 $Hcode $Hstk]"); eauto; [solve_addr|].
     iSplitL; cycle 1.
     { iIntros "!> %"; simplify_eq. }
diff --git a/theories/switcher/switcher_spec_call.v b/theories/switcher/switcher_spec_call.v
index b7ccf471..140b7fb8 100644
--- a/theories/switcher/switcher_spec_call.v
+++ b/theories/switcher/switcher_spec_call.v
@@ -570,7 +570,9 @@ Section Switcher.
     { rewrite /withinBounds. solve_addr. }
 
     (* --- WriteSR mtdc ct2 --- *)
+    iExtract "Hregs" cnull as "Hcnull".
     iInstr "Hcode".
+    iInsert "Hregs" cnull.
 
     unfocus_block "Hcode" "Hcls" as "Hcode"; subst hcont.
 
@@ -778,6 +780,7 @@ Section Switcher.
     focus_block 10 "Hcode" as a_clear' Ha_clear' "Hcode" "Hcls"; iHide "Hcls" as hcont
     ; clear dependent Ha_clear.
 
+    do 2 (rewrite -delete_insert_ne; last done).
     iDestruct (big_sepM_insert_2 with "[Hctp] Hregs") as "Hregs";[iFrame|].
     rewrite insert_delete_insert.
     rewrite -delete_insert_ne; last done.
diff --git a/theories/switcher/switcher_spec_return.v b/theories/switcher/switcher_spec_return.v
index 74205e7d..cd7bfc6d 100644
--- a/theories/switcher/switcher_spec_return.v
+++ b/theories/switcher/switcher_spec_return.v
@@ -109,6 +109,8 @@ Section Switcher.
     iExtract "Hrmap" ct0 as "Hct0".
     assert (is_Some (rmap !! ct1)) as [??];[apply elem_of_dom;rewrite Hrmap;set_solver-|].
     iExtract "Hrmap" ct1 as "Hct1".
+    assert (is_Some (rmap !! cnull)) as [??];[apply elem_of_dom;rewrite Hrmap;set_solver-|].
+    iExtract "Hrmap" cnull as "Hcnull".
 
     (* --- ReadSR ctp mtdc --- *)
     iInstr "Hcode"; try solve_pure.
@@ -525,6 +527,7 @@ Section Switcher.
 
     (* -------- CLEAR STACK --------- *)
     focus_block 13 "Hcode" as a7 Ha7 "Hcode" "Hcont"; iHide "Hcont" as hcont.
+    iInsert "Hrmap" cnull.
     iAssert ([[ a_stk , csp_e ]] ↦ₐ [[wastk :: wastk1 :: wastk2 :: wastk3 :: stk_mem]])%I
       with "[Ha_stk Ha_stk1 Ha_stk2 Ha_stk3 Hstk]" as "Hstk".
     {
@@ -546,6 +549,7 @@ Section Switcher.
 
     (* -------- CLEAR REGISTERS --------- *)
     focus_block 14 "Hcode" as a9 Ha9 "Hcode" "Hcont"; iHide "Hcont" as hcont.
+    rewrite -!delete_insert_ne //.
     iDestruct (big_sepM_insert_delete with "[$Hrmap $Hct1]") as "Hrmap".
     rewrite -delete_insert_ne //.
     iDestruct (big_sepM_insert_delete with "[$Hrmap $Hct0]") as "Hrmap".