AI Contract Runner

This lesson is the practical entry point for using Circle Calculus on an AI configuration you provide. The contract pack is the curated public fixture set. The runner is the parameterized tool that turns your values into a theorem-linked receipt.

Goal

Take one AI component, name its finite circular object, run the contract runner, and read the receipt without confusing formal proof, executable computation, and numerical support.

Concept

The runner follows one pattern:

user config
  -> finite circular contract
  -> Python certificate fields
  -> theorem ids from the contract pack
  -> text / JSON receipt
  -> explicit non-claims

The receipt is not a new proof source. Lean remains the formal proof source, and the theorem manifests plus generated contract pack remain the status source.

Picture

RoPE / KV-cache / sparse attention / recurrence schedule
        |
        v
circle-ai-certify ...
        |
        v
contract receipt
        |
        +--> evidence fields
        +--> theorem ids
        +--> recommendations
        +--> validation commands
        +--> request / normalized-request fingerprints
        +--> proof-status summary
        +--> non-claims

A JSON receipt can say that a finite structural field is theorem-backed. It cannot upgrade a numerical scan, benchmark, widget, or engineering guess into a formal theorem.

The runner is not proof by itself. It is an executable reference surface separate from Lean proof status, and it does not make performance claims, model-quality claims, or real-data usefulness claims.

First Run

Start with the RoPE flagship contract:

circle-ai-certify rope \
  --head-dim 128 \
  --base 10000 \
  --context 131072 \
  --requested-margin 1/328459

If you already have a standard RoPE model config.json, import the common fields directly. The --model-config path may be the JSON file itself or the containing model directory with config.json:

circle-ai-certify rope \
  --model-config examples/circle_ai_model_configs/standard_rope_config.json \
  --requested-margin 1/328459 \
  --format json \
  --request-out reports/rope_request.json \
  --request-validation-report-out reports/rope_request_validation.json \
  --model-config-import-report-out reports/rope_import.json \
  --require-status proved \
  --require-decision passed \
  --require-assurance mixed_theorem_and_computation \
  --require-passed

The importer reads explicit RoPE dimensions such as rotary_dim, rotary_emb_dim, rotary_ndims, qk_rope_head_dim, or rope_head_dim; otherwise it reads head_dim or hidden_size / num_attention_heads, optional partial_rotary_factor or rotary_pct, base/theta fields rope_theta, rope_base, rotary_emb_base, rotary_base, or rotary_theta, and max_position_embeddings, max_seq_len, max_seq_length, max_sequence_length, model_max_length, seq_len, context_length, seq_length, or n_positions. Explicit CLI flags override inferred values. Non-default rope_scaling metadata is rejected because the current receipt does not prove scaled-RoPE semantics. head_dim must be even because the current RoPE contract models rotary dimension pairs. Use --model-config-import-report-out reports/rope_import.json when CI needs a schema-validated explanation of whether a real config converted into the standard-RoPE request frontier. That report is not a receipt and does not prove scaled-RoPE behavior. For partial-rotary configs, it records both the head dimension field and the rotary-fraction field used to derive the certified rotary sub-dimension; when an explicit rotary-dimension field is present, the fraction is not applied again. It includes fingerprints for the source config and the emitted request when one exists, so CI can pin the import boundary. Its parameter_sources object records whether each standard-RoPE request parameter came from an explicit override, a config field, derived config fields, a default, or an omitted optional input. The saved request is the exact versioned Circle request object used to produce the receipt, so downstream tools can pin it before rerunning or auditing the certificate. Use --request-validation-report-out reports/rope_request_validation.json to save the schema-validated preflight report for that same request. The --require-* flags are CI gates: the receipt is still printed or written, then the command exits nonzero if the requested status/pass policy is not met. Use --json-out reports/rope_receipt.json when CI also needs the receipt saved as a file. Use --format compact-json when a downstream tool needs a small stable object instead of the full audit receipt:

circle-ai-certify rope \
  --head-dim 128 \
  --base 10000 \
  --context 131072 \
  --requested-margin 1/328459 \
  --format compact-json \
  --compact-json-out reports/rope_compact_receipt.json

The compact receipt is validated against site/data/generated/circle_ai_contract_compact_receipt.schema.json. It keeps the decision, proof-status summary, selected evidence fields, theorem ids, validation commands, non-claims, and fingerprints, including the full receipt_content_fingerprint. It does not replace the full receipt for audit or replay.

For a downstream project that already has several versioned Circle request files, standard RoPE model configs, or AI architecture configs, use the installed package batch mode:

circle-ai-certify batch \
  --request-file examples/circle_ai_requests/kv_cache_request.json \
  --request-file examples/circle_ai_requests/sparse_attention_request.json \
  --model-config-file examples/circle_ai_model_configs/standard_rope_config.json \
  --architecture-config-file examples/circle_ai_architecture_configs/basic_transformer_contract_config.json \
  --artifact-dir reports/circle_ai_contract_batch \
  --artifact-prefix architecture-suite \
  --require-passed \
  --require-status proved \
  --require-decision passed \
  --format json

