scale back proposal

riscv · Feb 10, 2025 · 9d0d3cc · 9d0d3cc
1 parent 1ab7e6a
commit 9d0d3cc
Show file tree

Hide file tree

Showing 10 changed files with 9 additions and 27 deletions.
diff --git a/src/cap-description.adoc b/src/cap-description.adoc
@@ -542,17 +542,6 @@ 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_&#8805;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
 
@@ -577,7 +566,6 @@ 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

diff --git a/src/insns/atomic_exceptions.adoc b/src/insns/atomic_exceptions.adoc
@@ -35,8 +35,7 @@ reported in the CAUSE field of <<mtval2>>, <<stval2>> or <<vstval2>>:
 | 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, or
-the <<section_top_out_of_range,top bound is out of range>>
+| Bounds violation      | At least one byte accessed is outside the authority capability bounds, or the capability has <<section_cap_malformed,malformed>> bounds
 |==============================================================================
 
 :!cap_atomic:
diff --git a/src/insns/cbld_32bit.adoc b/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 the <<section_top_out_of_range,top bound is not out of range>>, and
+. `cs1` 's bounds are not <<section_cap_malformed,malformed>>, and all reserved fields are zero, 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 the <<section_top_out_of_range,top bound is not out of range>>, and
+. `cs2` 's bounds are not <<section_cap_malformed,malformed>>, and all reserved fields are zero, and
 . `cs2` 's permissions could have been legally produced by <<ACPERM>>, and
 . All reserved bits in `cs2` 's metadata are 0;
 

diff --git a/src/insns/cbo_exceptions.adoc b/src/insns/cbo_exceptions.adoc
@@ -32,8 +32,7 @@ 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, or
-the <<section_top_out_of_range,top bound is out of range>>
+| Bounds violation      | None of the bytes accessed are within the bounds, or the capability has <<section_cap_malformed,malformed>> bounds
 |==============================================================================
 
 

diff --git a/src/insns/jalr_32bit.adoc b/src/insns/jalr_32bit.adoc
@@ -54,7 +54,7 @@ reported in the CAUSE field of <<mtval2>>, <<stval2>> or <<vstval2>>:
 | 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 or the <<section_top_out_of_range,top bound is out of range>> in {cheri_cap_mode_name}.
+if `cs1` has <<section_cap_malformed,malformed>> bounds in {cheri_cap_mode_name}.
 |==============================================================================
 
 include::pcrel_debug_warning.adoc[]

diff --git a/src/insns/load_exceptions.adoc b/src/insns/load_exceptions.adoc
@@ -19,8 +19,7 @@ listed below; in this case, _CHERI data fault_ is reported in the <<mtval2>>,
 | 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,
-or the <<section_top_out_of_range,top bound is out of range>>
+| Bounds violation      | At least one byte accessed is outside the authority capability bounds, or the capability has <<section_cap_malformed,malformed>> bounds
 |==============================================================================
 +
 If virtual memory is enabled, then the state of <<cheri_pte_ext,PTE>>.CW,

diff --git a/src/insns/malformed_top_range_clear_tag.adoc b/src/insns/malformed_top_range_clear_tag.adoc
@@ -1,3 +1,2 @@
-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>>,
+NOTE: This instruction sets `cd.tag=0` if `cs1` 's bounds are <<section_cap_malformed,malformed>>
 or if any of the reserved fields are set.
diff --git a/src/insns/scss_32bit.adoc b/src/insns/scss_32bit.adoc
@@ -29,7 +29,6 @@ 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>>
 

diff --git a/src/insns/store_exceptions.adoc b/src/insns/store_exceptions.adoc
@@ -19,8 +19,7 @@ listed below; in this case, _CHERI data fault_ is reported in the <<mtval2>>,
 | 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,
-or the <<section_top_out_of_range,top bound is out of range>>
+| Bounds violation      | At least one byte accessed is outside the authority capability bounds, or the capability has <<section_cap_malformed,malformed>> bounds
 |==============================================================================
 +
 If {cheri_pte_ext_name} is implemented, and virtual memory is enabled, then the state of

diff --git a/src/riscv-integration.adoc b/src/riscv-integration.adoc
@@ -40,7 +40,7 @@ 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.
-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
+The top bound being out of range 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.