From 311610f7dac772b4b47b1d9397a2928e7d8d572c Mon Sep 17 00:00:00 2001
From: Marcella Hastings <marcella@galois.com>
Date: Wed, 13 Nov 2024 16:12:10 -0500
Subject: [PATCH 1/4] wots: move WOTS scheme to its own directory #175

---
 .../Instantiations/WOTSP_SHA2_256.cry               |  4 ++--
 .../{XMSS/Wots.cry => WOTS/Specification.cry}       | 13 ++++++++-----
 2 files changed, 10 insertions(+), 7 deletions(-)
 rename Primitive/Asymmetric/Signature/{XMSS => WOTS}/Instantiations/WOTSP_SHA2_256.cry (91%)
 rename Primitive/Asymmetric/Signature/{XMSS/Wots.cry => WOTS/Specification.cry} (97%)

diff --git a/Primitive/Asymmetric/Signature/XMSS/Instantiations/WOTSP_SHA2_256.cry b/Primitive/Asymmetric/Signature/WOTS/Instantiations/WOTSP_SHA2_256.cry
similarity index 91%
rename from Primitive/Asymmetric/Signature/XMSS/Instantiations/WOTSP_SHA2_256.cry
rename to Primitive/Asymmetric/Signature/WOTS/Instantiations/WOTSP_SHA2_256.cry
index e3fb8a85..55fba00d 100644
--- a/Primitive/Asymmetric/Signature/XMSS/Instantiations/WOTSP_SHA2_256.cry
+++ b/Primitive/Asymmetric/Signature/WOTS/Instantiations/WOTSP_SHA2_256.cry
@@ -20,8 +20,8 @@
  * @copyright Galois, Inc.
  * @author Marcella Hastings <marcella@galois.com>
  */
-module Primitive::Asymmetric::Signature::XMSS::Instantiations::WOTSP_SHA2_256 =
-    Primitive::Asymmetric::Signature::XMSS::Wots where
+module Primitive::Asymmetric::Signature::WOTS::Instantiations::WOTSP_SHA2_256 =
+    Primitive::Asymmetric::Signature::WOTS::Specification where
         import Primitive::Keyless::Hash::SHA2::Instantiations::SHA256 as SHA256
 
         type n = 32
diff --git a/Primitive/Asymmetric/Signature/XMSS/Wots.cry b/Primitive/Asymmetric/Signature/WOTS/Specification.cry
similarity index 97%
rename from Primitive/Asymmetric/Signature/XMSS/Wots.cry
rename to Primitive/Asymmetric/Signature/WOTS/Specification.cry
index 39cd8fe8..c1f7bf52 100644
--- a/Primitive/Asymmetric/Signature/XMSS/Wots.cry
+++ b/Primitive/Asymmetric/Signature/WOTS/Specification.cry
@@ -1,9 +1,13 @@
 /**
  * WOTS+: One-Time Signatures.
  *
- * This signature primitive is used in the XMSS signature scheme. In WOTS+,
- * a private key can be used to sign any message, but each private key can
- * be used only once.
+ * WOTS+ is a signature scheme. A notable limitation of WOTS+ is that a given
+ * key pair can produce exactly ONE signature; repeated signatures with a
+ * single key pair will compromise the private key!!
+ *
+ * This scheme should typically be used as a component of a less limited
+ * signature scheme, like XMSS, LMS, or SPHINCS+.
+ *
  * Warning: If a private key is used to sign two different messages, the scheme
  * becomes insecure! Cryptol cannot protect against this failure mode!
  *
@@ -22,8 +26,7 @@
  * @copyright Galois, Inc.
  * @author Marcella Hastings <marcella@galois.com>
  */