That writes a portable handoff directory with subdirectories for full receipts, compact receipts, model-config import reports, architecture-config import reports, request-validation preflight reports, certification bundles, and bundle checks, plus one runner-check report named from the artifact prefix. The runner-check schema id is circle_calculus.ai_contract_runner_check.v0. Model-config summaries include parameter-source provenance, so a downstream reader can see whether RoPE values came from config fields, derived fields, explicit overrides, defaults, or omitted optional inputs. Architecture-config summaries include parameter-source provenance for the architecture-derived receipts emitted from that config. For RoPE, architecture sections such as rope, model, or transformer may provide an explicit rotary/head dimension or a hidden-size plus attention-head-count pair; the import report records the fields used and does not treat unrelated architecture fields as part of the theorem-linked claim. The default batch emits RoPE, KV-cache, sparse-attention, and recurrence receipts; pass --architecture-config-kind to restrict the set. For model-only or otherwise partial architecture files, set circle_ai_contract_kinds, for example ["rope"], to restrict that one file without changing the whole batch command. It is the package-native batch handoff path and does not require importing repository-only scripts. Use the explicit --receipt-out-dir and related directory flags only when a downstream CI system needs a custom layout instead of the standard artifact directory. Add --require-no-unsupported-architecture-fields when the generated runner-check report should fail if an architecture config contains fields that Circle did not map into a theorem-linked request. Add --require-no-unsupported-model-config-fields when standard-RoPE model-config imports should reject unsupported model features rather than only reporting them.

After copying that directory into another project, a standard-library verifier can check the runner report and every named sidecar without importing Circle:

python examples/downstream_ci_verify_circle_ai_batch.py \
  reports/circle_ai_contract_batch/architecture-suite_runner_check.json \
  --require-status proved \
  --require-decision passed \
  --require-passed \
  --require-kind rope_position_distinguishability \
  --require-kind kv_cache_ring_buffer \
  --require-kind sparse_attention_coverage \
  --require-kind recurrence_schedule

The verifier output preserves unsupported architecture-config field counts and names. A model-only config that declares circle_ai_contract_kinds: ["rope"] still reports extra fields such as model.model_type as unsupported rather than folding them into the theorem-linked request. Add --require-no-unsupported-architecture-fields when downstream CI should fail on that boundary instead of accepting the receipt with an explicit non-claim. For standard-RoPE model configs, add --require-no-unsupported-model-config-fields to reject unsupported model-config features at the same batch gate. The verifier also validates the runner report’s own gate_policy, example_count, and selected_kinds, so stale reports with mismatched metadata or missing current policy fields fail before being accepted as CI evidence. Accepted verifier reports include a reusable pin_policy; pass that report back with --pin-policy to reject a future runner-check whose gate_policy has drifted from the pinned CI contract. Each runner summary includes both theorem_count and the concrete theorem_ids cited by that receipt, plus resolved/proved booleans and any unresolved or unproved theorem ids. When --artifact-dir is used, the batch command also writes an artifact manifest and manifest-check that fingerprint the runner report and every emitted receipt, compact receipt, import report, preflight, bundle, and bundle-check sidecar. The copyable verifier checks the manifest automatically when the runner report names it; --artifact-manifest is only needed for older or relocated reports. The top-level report records artifact_manifest_path, artifact_manifest_check_path, validation_commands, required_kinds, and kind_counts, so a batch consumer can assert that RoPE, KV-cache, sparse-attention, recurrence, or another contract family was actually emitted instead of merely trusting that a full architecture-contract run happened. Use circle-ai-certify batch --require-kind kv-cache or the copyable verifier’s --require-kind option when CI should reject a missing family before accepting the batch as evidence. When the batch command runs in text mode, it also prints each verifier command as a validation_command=... line and includes the artifact_manifest=... and artifact_manifest_check=... paths for copyable human handoffs. Each source line includes unsupported_model_fields=... and unsupported_architecture_fields=..., so the terminal log keeps the same import-boundary signal as the JSON report.

Python callers can build the same schema-valid runner-check report in memory with build_contract_runner_check_report. The helper accepts versioned request objects, standard RoPE model_configs, and AI architecture_configs. When architecture_configs is populated, it emits RoPE, KV-cache, sparse-attention, and recurrence summaries by default; pass any supported architecture_config_kinds list to restrict the contract families. This is the library path for downstream systems that already load configs and want the same pass/fail report without a subprocess. Pass required_kinds=("rope", "kv-cache", ...) when the in-memory runner report should fail unless the batch contains those contract families. Pass require_no_unsupported_architecture_fields=True when that in-memory report should reject architecture configs with source fields that were not mapped into the theorem-linked request.

Use --gate-report-out reports/rope_gate.json for a compact pack-aware pass/fail report, --receipt-check-out reports/rope_receipt_check.json for a saved receipt validation report, and --receipt-replay-check-out reports/rope_replay.json to rebuild the receipt from its embedded request and compare stable fingerprints. Use --certification-bundle-out reports/rope_bundle.json with --certification-bundle-check-out reports/rope_bundle_check.json when the installed command should also archive the request preflight, theorem-linked receipt, gate report, model-config provenance when present, and bundle verification result. Use --artifact-manifest-out reports/rope_manifest.json with --artifact-manifest-check-out reports/rope_manifest_check.json when the installed command should fingerprint every sidecar file it wrote and verify the manifest. Use --artifact-dir reports/rope_contract when the installed command should choose stable names for the request, request-validation report, receipt, diagnostics, certification bundle, manifest, and check-report set.

The repository-only python scripts/circle_ai_certify.py runner adds heavier audit workflows such as pin-policy checks, request preflight-only reports, and whole-directory artifact bundles. Use that script when a handoff needs the full repository audit trail rather than an installed-package receipt, batch request report, certification bundle, explicit artifact manifest, or package-managed artifact directory.

Expected shape:

circle_ai_contract_receipt=proved kind=rope_position_distinguishability ...
proof_status=theorems=... resolved=True proved=True ...
proof_layers=proved_fields=... computed_fields=... numerical_only_fields=... unsupported_fields=...
rope_exact_discrete=pass=True ...
rope_d19_request=status=proved theorem_backed=True ...
rope_d19_bank_bridge=applies=True radian_bank_form=True ...
rope_rational_turn_ratio=numerator=1 denominator=4099 pass=True requested_status=proved ...
rope_nearest_integer_bridge=applies=True positive_gaps=131071 theorem_backed=True ...
rope_dirichlet_guardrail=applies=True inv_context_margin=1/131072 ...
not_claimed=...

