diff --git a/libraries/persistent_store/src/buffer.rs b/libraries/persistent_store/src/buffer.rs
index ae35089..3acd39a 100644
--- a/libraries/persistent_store/src/buffer.rs
+++ b/libraries/persistent_store/src/buffer.rs
@@ -12,6 +12,11 @@
 // See the License for the specific language governing permissions and
 // limitations under the License.
 
+//! Flash storage for testing.
+//!
+//! [`BufferStorage`] implements the flash [`Storage`] interface but doesn't interface with an
+//! actual flash storage. Instead it uses a buffer in memory to represent the storage state.
+
 use crate::{Storage, StorageError, StorageIndex, StorageResult};
 use alloc::borrow::Borrow;
 use alloc::boxed::Box;
@@ -63,8 +68,8 @@ pub struct BufferOptions {
     ///
     /// When set, the following conditions would panic:
     /// - A bit is written from 0 to 1.
-    /// - A word is written more than `max_word_writes`.
-    /// - A page is erased more than `max_page_erases`.
+    /// - A word is written more than [`Self::max_word_writes`].
+    /// - A page is erased more than [`Self::max_page_erases`].
     pub strict_mode: bool,
 }
 
@@ -110,15 +115,13 @@ impl BufferStorage {
     ///
     /// Before each subsequent mutable operation (write or erase), the delay is decremented if
     /// positive. If the delay is elapsed, the operation is saved and an error is returned.
-    /// Subsequent operations will panic until the interrupted operation is [corrupted] or the
-    /// interruption is [reset].
+    /// Subsequent operations will panic until either of:
+    /// - The interrupted operation is [corrupted](BufferStorage::corrupt_operation).
+    /// - The interruption is [reset](BufferStorage::reset_interruption).
     ///
     /// # Panics
     ///
     /// Panics if an interruption is already armed.
-    ///
-    /// [corrupted]: struct.BufferStorage.html#method.corrupt_operation
-    /// [reset]: struct.BufferStorage.html#method.reset_interruption
     pub fn arm_interruption(&mut self, delay: usize) {
         self.interruption.arm(delay);
     }
@@ -130,10 +133,8 @@ impl BufferStorage {
     /// # Panics
     ///
     /// Panics if any of the following conditions hold:
-    /// - An interruption was not [armed].
+    /// - An interruption was not [armed](BufferStorage::arm_interruption).
     /// - An interruption was armed and it has triggered.
-    ///
-    /// [armed]: struct.BufferStorage.html#method.arm_interruption
     pub fn disarm_interruption(&mut self) -> usize {
         self.interruption.get().err().unwrap()
     }
@@ -142,16 +143,14 @@ impl BufferStorage {
     ///
     /// # Panics
     ///
-    /// Panics if an interruption was not [armed].
-    ///
-    /// [armed]: struct.BufferStorage.html#method.arm_interruption
+    /// Panics if an interruption was not [armed](BufferStorage::arm_interruption).
     pub fn reset_interruption(&mut self) {
         let _ = self.interruption.get();
     }
 
     /// Corrupts an interrupted operation.
     ///
-    /// Applies the [corruption function] to the storage. Counters are updated accordingly:
+    /// Applies the corruption function to the storage. Counters are updated accordingly:
     /// - If a word is fully written, its counter is incremented regardless of whether other words
     ///   of the same operation have been fully written.
     /// - If a page is fully erased, its counter is incremented (and its word counters are reset).
@@ -159,13 +158,10 @@ impl BufferStorage {
     /// # Panics
     ///
     /// Panics if any of the following conditions hold:
-    /// - An interruption was not [armed].
+    /// - An interruption was not [armed](BufferStorage::arm_interruption).
     /// - An interruption was armed but did not trigger.
     /// - The corruption function corrupts more bits than allowed.
     /// - The interrupted operation itself would have panicked.
-    ///
-    /// [armed]: struct.BufferStorage.html#method.arm_interruption
-    /// [corruption function]: type.BufferCorruptFunction.html
     pub fn corrupt_operation(&mut self, corrupt: BufferCorruptFunction) {
         let operation = self.interruption.get().unwrap();
         let range = self.operation_range(&operation).unwrap();
@@ -217,7 +213,8 @@ impl BufferStorage {
     ///
     /// # Panics
     ///
-    /// Panics if the maximum number of erase cycles per page is reached.
+    /// Panics if the [maximum number of erase cycles per page](BufferOptions::max_page_erases) is
+    /// reached.
     fn incr_page_erases(&mut self, page: usize) {
         // Check that pages are not erased too many times.
         if self.options.strict_mode {
@@ -243,7 +240,8 @@ impl BufferStorage {
     ///
     /// # Panics
     ///
-    /// Panics if the maximum number of writes per word is reached.
+    /// Panics if the [maximum number of writes per word](BufferOptions::max_word_writes) is
+    /// reached.
     fn incr_word_writes(&mut self, index: usize, value: &[u8], complete: &[u8]) {
         let word_size = self.word_size();
         for i in 0..value.len() / word_size {
diff --git a/libraries/persistent_store/src/driver.rs b/libraries/persistent_store/src/driver.rs
index f17f576..d2baee0 100644
--- a/libraries/persistent_store/src/driver.rs
+++ b/libraries/persistent_store/src/driver.rs
@@ -12,6 +12,10 @@
 // See the License for the specific language governing permissions and
 // limitations under the License.
 
+//! Store wrapper for testing.
+//!
+//! [`StoreDriver`] wraps a [`Store`] and compares its behavior with its associated [`StoreModel`].
+
 use crate::format::{Format, Position};
 #[cfg(test)]
 use crate::StoreUpdate;
diff --git a/libraries/persistent_store/src/format.rs b/libraries/persistent_store/src/format.rs
index a70dcc4..a7dd4f5 100644
--- a/libraries/persistent_store/src/format.rs
+++ b/libraries/persistent_store/src/format.rs
@@ -12,6 +12,8 @@
 // See the License for the specific language governing permissions and
 // limitations under the License.
 
+//! Storage representation of a store.
+
 #[macro_use]
 mod bitfield;
 
@@ -26,13 +28,14 @@ use core::convert::TryFrom;
 
 /// Internal representation of a word in flash.
 ///
-/// Currently, the store only supports storages where a word is 32 bits.
+/// Currently, the store only supports storages where a word is 32 bits, i.e. the [word
+/// size](Storage::word_size) is 4 bytes.
 type WORD = u32;
 
 /// Abstract representation of a word in flash.
 ///
-/// This type is kept abstract to avoid possible confusion with `Nat` if they happen to have the
-/// same representation. This is because they have different semantics, `Nat` represents natural
+/// This type is kept abstract to avoid possible confusion with [`Nat`] if they happen to have the
+/// same representation. This is because they have different semantics, [`Nat`] represents natural
 /// numbers while `Word` represents sequences of bits (and thus has no arithmetic).
 #[derive(Clone, Copy, Debug, PartialEq, Eq)]
 pub struct Word(WORD);
@@ -47,7 +50,7 @@ impl Word {
     ///
     /// # Panics
     ///
-    /// Panics if `slice.len() != WORD_SIZE`.
+    /// Panics if `slice.len()` is not [`WORD_SIZE`] bytes.
     pub fn from_slice(slice: &[u8]) -> Word {
         Word(WORD::from_le_bytes(<WordSlice>::try_from(slice).unwrap()))
     }
@@ -60,47 +63,49 @@ impl Word {
 
 /// Size of a word in bytes.
 ///
-/// Currently, the store only supports storages where a word is 4 bytes.
+/// Currently, the store only supports storages where the [word size](Storage::word_size) is 4
+/// bytes.
 const WORD_SIZE: Nat = core::mem::size_of::<WORD>() as Nat;
 
 /// Minimum number of words per page.
 ///
-/// Currently, the store only supports storages where pages have at least 8 words.
-const MIN_NUM_WORDS_PER_PAGE: Nat = 8;
+/// Currently, the store only supports storages where pages have at least 8 [words](WORD_SIZE), i.e.
+/// the [page size](Storage::page_size) is at least 32 bytes.
+const MIN_PAGE_SIZE: Nat = 8;
 
 /// Maximum size of a page in bytes.
 ///
-/// Currently, the store only supports storages where pages are between 8 and 1024 [words].
-///
-/// [words]: constant.WORD_SIZE.html
+/// Currently, the store only supports storages where pages have at most 1024 [words](WORD_SIZE),
+/// i.e. the [page size](Storage::page_size) is at most 4096 bytes.
 const MAX_PAGE_SIZE: Nat = 4096;
 
 /// Maximum number of erase cycles.
 ///
-/// Currently, the store only supports storages where the maximum number of erase cycles fits on 16
-/// bits.
+/// Currently, the store only supports storages where the [maximum number of erase
+/// cycles](Storage::max_page_erases) fits in 16 bits, i.e. it is at most 65535.
 const MAX_ERASE_CYCLE: Nat = 65535;
 
 /// Minimum number of pages.
 ///
-/// Currently, the store only supports storages with at least 3 pages.
+/// Currently, the store only supports storages where the [number of pages](Storage::num_pages) is
+/// at least 3.
 const MIN_NUM_PAGES: Nat = 3;
 
 /// Maximum page index.
 ///
-/// Thus the maximum number of pages is one more than this number. Currently, the store only
-/// supports storages where the number of pages is between 3 and 64.
+/// Currently, the store only supports storages where the [number of pages](Storage::num_pages) is
+/// at most 64, i.e. the maximum page index is 63.
 const MAX_PAGE_INDEX: Nat = 63;
 
 /// Maximum key index.
 ///
-/// Thus the number of keys is one more than this number. Currently, the store only supports 4096
-/// keys.
+/// Currently, the store only supports 4096 keys, i.e. the maximum key index is 4095.
 const MAX_KEY_INDEX: Nat = 4095;
 
 /// Maximum length in bytes of a user payload.
 ///
-/// Currently, the store only supports values smaller than 1024 bytes.
+/// Currently, the store only supports values at most 1023 bytes long. This may be further reduced
+/// depending on the [page size](Storage::page_size), see [`Format::max_value_len`].
 const MAX_VALUE_LEN: Nat = 1023;
 
 /// Maximum number of updates per transaction.
@@ -109,9 +114,15 @@ const MAX_VALUE_LEN: Nat = 1023;
 const MAX_UPDATES: Nat = 31;
 
 /// Maximum number of words per virtual page.
-const MAX_VIRT_PAGE_SIZE: Nat = div_ceil(MAX_PAGE_SIZE, WORD_SIZE) - CONTENT_WORD;
+///
+/// A virtual page has [`CONTENT_WORD`] less [words](WORD_SIZE) than the storage [page
+/// size](Storage::page_size). Those words are used to store the page header. Since a page has at
+/// least [8](MIN_PAGE_SIZE) words, a virtual page has at least 6 words.
+const MAX_VIRT_PAGE_SIZE: Nat = MAX_PAGE_SIZE / WORD_SIZE - CONTENT_WORD;
 
 /// Word with all bits set to one.
+///
+/// After a page is erased, all words are equal to this value.
 const ERASED_WORD: Word = Word(!(0 as WORD));
 
 /// Helpers for a given storage configuration.
@@ -121,33 +132,31 @@ pub struct Format {
     ///
     /// # Invariant
     ///
-    /// - Words divide a page evenly.
-    /// - There are at least 8 words in a page.
-    /// - There are at most `MAX_PAGE_SIZE` bytes in a page.
+    /// - [Words](WORD_SIZE) divide a page evenly.
+    /// - There are at least [`MIN_PAGE_SIZE`] words in a page.
+    /// - There are at most [`MAX_PAGE_SIZE`] bytes in a page.
     page_size: Nat,
 
     /// The number of pages in the storage.
     ///
     /// # Invariant
     ///
-    /// - There are at least 3 pages.
-    /// - There are at most `MAX_PAGE_INDEX + 1` pages.
+    /// - There are at least [`MIN_NUM_PAGES`] pages.
+    /// - There are at most [`MAX_PAGE_INDEX`] + 1 pages.
     num_pages: Nat,
 
     /// The maximum number of times a page can be erased.
     ///
     /// # Invariant
     ///
-    /// - A page can be erased at most `MAX_ERASE_CYCLE` times.
+    /// - A page can be erased at most [`MAX_ERASE_CYCLE`] times.
     max_page_erases: Nat,
 }
 
 impl Format {
     /// Extracts the format from a storage.
     ///
-    /// Returns `None` if the storage is not [supported].
-    ///
-    /// [supported]: struct.Format.html#method.is_storage_supported
+    /// Returns `None` if the storage is not [supported](Format::is_storage_supported).
     pub fn new<S: Storage>(storage: &S) -> Option<Format> {
         if Format::is_storage_supported(storage) {
             Some(Format {
@@ -163,21 +172,12 @@ impl Format {
     /// Returns whether a storage is supported.
     ///
     /// A storage is supported if the following conditions hold:
-    /// - The size of a word is [`WORD_SIZE`] bytes.
-    /// - The size of a word evenly divides the size of a page.
-    /// - A page contains at least [`MIN_NUM_WORDS_PER_PAGE`] words.
-    /// - A page contains at most [`MAX_PAGE_SIZE`] bytes.
-    /// - There are at least [`MIN_NUM_PAGES`] pages.
-    /// - There are at most [`MAX_PAGE_INDEX`]` + 1` pages.
-    /// - A word can be written at least twice between erase cycles.
-    /// - The maximum number of erase cycles is at most [`MAX_ERASE_CYCLE`].
-    ///
-    /// [`WORD_SIZE`]: constant.WORD_SIZE.html
-    /// [`MIN_NUM_WORDS_PER_PAGE`]: constant.MIN_NUM_WORDS_PER_PAGE.html
-    /// [`MAX_PAGE_SIZE`]: constant.MAX_PAGE_SIZE.html
-    /// [`MIN_NUM_PAGES`]: constant.MIN_NUM_PAGES.html
-    /// [`MAX_PAGE_INDEX`]: constant.MAX_PAGE_INDEX.html
-    /// [`MAX_ERASE_CYCLE`]: constant.MAX_ERASE_CYCLE.html
+    /// - The [`Storage::word_size`] is [`WORD_SIZE`] bytes.
+    /// - The [`Storage::word_size`] evenly divides the [`Storage::page_size`].
+    /// - The [`Storage::page_size`] is between [`MIN_PAGE_SIZE`] words and [`MAX_PAGE_SIZE`] bytes.
+    /// - The [`Storage::num_pages`] is between [`MIN_NUM_PAGES`] and [`MAX_PAGE_INDEX`] + 1.
+    /// - The [`Storage::max_word_writes`] is at least 2.
+    /// - The [`Storage::max_page_erases`] is at most [`MAX_ERASE_CYCLE`].
     fn is_storage_supported<S: Storage>(storage: &S) -> bool {
         let word_size = usize_to_nat(storage.word_size());
         let page_size = usize_to_nat(storage.page_size());
@@ -186,7 +186,7 @@ impl Format {
         let max_page_erases = usize_to_nat(storage.max_page_erases());
         word_size == WORD_SIZE
             && page_size % word_size == 0
-            && (MIN_NUM_WORDS_PER_PAGE * word_size <= page_size && page_size <= MAX_PAGE_SIZE)
+            && (MIN_PAGE_SIZE * word_size <= page_size && page_size <= MAX_PAGE_SIZE)
             && (MIN_NUM_PAGES <= num_pages && num_pages <= MAX_PAGE_INDEX + 1)
             && max_word_writes >= 2
             && max_page_erases <= MAX_ERASE_CYCLE
@@ -199,28 +199,28 @@ impl Format {
 
     /// The size of a page in bytes.
     ///
-    /// We have `MIN_NUM_WORDS_PER_PAGE * self.word_size() <= self.page_size() <= MAX_PAGE_SIZE`.
+    /// This is at least [`MIN_PAGE_SIZE`] [words](WORD_SIZE) and at most [`MAX_PAGE_SIZE`] bytes.
     pub fn page_size(&self) -> Nat {
         self.page_size
     }
 
-    /// The number of pages in the storage, denoted by `N`.
+    /// The number of pages in the storage, denoted by N.
     ///
-    /// We have `MIN_NUM_PAGES <= N <= MAX_PAGE_INDEX + 1`.
+    /// We have [`MIN_NUM_PAGES`] ≤ N ≤ [`MAX_PAGE_INDEX`] + 1.
     pub fn num_pages(&self) -> Nat {
         self.num_pages
     }
 
     /// The maximum page index.
     ///
-    /// We have `2 <= self.max_page() <= MAX_PAGE_INDEX`.
+    /// This is at least [`MIN_NUM_PAGES`] - 1 and at most [`MAX_PAGE_INDEX`].
     pub fn max_page(&self) -> Nat {
         self.num_pages - 1
     }
 
-    /// The maximum number of times a page can be erased, denoted by `E`.
+    /// The maximum number of times a page can be erased, denoted by E.
     ///
-    /// We have `E <= MAX_ERASE_CYCLE`.
+    /// We have E ≤ [`MAX_ERASE_CYCLE`].
     pub fn max_page_erases(&self) -> Nat {
         self.max_page_erases
     }
@@ -235,19 +235,18 @@ impl Format {
         MAX_UPDATES
     }
 
-    /// The size of a virtual page in words, denoted by `Q`.
+    /// The size of a virtual page in words, denoted by Q.
     ///
     /// A virtual page is stored in a physical page after the page header.
     ///
-    /// We have `MIN_NUM_WORDS_PER_PAGE - 2 <= Q <= MAX_VIRT_PAGE_SIZE`.
+    /// We have [`MIN_PAGE_SIZE`] - 2 ≤ Q ≤ [`MAX_VIRT_PAGE_SIZE`].
     pub fn virt_page_size(&self) -> Nat {
         self.page_size() / self.word_size() - CONTENT_WORD
     }
 
     /// The maximum length in bytes of a user payload.
     ///
-    /// We have `(MIN_NUM_WORDS_PER_PAGE - 3) * self.word_size() <= self.max_value_len() <=
-    /// MAX_VALUE_LEN`.
+    /// This is at least [`MIN_PAGE_SIZE`] - 3 [words](WORD_SIZE) and at most [`MAX_VALUE_LEN`].
     pub fn max_value_len(&self) -> Nat {
         min(
             (self.virt_page_size() - 1) * self.word_size(),
@@ -255,57 +254,50 @@ impl Format {
         )
     }
 
-    /// The maximum prefix length in words, denoted by `M`.
+    /// The maximum prefix length in words, denoted by M.
     ///
     /// A prefix is the first words of a virtual page that belong to the last entry of the previous
     /// virtual page. This happens because entries may overlap up to 2 virtual pages.
     ///
-    /// We have `MIN_NUM_WORDS_PER_PAGE - 3 <= M < Q`.
+    /// We have [`MIN_PAGE_SIZE`] - 3 ≤ M < Q.
     pub fn max_prefix_len(&self) -> Nat {
         self.bytes_to_words(self.max_value_len())
     }
 
-    /// The total virtual capacity in words, denoted by `V`.
+    /// The total virtual capacity in words, denoted by V.
     ///
-    /// We have `V = (N - 1) * (Q - 1) - M`.
+    /// We have V = (N - 1) × (Q - 1) - M.
     ///
-    /// We can show `V >= (N - 2) * (Q - 1)` with the following steps:
-    /// - `M <= Q - 1` from `M < Q` from [`M`] definition
-    /// - `-M >= -(Q - 1)` from above
-    /// - `V >= (N - 1) * (Q - 1) - (Q - 1)` from `V` definition
-    ///
-    /// [`M`]: struct.Format.html#method.max_prefix_len
+    /// We can show V ≥ (N - 2) × (Q - 1) with the following steps:
+    /// - M ≤ Q - 1 from M < Q from [M](Format::max_prefix_len)'s definition
+    /// - -M ≥ -(Q - 1) from above
+    /// - V ≥ (N - 1) × (Q - 1) - (Q - 1) from V's definition
     pub fn virt_size(&self) -> Nat {
         (self.num_pages() - 1) * (self.virt_page_size() - 1) - self.max_prefix_len()
     }
 
-    /// The total user capacity in words, denoted by `C`.
+    /// The total user capacity in words, denoted by C.
     ///
-    /// We have `C = V - N = (N - 1) * (Q - 2) - M - 1`.
+    /// We have C = V - N = (N - 1) × (Q - 2) - M - 1.
     ///
-    /// We can show `C >= (N - 2) * (Q - 2) - 2` with the following steps:
-    /// - `V >= (N - 2) * (Q - 1)` from [`V`] definition
-    /// - `C >= (N - 2) * (Q - 1) - N` from `C` definition
-    /// - `(N - 2) * (Q - 1) - N = (N - 2) * (Q - 2) - 2` by calculus
-    ///
-    /// [`V`]: struct.Format.html#method.virt_size
+    /// We can show C ≥ (N - 2) × (Q - 2) - 2 with the following steps:
+    /// - V ≥ (N - 2) × (Q - 1) from [V](Format::virt_size)'s definition
+    /// - C ≥ (N - 2) × (Q - 1) - N from C's definition
+    /// - (N - 2) × (Q - 1) - N = (N - 2) × (Q - 2) - 2 by calculus
     pub fn total_capacity(&self) -> Nat {
         // From the virtual capacity, we reserve N - 1 words for `Erase` entries and 1 word for a
         // `Clear` entry.
         self.virt_size() - self.num_pages()
     }
 
-    /// The total virtual lifetime in words, denoted by `L`.
+    /// The total virtual lifetime in words, denoted by L.
     ///
-    /// We have `L = (E * N + N - 1) * Q`.
+    /// We have L = (E × N + N - 1) × Q.
     pub fn total_lifetime(&self) -> Position {
         Position::new(self, self.max_page_erases(), self.num_pages() - 1, 0)
     }
 
     /// Returns the word position of the first entry of a page.
-    ///
-    /// The init info of the page must be provided to know where the first entry of the page
-    /// starts.
     pub fn page_head(&self, init: InitInfo, page: Nat) -> Position {
         Position::new(self, init.cycle, page, init.prefix)
     }
@@ -557,7 +549,7 @@ impl Format {
     ///
     /// # Preconditions
     ///
-    /// - `bytes + self.word_size()` does not overflow.
+    /// - `bytes` + [`Self::word_size`] does not overflow.
     pub fn bytes_to_words(&self, bytes: Nat) -> Nat {
         div_ceil(bytes, self.word_size())
     }
@@ -571,7 +563,7 @@ const COMPACT_WORD: Nat = 1;
 
 /// The word index of the content of a page.
 ///
-/// Since a page is at least 8 words, there is always at least 6 words of content.
+/// This is also the length in words of the page header.
 const CONTENT_WORD: Nat = 2;
 
 /// The checksum for a single word.
@@ -718,21 +710,21 @@ bitfield! {
 
 /// The position of a word in the virtual storage.
 ///
-/// With the notations defined in `Format`, let:
-/// - `w` a virtual word offset in a page which is between `0` and `Q - 1`
-/// - `p` a page offset which is between `0` and `N - 1`
-/// - `c` the number of erase cycles of a page which is between `0` and `E`
+/// With the notations defined in [`Format`], let:
+/// - w denote a word offset in a virtual page, thus between 0 and Q - 1
+/// - p denote a page offset, thus between 0 and N - 1
+/// - c denote the number of times a page was erased, thus between 0 and E
 ///
-/// Then the position of a word is `(c*N + p)*Q + w`. This position monotonically increases and
+/// The position of a word is (c × N + p) × Q + w. This position monotonically increases and
 /// represents the consumed lifetime of the storage.
 ///
-/// This type is kept abstract to avoid possible confusion with `Nat` and `Word` if they happen to
-/// have the same representation. Here is an overview of their semantics:
+/// This type is kept abstract to avoid possible confusion with [`Nat`] and [`Word`] if they happen
+/// to have the same representation. Here is an overview of their semantics:
 ///
 /// | Name       | Semantics                   | Arithmetic operations | Bit-wise operations |
 /// | ---------- | --------------------------- | --------------------- | ------------------- |
-/// | `Nat`      | Natural numbers             | Yes (no overflow)     | No                  |
-/// | `Word`     | Word in flash               | No                    | Yes                 |
+/// | [`Nat`]    | Natural numbers             | Yes (no overflow)     | No                  |
+/// | [`Word`]   | Word in flash               | No                    | Yes                 |
 /// | `Position` | Position in virtual storage | Yes (no overflow)     | No                  |
 #[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord)]
 pub struct Position(Nat);
@@ -763,9 +755,9 @@ impl Position {
     /// Create a word position given its coordinates.
     ///
     /// The coordinates of a word are:
-    /// - Its word index in its page.
+    /// - Its word index in its virtual page.
     /// - Its page index in the storage.
-    /// - The number of times that page was erased.
+    /// - The number of times its page was erased.
     pub fn new(format: &Format, cycle: Nat, page: Nat, word: Nat) -> Position {
         Position((cycle * format.num_pages() + page) * format.virt_page_size() + word)
     }
@@ -928,11 +920,11 @@ pub fn is_erased(slice: &[u8]) -> bool {
 
 /// Divides then takes ceiling.
 ///
-/// Returns `ceil(x / m)` in mathematical notations (not Rust code).
+/// Returns ⌈x / m⌉, i.e. the lowest natural number r such that r ≥ x / m.
 ///
 /// # Preconditions
 ///
-/// - `x + m` does not overflow.
+/// - x + m does not overflow.
 const fn div_ceil(x: Nat, m: Nat) -> Nat {
     (x + m - 1) / m
 }
diff --git a/libraries/persistent_store/src/fragment.rs b/libraries/persistent_store/src/fragment.rs
index d19b511..661d5db 100644
--- a/libraries/persistent_store/src/fragment.rs
+++ b/libraries/persistent_store/src/fragment.rs
@@ -12,7 +12,7 @@
 // See the License for the specific language governing permissions and
 // limitations under the License.
 
-//! Helper functions for fragmented entries.
+//! Support for fragmented entries.
 //!
 //! This module permits to handle entries larger than the [maximum value
 //! length](Store::max_value_length) by storing ordered consecutive fragments in a sequence of keys.
@@ -36,7 +36,7 @@ pub trait Keys {
     ///
     /// # Preconditions
     ///
-    /// The position must be within the length: `pos < len()`.
+    /// The position must be within the length: `pos` < [`Self::len`].
     fn key(&self, pos: usize) -> usize;
 }
 
diff --git a/libraries/persistent_store/src/lib.rs b/libraries/persistent_store/src/lib.rs
index a8adc2b..e3735c3 100644
--- a/libraries/persistent_store/src/lib.rs
+++ b/libraries/persistent_store/src/lib.rs
@@ -12,191 +12,191 @@
 // See the License for the specific language governing permissions and
 // limitations under the License.
 
-// TODO(ia0): Add links once the code is complete.
+// The documentation is easier to read from a browser:
+// - Run: cargo doc --document-private-items --features=std
+// - Open: target/doc/persistent_store/index.html
+
 //! Store abstraction for flash storage
 //!
 //! # Specification
 //!
-//! The store provides a partial function from keys to values on top of a storage
-//! interface. The store total capacity depends on the size of the storage. Store
-//! updates may be bundled in transactions. Mutable operations are atomic, including
-//! when interrupted.
+//! The [store](Store) provides a partial function from keys to values on top of a
+//! [storage](Storage) interface. The store total [capacity](Store::capacity) depends on the size of
+//! the storage. Store [updates](StoreUpdate) may be bundled in [transactions](Store::transaction).
+//! Mutable operations are atomic, including when interrupted.
 //!
-//! The store is flash-efficient in the sense that it uses the storage lifetime
-//! efficiently. For each page, all words are written at least once between erase
-//! cycles and all erase cycles are used. However, not all written words are user
-//! content: lifetime is also consumed with metadata and compaction.
+//! The store is flash-efficient in the sense that it uses the storage [lifetime](Store::lifetime)
+//! efficiently. For each page, all words are written at least once between erase cycles and all
+//! erase cycles are used. However, not all written words are user content: lifetime is also
+//! consumed with metadata and compaction.
 //!
-//! The store is extendable with other entries than key-values. It is essentially a
-//! framework providing access to the storage lifetime. The partial function is
-//! simply the most common usage and can be used to encode other usages.
+//! The store is extendable with other entries than key-values. It is essentially a framework
+//! providing access to the storage lifetime. The partial function is simply the most common usage
+//! and can be used to encode other usages.
 //!
 //! ## Definitions
 //!
-//! An _entry_ is a pair of a key and a value. A _key_ is a number between 0
-//! and 4095. A _value_ is a byte slice with a length between 0 and 1023 bytes (for
-//! large enough pages).
+//! An _entry_ is a pair of a key and a value. A _key_ is a number between 0 and
+//! [4095](format::MAX_KEY_INDEX). A _value_ is a byte slice with a length between 0 and
+//! [1023](format::Format::max_value_len) bytes (for large enough pages).
 //!
 //! The store provides the following _updates_:
-//! -   Given a key and a value, `Insert` updates the store such that the value is
+//! -   Given a key and a value, [`StoreUpdate::Insert`] updates the store such that the value is
 //!     associated with the key. The values for other keys are left unchanged.
-//! -   Given a key, `Remove` updates the store such that no value is associated with
-//!     the key. The values for other keys are left unchanged. Additionally, if there
-//!     was a value associated with the key, the value is wiped from the storage
-//!     (all its bits are set to 0).
+//! -   Given a key, [`StoreUpdate::Remove`] updates the store such that no value is associated with
+//!     the key. The values for other keys are left unchanged. Additionally, if there was a value
+//!     associated with the key, the value is wiped from the storage (all its bits are set to 0).
 //!
 //! The store provides the following _read-only operations_:
-//! -   `Iter` iterates through the store returning all entries exactly once. The
-//!     iteration order is not specified but stable between mutable operations.
-//! -   `Capacity` returns how many words can be stored before the store is full.
-//! -   `Lifetime` returns how many words can be written before the storage lifetime
-//!     is consumed.
+//! -   [`Store::iter`] iterates through the store returning all entries exactly once. The iteration
+//!     order is not specified but stable between mutable operations.
+//! -   [`Store::capacity`] returns how many words can be stored before the store is full.
+//! -   [`Store::lifetime`] returns how many words can be written before the storage lifetime is
+//!     consumed.
 //!
 //! The store provides the following _mutable operations_:
-//! -   Given a set of independent updates, `Transaction` applies the sequence of
-//!     updates.
-//! -   Given a threshold, `Clear` removes all entries with a key greater or equal
-//!     to the threshold.
-//! -   Given a length in words, `Prepare` makes one step of compaction unless that
-//!     many words can be written without compaction. This operation has no effect
-//!     on the store but may still mutate its storage. In particular, the store has
-//!     the same capacity but a possibly reduced lifetime.
+//! -   Given a set of independent updates, [`Store::transaction`] applies the sequence of updates.
+//! -   Given a threshold, [`Store::clear`] removes all entries with a key greater or equal to the
+//!     threshold.
+//! -   Given a length in words, [`Store::prepare`] makes one step of compaction unless that many
+//!     words can be written without compaction. This operation has no effect on the store but may
+//!     still mutate its storage. In particular, the store has the same capacity but a possibly
+//!     reduced lifetime.
 //!
-//! A mutable operation is _atomic_ if, when power is lost during the operation, the
-//! store is either updated (as if the operation succeeded) or left unchanged (as if
-//! the operation did not occur). If the store is left unchanged, lifetime may still
-//! be consumed.
+//! A mutable operation is _atomic_ if, when power is lost during the operation, the store is either
+//! updated (as if the operation succeeded) or left unchanged (as if the operation did not occur).
+//! If the store is left unchanged, lifetime may still be consumed.
 //!
 //! The store relies on the following _storage interface_:
-//! -   It is possible to read a byte slice. The slice won't span multiple pages.
-//! -   It is possible to write a word slice. The slice won't span multiple pages.
-//! -   It is possible to erase a page.
-//! -   The pages are sequentially indexed from 0. If the actual underlying storage
-//!     is segmented, then the storage layer should translate those indices to
-//!     actual page addresses.
+//! -   It is possible to [read](Storage::read_slice) a byte slice. The slice won't span multiple
+//!     pages.
+//! -   It is possible to [write](Storage::write_slice) a word slice. The slice won't span multiple
+//!     pages.
+//! -   It is possible to [erase](Storage::erase_page) a page.
+//! -   The pages are sequentially indexed from 0. If the actual underlying storage is segmented,
+//!     then the storage layer should translate those indices to actual page addresses.
 //!
-//! The store has a _total capacity_ of `C = (N - 1) * (P - 4) - M - 1` words, where
-//! `P` is the number of words per page, `N` is the number of pages, and `M` is the
-//! maximum length in words of a value (256 for large enough pages). The capacity
-//! used by each mutable operation is given below (a transient word only uses
-//! capacity during the operation):
-//! -   `Insert` uses `1 + ceil(len / 4)` words where `len` is the length of the
-//!     value in bytes. If an entry was replaced, the words used by its insertion
-//!     are freed.
-//! -   `Remove` doesn't use capacity if alone in the transaction and 1 transient
-//!     word otherwise. If an entry was deleted, the words used by its insertion are
-//!     freed.
-//! -   `Transaction` uses 1 transient word. In addition, the updates of the
-//!     transaction use and free words as described above.
-//! -   `Clear` doesn't use capacity and frees the words used by the insertion of
-//!     the deleted entries.
-//! -   `Prepare` doesn't use capacity.
+//! The store has a _total capacity_ of C = (N - 1) × (P - 4) - M - 1 words, where:
+//! -   P is the number of words per page
+//! -   [N](format::Format::num_pages) is the number of pages
+//! -   [M](format::Format::max_prefix_len) is the maximum length in words of a value (256 for large
+//!     enough pages)
 //!
-//! The _total lifetime_ of the store is below `L = ((E + 1) * N - 1) * (P - 2)` and
-//! above `L - M` words, where `E` is the maximum number of erase cycles. The
-//! lifetime is used when capacity is used, including transiently, as well as when
-//! compaction occurs. Compaction frequency and lifetime consumption are positively
-//! correlated to the store load factor (the ratio of used capacity to total capacity).
+//! The capacity used by each mutable operation is given below (a transient word only uses capacity
+//! during the operation):
 //!
-//! It is possible to approximate the cost of transient words in terms of capacity:
-//! `L` transient words are equivalent to `C - x` words of capacity where `x` is the
-//! average capacity (including transient) of operations.
+//! | Operation/Update        | Used capacity    | Freed capacity    | Transient capacity |
+//! | ----------------------- | ---------------- | ----------------- | ------------------ |
+//! | [`StoreUpdate::Insert`] | 1 + value length | overwritten entry | 0                  |
+//! | [`StoreUpdate::Remove`] | 0                | deleted entry     | see below\*        |
+//! | [`Store::transaction`]  | 0 + updates      | 0 + updates       | 1                  |
+//! | [`Store::clear`]        | 0                | deleted entries   | 0                  |
+//! | [`Store::prepare`]      | 0                | 0                 | 0                  |
+//!
+//! \*0 if the update is alone in the transaction, otherwise 1.
+//!
+//! The _total lifetime_ of the store is below L = ((E + 1) × N - 1) × (P - 2) and above L - M
+//! words, where E is the maximum number of erase cycles. The lifetime is used when capacity is
+//! used, including transiently, as well as when compaction occurs. Compaction frequency and
+//! lifetime consumption are positively correlated to the store load factor (the ratio of used
+//! capacity to total capacity).
+//!
+//! It is possible to approximate the cost of transient words in terms of capacity: L transient
+//! words are equivalent to C - x words of capacity where x is the average capacity (including
+//! transient) of operations.
 //!
 //! ## Preconditions
 //!
 //! The following assumptions need to hold, or the store may behave in unexpected ways:
-//! -   A word can be written twice between erase cycles.
-//! -   A page can be erased `E` times after the first boot of the store.
-//! -   When power is lost while writing a slice or erasing a page, the next read
-//!     returns a slice where a subset (possibly none or all) of the bits that
-//!     should have been modified have been modified.
-//! -   Reading a slice is deterministic. When power is lost while writing a slice
-//!     or erasing a slice (erasing a page containing that slice), reading that
-//!     slice repeatedly returns the same result (until it is overwritten or its
-//!     page is erased).
-//! -   To decide whether a page has been erased, it is enough to test if all its
-//!     bits are equal to 1.
-//! -   When power is lost while writing a slice or erasing a page, that operation
-//!     does not count towards the limits. However, completing that write or erase
-//!     operation would count towards the limits, as if the number of writes per
-//!     word and number of erase cycles could be fractional.
-//! -   The storage is only modified by the store. Note that completely erasing the
-//!     storage is supported, essentially losing all content and lifetime tracking.
-//!     It is preferred to use `Clear` with a threshold of 0 to keep the lifetime
-//!     tracking.
+//! -   A word can be written [twice](Storage::max_word_writes) between erase cycles.
+//! -   A page can be erased [E](Storage::max_page_erases) times after the first boot of the store.
+//! -   When power is lost while writing a slice or erasing a page, the next read returns a slice
+//!     where a subset (possibly none or all) of the bits that should have been modified have been
+//!     modified.
+//! -   Reading a slice is deterministic. When power is lost while writing a slice or erasing a
+//!     slice (erasing a page containing that slice), reading that slice repeatedly returns the same
+//!     result (until it is overwritten or its page is erased).
+//! -   To decide whether a page has been erased, it is enough to test if all its bits are equal
+//!     to 1.
+//! -   When power is lost while writing a slice or erasing a page, that operation does not count
+//!     towards the limits. However, completing that write or erase operation would count towards
+//!     the limits, as if the number of writes per word and number of erase cycles could be
+//!     fractional.
+//! -   The storage is only modified by the store. Note that completely erasing the storage is
+//!     supported, essentially losing all content and lifetime tracking. It is preferred to use
+//!     [`Store::clear`] with a threshold of 0 to keep the lifetime tracking.
 //!
-//! The store properties may still hold outside some of those assumptions, but with
-//! an increasing chance of failure.
+//! The store properties may still hold outside some of those assumptions, but with an increasing
+//! chance of failure.
 //!
 //! # Implementation
 //!
 //! We define the following constants:
-//! -   `E < 65536` the number of times a page can be erased.
-//! -   `3 <= N < 64` the number of pages in the storage.
-//! -   `8 <= P <= 1024` the number of words in a page.
-//! -   `Q = P - 2` the number of words in a virtual page.
-//! -   `K = 4096` the maximum number of keys.
-//! -   `M = min(Q - 1, 256)` the maximum length in words of a value.
-//! -   `V = (N - 1) * (Q - 1) - M` the virtual capacity.
-//! -   `C = V - N` the user capacity.
+//! -   [E](format::Format::max_page_erases) ≤ [65535](format::MAX_ERASE_CYCLE) the number of times
+//!     a page can be erased.
+//! -   3 ≤ [N](format::Format::num_pages) < 64 the number of pages in the storage.
+//! -   8 ≤ P ≤ 1024 the number of words in a page.
+//! -   [Q](format::Format::virt_page_size) = P - 2 the number of words in a virtual page.
+//! -   [M](format::Format::max_prefix_len) = min(Q - 1, 256) the maximum length in words of a
+//!     value.
+//! -   [V](format::Format::virt_size) = (N - 1) × (Q - 1) - M the virtual capacity.
+//! -   [C](format::Format::total_capacity) = V - N the user capacity.
 //!
-//! We build a virtual storage from the physical storage using the first 2 words of
-//! each page:
+//! We build a virtual storage from the physical storage using the first 2 words of each page:
 //! -   The first word contains the number of times the page has been erased.
-//! -   The second word contains the starting word to which this page is being moved
-//!     during compaction.
+//! -   The second word contains the starting word to which this page is being moved during
+//!     compaction.
 //!
-//! The virtual storage has a length of `(E + 1) * N * Q` words and represents the
-//! lifetime of the store. (We reserve the last `Q + M` words to support adding
-//! emergency lifetime.) This virtual storage has a linear address space.
+//! The virtual storage has a length of (E + 1) × N × Q words and represents the lifetime of the
+//! store. (We reserve the last Q + M words to support adding emergency lifetime.) This virtual
+//! storage has a linear address space.
 //!
-//! We define a set of overlapping windows of `N * Q` words at each `Q`-aligned
-//! boundary. We call `i` the window spanning from `i * Q` to `(i + N) * Q`. Only
-//! those windows actually exist in the underlying storage. We use compaction to
-//! shift the current window from `i` to `i + 1`, preserving the content of the
-//! store.
+//! We define a set of overlapping windows of N × Q words at each Q-aligned boundary. We call i the
+//! window spanning from i × Q to (i + N) × Q. Only those windows actually exist in the underlying
+//! storage. We use compaction to shift the current window from i to i + 1, preserving the content
+//! of the store.
 //!
-//! For a given state of the virtual storage, we define `h_i` as the position of the
-//! first entry of the window `i`. We call it the head of the window `i`. Because
-//! entries are at most `M + 1` words, they can overlap on the next page only by `M`
-//! words. So we have `i * Q <= h_i <= i * Q + M` . Since there are no entries
-//! before the first page, we have `h_0 = 0`.
+//! For a given state of the virtual storage, we define h\_i as the position of the first entry of
+//! the window i. We call it the head of the window i. Because entries are at most M + 1 words, they
+//! can overlap on the next page only by M words. So we have i × Q ≤ h_i ≤ i × Q + M . Since there
+//! are no entries before the first page, we have h\_0 = 0.
 //!
-//! We define `t_i` as one past the last entry of the window `i`. If there are no
-//! entries in that window, we have `t_i = h_i`. We call `t_i` the tail of the
-//! window `i`. We define the compaction invariant as `t_i - h_i <= V`.
+//! We define t\_i as one past the last entry of the window i. If there are no entries in that
+//! window, we have t\_i = h\_i. We call t\_i the tail of the window i. We define the compaction
+//! invariant as t\_i - h\_i ≤ V.
 //!
-//! We define `|x|` as the capacity used before position `x`. We have `|x| <= x`. We
-//! define the capacity invariant as `|t_i| - |h_i| <= C`.
+//! We define |x| as the capacity used before position x. We have |x| ≤ x. We define the capacity
+//! invariant as |t\_i| - |h\_i| ≤ C.
 //!
-//! Using this virtual storage, entries are appended to the tail as long as there is
-//! both virtual capacity to preserve the compaction invariant and capacity to
-//! preserve the capacity invariant. When virtual capacity runs out, the first page
-//! of the window is compacted and the window is shifted.
+//! Using this virtual storage, entries are appended to the tail as long as there is both virtual
+//! capacity to preserve the compaction invariant and capacity to preserve the capacity invariant.
+//! When virtual capacity runs out, the first page of the window is compacted and the window is
+//! shifted.
 //!
-//! Entries are identified by a prefix of bits. The prefix has to contain at least
-//! one bit set to zero to differentiate from the tail. Entries can be one of:
-//! -   Padding: A word whose first bit is set to zero. The rest is arbitrary. This
-//!     entry is used to mark words partially written after an interrupted operation
-//!     as padding such that they are ignored by future operations.
-//! -   Header: A word whose second bit is set to zero. It contains the following fields:
-//!     -   A bit indicating whether the entry is deleted.
-//!     -   A bit indicating whether the value is word-aligned and has all bits set
-//!         to 1 in its last word. The last word of an entry is used to detect that
-//!         an entry has been fully written. As such it must contain at least one
-//!         bit equal to zero.
-//!     -   The key of the entry.
-//!     -   The length in bytes of the value. The value follows the header. The
-//!         entry is word-aligned if the value is not.
-//!     -   The checksum of the first and last word of the entry.
-//! -   Erase: A word used during compaction. It contains the page to be erased and
-//!     a checksum.
-//! -   Clear: A word used during the `Clear` operation. It contains the threshold
-//!     and a checksum.
-//! -   Marker: A word used during the `Transaction` operation. It contains the
-//!     number of updates following the marker and a checksum.
-//! -   Remove: A word used during the `Transaction` operation. It contains the key
-//!     of the entry to be removed and a checksum.
+//! Entries are identified by a prefix of bits. The prefix has to contain at least one bit set to
+//! zero to differentiate from the tail. Entries can be one of:
+//! -   [Padding](format::ID_PADDING): A word whose first bit is set to zero. The rest is arbitrary.
+//!     This entry is used to mark words partially written after an interrupted operation as padding
+//!     such that they are ignored by future operations.
+//! -   [Header](format::ID_HEADER): A word whose second bit is set to zero. It contains the
+//!     following fields:
+//!     -   A [bit](format::HEADER_DELETED) indicating whether the entry is deleted.
+//!     -   A [bit](format::HEADER_FLIPPED) indicating whether the value is word-aligned and has all
+//!         bits set to 1 in its last word. The last word of an entry is used to detect that an
+//!         entry has been fully written. As such it must contain at least one bit equal to zero.
+//!     -   The [key](format::HEADER_KEY) of the entry.
+//!     -   The [length](format::HEADER_LENGTH) in bytes of the value. The value follows the header.
+//!         The entry is word-aligned if the value is not.
+//!     -   The [checksum](format::HEADER_CHECKSUM) of the first and last word of the entry.
+//! -   [Erase](format::ID_ERASE): A word used during compaction. It contains the
+//!     [page](format::ERASE_PAGE) to be erased and a [checksum](format::WORD_CHECKSUM).
+//! -   [Clear](format::ID_CLEAR): A word used during the clear operation. It contains the
+//!     [threshold](format::CLEAR_MIN_KEY) and a [checksum](format::WORD_CHECKSUM).
+//! -   [Marker](format::ID_MARKER): A word used during a transaction. It contains the [number of
+//!     updates](format::MARKER_COUNT) following the marker and a [checksum](format::WORD_CHECKSUM).
+//! -   [Remove](format::ID_REMOVE): A word used inside a transaction. It contains the
+//!     [key](format::REMOVE_KEY) of the entry to be removed and a
+//!     [checksum](format::WORD_CHECKSUM).
 //!
 //! Checksums are the number of bits equal to 0.
 //!
@@ -204,107 +204,105 @@
 //!
 //! ## Compaction
 //!
-//! It should always be possible to fully compact the store, after what the
-//! remaining capacity should be available in the current window (restoring the
-//! compaction invariant). We consider all notations on the virtual storage after
-//! the full compaction. We will use the `|x|` notation although we update the state
-//! of the virtual storage. This is fine because compaction doesn't change the
-//! status of an existing word.
+//! It should always be possible to fully compact the store, after what the remaining capacity
+//! should be available in the current window (restoring the compaction invariant). We consider all
+//! notations on the virtual storage after the full compaction. We will use the |x| notation
+//! although we update the state of the virtual storage. This is fine because compaction doesn't
+//! change the status of an existing word.
 //!
-//! We want to show that the next `N - 1` compactions won't move the tail past the
-//! last page of their window, with `I` the initial window:
+//! We want to show that the next N - 1 compactions won't move the tail past the last page of their
+//! window, with I the initial window:
 //!
-//! ```text
-//! forall 1 <= i <= N - 1, t_{I + i} <= (I + i + N - 1) * Q
-//! ```
+//! |                  |            |   |                     |
+//! | ----------------:| ----------:|:-:|:------------------- |
+//! | ∀(1 ≤ i ≤ N - 1) | t\_{I + i} | ≤ | (I + i + N - 1) × Q |
 //!
-//! We assume `i` between `1` and `N - 1`.
+//! We assume i between 1 and N - 1.
 //!
-//! One step of compaction advances the tail by how many words were used in the
-//! first page of the window with the last entry possibly overlapping on the next
-//! page.
+//! One step of compaction advances the tail by how many words were used in the first page of the
+//! window with the last entry possibly overlapping on the next page.
 //!
-//! ```text
-//! forall j, t_{j + 1} = t_j + |h_{j + 1}| - |h_j| + 1
-//! ```
+//! |    |            |   |                                      |
+//! | --:| ----------:|:-:|:------------------------------------ |
+//! | ∀j | t\_{j + 1} | = | t\_j + \|h\_{j + 1}\| - \|h\_j\| + 1 |
 //!
 //! By induction, we have:
 //!
-//! ```text
-//! t_{I + i} <= t_I + |h_{I + i}| - |h_I| + i
-//! ```
+//! |            |   |                                      |
+//! | ----------:|:-:|:------------------------------------ |
+//! | t\_{I + i} | ≤ | t\_I + \|h\_{I + i}\| - \|h\_I\| + i |
 //!
 //! We have the following properties:
 //!
-//! ```text
-//! t_I <= h_I + V
-//! |h_{I + i}| - |h_I| <= h_{I + i} - h_I
-//! h_{I + i} <= (I + i) * Q + M
-//! ```
+//! |                           |   |                   |
+//! | -------------------------:|:-:|:----------------- |
+//! | t\_I                      | ≤ | h\_I + V          |
+//! | \|h\_{I + i}\| - \|h\_I\| | ≤ | h\_{I + i} - h\_I |
+//! | h\_{I + i}                | ≤ | (I + i) × Q + M   |
 //!
 //! Replacing into our previous equality, we can conclude:
 //!
-//! ```text
-//! t_{I + i}  = t_I + |h_{I + i}| - |h_I| + i
-//!           <= h_I + V + (I + i) * Q + M - h_I + i
-//!            = (N - 1) * (Q - 1) - M + (I + i) * Q + M + i
-//!            = (N - 1) * (Q - 1) + (I + i) * Q + i
-//!            = (I + i + N - 1) * Q + i - (N - 1)
-//!           <= (I + i + N - 1) * Q
-//! ```
+//! |            |   |                                             |
+//! | ----------:|:-:| ------------------------------------------- |
+//! | t\_{I + i} | = | t_I + \|h_{I + i}\| - \|h_I\| + i           |
+//! |            | ≤ | h\_I + V + (I + i) * Q + M - h\_I + i       |
+//! |            | = | (N - 1) × (Q - 1) - M + (I + i) × Q + M + i |
+//! |            | = | (N - 1) × (Q - 1) + (I + i) × Q + i         |
+//! |            | = | (I + i + N - 1) × Q + i - (N - 1)           |
+//! |            | ≤ | (I + i + N - 1) × Q                         |
 //!
-//! We also want to show that after `N - 1` compactions, the remaining capacity is
-//! available without compaction.
+//! We also want to show that after N - 1 compactions, the remaining capacity is available without
+//! compaction.
 //!
-//! ```text
-//! V - (t_{I + N - 1} - h_{I + N - 1}) >=    // The available words in the window.
-//!   C - (|t_{I + N - 1}| - |h_{I + N - 1}|) // The remaining capacity.
-//!   + 1                                     // Reserved for Clear.
-//! ```
+//! |   |                                               |                                   |
+//! | -:| --------------------------------------------- | --------------------------------- |
+//! |   | V - (t\_{I + N - 1} - h\_{I + N - 1})         | The available words in the window |
+//! | ≥ | C - (\|t\_{I + N - 1}\| - \|h\_{I + N - 1}\|) | The remaining capacity            |
+//! | + | 1                                             | Reserved for clear                |
 //!
-//! We can replace the definition of `C` and simplify:
+//! We can replace the definition of C and simplify:
 //!
-//! ```text
-//! V - (t_{I + N - 1} - h_{I + N - 1}) >= V - N - (|t_{I + N - 1}| - |h_{I + N - 1}|) + 1
-//! iff t_{I + N - 1} - h_{I + N - 1} <= |t_{I + N - 1}| - |h_{I + N - 1}| + N - 1
-//! ```
+//! |     |                                       |   |                                                       |
+//! | ---:| -------------------------------------:|:-:|:----------------------------------------------------- |
+//! |     | V - (t\_{I + N - 1} - h\_{I + N - 1}) | ≥ | V - N - (\|t\_{I + N - 1}\| - \|h\_{I + N - 1}\|) + 1 |
+//! | iff | t\_{I + N - 1} - h\_{I + N - 1}       | ≤ | \|t\_{I + N - 1}\| - \|h\_{I + N - 1}\| + N - 1       |
 //!
 //! We have the following properties:
 //!
-//! ```text
-//! t_{I + N - 1} = t_I + |h_{I + N - 1}| - |h_I| + N - 1
-//! |t_{I + N - 1}| - |h_{I + N - 1}| = |t_I| - |h_I| // Compaction preserves capacity.
-//! |h_{I + N - 1}| - |t_I| <= h_{I + N - 1} - t_I
-//! ```
+//!
+//! |                                         |   |                                              |        |
+//! | ---------------------------------------:|:-:|:-------------------------------------------- |:------ |
+//! | t\_{I + N - 1}                          | = | t\_I + \|h\_{I + N - 1}\| - \|h\_I\| + N - 1 |        |
+//! | \|t\_{I + N - 1}\| - \|h\_{I + N - 1}\| | = | \|t\_I\| - \|h\_I\|   | Compaction preserves capacity |
+//! | \|h\_{I + N - 1}\| - \|t\_I\|           | ≤ | h\_{I + N - 1} - t\_I |                               |
 //!
 //! From which we conclude:
 //!
-//! ```text
-//! t_{I + N - 1} - h_{I + N - 1} <= |t_{I + N - 1}| - |h_{I + N - 1}| + N - 1
-//! iff t_I + |h_{I + N - 1}| - |h_I| + N - 1 - h_{I + N - 1} <= |t_I| - |h_I| + N - 1
-//! iff t_I + |h_{I + N - 1}| - h_{I + N - 1} <= |t_I|
-//! iff |h_{I + N - 1}| - |t_I| <= h_{I + N - 1} - t_I
-//! ```
+//! |     |                                 |   |                                                 |
+//! | ---:| -------------------------------:|:-:|:----------------------------------------------- |
+//! |     | t\_{I + N - 1} - h\_{I + N - 1} | ≤ | \|t\_{I + N - 1}\| - \|h\_{I + N - 1}\| + N - 1 |
+//! | iff | t\_I + \|h\_{I + N - 1}\| - \|h\_I\| + N - 1 - h\_{I + N - 1} | ≤ | \|t\_I\| - \|h\_I\| + N - 1 |
+//! | iff | t\_I + \|h\_{I + N - 1}\| - h\_{I + N - 1}                    | ≤ | \|t\_I\| |
+//! | iff | \|h\_{I + N - 1}\| - \|t\_I\|                                 | ≤ | h\_{I + N - 1} - t\_I |
 //!
 //!
 //! ## Checksum
 //!
-//! The main property we want is that all partially written/erased words are either
-//! the initial word, the final word, or invalid.
+//! The main property we want is that all partially written/erased words are either the initial
+//! word, the final word, or invalid.
 //!
-//! We say that a bit sequence `TARGET` is reachable from a bit sequence `SOURCE` if
-//! both have the same length and `SOURCE & TARGET == TARGET` where `&` is the
-//! bitwise AND operation on bit sequences of that length. In other words, when
-//! `SOURCE` has a bit equal to 0 then `TARGET` also has that bit equal to 0.
+//! We say that a bit sequence `TARGET` is reachable from a bit sequence `SOURCE` if both have the
+//! same length and `SOURCE & TARGET == TARGET` where `&` is the bitwise AND operation on bit
+//! sequences of that length. In other words, when `SOURCE` has a bit equal to 0 then `TARGET` also
+//! has that bit equal to 0.
 //!
-//! The only written entries start with `101` or `110` and are written from an
-//! erased word. Marking an entry as padding or deleted is a single bit operation,
-//! so the property trivially holds. For those cases, the proof relies on the fact
-//! that there is exactly one bit equal to 0 in the 3 first bits. Either the 3 first
-//! bits are still `111` in which case we expect the remaining bits to be equal
-//! to 1. Otherwise we can use the checksum of the given type of entry because those
-//! 2 types of entries are not reachable from each other. Here is a visualization of
-//! the partitioning based on the first 3 bits:
+//! The only written entries start with `101` or `110` and are written from an erased word. Marking
+//! an entry as padding or deleted is a single bit operation, so the property trivially holds. For
+//! those cases, the proof relies on the fact that there is exactly one bit equal to 0 in the 3
+//! first bits. Either the 3 first bits are still `111` in which case we expect the remaining bits
+//! to be equal to 1. Otherwise we can use the checksum of the given type of entry because those 2
+//! types of entries are not reachable from each other. Here is a visualization of the partitioning
+//! based on the first 3 bits:
 //!
 //! | First 3 bits | Description        | How to check                 |
 //! | ------------:| ------------------ | ---------------------------- |
@@ -314,34 +312,27 @@
 //! | `100`        | Deleted user entry | No check, atomically written |
 //! | `0??`        | Padding entry      | No check, atomically written |
 //!
-//! To show that valid entries of a given type are not reachable from each other, we
-//! show 3 lemmas:
+//! To show that valid entries of a given type are not reachable from each other, we show 3 lemmas:
 //!
-//! 1.  A bit sequence is not reachable from another if its number of bits equal to
-//!     0 is smaller.
+//! 1.  A bit sequence is not reachable from another if its number of bits equal to 0 is smaller.
+//! 2.  A bit sequence is not reachable from another if they have the same number of bits equals to
+//!     0 and are different.
+//! 3.  A bit sequence is not reachable from another if it is bigger when they are interpreted as
+//!     numbers in binary representation.
 //!
-//! 2.  A bit sequence is not reachable from another if they have the same number of
-//!     bits equals to 0 and are different.
-//!
-//! 3.  A bit sequence is not reachable from another if it is bigger when they are
-//!     interpreted as numbers in binary representation.
-//!
-//! From those lemmas we consider the 2 cases. If both entries have the same number
-//! of bits equal to 0, they are either equal or not reachable from each other
-//! because of the second lemma. If they don't have the same number of bits equal to
-//! 0, then the one with less bits equal to 0 is not reachable from the other
-//! because of the first lemma and the one with more bits equal to 0 is not
-//! reachable from the other because of the third lemma and the definition of the
-//! checksum.
+//! From those lemmas we consider the 2 cases. If both entries have the same number of bits equal to
+//! 0, they are either equal or not reachable from each other because of the second lemma. If they
+//! don't have the same number of bits equal to 0, then the one with less bits equal to 0 is not
+//! reachable from the other because of the first lemma and the one with more bits equal to 0 is not
+//! reachable from the other because of the third lemma and the definition of the checksum.
 //!
 //! # Fuzzing
 //!
-//! For any sequence of operations and interruptions starting from an erased
-//! storage, the store is checked against its model and some internal invariant at
-//! each step.
+//! For any sequence of operations and interruptions starting from an erased storage, the store is
+//! checked against its model and some internal invariant at each step.
 //!
-//! For any sequence of operations and interruptions starting from an arbitrary
-//! storage, the store is checked not to crash.
+//! For any sequence of operations and interruptions starting from an arbitrary storage, the store
+//! is checked not to crash.
 
 #![cfg_attr(not(feature = "std"), no_std)]
 #![feature(try_trait)]
diff --git a/libraries/persistent_store/src/model.rs b/libraries/persistent_store/src/model.rs
index eebc329..e0bf9e3 100644
--- a/libraries/persistent_store/src/model.rs
+++ b/libraries/persistent_store/src/model.rs
@@ -12,13 +12,16 @@
 // See the License for the specific language governing permissions and
 // limitations under the License.
 
+//! Store specification.
+
 use crate::format::Format;
 use crate::{usize_to_nat, StoreError, StoreRatio, StoreResult, StoreUpdate};
 use std::collections::HashMap;
 
 /// Models the mutable operations of a store.
 ///
-/// The model doesn't model the storage and read-only operations. This is done by the driver.
+/// The model doesn't model the storage and read-only operations. This is done by the
+/// [driver](crate::StoreDriver).
 #[derive(Clone, Debug)]
 pub struct StoreModel {
     /// Represents the content of the store.
diff --git a/libraries/persistent_store/src/storage.rs b/libraries/persistent_store/src/storage.rs
index becd900..fb5b0cb 100644
--- a/libraries/persistent_store/src/storage.rs
+++ b/libraries/persistent_store/src/storage.rs
@@ -12,6 +12,8 @@
 // See the License for the specific language governing permissions and
 // limitations under the License.
 
+//! Flash storage abstraction.
+
 /// Represents a byte position in a storage.
 #[derive(Copy, Clone, Debug, PartialEq, Eq)]
 pub struct StorageIndex {
@@ -65,12 +67,14 @@ pub trait Storage {
     /// The following pre-conditions must hold:
     /// - The `index` must designate `value.len()` bytes in the storage.
     /// - Both `index` and `value.len()` must be word-aligned.
-    /// - The written words should not have been written too many times since last page erasure.
+    /// - The written words should not have been written [too many](Self::max_word_writes) times
+    ///   since the last page erasure.
     fn write_slice(&mut self, index: StorageIndex, value: &[u8]) -> StorageResult<()>;
 
     /// Erases a page of the storage.
     ///
-    /// The `page` must be in the storage.
+    /// The `page` must be in the storage, i.e. less than [`Storage::num_pages`]. And the page
+    /// should not have been erased [too many](Self::max_page_erases) times.
     fn erase_page(&mut self, page: usize) -> StorageResult<()>;
 }
 
diff --git a/libraries/persistent_store/src/store.rs b/libraries/persistent_store/src/store.rs
index f19f463..c143c89 100644
--- a/libraries/persistent_store/src/store.rs
+++ b/libraries/persistent_store/src/store.rs
@@ -12,6 +12,8 @@
 // See the License for the specific language governing permissions and
 // limitations under the License.
 
+//! Store implementation.
+
 use crate::format::{
     is_erased, CompactInfo, Format, Header, InitInfo, InternalEntry, Padding, ParsedWord, Position,
     Word, WordState,
@@ -55,17 +57,14 @@ pub enum StoreError {
     ///
     /// The consequences depend on the storage failure. In particular, the operation may or may not
     /// have succeeded, and the storage may have become invalid. Before doing any other operation,
-    /// the store should be [recovered]. The operation may then be retried if idempotent.
-    ///
-    /// [recovered]: struct.Store.html#method.recover
+    /// the store should be [recovered](Store::recover). The operation may then be retried if
+    /// idempotent.
     StorageError,
 
     /// Storage is invalid.
     ///
-    /// The storage should be erased and the store [recovered]. The store would be empty and have
-    /// lost track of lifetime.
-    ///
-    /// [recovered]: struct.Store.html#method.recover
+    /// The storage should be erased and the store [recovered](Store::recover). The store would be
+    /// empty and have lost track of lifetime.
     InvalidStorage,
 }
 
@@ -92,14 +91,12 @@ pub type StoreResult<T> = Result<T, StoreError>;
 
 /// Progression ratio for store metrics.
 ///
-/// This is used for the [capacity] and [lifetime] metrics. Those metrics are measured in words.
+/// This is used for the [`Store::capacity`] and [`Store::lifetime`] metrics. Those metrics are
+/// measured in words.
 ///
 /// # Invariant
 ///
-/// - The used value does not exceed the total: `used <= total`.
-///
-/// [capacity]: struct.Store.html#method.capacity
-/// [lifetime]: struct.Store.html#method.lifetime
+/// - The used value does not exceed the total: `used` ≤ `total`.
 #[derive(Copy, Clone, Debug, PartialEq, Eq)]
 pub struct StoreRatio {
     /// How much of the metric is used.
@@ -148,11 +145,11 @@ impl StoreHandle {
         self.key as usize
     }
 
-    /// Returns the length of value of the entry.
+    /// Returns the value length of the entry.
     ///
     /// # Errors
     ///
-    /// Returns `InvalidArgument` if the entry has been deleted or compacted.
+    /// Returns [`StoreError::InvalidArgument`] if the entry has been deleted or compacted.
     pub fn get_length<S: Storage>(&self, store: &Store<S>) -> StoreResult<usize> {
         store.get_length(self)
     }
@@ -161,7 +158,7 @@ impl StoreHandle {
     ///
     /// # Errors
     ///
-    /// Returns `InvalidArgument` if the entry has been deleted or compacted.
+    /// Returns [`StoreError::InvalidArgument`] if the entry has been deleted or compacted.
     pub fn get_value<S: Storage>(&self, store: &Store<S>) -> StoreResult<Vec<u8>> {
         store.get_value(self)
     }
@@ -211,7 +208,7 @@ pub struct Store<S: Storage> {
 
     /// The list of the position of the user entries.
     ///
-    /// The position is encoded as the word offset from the [head](Store#structfield.head).
+    /// The position is encoded as the word offset from the [head](Store::head).
     entries: Option<Vec<u16>>,
 }
 
@@ -224,7 +221,8 @@ impl<S: Storage> Store<S> {
     ///
     /// # Errors
     ///
-    /// Returns `InvalidArgument` if the storage is not supported.
+    /// Returns [`StoreError::InvalidArgument`] if the storage is not
+    /// [supported](Format::is_storage_supported).
     pub fn new(storage: S) -> Result<Store<S>, (StoreError, S)> {
         let format = match Format::new(&storage) {
             None => return Err((StoreError::InvalidArgument, storage)),
@@ -258,7 +256,7 @@ impl<S: Storage> Store<S> {
         )))
     }
 
-    /// Returns the current capacity in words.
+    /// Returns the current and total capacity in words.
     ///
     /// The capacity represents the size of what is stored.
     pub fn capacity(&self) -> StoreResult<StoreRatio> {
@@ -271,7 +269,7 @@ impl<S: Storage> Store<S> {
         Ok(StoreRatio { used, total })
     }
 
-    /// Returns the current lifetime in words.
+    /// Returns the current and total lifetime in words.
     ///
     /// The lifetime represents the age of the storage. The limit is an over-approximation by at
     /// most the maximum length of a value (the actual limit depends on the length of the prefix of
@@ -286,10 +284,11 @@ impl<S: Storage> Store<S> {
     ///
     /// # Errors
     ///
-    /// Returns `InvalidArgument` in the following circumstances:
-    /// - There are too many updates.
+    /// Returns [`StoreError::InvalidArgument`] in the following circumstances:
+    /// - There are [too many](Format::max_updates) updates.
     /// - The updates overlap, i.e. their keys are not disjoint.
-    /// - The updates are invalid, e.g. key out of bound or value too long.
+    /// - The updates are invalid, e.g. key [out of bound](Format::max_key) or value [too
+    ///   long](Format::max_value_len).
     pub fn transaction<ByteSlice: Borrow<[u8]>>(
         &mut self,
         updates: &[StoreUpdate<ByteSlice>],