detection of out of range top

src/cap-description.adoc

@@ -537,6 +537,17 @@ NOTE: A capability has infinite bounds if E=CAP_MAX_E and it is not
 malformed (see xref:section_cap_malformed[xrefstyle=short]); this check is
 equivalent to _b_=0 and _t_≥2^MXLEN^.
 
+[#section_top_out_of_range]
+===== The Top Bound is Out Of Range
+
+The top bound of the <<infinite-cap>> is defined to be 2^MXLEN^.
+
+There are cases where the decoded bounds of a capability could, in theory, exceed this value.
+
+These cases are computationally expensive to detect without expanding the bounds, therefore
+all instructions such as <<CBLD>> which expand bounds and output a capability will clear
+the output tag if the top bound is out of range.
+
 [#section_cap_malformed]
 ===== Malformed Capability Bounds
 
@@ -561,6 +572,7 @@ CHERI enforces the following invariants for all valid (i.e., tagged) capabilitie
 . The bounds are not malformed.
 . No reserved bit in the capability encoding is set.
 . The permissions can be legally produced by <<ACPERM>>.
+. The <<section_top_out_of_range,top bound must be no greater than 2^MXLEN^>>.
 
 A tagged capability that violates those invariants (i.e., a tagged but malformed capability or a tagged
 capability with any reserved bit set) can only possibly be caused by

src/insns/addi16sp_16bit.adoc

@@ -26,6 +26,8 @@ include::wavedrom/c-int-reg-immed.adoc[]
 Add the non-zero sign-extended 6-bit immediate to the value in the stack pointer (`csp=c2`), where the immediate is scaled to represent multiples of 16 in the range (-512,496). Clear the tag if the resulting capability is
 unrepresentable or `csp` is sealed.
 
+include::malformed_clear_tag_csp.adoc[]
+
 {cheri_int_mode_name} Description::
 
 Add the non-zero sign-extended 6-bit immediate to the value in the stack pointer (`sp=x2`), where the immediate is scaled to represent multiples of 16 in the range (-512,496).

src/insns/addi4spn_16bit.adoc

@@ -25,6 +25,8 @@ include::wavedrom/c-ciw.adoc[]
 
 Add a zero-extended non-zero immediate, scaled by 4, to the stack pointer, `csp`, and writes the result to `cd'`. This instruction is used to generate pointers to stack-allocated variables. Clear the tag if the resulting capability is unrepresentable or `csp` is sealed.
 
+include::malformed_clear_tag_csp.adoc[]
+
 {cheri_int_mode_name} Description::
 
 Add a zero-extended non-zero immediate, scaled by 4, to the stack pointer, `sp`, and writes the result to `rd'`. This instruction is used to generate pointers to stack-allocated variables.

src/insns/atomic_exceptions.adoc

@@ -35,7 +35,8 @@ reported in the CAUSE field of <<mtval2>> or <<stval2>>:
 | Seal violation        | Authority capability is sealed
 | Permission violation  | Authority capability does not grant <<r_perm>> or <<w_perm>>, or the AP field could not have been produced by <<ACPERM>>
 | Invalid address violation  | The effective address is invalid according to xref:section_invalid_addr_conv[xrefstyle=short]
-| Bounds violation      | At least one byte accessed is outside the authority capability bounds, or the capability has <<section_cap_malformed,malformed>> bounds
+| Bounds violation      | At least one byte accessed is outside the authority capability bounds, or the capability has <<section_cap_malformed,malformed>> bounds, or
+the <<section_top_out_of_range,top bound is out of range>>
 |==============================================================================
 
 :!cap_atomic:

src/insns/cbld_32bit.adoc

@@ -24,13 +24,13 @@ Description::
 Copy `cs2` to `cd` and set `cd.tag` to 1 if
 
 . `cs1.tag` is set, and
-. `cs1` 's bounds are not <<section_cap_malformed,malformed>>, and all reserved fields are zero, and
+. `cs1` 's bounds are not <<section_cap_malformed,malformed>>, and all reserved fields are zero, and the <<section_top_out_of_range,top bound is not out of range>>, and
 . `cs1` 's permissions could have been legally produced by <<ACPERM>>, and
 . `cs1` is not sealed, and
 . `cs2` 's permissions and bounds are equal to or a subset of `cs1` 's, and
 . `cs2` 's <<section_cap_level>> is equal to or lower than `cs1` 's, and
 .. _This is only relevant if {cheri_levels_ext_name} is implemented._
-. `cs2` 's bounds are not <<section_cap_malformed,malformed>>, and all reserved fields are zero, and
+. `cs2` 's bounds are not <<section_cap_malformed,malformed>>, and all reserved fields are zero, and the <<section_top_out_of_range,top bound is not out of range>>, and
 . `cs2` 's permissions could have been legally produced by <<ACPERM>>, and
 . All reserved bits in `cs2` 's metadata are 0;
 

src/insns/cbo_exceptions.adoc

@@ -32,8 +32,8 @@ ifdef::cbo_inval[]
 | Permission violation  | Authority capability does not grant <<w_perm>>, <<r_perm>> or <<asr_perm>>, or the AP field could not have been produced by <<ACPERM>>
 endif::[]
 | Invalid address violation  | The effective address is invalid according to xref:section_invalid_addr_conv[xrefstyle=short]
-| Bounds violation      | None of the bytes accessed are within the bounds, or the capability has <<section_cap_malformed,malformed>> bounds
-
+| Bounds violation      | None of the bytes accessed are within the bounds, or the capability has <<section_cap_malformed,malformed>> bounds, or
+the <<section_top_out_of_range,top bound is out of range>>
 |==============================================================================
 
 

src/insns/jalr_32bit.adoc

@@ -54,7 +54,7 @@ reported in the CAUSE field of <<mtval2>> or <<stval2>>:
 | Permission violation  |      | ✔     | `cs1` does not grant <<x_perm>>, or the AP field could not have been produced by <<ACPERM>>
 | Invalid address violation  | ✔    | ✔     | The target address is invalid according to xref:section_invalid_addr_conv[xrefstyle=short]
 | Bounds violation      | ✔    | ✔     | Minimum length instruction is not within the target capability's bounds, which will fail
-if `cs1` has <<section_cap_malformed,malformed>> bounds in {cheri_cap_mode_name}.
+if `cs1` has <<section_cap_malformed,malformed>> bounds or the <<section_top_out_of_range,top bound is out of range>> in {cheri_cap_mode_name}.
 |==============================================================================
 
 include::pcrel_debug_warning.adoc[]

src/insns/load_exceptions.adoc

@@ -19,8 +19,8 @@ listed below; in this case, _CHERI data fault_ is reported in the <<mtval2>> or
 | Seal violation        | Authority capability is sealed
 | Permission violation  | Authority capability does not grant <<r_perm>>, or the AP field could not have been produced by <<ACPERM>>
 | Invalid address violation  | The effective address is invalid according to xref:section_invalid_addr_conv[xrefstyle=short]
-| Bounds violation      | At least one byte accessed is outside the authority capability bounds, or the capability has <<section_cap_malformed,malformed>> bounds
-
+| Bounds violation      | At least one byte accessed is outside the authority capability bounds, or the capability has <<section_cap_malformed,malformed>> bounds,
+or the <<section_top_out_of_range,top bound is out of range>>
 |==============================================================================
 +
 If virtual memory is enabled, then the state of <<cheri_pte_ext,PTE>>.CW,

src/insns/malformed_clear_tag_csp.adoc

@@ -0,0 +1,2 @@
+NOTE: This instruction sets `cd.tag=0` if `csp` 's bounds are <<section_cap_malformed,malformed>>,
+or if any of the reserved fields are set.

src/insns/malformed_top_range_clear_tag.adoc

@@ -0,0 +1,3 @@
+NOTE: This instruction sets `cd.tag=0` if `cs1` 's bounds are <<section_cap_malformed,malformed>>,
+the <<section_top_out_of_range,top bound is out of range>>,
+or if any of the reserved fields are set.

src/insns/scss_32bit.adoc

@@ -29,6 +29,7 @@ Description::
 . `cs2` 's <<section_cap_level>> is equal to or lower than `cs1` 's
 .. _This is only relevant if {cheri_levels_ext_name} is implemented._
 . neither `cs1` or `cs2` have bounds which are <<section_cap_malformed,malformed>>, and
+. neither `cs1` or `cs2` have the <<section_top_out_of_range,top bound out of range>>, and
 . neither `cs1` or `cs2` have any bits set in reserved fields, and
 . neither `cs1` or `cs2` have permissions that could not have been legally produced by <<ACPERM>>
 

src/insns/store_exceptions.adoc

@@ -19,7 +19,8 @@ listed below; in this case, _CHERI data fault_ is reported in the <<mtval2>> or
 | Seal violation        | Authority capability is sealed
 | Permission violation  | Authority capability does not grant <<w_perm>>, or the AP field could not have been produced by <<ACPERM>>
 | Invalid address violation  | The effective address is invalid according to xref:section_invalid_addr_conv[xrefstyle=short]
-| Bounds violation      | At least one byte accessed is outside the authority capability bounds, or the capability has <<section_cap_malformed,malformed>> bounds
+| Bounds violation      | At least one byte accessed is outside the authority capability bounds, or the capability has <<section_cap_malformed,malformed>> bounds,
+or the <<section_top_out_of_range,top bound is out of range>>
 |==============================================================================
 +
 If {cheri_pte_ext_name} is implemented, and virtual memory is enabled, then the state of

src/riscv-integration.adoc

@@ -26,25 +26,23 @@ privileged architecture specified in the RISC-V ISA.
 === Memory
 
 A hart supporting {cheri_base_ext_name} has a single byte-addressable address
-space of 2^XLEN^ bytes for all memory accesses. Each memory region capable of
+space of 2^MXLEN^ bytes for all memory accesses. Each memory region capable of
 holding a capability also stores a tag bit for each naturally aligned CLEN bits
 (e.g. 16 bytes in RV64), so that capabilities with their tag set can only be
 stored in naturally aligned addresses. Tags must be atomically bound to the
 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
+2^MXLEN^ - 1 is adjacent to the byte at address zero. A capability's
 <<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^MXLEN^ - 1 is within the bounds.
 However, the decoded top field of a capability is MXLEN + 1 bits wide and does *not* wrap, so
 a capability with base 2^MXLEN^ - 1 and top 2^MXLEN^ + 1 is not a subset of the
 <<infinite-cap>> capability and does not authorize access to the byte at address 0.
-Like malformed bounds (see xref:section_cap_malformed[xrefstyle=short]), it is impossible for
+The top bound being out of range (see xref:section_top_out_of_range[xrefstyle=short]) is similar to malformed bounds (see xref:section_cap_malformed[xrefstyle=short]), it is impossible for
 a CHERI core to generate a tagged capability with top > 2^MXLEN^.
 If such a capability exists then it must have been caused by a logic or memory fault.
-Unlike malformed bounds, the top overflowing is not treated as a special case in the
-architecture: normal bounds check rules should be followed.
 
 [#section_riscv_programmers_model]
 === Programmer's Model for {cheri_base_ext_name}