Read that as:

Field	Meaning
status=proved	the requested D19 channel-0 margin branch is theorem-backed in the proved range
request_passed=True	the requested margin is accepted by the current theorem-backed classifier
rope_exact_discrete	exact integer-period phase-bank result for the declared discretization model
standard_channel0_d19_bank_bridge	conditional first-channel bank no-near-turn payload backed by AIRA-T0171, AIRA-T0172, and AIRA-T0234 through AIRA-T0237 when its context/margin premises pass
rational_turn_ratio_finite_margin_certificate	theorem-backed finite nearest-integer margin certificate for an explicitly declared rational/discretized scalar turn ratio such as 1/4099
rope_nearest_integer_bridge	theorem-backed bridge saying a real-phase finite margin certificate reduces to finite floor/ceiling nearest-integer checks over positive in-context gaps
rope_dirichlet_guardrail	theorem-backed 1/context upper-bound guardrail from AIRA-T0239 through AIRA-T0241
rope_real_phase_scan	numerical diagnostic only
not_claimed	boundary that prevents model-quality or full all-channel real-RoPE overclaims

The guardrail rejects requested margins strictly above 1/context. It does not prove margins at or below that ceiling; those still need the D19 classifier or a future sharper real-phase theorem. For smaller contexts below the D19 obstruction range, the receipt can still be proved when the standard_channel0_d19_bank_bridge applies: that bridge is a conditional one-separating-channel theorem for a finite bank whose first frequency is standard channel 0, not an independent all-channel margin theorem. For rationalized or discretized phase policies, pass --turn-ratio-numerator N --turn-ratio-denominator D to certify the declared scalar turn ratio N/D. This is a separate proof-carrying lane from the standard irrational RoPE schedule.

Nine Runner Surfaces

Surface	Command	What The Receipt Checks
RoPE	python scripts/circle_ai_certify.py rope --head-dim 128 --base 10000 --context 131072 --requested-margin 1/328459	exact integer-bank pass/fail plus optional D19 real-phase request classification or declared rational/discretized turn-ratio certificate
KV-cache	python scripts/circle_ai_certify.py kv-cache --cache-size 16 --current 31 --token 20 --batch-tokens 20,24,29,31 --sink-size 4	retained-window, stale-member, live-window, and optional sink-plus-rolling-window request facts
Sparse attention	python scripts/circle_ai_certify.py sparse-attention --context 120 --strides 7,13 --path-length 3 --local-window 4	covered lags, uncovered gaps, repair windows, and candidate-budget fields
Recurrence	python scripts/circle_ai_certify.py recurrence	finite loop budget, active work, inactive work, exit step, and whole-period shift invariants
Strided fanout	python scripts/circle_ai_certify.py strided-fanout	finite strided candidate reachability, visited count, and path-budget accounting
Cyclic memory	python scripts/circle_ai_certify.py cyclic-memory	residue slot, winding, and cyclic event-bank address facts
Multicoil phase	python scripts/circle_ai_certify.py multicoil-phase	period-bank residues, repeat horizon, and relative phase features
Cyclic mixer	python scripts/circle_ai_certify.py cyclic-mixer	circulant and block-cyclic parameter accounting for mixer layouts
Seed rule	python scripts/circle_ai_certify.py seed-rule	exact regeneration and storage-accounting facts for a deterministic finite generator

The last five rows expose compact ready contracts from the same proof-carrying pack. They are useful as structural certifiers and fixture sources; they do not claim better training, inference quality, retrieval quality, or hardware efficiency.

For project-level configs, the runner can translate a small architecture JSON into a versioned request for explicit RoPE, KV-cache, sparse-attention, or recurrence surfaces:

python scripts/circle_ai_certify.py rope \
  --architecture-config examples/circle_ai_architecture_configs/basic_transformer_contract_config.json \
  --architecture-config-import-report-out reports/rope_architecture_import.json \
  --format json \
  --require-passed

python scripts/circle_ai_certify.py sparse-attention \
  --architecture-config examples/circle_ai_architecture_configs/basic_transformer_contract_config.json \
  --architecture-config-import-report-out reports/sparse_architecture_import.json \
  --format json \
  --require-passed

The adapter reads documented sections such as rope, kv_cache, sparse_attention, and recurrence, plus aliases like rotary_dim, rope_theta, context_length, sliding_window, max_hops, max_recurrence_steps, horizon_steps, loop_budget, tokens, and block_width. For recurrence, shift_amount is accepted only when it is a nonnegative exact multiple of loop_period; the import report then records the canonical shift_passes value as a derived config field. An explicit --shift-amount override is recorded as a derived explicit source in the same report. The config import is provenance only; the receipt remains the theorem-linked artifact. The saved import report is validated against site/data/generated/circle_ai_architecture_config_import.schema.json; it records the source config fingerprint, the emitted request fingerprint, and which field or explicit override supplied each request parameter. It also lists unsupported target-section fields so extra architecture behavior is visible but not silently promoted into the theorem-linked receipt. In default text mode, config-backed runs also print a source_config= line with the source path, source config fingerprint, derived request kind, unsupported architecture-field count/names, and request fingerprint, so a terminal log can be replayed or pinned later. When --certification-bundle-out is also used with --architecture-config, that same architecture import report is embedded in the bundle beside the request preflight, receipt, and gate report.

