Conversation
…clone
Remove the last three places a topic's identity or behavior could come from
compiled code or an operator-cloned document rather than from the topic's own
RLM. Data-driven topic_id / install / pin only; the contract is the generic
`harbor-trials-v1`.
(1) Residual tbench/TB4 hardcode
- `proof-results`: `CONTRACT_TBENCH_HARBOR` is now
`CONTRACT_HARBOR_TRIALS_LEGACY` — the *value* stays (it is signed wire data
a live document still pins) but the constant name stops naming a topic.
New topics pin `harbor-trials-v1`.
- Stripped topic names from product comments, CLI help, and the operator
fixture, which is renamed `topic.install-bundle.json` and regenerated with a
neutral slug / custom id / alias. `proof-admin topic validate --bundle
topic.json`, `ctx-client` timeout rationale, `0024` migration comment, and
the bundle crate's alias docs no longer claim an "Owner default" topic.
(2) RLM TopicSetup authors topic behavior; fail-closed without RLM provenance
- The guest `propose_rules` had a fallback that **echoed the operator's signed
checklist** back as a rule proposal while the driver stamped it
`RuleSource::Rlm` — an operator-cloned TopicDocument masquerading as RLM
authorship. That fallback is gone: a runner shipping no `propose_rules`
entrypoint is `Failed` (503, no row, nothing scored).
- New `RlmStore::current_rules_source` / `rlm_authored_rules` (Pg + Memory) and
`proof_topic_install::{rlm_authored_rules, rules_source}` read
`proof_rule_version.source` directly. `TopicSetup::propose_rules` re-reads
the store after writing and refuses with `RulesNotRlmAuthored` unless the
version in force is `rlm`-sourced.
- The publish gate (`PgInstallJournal::applied`) now requires **both** an
`applied` install row and RLM-authored rules, so an `open` document whose
behavior nobody authored is a 409 rather than a live topic.
- `proof-topic-install::install_rules` documents that what it seeds is
`topic_document` provenance — honest, and explicitly not a substitute.
(3) DB/install-driven open + scorable only
- `load_topics` on the **live** backend skips an `open` document it cannot
prove was installed *and* RLM-authored, logging the provenance that blocked
it, instead of admitting it from the operator's file into `open_topics` /
`scorable_topics`. Sim is exempt: it is the CI/local opt-in backend with no
install, no RLM, and no topic VM.
- New repo-wide guard test asserts no topic id (`tbench`, `tb4`,
`terminal-bench`, `harbor-trials`) is compiled into the challenge, gateway,
orchestrator, or guest product branches. Proven non-vacuous: it catches an
injected literal in non-test logic.
Kept: one VM per submission (`VMS_PER_SUBMISSION = 1`, untouched) and the
`custom_ids` / `ready_for_topic` / family-mux wiring.
Gates: fmt, clippy -D warnings, all 5 xtask checks green; `cargo test
--workspace` has zero new failures vs base 870a3b8 (the 4 remaining failures
are pre-existing root-permission tests). `cargo deny` advisories fails
identically on base.
Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
… rules, supersede guard, guard blind spots
P1 — live startup skipped every open topic. `load_topics` ran after the
runtime's `block_on` scopes had returned, so `open_topic_admissible`'s
`Handle::try_current()` failed and each valid open topic was logged as
skipped. The loader is now `async` and driven through `rt.block_on`, and
the gate needs no ambient runtime. A test pins that it is callable from a
synchronous context with no runtime entered.
P1 — the publish gate composed two independent predicates ("newest install
is applied", "newest rule version is rlm"). A topic whose install landed
rule version 1 from the signed document (`topic_document`) was admitted as
soon as any later version was RLM-authored, so it could open with the
operator's vector in force — the exact operator-cloned document the gate
exists to refuse. `proof_topic_install::installed_rules` replaces the pair
with one query joining `proof_rule_version.version =
proof_topic_install.rules_version`, and both the publish route and the
startup gate read it. The join is what binds provenance to the vector in
force.
P1 — setup verified the source of whichever rule version was newest, not
the version it wrote. A concurrent RLM write made the check pass while the
version the baseline is measured against was never verified. It now reads
back the exact version and digest it wrote, and a second guard refuses
before persisting a baseline if a different version is in force (the
measurement is stored per rule version, so a vector that moved under the
run would seal a bar measured under rules nobody scores with).
P2 — the topic-id guard had two blind spots: it omitted
`proof-challenge/src/topic_routes.rs`, and it split on the first
`#[cfg(test)]` marker, dropping all production code after a test-only
method. The strip is now brace-depth based over `mod` items only, the list
covers the challenge's dynamic routes and the VM agent's router, and a
non-vacuous test asserts the guard catches an injected literal, ignores a
`cfg(test)` mod, and still scans production code that follows a test-only
method — the shape in `proof-vm-guest/src/runner.rs` that the old split
stopped guarding.
Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
The install-bound read closed one direction of the provenance defect: a topic whose install landed the signed document's vector while a later version happened to be RLM-authored. The opposite direction was still open. An install lands the RLM's version N, and a later `operator` edit supersedes it as version N+1; a gate that binds only the install's recorded version admits the topic, which then serves rules no RLM wrote. `installed_rules` now reads both halves in one statement — the version the newest `applied` install recorded, and the version in force — and admits only when both are `rlm`-sourced. The new `InstalledRules::SupersededByOperator` names the case so the refusal says which vector is in force. This is deliberately not "the two versions must be equal": an RLM that rewrites its own rules after the install (N → N+1, both `rlm`) is the autonomy this track exists to protect, and it stays admitted. The DB-gated test covers all three transitions: operator edit refused, RLM rewrite admitted, non-`applied` row refused. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
Greptile found the new guard's own blind spot: the stripper counted `{` and
`}` in raw bytes, so a brace inside a `//` comment, a `"…"` literal, an
`r#"…"#` block, or a macro's input left the depth non-zero after a
`#[cfg(test)]` module closed. Every line after it was then dropped from the
scan, and a prohibited topic literal placed there passed the guard.
`mask_non_code` now blanks comments, string bodies (normal, byte, and raw),
and character literals before any depth is computed, keeping byte offsets
and newlines so line-by-line pairing with the original source holds. The
attribute and `mod` markers are read from the masked line too, so a `mod `
inside a string is not mistaken for a module.
A char literal is distinguished from a lifetime (`'a` is code and stays),
and an unbalanced brace in text can no longer end a module early or keep
one open. The regression test drives all four shapes Greptile named, each
followed by production code carrying a literal, and asserts both that the
literal is seen and that the module is still stripped.
Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
The crate-local guards in `proof-rlm`, `proof-experiment`, and
`proof-topic-install` strip test code with
`split("#[cfg(test)]").next()`, which stops at the first marker even when
it annotates a method rather than a module. Their sources are safe today —
each marker starts a trailing `mod tests` — but the strip is the same
shape that hid production code in the guest's `runner.rs`, so a literal
added after such a marker would pass them.
Running those sources through the structural strip here closes that
latent gap without rewriting four crates' tests: the same files are now
scanned by a strip that removes only `#[cfg(test)] mod` items and counts
braces in code rather than in text. Proven non-vacuous by injecting a
literal into `proof-rlm/src/lib.rs`, which the guard now names.
Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
The Rust side already renamed `CONTRACT_TBENCH_HARBOR` to `CONTRACT_HARBOR_TRIALS_LEGACY`, keeping the *value* because it is a signed wire spelling while dropping the topic name from the identifier. The guest adaptor still carried `CONTRACT_TBENCH`, which names a topic the harness does not know. Renamed to `CONTRACT_HARBOR_TRIALS_LEGACY`, matching the Rust constant and its rationale. The string is untouched: a topic signed before the generic id existed pins `tbench-harbor-v1` in its signed `constraints.params.results_contract`, and a signed document cannot be edited. Nothing branches on a topic; the harness accepts both spellings. The deploy gate `assert-harbor-runner-results-emit.sh` asserts the new identifier, and the adaptor suites (148 Python tests, the shell suite) pass. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
The guard covered ten modules chosen by hand. Sixteen more decide what a topic may do and were unguarded: the install executor's engine, routes, section reader, and gate; the guest's fetch and staging; the VM agent's router, auth, hypervisor, and stamp; the gateway's auth, attestation, and proxy paths; and `gateway-core/src/lib.rs`. All thirty-two are now scanned with the structural strip, and the tree is clean for every one of them today — this closes the surface a future edit could put a literal back into. The guard's self-test still asserts it names the file the check was written for and that an injected literal is caught. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
Both docs described the state before this stack shipped the install path, and both were wrong in the same direction: they understated what is enforced. `deploy/guest/runners/README.md` said a runner without a `propose_rules` entrypoint makes the agent propose the signed topic's own `checklist`. That echo was removed: it is exactly how an operator-cloned document gets recorded as `source = rlm`. The guest now refuses the job (Failed → 503, no row, nothing scored), and the row says so. `docs/COMPLETENESS.md` called topic installs a **skeleton** with the real install unimplemented (exit 3) and `enable` / `disable` / `seal` as stubs. All three shipped: `topic install` applies the bundle's RLM section and journals it, `seal` drives `mark_sealed`, and the gate rows live in `0026_proof_topic_gate.sql`. The row now records the three migrations, the mounted dynamic route table, the install-bound provenance gate (both the recorded version and the version in force), and — explicitly — that the six live gates are staged but **not** claimed green. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
Every real topic id is a hyphen slug (`[a-z0-9][a-z0-9-]{1,62}`), and a
bare SQL identifier cannot contain a hyphen. The migration guard required
a literal `{topic_id}_` prefix, so its requirement was **unsatisfiable**:
`CREATE TABLE fixture-topic-v0_scratch` is a syntax error at the first
`-`, and the underscore spelling was refused as unscoped. An operator
running `topic install --drive-rlm` would provision the VM, run the paid
baseline, and only then hit the deny-list — a paid run that could never
publish.
`topic_sql_prefix` maps `-` to `_`, and `is_topic_scoped` accepts that
identifier-safe spelling alongside the literal one. It stays a boundary:
ids contain no underscores, so the mapping is injective and two ids cannot
collide on one prefix. A sibling topic's table, a `topic_*` name, and a
`proof_*` object are all still refused.
The refusal message also claimed `topic_*` was allowed, which the code has
always refused; it now names the prefix that actually works.
This was invisible in CI: the guard's own suite only used `tb4` (no
hyphen), and the tests that would have caught it are DB-gated and CI has
no Postgres. Found by running the DB-gated suites against a real database.
Two `proof-admin` tests that had never executed now pass; one of them also
asserted the topic's alias where the code correctly prints the custom id.
Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
The install-engine suite exercised only `tb4`, which is why the guard's unsatisfiable prefix requirement (fixed in 724ff5b) went unnoticed: `tb4` is both a legal id and a legal bare SQL identifier, so `tb4_scratch` happened to satisfy it. Every real id is a hyphen slug, where it cannot. This test drives the whole path for `fixture-topic-v0`: the migration applies, its table exists in the schema, and a sibling's table, a `topic_*` name, and a `proof_*` object are all still refused — the fix widened the namespace rather than removing it. Proven non-vacuous: with the guard's pre-fix logic restored, the test fails with exactly the LIVE blocker's refusal. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
Greptile found that the literal spelling I documented in 724ff5b is unreachable. `is_topic_scoped` accepts `"fixture-topic-v0_scratch"`, but `tokens` split on every character that is not alphanumeric, `_`, or `.`, so the `-` broke the quoted run into `fixture` / `topic` / `v0_scratch` — none of which is inside the topic's namespace, so a legal quoted name was refused as unscoped. `tokens` now keeps a double-quoted run whole, stripping the quotes (and folding `""` to one literal quote) so the token is the name the database stores and the deny rules match it exactly as before. The SQL-safe underscore spelling always worked; this makes the documented literal one work too. Non-vacuous: with the tokenizer reverted, both new tests fail — the quoted-name test on the refusal, and the escaped-quote test showing the name tokenized as `["a"]`. Quoting remains no escape hatch: a sibling, a `topic_*` name, and a `proof_*` object are all still refused when quoted. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
`topic install --drive-rlm` prints one line and then nothing until the whole
run returns. Provisioning a VM, the RLM's `propose_rules` job, and a paid
baseline can legitimately take hours, so an operator watching a working run
sees exactly the same output as one watching a run that died — and the
first question a stalled run raises ("why are there still 0 rows in
`proof_baseline_measurement`?") cannot be answered from the CLI at all.
`proof-admin topic lifecycle <id>` reads the durable progress: the newest
`proof_lifecycle_event` transition, the rule version in force and its
provenance, whether a baseline exists and under which version, the full
transition history, and what to do next read off the state. Read-only — it
never writes, never moves the lifecycle, and never spends.
The states it names are the ones that actually stall: `provisioning` (the
VM is being created; re-run the same command to resume if no CLI is
attached) and `baselining` with no baseline row (the RLM's `propose_rules`
→ `baseline` jobs run there, and a paid baseline can take hours). A topic
with no transitions is an error that says nothing has driven it, not an
empty success an operator could misread as healthy.
Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
LIVE Gate 1 root cause. `task_slice=tb4-first-5` on a pack whose only slice-ish file was `MANIFEST_FIRST15` (no `slices/`) resolved to nothing, and `select_base` treated that as *informational* when the pack defined no slices — falling through to the next rule and scoring **every** task the pack held. A topic that named 5 tasks was scored on 10, the run overran its 14400 s wall clock, and no baseline was measured at all. The label is the topic's assertion about *which* tasks to score, so the guest must never silently widen it. An unresolved label is now a refusal whether or not the pack defines any other slice, and the refusal names what the pack does define (the labels and their files, or plainly that it has none) plus the two ways forward: name the set with `params.tasks`, or add the slice to the pack. `task_count` is now accepted as a **legacy alias for `n_tasks`**, used only when `n_tasks` is absent (`n_tasks` wins). It is a count, never a selector: it cannot stand in for a slice, so a topic that sets both an unresolvable slice and a count is refused rather than scored on an arbitrary N. Tests: the informational case is replaced by three fail-closed cases (no slices / typo against a pack with slices / never widens to `allow` or the whole pack), plus the `task_count` alias and the property that a count cannot substitute for a slice. Proven non-vacuous: with the old escape restored, 3 tests fail. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
The Python suite pins the rule; the shell suite is what runs the real `proof_filter_tasks` against a real pack, and it only covered a pack that *had* slices. The LIVE failure was a pack with none, so the exact configuration was untested at the layer that ran it. Adds three cases against a pack with no `slices/`: an unresolved label refuses and the refusal says the pack defines no slices; the same pack still scores a set the topic names explicitly (the documented escape); and the run stops before Harbor. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
The durable half of the Gate 1 fix. The guest now refuses an unresolved `task_slice`, which is correct — but a bad selection is then only discovered after provisioning a VM and booting it, and (for a baseline) after paying for the run. `deploy/scripts/proof-slice-preflight.sh` runs the **guest's own** selection on the host in seconds: it execs the adaptor's `filter_tasks.py` with the arguments `lib.sh` passes, so a PASS is the guest's own answer rather than a re-implementation that could drift. It prints `task_slice_resolved`, the kept set, and the source, and asserts the things the Arch PIN asks for: `resolved=true` when a label was set, exactly N selected (`--expect`), and the exact ordered set (`--keep`). A label the pack cannot resolve is a refusal naming what the pack does define. Read-only: it writes to a temp dir it removes and leaves the pack byte-identical (asserted). Also closes a real gap the new tests found: `run-harbor` interpolated `--n-concurrent` / `--n-attempts` straight from the environment, unlike its sibling knobs, so a malformed value fell through to Harbor's default instead of refusing. `proof_harbor_concurrency_flags` validates both and defaults to 1 — a topic that asked for 5 concurrent trials and silently got 1 would take five times as long and could miss the baseline deadline, which is the same shape as the Gate 1 failure. Non-vacuous: with the old interpolation restored, the malformed-value test fails. CI now runs the adaptor Python suite, the adaptor shell suite, the preflight suite, and the harbor results gate. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
Greptile found the lifecycle command's `open` guidance claimed miners could submit. That is only true once the document is **published**: `mark_sealed` records the seal and moves the topic to `open` in the registry, while `--publish` is a separate step. A seal without it leaves the host serving the previous document, so an operator reading "miners can submit" would wait for submissions that can never arrive. The advice now says the seal is recorded, that an unpublished seal leaves the previous document live, how to confirm (the published document, `can_score`), and that re-running `topic seal … --publish` is the retry (the seal is already recorded, so the same document publishes as-is). Two tests pin it: the `open` advice must name `--publish`, say the previous document is still served, and must **not** promise submissions; and each state's advice must match the state (in-flight `provisioning`, an unmeasured `baselining` vs one with a baseline, and `draft`). Non-vacuous: with the old sentence restored, the first test fails. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
Two defects found while driving the LIVE gates. **The preflight could bless a set the guest never runs.** Greptile's open P1: `proof-slice-preflight.sh` forwarded only `tasks` / `exclude` / `n_tasks` / `task_slice`, while `lib.sh`'s `proof_filter_tasks` also passes `task_count` (the legacy alias, only when `n_tasks` is absent), `filter_rel`, `max_duration_s` and `drop_unknown`. On Greptile's own fixture the preflight kept three tasks where the guest kept one — a clean PASS for a run that would have been refused or scored differently. All four are now forwarded with `lib.sh`'s precedence, and the test is no longer a set of hand-written expectations: it sources the adaptor's own `lib.sh`, drives `proof_filter_tasks` the way the guest does, and requires the two to agree on every selector, including Greptile's exact combined case. Non- vacuous: with the four arguments removed, the `task_count` case fails. **A degenerate baseline could be sealed into a permanently dead topic.** Gate 1 measured five Harbor tasks at `primary=0.0` — a reference run that solved nothing. This family scores a *relative* win (`challenger >= bar * (1 + epsilon_rel)`), so a zero bar has no solution: `relative_win` refuses every challenger and the topic would be open, scorable and impossible for every miner to pass. That is a real measurement, not a defect in the seal, so it is refused at the boundary instead of published: - `proof_score::bar_is_degenerate` names the threshold `relative_win` already used (`1e-12`), so the two cannot drift; `family_bar_is_degenerate` scopes it to the relative-win families — `nll` compares absolutely, so a zero bar there stays a hard but meaningful target, and a missing primary stays `EvidenceMissing` rather than being misread as a zero. - `TopicSetup::mark_sealed` refuses with `SetupError::DegenerateBar`, and `proof-admin topic seal` prints the two ways forward (re-run the reference against something that scores, or fix the task selection). - The boot-time baseline file is the other door into the store, so `record_one_baseline` applies the same refusal: a hand-written file cannot install an unwinnable bar either. **No auto-reseal.** The stored measurement is left exactly as the RLM wrote it in both paths; the refusal is the whole behavior. Tests pin that (`a_degenerate_zero_baseline_is_refused_and_nothing_moves` asserts the lifecycle stays `baselining`, the version does not move, and the row is unchanged; `a_baseline_file_cannot_install_a_degenerate_bar` asserts nothing is recorded), and both are non-vacuous — with the guard removed the topic opens at `Open` and the file loads. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
The paragraph claimed all three exit 3 with "not implemented in this slice". They are implemented on this branch: `disable` appends a `disabled` row to `proof_topic_gate` (migration 0026) and `topic_routes` refuses the next submit with the operator's reason, with `enable` as the only way back and `seal` the baseline ceremony. An operator reading the old text would re-sign and re-publish instead of throwing the switch. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
Greptile's open P1, both halves. `mark_sealed` compared the measured primary to the stored row and checked the seal binds to the document, but never asked whether the rules the measurement was taken under are still the ones in force. `baseline` already refuses a vector that moved *while* the run was measuring (`rules_still_in_force`); the store can still be advanced between that write and the operator's seal, so a baseline from rules v1 could open and persist a v2 topic — miners judged by the newer checklist against an older number. `baseline_still_in_force` is that same invariant at seal time, and `SetupError::BaselineStale` names both versions. The lifecycle report had the matching defect: `baselining` recommended "Seal it" from the mere existence of a baseline row, so an operator would walk straight into the refusal. The condition now mirrors the check exactly — the version in force must *equal* the measured one — which also means a measured baseline with **no** rule row in force is stale rather than sealable; the old advice promised a seal there too. Tests, all non-vacuous: - `mark_sealed_refuses_a_measurement_taken_under_superseded_rules` drives the real `mark_sealed` (the wiring, not just the helper) and asserts nothing moves; with the call removed the topic opens at `Open`. - `a_stale_measured_baseline_must_not_seal` pins the helper's contract. - `the_baselining_advice_refuses_to_recommend_sealing_a_stale_baseline` pins the advice, including the no-rules case; with the old condition restored it fails. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
The corrected paragraph said a disabled topic refuses the next submit without saying how, so an operator testing Gate 5 has no expected status to assert. It is **403** with the operator's reason, checked before anything is spent, and a gate that cannot be read is **503** rather than an admission on an unread fact. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
… signed `topic seal` refuses a degenerate bar, which is correct but late: by then the operator has already put the number in an `open` document and signed it. `topic baseline` is the read that happens *before* that, so it now prints `degenerate_bar` in its JSON and a plain warning in the human output, naming the family rule and the two ways forward. The flag and the refusal call the same `proof_score` predicate, so the early read cannot disagree with what the seal will do. `nll` is never flagged: it compares absolutely, so a zero bar there is a hard but meaningful target. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
Owner's Gate 3 failure: no `pf_` row, with the topic VM `tb4-0001` up from the baseline while `tb4-x0004` / `tb4-x0002` died at `ioctl(TUNSETIFF): Device or resource busy` and a 409 `AlreadyExists` when a recreate met the leftover VM. Three defects, all in how a VM takes its TAP and how a create treats one that is already there. **The allocator only knew its own counter.** `net_index` is process-local, but a jailed VM outlives the agent that booted it: the jailer is handed over, not a child of the agent. After a restart — or with a VM an earlier agent left behind, exactly the baseline's `tb4-0001` — the counter starts at zero and names `pfc0`, which is still up. `ip tuntap add` answers `ioctl(TUNSETIFF): Device or resource busy`, so every experiment VM died before its guest ever booted. `NetPlan::first_free` now asks the **host** (`ip -o link show`) for the `pfc<n>` that exist and picks the first free index at or above the counter; `boot_verified` retries on the next free one when two boots race the same index, so the second boot moves on instead of failing. **A failed boot tore down a TAP it never created.** `JailGuard::destroy` unconditionally ran `net.down()` — `nft delete table` plus `ip link del` — so the experiment boot that lost the name to `tb4-0001` deleted `tb4-0001`'s interface and nftables table on its way out. One VM's collision became another VM's outage, and the topic VM the retry would have attached to was gone. The guard now tracks whether **its** boot brought the interface up (`net_brought_up`, set only after `net.up` returns) and releases the network only then; it still always removes its own jail. **`AlreadyExists` hard-failed the submission.** A topic that already has a live VM is not an error — it is the VM the run wants, and an operator should not have to clear the host by hand. `create` now attaches on the agent's 409 and returns that handle, so the submit path is idempotent. Only **topic** specs may attach: an experiment spec asks for a dedicated VM per paid job, and attaching would run the job in the topic's RLM guest, so a 409 there stays an error. The host plumbing (`config`, `shell`, `net`) moves to a new `proof-fc-net` crate, re-exported through `proof-fc-host` so every existing path still works — the fix took `proof-fc-host` past the 1500 non-test LOC cap, and these three modules depend on nothing in the backend. Tests, all non-vacuous (verified by reverting each guard): `a_leftover_topic_vm_does_not_take_the_next_index` and `the_scan_counts_only_pfc_indexes` pin the allocator against a canned `ip -o link show`; `a_guard_that_did_not_create_the_tap_leaves_it_alone` pins the ownership rule; `the_created_vm_must_run_the_pinned_image_and_a_fake_answer_is_refused` now asserts the duplicate create attaches without a second boot; `an_experiment_create_boots_its_own_vm_and_never_attaches` pins the exception. The two boot-failure cases in `a_boot_that_fails_before_the_handshake_releases_its_jail_and_network` now assert per-case ownership: the `ip tuntap` failure must leave the TAP, the `nft -f` failure must release it. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
Both P1s from Greptile's review of `26cb6b15`, both real. **A step after `ip tuntap add` failing leaked the interface.** The guard's ownership flag is set from `NetPlan::up` returning `Ok`, so a failure at `ip addr add`, `ip link set`, or the `sysctl` left the caller believing it owned nothing: cleanup removed the jail and left `pfc<n>` up, holding a name that later boots then allocate around. `up` now rolls the whole plan back itself once the interface exists — the only place that knows it was created and not yet handed over. **The attach fallback did not check what it attached to.** A leftover VM booted from an older image pin, or at another shape or sandbox policy, would have run the submission in a guest the topic does not describe, and its evidence would be evidence about a configuration nobody signed. `create` and `attach` now share one `check_record`, so the topic bind, image digest, vCPU/memory shape, sandbox policy, and VM kind are verified on the created **and** the attached record alike; an incompatible leftover is refused with the reason, and the VM itself is left untouched. Tests, both non-vacuous (verified by reverting each fix): `a_failure_after_the_tap_exists_rolls_the_interface_back` covers all three post-create steps and asserts a taken name is still *not* rolled back; `a_duplicate_create_refuses_an_incompatible_existing_vm` boots a VM under an older pin and asserts the newer run refuses it without booting or reusing anything. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
…r it Gate 4 runs two VMs at once, and the retry path added for Gate 3 is what makes that safe — but nothing exercised it. The recording shell always answers "the name is free", so it can never show a collision, and the counter's race window was untested. `TapNamespace` models the host's TAP namespace: `ip tuntap add` fails with the kernel's own `ioctl(TUNSETIFF): Device or resource busy` when a name is taken, `ip link del` frees it, `ip -o link show` lists what is live, and `rm -rf <jail>` really removes the jail (a shell that only *records* the removal would leave one behind and make a retry fail for a reason a real host never produces). It can also stage the race — a concurrent boot taking an index between this boot's scan and its `ip tuntap add` — and exhaust the pool outright. Three tests: a leftover topic VM holding `pfc0` does not take the next boot off the air (it takes `pfc1`, and its teardown frees only its own TAP); a raced index moves the loser to the next free one, with the failed attempt's jail released in between; and a host with no free TAP refuses after exactly `TAP_ATTEMPTS` attempts instead of spinning. All three are non-vacuous — with the retry loop removed, two of them fail. Writing them found two defects in the fix itself: the counter used `store` where a concurrent boot needs `fetch_max` (a slower boot could move it backwards past an index the faster one had claimed), and `TAP_ATTEMPTS` was documented as retries while the loop counted attempts, so the budget was silently one short. Both are corrected here, with `TAP_ATTEMPTS` now counting attempts (so `1` means "no retry"). Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
Gate 4's OOM. Two 8192 MiB experiment VMs beside the topic's resident 8192 MiB RLM VM on a 16 GiB host with swap=0: the **count** cap (`MAX_EXPERIMENT_VMS=2`) was satisfied, so all three booted, the kernel OOM-killed the guests, and **both** submissions answered 503 with no row. Gate 3 (one topic + one experiment) fits and passes. A count is not a capacity cap. `MemoryBudget` reads `MemTotal` once at boot and refuses a boot that would not fit, with `503 capacity` naming what holds the memory, what was asked for, and the ceiling — so the requests that fit keep running and only the one that does not is refused. Refusing one is strictly better than losing both. Every live VM counts, **the topic's RLM VM included**: it is resident for the topic's whole life and is not free capacity. An experiment-only budget is exactly the mistake the count cap made. Crashed VMs are swept before the check, so they do not hold budget. `PROOF_VM_AGENT_MEMORY_RESERVE_MIB` (default **0**) is the operator's headroom. The default is deliberately 0 so the shape that demonstrably works keeps working — a topic VM beside one experiment VM fills a 16 GiB host exactly, and a non-zero default would refuse Gate 3. Nothing here sizes a VM: the numbers stay the topic's and the operator's, and this only decides whether the host can carry what was asked for. No swap, and no default memory change: a host that cannot fit its own ceiling set is a sizing problem the operator fixes, not one the agent papers over by clamping. `GET /v1/health` now carries `total_mib` / `reserve_mib` / `used_mib`, so an operator reading a `503 capacity` sees what the host thinks it has without reaching for `free`. An older agent omits them and reports 0 rather than a guess. Tests, all non-vacuous (verified by removing the check): the Gate 4 shape is refused before any jail with the numbers in the message; the Gate 3 shape still fits; the guard counts the topic VM rather than experiments alone; the reserve lowers the ceiling; and an unset budget admits everything, so a state built without one behaves exactly as before. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
Greptile's P1 on `f0800353`, and it was the risk that mattered: the guard would have taken the **proven Gate 3 pair** offline. `MemTotal` is the RAM the kernel can hand out, not the RAM the host has. A nominal 16 GiB droplet reports `MemTotal: 16326344 kB` = 15_943 MiB — ~441 MiB the kernel keeps for itself. Comparing guest memory against that figure refused the 8192 MiB experiment VM beside the resident 8192 MiB topic VM on exactly the host where that pair demonstrably passes, so the fix for Gate 4 would have broken Gate 3. `MemoryBudget::from_meminfo` now rounds `MemTotal` up to the whole GiB the host was sold as. That is not an invented tolerance: RAM ships in whole GiB, so this restores the operator's number and nothing more — a nominal 16 GiB host admits the two 8 GiB guests it runs and still refuses Gate 4's third (three 8 GiB guests on a 16 GiB host is the oversubscription that OOM-killed every guest at ~154% of `MemTotal`). A host already reporting a whole GiB is unchanged. The regression test drives `from_meminfo` — the real read path — with Greptile's exact `MemTotal` line, so it fails if the rounding is dropped; a test that built the budget by hand would have passed with the bug in, which is how the first version of it read. Verified non-vacuous: reverting the rounding fails it. A second test pins the raw figure refusing the working shape, so the rounding cannot be dismissed as noise later. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
Checking my own guard for blind spots turned up the boundary that has to be written down, because getting it wrong in either direction breaks a gate that passes today. The guard compares **configured** guest memory against the host's. It is not a residency model, and the sister guest is deliberately outside it: - A paid run on the proven Gate 3 shape is 8 GiB topic + 8 GiB experiment + the 4 GiB **sister** = 20 GiB of configured memory on a 16 GiB host, and it **passes**. Guest RAM is lazily populated — Firecracker maps the region and the guest touches pages as it works — so the configured sum is not the resident set. - The sister is booted by the hypervisor inside a job, so it never enters `state.vms` and never enters the count. Counting it would refuse the Gate 3 shape; that is the same class of mistake as `f0800353`'s raw-`MemTotal` comparison, which Greptile caught taking that shape offline. So the guard is sized to refuse the oversubscription that actually happened (three 8 GiB guests on a 16 GiB host) with margin, not to model the kernel. The doc says so at the function, and `the_guard_is_not_a_residency_model` pins the arithmetic both ways so a later "fix" that sums every guest the host could ever boot fails a test instead of a live gate. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
… shape Arch PIN hardening, points 1 and 2. **The refusal now leads with what is free.** An operator reading a 503 gets `N MiB requested, N MiB free of the N MiB VM ceiling … N MiB is held by M live vm(s) [topic <id> (N MiB), experiment <id> (N MiB)]` and the sentence that says why it refuses at all: keeping the running VMs alive instead of letting the host OOM-kill them. The wording is deliberately distinct from the `MAX_EXPERIMENT_VMS` refusal — a host too small for the shape is not "retry when one finishes" — and a test pins that the two cannot be confused. **The tipped Gate 4 retry shape is pinned.** Owner is tipping staging to `experiment_mem_mib: 4096`, so a 16 GiB host runs the resident 8 GiB topic VM beside **two** 4 GiB experiment VMs: 16,384 MiB, an exact fit, both admitted. That is the retry Gate 4 depends on, so an off-by-one or a non-zero reserve default must fail a test rather than stall the gate — verified non-vacuous: a 1 MiB phantom reserve fails seven tests including this one. The runbook now works the arithmetic through for both 4096 and 8192 asks. PIN 2 (teardown / TAP / `AlreadyExists` idempotency) is unchanged and still covered by the tests from `26cb6b15` / `0c207628` / `e48bcda9`. PIN 3 (park the topic VM before dual eval) is **not** done: `inspect` — the anti-cheat checklist that authorises spend — still runs on the topic VM, so it is not unused. PIN 4 holds: `DEFAULT_MAX_EXPERIMENT_VMS` is still 2. PIN 5: draft, not merged. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
Greptile's P2 on `7095d5a6`. When the ask alone is larger than the whole VM ceiling, "free a vm, retry when one finishes" is a loop that cannot end: nothing freed can make that request fit. The refusal now splits on whether freeing memory can help at all. - `want > ceiling`: the ask is larger than the host's whole VM ceiling, so the refusal says so and names the remedies that can work — a smaller ask or a host whose memory carries it. - otherwise: the normal advice, because freeing a vm genuinely can help. Both are pinned, and the boundary between them is: a request that would fit an empty host keeps the normal advice, so the two cases cannot be conflated in either direction. Non-vacuous — reverting to the single always-free-a-vm sentence fails the test. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
Auditing the RLM-authorship PIN against the code, one requirement does not
hold as the prose reads: **the RLM cannot author a topic's migrations or
APIs.**
The job surface is `VmJob::{ProposeRules, Baseline, Inspect, Evaluate,
Archive}` and the only behavior it can hand back is
`VmJobOutput::Rules(Vec<ChecklistRule>)`. A topic's `migrations` and `apis`
come from the operator's bundle `rlm` section
(`proof-topic-install::SectionPlan`) and are applied by the install. There is
no job that emits them, no wire message that could carry one, and no command
that generates a bundle — an operator writes it.
What *is* RLM-authored is the **rule vector**: `propose_rules` runs inside
the topic VM and its answer becomes the version in force
(`proof_rule_version.source = 'rlm'`), which is the gate an `open` document
must pass. That requirement holds and is enforced in three places
(`propose_rules` read-back, the boot admission gate, and the seal-time
version checks).
So the claim was over-broad, not the code. The prose said the bundle's `rlm`
section (rules / migrations / apis / …) "is handed to the RLM" and called
topics "RLM-owned", which reads as authorship of all five parts. Corrected
in `ARCHITECTURE.md`, `COMPLETENESS.md`, `PROOF.md`, and the bundle crate's
own module doc: the section is *topic-owned data* Rust never interprets, and
**rules** are the part the RLM additionally *authors*.
`the_rlm_authors_rules_and_the_bundle_carries_migrations_and_apis` pins the
boundary structurally — it reads the job/output enums and the section's
parts, and fails if a variant that could carry a migration or an API
appears, so a future change that widens authorship fails a test instead of
silently outdating four documents. Non-vacuous: injecting a `Migrations`
variant into `VmJob` fails it. (The first version of this guard matched only
the tuple spelling `Migrations(`, so the injected struct variant
`Migrations { … }` slipped past it; it matches the name now.)
This is the honest reading of the PIN, not a workaround: nothing here claims
the RLM authors schema or routes, because it does not.
Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
…enylist
Greptile's P2 on `81db11a1`, and it is the right critique: a denylist of
names this test happens to think of cannot hold an authorship boundary. It
demonstrated the bypass concretely — adding `ApplySchema(Vec<SchemaSpec>)`
and `DeployRoutes { routes: Vec<RouteSpec> }` to `VmJob` authors schema and
routes without naming either, and the old guard passed.
The check now enumerates the **whole** permitted surface and fails on
anything else: `enum_variants` reads the top-level variants of `VmJob` and
`VmJobOutput` and asserts the exact lists. A new variant has to be added
deliberately, which is the moment the prose gets updated with it — the
inversion is the point, since the failure mode being guarded is a *silent*
widening.
Non-vacuous against the exact bypass Greptile built: injecting those two
neutral-named variants fails with
`left: [… "ApplySchema", "DeployRoutes" …] right: [ProposeRules … Archive]`.
The extractor is pinned too (both variant shapes, and a missing enum yields
nothing rather than a guess).
Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
The evidence pack for the RLM-authorship DONE criterion, covering all six checklist items with the code path and the command/observed result for each. Two things in it are stated rather than smoothed over: **`pin_policy` does not exist in this tree.** The checklist names it as journal content; there is no such field, column, or parameter (`rg -rni 'pin_policy' .` is empty). What exists is the substance: the pin is global and per-challenge (`config/proof-pin.toml`), and a topic may only tighten a floor (`TopicError::LoosenedFloor`, `crates/proof-task/src/topic.rs`). Reported by name rather than renaming something to match the checklist. **Live staging journal rows are not claimed.** Item 2's evidence is a real Postgres running the real install path (26/26 migrations applied, the DB-gated install-engine suite green, journal fields asserted) — but it is a scratch DB in this container, not cortex-staging. The pack gives Arch the three queries to read the staging rows directly. Also recorded honestly: `cargo deny` fails on RUSTSEC-2026-0285 (`rustls 0.23.43`), which is pre-existing at `6712e7b0` and untouched by this branch; and four test failures in this container are environmental (they assert `0o000` permission denial, which root bypasses — verified identical at `6712e7b0` in a detached worktree). Every cited line number and command output was verified against the tree at `612bdbd1` before committing. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
…fore/after Incorporates Dev's live `cortex-staging` dig and closes the checklist boxes that were still thin. **Live staging evidence (item 2, strongest in the pack):** `proof_rule_version` v5–v7 for `tb4` are all `source=rlm` (v7 `7231a716…`); install #11 is `applied` with `rules_version=7`, `migrations=["0001_scratch"]`, `binding.runner=rlm_fc_in_guest_harbor`, `vms_per_submission=1`, `custom_id=tbench`; `proof_topic_api` holds only `GET status`. **The authorship gap, stated exactly (§2f).** The checklist asks to prove migrations / apis / submission_format / pin_policy are RLM-authored. They are not: the job surface is `VmJob::{ProposeRules, Baseline, Inspect, Evaluate, Archive}` and the only behavior it can return is `VmJobOutput::Rules(Vec<ChecklistRule>)`. There is no variant that carries a migration or a route, and no wire message that could transport one. The pack gives the per-part table (who authors what, where it lands, how it is enforced) and scopes the four things closing it would take. Not started: it changes what the RLM *is*, and the PIN reads as a claim about the system, not a work order. **The live SoT gap (§3e).** B1 FIXED was driven by a human-authored YAML, and the pack says so rather than rounding up. What holds: the host serves what `proof_topic_version` holds, and admits an `open` document only under an `applied` install with RLM-authored rules, so a local YAML has no path to being served on its own. What does not: the document and the schema are the operator's. The honest label is "RLM-ruled, operator-declared". **Before/after inventory (item 4).** `bins/proof-admin/src/main.rs` production literals **6 → 0** across `8e36538a`; the six removed are CLI usage examples and doc-comment examples, now generic (`--bundle <path>`). The one `terminal-bench` left in `bins/proof-admin/tests/cli.rs:1139` is a member of that file's own forbidden-literal guard — the check, not a usage. (An earlier draft of this section said 46 for that file; that was a shell bug in my counting script and is corrected here.) Also corrected: the tip is `e204b426`, and PR #302 now exists for this session's branch — the earlier "pr_url was null" report was accurate, the branch had never been pushed. Every cited line number and number re-verified against the tree at `e204b426` before committing. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
Contributor
Author
RLM-authorship evidence pack (v2)Pack:
RLM-authorship evidence packChecklist: Tip under review:
Verdict summary
The one open authorship gap is item 2, and it is architectural, not a defect: the RLM Item 1 — CLI is trigger-only (no operator topic logic)Claim. Surface (
Evidence — no topic literal anywhere in the CLI's source: Evidence — the bundle is hand-authored input, not generated by any command. There is no Item 2 — TopicSetup journal: what lands, and with what provenanceClaim. An install lands migrations, routes, rules, the submission-format and scoring 2a. The journal schema
2b. The executor binding (the pin-carrying record)
pub handler: String, // allow-listed family ("harbor")
pub runner_id: Option<String>, // the signed document's runner
pub custom_id: String, // the topic's metric.custom_id
pub pack_digest: Option<String>, // the signed document's pack pin
pub vms_per_submission: u32, // always VMS_PER_SUBMISSION (=1, item 5)
pub submission_format_digest: Option<String>,
pub scoring_digest: Option<String>,2c. Provenance: the install seeds
|
| Gate | Path | Refuses |
|---|---|---|
propose_rules read-back |
crates/proof-topic-setup/src/lib.rs:388 |
a version whose source != Rlm or whose digest moved |
| boot admission | bins/proof-challenge/src/main.rs:854 load_topics |
an open doc whose install is not applied or whose rules are not RLM-authored (skipped, logged) |
| seal-time | crates/proof-topic-setup/src/lib.rs:415 + :439 |
a measurement taken under a superseded / no-longer-in-force rule version |
2d. Observed result — live cortex-staging [staging]
Dev's dig on cortex-staging, which is the strongest evidence in this pack because it is the
real host:
| Fact | Value |
|---|---|
proof_rule_version for tb4, versions v5–v7 |
all source=rlm |
| v7 digest | 7231a716… |
| install #11 | applied, bundle sha256:d2429e99… |
└ rules_version |
7 |
└ migrations |
["0001_scratch"] |
└ binding.runner |
rlm_fc_in_guest_harbor |
└ binding.vms_per_submission |
1 |
└ binding.custom_id |
tbench |
proof_topic_api |
only GET status for tb4 |
What this proves. The rule vector in force on staging is RLM-authored, three versions
deep (v5–v7), and the install journal's rules_version matches it (7). The VM pin is 1.
The routes table is live and scoped to the topic.
What it also shows — and this is the gap. migrations = ["0001_scratch"] and
apis = [GET status] are the bundle's section, applied by the install. Nothing in the
journal records an RLM as their author, because nothing can: see §2f.
2e. Observed result — real database, real install path [local-db]
The install engine's suite is DB-gated (crates/proof-topic-install/tests/install_engine.rs:3
— runs when DATABASE_URL names a Postgres). Run here against a real Postgres 18 with
this branch's migrations applied:
$ sqlx migrate run --source crates/db/migrations # applied 26/26
$ DATABASE_URL=postgres://…/proof_authz_evidence cargo test -p proof-topic-install
test result: ok. 15 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out
test result: ok. 7 passed; 0 failed; …
test result: ok. 15 passed; 0 failed; …
test result: ok. 6 passed; 0 failed; …
The journal-recording test
(install_engine.rs:197 a_permitted_bundle_installs_and_the_journal_records_it) asserts the
item-2 fields directly:
report.migrations_applied == ["0001_scratch", "0002_index"] # in bundle order
report.rules_version == 1
report.rule_ids == ["no_short_circuit", "no_holdout_leak"]
report.binding.handler == "harbor"
report.binding.runner_id == Some("operator_adaptor_v0") # the document's runner
report.binding.vms_per_submission == 1
report.binding.submission_format_digest.is_some()
report.binding.scoring_digest.is_some()
report.apis.len() == 2
SELECT to_regclass('tb4_scratch') == "tb4_scratch" # the migration really ran
The scratch DB was dropped after the run. This is a real install path on a real database —
but it is not cortex-staging; §2d is.
2f. The authorship gap, stated exactly
The checklist asks to prove migrations / apis / submission_format / pin_policy are
RLM-authored. They are not. Here is the whole boundary:
| Part | Who authors it | Where it lands | Enforced how |
|---|---|---|---|
| rules | the RLM (propose_rules in its topic VM) |
proof_rule_version.source='rlm' |
three gates: propose_rules read-back (proof-topic-setup/src/lib.rs:388), boot admission (bins/proof-challenge/src/main.rs:854), seal-time version checks (:415, :439) |
migrations |
the operator (bundle rlm section) |
applied by the install; names in proof_topic_install.migrations |
deny-list (proof-topic-sql-guard) before the first statement runs |
apis |
the operator (bundle rlm section) |
proof_topic_api rows |
path/method shape checks; topic-relative paths only |
submission_format |
the operator (bundle) | digest in binding.submission_format_digest |
shape + digest |
scoring |
the operator (bundle) | digest in binding.scoring_digest |
shape + digest |
pin_policy |
does not exist | — | the pin is global (config/proof-pin.toml); topics may only tighten (TopicError::LoosenedFloor, crates/proof-task/src/topic.rs:506) |
Why the RLM cannot author the others today: the job surface is
VmJob::{ProposeRules, Baseline, Inspect, Evaluate, Archive} and the only behavior it can
return is VmJobOutput::Rules(Vec<ChecklistRule>)
(crates/proof-rlm/src/vm.rs:203, :315). There is no variant that carries a migration or
a route, and no wire message (proof-vm-proto::guest) that could transport one. The install
seeds rule version 1 as RuleSource::TopicDocument by design
(crates/proof-topic-install/src/install.rs:493), and says so:
Provenance is the point here. What this seeds is
topic_document… An install therefore
never makes a topic's behavior RLM-authored.
What closing it would require (scoped, not started — it is a real architectural change,
not a doc fix):
- Two new
VmJobOutputvariants (e.g. schema + routes) and the correspondingVmJob
inputs, so the RLM can propose them the way it proposes rules. - A guest-side authorship path: the adaptor would have to emit them from the topic VM, with
the same read-back-and-verify provenance the rule path has. - A new trust story for RLM-written DDL — the deny-list stays, but "the RLM authored
this table" becomes a claim the install must verify rather than assume. - Versioning + supersede semantics matching the rule path (
rules_still_in_forcehas no
analogue for schema), and journal columns recording provenance per part.
I did not do this unasked: it changes what the RLM is, and the PIN reads as a claim about
the system rather than a work order. Say the word and it becomes its own PR.
Item 3 — Source of truth is not an operator clone of legacy tbench
Claim. No human-minted tb4/tbench document is the source of truth; the topic
registry is the database, and the topic's behavior is RLM-authored.
Evidence 3a — no committed topic document. No topic draft (.yaml/.yml) exists
anywhere in the tree, and no committed .json carries "id": "tb4" as a topic document.
The only tb4/tbench JSON is a results fixture
(crates/proof-results/fixtures/harbor-trials-v1.json), which is a wire-shape fixture, not
a topic.
Evidence 3b — the "locked default" prose is gone. Commit 8e36538a ("the bundle owns
topic behavior; the CLI hands it to the RLM") removed the earlier wording that made tb4 /
tbench locked defaults:
- … Locked defaults: first slug `tb4` with temporary alias `tbench` (`proof_topic_alias`), …
- … Locked defaults: first topic slug **`tb4`** with temporary alias **`tbench`** …
Evidence 3c — remaining tb4 references are test fixtures, below #[cfg(test)].
In crates/proof-topic-bundle/src/lib.rs the marker is at line 942; the fixtures
(fn tb4() -> TopicInstallBundle at 983, assert_eq!(plan.topic_id, "tb4") at 1022) are
all after it. In crates/gateway/tests/, crates/proof-rlm-store/tests/, and
crates/proof-topic-install/tests/ they are test code by construction.
Evidence 3d — which topics exist is a DB fact. proof_topic_version +
proof_topic_install; the challenge's load_topics admits only documents whose install is
applied and whose rules are RLM-authored (§2c). On staging, proof_rule_version v5–v7 for
tb4 are all source=rlm [staging] (§2d).
3e. The live SoT gap — B1 FIXED used a human YAML
Dev's dig found the thing that matters: the B1 FIXED run that took Gates 1–6 to GO was
driven by a human-authored YAML topic document. That is not the final authorship SoT, and
this pack does not claim otherwise.
What it means precisely, and what it does not:
| Question | Answer |
|---|---|
| Was the rule vector the RLM's? | Yes — proof_rule_version v5–v7 all source=rlm [staging]. The authorship gate for rules held on the live host. |
| Was the document (statement, metric, constraints, floors, pack pin) the RLM's? | No — an operator wrote it. It is signed by the topic key, so the host trusts it, but a human chose its contents. |
| Does a human YAML have a path to being served? | No, not on its own. The host serves what is in proof_topic_version, and only admits an open document whose install is applied and whose rules are RLM-authored. A local YAML that was never installed and never had rules proposed is not admitted. |
| So is the SoT "operator clone of legacy tbench"? | No — but it is operator-authored, which is one step short of the PIN's intent. |
The honest distinction: the PIN's first clause ("no operator-cloned tb4 as SoT") holds —
nothing in the tree is a clone of the legacy topic, and the host's registry is the DB. The
PIN's deeper intent ("the topic authors itself") is partly met: the rules are the
RLM's, the document and the schema are the operator's.
What would close it: the same work as §2f — the RLM has to be able to propose the parts
of the document that are currently hand-written (at minimum constraints.params, the metric
choice, and the migrations/APIs), with the provenance recorded per part. Until then, a topic
is "RLM-ruled, operator-declared", and the pack should say so rather than round up.
Diff vs a human-minted tb4 YAML: there is no such YAML in this repo to diff
against. The pre-8e36538a prose ("Locked defaults: first slug tb4 with temporary alias
tbench") is the closest thing that existed, and it was documentation of an intended
default, not a document the host read. The live B1 YAML is operator-held on staging, outside
this repo; the check that matters is the one above — the host only serves what
proof_topic_version holds under an applied install with RLM-authored rules.
Item 4 — Residual tbench/tb4 product hardcode: ZERO on tip
Claim. No product branch carries a topic id, benchmark name, or results-contract id.
Guard — crates/proof-topic-bundle/src/lib.rs:1300 no_topic_id_is_compiled_into_the_product_branches scans 32 product modules (challenge,
gateway, orchestrator, guest, bundle, CLI) for
FORBIDDEN_LITERALS = ["tbench", "tb4", "terminal-bench", "terminal bench", "harbor-trials"]
(guard at :1865), using a structural strip that removes test modules and masks non-code
braces (ec13bb4a fixed a brace-counting hole; 7b05a293 closed blind spots Greptile
found).
$ cargo test -p proof-topic-bundle no_topic_id_is_compiled_into_the_product_branches
test result: ok. 1 passed; 0 failed
Before/after inventory. "Production code" below means every line before the file's
first #[cfg(test)]; the pre-strip column is 8e36538a^ (the commit that moved topic
behavior out of product code), the tip column is e204b426.
| Module | Pre-strip | Tip |
|---|---|---|
bins/proof-admin/src/main.rs |
6 | 0 |
crates/proof-challenge/src/topic_routes.rs |
0 | 0 |
crates/proof-challenge/src/lib.rs |
0 | 0 |
crates/proof-challenge/src/emit.rs |
0 | 0 |
crates/gateway-core/src/topic_routes.rs |
0 | 0 |
crates/gateway-core/src/admin_route.rs |
0 | 0 |
crates/gateway-core/src/proxy_paths.rs |
0 | 0 |
The six that were removed from proof-admin's production code were CLI usage examples and
doc-comment examples, e.g.:
62: proof-admin topic validate --bundle tb4.json --pin config/proof-pin.toml
65: proof-admin topic install --bundle tb4.json --env metal --dry-run
171: /// The alias slug (e.g. `tbench`).
173: /// The canonical topic slug it resolves to (e.g. `tb4`).
595: // An alias resolves to its canonical slug first, so `show tbench` finds
596: // `tb4`. Resolution is fail-closed in the store: an alias whose topic has
They are now generic (--bundle <path>), which is the difference between "the CLI knows a
topic" and "the CLI takes one".
bins/proof-admin/tests/cli.rs carries one occurrence of terminal-bench — inside the
CLI's own guard test, as a member of its forbidden list (cli.rs:1139). It is the check,
not a usage.
Whole-tree production-code sweep on the tip (the 32 guarded modules plus the CLI):
$ cargo test -p proof-topic-bundle no_topic_id_is_compiled_into_the_product_branches
test result: ok. 1 passed; 0 failed
Hand grep on the modules with the most historical hits — raw hits vs hits before each
file's first #[cfg(test)]:
| Module | Raw hits | First #[cfg(test)] |
Production-code hits |
|---|---|---|---|
crates/proof-challenge/src/topic_routes.rs |
20 | line 257 | 0 |
crates/gateway-core/src/topic_routes.rs |
12 | line 103 | 0 |
crates/gateway-core/src/admin_route.rs |
1 | line 83 | 0 |
Known remaining occurrences on tip, none of which is a product branch:
| Where | What | Why it stays |
|---|---|---|
crates/proof-results/src/lib.rs:94 |
CONTRACT_HARBOR_TRIALS_LEGACY = "tbench-harbor-v1" |
a wire value: a topic signed before the generic id pins it, and a signed document cannot be edited. proof-results is deliberately not in the guarded 32 because the id is its interface; no guarded module may branch on it |
deploy/guest/runners/…/lib.sh, summarize.py comments |
metal RCA notes (tbench-x0004, x0032, x0039) |
comments recalling which metal run showed a defect |
deploy/guest/runners/…/tests/* |
fixtures | test code |
docs/runbooks/* |
metal RCAs | documentation |
The shipping adaptor has its own genericity guard —
deploy/guest/runners/rlm_fc_in_guest_harbor/tests/test_filter_tasks.py:399 test_no_compiled_task_names_or_modes asserts filter_tasks.py contains none of
first15 / first-15 / shortpack / x0017 / tb4 / duration_hints.
Item 5 — 1 VM per submission, and no product default of max_experiment_vms = 1
Claim. The one-VM-per-submission pin holds, is recorded, and is enforced on the submit
path; the experiment-VM count default is unchanged.
Evidence 5a — the pin.
// crates/proof-topic-install/src/install.rs:79
pub const VMS_PER_SUBMISSION: u32 = 1;Its doc comment states the intent: "the constant is the pin the install records; a future
slice cannot quietly allow a second concurrent VM per submission without changing this value
and the journal rows that carry it." It lands in every install's ExecutorBinding
(:123), and the install engine's own test asserts it
(crates/proof-topic-install/src/lib.rs:147 assert_eq!(VMS_PER_SUBMISSION, 1)).
Evidence 5b — the host refuses a topic installed under a different pin. On the submit
path (crates/proof-http/src/operator.rs:108):
Some(n)withn != 1is refused on the submit path: this build runs one VM per
submission, and a topic installed with a different pin is one it cannot honour.
Evidence 5c — the product default is untouched (checklist item 4 of the Arch PIN):
$ grep -n 'DEFAULT_MAX_EXPERIMENT_VMS: usize' crates/proof-vm-agent/src/router.rs
55:pub const DEFAULT_MAX_EXPERIMENT_VMS: usize = 2;
Still 2. The Gate 4 hardening added a second cap beside it (host memory admission,
f0800353 → dbd26cdd) — it did not replace or lower the count cap.
Item 6 — Tips, checks, and the stacked PRs
Branch tips
| PR | Branch | Tip | Base | Draft | Merge state |
|---|---|---|---|---|---|
| #297 | droid/795020b8-sn100-p0-topics-table-admin |
f298c4d7cfbf |
main |
yes | BLOCKED (branch protection) |
| #298 | droid/9f68584e-sn100-p1a-rlm-topic-install |
b735f3358d3d |
#297 | yes | CLEAN |
| #299 | droid/9822d526-sn100-100-live-gaps-p1b-disa |
37fa0920610c |
#298 | yes | CLEAN |
| #300 | droid/933f76bf-b1-raise-max-proof-deadline |
870a3b875533 |
#299 | yes | CLEAN |
| #301 | droid/2edcb0c8-100-rlm-autonomous-strip-tbe |
e204b426 |
#300 | yes | CLEAN |
| #302 | droid/1d0afa5f-sn100-stay-lit-cont-gate1-pa |
e204b426 |
#300 | yes | CLEAN |
main is aabd1724eb90. The stack is linear: #301 → #300 → #299 → #298 → #297 → main.
#301 is the canonical stack position. #302 is a mirror this session opened so the branch
has its own URL (the earlier "pr_url was null" report was accurate for
droid/1d0afa5f-…, which had never been pushed — it is pushed now, and #302 is its PR).
Both PRs carry the same HEAD; merge #301.
Checks
| PR | CI (ci.yml) |
Greptile |
|---|---|---|
| #297 | SUCCESS (run 34858683718, 5m16s) + CodeQL SUCCESS + Analyze SUCCESS |
SUCCESS |
| #298 | not triggered (base is a droid branch, not main) |
SUCCESS |
| #299 | not triggered | SUCCESS |
| #300 | not triggered | SUCCESS |
| #301 | not triggered | SUCCESS (69 files reviewed, 0 comments) |
| #302 | not triggered (mirror of #301) | see PR |
Why CI runs only on #297: ci.yml triggers on pull_request: branches: [main]. #297 is
the only PR in the stack whose base is main; #298–#301 are stacked on each other, so
GitHub never fires that workflow for them. To compensate, every gate ci.yml runs was
executed locally on the tip — see below.
Local gate run on 612bdbd1 (CI parity)
| Gate | Result |
|---|---|
cargo fmt --all -- --check |
pass |
cargo clippy --workspace --all-targets -- -D warnings |
pass |
cargo test --workspace |
pass (4 pre-existing failures excluded — see caveat) |
cargo run -p xtask -- loc-cap |
pass |
cargo run -p xtask -- consensus-lint |
pass |
cargo run -p xtask -- spec-check |
pass |
cargo run -p xtask -- design-check |
pass |
cargo run -p xtask -- external-docs-check |
pass |
cargo deny check |
advisories FAILED — pre-existing, see caveat |
adaptor suites (python3 -m unittest …, test_adaptor.sh) |
pass |
deploy/scripts/test_proof_slice_preflight.sh |
pass |
Two caveats, stated rather than buried:
cargo deny checkfails onRUSTSEC-2026-0285(rustls 0.23.43, "TLS 1.3 handshake
messages incorrectly accepted across encryption level boundaries"). This is pre-existing
and not introduced by this branch:rustls 0.23.43is the version at6712e7b0and the
lockfile's rustls entry is untouched by these commits. It needs acargo update -p rustls
sweep, which is its own change and touches every crate that depends on rustls. Flagged,
not silently ignored. Note feat(proof): proof-admin install bundle over the existing topic publish path (P0) #297's CI was green when it last ran (2026-09-14), before this
advisory landed in the database.- Four test failures in this container are environmental, not regressions. They fail
identically at pristine6712e7b0(verified by running them in a detached worktree at
that SHA) because they assert on0o000permission denial, which root bypasses — this
container runs as uid 0:
seed_pf_allocator_refuses_boot_when_a_topic_dir_cannot_be_read,
max_zip_numeric_id_fails_closed_when_a_topic_dir_cannot_be_read,
paid_run_fails_closed_when_work_tree_cannot_be_synced,
deadline_cut_still_persists_work_tree. They are excluded from the "pass" above, not
hidden.
Summary
| # | Item | Verdict |
|---|---|---|
| 1 | CLI trigger-only | met — zero topic literals in bins/proof-admin/src; no bundle-generating command; six such literals removed by 8e36538a (before/after in §4) |
| 2 | Journal: rules source=rlm, migrations, proof_topic_api, submission_format, runner |
partly met — rules are RLM-authored on live staging (v5–v7, source=rlm); migrations / apis / submission_format / scoring come from the operator bundle; pin_policy does not exist (§2f gives the exact boundary and what closing it needs) |
| 3 | SoT ≠ operator clone of legacy tbench |
met in code; live gap flagged — B1 FIXED was driven by a human YAML (§3e). The host's SoT is the DB, and an operator YAML has no path to being served without an applied install + RLM-authored rules |
| 4 | Residual product hardcode ZERO | met — proof-admin production literals 6 → 0; 32-module guard passes; hand grep shows 0 hits before every #[cfg(test)]; the legacy tbench-harbor-v1 string is a signed-document wire value, not a branch |
| 5 | 1 VM/submission | met — VMS_PER_SUBMISSION = 1, recorded per install (1 on staging install #11), refused on the submit path when mismatched; DEFAULT_MAX_EXPERIMENT_VMS still 2 |
| 6 | Tips / checks / PRs | given — stack table above; CI fires only on #297 by design, local CI-parity run on the tip |
The open item is 2, and it is architectural. The RLM authors the rule vector — proven
live. It cannot author migrations, APIs, submission-format or scoring, because no job or wire
message carries them (§2f). Closing that changes what the RLM is; it is scoped in §2f and
not started.
Not claimed: that the RLM authors the schema or the routes; that B1's human YAML is the
final authorship SoT; the pin_policy field by that name.
Not merged. PR #301 is a draft; the merge HOLD stands pending Mathis GO.
Contributor
Author
|
@greptileai review — pack v2 ( |
Greptile SummaryThe update adds a registry-aware preflight check for SQL object-name collisions between topics and adds regression coverage for existing registered-topic collisions. Merge safetyNot merge-safe. The existing SQL namespace security issue can still occur when colliding topics are installed concurrently, and the existing VM memory-admission issue still permits an exact nominal-RAM allocation without budgeted host headroom. Confidence Score: 2/5Not merge-safe while the two outstanding existing issues remain. The existing security thread remains outstanding: the registry-aware preflight check rejects collisions only with topics already visible in the registry. Since the topic is published after installation and no lock or durable claim protects the check-and-install interval, concurrent installs of colliding topic IDs can both pass and access the same SQL object. The existing host-memory admission thread also remains outstanding: the code rounds kernel-reported MemTotal upward to the next GiB and uses a zero default reserve, permitting configured VM allocations that exceed reported RAM and reserve no capacity for the host. Files Needing Attention: None. Reviews (2): Last reviewed commit: "fix(proof): close the cross-topic SQL na..." | Re-trigger Greptile |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
| return true; | ||
| } | ||
| bare.starts_with(&format!("{topic}_")) | ||
| bare.starts_with(&format!("{topic}_")) || bare.starts_with(&format!("{sql_topic}_")) |
There was a problem hiding this comment.
The prefix-only check lets the valid topic aa authorize aa_b_scratch through aa_, while the valid sibling topic aa-b uses that same object name through its normalized aa_b_ prefix. The migration gate accepts CREATE, INSERT, and SELECT on this shared name for the shorter topic, so a migration from aa can read, modify, or drop tables belonging to aa-b in the shared database. Use an unambiguous, non-overlapping namespace encoding before merging.
How this was verified: A focused authorization check confirmed that both legal topic IDs pass the migration gate for aa_b_scratch, including cross-topic reads and writes.
Artifacts
- Runs the authored Rust integration test before and after the normalized-prefix commit, showing whether a prefix topic is admitted to a hyphenated sibling's object namespace.
- Captured `cargo test` output from commit 6b89187 shows both `a`/`a-b` and legal `aa`/`aa-b` pairs authorize the same bare object, so the namespace collision predates the PR change.
- Captured `cargo test` output on HEAD shows `is_topic_scoped` and `check_migration` admit CREATE, INSERT, and SELECT across the legal `aa`/`aa-b` boundary, confirming the defect remains.
Comment on lines
+202
to
+208
| pub fn nominal_total_mib(mem_total_mib: u64) -> u64 { | ||
| const GIB: u64 = 1024; | ||
| if mem_total_mib == 0 { | ||
| return 0; | ||
| } | ||
| mem_total_mib.div_ceil(GIB) * GIB | ||
| } |
There was a problem hiding this comment.
The changed admission calculation rounds a kernel-reported 15,943 MiB MemTotal up to 16,384 MiB. With the default zero reserve, it admits one live 8,192 MiB VM plus another 8,192 MiB VM even though their configured total exceeds reported RAM by 441 MiB and leaves no budgeted space for the host OS, agent, Firecracker processes, or guest page faults. If those workloads commit sufficient memory, the host can OOM instead of rejecting the placement. Do not round available memory upward for default admission, or apply a conservative non-zero default reserve before merging.
Artifacts
- Authored and executed script creates isolated probes for the parent of the rounding change and current HEAD, runs the real Rust admission path, captures complete output, and removes temporary source tests; it provides the reproducible comparison.
- Executed Rust probe against the parent of `d809e020` with a 15,943 MiB budget, zero reserve, and 16,384 MiB configured VM total; the admission was refused, showing the prior safe boundary.
- Executed Rust probe at current HEAD using the real `from_meminfo` path with the same meminfo and allocation; it rounded to 16,384 MiB and admitted the request, confirming the default headroom loss.
Greptile's P1 security finding on the tip, reproduced independently before fixing. The migration deny-list namespaces objects by the topic's mapped prefix (`-` → `_`). The mapping is injective, but its **prefixes are not prefix-free**: `aa` and `aa-b` are both legal ids, and `aa_b_scratch` reads as `aa` + `b_scratch` **and** as `aa-b` + `scratch`. Both pass `is_topic_scoped`, so a migration approved for `aa` could create, read, or drop a table belonging to `aa-b` in the shared database. **The per-topic guard cannot fix this.** It sees one topic. Refusing every name with an underscore after the prefix would close the hole but also refuse ordinary names like `tb4_scratch_idx` — including the live shape's own index naming. I implemented that first, watched it break three legitimate tests, and backed it out: the question is about the **registry**, so it belongs where the registry is visible. - `proof_topic_sql_guard::claim_collisions` reports any name another registered topic also claims. - `Installer::refuse_cross_topic_claims` runs it **before the journal opens**, so a collision writes nothing at all — no row, no rule, no table — and refuses with `InstallError::CrossTopicClaim`, naming the migration, the object, and both topics. A store it cannot read is a refusal too: a collision check that cannot enumerate the registry would pass by default. Tests, both non-vacuous (neutering the check fails them): `a_bare_name_two_topics_claim_is_reported_as_a_collision` and `a_name_no_registered_sibling_claims_is_not_a_collision` at the guard, and `a_migration_that_reaches_a_sibling_topics_namespace_is_refused` at the install, which asserts the refusal plus the absence of a journal row and of the colliding table. Also updates the evidence pack with this fix, and records that the pack's `cargo deny` / four-test caveats were re-checked: the four failures are environmental (root bypasses `0o000`), and `cargo deny`'s rustls advisory is pre-existing at `6712e7b0`. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
Contributor
Author
Security fix + pack update —
|
The authorship pin said the RLM must author rules + SQL migrations + dynamic APIs + submission_format + pin_policy. The wire could only carry rules: the job surface was `VmJobOutput::Rules(Vec<ChecklistRule>)`, so the install had to take the other four parts from the operator's bundle. This closes that. **One document, five parts.** `proof-topic-authoring` is the new home of what a topic's RLM authors — the shape, the bounds, the canonical digests, and the tightening rule that makes a pin policy a policy (a topic may raise a floor, lower a ceiling, and never the reverse; three knobs are equalities, not tightenings, because every topic is measured against the same image and machine class). It holds no database and no VM, which is the point: the guest checks an answer before it becomes a job output, and the install checks it again before it applies anything, and both link the same code. **The wire carries the set.** `VmJobOutput::Authored(Box<TopicAuthoring>)` is what `ProposeRules` answers, and `VmJob` carries the set an RLM is re-authoring. `Rules(Vec<ChecklistRule>)` survives for an adaptor baked before the set existed — and it is treated as what it is: a **fragment**. The host records the rules with honest `rlm` provenance and refuses to treat the topic as set up, naming the parts that have no author. It never widens a fragment into a set, because the parts that would fill it are the operator's. **The install applies the RLM's set, and says who wrote what.** When the driver got one, `Installer` applies *it* and not the bundle's section: the declaration of intent is superseded by the topic's own answer. The journal's `binding.authorship` records `rlm` (or `topic_document`) per part, with each part's digest and, for migrations and routes, what landed — so "the RLM authored this topic" is a fact an audit reads back per part rather than a label on the row as a whole. **Fail-closed, three times over.** The guest holds an answer to the deny-list and to the document's own knobs before it answers; the setup driver refuses an incomplete set (`IncompleteAuthoring`, naming the parts) rather than proceeding; the install holds the set to the pin, which the guest cannot see. A migration reaching another topic's namespace, a route inside the admin namespace, a policy that loosens a global floor: each is refused where it arrives. **Two crates moved to make room, unchanged in behavior.** `proof-rlm-lifecycle` (the transition table and owner hooks, out of `proof-rlm`) and `proof-vm-staging` (the staging layer, out of `proof-vm-guest`) — both were at 1494/1495 of the repository's 1500-line per-crate cap, and the authoring surface needs the room. Both are re-exported under their old paths, so no caller changes. Tests: the guest's whole-set path (complete set travels; another topic's set, a denied migration, and an incomplete set are each refused by name; a rules-only answer stays a fragment), and an end-to-end install against a real Postgres where the operator's section and the RLM's set differ in every part, so a run that quietly applied the bundle would fail every assertion. The bundle guard flipped with the code, as its own doc comment said it would. Docs corrected where they claimed the old boundary: `docs/PROOF.md`, `docs/COMPLETENESS.md`, the bundle crate's header, and the guest's. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
…ner run that proves it Rewrites the pack against the tip that closed the authorship gap. **Item 2 is now met in code, and the pack says where it is not yet live.** The gap pack v2 stated exactly (§2f: no job or wire message could carry a migration or a route) is closed: `VmJobOutput::Authored(TopicAuthoring)` carries all five parts, the install applies the RLM's set rather than the bundle's section, and the journal records `binding.authorship` per part with a digest each. §2d keeps Dev's live staging dig as it stands and says plainly that install #11 predates the change — its `migrations`/`apis` came from the bundle and its binding carries no `authorship` entry. §2g is the Owner LIVE run that moves the host onto the new shape, with the exact journal entry that proves it. **Item 3's distinction is stated rather than rounded up.** The RLM authors the topic's **behavior**; the **document** (statement, metric, floors, pack pin) stays the operator's, because miners need a signed document and only the operator holds the `proof` key. §3e is rewritten as a before/after table so the claim is legible, and the B1 FIXED YAML's status is explicit: it cannot produce an `authorship: rlm` row, because an install from a bundle records `topic_document` provenance and the publish gate refuses to open on it. **Item 4's inventory is measured, not asserted.** Two counts per module, both over production code: `raw` (comments included, what a reader greps) and `logic` (comments stripped, what the guard enforces). The earlier pack's "6 → 0" for `proof-admin` is reproduced as raw 6 → 0 / logic 2 → 0, and the two comment-only survivors in `proof-topic-ops` are now 0 raw as well — this tip made those doc examples generic too. **Two new caveats, both about this container rather than the change.** The `rustls` advisory is confirmed pre-existing (the lockfile's rustls entry is untouched; the diff adds only the three new crates), and six failures that appear only with `DATABASE_URL` set are in crates this branch does not touch (`git diff c842598 -- crates/db crates/gateway-store-pg` is empty). **New runbook:** `docs/runbooks/proof-rlm-authorship-install.md` is the Owner ceremony — preconditions, the `authoring.json` contract with every refusal it can produce, the four commands, the journal entry that proves it worked, and the rollback notes. It says explicitly that it is not a re-run of the B1 YAML and why that ceremony cannot satisfy it. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
…guard Both are P1, both reproduced before fixing, and both are in the same check — the one place that can see the whole registry. **1. Function bodies bypassed the collision check.** The check scanned `statement.blanked`, which blanks dollar-quoted bodies *along with* string literals — so object names inside a body were never compared to the registry. Greptile's reproduction: topic `aa` installs `CREATE FUNCTION aa_delete_sibling() … $$ DELETE FROM aa_b_scratch $$ LANGUAGE sql` while sibling `aa-b` is registered, the install completes, and calling the function deletes the sibling's rows. The body is what runs, so the body is what the check reads: `collision_in` scans `blanked` **and** `bodies`. **2. Unpublished installs were invisible, and the check was not atomic.** The check enumerated `proof_topic_version` only, so a topic that had installed but not yet published did not exist as far as it was concerned: `aa` and `aa-b` could both install and both create `aa_b_scratch`. A topic claims a namespace by installing into it, so the claim is read from the **journal** too. And under READ COMMITTED two concurrent installs each see no row from the other and both commit — the same defect with a race on top. Both close in one place. `Installer::claim_namespace` is a single transaction that takes `pg_advisory_xact_lock` (the pattern this repo already uses for the alias slug race), reads the union of `proof_topic_version` and `proof_topic_install`, and writes the `pending` row that records the claim **inside the same transaction** — so the next install to take the lock sees it. A refusal rolls back and writes nothing: no row, no rule, no table. The advisory lock is deliberately coarse — one lock for all installs — because installs are rare operator actions and a per-namespace lock would have to reason about prefix overlap, which is the very thing that is hard here. It is a transaction lock, so a crashed install cannot wedge it. **Tests, each verified non-vacuous.** Neutering the body scan fails `a_function_body_that_reaches_a_sibling_is_refused`; narrowing the registry read back to `proof_topic_version` fails `two_unpublished_installs_cannot_claim_the_same_object`. A third test races two installs and asserts exactly one is refused. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
Greptile's P1 on the whole-set change, and it was right: the wire carried `VmJob::ProposeRules.current` but the driver always sent `None`. An adaptor that cannot read its previous set cannot **retain** the parts it is not changing, so a second authoring run was a rewrite from nothing — and the install would apply that lossy set, silently dropping a migration the topic still needs. Three places, because the set has to be stored, carried, and reachable: 1. **Stored.** `proof_topic_authoring` (migration 0027) keeps every set an RLM authored, versioned and append-only, with the canonical digest beside it. Read from the store rather than held in memory, so a restart — or a different operator process — is handed the same set. The version advances under an advisory lock, so two concurrent authoring runs see each other and report a `VersionGap` rather than racing into a duplicate-key error. 2. **Carried.** `TopicSetup::current_authoring` populates the job's `current`, and a topic with no prior set carries `None` — the first run is unchanged. 3. **Reachable by the adaptor.** The guest writes the previous set to `$PROOF_WORK_DIR/current-authoring.json` and exports its path as `PROOF_CURRENT_AUTHORING_FILE`: always set, empty when there is none, so an adaptor branches on one variable rather than on a variable's presence. **A fragment is not stored as the set in force.** A rules-only answer is persisted as *rules* (honest `rlm` provenance) and **not** as the authored set — storing it would hand the next run a set that was never authored, and the re-authoring path would treat a partial answer as the retention baseline. Tests, each verified non-vacuous: - `a_re_authoring_run_is_handed_the_set_the_first_one_wrote` — first run carries `None`, the set is persisted, the second carries **that** set complete, the store advances to v2. Neutering `current` back to `None` fails it. - `a_rules_only_answer_is_not_persisted_as_the_authored_set` — the fragment path: `IncompleteAuthoring`, no stored set, rules still stored as `rlm`. - `the_previous_set_survives_a_new_driver` — a different `TopicSetup` over the same store is handed the same set, so nothing depends on in-memory state. Docs: the Owner runbook documents the new adaptor input, and the evidence pack and completeness table say what re-authoring now guarantees. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
… the document Two more Greptile P1s on the whole-set change, both reproduced before fixing. **1. A re-install did not remove the routes of the set it replaced.** `register_apis` was insert-only and `proof_topic_api` was `SELECT, INSERT` for the application role, so the table could only grow. When an RLM-authored install superseded a bundle-authored one, the bundle's routes were still there — and the mux loads **every** row for a topic, so a miner could still reach an endpoint the topic's current install does not declare while the journal said the newer set was in force. The install now **reconciles**, in one transaction: it deletes the topic's rows the new set does not claim, upserts the set's rows, and bumps the topic's route revision (migration 0028, which grants the DELETE this needs). The mux's change signal had to change with it: the generation probe was `count(*) FROM proof_topic_api`, and a count cannot see a replacement — delete one, insert one, and it is unchanged while the routes are not. It reads the sum of `proof_topic_route_revision` now: monotonic per topic, bumped in the same transaction as the reconciliation. **2. An accepted pin policy had no effect on scoring.** The check accepted a policy *tighter* than the signed document and the install recorded it, but scoring reads the document (`proof-score::nll_gates` takes `topic.epsilon_nll`; the split-regression gate takes `topic.epsilon_topic_max_regress`). So the host recorded the RLM's tighter number while challengers were judged by the document's — a threshold nobody is scored against, in either direction. `PinPolicy::agrees_with_document` (renamed from `tightens_document`) makes it an **equality**: a policy restates the document — proving its RLM considered the knob — and cannot choose for it. A topic that wants a tighter floor puts it in the document, where it is signed and verifiable. Tests, each verified non-vacuous: - `a_re_install_replaces_the_route_set` — bundle routes, then an RLM set with one different route: only the new route is in the table and the mux answers `NotRegistered` for both old paths. Neutering the delete shows all three, which is exactly the reported bug. - `a_same_count_replacement_still_moves_the_generation` — one route replaced by one route: the count is unchanged, the generation must still move. - `a_pin_policy_restates_the_signed_document_and_cannot_diverge` — restating accepted, diverging refused by name in both directions. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
Greptile's follow-up on the re-authoring fix: the rules went through
`put_rules` and the set through `put_authoring`, two separate store
operations, so a failure between them would leave newer rules with the
**previous** set. A retry would then be handed a set whose rules are not the
ones in force — the two halves of one fact ("this topic's RLM authored *this*
at rule version *N*") disagreeing.
`RlmStore::put_authoring` now takes both and lands them in **one
transaction**:
- Postgres: one `BEGIN`, one advisory lock, the set insert, the rule insert
(with the same version check `put_rules` runs), one `COMMIT`. A vector that
does not advance rolls the set back with it.
- Memory: one lock, the same check, both pushes or neither.
`the_rules_and_the_set_land_in_one_write` pins it: a first run lands both at
v1; a second whose rules do not advance is refused and appends **no** set, so
the set in force stays the one that landed with the rules in force; the next
valid run advances both. `the_atomic_write_still_reports_rlm_provenance`
confirms the provenance read is unchanged.
The fragment path still uses `put_rules`: a rules-only answer is not a set, so
there is nothing to pair it with.
Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
Greptile caught a real bug in the previous commit's Postgres path: `proof_rule_version.digest` is `NOT NULL` and CHECK'd as 64 hex, and the new paired insert omitted it — so **every** complete authoring would have been rejected by the database. The memory store did not, because its `RuleSet` is the object itself; only the real database could say so. The insert now binds `rules.digest()`, exactly as `put_rules` does. **And the contract test now covers it.** `store_contract.rs` runs one contract against both stores, so the paired write is exercised against a real Postgres in CI — which is what makes this class of defect (a column the memory store does not have) a test failure rather than a production surprise. Reverting the digest bind fails it with the not-null violation, verbatim. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
Greptile's last review (of `dc6ca1a4`) scores **5/5**: "Safe to merge; there are no outstanding blocking issues." The pack now carries the finding-to-fix table, so a reader does not have to reconstruct the review history: nine findings across this branch, each fixed in a named commit, each with a regression test that was verified non-vacuous by neutering the fix and watching the test fail. Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Draft mirror of
droid/2edcb0c8-100-rlm-autonomous-strip-tbe(PR #301) at the same HEAD.Canonical stack position: #301. This PR exists so this session's branch has its own URL; the commits are identical.
What this branch carries
Gate 3 (no
pf_) root cause and Gate 4 (host OOM) hardening, the RLM-authorship audit, and the evidence pack:e204b426docs/evidence/rlm-authorship-evidence.md)612bdbd181db11a1dbd26cdd7095d5a63767fe19d809e020f0800353e48bcda90c20762826cb6b15Not for merge. Draft; the merge HOLD stands pending Mathis GO. Merge #301, which is the stack head.