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

Decide where reference implementations are still written

Browse Source 
From M3a: a full reference for the audit chain and the approval
handoff, the property test's oracle for policy, and compiling
skeletons for everything else. Each plan records what its checks
exposed, and that record decides what the next milestone gets.
Tip T17; the spec's handover section says which check each module has.

Also restores three / examples that an editing tool had decoded
to a plain slash.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
This commit is contained in:
kyle
2026-09-18 22:28:53 -07:00
co-authored by Claude Fable 5.1
parent 0ee375dd03
commit 1008dce351
3 changed files with 22 additions and 8 deletions
Download Patch File Download Diff File Expand all files Collapse all files
docs/decisions.md
+2 -1
View File
@@ -6,7 +6,8 @@ Newest first. A decision that changes `docs/design.md` lands in the same commit
| Date | Decision | Reason | | Date | Decision | Reason |
|---|---|---| |---|---|---|
| 2026-09-18 | Spec review of M3a, approvals. The approval block in `bxctl chat` is fetched from `brokerd` by id, never taken from `loopd`'s event. It shows the parsed arguments serialised again, with control, invisible and direction-changing characters as `\uXXXX`. The owner types the approval id, not `y`. `bxctl chat` escapes model text the same way. A `tool_denied` turn event carries the reason to the owner. | A compromised `loopd` must not choose what the owner approves; `/etc` and `/etc` must look alike; U+202E can make a path read as another; a line already waiting in stdin must never approve; `chat` wrote model text raw, so a conceal sequence could hide the block. | | 2026-09-18 | From M3a, a full reference implementation is written only where it still pays: the audit writer and `ChainVerifier` (which also generates the tampering fixtures) and the approval handoff. `policy` is checked by the naive oracle inside its property test. Everything else gets a skeleton: the task's real signatures with `todo!()` bodies, checked to compile against the given tests. Each plan's README records, per task, which check it had and what defect in the spec, task or tests that check exposed; a category that exposes none across a milestone drops a level (reference, skeleton, nothing). Given tests stay for policy, audit and approvals whatever the record says. | In M1 to M2b the reference checked the tasks, not the implementer: it proved tests could pass and signatures compiled (T16), shared the author's blind spots (T5), and caught none of the implementer's defects, which review and probing found. An unsatisfiable test costs one stop-and-report. The tokens are better spent on review. Where a wrong implementation is an authority bypass, the code's author must not also write its acceptance tests. |
| 2026-09-18 | Spec review of M3a, approvals. The approval block in `bxctl chat` is fetched from `brokerd` by id, never taken from `loopd`'s event. It shows the parsed arguments serialised again, with control, invisible and direction-changing characters as `\uXXXX`. The owner types the approval id, not `y`. `bxctl chat` escapes model text the same way. A `tool_denied` turn event carries the reason to the owner. | A compromised `loopd` must not choose what the owner approves; `\u002fetc` and `/etc` must look alike; U+202E can make a path read as another; a line already waiting in stdin must never approve; `chat` wrote model text raw, so a conceal sequence could hide the block. |
| 2026-09-18 | Spec review of M3a, `brokerd` internals. One lock (the ledger) covers the audit writer and the session state files; the pending table has its own, and whoever removes an entry answers it. After any failed audit write, `brokerd` denies with `audit_unavailable` until restarted. `policy` is pure, and `decide` never returns a `Decision` for an `ask` grant: only `redecide` turns an `Ask` into one. A `RunError`'s text is fixed text, never tool output, and a failure does not raise taint. `BrokerPort` waits `[broker] timeout_ms` for a first frame, and until `expires` plus that after a pending one. | Without the lock two results could lower a session's taint. A partial line followed by more records is a broken chain. `loopd` logs failures as `public`, so tool output in one would be unlabelled. | | 2026-09-18 | Spec review of M3a, `brokerd` internals. One lock (the ledger) covers the audit writer and the session state files; the pending table has its own, and whoever removes an entry answers it. After any failed audit write, `brokerd` denies with `audit_unavailable` until restarted. `policy` is pure, and `decide` never returns a `Decision` for an `ask` grant: only `redecide` turns an `Ask` into one. A `RunError`'s text is fixed text, never tool output, and a failure does not raise taint. `BrokerPort` waits `[broker] timeout_ms` for a first frame, and until `expires` plus that after a pending one. | Without the lock two results could lower a session's taint. A partial line followed by more records is a broken chain. `loopd` logs failures as `public`, so tool output in one would be unlabelled. |
| 2026-09-18 | Spec review of M3a, policy. A `deny` grant must have `max_taint = "secret"` or the grant set is invalid. A result's `result_class` and `untrusted` are combined over every matching grant (highest class; untrusted if any says so), and within a mode the grant with the longest matched path wins before the id tie-break. A grant path of `/` is invalid. | A `deny` grant with a lower `max_taint` stopped denying once the session read a secret. With overlapping `auto` grants the id tie-break chose the label, so a secret could come back `private`. M3b mounts grant paths at the same path, where `/` would replace the tool image. | | 2026-09-18 | Spec review of M3a, policy. A `deny` grant must have `max_taint = "secret"` or the grant set is invalid. A result's `result_class` and `untrusted` are combined over every matching grant (highest class; untrusted if any says so), and within a mode the grant with the longest matched path wins before the id tie-break. A grant path of `/` is invalid. | A `deny` grant with a lower `max_taint` stopped denying once the session read a secret. With overlapping `auto` grants the id tie-break chose the label, so a secret could come back `private`. M3b mounts grant paths at the same path, where `/` would replace the tool image. |
| 2026-09-18 | Spec review of M3a, audit. A line followed by a matching `Recovery` is recovered whether or not it parses; an unparseable last line is recovered like a torn one. The writer never moves to an earlier day's file, and `Recovery` and `AcceptedBreak` go in the latest file. `--accept-break` verifies the whole log; the verifier checks an `AcceptedBreak`'s `file`, `line`, `last_good`, `prev` and `seq`, and the `seq` is counted from lines, not read from them. The `Approval` record carries the re-decision's grant and session state. The report lists allowed calls with no `Result`. | As first written, a record cut exactly before its newline made `brokerd` break its own chain; so did a clock stepped back over midnight; a break in an older file could never be accepted; and a damaged line could choose the next `seq`. | | 2026-09-18 | Spec review of M3a, audit. A line followed by a matching `Recovery` is recovered whether or not it parses; an unparseable last line is recovered like a torn one. The writer never moves to an earlier day's file, and `Recovery` and `AcceptedBreak` go in the latest file. `--accept-break` verifies the whole log; the verifier checks an `AcceptedBreak`'s `file`, `line`, `last_good`, `prev` and `seq`, and the `seq` is counted from lines, not read from them. The `Approval` record carries the re-decision's grant and session state. The report lists allowed calls with no `Result`. | As first written, a record cut exactly before its newline made `brokerd` break its own chain; so did a clock stepped back over midnight; a break in an older file could never be accepted; and a damaged line could choose the next `seq`. |
docs/implementer-lessons.md
+1
View File
@@ -49,6 +49,7 @@ How it is used:
| T14 | When a rule has a "before the final frame" or "on every exit" shape, list the exits in the task, or say "including the early returns". The implementer follows the path the task walks through. | M2b finding 1: task 07 walked the success path and the turn's error; the open and create errors were early returns it did not mention. | | T14 | When a rule has a "before the final frame" or "on every exit" shape, list the exits in the task, or say "including the early returns". The implementer follows the path the task walks through. | M2b finding 1: task 07 walked the success path and the turn's error; the open and create errors were early returns it did not mention. |
| T15 | Running the whole plan through `tools/run-plan.sh` worked: ten tasks, one commit each, unattended, in about three hours. Keep the TUI closed while it runs; a second message into the driver's session starts a second agent on the same tree. | M2b run, 2026-09-18. | | T15 | Running the whole plan through `tools/run-plan.sh` worked: ten tasks, one commit each, unattended, in about three hours. Keep the TUI closed while it runs; a second message into the driver's session starts a second agent on the same tree. | M2b run, 2026-09-18. |
| T16 | When a task prescribes the fix, check that it compiles against the types as they are, in the reference tree, before handing it over. A fix that cannot be written as described pushes the implementer outside the listed paths. | M2b task 11: "`unwrap_or_else` with a fixed valid id" had no non-panicking form outside `proto`; the implementer added `Default` to `SessionId` and reported it. | | T16 | When a task prescribes the fix, check that it compiles against the types as they are, in the reference tree, before handing it over. A fix that cannot be written as described pushes the implementer outside the listed paths. | M2b task 11: "`unwrap_or_else` with a fixed valid id" had no non-panicking form outside `proto`; the implementer added `Default` to `SessionId` and reported it. |
| T17 | Match the check to the risk. A full reference for intricate logic whose writing debugs the spec (state machines, concurrency); a naive oracle inside the test for decision logic; a compiling skeleton (`todo!()` bodies under the real signatures) for plumbing. Record what each check exposed, and let the record decide what the next milestone gets. | Across M1 to M2b the references caught no implementer defect. They caught task defects (T16) and missed what they shared with the tests (T5). Decision of 2026-09-18. |
## What worked and should be kept ## What worked and should be kept
docs/specs/2026-09-18-m3a-decision-path.md
+19 -7
View File
@@ -582,7 +582,7 @@ 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 `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.
The owner approves what policy matched: in the raw string `"/etc"` and `"/etc"` look 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 different and mean the same, and the re-serialised form shows both as `/etc`. The audit log keeps
the raw string. the raw string.
@@ -746,8 +746,8 @@ Every message for such a state ends with `see docs/runbook.md#<anchor>`. A gate
## 12. Testing ## 12. Testing
Tests and fixtures are given to the implementer and checked against a reference implementation Tests and fixtures are given to the implementer. How each was checked first (a reference
first, as in M2. implementation, the oracle, or a compiling skeleton) is in section 15.
- **Policy tables.** Every row of every table in section 3 is a case, plus: mode precedence among - **Policy tables.** Every row of every table in section 3 is a case, plus: mode precedence among
three matching grants; the reason order when one candidate is expired and another has too much three matching grants; the reason order when one candidate is expired and another has too much
@@ -814,7 +814,7 @@ first, as in M2.
arrives after `expires` but within `timeout_ms` of it (delivered). The turn loop with arrives after `expires` but within `timeout_ms` of it (delivered). The turn loop with
`approval_pending` and `tool_denied`. `approval_pending` and `tool_denied`.
- **`bxctl`.** `approvals` output with an argument full of escape sequences and one with U+202E, - **`bxctl`.** `approvals` output with an argument full of escape sequences and one with U+202E,
U+200B and U+2066; `/etc` in the request shown as `/etc`; `approve`, `refuse`, U+200B and U+2066; `\u002fetc` in the request shown as `/etc`; `approve`, `refuse`,
`grants check` and `audit verify` against fakes and fixture directories. `chat` against a fake `grants check` and `audit verify` against fakes and fixture directories. `chat` against a fake
`loopd` and a fake `brokerd`: when the event says `read_file` and `brokerd`'s entry says `shell`, `loopd` and a fake `brokerd`: when the event says `read_file` and `brokerd`'s entry says `shell`,
the block says `shell`; the block says `shell`;
@@ -873,6 +873,18 @@ accepts only allowlisted host names refuses other hosts and IP literals.
## 15. How the work is handed over ## 15. How the work is handed over
As in M2: small closed tasks with given tests, driven by `tools/run-plan.sh`, reviewed once after As in M2: small closed tasks with given tests, driven by `tools/run-plan.sh`, reviewed once after
the last M3a task. The reference implementation lives in a git worktree at `~/src/boxmaker-ref` the last M3a task. No task mixes policy with plumbing. Every task that adds a fail-closed path
on an unpushed branch, not in `/tmp`. No task mixes policy with plumbing. Every task that adds a lists its exits and its runbook anchor (tips T14 and T16).
fail-closed path lists its exits and its runbook anchor (tips T14 and T16).
What changes from M2 is how the given tests are checked before they are handed over (decision of
2026-09-18, tip T17):
| Check | Used for | What it proves |
|---|---|---|
| Reference implementation | `proto::audit` (the verifier), `brokerd::audit` (the writer and startup), `brokerd::approvals` | The tests pass, and the spec can be implemented as written. It also generates the tampering fixtures, whose hashes must be real. |
| Oracle | `brokerd::policy`, `args`, `grants` | The property test carries its own naive second implementation. |
| Skeleton | Everything else | The given tests compile against the task's signatures with `todo!()` bodies. |
The reference and the skeletons live in a git worktree at `~/src/boxmaker-ref` on an unpushed
branch, not in `/tmp`. The plan's README records, for each task, which check it had and what that
check exposed.