For KV-cache requests with positive --sink-size, the human receipt includes a kv_cache_sink_window= line with the generated pinned-prefix plus rolling-window request size, exact-policy flag, distinct-token flag, and sink-token retention facts. When sink_size = 0, the sink certificate is not listed as a proved field. This keeps the StreamingLLM-style sink-token contract visible without claiming retrieval quality, throughput, memory savings, or serving-stack correctness.

For recurrence requests, the human receipt includes recurrence_post_period= and recurrence_periodic_shift= lines. These expose the post-period work-saving extension and the whole-period token-shift invariants as finite schedule facts. They do not claim better reasoning, adaptive-exit quality, speed, or model performance.

For sparse-attention requests, the human receipt includes sparse_intervals=, sparse_interval_repair=, sparse_repair_plan=, and sparse_collision_accounting= lines. These expose the first uncovered lag interval, the largest uncovered interval, the complete local repair threshold, the deterministic interval-repair plan, and lag/query candidate alias severity. They are finite coverage and budget facts, not claims about attention quality, layout optimality, runtime speed, or model accuracy.

Use --format json when another project will consume the full audit result:

python scripts/circle_ai_certify.py sparse-attention \
  --context 120 \
  --strides 7,13 \
  --path-length 3 \
  --local-window 4 \
  --format json \
  --request-out reports/sparse_attention_request.json \
  --json-out reports/sparse_attention_receipt.json \
  --require-status proved

Use --format compact-json for a smaller pass/fail receipt view when the consumer only needs proof status, selected evidence fields, non-claims, and fingerprints. The compact object includes selected_evidence_proof_layers, which labels each selected evidence path as proved, computed, numerical_only, unsupported, mixed, or unclassified. For sparse-attention receipts, the selected evidence includes lag-side and query-side no-collision booleans, dedup-loss counts, pair-collision counts, pair-count-bounds-dedup-loss checks, and unique-plus-loss-equals-raw accounting. The compact view also carries selected fields for strided fanout, cyclic memory, multicoil phase features, cyclic mixers, and seed-rule regeneration. Fields outside the theorem-backed minimum consumer set are labeled computed, not proved.

Add --request-validation-report-out reports/request_validation.json when a single-config run should also save the schema-validated preflight report for the exact request that produced the receipt. Add --certification-bundle-out reports/certification_bundle.json when CI wants one schema-validated artifact containing request preflight, receipt, gate report, and any model-config or architecture-config import report that records parameter provenance. If strict config-import gates are enabled, the bundle and its embedded gate report also carry those import-boundary failures. In text mode, config-backed runs print source provenance before any artifact paths, making the source config fingerprint visible even when no sidecar is written.

For a project that already stores configs as files, use the request schema:

{
  "schema_id": "circle_calculus.ai_contract_request.v0",
  "kind": "rope_position_distinguishability",
  "parameters": {
    "head_dim": 128,
    "base": 10000.0,
    "context": 131072,
    "requested_margin": "1/328459"
  }
}

Then run:

python scripts/circle_ai_certify.py request \
  --request-json reports/rope_request.json \
  --format json \
  --json-out reports/rope_receipt.json \
  --receipt-check-out reports/rope_receipt_check.json

Preflight a request before issuing a receipt:

python scripts/circle_ai_certify.py request \
  --request-json reports/rope_request.json \
  --validate-only \
  --format json \
  --json-out reports/request_validation.json

The validate-only report is checked against site/data/generated/circle_ai_contract_request_validation.schema.json before it is printed or written. It includes the request-content fingerprint so CI can pin the exact request JSON that was preflighted.

Every emitted receipt is checked against site/data/generated/circle_ai_contract_receipt.schema.json and then validated against the loaded contract pack before it is printed or written. The pack-aware check covers the claimed pack fingerprint, contract fingerprint, contract id, and theorem-id membership. Use --receipt-schema to pin a generated schema path in a downstream project. By default, emitted receipts are issued against site/data/generated/circle_ai_contract_pack.json, the same public pack used by the saved-receipt verifier. Use --pack only when intentionally testing a different generated pack. Use --receipt-check-out with --json-out to write the same schema-validated pack-aware check report that a later scripts/check_circle_ai_receipt.py run would produce for the saved receipt. Use --gate-report-out without --json-out to write the same report shape for the in-memory receipt. Strict model-config and architecture-config import gate failures are included in this sidecar before the command exits:

python scripts/circle_ai_certify.py rope \
  --head-dim 128 \
  --base 10000 \
  --context 131072 \
  --requested-margin 1/328459 \
  --gate-report-out reports/rope_gate.json \
  --require-status proved \
  --require-decision passed \
  --require-assurance mixed_theorem_and_computation \
  --require-passed

Use --certification-bundle-check-out with --certification-bundle-out when a single config run should leave behind the portable bundle and the CI-facing verification report for that bundle:

python scripts/circle_ai_certify.py rope \
  --head-dim 128 \
  --base 10000 \
  --context 131072 \
  --requested-margin 1/328459 \
  --json-out reports/rope_receipt.json \
  --certification-bundle-out reports/rope_certification_bundle.json \
  --certification-bundle-check-out reports/rope_certification_bundle_check.json \
  --require-status proved \
  --require-decision passed \
  --require-assurance mixed_theorem_and_computation \
  --require-passed

In text mode, the certifier prints an artifacts= line listing every request, receipt, gate, bundle, or check file written by that invocation. Use --artifact-dir reports/rope_contract when you want the standard audit set without naming every file. It fills unset paths for:

