hacspec/hax

A Rust verification tool

hacspec

A specification language for crypto primitives in Rust.

This is the successor of https://github.com/HACS-workshop/hacspec but a predecessor of https://github.com/hacspec/hax. Development in this repository has mostly stopped, see hax instead.

For a quick intro, you can look at the presentation slides. More information is available in the book. Also, see the Publications below.

Crates

Name	Crates.io	Docs	CI
hacspec
hacspec-lib
hacspec-provider

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

Make sure you have at least rustup 1.23.0. The rust-toolchain automatically picks the correct Rust nightly version and components. The compiler version is currently pinned to nightly-2023-01-15.

Installing the typechecker from the repository

cargo install --path language

Installing the typechecker from crates.io (not always up to date)

cargo install hacspec --version 0.2.0-beta.4

Manually installing dependencies

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

cd language
rustup toolchain install nightly-2023-01-15
rustup component add --toolchain nightly-2023-01-15 rustc-dev
cargo +nightly-2023-01-15 install hacspec

Depending on your system you might also need llvm-tools-preview

rustup component add --toolchain nightly-2023-01-15 llvm-tools-preview

Usage

In a hacspec crate or workspace directory typechecking can be done as follows now: (Specifying +nightly-2023-01-15 is only necessary if it's not specified in the toolchain as it is in this main repository.)

cargo +nightly-2023-01-15 hacspec <crate-name>

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

cargo +nightly-2023-01-15 build

If typechecking succeeds, it should show

> Successfully typechecked.

Generating code

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

cargo +nightly-2021-11-14 hacspec -o <fst-name>.fst <crate-name>
cargo +nightly-2021-11-14 hacspec -o <ec-name>.ec <crate-name>
cargo +nightly-2021-11-14 hacspec -o <coq-name>.v <crate-name>

Publications & Other material

• 📕 Tech report
• 📕 HACSpec: A gateway to high-assurance cryptography
• 📕 Original hacspec paper

Secondary literature, using hacspec:

• 📕 Last yard

Repository Structure

This is a cargo workspace consisting of three main crates:

• hacspec: the compiler, typechecker and language infrastructure for the hacspec subset of Rust
  • Note that the language infrastructure is excluded from the main workspace of crates, so it won't be build when you launch cargo build from the root of the repository.
• hacspec-lib: the standard library of hacspec programs
• hacspec-provider: a cryptography provider with a set of cryptographic primitives written in hacspec
  • This combines the individual crates from the examples directory and implements the RustCrypto API on top to use them from regular Rust code.

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

• abstract-integers: wrapper around BigInt for modular natural integers
• secret-integers: wrapper around integer types for constant-timedness
• unsafe-hacspec-examples: cryptographic specs written in hacspec but not formally typechecked yet(hence the unsafety) as hacspec is a work in progress
• examples: cryptographic primitives that have passed the hacspec typechecking
• hacspec-attributes: helper for the hacspec library
• hacspec-dev: utilities that are not part of the language

Compiled code:

• fstar: contains F* translations of the cryptographic specs, produced by the hacspec compiler
• easycrypt: contains EasyCrypt translations of the cryptographic specs, produced by the hacspec compiler
• coq: contains Coq translations of the cryptographic specs, produced by the hacspec compiler

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

• the language if you want to work on the hacspec language itself
  • improve the typechecker
  • improve the existing compiler backends (F* and EasyCrypt)
  • add a new compiler backend
• hacspec implementations
  • implementing new cryptographic primitives in hacspec
  • improve the provider
• the standard library
  • enhance numeric implementations
  • enhance vector arithmetic

Examples

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

Examples

• Chacha20
• Poly1305
• Chacha20Poly1305
• AES 128
• GF 128
• AES-GCM 128
• SHA256
• SHA512
• Curve25519
• NTRU-prime
• SHA-3
• HKDF-SHA256
• HMAC-SHA256
• BLS12-381
• BLS12-381 Hash To Curve
• RIOT bootloade
• GIMLI
• P256
• ECDSA-P256-SHA256
• Ed25519
• RSA-FDH-VRF
• ECVRF
• BIP-340 text blog, including secp.
• merlin
• ristretto

Unsafe examples

• AES 128/256
• AES-GCM 128/256
• Blake2b

hax's Issues

Add a diagram for phases

Alignement between the Rust linter and the actual extraction

List of all "un-alignments":

• infinite loops

Please feel free to comment if you notice anything that seems to belong to this list

Improve OCaml compile time

Currently, the compile times are pretty bad, and there's almost no incrementally while compiling.
There are a lot of ML modules lacking a signature, so that is probably the reason.

Transition from v1

Plan transition from v1 to v2.

• start transition when all hacspec/specs are passing
• repository names
• update website
• update book
• archiving old version

OCaml part: build static binaries and JS for distribution without `opam` or `dune` + package as Cargo crate

• binary releases for ocaml
  Though those binaries are not static. Though for distribution, we also release JS.
• build ocaml from cargo we actually don't want to do this any longer

Add a phase for reodering definitions

related to #43

Renaming

v2 Architecture

High level diagram of hacspec architecture and organisation.

wip: https://github.com/hacspec/hacspec-v2/blob/franziskus/architecture-v1/architecture.excalidraw

Calling function with unit return type

There seems to be an issue with the unification of spans. The following code fails in the "Desugar_direct_and_mut" phase.

pub fn a_test () {

}

pub fn b_test () {
    a_test()
}

This is because List.reduce_exn is given an empty list.

Target language

In the future, we may expect backends in the HOL theorem provers, agda/lean/idris and haskell/ocaml, ...

Would it be worth making the target language explicit?
I'm also thinking of projects like

https://www.gilith.com/opentheory/
and
deducti
that are trying to provide cross prover technology.

Link to the DeterminateSystems Nix installer

Just a suggestion to also link to the DeterminateSystems Nix installer in the readme as it comes with flake support preconfigured.

hacspec linter

Track progress of the hacspec linter, linting for the hacspec subset.

The language definition right now is in the book.

• refine syntax
• document syntax
• write syntax tests
• implement linter for this syntax

Make `setup.sh` check nodejs version

• add a check to script.sh that node is in PATH
• figure out what is the minimal version VERSION of nodejs so that engine/utils/ocaml_of_json_schema/ocaml_of_json_schema.js works
• add a check to script.sh that node is at least version VERSION

Add phase: trait method name disambiguation

Two traits in the same namespace in Rust can share method names.
This is not true in some backends (for instance F*).

We need a phase that globally adds prefixes or suffixes to such methods whose name collides.

The F* case

In F*, a trait is translated as a typeclass. F* treats typeclasses as records, but generates a top-level let for each field (aka trait methods), with an implicit meta argument that takes care of resolving the correct instance when called.

The issue is thus that two typeclasses sharing a method name will attempt to generate two let bindings with the same name.

If we have #20, we can stop relying on F* typeclasses entirely and this issue will disappear.

`cargo test` fails with example crates

[main][~/github.com/hacspec/hacspec-v2/examples/chacha20]$ cargo test

... snipped ...

error[E0433]: failed to resolve: use of undeclared crate or module `hacspec_dev`
 --> chacha20/tests/test_chacha20.rs:1:5
  |
1 | use hacspec_dev::prelude::*;
  |     ^^^^^^^^^^^ use of undeclared crate or module `hacspec_dev`
  |
help: there is a crate or module with a similar name
  |
1 | use hacspec_lib::prelude::*;
  |     ~~~~~~~~~~~

error[E0425]: cannot find function `random_byte_vec` in this scope
   --> chacha20/tests/test_chacha20.rs:125:45
    |
125 |     let key = ChaChaKey::from_public_slice(&random_byte_vec(ChaChaKey::length()));
    |                                             ^^^^^^^^^^^^^^^ not found in this scope

error[E0425]: cannot find function `random_byte_vec` in this scope
   --> chacha20/tests/test_chacha20.rs:126:43
    |
126 |     let iv = ChaChaIV::from_public_slice(&random_byte_vec(ChaChaIV::length()));
    |                                           ^^^^^^^^^^^^^^^ not found in this scope

error[E0425]: cannot find function `random_byte_vec` in this scope
   --> chacha20/tests/test_chacha20.rs:127:41
    |
127 |     let m = ByteSeq::from_public_slice(&random_byte_vec(40));
    |                                         ^^^^^^^^^^^^^^^ not found in this scope

Some errors have detailed explanations: E0425, E0433.
For more information about an error, try `rustc --explain E0425`.
error: could not compile `hacspec-chacha20` due to 4 previous errors
warning: build failed, waiting for other jobs to finish...

Allow secret byes / secret arrays macros

Add support for parsing secret_bytes and secret_arrays.

Rust playground

Have a fork of the rust playground with an option for running Hax for a given backend. (I have some WIP proto, but it's very outdated)

Another option would be to write something from scratch, maybe that would be easier.

Make a custom playground dedicated to running Hax.

I already have a prototype for this. Would need half a day to make it work, and a bit more to make it nice.

Add facilities for grouping items as recursive bundles

Currently there is no easy way of grouping recursive items from a backend.
However, the feature is already implemented in module engine/lib/dependencies.ml.

Related to that, there is #396.
But this is completely orthogonal: we should still have a simple way for backends to view a set of items as a set of recursive bundles.

Thus, this issue is about exposing a function item list -> item list list using what already exists in engine/lib/dependencies.ml.

Fix `attempted to read from stolen value`

The frontend browses items of a crate in an order that causes this bug.
Some data in the Rust compiler is kept in a Steal, which is basically a box whose content can be stolen, that is pulled out of the memory (rustc uses arenas)

Thus, the order in which we browse the crate to export every item matters: sometimes I inspect things that happens to be stolen before because of some previous inspections.
This is particularly true for constants, it seems.

Status: mostly fixed

• @geonnave's bug (#27 (comment)) is fixed
• @franziskuskiefer's bug (#27 (comment)) is fixed

However, I tried Hax on core, and I get new stolen stuff. Thus, there exists some scenarios in which this still fails.

Meta issue: support `return`/`continue`/`?`/`break`

This issue is about any expression that can yield an early return: ?, return, continue, break.

The engine has a module side_effect_utils.ml that deals with any expression with side effects: its approach is to hoist every side effect within an expression.

After applying this side effect phase, expressions are trees with let, if, match, loop nodes, and the side-effects occur only on rhs of lets.

Note early return is one of the different possible side effects. Also, one cannot rewrite early returns without considering other side effects: for instance, early returns can interact badly with mutation.

From there:

• CfIntoMonads lifts early return bottom up into various monads.
• we also want a phase that attempts to restructure control flow, to push early returns to end positions.

Road map

• resugar questions marks (Rustc rewrite ? with returns);
• add a phase that transforms early returns into monadic constructions;
  • test this monadic phase;
  • fix bugs;
• add a phase that attempts at reformulating control flow to avoid early returns (i.e. we'd better do if c {return e1} return e2 -> return (if c {e1} {e2}) than a monadic transformation) (see #393 and #254);
• wrap the monadic and reformulation phase into another phase that decides heuristically which looks best.
• support continue/return within loops: #196

Original issue

This is related to the question mark operator, since e? actually expands to a match whose one branch is a return statement.

TODOs:

• add a phase that transforms early returns into monadic constructions;
• fix the current monadic encoding #399;
• add a phase that attempts at reformulating control flow to avoid early returns (i.e. we'd better do if c {return e1} return e2 -> return (if c {e1} {e2}) than a monadic transformation) (see #393);
• add a phase that tries both monadic and control-flow reformulation phases and decides heuristically which seems better;
• figure out how to translate code containing the ? operator nicely (some resugaring?).

Remove our dependency to F*

CI: use [bors](https://bors.tech/) or something similar

We could also go a step further and use something like bors.

Originally posted by @franziskuskiefer in #57 (comment)

Build docker image fails on mac

I tried to build the docker image on a mac m1 and got the following:

$ docker build -f .docker/Dockerfile . -t hacspec-v2
 => [2/6] COPY . /circus-sources
 => [3/6] RUN cd /circus-sources && git init && git add .
 => ERROR [4/6] RUN nix-env -iA cachix -f https://cachix.org/api/v1/install
------
 > [4/6] RUN nix-env -iA cachix -f https://cachix.org/api/v1/install:
#8 1.244 installing 'cachix-1.3.3'
#8 1.479 copying path '/nix/store/6yjms3wa9f2hrpmbzk7ivm1s9jz2m0sw-busybox-static-x86_64-unknown-linux-musl-1.36.0' from 'https://cache.nixos.org'...

(... truncated ...)

#8 12.65 copying path '/nix/store/aly587hv5cyjsbl0fy4ps3lyy7r8cr8n-cachix-1.3.3' from 'https://cache.nixos.org'...
#8 14.67 error: unable to load seccomp BPF program: Invalid argument
#8 14.67 (use '--show-trace' to show detailed location information)
------
executor failed running [/bin/sh -c nix-env -iA cachix -f https://cachix.org/api/v1/install]: exit code: 1

Possible solution

In this issue I learned that it could be fixed by adding filter-syscalls = false to nix.conf (which indeed makes the build work).

A possible solution is to modify the Dockerfile as follows (although it does not seem super safe to disable filter-syscalls).

diff --git a/.docker/Dockerfile b/.docker/Dockerfile
index 0a46de5..e960589 100644
--- a/.docker/Dockerfile
+++ b/.docker/Dockerfile
@@ -3,6 +3,8 @@

 FROM nixpkgs/nix-flakes

+RUN [ "$(uname)" = Darwin ] && echo "filter-syscalls = false" >> /etc/nix/nix.conf
+
 # Prepare the sources
 COPY . /circus-sources
 RUN cd /circus-sources && git init && git add .

Versions

• Mac M1, MacOS Ventura 13.2.1 (22D68)
• Docker version 20.10.24, build 297e128

diagnostics: display errors properly

Add documentation

Add documentation how to get started with this repository.

Documentation

• readme
• blog: https://github.com/hacspec/blog | https://hacspec.org/blog/
• website: https://github.com/hacspec/hacspec.github.io | https://hacspec.org/
• book: https://github.com/hacspec/book | https://hacspec.org/book/
• rust docs: on all crates, especially on cargo-hax
• ocaml docs (see issue #436)
• examples & demos: https://github.com/hacspec/hax/tree/main/examples

Tasks

• installation instructions
• cli instructions
• update/replace book
  • User
    • Examples
    • Tutorials
    • Proofs
      • F*
      • Coq
      • libcore
  • Contributing
    • Structure
    • Cargo command
    • Frontend
    • Engine
    • Backends
    • Utilities
    • Library & Macros
    • libcore
• Architecture & Design technical documentation
• Architecture & Design blog post
• Update website
• Update readme

Add option for marking items as non-export

We should have both:

• CLI options
• Rust attributes

We should be able to express "everything but foo" and "nothing but foo" (at the module level)

improve setup.sh

• #51
• #50

Unexpand type synonym

Type synonyms are expanded by Rust before we hook in.
We should have a best-effort strategy for recovering as much as possible those synonyms.

Given a type synonym definition and an expanded type, I think it will be relatively easy to check whether the expanded type can be reformulated using the type synonym.
This combined with span information and HIR/surface AST analysis, we should get some nice synonym recovering.

Maybe just resugar when HIR information is available

Update nightly (frontend dependency)

• define update policy, e.g. update every 3 months
• update GH actions (1.67 -> stable)

Generic constants: expressions

For now, the frontend supports only concrete literals, we need arbitrary expressions.

(ordered) Todo list

1. the expr and ty engine AST are currently not mutually recursive, make them mut. rec.
2. update the inlining PPX so that we can easily inline definitions in a let bundle
3. make array type contain an expression
4. update all phases
5. add consts generics everywhere
6. test

Port specifications from repository `hacspec/specs`

• tls_cryptolib (fstar: ❌CE0001¹, coq: ❌CE0001¹)
• hacspec-curve25519 (fstar: ✅, coq: ✅)
• hacspec-chacha20 (fstar: ✅, coq: ✅)
• hacspec-ristretto (fstar: ✅, coq: ✅)
• hacspec-linalg (fstar: ✅, coq: ✅)
• hacspec-merlin (fstar: ❌CE0002², coq: ❌CE0002²)
• hacspec-poly1305 (fstar: ✅, coq: ✅)
• hacspec-chacha20poly1305 (fstar: ✅, coq: ✅)
• hacspec-gimli (fstar: ✅, coq: ✅)
• hacspec-sha1 (fstar: ✅, coq: ✅)
• hacspec-sha256 (fstar: ✅, coq: ✅)
• hacspec-sha3 (fstar: ✅, coq: ✅)
• hacspec-ntru-prime (fstar: ✅, coq: ✅)
• hacspec-riot-bootloader (fstar: ✅, coq: ✅)
• hacspec-riot-runqueue (fstar: ✅, coq: ✅)
• hacspec-hmac (fstar: ✅, coq: ✅)
• hacspec-hkdf (fstar: ✅, coq: ✅)
• hacspec-p256 (fstar: ✅, coq: ✅)
• hacspec-bls12-381 (fstar: ✅, coq: ✅)
• hacspec-ecdsa-p256-sha256 (fstar: ✅, coq: ✅)
• hacspec-aes (fstar: ✅, coq: ✅)
• hacspec-aes-jazz (fstar: ✅, coq: ✅)
• hacspec-gf128 (fstar: ✅, coq: ✅)
• hacspec-aes128-gcm (fstar: ✅, coq: ✅)
• hacspec-bls12-381-hash (fstar: ✅, coq: ✅)
• hacspec-ed25519 (fstar: ✅, coq: ✅)
• hacspec-edwards25519 (fstar: ✅, coq: ✅)
• hacspec-edwards25519-hash (fstar: ✅, coq: ✅)
• hacspec-edwards25519-ecvrf (fstar: ✅, coq: ✅)
• hacspec-rsa-pkcs1 (fstar: ✅, coq: ✅)
• hacspec-bip-340 (fstar: ✅, coq: ✅)
• hacspec-rsa-fdh-vrf (fstar: ✅, coq: ✅)
• hacspec-xor (fstar: ✅, coq: ✅)

Footnotes

1. (Diagnostics.Context.Phase FunctionalizeLoops): something is not implemented yet. Loop without mutation? ↩ ↩²

2. Fatal error: something we considered as impossible occurred! Please report this by submitting an issue on GitHub! Details: Import_thir.UnsafeBlock ↩ ↩²

Make `setup.sh` work with opam `2.0.5` (current version on Ubuntu)

We require nodejs as a external dependency (depext), on mac it yielded huge amount of installation, this I disabled it in setup.sh script with the flag assume-depexts on Opam's cli.

But Ubuntu ships a pretty old opam (2.0.5 released in 2019...), which lacks the flag assume-depexts.

Add CI

Add CI for all parts in this repository to ensure things don't break.

• build & release the toolchain
  • build (without Nix) on:
    • Mac
    • Linux
    • Windows (requires #4)
      opam is not able to install gmp and pkgconf, we need to install those manually in the GH Action
  • JS
  • Using Nix
• run on hacspec/specs
  (that's done using Nix)
• run backends
  • F*
  • Coq

Attributes: introduce them in engine's AST

Currently, attributes are translated from the rust compiler to our THIR' JSON file, but we drop them in the module Import_thir in the engine.

• have attributes on item
• have attributes on expression
• have attributes on other specific places (e.g. arms)

Replace `ocaml_of_json_schema.js` with something cleaner

ocaml_of_json_schema.js is a script that takes a JSON Schema created by schemars and outputs an OCaml module with type definitions, (yo)JSON serializers and deserializers.

We would like to drop the dependency on NodeJS at build time, so the idea here would be to replace that script with an OCaml (or Rust) program.

Handle `use` statements

• F*
• Coq
• EasyCrypt

Make coq backend parse all examples

The coq backend should at a minimum be able to parse all the examples, that we can do in V2.

`circus` command: set nightly temporarily

Renaming: use `phase` instead of `desugaring`

Macro arguments: name resolution issues?

Hacspec_lib currently has got some macros that pretend to eat Rust expressions, but this is sort of a lie: it's only tokens that we choose to process, independently to the Rust compiler, as expressions.
Thus, we lose everything semantical from the Rust compiler.
One example is name resolution: we have no way to decide to which namespace belongs a constant for example.

This is related to #22: we should not address this issue unless while redesigning the library, we find we truly need such macros.

Improve/add errors in simplification phases

• have an error architecture in OCaml & Rust
• make all phases and backends to throw errors properly

Figure out how to package together a crate with proofs

Traits: compute explicit implementation expressions

Consider the following code:

trait Show {
    fn show(self) -> String;
}
// Let's name this impl. `ShowStr`
impl Show for &str {
    fn show(self) -> String {
        self.to_string()
    }
}
// Let's name this impl. `ShowU8`
impl Show for u8 {
    fn show(self) -> String {
        format!("{}", self)
    }
}
// Let's name this impl. `ShowVec`
impl<T: Show, U: Show> Show for (T, U) {
    fn show(self) -> String {
        format!("({}, {})", self.0.show(), self.1.show())
    }
}

The expression (1, "a").show() is for now translated as a call to the method show of the typeclass/trait Show with argument (1, "a").
Some backends might have no typeclasses or traits, and some (like F*) have typeclasses mechanisms whose inference mechanism is not great.

Thus, we need the frontend to derive the implementation expressions (i.e. ShowVec ShowU8 ShowStr for (1, "a").show()).

---

Edit: we've got another constraint.
In the engine, we often transform some patterns (i.e. mutation, loops) into function calls that are trait methods.
Thus, maybe we should not do impl resolution in Rust, but on the OCaml side. Or do both: we should anyway export as much info in the frontend, but we'll need to do some impl resolution in the engine.

---

Status: @sonmarcho has some great prototype for that 🎉

---

Status (2023-12-21): this was done by #249 on the frontend side, and will be completed in the engine by #372

Rework binary cargo circus, move call to ocaml to driver

Hacspec lib: redesign with minimality in mind

Start by making everything in hacpsec/specs work with the new lib while getting rid of hacspec specific types like arrays and seqs.

• define core and std parts (feature guarded)
• polynomials
• big int
• array helper
• secret integers/marker

Migrate the diagnostics generated by the linter

• frontend/diagnostics & frontend/linter: move from diagnostics::error::error_name() to diagnostics::Kind::ErrorName
• engine: move from failwith and custom raises to actual diagnostics

Print to Rust

We should have a generic printer for the whole AST (that is, with every feature enabled) to something that looks like Rust, so that it's easy to inspect, for debugging purposes.

Export external items as interfaces

External Rust items have no special treatment in the frontend.
We need to collect them to produce interface files in the various backends so that one can provide models in the backends for external crates.
For instance, Hacspec_lib is an external crate, and we would like Circus to generate an interface each backend should implement.

TODO:

• the frontend should collect every item signature for every external crate;
• the frontend should mark which external item is used by the exported crate;
• have an interface generation mode for backends.

`circus` subcommand: detect runtime dependencies and guide their installation

Incomplete phase `direct_and_mut`