Skip to content

fix(contracts): describe producer-emitted members in compose output schemas - #224

Merged
iperev merged 1 commit into
mainfrom
chain/r0-release-0-17-subject-fixes
Oct 20, 2026
Merged

iperev merged 1 commit into
mainfrom
chain/r0-release-0-17-subject-fixes

Conversation

@iperev

@iperev iperev commented Oct 17, 2026

Copy link
Copy Markdown
Contributor

Pre-release corrections for 0.17.0. A read-only release-readiness review of main (the reviewed stack after #222) found that three compose output schemas understate what their producers always emit, that the change record misstates or omits some consumer-visible changes, and two small shipped-text gaps. This single commit fixes them before the 0.17.0 subject is tagged.

What changes

Output schemas (no contractId, schemaVersion or output-byte change).

  • registry-consumer-proof-input-compose: registryConsumerInput.input.releaseAuthorityInput was published as an optional value of any type, although the producer always emits the admitted release-authority input. It is now required and described by the schemaVersion 3 release-authority input structure, with channel registry_release, rolloutClaim false and the non-null registry members.
  • requirement-coverage-input-compose and requirement-context-compose: the binding selection now requires changedPaths, ownerIds and requirementIds, which the producer always emits.
  • Only the output schemas change; the input shapes used by native admission are untouched. The remaining looser members and the other output structures that embed input structures are listed in the commit message.

Change record (release/change-record.v2.json, pinned copy in record_test.go).

  • Corrects the claim that diagnostic changes leave stdout unchanged: the unsupported-field count replaces caller key names in some envelope and failed-report text.
  • Declares the rollback owner and versionPin redaction for gradual-adoption and adoption-contract-envelope --mode adoption, and the changed anchor IDs of static HTML views, with migration steps.
  • Corrects the $defs embedding migration advice; some variants also reference owner-named root $defs.
  • Declares the output schema corrections above and states, as a non-exhaustive known limitation, that output schemas may admit values their producers never emit.
  • Now 33 breaking changes and 11 additions against 0.16.0.

Shipped text. CLI help says the contract publishes structural JSON Schemas instead of "root JSON shapes". LICENSE names the Go standard library among the bundled BSD-3-Clause components, and a test requires it.

Compatibility

Not breaking. Command behavior and JSON output bytes are unchanged; the help pages differ only by the corrected phrase. Contract identities are unchanged under the contract-identity rule.

Proof

  • A local npm run check on darwin/arm64 passed (exit 0) on tree 397c987e8043 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.
  • New falsifiers: consumer-evidence and inventory-coverage oracles and a commandcontractgen test refuse the impossible values the old schemas accepted, and pass on every real output; the LICENSE test fails on the previous LICENSE.
  • A sweep of 31,366 CLI invocations validated every real output and admitted input against the new contract: none rejected, every published variant produced.
  • Independent adversarial review and adjudication: approved with four minor fixes, all included.

Non-claims

  • Not a release: no tag, registry publication or provider change.
  • Output schemas remain a structural description; native admission stays authoritative, and the known limitation records the remaining looseness.
  • Follow-ups: an SBOM component for the Go standard library, Linux arm64 CI, a refreshed README screenshot, and updating requirement statements that still use root-shape wording.

…chemas

Three composition output schemas reused a caller-input structure for a
member that their producer always re-serializes, so they admitted values
the producer never emits:

- registry-consumer-proof-input-compose: a materialized
  registryConsumerInput now requires input.releaseAuthorityInput and
  describes it with the release-authority input structure of
  schemaVersion 3, refined to channel registry_release, rolloutClaim
  false, a non-null registryAuthority and a present non-null package
  publishConfigRegistry. Build materializes registryConsumerInput only
  for a passed composition, and a passed composition requires these
  values. The previous schema admitted any JSON value or no value there.
- requirement-coverage-input-compose and requirement-context-compose: a
  non-null proof-binding selection now requires changedPaths, ownerIds
  and requirementIds, which requirementbinding.InputValue always emits.
  The refinement applies only to these two output schemas; snapshot and
  binding input admission keep the members optional.

ContractIds and wire schemaVersions are unchanged, and the three
commands emit the same JSON output bytes as before. In the contract only the
three output definitions, the root definition digests that reference
them and the native source digests of the five edited packages change;
the generated Go projections follow.

Command help pages name structural JSON Schemas instead of root JSON
shapes among the surfaces that proofkit/cli-contract.v2.json owns.
LICENSE names the Go standard library among the bundled BSD-3-Clause
components; the reproduced Go Authors notice already covered it.

The 0.17.0 change record now declares where the unsupported-field count
reaches stdout, rollback text redaction in gradual-adoption reports as a
breaking change, the new static HTML anchor IDs, the changed
requirement-browser-server non-claim and the element-wise
conformance-profile nonClaims comparison. It corrects the embedding
instruction for variant schemas, scopes the native-evidence-guidance
change to help, moves the native test observation rule to source-checkout
coverage tooling, declares the structural-text corrections of
directions that 0.16.0 already published and the corrections above, the
help stanza and the LICENSE text, extends the migration step for
consumers keyed on changed values, and adds one known limitation on
output schema precision. The record has 33 breaking changes and 11
additions, and the pinned copy in the releasechange test is regenerated
from it.

Tests:
- The consumer-evidence oracle refuses a passed composition output whose
  releaseAuthorityInput is absent, 0, {}, [0], "x" or null, or carries
  schemaVersion 2, channel tarball_pilot, rolloutClaim true, a null
  registryAuthority or a null or absent publishConfigRegistry, while the
  registry-consumer input schema still admits each of these children. Its
  generic boundary sweep now walks the composed release-authority input.
- The inventory-coverage oracle refuses an empty selection or a missing
  selection member in real coverage-compose and context-compose outputs,
  while the receiving coverage-view and context-slice input schemas still
  admit them.
- The commandcontractgen test pins the composed structure to the
  registry-consumer and release-authority owner projections plus exactly
  these refinements.
- The four oracles that replay recorded help streams declare the help
  stanza delta.
- Re-pinned from test output after confirming the cause: the public CLI
  ABI hash, eleven compact union hashes of contract records whose native
  source digests or root definition digest changed, and the
  coverage-compose output mutant record, which gains the three required
  selection members.
- The repository LICENSE test requires the bundled-components line to name
  the Go standard library.

Members of the refined structures that keep the input structure's
domain:
- registry-consumer-proof-input-compose: registryConsumerInput.proof
  stays optional and nullable and keeps the input domains of its
  members, although a passed composition fixes its nine lock and pack
  booleans, releaseAuthorityReportKind, releaseAuthorityState and
  tempConsumerLocation; the composed release-authority input keeps an
  optional registryPublishDryRunProofId and the input domains of
  manifestPrivate, dependencyPinType and the three consumerContract
  booleans.
- requirement-coverage-input-compose and requirement-context-compose: the
  selection stays optional and nullable with nullable members,
  bindings[].witnessSelectors stays nullable, and witnessCommands keep
  the singular environmentClass alternative.

Other output structures embed a caller-input structure for a member
their producer emits and are not refined by this change:
- requirement-coverage-input-compose: requirementSource,
  compactProofContract, coverageUniverse, ownerInvariantRegistry,
  localEnvironmentPolicy and options.
- requirement-context-compose: projections.specTree and
  projections.requirementSources.
- requirement-context-slice, and the one-shot submitted context of
  requirement-browser-server and view: proof-binding fragment members.
- selective-gate-obligation-decision-input, requirement-impact-input-compose
  and requirement-source-conversion: the whole output.
- requirement-proof-source-set: the compact proof contract it emits.
- requirement-authoring-plan: the requirement source preview.
- requirement-source-view, the requirementCoverage rows of
  requirement-coverage-view and requirement-semantic-diff: members built
  from requirement-source input sub-shapes, not audited member by member.
Optional, nullable or alternative members at these sites may admit values
the producer never emits; the new known limitation covers them.

Follow-ups outside this change:
- The release SBOM lists no component for the statically linked Go
  standard library.
- No CI job executes the Linux arm64 binary or the aarch64 wheel.
- The README workspace screenshot predates later workspace UI changes.
- The statements of REQ-PROOFKIT-WORKFLOW-011, REQ-PROOFKIT-WORKFLOW-018,
  REQ-PROOFKIT-PACKAGE-002, REQ-PROOFKIT-SPEC-011 and
  REQ-PROOFKIT-QUALITY-004 and three overview lines still use root-shape
  terminology for contract declarations; requirement statement changes
  need owner impact and proof-binding review.

Proof on this tree:
A local npm run check on darwin/arm64 passed (exit 0) on tree 397c987 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

iperev commented Oct 20, 2026

Copy link
Copy Markdown
Contributor Author

Reviewed candidate: 098eab7754bf698819e3429e42ada3824b3522e0 -> 01db2f0866456255c08cf38803485ec64e013c52, tree 397c987e80430e4063a865e89082f7bf2b617c2b.

The following corrections are justified; these are not runtime producer fixes:

Correction Contract and counterexample Impact boundary Rejected alternative Preserved behavior
Materialized registry input A passed composer carries the admitted header3 release-authority input. The old output schema accepts a materialized child with that member absent; the new oracle rejects it and the other listed impossible forms. Composer output schema and generated source/digest projections only. Tightening registry-consumer input would change its existing admission/failure boundary; a second hand-written child schema would duplicate native owners. Real outputs validate; the receiving input schema stays unchanged and still accepts the same structural input forms.
Binding selection in both composers requirementbinding.InputValue always emits changedPaths, ownerIds and requirementIds. The old coverage/context output schemas accept {} in their place. The two compose output definitions; catalog proof-binding absence remains supported. Tightening InputShape, requiring every catalog to have a binding, or duplicating the emitted-member policy in both parents. Mutants remain accepted as receiving inputs but fail output validation; direct binary comparisons include empty/omitted selection and catalogs with/without bindings.
Release record and help The previous pending record incorrectly confines all diagnostics to stderr and omits existing rollback redaction and changed HTML anchors; shared-definition expansion alone is not sufficient for every variant. Pending release declarations, the help stanza and exact declared help-stream deltas; not new runtime behavior or publication. Changing runtime to fit old prose, rewriting predecessor corpora, or bumping unrelated input identities. Old observation corpora remain intact; help guards allow only named changes. All input definitions and all command contract IDs are unchanged.
Bundled runtime identification The existing Go Authors notice remains; the bundled-components line now explicitly names the standard library. LICENSE identification line and packaging assertion. Replacing the license or inferring exhaustive SBOM/legal compliance from this text change. Existing notices and package-license expression remain; Python packaging tests pass.

Independent checks include the affected eight Go packages, 59 CLI/schema oracle tests with zero failures/skips, generator freshness, three intentionally failing predecessor-schema controls, and 79 main/head comparisons with identical exit code, stdout and stderr.

The complete local npm run check passed with exit 0 on this clean candidate, including 561 browser cases, package artifacts, self-hosting and release closeout. Two separate fresh-context source reviews returned scoped approval; no additional product changes were needed. Exact-head GitHub checks and protected-base identity are revalidated immediately before squash merge. No release, registry publication, universal schema precision, independent human audit or absence-of-all-defects claim follows.

@iperev
iperev merged commit 75caaf1 into main Oct 20, 2026
12 checks passed
@iperev
iperev deleted the chain/r0-release-0-17-subject-fixes branch October 20, 2026 04:59
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Development

Successfully merging this pull request may close these issues.

1 participant