width not working correctly

[weaversa]

width does not seem to work correctly.

Cryptol> `(width 39402006196394479212279040100143613805079739270465446667948293404245721771496870329047266088258938001861606973112319)
Showing a specific instance of polymorphic result:
  * Using 'Integer' for type argument 'rep' of 'Cryptol::number'
384
Cryptol> width 39402006196394479212279040100143613805079739270465446667948293404245721771496870329047266088258938001861606973112319
Showing a specific instance of polymorphic result:
  * Using '512' for type argument 'n' of 'Cryptol::width'
  * Using '10' for type argument 'bits' of 'Cryptol::width'
512

[brianhuffman]

You don't need to use such a big number to get a similar result:

Cryptol> width 20
Showing a specific instance of polymorphic result:
  * Using '8' for type argument 'n' of 'Cryptol::width'
  * Using '4' for type argument 'bits' of 'Cryptol::width'
8
Cryptol> `(width 20)
Showing a specific instance of polymorphic result:
  * Using 'Integer' for type argument 'rep' of 'Cryptol::number'
5

I think the real reason for the confusion here is that we screwed up by giving the type-level width operator and the value-level width function the same name. They do different things. (I think it would be better to call the value-level one length.)

The type-level width computes the minimum number of bits required to represent the given size argument. On the other hand, the value-level width ignores its argument; its result only depends on its argument's type.

So why does width 20 evaluate to 8 instead of 5? The reason is that width 20 is polymorphic, so the REPL needs to choose a type instance to evaluate:

Cryptol> :t width 20
width 20 : {n, m} (n >= 5, m >= width n, fin n, fin m) => [m]

When you type width 20, Cryptol arbitrarily chooses n = 8 and m = 4. (It used to be the case that Cryptol would always choose the smallest possible values for numeric type variables, but we don't guarantee this.) The result then simply comes from the value of the type variable n, which is 8.

[yav]

We do some model shrinking to try and find "smaller" examples, but what exactly constitutes smaller is not very obvious. The behavior might also differ based on the solver you are using. For example, I get slightly different behavior then both of you:

• on @weaversa's example I get 384, using 15 bits
• while width 20 doesn't even work for some reason
• however, width 10 does work with result 7, represented in 4 bits

So I think it would be good to see if we can come up with some more consistent behavior.

[brianhuffman]

I went ahead and renamed the value-level width function to length (see #550)

[brianhuffman]

Is there anything left that we need to do for this ticket? Are there any more tweaks to the defaulting that we want to do, or should we close?

[kiniry]

Syntax.md and Programming Cryptol need to be updated given the rename of value-level width to length. There are also, I imagine, a number of examples that need to be updated. I just was bit by this rename in work on our SHA2 specification, e.g.