Skip to content

chore(spec): adopt the adjudicated proof→ledger bindings, and correct the stale systemPermissions note - #11209

Merged
os-sam merged 2 commits into
mainfrom
claude/issue-10959-proof-ledger-bindings
Aug 23, 2026
Merged

chore(spec): adopt the adjudicated proof→ledger bindings, and correct the stale systemPermissions note#11209
os-sam merged 2 commits into
mainfrom
claude/issue-10959-proof-ledger-bindings

Conversation

@claude

@claudeclaudeBot commented Aug 23, 2026

Copy link
Copy Markdown
Contributor

Fixes#10959

Executes the spec seat's adjudication recorded as the ACCEPT comment on PR #10934
(issuecomment-5376518715). That PR registered eleven dogfood proof tags and
proposed three ledger bindings without adopting any; this card carries the ledger
edits that were deliberately held out of a registration PR.

⚠️One deviation from the card's acceptance line — see "The delta is six, not five"
below.
Item ③'s conditional fired, so BOUND_PROOF_PATHS moves by six entries rather
than the five the acceptance line anticipated. Adjudicated by the PM seat on review:
keep the six
— the item-③ conditional is the adjudicated clause and the acceptance line
was pre-writing the default branch's outcome. The skip-changeset reasoning below was
reviewed and stands in the same pass.

Premise re-verified on merged main, not on the adjudicated ref

The adjudication was written against 23e27af370. Every binding below was re-verified
against merged origin/main @ 2b5a7ce before it was written. All three proof files
still exist, still declare their @proof: tag exactly once, and still assert what the
adjudication credited them with. No premise died.

showcase-fls-read-mask-strippermission.fields.readable — ADOPTED

Re-confirmed on today's tree: the file authors a scratch permission set carrying
readable: false (line 131) and asserts the runtime outcome both ways on the same
field, row and request
— the key is absent from the wire ('budget' in record is
false at line 172, which toBeUndefined() cannot distinguish from a mask), while the
entitled caller gets the real stored value (lines 185-186, 244).

permission.fields.editable is deliberately NOT bound. Re-read on today's tree, the
file's write-refusal block (lines 280-290) asserts the refusal as a consequence of
unreadability
, not as the write-deny axis — showcase-permission-zoo pins that half.
Binding it would repeat the owner-anchor / allowTransfer mistake: a proof cited for a
property it does not exercise.

showcase-crud-persona-matrix → all four permission.objects.allow* — ADOPTED

The four verbs map one-to-one onto the four entries. Re-confirmed that each is exercised
in both directions per cell and on post-state, not merely on status codes: an allowed
create returns an id and the row is really there / a denied one is 403
PERMISSION_DENIED and persisted nothing (lines 294-309); the allowed edit persisted and
the denied edit changed nothing (337-344); the deleted row is gone and the denied delete
left the row standing (365-372).

The scope worry the registration PR raised — one breadth proof anchoring four properties
— is answered by the file's own shape: the exact allow/deny split is asserted, 54 allow
/ 54 deny
, one verdict per (set × object × verb) (lines 433-462). A narrowing sweep, or
a persona silently failing to provision, breaks the build rather than quietly shrinking
what four entries cite. semantic-roles is the multi-entry precedent (it binds three).

Also re-confirmed the ADR-0090 D5 subtlety the file already handles: cells are judged as a
union with the everyone-baseline set, because capability is additive.

sharing-rule-org-less-callerpermission.systemPermissions — the note was STALE, so: corrected AND bound

The card held this one back pending a measurement, with an explicit conditional: "If it
is stale, correct the note and bind in the same PR; if the note is accurate and the two
really are different consumers, leave the proof unbound."

The measurement says stale, on both halves of the entry.

(a) The evidence pointer does not exist. The entry cited
packages/plugins/plugin-hono-server/src/hono-plugin.ts:1222. That file is 717 lines
long, and a grep for systemPermissions across the whole package finds no hit in it at
all
— the app-entry/nav consumer has moved to current-user-endpoints.ts, where
/auth/me/apps filters on AppSchema.requiredPermissions ⊆ ctx.systemPermissions
(line 897).

