Merge pull request #11 from hacspec/archive-old-book

Archive old book, replace with draft one
hacspec · Nov 1, 2023 · 083720b · 083720b
2 parents d6ddaf9 + 1440178
commit 083720b
Show file tree

Hide file tree

Showing 45 changed files with 127 additions and 67 deletions.
diff --git a/.envrc b/.envrc
@@ -0,0 +1 @@
+use flake .#
diff --git 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
@@ -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
@@ -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 → archive/src/developers/compiler.md b/src/developers/compiler.md → archive/src/developers/compiler.md
diff --git a/src/developers/hacspec_architecture.png → ...e/src/developers/hacspec_architecture.png b/src/developers/hacspec_architecture.png → ...e/src/developers/hacspec_architecture.png
diff --git a/src/developers/readme.md → archive/src/developers/readme.md b/src/developers/readme.md → archive/src/developers/readme.md
diff --git a/archive/src/examples/readme.md 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 → archive/src/language/core.md b/src/language/core.md → archive/src/language/core.md
diff --git a/src/language/enums.md → archive/src/language/enums.md b/src/language/enums.md → archive/src/language/enums.md
diff --git a/src/language/errors.md → archive/src/language/errors.md b/src/language/errors.md → archive/src/language/errors.md
diff --git a/src/language/readme.md → archive/src/language/readme.md b/src/language/readme.md → archive/src/language/readme.md
diff --git a/src/language/seq.md → archive/src/language/seq.md b/src/language/seq.md → archive/src/language/seq.md
diff --git a/src/language/syntax.md → archive/src/language/syntax.md b/src/language/syntax.md → archive/src/language/syntax.md
diff --git a/archive/src/misc/contributors.md 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.
diff --git a/archive/src/readme.md 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 → archive/src/std/abstract_integers.md b/src/std/abstract_integers.md → archive/src/std/abstract_integers.md
diff --git a/src/std/arithmetic.md → archive/src/std/arithmetic.md b/src/std/arithmetic.md → archive/src/std/arithmetic.md
diff --git a/src/std/readme.md → archive/src/std/readme.md b/src/std/readme.md → archive/src/std/readme.md
diff --git a/src/std/seq.md → archive/src/std/seq.md b/src/std/seq.md → archive/src/std/seq.md
diff --git a/src/usage/readme.md → archive/src/usage/readme.md b/src/usage/readme.md → archive/src/usage/readme.md
diff --git a/src/usage/specifications.md → archive/src/usage/specifications.md b/src/usage/specifications.md → archive/src/usage/specifications.md
diff --git a/src/usage/test_vectors.md → archive/src/usage/test_vectors.md b/src/usage/test_vectors.md → archive/src/usage/test_vectors.md
diff --git a/src/usage/verification.md → archive/src/usage/verification.md b/src/usage/verification.md → archive/src/usage/verification.md
diff --git 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/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
diff --git a/src/contributing/engine.md b/src/contributing/engine.md
diff --git a/src/contributing/exporter.md b/src/contributing/exporter.md
diff --git a/src/contributing/hax-cargo-subcommand.md b/src/contributing/hax-cargo-subcommand.md
diff --git a/src/contributing/libcore.md b/src/contributing/libcore.md
diff --git a/src/contributing/libraries_macros.md b/src/contributing/libraries_macros.md
diff --git a/src/contributing/readme.md b/src/contributing/readme.md
diff --git a/src/contributing/rustc-driver.md b/src/contributing/rustc-driver.md
diff --git a/src/contributing/structure.md b/src/contributing/structure.md
diff --git a/src/contributing/utilities.md b/src/contributing/utilities.md
diff --git 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
@@ -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/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.

diff --git a/src/proofs/coq.md b/src/proofs/coq.md
diff --git a/src/proofs/fstar.md b/src/proofs/fstar.md
diff --git a/src/proofs/libcore.md b/src/proofs/libcore.md
diff --git a/src/proofs/readme.md b/src/proofs/readme.md
diff --git 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