Update the soundness section to the landed enforcement

This commit is contained in:
Dennis Kobert
2026-09-06 16:57:31 +00:00
parent 5d967a6a17
commit 2e1d9c04f7
+19 -13
View File
@@ -750,19 +750,25 @@ cannot misalign an offset. Kernels see contexts only as an opaque
`impl Ctx + ...` they cannot construct, and lifetimes keep them from `impl Ctx + ...` they cannot construct, and lifetimes keep them from
stashing handles in node state. stashing handles in node state.
That is the property the design is for, and reaching it is work rather That is the property the design is for, and the enforcement now rests
than a consequence. Type identity is stamped on every layout field and on construction at the seams that used to be open. Type identity is
checked where layouts are built and where the safe builders write, which stamped on every layout field and on the element write, and both
is the enforcement this rests on. What is not yet closed, and is tracked participate in layout equality, so the union's shared-element assertion
as such: a producer whose layout was never installed writes through a and the identity-forwarding decision distinguish same-shape
path that assumes the inline width, an owned record replays against a different-type layouts. Retiring the inline register-return path in
caller-supplied layout it does not check, and the record stack's own favor of always-spill removed the one producer that wrote without an
bounds check is a debug assertion while its buffer can be reset under installed layout. Serving closes only through a frame claim's own
live records. Each is reachable from safe code, so the claim above holds methods, whose proof cannot be minted elsewhere, and assertion reads go
by the discipline of the generated code and not yet by construction. The through an owned capture at the node's declared layout rather than raw
direction is to replace the emitted raw operations with a small set of frame reads. Serving lifetimes make an arena-resident value
checked surfaces, so that the remaining unsafe is the erased glue and inexpressible beyond its evaluation in safe code, and an arena move is
the wiring-computed byte plans, where it is irreducible. keyed by the park's static type, so a mistyped or unkeyed reference
declines into the clone path instead of moving foreign bytes. What
remains unsafe is the irreducible core, the erased glue and the
wiring-computed byte plans, plus a small tracked set of open seams of
which the hoist mask's positional contract is the last
soundness-relevant survivor; an adversarial audit round over every
safety contract is scheduled before this lands upstream.
# Drawbacks # Drawbacks