(b) The scoping claim is falsified. The note read "PARTIAL — app-entry/nav visibility
only, not a general capability gate."
ADR-0111 D6 (Accepted 2026-07-30, P0
implemented
) makes that false: SharingRuleService.assertCanManageRules
(sharing-rule-service.ts:136) reads context.systemPermissions and refuses every
sharing-rule verb — list and get included — with PERMISSION_DENIED unless the caller
holds manage_sharingor the legacy manage_platform_settings admin override
(sharing-rule-service.ts:139), system contexts bypassing. Its own comment says it is
enforced "HERE, not at the route, so every caller is covered". That is a data-layer
authorization gate, not nav visibility. sharing-plugin.ts:993 carries the same check,
and permission-evaluator.ts:267 (ADR-0066 D3) is the union that puts the authored
capability into the execution context.

The admit set is deliberately named in full in the ledger text (amended in 6dba71b
after PM review — an earlier draft said "without manage_sharing", which over-claimed in
exactly the declared-not-enforced class this card polices). It is wider than one
capability, but every member of it is read from systemPermissions, which is what
this entry classifies — so the binding is unaffected.

The proof measures exactly that, and proves the gate was CLEARED by the authored key.
The file authors system_permissions: ['manage_sharing'] on a permission set (line 123),
then asserts the refusal it gets back names the organization and explicitly does not
match /requires the manage_sharing capability/ (lines 231-233) — which is precisely how
the file knows the capability gate was passed rather than failed. The entitled contrast is
the org-bound holder of the same grant reading its own tenant with 200 (lines 279-290),
over two organizations so a single-tenant fixture cannot pass on the broken build.

