Task files, the files they copy in (byte-identical to the reference on m3a-ref), each area's check record, and a README with the per-task table of what each check exposed. The handoff note is done with. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
161 lines
11 KiB
Markdown
161 lines
11 KiB
Markdown
# M3a checks, part B: the policy side (tasks 02, 04 to 08)
|
|
|
|
What each task's given tests were checked against before hand-over, and every defect that the
|
|
checking exposed in the spec, the task or the tests. Written for the record that decides how much
|
|
checking the next milestone gets (decision of 2026-09-18, tip T17).
|
|
|
|
**What happened to the plan.** The decision gave `policy` the oracle and `config`, `args`,
|
|
`grants`, `state` a compiling skeleton. All five got a minimal reference implementation instead
|
|
(about 900 lines in all), because the reference for the broker and the approval handoff (tasks 10
|
|
to 15) cannot run without working policy, grants, arguments and state underneath it. So the
|
|
saving the decision expected from these five did not happen in M3a. The record below says what
|
|
the references caught that a skeleton or the oracle would not have, so the next milestone can
|
|
judge: it is very little.
|
|
|
|
| Task | Check it had | Tests | First run against the check |
|
|
|---|---|---|---|
|
|
| 02 proto admin wire | the contract types, run | 30 in four files | 2 failures, both real (below) |
|
|
| 04 config | reference | 7 | all passed |
|
|
| 05 args | reference | 13 | all passed |
|
|
| 06 grants | reference | 17 | all passed |
|
|
| 07 policy | oracle, and a reference | 28 in four files, 7 doctests | all passed |
|
|
| 08 state | reference | 9 | all passed |
|
|
|
|
All of `brokerd`'s suites pass three times in a row and once under four busy loops; clippy with
|
|
`-D warnings` is clean on `brokerd`, `bxctl`, `loopd` and on `proto`'s library and the four test
|
|
files of task 02. `proto/tests/records.rs` does not compile in this worktree: it is task 01's.
|
|
|
|
## Task 02: the contract types, run against the tests
|
|
|
|
1. **Contract defect, real.** `DecisionRecord` accepted unknown fields:
|
|
`{"outcome":"allowed","zz":1}` decoded. serde does not apply `deny_unknown_fields` to the unit
|
|
variants of an internally tagged enum. Found by `strict.rs`, which walks every object of every
|
|
fixture (tip T2), on the first `approve_result` fixture. It affects the audit records of task 01
|
|
as much as the wire. Fixed in the worktree's `proto/src/audit.rs` by decoding through a private
|
|
`RawDecision { outcome, reason: Option<DenyReason> }` with `#[serde(try_from = …)]`; the public
|
|
type, its variants and its JSON are unchanged. A hand-picked test now pins it
|
|
(`an_outcome_rejects_unknown_and_misplaced_fields`). Left over: `{"outcome":"allowed",
|
|
"reason":null}` still decodes, because an absent and a null `Option` look alike to serde.
|
|
**Task 01 must carry this fix**; task 02 checks for it and stops if it is missing.
|
|
2. **Observation, not fixed.** serde's derived `Deserialize` for a struct also accepts a JSON
|
|
array of the fields in order, so `"body":[]` decodes as `Empty` and a four-element array decodes
|
|
as a `ToolRequest`. This has been true of every `proto` struct since M1. It is not an authority
|
|
problem (the values are validated the same way), and closing it means a hand-written
|
|
`Deserialize` for every struct. The test that tried to forbid `"body":[]` was removed. Worth a
|
|
decision, not worth a task now.
|
|
3. **Plan defect.** `strict.rs` is touched by task 01 (the audit fixture's object count changes
|
|
with the nested `event`) and by task 02 (sixteen wire fixtures). Task 02's copy overwrites task
|
|
01's, so the file handed over with task 02 must contain both changes. The version here has only
|
|
task 02's.
|
|
4. Task 02 adds a test the directive did not list: an approval id is a JSON number, and a string
|
|
or a negative number is refused.
|
|
|
|
Neither defect would have been found by a compiling skeleton. Both were found by running the
|
|
tests against real types, which for `proto` costs almost nothing.
|
|
|
|
## Task 04: config
|
|
|
|
- **Spec gap.** The spec shows the socket paths written out under the default home and does not
|
|
say what they are when only `home` is set. Settled as in `loopd`: an empty socket path means
|
|
"under `home`", read through `broker_socket()` and `admin_socket()`.
|
|
- **Repo defect found on the way.** The "Used by" column of `docs/dependencies.md` is stale: it
|
|
names only `proto` for `serde` and `serde_json`, though `loopd` and `bxctl` use both.
|
|
`check-dep-docs.sh` checks crate names only. The task has the implementer add `brokerd`.
|
|
- Test design: the default-home test does not set `BOXMAKER_HOME` (in edition 2024 `set_var` is
|
|
`unsafe`, and it would race); it computes what the default must be in this process.
|
|
- The reference caught nothing. A skeleton would have done.
|
|
|
|
## Task 05: args
|
|
|
|
- **Spec defect.** Section 3 "Hosts" says a URL's host "is a host name as above (so no IP
|
|
literals…)". That does not follow: `127.0.0.1`, `127.1` and `10.0.0.0x1` all fit the host-name
|
|
grammar (labels of `[a-z0-9-]`), and curl normalises each to an IPv4 address. The runbook also
|
|
tells the owner that an IP address in a grant is a problem, which the grammar did not make
|
|
true. Rule added: **the last label starts with a letter `a-z`**. Proposed wording for the spec:
|
|
"…each label 1 to 63 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." Found by writing the
|
|
test table (listing the spellings), not by the reference.
|
|
- **Spec gaps settled in the task:** an absent `cwd` is left out of `canonical_json`, and
|
|
`"cwd": null` means absent; `host` is never in `canonical_json`; `https://example.com?x` is
|
|
invalid because what follows the host must be the end, `:443` or `/`; the root `/` is a valid
|
|
argument path (it is only invalid in a grant).
|
|
- **Tooling.** The editing tool decodes backslash-u escapes in text it writes (the same fault that
|
|
hit the spec). The test that needs the escaped slash builds it from pieces at run time.
|
|
- The reference caught nothing the tests had wrong.
|
|
|
|
## Task 06: grants
|
|
|
|
- **Spec gaps settled in the task:** a missing or unreadable grants directory is a problem, not
|
|
an empty set (I12); an empty directory is a valid empty set; problems come out sorted by file
|
|
name; when `tool` is unknown the constraint table (rule 6) is skipped for that grant; a hidden
|
|
file such as `.toml` has an invalid id; `from_grants` refuses two grants with one id, which
|
|
files cannot produce but the property test's generator could.
|
|
- **Fixture defect, caught before hand-over.** A fixture named `notes-read.toml~` (to prove editor
|
|
backups are ignored) is matched by the owner's global gitignore, so it would never have been
|
|
committed and the implementer's copy would have differed from the plan's. The case now lives in
|
|
a temporary directory the test makes. Rule for fixture authors: run `git check-ignore` on odd
|
|
names.
|
|
- The reference caught nothing: 17 of 17 on the first run, line numbers included. A skeleton would
|
|
have done, at the cost of not knowing that `toml`'s span for an unknown field points at the key.
|
|
|
|
## Task 07: policy
|
|
|
|
- **Spec ambiguity.** "`write_file` … is inside one of the grant's `paths` and is not the grant
|
|
path itself", together with "the longest one is the matched path", does not say what happens
|
|
when a grant lists `/s` and `/s/out` and the call writes `/s/out`. Settled: a grant path equal to
|
|
the argument does not count; the longest path that counts is the matched one, so the write is
|
|
covered through `/s`. Both the reference and the oracle were written to this reading, so neither
|
|
could have caught the other; the ambiguity was found while writing the table test.
|
|
- **Test defect inherited from M1.** The M1 pattern of `compile_fail` doctests loses its teeth
|
|
under the new shape: a struct literal that leaves a field out fails to compile whether or not
|
|
the fields are private, and a call to `Decision::new` fails because there is no `new`. Replaced
|
|
by a literal that names all three fields with `matched: todo!()` (compiles if and only if the
|
|
fields are public) and by trait-bound probes for `Clone` and `DeserializeOwned`. Teeth checked:
|
|
with the fields made `pub`, the literal doctest fails. The task has the implementer repeat that.
|
|
- **Spec gap.** `redecide` returning `Result<Decision, DenyReason>` loses the `deny` grant's id and
|
|
file hash, which the `Approval` record needs. `Denial { reason, grant, grant_sha256 }` carries
|
|
them, for `decide` too.
|
|
- **Scope note for tasks 12 and 13.** Section 12's properties over sequences of calls (taint never
|
|
goes down, every `Result` follows a `Decision`, the runtime sees a call only after `allowed` or
|
|
an approval) cannot be tested in a pure `policy` test. They belong with the ledger and broker.
|
|
So does "one invalid file among valid ones denies a call a valid file would allow": `grants`
|
|
proves the set does not load; the denial with `grants_invalid` is the broker's.
|
|
- **Oracle against reference.** Zero disagreements in 15,000 cases on the first run. That is weak
|
|
evidence by itself, since one author wrote both (T5), so the oracle was tested: six mutants
|
|
of the reference (expiry `>` for `>=`, highest id for lowest, prefix match by bytes, taint `>=`
|
|
for `>`, write allowed at the grant path itself, the `untrusted` label dropped) were each
|
|
caught by the oracle alone, and each also by a table test. **The reference caught nothing the oracle would not have.** Its uses were to show that
|
|
the generator reaches every kind of outcome (each test asserts more than 200 cases of each) and
|
|
to stand under the broker's reference.
|
|
|
|
## Task 08: state
|
|
|
|
- **Spec gaps settled in the task:** a state file that says `public` is treated as damaged (a
|
|
session is never below `private`, so `brokerd` did not write it); `raise` always writes, so the
|
|
file exists from the first result; `raise` trusts the state it is given and does not read
|
|
again, because the caller holds the ledger lock; the file ends with a newline and reads with or
|
|
without one; the directory is made 0700 with its parents, the file 0600.
|
|
- Test design: the write-failure test makes the directory read-only, so it skips itself with a
|
|
message when the user can read a mode 000 file (root). `TempDir`'s `Drop` puts the permissions
|
|
back before removing the directory.
|
|
- The reference caught nothing. A skeleton would have done.
|
|
|
|
## Summary for the process decision
|
|
|
|
| Found by | Defects |
|
|
|---|---|
|
|
| Running real types against the tests (task 02) | 2: `DecisionRecord` accepts unknown fields; the array form |
|
|
| Writing the test tables | 3: IPv4 spellings pass the host grammar; the `write_file` ambiguity; toothless doctests |
|
|
| Writing the task files | 5 spec gaps settled (config sockets, grants directory, `Denial`, state `public`, canonical `cwd`) and the stale dependency table |
|
|
| Preparing fixtures | 1: a fixture name swallowed by a global gitignore |
|
|
| The references for tasks 04 to 08 | 0 |
|
|
| The oracle, against six mutants of the reference | 6 of 6 |
|
|
|
|
For plumbing the skeleton level would have been enough. For `policy` the oracle is enough,
|
|
provided it is mutation-tested once: an oracle that has never failed has not been shown to work.
|
|
|
|
**Resolved at the merge (2026-09-18).** Area A fixed the same `DecisionRecord` hole with empty
|
|
struct variants, `Allowed {}` and `Ask {}`. That fix was kept: it is four lines of derive rather
|
|
than 35 of hand-written decoding, and it also refuses `{"outcome":"allowed","reason":null}`, which
|
|
`admin_wire.rs` now pins. Task 02's "Check first" looks for `Allowed {},`.
|