hacspec hacspec chat

A specification language for crypto primitives in Rust.

This is the successor of https://github.com/HACS-workshop/hacspec.

Crates

Name Crates.io Docs CI
hacspec crates.io   Build & Test Status
hacspec-lib crates.io Docs Build & Test Status
hacspec-provider crates.io Docs Build & Test Status

Usage

Writing hacspec

hacspec is always valid Rust code such that starting to write hacspec is as simple as writing Rust code that is compliant with the language specification. However, this is very tedious. It is recommended to use the hacspec standard library to write hacspec. In order to ensure that the code is a hacspec one can use the typecheker.

Typechecking

First ensure that Rust nightly is installed and the typechecker is installed.

rustup toolchain install nightly
rustup component add --toolchain nightly rustc-dev
cargo +nightly install hacspec

In a hacspec crate or workspace directory typechecking can be done as follows now:

cargo +nightly hacspec <crate-name>

Note that the crate needs to be compiled before it can be typechecked.

cargo +nightly build

If typechecking succeeds, it should show

> Successfully verified.

Generating code

To generate F* or EasyCrypt code from hacspec the typechecker (see above) is required.

cargo +nightly hacspec -o <fst-name>.fst <crate-name>
cargo +nightly hacspec -o <ec-name>.ec <crate-name>

Repository Structure

This is a cargo workspace consisting of three main crates:

The three main crates make use of a set of additional crates:

Compiled code:

Contributing

Before starting any work please join the Zulip chat, start a discussion on Github, or file an issue to discuss your contribution.

The main entry points for contributions and some general work items are

Examples

There’s a set of example specs, divided between the safe and unsafe. To run all examples one can use cargo test.

Examples

Unsafe examples