From 5bc12510b659a702347b4736fa4abd5ea5b0299f Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Tue, 16 Jul 2024 14:49:18 +0200 Subject: [PATCH 1/5] Small typo fixes. --- book/src/tutorial/panic-freedom.md | 4 ++-- book/src/tutorial/sources.rs | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/book/src/tutorial/panic-freedom.md b/book/src/tutorial/panic-freedom.md index 3b41af323..87ab4f406 100644 --- 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. diff --git a/book/src/tutorial/sources.rs b/book/src/tutorial/sources.rs index ad12acd84..e4eb8fae4 100644 --- a/book/src/tutorial/sources.rs +++ b/book/src/tutorial/sources.rs @@ -17,7 +17,7 @@ fn square_option(x: u8) -> Option { // ANCHOR_END: square_option // ANCHOR: square_requires -#[hax_lib_macros::requires(x < 16)] +#[hax::requires(x < 16)] fn square_requires(x: u8) -> u8 { x * x } From 21b0ebf186decfde9a918d26574b339d5491c965 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Tue, 16 Jul 2024 14:53:39 +0200 Subject: [PATCH 2/5] Use hax_lib_macros directly from hax_lib. --- book/src/tutorial/Cargo.toml | 2 -- book/src/tutorial/sources.rs | 24 +++++++++++------------- 2 files changed, 11 insertions(+), 15 deletions(-) diff --git a/book/src/tutorial/Cargo.toml b/book/src/tutorial/Cargo.toml index d2fd3154e..de5569b89 100644 --- 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/sources.rs b/book/src/tutorial/sources.rs index e4eb8fae4..c12cf1033 100644 --- 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 { // ANCHOR_END: square_option // ANCHOR: square_requires -#[hax::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,7 +93,7 @@ enum F3 { // ANCHOR: F pub const Q: u16 = 2347; -#[hax::attributes] +#[hax_lib::attributes] pub struct F { #[refine(v < Q)] pub v: u16, @@ -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, From e2afa0bd81fa447ef9899778d5ab2412a4c49d75 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Tue, 16 Jul 2024 15:23:16 +0200 Subject: [PATCH 3/5] Fix broken link and sentence. --- book/src/tutorial/panic-freedom.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/book/src/tutorial/panic-freedom.md b/book/src/tutorial/panic-freedom.md index 87ab4f406..38d2f2c33 100644 --- a/book/src/tutorial/panic-freedom.md +++ b/book/src/tutorial/panic-freedom.md @@ -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. From f4d3d618d6eb0ef0b29a5c496fc885a5d49fc4ab Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Tue, 16 Jul 2024 16:12:31 +0200 Subject: [PATCH 4/5] Add hax_lib namespace for refines. --- book/src/tutorial/sources.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/book/src/tutorial/sources.rs b/book/src/tutorial/sources.rs index c12cf1033..74bd51b6f 100644 --- a/book/src/tutorial/sources.rs +++ b/book/src/tutorial/sources.rs @@ -95,7 +95,7 @@ pub const Q: u16 = 2347; #[hax_lib::attributes] pub struct F { - #[refine(v < Q)] + #[hax_lib::refine(v < Q)] pub v: u16, } // ANCHOR_END: F From 1c7733c71fba1d1a6cdd4722a508786217bd542f Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Tue, 16 Jul 2024 16:16:50 +0200 Subject: [PATCH 5/5] Correct condition on absolute value of result. --- book/src/tutorial/properties.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/book/src/tutorial/properties.md b/book/src/tutorial/properties.md index 14b671c12..5e1a438ab 100644 --- 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.