kyle/boxmaker
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

M3a spec: fold in the defects the plan's checks found in areas A to D

Browse Source 
DecisionRecord's empty struct variants, the verifier's report fields and
region rule, the startup fallback, the IPv4 host rule, Denial, BrokerPort
deadlines and envelope id, the runbook anchor rule, bxctl's --say/--json
and escaping. Recorded in docs/decisions.md; the array-form question is
left open.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This commit is contained in:
kyle
2026-09-18 23:09:32 -07:00
co-authored by Claude Opus 5
parent b39dac3f71
commit 43f5b8abc6
2 changed files with 109 additions and 40 deletions
Download Patch File Download Diff File Expand all files Collapse all files
docs/specs/2026-09-18-m3a-decision-path.md
+105 -40
View File
@@ -1,7 +1,8 @@
# M3a design: the decision path
Status: draft for owner review, 2026-09-18; revised the same day after a design review (the
"Spec review of M3a" rows in `docs/decisions.md`). M3 is split in two (`docs/decisions.md`). M3a is
"Spec review of M3a" rows in `docs/decisions.md`), and again after the plan's checks (the "M3a plan
checks" rows there). M3 is split in two (`docs/decisions.md`). M3a is
everything that decides whether a tool call may run and records it: grant files and matching,
session taint, the audit log, approvals through `bxctl`, the two `brokerd` sockets, and `loopd`'s
real tool port. Tools themselves do not run in M3a: the runner is a trait whose only
@@ -98,13 +99,16 @@ admin = "/var/lib/boxmaker/run/owner-broker/admin.sock"
ttl_ms = 900000 # 15 min
```
A socket path that is absent or empty means the default under `home`, as in `loopd`.
## 3. Grants
### Files
One grant per file, `grants/<id>.toml`. The id is the file stem: 1 to 64 characters of
`[a-z0-9-]`. Other files in the directory (not ending in `.toml`) are ignored; a `.toml` file with
a bad stem is an invalid grant. The fields are `proto::Grant` as defined in M1.
a bad stem is an invalid grant. A grants directory that is missing or cannot be read makes the set
invalid; an empty directory is a valid empty set. The fields are `proto::Grant` as defined in M1.
```toml
# grants/notes-read.toml
@@ -228,12 +232,16 @@ component. Paths are compared as they are, never normalised, and matching is by
`brokerd` does not resolve symlinks. In M3b only the matched grant directory is mounted, at the
same path, so a symlink pointing outside it points at nothing inside the container.
When several of a grant's paths contain the argument, the longest one is the matched path.
When several of a grant's paths contain the argument, the longest one is the matched path. For
`write_file`, a grant path equal to the argument does not count: with `paths = ["/s", "/s/out"]`,
a write to `/s/out` is covered through `/s`, and `/s` is the matched path.
### Hosts
A host name: 1 to 253 bytes, lowercase, at least two labels separated by `.`, each label 1 to 63
bytes of `[a-z0-9-]` not starting or ending with `-`. A host pattern in a grant is a host name, or
bytes of `[a-z0-9-]` not starting or ending with `-`, and the last label starts with a letter,
which excludes every spelling of an IPv4 address (`127.0.0.1`, `127.1`, `10.0.0.0x1`). A host
pattern in a grant is a host name, or
`*.` followed by a host name.
| Grant host | URL host | Result |
@@ -256,16 +264,18 @@ the property test drive it.
```rust
pub struct SessionState { pub taint: DataClass, pub untrusted: bool }
pub enum Outcome {
Allowed(Decision),
Ask(Ask),
Denied { reason: DenyReason, grant: Option<String> },
pub struct Denial {
pub reason: DenyReason,
pub grant: Option<String>, // the `deny` grant, for `denied_by_grant` only
pub grant_sha256: Option<Hash32>,
}
pub enum Outcome { Allowed(Decision), Ask(Ask), Denied(Denial) }
pub fn decide(request: ToolRequest, grants: &GrantSet, state: SessionState, now: Timestamp)
-> Outcome;
pub fn redecide(ask: Ask, grants: &GrantSet, state: SessionState, now: Timestamp)
-> Result<Decision, DenyReason>;
-> Result<Decision, Denial>;
```
- `Ask` is built like `Decision`: private fields, no `Clone`, no `Deserialize`, a `compile_fail`
@@ -274,7 +284,7 @@ pub fn redecide(ask: Ask, grants: &GrantSet, state: SessionState, now: Timestamp
into a `Decision`, so "this call was approved" is a fact about the types, not about the order
of statements in `broker`.
- `redecide` runs the same matching again. `ask` and `auto` both give a `Decision`; anything else
gives the reason.
gives the `Denial`, whose grant and file hash the `Approval` record needs.
- `broker` checks in this order, and the first that applies is the answer: the grant set is
invalid (`grants_invalid`); the session's state cannot be read (`state_unreadable`); then
`decide`, inside which: the tool is not one of the four (`no_grant`, arguments not parsed); the
@@ -295,7 +305,8 @@ pub fn redecide(ask: Ask, grants: &GrantSet, state: SessionState, now: Timestamp
Neither ever goes down. The read, the comparison and the write happen under the ledger lock
(section 2). A `failed` call changes nothing: its message is `brokerd`'s own text (section 7).
- Writes are atomic: write `<id>.json.tmp`, `fsync`, rename over `<id>.json`, `fsync` the directory.
- A file that exists but cannot be read or parsed is an error: every call for that session is
- A file that exists but cannot be read or parsed, or that says `public` (a session is never below
`private`, so `brokerd` did not write it), is an error: every call for that session is
denied with `state_unreadable` and `brokerd` prints `see docs/runbook.md#broker-state-damaged`.
- The brief's State list names this file (P14, applied 2026-09-18).
- `loopd` has no access to `<home>/broker/`. The `class` and `untrusted` values it logs are a copy
@@ -342,9 +353,13 @@ pub enum AuditEvent {
}
#[serde(tag = "outcome", rename_all = "snake_case")]
pub enum DecisionRecord { Allowed, Ask, Denied { reason: DenyReason } }
pub enum DecisionRecord { Allowed {}, Ask {}, Denied { reason: DenyReason } }
```
`Allowed {}` and `Ask {}` are empty struct variants, not unit variants: serde does not apply
`deny_unknown_fields` to a unit variant of an internally tagged enum, so with `Allowed` the text
`{"outcome":"allowed","x":1}` would decode. The JSON is the same either way.
`DecisionRecord` keeps the name the brief uses for the plain record of a decision; its M1 shape
(with `grant` inside and an `Approved` variant) is replaced, since approval is now its own event.
@@ -411,20 +426,35 @@ impl ChainVerifier {
pub fn resume(next_seq: u64, prev: Hash32) -> Self; // continue from a known point
pub fn file(&mut self, name: &str); // starts the next file
pub fn line(&mut self, bytes: &[u8], has_newline: bool); // false only for a file's last line
pub fn feed(&mut self, name: &str, content: &[u8]); // file, then each of its lines
pub fn finish(self) -> ChainReport;
}
pub struct ChainReport {
pub records: u64, pub head: Option<Hash32>, pub next_seq: u64,
pub failure: Option<ChainFailure>, // the first one: file, line (1-based), what
pub failure: Option<ChainFailure>, // the first one since the last accepted break
pub recoveries: Vec<Location>, pub accepted_breaks: Vec<Location>,
pub abandoned: Vec<u64>, // seq of Ask decisions with no Approval after them
pub unfinished: Vec<u64>, // seq of allowed decisions, and of approvals whose
// outcome is allowed, with no Result after them
pub unfinished: Vec<u64>, // seq of decisions allowed, at once or by approval,
// with no Result after them
pub clock_warnings: Vec<Location>, // time went backwards
pub torn_tail: Option<Location>, // the last line of the last file needs recovery
pub torn_tail: Option<TornTail>, // the last line of the last file needs recovery
}
pub struct ChainFailure { // file, line (1-based), what; and what an
pub file: String, pub line: u64, pub what: String, // AcceptedBreak appended now must carry
pub last_good: Hash32, pub break_prev: Hash32, pub break_seq: u64,
pub tail_torn: bool, // the last line fed has no newline
}
pub struct TornTail { // and what its Recovery record must carry
pub at: Location, pub has_newline: bool, pub bytes: u64, pub sha256: Hash32,
pub recovery_prev: Hash32, pub recovery_seq: u64,
}
```
The report carries what the writer must put in a `Recovery` or `AcceptedBreak` record, so that no
consumer computes `seq` or `prev` a second time. Both lists name the *decision's* `seq`, for an
approved call too: `Approval.decision` and `Result.decision` both refer to it, and it is the
approval id the owner saw.
A line fails if it does not parse as an `AuditRecord`, its `seq` is not the next one, or its
`prev` is not the hash of the line before. Files are fed in name order; a file whose first record
does not chain from the previous file's last line fails at its line 1. Two cases are not failures:
@@ -440,6 +470,9 @@ does not chain from the previous file's last line fails at its line 1. Two cases
record exactly before its newline, leaving complete JSON. A recovered line is not a record and
nothing may refer to its `seq`, which the `Recovery` record reuses. Reported in `recoveries`.
A `Recovery` record that describes no line (its hash and length match nothing before it) is a
failure at the `Recovery` record.
The verifier therefore holds each line back until it has seen the next one, and judges it then (or
at `finish`).
@@ -462,15 +495,21 @@ record and are not checked, so one break covers every failure before it.
A verifier started with `resume` has not seen the earlier files. When it meets an `AcceptedBreak`
whose `file` sorts before the first file it was given, it checks only `prev`, accepts it and
continues from it; the full verification judges the rest.
continues from it; the full verification judges the rest. This holds inside a failed region too:
if the latest file has damage before such a break record, the resumed verifier is already in a
region when it meets the break, and the break still clears it. Otherwise a correctly accepted
break would stop every later start while `--accept-break` said "nothing to accept".
### Startup
1. Take the lock. If it is held: print "brokerd is already running"
and `see docs/runbook.md#brokerd-already-running`, exit 1.
2. Without `--accept-break`: verify the latest file, resumed from the last line of the file before
it (if any). That line must parse as a record, or it is the failure. The earlier files are not
re-read; `bxctl audit verify` does that. With `--accept-break`: verify every file, exactly as
it (if any). If that line does not parse as a record, there is no point to resume from, and the
whole log is verified instead. (Treating it as the failure would deadlock: after a break at
that very line is accepted, every later start would fail on it again.) Otherwise the earlier
files are not re-read; `bxctl audit verify` does that. Damage in an older file is therefore not
seen by an ordinary start, by design. With `--accept-break`: verify every file, exactly as
`bxctl audit verify` does, because the break to accept must be the first failure of the whole
log, and it may lie in an older file that the short check never reads.
3. If the report has a failure: without `--accept-break`, write nothing, print the failure's file,
@@ -481,7 +520,8 @@ continues from it; the full verification judges the rest.
4. Otherwise, if the report has a torn tail: write `\n` after the torn bytes if it is missing,
then a `Recovery` record chained from the line before the torn one. Print "audit: recovered a
torn final line" and `see docs/runbook.md#audit-recovered`.
5. `--accept-break` with no failure is an error: "nothing to accept". Exit 2.
5. `--accept-break` with no failure is an error: "nothing to accept". Exit 2. It writes nothing,
not even the recovery of a torn tail; the next start without the flag does that.
An empty latest file (created, then a crash before its first record) is not a failure and needs
no recovery: the next record is its line 1 and chains from the file before.
@@ -582,7 +622,8 @@ pub struct GrantProblem { pub file: String, pub line: Option<u64>, pub problem:
An unknown or already answered `approval` is `error` `no_such_approval`.
`PendingApproval.arguments` is not the string `loopd` sent. It is the parsed arguments serialised
again by `serde_json` from the typed value in `args`, fields in the order of section 3's table.
again by `serde_json` from the typed value in `args`, fields in the order of section 3's table,
compact, with an absent `cwd` left out (`"cwd": null` in the request means absent).
The owner approves what policy matched: in the raw string `"\u002fetc"` and `"/etc"` look
different and mean the same, and the re-serialised form shows both as `/etc`. The audit log keeps
the raw string.
@@ -633,17 +674,27 @@ processes, output size) are M3b's.
- **`BrokerPort`** implements `ToolPort` over `broker.sock`. `ToolPort::call` gains a callback:
`fn call(&self, req: &ToolRequest, on_pending: &mut dyn FnMut(&Pending)) -> ToolResponse`.
The read timeout is `[broker] timeout_ms` (default 120,000) until the first frame. After a
pending frame it runs until the frame's `expires` plus `timeout_ms`, which leaves a call
approved at the last moment the same time to run as any other. M3b must keep its tool time
limit under `timeout_ms`. If the socket cannot be reached, closes early or times out, the answer
is `Failed { "the tool broker is unavailable" }`, and `loopd` prints
`BrokerPort` waits for the first frame until `[broker] timeout_ms` (default 120,000) after the
call began, and after a pending frame until the frame's `expires` plus `timeout_ms`, which
leaves a call approved at the last moment the same time to run as any other. These are
deadlines, not per-read socket timeouts: a peer that trickles bytes must not hold a turn for
ever. (Unlike the inference path's liveness rule, this is a total limit.) M3b must keep its tool
time limit under `timeout_ms`. If the socket cannot be reached, closes early or times out, the
answer is `Failed { "the tool broker is unavailable" }`, and `loopd` prints
`see docs/runbook.md#broker-unavailable`. The turn goes on.
- The envelope `id` of a tool request is `request.call.0`, and every answer must carry it. Also
failures of the port, each with its own fixed text and no runbook pointer unless it says so: a
request too large for one frame ("the request is too large for the tool broker"); a pending
frame as the final answer ("the tool broker gave no final answer"); an `expires` so far off
that the deadline cannot be computed is a broker that is unavailable. `timeout_ms = 0` is not
refused at load; every call then fails closed as unavailable.
- **`clock` moves into `loopd`**, beside `find_tool` and `call_tool`: the time is not authority and
needs no broker. The core tools stay `clock`, `find_tool`, `call_tool`. The registry's
discoverable tools become `read_file`, `write_file`, `shell`, `http_fetch`, with the argument
schemas from section 3. `echo` stays in `FakeTools` for tests only. This changes the baseline of
new sessions only.
schemas from section 3. `echo` stays in `FakeTools` and in the test registry `Registry::m2b()`,
which recorded conversations and tests find it through; `loopd serve` uses `Registry::m3a()`.
The `tools` array is the same for both (`clock`, `find_tool`, `call_tool`), so this changes only
what `find_tool` finds.
- **Denials become tool results** the model can explain, written by `loopd` (`class` public,
`untrusted` false):
@@ -664,7 +715,9 @@ processes, output size) are M3b's.
frame arrives. It is a notice that something is waiting, not a description of it: `loopd` does
not know the grant or the taint, and what the owner is shown must not come from `loopd`
(section 9). `tool_denied { name, reason }` is sent before the `tool_result` event of a denied
call, so the owner sees the reason itself and not only the model's account of it.
call, so the owner sees the reason itself and not only the model's account of it. In both
events the tool is the one `brokerd` decides on (`request.tool`), not `call_tool`;
`tool_call_started` and `tool_result` keep the name the model called.
- **Config**: `[broker] socket` and `[broker] timeout_ms`. If `socket` is absent, `loopd serve`
uses no port and every tool call except the core ones fails with "no tool broker is
configured"; `loopd` prints that once at startup with `see docs/runbook.md#broker-unavailable`.
@@ -678,7 +731,7 @@ processes, output size) are M3b's.
```
41 2 min ago expires in 13 min session chat-1758… grant shell-scratch taint private
shell {"command": "rm -rf /home/kyle/scratch/build", "cwd": "/home/kyle/scratch"}
shell {"command":"rm -rf /home/kyle/scratch/build","cwd":"/home/kyle/scratch"}
```
- `bxctl approve <id>` prints `approved 41: runs` (exit status 0) or
@@ -689,8 +742,10 @@ processes, output size) are M3b's.
status 1 if there are problems.
- `bxctl audit verify [--home <path>]` reads `<home>/audit/` itself (no daemon) and prints
`audit: ok, <n> records, head <hex>`, then any recoveries, accepted breaks, approvals "pending or
abandoned", calls "running or unfinished" and clock warnings, one per line; or the failure as
`<file>:<line>: <what>` and exit status 1. The two double names are because `bxctl` reads the
abandoned", calls "running or unfinished", clock warnings and a torn final line, one per line
(the exact lines are fixed in task 19; a torn tail is also what a `brokerd` mid-write looks
like, so it is not a failure); or the failure as `<file>:<line>: <what>` and the runbook pointer,
and exit status 1. The two double names are because `bxctl` reads the
files without asking `brokerd`: an approval still waiting and a call still running look the same
on disk as ones a crash cut off.
- `bxctl chat`: on an `approval_pending` event it sends `approvals` on `admin.sock`, finds the
@@ -701,7 +756,12 @@ processes, output size) are M3b's.
on stderr and reads one line from stdin; exactly the id sends `approve`, anything else sends
`refuse`. The id, not `y`, because lines typed while the turn ran are still waiting in stdin,
and `bxctl` cannot discard them without a terminal library: a stray line must never approve.
`--say` and `--json` print the event only. `bxctl chat` gains `--admin-socket`.
`--say` shows the block and does not ask; the owner answers with `bxctl approve` from another
terminal. `--json` prints the event as JSON and nothing else, and never contacts `brokerd`. The
chat lines and the approval's answer are read from one buffered reader on stdin. `bxctl chat`
gains `--admin-socket`. The exact texts of the block, the spans and the one-line failures
(`brokerd` unreachable, an approval expired before the answer, end of input at the question,
which refuses) are fixed in tasks 18 and 20.
- A `tool_denied` event prints `[denied <name>: <reason>]`, and for `grants_invalid`,
`audit_unavailable` and `state_unreadable` the runbook pointer (`grants-invalid`,
`audit-unavailable`, `broker-state-damaged`) on the next line.
@@ -714,7 +774,8 @@ processes, output size) are M3b's.
spelling of the same character, so the printed text is still exactly the arguments and cannot
be forged: a real backslash in a value is already `\\` there.
- **Model text is printed the same way** from M3a: `bxctl chat` applies the same escaping to
reasoning and content, except that newline and tab pass through, and writes `ESC[0m` before an
everything the model wrote (reasoning, content, tool names, and the answer on stdout), except
that newline and tab pass through, and writes `ESC[0m` before an
approval block. Until now it wrote model text to the terminal as it came, and a colour or
conceal sequence in it would have carried into the block that follows.
- The admin socket defaults to `<BOXMAKER_HOME>/run/owner-broker/admin.sock`.
@@ -742,8 +803,12 @@ heading whose text is its anchor (`## grants-invalid`), with five parts: what yo
system refuses, how to confirm, how to fix, and how to check the fix.
Every message for such a state ends with `see docs/runbook.md#<anchor>`. A gate script,
`scripts/check-runbook.sh`, collects every `docs/runbook.md#<anchor>` in `crates/` and fails if
`docs/runbook.md` lacks the heading `## <anchor>`. It has a self-test like the other gate scripts.
`scripts/check-runbook.sh`, collects every `docs/runbook.md#<anchor>` in the `*.rs` files under
`crates/` (tests included, `target/` excluded) and fails if `docs/runbook.md` lacks the heading
`## <anchor>`. An anchor must be written out in the source: a pointer whose anchor the script
cannot read (built with `format!`, or a placeholder in a comment) is an error. It also fails if it
finds no pointer at all, since that means the search is broken. It has a self-test like the other
gate scripts.
## 12. Testing
@@ -769,12 +834,12 @@ implementation, the oracle, or a compiling skeleton) is in section 15.
- **Audit.** The writer: chain across a day boundary, `seq` across files, sync on each record, the
lock refusing a second writer. The tampering suite, each a fixture directory: a changed byte in a
middle line; a deleted line; two lines swapped; a `seq` gap; a file that does not chain from the
one before; a middle line cut short. Each must fail at the right file and line in both
`ChainVerifier` and `brokerd`'s startup. Not failures: a torn tail (startup writes a `Recovery`,
one before; a middle line cut short. Each must fail at the right file and line in `ChainVerifier`, and in
`brokerd`'s startup when the damaged file is the latest (an ordinary start reads only that one). Not failures: a torn tail (startup writes a `Recovery`,
and the next verify reports it); an accepted break (reported by every later verify). Failures:
an `AcceptedBreak` naming the wrong line, or with the wrong `last_good`, `prev` or `seq`; a
`Recovery` whose hash or length does not match the line before it; a line no `Recovery`
describes followed by a torn `Recovery`.
`Recovery` whose hash or length does not match the line before it, or that describes no line; a
line no `Recovery` describes followed by a torn `Recovery`.
- **Audit edges**, each a fixture or a scripted writer test: a torn tail that is complete JSON
lacking only its newline (recovered, and the chain verifies afterwards: this is the case a
"does not parse" rule gets wrong); an unparseable last line that has its newline (recovered