From 5e27e6449d4332d080da1d5d8bf660c7b8eefe46 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Tue, 31 Oct 2023 17:31:57 +0100 Subject: [PATCH 1/3] Archive old book, replace with draft one --- .envrc | 1 + .github/workflows/gh-pages.yml | 2 +- archive/book.toml | 9 +++++ archive/src/SUMMARY.md | 22 +++++++++++ {src => archive/src}/developers/compiler.md | 0 .../src}/developers/hacspec_architecture.png | Bin {src => archive/src}/developers/readme.md | 0 archive/src/examples/readme.md | 13 +++++++ {src => archive/src}/language/core.md | 0 {src => archive/src}/language/enums.md | 0 {src => archive/src}/language/errors.md | 0 {src => archive/src}/language/readme.md | 0 {src => archive/src}/language/seq.md | 0 {src => archive/src}/language/syntax.md | 0 archive/src/misc/contributors.md | 15 ++++++++ archive/src/readme.md | 25 +++++++++++++ {src => archive/src}/std/abstract_integers.md | 0 {src => archive/src}/std/arithmetic.md | 0 {src => archive/src}/std/readme.md | 0 {src => archive/src}/std/seq.md | 0 {src => archive/src}/usage/readme.md | 0 {src => archive/src}/usage/specifications.md | 0 {src => archive/src}/usage/test_vectors.md | 0 {src => archive/src}/usage/verification.md | 0 src/SUMMARY.md | 35 +++++++++--------- src/contributing/backends.md | 0 src/contributing/engine.md | 0 src/contributing/exporter.md | 0 src/contributing/hax-cargo-subcommand.md | 0 src/contributing/libcore.md | 0 src/contributing/libraries_macros.md | 0 src/contributing/readme.md | 0 src/contributing/rustc-driver.md | 0 src/contributing/structure.md | 0 src/contributing/utilities.md | 0 src/examples/readme.md | 13 ------- src/misc/archive.md | 7 ++++ src/misc/contributors.md | 15 -------- src/proofs/coq.md | 0 src/proofs/fstar.md | 0 src/proofs/libcore.md | 0 src/proofs/readme.md | 0 src/readme.md | 35 ++++++++---------- src/tutorial/readme.md | 0 44 files changed, 126 insertions(+), 66 deletions(-) create mode 100644 .envrc create mode 100644 archive/book.toml create mode 100644 archive/src/SUMMARY.md rename {src => archive/src}/developers/compiler.md (100%) rename {src => archive/src}/developers/hacspec_architecture.png (100%) rename {src => archive/src}/developers/readme.md (100%) create mode 100644 archive/src/examples/readme.md rename {src => archive/src}/language/core.md (100%) rename {src => archive/src}/language/enums.md (100%) rename {src => archive/src}/language/errors.md (100%) rename {src => archive/src}/language/readme.md (100%) rename {src => archive/src}/language/seq.md (100%) rename {src => archive/src}/language/syntax.md (100%) create mode 100644 archive/src/misc/contributors.md create mode 100644 archive/src/readme.md rename {src => archive/src}/std/abstract_integers.md (100%) rename {src => archive/src}/std/arithmetic.md (100%) rename {src => archive/src}/std/readme.md (100%) rename {src => archive/src}/std/seq.md (100%) rename {src => archive/src}/usage/readme.md (100%) rename {src => archive/src}/usage/specifications.md (100%) rename {src => archive/src}/usage/test_vectors.md (100%) rename {src => archive/src}/usage/verification.md (100%) create mode 100644 src/contributing/backends.md create mode 100644 src/contributing/engine.md create mode 100644 src/contributing/exporter.md create mode 100644 src/contributing/hax-cargo-subcommand.md create mode 100644 src/contributing/libcore.md create mode 100644 src/contributing/libraries_macros.md create mode 100644 src/contributing/readme.md create mode 100644 src/contributing/rustc-driver.md create mode 100644 src/contributing/structure.md create mode 100644 src/contributing/utilities.md create mode 100644 src/misc/archive.md create mode 100644 src/proofs/coq.md create mode 100644 src/proofs/fstar.md create mode 100644 src/proofs/libcore.md create mode 100644 src/proofs/readme.md create mode 100644 src/tutorial/readme.md diff --git a/.envrc b/.envrc new file mode 100644 index 0000000..bc49353 --- /dev/null +++ b/.envrc @@ -0,0 +1 @@ +use flake .# diff --git a/.github/workflows/gh-pages.yml b/.github/workflows/gh-pages.yml index 8215eb1..09fc750 100644 --- a/.github/workflows/gh-pages.yml +++ b/.github/workflows/gh-pages.yml @@ -19,7 +19,7 @@ jobs: with: mdbook-version: 'latest' - - run: mdbook build + - run: mdbook build && mdbook build archive -d ../book/archive - name: Deploy uses: peaceiris/actions-gh-pages@v3 diff --git a/archive/book.toml b/archive/book.toml new file mode 100644 index 0000000..530d585 --- /dev/null +++ b/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/archive/src/SUMMARY.md b/archive/src/SUMMARY.md new file mode 100644 index 0000000..6ff0d4f --- /dev/null +++ b/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/src/developers/compiler.md b/archive/src/developers/compiler.md similarity index 100% rename from src/developers/compiler.md rename to archive/src/developers/compiler.md diff --git a/src/developers/hacspec_architecture.png b/archive/src/developers/hacspec_architecture.png similarity index 100% rename from src/developers/hacspec_architecture.png rename to archive/src/developers/hacspec_architecture.png diff --git a/src/developers/readme.md b/archive/src/developers/readme.md similarity index 100% rename from src/developers/readme.md rename to archive/src/developers/readme.md diff --git a/archive/src/examples/readme.md b/archive/src/examples/readme.md new file mode 100644 index 0000000..46897ea --- /dev/null +++ b/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/src/language/core.md b/archive/src/language/core.md similarity index 100% rename from src/language/core.md rename to archive/src/language/core.md diff --git a/src/language/enums.md b/archive/src/language/enums.md similarity index 100% rename from src/language/enums.md rename to archive/src/language/enums.md diff --git a/src/language/errors.md b/archive/src/language/errors.md similarity index 100% rename from src/language/errors.md rename to archive/src/language/errors.md diff --git a/src/language/readme.md b/archive/src/language/readme.md similarity index 100% rename from src/language/readme.md rename to archive/src/language/readme.md diff --git a/src/language/seq.md b/archive/src/language/seq.md similarity index 100% rename from src/language/seq.md rename to archive/src/language/seq.md diff --git a/src/language/syntax.md b/archive/src/language/syntax.md similarity index 100% rename from src/language/syntax.md rename to archive/src/language/syntax.md diff --git a/archive/src/misc/contributors.md b/archive/src/misc/contributors.md new file mode 100644 index 0000000..adc2dc2 --- /dev/null +++ b/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/archive/src/readme.md b/archive/src/readme.md new file mode 100644 index 0000000..7f9bfcd --- /dev/null +++ b/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/src/std/abstract_integers.md b/archive/src/std/abstract_integers.md similarity index 100% rename from src/std/abstract_integers.md rename to archive/src/std/abstract_integers.md diff --git a/src/std/arithmetic.md b/archive/src/std/arithmetic.md similarity index 100% rename from src/std/arithmetic.md rename to archive/src/std/arithmetic.md diff --git a/src/std/readme.md b/archive/src/std/readme.md similarity index 100% rename from src/std/readme.md rename to archive/src/std/readme.md diff --git a/src/std/seq.md b/archive/src/std/seq.md similarity index 100% rename from src/std/seq.md rename to archive/src/std/seq.md diff --git a/src/usage/readme.md b/archive/src/usage/readme.md similarity index 100% rename from src/usage/readme.md rename to archive/src/usage/readme.md diff --git a/src/usage/specifications.md b/archive/src/usage/specifications.md similarity index 100% rename from src/usage/specifications.md rename to archive/src/usage/specifications.md diff --git a/src/usage/test_vectors.md b/archive/src/usage/test_vectors.md similarity index 100% rename from src/usage/test_vectors.md rename to archive/src/usage/test_vectors.md diff --git a/src/usage/verification.md b/archive/src/usage/verification.md similarity index 100% rename from src/usage/verification.md rename to archive/src/usage/verification.md diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 6ff0d4f..e6b54ed 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -1,22 +1,23 @@ # 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) +- [Examples]() +- [Tutorial]() +- [Proofs]() + - [F*]() + - [Coq]() + - [`libcore`]() +- [Contributing]() + - [Structure]() + - [Hax Cargo subcommand]() + - [Frontend: the Rustc driver]() + - [Frontend: the exporter]() + - [Engine]() + - [Backends]() + - [Utilities]() + - [Libraries & Macros]() + - [`libcore`]() --- -[Contributors](misc/contributors.md) +[Contributors]() +[Archive](misc/archive.md) diff --git a/src/contributing/backends.md b/src/contributing/backends.md new file mode 100644 index 0000000..e69de29 diff --git a/src/contributing/engine.md b/src/contributing/engine.md new file mode 100644 index 0000000..e69de29 diff --git a/src/contributing/exporter.md b/src/contributing/exporter.md new file mode 100644 index 0000000..e69de29 diff --git a/src/contributing/hax-cargo-subcommand.md b/src/contributing/hax-cargo-subcommand.md new file mode 100644 index 0000000..e69de29 diff --git a/src/contributing/libcore.md b/src/contributing/libcore.md new file mode 100644 index 0000000..e69de29 diff --git a/src/contributing/libraries_macros.md b/src/contributing/libraries_macros.md new file mode 100644 index 0000000..e69de29 diff --git a/src/contributing/readme.md b/src/contributing/readme.md new file mode 100644 index 0000000..e69de29 diff --git a/src/contributing/rustc-driver.md b/src/contributing/rustc-driver.md new file mode 100644 index 0000000..e69de29 diff --git a/src/contributing/structure.md b/src/contributing/structure.md new file mode 100644 index 0000000..e69de29 diff --git a/src/contributing/utilities.md b/src/contributing/utilities.md new file mode 100644 index 0000000..e69de29 diff --git a/src/examples/readme.md b/src/examples/readme.md index 46897ea..e69de29 100644 --- a/src/examples/readme.md +++ b/src/examples/readme.md @@ -1,13 +0,0 @@ -# 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/src/misc/archive.md b/src/misc/archive.md new file mode 100644 index 0000000..788afc6 --- /dev/null +++ b/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), but keep in mind most of the information +there is outdated. + diff --git a/src/misc/contributors.md b/src/misc/contributors.md index adc2dc2..e69de29 100644 --- a/src/misc/contributors.md +++ b/src/misc/contributors.md @@ -1,15 +0,0 @@ -# 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/src/proofs/coq.md b/src/proofs/coq.md new file mode 100644 index 0000000..e69de29 diff --git a/src/proofs/fstar.md b/src/proofs/fstar.md new file mode 100644 index 0000000..e69de29 diff --git a/src/proofs/libcore.md b/src/proofs/libcore.md new file mode 100644 index 0000000..e69de29 diff --git a/src/proofs/readme.md b/src/proofs/readme.md new file mode 100644 index 0000000..e69de29 diff --git a/src/readme.md b/src/readme.md index 7f9bfcd..0bc832f 100644 --- a/src/readme.md +++ b/src/readme.md @@ -1,25 +1,20 @@ # 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. +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. -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). +> So what is hacspec now? -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. +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. + +# Warning: this book is currently being rewritten! + +hax is the successor of hacspec. You can find the previous book +describing hacspec [here](/archive), but keep in mind most of the information +there is outdated. -[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/src/tutorial/readme.md b/src/tutorial/readme.md new file mode 100644 index 0000000..e69de29 From 8a2379db053628f11ffacaead7ae5c03b2510be0 Mon Sep 17 00:00:00 2001 From: Franziskus Kiefer Date: Wed, 1 Nov 2023 13:18:38 +0100 Subject: [PATCH 2/3] fix archive link --- src/misc/archive.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/misc/archive.md b/src/misc/archive.md index 788afc6..923376f 100644 --- a/src/misc/archive.md +++ b/src/misc/archive.md @@ -2,6 +2,6 @@ # Warning: this book is currently being rewritten! hax is the successor of hacspec. You can find the previous book -describing hacspec [here](/archive), but keep in mind most of the information +describing hacspec [here](../archive/index.html), but keep in mind most of the information there is outdated. From 144017888019bac228002543243ad46ab6ad8382 Mon Sep 17 00:00:00 2001 From: Franziskus Kiefer Date: Wed, 1 Nov 2023 13:22:12 +0100 Subject: [PATCH 3/3] minor text changes --- book.toml | 2 +- src/readme.md | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/book.toml b/book.toml index 530d585..c47f710 100644 --- a/book.toml +++ b/book.toml @@ -3,7 +3,7 @@ authors = ["Franziskus Kiefer"] language = "en" multilingual = false src = "src" -title = "hacspec" +title = "hax" [output.html] mathjax-support = true diff --git a/src/readme.md b/src/readme.md index 0bc832f..f10b928 100644 --- a/src/readme.md +++ b/src/readme.md @@ -5,14 +5,14 @@ Rust into formal languages such as [F\*](https://www.fstar-lang.org/) or [Coq](h 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? +> 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. -# Warning: this book is currently being rewritten! +# ⚠️ Warning: this book is currently being rewritten! ⚠️ hax is the successor of hacspec. You can find the previous book describing hacspec [here](/archive), but keep in mind most of the information