overhaul representable region description

src/cap-description.adoc

@@ -349,13 +349,6 @@ Decoding the bounds:
 top:    t = { a[XLENMAX - 1:E + MW] + ct, T[MW - 1:0]    , {E{1'b0}} }
 base:   b = { a[XLENMAX - 1:E + MW] + cb, B[MW - 1:0]    , {E{1'b0}} }
 ```
-NOTE: The representable range
- is defined by the space beneath the bottom address bit (`a[E + MW]`)
- in the expression above. If the capability address changes causing that address bit
- to change, then the representable range is violated and so the tag will be cleared
- by an instruction such as <<CINCOFFSET>>. This is represented by a range
- of `s=2^E+MW^` in xref:cap_bounds_map[xrefstyle=short].
-
 The corrections c~t~ and c~b~ are calculated as as shown below using the
 definitions in xref:cap_encoding_ct[xrefstyle=short] and
 xref:cap_encoding_cb[xrefstyle=short].
@@ -423,7 +416,7 @@ A capability whose bounds cover the entire address space has 0 base and top
 equals 2^XLENMAX^, i.e. _t_ is a XLENMAX + 1 bit value. However, _b_ is a
 XLENMAX bit value and the size mismatch introduces additional complications
 when decoding, so the following condition is required to correct _t_ for
-capabilities whose representable region wraps the edge of the address
+capabilities whose <<section_cap_representable_check>> wraps the edge of the address
 space:
 
 ```
@@ -484,28 +477,60 @@ or 'root' capability.
 | Address | zeros | Capability address
 |==============================================================================
 
-[#section_cap_representable_check]
-=== Representable Limit Check
+[#section_cap_representable_check, reftext="Representable Range"]
+=== Representable Range Check
+
+The new address, after updating the address of a capability, is within the
+_representable range_ if decompressing the capability's bounds with the
+original and new addresses yields the same base and top addresses.
 
-Pointer arithmetic on capabilities must be checked to ensure that the new
-address is within the capability's representable region described in
-xref:section_cap_encoding[xrefstyle=short]. The new address, after pointer
-arithmetic, is within the representable region if decompressing the
-capability's bounds with the original and new addresses yields the same base
-and top addresses. In other words, given a capability with address _a_ and the
+In other words, given a capability with address _a_ and the
 new address `a' = a + x`, the bounds _b_ and _t_ are decoded using _a_ and the
 new bounds _b'_ and _t'_ are decoded using _a'_. The new address is within the
-capability's representable region if `b == b' && t == t'`.
+capability's _representable range_ if `b == b' && t == t'`.
+
+Changing a capability's address to a value outside the _representable range_
+unconditionally clears the capability's tag. Examples are:
+
+* Instructions such as <<CINCOFFSET>> which include pointer arithmetic.
+* The <<CSETADDR>> instruction which updates the capability address field.
 
-Changing a capability's address to a value outside the representable region
-unconditionally clears the capability's tag.
+==== Practical Information
 
-NOTE: The encoding of the bounds depends upon the leading 1 of the address
-which is used to determine the exponent. If the leading 1 of the address moves
-then the bounds will need to be recalculated. Instructions like <<CINCOFFSET>>
-and <<CSETADDR>> update the address field but do not recalculate the bounds.
-Therefore, if the leading 1 moves relative to when the bounds were calculated
-then the tag is cleared on the result as the encoding has been invalidated.
+In the bounds encoding in this specification, the top and bottom capability
+bounds are formed of two or three sections:
+
+* Upper bits from the address
+* Middle bits from T and B decoded from the metadata
+* Lower bits are set to zero
+** This is only if there is an embedded exponent (EF=0)
+
+.Composition of address bounds
+[#comp_addr_bounds,options=header,align="center"]
+|==============================================================================
+| Configuration  | Upper section | Middle Section | Lower section
+| EF=0, E varies | address[XLENMAX-1:E + MW] + ct | T[MW - 1:0] | {E{1'b0}}
+| EF=1, i.e. E=0 | address[XLENMAX:MW] + ct     2+| T[MW - 1:0]
+|==============================================================================
+
+The _representable range_ defines the range of addresses which do not corrupt
+the bounds encoding. The encoding was first introduced in
+xref:section_cap_encoding[xrefstyle=short], and is repeated in a different
+form in xref:comp_addr_bounds[xrefstyle=short] to aid this description.
+
+For the address to be valid for the current bounds encoding, the address
+bits in the _Upper Section_ of xref:comp_addr_bounds[xrefstyle=short] _must
+not change_ as this will change the meaning of the bounds.
+
+This gives a range of `s=2^E+MW^`, which as shown in
+xref:cap_bounds_map[xrefstyle=short].
+
+The gap between the bounds of the representable range is always guaranteed
+to be at least 1/8 of `s`. This is represented by `R = Bc - 1` in
+xref:section_cap_encoding[xrefstyle=short].
+This gives useful guarantees, such that if an executed instruction is in
+<<pcc>> bounds, then it is also guaranteed that the next linear instruction
+is _representable_.
 
 [#section_cap_malformed]
 === Malformed Capability Bounds

src/insns/auipcc_32bit.adoc

@@ -25,7 +25,7 @@ Form a 32-bit offset from the 20-bit immediate filling the lowest 12 bits with
 zeros. Increment the address of the <<AUIPCC>> instruction's <<pcc>> by the
 32-bit offset, then write the output capability to `cd`. The tag bit of the
 output capability is 0 if the incremented address is outside the <<pcc>>'s
-representable region.
+<<section_cap_representable_check>>.
 
 Legacy Mode Description::
 Form a 32-bit offset from the immediate, filling in the lowest 12 bits with

src/insns/cincoffset_32bit.adoc

@@ -31,7 +31,7 @@ cleared by <<CMOVE>>.
 Description::
 Increment the address field of the capability `cs1`  and write the result to
 `cd` . The tag bit of the output capability is 0 if `cs1`  did not have its tag
-set to 1, the incremented address is outside `cs1` 's representable region or
+set to 1, the incremented address is outside `cs1` 's <<section_cap_representable_check>> or
 `cs1`  is sealed. +
 For <<CINCOFFSET>>, the address is incremented by the value in
 `rs2` . +

src/insns/csetaddr_32bit.adoc

@@ -17,7 +17,7 @@ include::wavedrom/csetaddr.adoc[]
 Description::
 Set the address field of capability `cs1` to `rs2` and write the output
 capability to `cd`. The tag bit of the output capability is 0 if `cs1` did not
-have its tag set to 1, `rs1` is outside the representable range of `cs1`
+have its tag set to 1, `rs1` is outside the <<section_cap_representable_check>> of `cs1`
 or if `cs1` is sealed.
 
 Prerequisites::

src/riscv-integration.adoc

@@ -24,8 +24,8 @@ data they protect.
 
 The memory address space is circular, so the byte at address
 2^XLEN^ - 1 is adjacent to the byte at address zero. A capability's
-representable region described in xref:section_cap_encoding[xrefstyle=short] is
-also circular, so address 0 is within the representable region of a capability
+<<section_cap_representable_check>> described in xref:section_cap_encoding[xrefstyle=short] is
+also circular, so address 0 is within the <<section_cap_representable_check>> of a capability
 where address 2^XLENMAX^ - 1 is within the bounds.
 
 [#section_riscv_programmers_model]
@@ -207,7 +207,7 @@ build <<pcc>>-relative capabilities. <<AUIPCC>> forms a 32-bit offset from the 2
 immediate and filling the lowest 12 bits with zeros. The <<pcc>> address is then
 incremented by the offset and a representability check is performed so the
 capability's tag is cleared if the new address is outside the <<pcc>>'s
-representable region. The resulting CLEN value along with the new tag are
+<<section_cap_representable_check>>. The resulting CLEN value along with the new tag are
 written to a *c* register.
 
 ==== Control Transfer Instructions
@@ -298,7 +298,7 @@ xref:csr-numbers-section[xrefstyle=short].
 
 Reading or writing any part of a CLEN-bit CSR may cause
 side-effects. For example, the CSR's tag bit may be cleared if a new address
-is outside the representable region of a CSR capability being written.
+is outside the <<section_cap_representable_check>> of a CSR capability being written.
 
 This section describes how the CSR instructions operate on these CSRs in
 {cheri_base_ext_name}.
@@ -564,7 +564,7 @@ Capabilities written to <<mepcc>> must be legalised by implicitly zeroing bit
 either 16 or 32, then whenever IALIGN=32, the capability read from <<mepcc>>
 must be legalised by implicitly zeroing bit **mepcc[1]**. Therefore, the
 capability read or written has its tag bit cleared if the legalised address is
-not within the representable region.
+not within the <<section_cap_representable_check>>.
 
 NOTE: When reading or writing a sealed capability in <<mepcc>>, the
 tag is not cleared if the original address equals the legalized