Skip to content

Structured result and verification contract

The v0.2.x result contract is schema version 1. It is shared by the shipped structured results and is the envelope intended for future certificate replay and snapshot operations. It is deliberately separate from the live registry website and from any mutable database.

Success records

GeneratorSeriesResult.to_dict() and FeketeSzegoResult.to_dict() retain the legacy v0.2.x fields and add the following closed envelope:

  • schema_version: integer contract version (1);
  • result_type: trusted operation name;
  • canonical_inputs: exact, direction-preserving problem inputs;
  • exact_expressions: non-executable display strings and exact output values;
  • exact_expression_dag: a bounded canonical exact-expression DAG. The DAG, not the lossy printer strings, is the authoritative expression identity;
  • method, evidence_status, and computational_status: computational method and evidence state (computational_status is explicit so literature status cannot be mistaken for computational evidence);
  • assumptions: explicit assumptions, not implied claims;
  • source_references: citations or artifact references used by the result;
  • package_version and artifact_versions: software and input-artifact identities;
  • literature_status: separate from computational evidence;
  • novelty_claim: always false in this package candidate;
  • failure_state: null for a success record; and
  • verification: a fail-closed VerificationReport.

Shipped records also require non-empty operation-specific assumptions, source references, and artifact identity keys for the source commit and fixture/proof. provenance is derived as built_in or caller_supplied; it is not an affirmative literature or novelty state. evidence_status is derived from the verification report and the operation kind rather than accepted as a public constructor claim: a failed report becomes unresolved, while a passing report becomes proven_exact_under_declared_assumptions. Evidence and literature statuses are closed package-owned values in this release, and the result-level __all__ surface intentionally remains the shipped operation names rather than exporting every contract helper.

The JSON schema is shipped at geometric_function_atlas/schema/result.schema.json. Unknown top-level, canonical-input, exact-expression, verification-report, and check fields are rejected by the dependency-free validator validate_result_payload. The validator also requires operation-specific canonical/exact keys and checks that the retained v0.1.x fields agree with those canonical values. A passing report must have failure_state: null; a failed report must name one of the explicit failure states and use the same value for computational_status.

Exact expressions are display data, while the bounded exact-expression DAG is the authoritative identity. The validator decodes only the closed opcode set, checks canonical node identity, and recomputes shipped outputs from that DAG; it never parses or executes a caller formula string. Custom generators must still be supplied as preconstructed SymPy expressions using the trusted z symbol; formula strings and undeclared symbols remain invalid.

Verification reports

A VerificationReport contains named VerificationCheck records. Every check records:

  • what was checked (checked);
  • expected and observed values without forced floating-point conversion;
  • pass, fail, or skip status;
  • scope;
  • a failure reason when it fails; and
  • whether it is required for aggregate success.

A report is successful only when it contains at least one required check and all required checks pass. A required skip is not success. Optional checks do not promote a failed required check. This prevents a missing leaf, failed mutation check, or incomplete certificate from being reported as proven.

Failure states and CLI exit codes

Failure records use the separate closed geometric_function_atlas/schema/error.schema.json contract. The states are:

State Meaning CLI code
invalid_input malformed, undeclared, or mathematically invalid input 2
unsupported operation or artifact kind outside the package scope 3
unresolved available evidence cannot discharge the requested claim 4
resource_limit a documented bound prevented symbolic work 5
corrupt_artifact structure or checksum validation failed 6

CLI commands preserve the existing human-readable argparse errors. With --json, failures are emitted as a versioned JSON error record on stdout with no traceback and the stable code above. Without --json, a structured failure prints one concise explanation (status, direction, reason) plus a pointer to --json on stderr.

Radius certificate replay has its own closed envelope, distinct from result.schema.json (which requires a verification report and an expression DAG that radius replay does not emit). Validate the complete gfa verify-radius-certificate SOURCE TARGET --json stdout, including nonzero-exit JSON, against the packaged geometric_function_atlas/schema/radius-replay.schema.json using JSON Schema Draft 2020-12. With the test extra installed, an exact validator call is:

import json
from importlib import resources
from jsonschema import Draft202012Validator

from geometric_function_atlas import verify_radius_certificate

schema = json.loads(resources.files("geometric_function_atlas").joinpath(
    "schema/radius-replay.schema.json").read_text(encoding="utf-8"))
Draft202012Validator.check_schema(schema)
payload = verify_radius_certificate("sine", "sigmoid").to_dict()
Draft202012Validator(schema).validate(payload)

This schema is shipped in wheel/sdist and checks closed top-level, input, expression and step keys, status/method/failure combinations, and certified versus global_containment_check. bounded_chain_replayed means the eight fixture lanes passed their bounded package checks (some inequality steps are recorded analytic premises), not that every global theorem was formally proved by software. The two paper-symbolic routes have symbolic_replay_only, certified: false, not_mechanized; nine other written paper lanes are not_replayable, also not_mechanized. No written-paper label is upgraded by schema validation.

Radius certificate replay keeps "unavailable" separate from "damaged": an unchanged snapshot row that has no bundled replay certificate reports the not_replayable status with the unsupported failure state (exit code 3), and the row keeps its own evidence status. corrupt_artifact (exit code 6) is reserved for malformed records and for any record that is not its unchanged trusted snapshot row, including a reviewed lane whose bundled certificate was removed.

A standard-output broken pipe (for example gfa ... | head when the consumer closes the pipe early) exits with code 1 after silencing the pipe; no traceback is emitted. It is an I/O condition, not an operation failure.

The release gate python scripts/check_clean_install.py <wheel> creates a fresh virtual environment outside the checkout, installs the wheel, exercises the API and trusted registry, mutates a verification record, and checks the bounded-input rejection path through the installed console module.

Collaborator-bundle integrity

write_research_bundle_manifest() records a closed set of relative regular files together with the package version, package source identity, declared entry point, canonical replay parameters, byte counts, and SHA-256 digests. The manifest is deterministic for identical inputs. Paths that are absolute, escape the bundle root, name the manifest itself, or traverse a symlink are rejected; file count and total bytes are bounded before hashing.

verify_research_bundle_manifest() revalidates that structure and fails closed when an artifact is absent, replaced, resized, or changed. It intentionally does not execute the recorded entry point. Bundle verification proves only that the named bytes and replay metadata match the manifest; the mathematical status of each artifact remains whatever its own result or certificate says.

Trusted implementation registry

get_trusted_implementation() resolves only the explicit package-owned names listed by list_trusted_implementations(). Records cannot provide Python import paths, expressions, or code. Future certificate and snapshot readers must use the same closed-registry rule rather than dynamic imports or eval.

Literature boundary

literature_status is not inferred from evidence_status. A computationally exact result can still be not_assessed, known, candidate_improvement, no_extracted_claim, or unresolved in the literature. NO_EXTRACTED_CLAIM does not mean novel, and this package never emits an affirmative novelty_claim.