So the note was corrected (both the pointer and the claim, with verifiedAt stamped to
today per the gate's own prescribed remedy for a moved consumer) and the binding adopted,
in this PR, exactly as the conditional directs.

The delta is six, not five — flagged, not silently chosen

The dispatch's acceptance line said BOUND_PROOF_PATHS should move by "EXACTLY the
entries of items 1 and 2" (five). Because item ③'s stale branch fired, it moves by six.
The card carries both clauses and they conflict; this PR follows the card's item-③
conditional and flags the tension rather than picking a side quietly. If the reviewer
prefers the binding deferred, dropping item ③ is a self-contained revert of one registry
entry, one ledger proof key and one line in the pin — the note correction should stand
either way, since the old pointer resolves to nothing.

Measured mechanically by importing BOUND_PROOF_PATHS from both revisions:

  • before (2b5a7ce): 20 paths
  • after (07e8615): 26 paths
  • delta: 6 additions, 0 removalspermission/fields.readable,
    permission/objects.allowCreate, permission/objects.allowRead,
    permission/objects.allowEdit, permission/objects.allowDelete,
    permission/systemPermissions

No stale blockedReason is left beside a live binding: all three flipped entries drop
theirs, and the suite's own no bound class is left with an unresolved proof or a blockedReason test passes by name.

Reverse verification — the new bindings are CI-enforced, not decorative

Dropping the proof ref from one newly-bound ledger entry
(permission.objects.allowRead) and re-running the gate:

== post-mutation: proof-ref count (MUST have dropped by exactly 1) ==
3 (pre-mutation: 4)
== git diff proves it landed ==
17	8	packages/spec/liveness/permission.json
== gate under mutation ==
GATE_EXIT=1
✗ 1 high-risk 'live' propert(ies) missing a runtime proof:
permission/objects.allowRead (Persona × CRUD-cell permission matrix) — high-risk
live property requires a proof: expected "packages/qa/dogfood/test/
showcase-crud-persona-matrix.dogfood.test.ts#showcase-crud-persona-matrix"
== RESTORED (trap) ==

Predicted direction before running: RED. Unlike the unregistered-tag channel (a
warning, exit 0), a bound-but-proofless entry is a hard failure — so the exit code is the
readout here, not a warning line. That is what was observed.

The mutation was confirmed on disk before the gate ran — the anchored proof-ref count
went 4 → 3 and git diff --numstat shows the change; an editor's exit code is not evidence
a mutation landed, and the mutation script asserts its anchor matched exactly one line and
aborts the reading as void otherwise. Restore ran from an EXIT INT TERM trap and is
byte-identical (proof-ref count back to 4, git diff --numstat back to 18/8, JSON
re-parses).

No rebuild leg applies.check:liveness runs tsx scripts/liveness/check-liveness.mts,
which imports the registry from source — there is no dist/ between the edit and the
measurement, so the ablation cannot be reading a stale artifact.

Gates — union re-derived and re-run at HEAD 07e8615, ratchets re-run at final HEAD 6dba71b

Union derived with node scripts/pm/dispatch-gates.mjs --repo objectstack-ai/objectstack
(no hand-fed paths — it took the change set from the merge base itself: 3 paths). The
--repo assertion was checked against this checkout's origin and holds. Every exit code
was captured to a file before any pipe. All eighteen re-run green at the final commit:

gateverdict
@objectstack/spec check:liveness0 — the ✓ summary line, "all bound high-risk proofs resolve"
@objectstack/spec check:empty-state0
@objectstack/spec check:strictness-ledger0
@objectstack/spec check:variant-docs0
pnpm check:merge-driver0
pnpm check:slot-lookup0
pnpm check:test-source-alias0
pnpm check:type-source-resolution0
scripts/check-ci-filter-parity.mjs0
scripts/check-dev-prereqs.mjs --self-test0
scripts/check-plugin-teardown-shape.mjs0
scripts/docs-audit/check-affected-docs.mjs0
scripts/check-nul-bytes.mjs0 (plus a direct control-byte scan of all three changed files)
pnpm check:query-options-erasure0 — convention family (this diff edits a test file)
pnpm check:type-check-coverage0 — convention family, the STRUCTURAL half
pnpm check:engine-double-contract0 — convention family
pnpm check:where-matcher0 — convention family
@objectstack/spec typecheck0 across all three legs — tsc --noEmit, check:scripts-typecheck (what compiles the .mts), check:test-typecheck

Plus the affected package, through the shared verify lock and re-run at that same final
commit (the run prints SUITE AT HEAD=07e8615 before it starts):
pnpm --filter @objectstack/spec testTest Files 416 passed (416) /
Tests 11075 passed (11075)
, VERDICT command-exit 0. The @objectstack/spec@17.1.0
banner is echoed in every run above, confirming the filter matched rather than a
zero-match green.

The proof-registry.test.ts file was also run alone under a verbose reporter, so the six
new bindings are visible by name rather than inferred from a suite total — each of
permission.fields.readable, the four permission.objects.allow* and
permission.systemPermissions prints its own carries the … proof and it resolves line,
alongside BOUND_PROOF_PATHS maps the expected entries this phase and no bound class is left with an unresolved proof or a blockedReason.

packages/spec declares no workspace dependencies (pg-connection-string, zod only),
so no dependency-closure build was required.

Declared narrowing, one item.pnpm check:type-check-debt's --re-measure half
was NOT MEASURED locally: it refuses outright on an unbuilt worktree ("56 workspace
dependencies of the ledgered packages have no built type entry point on disk") and its own
message is explicit that this throw means not-measured, never not-applicable. Building the
closure is turbo run build over ~78 packages, which is CI's run. What did run green
covers the risk this diff actually carries: the gate's --self-test half (47 semantic + 59
observation + 29 re-measure + 28 built-closure + 19 auto-lowering cases), the STRUCTURAL
half check:type-check-coverage, and — the one that matters here — check:test-typecheck,
the shrink-only ratchet over packages/spec's own test layer, which reports OK with 55
files / 263 frozen errors held. That is the ledger covering the single test file this diff
edits. Repo-wide pnpm lint was likewise not run locally; it is CI's run.

Changeset — none, and the reasoning is NOT PR #10934's

Re-derived rather than inherited, because this diff differs from that PR's in the way
that mattered to its reasoning
. PR #10934 argued no-changeset on the grounds that its one
changed file lived under scripts/, outside @objectstack/spec's published files set,
and it explicitly noted that the liveness entry in that set is the ledger JSON
directory — "untouched here". This PR does touch it.
packages/spec/liveness/permission.json ships to consumers.

It still releases nothing, for a different reason: the liveness ledger is ADR-0054/#1919
governance metadata about the spec's own verification state — which properties carry a
runtime proof, and what evidence backs each live classification. This diff adds proof
references and corrects one entry's stale note and evidence pointer. No authorable key,
schema, type, export or runtime behaviour changes; an app built on @objectstack/spec
behaves identically before and after. Per AGENTS.md ("Add a changeset for feature work …
Pure bug fixes do not require a changeset") this is neither a feature nor a functional
improvement, so it carries the skip-changeset label instead.

Reviewer: this is the judgment call in this PR most worth a second opinion, since the
published-file half of it is genuinely new relative to the precedent it follows.


Generated by Claude Code


Generated by Claude Code

…t the stale systemPermissions note
Executes the spec seat's adjudication on PR #10934 (issuecomment-5376518715).
Each binding was re-verified against merged origin/main @ 2b5a7ce, not the
23e27af the adjudication was written against.
- showcase-fls-read-mask-strip -> permission.fields.readable (not editable).
- showcase-crud-persona-matrix -> all four permission.objects.allow* verbs.
- sharing-rule-org-less-caller -> permission.systemPermissions, whose ledger
note turned out STALE on re-verification, so it is corrected here and the
binding adopted in the same PR, per the ruling's own conditional.
BOUND_PROOF_PATHS moves 20 -> 26: six additions, no removals.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RadETjNRLALFLhFA3xehZP
@claudeclaudeBot added the skip-changeset PR has no user-facing published change; bypasses the changeset gate label Aug 23, 2026
@github-actions

Copy link
Copy Markdown
Contributor

📓 Docs Drift Check

Nothing in this diff resolved to a documentable surface (no symbol, route or SDK anchor derived from 1 changed package(s)), so this run has no opinion about the docs.

What this run could not see
  • 1 changed file(s) yielded no anchor (packages/spec/liveness/permission.json) — pages documenting those are invisible to this run

Coarse fallback — 126 page(s) merely mention a changed package (the pre-#9192 predicate, kept for the deliberately-wide backstop): node scripts/docs-audit/affected-docs.mjs --json 9cc1940a11e1805fc88a1fb943ec41529d2f0b9bpackageMentionDocs.

…Permissions citation
PM review of PR #11209: the new evidence/note text said the sharing-rule
surface "refuses without manage_sharing", but assertCanManageRules
(sharing-rule-service.ts:139) admits `manage_sharing` OR the legacy
`manage_platform_settings` admin override, and bypasses for system
contexts. Over-claiming an admit set is the declared-not-enforced class
this card polices, so the three sites carrying the claim now name it.
The classification is unchanged: every member of the admit set is read
from `systemPermissions`, which is what the bound entry classifies.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RadETjNRLALFLhFA3xehZP
@os-sam
os-sam marked this pull request as ready for review August 23, 2026 03:59
@os-sam
os-sam added this pull request to the merge queueAug 23, 2026
Merged via the queue into main with commit de6e2bfAug 23, 2026
36 checks passed
@os-sam
os-sam deleted the claude/issue-10959-proof-ledger-bindings branch August 23, 2026 04:15
os-steve pushed a commit that referenced this pull request Aug 23, 2026
check:liveness resolved a `path/to/file.ts:NNN` pointer with existsSync on
the path alone. The parser did not even retain the `:NNN` — bareToken()
stripped it before classification — so nothing downstream could bound it.
A consumer that moved out of a file which still EXISTS therefore kept a
passing pointer, was counted under the word "resolved", and left its entry
reading as freshly verified.
That is worse than a missing file: a dead citation with a precise line
survives review because it looks measured, and the next agent re-verifying
the entry follows it, finds nothing, and rebuilds the call graph by hand.
- evidence.mts retains the line (`localCitations`, deduped on path:line so a
file cited at three call sites contributes three), and `checkCitationLines`
bounds each one. A range `:12-34` is bounded by its END — a tail past EOF
overruns the file even when its head is inside.
- The bound is a separate function, not a third parameter on checkEvidence:
an optional parameter a caller omits is a silent opt-out, and
empty-state.mts shares that resolver without having measured its own
citations this way.
- check-liveness.mts applies it to `producer` as well as `evidence` — those
already share one resolver by decision (#4837), and a standard applied to
one and not the other leaves the weaker one as the place a rotted line
hides. Zero producer violations today; the hole is closed before it opens.
- The run prints citations checked beside citations in range, the #5623
two-number discipline: printing only the second reads as a pass on a run
where the parser extracted nothing.
Two shipped instances, both repaired, both measured:
- permission.tabPermissions cited hono-plugin.ts:1200 in a 717-line file with
zero `tabPermissions` occurrences. All THREE of its pointers were dead —
one past EOF, and resolve-execution-context.ts:205 / rest-server.ts:1551
within bounds with zero occurrences each. Repointed at the real consumers
in current-user-endpoints.ts (the /me/apps rank merge and hidden-drop, and
the /auth/me/permissions projection) plus the resolution chain, verifiedAt
stamped. Same code movement that #11209 repaired for the sibling entry.
- mapping.fieldMapping cited :115-167 of a 164-line file. The consumer never
moved; the file shrank under the citation.
Part of #11210
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01T9cDbY2NBiVJWYx3BpWfH2
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Labels

size/mskip-changesetPR has no user-facing published change; bypasses the changeset gateteststooling

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Adopt the adjudicated proof→ledger bindings from #10773 (two bind now, one blocked on a stale note)

2 participants

@os-sam@claude