[quantova-inc]

This builds on the discussion in issue 8.

I give every function across the seven modules a docstring that follows the
style guide in docs cryptol-style.md. Each one says what the function does
and keeps the standard names from the publication.

I renamed SLH_DSA.cry to Main.cry as suggested in the review.

I added a key generation function named slhKeyGen in Main. It returns the
secret key and the public key in the FIPS 205 byte layout.

I added two test modules. KeyGen checks that both keys carry the same public
root and that a signature made under a generated key verifies. Negative
checks that verification rejects a wrong message at the WOTS plus layer and
for the whole scheme so the recovery proofs are not vacuous.

Every file loads under the load all check with no new warnings. The
properties hold in the interpreter at the small test parameters.

The known answer tests over the full NIST parameter sets ride with the FFI
accelerator you mentioned since those sets are too heavy for the interpreter
on its own. I will send that as the next pull request.

[weaversa]

@WeeknightMVP Is there a better way here?

[weaversa]

@quantova-inc Would you be willing to also add documentation for parameters?

[weaversa]

Remove extraneous newline

[weaversa]

I don't think this needs to be typed twice. For example, shifted = drop (csum << 4) : [16] should suffice.

[weaversa]

Is there a way to be more explicit about the bounds here? Does ixs = [0 ..< len] work? We may also want to ensure len isn't bigger than 2^^IdxW or the values could overflow/wrap around, giving duplicates.

[weaversa]

I wonder if this could be rewritten as a map. If so, Cryptol has a parmap function that may accelerate the computation.

[quantova-inc]

Here is what I changed for each point and how I checked it.

Parameter documentation. I added a docstring to every parameter across the modules. n is the security parameter in bytes. m is the message digest length that the message hash produces. k is the number of FORS trees. a is the height of each FORS tree. hp is the height of each XMSS tree within one layer. d is the number of hypertree layers.

The extraneous newline in WOTS is removed.

The shifted value in the WOTS checksum no longer carries the width twice. It now reads drop (csum << 4) : [16] as you suggested.

The index helper is now ixs = [0 ..< len] with the constraint len <= 2 ^^ IdxW. That keeps every index inside the thirty two bit word so the values cannot wrap and repeat. I made the same change to the index helper in FORS and HyperTree so the three stay consistent.

The level comprehensions in xmssLevels are now parmap. The leaf generation and the node combination are independent within a level so each is a clean map and parmap can spread the work. The walk up the levels stays sequential since each level feeds the one above it.

On the parameter forwarding at Main. I tried the direct form where type n = n and Cryptol rejects it with Invalid self dependency, so the local alias is doing real work. It forwards each module parameter into the imported parameterized modules. If WeeknightMVP has a cleaner idiom in mind I will fold it in.

Checks. Every file loads under the load all check with no new warnings. I re-ran the whole property suite after the changes and all fourteen properties hold. That is the six SHAKE hash equalities. It is both key generation properties. It is the two rejection properties. It is the four recovery properties at the WOTS FORS XMSS and whole scheme layers. The parmap rewrite and the new index helper are both covered since the key generation and recovery proofs run through xmssLevels.