Cryptol

Installation note

On Ubuntu 18.04 x86_64, the downloaded binary 2.11.0 fails with

error while loading shared libraries: libtinfo.so.6: cannot open shared object file: No such file or directory

Using Docker worked, thanks to git comment from weaversa.

my-cryptol.Dockerfile:

FROM ghcr.io/galoisinc/cryptol:2.11.0
USER cryptol
ENTRYPOINT ["/usr/local/bin/cryptol"]

Build the dockerifle with docker build:

docker build -t my-cryptol -f my-cryptol.Dockerfile .

Run:

docker run --rm --name my-cryptol -it my-cryptol

To start bash in the container:

docker exec -it my-cryptol bash

[6] is an abbreviation of [6]Bit, meaning a Bit sequence of length 6. Likewise, [4][2] means a sequence of two bit numbers of length 4.

Cryptol> :t take
take : {front, back, a} (fin front) => [front + back]a -> [front]a
Cryptol> take `{3} 0xFF
0x7

Cryptol cannot prove polymorphic properties. The user must tell Cryptol what particular monomorphic instance of the property she would like Cryptol to prove.

Cryptol’s :prove command is complete. I.e., it will always either prove the property or find a counterexample. It might take infeasible amounts of resources (e.g., memory and time).

• Cryptol Course by weaversa