From 2ca4113ce5120153de7fcdbad7a61252d8758407 Mon Sep 17 00:00:00 2001 From: Patrick Buckley Date: Thu, 9 Jul 2026 19:12:32 -0700 Subject: [PATCH] docs(hypothesis): carry the factored Q_E reading into the glossary; primer wording Review follow-ups: the s-shorthand convention and its glossary echo now cover Q_E's own state argument (s -> w where Q_E reads it), and the Q_E glossary row carries the factored (w, a) ~> (w', o) reading so the symbol table no longer reintroduces the environment-reads-all-of-s interpretation the outer-kernel note warns against. PRIMER: the top-alone-widens bullet keeps owner language anchored to the simple-case top; success is defined as an accepted end, consistent with the declared-vs-actually-right distinction two sentences later. --- HYPOTHESIS.md | 6 +++--- PRIMER.md | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/HYPOTHESIS.md b/HYPOTHESIS.md index 9cdfdb63..ed770c09 100644 --- a/HYPOTHESIS.md +++ b/HYPOTHESIS.md @@ -20,7 +20,7 @@ Most descriptions of an agent framework are a feature list. This is an attempt a $$T(s, A) = \int_{\mathcal{Y}}\!\int_{\mathcal{E}} \mathbf{1}_A\!\big(\rho(s, y, \gamma(s,y), e)\big)\; Q_E\big(s, \gamma(s,y), de\big)\; M_W(\pi(s), dy), \qquad T(s,A)=\mathbf{1}_A(s)\ \text{ for } s\in H,$$ -and the harness runs $s_{n+1} \sim T(s_n)$ from an initial $s_0 \sim \mu_0$ until $\tau_H = \inf\{n : s_n \in H\}$. Because $\pi, \gamma, \rho, H$ are deterministic they contribute no integration variable of their own — they appear as measurable transformations inside the integrand (the pushforward), not literally outside it — so the controller injects no randomness, and every coin is inherited from $M_W$ and $Q_E$. (The earlier shorthand $T = \rho \circ (M_W \circ \pi, E)$ is suggestive but ill-typed — $M_W$ returns a *law*, while $\rho$ consumes a *sample* together with the prior state $s$; the integral is what the shorthand meant.) One typing subtlety the displayed form hides, and the chokepoint claim depends on it: writing $Q_E(s,a)$ lets the environment read *all* of $s$ — including secrets and prior model output $\rho$ folded in, which would be a delayed model-to-world path $y_n \to s_{n+1} \to Q_E$ that never re-crossed $\gamma$. The intended reading factors the state, $s=(q,w)$ with $q$ controller-observable and $w$ possibly-latent world state, and restricts the tool kernel to $Q_E(w, a)$: the environment sees only the world and the *authorized, capability-scoped* action, so anything from $q$ the tool needs must be placed **inside $a$**, after authorization. The factorization retypes the kernel's *output* as well, and has to: $Q_E$ becomes a kernel $(w,a)\rightsquigarrow(w',o)$ — the actual next world together with the observed receipt — and $\rho$ acts as $\rho\big((q,w),y,a,(w',o)\big)=(\rho_q(q,y,a,o),\,w')$, folding only the receipt into controller state while the world writes itself; the displayed $T$, in which $\rho$ appears to manufacture the entire next state from $e$, is the unfactored shorthand — read $e=(w',o)$ with $\rho_q$ blind to the $w'$ coordinate — for if $\rho$ *computed* the world from the receipt, the ledger would be true by construction and the reported-vs-actual gap of *Reading it* could not exist. Under that factorization $B$ is properly a subset of the global $(q,w)$, and $\gamma$ is genuinely the only channel from model output into the world; the single-symbol $s$ elsewhere in this document is shorthand for $q$ wherever a controller map reads it and for $(q,w)$ wherever reach-avoid is evaluated. +and the harness runs $s_{n+1} \sim T(s_n)$ from an initial $s_0 \sim \mu_0$ until $\tau_H = \inf\{n : s_n \in H\}$. Because $\pi, \gamma, \rho, H$ are deterministic they contribute no integration variable of their own — they appear as measurable transformations inside the integrand (the pushforward), not literally outside it — so the controller injects no randomness, and every coin is inherited from $M_W$ and $Q_E$. (The earlier shorthand $T = \rho \circ (M_W \circ \pi, E)$ is suggestive but ill-typed — $M_W$ returns a *law*, while $\rho$ consumes a *sample* together with the prior state $s$; the integral is what the shorthand meant.) One typing subtlety the displayed form hides, and the chokepoint claim depends on it: writing $Q_E(s,a)$ lets the environment read *all* of $s$ — including secrets and prior model output $\rho$ folded in, which would be a delayed model-to-world path $y_n \to s_{n+1} \to Q_E$ that never re-crossed $\gamma$. The intended reading factors the state, $s=(q,w)$ with $q$ controller-observable and $w$ possibly-latent world state, and restricts the tool kernel to $Q_E(w, a)$: the environment sees only the world and the *authorized, capability-scoped* action, so anything from $q$ the tool needs must be placed **inside $a$**, after authorization. The factorization retypes the kernel's *output* as well, and has to: $Q_E$ becomes a kernel $(w,a)\rightsquigarrow(w',o)$ — the actual next world together with the observed receipt — and $\rho$ acts as $\rho\big((q,w),y,a,(w',o)\big)=(\rho_q(q,y,a,o),\,w')$, folding only the receipt into controller state while the world writes itself; the displayed $T$, in which $\rho$ appears to manufacture the entire next state from $e$, is the unfactored shorthand — read $e=(w',o)$ with $\rho_q$ blind to the $w'$ coordinate — for if $\rho$ *computed* the world from the receipt, the ledger would be true by construction and the reported-vs-actual gap of *Reading it* could not exist. Under that factorization $B$ is properly a subset of the global $(q,w)$, and $\gamma$ is genuinely the only channel from model output into the world; the single-symbol $s$ elsewhere in this document is shorthand for $q$ wherever a controller map reads it, for $w$ alone where $Q_E$ reads it, and for $(q,w)$ wherever reach-avoid is evaluated. *Fail-closed.* The gate $\gamma$ is what makes **fail-closed** a property, not just a name: model output is an *untrusted proposal*, and $\gamma(s,y)=\bot$ forces a no-op environment response ($Q_E(s,\bot,\cdot)=\delta_{e_0}$) — so a malformed or unauthorized tool call is rejected *before* it can act, not validated after its side effects have landed. Fail-closed is then the property that a rejected proposal causes *no unauthorized side effect* and lands in a **safe, non-bad** set — but quantified honestly it holds only *from* already-safe states, so the sharp form names a **rejection-invariant safe set** $K$ with $s\in K,\ \gamma(s,y)=\bot_{\mathcal{A}} \Rightarrow \rho(s,y,\bot_{\mathcal{A}},e_0)\in K$ (and $K\cap B=\varnothing$): a rejection from inside $K$ stays inside $K$, landing in a non-accepting terminal $H\setminus H_{\mathrm{ok}}$ in the strict case or a safe non-terminal state when the spec retries. Fail-closed is closure of $K$ under rejection, not a claim that rejection rescues a state already in $B$. And $\rho$ must validate the tool *response* $e$, not only the proposal that $\gamma$ already gated: a malformed or adversarial response $e$ is caught at fold-back, not just at the gate. But response-validation has a hard limit: $\rho$ can reject a bad tool *response*, yet it cannot undo side effects an *authorized* action already caused — so $\gamma$, not $\rho$, is the last line before irreversible effects, and anything irreversible must be gated at authorization. The boundary is also only real if raw model output reaches *no* sink — tool, logger, browser, or remote call — before $\gamma$; any pre-authorization escape bypasses the gate. The user-visible final response and any logging are themselves effects, and the rule binds *model-authored* bytes: they reach a sink either as an authorized action through $\gamma$, or only after an accepted halt in $H_{\mathrm{ok}}$. Shell-*templated* text — a refusal notice, a cancellation report reading the ledger — is controller output, outside $\gamma$'s jurisdiction, and may accompany any halt (a template that *interpolates* model-authored fragments inherits the model's label — the appendix's meet rule — and those bytes are gated like any others); the invariant is that raw model text never reaches a sink ungated, not that failed runs die silent. @@ -41,11 +41,11 @@ Two stopped processes, nested: **deterministic control over stochastic dynamics | Symbol | Is | |---|---| | $\mathcal{H},\ \mu_0$ | the harness — the whole controlled system, *not* the model — with **initial law** $\mu_0$ on $\mathcal{S}$ a member of the tuple (determinism is conditional on a fixed $s_0$; a free $\mu_0$ is itself a coin) | -| $s \in \mathcal{S}$ | task-state: IR / dialect stack, tool results, plan, counters, **and every mutable interface variable** (model/tool versions, permissions, retrieved context) — only Markov *after* that augmentation. Factored where precision demands it (*The outer kernel*) as $s=(q,w)$: **controller-observable** $q$ (what $\pi,\gamma,\rho$ read) and **possibly-latent world state** $w$ (what only $Q_E$ touches); the observed effect $o$ is the receipt $Q_E$ returns, in general *reported* not actual. Elsewhere the single $s$ means $q$ where a controller map reads it, $(q,w)$ where reach-avoid is evaluated | +| $s \in \mathcal{S}$ | task-state: IR / dialect stack, tool results, plan, counters, **and every mutable interface variable** (model/tool versions, permissions, retrieved context) — only Markov *after* that augmentation. Factored where precision demands it (*The outer kernel*) as $s=(q,w)$: **controller-observable** $q$ (what $\pi,\gamma,\rho$ read) and **possibly-latent world state** $w$ (what only $Q_E$ touches); the observed effect $o$ is the receipt $Q_E$ returns, in general *reported* not actual. Elsewhere the single $s$ means $q$ where a controller map reads it, $w$ where $Q_E$ reads it, $(q,w)$ where reach-avoid is evaluated | | $\mathcal{C},\ \mathcal{Y},\ \mathcal{A},\ \mathcal{E}$ | the **context / readout / action / effect spaces** — model-visible context $\mathcal{C}$, model readout $\mathcal{Y}$ (incl. the **parse-failure** $\bot_{\mathcal{Y}}$, emitted by $M_W$ when no readout forms), authorized actions $\mathcal{A}$ (with $\mathcal{A}_{\bot} = \mathcal{A}\cup\{\bot_{\mathcal{A}}\}$, the **authorization rejection** returned by $\gamma$), and tool/environment effects $\mathcal{E}$; the two $\bot$s are distinct events — un-parsed vs parsed-and-refused — both forcing the no-op $e_0$ | | $\pi : \mathcal{S} \to \mathcal{C}$ | **lowering** — prompt construction, dialect lowering, effective-program selection (deterministic) | | $M_W(c, dy)$ | the **model-run kernel** (inner solver) — a stopped autoregressive process; $\Phi_W$ is the residual-stream ("manifold") core in the transformer case | -| $Q_E(s, a, de)$ | the **environment/tool kernel** on the authorized action $a\in\mathcal{A}_{\bot}$ (with $Q_E(s,\bot,\cdot)=\delta_{e_0}$, the no-op $e_0$) — tool effects, API responses, the world (possibly adversarial) | +| $Q_E(s, a, de)$ | the **environment/tool kernel** on the authorized action $a\in\mathcal{A}_{\bot}$ (with $Q_E(s,\bot,\cdot)=\delta_{e_0}$, the no-op $e_0$) — tool effects, API responses, the world (possibly adversarial); factored (*The outer kernel*) as $Q_E(w,a)\rightsquigarrow(w',o)$ — the environment reads world state and the authorized action, never $q$ | | $\gamma,\ \rho$ | the deterministic **authorization gate** $\gamma:\mathcal{S}\times\mathcal{Y}\to\mathcal{A}_{\bot}$ (untrusted proposal → authorized action or $\bot$) and the **fail-closed verify-and-fold-back** $\rho:\mathcal{S}\times\mathcal{Y}\times\mathcal{A}_{\bot}\times\mathcal{E}\to\mathcal{S}$ | | $H,\ \tau_H$ | the **halt set** (absorbing) and the outer **halting time** — a hitting-time process, not a single pass | | $H_{\mathrm{ok}},\ B$ | the **accepting halts** $H_{\mathrm{ok}}\subseteq H$ — read operationally as $H_{\mathrm{acc}}$, what the *controller declares* accepted (all an implementation can test), as against an **analysis-only** ground-truth success $G\subseteq H$ that need not be computable ($H_{\mathrm{acc}}\setminus G$ is the semantic-adequacy gap: accepted yet wrong) — and the **bad set** $B$, unsafe states for reach-avoid ($B\cap H_{\mathrm{ok}}=\varnothing$), evaluated on the global $(q,w)$, *separate* from $H$ and possibly entered mid-run before any halt | diff --git a/PRIMER.md b/PRIMER.md index f9dcad2d..d1d0c953 100644 --- a/PRIMER.md +++ b/PRIMER.md @@ -85,13 +85,13 @@ A measurement is a risk metric. A proof is a certificate. Keeping those two word Formally, security here is a *reach-avoid* problem: reach a good stop, never touch the danger zone, **while an adversary picks the worst tool outputs your setup permits**. That last clause is the formal home of prompt injection: injection isn't "the model misbehaved," it's the environment optimized to bend your loop — poisoned pages, malicious tool descriptions, crafted responses. -Two different numbers fall out here, and dashboards love to collapse them: *success* (reached the right end before anything went wrong — a safe refusal counts against it) and *safety* (never touched the danger zone — a safe refusal is perfectly safe). Track both. They move independently. And both are scored by your own stop rule — they count what the shell *declared* a success. Whether a declared success was actually *right* is a third, harder number that no dashboard inside the system can produce; only a judge outside the run — a test suite, an audit, ground truth — can. +Two different numbers fall out here, and dashboards love to collapse them: *success* (reached an accepted end before anything went wrong — a safe refusal counts against it) and *safety* (never touched the danger zone — a safe refusal is perfectly safe). Track both. They move independently. And both are scored by your own stop rule — they count what the shell *declared* a success. Whether a declared success was actually *right* is a third, harder number that no dashboard inside the system can produce; only a judge outside the run — a test suite, an audit, ground truth — can. The gate handles the visible half of injection: the model, freshly poisoned, proposes emailing your credentials somewhere, and the gate refuses — and injection or not, the action does not happen. But the deeper attack doesn't propose a bad action today. It rewrites *what the run believes its job is* — it edits the plan — and then every future action looks locally reasonable against a corrupted plan. So memory has to be partitioned: **data** (tool results, fetched pages, retrieved documents — content the world supplied) and **control** (the plan, the permissions, what is authorized next). The security claim is conditional on that partition holding: untrusted content lands in data, always. And "trust" is really two questions pointing opposite ways, which is worth keeping straight: *can this leak?* (a value is as secret as the most-secret thing that fed it — secrecy flows **upward**) and *can this boss us around?* (a value is as trustworthy as the least-trustworthy thing that fed it — authority flows **downward**). Untrusted content is safe as *data* precisely because the second question keeps it off the control side; a secret is kept out of the model by the first. Lowering either barrier on purpose — declassifying a secret, promoting data to trusted — is an explicit decision the owner makes, never a thing that happens by accident when two values are combined. Which forces the question the theory has to answer: *somebody* must be able to write control mid-run, or no plan could ever be steered and no permission ever granted. The answer is a small hierarchy with a top the model can't reach. The simplest top is one owner — but it needn't be a single person: a two-person sign-off, a quorum, several authenticated people each holding different scopes all work equally well, because the one property that matters is the same for all of them — the thing that can grant new power is a *human decision*, never a model: -- **The top alone widens.** New permission, bigger budget, approval of the irreversible thing — asking the owner is itself an ordinary tool call, and the owner's answer is the one kind of tool result allowed to change control. +- **The top alone widens.** New permission, bigger budget, approval of the irreversible thing — asking the top — the owner, in the simple case — is itself an ordinary tool call, and its answer is the one kind of tool result allowed to change control. - **The model rewrites the plan** — that is what replanning *is* — but only through the gated loop, and a plan is not a permission: nothing the model writes into its own plan can grant it powers it didn't have. - **Everything else is data.** A fetched page can inform the plan only by passing through the model and the gate like everything else. It can suggest. It cannot promote itself to boss. - **AI judges only tighten.** Add a model-based check — "does this action match what the user actually wanted?" — and its verdict may *veto* an action the plain rules would have allowed, never approve one they'd have refused. A judge that can approve is a tricked judge that can open the vault. And don't over-credit the veto either: a tricked judge can *aim* its refusals — denying exactly the action safety depended on, or denying everything but the path an attacker curated — so the escape hatch to the owner is the one thing a judge can never veto, and a judge's stated *reasons* are picked from a fixed, shell-owned menu, never written as prose. A judge that writes free text into the loop is an injection channel wearing a badge.