Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
18 commits
Select commit Hold shift + click to select a range
ccfa79f
test(PMAT-565): RED — the lock file keeps the first writer's version …
noahgift Sep 15, 2026
e4a081e
fix(PMAT-565): the lock names its writer on every write, keeps its cr…
noahgift Sep 15, 2026
ad097fa
docs(PMAT-565): contract, CHANGELOG, lock schema in the book (Refs #565)
noahgift Sep 15, 2026
4f4dc6a
fix(PMAT-565): lock-repair and lock-migrate write through the writer;…
noahgift Sep 15, 2026
fd79253
docs(PMAT-565): the contract stops saying a word gate G reads as gove…
noahgift Sep 15, 2026
7a46a22
docs(PMAT-565): receipt, quorum evidence, estimates row; M1 kills 6 o…
noahgift Sep 15, 2026
58964c5
quorum(PMAT-565): every adjudicated item carries its full claim (Refs…
noahgift Sep 15, 2026
2df49b0
quorum(PMAT-565): committed receipt — 3 lanes, 5 confirmed, 4 refuted…
noahgift Sep 15, 2026
4f20f6d
quorum(PMAT-565): re-bind the receipt after the rebase onto PMAT-564 …
noahgift Sep 15, 2026
b5a0205
quorum(PMAT-565): re-bind the receipt after the rebase onto the rebas…
noahgift Sep 15, 2026
c44400e
quorum(PMAT-565): re-bind the receipt after PMAT-564 merged as d324c5…
noahgift Sep 15, 2026
89c853e
test(PMAT-565): split the planner-proof falsification at 500 lines (R…
noahgift Sep 16, 2026
163aac3
fix(PMAT-565): rebase onto 1.31.0 — one row, and the paragraph under …
noahgift Sep 16, 2026
c324c9a
quorum(PMAT-565): re-bind the receipt after the 1.31.0 cut merged (Re…
noahgift Sep 16, 2026
f265795
fix(PMAT-565): keep this ticket's own row through the rebase (Refs #565)
noahgift Sep 16, 2026
bf4c9fc
quorum(PMAT-565): re-bind after the v1.31.0 booking merged (Refs #565)
noahgift Sep 16, 2026
0a4192c
fix(PMAT-565): three more writers bypassed save_lock — destroy, defra…
noahgift Sep 16, 2026
137cb17
quorum(PMAT-565): the merge-rail round refuted the branch's own every…
noahgift Sep 16, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
132 changes: 132 additions & 0 deletions .quorum/PMAT-565-lock-writer-provenance.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,132 @@
{
"kind": "code",
"issue": "PMAT-565 (forjar#565; paiml/infra#605 third signature) \u2014 four fleet locks under one 1.30.0 binary said generator forjar 1.1.1, 1.13.1, 1.27.0 and 1.10.0 while generated_at rolled; the field was stamped once and never touched. Every StateLock write now stamps the writing binary and keeps the creator; `forjar lock --restamp` converges a state dir in one run.",
"branch": "PMAT-565-lock-writer-provenance",
"base": "cb94fc21",
"base_commit": "583a58eaabddfe24799cea9d143fdbd95b98e8f2",
"diff_sha256": "fe4fd4119e86b66c117f6c260f7e8de9d94c05f4",
"recorded_at": "rebased onto the rebased PMAT-564 (e91639ee) after #571 merged; the diff against main still includes PMAT-564 until #569 merges",
"quorum": {
"lanes": [
"lane 1 \u2014 gemini-3.1-pro-high (lane-1.json, FAIL)",
"lane 2 \u2014 gemini-3.7-flash-high (lane-2.json, PASS)",
"lane 3 \u2014 gemini-3.1-pro-high (lane-3.json, FAIL)",
"merge-rail round, head bf4c9fcd \u2014 lane 1 gemini-3.1-pro-high FAIL with the three-citation finding above (CONFIRMED, fixed in 0a4192cc); lane 2 gemini-3.1-pro-low PASS; lane 3 gemini-3.6-flash-high PASS"
],
"judges": 3,
"refuters_per_claim": 3,
"rounds": "one round of three sandboxed agy quorum lanes against self-contained clones of the PR worktree at a0070731, diffed against the base branch PMAT-564-drift-declines-on-empty-scope, --not-before pinned, out_dir keyed by ticket AND session id; agreed=false (2 FAIL / 1 PASS), partial_reasons recording two lanes sharing a model id \u2014 then a SECOND round on the merge rail, at head bf4c9fcd, which refuted the branch's own 'every write goes through save_lock' clause with three citations and is recorded below",
"kill_rule": "both FAIL lanes' writer-bypass finding was confirmed by reading lock_repair.rs and lock_audit.rs; all three bypassing writes now go through save_lock with a falsifier through the binary; the PASS lane's contrary claim was checked and was wrong; four mutations were run against the committed tree",
"claims_confirmed": 5,
"claims_refuted": 5,
"refuted_claims": [
"That every path writes through save_lock. lock-repair (the minimal lock and the normalised form) and lock-migrate wrote with a bare fs::write, unstamped and with a stale .b3 sidecar; all three go through the writer now, and lock-restore and lock-tag are named as byte copies.",
"That lock --restamp rewrites every lock under a state dir. It walks <machine>/state.lock.yaml one level; nested state dirs, forjar.lock.yaml and .yaml.age are stated as outside it.",
"That no direct serde_yaml_ng + fs::write of a StateLock exists (the one distinct-model lane). It did, at three sites.",
"That the review could not be interrupted without cost. The first dispatch was interrupted by the operator before any lane launched; the round recorded is the re-dispatch.",
"R5: 'every path that writes a StateLock goes through save_lock' \u2014 the branch's own contract clause, refuted by the merge-rail round with three citations: src/cli/destroy.rs:93 (cleanup_succeeded_entries rewrote a pruned lock by hand), src/cli/lock_lifecycle.rs:185 (lock-defrag MIRRORED save_lock instead of calling it, and the mirror never grew the writer stamp) and src/cli/lock_merge.rs:61/70/138 (a bare fs::write with NO .b3 sidecar, so a merged state dir failed the next apply's integrity check). All three call save_lock now; three cases cover them, and the two that drive the binary were RED on the unfixed source in a scratch clone with 'forjar 0.0.0-fake-first-writer' surviving."
],
"lane_errors": [
"two of three lanes shared a model id (gemini-3.8-flash-high was returning 503); recorded by lane-reduce, not refused"
]
},
"falsification": {
"test": "six cases through the writer and the binary: a write stamps the real writer and keeps the creator; the creator is set once and the writer every time; a legacy lock migrates its stale generator into created_by; apply rewrites the writer on a forged legacy lock; lock --restamp converges three locks (dry-run writes nothing, a second run restamps 0, sidecars present); lock-repair writes through the writer, sidecar included",
"test_file": "tests/falsification_lock_names_its_writer.rs",
"cargo_test_target": "falsification_lock_names_its_writer",
"reverted": "four mutations over the COMMITTED tree, each restored from HEAD: M1 (serialise the raw lock in save_lock) kills 6 of 6; M2 (roll created_by on every write) kills the set-once case; M3 (write on --dry-run) kills the restamp case; M4 (bare fs::write in lock-repair) kills the repair case. An earlier draft of the evidence said M1 killed 5 of 6 before it had been run; the number is now the measurement.",
"observed_failure": "5 of 5 RED before the stamp existed \u2014 the file carried the struct's fake first-writer string as its generator, exactly as the fleet's locks carry 1.1.1",
"still_green_when_reverted": "the workspace: 341 targets, 19,796 passed after the repair/migrate change, including every lock_* and state test"
},
"crux": {
"systems": [
"Terraform (state records terraform_version on every write)",
"Nix (immutable generations record what produced them)",
"systemd (unit state rewritten by the running manager; a fleet-wide correction is one command)",
"git (reflog records who moved a ref and when)"
],
"verdict": "accept(Terraform stamps the writing version on every state write; forjar had the field and stamped it once. Adopted the every-write stamp and the kept creator. Not adopted in this release: Terraform's refusal of state written by a newer version \u2014 that is forjar#561's host-resident lock.)"
},
"agy_teamwork": {
"ran": true,
"mode": "one round of three sandboxed agy quorum lanes, review-only, writes=false, mode=plan",
"verdict": "2 FAIL / 1 PASS; both FAILs confirmed and fixed; agreed=false from lane-reduce",
"rounds": 1,
"lanes_per_round": 3,
"writes": false,
"sandbox": true,
"out_dir": "keyed by ticket AND session id"
},
"pmat": {
"ticket": "PMAT-565",
"tools": [
"cargo test --workspace --no-fail-fast (341 targets)",
"cargo clippy --all-targets -D warnings",
"cargo fmt --all -- --check",
"cargo check --all-targets (the 140 literal patches)",
"pv validate contracts/lock-names-its-writer-v1.yaml",
"bash scripts/dogfood/contracts.sh (GATE G)",
"analyze_vacuous_tests",
"PRINT_HASH=1 bash scripts/quorum-gate.sh"
],
"vacuous_tests_in_touched_paths": 0,
"vacuous_scan": "not re-run; every case asserts a value a control would contradict and four mutations were executed. Necessary and not sufficient.",
"bashrs": "not applicable: no .sh file changed",
"quality_gate": "19,796 workspace tests green; clippy, fmt and check clean; gate G PASS",
"tool_defects_found": [
"none new in the review harness this round"
]
},
"evidence": {
"claims_digest": ".quorum/evidence/lock-writer-judges.md",
"total_bytes": 14139,
"files": [
{
"path": ".quorum/evidence/lock-writer-claims.md",
"roles": [
"claims"
],
"bytes": 1863,
"sha256": "6392348c3f0be7806cf455f463e1905e9252229f9afee210792cc5e9d7c24a39",
"blob": "9cddef2e1fcc8b5fd846d0a02bf8adb8611ceed0"
},
{
"path": ".quorum/evidence/lock-writer-lanes.md",
"roles": [
"lanes"
],
"bytes": 2677,
"sha256": "7eb1f5ec03009a3ba8b5afbe0c727297b4ac3d30ecba8dc71bd25d0f714194d9",
"blob": "6c827f60e929a7ee49103025aee6111af485a5ad"
},
{
"path": ".quorum/evidence/lock-writer-judges.md",
"roles": [
"judges",
"crux"
],
"bytes": 6403,
"sha256": "d8fae41bf9ef46eabf4e52fd599f6848a34bd7d07c86fb794de828e0225caac6",
"blob": "77679108ac8c02f1a02c45d9d1fb9bf0f3c030a4"
},
{
"path": ".quorum/evidence/lock-writer-agy.md",
"roles": [
"agy"
],
"bytes": 1128,
"sha256": "7bc2aa2ca2dfb894638d395835c203d3a70554aee405063e8461910538c3f301",
"blob": "edf91ff602879876fc8da9093302ff188e3354c0"
},
{
"path": ".quorum/evidence/lock-writer-pmat.md",
"roles": [
"pmat"
],
"bytes": 2068,
"sha256": "347d7179de39e6bd155f852637eaf713358ac233716047c7ba4d9849c0d76f07",
"blob": "36a792bff31a8af79d9f19967f806542c3006860"
}
]
}
}
23 changes: 23 additions & 0 deletions .quorum/evidence/lock-writer-agy.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
# PMAT-565 — the agy round

lane=quorum width=3 writes=false sandbox=true mode=plan
schema=quorum-lane-schema.json timeout=25m
out_dir=.../paiml-implement/agy/PMAT-565/<session>/ph3
not_before=1789488090 (the dispatch instant)
repo_root=<the PR worktree>, reviewed_commit=a0070731
base for the diff: PMAT-564-drift-declines-on-empty-scope, not main

Composed by the paiml-agy-delegate through `agy-lane.sh --repo-root
<worktree>`; each lane in a self-contained sandbox clone, tree witness
asserted before, byte-identical after, removed. The dispatch-local model
config was named `models.config.json` so `fanout.sh` counted three children,
not four (the PMAT-564 round's edge). No `--concurrent-scope` was declared.
Every lane was briefed NO WRITES and none wrote; no KEPT, no exit 3, no
exit 4. The delegate returned within budget (20 tool uses).

A first dispatch of this round was interrupted by the operator before any
lane launched; the round above is the re-dispatch, with a fresh
`--not-before`.

Result: 2 FAIL / 1 PASS, `agreed=false`. The FAILs were re-executed here and
acted on in adad4e6e.
35 changes: 35 additions & 0 deletions .quorum/evidence/lock-writer-claims.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
# PMAT-565 — the claims put to the round

The branch makes the per-machine lock name the binary that WROTE it, on
every write, and keep the binary that created it: `state::save_lock`
serialises `stamped_for_write(lock)` — `generator` := this binary,
`created_by` := the value replaced, once — and `forjar lock --restamp` walks
a state dir and writes every stale lock through it in one run. Measured
before: four fleet locks under one 1.30.0 binary said 1.1.1, 1.13.1, 1.27.0
and 1.10.0 (paiml/infra#605, third signature).

Three lanes, read-only, sandboxed, against self-contained clones of the PR
worktree at `a0070731`, diffed against the base branch
`PMAT-564-drift-declines-on-empty-scope`, dispatched in one message with
`--not-before` pinned and `out_dir` keyed by ticket AND session id. Models
named in the brief (gemini-3.1-pro-high twice, gemini-3.7-flash-high once;
gemini-3.8-flash-high had 503'd all day).

The questions, identical to every lane:

1. Every writer: is there any path that writes a per-machine lock WITHOUT
`save_lock` — a bare `serde_yaml_ng::to_string` + `fs::write`?
2. `created_by` semantics: a fresh lock, an empty generator, `lock-audit`'s
`starts_with("forjar")`.
3. Compatibility: an older forjar parsing the file; the `.b3` sidecar under
restamp; encrypted `.yaml.age` locks.
4. What `lock --restamp` walks and what it misses — nested state dirs,
`forjar.lock.yaml`, `.yaml.age` — and whether that is stated.
5. The contract, CHANGELOG and book: quote any false sentence; do the
falsifiers' mutations turn their tests red?
6. The 137 scripted `created_by: None` insertions: any misplaced into a
GlobalLock or StackStamp literal?

The acceptance command every lane was told to run:
`falsification_lock_names_its_writer`, `cli::lock_restamp core::state`,
`falsification_contract_citations_resolve`.
108 changes: 108 additions & 0 deletions .quorum/evidence/lock-writer-judges.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,108 @@
# PMAT-565 — adjudicated claims

One round of three sandboxed agy quorum lanes: 2 FAIL, 1 PASS, not agreed.
Five confirmations and four refutations, every one re-measured on this host
before it was acted on. The stamp held; the branch's claim that it sat on the
ONLY writer did not, and the one lane that said so was the one that was wrong.

## CONFIRMED

1. [stamp] That `save_lock` writes the real writer into `generator` whatever
the in-memory struct carried, and moves the value it replaces into
`created_by` exactly once, the first time (all three lanes; lane 1 graded it
measured).
- evidence: `src/core/state/mod.rs:58` — `stamped_for_write` sets
`created_by` only when None, then `generator = writer_stamp()`;
`src/core/state/mod.rs:79` is the write. The fixture at
`tests/falsification_lock_names_its_writer.rs:50` writes a fake first
writer and reads the real one back; mutation M1 (serialise the raw lock)
kills five of six cases.

2. [empty-generator] That a lock whose `generator` is the empty string keeps
`created_by` None rather than recording an empty creator, and that
`lock-audit`'s `starts_with("forjar")` check passes after every write
because the stamped writer always begins with `forjar` (lane 1 measured).
- evidence: the `!out.generator.is_empty()` guard at
`src/core/state/mod.rs:58`; the written generator is always
`forjar <version>`.

3. [compat] That an older forjar parses the file (no `deny_unknown_fields`
on `StateLock`), the `.b3` sidecar stays consistent under restamp, and
encrypted locks are untouched (lanes 1 and 2).
- evidence: `src/core/types/state_types.rs:100` carries serde default
and skip_serializing_if; restamp writes through `save_lock`, which
writes the sidecar, asserted at
`tests/falsification_lock_names_its_writer.rs:213`.

4. [literals] That none of the 140 scripted `created_by: None` insertions
landed inside a GlobalLock or StackStamp literal, both of which also carry a
`generator` line the script keyed on (lanes 1 and 2 spot-checked).
- evidence: neither struct has the field, so a misplacement is a compile
error, and `cargo check --all-targets` is clean.

5. [falsifiers] That each falsifier in `contracts/lock-names-its-writer-v1.yaml`
names a mutation that turns its cited test red — which lanes 1 and 2 reasoned
from the test bodies, and which was run here rather than accepted.
- evidence: M1–M4 in the pmat digest.

## REFUTED

1. [one-writer] That "every path writes through save_lock — apply's
finalize, --refresh, repair, restamp" (this author, in the contract as
first written, and "the one writer every path goes through" in the
CHANGELOG).
- corrected: lanes 1 and 3 read `src/cli/lock_repair.rs` and found the
minimal repaired lock and the normalised form written with a bare
`fs::write`; lane 1 added `lock-migrate`. All three go through the
writer now — `src/cli/lock_repair.rs:44`, `src/cli/lock_repair.rs:106`,
`src/cli/lock_audit.rs:333` — with a falsifier at
`tests/falsification_lock_names_its_writer.rs:298` that also checks the
`.b3` sidecar those paths used to leave stale for the next apply to
refuse on. `lock-restore` and `lock-tag` copy bytes and are named as the
exception in the contract.

2. [restamp-scope] That `forjar lock --restamp` "rewrites every lock under a
state dir", as the CHANGELOG paragraph at `CHANGELOG.md:10` said when this
author first wrote it (lane 1, graded measured).
- corrected: it walks `<state_dir>/<machine>/state.lock.yaml`, one level.
Lane 1 named the three things that leaves out — a nested state dir,
`forjar.lock.yaml` (restamped by every apply through `state::stamp`),
and encrypted `.yaml.age` locks. The CHANGELOG, the book and the
contract now say exactly that; the walk itself is unchanged, because a
nested dir is a state dir of its own and is restamped by naming it.

3. [no-bypass] That "no direct serde_yaml_ng + fs::write exists in src/ for
StateLock" — the claim lane 2, the only lane with a distinct model id,
graded measured and passed the branch on.
- corrected: it did, at the three sites above. The two lanes that shared
a model id found it; the distinct one missed it — the opposite of the
PMAT-564 round, where the two resamples were wrong together. Recorded
because the duplicate-model caveat cuts both ways.

4. [no-writes] That dispatching the review round once was enough and that an
interruption part-way through could not leave a partial round behind (this
author's assumption in dispatching it).
- corrected: the first dispatch was interrupted by the operator before
any lane launched; a second dispatch with a fresh `--not-before` ran the
round. Nothing from the first reached disk; the re-dispatch is the one
the numbers above describe. Named so the receipt's single round is not
read as a single attempt.

5. [fixed-once-means-fixed] That the every-write claim held after the FIRST
round's repair of lock-repair and lock-migrate — the contract clause, the
receipt's verdict and the suite all said so, and all three were wrong about
three more verbs that were rewriting a StateLock by hand.
- evidence: the merge-rail round cited `src/cli/destroy.rs:93`
(`cleanup_succeeded_entries` serialising and writing a pruned lock, then
re-sealing by hand), `src/cli/lock_lifecycle.rs:185` (lock-defrag MIRRORING
save_lock through a local helper that never grew the writer stamp) and
`src/cli/lock_merge.rs:61` with two siblings (a bare write that also
produced NO `.b3` sidecar, so a merged state dir failed the next apply's
integrity check). All three call `save_lock` now and the mirror is deleted.
- corrected: `tests/falsification_lock_names_its_writer.rs:368` and `:404`
drive lock-defrag and lock-merge through the binary and were RED on the
unfixed source in a scratch clone, with `forjar 0.0.0-fake-first-writer`
surviving the rewrite; `cleanup_succeeded_entries_writes_through_the_writer`
covers the third in-crate, since the function is `pub(crate)`. The contract
clause and the receipt verdict now name all five verbs and say which round
found which, because a claim is worth exactly what its cases cover.
Loading
Loading