<prefix>_request.json
<prefix>_request_validation.json
<prefix>_model_config_import.json       # RoPE model-config runs only
<prefix>_architecture_config_import.json # architecture-config runs only
<prefix>_receipt.json
<prefix>_receipt_check.json
<prefix>_receipt_replay_check.json
<prefix>_gate_report.json
<prefix>_certification_bundle.json
<prefix>_certification_bundle_check.json
<prefix>_artifact_manifest.json
<prefix>_artifact_manifest_check.json

The default prefix is the request or model-config filename stem when available, otherwise the contract family name. Use --artifact-prefix to override it. The manifest indexes the generated files, their schema ids, and their file SHA-256 hashes. The manifest-check report re-hashes those indexed files and verifies the manifest’s mirrored receipt status fields. When a _receipt_replay_check.json sidecar is present, the manifest-check report also requires that replay report to be ok, that its replay command matches the embedded request, that its installed-package replay command also matches, that all replay comparison fields match, and that its original and replayed receipt fingerprints match the saved receipt. The saved _receipt_check.json, _gate_report.json, and _certification_bundle_check.json sidecars are also audited: each must be ok, use the manifest’s gate policy, and point back to the same receipt fingerprint. Request preflight sidecars are checked too: _request_validation.json, RoPE _model_config_import.json, and _architecture_config_import.json must be ok and must point back to the same request fingerprint. Pass the dependency-pin flags below directly to scripts/circle_ai_certify.py with --artifact-dir when the first generated _artifact_manifest_check.json should already carry and enforce the reusable pin_policy.

Verify the whole artifact directory from the manifest:

python scripts/check_circle_ai_artifact_manifest.py \
  reports/rope_contract/standard_rope_config_artifact_manifest.json \
  --report-out reports/rope_contract/standard_rope_config_artifact_manifest_check.json

That checker re-hashes every referenced file, validates declared content schema ids, and confirms the manifest’s status fields still match the saved receipt. It also audits any saved replay-check sidecar against the receipt fingerprint, so stale replay reports fail the whole artifact directory instead of being silently listed as extra files. The receipt-check, gate-report, and bundle-check sidecars get the same semantic treatment: if a downstream job updates their file hash but leaves stale receipt facts inside, the manifest check still fails. Request-validation and model-config import sidecars are also checked against the manifest request fingerprint. It also accepts --require-kind, --require-theorem-id, --require-evidence-field, --require-recommendation-id, and --require-validation-command for first-party CI jobs that need the same policy pins as the copyable standalone verifier. For RoPE model-config imports, add --require-model-config-fingerprint FINGERPRINT with the SHA-256 value from the import report when CI must pin the exact source config.json. For architecture-config imports, add --require-architecture-config-fingerprint FINGERPRINT with the SHA-256 value from the architecture-config import report. Use --require-normalized-param KEY=JSON_VALUE to pin the parameter value a downstream job depends on. For a copyable standard-library-only downstream gate, use examples/downstream_ci_verify_circle_ai_artifacts.py; it performs the same artifact-integrity checks without importing Circle or jsonschema. It also accepts --pin-policy with either a whole prior report or just the pin_policy object, and its JSON report records the merged pin_policy for replay. The standalone verifier also validates architecture_config_import_report sidecars against the manifest request fingerprint and supports the same architecture-config fingerprint pin. The standard artifact-directory path and standalone verifier are checked for all nine ready receipt families, so downstream CI can use the same gate shape across the current contract suite. When a downstream job emits multiple manifests, add --require-kind for each contract family that must be present; the verifier fails if any required family is missing. Add --require-theorem-id THEOREM_ID when the downstream job depends on a specific theorem appearing in at least one saved receipt artifact. Add --require-evidence-field FIELD or --require-recommendation-id ID when automation consumes a specific receipt field or planner recommendation. Add --require-validation-command COMMAND when CI depends on an exact recheck command emitted by the receipt. Add --require-model-config-fingerprint FINGERPRINT when a RoPE artifact directory was produced from a model config.json and CI must pin that source config hash. Add --require-architecture-config-fingerprint FINGERPRINT when an artifact directory was produced from an architecture config and CI must pin that source config hash. Add --require-normalized-param KEY=JSON_VALUE when CI needs to pin a top-level normalized_request value such as head_dim=128 or sequence_length=32. First-party check reports include a pin_policy block recording these requested dependencies, so audit logs show both what was required and what was observed. Reuse that policy later with --pin-policy reports/check_report.json; the checker accepts either the whole report or just the pin_policy object, and explicit --require-* flags are merged with the loaded pins. scripts/circle_ai_certify.py --artifact-dir ... --pin-policy reports/check_report.json accepts the same shape when regenerating a contract artifact set under a previously saved dependency policy.

Checked-in examples are available for all nine runner surfaces:

examples/circle_ai_requests/rope_request.json
examples/circle_ai_requests/rope_rational_turn_ratio_request.json
examples/circle_ai_requests/kv_cache_request.json
examples/circle_ai_requests/sparse_attention_request.json
examples/circle_ai_requests/recurrence_request.json
examples/circle_ai_requests/strided_fanout_request.json
examples/circle_ai_requests/cyclic_memory_request.json
examples/circle_ai_requests/multicoil_phase_request.json
examples/circle_ai_requests/cyclic_mixer_request.json
examples/circle_ai_requests/seed_rule_request.json

Check those examples and their generated receipts with:

python scripts/check_circle_ai_contract_runner.py

For a directory of request files, write all generated receipt JSON files:

python scripts/check_circle_ai_contract_runner.py \
  --example-dir examples/circle_ai_requests \
  --receipt-out-dir reports/circle_ai_receipts \
  --compact-receipt-out-dir reports/circle_ai_compact_receipts \
  --model-config-import-report-out-dir reports/circle_ai_imports \
  --architecture-config-import-report-out-dir reports/circle_ai_architecture_imports \
  --request-validation-report-out-dir reports/circle_ai_request_validation \
  --certification-bundle-out-dir reports/circle_ai_certification_bundles \
  --certification-bundle-check-out-dir reports/circle_ai_certification_bundle_checks \
  --report-out reports/circle_ai_runner_check.json \
  --require-status proved \
  --require-decision passed \
  --require-passed

For a fast lane-specific CI check, filter by contract family:

python scripts/check_circle_ai_contract_runner.py \
  --kind sparse-attention \
  --report-out reports/sparse_runner_check.json

The filter accepts the same aliases as the request schema, including rope, kv-cache, sparse-attention, recurrence, strided-fanout, cyclic-memory, multicoil-phase, cyclic-mixer, and seed-rule. The JSON report records the canonical selected_kinds list so a downstream audit can distinguish a full batch check from a lane-specific check.

The report file uses schema id circle_calculus.ai_contract_runner_check.v0 and records the selected contract-kind filter, source type, source path, optional generated request path, optional model-config or architecture-config import-report path, optional request-validation report path, optional certification-bundle path, optional receipt path, status, theorem count, recommendation count, validation-command count, decision verdict, assurance level, the normalized_request parameters, the source-content fingerprint, and receipt fingerprints for each checked item. Model-config summaries also inline model_config_parameter_sources, so a reader can see which RoPE request values were overridden, read from config fields, derived, defaulted, or omitted without opening the import sidecar. Architecture-config summaries similarly inline architecture_config_parameter_sources; optional architecture parameters that use receipt defaults are materialized in the emitted request and labeled default, so certification bundles can verify the import request against the receipt request. They also inline unsupported_architecture_config_fields, so batch reports show target-section behavior that was present in the source config but not certified by the emitted request. Add --require-no-unsupported-architecture-fields when the checker should reject any architecture-config example with unmapped source fields instead of accepting the receipt with an explicit non-claim. Model-config summaries similarly inline unsupported_model_config_fields; add --require-no-unsupported-model-config-fields when a standard-RoPE batch should reject unsupported model-config features instead of only preserving the boundary in the report. It also records the batch gate policy. If a receipt violates the required status, decision, assurance, or pass condition, the checker still writes the report and exits nonzero. The checker also builds the compact receipt for every request, model-config, and architecture-config example and fails if selected compact evidence is empty, if proof-layer labels do not cover exactly those selected paths, or if any selected path is unclassified. Add --compact-receipt-out-dir to save those compact handoff files for every checked item. Each summary records the compact receipt path, selected-evidence count, unclassified count, and label set. Use --model-config-import-report-out-dir when the model-config conversion itself should be saved as an audit artifact. Use --architecture-config-import-report-out-dir when architecture-config conversion should be saved as an audit artifact. Use --request-validation-report-out-dir when the request preflight report should be saved for every request before the receipt step. Use --certification-bundle-out-dir when each checked request, model config, or architecture config should write a portable bundle containing preflight, receipt, gate report, and any model-config or architecture-config import provenance. Use --certification-bundle-check-out-dir with it when the batch should also write a schema-validated verification report for every bundle. By default the batch includes request-file examples, standard RoPE model-config examples currently including 128k examples at RoPE bases 10000 and 500000, and architecture-config examples that emit RoPE, KV-cache, sparse-attention, and recurrence receipts by default. Pass --architecture-config-kind to restrict architecture-derived contract families globally, or set circle_ai_contract_kinds inside one architecture config to restrict that file only.

Validate a saved certification bundle after it has been handed to another project:

python scripts/check_circle_ai_certification_bundle.py \
  reports/rope_certification_bundle.json \
  --require-status proved \
  --require-decision passed \
  --require-assurance mixed_theorem_and_computation \
  --require-passed \
  --report-out reports/rope_certification_bundle_check.json

This is the preferred downstream CI check when the full certification bundle is available. It validates the bundle JSON Schema, request-validation report, embedded receipt against the loaded contract pack, embedded gate report, optional model-config or architecture-config import provenance, and the optional status, decision, assurance, pass, theorem-id, evidence-field, recommendation-id, validation-command, normalized-parameter, model-config fingerprint, and architecture-config fingerprint gates. Add --require-kind KIND, --require-theorem-id THEOREM_ID, --require-evidence-field FIELD, --require-recommendation-id ID, --require-validation-command COMMAND, or --require-normalized-param KEY=JSON_VALUE when a downstream project depends on specific embedded receipt content. Add --require-model-config-fingerprint FINGERPRINT with the model_config_fingerprint from the embedded import report when the bundle came from an imported RoPE config.json. Add --require-architecture-config-fingerprint FINGERPRINT with the architecture_config_fingerprint from the embedded import report when the bundle came from an architecture config. The bundle-check report records those requested dependencies in pin_policy. Reuse the same bundle dependency contract later with --pin-policy reports/rope_certification_bundle_check.json; the checker accepts either the whole report or just the pin_policy object, and explicit --require-* flags are merged with the loaded pins.

Validate a receipt file after it has been handed to another project:

python scripts/check_circle_ai_receipt.py reports/rope_receipt.json \
  --require-status proved \
  --require-decision passed \
  --require-assurance mixed_theorem_and_computation \
  --require-passed \
  --report-out reports/rope_receipt_check.json

