# Tokitai Operator Artifact
This file is the reviewer-facing reproduction guide for the SCI-Q2 paper
artifact.
## Requirements
- Rust toolchain with Cargo.
- No network access is required for normal verification after dependencies are
available in `Cargo.lock`.
- Optional external Lean checking is documented in
`docs/paper/proof_assistant_scope.md`; the current automated artifact uses a
scoped checker-output path and does not require Lean to run.
- Release checklist: `docs/paper/release_checklist.md`.
- Release bundle manifest and checksum inventory:
`docs/paper/release_bundle_manifest.md`.
## Clean-Checkout Release Checklist
For the condensed reviewer path, environment assumptions, generated output
checks, signed trace validation, optional Lean scope, and failure triage, see
`docs/paper/release_checklist.md`.
For the file inventory, generated-versus-source distinction, signed trace artifact list,
and checksum policy, see
`docs/paper/release_bundle_manifest.md`.
## Reproduce Core Validation
```bash
python -m json.tool todo.json >/dev/null
cargo fmt --check
cargo test
```
## Regenerate Paper Results
```bash
cargo run --quiet --example paper_benchmarks
```
This writes:
- `target/paper-results/paper-results.json`
- `target/paper-results/paper-results.csv`
- `target/paper-results/measurement-summary.csv`
- `target/paper-results/baseline-scale-comparison.csv`
- `target/paper-results/tamper-matrix.csv`
- `target/paper-results/claim-to-test-matrix.csv`
- `target/paper-results/trace-architecture.csv`
- `target/paper-results/theory-support-matrix.json`
- `target/paper-results/theory-support-matrix.md`
- `target/paper-results/theory-release-gate.json`
- `target/paper-results/theory-release-gate.md`
## Regenerate Feature-Gated p-adic GEMM Benchmarks
On a local ROCm/HIP validation target:
```bash
cargo test --offline --features rocm-hip --test rocm_padic_stratified_benchmarks
cargo run --quiet --offline --features rocm-hip --example rocm_padic_stratified_benchmarks
```
This writes:
- `target/paper-results/padic-stratified-benchmarks/padic-stratified-benchmarks.json`
- `target/paper-results/padic-stratified-benchmarks/padic-stratified-benchmarks.csv`
- `target/paper-results/padic-stratified-benchmarks/padic-stratified-benchmarks.md`
The generated rows are scoped certified p-adic GEMM smoke evidence with CPU
oracle, certificate, fallback, timing, and speed-claim guard fields. They are
not production speedup or portable GPU support evidence.
## Regenerate Signed Audit Trace
```bash
tmpdir=$(mktemp -d)
TOKITAI_AUDIT_TRACE_DIR="$tmpdir" \
TOKITAI_AUDIT_TRACE_KEY_ID="test key" \
TOKITAI_AUDIT_TRACE_SECRET="trace-secret" \
cargo run --quiet --example audit_traces
test -f "$tmpdir/matmul.proof-adapters.json"
rg -Fq '"admission_artifact_digest":null' "$tmpdir/matmul.proof-adapters.json"
rg -Fq '"capability_fingerprint":"sha256:' "$tmpdir/matmul.proof-adapters.json"
rg -Fq '"adapter_capability_fingerprint":"sha256:' "$tmpdir/tokitai-trace-manifest.json"
rm -rf "$tmpdir"
```
## Verify Canonical JSON Normalization
Tokitai accepts reordered JSON object fields for paper-critical trace artifacts,
then normalizes imports back to deterministic canonical JSON before computing
artifact digests or checking signatures. Reviewers can exercise this without
reading source internals:
```bash
cargo test --test json_parser_regression \
reordered_imports_normalize_to_canonical_json_and_digests
```
This checks that reordered imports for replay reports, checker indexes, signed
trace manifests, and benchmark artifacts render back to the canonical bytes used
by `proof_replay_artifact_digest` and manifest signature verification. The
generated paper tables also expose this as claim `C5` in
`target/paper-results/claim-to-test-matrix.csv` and as the
`ordinary_json_import -> canonical_json_renderer` edge in
`target/paper-results/trace-architecture.csv`.
## Verify Selected Lean Witness Metadata
Tokitai exposes selected proof-assistant witness families in both the generated
Lean checkable artifact header and the generated paper JSON. Reviewers can
verify the shape and p-adic witness metadata without reading the full Lean file:
```bash
cargo test --test operator_registry --test padic
cargo run --quiet --example paper_benchmarks
rg -Fq '"witness_metadata":[' target/paper-results/paper-results.json
rg -Fq '"selected_witness_family":"shape_equality_dimension_witness_v1"' target/paper-results/paper-results.json
rg -Fq '"selected_nonstandard_witness_family":"padic_precision_cutoff_witness_v1"' target/paper-results/paper-results.json
rg -Fq '"selected_shape_witness_count":1' target/paper-results/paper-results.json
rg -Fq '"selected_padic_witness_count":1' target/paper-results/paper-results.json
```
This corresponds to claim `C8` in
`target/paper-results/claim-to-test-matrix.csv`. The schema inventory documents
the same fields for the `tokitai-proof-assistant-lean-checkable` artifact:
`selected_witness_family`, `selected_nonstandard_witness_family`,
`selected_shape_witness_count`, and `selected_padic_witness_count`.
## Paper Claim Mapping
- Formal model: `docs/paper/formal_model.md`
- Proof assistant scope: `docs/paper/proof_assistant_scope.md`
- Theory contract core: `docs/theory_contract_core.md`
- Theorem binding registry: `docs/theorem_binding_registry.md`
- Certified rewrite and lowering contracts:
`docs/certified_rewrite_lowering_contracts.md`
- Theory-specific operator hardening:
`docs/theory_specific_operator_hardening.md`
- Semantic conformance report:
`docs/semantic_conformance_report.md`
- Theory-aware support matrix:
`docs/theory_support_matrix.md`
- Theory-engineering release gate:
`docs/theory_engineering_release_gate.md`
- First-of-kind novelty dossier: `docs/first_of_kind_novelty_evidence.md`
- Trust model: `docs/paper/trust_model.md`
- Serialization strategy: `docs/paper/serialization_strategy.md`
- Paper outline: `docs/paper/outline.md`
- Contribution map: `docs/paper/contribution_map.md`
- Release checklist: `docs/paper/release_checklist.md`
- Release bundle manifest: `docs/paper/release_bundle_manifest.md`
- Generated claim matrix:
`target/paper-results/claim-to-test-matrix.csv`
## Interpreting Results
- `paper-results.csv` reports deterministic workload costs for ordinary tensor,
p-adic valuation-skip, and sheaf glue workloads.
- `measurement-summary.csv` separates deterministic proxy rows from repeated
wall-clock validation smoke measurements.
- `baseline-scale-comparison.csv` reports controlled baseline and scale rows
for ordinary tensor, p-adic valuation, sheaf glue, proof-trace, and selected
witness metadata costs.
- `tamper-matrix.csv` reports which validation mode detects each tamper class.
- `trace-architecture.csv` lists artifact graph edges and binding mechanisms.
- `claim-to-test-matrix.csv` links paper claims to code, tests, and generated
experiment artifacts.
- `theory-support-matrix.json` and `theory-support-matrix.md` state supported,
fallback-only, feature-gated, and unsupported theory/backend/API boundaries.
- `theory-release-gate.json` and `theory-release-gate.md` state the current
theory-engineering release gate checks, blockers, required commands, deferred
work, and known limits.
## Known Limits
- CPU reference execution remains the semantic oracle. ROCm/HIP evidence is
feature-gated and limited to the scoped local p-adic pilot plus benchmark
smoke artifacts.
- Deterministic timing proxies are used for paper-table stability.
- Lean full theorem generation is not complete; P108 documents the current
Lean-first smoke-check boundary.
- Ed25519 verification is explicitly scoped as not implemented in P109; keyed
SHA-256 signatures and clear authenticity failures are currently tested.