Cbuildcap and ctestsubset do not use DDC (#82)

* Made clear that ddc is not used when cs1 == 0 in cbuildcap and ctestsubset
* Minor fixes for cbuildcap and ctestsubset

src/insns/cbuildcap_32bit.adoc

@@ -3,6 +3,10 @@
 [#CBUILDCAP,reftext="CBUILDCAP"]
 ==== CBUILDCAP
 
+ifdef::cheri_v9_annotations[]
+NOTE: *CHERI v9 Note:* cbuildcap does not use ddc if cs1==0
+endif::[]
+
 include::new_encoding_note.adoc[]
 
 Synopsis::
@@ -20,19 +24,20 @@ sealed, `cs1` 's permissions and bounds are equal or a superset of `cs2` 's,
 `cs2` 's bounds are not malformed (see
 xref:section_cap_malformed[xrefstyle=short]), and all reserved bits in `cs2` 's
 metadata are 0. <<CBUILDCAP>> is typically used alongside <<CSETHIGH>> to build
-capabilities from integer values.
+capabilities from integer values. The case `cs1 == 0` trivially leads to the tag
+of `cd` being stripped.
 
 Prerequisites::
 {cheri_base_ext_name}
 
 Simplified Operation TODO #not debugged much easier to read than the existing SAIL# ::
 [source,SAIL,subs="verbatim,quotes"]
 --
-let cs1_val = if unsigned(cs1) == 0 then DDC else C(cs1);
+let cs1_val = C(cs1);
 let cs2_val = C(cs2) [with tag=1];
 //isCapSubset includes derivability checks on both operands
 let subset  = isCapSubset(cs1_val, cs2_val);
-//Clear cd.tag if cs1 isn't a subset of cs1, or if
+//Clear cd.tag if cs2 isn't a subset of cs1, or if
 //cs1 is untagged or sealed, or if either is underivable
 C(cd)       = clearTagIf(cs2_val, not(subset) |
                                   not(cs1_val.tag) |

src/insns/ctestsubset_32bit.adoc

@@ -3,6 +3,10 @@
 [#CTESTSUBSET,reftext="CTESTSUBSET"]
 ==== CTESTSUBSET
 
+ifdef::cheri_v9_annotations[]
+NOTE: *CHERI v9 Note:* ctestsubset does not use ddc if cs1==0
+endif::[]
+
 include::new_encoding_note.adoc[]
 
 Synopsis::
@@ -16,7 +20,7 @@ include::wavedrom/ctestsubset.adoc[]
 
 Description::
 `rd` is set to 1 if the tag of capabilities `cs1`  and `cs2`  are equal and the
-bounds and permissions of `cs2`  are a subset of those of `cs1` .
+bounds and permissions of `cs2`  are a subset of those of `cs1`.
 
 NOTE: The implementation of this instruction is similar to <<CBUILDCAP>>, although
 <<CTESTSUBSET>> does not include the sealed bit in the check.