This is the smallest downstream CI check. It validates the receipt JSON Schema, the in-process receipt shape, the receipt fingerprint, the loaded contract-pack fingerprint, the contract fingerprint, theorem-id membership in the loaded contract, and the optional status, decision, assurance, pass, theorem-id, evidence-field, recommendation-id, validation-command, and normalized-parameter gates. Add --require-kind KIND, --require-theorem-id THEOREM_ID, --require-evidence-field FIELD, --require-recommendation-id ID, --require-validation-command COMMAND, or --require-normalized-param KEY=JSON_VALUE when a downstream project depends on specific receipt content. It does not run Lean; it verifies that the receipt still points at the public contract pack it claims to use. The checker validates its own report against site/data/generated/circle_ai_contract_receipt_file_check.schema.json and can write that report to disk for audit logs. The report summary includes the loaded contract-pack fingerprint, contract fingerprint, receipt fingerprint, request-content fingerprint, normalized-request fingerprint, theorem ids, evidence fields, recommendation ids, validation commands, and normalized request, so CI can record what was certified without reopening every receipt file. The receipt-check report also records requested dependency pins in pin_policy. Reuse the same receipt dependency contract later with --pin-policy reports/rope_receipt_check.json; the checker accepts either the whole report or just the pin_policy object, and explicit --require-* flags are merged with the loaded pins.

Replay a saved receipt when CI needs to prove it can still be regenerated from its embedded request under the current runner code and contract pack:

python scripts/check_circle_ai_receipt_replay.py reports/rope_receipt.json \
  --report-out reports/rope_receipt_replay.json

The replay checker does not execute shell commands embedded in the receipt. It rebuilds the receipt through the public Python request API, then compares the original and regenerated status, decision, request fingerprint, normalized request fingerprint, and receipt fingerprint. This catches stale-but-well-formed receipt files whose JSON shape and pack fingerprints still validate but whose computed evidence no longer matches the current runner.

Receipt JSON is strict at the top level: unknown fields are rejected, while contract-specific details live under evidence, support, and proof_layers. The embedded request object is also validated against the public request schema, and its contract kind must match the receipt kind.

Receipt Reading Loop

Read every receipt in this order:

1. kind: which contract family was used;
2. decision: the stable downstream verdict and assurance level;
3. normalized_request: what parameters the tool actually checked;
4. status and request_passed: whether the request was accepted, rejected, undecided, numerical-only, or outside scope;
5. evidence: the family-specific certificate fields;
6. proof_status.theorem_ids: the proof trail;
7. proof_layers: proved versus computed versus numerical-only fields;
8. recommendations and validation_commands: how a downstream tool should act on and recheck the receipt;
9. request_content_fingerprint and normalized_request_fingerprint: stable hashes for audit logs, caches, and stale-receipt detection;
10. not_claimed: what the receipt deliberately does not prove.

Python API

from circle_math.applications import (
    build_architecture_config_certification_bundle,
    build_contract_artifact_manifest_file_check_report,
    build_contract_certification_bundle,
    build_contract_certification_bundle_file_check_report,
    build_contract_receipt_file_check_report,
    build_contract_receipt_gate_report,
    build_contract_receipt_replay_check_report,
    build_contract_request,
    build_contract_request_validation_report,
    build_rope_contract_request_from_model_config,
    build_rope_model_config_certification_bundle,
    build_validated_rope_receipt_from_model_config,
    load_contract_pack,
    require_contract_receipt_gate,
    build_validated_contract_receipt,
    build_validated_contract_receipt_from_request,
    validate_contract_request,
    validate_contract_receipt_against_pack,
)

pack = load_contract_pack("site/data/generated/circle_ai_contract_pack.json")
model_config = {
    "hidden_size": 4096,
    "num_attention_heads": 32,
    "rope_theta": 10000.0,
    "max_position_embeddings": 131072,
}
request = build_rope_contract_request_from_model_config(
    model_config,
    requested_margin="1/328459",
)
receipt = build_validated_rope_receipt_from_model_config(
    model_config,
    requested_margin="1/328459",
    pack=pack,
)
assert receipt["request"] == request
rope_bundle = build_rope_model_config_certification_bundle(
    model_config,
    requested_margin="1/328459",
    pack=pack,
    required_statuses=("proved",),
    required_decision_verdicts=("passed",),
    required_assurance_levels=("mixed_theorem_and_computation",),
    require_passed=True,
)
assert rope_bundle["model_config_import_report"]["request"] == request

request = build_contract_request(
    "kv-cache",
    {
        "cache_size": 16,
        "current": 31,
        "token": 20,
        "batch_tokens": (20, 24, 29, 31),
        "sink_size": 4,
    },
)

receipt = build_validated_contract_receipt(
    request["kind"],
    request["parameters"],
    pack=pack,
)

assert validate_contract_receipt_against_pack(receipt, pack) == []
assert receipt["validation_commands"][0].startswith(
    "python scripts/circle_ai_certify.py kv-cache "
)
replay_report = build_contract_receipt_replay_check_report(
    receipt,
    pack,
    receipt_path="reports/kv_receipt.json",
)
assert replay_report["ok"] is True
assert replay_report["comparison"]["all_replay_fields_match"] is True
check_report = build_contract_receipt_file_check_report(
    receipt,
    pack,
    receipt_path="reports/kv_receipt.json",
    required_statuses=("proved",),
    required_decision_verdicts=("passed",),
    required_assurance_levels=("theorem_backed",),
    require_passed=True,
)
assert check_report["ok"] is True
gate_report = build_contract_receipt_gate_report(
    receipt,
    pack,
    required_statuses=("proved",),
    required_decision_verdicts=("passed",),
    required_assurance_levels=("theorem_backed",),
    require_passed=True,
)
assert gate_report["ok"] is True
require_contract_receipt_gate(
    receipt,
    pack,
    required_statuses=("proved",),
    required_decision_verdicts=("passed",),
    required_assurance_levels=("theorem_backed",),
    require_passed=True,
)

