Repository navigation
docs: verify owner-surface claims and record two proof rules - #219
Merged
Merged
Conversation
… to 3.11 - Wheel metadata requires Python >=3.11; the installed minimum smoke runs exact CPython 3.11.0 from digest-pinned official python:3.11.0-slim images with a checksum-pinned pip 26.2.1. REQ-PROOFKIT-PACKAGE-006 and REQ-PROOFKIT-QUALITY-011 state the same floor, and a test ties the package requirement to the metadata floor and minimum smoke constant. - CI and release jobs that consume host Python pin actions/setup-python to 3.15.0. A workflow oracle identifies the installation by action identity, not step name, and rejects unpinned, misplaced or duplicate Python installations. - The launcher imports subprocess only in its Windows fallback and takes Sequence from collections.abc, so the POSIX exec path loads neither subprocess nor typing on any supported interpreter. - Update npm 12.2.0, Node 26.11.1, axe-core 4.14.0, Playwright 1.63.0, Go x/* modules, govulncheck 1.9.0, osv-scanner 2.6.0 and pinned GitHub Actions (setup-node v7.1.0, upload-artifact v7.0.2, download-artifact v8.0.2, codeql-action v4.38.3) with independently read back pins. - Playwright 1.64.0 stays rejected: its WebKit 27.2 refuses a select element's internal style attribute under style-src; BROWSER-TOOLCHAIN-01 is updated.
…schemas Replace the last 34 root-shape-only public CLI directions with structural JSON Schema owned by the native command packages. After this change all 170 command directions publish structural definitions (166 definitions, none root-shape). Each schema covers nested fields, variants, cardinalities, bounds, enums and closed-object policy. Native admission remains the semantic authority. Commands described: - capability-map-admission, deployment-evidence-admission, repo-profile-admission, spec-proof-bundle-admission (input and output); - agent-route and change-workflow-plan (input and output), native-evidence-guidance (output); - adoption-contract-envelope, adoption-workflow-plan, pilot-admission (input and output); - conformance-profile, migration-plan, workspace-registry (input and output); - requirement-browser-server (input and output), view (output); - adoption-doctor, scaffold-project-structure, scaffold-profile-plan (input and output). Published contractId and schemaVersion values are kept. Where variants were re-partitioned, the change follows native admission: - adoption-contract-envelope input 01-root becomes 14 variants, one per --mode, pilot selection and guidance override; - pilot-admission input 04-direct-first and 05-direct-stack-diverse merge into 04-direct; - the requirement-browser-server output plan becomes 01-plan-<view>; - adoption-doctor and scaffold-project-structure outputs gain 03-invalid-input-envelope; - the two conformance-profile 02-profile conditions merge into one. Several members that the predecessor root shapes listed as required are optional or nullable in native admission. The schemas now describe them that way. Contract identity: docs/proofkit-contract-map.md now states when a direction's contractId changes. It changes when the wire shape changes, or when the CLI contract or a bound requirement statement gives a record that both releases handle a different meaning. Defect corrections, narrower or wider admission, changed values of behavior the previous text did not specify, diagnostics and renderings keep the contractId; the release change record declares them and states whether they are breaking. Correcting published text that the previous release's behavior already contradicted is a defect correction. The rule governs changes made after its adoption, and identities set before it are retained. Under this rule the directions changed here keep their contractIds. Their behavior changes are changed values or changed admission of behavior that the previous contract text did not specify. The previous root shapes of eight inputs listed members as required that native admission did not require: adoption-doctor, adoption-workflow-plan, capability-map-admission, deployment-evidence-admission, pilot-admission, requirement-browser-server, scaffold-profile-plan and workspace-registry. Their schemas now describe those members as optional; under the rule this is a defect correction. Generator: a variant can carry several CLI conditions. Aggregate outputs can declare array roots and exclusive sums of closed objects. admitChildBindings checks only the variants that carry the bound member, and schemaChildAtPath crosses value unions only when every alternative resolves the same child. A retired root-shape note is refused unless its predecessor retires it. internal/testsupport/schemacheck is a fail-closed evaluator for the draft 2020-12 keyword subset that the command structure tests use. It reports unsupported subschemas below not/oneOf/anyOf/allOf/contains as errors instead of counting them as mismatches. Contract size: with inline schemas the contract would be about 4.5 MB, above the previous 4 MiB installed bound. The generator now publishes each variant schema through internal/kernel/schemadefs.Hoist. Hoist shares a repeated object subschema of the variant's root resource when the subschema carries no $id, $anchor, $dynamicAnchor, $dynamicRef, $recursiveAnchor or $recursiveRef, is neither the root nor a direct root $defs entry, and sharing it saves canonical bytes. Larger subschemas are decided first. Other repetitions stay inline. A shared subschema becomes one root $defs entry named "shared-" plus the first 16 hex digits of the SHA-256 of the canonical subtree, and each occurrence becomes a pure $ref. Hoist returns only when Expand(Hoist(S)) == S canonically, and --check requires the published record to equal that result. Every $ref, $dynamicRef and $recursiveRef must name a direct $defs entry of its own resource. Shared entries form a DAG. scripts/schema-definitions.mjs is the matching JavaScript helper. scripts/schema-definitions.test.mjs is an independent oracle: it re-derives digests, closure, acyclicity, names, use counts and savings, and it compiles every variant with Ajv. The contract is 3,481,616 bytes. installedclicontract.MaximumContractBytes rises from 4 MiB to 8 MiB as growth headroom, not as a size target. The generator refuses to read or publish a larger contract. Every dedicated reader of the contract in the non-test Go code takes its limit from that constant. The generator, the coverage tool and the release closeout input previously used 16 MiB, and the Python wheel build and wheel record verification read the source contract without a limit. The npm, wheel and command-family carrier readers already used the constant, and the bounded contract decodes of the internal/app and requirement-coverage-input tests now use it too. Generic package-entry scans are outside this bound: package verification's scan of packed text entries still bounds each entry, the contract included, at 128 MiB before its carrier check applies the contract bound. TestEveryCLIContractReadTakesMaximumContractBytes scans the Go sources and fails when DecodeJSON, DecodeTypedJSON, LimitReader, ReadBounded or a same-package function receives the contract path, directly or through a derived path, file, reader or byte value, together with a literal byte limit or a package-level constant defined by one. Behavior changes for consumers: - workspace-registry: an absent or null admittedRootScriptNames now means no allowlist, so root scripts are unrestricted. An explicit [] is still an empty allowlist. Before, absent and null were admitted as [], which failed every root script. The other optional script lists keep absent == []. - migration-plan: blockerReasonSlug splits camelCase before lowercasing. The retained-owner blockerId suffix changes from "...-retained-wners" to "...-listed-in-retained-owners". - pilot-admission: caller text that the report echoes (blocking status, stack dimension, cache expectedOutcome and invalidatedInputClass, and the compact serialization of pilotMode) is checked before projection. Secret-shaped text refuses the input with no report and no echo. Ordinary unknown values remain collected failures. pilotMode uses admit.ContainsSecretLikeValue, so credential pairs split across JSON structure are refused. - Published variant schemas reference root "$defs" entries named shared-*. Consumers must compile each variant as its own document, or expand it first, before embedding it elsewhere. Ajv error schemaPath values differ from the inline form. - The installed contract bound is 8 MiB (8,388,608 bytes). - scaffold-profile-plan records environment-class provenance from the operand that supplied the classes. An omitted paths.specGlobs for a preset without a docs/specs/ starter path is still refused; only the diagnostic changes, which now says "paths.specGlobs must be caller-provided". The published input schema encodes the refusal with a root "not" clause. Other fixes and witnesses: - packageverify gives dependentRequired its own scope, so its member names are not treated as package references. - Whole-operation guard-order tests for verifyExactTarballConsumer and runBrowserProof check that admission happens before install, execution and proof writes. - scripts/browser-server-structure.test.mjs validates real one-shot stdout of requirement-browser-server and view against the published variants. Its refusal checks go through refused(). When the CLI rejects flags before reading stdin, spawnSync reports EPIPE for the unwritten payload, and refused() accepts that error and nothing else. The CLI must still exit with status 1, no signal, empty stdout and non-empty stderr. This follows internal/tools/workflowsmoke/process_streams.go. run() still fails on every spawn error. A deterministic test with an 8 MiB payload covers both paths. - proofkit.boundary-contract-check selects proofkit/requirement-bindings.json. - adoption-doctor and agent-route bind their vocabularies once and keep the predecessor variant labels. - docs/proofkit-contract-map.md describes structural parent schemas and the exact $defs sharing criterion. - The REQ-PROOFKIT-QUALITY-004 overview now says that published structural schemas describe nested fields, leaf types, cardinality and nullability; cross-field semantics, canonicalization and completeness parity remain native-command concerns. No requirement statement changes. - SCHEMA-01 is narrowed to the remaining completeness proof and stays BLOCKED. Each structure has independent oracles, wired into boundary-contract:check and the boundary witness plan: admission-records, adoption-envelope, agent-workflow, browser-server, profile-registry, scaffold-doctor and schema-definitions. Native source digests, cliContractPublicABISHA256, the compact v2 changed-observation pins and the cutover version-edge counts (168/164) were re-pinned from test output, and each drift was traced to these changes. The scaffold-project-structure source digests include projectstructure/input_structure.go, which copies the required list with slices.Clone; the generated output is unchanged by that copy. Non-claims: the structural schemas do not replace native semantic admission, secret and timestamp policy, path safety, sorted-unique normalization or cross-record checks. Structural validity does not execute witnesses or approve merge, release or rollout. Sharing changes only the published encoding, not validation semantics. SCHEMA-01 completeness is not claimed. The admission-records, adoption-envelope, agent-workflow, profile-registry and scaffold-doctor oracles treat a stdin EPIPE as a failure when the CLI refuses before reading its input, so they can fail intermittently under load; this commit does not fix that race. Go tests and the JavaScript oracles that read the repository contract are not all size-limited. Nothing is published. New or changed tests named here include TestEveryCLIContractReadTakesMaximumContractBytes, TestWheelBuildAndVerifyReadSourceContractUnderMaximumContractBytes and TestContractReadBoundsActualWorkAndPreservesOneSnapshot, which now exercises the 8 MiB bound. Proof on this tree: A local npm run check on darwin/arm64 passed (exit 0) on tree 3f0f398 with npm 12.2.0, CPython 3.15.0 and Go 1.27.2: 543/543 browser cases in Chromium, Firefox and WebKit with zero retries. BREAKING CHANGE: Every public CLI direction publishes a structural JSON Schema and the root-shape-only definitions are retired, so definition references and digests change for most directions. Each variant schema references root $defs entries named shared-*, so consumers must compile each variant as its own document or expand it before embedding it, and Ajv schemaPath values differ from the inline form. The shipped contract grows to 3,481,616 bytes and the installed contract bound rises to 8 MiB, so readers with a smaller limit must raise it. An absent or null workspace-registry admittedRootScriptNames leaves root scripts unrestricted instead of refusing them. The migration-plan retained-owner blockerId suffix changes to -listed-in-retained-owners. pilot-admission refuses secret-shaped text in the fields its report echoes, including credential pairs split across JSON structure in pilotMode, before any report exists. scaffold-profile-plan records environment-class provenance from the operand that supplied the classes.
…reign Darwin reaps Protected presentation output: requirement-spec-tree-view --output is the only Proofkit CLI writer of caller-named files outside the repository transaction kernel. Before this change it accepted paths inside Git metadata and kept an existing file's mode on replacement. A caller-named .git/hooks/pre-commit (0755) was therefore replaced with rendered bytes and stayed executable, and .GIT/... reached the same file through the case alias on case-insensitive APFS. Decision and owner boundary: the fix lives only in the presentation writer in internal/app/requirement_commands.go. One predicate, admitPresentationOutputPath, runs at argument admission, before stdin is read or any filesystem effect, and again at the writer sink. It refuses three classes of path: - A path with any component, at any depth, equivalent to .git or to repositorytransaction.ControlRoot (.agentic-proofkit). Equivalence is canonical caseless matching after removal of HFS+-ignorable code points, through pathidentity.ContainsComponentEquivalent. Any depth is required because the writer root is the working directory, not a known repository root. A path only in this class reports that the output must not enter repository metadata or Proofkit control state. - A path outside the path-identity domain: invalid UTF-8, more than 1024 bytes or more than 64 components. - A path with a component that becomes "." or ".." once HFS+-ignorable code points are removed, for example "." followed by U+200C. The literal repository-relative check admits such a component, but its HFS+-visible form is a dot segment. A path only in the last two classes reports "output path identity is invalid", because pathidentity cannot classify its aliasing. A path in more than one class gets one diagnostic: a domain violation always reports the identity diagnostic; otherwise the first component in path order that is .git-equivalent or whose visible form is a dot segment decides, and a .agentic-proofkit-equivalent component decides only when neither occurs. Replacing an existing file keeps its read and write bits and drops every execute bit. New files stay 0644. The existing symlink-leaf, symlink-parent, parent-swap and temporary-object identity checks are unchanged. The kernel is not changed. A kernel-wide .git refusal was rejected: integration lifecycle and adoption materialization write declared 0644 modes and refuse to replace files that are not admitted Proofkit artifacts, so the hazard does not exist there, and a kernel-wide name blacklist would merge these separate owners. The adopt-materialize input domain is unchanged for the same reason, and the requirement-authoring-plan domain is unchanged because its paths are labels with no filesystem sink. A --replace flag was rejected because it adds no authority and breaks regenerate-in-place. pathidentity.ContainsComponentEquivalent is a generic helper in the existing path-identity owner. Both operands are normalized the same way: HFS+-ignorable scalars are removed from the reserved name and from every component before the canonical caseless key is computed. A reserved name whose visible form is empty, "." or ".." is an error, and so is a path component whose visible form is "." or "..". A component whose visible form is empty is skipped. REQ-PROOFKIT-SPEC-009 and its overview line state all three refusal classes and the replacement-mode rule. Its non-claims add non-Git version-control metadata, hook files outside .git beyond execute-bit removal, and a working directory inside Git metadata. proofkit/requirement-bindings.json mirrors the non-claims and adds the binding proofkit.requirement-spec-tree-view.protected-output-falsifier. Foreign Darwin reaps: on Darwin, x/sys SysctlKinfoProc reports both a zero-length kern.proc.pid answer and a short record as EIO. EIO was an ordinary failure, so after a foreign reap the abort path and the final sweep still signalled the numeric process group, whose ID may have been reused. The Darwin observer now calls SysctlKinfoProcSlice and classifies the answer: - zero records: ErrOwnershipLost. No signal, Wait or probe follows, and the error reports child cleanup unverified. - exactly one record: the existing PID, parent, group and SZOMB checks. - more than one record: an ordinary failure. - truncation, EPERM and kernel EIO: ordinary failures. They are not evidence of absence. The observer runs only before the sole reap, so the unreaped child still pins its PID and group, and retained cleanup may signal them. Under the admitted schedule absence is unreachable; it means the no-foreign-reap contract was violated, and the lifecycle now fails closed. Darwin support: the supported Darwin claim narrows from macOS 13 or later, the 0.16.0 support claim, to verified macOS 15 or later on arm64 and x86_64. macOS 13 and 14 are no longer supported targets. The Mach-O minimum stays macOS 13.0, so macOS 13 and 14 are an explicit non-claim: binary-compatible by Mach-O metadata only, not executed. No hosted macOS 13 image exists, and GitHub retires macos-14 on 2026-11-02 after failing brownouts (actions/runner-images#13518), so no macos-14 job is added. - ci.yml adds the required job platform-smoke-intel ("quality / platform smoke / macos-15-intel", runs-on macos-15-intel, 20 minute timeout). ci-required-gate needs it and checks its result. - Both Darwin jobs now start with "Verify native Darwin architecture". The step prints and checks uname -m and sysctl.proc_translated, and fails unless uname -m is the job's architecture (arm64 on macos-15, x86_64 on macos-15-intel) and sysctl.proc_translated is empty or 0, so a job translated by Rosetta fails. The runner label is therefore backed by evidence from inside the job. The other seven steps are the same in both jobs, including the pinned actions/setup-python 3.15.0 step and Node 26.11.1. - The package-gate workflow oracle checks the exact job inventory, needs, names, runners and timeouts, the exact step list for each Darwin job and the aggregate shell. The expected architecture comes from the job ID. Every platform-smoke substitution mutant runs against both jobs. The mutants include an omitted or moved architecture step, the other job's architecture, and a removed architecture or translation check. x86_64-specific mutants cover relabeling to arm64, removal from needs, an unchecked result, consistent removal and continue-on-error. - The Python runtime oracle lists platform-smoke-intel as a host Python consumer and rejects omitting its pinned setup-python step or changing its version. - README, CONTRIBUTING, NON_CLAIMS and REQ-PROOFKIT-QUALITY-011 state the split. QUALITY-011 keeps the Python 3.11.0 installed-wheel floor and now counts four required leaf jobs. The README projection test pins the README text. It also pins the wheel-tag minimum (macosx_13_0); the only check of the Mach-O minimum is the wheel verifier's tag >= minos. Generated files: the internal/app and internal/kernel/pathidentity native-source digests were re-pinned in the CLI contract. Nothing else in the contract changed, and --refresh-structures and command-family:check report no further change. cliContractPublicABISHA256 and the pilot-admission|output|union compact observation pin were re-recorded from test output. With the pre-refresh contract, generated metadata and pin values, both pin tests pass on this tree, so the pin drift comes only from the regenerated digests. New or changed tests: - internal/app: TestPresentationOutputRefusesProtectedNamespacesPreservingBytesAndMode, TestPresentationOutputSymlinkAndHardLinkAliasesNeverReachHooks, TestPresentationOutputReplacementKeepsReadWriteBitsAndDropsExecuteBits and TestPresentationOutputRefusesPathsOutsidePathIdentityDomain. The last one covers invalid UTF-8, the byte and component limits, both dot-collapse cases and the admitted 64-component maximum. - internal/kernel/pathidentity: TestReservedComponentEquivalenceCoversPortableSpellings. It also covers a component whose visible form is empty, which is skipped. - internal/kernel/processgroup: TestDarwinRecordSliceSeparatesAbsenceFromShortRecords, TestDarwinObservationOutcomesDriveRetainedCleanup and TestRetainedForeignReapRevokesOwnership. - scripts: TestCIWorkflowDeclaresFailClosedRequiredAggregate, TestCIRequiredAggregateRejectsPlatformSmokeSubstitution and TestWorkflowPythonRuntimeRejectsUnpinnedConsumers. - internal/tools/pythonpackage: TestREADMEPlatformAndPythonProjection. Non-claims: local proof ran on arm64 only. x86_64 Darwin execution is evidenced only by the hosted macos-15-intel job. The architecture check was exercised locally as a script, natively on arm64 and under Rosetta, not on an Intel host. macOS 13 and 14 are not executed. A foreign reap between a successful observation and the abort remains a window on Darwin, which has no process handle, and hosts that answer EPERM cannot detect a foreign reap. A working directory inside Git metadata is not detected. Non-Git version-control metadata, hooks sourced regardless of mode, and the generated consumer TypeScript output writer are not covered. There is no kernel-wide path policy. Nothing is published. Proof on this tree: A local npm run check on darwin/arm64 passed (exit 0) on tree 0c8d17e with npm 12.2.0, CPython 3.15.0 and Go 1.27.2: 543/543 browser cases in Chromium, Firefox and WebKit with zero retries. BREAKING CHANGE: requirement-spec-tree-view --output refuses paths with a component equivalent to .git or .agentic-proofkit (canonical caseless, HFS+-ignorable code points removed), paths that are invalid UTF-8 or exceed 1024 bytes or 64 components, and paths with a component that becomes "." or ".." once HFS+-ignorable code points are removed. Replacing an existing file no longer keeps its execute bits. The supported Darwin claim narrows from macOS 13 or later (the 0.16.0 support claim) to verified macOS 15 or later on arm64 and x86_64; required CI executes macOS 15 on both architectures. macOS 13 and 14 are no longer supported targets; they remain binary-compatible through the macOS 13.0 Mach-O minimum only and are not executed. The CLI flag set, contract shapes, contractId and schemaVersion values are unchanged. The next release record must declare these changes; the published 0.16.0 record is not edited here.
…ed pipe
Problem: the full gate failed with "spawnSync ... EPIPE" in
scripts/agent-workflow-structure.test.mjs. The CLI correctly refuses
"change plan --agent-envelope --format text" before it reads stdin.
The child can exit before spawnSync has written the input, even for a
single small write, so spawnSync can report EPIPE. The oracle's run()
required result.error === undefined, which turned a correct early
refusal into a nondeterministic transport failure. The same assertion
guarded every node oracle that runs the Proofkit CLI with stdin input.
Only scripts/browser-server-structure.test.mjs had a narrow EPIPE
allowance, in refused().
Rule: scripts/cli-process.mjs exports assertCLITransport(result, label).
EPIPE is accepted only when the child exited normally with a non-zero
integer status and no signal, which is an early refusal. These still
fail: any other spawn error, a timeout, a signal, and EPIPE with status
0 (a success that did not consume its required input). Each caller
keeps its own status, stdout and stderr assertions, so a caller that
expects success still fails on the refusal status.
Precedent: internal/tools/workflowsmoke/process_streams.go treats EPIPE
from the stdin copier as an ordinary early exit and fails on every
other copier error. The Node rule is stricter: process_streams.go
accepts stdin EPIPE regardless of exit status, while assertCLITransport
also requires a non-zero exit status and no signal.
Changes:
- 28 oracles use assertCLITransport for every spawnSync CLI call that
sends stdin input, except the two scaffold-doctor calls named under
Non-claims. This includes the predecessor-baseline invocations in
the impact, inventory-coverage, proof-routing and selective-proof
oracles. The CLI spawns without stdin input (generated-starter,
integration, --input file and --help calls) and the go build helpers
are unchanged.
- browser-server run() and refused() both use the shared check. The
8 MiB test now asserts that the refusal reports EPIPE and is accepted
by refused(), and that json() rejects the same invocation on status
1. Before, it asserted that run() rejects EPIPE, and the new rule
replaces that per-path allowance.
- scripts/cli-process.test.mjs forces EPIPE with an 8 MiB input. It
checks that the CLI flag refusal is accepted, a child that exits 0
without reading stdin is rejected, and a child killed by SIGKILL is
rejected with or without EPIPE. It also rejects ENOENT, ETIMEDOUT, and
ENOBUFS from a child that traps the kill and exits non-zero. A
small-input control sends "{}" to the same refusal, applies the same
transport check, and asserts status 1 and the same stderr but not the
absence of EPIPE, because EPIPE can occur for any non-empty input.
- boundary-contract:check runs the helper test, and
TestBoundarySchemaGateWiring requires it in that gate's command.
proofkit/witness-plan.json lists scripts/cli-process.mjs in the
inputSelectors of the boundary, compact, receipt and spec-tree
contract checks, and lists the helper test in the boundary check.
Each mutation of the helper (no status check, no EPIPE code check, no
signal check, accept everything, the old error === undefined rule)
fails the helper test.
Non-claims: this changes only test oracles and their gate wiring. CLI
behavior, published contracts and the Go workflowsmoke carrier are
unchanged. It does not prove that every early exit is a flag refusal.
It only stops a closed pipe from hiding or replacing the caller's own
status assertion. CLI spawns that have no transport assertion today
(the scaffold-doctor workflow and replay calls) are not changed.
Proof on this tree:
A local npm run check on darwin/arm64 passed (exit 0) on tree
0c8f213 with npm 12.2.0, CPython 3.15.0 and Go 1.27.2: 543/543
browser cases in Chromium, Firefox and WebKit with zero retries.
…at documents
Add requirement-source-conversion (REQ-PROOFKIT-SPEC-044). Agents and
reviewers often edit one resolved record per requirement, while the
grouped v2 source keeps statement stems, shared premises and
profile-owned metadata once. Without an owner a flat copy either loses
that ownership or becomes a second editable source.
The grouped source stays the only source of record. The flat document
(kind proofkit.requirement-source-flat, schemaVersion 1) is a complete
derived interchange format:
- one resolved record per requirement with all ten metadata fields;
- profiles[] {profileId, fieldIds} and groups[] {groupId, profileId,
statementStemBytes, requirementIds} as ownership coordinates, so
membership exists only once;
- basisDigest, the sha256 of the canonical grouped bytes of the
admitted model.
CLI: --input <path|-> [--input-pointer] --to flat|grouped
[--baseline <path>] [--output <repo-relative path>].
- The format is decided by the admitted kind and schemaVersion only;
there is no --from flag.
- --to flat succeeds on every admitted grouped source whose emission
fits the CLI input bound.
- --to grouped requires --baseline (stdin is reserved for --input).
The baseline's canonical digest must equal basisDigest. Source
identity, requirement set, group membership, profile assignment,
field ownership and statement stems must equal the baseline, so only
values change. Profile values, premises and stems are read from one
coordinate-selected record and every other member record must state
them identically; ownership is never inferred from equal values.
- The retired flat v1 source (no kind, schemaVersion 1) is refused with
legacy_source_unsupported; every other identity, and a same-format
request, is refused.
- Both directions enter through the grouped codec and model and re-admit
the emission with equal resolved, layout and reference projections.
No semantic rule is re-implemented and no loss flag exists.
- Refusals leave stdout empty. Decoded input and baseline document
refusals carry one closed code and a JSON pointer or structural path
into the caller's document and no caller value; argument, path,
file-system and JSON decoding refusals use the shared CLI
diagnostics. An emission above the 32 MiB CLI input bound is
refused, so every output can be read back.
- --output publishes a complete new file only. The confined writer gains
a no-replace mode (temporary file, identity, mode and digest rechecks,
then os.Root.Link and temporary removal); an existing or concurrently
created name is never replaced. requirement-spec-tree-view keeps its
replace mode.
Rejected alternatives: a resolved-only flat format with a loss flag
cannot reconstruct ownership; a baseline-free import makes the flat
document a second editable source; an exact-file-byte digest would call
a reformatted unchanged baseline stale; importing flat v1 would need
invented group identities and an unproved field mapping. A future
representation, including a DSL, needs its own versioned identity, a
bounded codec and the same model, coordinate and re-admission
obligations; no adapter interface or plugin registry is added.
Contract: the native structural owners
proofkit.requirement-source-conversion.{input,output}.v1.json-schema
are registered in nativeStructures() with one variant per --to target.
The grouped variants are the grouped codec descriptor and are bound to
proofkit.requirement-source.input.v2.json-schema as root child
bindings. The variants are published through the shared $defs
publication like every other direction, so the contract now describes
172 directions (78 input, 94 output) in 168 definitions. The
generator test compares the grouped variant with the codec descriptor
through schemadefs.Expand and equalPublishedSchema instead of comparing
the shared publication directly. Inventories are extended:
- source-cutover version edge: 168 removed and 164 + residue + 2 added
definitions, plus the declared command addition;
- the cli_contract_test structural definition set and the rendered
usage line;
- the changed source-child path count, 40 -> 42;
- boundary-contract:check, its wiring oracle and the witness-plan
inputs gain scripts/source-conversion-structure.test.mjs (Ajv against
the published variants plus a JavaScript projection and node:crypto
digest that do not use the converter); its CLI runs use
assertCLITransport from scripts/cli-process.mjs;
- requirement bindings and the coverage required inventory gain nine
REQ-PROOFKIT-SPEC-044 scenarios, and the installed-carrier smoke runs
export, baseline import and five refusals.
Protected output paths: the output-path policy from the presentation
writer fix states that caller-named --output files never enter Git
metadata or Proofkit control state, with one predicate applied at
argument admission and again at the writer sink.
requirement-source-conversion --output is now a second writer of
caller-named files outside the transaction kernel and publishes through
the same sink, so it uses the same predicate.
admitPresentationOutputPath takes the admitting command's diagnostic
label; the spec-tree-view messages are unchanged and the shared sink
uses the label "output". No-replace and mode 0644 remove the
hook-overwrite hazard, but a new file could still be created under .git
(for example objects/info/alternates or info/attributes) or inside
.agentic-proofkit, which the policy forbids. REQ-PROOFKIT-SPEC-044, the
overview, ADOPTION.md and the command guide state the refusal, and the
requirement's non-claims (mirrored in requirement-bindings.json) add
non-Git version-control metadata and a working directory inside Git
metadata.
TestRequirementSourceConversionOutputRefusesProtectedNamespaces covers
case, HFS+-ignorable and nested aliases, refusal before an unparseable
input is read, the sink, the identity-domain refusal and publishable
near names. Dropping the guard at admission or at the sink makes it
fail.
TestRequirementSourceConversionCLI exports and baseline-imports the
hand-authored fixtures through the public CLI, refuses the unsupported
invocations and source classes with empty stdout, publishes a complete
new --output file, and refuses an --output name that another writer
creates just before the no-replace link while keeping that writer's
bytes, so publishing with a rename instead of the link fails the route
test.
Re-pins, each traced to its cause:
- native source digests of internal/app (descriptor, runner, help and
writer changes) and internal/command/requirementsourceconversion;
- cliContractPublicABISHA256: the new command, its two definitions and
those digests; the version-edge tests bound the command and
definition delta to exactly this command;
- compact pilot-admission|output|union: its native sources include
internal/app; with only that digest reverted the old pin passes.
Non-claims: conversion does not establish requirement meaning, make a
flat document a source of record, synchronize representations, migrate
proof bindings or references, preserve input formatting, key order or
bytes, import flat v1 sources or authenticate a baseline beyond its
admitted model digest. --output does not protect publication from
adversarial concurrent namespace mutation by the same operating-system
user and does not guarantee filesystem crash or fsync durability; it
needs hard-link support and fails closed without it, and parent
directories it creates may remain after a later failure.
REQ-PROOFKIT-SPEC-044 states these writer limits as non-claims.
Equal but differently spelled shared values are refused. The provider
carrier jobs have not run on this object, so the SOURCE-CONVERSION-01
backlog row stays open until they pass. Nothing is published.
Proof on this tree:
A local npm run check on darwin/arm64 passed (exit 0) on tree
48e3c2f with npm 12.2.0, CPython 3.15.0 and Go 1.27.2: 543/543
browser cases in Chromium, Firefox and WebKit with zero retries.
…rough the installed CLI Add REQ-PROOFKIT-WORKFLOW-020 and one whole-operation witness, workflowsmoke.VerifyTrajectory. Unit guide tests could not show that an agent can reach every needed instruction from CLI output alone, because they read repository files such as proofkit/witness-plan.json. The trajectory drives one fixture repository (Python and Go greeter, two requirements, two scenarios) through the public CLI only, from install bootstrap to current proof, and asserts exact facts at every step. Carriers: VerifyProcess now runs Verify and then VerifyTrajectory (AST-pinned by TestVerifyProcessComposesWorkflowAndTrajectory), so the installed npm carrier (packageverify) and the host wheel's module and console-script carriers (pythonpackage verify) execute the same trajectory without new carrier code. The CPython 3.11.0 floor smoke keeps its finite carrier cases through VerifyCarrier (REQ-PROOFKIT-PACKAGE-006) and does not run the trajectory. TestVerifyProcessAcceptsSourceBuiltBinary runs it against a go-built binary through real processes; TestVerifyTrajectoryAcceptsApplicationCLI runs it in process for the mutants. The trajectory stays out of Verify because the existing mutation tests re-run Verify about 35 times and pin invocation counts. Route ledger: before every invocation, including each --help, the route must have been printed by an earlier output of the same session, either as an installed-launcher command line (carrier prefix taken from "Installed invocation:") or as a JSON route (commandRoute, task commandId). The only assumed route is the install-time integration source. Prose mentions do not count (TestTrajectoryLedgerRefusesUnnamedRoutesBeforeExecution). About 170 invocations run per trajectory. Trajectory: integration source -> next -> adopt plan in the three trust modes (audit_from_code, code_baseline, fresh) -> capability-map and authoring candidates -> materialization plan and reviewed apply -> scenario storage round trip -> witness-plan projection and witness-scheduler-plan -> receipt admission, spec-proof-bundle linkage and receipt-currentness-scope -> coverage view -> requirement change, review repair, scenario-body change, native test change, Python to Go witness migration, drift and repair. Candidate-only planning, intake and authoring leave the repository tree and the status identity byte-identical. Acceptance predicate of the witness for an edge (requirementId, scenarioId): the receipt is admitted with status passed for the binding command and scenario selector, the bundle links it to the current bindings and scheduler, and currentness passes with recorded digests from the receipt and current digests recomputed from fresh CLI output and file bytes. The passed conjunct belongs to this predicate: receipt-currentness-scope does not read receipt status, and spec-proof-bundle-admission requires status passed only for merge-required receipts, so requireCurrent checks the admitted status in the receipt admission report, not the caller's input. Negative controls, each asserted with its exact failure: apply without reviewed identities; forged transaction identity; stale desired-state identity (three times); scenario membership omitting a bound requirement; a merge-required binding without a receipt, with a differential control that adds the receipt; not-run attempt; relabelled failed run; forged recorded subject; not-run and failed receipts with fresh subjects offered through requireCurrent; Python evidence after migration, alone and beside Go evidence. Mutant CLIs that accept a control, mis-invalidate an edge or drop one continuation line must make the witness fail. Invalidation matrix (only the changed edge goes stale; the unrelated requirement keeps its original receipt): - requirement statement change: REQ-GREETER-001 stale on binding; after the Python witness gains a whitespace-only case, stale on binding and dependency; one new REQ-GREETER-001 receipt makes both current. The tightening is reaffirmed only after the native test bytes change; the fixture also repairs the implementation, but that repair is a fixture step, not a checked subject; - scenario body change: REQ-GREETER-001 stale on binding through sourceReviewDigest; - native test bytes: semantic diff count 0, REQ-GREETER-002 stale on dependency; - Python to Go migration with stable requirement and scenario ids: REQ-GREETER-001 stale on binding, command, dependency and environment; only the Go receipt reaffirms it and the Python receipt never links again; - direct binding edit: next reports project_record_digest_mismatch and rematerialize_project; after reviewed apply both receipts are current. Fixture scheduler: each policy declares as inputSelectors every repository path its native command reads (the Python package and witness, or go.mod and the Go package directory), as the witness-scheduler-plan input guide requires. TestTrajectorySchedulerDeclaresEveryFixtureInput derives those reads from the command text and the fixture bytes at the initial and migrated scheduler. Input selectors are declared policy, not receipt subjects. CLI guidance defects fixed (each was a missing instruction that the trajectory needed): - witness-scheduler-plan --help gains an input guide (projection through witness-plan, template, policy rules); the spec-proof-bundle guide points to it. - requirement-context-slice and requirement-semantic-diff gain the input guides that requirement-context-compose --help already promised. - native-evidence-guidance step 7 no longer routes materialized projects to requirement-impact-input-compose, which reads compact proof contracts only; it routes to semantic diff, slice and currentness. - status --help and next --help print a total next-action continuation owned by projectstatus and checked against canonicalAction: for each action class, a help route or, for repair_project_records and repair_control_state, an owner stop. - requirement-source-admission --help teaches the scenario body shape and the one-editable-copy rule. - The help dispatcher keeps the requirement-source-conversion guide beside the new guides. Documentation: the ADOPTION.md reverse-review flowchart and text route materialized v1 bindings through requirement-semantic-diff, requirement-context-slice and receipt-currentness-scope, matching native-evidence-guidance step 7; requirement-impact-input-compose reads compact proof contracts and impact routes its composed input. The agent workflow overview states the installed-carrier scope and the two owner-stop action classes. Bindings and coverage: five REQ-PROOFKIT-WORKFLOW-020 bindings (whole operation, route ledger, installed carriers with proofkit.package-artifact, CLI guides, continuation owner) and the matching coverage required inventory, added beside the REQ-PROOFKIT-SPEC-044 conversion rows. Re-pins, each traced to its cause: - native source digests of internal/app and of nativeevidenceguidance, projectstatus, requirementcontext, requirementdiff, requirementsourceadmission, specproofbundleadmission and witnessschedulerplan (help guide sources); these 27 nativeSources leaves are the whole contract delta; - cliContractPublicABISHA256: those digests only; - compact pilot-admission|output|union: its native sources include internal/app; with only that digest reverted the old pin passes. Non-claims: Proofkit and the trajectory never execute the native Python or Go witnesses; fixture receipts are labelled observations, so this proves CLI admission, linkage, currentness and route closure, not native test truth or oracle adequacy. The fixture's per-edge dependency subject is the native witness file bytes, so an implementation-only change leaves the edge current. Producer trust, merge-satisfying receipts, compact-proof impact composition for materialized projects and selective-gate planning are outside the trajectory. One fixture does not establish universal repository fit, token cost or a paired pilot result. No CI wall-time budget is claimed for the extra installed-carrier invocations. Nothing is published. Tests named by this change: TestVerifyTrajectoryAcceptsApplicationCLI, TestVerifyTrajectoryRejectsAcceptedNegativeControls, TestVerifyTrajectoryRejectsWrongInvalidation, TestVerifyTrajectoryRequiresCLINamedRoutes, TestVerifyProcessAcceptsSourceBuiltBinary, TestVerifyProcessComposesWorkflowAndTrajectory, TestTrajectoryLedgerRefusesUnnamedRoutesBeforeExecution, TestTrajectorySchedulerDeclaresEveryFixtureInput, TestActionContinuationsMatchTheCanonicalActionTable and the guide tests in internal/app/trajectory_guides_test.go. Proof on this tree: A local npm run check on darwin/arm64 passed (exit 0) on tree b907fce with npm 12.2.0, CPython 3.15.0 and Go 1.27.2: 543/543 browser cases in Chromium, Firefox and WebKit with zero retries.
…nd nested source views Requirement source admission now reports up to eight independent faults of one rejected source on one line and counts the rest as "N more" (within the 512-scalar diagnostic bound). Dependent phases resolve only identities that were declared, so no reported fault is a consequence of another; beyond eight, faults are counted rather than described, so fixing one fault can move a later description into the count. Duplicate identity diagnostics point at the repeated entry's identity field. A single fault keeps its previous error identity and text, except that duplicate-identity paths now name the repeated entry. Shape-fault coordinates are computed in one sweep over at most eight kept faults, so cost stays linear in input size. The kernel JSON decoder keeps its error text and now also exposes the rejected byte's offset, line and column, including inside string tokens. A nesting-depth rejection points at the first value past the depth limit, not at the whitespace before it. Every --input reader appends that position. Nine generic-runner commands whose frozen predecessor corpora pin exact stderr bytes keep the unlocated message through a descriptor property: self-check, external-consumer, registry-consumer, registry-consumer-proof-input-compose, producer-policy-self-proof, migration-parity-admission, spec-overview-claims, release-authority and readiness-closeout. A test derives that set from the 13 frozen syntax-rejection rows and replays them byte for byte. requirement-source-transition lists addedRequirementIds, lifecycleChangedRequirementIds and missingRequirementIds beside their counts. requirement-semantic-diff adds scenario entries (entityKind "scenario") under /requirementSources/<sourceId>/scenarios/<scenarioId>, compared by owner-declared set, sequence and opaque fields, beside the requirement sourceReviewDigest change. Scenario entries count toward query.maxChanges together with requirement entries. Scenario identities are source-scoped in output re-admission, and empty arrays stay representable in before/after values. Source views nest a scenario's record under its requirement when it links to exactly one requirement. Otherwise the record is rendered once in a "Shared Scenarios" section, and every linked requirement lists its ID, as an in-page link in HTML, so rendered size stays linear in links. The workspace shows owner-declared deferral records and a deferred count. A shared stylesheet rule now hides unmatched static card groups, which changes the bytes of every static HTML view; the proof-lookup frozen-stream oracle declares that one stylesheet delta for its three HTML rows. ADOPTION.md explains source synthesis, the evidence chain and a bounded comparison note whose evidence is private and not shipped. Stderr addition: JSON syntax rejections of --input from every other command end with "at line L, column C (byte offset B)". This includes requirement-source-conversion --input and --baseline. Exit code and stdout are unchanged. Changes to surfaces from the parent commits: - The contract was regenerated from the native owners with commandcontractgen --refresh-structures. The two version bumps go through the structural generator: the predecessor of each bumped definition is the earlier json-schema definition, and its generated annotation is retired. - The semantic diff input guide now describes scenario entries and requirement-and-scenario comparison. The scenario body guide says the diff reports the scenario's own entries. - REQ-PROOFKIT-SPEC-022 and its overview bullet state schema-v3 input, schema-v4 output, scenario fields, and the retired v1/v2 inputs and v1-v3 outputs. A test ties those version numbers to the published contract. REQ-PROOFKIT-SPEC-021 now names its semantic diff as built from schema-v3 diff input. - REQ-PROOFKIT-SPEC-022 gains the binding scenario proofkit.spec-proof-core.requirement-semantic-diff-scenario-entries. Its witness, scenario_changes_test.go, falsifies scenario entries, changes between empty and non-empty arrays, scoped scenario identities and the owner-declared scenario comparison fields. The coverage tool's required binding inventory pins that binding's witness path, command, environment and four selectors, so deleting the binding or dropping a selector fails the coverage check. - The trajectory scenario-change diff and the guide test for scenario-body edits now also expect the scenario entry. - The ADOPTION.md comparison note refers to the compared tool releases by date. packageverify forbids exact release version tokens in shipped markdown, and the private run log keeps the exact versions. - A browser fixture with one scenario linked to two requirements exercises the Shared Scenarios link in Chromium, Firefox and WebKit, with an axe check at 390px. - Re-pinned from test output after checking each cause: the public ABI hash, and three compact observations. pilot-admission|output|union moved with the internal/app digest. requirement-browser-server|input|union moved with the requirementbrowser digest. requirement-semantic-diff|output| coverage-runtime moved with the v4 output. - The two CLI runs of the proof-lookup stylesheet-delta test use assertCLITransport from scripts/cli-process.mjs. Non-claims: no command is added. No admission, lifecycle or merge semantics change beyond the listed outputs and the maxChanges count. Nine commands keep unlocated syntax diagnostics. The comparison note in ADOPTION.md is not a ranking, and its evidence is private and not shipped. New or changed tests include TestSyntaxErrorKeepsMessageAndLocatesRejectedByte, TestPredecessorStreamOwnersReplayFrozenSyntaxStreams, TestInputSyntaxRejectionReportsLocationOutsidePredecessorOwners, TestManyShapeFaultsCostOneCoordinateSweep, TestComparisonValueShapeArrayAlternativesAreDisjoint, TestBuildReportsScenarioLevelChanges, TestBuildRepresentsChangesBetweenEmptyAndNonEmptyArrays, TestScopedScenarioIdentityRoundTripsThroughOutputAdmission, TestScenarioComparisonFieldsCoverEveryScenarioField, TestCurrentDiffIdentityRejectsRetiredContracts, TestWorkspaceAdmitsScopedScenarioDiffFromProducer and TestSourceRenderersGrowByIDsPerLinkedRequirement. Proof on this tree: A local npm run check on darwin/arm64 passed (exit 0) on tree 074517d with npm 12.2.0, CPython 3.15.0 and Go 1.27.2: 561/561 browser cases in Chromium, Firefox and WebKit with zero retries. BREAKING CHANGE: requirement-source-transition output is proofkit.requirement-source-transition.output.v3 (schemaVersion 3) with three new diagnostics entries; v2 validators reject v3 reports. requirement-semantic-diff output is proofkit.requirement-semantic-diff.output.v4 (schemaVersion 4): entityKind may be "scenario", scenario pointers and value shapes are added, and the non-claim text changed. The input stays schema v3. v3 validators reject v4 reports, and output admission accepts only v4. Scenario entries count toward query.maxChanges (default 8192): requirement-semantic-diff, and requirement-browser-server --view workspace with a diffInput, now exit 1 where they previously succeeded when scenario edits push the count past maxChanges. To migrate, refresh the published contract, and raise maxChanges or narrow requirementIds.
Six read-only audit reports named 24 candidate defects, and adjudication found one more. Each candidate was checked by execution or a code-cited argument: 18 confirmed, 5 refuted, 2 undecidable here. This commit repairs the 15 confirmed defects owned here. 13 of the 15 repairs have a test that fails on the parent; the other two are proof repairs whose tests pass on the parent and kill named mutants. Confirmed defects, fixes and tests: - Markdown code spans (markdownfmt.CodeSpan) emitted unmatched delimiters for payloads with edge backticks and displayed a&b as a&b. Fix: code spans pad edge backticks and spaces per CommonMark, and line endings become spaces. Payloads containing <, > or &, and the empty payload, render as escaped inline text, because a code span cannot escape them. The shared escaper also escapes ~. Tests: TestCodeSpanPadsEdgeBackticksAndSpaces, TestCodeSpanRendersHTMLSensitivePayloadAsEscapedText, TestCodeListOrNone. A goldmark v1.8.5 corpus of 230 cases fails 194 on the parent and 0 here, with no raw HTML node and no raw < byte. - A Go test-source oracle fixture in gotestsource was not valid Go, so a mutant that lets blank parameter names consume no argument survived. Fix: type-valid grouped-name and blank-leading fixtures. Test: TestHasFailureCapableAssertionCandidateAlignsArgumentsAcrossParameterNames. It passes on the parent and kills that mutant. - external-consumer required AGENTS.md and CONTRIBUTING.md, which package.json never packs. Fix: drop both from the required packed files. Test: TestBuildAdmitsCurrentPackageFilesAndRequiresRuntimeAssets, whose positive fixture is an independent literal of the current package contents. - adoption-doctor envelopes matched gaps to routes and candidates by ID prefix, so a child record received its parent's commands, selectors and facts. Fix: gaps carry the exact route or candidate identity and are looked up by that identity. Test: TestBuildAgentEnvelopeProjectsPrefixRelatedRecordsByExactIdentity, which checks the route, candidate-boundary and blocked-precondition actions of prefix-related records. - pilot-admission checked custom rule IDs for adjacent duplicates without sorting first, so [a,b,a] passed. Fix: check a sorted copy; diagnostics keep caller order. Test: TestBuildRejectsDuplicateCustomRuleIDsRegardlessOfPosition. - typescript-public-api-surfaces inventoried export const enum as a runtime export named enum when a line break followed enum. Fix: refuse const enum exports as unsupported source grammar. 0.16.0 already refused const enum exports, so this repairs a regression introduced after 0.16.0, and only the refusal message differs from 0.16.0. Test: TestCollectExportsRejectsConstEnumExports. - requirement-context-compose and repository-inventory blocked on a FIFO repository root until a writer appeared. Fix: rootpath.OpenDirectoryRoot rejects a static non-directory before os.OpenRoot. typescript-public-api-surfaces now uses the same helper instead of its own copy. Tests: TestComposeRejectsFIFORepositoryRootWithoutWriter, TestScanRejectsFIFORepositoryRootWithoutWriter. - requirement-context-compose opened catalog sources with a blocking open, so a FIFO swapped in after the path check blocked. Fix: O_NONBLOCK open on darwin and linux before the handle kind check. Test: TestReadCatalogSourceRejectsFIFOReplacementWithoutWriter. - workspace-shard-partition succeeded when a root's dependencies contradicted its package record. Fix: fail the shard when they differ and the closure otherwise succeeds. Test: TestShardPartitionRejectsRootDependenciesThatContradictPackages. - Compact requirement-coverage-view Markdown and HTML showed no witness routes although JSON had them. Fix: render declared witness routes (role and selector). Structured output is unchanged. Test: TestCompactRenderingsShowDeclaredWitnessRoutes. - PyPI registry evidence admitted duplicate wheel filenames, so [A,B,C,B] matched [A,B,C,D]. Fix: reject duplicates at admission. Test: TestPyPIRegistryEvidenceRejectsDuplicateWheelSubstitution. - The Python package verifier read each wheel three times (hash, ZIP inspection, pip), blocked on a FIFO wheel, and its local consumer check installed from the mutable path. Fix: one bounded read admits the bytes, and the local consumer check installs a private copy of them. Tests: TestVerifyWheelRecordRejectsFIFOWheelWithoutWriter, TestMaterializeAdmittedWheelWritesAdmittedBytesToPrivatePath, TestVerifyLocalPythonConsumerInstallsAdmittedBytesAfterArtifactReplacement. The last one kills a mutant that reinstalls from artifacts/pypi. - Installed-CLI probes accepted help that was written only to stderr. Fix: probes return stdout only and require empty stderr on success. Test: TestRunArgvWithEnvironmentDistinguishesStdoutFromStderr. - release.yml passed the GitHub token to curl in argv. Fix: the printf builtin writes the Authorization header to curl on stdin (-H @-). --fail, pipefail, URLs and the other headers are unchanged, and so is the pinned setup-python step in the same job. Test: TestReleaseTagVerificationKeepsTokenOutOfArgv, which executes the step with stub host commands. - REQ-PROOFKIT-QUALITY-027 said diagnostics are bounded to 512 scalars, but four owners emit up to 512 caller scalars plus a fixed 25-scalar truncation marker. Fix: the statement now says at most 537 in total. No behavior change. Test: TestRedactDiagnosticValueBoundsCallerScalarsAndTotalProjection pins both bounds. It passes on the parent and kills a mutant that raises the diagnostic bound to 520 scalars. The FIFO tests use a nonblocking writer for cleanup and a bounded wait. A late correct rejection therefore fails at the deadline instead of hanging the package. Three confirmed defects belong to earlier PRs in this chain and are fixed on the base: static browser views left a card group visible after a search had hidden it (#206); workspace-registry treated an omitted or null root-script allowlist as an empty allowlist, and scaffold-profile-plan attributed caller environment classes to the stack preset (#201). Refuted: a generated JSON report adapter that stops on a nonzero exit before reading --output (the only --output route exits 0 whenever it writes); repeated adoption-doctor blocked-precondition step IDs (no uniqueness contract on step IDs); order-dependent handling of a repeated --input-pointer whose value is empty (the contract declares no single-occurrence obligation for that flag); repeated command descriptors and adapters (no lower-cost alternative with the same observations was shown); and separated duplicate shard roots (they are still rejected). The two items that were undecidable here stand as follows. Whether scaffold-profile-plan defaults spec globs for a preset without a docs/specs/ starter path was decided in #201: paths.specGlobs must be caller-provided. Whether gh release create with assets creates a draft before uploading on the hosted runner is left to release preparation. Integration with the earlier PRs: - adoption-doctor keeps #201's kind and phase constants and adds the exact identity fields. The structural oracles (Go structure_test.go and scripts/scaffold-doctor-structure.test.mjs) required one action with both route and candidate selectors. That state was reachable only through the prefix defect. Both oracles now require route-only and candidate-only actions and reject an action that carries both. The schema is unchanged. - scripts/consumer-evidence-structure.test.mjs declares one stream delta, caused by the packed-file change, for the frozen external-consumer/pack-empty-files row. It rebuilds the predecessor stdout from the current bytes, by restoring the two removed failures and renumbering them, and compares the hash with the untouched corpus. Mutants show the delta is exact and limited to that row. - The compact relation-parity digest and the pilot-admission and requirement-coverage-view union observations were re-pinned. With the parent's render.go, or with the parent's contract, the old values hold. - The corrected #201 test that calls verifyWheelRecord now takes its two results (`_, verifyErr =`), so it still catches the same mutation. - Native source digests were regenerated: 28 canonicalDigest values in 9 source paths and no other contract change. The public CLI ABI hash was re-pinned from test output; the old hash holds with the parent's contract and generated metadata. Compatibility: no command, flag, contractId, schemaVersion or schema changes. Compared with 0.16.0, four of these repairs are breaking; the footer names them. The other observable changes include Markdown and HTML renderings, FIFO repository roots and sources that now fail instead of blocking, the const enum refusal message, the requirement-context-compose diagnostic for a missing repository root, native-source digests in the shipped CLI contract, the REQ-PROOFKIT-QUALITY-027 wording, and repository release tooling. Non-claims: the FIFO tests ran locally on Darwin and, on an earlier revision of this change with the same FIFO tests, in the hosted quality / source job on ubuntu-24.04 (GitHub Actions run 38207222469); other platforms are not claimed. The release workflow change was not executed on a GitHub runner with a real token, and no live registry execution is claimed. The Python minimum-version smoke still re-reads the wheel and installs it from its snapshot path after verifying it. Markdown escaping was checked against CommonMark and three GFM extensions, not against every Markdown dialect. Proof on this tree: A local npm run check on darwin/arm64 passed (exit 0) on tree 203f08b with npm 12.2.0, CPython 3.15.0 and Go 1.27.2: 561/561 browser cases in Chromium, Firefox and WebKit with zero retries. BREAKING CHANGE: compared with 0.16.0, workspace-shard-partition fails a shard whose root's workspaceDependencies contradict that package's record, where it previously succeeded. pilot-admission rejects duplicate custom rule IDs wherever they occur, not only when adjacent. external-consumer no longer requires AGENTS.md and CONTRIBUTING.md in the npm pack metadata, so a report that failed only for those files now passes. adoption-doctor --agent-envelope actions take route and candidate data only from the record their gap names by exact ID: a route or candidate whose ID is another record's ID plus a dot-separated suffix no longer receives that record's commands, selectors, owner questions or facts, and no action carries both route and candidate selectors. contractId and schemaVersion values are unchanged.
…sting Retire WEB-PUBLISH-DESIGN-01 by deciding its owner boundary. The row records an owner request for optional authenticated publication of the specification browser at a configurable domain, so the need exists; the open question was where the capability belongs. Decision: authorized remote readers get a read-only view through the existing --format html export, published from a consumer-owned static host behind a consumer-owned access gateway. Proofkit keeps rendering (requirement-source-view, requirement-proof-view, requirement-coverage-view, requirement-spec-tree-view) and the existing secret-scan and rendered-artifact-freshness checks. The consumer owns the domain, DNS, TLS, identity, authorization, upload, caching, revocation, rollback and disclosure approval. Rejected alternatives: - A Proofkit deployment adapter covers the same read-only need and adds custody of provider credentials, upload and partial-publication rollback, a provider-specific topology and a second deployment authority. Proofkit can neither own nor prove these generically. - An authenticated hosted server adds identity, sessions, CSRF, tenancy and internet exposure to a server whose security model is loopback binding, Host/Origin refusal and a per-session capability. Its extra value, remote interactive use, was not requested. Reconsider only for a confirmed need the static route cannot meet, with owner decisions for hosting, identity and revocation, a feasibility witness and negative cases for unauthorized access and unintended publication. Changes: - ADOPTION.md, Rendering And Browser Views: the loopback contract of requirement-browser-server and view; remote reading as a consumer hosting concern; every delivered byte is disclosed and client-side filters are not redaction; text/html, nosniff and a script CSP that admits only the embedded script hash; secret-scan as an advisory byte check; rendered-artifact-freshness for hosted copies; presentation_only authority; workspace, comparison and question handoff stay local; the reopen condition. The loopback hosts are named through the --host choices without an IPv4 literal, because packageverify rejects dotted numeric triples in shipped markdown. - NON_CLAIMS.md: remote publication, hosting, authentication, access control, TLS, revocation and freshness of specification views. The item precedes the macOS 13/14 item so the list keeps one terminal item. - BACKLOG.md: remove WEB-PUBLISH-DESIGN-01. Its completion branch, retain local-only behavior and retire the candidate with rationale, is met; the durable rule lives in ADOPTION.md and NON_CLAIMS.md. - requirementbrowser server_test.go: TestStartServerFailsClosedForNonLoopbackHosts covers ten unspecified, named, bracketed, padded, alternate-loopback and routable hosts, requires the host-admission error rather than a listen error, and closes the server if a weakened admission lets it start. Witnesses on an earlier revision of this change, with a binary built from it: - requirement-source-view --format html on the spec-proof-core source exits 0 with 301589 bytes. The bytes are identical with cwd / and an empty environment, and with all network denied by a sandbox. They hold one inline script and one inline style, no external reference, no non-fragment link and no local path; secret-scan passes with 0 findings. - requirement-browser-server --view source --serve listens only on the IPv4 loopback address and serves the same bytes with text/html; charset=utf-8, nosniff and a CSP whose only script source is the SHA-256 hash of the embedded script. A foreign Host or Origin gets 403 without specification bytes, and POST gets 405. - The proof, coverage and spec-tree views on the browser static fixtures give the same results: exports independent of cwd and environment, no external reference, 0 secret findings, and served bytes identical to the export under the same headers. - --host 0.0.0.0, ::, localhost, 127.0.0.2, [::1], ::ffff:127.0.0.1, 192.0.2.1 and example.com are refused before listening, for requirement-browser-server, view and the plan mode. - rendered-artifact-freshness passes with the recorded digests and fails with source digest drift after a source edit. - Mutants of the host admission: loopback by net.ParseIP fails 5 host cases; an allow-list extended with wildcard and named hosts fails 3. Issues #64 to #66 (GOVERNANCE-01, VALUE-01, RELOCATION-01) stay unchanged. Repository evidence leaves at least one promotion conjunct of each row unsatisfied: #64 has no sanitized consumer fixture, no insufficiency proof against adoption-doctor and no second consumer; #65 has no execution-receipt projection, baseline producer or downstream consumer; #66 has no owner-admitted content-addressed baseline, and the lifecycle baseline owns a different tool/bootstrap authority. Retiring or promoting them would be an owner decision without new evidence. Proof on that revision: gofmt -l, go vet ./..., go tool staticcheck ./..., npm run text-policy, go test -p 2 ./internal/command/requirementbrowser/..., the packageverify stale-doc tests, commandcontractgen --check and npm run package:artifact. npm run check on that revision (npm 12.2.0, CPython 3.15.0, Go 1.27.2) passed, including 561/561 browser cases in three engines with zero retries. Proof on this tree: A local npm run check on darwin/arm64 passed (exit 0) on tree ee6d116 with npm 12.2.0, CPython 3.15.0 and Go 1.27.2: 561/561 browser cases in Chromium, Firefox and WebKit with zero retries. Non-claims: no remote publication, deployment, domain, DNS, TLS, gateway, identity provider or audience was configured or authorized. No hosted, gateway, revocation, alternate-origin or cache behavior is proven. secret-scan does not decide confidentiality. The network-denial witness uses macOS sandbox-exec and is not an isolation proof. No consumer repository was inspected for #64 to #66.
…ilot
Two blind agent pilots used only the installed CLI on two different
repositories (a Python and Go greeter and a Python delivery-quote
service). Both completed every task step, and neither accepted stale
evidence as current. An independent scorer reduced their reports to 21
distinct defects and reproduced all of them. This commit makes 5
behavior fixes and answers the remaining findings with guidance at the
route where each decision is made or with a stated reason for making
no change.
Behavior fixes:
- Proof linkage integrity: bundle linkage compared only the scheduler
plan ID, so a receipt recorded under one command definition linked
under another plan that reused the ID. witness-scheduler-plan now
reports a proofNodeDigest per command: the SHA-256 of exactly that
node's execution decision (its admitted command record, its policy
without prose nonClaims, and the vocabulary rows it references: the
policy rows of its environment classes and whether its credential
class is non-cacheable). Receipts record their node digest, and
linkage requires the plan ID plus the node digest of receiptKind; a
missing node never links. Edits to another node, to nonClaims or to
spelling do not unlink, so the edge-local reaffirmation of
REQ-PROOFKIT-WORKFLOW-020 holds: after a witness migration the
unaffected receipt still links. A reflection test proves every
command, policy and vocabulary field is either hashed or excluded
with a reason; mutants restoring ID-only or whole-plan binding are
refused. Bare vocabulary memberships are not hashed, because
admission requires them and the names are already in the command
record.
- Stale source plan: adopt materialize plan/apply accepted a stale
sourcePlan as ready. A sourcePlan is now accepted only when it is the
plan recorded in proofkit/project.v1.json or an observation of the
current repository root; otherwise both refuse before any write, and
the guide names every root change that makes a plan stale.
- Owned source paths: requirement-source-admission listed overview.md
in sourcePaths although nothing creates it; the owner-written
overview stays a reserved path and is no longer listed.
- Missing context files: a missing context catalog file is named by
kind and path together with the step that creates it.
- Verification route: next and status named an empty route for
verification_required; they now name native-evidence-guidance.
Guidance at the decision route:
- root help names the agent bootstrap route, integration source, then
next;
- adopt plan --help explains each adoption mode;
- adopt materialize plan --help states what the .agentic-proofkit/
control state holds and that it stays out of version control;
- oracleKind and runnerClass are stated as consumer labels that
Proofkit admits and never interprets;
- proof-receipt-admission --help maps native bytes to the receipt
subject digests and gives one admissible example digest encoding;
- identifier grammars and the sideEffectClass values are rendered from
native constants, and the scheduler guide states only what admission
enforces for sideEffectClass none;
- the scheduler template leaves sideEffectClass null, like the other
reviewed facts, instead of prefilling none, so a copied template is
refused at sideEffectClass until the owner declares a class;
- witness-scheduler-plan --help states that the binding projection
passes no environment variable and that two writers of one resource
or lock need separate groups in an explicit catalog;
- usage lines name the admitted --format values;
- requirement-authoring-plan --help explains non-empty ownerQuestions;
- native-evidence-guidance --help step 8 gives a witness-migration
recipe that never relabels receipts: the moved edge's old receipt
goes stale, receipts of unchanged commands stay linked, and they stay
current only if the moved files are outside their declared dependency
scope;
- change plan --help step 1 states that a dependency scope includes
modules reached only through a shared import, so their receipts go
stale together, and that a scope is never narrowed to keep a receipt
current.
Declined, with reasons: a terminal completed state in status (status
reads no receipts; completion is the owner's decision over a passed
bundle and current receipts, which the guide now says), a shipped test
runner or digest helper (Proofkit must not execute native tests), a
text format for requirement-coverage-view (markdown is its human
rendering), and a general help reduction (the guidance above adds
lines to the affected pages).
Contract identities: the stale-plan refusal narrows admission, and the
verification route sets a value the previous contract text left open.
Neither changes a wire shape or makes earlier contract text false, so
adopt materialize plan/apply input keeps
proofkit.adopt-materialize-{plan,apply}.input.v3 and status and next
output keep proofkit.status.output.v1 and proofkit.next.output.v1.
Their compatibility summaries now state both rules. Both changes are
still breaking and are declared below.
ADOPTION.md now states that interrupted transaction residue does not
block a later plan built from current inputs, and that residue which
adds .agentic-proofkit/ before the first adoption materialization makes
an earlier source plan stale, so adopt plan must be rerun.
The agent trajectory witness records node digests and its migration
step shows the unaffected receipt staying linked. Because the scheduler
guide now defines sideEffectClass none as no write at all, caches and
bytecode included, the trajectory fixture declares its native commands
as local_write: the Python unittest command writes Python bytecode and
the go test commands write the Go build cache. After the migration both
Go commands write the build cache, so, as the guide prescribes for two
writers of one resource, the trajectory admits an explicit witness-plan
catalog that moves the migrated empty-name command to its own parallel
group; the farewell command keeps its group and its node digest.
Non-claims: Proofkit still does not execute native tests or compute
witness digests for the consumer; node digests bind execution
decisions, not test truth. Pilot evidence is two runs with one model
family on synthetic fixtures.
Tests: TestBundleLinkageBindsSchedulerPlanNode,
TestProofNodeDigestCoversEveryExecutionMember,
TestProofNodeDigestProjectsVocabularyOntoReferencedNames,
TestSourcePlanMustBeRecordedOrObserveCurrentRoot,
TestSourcePlanFreshnessGuideNamesEveryRootChange,
TestSourcePathsListOnlyPathsTheSourceOwns,
TestActionContinuationsMatchTheCanonicalActionTable,
TestPilotSemanticChangesKeepTheirContractIdentities,
TestSchedulerGuideProjectsTheConnectedBinding,
TestDecisionGuidesExplainOwnerQuestionsWitnessMovesAndDependencyScope
and the workflowsmoke trajectory with its mutants.
Proof on this tree:
A local npm run check on darwin/arm64 passed (exit 0) on tree
f654a1e with npm 12.2.0, CPython 3.15.0 and Go 1.27.2: 561/561
browser cases in Chromium, Firefox and WebKit with zero retries.
BREAKING CHANGE: witness-scheduler-plan output is contract v2
(schemaVersion 2) with a required proofNodeDigests diagnostic.
proof-receipt-admission input is contract v2 (schemaVersion 2) and
requires receipts[].proofNodeDigest; v1 receipts are refused with a
migration message. spec-proof-bundle-admission input is semantic v2
(wire schemaVersion 1): child receipts carry proofNodeDigest, and a
receipt links only when both the scheduler plan ID and the node digest
of its receipt kind match, so a receipt recorded under one command
definition no longer links under another plan that reuses the plan ID.
requirement-source-admission output is contract v3 (schemaVersion 3)
and its sourcePaths no longer lists overview.md. These four directions
change their JSON Schema, so closed-schema validators of the previous
versions reject the new records. Two breaking behavior changes keep
their contract identities, wire versions and JSON Schema: adopt
materialize plan and apply (input
proofkit.adopt-materialize-{plan,apply}.input.v3, wire schemaVersion 2)
refuse, before any write, a sourcePlan that is neither the plan
recorded in proofkit/project.v1.json nor an observation of the current
repository root; and status and next (output proofkit.status.output.v1
and proofkit.next.output.v1, wire schemaVersion 1) name
native-evidence-guidance instead of an empty route for
verification_required, so statusId and packetId values change and
records with an empty verification route are refused. Migration:
refresh the contract, record proofNodeDigest from the scheduler report
in every receipt, and rerun adopt plan when the repository root changed
after a plan that is not the one recorded in proofkit/project.v1.json.
…ed lower bound for native ownership
Owner decision (2026-10-12): the manifest's native-owned records are a
verified lower bound, and an input "absent" disposition is absent
relative to the class indicators over everything that Rapid Type
Analysis reaches from the direction's route. The completion condition of
the SCHEMA-01 backlog row is reformulated to exactly what the committed
oracles prove. The row is removed from BACKLOG.md, and its former open
obligations become documented limitations in the manifest nonClaims.
Reformulated completion condition: an independently authored
completeness manifest enumerates every published direction, definition
and variant. Per direction, it records which cardinality, bound, enum,
default, duplicate, unknown-field and cross-field constraints the
schema expresses, and it records the native-owned constraint classes as
a verified lower bound:
- every named owner is RTA-reachable from its direction's route;
- every input owner and output enforcer of an indicator class other
than default reaches an indicator of that class through static calls;
- output producers own their output classes by role;
- default and semantic records are tied by reachability and by any
recorded witness;
- every recorded witness resolves (test, mutation, cli);
- an input "absent" means no indicator of the class is reachable from
the route.
The published schemas pass enumeration, expression and disposition
parity against that manifest and a class-targeted mutant corpus of
recorded native observations. The argv observations replay natively
inside their route reach sets. No published schema content changes in
this commit (the contract delta is the internal/app nativeSource digest
only), and native admission stays authoritative (manifest nonClaims[0]);
every published uniqueItems that refuses a duplicate of the first item
of an observed argv-input array is also a native refusal.
Clause-by-clause proof. JS tests are in
scripts/schema-completeness.test.mjs; Go tests are in the new package
internal/app/schemacompleteness.
1. Enumeration: "manifest enumerates exactly every published direction,
definition and variant" and "enumeration parity refuses added,
removed and renamed directions and variants".
2. Expressed classes: "declared schema-expressed classes equal the
classes the published schemas express" and "crossField is expressed
only by relations between members".
3. Verified lower bound:
- route reachability, class-indicator tie and test-witness reach:
TestSchemaCompletenessOwnersAreReachableFromTheirRouteHandlers;
- disposition completeness, output producers, witness evidence that
matches the class literal, and witnessSummary: "every native-owned
disposition names existing owners with checkable witnesses";
- mutation witnesses:
TestSchemaCompletenessMutationWitnessesFailTheirTests;
- cli witnesses: "committed native residue rows are schema-admitted,
natively refused and owned by the named owner";
- reach sets against execution:
TestSchemaCompletenessReplayedExecutionStaysWithinRouteReach;
- the slicing input does not perturb reach:
TestSchemaCompletenessRouteSlicesStartAtTheCLIEntryAndExcludeTheRouteInventory
and TestCommandRouteRunnersEqualCommandDescriptors;
- refuted records cannot return:
TestSchemaCompletenessCallGraphChecksRefuteReviewedRecords.
4. "absent" is relative to the class indicators: the class-indicator
check of TestSchemaCompletenessOwnersAreReachableFromTheirRouteHandlers,
the default and output rules of the expression test, and the two-sided
indicator pins TestSchemaCompletenessClassIndicatorsEnumerateKnownHelpers
and TestSchemaCompletenessClassIndicatorsExcludeOtherClassHelpers.
5. Parity and mutant corpus (110,057 refused mutants):
- "structural and multi-member not mutants are refused by their
keyword";
- "class-targeted mutants of recorded native observations are
refused at every evaluated location";
- "observation rows bind their command and the variant their argv
selects";
- "argv observations replay natively: inputs are admitted and
outputs are reproduced exactly".
6. No semantic or policy authority: this commit changes no published
schema content, and native admission stays authoritative (manifest
nonClaims[0]). Two tests are narrow witnesses of that boundary, not
a proof of it: "every published uniqueItems that refuses an observed
duplicate agrees with native refusal" (231 agreement rows), and
"committed native residue rows are schema-admitted, natively refused
and owned by the named owner" (184 residue rows), in which native
admission refuses schema-admitted perturbations. No test replays
schema-refused corpus mutants natively, so a published constraint
stricter than native admission is not excluded.
Documented limitations (manifest nonClaims):
- Unclassified reachable refusal sites belong to no class, so "absent"
does not exclude them. This covers literals that no indicator
matches, messages built in composite literals or message tables, and
refusals without a message literal.
- Shared-literal ties: an indicator literal can also match other
classes, and only mutation witnesses prove the named refusal.
- Owner lists are a lower bound over the refusal sites that the
replayed inputs execute.
- Observations without argv are admitted by their published variants
under Ajv only and are not reproduced from committed inputs: the 104
output and 4 input rows below index 207 (input rows 0, 2, 128 and
190), recorded at commit 669ee3f, which is not on the published
history, and the 33 appended output rows from index 207 onward.
- Residue evidence is not unique among route literals.
- The order-free exact-residue uniqueItems deferral keeps its overturn
condition.
What the commit adds:
- Test-owned fixtures under internal/app/testdata: the completeness
manifest, the native observations, the native residue and uniqueItems
agreement rows, and the mutant corpus record. Observation row 176 of
spec-proof-bundle-admission embeds the witness plan and the
requirement bindings, and row 252 only the requirement bindings. Both
read committed snapshots, schema-completeness-embed-witness-plan.json
and schema-completeness-embed-requirement-bindings.json, copied from
proofkit/witness-plan.json and proofkit/requirement-bindings.json
when the mutant corpus was last recorded and not kept equal to them.
Edits to the live files therefore do not change the observations or
the corpus record. The corpus record changes only when an observed
constraint or an observation value (an embedded snapshot or a
referenced oracle-corpus row) changes.
- scripts/schema-completeness.test.mjs, run by boundary-contract:check
before scripts/cli-process.test.mjs, with the gate wiring oracle and
the witness-plan selector updated to match.
- The RTA, coverage and mutation tests in the test-only package
internal/app/schemacompleteness, which runs in its own test binary so
that the internal/app tests stay inside go test's default timeout;
go test ./... still runs it. The package has no non-test Go file, so
it does not enter the internal/app nativeSource digest. It reads the
route slicing inventory through the new module-private accessor
app.CommandRouteRunners, a sorted deep copy of the command
descriptors (name, route, runner) that no CLI path calls.
- Native ownership is authored from native code and an RTA indicator
dump, never from the published contract. It covers both directions
of requirement-source-conversion, the stale sourcePlan refusal of
the adopt materialize plan and apply inputs
(adoptionmaterialization.validateSourcePlanFreshness, with a mutation
witness), and the multi-fault requirement source codec: the
refusal-call name pattern includes Fault (capitalized, so Default
does not match), and the two codec pins name addUnexpectedFieldFault
(unknownField) and shapeNodeFault (default), the functions that spell
unknown_field and missing_field.
- Observation rows 88, 148, 150, 152, 198, 267 and 274 and the
requirement-source-conversion rows 312 to 315 were recorded against
the native sources of b5804e1; the observation capture records how.
Two oracle mechanics serve them: a {repoRoot}/<name> argv token names
a repoRootFiles file (JS replay and Go coverage replay), which
--baseline needs, and a "--flag naming ..." variant condition is a
presence requirement.
- Three native unit tests that the manifest names as witnesses: sorted
and unique nonClaims in registryconsumer and specoverviewclaims, and
duplicate changedPaths in selectivegateplan.
- docs/proofkit-contract-map.md describes the oracles and their limits.
Contract and compatibility impact: no command, flag or schema content
changes, and nothing is breaking. The only published contract delta is
one nativeSource digest in proofkit/cli-contract.v2.json; the other
shipped changes (a contract-map paragraph, the boundary-contract:check
script in package.json and one self-hosting witness-plan selector)
change no command, flag or schema. commandcontractgen digests the
non-test, non-generated Go sources under internal/app, so the accessor
changes the internal/app nativeSource digest in the published contract:
- its 12 occurrences change, and the generated contract and the preset
source SHA follow;
- cliContractPublicABISHA256 in TestCLIContractPublicABIGoldenStable is
re-pinned;
- the compact pilot-admission|output|union hash, which
TestCurrentCompactV2WireSemanticsMatchFrozenVersionEdge reads from
internal/app/testdata/compact-v2-current-changed-hashes.json, is
re-pinned, because that output contract carries the internal/app
digest.
Non-claims: the manifest, observations, snapshots, residue and corpus
are test-owned fixtures, not public contracts. Native admission stays
authoritative. release/change-record.v2.json (0.16.0) is a historical
record that still says "remain open under SCHEMA-01"; the next release
record owns that change. No schema-refused corpus mutant is replayed
natively.
New or changed tests: the schema-completeness.test.mjs tests and the
internal/app/schemacompleteness tests named above,
TestCommandRouteRunnersEqualCommandDescriptors, three native test
witnesses that the manifest names
(TestRegistryConsumerRejectsUnsortedOrDuplicateNonClaims, selectivegateplan
TestBuildRejectsDuplicateChangedPaths and specoverviewclaims
TestBuildRejectsUnsortedOrDuplicateBoundaryNonClaims), the gate wiring
oracle TestBoundarySchemaGateWiring, and the re-pinned
TestCLIContractPublicABIGoldenStable and
TestCurrentCompactV2WireSemanticsMatchFrozenVersionEdge.
Proof on this tree:
A local npm run check on darwin/arm64 passed (exit 0) on tree
ac69eea with npm 12.2.0, CPython 3.15.0 and Go 1.27.2: 561/561
browser cases in Chromium, Firefox and WebKit with zero retries.
Verify the factual claims in README, ADOPTION, NON_CLAIMS, CONTRIBUTING, SECURITY, the contract map, the release process, the spec overviews, the CLI help and the browser UI strings against the code, the CLI contract, tests, registry data and real runs of the built CLI. Correct the claims that this verification found false or stale: - ADOPTION, agent-workflow overview, contract map: new repository transaction journals use schema v3 for presence and absence; v2 is only a retained absence-bearing version. The downgrade guidance now covers retained v2 and v3 evidence. In ADOPTION, only new v3 journals require this or a later binary; earlier releases already read v2 terminal receipts. - ADOPTION comparison note: the OpenSpec and StrictDoc releases were pinned and were not the newest available on that date, and the exact versions are recorded in the private summary, not in the run log. - SECURITY: remove staged-import wording; the runtime surfaces and the release process exist in this repository. Add TestContractMapDocStatesLifecycleContractVersions. It derives the contract map's lifecycle version sentences and the new-journal sentences of ADOPTION and the agent-workflow overview from the shipped contract, because the journal version statements in these three owner surfaces drifted after #163 introduced v3 journals. Record two proof rules in AGENTS.md under Proof And Gates. They meet the durable-rule criteria: - Confirmed repeatable weakness: in 16 incidents in the recent pull request chain and 5 earlier ones, a witness or an expected value encoded the defect, was too weak, or was edited to fit a change instead of the requirement. The EPIPE early-refusal race in the CLI test transport was fixed at one site and was then found 4 times before its class was swept. - Owner: the author of the change; review checks it. - Trigger: a change that alters behavior covered by a requirement or its witness, or edits an expected value; a fix to a reusable mechanism. - Proof path: review confirms that a falsified requirement clause was changed explicitly or escalated, and that every other site of the mechanism was fixed or recorded. - Rejected lower-cost alternative: relying on review and the full gate. They caught these incidents late, at the cost of review-fix rounds, a failed 13-minute gate, an inserted pull request and restacks. Proof on this tree: A local npm run check on darwin/arm64 passed (exit 0) on tree 8648f63 with npm 12.2.0, CPython 3.15.0 and Go 1.27.2: 561/561 browser cases in Chromium, Firefox and WebKit with zero retries.
iperev
marked this pull request as draft
October 15, 2026 14:32
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
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.
PR 11 of the 2026-10 completion chain. Base:
chain/s1-schema-completeness(the structural contract completeness PR,test(contracts): prove structural contract completeness with a verified lower bound for native ownership). Exactly one commit on top of it; merge only after it.What changes
The factual claims in README, ADOPTION, NON_CLAIMS, CONTRIBUTING, SECURITY, the contract map, the release process, the spec overviews, the CLI help and the browser UI strings were checked against the code, the CLI contract, tests, registry data and real runs of the built CLI. This PR corrects the claims that this verification found false or stale:
ADOPTION.md, the agent-workflow overview,docs/proofkit-contract-map.md): new repository transaction journals use schema v3 for presence and absence; v2 is only a retained absence-bearing version. Present-only v1 and absence-bearing v2 journals and historical v1 receipts remain readable. The contract map's downgrade guidance now covers retained v2 and v3 evidence: finish recovery before downgrading, and retained evidence needs a binary that reads it. InADOPTION.md, only new v3 journals require this or a later binary; new identity-bound terminal receipts stay at schema v2, which earlier releases already read.ADOPTION.md): the OpenSpec and StrictDoc releases of the 2026-10-11 comparison were pinned and were not the newest available on that date. The exact versions are recorded in a private summary, not in the run log; both stay private review evidence and are not shipped.SECURITY.md: the staged-import wording is removed, because the runtime surfaces and the release process exist in this repository.Witness.
TestContractMapDocStatesLifecycleContractVersionsderives the expected sentences from the shipped CLI contract: the contract map's adoption materialization input version, lifecycle output version and fresh journal version, and the new-journal sentences ofADOPTION.mdand the agent-workflow overview. A version bump that leaves one of these owner surfaces behind fails it. The journal statements in these three surfaces had drifted after #163 introduced v3 journals.Two proof rules in
AGENTS.md(Proof And Gates).They meet the repository's criteria for a durable rule:
Compatibility
Not breaking. Documentation, two rules in
AGENTS.mdand one new test. No command, flag, schema, contract identity or CLI contract byte changes.Proof
Proof: A local npm run check on darwin/arm64 passed (exit 0) on tree 8648f63f73ab with npm 12.2.0, CPython 3.15.0 and Go 1.27.2: 561/561 browser cases in Chromium, Firefox and WebKit with zero retries.
TestContractMapDocStatesLifecycleContractVersions(internal/app/canonical_path_contract_test.go).Non-claims