use std::fs;
use std::process::Command;
use serde::{Deserialize, Serialize};
use tokitai_operator::verify::proof_replay_artifact_digest;
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdePaperBenchmarkResults {
artifact: String,
version: u64,
workloads: Vec<SerdeWorkloadResult>,
measurements: Vec<SerdeMeasurementSummary>,
baseline_comparisons: Vec<SerdeBaselineComparison>,
evidence_matrix: Vec<SerdeApplicationEvidenceRow>,
ablations: Vec<SerdeAblationResult>,
claims: Vec<SerdeClaimTrace>,
trace_architecture: Vec<SerdeTraceArchitectureEdge>,
witness_metadata: Vec<SerdeWitnessMetadata>,
}
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeWorkloadResult {
name: String,
reference_duration_ns: u64,
optimized_duration_ns: u64,
proof_trace_validation_ns: u64,
plan_steps: u64,
proof_objects: u64,
checked_proofs: u64,
domain_metric: String,
}
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeMeasurementSummary {
name: String,
measurement_kind: String,
runs: u64,
min_ns: u64,
median_ns: u64,
max_ns: u64,
notes: String,
}
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeBaselineComparison {
family: String,
workload: String,
scale_point: String,
baseline_kind: String,
baseline_ns: u64,
candidate_kind: String,
candidate_ns: u64,
proof_overhead_ns: u64,
ratio_milli: u64,
interpretation: String,
}
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeApplicationEvidenceRow {
axis: String,
workload: String,
backend_id: String,
candidate_backend: String,
capability_fingerprint: String,
p_adic_constraint_fingerprint: String,
sheaf_constraint_fingerprint: String,
correctness_evidence: String,
speed_evidence: String,
fallback_rate: String,
conformance_status: String,
precision_or_locality: String,
proof_evidence: String,
}
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeAblationResult {
tamper_class: String,
no_proof_detected: bool,
digest_only_detected: bool,
count_only_detected: bool,
per_theorem_index_detected: bool,
}
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeClaimTrace {
claim_id: String,
paper_claim: String,
code_artifacts: String,
tests: String,
experiment_artifacts: String,
}
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeTraceArchitectureEdge {
source: String,
target: String,
binding: String,
}
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeWitnessMetadata {
artifact: String,
selected_witness_family: String,
selected_nonstandard_witness_family: String,
selected_shape_witness_count: u64,
selected_padic_witness_count: u64,
verification_command: String,
}
fn schema_required_fields(schema: &str, artifact: &str) -> Vec<String> {
let compact_schema = compact_json(schema);
let artifact_marker = format!("\"artifact\":\"{artifact}\"");
let artifact_start = compact_schema
.find(&artifact_marker)
.unwrap_or_else(|| panic!("schema should include artifact {artifact}"));
let required_start = compact_schema[artifact_start..]
.find("\"required_fields\":[")
.map(|offset| artifact_start + offset + "\"required_fields\":[".len())
.unwrap_or_else(|| panic!("schema artifact {artifact} should include required_fields"));
let required_end = compact_schema[required_start..]
.find(']')
.map(|offset| required_start + offset)
.unwrap();
compact_schema[required_start..required_end]
.split(',')
.map(|field| field.trim().trim_matches('"').to_string())
.filter(|field| !field.is_empty())
.collect()
}
fn schema_csv_header(schema: &str, filename: &str) -> String {
let compact_schema = compact_json(schema);
let filename_marker = format!("\"filename\":\"{filename}\"");
let filename_start = compact_schema
.find(&filename_marker)
.unwrap_or_else(|| panic!("CSV schema should include {filename}"));
let header_start = compact_schema[filename_start..]
.find("\"header\":\"")
.map(|offset| filename_start + offset + "\"header\":\"".len())
.unwrap_or_else(|| panic!("CSV schema entry {filename} should include header"));
let header_end = compact_schema[header_start..]
.find('"')
.map(|offset| header_start + offset)
.unwrap();
compact_schema[header_start..header_end].to_string()
}
fn compact_json(json: &str) -> String {
json.chars()
.filter(|character| !character.is_whitespace())
.collect()
}
fn run_paper_benchmarks_example(test_name: &str) -> (std::path::PathBuf, String) {
let output_dir = std::env::temp_dir().join(format!(
"tokitai-paper-results-{test_name}-{}",
std::process::id()
));
let _ = fs::remove_dir_all(&output_dir);
let output = Command::new(env!("CARGO"))
.args(["run", "--quiet", "--example", "paper_benchmarks", "--"])
.arg(&output_dir)
.output()
.expect("paper_benchmarks example should run");
assert!(
output.status.success(),
"paper_benchmarks failed: {}",
String::from_utf8_lossy(&output.stderr)
);
let json = fs::read_to_string(output_dir.join("paper-results.json")).unwrap();
(output_dir, json)
}
fn canonical_paper_results_json(results: &SerdePaperBenchmarkResults) -> String {
format!(
"{{\"artifact\":\"{}\",\"version\":{},\"workloads\":[{}],\"measurements\":[{}],\"baseline_comparisons\":[{}],\"evidence_matrix\":[{}],\"ablations\":[{}],\"claims\":[{}],\"trace_architecture\":[{}],\"witness_metadata\":[{}]}}",
results.artifact,
results.version,
results
.workloads
.iter()
.map(canonical_workload_json)
.collect::<Vec<_>>()
.join(","),
results
.measurements
.iter()
.map(canonical_measurement_json)
.collect::<Vec<_>>()
.join(","),
results
.baseline_comparisons
.iter()
.map(canonical_baseline_comparison_json)
.collect::<Vec<_>>()
.join(","),
results
.evidence_matrix
.iter()
.map(canonical_application_evidence_json)
.collect::<Vec<_>>()
.join(","),
results
.ablations
.iter()
.map(canonical_ablation_json)
.collect::<Vec<_>>()
.join(","),
results
.claims
.iter()
.map(canonical_claim_json)
.collect::<Vec<_>>()
.join(","),
results
.trace_architecture
.iter()
.map(canonical_trace_architecture_json)
.collect::<Vec<_>>()
.join(","),
results
.witness_metadata
.iter()
.map(canonical_witness_metadata_json)
.collect::<Vec<_>>()
.join(",")
)
}
fn canonical_application_evidence_json(result: &SerdeApplicationEvidenceRow) -> String {
format!(
"{{\"axis\":\"{}\",\"workload\":\"{}\",\"backend_id\":\"{}\",\"candidate_backend\":\"{}\",\"capability_fingerprint\":\"{}\",\"p_adic_constraint_fingerprint\":\"{}\",\"sheaf_constraint_fingerprint\":\"{}\",\"correctness_evidence\":\"{}\",\"speed_evidence\":\"{}\",\"fallback_rate\":\"{}\",\"conformance_status\":\"{}\",\"precision_or_locality\":\"{}\",\"proof_evidence\":\"{}\"}}",
result.axis,
result.workload,
result.backend_id,
result.candidate_backend,
result.capability_fingerprint,
result.p_adic_constraint_fingerprint,
result.sheaf_constraint_fingerprint,
result.correctness_evidence,
result.speed_evidence,
result.fallback_rate,
result.conformance_status,
result.precision_or_locality,
result.proof_evidence
)
}
fn canonical_workload_json(result: &SerdeWorkloadResult) -> String {
format!(
"{{\"name\":\"{}\",\"reference_duration_ns\":{},\"optimized_duration_ns\":{},\"proof_trace_validation_ns\":{},\"plan_steps\":{},\"proof_objects\":{},\"checked_proofs\":{},\"domain_metric\":\"{}\"}}",
result.name,
result.reference_duration_ns,
result.optimized_duration_ns,
result.proof_trace_validation_ns,
result.plan_steps,
result.proof_objects,
result.checked_proofs,
result.domain_metric
)
}
fn canonical_measurement_json(result: &SerdeMeasurementSummary) -> String {
format!(
"{{\"name\":\"{}\",\"measurement_kind\":\"{}\",\"runs\":{},\"min_ns\":{},\"median_ns\":{},\"max_ns\":{},\"notes\":\"{}\"}}",
result.name,
result.measurement_kind,
result.runs,
result.min_ns,
result.median_ns,
result.max_ns,
result.notes
)
}
fn canonical_baseline_comparison_json(result: &SerdeBaselineComparison) -> String {
format!(
"{{\"family\":\"{}\",\"workload\":\"{}\",\"scale_point\":\"{}\",\"baseline_kind\":\"{}\",\"baseline_ns\":{},\"candidate_kind\":\"{}\",\"candidate_ns\":{},\"proof_overhead_ns\":{},\"ratio_milli\":{},\"interpretation\":\"{}\"}}",
result.family,
result.workload,
result.scale_point,
result.baseline_kind,
result.baseline_ns,
result.candidate_kind,
result.candidate_ns,
result.proof_overhead_ns,
result.ratio_milli,
result.interpretation
)
}
fn canonical_ablation_json(result: &SerdeAblationResult) -> String {
format!(
"{{\"tamper_class\":\"{}\",\"no_proof_detected\":{},\"digest_only_detected\":{},\"count_only_detected\":{},\"per_theorem_index_detected\":{}}}",
result.tamper_class,
result.no_proof_detected,
result.digest_only_detected,
result.count_only_detected,
result.per_theorem_index_detected
)
}
fn canonical_claim_json(result: &SerdeClaimTrace) -> String {
format!(
"{{\"claim_id\":\"{}\",\"paper_claim\":\"{}\",\"code_artifacts\":\"{}\",\"tests\":\"{}\",\"experiment_artifacts\":\"{}\"}}",
result.claim_id,
result.paper_claim,
result.code_artifacts,
result.tests,
result.experiment_artifacts
)
}
fn canonical_trace_architecture_json(result: &SerdeTraceArchitectureEdge) -> String {
format!(
"{{\"source\":\"{}\",\"target\":\"{}\",\"binding\":\"{}\"}}",
result.source, result.target, result.binding
)
}
fn canonical_witness_metadata_json(result: &SerdeWitnessMetadata) -> String {
format!(
"{{\"artifact\":\"{}\",\"selected_witness_family\":\"{}\",\"selected_nonstandard_witness_family\":\"{}\",\"selected_shape_witness_count\":{},\"selected_padic_witness_count\":{},\"verification_command\":\"{}\"}}",
result.artifact,
result.selected_witness_family,
result.selected_nonstandard_witness_family,
result.selected_shape_witness_count,
result.selected_padic_witness_count,
result.verification_command
)
}
#[test]
fn paper_benchmarks_example_generates_reproducible_tables() {
let (output_dir, json) = run_paper_benchmarks_example("reproducible");
let workloads_csv = fs::read_to_string(output_dir.join("paper-results.csv")).unwrap();
let measurement_csv = fs::read_to_string(output_dir.join("measurement-summary.csv")).unwrap();
let baseline_csv =
fs::read_to_string(output_dir.join("baseline-scale-comparison.csv")).unwrap();
let evidence_csv =
fs::read_to_string(output_dir.join("application-evidence-matrix.csv")).unwrap();
let tamper_csv = fs::read_to_string(output_dir.join("tamper-matrix.csv")).unwrap();
let claim_csv = fs::read_to_string(output_dir.join("claim-to-test-matrix.csv")).unwrap();
let trace_architecture_csv =
fs::read_to_string(output_dir.join("trace-architecture.csv")).unwrap();
let support_matrix_json =
fs::read_to_string(output_dir.join("theory-support-matrix.json")).unwrap();
let support_matrix_md =
fs::read_to_string(output_dir.join("theory-support-matrix.md")).unwrap();
let release_gate_json =
fs::read_to_string(output_dir.join("theory-release-gate.json")).unwrap();
let release_gate_md = fs::read_to_string(output_dir.join("theory-release-gate.md")).unwrap();
let artifact_schema = fs::read_to_string("docs/schemas/tokitai-artifacts-v1.schema.json")
.expect("artifact schema should exist");
let csv_schema = fs::read_to_string("docs/schemas/tokitai-paper-csv-v1.schema.json")
.expect("CSV schema should exist");
assert!(json.contains("\"artifact\":\"tokitai-paper-benchmark-results\""));
assert!(json.contains("\"version\":1"));
for field in schema_required_fields(&artifact_schema, "tokitai-paper-benchmark-results") {
assert!(
json.contains(&format!("\"{field}\":")),
"paper results JSON should contain schema-required field {field}: {json}"
);
}
for field in [
"workloads",
"measurements",
"baseline_comparisons",
"evidence_matrix",
"ablations",
"claims",
"trace_architecture",
"witness_metadata",
"reference_duration_ns",
"optimized_duration_ns",
"proof_trace_validation_ns",
"plan_steps",
"proof_objects",
"checked_proofs",
"domain_metric",
"measurement_kind",
"runs",
"min_ns",
"median_ns",
"max_ns",
"notes",
"family",
"workload",
"scale_point",
"baseline_kind",
"baseline_ns",
"candidate_kind",
"candidate_ns",
"proof_overhead_ns",
"ratio_milli",
"interpretation",
"axis",
"backend_id",
"candidate_backend",
"capability_fingerprint",
"p_adic_constraint_fingerprint",
"sheaf_constraint_fingerprint",
"correctness_evidence",
"speed_evidence",
"fallback_rate",
"conformance_status",
"precision_or_locality",
"proof_evidence",
"tamper_class",
"digest_only_detected",
"count_only_detected",
"per_theorem_index_detected",
"claim_id",
"code_artifacts",
"experiment_artifacts",
"source",
"target",
"binding",
"selected_witness_family",
"selected_nonstandard_witness_family",
"selected_shape_witness_count",
"selected_padic_witness_count",
"verification_command",
] {
assert!(
json.contains(&format!("\"{field}\":")),
"paper results JSON should contain stable field {field}: {json}"
);
}
assert!(json.contains("\"name\":\"ordinary_tensor_add\""));
assert!(json.contains("\"name\":\"ordinary_tensor_add_large\""));
assert!(json.contains("\"name\":\"padic_matmul_valuation_skip\""));
assert!(json.contains("\"name\":\"padic_matmul_valuation_skip_large\""));
assert!(json.contains("\"name\":\"sheaf_cover_glue\""));
assert!(json.contains("\"name\":\"sheaf_cover_glue_large\""));
assert!(json.contains("\"name\":\"proof_trace_validation_scale\""));
assert!(json.contains("\"measurement_kind\":\"deterministic_proxy\""));
assert!(json.contains("\"measurement_kind\":\"repeated_wall_clock\""));
assert!(json.contains("\"baseline_comparisons\":["));
assert!(json.contains("\"evidence_matrix\":["));
assert!(json.contains("\"family\":\"ordinary_tensor\""));
assert!(json.contains("\"family\":\"padic_valuation\""));
assert!(json.contains("\"family\":\"sheaf_glue\""));
assert!(json.contains("\"family\":\"proof_trace\""));
assert!(json.contains("\"family\":\"selected_witness_metadata\""));
assert!(json.contains("\"scale_point\":\"shape=4x4x4\""));
assert!(json.contains("\"scale_point\":\"cover_opens=3\""));
assert!(json.contains("\"scale_point\":\"theorem_count=3;artifact_count=11\""));
assert!(json.contains("\"scale_point\":\"families=2;metadata_fields=5;witnesses=6\""));
assert!(json.contains("\"candidate_kind\":\"valuation_skip_plan\""));
assert!(json.contains("\"workload\":\"native_trace_validation_scale\""));
assert!(json.contains("\"workload\":\"selected_lean_witness_metadata_scale\""));
assert!(json.contains("\"tamper_class\":\"checker_index_adapter\""));
assert!(json.contains("\"per_theorem_index_detected\":true"));
assert!(json.contains("\"claims\":["));
assert!(json.contains("\"paper_claim\":\"trace_bound_semantic_evidence\""));
assert!(json.contains("\"trace_architecture\":["));
assert!(json.contains("\"witness_metadata\":["));
assert!(json.contains("\"selected_witness_family\":\"shape_equality_dimension_witness_v1\""));
assert!(
json.contains(
"\"selected_nonstandard_witness_family\":\"padic_precision_cutoff_witness_v1\""
)
);
assert!(json.contains("\"selected_shape_witness_count\":1"));
assert!(json.contains("\"selected_padic_witness_count\":1"));
assert!(json.contains("\"binding\":\"plan_fingerprint\""));
assert!(json.contains("\"axis\":\"cpu_reference_correctness\""));
assert!(json.contains("\"axis\":\"padic_precision_valuation\""));
assert!(json.contains("\"axis\":\"sheaf_local_to_global\""));
assert!(json.contains("\"axis\":\"gpu_scaffold_fallback_conformance\""));
assert!(json.contains("\"candidate_backend\":\"gpu_scaffold\""));
assert!(json.contains("\"fallback_rate\":\"6/6\""));
assert!(json.contains("\"conformance_status\":\"fallback_conformance_passed\""));
assert!(json.contains("\"precision_or_locality\":\"Q_5_precision=3;valuation_cutoff=3\""));
assert!(json.contains("\"correctness_evidence\":\"precision_bounded_equality_digits=3\""));
assert!(json.contains("\"speed_evidence\":\"no_speed_claim_scaffold_only\""));
assert!(json.contains("\"proof_evidence\":\"math_bound_trace_links_conformance_result\""));
assert!(support_matrix_json.contains("\"artifact\":\"tokitai-theory-support-matrix\""));
assert!(support_matrix_json.contains("\"rows\":["));
assert!(support_matrix_json.contains("\"support_status\":\"supported\""));
assert!(support_matrix_json.contains("\"support_status\":\"fallback_only\""));
for field in [
"domain",
"operator",
"theory_constraints",
"theorem_packages",
"backend",
"backend_capability",
"lowering_rule_id",
"support_status",
"fallback_mode",
"public_api",
"tests",
"non_claims",
] {
assert!(
support_matrix_json.contains(&format!("\"{field}\":")),
"support matrix JSON should contain stable row field {field}: {support_matrix_json}"
);
}
assert!(support_matrix_json.contains("tokitai_padic_valuation_skip_sound_mod_pk"));
assert!(support_matrix_json.contains("rocm_hip_padic_stratified_matmul_pilot"));
assert!(support_matrix_json.contains("per_output_certificate_required"));
assert!(support_matrix_json.contains("not production speedup evidence"));
assert!(support_matrix_json.contains("Tokitai::plan_padic_sum_products"));
assert!(support_matrix_md.contains("# Theory-Aware Support Matrix"));
assert!(support_matrix_md.contains("gpu_dense_i64_pilot"));
assert!(release_gate_json.contains("\"artifact\":\"tokitai-theory-engineering-release-gate\""));
assert!(release_gate_json.contains("\"passed\":true"));
assert!(release_gate_json.contains("\"name\":\"optional Lean timeout policy\""));
assert!(release_gate_json.contains(
"p-adic valuation theorem checker: bounded optional Lean timeout policy and success transcript capture present"
));
assert!(release_gate_json.contains(
"finite-sheaf gluing theorem checker: bounded optional Lean timeout policy and success transcript capture present"
));
assert!(release_gate_json.contains(
"TOKITAI_REQUIRE_LEAN=1 TOKITAI_LEAN_TIMEOUT_SECONDS=20 sh scripts/check_padic_valuation_skip_theorem.sh"
));
assert!(release_gate_json.contains(
"TOKITAI_REQUIRE_LEAN=1 TOKITAI_LEAN_TIMEOUT_SECONDS=20 sh scripts/check_finite_sheaf_gluing_theorem.sh"
));
assert!(release_gate_json.contains("default timeout evidence is non-blocking"));
assert!(release_gate_json.contains("success transcripts are captured when Lean runs"));
assert!(release_gate_md.contains("# Theory-Engineering Release Gate"));
assert!(release_gate_md.contains("cargo test --offline"));
assert!(release_gate_md.contains("optional Lean timeout policy"));
assert!(release_gate_md.contains("TOKITAI_LEAN_TIMEOUT_SECONDS"));
assert!(
workloads_csv.starts_with(
"name,reference_duration_ns,optimized_duration_ns,proof_trace_validation_ns"
)
);
assert!(workloads_csv.starts_with(&format!(
"{}\n",
schema_csv_header(&csv_schema, "paper-results.csv")
)));
assert!(workloads_csv.contains("ordinary_tensor_add"));
assert!(workloads_csv.contains("ordinary_tensor_add_large"));
assert!(workloads_csv.contains("padic_matmul_valuation_skip"));
assert!(workloads_csv.contains("skipped_terms=4;evaluated_terms=8"));
assert!(workloads_csv.contains("padic_matmul_valuation_skip_large"));
assert!(workloads_csv.contains("shape=4x4x4"));
assert!(workloads_csv.contains("sheaf_cover_glue"));
assert!(workloads_csv.contains("sheaf_cover_glue_large"));
assert!(workloads_csv.contains("cover_opens=3"));
assert!(measurement_csv.starts_with(&format!(
"{}\n",
schema_csv_header(&csv_schema, "measurement-summary.csv")
)));
assert!(measurement_csv.contains("ordinary_tensor_add,deterministic_proxy,3"));
assert!(measurement_csv.contains("ordinary_tensor_add_large,deterministic_proxy,3"));
assert!(measurement_csv.contains("padic_matmul_valuation_skip_large,deterministic_proxy,3"));
assert!(measurement_csv.contains("sheaf_cover_glue_large,deterministic_proxy,3"));
assert!(measurement_csv.contains("proof_trace_validation_scale,deterministic_proxy,3"));
assert!(measurement_csv.contains("ordinary_tensor_add_validation,repeated_wall_clock,5"));
assert!(measurement_csv.contains("selected_witness_metadata_overhead,deterministic_proxy,3"));
assert!(measurement_csv.contains(
"deterministic proxy for selected Lean witness metadata generation and validation overhead"
));
assert!(baseline_csv.starts_with(&format!(
"{}\n",
schema_csv_header(&csv_schema, "baseline-scale-comparison.csv")
)));
assert!(
baseline_csv
.contains("ordinary_tensor,ordinary_tensor_add_large,elements=64,cpu_reference_plan")
);
assert!(baseline_csv.contains(
"padic_valuation,padic_matmul_valuation_skip_large,shape=4x4x4,dense_padic_matmul"
));
assert!(baseline_csv.contains("valuation_skip_plan"));
assert!(
baseline_csv
.contains("sheaf_glue,sheaf_cover_glue,cover_opens=2,finite_cover_compatibility")
);
assert!(
baseline_csv
.contains("sheaf_glue,sheaf_cover_glue_large,cover_opens=3,finite_cover_compatibility")
);
assert!(baseline_csv.contains(
"proof_trace,native_trace_validation,theorem_count=1;artifact_count=8,digest_only_manifest_check"
));
assert!(baseline_csv.contains(
"proof_trace,native_trace_validation_scale,theorem_count=3;artifact_count=11,digest_only_manifest_check"
));
assert!(baseline_csv.contains(
"selected_witness_metadata,selected_lean_witness_metadata,families=2;metadata_fields=5;witnesses=2,no_selected_witness_metadata"
));
assert!(baseline_csv.contains(
"selected_witness_metadata,selected_lean_witness_metadata_scale,families=2;metadata_fields=5;witnesses=6,no_selected_witness_metadata"
));
assert!(baseline_csv.contains(
"scaled theorem-result and artifact-count validation cost for reviewer-facing trace evidence"
));
assert!(baseline_csv.contains(
"scaled selected witness metadata cost for multiple ordinary and p-adic theorem witnesses"
));
assert!(baseline_csv.contains("ratio_milli"));
assert!(evidence_csv.starts_with(&format!(
"{}\n",
schema_csv_header(&csv_schema, "application-evidence-matrix.csv")
)));
assert!(
evidence_csv
.contains("cpu_reference_correctness,ordinary_tensor_add,cpu_scalar,cpu_scalar")
);
assert!(
evidence_csv.contains(
"padic_precision_valuation,padic_matmul_valuation_skip,cpu_scalar,cpu_scalar"
)
);
assert!(evidence_csv.contains("sheaf_local_to_global,sheaf_cover_glue,cpu_scalar,cpu_scalar"));
assert!(evidence_csv.contains(
"gpu_scaffold_fallback_conformance,cpu_oracle_fixture_suite,gpu_scaffold,gpu_scaffold"
));
assert!(evidence_csv.contains("fallback_conformance_passed"));
assert!(evidence_csv.contains("fallback_rate"));
assert!(evidence_csv.contains("Q_5_precision=3;valuation_cutoff=3"));
assert!(evidence_csv.contains("finite_site_cover_opens=2"));
assert!(evidence_csv.contains("mixed_dense_padic_sheaf_categorical_fixtures"));
assert!(evidence_csv.contains("deterministic_proxy_reference_ns="));
assert!(tamper_csv.starts_with(
"tamper_class,no_proof_detected,digest_only_detected,count_only_detected,per_theorem_index_detected"
));
assert!(tamper_csv.starts_with(&format!(
"{}\n",
schema_csv_header(&csv_schema, "tamper-matrix.csv")
)));
assert!(tamper_csv.contains("manifest_digest,false,true,true,true"));
assert!(tamper_csv.contains("native_count,false,false,true,true"));
assert!(tamper_csv.contains("theorem_result_fingerprint,false,false,false,true"));
assert!(tamper_csv.contains("checker_index_adapter,false,false,false,true"));
assert!(tamper_csv.contains("checker_index_admission,false,false,false,true"));
assert!(tamper_csv.contains("witness_metadata,false,false,false,true"));
assert!(
claim_csv.starts_with("claim_id,paper_claim,code_artifacts,tests,experiment_artifacts")
);
assert!(claim_csv.starts_with(&format!(
"{}\n",
schema_csv_header(&csv_schema, "claim-to-test-matrix.csv")
)));
assert!(claim_csv.contains("C1,trace_bound_semantic_evidence"));
assert!(claim_csv.contains("C2,nonstandard_domain_planning"));
assert!(claim_csv.contains("C3,native_checker_admission_binding"));
assert!(claim_csv.contains("C4,authenticity_vs_semantic_failures"));
assert!(claim_csv.contains("C5,canonical_import_normalization"));
assert!(claim_csv.contains("C6,selected_native_shape_witness"));
assert!(claim_csv.contains("C7,selected_nonstandard_padic_witness"));
assert!(claim_csv.contains("C8,reviewer_visible_witness_metadata"));
assert!(claim_csv.contains("C9,benchmark_application_evidence_matrix"));
assert!(claim_csv.contains("C10,certified_valuation_sparse_padic_gemm"));
assert!(claim_csv.contains("docs/paper/serialization_strategy.md;src/verify/mod.rs"));
assert!(claim_csv.contains("docs/paper/proof_assistant_scope.md;src/verify/mod.rs"));
assert!(claim_csv.contains("tests/json_parser_regression.rs;tests/paper_artifacts.rs"));
assert!(claim_csv.contains(
"tests/operator_registry.rs;tests/audit_traces_example.rs;tests/paper_artifacts.rs"
));
assert!(
claim_csv
.contains("tests/padic.rs;tests/paper_artifacts.rs;tests/paper_benchmarks_example.rs")
);
assert!(
claim_csv
.contains("docs/paper/schema_inventory.md;ARTIFACT.md;examples/paper_benchmarks.rs")
);
assert!(claim_csv.contains(
"tests/schema_guards.rs;tests/paper_artifacts.rs;tests/paper_benchmarks_example.rs"
));
assert!(
claim_csv
.contains("examples/paper_benchmarks.rs;docs/benchmark_application_evidence_matrix.md")
);
assert!(claim_csv.contains(
"target/paper-results/application-evidence-matrix.csv;target/paper-results/paper-results.json"
));
assert!(claim_csv.contains("tests/padic.rs;tests/sheaf.rs;tests/generic_backend.rs"));
assert!(trace_architecture_csv.starts_with("source,target,binding"));
assert!(trace_architecture_csv.starts_with(&format!(
"{}\n",
schema_csv_header(&csv_schema, "trace-architecture.csv")
)));
assert!(trace_architecture_csv.contains("execution_plan,proof_replay_report,plan_fingerprint"));
assert!(
trace_architecture_csv.contains("checker_output,native_admission,checker_output_digest")
);
assert!(
trace_architecture_csv.contains("trace_manifest,all_artifacts,sha256_digest_and_signature")
);
assert!(trace_architecture_csv.contains(
"ordinary_json_import,canonical_json_renderer,field_order_independent_import_to_digest_stable_bytes"
));
assert!(trace_architecture_csv.contains(
"shape_equality_replay,selected_lean_shape_witness,output_shape_evidence_to_rfl_equality"
));
assert!(trace_architecture_csv.contains(
"selected_lean_shape_witness,lean_checkable_artifact,witness_theorem_digest_bound_by_artifact"
));
assert!(trace_architecture_csv.contains(
"padic_valuation_replay,selected_lean_padic_witness,precision_cutoff_evidence_to_rfl_equality"
));
assert!(trace_architecture_csv.contains(
"selected_lean_padic_witness,lean_checkable_artifact,nonstandard_witness_digest_bound_by_artifact"
));
let _ = fs::remove_dir_all(&output_dir);
}
#[test]
fn serde_paper_benchmark_fixture_preserves_canonical_bytes_and_digest() {
let (output_dir, json) = run_paper_benchmarks_example("serde-equivalence");
let serde_results: SerdePaperBenchmarkResults =
serde_json::from_str(&json).expect("paper-results.json should parse through serde_json");
assert_eq!(serde_results.artifact, "tokitai-paper-benchmark-results");
assert_eq!(serde_results.version, 1);
assert!(!serde_results.workloads.is_empty());
assert!(!serde_results.measurements.is_empty());
assert!(!serde_results.baseline_comparisons.is_empty());
assert!(!serde_results.evidence_matrix.is_empty());
assert!(!serde_results.ablations.is_empty());
assert!(!serde_results.claims.is_empty());
assert!(!serde_results.trace_architecture.is_empty());
assert!(!serde_results.witness_metadata.is_empty());
let serde_default_json = serde_json::to_string(&serde_results)
.expect("serde-derived paper benchmark model should serialize");
assert_eq!(
serde_default_json, json,
"serde default output currently matches this fixture, but it is still not the declared digest source"
);
let value_json = serde_json::to_string(
&serde_json::from_str::<serde_json::Value>(&json)
.expect("paper-results.json should parse as generic serde_json value"),
)
.expect("generic serde_json value should serialize");
assert_ne!(
value_json, json,
"generic serde_json Value output is an interchange representation, not Tokitai canonical bytes"
);
assert_ne!(
proof_replay_artifact_digest(&value_json),
proof_replay_artifact_digest(&json),
"generic serde_json output must not be accepted as the canonical digest source"
);
let canonical_json = canonical_paper_results_json(&serde_results);
assert_eq!(
canonical_json, json,
"serde paper benchmark model must round-trip through the explicit canonical renderer without changing version-1 bytes"
);
assert_eq!(
proof_replay_artifact_digest(&canonical_json),
proof_replay_artifact_digest(&json),
"serde paper benchmark fixture must preserve proof_replay_artifact_digest"
);
assert_eq!(
proof_replay_artifact_digest(&canonical_json),
proof_replay_artifact_digest(&serde_default_json),
"digest equality is accepted only because serde output matches explicit canonical bytes for this fixture"
);
let reparsed: SerdePaperBenchmarkResults = serde_json::from_str(&canonical_json)
.expect("canonical paper benchmark JSON should parse through serde_json");
assert_eq!(reparsed.artifact, "tokitai-paper-benchmark-results");
assert_eq!(reparsed.version, 1);
assert_eq!(reparsed.workloads.len(), serde_results.workloads.len());
assert_eq!(
reparsed.measurements.len(),
serde_results.measurements.len()
);
assert_eq!(
reparsed.baseline_comparisons.len(),
serde_results.baseline_comparisons.len()
);
assert_eq!(
reparsed.evidence_matrix.len(),
serde_results.evidence_matrix.len()
);
assert_eq!(reparsed.ablations.len(), serde_results.ablations.len());
assert_eq!(reparsed.claims.len(), serde_results.claims.len());
assert_eq!(
reparsed.trace_architecture.len(),
serde_results.trace_architecture.len()
);
assert_eq!(
reparsed.witness_metadata.len(),
serde_results.witness_metadata.len()
);
let artifact_schema = fs::read_to_string("docs/schemas/tokitai-artifacts-v1.schema.json")
.expect("artifact schema should exist");
for field in schema_required_fields(&artifact_schema, "tokitai-paper-benchmark-results") {
assert!(
canonical_json.contains(&format!("\"{field}\":")),
"serde canonical renderer fixture should preserve schema-required field {field}"
);
}
let _ = fs::remove_dir_all(&output_dir);
}