diff --git a/.github/workflows/gh_pages.yml b/.github/workflows/gh_pages.yml index bdce044da..36413e885 100644 --- a/.github/workflows/gh_pages.yml +++ b/.github/workflows/gh_pages.yml @@ -1,4 +1,4 @@ -name: Deploy documentation to GH Pages +name: Deploy to GH Pages on: workflow_dispatch: @@ -6,7 +6,7 @@ on: branches: [main] jobs: - build: + build-documentation: runs-on: ubuntu-latest steps: - uses: actions/checkout@v3 @@ -19,9 +19,9 @@ jobs: # deploys the result of `build` # this job is a copy paste from - deploy: + deploy-documentation: # Add a dependency to the build job - needs: build + needs: build-documentation # Grant GITHUB_TOKEN the permissions required to make a Pages deployment permissions: @@ -39,3 +39,74 @@ jobs: - name: Deploy to GitHub Pages id: deployment uses: actions/deploy-pages@v2 # or the latest "vX.X.X" version tag for this action + + # Builds and deploy "external" GH pages: pushes to the repos + # `hacspec/hacspec.github.io` and `hacspec/book` + build-and-deploy-external-gh-pages: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + with: + path: hax + - uses: actions/checkout@v4 + with: + repository: "hacspec/hacspec.github.io" + path: hacspec.github.io + token: ${{secrets.PUSH_HACSPEC_GITHUB_TOKEN}} + - uses: actions/checkout@v4 + with: + repository: "hacspec/book" + path: book + token: ${{secrets.PUSH_HACSPEC_GITHUB_TOKEN}} + + - uses: DeterminateSystems/nix-installer-action@main + + - name: Configure git + run: | + git config --global user.name "github-actions[bot]" + git config --global user.email "41898282+github-actions[bot]@users.noreply.github.com" + + - name: Patch and push `README.md` in `hacspec.github.io` + run: | + ( + README_ORIGINAL="https://github.com/hacspec/hax/blob/main/README.md" + echo "" + echo "" + cat hax/README.md + ) > hacspec.github.io/README.md + cd hacspec.github.io + + # Replace the `๐ŸŒ Website` link to a GitHub link + sed -i 's#.*๐ŸŒ Website.*# ๐Ÿ”— GitHub |#' README.md + + # Replace relative links to absolute links + sed -i 's|(\./|(https://github.com/hacspec/hax/tree/main/|g' README.md + + git add -A + if git commit -m "Readme update"; then + git push https://$USERNAME:$PUSH_HACSPEC_GITHUB_TOKEN@github.com/hacspec/hacspec.github.io + fi + + - name: Regenerate and push the book + run: | + nix build ./hax#hax-book -o result-hax-book + HAX_COMMIT=$(git -C ./hax rev-parse --short HEAD) + + mkdir hax-book + rsync -rq --no-perms --chown=$(id -un):$(id -gn) "$(realpath result-hax-book)/" hax-book + mv book/.git hax-book/.git + cd hax-book + + { + echo "# Warning: this repository only contains generated files" + echo "The sources of the book are in https://github.com/hacspec/hax/tree/main/book" + echo "Please file issues, and push PRs to https://github.com/hacspec/hax." + } > README.md + + git add -A + if git commit -m "Book update (generated from hacspec/hax@$HAX_COMMIT)"; then + git push https://$USERNAME:$PUSH_HACSPEC_GITHUB_TOKEN@github.com/hacspec/book + fi + env: + PUSH_HACSPEC_GITHUB_TOKEN: ${{secrets.PUSH_HACSPEC_GITHUB_TOKEN}} + USERNAME: github-actions[bot] diff --git a/.github/workflows/push_readme.yml b/.github/workflows/push_readme.yml deleted file mode 100644 index d4b17ec0e..000000000 --- a/.github/workflows/push_readme.yml +++ /dev/null @@ -1,43 +0,0 @@ -name: Push `README.md` - -on: - push: - branches: [main] - -jobs: - push_readme: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v4 - with: - path: hax - - uses: actions/checkout@v4 - with: - repository: "hacspec/hacspec.github.io" - path: website - token: ${{secrets.PUSH_HACSPEC_GITHUB_TOKEN}} - - name: Publish documentation - run: | - ( - README_ORIGINAL="https://github.com/hacspec/hax/blob/main/README.md" - echo "" - echo "" - cat hax/README.md - ) > website/README.md - cd website - - # Replace the `๐ŸŒ Website` link to a GitHub link - sed -i 's#.*๐ŸŒ Website.*# ๐Ÿ”— GitHub |#' README.md - - # Replace relative links to absolute links - sed -i 's|(\./|(https://github.com/hacspec/hax/tree/main/|g' README.md - - git config --local user.name "github-actions[bot]" - git config --local user.email "41898282+github-actions[bot]@users.noreply.github.com" - git add -A - if git commit -m "Readme update"; then - git push https://$USERNAME:$PUSH_HACSPEC_GITHUB_TOKEN@github.com/hacspec/hacspec.github.io - fi - env: - PUSH_HACSPEC_GITHUB_TOKEN: ${{secrets.PUSH_HACSPEC_GITHUB_TOKEN}} - USERNAME: github-actions[bot] diff --git a/book/.gitignore b/book/.gitignore new file mode 100644 index 000000000..05ff2e452 --- /dev/null +++ b/book/.gitignore @@ -0,0 +1,2 @@ +book +target diff --git a/book/archive/book.toml b/book/archive/book.toml new file mode 100644 index 000000000..530d58507 --- /dev/null +++ b/book/archive/book.toml @@ -0,0 +1,9 @@ +[book] +authors = ["Franziskus Kiefer"] +language = "en" +multilingual = false +src = "src" +title = "hacspec" + +[output.html] +mathjax-support = true diff --git a/book/archive/src/SUMMARY.md b/book/archive/src/SUMMARY.md new file mode 100644 index 000000000..6ff0d4f43 --- /dev/null +++ b/book/archive/src/SUMMARY.md @@ -0,0 +1,22 @@ +# Summary + +- [Introduction](./readme.md) +- [The hacspec language](./language/readme.md) + - [Syntax](./language/syntax.md) + - [Core](./language/core.md) + - [Sequences and arrays](./language/seq.md) + - [Structs and enums](./language/enums.md) + - [Error handling](./language/errors.md) +- [The hacspec std library](./std/readme.md) + - [Arithmetic](./std/arithmetic.md) + - [Sequence and array operations](./std/seq.md) +- [Examples](./examples/readme.md) +- [Usage](./usage/readme.md) + - [Specifications](./usage/specifications.md) + - [Verification](./usage/verification.md) + - [Test Vectors](./usage/test_vectors.md) +- [For Developers](./developers/readme.md) + - [Working on the compiler](./developers/compiler.md) + +--- +[Contributors](misc/contributors.md) diff --git a/book/archive/src/developers/compiler.md b/book/archive/src/developers/compiler.md new file mode 100644 index 000000000..48a8dde17 --- /dev/null +++ b/book/archive/src/developers/compiler.md @@ -0,0 +1,152 @@ +# Working on the compiler + +## High-level architecture + +![Hacspec compiler architecture](hacspec_architecture.png) + +The Rustspec compiler intervenes after the regular Rust typechecking, +by translating the Rust AST into a stricter hacspec AST, +yielding error messages if you're not in the subset. + +The hacspec AST then undergoes a typechecking phase that replicates the +formal typechecking judgment of hacspec, before being compiled +to the proof backends like F* or Coq. + +## Code organization + +The source code for the compiler is located in the `language/` folder. +`main.rs` is the file containing the driver for the different compiler +passes. + +### Hacspec AST + +The main file of the compiler is `rustspec.rs` and it contains the AST +structure. + +Types are usually enclosed into `Spanned<...>` blocks that attach a location +information to an AST node, thereby providing a way to display beautiful error +message. + +Several nodes also contain a `Fillable<...>` node standing for information +that is filled by the typechecking phase but that can be left to `None` when +building the AST. + +### Translation from Rust AST + +This phase is contained in `ast_to_rustspec.rs`. The trickyness of this +translation is that it needs to be aware of certain special names contained +in the structure `SpecialNames`. Indeed, while the Rust AST treats the application +enum constructors like function applications, the hacspec AST considers them as +proper injection so we need to distinguish them in the Rust AST. For that, we +need to know all declared enums at this point of the program. + +Enums and other `SpecialNames` are also defined in the `ExternalData` that +contains the signatures and types imported in crates used by the hacspec +program being compiled. + +### Name resolution + +When the translation from Rust AST is finished, the identifiers for all +variables inside function bodies are of the following type: + +```rust, noplaypen +pub enum Ident { + Unresolved(String), + Local(LocalIdent), + TopLevel(TopLevelIdent), +} +``` + +More precisely, they are still in the `Ident::Unresolved` case. The compiler +pass in `name_resolution.rs` resolves the identifiers by linking them to local or global identifiers, +each one having a unique ID. hacspec does not feature De Bruijn variable +handling, instead relying on unique fresh IDs for differentiating local +and global variables from each other. + +### External data + +A hacspec file can never (in principal) be considered alone, as it usually imports +at least several other crates like the hacspec standard library. These external +crates must pre-populate the typechecking context with the types and function +signatures that they define. + +It's the job of `hir_to_rustspec.rs` to retrieve this data. The critical +piece of code in this file is [the following](https://github.com/hacspec/hacspec/blob/cc609254b0aa978646f494291b9c91a92fe107ee/language/src/hir_to_rustspec.rs#L733-L737): + +```rust, noplaypen +let num_def_ids = crate_store.num_def_ids_untracked(*krate_num); +let def_ids = (0..num_def_ids).into_iter().map(|id| DefId { + krate: *krate_num, + index: DefIndex::from_usize(id), +}); +``` + +First, we retrieve the number of exported symbols by an external crate using +`num_def_ids_untracked`, a function that is [specifically labeled](https://github.com/rust-lang/rust/pull/85889) +as critical to the hacspec compiler in the Rust compiler codebase. Then, +we manufacture definition IDs for all these exported symbols, relying on the +invariant that they are numbered from 0 to the number of exported symbols +in Rust's compiled crate metadata format. + +Then, we use those definition IDs (`DefId`) to query the Rust compiler +via the central [`TyCtxt`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/struct.TyCtxt.html) +data structure. If the `DefId` corresponds to a type definition, we examine the +type definition structurally and check whether it corresponds to a hacspec-compatible +type definition. Notably, the type definitions generated by macros like `array!` +or `nat_mod!` are only seen here in their expanded version, so we have to retro-engineer +which expanded version corresponds to which macro expansion. This is a vulnerability +of the compiler since it's possible to break the abstraction of the language +by smuggling in a type not defined via a hacspec macro this way. That's why hacspec +developers should be very careful about which dependencies they import in order +to have a 100% safety guarantee. + +For `DefId`s corresponding to functions, the signature of the function is analysed +and if it fits the subset of types expected by hacspec, the function is imported +along with its type in a pre-populated typechecking context. + +Note that it is not possible any more at this point to retrieve the `#[in_hacspec]`, +`#[unsafe_hacspec]`, etc. attributes that would tag the external definitions, +since these attributes get erased by the Rust compiler before reaching the +compiled crates metadata. + + +### Typechecking + +The typechecking is done in `typechecker.rs` and follows a very regular structure, +making heavy use of immutable data structures to not mess up the various +context manipulations. + +Note that we need to perform a full typechecking complete with method resolution +because the proof backends need very fine-grained typechecking information +to generate correct code. + +Be careful: types often need to be de-aliased with `dealias_type` before +being matched on structurally. Forgetting to dealias will lead to bugs with +type aliases. + +### Proof backends + +The different proof backends (`rustspec_to_fstar.rs`, etc) all enjoy a similar +structure that ought to be refactored to showcase their commonality. The backends +don't use an intermediate AST to generate the code in the proof assistant but +rather directly print code as string using the [`pretty`](https://crates.io/crates/pretty) +pretty-printing library. If you want to start a new proof backend, the easiest +solution is probably to copy an existing proof backend and tweak it until +you get the right result. + +The code generation has to be fine-tuned to interface with a replica of the +hacspec standard library in the host proof assistant, whose correspondence with +the original hacspec library in Rust is part of the trusted code base. More specially, +clever solutions to encode sequences and array, as well as all the different types +of public and secret machine integers, and the interaction between the two +(seeing a double as a string of bytes) have to be implemented through proof +assistant libraries. + +## Unit tests + +The compiler has various unit tests that are controlled trough the `language/tests` +files. Please enrich the unit tests bases in `language-tests`, +`negative-language-tests` and `test-crate` as you implement new features for +the compiler. The compiler can also be tested against all the hacspec cryptographic +specifications by running `examples/typecheck_examples.sh` from the root of +the repository. diff --git a/book/archive/src/developers/hacspec_architecture.png b/book/archive/src/developers/hacspec_architecture.png new file mode 100644 index 000000000..009b7cd5a Binary files /dev/null and b/book/archive/src/developers/hacspec_architecture.png differ diff --git a/book/archive/src/developers/readme.md b/book/archive/src/developers/readme.md new file mode 100644 index 000000000..23e631007 --- /dev/null +++ b/book/archive/src/developers/readme.md @@ -0,0 +1,4 @@ +# For Developers + +This section contains a handy guide for hacspec developers working on the +standard library or the compiler. diff --git a/book/archive/src/examples/readme.md b/book/archive/src/examples/readme.md new file mode 100644 index 000000000..46897eadd --- /dev/null +++ b/book/archive/src/examples/readme.md @@ -0,0 +1,13 @@ +# Examples + +The main [hacspec repository] contains a set of [example specifications]. +In this section we pull out some interesting bits to demonstrate the hacspec +language. + +There's also a provider that bundles the different cryptographic primitives +into a single library. +The provider implements the [RustCrypto traits] in order to facilitate interoperability. + +[RustCrypto traits]: https://github.com/RustCrypto/traits +[hacspec repository]: https://github.com/hacspec/hacspec/ +[example specifications]: https://github.com/hacspec/hacspec/tree/master/examples diff --git a/book/archive/src/language/core.md b/book/archive/src/language/core.md new file mode 100644 index 000000000..79ec4b596 --- /dev/null +++ b/book/archive/src/language/core.md @@ -0,0 +1,157 @@ +# The core of hacspec + +## Crates and modules + +hacspec only supports single-module crates, due to a technical limitation +of the Rust compiler. Inside this single file, a hacspec program shall always +start with: + +```rust, noplaypen +use hacspec_lib::*; + +// Optional: dependencies on other crates containing hacspec programs +use other_hacpsec_crate::*; +``` + +No other form of `use` is allowed in hacspec, because allowing Rust's +complex import patterns would increase the complexity of the hacspec compiler +and conflict with the module systems of most proof assistants. + +## Functions + +hacspec is a functional language, and only supports the declaration of +top-level functions: + +```rust, noplaypen +fn hacspec_function(x: bool) -> () { + ... +} +``` + +The functions can take any number of arguments, and may return a value (or not). +Note that recursive functions are forbidden in hacspec. + +The control flow inside hacspec functions is limited, as `return` statements +are forbidden. + +## Basic Types + +hacspec supports all the Rust primitive types: integers (signed and unsigned), +booleans, unit, tuples. hacspec possesses some support for generic +types, but only for primitive types defined by the language creators, and +not for user-defined types. + +Type aliases are allowed in hacspec: + +```rust, noplaypen +type OneTypeAlias = u32; +``` + +## Borrows + +hacspec forbids mutable borrows in all places. Immutable borrows are allowed +in hacspec, but only for function arguments. Indeed, you can declare a function +argument as immutably borrowed: + +```rust, noplaypen +fn hacspec_function(arg: &Seq) { + ... +} +``` + +You can also immutably borrow a value at the call site of a function: + +```rust, noplaypen +hacspec_function(&Seq::::new(64)) +``` + +In particular, return types cannot contain references, and the same is true +for types inside tuples or any data structure. + +## Constants + +hacspec allows the declaration of constants: + +```rust, noplaypen +const ONE_CONST : bool = false; +``` + +## Assignments + +Inside a function body, hacspec allows regular Rust let-bindings: + +```rust, noplaypen +let x = ...; +``` + +hacspec also allows mutable let bindings, and subsequent reassignments: + +```rust, noplaypen +let mut x = ...; +... +x = ...; +``` + +This allowing of mutable variable might come as a contradiction to hacspec's +philosophy of forbidding mutable state. But in fact, mutable local variables in +hacspec can be translated to a completely side-effect free form with a state-passing +like monadic structure. + +Left-hand sides of assignments support destructuring, which is currently the +only way to access the members of a tuple: + +```rust, noplaypen +let (x, y) = z; +``` + +## Loops + +Looping is severely restricted in hacspec compared to Rust, as the only accepted form is +`for` looping with a counter over an integer range: + +```rust, noplaypen +for i in low..hi { + ... // The block can use i and reassign mutable variables +} +``` + +The motivation for this restriction is to ease the proof of termination of +loops. `break` or `continue` statements are forbidden. + +## Conditionals + +hacspec allows statement-like conditionals as well as expression-like +conditionals: + +```rust, noplaypen +if cond1 { + ... // the block can modify mutable variables +} else { // else block is optional here + ... +} +let x = if cond2 { ... } else { ... }; +``` + +## Statements and expressions + +In regular Rust, statements and expressions can be mixed together freely. +This not the case in hacspec that imposes a strict precedence of statements +over expressions. For instance, the following code is not allowed in +hacspec: + +```rust, noplaypen +let x = if cond { + y = true; // ERROR: the reassignment is a statement, which cannot + // be contained in the expression to which x is assigned. + 3 +} else { + 4 +}; +``` + +## Visibility + +hacspec allows for both `pub` and non-`pub` versions of item declarations +(pub, non-pub, etc). You simply have to respect the Rust visibility rules. Note +that these visibility distinctions might not be translated in the proof +backends. diff --git a/book/archive/src/language/enums.md b/book/archive/src/language/enums.md new file mode 100644 index 000000000..7fc0975c8 --- /dev/null +++ b/book/archive/src/language/enums.md @@ -0,0 +1,71 @@ +# Structs and enums + +hacspec also supports user-defined structs and enums with some restrictions. + +## Structs + +The only form of struct declaration currently allowed in hacspec is: + +```rust, noplaypen +struct Foo(u32, Seq); +``` + +The struct thus declared can have one or more components. This form of struct +declaration effectively corresponds to a single-case enum, and is implemented +as such. Struct components can be accessed through let-binding destructuring: + +```rust, noplaypen +let Foo(x, y) = z; +``` + +Note that you can't store borrowed types inside hacspec structs, hence there is no +need for lifetime variables. + +## Enums + +hacspec supports very restricted `enum` declarations: + +```rust, noplaypen +enum Foo { + CaseA, + CaseB(u16), + CaseC(Seq, u64) +} +``` + +These declaration don't support the basic Rust features such as C-style +union declarations with assignments for each case. + +Enumeration values can be pattern-matched in an expression: + +```rust, noplaypen +match x { + Foo::CaseA => ..., + Foo::CaseB(y) => ..., + Foo::CaseC(y,z) => ... +} +``` + +Note that you can't store borrowed types inside hacspec enums, hence there is no +need for lifetime variables. + +## Option and Result + +User-defined structs and enums presented above don't support generic type +parameters yet. However, the built-in enums `Option` and `Result` +support type parameters. Those type parameters have to be explicitly declared +each time, as hacspec does not currently support type inference: + +```rust, noplaypen +match x { + Result::, bool>::Ok(y) => ..., + Result::, bool>::Err(err) => ... +} +``` + +Such type parameter declaration is cumbersome; as a workaround we advise +to declare a type alias as such: + +```rust, noplaypen +type MyResult = Result::, bool>; +``` diff --git a/book/archive/src/language/errors.md b/book/archive/src/language/errors.md new file mode 100644 index 000000000..30c3e6b0b --- /dev/null +++ b/book/archive/src/language/errors.md @@ -0,0 +1,16 @@ +# Error handling + +Error handling in Rust is done via the `Result` type (see the structs and +enums section). But on top of explicit pattern-matching, hacspec also +supports the popular `?` operator to quickly perform an early return and +propagate the error case upwards. + +`?` is only allowed at the very end of an expression in a let-binding or +reassignment statement: + +```rust, noplaypen +let x = foo(true)?; // GOOD +let y = foo(bar(0)?); // ERROR: the ? is not at the end of the statement +``` + +Currently, `?` is the only way to return early in a hacspec function. diff --git a/book/archive/src/language/readme.md b/book/archive/src/language/readme.md new file mode 100644 index 000000000..7d8d768c6 --- /dev/null +++ b/book/archive/src/language/readme.md @@ -0,0 +1,18 @@ +# The hacspec language + +This section gives an informal description of the hacspec language, whose +goal is to provide hands-on documentation for users of the language. For +a formal specification of the semantics of the language, please refer +to the [technical report][1]. + +hacspec is a domain-specific language embedded inside Rust. This means that +all correct hacspec programs are correct Rust programs: you can use +the usual Rust tooling for working on your hacspec developments. However, +hacspec is a strict subset of Rust: this means that some features of Rust +are forbidden inside hacspec. The goal of restricting the expressiveness of +the language is twofold: first, help domain experts such as cryptographers +convey their specifications in a fashion that should help them avoid +mistakes; second, provide a way for Rust programmers to interact with theorem +provers such as F\* or Coq. + +[1]: https://hal.inria.fr/hal-03176482 diff --git a/book/archive/src/language/seq.md b/book/archive/src/language/seq.md new file mode 100644 index 000000000..1f32d5d79 --- /dev/null +++ b/book/archive/src/language/seq.md @@ -0,0 +1,32 @@ +# Sequences and arrays + +## Sequences + +The staple `Vec` type is forbidden in hacspec. Instead, you have to use the +type `Seq`, which is implemented as a wrapper around `Vec`. + +The most notable differences between `Seq` and `Vec` is that `Seq` is not +resizable, and does not support `push` and `pop` operations. Instead, the +final length of the seq has to be provided at creation time. See the +hacspec standard library documentation for more details. + +`Seq` is a built-in generic type that always has to be indexed by the content of the +cells: `Seq`, etc. + +## Arrays + +The native Rust array types `[, ]` is forbidden in +hacspec. Instead, you have to declare nominally at the top-level new array types +for a specific cell content and size with: + +```rust, noplaypen +array!(FooArray, u8, 64); +// This declares type FooArray as an array of u8 of size 64 +bytes!(BarArray, 64); +// bytes! is a specialized version of array! with secret bytes +array!(BazArray, u8, 64, type_for_indexes:BazIndex); +// The additional argument type_for_indexes defines an alias of usize +// intended to spot which usizes are used to index BazArray (useful for +// verification) +``` + diff --git a/book/archive/src/language/syntax.md b/book/archive/src/language/syntax.md new file mode 100644 index 000000000..317173b0f --- /dev/null +++ b/book/archive/src/language/syntax.md @@ -0,0 +1,58 @@ +# Syntax + +``` +P ::= [i]\* Program items +i ::= array!(t, ฮผ, n) Array type declaration where n is a natural number + | nat_mod!(t, n) Modular integer + | fn f([d]+) -> ฮผ b Function declaration + | type t = enum { [c(ฮผ)]+ } Enum declaration (with constructors) + | type t = struct([ฮผ]+) Struct declaration (without named fields) + | const x: ฮผ = e Constant declaration + | use crate::* External crate import + | use mod::* Internal module import +d ::= x: ฯ„ Function argument + | mut x: ฯ„ Mutable function argument +ฮผ ::= unit|bool|u8|U8|i8|I8... Base types + | Seq<ฮผ> Sequence + | String Strings + | ([ฮผ]+) Tuple + | unit Unit type + | t Named type +ฯ„ ::= ฮผ Plain type + | &ฮผ Immutable reference +b ::= {[s;]+} Block +p ::= x Variable pattern + | ([p]+) Tuple pattern + | t (p) Struct constructor pattern + | _ Wildcard pattern +s ::= let p: ฯ„ = e Let binding + | let mut p: ฯ„ = e Mutable let binding + | x = e Variable reassignment + | x = e? Variable reassignment with result/option catching + | let p: ฯ„ = e? Let binding with result/option catching + | if e then b (else b) Conditional statements + | c(e) Enum injection + | match e { [c(p) => e]+ } Pattern matching + | for x in e..e b For loop (integers only) + | e Return expression + | b Statement block +e ::= ()|true|false Unit and boolean literals + | n Integer literal + | U8(e)|I8(e)|... Secret integer classification + | "..." String literal + | t([e]+) Array literal + | e as ฮผ Integer casting + | x Variable + | () Unit + | f([a]+) Function call + | if e then e else e Conditional expression + | e โŠ™ e Binary operations + | โŠ˜ e Unary operations + | ([e]+) Tuple constructor + | x[e] Array or sequence index +a ::= e Linear argument + | &e Call-site borrowing +โŠ™ ::= + | - | * | / | && + | || | == | != | > | < +โŠ˜ ::= - | ~ +``` diff --git a/book/archive/src/misc/contributors.md b/book/archive/src/misc/contributors.md new file mode 100644 index 000000000..adc2dc245 --- /dev/null +++ b/book/archive/src/misc/contributors.md @@ -0,0 +1,15 @@ +# Contributors + +A list of contributors to the hacspec project. + +- Franziskus Kiefer ([franziskuskiefer](https://github.com/franziskuskiefer/)) +- Denis Merigoux ([denismerigoux](https://github.com/denismerigoux)) +- Karthik Bhargavan +- Tomer Yavor ([TomerHawk](https://github.com/TomerHawk)) +- Tanmay Garg ([tanmay2004](https://github.com/tanmay2004)) +- Peter Schwabe ([cryptojedi](https://github.com/cryptojedi)) +- Kaspar Schleiser ([kaspar030](https://github.com/kaspar030)) +- [Kasserne](https://github.com/Kasserne) +- Tony Arcieri ([tarcieri](https://github.com/tarcieri)) + +If you feel you're missing from this list, feel free to add yourself in a PR. \ No newline at end of file diff --git a/book/archive/src/readme.md b/book/archive/src/readme.md new file mode 100644 index 000000000..7f9bfcdb1 --- /dev/null +++ b/book/archive/src/readme.md @@ -0,0 +1,25 @@ +# Introduction + +hacspec is a specification language for crypto primitives, protocols, and more. +It is a subset of the [Rust] programming language, focused on functional +programming and it avoids the use of mutable state as much as possible. + +This book gives an overview of: +* [The hacspec language](./language); +* The different parts of the project: + * [the standard library](./std), + * [examples of hacspec programs](./examples); +* How to use hacspec to write [specifications] for standards and [verification]; +* How to use hacspec to generate [test vectors]; +* [Work on the hacspec compiler and tooling itself](./developers). + +For a quick introduction you can also check out these [slides] from April 2021. +An in-depth [technical report] is also available, and serves as a reference +for the language formalization. + +[slides]: https://raw.githubusercontent.com/hacspec/hacspec/master/presentation_slides.pdf +[technical report]: https://hal.inria.fr/hal-03176482 +[Rust]: https://www.rust-lang.org/ +[specifications]: ./usage/specifications.md +[verification]: ./usage/verification.md +[test vectors]: ./usage/test_vectors.md diff --git a/book/archive/src/std/abstract_integers.md b/book/archive/src/std/abstract_integers.md new file mode 100644 index 000000000..baf0324c5 --- /dev/null +++ b/book/archive/src/std/abstract_integers.md @@ -0,0 +1 @@ +# Astract integers diff --git a/book/archive/src/std/arithmetic.md b/book/archive/src/std/arithmetic.md new file mode 100644 index 000000000..43b116ae0 --- /dev/null +++ b/book/archive/src/std/arithmetic.md @@ -0,0 +1,76 @@ +# Arithmetic + +hacspec overloads the arithmetic operators for a wide variety of types +corresponding to mathematical values mentioned in cryptographic specifications. + +## The `Numeric` trait + +All of these types implement the `Numeric` trait defined by the hacspec standard +library. The arithmetic operators work for all kinds of integers, but also +arrays and sequences (point-wise operations). + +Note that the list of types implementing `Numeric` is hardcoded in the +hacspec compiler, and as of this day cannot be extended by the user. + +While the Rust compiler can infer the type of integer literals automatically, +this feature is not implemented by the hacspec compiler: + +``` +let w: u32 = 0; // ERROR: an integer without a suffix will have type usize +let x: u64 = 0x64265u64; // GOOD +let y: u64 = 4u64; // GOOD +``` + +## Public and secret integers + +One of hacspec's goal is to enable users to quickly check whether their +application does not obviously break the constant-time guarantee. +Certain processor instructions take more or less time to complete depending +on their inputs, which can cause secret leakage and break the security of +an application. Hence, hacspec offers for each type of integer (`u8`, `u32`, etc.) +a mirror secret integer type (`U8`, `U32`, etc.) for which operations +that break constant-timedness are forbidden. + +This public/private distinction can be found at a lot of places in the standard +library, and is made to forbid functions and data structures from leaking secrets. + +Conversions between public and secret integers are restricted to two functions: +`classify` and `declassify`. + +## Abstract integers + +Some cryptographic specifications talk about modular arithmetic in large +fields, whose size overflows even `u128`. To ease the expression of such +specifications, hacspec offers wrapper types around `BigInt` that can be +declared using the following API: + +```rust, noplaypen +abstract_nat_mod!( + NameOfModularInts, + NameOfUnderlyingByteRepresentation, + 256, // Number of bits for the representation of the big integer, + "ffffffffffffffff00000000000065442", // Hex representation of the modulo value as hex +) + +abstract_public_nat_mod!( + ... // Public version of above +) +``` + +## Integers as bytes + +It is often useful to view an integer as a sequence of bytes that can be +manipulated individually. The hacspec standard library provides a number +of function to translate back and forth from integer to sequence of bytes: + +```rust, noplaypen +pub fn u16_to_le_bytes(x: u16) -> u16Word; + +pub fn u16_from_le_bytes(s: u16Word) -> u16; + +pub fn U64_to_be_bytes(x: U64) -> U64Word; + +pub fn U64_from_be_bytes(s: U64Word) -> U64; + +... +``` diff --git a/book/archive/src/std/readme.md b/book/archive/src/std/readme.md new file mode 100644 index 000000000..039253473 --- /dev/null +++ b/book/archive/src/std/readme.md @@ -0,0 +1,15 @@ +# The hacspec std library + +The hacspec standard library contains a host of functions, type generators +and methods that define the base objects manipulated in classic cryptographic +primitives. + +Methods in the standard library can be divided into three categories: +1. The `not_hacspec` methods whose signature and body does not belong to the +hacspec fragment of Rust. They should not be used in hacspec code, but can +be used as helpers for e.g. testing. +2. The `unsafe_hacspec` methods whose signature belongs to hacspec but not +the body. These methods can be used in hacspec programs but their body +is part of the trusted codebase. +3. The `in_hacspec` methods whose signatures and bodies belong to the +hacspec fragment of Rust. These can be used safely in hacspec programs. diff --git a/book/archive/src/std/seq.md b/book/archive/src/std/seq.md new file mode 100644 index 000000000..319f3d5e2 --- /dev/null +++ b/book/archive/src/std/seq.md @@ -0,0 +1,58 @@ +# Sequence and array operations + +## Operations common to sequences and arrays + +### Base traits + +Some operations are common to both [sequences and arrays](/book/language/seq.md) +by design, and can be used as the interoperability base between the two types +of collections. These operations are the following: +* `len`: gives the length of an array or sequence; +* `iter`: iterates over the content of the array or sequence +(unsafe in hacspec but can be used for implementing primitives) +* `create`: creates a sequence or array and initializes the elements to the +default value (0 for arithmetic types); +* `update_slice`, `update` and `update_start`: produce a new sequence or array +with modified contents. + +Both sequences and arrays implement indexing with any type of unsigned public +integer. + +### Chunking + +Both arrays and sequences support chunking with methods like: +* `num_chunks` and `num_exact_chunks` (whole or partial blocks); +* `get_chunk`, `get_exact_chunk` and `get_remainder_chunk`; +* `set_chunk` and `set_exact_chunk`. + +The read operations borrow the sequence or array, but the write operations +create a new sequence or array. + +### Conversions + +Sequences and arrays can be created from other types via methods like: +* `from_public_slice` and `from_slice`; +* `from_vec` and `from_native_slice`; +* `from_public_seq` and `from_seq` (to convert a seq into an array of the correct size); +* `from_string` and `from_hex` for byte or hex strings (hex only for `u8` sequences and arrays). + +### Secrecy + +The methods prefixed by `public` performs an element-wise classification of the +data under the hood. + +### Ownage + +Some methods have two versions: an `owned` and a non-`owned` version, depending +on whether the `self` argument is consumed or not by the method. This distinction +is useful to avoid unnecessary copies and thus be more performant. + +## Array-specific operations + +Since array length is known statically, `new` does not take any argument, +same as `length`. `slice`s of arrays become `Seq`. + +## Sequence-specific operations + +Sequences can be extended (by creating a new sequence under the hood) with +`push` or `concat`. Sequences can also be sliced with `slice`. diff --git a/book/archive/src/usage/readme.md b/book/archive/src/usage/readme.md new file mode 100644 index 000000000..8f04b05ad --- /dev/null +++ b/book/archive/src/usage/readme.md @@ -0,0 +1 @@ +# Usage diff --git a/book/archive/src/usage/specifications.md b/book/archive/src/usage/specifications.md new file mode 100644 index 000000000..247b1857d --- /dev/null +++ b/book/archive/src/usage/specifications.md @@ -0,0 +1 @@ +# Specifications diff --git a/book/archive/src/usage/test_vectors.md b/book/archive/src/usage/test_vectors.md new file mode 100644 index 000000000..4e7735f6c --- /dev/null +++ b/book/archive/src/usage/test_vectors.md @@ -0,0 +1 @@ +# Test Vectors diff --git a/book/archive/src/usage/verification.md b/book/archive/src/usage/verification.md new file mode 100644 index 000000000..d7ae51f2d --- /dev/null +++ b/book/archive/src/usage/verification.md @@ -0,0 +1,65 @@ +# Verification + +## Coq + +### QuickCheck / QuickChick + +You can test your hacspec code using [QuickCheck](https://github.com/BurntSushi/quickcheck) (a Rust library for randomized property-based testing), by simply implementing `quickcheck::Arbitrary` for the type you want to generate tests for. For example: +```rust,ignore +impl Arbitrary for Fp { + fn arbitrary(g: &mut Gen) -> Fp { + let mut a: [u64; 6] = [0; 6]; + for i in 0..6 { + a[i] = u64::arbitrary(g); + } + let mut b: [u8; 48] = [0; 48]; + for i in 0..6 { + let val: u64 = a[i]; + b[(i*8)..((i+1)*8)].copy_from_slice(&(val.to_le_bytes())); + } + Fp::from_byte_seq_le(Seq::::from_public_slice(&b)) + } +} +``` +then you can use the `quickcheck` attribute, to make QuickCheck do property based testing for this function: +```rust,ignore +#[cfg(test)] +#[quickcheck] //Using the fp arbitraty implementation from above to generate fp2 elements. +fn test_fp2_prop_add_neg(a: Fp2) -> bool { + let b = fp2neg(a); + fp2fromfp(Fp::ZERO()) == fp2add(a, b) +} +``` +which will run when you do `cargo test`. If you then add the tag `#[cfg(proof)]` and export to Coq, +``` +cargo hacspec -o coq/src/.v +``` +then you get corresponding [QuickChick](https://github.com/QuickChick/QuickChick) test, +``` +Definition test_fp2_prop_add_neg (a_320 : fp2) : bool := + let b_321 := + fp2neg (a_320) in + (fp2fromfp (nat_mod_zero )) =.? (fp2add (a_320) (b_321)). + +QuickChick (forAll g_fp2 (fun a_320 : fp2 =>test_fp2_prop_add_neg a_320)). +``` +and generators will be constructed for the types automatically as, +``` +Instance show_fp : Show (fp) := Build_Show (fp) (fun x => show (GZnZ.val _ x)). +Definition g_fp : G (fp) := @bindGen Z (fp) (arbitrary) (fun x => returnGen (@Z_in_nat_mod _ x)). +Instance gen_fp : Gen (fp) := Build_Gen fp g_fp. +``` +which you can then run through coq in the folder `coq/` +``` +coqc -R src/ Hacspec src/.v +``` +Make sure you run: +``` +coqc -R src/ Hacspec src/MachineIntegers.v +coqc -R src/ Hacspec src/Lib.v +``` +or `make` to generate the `.vo` files used by `.v`. + +For more information: +- on QuickCheck (in rust): [BurntSushi/quickcheck](https://github.com/BurntSushi/quickcheck) +- on QuickChick: [Software foundations book on QuickChick](https://softwarefoundations.cis.upenn.edu/qc-current/index.html) diff --git a/book/book.toml b/book/book.toml new file mode 100644 index 000000000..c7377ded6 --- /dev/null +++ b/book/book.toml @@ -0,0 +1,10 @@ +[book] +authors = ["Franziskus Kiefer"] +language = "en" +multilingual = false +src = "src" +title = "hax" + +[output.html] +mathjax-support = true + diff --git a/book/default.nix b/book/default.nix new file mode 100644 index 000000000..a7358b93f --- /dev/null +++ b/book/default.nix @@ -0,0 +1,14 @@ +{ + stdenv, + mdbook, +}: +stdenv.mkDerivation { + name = "hax-book"; + src = ./.; + buildInputs = [mdbook]; + buildPhase = '' + mdbook build + mdbook build archive -d ../book/archive + ''; + installPhase = "mv book $out"; +} diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md new file mode 100644 index 000000000..7da2c743f --- /dev/null +++ b/book/src/SUMMARY.md @@ -0,0 +1,30 @@ +# Summary + +- [Introduction](./readme.md) +- [Examples]() +- [Quick start](quick_start/intro.md) +- [Tutorial](tutorial/readme.md) + - [Panic freedom](tutorial/panic-freedom.md) + - [Properties on functions](tutorial/properties.md) + - [Data invariants](tutorial/data-invariants.md) +- [Proofs]() + - [F*]() + - [Coq]() + - [`libcore`]() +- [Troubleshooting/FAQ](faq/into.md) + - [Command line usage]() + - [The include flag: which items should be extracted, and how?](faq/include-flags.md) +- [Contributing]() + - [Structure]() + - [Hax Cargo subcommand]() + - [Frontend: the Rustc driver]() + - [Frontend: the exporter]() + - [Engine]() + - [Backends]() + - [Utilities]() + - [Libraries & Macros](contributing/libraries_macros.md) + - [`libcore`]() + +--- +[Contributors]() +[Archive](misc/archive.md) diff --git a/book/src/contributing/backends.md b/book/src/contributing/backends.md new file mode 100644 index 000000000..e69de29bb diff --git a/book/src/contributing/engine.md b/book/src/contributing/engine.md new file mode 100644 index 000000000..e69de29bb diff --git a/book/src/contributing/exporter.md b/book/src/contributing/exporter.md new file mode 100644 index 000000000..e69de29bb diff --git a/book/src/contributing/hax-cargo-subcommand.md b/book/src/contributing/hax-cargo-subcommand.md new file mode 100644 index 000000000..e69de29bb diff --git a/book/src/contributing/libcore.md b/book/src/contributing/libcore.md new file mode 100644 index 000000000..e69de29bb diff --git a/book/src/contributing/libraries_macros.md b/book/src/contributing/libraries_macros.md new file mode 100644 index 000000000..dfd145c61 --- /dev/null +++ b/book/src/contributing/libraries_macros.md @@ -0,0 +1,25 @@ +# Libraries + +# Macros and attributes +The hax engine understands only one attribute: `#[_hax::json(PAYLOAD)]`, +where `PAYLOAD` is a JSON serialization of the Rust enum +`hax_lib_macros_types::AttrPayload`. + +Note `#[_hax::json(PAYLOAD)]` is a [tool +attribute](https://github.com/rust-lang/rust/issues/66079): an +attribute that is never expanded. + +In the engine, the OCaml module `Attr_payloads` offers an API to query +attributes easily. The types in crate `hax_lib_macros_types` and +corresponding serializers/deserializers are automatically generated in +OCaml, thus there is no manual parsing involved. + +## User experience +Asking the user to type `#[_hax::json(some_long_json)]` is not very +friendly. Thus, the crate `hax-lib-macros` defines a bunch of [proc +macros](https://doc.rust-lang.org/beta/reference/procedural-macros.html) +that defines nice and simple-to-use macros. Those macro take care of +cooking some `hax_lib_macros_types::AttrPayload` payload(s), then +serialize those payloads to JSON and produce one or more +`#[_hax::json(serialized_payload)]` attributes. + diff --git a/book/src/contributing/readme.md b/book/src/contributing/readme.md new file mode 100644 index 000000000..e69de29bb diff --git a/book/src/contributing/rustc-driver.md b/book/src/contributing/rustc-driver.md new file mode 100644 index 000000000..e69de29bb diff --git a/book/src/contributing/structure.md b/book/src/contributing/structure.md new file mode 100644 index 000000000..e69de29bb diff --git a/book/src/contributing/utilities.md b/book/src/contributing/utilities.md new file mode 100644 index 000000000..e69de29bb diff --git a/book/src/examples/readme.md b/book/src/examples/readme.md new file mode 100644 index 000000000..e69de29bb diff --git a/book/src/faq/include-flags.md b/book/src/faq/include-flags.md new file mode 100644 index 000000000..ff6fbe1d6 --- /dev/null +++ b/book/src/faq/include-flags.md @@ -0,0 +1,65 @@ +# The include flag: which items should be extracted, and how? + +Often, you need to extract only a portion of a crate. The subcommand +`cargo hax into` accepts the `-i` flag which will help you to include +or exclude items from the extraction. + +Consider the following `lib.rs` module of a crate named `mycrate`. + +```rust +fn interesting_function() { aux() } +fn aux() { foo::f() } +fn something_else() { ... } +mod foo { + fn f() { ... } + fn g() { ... } + fn h() { ... } + fn interesting_function() { something() } + fn something() { ... } + mod bar { + fn interesting_function() { ... } + } +} +fn not_that_one() { not_that_one_dependency() } +fn not_that_one_dependency() { ... } +``` + +Here are a few examples of the `-i` flag. + - `cargo hax into -i '-** +mycrate::**::interesting_function' ` + The first clause `-**` makes items not to be extracted by default. + This extracts any item that matches the [glob pattern](https://en.wikipedia.org/wiki/Glob_(programming)) `mycrate::**::interesting_function`, but also any (local) dependencies of such items. `**` matches any sub-path. + Thus, the following items will be extracted: + + `mycrate::interesting_function` (direct match); + + `mycrate::foo::interesting_function` (direct match); + + `mycrate::foo::bar::interesting_function` (direct match); + + `mycrate::aux` (dependency of `mycrate::interesting_function`); + + `mycrate::foo::f` (dependency of `mycrate::aux`); + + `mycrate::foo::something` (dependency of `mycrate::foo::interesting_function`). + - `cargo hax into -i '+** -*::not_that_one' ` + Extracts any item but the ones named `::not_that_one`. Here, + everything is extracted but `mycrate::not_that_one`, including + `mycrate::not_that_one_dependency`. + - `cargo hax into -i '-** +!mycrate::interesting_function' ` + Extracts only `mycrate::interesting_function`, not taking into + account dependencies. + - `cargo hax into -i '-** +~mycrate::interesting_function' ` + Extracts `mycrate::interesting_function` and its direct + dependencies (no transitivity): this includes `mycrate::aux`, but + not `mycrate::foo::f`. + +Now, suppose we add the function `not_extracting_function` +below. `not_extracting_function` uses some unsafe code: this is not +supported by hax. However, let's suppose we have a functional model +for this function and that we still want to extract it as an +axiomatized, assumed symbol. +```rust +fn not_extracting_function(u8) -> u8 { + ... + unsafe { ... } + ... +} +``` + + - `cargo hax into -i '+:mycrate::not_extracting_function' ` + Extracts `mycrate::not_extracting_function` in signature-only mode. + diff --git a/book/src/faq/into.md b/book/src/faq/into.md new file mode 100644 index 000000000..cefa77ebd --- /dev/null +++ b/book/src/faq/into.md @@ -0,0 +1,3 @@ +# Troubleshooting/FAQ + +This chapter captures a list of common questions or issues and how to resolve them. If you happen to run into an issue that is not documented here, please consider submitting a pull request! diff --git a/book/src/misc/archive.md b/book/src/misc/archive.md new file mode 100644 index 000000000..923376fd0 --- /dev/null +++ b/book/src/misc/archive.md @@ -0,0 +1,7 @@ + +# Warning: this book is currently being rewritten! + +hax is the successor of hacspec. You can find the previous book +describing hacspec [here](../archive/index.html), but keep in mind most of the information +there is outdated. + diff --git a/book/src/misc/contributors.md b/book/src/misc/contributors.md new file mode 100644 index 000000000..e69de29bb diff --git a/book/src/proofs/coq.md b/book/src/proofs/coq.md new file mode 100644 index 000000000..e69de29bb diff --git a/book/src/proofs/fstar.md b/book/src/proofs/fstar.md new file mode 100644 index 000000000..e69de29bb diff --git a/book/src/proofs/libcore.md b/book/src/proofs/libcore.md new file mode 100644 index 000000000..e69de29bb diff --git a/book/src/proofs/readme.md b/book/src/proofs/readme.md new file mode 100644 index 000000000..e69de29bb diff --git a/book/src/quick_start/intro.md b/book/src/quick_start/intro.md new file mode 100644 index 000000000..341bcf01f --- /dev/null +++ b/book/src/quick_start/intro.md @@ -0,0 +1,86 @@ +# Quick start with hax and F* + +Do you want to try hax out on a Rust crate of yours? This chapter is +what you are looking for! + +## Setup the tools + + - **user-checkable** [Install the hax toolchain](https://github.com/hacspec/hax?tab=readme-ov-file#installation). + ๐Ÿช„ Running `cargo hax --version` should print some version info. + - **user-checkable** [Install F*](https://github.com/FStarLang/FStar/blob/master/INSTALL.md) *(optional: only if want to run F\*)* + +## Setup the crate you want to verify + +*Note: the instructions below assume you are in the folder of the specific crate (**not workspace!**) you want to extract.* + +*Note: this part is useful only if you want to run F\*.* + + + - **user-checkable** Create the folder `proofs/fstar/extraction` folder, right next to the `Cargo.toml` of the crate you want to verify. + ๐Ÿช„ `mkdir -p proofs/fstar/extraction` + - **user-checkable** Copy [this makefile](https://gist.github.com/W95Psp/4c304132a1f85c5af4e4959dd6b356c3) to `proofs/fstar/extraction/Makefile`. + ๐Ÿช„ `curl -o proofs/fstar/extraction/Makefile https://gist.githubusercontent.com/W95Psp/4c304132a1f85c5af4e4959dd6b356c3/raw/Makefile` + - **user-checkable** Add `hax-lib` as a dependency to your crate. + ๐Ÿช„ `cargo add --git https://github.com/hacspec/hax hax-lib` + ๐Ÿช„ *(`hax-lib` is not mandatory, but this guide assumes it is present)* + +## Partial extraction + +*Note: the instructions below assume you are in the folder of the +specific crate you want to extract.* + +Run the command `cargo hax into fstar` to extract every item of your +crate as F* modules in the subfolder `proofs/fstar/extraction`. + +**What is critical? What is worth verifying?** +Probably, your Rust crate contains mixed kinds of code: some parts are +critical (e.g. the library functions at the core of your crate) while +some others are not (e.g. the binary driver that wraps the +library). In this case, you likely want to extract only partially your +crate, so that you can focus on the important part. + +**Partial extraction.** +If you want to extract a function +`your_crate::some_module::my_function`, you need to tell `hax` to +extract nothing but `my_function`: + +```bash +cargo hax into -i '-** +your_crate::some_module::my_function' fstar +``` + +Note this command will extract `my_function` but also any item +(function, type, etc.) from your crate which is used directly or +indirectly by `my_function`. If you don't want the dependency, use +`+!` instead of `+` in the `-i` flag. + +**Unsupported Rust code.** +hax [doesn't support every Rust +constructs](https://github.com/hacspec/hax?tab=readme-ov-file#supported-subset-of-the-rust-language), +`unsafe` code, or complicated mutation scheme. That is another reason +for extracting only a part of your crate. When running hax, if an item +of your crate, say a function `my_crate::f`, is not handled by hax, +you can append `-my_crate::f` to the `-i` flag. You can learn more +about the `-i` flag [in the FAQ](../faq/include-flags.html). + + + +## Start F* verification +After running the hax toolchain on your Rust code, you will end up +with various F* modules in the `proofs/fstar/extraction` folder. The +`Makefile` in `proofs/fstar/extraction` will run F*. + +1. **Lax check:** the first step is to run `OTHERFLAGS="--lax" make`, + which will run F* in "lax" mode. The lax mode just makes sure basic + typechecking works: it is not proving anything. This first step is + important because there might be missing libraries. If F* is not + able to find a definition, it is probably a `libcore` issue: you + probably need to edit the F* library, which lives in the + `proofs-libs` directory in the root of the hax repo. +2. **Typecheck:** the second step is to run `make`. This will ask F* + to typecheck fully your crate. This is very likely that you need to + add preconditions and postconditions at this stage. Indeed, this + second step is about panic freedom: if F* can typecheck your crate, + it means your code *never* panics, which already is an important + property. + +To go further, please read the next chapter. diff --git a/book/src/readme.md b/book/src/readme.md new file mode 100644 index 000000000..c4880e4ce --- /dev/null +++ b/book/src/readme.md @@ -0,0 +1,14 @@ +# Introduction + +hax is a tool for high assurance translations that translates a large subset of +Rust into formal languages such as [F\*](https://www.fstar-lang.org/) or [Coq](https://coq.inria.fr/). +This extends the scope of the hacspec project, which was previously a DSL embedded in Rust, +to a usable tool for verifying Rust programs. + +> So what is **hacspec** now? + +hacspec is the functional subset of Rust that can be used, together with a hacspec +standard library, to write succinct, executable, and verifiable specifications in +Rust. +These specifications can be translated into formal languages with hax. + diff --git a/book/src/tutorial/Cargo.lock b/book/src/tutorial/Cargo.lock new file mode 100644 index 000000000..9675766ca --- /dev/null +++ b/book/src/tutorial/Cargo.lock @@ -0,0 +1,239 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "cfg-if" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" + +[[package]] +name = "dyn-clone" +version = "1.0.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0d6ef0072f8a535281e4876be788938b528e9a1d43900b82c2569af7da799125" + +[[package]] +name = "getrandom" +version = "0.2.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "190092ea657667030ac6a35e305e62fc4dd69fd98ac98631e5d3a2b1575a12b5" +dependencies = [ + "cfg-if", + "libc", + "wasi", +] + +[[package]] +name = "hax-lib" +version = "0.1.0-pre.1" +source = "git+https://github.com/hacspec/hax#d668de4d17e5ddee3a613068dc30b71353a9db4f" + +[[package]] +name = "hax-lib-macros" +version = "0.1.0-pre.1" +source = "git+https://github.com/hacspec/hax#d668de4d17e5ddee3a613068dc30b71353a9db4f" +dependencies = [ + "hax-lib-macros-types", + "proc-macro-error", + "proc-macro2", + "quote", + "syn 2.0.52", +] + +[[package]] +name = "hax-lib-macros-types" +version = "0.1.0-pre.1" +source = "git+https://github.com/hacspec/hax#d668de4d17e5ddee3a613068dc30b71353a9db4f" +dependencies = [ + "proc-macro2", + "quote", + "schemars", + "serde", + "serde_json", + "uuid", +] + +[[package]] +name = "itoa" +version = "1.0.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b1a46d1a171d865aa5f83f92695765caa047a9b4cbae2cbf37dbd613a793fd4c" + +[[package]] +name = "libc" +version = "0.2.153" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9c198f91728a82281a64e1f4f9eeb25d82cb32a5de251c6bd1b5154d63a8e7bd" + +[[package]] +name = "proc-macro-error" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c" +dependencies = [ + "proc-macro-error-attr", + "proc-macro2", + "quote", + "syn 1.0.109", + "version_check", +] + +[[package]] +name = "proc-macro-error-attr" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869" +dependencies = [ + "proc-macro2", + "quote", + "version_check", +] + +[[package]] +name = "proc-macro2" +version = "1.0.79" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e835ff2298f5721608eb1a980ecaee1aef2c132bf95ecc026a11b7bf3c01c02e" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.35" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "291ec9ab5efd934aaf503a6466c5d5251535d108ee747472c3977cc5acc868ef" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "ryu" +version = "1.0.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e86697c916019a8588c99b5fac3cead74ec0b4b819707a682fd4d23fa0ce1ba1" + +[[package]] +name = "schemars" +version = "0.8.16" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "45a28f4c49489add4ce10783f7911893516f15afe45d015608d41faca6bc4d29" +dependencies = [ + "dyn-clone", + "schemars_derive", + "serde", + "serde_json", +] + +[[package]] +name = "schemars_derive" +version = "0.8.16" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c767fd6fa65d9ccf9cf026122c1b555f2ef9a4f0cea69da4d7dbc3e258d30967" +dependencies = [ + "proc-macro2", + "quote", + "serde_derive_internals", + "syn 1.0.109", +] + +[[package]] +name = "serde" +version = "1.0.197" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3fb1c873e1b9b056a4dc4c0c198b24c3ffa059243875552b2bd0933b1aee4ce2" +dependencies = [ + "serde_derive", +] + +[[package]] +name = "serde_derive" +version = "1.0.197" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7eb0b34b42edc17f6b7cac84a52a1c5f0e1bb2227e997ca9011ea3dd34e8610b" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.52", +] + +[[package]] +name = "serde_derive_internals" +version = "0.26.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "85bf8229e7920a9f636479437026331ce11aa132b4dde37d121944a44d6e5f3c" +dependencies = [ + "proc-macro2", + "quote", + "syn 1.0.109", +] + +[[package]] +name = "serde_json" +version = "1.0.114" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c5f09b1bd632ef549eaa9f60a1f8de742bdbc698e6cee2095fc84dde5f549ae0" +dependencies = [ + "itoa", + "ryu", + "serde", +] + +[[package]] +name = "syn" +version = "1.0.109" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "syn" +version = "2.0.52" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b699d15b36d1f02c3e7c69f8ffef53de37aefae075d8488d4ba1a7788d574a07" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "tutorial-src" +version = "0.1.0" +dependencies = [ + "hax-lib", + "hax-lib-macros", +] + +[[package]] +name = "unicode-ident" +version = "1.0.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b" + +[[package]] +name = "uuid" +version = "1.7.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f00cc9702ca12d3c81455259621e676d0f7251cec66a21e98fe2e9a37db93b2a" +dependencies = [ + "getrandom", +] + +[[package]] +name = "version_check" +version = "0.9.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f" + +[[package]] +name = "wasi" +version = "0.11.0+wasi-snapshot-preview1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" diff --git a/book/src/tutorial/Cargo.toml b/book/src/tutorial/Cargo.toml new file mode 100644 index 000000000..d2fd3154e --- /dev/null +++ b/book/src/tutorial/Cargo.toml @@ -0,0 +1,12 @@ +[package] +name = "tutorial-src" +version = "0.1.0" +edition = "2021" + +[lib] +path = "sources.rs" + +[dependencies] +hax-lib = { git = "https://github.com/hacspec/hax", version = "0.1.0-pre.1" } +hax-lib-macros = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax" } +# hax-lib = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax"} diff --git a/book/src/tutorial/Sources.fst b/book/src/tutorial/Sources.fst new file mode 100644 index 000000000..cedf378a5 --- /dev/null +++ b/book/src/tutorial/Sources.fst @@ -0,0 +1,110 @@ +module Tutorial_src +#set-options "--fuel 0 --ifuel 1 --z3rlimit 150" +open Core +open FStar.Mul + +// ANCHOR: F3 +type t_F3 = + | F3_E1 : t_F3 + | F3_E2 : t_F3 + | F3_E3 : t_F3 + +let t_F3_cast_to_repr (x: t_F3) : isize = + match x with + | F3_E1 -> isz 0 + | F3_E2 -> isz 1 + | F3_E3 -> isz 3 +// ANCHOR_END: F3 + +// ANCHOR: barrett +unfold +let t_FieldElement = i32 + +let v_BARRETT_MULTIPLIER: i64 = 20159L + +let v_BARRETT_R: i64 = 67108864L + +let v_BARRETT_SHIFT: i64 = 26L + +let v_FIELD_MODULUS: i32 = 3329l + +let barrett_reduce (value: i32) + : Pure i32 + (requires + (Core.Convert.f_from value <: i64) >=. (Core.Ops.Arith.Neg.neg v_BARRETT_R <: i64) && + (Core.Convert.f_from value <: i64) <=. v_BARRETT_R) + (ensures + fun result -> + let result:i32 = result in + result >. (Core.Ops.Arith.Neg.neg v_FIELD_MODULUS <: i32) && result <. v_FIELD_MODULUS && + (result %! v_FIELD_MODULUS <: i32) =. (value %! v_FIELD_MODULUS <: i32)) = + let t:i64 = (Core.Convert.f_from value <: i64) *! v_BARRETT_MULTIPLIER in + let t:i64 = t +! (v_BARRETT_R >>! 1l <: i64) in + let quotient:i64 = t >>! v_BARRETT_SHIFT in + let quotient:i32 = cast (quotient <: i64) <: i32 in + let sub:i32 = quotient *! v_FIELD_MODULUS in + let _:Prims.unit = Tutorial_src.Math.Lemmas.cancel_mul_mod quotient 3329l in + value -! sub +// ANCHOR_END: barrett + +// ANCHOR: encrypt_decrypt +let decrypt (ciphertext key: u32) : u32 = ciphertext ^. key + +let encrypt (plaintext key: u32) : u32 = plaintext ^. key +// ANCHOR_END: encrypt_decrypt + + + + + + + +// ANCHOR: encrypt_decrypt_identity +let encrypt_decrypt_identity (key plaintext: u32) + : Lemma (requires true) + (ensures (decrypt (encrypt plaintext key <: u32) key <: u32) =. plaintext) = () +// ANCHOR_END: encrypt_decrypt_identity + +// ANCHOR: square +let square (x: u8) : u8 = x *! x +// ANCHOR_END: square + +// ANCHOR: square_ensures +let square_ensures (x: u8) + : Pure u8 + (requires x <. 16uy) + (ensures fun result -> result >=. x) + = x *! x +// ANCHOR_END: square_ensures + +// ANCHOR: square_option +let square_option (x: u8) : Core.Option.t_Option u8 = + if x >=. 16uy + then Core.Option.Option_None <: Core.Option.t_Option u8 + else Core.Option.Option_Some (x *! x) <: Core.Option.t_Option u8 +// ANCHOR_END: square_option + +// ANCHOR: square_requires +let square_requires (x: u8) + : Pure u8 (requires x <. 16uy) (requires fun _ -> True) + = x *! x +// ANCHOR_END: square_requires + +// ANCHOR: F +let v_Q: u16 = 2347us + +type t_F = { f_v:f_v: u16{f_v <. v_Q} } +// ANCHOR_END: F + +// ANCHOR: AddF +[@@ FStar.Tactics.Typeclasses.tcinstance] +let impl: Core.Ops.Arith.t_Add t_F t_F = + { + f_Output = t_F; + f_add_pre = (fun (self: t_F) (rhs: t_F) -> true); + f_add_post = (fun (self: t_F) (rhs: t_F) (out: t_F) -> true); + f_add = fun (self: t_F) (rhs: t_F) -> { + f_v = (self.f_v +! rhs.f_v <: u16) %! v_Q + } <: t_F + } +// ANCHOR_END: AddF diff --git a/book/src/tutorial/data-invariants.md b/book/src/tutorial/data-invariants.md new file mode 100644 index 000000000..a6777795f --- /dev/null +++ b/book/src/tutorial/data-invariants.md @@ -0,0 +1,78 @@ +# Data invariants + +In the two previous chapters we saw how to write specifications on +functions, be it with pre and post-condition or with lemmas. In this +chapter, we will see how to maintain invariants with precise types. + +## Making illegal states unpresentable +With the Barrett example, we were working on a certain field, whose +elements were represented as `i32` integers. To simplify, let's +consider `Fโ‚ƒ`, the finite field with 3 elements (say `0`, `1` and +`2`). Every element of `F3` can be represented as a `i32` integers, +but the converse doesn't hold: the vast majority of `i32` integers are +not in of `Fโ‚ƒ`. + +Representing `Fโ‚ƒ` as `i32`s, every time we define a function consuming +`Fโ‚ƒ` elements, we face the risk to consume *illegal* elements. We are +thus back to [chapter 4.1](panic-freedom.md): we should panic on +illegal elements, and add hax pre-conditions on every single +function. That's not ideal: the property of being either `0`, `1` or +`2` should be encoded directly on the type representing `Fโ‚ƒ` elements. + +### `enum`s to then rescue +Rust alone already can solve our representation issues with +[enums](https://doc.rust-lang.org/book/ch06-00-enums.html)! Below, we +define the `enum` type `F3` which has only three constructor: `F3` +represent exactly the elements of `Fโ‚ƒ`, not more, not less. + +```rust,noplaypen +{{#include sources.rs:F3}} +``` +```ocaml +{{#include Sources.fst:F3}} +``` + +With `F3`, there doesn't exist illegal values at all: we can now +define [*total* +functions](https://en.wikipedia.org/wiki/Partial_function) on `Fโ‚ƒ` +elements. We dropped altogether a source of panic! + +Soon you want to work with a bigger finite field: say +`Fโ‚‚โ‚ƒโ‚„โ‚‡`. Representing this many `q` different elements with an Rust +enum would be very painful... The `enum` apporach falls appart. + +### Newtype and refinements +Since we don't want an `enum` with 2347 elements, we have to revert to +a type that can hold this many elements. The smallest integer type +large enough provided by Rust is `u16`. + +Let's define `F` a +["newtype"](https://matklad.github.io/2018/06/04/newtype-index-pattern.html): +a [struct](https://doc.rust-lang.org/book/ch05-00-structs.html) with +one `u16` field `v`. Notice the refinment annotation on `v`: the +extraction of this type `F` via hax will result in a type enforcing +`v` small enough. + +```rust,noplaypen +{{#include sources.rs:F}} +``` +```ocaml +{{#include Sources.fst:F}} +``` + +In Rust, we can now define functions that operates on type `F`, +assuming they are in bounds with respect to `Fโ‚‚โ‚ƒโ‚„โ‚‡`: every such +assumption will be checked and enforced by the proof assistant. As an +example, below is the implementation of the addition for type `F`. + +```rust,noplaypen +{{#include sources.rs:AddF}} +``` +```ocaml +{{#include Sources.fst:AddF}} +``` + +Here, F* is able to prove automatically that (1) the addition doesn't +overflow and (2) that the invariant of `F` is preserved. The +definition of type `F` in F* (named `t_F`) very explicitely requires +the invariant as a refinement on `v`. diff --git a/book/src/tutorial/panic-freedom.md b/book/src/tutorial/panic-freedom.md new file mode 100644 index 000000000..3b41af323 --- /dev/null +++ b/book/src/tutorial/panic-freedom.md @@ -0,0 +1,121 @@ +# Panic freedom + +Let's start with a simple example: a function that squares a `u8` +integer. To extract this function to F* using hax, we simply need to +run the command `cargo hax into fstar` in the directory of the crate +in which the function `square` is defined. + +*Note: throughout this tutorial, you can inspect the hax extraction to +F\* for each code Rust snippets, by clicking on the "F\* extraction" +tab.* + +```rust,noplaypen +{{#include sources.rs:square}} +``` +```ocaml +{{#include Sources.fst:square}} +``` + +Though, if we try to verify this function, F* is complaining about a +subtyping issue: F* tells us that it is not able to prove that the +result of the multiplication `x * x` fits the range of `u8`. The +multiplication `x * x` might indeed be overflowing! + +For instance, running `square(16)` panics: `16 * 16` is `256`, which +is just over `255`, the largest integer that fits `u8`. Rust does not +ensure that functions are not *total*: a function might panic at any +point, or might never terminate. + +## Rust and panicking code +Quoting the chapter [To `panic!` or Not to +`panic!`](https://doc.rust-lang.org/book/ch09-03-to-panic-or-not-to-panic.html) +from the Rust book: + +> The `panic!` macro signals that your program is in a state it can't +> handle and lets you tell the process to stop instead of trying to +> proceed with invalid or incorrect values. + +A Rust program should panics only in a situation where an assumption +or an invariant is broken: a panics models an *invalid* state. Formal +verification is about proving such invalid state cannot occur, at all. + +From this observation emerges the urge of proving Rust programs to be +panic-free! + +## Fixing our squaring function +Let's come back to our example. There is an informal assumption to the +multiplication operator in Rust: the inputs should be small enough so +that the addition doesn't overflow. + +Note that Rust also provides `wrapping_mul`, a non-panicking variant +of the multiplication on `u8` that wraps when the result is bigger +than `255`. Replacing the common multiplication with `wrapping_mul` in +`square` would fix the panic, but then, `square(256)` returns zero. +Semantically, this is not what one would expect from `square`. + +Our problem is that our function `square` is well-defined only when +its input is within `0` and `15`. + +### Solution A: reflect the partialness of the function in Rust +A first solution is to make `square` return an `Option` instead of a `u8`: +```rust,noplaypen +{{#include sources.rs:square_option}} +``` +```ocaml +{{#include Sources.fst:square_option}} +``` + +Here, F* is able to prove panic-freedom: calling `square` with any +input is safe. Though, one may argue that `square`'s input being small +enough should really be an assumption. Having to deal with the +possible integer overflowing whenever squaring is a huge burden. Can +we do better? + +### Solution B: add a precondition +The type system of Rust doesn't allow the programmer to formalize the +assumption that `multiply_by_two` expects a small `u8`. This becomes +possible using hax: one can annotate a function with a pre-condition +on its inputs. + +The pre-conditions and post-conditions on a function form a +*contract*: "if you give me some inputs that satisfies a given formula +(*the precondition*), I will produce a return value that satisfy +another formula (*the postcondition*)". Outside this contracts, +anything might happen: the function might panic, might run forever, +erase your disk, or anything. + +The helper crate +[hax-lib-macros](https://github.com/hacspec/hax/tree/main/hax-lib-macros) +provdes the `requires` +[proc-macro](https://doc.rust-lang.org/reference/procedural-macros.html) +which lets user writting pre-conditions directly in Rust. + +```rust,noplaypen +{{#include sources.rs:square_requires}} +``` +```ocaml +{{#include Sources.fst:square_requires}} +``` + +With this precondition, F* is able to prove panic freedom. From now +on, it is the responsability of the clients of `square` to respect the +contact. The next step is thus be to verify, through hax extraction, +that `square` is used correctly at every call site. + +## Common panicking situations +Mutipication is not the only panicking function provided by the Rust +library: most of the other integer arithmetic operation have such +informal assumptions. + +Another source of panics is indexing. Indexing in an array, a slice or +a vector is a partial operation: the index might be out of range. + +In the example folder of hax, you can find the [`chacha20` +example](https://github.com/hacspec/hax/blob/main/examples/chacha20/src/lib.rs) +that makes use of pre-conditions to prove panic freedom. + +Another solution for safe indexing is to use the [newtype index +pattern](https://matklad.github.io/2018/06/04/newtype-index-pattern.html), +which is [also supported by +hax](https://github.com/hacspec/hax/blob/d668de4d17e5ddee3a613068dc30b71353a9db4f/tests/attributes/src/lib.rs#L98-L126). The chapter [The newtype idiom](newtype.md) gives some. + diff --git a/book/src/tutorial/proofs/fstar/extraction/Makefile b/book/src/tutorial/proofs/fstar/extraction/Makefile new file mode 100644 index 000000000..b346e98f5 --- /dev/null +++ b/book/src/tutorial/proofs/fstar/extraction/Makefile @@ -0,0 +1,139 @@ +# This is a generically useful Makefile for F* that is self-contained +# +# It is tempting to factor this out into multiple Makefiles but that +# makes it less portable, so resist temptation, or move to a more +# sophisticated build system. +# +# We expect: +# 1. `fstar.exe` to be in PATH (alternatively, you can also set +# $FSTAR_HOME to be set to your F* repo/install directory) +# +# 2. `cargo`, `hax` and `rustup` to be installed and in PATH. +# +# 3. the extracted Cargo crate to have "hax-lib" as a dependency: +# `hax-lib = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax"}` +# +# Optionally, you can set `HACL_HOME`. +# +# ROOTS contains all the top-level F* files you wish to verify +# The default target `verify` verified ROOTS and its dependencies +# To lax-check instead, set `OTHERFLAGS="--lax"` on the command-line +# +# To make F* emacs mode use the settings in this file, you need to +# add the following lines to your .emacs +# +# (setq-default fstar-executable "/bin/fstar.exe") +# (setq-default fstar-smt-executable "/bin/z3") +# +# (defun my-fstar-compute-prover-args-using-make () +# "Construct arguments to pass to F* by calling make." +# (with-demoted-errors "Error when constructing arg string: %S" +# (let* ((fname (file-name-nondirectory buffer-file-name)) +# (target (concat fname "-in")) +# (argstr (car (process-lines "make" "--quiet" target)))) +# (split-string argstr)))) +# (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make) +# + +HACL_HOME ?= $(HOME)/.hax/hacl_home +FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe") + +CACHE_DIR ?= .cache +HINT_DIR ?= .hints + +.PHONY: all verify clean + +all: + rm -f .depend && $(MAKE) .depend + $(MAKE) verify + +# If $HACL_HOME doesn't exist, clone it +${HACL_HOME}: + mkdir -p "${HACL_HOME}" + git clone --depth 1 https://github.com/hacl-star/hacl-star.git "${HACL_HOME}" + +# By default, we process all the files in the current directory +ROOTS = $(wildcard *.fst *fsti) + +# The following is a bash script that discovers F* libraries +define FINDLIBS + # Prints a path if and only if it exists. Takes one argument: the + # path. + function print_if_exists() { + if [ -d "$$1" ]; then + echo "$$1" + fi + } + # Asks Cargo all the dependencies for the current crate or workspace, + # and extract all "root" directories for each. Takes zero argument. + function dependencies() { + cargo metadata --format-version 1 | + jq -r '.packages | .[] | .manifest_path | split("/") | .[:-1] | join("/")' + } + # Find hax libraries *around* a given path. Takes one argument: the + # path. + function find_hax_libraries_at_path() { + path="$$1" + # if there is a `proofs/fstar/extraction` subfolder, then that's a + # F* library + print_if_exists "$$path/proofs/fstar/extraction" + # Maybe the `proof-libs` folder of hax is around? + MAYBE_PROOF_LIBS=$$(realpath -q "$$path/../proof-libs/fstar") + if [ $$? -eq 0 ]; then + print_if_exists "$$MAYBE_PROOF_LIBS/core" + print_if_exists "$$MAYBE_PROOF_LIBS/rust_primitives" + fi + } + { while IFS= read path; do + find_hax_libraries_at_path "$$path" + done < <(dependencies) + } | sort -u +endef +export FINDLIBS + +FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(shell bash -c "$$FINDLIBS") + +FSTAR_FLAGS = --cmi \ + --warn_error -331 \ + --cache_checked_modules --cache_dir $(CACHE_DIR) \ + --already_cached "+Prims+FStar+LowStar+C+Spec.Loops+TestLib" \ + $(addprefix --include ,$(FSTAR_INCLUDE_DIRS)) + +FSTAR = $(FSTAR_BIN) $(FSTAR_FLAGS) + +.depend: $(HINT_DIR) $(CACHE_DIR) $(ROOTS) + $(info $(ROOTS)) + $(FSTAR) --cmi --dep full $(ROOTS) --extract '* -Prims -LowStar -FStar' > $@ + +include .depend + +$(HINT_DIR): + mkdir -p $@ + +$(CACHE_DIR): + mkdir -p $@ + +$(CACHE_DIR)/%.checked: | .depend $(HINT_DIR) $(CACHE_DIR) + $(FSTAR) $(OTHERFLAGS) $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $*).hints + +verify: $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS))) + +# Targets for interactive mode + +%.fst-in: + $(info $(FSTAR_FLAGS) \ + $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(basename $@).fst.hints) + +%.fsti-in: + $(info $(FSTAR_FLAGS) \ + $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(basename $@).fsti.hints) + + +# Clean targets + +SHELL=bash + +clean: + rm -rf $(CACHE_DIR)/* + rm *.fst + diff --git a/book/src/tutorial/proofs/fstar/extraction/Tutorial_src.Math.Lemmas.fst b/book/src/tutorial/proofs/fstar/extraction/Tutorial_src.Math.Lemmas.fst new file mode 100644 index 000000000..4148f70e3 --- /dev/null +++ b/book/src/tutorial/proofs/fstar/extraction/Tutorial_src.Math.Lemmas.fst @@ -0,0 +1,9 @@ +module Tutorial_src.Math.Lemmas +#set-options "--fuel 0 --ifuel 1 --z3rlimit 150" +open Core +open FStar.Mul + + +val cancel_mul_mod (a:i32) (n:i32 {v n >= 0}) : Lemma ((v a * v n) % v n == 0) +let cancel_mul_mod a n = + FStar.Math.Lemmas.cancel_mul_mod (v a) (v n) diff --git a/book/src/tutorial/proofs/fstar/extraction/Tutorial_src.fst b/book/src/tutorial/proofs/fstar/extraction/Tutorial_src.fst new file mode 100644 index 000000000..002994bfe --- /dev/null +++ b/book/src/tutorial/proofs/fstar/extraction/Tutorial_src.fst @@ -0,0 +1,82 @@ +module Tutorial_src +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +type t_F3 = + | F3_E1 : t_F3 + | F3_E2 : t_F3 + | F3_E3 : t_F3 + +let t_F3_cast_to_repr (x: t_F3) : isize = + match x with + | F3_E1 -> isz 0 + | F3_E2 -> isz 1 + | F3_E3 -> isz 3 + +unfold +let t_FieldElement = i32 + +let v_BARRETT_MULTIPLIER: i64 = 20159L + +let v_BARRETT_R: i64 = 67108864L + +let v_BARRETT_SHIFT: i64 = 26L + +let v_FIELD_MODULUS: i32 = 3329l + +let v_Q: u16 = 2347us + +let barrett_reduce (value: i32) + : Prims.Pure i32 + (requires + (Core.Convert.f_from value <: i64) >=. (Core.Ops.Arith.Neg.neg v_BARRETT_R <: i64) && + (Core.Convert.f_from value <: i64) <=. v_BARRETT_R) + (ensures + fun result -> + let result:i32 = result in + result >. (Core.Ops.Arith.Neg.neg v_FIELD_MODULUS <: i32) && result <. v_FIELD_MODULUS && + (result %! v_FIELD_MODULUS <: i32) =. (value %! v_FIELD_MODULUS <: i32)) = + let t:i64 = (Core.Convert.f_from value <: i64) *! v_BARRETT_MULTIPLIER in + let t:i64 = t +! (v_BARRETT_R >>! 1l <: i64) in + let quotient:i64 = t >>! v_BARRETT_SHIFT in + let quotient:i32 = cast (quotient <: i64) <: i32 in + let sub:i32 = quotient *! v_FIELD_MODULUS in + let _:Prims.unit = Tutorial_src.Math.Lemmas.cancel_mul_mod quotient 3329l in + value -! sub + +let decrypt (ciphertext key: u32) : u32 = ciphertext ^. key + +let encrypt (plaintext key: u32) : u32 = plaintext ^. key + +let encrypt_decrypt_identity (key plaintext: u32) + : Lemma (requires true) + (ensures (decrypt (encrypt plaintext key <: u32) key <: u32) =. plaintext) = () + +let square (x: u8) : u8 = x *! x + +let square_ensures (x: u8) + : Prims.Pure u8 + (requires x <. 16uy) + (ensures + fun result -> + let result:u8 = result in + result >=. x) = x *! x + +let square_option (x: u8) : Core.Option.t_Option u8 = + if x >=. 16uy + then Core.Option.Option_None <: Core.Option.t_Option u8 + else Core.Option.Option_Some (x *! x) <: Core.Option.t_Option u8 + +let square_requires (x: u8) : Prims.Pure u8 (requires x <. 16uy) (fun _ -> Prims.l_True) = x *! x + +type t_F = { f_v:f_v: u16{f_v <. v_Q} } + +[@@ FStar.Tactics.Typeclasses.tcinstance] +let impl: Core.Ops.Arith.t_Add t_F t_F = + { + f_Output = t_F; + f_add_pre = (fun (self: t_F) (rhs: t_F) -> true); + f_add_post = (fun (self: t_F) (rhs: t_F) (out: t_F) -> true); + f_add = fun (self: t_F) (rhs: t_F) -> { f_v = (self.f_v +! rhs.f_v <: u16) %! v_Q } <: t_F + } diff --git a/book/src/tutorial/properties.md b/book/src/tutorial/properties.md new file mode 100644 index 000000000..14b671c12 --- /dev/null +++ b/book/src/tutorial/properties.md @@ -0,0 +1,106 @@ +# Proving properties + +In the last chapter, we proved one property on the `square` function: +panic freedom. After adding a precondition, the signature of the +`square` function was `x:u8 -> Pure u8 (requires x <. 16uy) (ensures fun _ -> True)`. + +This contract stipulates that, given a small input, the function will +_return a value_: it will not panic or diverge. We could enrich the +contract of `square` with a post-condition about the fact it is a +increasing function: + +```rust,noplaypen +{{#include sources.rs:square_ensures}} +``` + +```ocaml +{{#include Sources.fst:square_ensures}} +``` + +Such a simple post-condition is automatically proven by F\*. The +properties of our `square` function are not fasinating. Let's study a +more interesting example: [Barrett reduction](https://en.wikipedia.org/wiki/Barrett_reduction). + +## A concrete example of contract: Barrett reduction + +While the correctness of `square` is obvious, the Barrett reduction is +not. + +Given `value` a field element (a `i32` whose absolute value is at most +`BARRET_R`), the function `barrett_reduce` defined below computes +`result` such that: + +- `result โ‰ก value (mod FIELD_MODULUS)`; +- the absolute value of `result` is bound as follows: + `|result| โ‰ค FIELD_MODULUS / 2 ยท (|value|/BARRETT_R + 1)`. + +It is easy to write this contract directly as `hax::requires` and +`hax::ensures` annotations, as shown in the snippet below. + +```rust,noplaypen +{{#include sources.rs:barrett}} +``` + +```ocaml +{{#include Sources.fst:barrett}} +``` + + + +Before returning, a lemma may have to be called in F* to prove the correctness +of the reduction. +The lemma is `Math.Lemmas.cancel_mul_mod (v quotient) 3329;`, which establishes +that `(quotient * 3329) % 3329` is zero. +With the help of that one lemma, F\* is able to prove the +reduction computes the expected result. +(We may expose lemmas like this to call from Rust directly in future.) + +This Barrett reduction examples is taken from +[libcrux](https://github.com/cryspen/libcrux/tree/main)'s proof of +Kyber which is using hax and F\*. + +This example showcases an **intrinsic proof**: the function +`barrett_reduce` not only computes a value, but it also ship a proof +that the post-condition holds. The pre-condition and post-condition +gives the function a formal specification, which is useful both for +further formal verification and for documentation purposes. + +## Extrinsic properties with lemmas + +Consider the `encrypt` and `decrypt` functions below. Those functions +have no precondition, don't have particularly interesting properties +individually. However, the compostion of the two yields an useful +property: encrypting a ciphertext and decrypting the result with a +same key produces the ciphertext again. `|c| decrypt(c, key)` is the +inverse of `|p| encrypt(p, key)`. + +```rust,noplaypen +{{#include sources.rs:encrypt_decrypt}} +``` + +```ocaml +{{#include Sources.fst:encrypt_decrypt}} +``` + +In this situation, adding a pre- or a post-condition to either +`encrypt` or `decrypt` is not useful: we want to state our inverse +property about both of them. Better, we want this property to be +stated directly in Rust: just as with pre and post-conditions, the +Rust souces should clearly state what is to be proven. + +To this end, Hax provides a macro `lemma`. Below, the Rust function +`encrypt_decrypt_identity` takes a key and a plaintext, and then +states the inverse property. The body is empty: the details of the +proof itself are not relevant, at this stage, we only care about the +statement. The proof will be completed manually in the proof +assistant. + +```rust,noplaypen +{{#include sources.rs:encrypt_decrypt_identity}} +``` + +```ocaml +{{#include Sources.fst:encrypt_decrypt_identity}} +``` diff --git a/book/src/tutorial/readme.md b/book/src/tutorial/readme.md new file mode 100644 index 000000000..dbe20068d --- /dev/null +++ b/book/src/tutorial/readme.md @@ -0,0 +1,15 @@ +# Tutorial + +This tutorial is a guide for formally verifying properties about Rust +programs using the hax toolchain. hax is a tool that translates Rust +programs to various formal programming languages. + +The formal programming languages we target are called *backends*. Some +of them, e.g. [F*](https://fstar-lang.org/) or +[Coq](https://coq.inria.fr/), are general purpose formal programming +languages. Others are specialized tools: +[ProVerif](https://bblanche.gitlabpages.inria.fr/proverif/) is +dedicated to proving properties about protocols. + +This tutorial focuses on proving properties with the +[F* programming language](https://fstar-lang.org/). diff --git a/book/src/tutorial/sources.rs b/book/src/tutorial/sources.rs new file mode 100644 index 000000000..ad12acd84 --- /dev/null +++ b/book/src/tutorial/sources.rs @@ -0,0 +1,140 @@ +use hax_lib_macros as hax; + +// ANCHOR: square +fn square(x: u8) -> u8 { + x * x +} +// ANCHOR_END: square + +// ANCHOR: square_option +fn square_option(x: u8) -> Option { + if x >= 16 { + None + } else { + Some(x * x) + } +} +// ANCHOR_END: square_option + +// ANCHOR: square_requires +#[hax_lib_macros::requires(x < 16)] +fn square_requires(x: u8) -> u8 { + x * x +} +// ANCHOR_END: square_requires + +// ANCHOR: square_ensures +#[hax::requires(x < 16)] +#[hax::ensures(|result| result >= x)] +fn square_ensures(x: u8) -> u8 { + x * x +} +// ANCHOR_END: square_ensures + +// ANCHOR: barrett +type FieldElement = i32; +const FIELD_MODULUS: i32 = 3329; +const BARRETT_SHIFT: i64 = 26; +const BARRETT_R: i64 = 0x4000000; // 2^26 +const BARRETT_MULTIPLIER: i64 = 20159; // โŒŠ(BARRETT_R / FIELD_MODULUS) + 1/2โŒ‹ + +#[hax::requires((i64::from(value) >= -BARRETT_R && i64::from(value) <= BARRETT_R))] +#[hax::ensures(|result| result > -FIELD_MODULUS && result < FIELD_MODULUS + && result % FIELD_MODULUS == value % FIELD_MODULUS)] +fn barrett_reduce(value: i32) -> i32 { + let t = i64::from(value) * BARRETT_MULTIPLIER; + let t = t + (BARRETT_R >> 1); + + let quotient = t >> BARRETT_SHIFT; + let quotient = quotient as i32; + + let sub = quotient * FIELD_MODULUS; + + // Here a lemma to prove that `(quotient * 3329) % 3329 = 0` + // may have to be called in F*. + + value - sub +} +// ANCHOR_END: barrett + +#[hax::exclude] +pub(crate) mod math { + pub(crate) mod lemmas { + pub(crate) fn cancel_mul_mod(a: i32, n: i32) {} + } +} + +// ANCHOR: encrypt_decrypt +fn encrypt(plaintext: u32, key: u32) -> u32 { + plaintext ^ key +} + +fn decrypt(ciphertext: u32, key: u32) -> u32 { + ciphertext ^ key +} +// ANCHOR_END: encrypt_decrypt + +// ANCHOR: encrypt_decrypt_identity +#[hax::lemma] +#[hax::requires(true)] +fn encrypt_decrypt_identity( + key: u32, + plaintext: u32, +) -> Proof<{ decrypt(encrypt(plaintext, key), key) == plaintext }> { +} +// ANCHOR_END: encrypt_decrypt_identity + +// ANCHOR: F3 +enum F3 { + E1, + E2, + E3, +} +// ANCHOR_END: F3 + +// ANCHOR: F +pub const Q: u16 = 2347; + +#[hax::attributes] +pub struct F { + #[refine(v < Q)] + pub v: u16, +} +// ANCHOR_END: F + +// ANCHOR: AddF +use core::ops::Add; + +impl Add for F { + type Output = Self; + fn add(self, rhs: Self) -> Self { + Self { + v: (self.v + rhs.v) % Q, + } + } +} +// ANCHOR_END: AddF + +// fn is_divisible_by(lhs: u32, rhs: u32) -> bool { +// if rhs == 0 { +// return false; +// } + +// lhs % rhs == 0 +// } + +// fn encrypt(plaintext: u32, key: u32) -> u32 { +// plaintext ^ key +// } + +// fn decrypt(ciphertext: u32, key: u32) -> u32 { +// ciphertext ^ key +// } + +// #[hax::lemma] +// #[hax::requires(true)] +// fn encrypt_decrypt_identity( +// plaintext: u32, +// key: u32, +// ) -> Proof<{ decrypt(encrypt(plaintext, key), key) == plaintext }> { +// } diff --git a/flake.nix b/flake.nix index 5799df0b0..9327e8582 100644 --- a/flake.nix +++ b/flake.nix @@ -59,6 +59,7 @@ in rec { packages = { inherit rustc ocamlformat rustfmt fstar hax-env; + hax-book = pkgs.callPackage ./book {}; hax-engine = pkgs.callPackage ./engine { hax-rust-frontend = packages.hax-rust-frontend.unwrapped; # `hax-engine-names-extract` extracts Rust names but also @@ -127,7 +128,14 @@ type = "app"; program = "${pkgs.writeScript "serve-rustc-docs" '' cd ${packages.rustc.passthru.availableComponents.rustc-docs}/share/doc/rust/html/rustc - ${pkgs.python3}/bin/python -m http.server + ${pkgs.python3}/bin/python -m http.server "$@" + ''}"; + }; + serve-book = { + type = "app"; + program = "${pkgs.writeScript "serve-book" '' + cd ${packages.hax-book} + ${pkgs.python3}/bin/python -m http.server "$@" ''}"; }; };