load to ceh must be a capability; add note about CLENBYTES content

parts/cap-man-insn.adoc

@@ -459,6 +459,8 @@ github_ref:SEAL[Sail definition]
 - The size of the memory region associated with `x[rs1]` is smaller than
 `CLENBYTES * 33` bytes (i.e., `x[rs1].end - x[rs1].base < CLENBYTES * 33`).
 - `x[rs1].base` is not aligned to `CLENBYTES` bytes.
+- The content of the memory region `[x[rs1].base, x[rs1].base + CLENBYTES)`
+does not contain a capability.
 ****
 
 *If no exception is raised:* 

parts/int-except.adoc

@@ -230,7 +230,6 @@ image::trans-exc.svg[trans-exception]
 *If the content in `ceh` satisfies the following conditions:*
 
 ****
-* `ceh` is a capability.
 * `ceh.type` is `4` (sealed).
 * `ceh.valid` is `1` (valid).
 * `ceh.async` is `0` (synchronous)

parts/prog-model.adoc

@@ -360,6 +360,20 @@ also store a capability.
 The type of data contained in a memory location is maintained and
 confusion of the type is not allowed.
 
+.Note
+****
+In this document, when we say the memory location `[addr, addr + CLENBYTES]`,
+we mean that the following content will be loaded from or stored to the memory location:
+
+* Depending on the type of data contained in the memory location,
+the content being loaded from the memory location is either a capability at
+the memory location `[addr, addr + CLENBYTES]`,
+or an integer at the memory location `[addr, addr + XLENBYTES]`.
+* Depending on the type of data being stored to the memory location,
+the data is either stored as a capability at the memory location `[addr, addr + CLENBYTES]`,
+or an integer at the memory location `[addr, addr + XLENBYTES]`.
+****
+
 The physical memory is divided into two disjoint regions:
 the _normal memory_ and the _secure memory_.
 While the normal memory is only accessible through _Memory Management Unit_ (MMU),