With the other formulation, Z3 became really bad at finding any kind
of model. Basically, it would always answer `unsat` or `unknown`.
This is undesirable, because we use models when instantiating things
at the command line. In those cases, however, we probably don't
need the rule at all... Perhaps, we should provide a way to disable
the axioms when we are looking for models?
"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 width table in CryptolTC.z3 wasn't large enough to solve constraints
about the width of 64-bit words. This change is a bit of a band-aid, as
larger words will expose the same problem. Longer-term, we should try to
solve these constraints after the SMT-based phase, using some other
approach.
The constraints in CryptoBox were too permissive, and when adjusted to
represent the true intent (that values fit within 64-bits), and the
width table was updated, the example will type-check again.
Thanks to @tommd for tracking both of these down.
