docs/vEP: record the r452 copy-out fingerprint rule (a change-detection fingerprint must not be an algebraic invariant of any plausible kernel operation - the 32-bit additive page checksum was blind to in-place power-of-two scales: 1024 words x 2^23 = 2^33 == 0 mod 2^32; FNV-1a 64 since r452) and the r453 rel_mod=1 default (guest release authored only on the post-copy-out completion edge)

1 files changed, 33 insertions, 0 deletions

diff --git a/docs/03-architecture/13-vexecution-plane.md b/docs/03-architecture/13-vexecution-plane.md
index caaad01..3d97d07 100644
--- a/docs/03-architecture/13-vexecution-plane.md
+++ b/docs/03-architecture/13-vexecution-plane.md
@@ -568,6 +568,39 @@ forwards (local evidence and the prepared harness:
 forwarding-service cost, not engine time — the number to drive down is the
 7.9 ms and the per-window round trips.
 
+### 3.5a Copy-out change detection: fingerprint rule
+
+A forwarded launch stages every referenced data page into the data-bounce
+chunk, and after the retire wait the copy-out ships back only the pages the
+engine actually modified. That decision used to be a 32-bit additive
+checksum of the page's words, compared against a baseline captured at
+copy-in. The additive form has a structural blind spot: doubling every word
+of a 4 KB page raises each float exponent by one (+2^23 per word), and 1024
+words contribute `1024 * 2^23 = 2^33`, which is exactly `0 (mod 2^32)` — an
+in-place power-of-two scale of a whole page (`c[i] *= 2.0f`) left the
+checksum bit-identical, the page was classified "engine did not touch",
+the write-back was skipped, and the client read the pre-scale values. The
+same blindness applies to `*= 0.5f`, `* 4`, `* 8`, etc. Since `r452`
+(commit `19399f4f`) every change decision in the copy path — the retire
+wait's settle scan, the tracked and gap copy-outs, the window witness, the
+late-store witness and the idempotent-launch fingerprint — uses a 64-bit
+FNV-1a hash over the page instead; the additive sum survives only as the
+all-zero filter. Policy rule for the plane: **a change-detection
+fingerprint must not be an algebraic invariant of any plausible kernel
+operation** — use a hash, never a sum.
+
+The reader side of the same decision is the landing table: a D2H copy of a
+device VA resolves through the last recorded write of that VA. Since `r453`
+the forwarded QMD's release0 is redirected to the module semaphore by
+default (`gsp_phys_rmcall_gr_rel_mod=1`): the guest-visible release word is
+authored by the host only on the completion edge, after the copy-out has
+shipped the engine's stores, so a client's stream-ordered readback can no
+longer run ahead of the write-back (the historical shape: the engine's own
+release satisfied the guest while the copy-out was still pending). The
+engine-completion observable remains the module semaphore, and the
+per-outcome authoring path guarantees the guest word is applied on every
+outcome (timeout, wedge, no-write).
+
 ### 3.6 Citation map for this section
 
 | Claim | Authority |