-module Primitive::Asymmetric::Signature::XMSS::Wots where
-
+module Primitive::Asymmetric::Signature::WOTS::Specification where
 
 parameter
     /**

From a544acdfb0035f8b505a890e5e8b05bb246e0822 Mon Sep 17 00:00:00 2001
From: Marcella Hastings <marcella@galois.com>
Date: Wed, 13 Nov 2024 16:25:23 -0500
Subject: [PATCH 2/4] wots: copy public API into an interface #175

The practical use case for WOTS+ is as a component of other protocols.
These are typically implemented generically over WOTS+, and then
instantiated with a joint set of parameters for WOTS+ and the parent
scheme.

This means that just instantiating WOTS+ with the approved parameter
sets isn't suitable, since we want to define other protocols based on
the generic specification.

This commit adds an interface that defines the parameters (n, w, F, PRF)
and the public API (genPK, sign, pkFromSig) for WOTS+. This way, we can
define other protocols based on the interface and instantiate them with
the approved WOTS parameter sets.

I duplicated most of the docs.
---
 .../WOTS/Instantiations/WOTSP_SHA2_256.cry    |  10 +-
 .../Asymmetric/Signature/WOTS/Interface.cry   | 131 ++++++++++++++++++
 .../Signature/WOTS/Specification.cry          |  23 +--
 3 files changed, 149 insertions(+), 15 deletions(-)
 create mode 100644 Primitive/Asymmetric/Signature/WOTS/Interface.cry

diff --git a/Primitive/Asymmetric/Signature/WOTS/Instantiations/WOTSP_SHA2_256.cry b/Primitive/Asymmetric/Signature/WOTS/Instantiations/WOTSP_SHA2_256.cry
index 55fba00d..d96c0327 100644
--- a/Primitive/Asymmetric/Signature/WOTS/Instantiations/WOTSP_SHA2_256.cry
+++ b/Primitive/Asymmetric/Signature/WOTS/Instantiations/WOTSP_SHA2_256.cry
@@ -24,10 +24,8 @@ module Primitive::Asymmetric::Signature::WOTS::Instantiations::WOTSP_SHA2_256 =
     Primitive::Asymmetric::Signature::WOTS::Specification where
         import Primitive::Keyless::Hash::SHA2::Instantiations::SHA256 as SHA256
 
-        type n = 32
-        type w = 16
-
-        F KEY M = split (SHA256::hash (join ((zero : [32][8]) # KEY # M)))
-        PRF KEY M = split (SHA256::hash (join ((zero : [31][8]) # [(3 : [8])] # KEY # M)))
-
+        type n' = 32
+        type w' = 16
 
+        F' KEY M = split (SHA256::hash (join ((zero : [32][8]) # KEY # M)))
+        PRF' KEY M = split (SHA256::hash (join ((zero : [31][8]) # [(3 : [8])] # KEY # M)))
diff --git a/Primitive/Asymmetric/Signature/WOTS/Interface.cry b/Primitive/Asymmetric/Signature/WOTS/Interface.cry
new file mode 100644
index 00000000..48a081d8
--- /dev/null
+++ b/Primitive/Asymmetric/Signature/WOTS/Interface.cry
@@ -0,0 +1,131 @@
+interface module Primitive::Asymmetric::Signature::WOTS::Interface where
+
+/**
+ * Security parameter.
+ * This defines the message length, the length of a private key, the length
+ * of a public key, and a signature element (in bytes).
+ * [RFC-8391] Section 3.1.1.
+ */
+type n : #
+type constraint (fin n)
+
+/**
+ * The Winternitz parameter. This must be either 4 or 16.
+ * [RFC-8391] Section 3.1.1.
+ *
+ * The type constraint is a bit contrived, but it requires that
+ * `w` is in the range `[0, 16]`, is divisible by 4 (`{0, 4, 8, 12, 16}`),
+ * and is congruent to 1 mod 3 (`{4, 16}`).
+ */
+type w : #
+type constraint (fin w, w % 4 == 0, w % 3 == 1, w <= 16)
+
+/**
+ * A keyed cryptographic hash function that takes a key and a message.
+ * [RFC-8391] Section 3.1.1.1.
+ */
+F : [n][8] -> [n][8] -> [n][8]
+
+/**
+ * A pseudorandom function that takes a key and an index.
+ * [RFC-8391] Section 3.1.1.1.
+ */
+PRF : [n][8] -> [32][8] -> [n][8]
+
+/**
+ * A length value (fixed with respect to `n` and `w`).
+ * [RFC-8391] Section 3.1.1.
+ */
+type len_1 = (8 * n) /^ (lg2 w)
+
+/**
+ * A length value (fixed with respect to `n` and `w`).
+ * [RFC-8391] Section 3.1.1.
+ */
+
+type len_2 = lg2 (len_1 * (w - 1)) / lg2 w + 1
+
+/**
+ * The number of `n`-byte string elements in a WOTS+ private key, public key,
+ * and signature.
+ * [RFC-8391] Section 3.1.1.
+ */
+type len = len_1 + len_2
+
+/**
+ * A byte is a sequence of 8 bits using big-endian representation.
+ * [RFC-8391] Section 2.1.
+ */
+type Byte = [8]
+
+/**
+ * Address scheme for randomizing hash function calls in the OTS scheme.
+ * [RFC-8391] Section 2.5.
+ *
+ * The address breaks down 7 components, each 1 word (4 bytes) long, except
+ * for the tree address.
+ *
+ * 1. Layer address
+ * 2-3. Tree address (2 Words)
+ * 4. Type (fixed at 0)
+ * 5. OTS address
+ * 6. Chain address
+ * 7. Hash address
+ * 8. keyAndMask
+ */
+type OTSHashAddress = [8 * 4]Byte
+
+/**
+ * A private, or secret, key in WOTS+ is a length `len` array of `n`-byte
+ * strings.
+ *
+ * It represents the start nodes in a set of hash chains.
+ *
+ * ⚠️ Warning ⚠️: A private key MUST be selected randomly from the uniform
+ * distribution or selected using a cryptographically secure pseudorandom
+ * process! Cryptol cannot verify that a `PrivateKey` was chosen suitably!
+ * Implementors must independently audit private key generation!
+ *
+ * [RFC-8391] Section 3.1.3.
+ *
+ * An implementation may also use a cryptographically secure pseudorandom
+ * method to generate the private key from a single `n`-byte value. See
+ * [RFC-8391] Section 3.1.7 for a sample method.
+ */
+type PrivateKey = [len][n]Byte
+
+/**
+ * A WOTS+ public key is a length `len` array of `n`-byte strings.
+ *
+ * It represents the end nodes i a set of length-`w` hash chains, where the
+ * start nodes are defined in the corresponding `PrivateKey`.
+ */
+type PublicKey = [len][n]Byte
+
+/**
+ * A WOTS+ signature.
+ * [RFC-8391] Section 3.1.5.
+ */
+type Signature = [len][n]Byte
+
+/**
+ * Generate a WOTS+ public key from a private key.
+ * [RFC-8391] Section 3.1.4, Algorithm 4 (called `WOTS_genPK` in the spec).
+ */
+genPK : PrivateKey -> OTSHashAddress -> [n]Byte -> PublicKey
+
+/**
+ * Generate a signature from a private key and a message.
+ * [RFC-8391] Section 3.1.5, Algorithm 5 (called `WOTS_sign` in the spec).
+ */
+sign : [n]Byte -> PrivateKey -> OTSHashAddress -> [n]Byte -> Signature
+
+/**
+ * Compute a WOTS+ public key from a message and its signature.
+ * [RFC-8391] Section 3.1.6, Algorithm 6 (called `WOTS_pkFromSig` in the spec).
+ *
+ * The result of this function must be compared to the given public key. If
+ * the values are not equal, the signature MUST be rejected. This algorithm
+ * does not actually reject any signatures!!
+ */
+pkFromSig : [n]Byte -> Signature -> OTSHashAddress -> [n]Byte -> PublicKey
diff --git a/Primitive/Asymmetric/Signature/WOTS/Specification.cry b/Primitive/Asymmetric/Signature/WOTS/Specification.cry
index c1f7bf52..b657526c 100644
--- a/Primitive/Asymmetric/Signature/WOTS/Specification.cry
+++ b/Primitive/Asymmetric/Signature/WOTS/Specification.cry
@@ -35,8 +35,8 @@ parameter
      * of a public key, and a signature element (in bytes).
      * [RFC-8391] Section 3.1.1.
      */
