fix typos in the book

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`.

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.
 

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)`.