use std::fs;
use std::path::Path;
use serde_json::Value;
use tokitai_operator::verify::{
current_claim_status_expectation, current_validation_status_expectation,
p268_claim_status_expectation, parse_status_block, validate_claim_status_block,
validate_status_block, validate_validation_status_block,
};
fn assert_contains_all(label: &str, content: &str, required: &[&str]) {
for item in required {
assert!(
content.contains(item),
"{label} should mention required item {item}"
);
}
}
fn collapse_whitespace(content: &str) -> String {
content.split_whitespace().collect::<Vec<_>>().join(" ")
}
fn read_todo_json() -> Value {
let todo = fs::read_to_string("todo.json").expect("todo.json should exist");
serde_json::from_str(&todo).expect("todo.json should parse as JSON")
}
fn todo_phase<'a>(todo: &'a Value, phase_id: &str) -> &'a Value {
todo["active_backlog"]
.as_array()
.expect("todo active_backlog should be an array")
.iter()
.find(|phase| phase["id"].as_str() == Some(phase_id))
.unwrap_or_else(|| panic!("todo active_backlog should contain phase {phase_id}"))
}
#[test]
fn todo_tracks_functional_hardening_roadmap_after_p247() {
let todo = fs::read_to_string("todo.json").expect("todo.json should exist");
assert_contains_all(
"todo functional hardening roadmap",
&todo,
&[
"Productize Tokitai from a publication-ready certified valuation-sparse p-adic GEMM artifact",
"P248-P275 are completed and preserved as validated functional hardening evidence",
"The roadmap is in functional-expansion state",
"HIP machine-code evidence and audit binding",
"external baseline and profiler fields",
"portable ROCm support remains blocked until at least two reviewed passing device/compiler combinations exist",
"remaining non-claim boundaries",
"generic GPU execution",
"production speedup",
"portable ROCm support",
"arbitrary precision p-adic fields",
"broader p-adic algebra",
"complete sheaf theory",
"full proof-assistant verification",
"submission-readiness evidence",
"smoke, mock, scaffold, narrow pilot, and remaining non-claim boundaries",
"certified valuation-sparse p-adic GEMM",
"P248 generalized the ROCm/HIP valuation-stratified p-adic GEMM pilot",
"runtime M/K/N shape arguments for validated small Q_5 precision-3 matrices",
"P249 replaced p-adic benchmark single-run smoke timing",
"min/median/max transfer, kernel, and wall-clock summaries",
"P250 promoted the ROCm/HIP p-adic valuation helper",
"device/kernel/compiler contract fingerprints included in plan-cache identity",
"P251 replaced dense integer add prefer-gpu scaffold selection",
"real feature-gated gpu_dense_i64_pilot or rocm_hip_dense_i32_pilot public execution",
"P252 strengthened the ROCm/HIP finite-site sheaf locality helper",
"structured compatibility reports, obstruction provenance, restriction witness counts",
"P253 added optional Lean success transcript capture",
"stdout/stderr transcript paths, artifact digests, timeout policy",
"P254 added a Journal of Symbolic Computation target verification packet template",
"claim_allowed=false guards until external evidence is supplied and reviewed",
"P255 synchronized CLAIMS.md, manuscript drafts, readiness audits",
"P256 added a machine-checkable GPU execution contract surface on public plans",
"rocm_hip_dense_i32_pilot records real device allocation, host/device copies, synchronization, kernel registry metadata, and CPU-oracle verification",
"P257 added external-baseline and profiler-evidence fields",
"reviewed external baseline, profiler capture, and measured speedup all pass",
"P258 added a ROCm portability matrix model",
"portable ROCm support remains blocked until at least two reviewed passing device/compiler combinations exist",
"P259 added HIP machine-code provenance binding in audit traces",
"kernel symbol, code-object metadata fingerprint, disassembly metadata status",
"no-formal-machine-code-verification boundary",
"P260 added a dynamically bounded p-adic CPU model",
"base-p digit storage beyond u128 modulus limits",
"conversion from u128 or canonical digit vectors, valuation, addition, multiplication, precision truncation, precision-bounded equality",
"P261 expanded the broader p-adic algebra subset",
"vector addition, pointwise vector multiplication, dot product, matrix-vector multiplication",
"unit-inverse checks, distributivity checks, vector operation oracle checks",
"runtime theory-contract evidence for those laws",
"P262 added a finite-site Cech-style obstruction summary",
"compatible H0 local-section counts, H1-style obstruction counts, obstruction supports",
"CPU oracle fingerprints, and theory evidence bound to the existing finite-sheaf obstruction theorem boundary",
"P263 added a selected-theorem strict proof-assistant evidence profile",
"theorem checker scripts emit selected-theorem profile metadata",
"TOKITAI_REQUIRE_LEAN=1",
"no-full-formalization boundary",
"Do not claim generic GPU execution, production speedup, portable ROCm support, verified HIP machine code",
"completed_phase_history",
"Detailed P200-P247 history lives in source files",
"implemented_functional_capabilities",
"smoke_mock_or_scaffold_inventory",
"generic GPU backend",
"GpuScaffoldBackend remains a fallback-only planning scaffold with no runtime kernels",
"accelerated-pilot feature",
"GpuDenseI64PilotBackend selectable through the public prefer-gpu dense i64 add path",
"ROCm/HIP p-adic GEMM",
"runtime-shape pilot for small Q_5 precision-3 fixtures",
"ROCm/HIP benchmark timing",
"configurable warmup and repeated measured runs",
"ROCm/HIP p-adic valuation helper",
"planner-selectable through a ROCm/HIP lowering contract",
"ROCm/HIP sheaf locality helper",
"check all declared pairwise overlap equalities for tested finite covers",
"preserve structured obstruction provenance",
"optional Lean",
"records optional Lean success transcripts when Lean is available",
"strict TOKITAI_REQUIRE_LEAN failure mode",
"submission venue status",
"Journal of Symbolic Computation target verification packet",
"machine-checkable missing-evidence fields",
"\"active_backlog\"",
"\"id\": \"P248\"",
"Replace p-adic GEMM hard-coded HIP shape with runtime shape support",
"\"status\": \"completed\"",
"\"id\": \"P249\"",
"Add repeated benchmark timing and summary statistics",
"\"status\": \"completed\"",
"\"id\": \"P250\"",
"Promote HIP p-adic valuation helper into planner-selected lowering",
"\"status\": \"completed\"",
"\"id\": \"P251\"",
"Replace generic GPU scaffold for dense integer add with real backend selection",
"\"status\": \"completed\"",
"\"id\": \"P252\"",
"Strengthen sheaf locality beyond equality-only pilot",
"\"status\": \"completed\"",
"\"id\": \"P253\"",
"Capture optional Lean success transcripts when Lean is installed",
"\"status\": \"completed\"",
"\"id\": \"P254\"",
"Add target-venue verification packet for JSC",
"\"status\": \"completed\"",
"\"id\": \"P255\"",
"Re-audit claim language after functional hardening",
"\"status\": \"completed\"",
"\"id\": \"P256\"",
"Define real GPU execution contract beyond scaffold fallback",
"\"status\": \"completed\"",
"explicit device allocation, host/device transfer lifecycle, stream or synchronization model",
"Tokitai has a scoped real GPU execution contract for the implemented dense operation family",
"\"id\": \"P257\"",
"Add speedup evidence gate with external baseline and profiler fields",
"\"status\": \"completed\"",
"speed_claim_allowed=false unless all criteria pass",
"\"id\": \"P258\"",
"Build ROCm portability evidence matrix",
"\"status\": \"completed\"",
"docs/paper/rocm_portability_matrix.md",
"multiple reviewed devices pass",
"\"id\": \"P259\"",
"Add HIP machine-code evidence and audit binding",
"\"status\": \"completed\"",
"not formal machine-code verification",
"\"id\": \"P260\"",
"Introduce arbitrary-precision p-adic field model behind explicit gates",
"\"status\": \"completed\"",
"Tokitai has a tested arbitrary-precision or dynamically bounded p-adic CPU model for scoped operations",
"\"id\": \"P261\"",
"Expand p-adic algebra operations and law checks",
"\"status\": \"completed\"",
"\"id\": \"P262\"",
"Extend finite-site sheaf theory beyond locality checks",
"\"status\": \"completed\"",
"\"id\": \"P263\"",
"Promote selected theorem bindings to mandatory proof-assistant evidence profile",
"\"status\": \"completed\"",
"\"id\": \"P264\"",
"Instantiate submission-readiness evidence packet",
"\"status\": \"completed\"",
"P264 instantiated the JSC/SCI-Q2/submission-readiness evidence packet",
"reviewed missing-evidence blocker record",
"P265 converted the post-P264 validation-maintenance state into machine-checked paper artifact guards",
"P266 synchronized CLAIMS.md and the final validation record",
"P267 added explicit fenced claim and validation status blocks",
"P268 moved fenced status block parsing and validation into reusable verify APIs",
"P269 replaced hard-coded status validators with expectation-driven validation APIs",
"P270 made fenced status block parsing fail closed on duplicate keys",
"P271 expanded the dynamically bounded p-adic CPU model",
"dense matrix-matrix multiplication, including high-precision digit tests",
"P272 completed the dynamically bounded p-adic unit arithmetic surface",
"bounded digit inverse, and division",
"P273 added dynamic p-adic matrix utility operations",
"identity-multiplication checks",
"P274 added executable finite-site sheaf restriction-chain evaluation",
"per-step witnesses, final restricted section output",
"P275 added finite-site sheaf inferred gluing",
"callers no longer need to provide a global value manually",
"\"id\": \"P265\"",
"Machine-check validation-maintenance roadmap state",
"\"status\": \"completed\"",
"\"id\": \"P266\"",
"Synchronize claim docs and structure roadmap guards",
"\"status\": \"completed\"",
"\"id\": \"P267\"",
"Add fenced claim and validation status blocks",
"\"status\": \"completed\"",
"\"id\": \"P268\"",
"Move status block validation into verify APIs",
"\"status\": \"completed\"",
"\"id\": \"P269\"",
"Parameterize status block validation expectations",
"\"status\": \"completed\"",
"\"id\": \"P270\"",
"Reject duplicate status block keys",
"\"status\": \"completed\"",
"\"id\": \"P271\"",
"Extend dynamic p-adic vector and matrix operations",
"\"status\": \"completed\"",
"\"id\": \"P272\"",
"Complete dynamic p-adic unit arithmetic operations",
"\"status\": \"completed\"",
"\"id\": \"P273\"",
"Add dynamic p-adic matrix utility operations",
"\"status\": \"completed\"",
"\"id\": \"P274\"",
"Add executable finite-sheaf restriction chains",
"\"status\": \"completed\"",
"\"id\": \"P275\"",
"Infer finite-sheaf glued values from compatible covers",
"\"status\": \"completed\"",
"reject stale P264-selected-next roadmap text",
"Validation-maintenance state is machine-checked against stale roadmap regressions.",
"no SCI-Q2 claim without current authoritative evidence",
"cargo test --offline --features rocm-hip",
"cargo test --offline --features accelerated-pilot --test accelerated_pilot",
"Functional expansion succeeds when P248-P275 tests",
],
);
for obsolete_current_state in [
"\"active_backlog\": []",
"The roadmap is complete when final validation proves",
"P247 is implemented. Journal of Symbolic Computation is the conditional first writing target",
"hard-coded to M=2, K=3, N=2",
"Benchmark rows use single-run local smoke timings",
"not integrated as a planner-selected general backend operation",
"P248, P249, and P250 are implemented; P251 is selected next",
"P248, P249, P250, and P251 are implemented; P252 is selected next",
"P248, P249, P250, P251, and P252 are implemented; P253 is selected next",
"P248, P249, P250, P251, P252, and P253 are implemented; P254 is selected next",
"P248, P249, P250, P251, P252, P253, and P254 are implemented; P255 is selected next",
"P248-P255 are implemented and ready for final validation audit",
"P248-P255 are completed and preserved as validated functional hardening evidence",
"The next roadmap milestone is complete when P248-P255",
"P256 is selected next",
"P256 is complete when a scoped real GPU execution contract exists beyond scaffold fallback",
"P248-P256 are completed and preserved as validated functional hardening evidence",
"P257 is selected next",
"P257 is complete when benchmark artifacts include external baseline and profiler evidence fields",
"P248-P257 are completed and preserved as validated functional hardening evidence",
"P258 is selected next",
"P258 is complete when a ROCm portability evidence matrix exists",
"P248-P258 are completed and preserved as validated functional hardening evidence",
"P259 is selected next",
"P259 is complete when HIP kernel artifacts bind source, compiler, device, code object or disassembly metadata",
"P248-P259 are completed and preserved as validated functional hardening evidence",
"P260 is selected next",
"P260 is complete when an arbitrary-precision or dynamically bounded p-adic CPU model has conversion, valuation, precision truncation, equality, and CPU oracle tests",
"P248-P260 are completed and preserved as validated functional hardening evidence",
"P261 is selected next",
"P261 is complete when scoped p-adic algebra operations and property/law checks extend beyond GEMM-focused arithmetic",
"P248-P261 are completed and preserved as validated functional hardening evidence",
"P262 is selected next",
"P262 is complete when one additional scoped finite-site sheaf construction beyond compatibility/gluing locality has CPU oracle and theorem-binding guards",
"P248-P262 are completed and preserved as validated functional hardening evidence",
"P263 is selected next",
"P263 is complete when a selected theorem subset can require proof-assistant success evidence in strict release profiles",
"P248-P263 are completed and preserved as validated functional hardening evidence",
"P264 is selected next",
"P264 is complete when JSC/SCI-Q2/submission-readiness evidence packet fields are instantiated with reviewed external evidence or explicit missing-evidence blockers",
"P248-P264 are completed and preserved as validated functional hardening evidence",
"P248-P265 are completed and preserved as validated functional hardening evidence",
"P248-P266 are completed and preserved as validated functional hardening evidence",
"P248-P267 are completed and preserved as validated functional hardening evidence",
"P248-P268 are completed and preserved as validated functional hardening evidence",
"P248-P269 are completed and preserved as validated functional hardening evidence",
"GpuScaffoldBackend participates in planning but has no runtime kernels and always reports CPU fallback for executable work",
"checks overlap equality for simple integer sections",
"Default validation records bounded optional Lean behavior and strict failure mode",
"Journal of Symbolic Computation is a conditional writing target, but current SCI indexing",
] {
assert!(
!todo.contains(obsolete_current_state),
"todo should no longer describe the P247 paper-only state as current: {obsolete_current_state}"
);
}
}
#[test]
fn todo_has_structured_validation_maintenance_phase_guards() {
let todo = read_todo_json();
assert_eq!(
todo["current_focus"].as_str(),
Some(
"P248-P275 are completed and preserved as validated functional hardening evidence. The roadmap is in functional-expansion state: extend executable p-adic and sheaf capabilities while preserving claim guards and keeping SCI-Q2 and submission-readiness claims blocked until current external evidence is supplied and reviewed."
),
"todo current_focus should name the current functional-expansion phase range exactly"
);
assert!(
todo["next_success"]
.as_str()
.expect("next_success should be a string")
.contains("Functional expansion succeeds when P248-P275 tests"),
"next_success should name P248-P275 functional-expansion gates"
);
let phases = todo["active_backlog"]
.as_array()
.expect("todo active_backlog should be an array");
let phase_ids = phases
.iter()
.map(|phase| phase["id"].as_str().expect("phase id should be a string"))
.collect::<Vec<_>>();
assert_eq!(
phase_ids,
(248..=275)
.map(|phase| format!("P{phase}"))
.collect::<Vec<_>>(),
"todo active_backlog should contain only contiguous completed P248-P275 phases"
);
for phase in phases {
assert_eq!(
phase["status"].as_str(),
Some("completed"),
"phase {} should be completed",
phase["id"].as_str().unwrap_or("<missing>")
);
}
let p266 = todo_phase(&todo, "P266");
assert_eq!(
p266["implementation_targets"]
.as_array()
.expect("P266 implementation_targets should be an array")
.iter()
.map(|target| target.as_str().expect("target should be a string"))
.collect::<Vec<_>>(),
vec![
"CLAIMS.md",
"docs/paper/final_validation_record.md",
"todo.json",
"tests/paper_artifacts.rs",
],
"P266 should record the synchronized claim-doc and structured-test surface"
);
for required_command in [
"python -m json.tool todo.json >/dev/null",
"cargo fmt --check",
"cargo test --offline --test paper_artifacts",
"cargo test --offline",
] {
assert!(
p266["acceptance_tests"]
.as_array()
.expect("P266 acceptance_tests should be an array")
.iter()
.any(|command| command.as_str() == Some(required_command)),
"P266 acceptance tests should include {required_command}"
);
}
let p267 = todo_phase(&todo, "P267");
assert_eq!(
p267["implementation_targets"]
.as_array()
.expect("P267 implementation_targets should be an array")
.iter()
.map(|target| target.as_str().expect("target should be a string"))
.collect::<Vec<_>>(),
vec![
"CLAIMS.md",
"docs/paper/final_validation_record.md",
"todo.json",
"tests/paper_artifacts.rs",
],
"P267 should record the fenced-status implementation surface"
);
let p268 = todo_phase(&todo, "P268");
assert_eq!(
p268["implementation_targets"]
.as_array()
.expect("P268 implementation_targets should be an array")
.iter()
.map(|target| target.as_str().expect("target should be a string"))
.collect::<Vec<_>>(),
vec![
"src/verify/claim_status.rs",
"src/verify/mod.rs",
"CLAIMS.md",
"docs/paper/final_validation_record.md",
"todo.json",
"tests/paper_artifacts.rs",
],
"P268 should record the reusable verify API surface"
);
let p269 = todo_phase(&todo, "P269");
assert_eq!(
p269["implementation_targets"]
.as_array()
.expect("P269 implementation_targets should be an array")
.iter()
.map(|target| target.as_str().expect("target should be a string"))
.collect::<Vec<_>>(),
vec![
"src/verify/claim_status.rs",
"src/verify/mod.rs",
"CLAIMS.md",
"docs/paper/final_validation_record.md",
"todo.json",
"tests/paper_artifacts.rs",
],
"P269 should record the expectation-driven verify API surface"
);
let p270 = todo_phase(&todo, "P270");
assert_eq!(
p270["implementation_targets"]
.as_array()
.expect("P270 implementation_targets should be an array")
.iter()
.map(|target| target.as_str().expect("target should be a string"))
.collect::<Vec<_>>(),
vec![
"src/verify/claim_status.rs",
"CLAIMS.md",
"docs/paper/final_validation_record.md",
"todo.json",
"tests/paper_artifacts.rs",
],
"P270 should record the duplicate-key parser hardening surface"
);
let p271 = todo_phase(&todo, "P271");
assert_eq!(
p271["implementation_targets"]
.as_array()
.expect("P271 implementation_targets should be an array")
.iter()
.map(|target| target.as_str().expect("target should be a string"))
.collect::<Vec<_>>(),
vec![
"src/domain/padic.rs",
"src/domain/mod.rs",
"tests/padic.rs",
"todo.json",
],
"P271 should record the dynamic p-adic functionality surface"
);
let p272 = todo_phase(&todo, "P272");
assert_eq!(
p272["implementation_targets"]
.as_array()
.expect("P272 implementation_targets should be an array")
.iter()
.map(|target| target.as_str().expect("target should be a string"))
.collect::<Vec<_>>(),
vec!["src/domain/padic.rs", "tests/padic.rs", "todo.json"],
"P272 should record the dynamic p-adic unit arithmetic surface"
);
let p273 = todo_phase(&todo, "P273");
assert_eq!(
p273["implementation_targets"]
.as_array()
.expect("P273 implementation_targets should be an array")
.iter()
.map(|target| target.as_str().expect("target should be a string"))
.collect::<Vec<_>>(),
vec!["src/domain/padic.rs", "tests/padic.rs", "todo.json"],
"P273 should record the dynamic p-adic matrix utility surface"
);
let p274 = todo_phase(&todo, "P274");
assert_eq!(
p274["implementation_targets"]
.as_array()
.expect("P274 implementation_targets should be an array")
.iter()
.map(|target| target.as_str().expect("target should be a string"))
.collect::<Vec<_>>(),
vec!["src/object/sheaf.rs", "tests/sheaf.rs", "todo.json"],
"P274 should record the finite-sheaf restriction-chain surface"
);
let p275 = todo_phase(&todo, "P275");
assert_eq!(
p275["implementation_targets"]
.as_array()
.expect("P275 implementation_targets should be an array")
.iter()
.map(|target| target.as_str().expect("target should be a string"))
.collect::<Vec<_>>(),
vec!["src/object/sheaf.rs", "tests/sheaf.rs", "todo.json"],
"P275 should record the finite-sheaf inferred-gluing surface"
);
}
#[test]
fn todo_preserves_paper_route_as_historical_capability() {
let todo = fs::read_to_string("todo.json").expect("todo.json should exist");
assert_contains_all(
"todo preserved paper evidence",
&todo,
&[
"Theory contracts, theorem bindings, semantic conformance reports, support matrices, release gates, optional Lean timeout and success-transcript handling, schema guards, and generated paper artifacts are implemented and tested.",
"ROCm/HIP hardware detection, dense i32 HIP add, p-adic valuation HIP helper, finite-site sheaf overlap helper, and valuation-stratified p-adic GEMM pilot execute behind feature gates",
"Feature-gated p-adic benchmark artifacts emit dense CPU, certified sparse CPU, HIP-or-fallback rows",
"Paper route through P247 is preserved",
"JSC is the conditional first writing target",
],
);
for obsolete_active_item in [
"Revision response package template",
"\"id\": \"P146\"",
"\"id\": \"P150\"",
"\"id\": \"P160\"",
"\"id\": \"P176\"",
"\"as_of_phase\"",
"\"recent_completed_phases\"",
"\"id\": \"P177\"",
"\"id\": \"P193\"",
"\"id\": \"P200\"",
"\"id\": \"P201\"",
"\"id\": \"P202\"",
"\"id\": \"P203\"",
"\"id\": \"P204\"",
"\"id\": \"P205\"",
"\"id\": \"P206\"",
"\"id\": \"P207\"",
"\"id\": \"P208\"",
"\"id\": \"P209\"",
"\"id\": \"P210\"",
"\"id\": \"P211\"",
"\"id\": \"P212\"",
"\"id\": \"P213\"",
"\"id\": \"P214\"",
"\"id\": \"P215\"",
"\"id\": \"P216\"",
"\"id\": \"P217\"",
"\"id\": \"P218\"",
"\"id\": \"P219\"",
"\"id\": \"P220\"",
"\"id\": \"P221\"",
"\"id\": \"P222\"",
] {
assert!(
!todo.contains(obsolete_active_item),
"todo should not keep obsolete completed-phase item {obsolete_active_item}"
);
}
}
#[test]
fn paper_artifact_documents_remain_available_as_historical_evidence() {
for path in [
"ARTIFACT.md",
"CLAIMS.md",
"docs/paper/formal_model.md",
"docs/paper/proof_assistant_scope.md",
"docs/paper/trust_model.md",
"docs/paper/evaluation_methodology.md",
"docs/paper/manuscript_skeleton.md",
"docs/paper/final_submission_readiness.md",
"docs/paper/post_submission_tracking_template.md",
"docs/theory_support_matrix.md",
"docs/theory_engineering_release_gate.md",
"docs/certified_valuation_sparse_padic_matmul.md",
"docs/valuation_stratified_padic_matmul_admission.md",
"docs/rocm_hip_padic_stratified_matmul.md",
"docs/rocm_padic_stratified_benchmarks.md",
"docs/certified_padic_gemm_release_gate.md",
"docs/paper/certified_padic_gemm_manuscript_delta.md",
] {
assert!(
Path::new(path).exists(),
"historical paper artifact should exist: {path}"
);
}
let formal_model = fs::read_to_string("docs/paper/formal_model.md")
.expect("formal model document should exist");
assert_contains_all(
"formal model",
&formal_model,
&[
"Trace-Bound Semantic Evidence Soundness",
"Registry-Aware Lowering Obligation Traceability",
"Nonstandard-Domain Obligation Coverage",
"p-adic valuation cutoff",
"Sheaf cover compatibility and gluing",
],
);
let p222_delta = fs::read_to_string("docs/paper/certified_padic_gemm_manuscript_delta.md")
.expect("P222 manuscript delta should exist");
assert_contains_all(
"P222 manuscript delta",
&p222_delta,
&[
"certified valuation-sparse fixed-precision p-adic GEMM",
"per-output certificates",
"dense CPU and certified sparse CPU oracles",
"ROCm/HIP pilot",
"Related-Work Boundary",
"Experiment Table Plan",
"Readiness Audit",
"not verified HIP machine code",
"not production speedup",
],
);
let methodology = fs::read_to_string("docs/paper/evaluation_methodology.md")
.expect("evaluation methodology should exist");
assert_contains_all(
"evaluation methodology",
&methodology,
&[
"CPU reference backend",
"p-adic",
"sheaf",
"proof-trace",
"baseline",
],
);
}
#[test]
fn readiness_audit_tracks_current_padic_gemm_final_validation_status() {
let readiness_audit =
fs::read_to_string("docs/paper/readiness_audit.md").expect("readiness audit should exist");
let normalized = collapse_whitespace(&readiness_audit);
assert_contains_all(
"P232 readiness audit",
&normalized,
&[
"This audit is synchronized through P241",
"This audit is synchronized through P255",
"P255 Functional Hardening Readiness Snapshot",
"P248-P254 complete the functional hardening roadmap",
"runtime-shape p-adic GEMM",
"real feature-gated dense integer add selection through public APIs",
"multi-overlap finite-site sheaf locality provenance",
"optional Lean success transcripts",
"claim_allowed=false",
"Current remaining repository blockers: none identified",
"P241 Current Manuscript Draft Readiness Snapshot",
"P240 closed the earlier manuscript-assembly gap",
"continuous draft for the certified",
"valuation-sparse fixed-precision p-adic GEMM route",
"theorem-bound skip certificates",
"dense CPU and certified sparse CPU oracle agreement",
"feature-gated ROCm/HIP pilot evidence",
"deterministic benchmark artifacts",
"fail-closed release gates",
"Historical P155 manuscript gap",
"Superseded",
"Continuous manuscript draft follows the current claim route",
"docs/paper/manuscript_draft.md",
"Historical P155 SCI-Q2 Submission Gap Audit",
"now itself superseded for current planning by P240/P241",
"No current skeleton-only blocker remains for the scoped C10 repository package",
"P240 assembled and synchronized the continuous manuscript draft",
"Historical P161 Manuscript Submission Readiness Audit",
"now superseded for current planning by P240-P243",
"P240 front matter leads with certified valuation-sparse p-adic GEMM",
"Historical consistency gap",
"Superseded by P242/P243 synchronization",
"P242 synchronizes the submission checklist and final readiness entry point",
"P243 synchronizes the final decision tail",
"no longer an active next backlog",
"P232 Current Readiness Snapshot",
"Current repository-level blockers",
"none identified for the scoped certified valuation-sparse p-adic GEMM",
"Current final-validation scope",
"feature-gated ROCm/HIP p-adic GEMM gate",
"rocm_padic_stratified_benchmarks",
"artifact id, certificate coverage, closed speed-claim guard",
"bounded optional Lean timeout evidence",
"Current Remaining Work Classification",
"The active roadmap backlog is empty",
"Current Next Action Policy",
"No new P128/P156-style implementation backlog is active",
"Historical P127/P128 Blocker Audit",
"They now survive only as revision, camera-ready, or",
],
);
let current_section = readiness_audit
.split("## Historical P127/P128 Blocker Audit")
.next()
.expect("readiness audit should have current section before historical audit");
for stale_current_claim in [
"Remaining SCI-Q2 Blockers",
"Next Backlog Recommendation",
"P128 should target",
"P156 should target",
"highest remaining blocker",
] {
assert!(
!current_section.contains(stale_current_claim),
"P232 current readiness section should not keep stale active-backlog text: {stale_current_claim}"
);
}
let historical_p155_section = readiness_audit
.split("## Historical P155 SCI-Q2 Submission Gap Audit")
.nth(1)
.expect("readiness audit should retain historical P155 section");
for stale_current_claim in [
"Text is now defensible, but it still needs to be assembled into a manuscript draft.",
"The repository has a skeleton rather than a continuous draft; this is the highest-value next phase.",
"P156 should assemble a manuscript draft document from the existing skeleton",
"P156 should target manuscript assembly, not another isolated feature.",
"implementation evidence, formal scope, evaluation tables, optional proof\nassistant boundary, reproducibility path, and novelty boundaries now exist but\nremain spread across multiple files",
] {
assert!(
!historical_p155_section.contains(stale_current_claim),
"P241 readiness audit should not keep stale P155 manuscript-gap text as current state: {stale_current_claim}"
);
}
let historical_p161_section = readiness_audit
.split("## Historical P161 Manuscript Submission Readiness Audit")
.nth(1)
.expect("readiness audit should retain historical P161 section");
for stale_current_claim in [
"## P161 Current Manuscript Submission Readiness Audit",
"`docs/paper/manuscript_draft.md` P160 front matter names trace-bound semantic evidence",
"`docs/paper/final_submission_readiness.md` still reflects the older P132 skeleton-era state",
"Select P162 to update final readiness and submission package index.",
"P162 should target submission package consistency hardening.",
"with the P156-P160 manuscript package",
] {
assert!(
!historical_p161_section.contains(stale_current_claim),
"P244 readiness audit should not keep stale P161 current-action text: {stale_current_claim}"
);
}
}
#[test]
fn table_figure_plan_tracks_current_padic_gemm_claim_route() {
let table_plan = fs::read_to_string("docs/paper/table_figure_plan.md")
.expect("table and figure plan should exist");
assert_contains_all(
"P233 table and figure plan",
&table_plan,
&[
"P233 Current Claim Route",
"synchronized through P233",
"certified valuation-sparse",
"fixed-precision p-adic GEMM",
"feature-gated ROCm/HIP evidence",
"Certified p-adic GEMM, as the primary manuscript claim",
"default paper-result artifacts from `paper_benchmarks`",
"feature-gated certified p-adic GEMM benchmark JSON/CSV/Markdown artifacts",
"schema-guarded release, support-matrix, and benchmark artifacts",
"optional theorem-checker timeout behavior as reproducibility evidence",
"Certified p-adic GEMM benchmark matrix",
"Figure 4: Certified p-adic GEMM evidence chain",
"local ROCm/HIP pilot rows",
"portable GPU support, verified HIP machine code, or production accelerator",
],
);
for stale_current_claim in [
"research claim remains the scoped integration of proof-aware adaptive operator",
"The current execution evidence uses a CPU reference backend; table captions",
] {
assert!(
!table_plan.contains(stale_current_claim),
"P233 table plan should not keep stale current-claim text: {stale_current_claim}"
);
}
}
#[test]
fn related_work_synthesis_tracks_current_padic_gemm_claim_route() {
let related_work = fs::read_to_string("docs/paper/related_work_synthesis.md")
.expect("related work synthesis should exist");
assert_contains_all(
"P234 related-work synthesis",
&related_work,
&[
"P234 Current Related-Work Claim Route",
"synchronized through P234",
"certified valuation-sparse",
"fixed-precision p-adic GEMM",
"theorem-bound per-output skip",
"certificates",
"dense CPU and",
"certified sparse CPU oracle agreement",
"feature-gated ROCm/HIP pilot evidence",
"fail-closed release gates in one auditable artifact",
"older proof-aware adaptive runtime framing remains supporting",
"infrastructure for traceability",
"primary novelty anchor while C10",
"Compact novelty anchor: certified valuation-sparse p-adic GEMM",
"feature-gated ROCm/HIP pilot rows",
"record local execution evidence",
"release gates prevent unsupported claims",
"docs/paper/certified_padic_gemm_manuscript_delta.md",
],
);
let current_novelty_section = related_work
.split("## No-Overclaim Boundaries")
.next()
.expect("related-work synthesis should have current novelty text");
for stale_current_claim in [
"Compact novelty anchor: proof-aware adaptive operator planning",
"Tokitai integrates proof-aware adaptive operator planning, domain-aware adaptive",
] {
assert!(
!current_novelty_section.contains(stale_current_claim),
"P234 related-work synthesis should not keep stale primary novelty text: {stale_current_claim}"
);
}
}
#[test]
fn manuscript_skeleton_tracks_current_padic_gemm_claim_route() {
let skeleton = fs::read_to_string("docs/paper/manuscript_skeleton.md")
.expect("manuscript skeleton should exist");
assert_contains_all(
"P235 manuscript skeleton",
&skeleton,
&[
"Certified Valuation-Sparse p-adic GEMM with Trace-Bound",
"P235 Current Manuscript Skeleton Route",
"synchronized through P235",
"certified valuation-sparse fixed-precision p-adic GEMM",
"valuation-bucket fingerprints",
"theorem-bound skip certificates",
"dense CPU and",
"certified sparse CPU oracle agreement",
"feature-gated ROCm/HIP pilot evidence",
"C1-C9 remain",
"supporting traceability",
"The core contribution is the certified p-adic GEMM pipeline",
"primary",
"novelty anchor",
"C10 `certified_valuation_sparse_padic_gemm`",
"docs/paper/certified_padic_gemm_manuscript_delta.md",
"target/paper-results/padic-stratified-benchmarks/padic-stratified-benchmarks.csv",
"release gates prevent",
"certified valuation-sparse",
"fixed-precision p-adic GEMM is feasible",
"auditable algorithm-system",
"The proof-carrying adaptive operator machinery remains",
"supporting infrastructure for trace-bound evidence",
"claim scoped to the certified p-adic GEMM pipeline",
"verified machine code, or production speedup",
],
);
for stale_current_claim in [
"Working title: Proof-Carrying Adaptive Operator Execution",
"The core contribution is a Rust proof-aware adaptive operator runtime",
"Tokitai integrates proof-aware adaptive operator planning, nonstandard-domain contracts",
"Tokitai's manuscript should conclude that proof-carrying adaptive operator\nexecution is feasible as a research artifact",
] {
assert!(
!skeleton.contains(stale_current_claim),
"P235 manuscript skeleton should not keep stale primary-claim text: {stale_current_claim}"
);
}
}
#[test]
fn contribution_map_tracks_current_padic_gemm_claim_route() {
let contribution_map = fs::read_to_string("docs/paper/contribution_map.md")
.expect("contribution map should exist");
assert_contains_all(
"P236 contribution map",
&contribution_map,
&[
"synchronized through P236",
"C10 certified valuation-sparse p-adic GEMM",
"C1-C9 remain",
"supporting traceability",
"P236 Prior-Art And Novelty Boundary Matrix",
"scoped algorithm-system claim",
"theorem-bound skip",
"certificates",
"dense CPU and certified sparse CPU oracle agreement",
"feature-gated ROCm/HIP pilot evidence",
"fail-closed non-claim gates",
"older trace-bound runtime machinery as supporting infrastructure",
"Tokitai integrates certified valuation-sparse fixed-precision p-adic GEMM",
"release gates prevent unsupported claims",
"verified machine code, or production speedup",
],
);
let current_novelty_section = contribution_map
.split("### P154 No-Overclaim Checklist")
.next()
.expect("contribution map should have current novelty section");
for stale_current_claim in [
"Tokitai integrates proof-aware adaptive operator planning and domain-aware adaptive operator planning",
"Tokitai's SCI-Q2 novelty claim is an integrated systems claim: domain-aware",
"is missing.\nis missing.",
] {
assert!(
!current_novelty_section.contains(stale_current_claim),
"P236 contribution map should not keep stale current-claim text: {stale_current_claim}"
);
}
}
#[test]
fn outline_tracks_current_padic_gemm_claim_route() {
let outline = fs::read_to_string("docs/paper/outline.md").expect("paper outline should exist");
assert_contains_all(
"P237 paper outline",
&outline,
&[
"Certified Valuation-Sparse p-adic GEMM with Trace-Bound Semantic Evidence",
"P237 Current Outline Route",
"synchronized through P237",
"certified valuation-sparse fixed-precision p-adic GEMM",
"per-output certificates expose theorem",
"dense CPU and certified sparse CPU oracles validate supported",
"feature-gated ROCm/HIP pilot rows",
"Trace-bound proof evidence",
"C10",
"valuation-bucket fingerprints and theorem-bound skip certificates",
"dense CPU and certified sparse CPU oracle agreement",
"deterministic benchmark distributions",
"docs/paper/certified_padic_gemm_manuscript_delta.md",
"src/backend/hip_padic_benchmarks.rs",
"cargo run --quiet --offline --features rocm-hip --example rocm_padic_stratified_benchmarks",
"target/paper-results/padic-stratified-benchmarks/padic-stratified-benchmarks.csv",
"Which valuation distributions produce skipped products",
"block production speedup",
"feature-gated ROCm/HIP evidence",
],
);
for stale_current_claim in [
"Working title: Proof-Carrying Adaptive Operator Execution",
"Scope: Rust reference runtime for proof-aware adaptive operators",
"contract-driven adaptive planning",
"The claimed novelty is theorem-result-level validation for",
] {
assert!(
!outline.contains(stale_current_claim),
"P237 outline should not keep stale current-route text: {stale_current_claim}"
);
}
}
#[test]
fn top_level_claims_trace_tracks_current_padic_gemm_paper_route() {
let claims = fs::read_to_string("CLAIMS.md").expect("CLAIMS.md should exist");
assert_contains_all(
"P238 CLAIMS trace",
&claims,
&[
"P440 Current Paper Claim Route",
"P440 Validation-Maintenance Claim Audit",
"P257 Speed Evidence Claim Gate",
"external-baseline and profiler-evidence fields",
"production speedup remains blocked",
"P258 ROCm Portability Claim Gate",
"remains blocked until at least two reviewed passing device/compiler",
"P248-P269 have hardened previously",
"runtime-shape ROCm/HIP",
"p-adic GEMM fixtures",
"public prefer-gpu dense integer add",
"selection, multi-overlap finite-site sheaf locality evidence",
"multi-overlap finite-site sheaf locality evidence",
"optional Lean success transcripts",
"JSC target verification packet blockers",
"post-P264 validation-maintenance guards",
"synchronized through P440",
"tokitai-claim-status-v1",
"certified valuation-sparse fixed-precision p-adic GEMM",
"theorem-bound skip certificates",
"dense CPU and certified sparse CPU oracle",
"feature-gated ROCm/HIP pilot evidence",
"deterministic benchmark",
"audit-gated non-claims",
"not be read as the current manuscript",
"claim numbering",
"docs/paper/contribution_map.md",
"docs/paper/certified_padic_gemm_manuscript_delta.md",
"older proof-aware",
"For paper drafting, frame the library around certified valuation-sparse",
"Treat proof-aware",
"not the primary paper claim",
],
);
for stale_current_claim in [
"For paper drafting, frame the library as a proof-aware operator compiler",
"with p-adic and finite-sheaf prototypes as demonstrations",
"This claim trace is synchronized through P238",
"P255 Functional Hardening Claim Audit",
"This claim trace is synchronized through P266",
"This claim trace is synchronized through P267",
"This claim trace is synchronized through P268",
"This claim trace is synchronized through P269",
] {
assert!(
!claims.contains(stale_current_claim),
"P238 CLAIMS.md should not keep stale paper-drafting route text: {stale_current_claim}"
);
}
validate_status_block(&claims, ¤t_claim_status_expectation())
.expect("CLAIMS.md claim status block should validate against current expectation");
validate_claim_status_block(&claims)
.expect("CLAIMS.md convenience claim status validator should use current expectation");
assert!(
validate_status_block(&claims, &p268_claim_status_expectation()).is_err(),
"current CLAIMS.md should not satisfy stale P268 claim status expectation"
);
let duplicate_key_claim_status = "```tokitai-claim-status-v1\nphase=P270\nphase=P269\n```";
let duplicate_err = parse_status_block(duplicate_key_claim_status, "tokitai-claim-status-v1")
.expect_err("duplicate status keys should fail closed");
assert!(
duplicate_err.to_string().contains("duplicate key phase"),
"duplicate-key error should name the repeated key: {duplicate_err}"
);
}
#[test]
fn venue_controls_track_current_padic_gemm_claim_fit_route() {
let docs = [
(
"venue shortlist protocol",
"docs/paper/venue_shortlist_protocol.md",
),
("venue decision brief", "docs/paper/venue_decision_brief.md"),
(
"venue evidence request",
"docs/paper/venue_evidence_request.md",
),
(
"venue evidence matrix",
"docs/paper/venue_evidence_matrix.md",
),
(
"venue evidence integration",
"docs/paper/venue_evidence_integration.md",
),
];
for (label, path) in docs {
let content = fs::read_to_string(path).expect("venue control document should exist");
let normalized = collapse_whitespace(&content);
assert_contains_all(
label,
&normalized,
&[
"P239 Current Claim-Fit Route",
"synchronized through P239",
"certified valuation-sparse",
"fixed-precision p-adic GEMM",
"theorem-bound skip certificates",
"dense CPU and",
"certified sparse CPU oracle",
"feature-gated ROCm/HIP pilot evidence",
"deterministic benchmark",
"fail-closed non-claim gates",
],
);
}
let shortlist = fs::read_to_string("docs/paper/venue_shortlist_protocol.md")
.expect("venue shortlist protocol should exist");
let shortlist = collapse_whitespace(&shortlist);
assert_contains_all(
"P239 shortlist claim fit",
&shortlist,
&[
"Record why Tokitai's certified valuation-sparse p-adic GEMM package fits the venue",
"Can the manuscript present certified valuation-sparse p-adic GEMM",
"portable GPU support, verified HIP machine code, or complete p-adic algebra",
],
);
let decision = fs::read_to_string("docs/paper/venue_decision_brief.md")
.expect("venue decision brief should exist");
let decision = collapse_whitespace(&decision);
assert_contains_all(
"P239 venue decision brief claim fit",
&decision,
&[
"Journal of Symbolic Computation is the conditional first writing target",
"claim-fit selection, not a SCI-Q2 or acceptance-readiness claim",
"P247 Conditional Target Selection",
"Target-specific draft: `docs/paper/jsc_submission_draft.md`",
"do not claim SCI-Q2 status",
"certified p-adic GEMM artifact system with reproducible evidence gates",
"not the first sentence of the venue pitch",
"certified p-adic GEMM, proof evidence, symbolic mathematics",
],
);
let request = fs::read_to_string("docs/paper/venue_evidence_request.md")
.expect("venue evidence request should exist");
let request = collapse_whitespace(&request);
assert_contains_all(
"P239 venue evidence request claim fit",
&request,
&[
"Do not ask authors to validate an old proof-carrying adaptive runtime pitch",
"certified p-adic GEMM artifact system with",
"theorem-bound certificates and reproducible artifacts",
],
);
let matrix = fs::read_to_string("docs/paper/venue_evidence_matrix.md")
.expect("venue evidence matrix should exist");
let matrix = collapse_whitespace(&matrix);
assert_contains_all(
"P239 venue evidence matrix claim fit",
&matrix,
&[
"Existing public evidence rows are unchanged",
"no row gains SCI-Q2, indexing, scope-fit, article-type, or",
"artifact-policy status from this synchronization",
"article type fit for a certified p-adic GEMM artifact system",
"Conditional first writing target",
"automated theorem proving",
"System Descriptions",
"jsc_target_verification_packet.md",
"P264 JSC Missing-Evidence Instantiation",
"missing-evidence blocker record",
"sci_q2_claim_allowed=false",
"submission_readiness_claim_allowed=false",
],
);
let packet = fs::read_to_string("docs/paper/jsc_target_verification_packet.md")
.expect("JSC target verification packet should exist");
let packet_normalized = collapse_whitespace(&packet);
assert_contains_all(
"P264 JSC target verification packet",
&packet_normalized,
&[
"Journal of Symbolic Computation Target Verification Packet",
"Packet status: P264 instantiated missing-evidence blocker packet",
"machine-checkable evidence checklist",
"packet_instantiation_status=instantiated_missing_evidence_blockers",
"packet_reviewer=Codex-P264",
"current_sci_indexing",
"current_jcr_quartile",
"article_type_fit",
"artifact_policy",
"apc_or_cost_route",
"formatting_requirements",
"requires_author_supplied_clarivate_or_jcr_evidence=true",
"requires_author_article_type_approval=true",
"requires_author_cost_route_approval=true",
"sci_q2_claim_allowed=false",
"submission_readiness_claim_allowed=false",
"acceptance_probability_claim_allowed=false",
"current_sci_indexing.blocker=missing_current_clarivate_or_institutional_sci_export",
"current_jcr_quartile.blocker=missing_current_jcr_year_category_quartile_source",
"article_type_fit.blocker=missing_reviewed_current_jsc_article_type_fit",
"artifact_policy.blocker=missing_reviewed_current_jsc_artifact_policy",
"apc_or_cost_route.blocker=missing_author_approved_current_cost_route",
"formatting_requirements.blocker=missing_reviewed_current_formatting_requirements",
"Current packet value",
"<missing-author-evidence>",
"Do not quote JCR quartile without JCR year and category",
"No SCI-Q2 claim without current JCR or equivalent verified evidence",
"P254 Packet Decision",
"P264 Packet Instantiation",
"reviewed hold record",
],
);
for overclaim in [
"sci_q2_claim_allowed=true",
"submission_readiness_claim_allowed=true",
"acceptance_probability_claim_allowed=true",
"current_sci_indexing.status=verified",
"current_jcr_quartile.status=verified",
] {
assert!(
!packet.contains(overclaim),
"P264 JSC verification packet must stay claim-closed without external evidence: {overclaim}"
);
}
let integration = fs::read_to_string("docs/paper/venue_evidence_integration.md")
.expect("venue evidence integration should exist");
let integration = collapse_whitespace(&integration);
assert_contains_all(
"P239 venue integration claim fit",
&integration,
&[
"must not replace the certified p-adic GEMM route",
"changing labels or starting target-specific formatting",
],
);
for (label, path) in docs {
let content = fs::read_to_string(path).expect("venue control document should exist");
for stale_current_claim in [
"Tokitai's proof-carrying adaptive operator runtime fits the venue",
"trace-bound proof-carrying adaptive operator execution",
"article type fit for a proof-carrying runtime artifact",
"Which article type best fits a proof-carrying adaptive operator runtime",
"It may fit Tokitai as a proof-carrying adaptive operator runtime",
] {
assert!(
!content.contains(stale_current_claim),
"{label} should not keep stale venue claim-fit route text: {stale_current_claim}"
);
}
}
}
#[test]
fn jsc_submission_draft_targets_symbolic_computation_without_sciq2_overclaim() {
let draft = fs::read_to_string("docs/paper/jsc_submission_draft.md")
.expect("JSC target submission draft should exist");
let normalized = collapse_whitespace(&draft);
assert_contains_all(
"P247 JSC submission draft",
&normalized,
&[
"Journal of Symbolic Computation Submission Draft",
"Target venue: Journal of Symbolic Computation",
"conditional first target",
"symbolic objects",
"algebraic objects",
"automated theorem proving",
"symbolic computation systems",
"System Descriptions",
"Current SCI indexing, JCR quartile, and SCI-Q2 status still require author-side verification",
"Target verification packet",
"docs/paper/jsc_target_verification_packet.md",
"sci_q2_claim_allowed=false",
"submission_readiness_claim_allowed=false",
"Certified Valuation-Sparse p-adic GEMM with Trace-Bound Semantic Evidence",
"auditable symbolic-computation artifact",
"per-output certificates",
"dense CPU and certified sparse CPU oracles",
"feature-gated ROCm/HIP pilot",
"schema-guarded JSON/CSV/Markdown artifacts",
"not a general p-adic algebra system",
"not portable AMD GPU support",
"not a production speedup claim",
"Keywords",
"p-adic arithmetic",
"symbolic computation",
"certified algorithms",
"The manuscript makes five contributions",
"A certified valuation-sparse fixed-precision p-adic GEMM pipeline",
"The problem is not merely sparse matrix multiplication",
"Tokitai separates semantic operators from backend lowerings",
"The ROCm/HIP pilot is feature-gated and intentionally narrow",
"The evaluation is artifact-centered",
"This positioning fits Journal of Symbolic Computation only if",
"The reviewer entry point is `ARTIFACT.md`",
"docs/paper/final_validation_record.md",
"Submission Risks Before First Upload",
"Verify Journal of Symbolic Computation SCI indexing and JCR quartile",
],
);
for stale_or_overclaim in [
"SCI-Q2 status is verified",
"accepted by Journal of Symbolic Computation",
"portable AMD GPU support is demonstrated",
"production speedup is demonstrated",
"HIP machine code is verified",
"a complete p-adic algebra system",
] {
assert!(
!draft.contains(stale_or_overclaim),
"P247 JSC draft should not overclaim target or technical status: {stale_or_overclaim}"
);
}
}
#[test]
fn manuscript_draft_tracks_current_padic_gemm_claim_route() {
let draft = fs::read_to_string("docs/paper/manuscript_draft.md")
.expect("continuous manuscript draft should exist");
let normalized = collapse_whitespace(&draft);
assert_contains_all(
"P240 manuscript draft",
&normalized,
&[
"Certified Valuation-Sparse p-adic GEMM With Trace-Bound Semantic Evidence",
"P255 Functional Hardening Synchronization",
"P248-P254 hardening route adds runtime-shape ROCm/HIP p-adic GEMM evidence",
"public prefer-gpu dense integer add selection",
"multi-overlap finite-site sheaf locality evidence",
"optional Lean success-transcript capture",
"claim-guarded JSC target verification packet",
"P240 Current Manuscript Draft Route",
"synchronized through P240",
"primary manuscript claim is certified valuation-sparse fixed-precision p-adic GEMM",
"valuation-bucket fingerprints",
"theorem-bound skip certificates",
"dense CPU and certified sparse CPU oracles",
"feature-gated ROCm/HIP pilot rows",
"deterministic benchmark artifacts",
"fail-closed release gates",
"C1-C9 remain supporting",
"certified p-adic GEMM plus the evidence infrastructure",
"scoped algorithm-system claim",
"C10) as the primary route",
"feature-gated certified p-adic GEMM benchmark emits",
"padic-stratified-benchmarks.json",
"padic-stratified-benchmarks.csv",
"speed_claim_allowed",
"cargo test --offline --features rocm-hip --test rocm_padic_stratified_benchmarks",
"P222/P234 rather than the older P154 primary framing",
"not sparse GEMM alone",
"not GPU exact arithmetic",
"This draft now follows the P240 route",
"final paper claim should remain certified valuation-sparse p-adic GEMM",
"verified HIP machine code",
],
);
for stale_current_claim in [
"# Proof-Carrying Adaptive Operator Execution For Nonstandard Mathematical Domains",
"The novelty boundary follows P154: Tokitai integrates proof-aware adaptive",
"The evaluation answers three questions.",
"This draft follows P155's selection",
"Tokitai demonstrates that adaptive operator execution can be organized around",
"an integrated proof-carrying adaptive operator evidence claim",
] {
assert!(
!draft.contains(stale_current_claim),
"P240 manuscript draft should not keep stale primary-route text: {stale_current_claim}"
);
}
}
#[test]
fn schemas_and_audit_examples_remain_part_of_the_validation_surface() {
for path in [
"docs/schemas/tokitai-artifacts-v1.schema.json",
"docs/schemas/tokitai-paper-csv-v1.schema.json",
"docs/paper/schema_inventory.md",
"docs/paper/rocm_portability_matrix.md",
"examples/audit_traces.rs",
"examples/paper_benchmarks.rs",
"tests/audit_traces_example.rs",
"tests/json_parser_regression.rs",
"tests/paper_benchmarks_example.rs",
"tests/finite_sheaf_gluing_theorem.rs",
"tests/padic_valuation_skip_theorem.rs",
"tests/theory_support_matrix.rs",
"tests/theory_release_gate.rs",
"tests/schema_guards.rs",
"docs/theorems/finite_sheaf_gluing.lean",
"docs/theorems/padic_valuation_skip.lean",
"scripts/check_finite_sheaf_gluing_theorem.sh",
"scripts/check_padic_valuation_skip_theorem.sh",
] {
assert!(
Path::new(path).exists(),
"validation artifact should exist: {path}"
);
}
let schema_inventory = fs::read_to_string("docs/paper/schema_inventory.md")
.expect("schema inventory should exist");
assert_contains_all(
"P260 schema inventory",
&schema_inventory,
&[
"P260 Dynamic P-Adic CPU Model Note",
"This inventory is synchronized through P260",
"dynamically bounded p-adic CPU model",
"canonical base-p digits",
"not GPU arbitrary precision support",
"P255 Schema And Artifact Surface Synchronization",
"post-hardening artifact package",
"repeated p-adic benchmark timing summaries keep `speed_claim_allowed=false`",
"optional Lean success transcript evidence",
"JSC target verification packet remains a Markdown evidence template",
"P255 does not introduce a new schema version",
],
);
let portability_matrix = fs::read_to_string("docs/paper/rocm_portability_matrix.md")
.expect("ROCm portability matrix should exist");
assert_contains_all(
"P258 ROCm portability matrix",
&portability_matrix,
&[
"ROCm Portability Matrix",
"claim_allowed: false",
"portable ROCm support requires at least two reviewed passing device/compiler combinations",
"single-host or unreviewed device evidence is not portable ROCm support",
"does not claim portable ROCm support",
],
);
let artifact_schema = fs::read_to_string("docs/schemas/tokitai-artifacts-v1.schema.json")
.expect("artifact schema should exist");
assert_contains_all(
"artifact schema",
&artifact_schema,
&[
"tokitai-proof-replay-trace-manifest",
"tokitai-proof-replay-report",
"tokitai-proof-assistant-adapter-registry",
"tokitai-paper-benchmark-results",
],
);
}
#[test]
fn release_docs_include_feature_gated_padic_gemm_benchmark_gate() {
let release_checklist = fs::read_to_string("docs/paper/release_checklist.md")
.expect("release checklist should exist");
assert_contains_all(
"release checklist feature-gated p-adic GEMM benchmark gate",
&release_checklist,
&[
"Feature-Gated ROCm/HIP p-adic GEMM Reproduction",
"cargo test --offline --features rocm-hip --test rocm_padic_stratified_benchmarks",
"cargo run --quiet --offline --features rocm-hip --example rocm_padic_stratified_benchmarks",
"target/paper-results/padic-stratified-benchmarks/padic-stratified-benchmarks.json",
"\"artifact\":\"tokitai-padic-stratified-matmul-benchmark-report\"",
"\"certificate_coverage\":true",
"\"speed_claim_allowed\":false",
"not a production speedup",
"portable AMD GPU support claim",
],
);
let release_manifest = fs::read_to_string("docs/paper/release_bundle_manifest.md")
.expect("release bundle manifest should exist");
assert_contains_all(
"release bundle manifest feature-gated p-adic GEMM benchmark inventory",
&release_manifest,
&[
"Feature-Gated Certified p-adic GEMM Benchmark Results",
"src/backend/hip_padic_benchmarks.rs",
"examples/rocm_padic_stratified_benchmarks.rs",
"tests/rocm_padic_stratified_benchmarks.rs",
"cargo test --offline --features rocm-hip --test rocm_padic_stratified_benchmarks",
"cargo run --quiet --offline --features rocm-hip --example rocm_padic_stratified_benchmarks",
"tokitai-padic-stratified-matmul-benchmark-report",
"speed-claim guard fields",
"HIP rows as local validation evidence only",
],
);
let submission_checklist = fs::read_to_string("docs/paper/submission_checklist.md")
.expect("submission checklist should exist");
let normalized_submission_checklist = collapse_whitespace(&submission_checklist);
assert_contains_all(
"submission checklist feature-gated p-adic GEMM benchmark validation",
&normalized_submission_checklist,
&[
"P242 Current Submission Package Route",
"synchronized through P242",
"P240 continuous manuscript draft",
"certified valuation-sparse fixed-precision p-adic GEMM route",
"theorem-bound skip certificates",
"dense CPU and certified sparse CPU oracle agreement",
"feature-gated ROCm/HIP pilot evidence",
"deterministic benchmark artifacts",
"schema-guarded release/support/benchmark outputs",
"fail-closed non-claim gates",
"P241 `docs/paper/readiness_audit.md` is the current readiness audit",
"P240 continuous paper body led by certified valuation-sparse p-adic GEMM",
"P242 synchronized entry point and go/no-go source for the current C10 route",
"old P155 manuscript gap superseded by the P240 continuous draft",
"Certified p-adic GEMM benchmark JSON",
"Certified p-adic GEMM benchmark CSV",
"cargo test --offline --features rocm-hip --test rocm_padic_stratified_benchmarks",
"cargo run --quiet --offline --features rocm-hip --example rocm_padic_stratified_benchmarks",
"local smoke evidence, not production speedup",
],
);
for stale_current_claim in [
"Current author-facing paper body with P160 front matter and contribution list",
"P162 synchronized entry point and go/no-go source",
"P161 audit and phase selection evidence",
] {
assert!(
!submission_checklist.contains(stale_current_claim),
"P242 submission checklist should not keep stale package-route text: {stale_current_claim}"
);
}
let artifact_guide = fs::read_to_string("ARTIFACT.md").expect("ARTIFACT.md should exist");
assert_contains_all(
"artifact guide feature-gated p-adic GEMM benchmark validation",
&artifact_guide,
&[
"Regenerate Feature-Gated p-adic GEMM Benchmarks",
"cargo test --offline --features rocm-hip --test rocm_padic_stratified_benchmarks",
"cargo run --quiet --offline --features rocm-hip --example rocm_padic_stratified_benchmarks",
"target/paper-results/padic-stratified-benchmarks/padic-stratified-benchmarks.json",
"oracle, certificate, fallback, timing",
"speed-claim guard fields",
"not production speedup or portable GPU support evidence",
],
);
}
#[test]
fn final_readiness_entrypoint_matches_current_release_gates() {
let final_readiness = fs::read_to_string("docs/paper/final_submission_readiness.md")
.expect("final submission readiness should exist");
let normalized_final_readiness = collapse_whitespace(&final_readiness);
assert_contains_all(
"final readiness current release gates",
&normalized_final_readiness,
&[
"P242-synchronized entry point",
"P240 continuous manuscript draft",
"P241 readiness audit",
"P242 package view",
"P242 Current Submission Package Entry Point",
"P242 Current Submission Package Entry Point: the P240 continuous manuscript",
"single entry point for authors and reviewers",
"P240 front matter, contribution list, evaluation path, related-work boundary",
"P241 readiness audit: `docs/paper/readiness_audit.md`",
"Continuous manuscript draft follows C10 route",
"P240 front matter and conclusion claim discipline are visible",
"P241 readiness audit is linked",
"P243 keeps this final decision synchronized with the P240 continuous manuscript draft",
"P242 submission package entry point",
"certified valuation-sparse p-adic GEMM route",
"single reviewer-facing entry point is the default gate, signed audit-trace gate, schema gate, and feature-gated ROCm/HIP p-adic benchmark gate",
"venue-specific formatting",
"Feature-gated certified p-adic GEMM benchmark validation",
"ARTIFACT.md",
"docs/paper/release_checklist.md",
"docs/paper/release_bundle_manifest.md",
"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",
"cargo test --offline --features rocm-hip --test rocm_padic_stratified_benchmarks",
"cargo run --quiet --offline --features rocm-hip --example rocm_padic_stratified_benchmarks",
"\"artifact\":\"tokitai-padic-stratified-matmul-benchmark-report\"",
"\"certificate_coverage\":true",
"\"speed_claim_allowed\":false",
"rocm_hip_padic_stratified_matmul_pilot",
"The same default gate, signed audit trace gate, and feature-gated p-adic GEMM",
"docs/paper/final_validation_record.md",
"P246 final validation record",
"`todo.json` `next_success` condition",
],
);
for stale_current_claim in [
"P230-synchronized entry point",
"The current P230 package view is",
"P230 Current Submission Package Entry Point",
"P160 front matter, contribution list, and conclusion:",
"P161 readiness audit: `docs/paper/readiness_audit.md`",
"P160 front matter, contribution list, and conclusion claim discipline",
"P160 front matter claim discipline is visible",
"P161 readiness audit is linked",
"P162 synchronizes the final\nreadiness report with the current P156-P161 manuscript package",
"P163 adds a venue-facing submission checklist without changing the no-blocker verdict",
] {
assert!(
!final_readiness.contains(stale_current_claim),
"P242 final readiness should not keep stale entry-point text: {stale_current_claim}"
);
}
}
#[test]
fn final_validation_record_maps_todo_next_success_to_current_gates() {
let record = fs::read_to_string("docs/paper/final_validation_record.md")
.expect("final validation record should exist");
assert_contains_all(
"P246 final validation record",
&record,
&[
"P440 Final Validation Record",
"synchronized through P440",
"P270 Final Validation Record",
"synchronized through P270",
"P248-P269 functional hardening and",
"post-P264 machine-checked roadmap guards",
"explicit fenced status blocks",
"reusable library validators",
"expectation-driven status validation",
"duplicate-key fail-closed status parsing",
"functional hardening and",
"validation-maintenance roadmap P248-P270",
"structured roadmap guards",
"P246 Final Validation Record",
"P255 Final Validation Record",
"supersedes the P269, P268, P267, P266, P255, and P246-only",
"P248-P254 functional hardening",
"evidence: runtime-shape ROCm/HIP p-adic GEMM",
"public prefer-gpu dense integer add selection",
"optional Lean success transcripts",
"JSC target verification packet",
"synchronized through P246",
"`todo.json` `next_success` condition",
"Current validation conclusion",
"no active implementation",
"certified valuation-sparse p-adic GEMM",
"P246 Completion Evidence Matrix",
"Default gate remains green",
"Schema-guarded artifacts remain valid",
"Generated paper artifacts regenerate",
"bounded optional Lean behavior",
"Signed audit trace gate passes",
"Feature-gated ROCm/HIP p-adic GEMM gate passes",
"ROCm/HIP benchmark artifact fields remain claim-safe",
"Reviewer-facing reproduction path is synchronized",
"Target-package controls keep the same gate",
"Manuscript route remains C10-centered",
"Readiness and final decision stay synchronized",
"Venue controls preserve no-SCI-Q2-overclaim boundary",
"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",
"TOKITAI_AUDIT_TRACE_DIR",
"cargo run --quiet --offline --example audit_traces",
"\"admission_artifact_digest\":null",
"\"capability_fingerprint\":\"sha256:",
"\"adapter_capability_fingerprint\":\"sha256:",
"cargo test --offline --features rocm-hip --test rocm_padic_stratified_benchmarks",
"cargo run --quiet --offline --features rocm-hip --example rocm_padic_stratified_benchmarks",
"\"artifact\":\"tokitai-padic-stratified-matmul-benchmark-report\"",
"\"certificate_coverage\":true",
"\"speed_claim_allowed\":false",
"rocm_hip_padic_stratified_matmul_pilot",
"P246 Claim Discipline",
"repository-ready evidence for",
"Do not claim general GPU acceleration",
"production speedup",
"portable AMD GPU",
"verified HIP machine code",
"arbitrary precision p-adic fields",
"current SCI-Q2 indexing",
],
);
validate_status_block(&record, ¤t_validation_status_expectation())
.expect("final validation status block should validate against current expectation");
validate_validation_status_block(&record)
.expect("final validation convenience validator should use current expectation");
let final_readiness = fs::read_to_string("docs/paper/final_submission_readiness.md")
.expect("final readiness should exist");
assert_contains_all(
"final readiness P246 validation record link",
&final_readiness,
&[
"final validation record: `docs/paper/final_validation_record.md`",
"The P246 final validation record in `docs/paper/final_validation_record.md`",
],
);
let release_manifest = fs::read_to_string("docs/paper/release_bundle_manifest.md")
.expect("release bundle manifest should exist");
assert_contains_all(
"release bundle P246 validation record link",
&release_manifest,
&[
"docs/paper/final_validation_record.md",
"maps the final validation gates to",
"current certified p-adic GEMM claim route",
],
);
let todo = fs::read_to_string("todo.json").expect("todo.json should exist");
assert_contains_all(
"todo current final validation dependency",
&todo,
&[
"final validation records",
"schema inventory",
"P248-P275 are completed and preserved as validated functional hardening evidence",
"The roadmap is in functional-expansion state",
"Functional expansion succeeds when P248-P275 tests",
],
);
}
#[test]
fn target_package_templates_preserve_feature_gated_padic_gemm_gate() {
for path in [
"docs/paper/target_formatting_instantiation_checklist.md",
"docs/paper/target_submission_package_manifest_template.md",
"docs/paper/target_package_freeze_protocol.md",
"docs/paper/target_package_evidence_review_log_template.md",
"docs/paper/final_author_approval_packet_template.md",
"docs/paper/post_approval_submission_readiness_gate.md",
] {
let content = fs::read_to_string(path).unwrap_or_else(|err| {
panic!("target package template should exist and be readable: {path}: {err}")
});
assert_contains_all(
path,
&content,
&[
"Feature-gated certified p-adic GEMM benchmark validation",
"cargo test --offline --features rocm-hip --test rocm_padic_stratified_benchmarks",
"cargo run --quiet --offline --features rocm-hip --example rocm_padic_stratified_benchmarks",
"\"artifact\":\"tokitai-padic-stratified-matmul-benchmark-report\"",
"\"certificate_coverage\":true",
"\"speed_claim_allowed\":false",
"rocm_hip_padic_stratified_matmul_pilot",
],
);
}
let manifest = fs::read_to_string("docs/paper/target_submission_package_manifest_template.md")
.expect("target package manifest template should exist");
assert_contains_all(
"target package manifest generated artifact records",
&manifest,
&[
"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",
"Include checksum after freeze when ROCm/HIP benchmark evidence is included",
],
);
let freeze_protocol = fs::read_to_string("docs/paper/target_package_freeze_protocol.md")
.expect("target package freeze protocol should exist");
assert_contains_all(
"target package freeze generated artifact records",
&freeze_protocol,
&[
"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",
"Regenerate and checksum when ROCm/HIP benchmark evidence is included",
],
);
}