-    type n : #
-    type constraint (fin n)
+    type n' : #
+    type constraint (fin n')
 
     /**
      * The Winternitz parameter. This must be either 4 or 16.
@@ -46,20 +46,20 @@ parameter
      * `w` is in the range `[0, 16]`, is divisible by 4 (`{0, 4, 8, 12, 16}`),
      * and is congruent to 1 mod 3 (`{4, 16}`).
      */
-    type w : #
-    type constraint (fin w, w % 4 == 0, w % 3 == 1, w <= 16)
+    type w' : #
+    type constraint (fin w', w' % 4 == 0, w' % 3 == 1, w' <= 16)
 
     /**
      * A keyed cryptographic hash function that takes a key and a message.
      * [RFC-8391] Section 3.1.1.1.
      */
-    F : [n][8] -> [n][8] -> [n][8]
+    F' : [n'][8] -> [n'][8] -> [n'][8]
 
     /**
      * A pseudorandom function that takes a key and an index.
      * [RFC-8391] Section 3.1.1.1.
      */
-    PRF : [n][8] -> [32][8] -> [n][8]
+    PRF' : [n'][8] -> [32][8] -> [n'][8]
 
     /**
      * A length value (fixed with respect to `n` and `w`).
@@ -68,15 +68,15 @@ parameter
      * The type constraint is drawn from Algorithm 5, where a computed checksum
      * of length `len_1 * (w - 1) * 2^8` must fit in 32 bits for correctness.
      */
-    type len_1 = (8 * n) /^ (lg2 w)
-    type constraint (width (len_1 * (w - 1) * 2^^8) <= 32)
+    type len_1 = (8 * n') /^ (lg2 w')
+    type constraint (width (len_1 * (w' - 1) * 2^^8) <= 32)
 
     /**
      * A length value (fixed with respect to `n` and `w`).
      * [RFC-8391] Section 3.1.1.
      */
 
-    type len_2 = lg2 (len_1 * (w - 1)) / lg2 w + 1
+    type len_2 = lg2 (len_1 * (w' - 1)) / lg2 w' + 1
 
     /**
      * The number of `n`-byte string elements in a WOTS+ private key, public key,
@@ -101,6 +101,11 @@ parameter
      */
     type constraint (32 >= width len)
 
+type n = n'
+type w = w'
+F = F'
+PRF = PRF'
+
 /**
  * A byte is a sequence of 8 bits using big-endian representation.
  * [RFC-8391] Section 2.1.

From 43f7816e1ab772560adff60a7da8b7228b86b172 Mon Sep 17 00:00:00 2001
From: Marcella Hastings <marcella@galois.com>
Date: Wed, 13 Nov 2024 16:58:00 -0500
Subject: [PATCH 3/4] xmss: add parameter definitions #175

- Defines a `Parameter` interface with the parameter definitions defined
  in the RFC, plus some additional types needed to compile things.
- Defines a `Specification` that pulls together the parameters defined
  for WOTS+ and XMSS.
- Instantiates one XMSS parameter set and the corresponding XMSS
  instantiation (e.g. in combination with the appropriate WOTS+
  parameter set) to make sure everything builds.
---
 .../XMSS/Instantiations/XMSS_SHA2_10_256.cry  | 12 ++++
 .../XMSS_SHA2_10_256_Parameters.cry           | 25 ++++++++
 .../Asymmetric/Signature/XMSS/Parameters.cry  | 58 +++++++++++++++++++
 .../Signature/XMSS/Specification.cry          | 18 ++++++
 4 files changed, 113 insertions(+)
 create mode 100644 Primitive/Asymmetric/Signature/XMSS/Instantiations/XMSS_SHA2_10_256.cry
 create mode 100644 Primitive/Asymmetric/Signature/XMSS/ParameterSets/XMSS_SHA2_10_256_Parameters.cry
 create mode 100644 Primitive/Asymmetric/Signature/XMSS/Parameters.cry
 create mode 100644 Primitive/Asymmetric/Signature/XMSS/Specification.cry

diff --git a/Primitive/Asymmetric/Signature/XMSS/Instantiations/XMSS_SHA2_10_256.cry b/Primitive/Asymmetric/Signature/XMSS/Instantiations/XMSS_SHA2_10_256.cry
new file mode 100644
index 00000000..5a43cb8e
--- /dev/null
+++ b/Primitive/Asymmetric/Signature/XMSS/Instantiations/XMSS_SHA2_10_256.cry
@@ -0,0 +1,12 @@
+/**
+ * Instantiation of XMSS with the approved parameter set `XMSS_SHA2_10_256`.
+ *
+ * @copyright Galois, Inc
+ * @author Marcella Hastings <marcella@galois.com>
+ */
+module Primitive::Asymmetric::Signature::XMSS::Instantiations::XMSS_SHA2_10_256 =
+    Primitive::Asymmetric::Signature::XMSS::Specification {
+        Parameters = Primitive::Asymmetric::Signature::XMSS::ParameterSets::XMSS_SHA2_10_256_Parameters,
+        WOTS = Primitive::Asymmetric::Signature::WOTS::Instantiations::WOTSP_SHA2_256
+
+    }
diff --git a/Primitive/Asymmetric/Signature/XMSS/ParameterSets/XMSS_SHA2_10_256_Parameters.cry b/Primitive/Asymmetric/Signature/XMSS/ParameterSets/XMSS_SHA2_10_256_Parameters.cry
new file mode 100644
index 00000000..466f842f
--- /dev/null
+++ b/Primitive/Asymmetric/Signature/XMSS/ParameterSets/XMSS_SHA2_10_256_Parameters.cry
@@ -0,0 +1,25 @@
+/**
+ * Definition of the approved parameter set used to instantiate
+ * `XMSS_SHA2_10_256`.
+ * [RFC-8391] Section 5.1.
+ *
+ * @copyright Galois, Inc
+ * @author Marcella Hastings <marcella@galois.com>
+ */
+module Primitive::Asymmetric::Signature::XMSS::ParameterSets::XMSS_SHA2_10_256_Parameters
+where
+    import Primitive::Keyless::Hash::SHA2::Instantiations::SHA256 as SHA256
+
+    type n = 32
+    type h = 10
+
+    H KEY M = split (SHA256::hash ((1 : [32 * 8]) # join (KEY # M)))
+
+    // The maximum message width is defined by SHA256.
+    type MaxMessageWidth = SHA256::MaxMessageWidth
+
+    // The padding in this instantiation includes the domain separator (32
+    // bytes) and the key (3n bytes).
+    type PaddingWidth = (32 * 8) + (3 * n * 8)
+
+    H_msg KEY M = split (SHA256::hash ((2 : [32 * 8]) # join (KEY # M)))
diff --git a/Primitive/Asymmetric/Signature/XMSS/Parameters.cry b/Primitive/Asymmetric/Signature/XMSS/Parameters.cry
new file mode 100644
index 00000000..3dd479a0
--- /dev/null
+++ b/Primitive/Asymmetric/Signature/XMSS/Parameters.cry
@@ -0,0 +1,58 @@
+/*
+ * Parameters for the XMSS signature scheme.
+ *
+ * @copyright Galois, Inc
+ * @author Marcella Hastings <marcella@galois.com>
+ */
+interface module Primitive::Asymmetric::Signature::XMSS::Parameters where
+
+/**
+ * Height of the XMSS tree.
+ * [RFC-8391] Section 4.1.1.
+ */
+type h : #
+type constraint (fin h)
+
+/**
+ * The length (in bytes) of the message digest, as well as each node.
+ * [RFC-8391] Section 4.1.1.
+ */
+type n : #
+type constraint (fin n)
+
+/**
+ * A cryptographic hash function that takes a key and a message.
+ * [RFC-8391] Section 4.1.2.
+ */
+H : [n][8] -> [2 * n][8] -> [n][8]
+
+/**
+ * Maximum width in bits for a message under the hash function used to
+ * instantiate `H_msg`.
+ *
+ * `H_msg` allows arbitrary-length messages, but in practice, the hash
+ * functions used to instantiate it may limit their input to some maximum
+ * width.
+ */
+type MaxMessageWidth : #
+
+/**
+ * Width of the non-message bits passed to the hash function in `H_msg`.
+ *
+ * In the approved instantiations defined in [RFC-8391] and [SP-800-208],
+ * this includes domain separation and a fixed-length key.
+ * This is used to enforce the max message width constraint.
+ */
+type PaddingWidth : #
+
+/**
+ * A cryptographic hash function that takes a key and an arbitrary-length
+ * message.
+ * [RFC-8391] Section 4.1.2.
+ *
+ * Note: Some approved instantiations of this function use hash functions that
+ * have a maximum width for messages. The type constraint enforces this by
+ * limiting the length of the hashed message to the maximum width.
+ */
+H_msg : {m} (fin m, (PaddingWidth + width (8 * m)) < MaxMessageWidth)
+    => [3 * n][8] -> [m][8] -> [n][8]
diff --git a/Primitive/Asymmetric/Signature/XMSS/Specification.cry b/Primitive/Asymmetric/Signature/XMSS/Specification.cry
new file mode 100644
index 00000000..09302907
--- /dev/null
+++ b/Primitive/Asymmetric/Signature/XMSS/Specification.cry
@@ -0,0 +1,18 @@
+/*
+ * XMSS: eXtended Merkle Signature Scheme.
+ *
+ * References:
+ * [RFC-8391]: Andreas Huelsing, Denis Butin, Stefan-Lukas Gazdag, Joost
+ *     Rijneveld, and Aziz Mohaisen. XMSS: eXtended Merkle Signature Scheme.
+ *     Internet Requests for Comments (RFC) 8391. May 2018.
+ *     @see https://datatracker.ietf.org/doc/rfc8391
+ *
+ * @copyright Galois, Inc.
+ * @author Marcella Hastings <marcella@galois.com>
+ */
+module Primitive::Asymmetric::Signature::XMSS::Specification where
+
+import interface Primitive::Asymmetric::Signature::XMSS::Parameters
+import interface Primitive::Asymmetric::Signature::WOTS::Interface as WOTS
+
+interface constraint (n == WOTS::n)

From 6b8b8630ceefe6c55d4e070d9736e4f8c3f2d736 Mon Sep 17 00:00:00 2001
From: Marcella Hastings <marcella@galois.com>
Date: Thu, 14 Nov 2024 14:18:05 -0500
Subject: [PATCH 4/4] wots: improve documentation #175

---
 .../Asymmetric/Signature/WOTS/Interface.cry   | 40 ++++++++++++-------
 .../Signature/WOTS/Specification.cry          |  2 +-
 2 files changed, 26 insertions(+), 16 deletions(-)

diff --git a/Primitive/Asymmetric/Signature/WOTS/Interface.cry b/Primitive/Asymmetric/Signature/WOTS/Interface.cry
index 48a081d8..4017d76e 100644
--- a/Primitive/Asymmetric/Signature/WOTS/Interface.cry
+++ b/Primitive/Asymmetric/Signature/WOTS/Interface.cry
@@ -1,3 +1,24 @@
+/*
+ * Public interface for the WOTS+ one-time signature scheme.
+ *
+ * We expect that there will only be one implementation of this scheme.
+ * However, to support its typical use as a component in a more complex scheme
+ * (like XMSS and SPHINCS+), we want to allow other protocols to be
+ * defined in terms of the generic WOTS, and then instantiated with both
+ * WOTS-specific and scheme-specific parameters (and potentially with
+ * additional interface constraints).
+ *
+ * Some documentation is duplicated between this interface and the
+ * specification. This is based on the API in [RFC-8391].
+ *
+ * [RFC-8391]: Andreas Huelsing, Denis Butin, Stefan-Lukas Gazdag, Joost
+ *     Rijneveld, and Aziz Mohaisen. XMSS: eXtended Merkle Signature Scheme.
+ *     Internet Requests for Comments (RFC) 8391. May 2018.
+ *     @see https://datatracker.ietf.org/doc/rfc8391
+ *
+ * @copyright Galois, Inc.
+ * @author Marcella Hastings <marcella@galois.com>
+ */
 interface module Primitive::Asymmetric::Signature::WOTS::Interface where
 
 /**
@@ -61,19 +82,8 @@ type Byte = [8]
 /**
  * Address scheme for randomizing hash function calls in the OTS scheme.
  * [RFC-8391] Section 2.5.
- *
- * The address breaks down 7 components, each 1 word (4 bytes) long, except
- * for the tree address.
- *
- * 1. Layer address
- * 2-3. Tree address (2 Words)
- * 4. Type (fixed at 0)
- * 5. OTS address
- * 6. Chain address
- * 7. Hash address
- * 8. keyAndMask
  */
-type OTSHashAddress = [8 * 4]Byte
+type Address = [8 * 4]Byte
 
 /**
  * A private, or secret, key in WOTS+ is a length `len` array of `n`-byte
@@ -112,13 +122,13 @@ type Signature = [len][n]Byte
  * Generate a WOTS+ public key from a private key.
  * [RFC-8391] Section 3.1.4, Algorithm 4 (called `WOTS_genPK` in the spec).
  */
-genPK : PrivateKey -> OTSHashAddress -> [n]Byte -> PublicKey
+genPK : PrivateKey -> Address -> [n]Byte -> PublicKey
 
 /**
  * Generate a signature from a private key and a message.
  * [RFC-8391] Section 3.1.5, Algorithm 5 (called `WOTS_sign` in the spec).
  */
-sign : [n]Byte -> PrivateKey -> OTSHashAddress -> [n]Byte -> Signature
+sign : [n]Byte -> PrivateKey -> Address -> [n]Byte -> Signature
 
 /**
  * Compute a WOTS+ public key from a message and its signature.
@@ -128,4 +138,4 @@ sign : [n]Byte -> PrivateKey -> OTSHashAddress -> [n]Byte -> Signature
  * the values are not equal, the signature MUST be rejected. This algorithm
  * does not actually reject any signatures!!
  */
-pkFromSig : [n]Byte -> Signature -> OTSHashAddress -> [n]Byte -> PublicKey
+pkFromSig : [n]Byte -> Signature -> Address -> [n]Byte -> PublicKey
diff --git a/Primitive/Asymmetric/Signature/WOTS/Specification.cry b/Primitive/Asymmetric/Signature/WOTS/Specification.cry
index b657526c..fac4f17f 100644
--- a/Primitive/Asymmetric/Signature/WOTS/Specification.cry
+++ b/Primitive/Asymmetric/Signature/WOTS/Specification.cry
@@ -6,7 +6,7 @@
  * single key pair will compromise the private key!!
  *
  * This scheme should typically be used as a component of a less limited
- * signature scheme, like XMSS, LMS, or SPHINCS+.
+ * signature scheme, like XMSS or SPHINCS+.
  *
  * Warning: If a private key is used to sign two different messages, the scheme
  * becomes insecure! Cryptol cannot protect against this failure mode!