# Certified Valuation-Sparse p-adic GEMM With Trace-Bound Semantic Evidence
## P255 Functional Hardening Synchronization
This manuscript draft is synchronized through P255. The P248-P254 hardening
route adds runtime-shape ROCm/HIP p-adic GEMM evidence, repeated benchmark
summaries, planner-selected ROCm/HIP p-adic valuation lowering, public
prefer-gpu dense integer add selection, multi-overlap finite-site sheaf
locality evidence, optional Lean success-transcript capture, and a
claim-guarded JSC target verification packet.
These additions strengthen the repository evidence package, but they do not
change the manuscript into a production-performance, portable-GPU,
fully-formalized, or submission-ready claim. The primary manuscript route
remains certified valuation-sparse fixed-precision p-adic GEMM with
trace-bound semantic evidence and explicit non-claims.
## P240 Current Manuscript Draft Route
This continuous draft is synchronized through P240. The primary manuscript claim
is certified valuation-sparse fixed-precision p-adic GEMM: valuation-bucket
fingerprints identify the certified workload, theorem-bound skip certificates
justify products that vanish modulo `p^k`, dense CPU and certified sparse CPU
oracles validate supported outputs, feature-gated ROCm/HIP pilot rows record
local execution evidence, deterministic benchmark artifacts expose
distribution-level behavior, and fail-closed release gates preserve non-claim
boundaries. C1-C9 remain supporting traceability, proof-evidence,
nonstandard-domain, and reproducibility infrastructure.
## Abstract
Adaptive tensor runtimes usually optimize execution while leaving mathematical
semantics, proof obligations, and artifact authenticity outside the runtime
contract. Tokitai explores a proof-carrying alternative through a concrete
algorithm-system result: certified valuation-sparse fixed-precision p-adic
GEMM. The system derives valuation lower bounds, skips products that vanish
modulo `p^k`, attaches per-output certificates, checks dense CPU and certified
sparse CPU oracles, executes a narrow ROCm/HIP pilot, and validates the evidence
through release gates. The scoped contribution is certified valuation-sparse
p-adic GEMM with trace-bound semantic evidence, not a claim of production
compiler maturity.
Front-matter anchor: scoped contribution is certified valuation-sparse p-adic
GEMM with trace-bound semantic evidence, not production tensor compiler
maturity.
Evidence anchor: valuation bucket fingerprints, per-output certificates, dense
and certified sparse CPU oracles, ROCm/HIP pilot evidence, theorem-result
fingerprints, controlled evaluation artifacts, related-work boundaries, native
admissions, reproducible artifacts.
The current artifact focuses on certified p-adic GEMM plus the evidence
infrastructure needed to keep that claim auditable. It does not claim production
tensor compiler maturity, full Rust verification, arbitrary CPU/SIMD/GPU kernel
verification, cryptographic novelty, verified compiler status, or full
Lean/Coq/Isabelle proof generation. Its claim is narrower: certified
valuation-sparse fixed-precision p-adic GEMM is bound to execution-plan
evidence, proof replay reports, proof-assistant summaries, native admissions,
theorem-result fingerprints, checker result indexes, canonical JSON imports,
selected theorem witnesses, controlled evaluation artifacts, related-work
boundaries, and signed manifests as auditable semantic evidence.
## 1. Introduction
Modern operator systems such as tensor compilers and graph runtimes optimize
programs through lowering, fusion, scheduling, and backend dispatch. Those
systems are effective for ordinary numeric workloads, but their correctness
story is usually external to the runtime artifact: proofs, if present, live in a
separate theorem prover or compiler-verification pipeline. This separation is
especially fragile for nonstandard mathematical domains. p-adic arithmetic
requires valuation and precision-cutoff reasoning; finite sheaf examples
require cover compatibility and gluing checks. Treating those structures as
ordinary dtypes hides the obligations that make an optimization valid.
Tokitai asks whether adaptive operator execution can carry semantic
accountability as part of the runtime trace. The design makes mathematical
domains, proof obligations, lowering evidence, proof replay, optional checker
evidence, and artifact validation first-class concerns. The repository evidence
is organized by claims C1-C10 in `docs/paper/contribution_map.md` and by
generated tables under `target/paper-results`.
The paper claim is a scoped algorithm-system claim. Tokitai contributes
certified valuation-sparse p-adic GEMM (C10) as the primary route, with
trace-bound semantic evidence (C1), nonstandard-domain planning (C2), native
checker admission binding (C3), authenticity-versus-semantic failure taxonomy
(C4), canonical artifact normalization (C5), selected theorem witnesses (C6 and
C7), reviewer-visible witness metadata (C8), and controlled baseline/scale
evaluation (C9). It does not claim that SHA-256, JSON schemas, optional Lean
invocation, CPU reference execution, p-adic arithmetic, sheaf theory, or tensor
kernels are novel in isolation.
The contribution list for the manuscript front matter is:
- Trace-bound semantic evidence for accepted operator traces, anchored in
`docs/paper/formal_model.md`.
- Certified valuation-sparse p-adic GEMM with theorem-bound skip
certificates, dense CPU and certified sparse CPU oracles, a feature-gated
ROCm/HIP pilot, benchmark matrix artifacts, and fail-closed claim gates,
anchored in `docs/paper/certified_padic_gemm_manuscript_delta.md`.
- Nonstandard-domain contracts for fixed-precision p-adic and finite-site sheaf
examples, anchored in `tests/padic.rs`, `tests/sheaf.rs`, and
`docs/paper/evaluation_methodology.md`.
- Native admission and theorem-result fingerprint binding for selected checker
evidence, anchored in `docs/paper/proof_assistant_scope.md`.
- Controlled artifact evaluation with manuscript table and figure traceability,
anchored in `docs/paper/table_figure_plan.md`.
- Reproducible paper artifacts and related-work novelty boundaries, anchored in
`docs/paper/related_work_synthesis.md` and `ARTIFACT.md`.
## 2. System Model And Architecture
Tokitai represents operator execution through semantic graphs whose nodes carry
domain, representation, shape, contract, and backend metadata. Semantic
operators are registered separately from backend lowering rules. A lowering is
valid only when it is registered for a known semantic operator and supports the
requested domain, representation, and backend. The planner emits execution
steps, rewrite evidence, proof objects, semantic costs, and unresolved
obligations. Backends execute lowered plans but do not define mathematical
semantics. For the current manuscript route, this separation lets the certified
p-adic GEMM path make valuation metadata, certificate policy, oracle authority,
and ROCm/HIP execution evidence explicit instead of burying them in a backend
dispatch decision.
This architecture matters for nonstandard domains. p-adic valuation and
precision-bounded equality can guide planning without being reduced to ordinary
integer dtype dispatch. Finite-site sheaf covers and restrictions can appear as
cover-local compatibility and gluing evidence rather than ad hoc runtime
checks. The CPU reference backend is the current semantic baseline; the scoped
feature-gated ROCm/HIP p-adic GEMM pilot is current local execution evidence,
while broad SIMD/GPU portability and production speedup remain future work.
Repository anchors for this section are `src/ir`, `src/op/registry.rs`,
`src/planner`, `src/backend`, `src/domain/padic.rs`, `src/object/sheaf.rs`, and
`src/verify/mod.rs`. The generated `target/paper-results/trace-architecture.csv`
summarizes the trace-binding architecture.
## 3. Formal Model And Soundness Scope
The formal model in `docs/paper/formal_model.md` states Tokitai's scoped
soundness claim. The central predicate is `Accept(T)`, which combines
`ManifestOk`, `ArtifactOk`, `CanonicalImportOk`, `ReplayOk`, `SummaryOk`,
`SummaryMatchesSkeleton`, `RegistryOk`, `SummaryMatchesRegistry`,
`NativeAdmissionOk`, `CheckerIndexOk`, and optional `SignatureOk`.
The main paper theorem is `Canonical Trace-Bound Semantic Evidence Soundness`:
if a trace directory is accepted, theorem-level checker results, native
admission evidence, replay summaries, adapter capabilities, manifest digests,
signature payloads, canonical imports, and plan fingerprints cannot be silently
replaced, reordered, retargeted, or reserialized without rejection by directory
validation. This is an evidence-preservation theorem under an explicit trusted
computing base, not a mechanically checked proof that the Rust validator is
correct.
P153 sharpens the theorem into four scoped statements:
- T1 Canonical Trace-Bound Semantic Evidence Soundness.
- T2 Registry-Aware Lowering Obligation Traceability.
- T3 Nonstandard-Domain Obligation Coverage.
- T4 Native Admission Boundary.
The proof obligation status map covers shape equality, p-adic valuation
cutoff, lowering semantic preservation, rewrite soundness, sheaf cover
compatibility and gluing, and native checker admission. Implemented replay
evidence is mapped to tests such as `tests/operator_registry.rs`,
`tests/padic.rs`, `tests/sheaf.rs`, `tests/properties.rs`,
`tests/audit_traces_example.rs`, and `tests/json_parser_regression.rs`.
The TCB is explicit: SHA-256 collision resistance, the Rust validator,
filesystem observation during validation, native checker truth for declared
backend/version, key policy for signatures, domain contract interpretation, and
canonical renderer/importer correctness are trusted to the extent documented in
the repository. These assumptions are limitations, not hidden claims of a fully
verified compiler.
## 4. Proof Assistant And Native Admission Evidence
Tokitai uses proof-assistant artifacts as scoped evidence. The repository
generates Lean-facing skeleton and checkable-artifact metadata, checker
transcripts, checker outputs, native admissions, adapter capability
fingerprints, and checker result indexes. The default release gate does not
require Lean to be installed. Optional local Lean execution is documented in
`docs/paper/optional_lean_checker.md` and packaged by
`scripts/optional_lean_check.sh`.
The current selected witness families are
`shape_equality_dimension_witness_v1` and
`padic_precision_cutoff_witness_v1`. They connect ordinary shape reasoning and
one nonstandard-domain p-adic precision-cutoff obligation to proof-assistant
metadata. The contribution is not full theorem generation. The contribution is
that checker evidence, native admissions, adapter registry capabilities,
checker result indexes, theorem-result fingerprints, and trace manifests are
validated together.
Evidence anchors include `docs/paper/proof_assistant_scope.md`,
`docs/paper/optional_lean_checker.md`, `tests/operator_registry.rs`,
`tests/audit_traces_example.rs`, and generated tables
`target/paper-results/trace-architecture.csv`,
`target/paper-results/tamper-matrix.csv`, and
`target/paper-results/claim-to-test-matrix.csv`.
## 5. Nonstandard Mathematical Domains
Tokitai's nonstandard-domain examples are intentionally small but semantically
explicit. For p-adic operators, the system models fixed-precision residues,
valuation, precision-bounded equality, and valuation cutoff planning. For
finite-site sheaf examples, the system models covers, restrictions,
compatibility, and gluing checks. These structures become planner-visible
obligations rather than comments or dtype conventions.
The p-adic evidence is implemented in `src/domain/padic.rs` and tested in
`tests/padic.rs` and `tests/properties.rs`. The sheaf evidence is implemented in
`src/object/sheaf.rs` and tested in `tests/sheaf.rs` and `tests/properties.rs`.
Generated paper rows in `target/paper-results/paper-results.csv`,
`target/paper-results/measurement-summary.csv`, and
`target/paper-results/baseline-scale-comparison.csv` expose p-adic valuation
skip, p-adic matmul valuation skip, sheaf cover glue, proof-trace validation,
and selected witness metadata workloads.
The limitations are deliberate. The p-adic implementation is fixed precision
over u128-backed residues. The sheaf implementation is a finite-site prototype.
Tokitai does not claim a complete p-adic algebra system, complete sheaf theory,
or sheaf cohomology formalization.
## 6. Evaluation
The evaluation is a controlled artifact evaluation, not a production benchmark
claim. The default generated `paper_benchmarks` example emits:
- `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`.
The feature-gated certified p-adic GEMM benchmark emits:
- `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 evaluation answers four questions. First, it shows whether valuation
distributions produce certified skipped and evaluated product counts with
explicit precision margins. Second, it verifies dense CPU and certified sparse
CPU oracle agreement for supported rows. Third, it records feature-gated
ROCm/HIP pilot execution or fallback status without turning local timing into a
portable speed claim. Fourth, the default artifacts continue to show trace
architecture, tamper-detection surfaces, and reviewer-visible witness metadata
as supporting evidence.
`docs/paper/evaluation_methodology.md` interprets these results. Deterministic
proxy rows are artifact-stable measurements. Repeated wall-clock rows are smoke
measurements. The tables support claims about trace overhead, nonstandard
planning behavior, tamper-detection surfaces, and witness metadata visibility;
they do not support production throughput claims against mature tensor
compilers. The certified p-adic GEMM benchmark rows support algorithmic evidence
about work reduction and oracle agreement while keeping `speed_claim_allowed`
closed. `docs/paper/table_figure_plan.md` maps each generated artifact to
manuscript tables or figures, captions, supported claims, regeneration commands,
and claim boundaries. The P158 evaluation prose in
`docs/paper/evaluation_methodology.md` adds RQ1-RQ5, result interpretation, and
threats-to-validity wording for Tables 1-5 and Figures 1-3.
## 7. Reproducibility And Artifact Package
The reviewer entry point is `ARTIFACT.md`. The clean-checkout gate is:
```bash
python -m json.tool todo.json >/dev/null
python -m json.tool docs/schemas/tokitai-artifacts-v1.schema.json >/dev/null
python -m json.tool docs/schemas/tokitai-paper-csv-v1.schema.json >/dev/null
cargo fmt --check
cargo test --offline
cargo run --quiet --offline --example paper_benchmarks
cargo test --offline --features rocm-hip --test rocm_padic_stratified_benchmarks -- --nocapture
cargo run --quiet --offline --features rocm-hip --example rocm_padic_stratified_benchmarks
```
Signed audit trace validation is:
```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 --offline --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"
```
Release guidance is documented in `docs/paper/release_checklist.md` and
`docs/paper/release_bundle_manifest.md`. Environment capture writes
`target/tokitai-release-env.txt` for reviewer notes. DOI archives, containers,
and broad CI matrices are camera-ready hardening, not current submission
blockers.
## 8. Related Work And Novelty Boundary
Tokitai should be positioned against six nearby prior-art families:
- Tensor compilers and operator runtimes such as MLIR, XLA, TVM, Triton, JAX,
PyTorch, and TensorFlow.
- Proof assistants and SMT/verification tools such as Lean, Coq, Isabelle,
Why3, Dafny, and SMT solvers.
- p-adic libraries and computer algebra systems such as SageMath and PARI/GP.
- Sheaf/category-theory tools and mathematical libraries.
- Verified compilers and translation validators such as CompCert and Alive2.
- Artifact reproducibility and supply-chain frameworks such as SLSA, in-toto,
Sigstore, and TUF.
The current novelty boundary follows P222/P234 rather than the older P154
primary framing: Tokitai integrates certified valuation-sparse fixed-precision
p-adic GEMM with trace-bound proof evidence. Valuation lower bounds justify
skipped products, per-output certificates expose theorem assumptions, dense CPU
and certified sparse CPU oracles validate supported rows, feature-gated ROCm/HIP
pilot rows record local execution evidence, deterministic benchmark
distributions expose where the optimization applies, and release gates prevent
unsupported claims about arbitrary precision, full p-adic algebra, portability,
verified machine code, or production speedup. It does not claim novelty for
SHA-256, JSON schemas, optional Lean invocation, CPU reference execution,
p-adic arithmetic, sheaf theory, sparse GEMM, GPU exact arithmetic, or tensor
kernels in isolation. The P234 related-work synthesis in
`docs/paper/related_work_synthesis.md` expands this section into
manuscript-ready comparison paragraphs and evidence anchors.
In short, the contribution is not SHA-256, not JSON schemas, not optional Lean
invocation, not CPU reference execution, not p-adic arithmetic alone, not sparse
GEMM alone, not GPU exact arithmetic, not sheaf theory alone, and not tensor
kernels in isolation.
The manuscript must not claim production performance superiority over mature
tensor compilers, replacement of Lean/Coq/Isabelle, novel p-adic or sheaf
mathematics, production deployment packaging, cryptographic novelty, or fully
verified compiler status.
## 9. Limitations
The main limitations are:
- CPU reference execution remains the semantic oracle.
- ROCm/HIP execution is feature-gated and limited to the scoped local p-adic
GEMM pilot.
- No SIMD execution backend.
- Fixed-precision p-adic arithmetic over u128-backed residues.
- Finite-site sheaf prototype with simplified overlap values.
- External Lean execution is optional in the default gate.
- No full Lean/Coq/Isabelle theorem generation for every obligation.
- The Rust validator is tested but not mechanically verified.
- Deterministic proxy timings and wall-clock smoke rows are not production benchmark claims.
- Key rotation and external key management are policy concerns, not integrated
infrastructure.
- DOI/container/CI publication artifacts are camera-ready hardening.
## 10. Artifact Appendix
The draft is grounded in the following repository artifacts:
| C1 trace-bound semantic evidence | `docs/paper/formal_model.md`, `tests/audit_traces_example.rs`, `target/paper-results/trace-architecture.csv` |
| C2 nonstandard-domain planning | `tests/padic.rs`, `tests/sheaf.rs`, `target/paper-results/baseline-scale-comparison.csv` |
| C3 native checker admission binding | `docs/paper/proof_assistant_scope.md`, `tests/operator_registry.rs`, `target/paper-results/tamper-matrix.csv` |
| C4 authenticity versus semantic failures | `docs/paper/trust_model.md`, `tests/audit_traces_example.rs` |
| C5 canonical artifact normalization | `docs/paper/serialization_strategy.md`, `tests/json_parser_regression.rs` |
| C6 selected native shape witness | `shape_equality_dimension_witness_v1`, `target/paper-results/claim-to-test-matrix.csv` |
| C7 selected nonstandard p-adic witness | `padic_precision_cutoff_witness_v1`, `target/paper-results/claim-to-test-matrix.csv` |
| C8 reviewer-visible witness metadata | `docs/paper/schema_inventory.md`, `target/paper-results/paper-results.json` |
| C9 controlled baseline and scale evaluation | `docs/paper/evaluation_methodology.md`, `target/paper-results/baseline-scale-comparison.csv` |
| C10 certified valuation-sparse p-adic GEMM | `docs/paper/certified_padic_gemm_manuscript_delta.md`, `target/paper-results/padic-stratified-benchmarks/padic-stratified-benchmarks.csv` |
| Table and figure plan | `docs/paper/table_figure_plan.md`, `target/paper-results/measurement-summary.csv`, `target/paper-results/tamper-matrix.csv`, `target/paper-results/paper-results.json` |
| T1-T4 scoped theorems | `docs/paper/formal_model.md`, `tests/paper_artifacts.rs` |
| Reproducibility | `ARTIFACT.md`, `docs/paper/release_checklist.md`, `docs/paper/release_bundle_manifest.md` |
| Prior-art boundary | `docs/paper/contribution_map.md`, `docs/paper/manuscript_skeleton.md` |
This draft now follows the P240 route: the continuous paper argument leads with
certified valuation-sparse p-adic GEMM and uses the older proof-aware runtime
machinery as supporting evidence. Further work can add optional Lean CI
evidence, Criterion-grade benchmarking, DOI/container packaging, or mechanized
semantics, but those are not required for the scoped certified p-adic GEMM
artifact claim.
## 11. Conclusion
Tokitai demonstrates that certified valuation-sparse fixed-precision p-adic
GEMM can be packaged as an auditable algorithm-system artifact. The artifact
integrates valuation-bucket fingerprints, theorem-bound skip certificates,
dense CPU and certified sparse CPU oracle agreement, feature-gated ROCm/HIP
pilot evidence, deterministic benchmark distributions, domain contracts,
registry-aware lowering, proof replay, selected proof-assistant witnesses,
native admissions, checker result indexes, canonical artifact normalization,
controlled evaluation, and reproducible release gates. The result is not a
production tensor compiler or full proof-assistant development. It is a
research artifact showing how a nonstandard mathematical operator can make
semantic obligations and evidence binding explicit, auditable, and
reproducible.
The conclusion follows the scoped theorem and obligation boundaries in
`docs/paper/formal_model.md`, the evaluation threats in
`docs/paper/evaluation_methodology.md`, and the no-overclaim boundaries in
`docs/paper/related_work_synthesis.md`. Tokitai's final paper claim should
remain certified valuation-sparse p-adic GEMM with trace-bound semantic
evidence: theorem-bound skipping, dense and certified sparse CPU oracles,
feature-gated ROCm/HIP pilot evidence, controlled evaluation, reproducible
artifacts, and explicit related-work boundaries. It should not become a claim
of production performance, proof-assistant replacement, cryptographic novelty,
complete p-adic/sheaf mathematics, portable GPU support, verified HIP machine
code, or fully verified compiler status.
Conclusion boundary anchor: should not become a claim of production performance, proof-assistant replacement, cryptographic novelty, complete p-adic/sheaf mathematics, or fully verified compiler status.
## P354 Evaluation Infrastructure Notes
The evaluation infrastructure now includes 30+ new CPU-reference operators
registered through the same `op struct + OpSignature + contracts +
lowering_rule + facade builder` pipeline as the C10 GEMM operator
surface. These operators (P335-P339) and the supporting proptest
property tests (P352) provide stronger oracle coverage for any
operator-chained experimental evaluation, but they are not the
primary claim. The C10 claim remains certified valuation-sparse
p-adic GEMM with the audit-gated non-claims; the expanded surface is
recorded as supporting infrastructure for reproducibility and
follow-on experiments.