Cryptol 2.3-alpha couldn't math, but thanks to @yav's hard work, Cryptol 2.3 and
later can math! So with our new found powers comes great simplification. Not
all is perfect, much like Dori-Mic's situation, but things are much better.
See the width constraints in SCrypt.cry for areas that could be improved with
some semi-obvious statements (forall x. 1 + width x >= width (x - 1)).
A new Cryptol user! Alexander Semenov from the Russian Academy of
Sciences is the developer of the Transalg tool, which can also translate
cryptographic algorithms (written in imperative form) into SAT problems.
He recently started experimenting with Cryptol, and wrote up
implementations of several stream ciphers, included in this commit.
This instance throws away a lot of the information in a `Name`, but
since we're not roundtripping that will probably be okay for now. A more
robust future interface should be able to roundtrip, however.
The definitions added in #299 cause a regression in Prelude typechecking
performance. Until we sort out the performance, we'll keep these
definitions in the module `Cryptol::Extras`.
The new type signature for popCount is simpler, and more importantly
passes the typechecker. The old one really _ought_ to typecheck, though,
so a shrunken version of it is now in the test suite for #126
The `random` primitive previously took a `[32]` seed, but this causes
inconsistency between 32-bit and 64-bit platforms when the seed is large
enough to wrap around in GHC's representation of an `Int`. This patch
switches to an API that seeds directly with four 64-bit words, and so
should behave the same way on our supported platforms.
Implication (==>), not, and, or, all, any, map, foldl, sum, scanl, extend,
extendSigned, foldr, scanr, zip, zipWith, repeat, curry, uncurry, and elem.
Rationale:
I've had to implement these functions several times for different problems.
While my problems were admittedly toy, not cryptographic, the functions are
generally applicable and unlikely to clash with many, if any, preexisting
operations of different semantic meaning.
I've found that exposing helper types that are only of internal concern to the
function to be bad form. These values should be in where clauses both to help
the type checker not get distracted and to keep the user-facing API as clean as
possible.
