memory tag update rules

parts/existing-insn.adoc

@@ -210,9 +210,6 @@ except that the following adjustments are made to these instructions:
 ****
 - A `Store/AMO access fault(7)` exception is raised
 if the address to be accessed (i.e., `x[rs1] + imm`) is within the range `(SBASE - size, SEND)`.
-- The content in the `CLENBYTES`-byte aligned memory location `[cbase, cend)`,
-which aliases with memory location `[x[rs1] + imm, x[rs1] + imm + size)`,
-is set to integer type, where `cbase = (x[rs1] + imm) & ~(CLENBYTES - 1)` and `cend = cbase + CLENBYTES`.
 ****
 
 ==== Secure world or normal world capability encoding mode
@@ -301,23 +298,9 @@ not in the range `[x[rs1].base + 3 * CLENBYTES, x[rs1].base + 33 * CLENBYTES - s
 
 ====
 . Store `x[rs2]` to the memory location `[x[rs1].cursor + imm, x[rs1].cursor + imm + size)` as an integer.
-. The content in the `CLENBYTES`-byte aligned memory location `[cbase, cend)`, which aliases with
-the memory location `[x[rs1].cursor + imm, x[rs1].cursor + imm + size)`, is set to integer type,
-where `cbase = (x[rs1].cursor + imm) & ~(CLENBYTES - 1)` and `cend = cbase + CLENBYTES`.
 . If `x[rs1].type` is `3` (uninitialised), set `x[rs1].cursor` to `x[rs1].cursor + size`.
 ====
 
-.*Note: undefined behaviour*
-[%collapsible]
-====
-****
-The following load results are _undefined_:
-
-* Load an integer from a memory location when the last capability store to its `CLENBYTES`-byte aligned memory location is
-more recent than the last integer store to the memory location itself.
-****
-====
-
 == Control Flow Instructions
 
 In {base_isa_name}, conditional branch instructions (i.e., `beq`, `bne`, `blt`, `bge`, `bltu`, and `bgeu`),

parts/prog-model.adoc

@@ -360,6 +360,22 @@ also store a capability.
 The type of data contained in a memory location is maintained and
 confusion of the type is not allowed.
 
+.*Note: maintaining the type of data*
+[%collapsible]
+====
+****
+For a store operation that accesses the memory location `[addr, addr + size)`,
+the type of data contained in the memory location is maintained as follows:
+
+* If a capability is stored to the memory location `[addr, addr + CLENBYTES)`,
+the type of data contained in the memory location will become a capability,
+where `addr` is `CLENBYTES`-byte aligned.
+* If an integer is stored to the memory location `[addr, addr + size)`,
+it will make the `CLEN`-bit aligned memory location `[cbase, cend)` an integer,
+where `cbase = addr & ~(CLENBYTES - 1)` and `cend = cbase + CLENBYTES`.
+****
+====
+
 .Note
 ****
 In this document, when we say the memory location `[addr, addr + CLENBYTES]`,
@@ -379,6 +395,8 @@ the _normal memory_ and the _secure memory_.
 While the normal memory is only accessible through _Memory Management Unit_ (MMU),
 the secure memory can only be accessed through capabilities.
 
+Hence, we have the following constraints on the memory accesses in different worlds.
+
 .Memory Accesses in the normal world and secure world
 [%header%autowidth.stretch]
 |===
@@ -397,6 +415,17 @@ But both `SBASE` and `SEND` are required to be `CLENBYTES`-byte aligned.
 | Secure memory | `[SBASE, SEND)` | Capabilities
 |===
 
+.*Note: undefined behaviour*
+[%collapsible]
+====
+****
+The following load results are _undefined_:
+
+* Load an integer from a memory location when the last capability store to its `CLENBYTES`-byte aligned memory location is
+more recent than the last integer store to the memory location itself.
+****
+====
+
 == Instruction Set
 
 The {isa_name} instruction set is based on the {base_isa_name} instruction set.