The request-file object can be used directly from Python:

request = {
    "schema_id": "circle_calculus.ai_contract_request.v0",
    "kind": "sparse-attention",
    "parameters": {
        "context": 120,
        "strides": (7, 13),
        "path_length": 3,
        "local_window": 4,
    },
}

assert validate_contract_request(request) == []
assert build_contract_request_validation_report(request)["ok"] is True
receipt = build_validated_contract_receipt_from_request(request, pack=pack)
bundle = build_contract_certification_bundle(
    request,
    pack=pack,
    required_statuses=("proved",),
    required_decision_verdicts=("passed",),
    required_assurance_levels=("theorem_backed",),
    require_passed=True,
)
assert bundle["request_validation_report"]["ok"] is True
assert bundle["receipt"] == receipt
assert bundle["gate_report"]["ok"] is True
bundle_check_report = build_contract_certification_bundle_file_check_report(
    bundle,
    pack,
    bundle_path="reports/sparse_attention_certification_bundle.json",
    required_statuses=("proved",),
    required_decision_verdicts=("passed",),
    required_assurance_levels=("theorem_backed",),
    require_passed=True,
)
assert bundle_check_report["ok"] is True

architecture_config = {
    "sparse_attention": {
        "context_length": 9,
        "sliding_window": 2,
        "strides": [3, 4, 7],
        "max_hops": 2,
    }
}
architecture_bundle = build_architecture_config_certification_bundle(
    "sparse-attention",
    architecture_config,
    pack=pack,
    required_statuses=("proved",),
    required_decision_verdicts=("passed",),
    required_assurance_levels=("theorem_backed",),
    require_passed=True,
    require_no_unsupported_architecture_fields=True,
)
assert architecture_bundle["architecture_config_import_report"]["ok"] is True

The bundle’s top-level request_content_fingerprint hashes the submitted request object used for preflight. If the request came from --model-config or from build_rope_model_config_import_report, the optional model_config_import_report section carries the model-config fingerprint, the config-to-request parameter sources, and the emitted request fingerprint. If it came from --architecture-config or build_architecture_config_import_report, the parallel architecture_config_import_report section carries the source config fingerprint, parameter sources, and emitted request fingerprint. The embedded receipt carries its own request_content_fingerprint for the canonical request emitted after contract defaults are applied. Use build_rope_model_config_certification_bundle or build_architecture_config_certification_bundle when downstream Python code wants receipt, gate report, and source-config provenance in one schema-validated object.

For every parameterized receipt, the first validation_commands entry is the repository-script replay command for those exact runner parameters. The second entry is the installed circle-ai-certify replay command for downstream projects. The remaining commands come from the contract pack and recheck fixture readiness, theorem coverage, and family-specific tests. The text summary prints those same commands as validation_command=... lines so a reader can copy the replay path before opening the full JSON. When a single receipt is built from a model config or architecture config, the text summary also prints an import-boundary line with unsupported source-field counts, so unmodeled source-config behavior remains visible. Add --require-no-unsupported-architecture-fields when a direct architecture-config receipt or a batch report should reject that boundary instead of only reporting it. Add --require-no-unsupported-model-config-fields when RoPE model-config imports should enforce the same strict boundary.

That returns the same schema as the CLI:

circle_calculus.ai_contract_receipt.v0

Downstream gates should read the receipt’s decision block before digging into contract-specific evidence. It carries the stable verdict, assurance level, claim status, request_passed, theorem count, and proof-layer counts, and the receipt validator rejects it if it drifts from the rest of the receipt. The CLI and saved-receipt checker can gate directly on it with --require-decision and --require-assurance.

The generated Circle AI runner schemas live at:

site/data/generated/circle_ai_contract_request.schema.json
site/data/generated/circle_ai_contract_request_validation.schema.json
site/data/generated/circle_ai_rope_model_config_import.schema.json
site/data/generated/circle_ai_contract_receipt.schema.json
site/data/generated/circle_ai_contract_compact_receipt.schema.json
site/data/generated/circle_ai_contract_runner_check.schema.json
site/data/generated/circle_ai_contract_receipt_file_check.schema.json
site/data/generated/circle_ai_contract_receipt_replay_check.schema.json
site/data/generated/circle_ai_contract_certification_bundle.schema.json
site/data/generated/circle_ai_contract_certification_bundle_file_check.schema.json
site/data/generated/circle_ai_contract_artifact_manifest.schema.json
site/data/generated/circle_ai_contract_artifact_manifest_file_check.schema.json

The request schema is contract-specific: it accepts defaults for RoPE, recurrence, and the five compact ready families; requires the core KV-cache and sparse-attention fields; rejects odd RoPE head_dim values; requires positive recurrence max_loops and selected_block_width values; rejects empty multicoil period lists, nonpositive bank sizes, and cyclic-mixer block sizes larger than the channel count; and rejects unknown top-level request keys or parameter names before a receipt is issued. The Python validate_contract_request(request) helper applies the same public checks for downstream code that does not invoke JSON Schema directly. The runner-check schema validates the batch reports emitted by circle-ai-certify batch --format json and by python scripts/check_circle_ai_contract_runner.py --format json, including the per-request receipt fingerprints and optional receipt paths.

What This Does Not Prove

The runner does not prove better language-model quality, better reasoning, training improvement, deployment safety, runtime speed, memory savings, or implementation correctness. Its value is narrower: it exposes finite circular failure modes and theorem-backed contract fields before those claims drift into ordinary AI prose.

Previous: AI Contract Suite Next: RoPE Certifier