From 8455f7646ae7afb6a1fb1e279396ba47600345e4 Mon Sep 17 00:00:00 2001 From: Rui Fernandes Date: Wed, 20 Nov 2024 11:31:07 +0100 Subject: [PATCH] fix typos in the book --- book/src/tutorial/data-invariants.md | 4 ++-- book/src/tutorial/panic-freedom.md | 4 ++-- book/src/tutorial/properties.md | 4 ++-- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/book/src/tutorial/data-invariants.md b/book/src/tutorial/data-invariants.md index 285413bb2..aa84fc349 100644 --- a/book/src/tutorial/data-invariants.md +++ b/book/src/tutorial/data-invariants.md @@ -40,7 +40,7 @@ elements. We dropped altogether a source of panic! Soon you want to work with a bigger finite field: say `F₂₃₄₇`. Representing this many `q` different elements with an Rust -enum would be very painful... The `enum` apporach falls appart. +enum would be very painful... The `enum` approach falls apart. ### Newtype and refinements Since we don't want an `enum` with 2347 elements, we have to revert to @@ -92,5 +92,5 @@ impl Add for F { Here, F* is able to prove automatically that (1) the addition doesn't overflow and (2) that the invariant of `F` is preserved. The -definition of type `F` in F* (named `t_F`) very explicitely requires +definition of type `F` in F* (named `t_F`) very explicitly requires the invariant as a refinement on `v`. diff --git a/book/src/tutorial/panic-freedom.md b/book/src/tutorial/panic-freedom.md index 0ec0d5284..33c7d0d25 100644 --- a/book/src/tutorial/panic-freedom.md +++ b/book/src/tutorial/panic-freedom.md @@ -99,12 +99,12 @@ fn square_requires(x: u8) -> u8 { ``` With this precondition, F* is able to prove panic freedom. From now -on, it is the responsability of the clients of `square` to respect the +on, it is the responsibility of the clients of `square` to respect the contact. The next step is thus be to verify, through hax extraction, that `square` is used correctly at every call site. ## Common panicking situations -Mutipication is not the only panicking function provided by the Rust +Multiplication is not the only panicking function provided by the Rust library: most of the other integer arithmetic operation have such informal assumptions. diff --git a/book/src/tutorial/properties.md b/book/src/tutorial/properties.md index fb411243e..6471a35b4 100644 --- a/book/src/tutorial/properties.md +++ b/book/src/tutorial/properties.md @@ -18,7 +18,7 @@ fn square_ensures(x: u8) -> u8 { ``` Such a simple post-condition is automatically proven by F\*. The -properties of our `square` function are not fasinating. Let's study a +properties of our `square` function are not fascinating. Let's study a more interesting example: [Barrett reduction](https://en.wikipedia.org/wiki/Barrett_reduction). ## A concrete example of contract: Barrett reduction @@ -89,7 +89,7 @@ further formal verification and for documentation purposes. Consider the `encrypt` and `decrypt` functions below. Those functions have no precondition, don't have particularly interesting properties -individually. However, the compostion of the two yields an useful +individually. However, the composition of the two yields an useful property: encrypting a ciphertext and decrypting the result with a same key produces the ciphertext again. `|c| decrypt(c, key)` is the inverse of `|p| encrypt(p, key)`.