Merge pull request #777 from hacspec/hax-book-small-fixes

Small typo fixes for hax book
hacspec · Jul 17, 2024 · 7810f40 · 7810f40
2 parents 23e01bf + 1c7733c
commit 7810f40
Show file tree

Hide file tree

Showing 4 changed files with 16 additions and 20 deletions.
diff --git a/book/src/tutorial/Cargo.toml b/book/src/tutorial/Cargo.toml
@@ -8,5 +8,3 @@ 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/panic-freedom.md b/book/src/tutorial/panic-freedom.md
@@ -23,7 +23,7 @@ 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
+ensure that functions are *total*: a function might panic at any
 point, or might never terminate.
 
 ## Rust and panicking code
@@ -73,7 +73,7 @@ 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
+assumption that `square` expects a small `u8`. This becomes
 possible using hax: one can annotate a function with a pre-condition
 on its inputs.
 
@@ -117,5 +117,5 @@ 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.
+hax](https://github.com/hacspec/hax/blob/d668de4d17e5ddee3a613068dc30b71353a9db4f/tests/attributes/src/lib.rs#L98-L126). The [data invariants](data-invariants.md#newtype-and-refinements) chapter gives more details about this.
 
diff --git a/book/src/tutorial/properties.md b/book/src/tutorial/properties.md
@@ -32,7 +32,7 @@ Given `value` a field element (a `i32` whose absolute value is at most
 
 - `result ≡ value (mod FIELD_MODULUS)`;
 - the absolute value of `result` is bound as follows:
-  `|result| ≤ FIELD_MODULUS / 2 · (|value|/BARRETT_R + 1)`.
+  `|result| < FIELD_MODULUS`.
 
 It is easy to write this contract directly as `hax::requires` and
 `hax::ensures` annotations, as shown in the snippet below.

diff --git a/book/src/tutorial/sources.rs b/book/src/tutorial/sources.rs
@@ -1,5 +1,3 @@
-use hax_lib_macros as hax;
-
 // ANCHOR: square
 fn square(x: u8) -> u8 {
     x * x
@@ -17,15 +15,15 @@ fn square_option(x: u8) -> Option<u8> {
 // ANCHOR_END: square_option
 
 // ANCHOR: square_requires
-#[hax_lib_macros::requires(x < 16)]
+#[hax_lib::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)]
+#[hax_lib::requires(x < 16)]
+#[hax_lib::ensures(|result| result >= x)]
 fn square_ensures(x: u8) -> u8 {
     x * x
 }
@@ -38,8 +36,8 @@ 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
+#[hax_lib::requires((i64::from(value) >= -BARRETT_R && i64::from(value) <= BARRETT_R))]
+#[hax_lib::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;
@@ -57,7 +55,7 @@ fn barrett_reduce(value: i32) -> i32 {
 }
 // ANCHOR_END: barrett
 
-#[hax::exclude]
+#[hax_lib::exclude]
 pub(crate) mod math {
     pub(crate) mod lemmas {
         pub(crate) fn cancel_mul_mod(a: i32, n: i32) {}
@@ -75,8 +73,8 @@ fn decrypt(ciphertext: u32, key: u32) -> u32 {
 // ANCHOR_END: encrypt_decrypt
 
 // ANCHOR: encrypt_decrypt_identity
-#[hax::lemma]
-#[hax::requires(true)]
+#[hax_lib::lemma]
+#[hax_lib::requires(true)]
 fn encrypt_decrypt_identity(
     key: u32,
     plaintext: u32,
@@ -95,9 +93,9 @@ enum F3 {
 // ANCHOR: F
 pub const Q: u16 = 2347;
 
-#[hax::attributes]
+#[hax_lib::attributes]
 pub struct F {
-    #[refine(v < Q)]
+    #[hax_lib::refine(v < Q)]
     pub v: u16,
 }
 // ANCHOR_END: F
@@ -131,8 +129,8 @@ impl Add for F {
 //     ciphertext ^ key
 // }
 
-// #[hax::lemma]
-// #[hax::requires(true)]
+// #[hax_lib::lemma]
+// #[hax_lib::requires(true)]
 // fn encrypt_decrypt_identity(
 //     plaintext: u32,
 //     key: u32,