Now, substitions are explicitly a sequence of maps from variables
to types. This means that composing substitions is nearly trivial
because the structure of maps does not need to be rebuilt. Instead,
we traverse the sequence of maps when substituions are applied.
This significantly reduces the garbage produced by type substituion.
Now, substitions are explicitly a sequence of maps from variables
to types. This means that composing substitions is nearly trivial
because the structure of maps does not need to be rebuilt. Instead,
we traverse the sequence of maps when substituions are applied.
This significantly reduces the garbage produced by type substituion.
To get acceptable performance, we need to be pretty aggressive about
using word representations instead of list-of-bits. Unfortunately,
with the new evaluator, this means we force things to be more strict
than is correct.
We are also still slower than the current evaluator. It is not
clear where the problems are.
In particular, the following keywords will now be suggested by
the REPL autocompletion:
else, if, let, then, where
These, I believe, are the only keywords which can be entered at
the command line.
Fixes#144
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.
