Clarify interaction of levels with sealed capabilities

See also CHERIoT-Platform/cheriot-sail#14

src/insns/atomic_exceptions.adoc

@@ -8,7 +8,8 @@ If <<c_perm>> is not granted then store the memory tag as zero, and load `cd.tag
 +
 If the authorizing capability does not grant <<lm_perm>>, and the tag of `cd` is 1 and `cd` is not sealed, then an implicit <<ACPERM>> clearing <<w_perm>> and <<lm_perm>> is performed to obtain the intermediate permissions on `cd` (see <<LC>>).
 +
-If the authorizing capability does not grant <<el_perm>>, and the tag of `cd` is 1, then an implicit <<ACPERM>> clearing <<el_perm>> and restricting the <<section_cap_level>> to the level of the authorizing capability is performed to obtain the final permissions on `cd` (see <<LC>>).
+If the authorizing capability does not grant <<el_perm>>, and the tag of `cd` is 1, then an implicit <<ACPERM>> restricting the <<section_cap_level>> to the level of the authorizing capability is performed.
+If `cd` is not sealed, this implicit <<ACPERM>> also clears <<el_perm>> to obtain the final permissions on `cd` (see <<LC>>).
 +
 The stored tag is also set to zero if the authorizing capability does not have <<sl_perm>> set but the stored data has a <<section_cap_level>> of 0 (see <<SC>>).
 endif::[]

src/insns/load_tag_perms.adoc

@@ -5,6 +5,8 @@ The tag value written to `cd` is 0 if the tag of the memory location loaded is
 If the authorizing capability does not grant <<lm_perm>>, and the tag of `cd` is 1 and `cd` is not sealed, then an implicit <<ACPERM>> clearing <<w_perm>> and <<lm_perm>> is performed to obtain the intermediate permissions on `cd`.
 +
 If the authorizing capability does not grant <<el_perm>>, and the tag of `cd` is 1, then an implicit <<ACPERM>> clearing <<el_perm>> and restricting the <<section_cap_level>> to the level of the authorizing capability is performed to obtain the final permissions on `cd`.
+If the authorizing capability does not grant <<el_perm>>, and the tag of `cd` is 1, then an implicit <<ACPERM>> restricting the <<section_cap_level>> to the level of the authorizing capability is performed.
+If `cd` is not sealed, this implicit <<ACPERM>> also clears <<el_perm>> to obtain the final permissions on `cd`.
 
 NOTE: Missing <<lm_perm>> does not affect untagged values since this could result in surprising bit patterns when copying non-capability data.
 Similarly, sealed capabilities are not modified as they are not directly dereferenceable.

src/level-ext.adoc

@@ -123,15 +123,15 @@ NOTE: A capability with <<section_cap_level,CL>>=1 is _global_ and with <<sectio
 NOTE: if W=0 or C=0 then SL is irrelevant
 
 .{cheri_levels_ext_name} `LVLBITS=1` summary table for loaded capabilities
-[#cap_level_load_summary,width="100%",options=header,align=center,cols="1,1,1,1,1,6"]
+[#cap_level_load_summary,width="100%",options=header,align=center,cols="1,1,1,1,1,1,6"]
 |==============================================================================
-   4+|Auth cap field             | Data cap field |
-    h|*R*   h|*C* h|*EL* h|*CL* h| Tag           h|Action
-.5+.^|1 .5+.^| 1   | 1    | X    | X              |Load data capability unmodified
-              .4+.^| 0    | 1    | 1              |Load data capability with EL=0
-                          | 1    | 0              |Load data capability unmodified
-                     .2+.^| 0    | 1              |Load data capability with CL=0,EL=0
-                                 | 0              |Load data capability unmodified
+   4+|Auth cap field             2+| Data cap field |
+    h|*R*   h|*C* h|*EL* h|*CL*   h| Tag h| Sealed h|Action
+.5+.^|1 .5+.^| 1   | 1 .3+.^| X    | X    | X  .2+.^|Load data capability unmodified
+              .4+.^| 0             | 0    | N/A
+                              .3+.^| 1    | Yes     |Load data capability with `CL=min(auth.CL, data.CL)`, EL unchanged
+                          | 1        .2+.^| No      |Load data capability with EL=0, CL unchanged
+                          | 0                       |Load data capability with CL=0, EL=0
 |==============================================================================
 
 NOTE: if R=0 or C=0 then EL and CL are irrelevant