diff --git a/docs/density-chain/DENSITY-CHAIN.md b/docs/density-chain/DENSITY-CHAIN.md index 06a78af..11c1f39 100644 --- a/docs/density-chain/DENSITY-CHAIN.md +++ b/docs/density-chain/DENSITY-CHAIN.md @@ -859,9 +859,15 @@ the RLM execution model, the doubts machinery it borrows, or the pillar it reali it exists an S6 pass would be a claim about `KataREPL` and not about `KataLauncher`. Then GB — which inherits S5's residuals: the watchdog is unproven against a real shim wedge, and the seccomp/allowlist divergence is recorded rather than resolved — GA-eq, GA-rt. Proposed: - doubt-filter Layers 1–2. Open owner calls: `MAX_FRAME_LEN` (ships 2 MiB, unratified against - `CONFORMANCE §2.3`'s 16 MiB), handle lifetime, the warm pool, depth-2. The remaining **[A]** halves - (S6, GB, GA-eq) are ≤$5 and **unspent**; S3's and S4's are **banked**. + doubt-filter Layers 1–2. **`MAX_FRAME_LEN` RATIFIED 2026-07-24** — slice 2 MiB, frame 4 MiB, frame + derived from slice, invariant `frame ≥ 2 × slice` asserted in `test_config.py`. The ruling corrected + a *layer*, not a number: a context-window derivation had been applied to the frame bound, where it + protects nothing (a 12 MiB namespace value returns a ~4 KB reply — `MarshalCaps` holds attention, + independently) while leaving the frame **below** `max_result_bytes`, so a legal broker result could + not cross the wire. The token rule now sizes the **slice**, as a sizing convention and never an + enforcing bound. **The REPL is meant to be gigabytes read in slices; the corpus ceiling is + `RLIMIT_AS`, not any wire number.** Still open: handle lifetime, the warm pool, depth-2. The + remaining **[A]** halves (S6, GB, GA-eq) are ≤$5 and **unspent**; S3's and S4's are **banked**. *Status ledger:* **control plane shipped; a microVM boots, a frame crosses to it, a real database query crosses holding a handle, and Tier-0 caps the worker from inside — STILL not a sandbox and must diff --git a/docs/product/repl-sandbox/REPL_SANDBOX_CONFORMANCE.md b/docs/product/repl-sandbox/REPL_SANDBOX_CONFORMANCE.md index bfc8f9e..1387463 100644 --- a/docs/product/repl-sandbox/REPL_SANDBOX_CONFORMANCE.md +++ b/docs/product/repl-sandbox/REPL_SANDBOX_CONFORMANCE.md @@ -121,7 +121,51 @@ written**; host-side `REPLResult.locals` holds reprs only. Two consequences: `CodeBlock.to_dict()` (`core/types.py:204-205`) into the logger. Interposing costs no driver compatibility. -### 2.3 `MAX_FRAME_LEN` — evidence for the owner decision (NOT closed here) +### 2.3 `MAX_FRAME_LEN` — CLOSED 2026-07-24 by owner ruling; the evidence that produced it follows + +**Ruling: `max_result_bytes` = 2 MiB, `max_frame_len` = 4 MiB, and the frame bound is derived from +the slice bound rather than from the model's context window.** The invariant +`max_frame_len >= 2 * max_result_bytes` is asserted in `src/repl_sandbox/tests/test_config.py`. + +**What the ruling corrects.** A previous edition derived `MAX_FRAME_LEN` from the worker's context +window — half of `gpt-5.4`'s 1,050,000 tokens at ~4 bytes each, giving 2 MiB — on the theory that no +single frame should context-saturate the worker it lands in. That is the right rule applied at the +wrong layer, and it had two consequences: + +1. **It protected nothing.** A slice does not reach the model's attention by landing in the guest + namespace. `MarshalCaps` holds that property independently and an order of magnitude lower — + demonstrated: a **12 MiB** value in the namespace produces a **~4 KB** `exec` reply, because the + marshaller describes the value (4 KiB repr, spill handle) rather than carrying it. +2. **It broke a live path.** It left the frame cap (2 MiB) *below* `max_result_bytes` (8 MiB), so a + result the broker considered legal could not cross the wire at all. Both numbers were individually + plausible; only their relationship was wrong, and nothing compared them. + +**The layering the ruling installs.** Four bounds, four questions, each with its own home: + +| what is bounded | question it answers | constant | +|---|---|---| +| REPL namespace | how large a corpus may the model work over? | `Tier0Limits.address_space_bytes` (1 GiB) | +| one slice | how much moves host store → guest namespace per call? | `BrokerCaps.max_result_bytes` (2 MiB) | +| model attention | how much reaches the transcript? | `MarshalCaps` (20 KiB stdout, 64 KiB answer) | +| one wire message | how large may a single frame be? | `DEFAULT_MAX_FRAME_LEN` (4 MiB) | + +**The REPL is meant to be large — potentially gigabytes — and read in slices.** No bound in this +table constrains that; the ceiling on the corpus is address space. The token derivation survives as +the way `max_result_bytes` is *chosen* — "about what one model pass could consider" — and is recorded +as a **sizing convention, not an enforcing bound**, because treating it as enforcing is exactly the +error above. + +**The cost, stated:** a 2 MiB slice means a corpus arrives in ~500 round trips per GB. If bulk +transfer needs to be cheaper, `max_result_bytes` is the single lever and `max_frame_len` follows it. + +**The DoS property is independent of all of this and always held:** `frame.read_frame` compares the +declared length against the bound *before* reading a body, so a frame declaring 4 GiB is refused for +four bytes and a hostile peer must actually send whatever it claims. Frame size was never protecting +memory; it protects nothing but the wire. + +--- + +**Evidence gathered before the ruling (the original §2.3, preserved):** This is an owner ratification, not a source read. The evidence: @@ -144,8 +188,17 @@ with any single value. It is attached only when a child logger is configured 2. Keep child trajectories and accept that no static cap is derivable; the frame must then be chunked or handle-addressed rather than sized. -Recommendation: **(1)**, ratify 16 MiB. Either way the cap is enforced before allocation by -`repl_sandbox/frame.py:142-143`, which is already built and tested. +Recommendation *(as written 2026-07-22; **superseded** by the ruling above)*: **(1)**, ratify 16 MiB. +Either way the cap is enforced before allocation by `repl_sandbox/frame.py`, which is already built +and tested. + +**How this evidence reads after the ruling.** Its *method* was right and is what the ruling adopts — +size the frame off the largest legitimate slice, times a margin. Only its inputs moved: the slice is +2 MiB rather than 8 MiB, so the frame is 4 MiB rather than 16 MiB. Two figures above are stale as +absolute values and are kept because the reasoning needs them: `BrokerCaps.max_result_bytes` was +8 MiB when this was written, and the shipped `DEFAULT_MAX_FRAME_LEN` it cites as 16 MiB had already +been changed to 2 MiB by the time the contradiction was found — which is how a record can be +internally sound and still describe a tree that has moved underneath it. ## 3. Load-bearing hazards found while reading diff --git a/docs/product/repl-sandbox/REPL_SANDBOX_INTERFACES.md b/docs/product/repl-sandbox/REPL_SANDBOX_INTERFACES.md index 7775691..3689062 100644 --- a/docs/product/repl-sandbox/REPL_SANDBOX_INTERFACES.md +++ b/docs/product/repl-sandbox/REPL_SANDBOX_INTERFACES.md @@ -560,21 +560,27 @@ reads exactly like an enforced one. crosses as `repr`/JSON-safe values or via pickle. The seam requires value-reprs so **no live object or pickle-gadget can ride back across the boundary** (§2); if rlms pickles, the backend must interpose a repr/JSON marshaller. Source-read gated ([RESEARCH §8 (Open items to close before any build) item 1](REPL_SANDBOX_RESEARCH.md)). -3. **`MAX_FRAME_LEN` value** (§3.2) — **derivation rule settled July 22, 2026; the shipped number - remains owner-gated.** The original framing here ("large enough for the biggest legitimate frame - plus headroom") had no derivable answer: the source read found the largest legitimate frame is an - `LMResponse` carrying a child run's whole trajectory, which grows with iteration count, so no - static cap follows from it ([CONFORMANCE §3](REPL_SANDBOX_CONFORMANCE.md)). - - The rule adopted instead sizes the cap off **the worker's context window**, which makes it a - structural guarantee rather than only a DoS bound: **no single frame can context-saturate the - worker it lands in.** Derivation — a 1,050,000-token window × 50% × ~4 bytes/token ≈ 2.1 MB → - **2 MiB**, set as `config.DEFAULT_MAX_FRAME_LEN` with `MODEL_CONTEXT_WINDOW_TOKENS` recorded - beside it so the number is re-derived, not re-guessed, when the model pin changes. This sits - above `ByteLedgerCaps.inbound_per_call`, so the two bounds stack; and the handle model keeps the - context load small by carrying tokens rather than payloads. The DoS property is unchanged — the - reader still rejects an over-length declaration **before** allocating. A ratified number is still - required before the bridge ships. +3. **`MAX_FRAME_LEN` value** (§3.2) — **RATIFIED July 24, 2026: `max_result_bytes` 2 MiB, + `max_frame_len` 4 MiB, the frame derived from the slice.** Full ruling and the evidence behind it: + [CONFORMANCE §2.3](REPL_SANDBOX_CONFORMANCE.md). + + The original framing here ("large enough for the biggest legitimate frame plus headroom") had no + derivable answer, because the largest frame rlms can produce is an `LMResponse` carrying a child + run's whole trajectory, which grows with iteration count. A July 22 rule sized the cap off **the + worker's context window** instead — 1,050,000 tokens × 50% × ~4 bytes/token ≈ 2.1 MB → 2 MiB — on + the theory that no single frame should context-saturate its worker. + + **That rule was right and its layer was wrong, and the correction is the point worth keeping.** A + slice does not enter the model's attention by landing in the guest namespace: `MarshalCaps` holds + that, independently and far lower — a 12 MiB namespace value returns a ~4 KB `exec` reply. So a + context-derived *frame* cap protected nothing, while leaving the frame bound **below** + `BrokerCaps.max_result_bytes`, so a result the broker considered legal could not cross the wire. + The token derivation now sizes the **slice** (`DEFAULT_MAX_RESULT_BYTES`), where "about what one + model pass could consider" is a sound way to choose a number — recorded there as a sizing + convention, never as an enforcing bound. The frame follows it at 2×, and + `tests/test_config.py` asserts `max_frame_len >= 2 * max_result_bytes` so the pair cannot diverge + silently again. The DoS property is unchanged and independent: the reader rejects an over-length + declaration **before** allocating. --- diff --git a/src/repl_sandbox/config.py b/src/repl_sandbox/config.py index e0a7da6..3b0b83b 100644 --- a/src/repl_sandbox/config.py +++ b/src/repl_sandbox/config.py @@ -46,41 +46,73 @@ def version_at_least(observed: str, minimum: str) -> bool: # --------------------------------------------------------------------------- -# Frame bound +# Slice bound, and the frame bound that follows it # --------------------------------------------------------------------------- +# +# Four different things get bounded in this system and they are easy to collapse +# into one number. Keeping them apart is the point of this block: +# +# REPL namespace the corpus the model works over `Tier0Limits.address_space_bytes` +# one slice host store -> guest namespace `BrokerCaps.max_result_bytes` +# model attention what reaches the transcript `MarshalCaps` (this file) +# one wire message a single frame `DEFAULT_MAX_FRAME_LEN` +# +# **The REPL is meant to be large — potentially gigabytes — and read in slices.** +# None of the bounds below constrain that; the namespace ceiling is the rlimit. +# A 12 MiB value in the namespace returns a ~4 KB exec reply, because the +# marshalling caps describe it rather than carrying it. + +#: The context window a slice is sized against, in tokens. Recorded so the +#: derivation below can be re-run rather than re-guessed. +MODEL_CONTEXT_WINDOW_TOKENS = 1_050_000 +#: Fraction of the window one slice may occupy. +SLICE_CONTEXT_FRACTION = 0.5 +#: Bytes per token used to convert the token budget into a byte bound. +BYTES_PER_TOKEN_ESTIMATE = 4 -#: Hard cap on the declared length of a single wire frame. +#: Largest single `materialize` / `slice` return: one unit of content moving from +#: the host store into the guest namespace. #: -#: Derivation rule proposed by the collaborator (Matt) July 22, 2026, with the -#: window he supplied; **the shipped value is still owner-gated** per INTERFACES -#: section 9 item 3, which requires a ratified number before the bridge ships. -#: Nothing ships yet (G1 is unmet), so this is the derived default, not the -#: ratification. +#: Derivation rule proposed by the collaborator (Matt) July 22, 2026 with the +#: window he supplied, and **re-homed onto this constant July 24, 2026** after it +#: was found applied to the frame bound instead. `gpt-5.4-2026-03-05` carries +#: 1,050,000 tokens; half is 525,000; at ~4 bytes per token that is ~2.1 MB, so +#: 2 MiB. Re-derive whenever the model pin changes. #: -#: The rule: size the cap off the worker's context window, not off the largest -#: frame the plumbing might carry. That converts it from a DoS bound into a -#: structural guarantee — **no single frame can context-saturate the worker it -#: lands in.** +#: **Read this as a sizing convention, not an enforcing bound** — the distinction +#: the July 24 correction turned on. A slice does not reach the model's attention +#: by landing in the namespace; `MarshalCaps` holds that, independently and at a +#: far smaller number. So "about what one model pass could consider" is a sound +#: way to *choose* this value and is not a property it *enforces*. Writing it here +#: as though it protected the context would repeat, one layer over, the error that +#: produced the correction. #: -#: Derivation: `gpt-5.4-2026-03-05` carries 1,050,000 tokens; half of that is -#: 525,000; at ~4 bytes per token that is ~2.1 MB, which is 2 MiB. Re-derive this -#: constant whenever the model pin changes — the window is the input, and it is -#: recorded here because it exists nowhere else in the repo. +#: Raising this is the single lever for bulk transfer: a corpus arrives in +#: `ceil(bytes / max_result_bytes)` round trips, so 2 MiB is ~500 calls per GB. +#: `DEFAULT_MAX_FRAME_LEN` follows it and must be re-derived with it. +DEFAULT_MAX_RESULT_BYTES = 2 * 1024 * 1024 + +#: Hard cap on the declared length of a single wire frame. **Derived from the +#: slice bound, never from the context window** (July 24, 2026 — owner ruling). #: -#: The DoS property still holds and is why the reader checks the declared length -#: *before* allocating: the 4-byte prefix admits 4 GiB and a hostile guest will -#: send it. This bound sits above `ByteLedgerCaps.inbound_per_call`, so the two -#: stack rather than contradict, and the handle model keeps the historically -#: largest frame (a context load) small by carrying tokens instead of payloads. -DEFAULT_MAX_FRAME_LEN = 2 * 1024 * 1024 - -#: The context window the frame cap is derived from, in tokens. Recorded so the -#: derivation above can be re-run rather than re-guessed. -MODEL_CONTEXT_WINDOW_TOKENS = 1_050_000 -#: Fraction of the window one frame may occupy. -FRAME_CONTEXT_FRACTION = 0.5 -#: Bytes per token used to convert the token budget into a byte bound. -BYTES_PER_TOKEN_ESTIMATE = 4 +#: The largest legitimate frame is a slice plus its envelope, so the frame cap is +#: the slice times a margin. JSON escaping can inflate a payload well past its raw +#: size, which is what the margin buys; 2x is the figure CONFORMANCE section 2.3 +#: reasoned to and it is kept. +#: +#: The history is worth carrying, because the shape recurs: this constant was +#: briefly derived from the model context window on the theory that no single +#: frame should context-saturate its worker. That protects nothing the marshal +#: caps do not already hold, and it left the shipped frame cap (2 MiB) *below* +#: `max_result_bytes` (8 MiB) — so a maximal legitimate result could not cross the +#: wire at all. The invariant that forecloses it is asserted in +#: `tests/test_config.py`: **`max_frame_len >= 2 * max_result_bytes`.** +#: +#: The DoS property is independent of the number and always held: `frame.read_frame` +#: compares the declared length to this bound *before* reading a body, so a frame +#: declaring 4 GiB is refused for the cost of four bytes and a hostile peer must +#: actually send whatever it claims. +DEFAULT_MAX_FRAME_LEN = 2 * DEFAULT_MAX_RESULT_BYTES @dataclass(frozen=True) @@ -144,7 +176,10 @@ class BrokerCaps: statement_timeout_ms: int = 15_000 bolt_timeout_ms: int = 15_000 max_rows: int = 10_000 - max_result_bytes: int = 8 * 1024 * 1024 + #: One slice, host store -> guest namespace. See `DEFAULT_MAX_RESULT_BYTES` + #: for the derivation and for why it is a sizing convention rather than a + #: bound on the model's attention. + max_result_bytes: int = DEFAULT_MAX_RESULT_BYTES @dataclass(frozen=True) diff --git a/src/repl_sandbox/tests/test_config.py b/src/repl_sandbox/tests/test_config.py new file mode 100644 index 0000000..44ddaa1 --- /dev/null +++ b/src/repl_sandbox/tests/test_config.py @@ -0,0 +1,101 @@ +"""The bounds, and the relationships between them that a single edit can break. + +Each constant here is defensible on its own and the failure this file exists for +is a *pair* going wrong while both members still look reasonable — which is +exactly how `max_frame_len` (2 MiB) came to sit below `max_result_bytes` (8 MiB), +leaving a maximal legitimate slice unable to cross the wire. Neither number was +absurd; only their relationship was. +""" + +from __future__ import annotations + +import math + +from repl_sandbox.config import ( + BYTES_PER_TOKEN_ESTIMATE, + DEFAULT_MAX_FRAME_LEN, + DEFAULT_MAX_RESULT_BYTES, + MODEL_CONTEXT_WINDOW_TOKENS, + SLICE_CONTEXT_FRACTION, + SandboxConfig, +) +from repl_sandbox.hardening import Tier0Limits + +#: The margin a frame carries over the slice it must be able to hold. JSON +#: escaping can inflate a payload well past its raw size; this is what pays for +#: that, and CONFORMANCE section 2.3 is where the figure was reasoned to. +FRAME_OVER_SLICE = 2 + + +def test_a_maximal_slice_fits_in_a_frame() -> None: + """The invariant the July 24 correction installed. + + A `materialize` result is built host-side against `max_result_bytes` and then + has to cross the wire. If the frame cap is the smaller of the two, a result + the broker considers legal cannot be delivered — and nothing else in the tree + compares them, so both stay individually plausible while the path is dead. + """ + config = SandboxConfig() + assert config.max_frame_len >= FRAME_OVER_SLICE * config.broker_caps.max_result_bytes + + +def test_the_frame_bound_is_derived_from_the_slice_bound_not_the_context_window() -> None: + """Derivation direction, pinned because reversing it is what went wrong. + + The frame bound is a function of the slice bound. It is *not* a function of + the model's context window: a slice does not enter the model's attention by + landing in the guest namespace, so a context-derived frame cap protects + nothing the marshal caps do not already hold, at a far smaller number. + """ + assert DEFAULT_MAX_FRAME_LEN == FRAME_OVER_SLICE * DEFAULT_MAX_RESULT_BYTES + + +def test_the_slice_bound_matches_its_recorded_token_derivation() -> None: + """The sizing convention re-runs from its own recorded inputs. + + A convention rather than an enforcing bound — "about what one model pass + could consider" is how the number is *chosen*, and `MarshalCaps` is what + actually keeps content out of the transcript. Recomputed here so a changed + model pin cannot leave the constant behind, silently. + """ + derived = MODEL_CONTEXT_WINDOW_TOKENS * SLICE_CONTEXT_FRACTION * BYTES_PER_TOKEN_ESTIMATE + # 2 MiB is the power-of-two the derivation rounds to; hold it to within one + # binary order so a re-derivation has to be witting rather than incidental. + assert 0.5 <= DEFAULT_MAX_RESULT_BYTES / derived <= 2.0 + + +def test_marshal_caps_are_the_thing_that_bounds_the_transcript() -> None: + """Each attention cap is far below a slice, which is the layering. + + If a marshal cap ever approached the slice bound, content would start + reaching the model by volume rather than by the model asking for it, and the + context property really would depend on the transfer bounds. + """ + config = SandboxConfig() + slice_bytes = config.broker_caps.max_result_bytes + for cap in ( + config.marshal_caps.stdout_bytes, + config.marshal_caps.stderr_bytes, + config.marshal_caps.answer_bytes, + ): + assert cap * 8 <= slice_bytes + + +def test_the_namespace_ceiling_is_the_rlimit_and_dwarfs_a_slice() -> None: + """What actually bounds a large REPL, stated where the caps live. + + The corpus ceiling is address space, not any wire or slice number. Holding + the ratio here keeps the "REPL is gigabytes, read in slices" property from + being quietly inverted by raising a slice toward the namespace size. + """ + limits = Tier0Limits() + assert limits.address_space_bytes >= 64 * DEFAULT_MAX_RESULT_BYTES + # A GiB namespace filled 2 MiB at a time: the round-trip cost is real and is + # the reason `max_result_bytes` is the lever to move for bulk transfer. + assert math.ceil(limits.address_space_bytes / DEFAULT_MAX_RESULT_BYTES) == 512 + + +def test_the_inbound_literal_cap_stays_under_a_frame() -> None: + """`load_context` literals ride a frame too, so they cannot exceed one.""" + config = SandboxConfig() + assert config.byte_caps.inbound_per_call <= config.max_frame_len