Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Small typo fixes for hax book #777

Merged
merged 5 commits into from
Jul 17, 2024
Merged

Small typo fixes for hax book #777

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
5bc1251
Small typo fixes.
maximebuyse Jul 16, 2024
21b0ebf
Use hax_lib_macros directly from hax_lib.
maximebuyse Jul 16, 2024
e2afa0b
Fix broken link and sentence.
maximebuyse Jul 16, 2024
f4d3d61
Add hax_lib namespace for refines.
maximebuyse Jul 16, 2024
1c7733c
Correct condition on absolute value of result.
maximebuyse Jul 16, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 0 additions & 2 deletions book/src/tutorial/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"}
6 changes: 3 additions & 3 deletions book/src/tutorial/panic-freedom.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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.

Expand Down Expand Up @@ -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.

2 changes: 1 addition & 1 deletion book/src/tutorial/properties.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
26 changes: 12 additions & 14 deletions book/src/tutorial/sources.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,3 @@
use hax_lib_macros as hax;

// ANCHOR: square
fn square(x: u8) -> u8 {
x * x
Expand All @@ -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
}
Expand All @@ -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;
Expand All @@ -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) {}
Expand All @@ -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,
Expand All @@ -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
Expand Down Expand Up @@ -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,
Expand Down
Loading