"x /^ y" is x/y rounded up, i.e. the least n such that x <= y*n.
"x %^ y" is the least k such that x+k is a multiple of y.
For comparison,
"x / y" is x/y rounded down, i.e. the greatest n such that x >= y*n.
"x % y" is the least k such that x-k is a multiple of y.
The new syntax is much more suggestive of the relation to "/" and "%".
The design is as described in issue #96:
blocks msgLen blockSize = the least n such that msgLen <= blockSize * n
padding msgLen blockSize = least k such that msgLen + k divides blockSize
or alternatively:
msgLen + padding msgLen blockSize = blocks msgLen blockSize * blockSize
The two are very similar anyway, so it makes sense to merge the types.
This also helps display module type parameters using their name, rather
than treating them as unknown variables.
The whole printing of names system is still quite confusing, so maybe
there is a better way to do this, but keeping track of the source of
type parameters seems potentially useful information anyway...
The main user visible effect of this might be that sometime things on
the Cryptol command line are instantiated in a slightly different way:
we get `inf` sometimes when we got a finite example before.
We could work around this if it is an issue, but I am not sure which
behavior is more reasonable.
The syntax is just as described in ticket #373: We have a new
declaration form consisting of the keyword 'constraint' followed
by a identifier and optionally a list of type parameters; the
right-hand side is either a single constraint or a parenthesized,
comma-separated list of type constraints. For example:
constraint NonZero n = (fin n, 1 <= n)
last : {n, a} NonZero n => [n]a -> a
last xs = xs!0
Previously, checking the type of e.g. "(&&) `{[2]b}" would not return
"(Logic [2]b) => [2]b -> [2]b -> [2]b" as expected, but
"Logic b => [2]b -> [2]b -> [2]b". This made it impossible to reconstruct
the instances necessary to produce the required Logic dictionary when
translating to saw-core.
