docs: state the per-page temporal replay boundary in its true form (#142)

THEORY.md

@@ -161,7 +161,17 @@ There is one **critical, revised** sub-decision that is easy to get wrong and wo
 
 **Why.** Envelope encryption makes credential rotation O(1) — you re-wrap the DEK — instead of O(database size). The per-slot KDF choice matches input entropy: HKDF is fast and correct for high-entropy keys, while Argon2id is memory-hard to resist brute-forcing low-entropy passphrases (its params are recorded per slot). And every rotation op is an ordinary superblock A/B + fsync commit, so it reuses the existing crash-safe protocol wholesale: a metadata-only `rewrite_crypto_header` commit persists a rotated slot table atomically (write the inactive slot, fsync, promote), so a crash mid-rotation leaves the old table intact.
 
-Two threat-model boundaries are documented rather than solved, and you should know them before you rely on this: there is **no rollback/replay resistance** (an attacker who substitutes a wholly older, validly-signed image is undetectable without an external trust anchor like a TPM), and the DEK sits in plaintext in process memory during a session (mitigated by zeroize-on-drop, not by encryption). See spec `2026-06-29` §3/§5/§9. Note that `rekey` (ADR 0018) does bear on the first boundary: it invalidates every page image sealed under the old DEK, so it ends an attacker's ability to splice in stale pages captured beforehand — it does not, however, make the engine detect such splicing, which remains open as [issue #142](https://github.com/pgexperts/chisel/issues/142).
+Two threat-model boundaries are documented rather than solved, and you should know them before you rely on this.
+
+**No replay resistance, at either granularity.** The coarse form is the familiar one: an attacker who substitutes a wholly older, validly-signed image is undetectable without an external trust anchor like a TPM. The finer form is sharper and was understated for a long time — page AAD is `page_id` and nothing else, so a sealed page authenticates *where* it belongs but not *when*. An attacker holding an old copy of the file can splice **individual** stale pages into the current one; each passes AEAD verification at the correct page id under the current DEK. What comes out is a mixed state that never existed at any commit — a stale freemap or tree page beside current siblings — which the engine may walk as though it were consistent, corrupting structure rather than raising `DecryptionFailed`. That is the worse failure mode of the two.
+
+The positional page-type checks (I148) are a partial and accidental mitigation worth knowing about: every radix descent now verifies that a page's type matches its position in the tree, so a splice is caught whenever the attacker's stale copy carries a different `PageType` than the one currently expected at that page id. It is silent only when the type happens to match — realistic for hot structural nodes that are repeatedly COW'd in place, but far from universal.
+
+It is worth being precise about what the AEAD does buy, because "cryptographic tamper-detection" reads like more than it is: the guarantees are *spatial*, not *temporal*. Anti-relocation stops a page being moved to the wrong place. Nothing stops it being moved to the wrong time. Fixing that means binding pages to a notion of "now" the attacker cannot forge — a commit epoch in the AAD (which rewrites every reachable page on each bump — amplification well beyond what shadow paging already accepts), or hash-chaining page tags into the sealed superblock body (which makes every commit touch a whole-file structure). Neither is implemented; see [issue #142](https://github.com/pgexperts/chisel/issues/142).
+
+`rekey` (ADR 0018) bounds the exposure without closing it: it does not make splicing detectable, but it invalidates every page image sealed under the old DEK, so pages captured before a rotation cannot be spliced in after one. An operator who suspects file-level access has a way to draw a line.
+
+**The DEK is plaintext in process memory** during a session, mitigated by zeroize-on-drop rather than by encryption. See spec `2026-06-29` §3/§5/§9.
 
 ### Encryption page format: 8232-byte stride, logical page stays 8192, MAJOR 1→2 (ADR-15)
 

docs/adr/0015-on-disk-encryption-xchacha20-poly1305-envelope-keys.md

@@ -37,5 +37,36 @@ status: Accepted
 
 Spec: `docs/specs/2026-06-29-on-disk-encryption-design.md`. Plan: `docs/plans/2026-06-29-on-disk-encryption.md`. Implemented 2026-06-30 across 6 phases (crypto core → superblock/key-flow → page-I/O + cache + spillway → public API + Python → key rotation → docs/version). See ARCHITECTURE.md "On-disk encryption" and ISSUES.md I142 (deferred bulk DEK rotation). Public API is deliberately narrow: only `Key`, `Argon2Params`, and the encryption error variants are public; the crypto/superblock internals are `pub(crate)`.
 
----
+## Addendum (2026-08-04)
+
+Two statements in the record above have been overtaken, and are corrected here
+rather than in place — an Accepted record's body is superseded or annotated, not
+rewritten.
+
+**Bulk DEK rotation is no longer deferred.** The Alternatives-considered bullet
+and the closing paragraph describe full DEK rotation as deferred to `ISSUES.md`
+I142. It shipped as `Chisel::rekey` — see ADR
+[0018](0018-bulk-dek-rotation-via-copy-and-rename.md) for the design (offline,
+path-taking, copy-then-atomic-rename, collapses the key-slot table to the
+supplied credential). `ISSUES.md` itself was retired in favour of GitHub issues;
+I142 is now
+[issue #140](https://github.com/pgexperts/chisel/issues/140).
 
+**The replay boundary is stronger than this record states.** The Consequences
+bullet says there is "no rollback/replay protection (an attacker substituting a
+wholly older, validly-signed image is undetectable...)". That describes only the
+coarse case. Page AAD is `page_id` and nothing else, so a sealed page
+authenticates *where* it belongs but not *when*: an attacker holding an older
+copy can splice INDIVIDUAL stale pages into a current file, each verifying at
+the correct page id under the current DEK. The result is a mixed state that
+never existed at any commit.
+
+That is strictly stronger than "wholly older image", and it is not covered by
+the anti-relocation property — relocation is about the wrong *place*, replay
+about the wrong *time*. The boundary is stated properly in the design spec §9
+and THEORY.md, and tracked as
+[issue #142](https://github.com/pgexperts/chisel/issues/142). `rekey` bounds the
+exposure (it invalidates every image sealed under the old DEK) without making a
+splice detectable.
+
+---

docs/specs/2026-06-29-on-disk-encryption-design.md

@@ -25,11 +25,16 @@ In scope:
 
 Out of scope (documented as known boundaries, see §9):
 
-- Full **Data Encryption Key (DEK) rotation** / bulk re-encryption (deferred; a heavy
-  whole-file operation reserved for "the DEK itself is compromised").
-- **Rollback / replay** resistance against an attacker who can substitute a wholly
-  older, validly-signed database image (needs an external trust anchor; impossible for
-  a self-contained file).
+- **Rollback / replay** resistance. Originally written as "an attacker who can
+  substitute a wholly older, validly-signed database image"; §9 now states the
+  boundary in its true, stronger form, which also covers splicing individual stale
+  pages into a current file.
+
+Formerly out of scope, now implemented:
+
+- Full **Data Encryption Key (DEK) rotation** / bulk re-encryption. Shipped as
+  `Chisel::rekey` (ADR 0018) — still a heavy whole-file operation reserved for
+  "the DEK itself is compromised", but no longer absent.
 
 ---
 
@@ -291,11 +296,46 @@ Provided (under the AEAD model):
 
 Not provided (documented boundaries):
 
-- **Rollback / replay resistance**: an attacker with file access who substitutes a
-  wholly older, validly-signed database image (or an older valid A/B superblock slot)
-  cannot be detected by self-contained authentication. Defeating this requires an
-  external monotonic trust anchor (e.g., TPM), which is out of scope for a file-based
-  embedded store.
+- **Rollback / replay resistance**, at two granularities. The coarse one was always
+  documented: an attacker with file access who substitutes a wholly older,
+  validly-signed database image (or an older valid A/B superblock slot) cannot be
+  detected by self-contained authentication.
+
+  The finer one is **per-page temporal replay**, and it is strictly stronger — this
+  wording is the correction the original text needed. Page AAD is `page_id` and
+  nothing else (`PageCipher::seal`, `AAD = page_id.to_le_bytes()`), so a sealed page
+  authenticates *where* it belongs but not *when*. An attacker holding an old copy of
+  the file can therefore splice INDIVIDUAL stale pages into the current one: each
+  spliced page passes AEAD verification, at the correct page id, under the current
+  DEK. The result is a mixed state that never existed at any commit — a stale freemap
+  or interior tree page next to current siblings, which the engine then walks as
+  though it were consistent, potentially corrupting structure silently rather than
+  surfacing `DecryptionFailed`.
+
+  This is NOT covered by the "wholly older image" wording, and it is not covered by
+  the anti-relocation property above: relocation is about moving a page to the wrong
+  *place*, replay is about moving it to the wrong *time*. Both the "cryptographic
+  tamper-detection" and "anti-relocation" claims in the Provided list should be read
+  with this in mind — they are spatial guarantees, not temporal ones.
+
+  Defeating either granularity requires binding pages to a notion of *now* that the
+  attacker cannot forge. The options, none of which are implemented:
+
+  1. an external monotonic trust anchor (e.g. a TPM), which is out of scope for a
+     self-contained file-based embedded store;
+  2. a commit epoch in the page AAD, which makes every epoch bump rewrite every
+     reachable page. Note the framing: shadow paging already ACCEPTS write
+     amplification as the price of crash-safety-by-inspection (ADR 0001 lists it
+     as a negative consequence, and THEORY.md says the cost is taken with eyes
+     open). The objection here is not amplification as such, but amplification
+     well beyond what that trade already buys;
+  3. hash-chaining page tags into the sealed superblock body, which turns every
+     commit into an update of a structure covering the whole file.
+
+  What DOES bound the exposure in practice is `Chisel::rekey` (ADR 0018). It does not
+  make splicing *detectable*, but it invalidates every page image sealed under the
+  old DEK, so pages captured before a rotation can no longer be spliced into the file
+  after one. An operator who suspects file-level access has a way to draw a line.
 - **In-memory protection**: the page cache and the DEK are plaintext in process memory
   during an open session (mitigated by zeroize-on-drop, not by encryption).
 - **Traffic-analysis / size**: file size, page count, and access patterns are not

src/crypto/mod.rs

@@ -364,6 +364,24 @@ impl PageCipher {
     /// blob: `ciphertext(8192) ‖ tag(16) ‖ nonce(24)`. AAD = page_id LE bytes
     /// (anti-relocation). A fresh random 192-bit nonce per call (spec §2.1) —
     /// safe under shadow-paging page reuse, and stored in the clear.
+    ///
+    /// The AAD is page_id and nothing else, and that is a documented boundary
+    /// rather than an oversight — but be precise about what it means, because
+    /// "anti-relocation" is easy to read as more than it is. A sealed page
+    /// authenticates WHERE it belongs, not WHEN. An attacker holding an older
+    /// copy of the file can splice INDIVIDUAL stale pages into the current one:
+    /// each verifies, at the right page id, under the current DEK. The engine
+    /// then may walk a mixed state that never existed at any commit — a stale
+    /// freemap or tree page beside current siblings — corrupting structure
+    /// instead of raising `DecryptionFailed`. The positional page-type checks
+    /// (I148) catch this whenever the stale page's type differs from the one
+    /// expected at that position, so it is silent only for a same-type splice.
+    ///
+    /// So the guarantee here is spatial, not temporal. Adding a commit epoch to
+    /// this AAD would close it, at the cost of rewriting every reachable page on
+    /// each epoch bump. See issue #142 and spec §9; `Chisel::rekey` bounds the
+    /// exposure by invalidating every image sealed under the old DEK, without
+    /// making the splice detectable.
     pub fn seal(&self, page_id: u64, plaintext: &[u8; 8192]) -> [u8; ENC_PAGE_SIZE] {
         let nonce = random_array::<NONCE_LEN>();
         let aad = page_id.to_le_bytes();