Spec: Improve definition of the encryption algorithm (#155)

This adds a missing return step to the algorithm definition, adds an
explicit instruction to throw when encryption fails, and attempts to
clarify our commentary on RFC9180.

Followup to #147

spec.bs

@@ -1066,16 +1066,35 @@ They return a [=byte sequence=] or an error.
     of « "`aggregation_service`", |sharedInfo| ».
 1. Let (|kem_id|, |kdf_id|, |aead_id|) be (0x0020, 0x0001, 0x0003).
 
-    Note: These indicate the HPKE algorithm identifiers, specifying the KEM
-        function as DHKEM(X25519, HKDF-SHA256), the KDF function as HKDF-SHA256
-        and the AEAD function as ChaCha20Poly1305.
-1. Let |hpkeContext| be the result of setting up an [[RFC9180|HPKE]]
-    [[RFC9180#name-encryption-to-a-public-key|sender's context]] with |pkR|,
-    |info|, |kem_id|, |kdf_id| and |aead_id|.
+    Note: The ciphersuite triple above is composed of [[RFC9180|HPKE]]
+        [[RFC9180#name-algorithm-identifiers|algorithm identifiers]], specifying
+        the [[RFC9180#name-key-encapsulation-mechanism|KEM]] as DHKEM(X25519,
+        HKDF-SHA256), the [[RFC9180#name-key-derivation-functions-kd|KDF]]
+        function as HKDF-SHA256 and the
+        [[RFC9180#name-authenticated-encryption-wi|AEAD]] function as
+        ChaCha20Poly1305.
+1. Let (|enc|, |hpkeContext|) be the result of setting up an [[RFC9180|HPKE]]
+    [[RFC9180#name-encryption-to-a-public-key|sender's context]] by calling
+    `SetupBaseS()` with a public key |pkR|, application-supplied information
+    |info|, KEM |kem_id|, KDF |kdf_id|, and AEAD |aead_id|. If this operation
+    fails, return an error.
+
+     Note: For clarity, we explicitly passed the KEM, KDF, and AEAD identifiers
+     to `SetupBaseS()` above, even though RFC9180 omits the parameters from its
+     pseudocode.
 1. Let |aad| be \`\` (an empty [=byte sequence=]).
-1. Let <var ignore>encryptedPayload</var> be the result of
-    [[RFC9180#name-encryption-and-decryption|encrypting]] |plaintextPayload|
-    with |hpkeContext| and |aad|.
+1. Let |ciphertext| be the result of
+    [[RFC9180#name-encryption-and-decryption|sealing]] the payload by calling
+    `ContextS.Seal()` on the |hpkeContext| object with additional authenticated
+    data |aad| and plaintext |plaintextPayload|. If this operation fails, return
+    an error.
+1. Let |encryptedPayload| be the concatenation of the [=byte sequences=] «
+    |enc|, |ciphertext| ».
+
+    Note: The length of the encapsulated symmetric key <var ignore>enc</var>
+     generated by our chosen KEM is exactly 32 bytes, as shown in RFC9180's
+     table of [[RFC9180#name-key-encapsulation-mechanism|KEM IDs]].
+1. Return the [=byte sequence=] |encryptedPayload|.
 
 </div>