width issue in manual and help text

[martin-d2]

Hi Galois, it's me again! 😁

I might have got completely the wrong end of the stick here, but I think I might have found a couple of super minor errors in the manual and Cryptol help text. Hopefully easy to fix — or equally likely explain what I've misunderstood!

For the width function, the manual says width is (lg2 rounded up) but what seems to be being calculated is:
(lg2 (arg+1))
i.e., it seems to increment the argument and then take the lg2, rather than taking the lg2 and then rounding up the answer. To me, the description of the function in the manual gives the wrong answer if arg is a power of 2.

Also, on page 70 the manual incorrectly says "Note that lg2 is the floor log base 2 function."

Separately, In the help text: :? lg2 says lg2 n = width (max 1 n-1).
This doesn't seem to be the case, because lg2 1 = 0 but width (max 1 0) = width 1 = 1.

Any thoughts?

Thanks for all your amazing work on Cryptol :-)

Martin

[brianhuffman]

That description of width in appendix F of the book is indeed wrong, as width is not just "lg2 rounded up", but rather lg2(x+1) as you say. We should also adjust the entry for lg2 in appendix F to say that it's the ceiling of the base-2 log. We should also fix the REPL help text for the lg2 type operator, which is both unhelpful and is not a full sentence ending with a period like all the other help texts are:

Cryptol> :? lg2

    type lg2 n = width (max 1 n - 1)

Define the base 2 logarithm function in terms of width

As to the other point, your confusion about lg2 n = width (max 1 n - 1) seems to be due to you misparsing it as width (max 1 (n - 1)) instead of width ((max 1 n) - 1). The intention is that we want lg2 n = width (n - 1), but we want to avoid the undefined subtraction for n = 0, so we replace n with max 1 n. The help text for lg2 n should probably explicitly say that lg2 n = width (n - 1) for nonzero n.

[martin-d2]

Brilliant, thanks for the changes!