[AAASM-5529] ✅ (test): Bind quick-start enforcement claims to their proving controls - #317
Merged
Merged
Conversation
…proves it docs/quick-start.md §"What just happened" carries the Python quick-start's enforcement claims, and nothing connected them to the negative controls. A claim could be added, reworded, or left standing after the behaviour beneath it changed, and no gate would notice. Each claim is now bound to the controls that prove it. The claim list is parsed from the document and the control names are extracted from the negative-control module's AST, so neither side is a transcribed constant checking another transcribed constant: adding a claim, rewording one, renaming a control, or renaming the exception the document names each fail here. Claim 1 is registered as deliberately unproven, naming AAASM-5661. Every control installs a fake native core that the documented configuration does not have, so binding it to one would launder that gap into evidence. The SDK symbols a claim names are resolved lazily rather than imported at module scope. Imported at module scope, a rename becomes a collection error that aborts before the assertion meant to catch it can run — the same inverted-order defect the round-1 review of this ticket found in all three SDKs. Refs AAASM-5529
ci.yaml's paths allow-list excludes docs/**, so a PR that only rewords a quick-start claim gets no CI at all — which is exactly the change the claim-binding gate exists to catch. quickstart-tabs-check.yml already triggers on docs/quick-start.md, so the gate runs there. The negative-control module and the exceptions package are added to the trigger paths as well. ci.yaml already covers both under test/**/*.py and agent_assembly/**/*.py; the entries here are what make a renamed control or a renamed exception re-run this workflow too. What the two jobs prove is deliberately different, and neither covers the other: drift-check round-trips the §3 tabs as text and never parses, imports or executes a snippet; claim-bindings gates the prose claims in §"What just happened" against named controls. Refs AAASM-5529
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
…ts in a region Review found the central promise breaks in under a minute. Three defects, all in this file: F1 — the gate asked whether the region CONTAINED a binding's quote, so a sentence could carry unlimited extra unbound claims as long as one fragment survived. Python bound at list-item granularity, so an appended sentence rode free. Quotes are now whole sentences compared with ==, and exactly one binding may match a sentence. F6 — only two regions were scanned, so claims elsewhere were invisible. Notably "the other modes add network/kernel interception" at the foot of the page, which is a named acceptance check of this very ticket. The scan now covers the whole document minus two named allow-lists, each entry carrying a reason. An allow-listed sentence must still be present verbatim, so an entry cannot silently cover a reworded claim. F4 — kind=LIFECYCLE was an unchecked one-word bypass: relabel a claim, drop its controls, no ticket needed, green. It was also already live in-tree, on a binding whose unproven_reason named no ticket. The field is removed rather than fixed; every claim now needs controls or a ticketed reason. F5 — the vocabulary was three alternatives, so a claim phrased around them was not treated as a claim. Widened to match the Go gate's, plus throws, routed, intercepts, governed, verified, protection and bypass. Refs AAASM-5529
Replacing a fenced block with a space glued the sentence before a code sample to the sentence after it. Measured on this document: 18 such pairs. A glued pair is fragment containment one level up — a binding quoting it would cover two claims at once, and the second could then be reworded or negated without the gate noticing. Found while fixing the same bug in the Go and Node gates, then checked for here rather than assumed absent. No binding changed: none of the 18 pairs carries enforcement vocabulary today. The hole was latent, not live. Refs AAASM-5529
Node's four Windows CI legs failed the equivalent gate: git checks the doc out with CRLF, so the paragraph split never fires and the section collapses into one "sentence" that matches no binding. This repo's CI is Linux-only, so the bug is latent here rather than live. Normalised anyway — a gate whose result depends on the checkout's line endings is not a gate. Verified against a CRLF copy of the document. Refs AAASM-5529
…no keyword filter
Review appended three plain sentences to the quick-start, the last of them
"Tool bodies always execute; the policy result is recorded alongside them" —
the negation of the product — and this gate stayed green. None of the three
used any of the 21 vocabulary terms. Widening 3 -> 21 closed the instance,
not the class: a keyword allow-list cannot be completed, because whoever
adds the claim picks the words after reading the list.
R1 — the vocabulary no longer gates anything. Every one of the document's 88
sentences must be bound to a control or allow-listed by exact text. The
vocabulary survives as a severity hint in the failure message, and as the
trigger for a stricter allow-list rule: waving through a sentence that reads
like a claim costs a written justification, not a category.
R3 — section exclusions are gone. An excluded section was a black hole: the
guard checked the heading still existed and said nothing about its contents,
so a claim inserted into "## Next steps" was never scanned. A positive
control now asserts that section is in the scan.
R4 — HTML and MDX comments are stripped, as fences already were, and for the
same reason: a reader cannot see them. Leaving them in let a bound claim be
commented out of the rendered page while the gate still counted it.
R5 — an unproven_reason may no longer name AAASM-5529, the ticket this
module implements. The mode=auto registration did, and would have resolved
to a closed issue the moment this merged, with nothing noticing. Repointed
at AAASM-5536, and the reason now states plainly that no ticket owns proving
the claim and the expected resolution is qualification.
R6 — the splitter no longer emits bare list markers as sentences, treats "!"
as text so mkdocs "!!! note" survives intact, handles "?" as a terminator,
splits table rows and list items as units, and strips front matter, which
Python lacked where Go and Node had it.
Inverting the default immediately found five claims every keyword-gated
revision was blind to, including the page's own central promise ("whose tool
calls pass through the Agent Assembly policy gate") and an unbounded breadth
claim ("governs whichever agent framework you already use"). Four are now
registered unproven against AAASM-5661 and AAASM-5536; the teardown claim,
previously exempt under the removed `kind` field, is bound to a real control.
Refs AAASM-5529
…nd count occurrences
R3-1 — the two-tier rule was inverted relative to risk. A written
justification was required only when the sentence matched the enforcement
vocabulary, i.e. only for sentences an author had already been warned about.
A sentence that EVADED the vocabulary — the entire reason the scan was
inverted — passed with a bare category constant. The bare constant is now
available only to structurally non-prose lines (tab labels, table rows,
migration import pairs, bare link items), matched by a pattern; every other
entry carries a written justification unique to that sentence.
R3-3 — the scan was keyed by sentence, so duplicates collapsed before
anything counted them and "matched == 1" could only ever be 0 or 1, while
the message printed "it matched {n}" as though n > 1 were reachable.
Occurrences are now a list of (text, section). Measured: duplicating a bound
true sentence into a "## What NOT to expect" section now fails with
"it matched 2 (sections: ['## What just happened', '## What NOT to
expect'])". Section attribution was last-write-wins for the same reason and
is now per-occurrence.
Splitter — closing markup between a terminator and the following space is
kept WITH its sentence, so "**Tool calls were governed.**" is its own unit
rather than running into the claim it introduces. Binding the glued pair
covered both halves at once. A backtick is deliberately excluded from that
trailing class: inline code such as `phi.*` was otherwise read as a sentence
end and split mid-sentence. Four bindings were re-derived and two bold
labels are now bound in their own right.
Tickets — the mode claim now names AAASM-5766 and the breadth claim
AAASM-5768. Both previously named AAASM-5536, a docs-CI-tooling ticket that
will prove neither.
Accepted residual, stated rather than implied: "written justification" is
enforced as non-empty, at least 40 characters, and distinct across entries.
No gate can tell a justification from noise; length and uniqueness only make
an empty gesture and a copy-paste visible.
Refs AAASM-5529
…tences that turn R4-1 — the structural pattern was the new bare-constant route. It asked whether a sentence STARTED with structure, not whether it was ONLY structure, so a link item, a table row or a bold link was waved through on its first characters while its anchor text — rendered prose a reader sees — went unexamined. It covered 44 of 78 entries here. Measured: both "[Every tool request is permitted to proceed and its outcome captured for later analysis](x.md)" and the table-row form passed with the bare constant; both now fail. The pattern is fully anchored and admits only a bare mkdocs tab label. The other 24 entries — migration import pairs, Source attributions, Next-steps link items — now carry written justifications. R4-3 — the contrastive-conjunction rule existed only in Go; it is ported here. A sentence that turns mid-way can under-claim and over-claim at once, and a justification arguing "this only says what the product does NOT do" cannot be trusted for one that does. Both attack payloads are rejected: the reviewer's "because" form and the "but" form the Go entry had. "so" is deliberately excluded from the conjunction list. It is consequential rather than adversative, and the two sentences it flagged here turn in the direction they started. Excluding it costs neither payload, and controls for both are recorded in the falsification run. Refs AAASM-5529
I excluded "so" from the contrastive list on the grounds that it is consequential rather than adversative. The grammar was right and the question was wrong: the risk "so" carries is POLARITY CHANGE between clauses, and on that axis it is the highest-risk connector, not the lowest. "We do not do X but Y" is a concession; "we do not do X so Y covers it" is a REASSURANCE, and reassurance is the register documentation over-claims in. The payload that was green in all three: "Network-layer interception is not enabled by default, so the in-process adapter verifies every outbound request before it leaves the host instead." The second clause is an unbound affirmative capability claim, and false — no SDK adapter inspects outbound network requests, which is why AAASM-5766 exists. "so" is now flagged only when the clause before it contains a negation and the clause after it does not. That is the one shape a limitation-plus- reassurance takes, and the payload is the only negative-to-positive case among the live sentences. Measured across the three repos: 7 live allow-listed sentences contain " so " (python 2, go 3, node 2) and the refined rule flags none of them, while the payload fails in all three. My earlier count of two was python-only; the reviewer's six was also short, and node's figure needed reading ALLOWED at runtime because a regex over the source recovers only 31 of its 50 keys. Refs AAASM-5529
|
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.
Description
Binds every sentence of the Python quick-start to a control that proves it, or to an explicit allow-list entry saying why it makes no claim.
R3-1 — the justification rule was inverted relative to risk
A written justification was required only when the sentence matched the enforcement vocabulary — only for sentences an author had already been warned about. A sentence that evaded the vocabulary, which is the entire reason the scan was inverted, passed with a bare category constant.
The bare constant is now available only to structurally non-prose lines (tab labels, table rows, migration import pairs, bare link items), matched by a pattern. Every other entry carries a justification unique to that sentence — 34 of them.
R3-3 —
matched == 1was structurally unreachable above 1The scan was keyed by sentence, so duplicates collapsed before anything counted them and the check could only ever see 0 or 1, while the message printed
it matched {n}as though n > 1 were reachable. Section attribution was last-write-wins for the same reason.Occurrences are now a list of
(text, section). Measured — duplicating a bound true sentence into an inverting section now fails:Splitter
Closing markup between a terminator and the following space is kept with its sentence, so
**Tool calls were governed.**is its own unit instead of running into the claim it introduces — binding the glued pair covered both halves. A backtick is deliberately excluded from that trailing class: inline code such as\phi.*`` was otherwise read as a sentence end and split mid-sentence. Four bindings were re-derived and two bold labels are now bound in their own right.Tickets — this body previously named the wrong one
The mode claim now names AAASM-5766 and the breadth claim AAASM-5768. Both previously named AAASM-5536, a docs-CI-tooling ticket that will prove neither.
Correcting this body: revision 3 of it said the mode claim was registered "naming AAASM-5529's own undelivered mode-probing check." That was stale — and naming 5529 is exactly what the self-reference guard forbids. Worth fixing in a PR about documentation drift.
What "green" means here, and what a written justification is not
Green means the page's unproven claims are enumerated, not that the page is true. The count is the most useful number this PR produces:
An unproven claim names the ticket that will resolve it, and may not name AAASM-5529 — a self-reference resolves to a closed issue on merge.
Accepted residual, stated rather than implied: "written justification" is enforced as non-empty, ≥40 characters, and not byte-identical to another entry. That is all it is. The check cannot separate a justification written per sentence from one templated with a substitution — one differing token satisfies distinctness — and no check can separate either from noise. It is worth having only because it makes the two cheapest ways of waving something through, an empty gesture and a verbatim copy-paste, visible in review. Uniqueness here should not be read as implying bespoke.
The three residuals — the honest boundary of what this gate buys
sois worth catching because it is ordinary prose that reads as reassurance — the register documentation over-claims in — but chasing;,—andandwould flag large amounts of benign text for very little gain. The rule catches the shapes that hide a claim, not every shape that could.so— corrected from the previous revisionI had excluded
sofrom the conjunction list as consequential rather than adversative. The grammar was right and the question was wrong: the risk is polarity change, and"we don't do X so Y covers it"is a reassurance — the highest-risk shape, not the lowest.sois now flagged when the clause before it is negated and the clause after is not.Measured across the three repos: 7 live allow-listed sentences contain
" so "(python 2, go 3, node 2); the refined rule flags none of them and catches the payload in all three. My earlier count of two was python-only.R4 additions
[Every tool request is permitted to proceed and its outcome captured for later analysis](x.md)passed. The pattern is fully anchored now and admits only lines that are entirely scaffolding."A LIMITATION disclaimer…", the wording that shipped one round earlier, evaded it.sois excluded from the conjunction list as consequential rather than adversative; both attack payloads (because,but) are still caught.Type of Change
Breaking Changes
Related Issues
Testing
Every check demonstrated able to fail, by mutation. Each mutation asserts it applied before measuring and each restore is sha256-verified:
pytest test/unit/test_quickstart_claim_bindings.pypytest test/unitruff check/format --checkmypy(cache cleared)F7 — enforcement scope
maindeclares no required status checks, andquick-start claim bindingsis in no aggregation — python-sdk has noci-success.yml, andCI Successis a job insideci.yaml, which a separate workflow file cannot join. Visible on the PR; not merge-blocking. AAASM-5677's scope.Pre-existing red on
main, untouchedpre-commit run --all-filesfails onscripts/check_contact_metadata.py(ruff-format) on pristineremote/main. Does not block commits (staged-files-only hook); no CI runs--all-files.Checklist