use serde::{Deserialize, Serialize};
use tokitai_operator::verify::{
CheckerResultEntry, CheckerResultIndex, ProofAssistantCheckerOutput, ProofAssistantDialect,
ProofAssistantNativeAdmission, ProofCertificate, ProofCertificateEntry, ProofReplayEntry,
ProofReplayReport, ProofReplayTraceArtifact, ProofReplayTraceBenchmarkRecord,
ProofReplayTraceBenchmarkSet, ProofReplayTraceTuning, checker_result_index_json,
parse_checker_result_index_json, parse_proof_assistant_adapter_registry_json,
parse_proof_assistant_checker_output_json, parse_proof_assistant_checker_transcript_json,
parse_proof_assistant_native_admission_json, parse_proof_replay_report_json,
parse_proof_replay_trace_benchmark_json, parse_proof_replay_trace_manifest_json,
parse_proof_replay_trace_tuning_json, proof_assistant_adapter_capability_fingerprint,
proof_assistant_adapter_registry_artifact_for_capabilities,
proof_assistant_adapter_registry_json_for_capabilities, proof_assistant_checker_output,
proof_assistant_checker_output_json, proof_assistant_checker_transcript,
proof_assistant_checker_transcript_json, proof_assistant_native_admission_json,
proof_assistant_replay_skeleton, proof_assistant_replay_skeleton_artifact,
proof_assistant_replay_summary_with_adapter_capability,
proof_assistant_replay_summary_with_adapter_registry,
proof_assistant_skeleton_adapter_capability, proof_replay_artifact_bundle,
proof_replay_artifact_digest, proof_replay_json_report, proof_replay_trace_benchmark_json,
proof_replay_trace_manifest, proof_replay_trace_manifest_json, proof_replay_trace_tuning_json,
sign_proof_replay_trace_manifest, verify_proof_replay_trace_manifest_signature,
};
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeTraceTuning {
artifact: String,
version: u32,
backend: String,
selected_strategy: String,
benchmark_count: usize,
enable_pointwise_fusion: bool,
enable_padic_matmul_valuation_skip: bool,
}
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeTraceBenchmarkSet {
artifact: String,
version: u32,
plan_fingerprint: String,
backend: String,
selected_strategy: String,
records: Vec<SerdeTraceBenchmarkRecord>,
}
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeTraceBenchmarkRecord {
plan_fingerprint: String,
backend: String,
strategy: String,
input_description: String,
duration_ns: u64,
}
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeProofReplayReport {
artifact: String,
version: u32,
plan_fingerprint: Option<String>,
checked_proofs: usize,
replayed_proofs: Vec<SerdeProofReplayEntry>,
warnings: Vec<String>,
}
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeProofReplayEntry {
theorem_id: String,
original_id: String,
kind: String,
status: String,
replayed: bool,
replay_rule: String,
}
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeCheckerTranscript {
artifact: String,
version: u32,
plan_fingerprint: String,
checker_command: String,
artifact_filename: String,
artifact_digest: String,
exit_status: i32,
stdout_digest: String,
stderr_digest: String,
result_status: String,
}
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeCheckerOutput {
artifact: String,
version: u32,
plan_fingerprint: String,
artifact_filename: String,
artifact_digest: String,
transcript_digest: String,
adapter_backend: String,
checker_version: String,
checked_theorem_count: usize,
result_status: String,
}
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeNativeAdmission {
artifact: String,
version: u32,
plan_fingerprint: Option<String>,
adapter_backend: String,
checker_version: String,
checked_theorem_count: usize,
result_status: String,
theorem_result_fingerprints: Vec<String>,
admission_claim: String,
evidence_digest: String,
}
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeCheckerResultIndex {
artifact: String,
version: u32,
plan_fingerprint: String,
entry_count: usize,
entries: Vec<SerdeCheckerResultEntry>,
}
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeCheckerResultEntry {
theorem_id: String,
theorem_result_fingerprint: String,
adapter_capability_fingerprint: String,
admission_artifact_digest: String,
plan_fingerprint: String,
}
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeAdapterRegistry {
artifact: String,
version: u32,
plan_fingerprint: Option<String>,
capabilities: Vec<SerdeAdapterCapability>,
}
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeAdapterCapability {
adapter_backend: String,
checker_version: String,
proof_status: String,
native_checked: bool,
admission_artifact_digest: Option<String>,
capability_fingerprint: String,
}
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeTraceManifest {
artifact: String,
version: u32,
trace_name: String,
plan_fingerprint: Option<String>,
artifacts: Vec<SerdeTraceArtifact>,
proof_assistant: Option<SerdeProofAssistantSummary>,
tuning: Option<SerdeManifestTuning>,
signature: Option<SerdeTraceSignature>,
}
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeTraceArtifact {
filename: String,
artifact: String,
version: u32,
format: String,
digest: String,
}
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeProofAssistantSummary {
dialect: String,
plan_fingerprint: Option<String>,
filename: String,
adapter_registry_filename: String,
adapter_registry_digest: String,
theorem_count: usize,
theorems: Vec<SerdeProofAssistantTheoremSummary>,
}
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeProofAssistantTheoremSummary {
theorem_id: String,
original_id: String,
kind: String,
status: String,
replay_rule: String,
obligations: Vec<String>,
evidence: Vec<String>,
obligation_count: usize,
evidence_count: usize,
statement_fingerprint: String,
adapter_backend: String,
checker_version: String,
proof_status: String,
adapter_capability_fingerprint: String,
}
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeManifestTuning {
backend: String,
selected_strategy: String,
benchmark_count: usize,
enable_pointwise_fusion: bool,
enable_padic_matmul_valuation_skip: bool,
}
#[derive(Debug, Clone, Deserialize, Serialize)]
struct SerdeTraceSignature {
key_id: String,
key_kind: String,
key_fingerprint: String,
algorithm: String,
value: String,
}
fn pretty_json(compact: &str) -> String {
let mut pretty = String::new();
let mut in_string = false;
let mut escaped = false;
for ch in compact.chars() {
if in_string {
pretty.push(ch);
if escaped {
escaped = false;
} else if ch == '\\' {
escaped = true;
} else if ch == '"' {
in_string = false;
}
continue;
}
match ch {
'"' => {
in_string = true;
pretty.push(ch);
}
'{' | '[' => {
pretty.push(ch);
pretty.push('\n');
pretty.push_str(" ");
}
'}' | ']' => {
pretty.push('\n');
pretty.push(ch);
}
',' => {
pretty.push(ch);
pretty.push('\n');
pretty.push_str(" ");
}
':' => pretty.push_str(" : "),
other => pretty.push(other),
}
}
pretty
}
fn canonical_serde_tuning_json(tuning: &SerdeTraceTuning) -> String {
format!(
"{{\"artifact\":\"{}\",\"version\":{},\"backend\":\"{}\",\"selected_strategy\":\"{}\",\"benchmark_count\":{},\"enable_pointwise_fusion\":{},\"enable_padic_matmul_valuation_skip\":{}}}",
tuning.artifact,
tuning.version,
tuning.backend,
tuning.selected_strategy,
tuning.benchmark_count,
tuning.enable_pointwise_fusion,
tuning.enable_padic_matmul_valuation_skip
)
}
fn canonical_serde_benchmark_json(benchmarks: &SerdeTraceBenchmarkSet) -> String {
let records = benchmarks
.records
.iter()
.map(canonical_serde_benchmark_record_json)
.collect::<Vec<_>>()
.join(",");
format!(
"{{\"artifact\":\"{}\",\"version\":{},\"plan_fingerprint\":\"{}\",\"backend\":\"{}\",\"selected_strategy\":\"{}\",\"records\":[{}]}}",
benchmarks.artifact,
benchmarks.version,
benchmarks.plan_fingerprint,
benchmarks.backend,
benchmarks.selected_strategy,
records
)
}
fn canonical_serde_benchmark_record_json(record: &SerdeTraceBenchmarkRecord) -> String {
format!(
"{{\"plan_fingerprint\":\"{}\",\"backend\":\"{}\",\"strategy\":\"{}\",\"input_description\":\"{}\",\"duration_ns\":{}}}",
record.plan_fingerprint,
record.backend,
record.strategy,
record.input_description,
record.duration_ns
)
}
fn canonical_serde_proof_replay_report_json(report: &SerdeProofReplayReport) -> String {
let plan_fingerprint = report
.plan_fingerprint
.as_ref()
.map_or_else(|| "null".to_string(), |value| format!("\"{value}\""));
let replayed_proofs = report
.replayed_proofs
.iter()
.map(canonical_serde_proof_replay_entry_json)
.collect::<Vec<_>>()
.join(",");
let warnings = report
.warnings
.iter()
.map(|warning| format!("\"{warning}\""))
.collect::<Vec<_>>()
.join(",");
format!(
"{{\"artifact\":\"{}\",\"version\":{},\"plan_fingerprint\":{},\"checked_proofs\":{},\"replayed_proofs\":[{}],\"warnings\":[{}]}}",
report.artifact,
report.version,
plan_fingerprint,
report.checked_proofs,
replayed_proofs,
warnings
)
}
fn canonical_serde_proof_replay_entry_json(entry: &SerdeProofReplayEntry) -> String {
format!(
"{{\"theorem_id\":\"{}\",\"original_id\":\"{}\",\"kind\":\"{}\",\"status\":\"{}\",\"replayed\":{},\"replay_rule\":\"{}\"}}",
entry.theorem_id,
entry.original_id,
entry.kind,
entry.status,
entry.replayed,
entry.replay_rule
)
}
fn canonical_serde_checker_transcript_json(transcript: &SerdeCheckerTranscript) -> String {
format!(
"{{\"artifact\":\"{}\",\"version\":{},\"plan_fingerprint\":\"{}\",\"checker_command\":\"{}\",\"artifact_filename\":\"{}\",\"artifact_digest\":\"{}\",\"exit_status\":{},\"stdout_digest\":\"{}\",\"stderr_digest\":\"{}\",\"result_status\":\"{}\"}}",
transcript.artifact,
transcript.version,
transcript.plan_fingerprint,
transcript.checker_command,
transcript.artifact_filename,
transcript.artifact_digest,
transcript.exit_status,
transcript.stdout_digest,
transcript.stderr_digest,
transcript.result_status
)
}
fn canonical_serde_checker_output_json(output: &SerdeCheckerOutput) -> String {
format!(
"{{\"artifact\":\"{}\",\"version\":{},\"plan_fingerprint\":\"{}\",\"artifact_filename\":\"{}\",\"artifact_digest\":\"{}\",\"transcript_digest\":\"{}\",\"adapter_backend\":\"{}\",\"checker_version\":\"{}\",\"checked_theorem_count\":{},\"result_status\":\"{}\"}}",
output.artifact,
output.version,
output.plan_fingerprint,
output.artifact_filename,
output.artifact_digest,
output.transcript_digest,
output.adapter_backend,
output.checker_version,
output.checked_theorem_count,
output.result_status
)
}
fn canonical_serde_native_admission_json(admission: &SerdeNativeAdmission) -> String {
let plan_fingerprint = admission
.plan_fingerprint
.as_ref()
.map_or_else(|| "null".to_string(), |value| format!("\"{value}\""));
let theorem_result_fingerprints = admission
.theorem_result_fingerprints
.iter()
.map(|fingerprint| format!("\"{fingerprint}\""))
.collect::<Vec<_>>()
.join(",");
format!(
"{{\"artifact\":\"{}\",\"version\":{},\"plan_fingerprint\":{},\"adapter_backend\":\"{}\",\"checker_version\":\"{}\",\"checked_theorem_count\":{},\"result_status\":\"{}\",\"theorem_result_fingerprints\":[{}],\"admission_claim\":\"{}\",\"evidence_digest\":\"{}\"}}",
admission.artifact,
admission.version,
plan_fingerprint,
admission.adapter_backend,
admission.checker_version,
admission.checked_theorem_count,
admission.result_status,
theorem_result_fingerprints,
admission.admission_claim,
admission.evidence_digest
)
}
fn canonical_serde_checker_result_index_json(index: &SerdeCheckerResultIndex) -> String {
let entries = index
.entries
.iter()
.map(canonical_serde_checker_result_entry_json)
.collect::<Vec<_>>()
.join(",");
format!(
"{{\"artifact\":\"{}\",\"version\":{},\"plan_fingerprint\":\"{}\",\"entry_count\":{},\"entries\":[{}]}}",
index.artifact, index.version, index.plan_fingerprint, index.entry_count, entries
)
}
fn canonical_serde_checker_result_entry_json(entry: &SerdeCheckerResultEntry) -> String {
format!(
"{{\"theorem_id\":\"{}\",\"theorem_result_fingerprint\":\"{}\",\"adapter_capability_fingerprint\":\"{}\",\"admission_artifact_digest\":\"{}\",\"plan_fingerprint\":\"{}\"}}",
entry.theorem_id,
entry.theorem_result_fingerprint,
entry.adapter_capability_fingerprint,
entry.admission_artifact_digest,
entry.plan_fingerprint
)
}
fn canonical_serde_adapter_registry_json(registry: &SerdeAdapterRegistry) -> String {
let plan_fingerprint = registry
.plan_fingerprint
.as_ref()
.map_or_else(|| "null".to_string(), |value| format!("\"{value}\""));
let capabilities = registry
.capabilities
.iter()
.map(canonical_serde_adapter_capability_json)
.collect::<Vec<_>>()
.join(",");
format!(
"{{\"artifact\":\"{}\",\"version\":{},\"plan_fingerprint\":{},\"capabilities\":[{}]}}",
registry.artifact, registry.version, plan_fingerprint, capabilities
)
}
fn canonical_serde_adapter_capability_json(capability: &SerdeAdapterCapability) -> String {
let admission_artifact_digest = capability
.admission_artifact_digest
.as_ref()
.map_or_else(|| "null".to_string(), |value| format!("\"{value}\""));
format!(
"{{\"adapter_backend\":\"{}\",\"checker_version\":\"{}\",\"proof_status\":\"{}\",\"native_checked\":{},\"admission_artifact_digest\":{},\"capability_fingerprint\":\"{}\"}}",
capability.adapter_backend,
capability.checker_version,
capability.proof_status,
capability.native_checked,
admission_artifact_digest,
capability.capability_fingerprint
)
}
fn canonical_serde_trace_manifest_json(manifest: &SerdeTraceManifest) -> String {
let plan_fingerprint = manifest
.plan_fingerprint
.as_ref()
.map_or_else(|| "null".to_string(), |value| format!("\"{value}\""));
let artifacts = manifest
.artifacts
.iter()
.map(canonical_serde_trace_artifact_json)
.collect::<Vec<_>>()
.join(",");
let proof_assistant = manifest.proof_assistant.as_ref().map_or_else(
|| "null".to_string(),
canonical_serde_proof_assistant_summary_json,
);
let tuning = manifest
.tuning
.as_ref()
.map_or_else(|| "null".to_string(), canonical_serde_manifest_tuning_json);
let signature = manifest
.signature
.as_ref()
.map_or_else(|| "null".to_string(), canonical_serde_trace_signature_json);
format!(
"{{\"artifact\":\"{}\",\"version\":{},\"trace_name\":\"{}\",\"plan_fingerprint\":{},\"artifacts\":[{}],\"proof_assistant\":{},\"tuning\":{},\"signature\":{}}}",
manifest.artifact,
manifest.version,
manifest.trace_name,
plan_fingerprint,
artifacts,
proof_assistant,
tuning,
signature
)
}
fn canonical_serde_trace_artifact_json(artifact: &SerdeTraceArtifact) -> String {
format!(
"{{\"filename\":\"{}\",\"artifact\":\"{}\",\"version\":{},\"format\":\"{}\",\"digest\":\"{}\"}}",
artifact.filename, artifact.artifact, artifact.version, artifact.format, artifact.digest
)
}
fn canonical_serde_proof_assistant_summary_json(summary: &SerdeProofAssistantSummary) -> String {
let plan_fingerprint = summary
.plan_fingerprint
.as_ref()
.map_or_else(|| "null".to_string(), |value| format!("\"{value}\""));
let theorems = summary
.theorems
.iter()
.map(canonical_serde_proof_assistant_theorem_summary_json)
.collect::<Vec<_>>()
.join(",");
format!(
"{{\"dialect\":\"{}\",\"plan_fingerprint\":{},\"filename\":\"{}\",\"adapter_registry_filename\":\"{}\",\"adapter_registry_digest\":\"{}\",\"theorem_count\":{},\"theorems\":[{}]}}",
summary.dialect,
plan_fingerprint,
summary.filename,
summary.adapter_registry_filename,
summary.adapter_registry_digest,
summary.theorem_count,
theorems
)
}
fn canonical_serde_proof_assistant_theorem_summary_json(
theorem: &SerdeProofAssistantTheoremSummary,
) -> String {
let obligations = theorem
.obligations
.iter()
.map(|item| format!("\"{item}\""))
.collect::<Vec<_>>()
.join(",");
let evidence = theorem
.evidence
.iter()
.map(|item| format!("\"{item}\""))
.collect::<Vec<_>>()
.join(",");
format!(
"{{\"theorem_id\":\"{}\",\"original_id\":\"{}\",\"kind\":\"{}\",\"status\":\"{}\",\"replay_rule\":\"{}\",\"obligations\":[{}],\"evidence\":[{}],\"obligation_count\":{},\"evidence_count\":{},\"statement_fingerprint\":\"{}\",\"adapter_backend\":\"{}\",\"checker_version\":\"{}\",\"proof_status\":\"{}\",\"adapter_capability_fingerprint\":\"{}\"}}",
theorem.theorem_id,
theorem.original_id,
theorem.kind,
theorem.status,
theorem.replay_rule,
obligations,
evidence,
theorem.obligation_count,
theorem.evidence_count,
theorem.statement_fingerprint,
theorem.adapter_backend,
theorem.checker_version,
theorem.proof_status,
theorem.adapter_capability_fingerprint
)
}
fn canonical_serde_manifest_tuning_json(tuning: &SerdeManifestTuning) -> String {
format!(
"{{\"backend\":\"{}\",\"selected_strategy\":\"{}\",\"benchmark_count\":{},\"enable_pointwise_fusion\":{},\"enable_padic_matmul_valuation_skip\":{}}}",
tuning.backend,
tuning.selected_strategy,
tuning.benchmark_count,
tuning.enable_pointwise_fusion,
tuning.enable_padic_matmul_valuation_skip
)
}
fn canonical_serde_trace_signature_json(signature: &SerdeTraceSignature) -> String {
format!(
"{{\"key_id\":\"{}\",\"key_kind\":\"{}\",\"key_fingerprint\":\"{}\",\"algorithm\":\"{}\",\"value\":\"{}\"}}",
signature.key_id,
signature.key_kind,
signature.key_fingerprint,
signature.algorithm,
signature.value
)
}
const PLAN_DIGEST: &str = "sha256:1111111111111111111111111111111111111111111111111111111111111111";
const ARTIFACT_DIGEST: &str =
"sha256:2222222222222222222222222222222222222222222222222222222222222222";
const TRANSCRIPT_DIGEST: &str =
"sha256:3333333333333333333333333333333333333333333333333333333333333333";
const THEOREM_RESULT_DIGEST: &str =
"sha256:4444444444444444444444444444444444444444444444444444444444444444";
const CAPABILITY_DIGEST: &str =
"sha256:5555555555555555555555555555555555555555555555555555555555555555";
const ADMISSION_DIGEST: &str =
"sha256:6666666666666666666666666666666666666666666666666666666666666666";
#[test]
fn paper_critical_json_parsers_accept_whitespace_outside_strings() {
let report_json = proof_replay_json_report(&tokitai_operator::verify::ProofReplayReport {
plan_fingerprint: None,
checked_proofs: 0,
replayed_proofs: Vec::new(),
warnings: Vec::new(),
});
assert_eq!(
parse_proof_replay_report_json(&pretty_json(&report_json)).unwrap(),
parse_proof_replay_report_json(&report_json).unwrap()
);
let bundle = tokitai_operator::verify::proof_replay_artifact_bundle(
"parser regression",
&parse_proof_replay_report_json(&report_json).unwrap(),
)
.unwrap();
let manifest = proof_replay_trace_manifest("parser regression", &bundle).unwrap();
let manifest_json = proof_replay_trace_manifest_json(&manifest);
assert_eq!(
parse_proof_replay_trace_manifest_json(&pretty_json(&manifest_json)).unwrap(),
manifest
);
let tuning = ProofReplayTraceTuning {
backend: "cpu scalar".to_string(),
selected_strategy: "dense baseline".to_string(),
benchmark_count: 1,
enable_pointwise_fusion: false,
enable_padic_matmul_valuation_skip: false,
};
let tuning_json = proof_replay_trace_tuning_json(&tuning);
assert_eq!(
parse_proof_replay_trace_tuning_json(&pretty_json(&tuning_json)).unwrap(),
tuning
);
let benchmarks = ProofReplayTraceBenchmarkSet {
plan_fingerprint: "sha256:1111111111111111111111111111111111111111111111111111111111111111"
.to_string(),
backend: "cpu scalar".to_string(),
selected_strategy: "dense baseline".to_string(),
records: vec![ProofReplayTraceBenchmarkRecord {
plan_fingerprint:
"sha256:1111111111111111111111111111111111111111111111111111111111111111"
.to_string(),
backend: "cpu scalar".to_string(),
strategy: "dense baseline".to_string(),
input_description: "keeps internal spaces".to_string(),
duration_ns: 42,
}],
};
let benchmark_json = proof_replay_trace_benchmark_json(&benchmarks);
assert_eq!(
parse_proof_replay_trace_benchmark_json(&pretty_json(&benchmark_json)).unwrap(),
benchmarks
);
let checkable_artifact = ProofReplayTraceArtifact {
filename: "parser_regression.lean-checkable.lean".to_string(),
artifact: "tokitai-proof-assistant-lean-checkable".to_string(),
version: 1,
format: "lean".to_string(),
digest: "sha256:2222222222222222222222222222222222222222222222222222222222222222"
.to_string(),
};
let transcript = proof_assistant_checker_transcript(
"sha256:1111111111111111111111111111111111111111111111111111111111111111",
&checkable_artifact,
"lean parser_regression.lean-checkable.lean",
0,
"Lean accepted with spaces",
"",
"accepted",
)
.unwrap();
let transcript_json = proof_assistant_checker_transcript_json(&transcript);
assert_eq!(
parse_proof_assistant_checker_transcript_json(&pretty_json(&transcript_json)).unwrap(),
transcript
);
}
#[test]
fn paper_critical_json_parsers_keep_schema_errors_explicit() {
let report_json = proof_replay_json_report(&tokitai_operator::verify::ProofReplayReport {
plan_fingerprint: None,
checked_proofs: 0,
replayed_proofs: Vec::new(),
warnings: Vec::new(),
});
assert!(
parse_proof_replay_report_json(&report_json.replace("\"version\":1", "\"version\":2"))
.is_err()
);
assert!(
parse_proof_replay_report_json(&report_json.replace("\"checked_proofs\":0,", "")).is_err()
);
}
#[test]
fn selected_proof_artifact_parsers_accept_reordered_object_fields() {
let report = ProofReplayReport {
plan_fingerprint: Some(PLAN_DIGEST.to_string()),
checked_proofs: 1,
replayed_proofs: vec![ProofReplayEntry {
theorem_id: "tokitai_replay_0".to_string(),
original_id: "replay-0".to_string(),
kind: "rewrite_soundness".to_string(),
status: "proven".to_string(),
replayed: true,
replay_rule: "rewrite_soundness_replay".to_string(),
}],
warnings: vec!["keeps internal spaces".to_string()],
};
let report_json = proof_replay_json_report(&report);
let reordered_report_json = format!(
"{{\"warnings\":[\"keeps internal spaces\"],\"replayed_proofs\":[{{\"replay_rule\":\"rewrite_soundness_replay\",\"replayed\":true,\"status\":\"proven\",\"kind\":\"rewrite_soundness\",\"original_id\":\"replay-0\",\"theorem_id\":\"tokitai_replay_0\"}}],\"checked_proofs\":1,\"plan_fingerprint\":\"{PLAN_DIGEST}\",\"version\":1,\"artifact\":\"tokitai-proof-replay-report\"}}"
);
assert_eq!(
parse_proof_replay_report_json(&reordered_report_json).unwrap(),
parse_proof_replay_report_json(&report_json).unwrap()
);
let checkable_artifact = ProofReplayTraceArtifact {
filename: "parser_regression.lean-checkable.lean".to_string(),
artifact: "tokitai-proof-assistant-lean-checkable".to_string(),
version: 1,
format: "lean".to_string(),
digest: ARTIFACT_DIGEST.to_string(),
};
let transcript = proof_assistant_checker_transcript(
PLAN_DIGEST,
&checkable_artifact,
"lean parser_regression.lean-checkable.lean",
0,
"Lean accepted with spaces",
"",
"accepted",
)
.unwrap();
let transcript_json = proof_assistant_checker_transcript_json(&transcript);
let reordered_transcript_json = format!(
"{{\"result_status\":\"accepted\",\"stderr_digest\":\"{}\",\"stdout_digest\":\"{}\",\"exit_status\":0,\"artifact_digest\":\"{ARTIFACT_DIGEST}\",\"artifact_filename\":\"parser_regression.lean-checkable.lean\",\"checker_command\":\"lean parser_regression.lean-checkable.lean\",\"plan_fingerprint\":\"{PLAN_DIGEST}\",\"version\":1,\"artifact\":\"tokitai-proof-assistant-checker-transcript\"}}",
transcript.stderr_digest, transcript.stdout_digest
);
assert_eq!(
parse_proof_assistant_checker_transcript_json(&reordered_transcript_json).unwrap(),
parse_proof_assistant_checker_transcript_json(&transcript_json).unwrap()
);
let output = ProofAssistantCheckerOutput {
plan_fingerprint: PLAN_DIGEST.to_string(),
artifact_filename: "parser_regression.lean-checkable.lean".to_string(),
artifact_digest: ARTIFACT_DIGEST.to_string(),
transcript_digest: TRANSCRIPT_DIGEST.to_string(),
adapter_backend: "lean-skeleton".to_string(),
checker_version: "tokitai-replay-skeleton-v1".to_string(),
checked_theorem_count: 1,
result_status: "accepted".to_string(),
};
let output_json = proof_assistant_checker_output_json(&output);
let reordered_output_json = format!(
"{{\"result_status\":\"accepted\",\"checked_theorem_count\":1,\"checker_version\":\"tokitai-replay-skeleton-v1\",\"adapter_backend\":\"lean-skeleton\",\"transcript_digest\":\"{TRANSCRIPT_DIGEST}\",\"artifact_digest\":\"{ARTIFACT_DIGEST}\",\"artifact_filename\":\"parser_regression.lean-checkable.lean\",\"plan_fingerprint\":\"{PLAN_DIGEST}\",\"version\":1,\"artifact\":\"tokitai-proof-assistant-checker-output\"}}"
);
assert_eq!(
parse_proof_assistant_checker_output_json(&reordered_output_json).unwrap(),
parse_proof_assistant_checker_output_json(&output_json).unwrap()
);
let admission = ProofAssistantNativeAdmission {
plan_fingerprint: Some(PLAN_DIGEST.to_string()),
adapter_backend: "lean-skeleton".to_string(),
checker_version: "tokitai-replay-skeleton-v1".to_string(),
checked_theorem_count: 1,
result_status: "accepted".to_string(),
theorem_result_fingerprints: vec![THEOREM_RESULT_DIGEST.to_string()],
admission_claim: "native checker accepted proof assistant artifact".to_string(),
evidence_digest: TRANSCRIPT_DIGEST.to_string(),
};
let admission_json = proof_assistant_native_admission_json(&admission);
let reordered_admission_json = format!(
"{{\"evidence_digest\":\"{TRANSCRIPT_DIGEST}\",\"admission_claim\":\"native checker accepted proof assistant artifact\",\"theorem_result_fingerprints\":[\"{THEOREM_RESULT_DIGEST}\"],\"result_status\":\"accepted\",\"checked_theorem_count\":1,\"checker_version\":\"tokitai-replay-skeleton-v1\",\"adapter_backend\":\"lean-skeleton\",\"plan_fingerprint\":\"{PLAN_DIGEST}\",\"version\":1,\"artifact\":\"tokitai-proof-assistant-native-admission\"}}"
);
assert_eq!(
parse_proof_assistant_native_admission_json(&reordered_admission_json).unwrap(),
parse_proof_assistant_native_admission_json(&admission_json).unwrap()
);
let index = CheckerResultIndex {
plan_fingerprint: PLAN_DIGEST.to_string(),
entry_count: 1,
entries: vec![CheckerResultEntry {
theorem_id: "tokitai_replay_0".to_string(),
theorem_result_fingerprint: THEOREM_RESULT_DIGEST.to_string(),
adapter_capability_fingerprint: CAPABILITY_DIGEST.to_string(),
admission_artifact_digest: ADMISSION_DIGEST.to_string(),
plan_fingerprint: PLAN_DIGEST.to_string(),
}],
};
let index_json = checker_result_index_json(&index);
let reordered_index_json = format!(
"{{\"entries\":[{{\"plan_fingerprint\":\"{PLAN_DIGEST}\",\"admission_artifact_digest\":\"{ADMISSION_DIGEST}\",\"adapter_capability_fingerprint\":\"{CAPABILITY_DIGEST}\",\"theorem_result_fingerprint\":\"{THEOREM_RESULT_DIGEST}\",\"theorem_id\":\"tokitai_replay_0\"}}],\"entry_count\":1,\"plan_fingerprint\":\"{PLAN_DIGEST}\",\"version\":1,\"artifact\":\"tokitai-proof-assistant-checker-result-index\"}}"
);
assert_eq!(
parse_checker_result_index_json(&reordered_index_json).unwrap(),
parse_checker_result_index_json(&index_json).unwrap()
);
}
#[test]
fn trace_artifact_parsers_accept_reordered_object_fields() {
let report = ProofReplayReport {
plan_fingerprint: Some(PLAN_DIGEST.to_string()),
checked_proofs: 1,
replayed_proofs: vec![ProofReplayEntry {
theorem_id: "tokitai_replay_0".to_string(),
original_id: "replay-0".to_string(),
kind: "rewrite_soundness".to_string(),
status: "proven".to_string(),
replayed: true,
replay_rule: "rewrite_soundness_replay".to_string(),
}],
warnings: Vec::new(),
};
let bundle = proof_replay_artifact_bundle("parser regression trace", &report).unwrap();
let mut manifest = proof_replay_trace_manifest("parser regression trace", &bundle).unwrap();
let adapter_capability = proof_assistant_skeleton_adapter_capability();
let registry_artifact = proof_assistant_adapter_registry_artifact_for_capabilities(
"parser regression trace",
Some(PLAN_DIGEST),
std::slice::from_ref(&adapter_capability),
)
.unwrap();
let certificate = ProofCertificate {
version: 1,
backend: "cpu scalar".to_string(),
proofs: vec![ProofCertificateEntry {
theorem_id: "tokitai_replay_0".to_string(),
original_id: "replay-0".to_string(),
kind: "rewrite_soundness".to_string(),
status: "proven".to_string(),
claim: "parser regression replay claim".to_string(),
obligations: Vec::new(),
evidence: vec!["semantic replay evidence".to_string()],
}],
};
let skeleton =
proof_assistant_replay_skeleton(&certificate, &report, ProofAssistantDialect::Lean)
.unwrap();
let skeleton_artifact =
proof_assistant_replay_skeleton_artifact("parser regression trace", &skeleton).unwrap();
let summary = proof_assistant_replay_summary_with_adapter_registry(
&skeleton_artifact.filename,
&skeleton,
®istry_artifact,
)
.unwrap();
let summary =
proof_assistant_replay_summary_with_adapter_capability(&summary, &adapter_capability)
.unwrap();
manifest.plan_fingerprint = Some(PLAN_DIGEST.to_string());
manifest.artifacts.push(skeleton_artifact);
manifest.artifacts.push(registry_artifact.clone());
manifest.proof_assistant = Some(summary.clone());
manifest.tuning = Some(ProofReplayTraceTuning {
backend: "cpu scalar".to_string(),
selected_strategy: "dense baseline".to_string(),
benchmark_count: 1,
enable_pointwise_fusion: true,
enable_padic_matmul_valuation_skip: false,
});
let signed_manifest =
sign_proof_replay_trace_manifest(&manifest, "parser key", "parser-secret").unwrap();
let manifest_json = proof_replay_trace_manifest_json(&signed_manifest);
let artifact_entries = signed_manifest
.artifacts
.iter()
.map(|artifact| {
format!(
"{{\"digest\":\"{}\",\"format\":\"{}\",\"version\":{},\"artifact\":\"{}\",\"filename\":\"{}\"}}",
artifact.digest, artifact.format, artifact.version, artifact.artifact, artifact.filename
)
})
.collect::<Vec<_>>()
.join(",");
let theorem_entries = summary
.theorems
.iter()
.map(|theorem| {
let obligations = theorem
.obligations
.iter()
.map(|item| format!("\"{}\"", item))
.collect::<Vec<_>>()
.join(",");
let evidence = theorem
.evidence
.iter()
.map(|item| format!("\"{}\"", item))
.collect::<Vec<_>>()
.join(",");
format!(
"{{\"adapter_capability_fingerprint\":\"{}\",\"proof_status\":\"{}\",\"checker_version\":\"{}\",\"adapter_backend\":\"{}\",\"statement_fingerprint\":\"{}\",\"evidence_count\":{},\"obligation_count\":{},\"evidence\":[{}],\"obligations\":[{}],\"replay_rule\":\"{}\",\"status\":\"{}\",\"kind\":\"{}\",\"original_id\":\"{}\",\"theorem_id\":\"{}\"}}",
theorem.adapter_capability_fingerprint,
theorem.proof_status,
theorem.checker_version,
theorem.adapter_backend,
theorem.statement_fingerprint,
theorem.evidence_count,
theorem.obligation_count,
evidence,
obligations,
theorem.replay_rule,
theorem.status,
theorem.kind,
theorem.original_id,
theorem.theorem_id
)
})
.collect::<Vec<_>>()
.join(",");
let signature = signed_manifest.signature.as_ref().unwrap();
let reordered_manifest_json = format!(
"{{\"signature\":{{\"value\":\"{}\",\"algorithm\":\"{}\",\"key_fingerprint\":\"{}\",\"key_kind\":\"{}\",\"key_id\":\"{}\"}},\"tuning\":{{\"enable_padic_matmul_valuation_skip\":false,\"enable_pointwise_fusion\":true,\"benchmark_count\":1,\"selected_strategy\":\"dense baseline\",\"backend\":\"cpu scalar\"}},\"proof_assistant\":{{\"theorems\":[{}],\"theorem_count\":{},\"adapter_registry_digest\":\"{}\",\"adapter_registry_filename\":\"{}\",\"filename\":\"{}\",\"plan_fingerprint\":\"{}\",\"dialect\":\"lean\"}},\"artifacts\":[{}],\"plan_fingerprint\":\"{}\",\"trace_name\":\"{}\",\"version\":1,\"artifact\":\"tokitai-proof-replay-trace-manifest\"}}",
signature.value,
signature.algorithm,
signature.key_fingerprint,
signature.key_kind,
signature.key_id,
theorem_entries,
summary.theorem_count,
summary.adapter_registry_digest,
summary.adapter_registry_filename,
summary.filename,
PLAN_DIGEST,
artifact_entries,
PLAN_DIGEST,
signed_manifest.trace_name
);
assert_eq!(
parse_proof_replay_trace_manifest_json(&reordered_manifest_json).unwrap(),
parse_proof_replay_trace_manifest_json(&manifest_json).unwrap()
);
let capability_fingerprint =
proof_assistant_adapter_capability_fingerprint(&adapter_capability);
let registry_json = proof_assistant_adapter_registry_json_for_capabilities(
Some(PLAN_DIGEST),
std::slice::from_ref(&adapter_capability),
);
let reordered_registry_json = format!(
"{{\"capabilities\":[{{\"capability_fingerprint\":\"{}\",\"admission_artifact_digest\":null,\"native_checked\":false,\"proof_status\":\"placeholder\",\"checker_version\":\"tokitai-replay-skeleton-v1\",\"adapter_backend\":\"lean-skeleton\"}}],\"plan_fingerprint\":\"{}\",\"version\":1,\"artifact\":\"tokitai-proof-assistant-adapter-registry\"}}",
capability_fingerprint, PLAN_DIGEST
);
assert_eq!(
parse_proof_assistant_adapter_registry_json(&reordered_registry_json).unwrap(),
parse_proof_assistant_adapter_registry_json(®istry_json).unwrap()
);
let tuning = ProofReplayTraceTuning {
backend: "cpu scalar".to_string(),
selected_strategy: "dense baseline".to_string(),
benchmark_count: 1,
enable_pointwise_fusion: true,
enable_padic_matmul_valuation_skip: false,
};
let tuning_json = proof_replay_trace_tuning_json(&tuning);
let reordered_tuning_json = "{\"enable_padic_matmul_valuation_skip\":false,\"enable_pointwise_fusion\":true,\"benchmark_count\":1,\"selected_strategy\":\"dense baseline\",\"backend\":\"cpu scalar\",\"version\":1,\"artifact\":\"tokitai-proof-replay-trace-tuning\"}";
assert_eq!(
parse_proof_replay_trace_tuning_json(reordered_tuning_json).unwrap(),
parse_proof_replay_trace_tuning_json(&tuning_json).unwrap()
);
let benchmarks = ProofReplayTraceBenchmarkSet {
plan_fingerprint: PLAN_DIGEST.to_string(),
backend: "cpu scalar".to_string(),
selected_strategy: "dense baseline".to_string(),
records: vec![ProofReplayTraceBenchmarkRecord {
plan_fingerprint: PLAN_DIGEST.to_string(),
backend: "cpu scalar".to_string(),
strategy: "dense baseline".to_string(),
input_description: "keeps internal spaces".to_string(),
duration_ns: 42,
}],
};
let benchmark_json = proof_replay_trace_benchmark_json(&benchmarks);
let reordered_benchmark_json = format!(
"{{\"records\":[{{\"duration_ns\":42,\"input_description\":\"keeps internal spaces\",\"strategy\":\"dense baseline\",\"backend\":\"cpu scalar\",\"plan_fingerprint\":\"{PLAN_DIGEST}\"}}],\"selected_strategy\":\"dense baseline\",\"backend\":\"cpu scalar\",\"plan_fingerprint\":\"{PLAN_DIGEST}\",\"version\":1,\"artifact\":\"tokitai-proof-replay-trace-benchmarks\"}}"
);
assert_eq!(
parse_proof_replay_trace_benchmark_json(&reordered_benchmark_json).unwrap(),
parse_proof_replay_trace_benchmark_json(&benchmark_json).unwrap()
);
}
#[test]
fn reordered_imports_normalize_to_canonical_json_and_digests() {
let report = ProofReplayReport {
plan_fingerprint: Some(PLAN_DIGEST.to_string()),
checked_proofs: 1,
replayed_proofs: vec![ProofReplayEntry {
theorem_id: "tokitai_replay_0".to_string(),
original_id: "replay-0".to_string(),
kind: "rewrite_soundness".to_string(),
status: "proven".to_string(),
replayed: true,
replay_rule: "rewrite_soundness_replay".to_string(),
}],
warnings: vec!["canonical renderer keeps this warning".to_string()],
};
let canonical_report_json = proof_replay_json_report(&report);
let reordered_report_json = format!(
"{{\"warnings\":[\"canonical renderer keeps this warning\"],\"replayed_proofs\":[{{\"replay_rule\":\"rewrite_soundness_replay\",\"replayed\":true,\"status\":\"proven\",\"kind\":\"rewrite_soundness\",\"original_id\":\"replay-0\",\"theorem_id\":\"tokitai_replay_0\"}}],\"checked_proofs\":1,\"plan_fingerprint\":\"{PLAN_DIGEST}\",\"version\":1,\"artifact\":\"tokitai-proof-replay-report\"}}"
);
let imported_report = parse_proof_replay_report_json(&reordered_report_json).unwrap();
assert_eq!(
proof_replay_json_report(&imported_report),
canonical_report_json
);
assert_eq!(
proof_replay_artifact_digest(&proof_replay_json_report(&imported_report)),
proof_replay_artifact_digest(&canonical_report_json)
);
let canonical_index = CheckerResultIndex {
plan_fingerprint: PLAN_DIGEST.to_string(),
entry_count: 1,
entries: vec![CheckerResultEntry {
theorem_id: "tokitai_replay_0".to_string(),
theorem_result_fingerprint: THEOREM_RESULT_DIGEST.to_string(),
adapter_capability_fingerprint: CAPABILITY_DIGEST.to_string(),
admission_artifact_digest: ADMISSION_DIGEST.to_string(),
plan_fingerprint: PLAN_DIGEST.to_string(),
}],
};
let canonical_index_json = checker_result_index_json(&canonical_index);
let reordered_index_json = format!(
"{{\"entries\":[{{\"plan_fingerprint\":\"{PLAN_DIGEST}\",\"admission_artifact_digest\":\"{ADMISSION_DIGEST}\",\"adapter_capability_fingerprint\":\"{CAPABILITY_DIGEST}\",\"theorem_result_fingerprint\":\"{THEOREM_RESULT_DIGEST}\",\"theorem_id\":\"tokitai_replay_0\"}}],\"entry_count\":1,\"plan_fingerprint\":\"{PLAN_DIGEST}\",\"version\":1,\"artifact\":\"tokitai-proof-assistant-checker-result-index\"}}"
);
let imported_index = parse_checker_result_index_json(&reordered_index_json).unwrap();
assert_eq!(
checker_result_index_json(&imported_index),
canonical_index_json
);
assert_eq!(
proof_replay_artifact_digest(&checker_result_index_json(&imported_index)),
proof_replay_artifact_digest(&canonical_index_json)
);
let checkable_artifact = ProofReplayTraceArtifact {
filename: "canonical.lean-checkable.lean".to_string(),
artifact: "tokitai-proof-assistant-lean-checkable".to_string(),
version: 1,
format: "lean".to_string(),
digest: ARTIFACT_DIGEST.to_string(),
};
let transcript = proof_assistant_checker_transcript(
PLAN_DIGEST,
&checkable_artifact,
"lean canonical.lean-checkable.lean",
0,
"accepted",
"",
"accepted",
)
.unwrap();
let canonical_transcript_json = proof_assistant_checker_transcript_json(&transcript);
let reordered_transcript_json = format!(
"{{\"result_status\":\"accepted\",\"stderr_digest\":\"{}\",\"stdout_digest\":\"{}\",\"exit_status\":0,\"artifact_digest\":\"{ARTIFACT_DIGEST}\",\"artifact_filename\":\"canonical.lean-checkable.lean\",\"checker_command\":\"lean canonical.lean-checkable.lean\",\"plan_fingerprint\":\"{PLAN_DIGEST}\",\"version\":1,\"artifact\":\"tokitai-proof-assistant-checker-transcript\"}}",
transcript.stderr_digest, transcript.stdout_digest
);
let imported_transcript =
parse_proof_assistant_checker_transcript_json(&reordered_transcript_json).unwrap();
assert_eq!(
proof_assistant_checker_transcript_json(&imported_transcript),
canonical_transcript_json
);
assert_eq!(
proof_replay_artifact_digest(&proof_assistant_checker_transcript_json(
&imported_transcript
)),
proof_replay_artifact_digest(&canonical_transcript_json)
);
let output = proof_assistant_checker_output(
PLAN_DIGEST,
&checkable_artifact,
&transcript,
"lean-skeleton",
"tokitai-replay-skeleton-v1",
1,
"accepted",
)
.unwrap();
let canonical_output_json = proof_assistant_checker_output_json(&output);
let reordered_output_json = format!(
"{{\"result_status\":\"accepted\",\"checked_theorem_count\":1,\"checker_version\":\"tokitai-replay-skeleton-v1\",\"adapter_backend\":\"lean-skeleton\",\"transcript_digest\":\"{}\",\"artifact_digest\":\"{ARTIFACT_DIGEST}\",\"artifact_filename\":\"canonical.lean-checkable.lean\",\"plan_fingerprint\":\"{PLAN_DIGEST}\",\"version\":1,\"artifact\":\"tokitai-proof-assistant-checker-output\"}}",
output.transcript_digest
);
let imported_output =
parse_proof_assistant_checker_output_json(&reordered_output_json).unwrap();
assert_eq!(
proof_assistant_checker_output_json(&imported_output),
canonical_output_json
);
assert_eq!(
proof_replay_artifact_digest(&proof_assistant_checker_output_json(&imported_output)),
proof_replay_artifact_digest(&canonical_output_json)
);
let admission = ProofAssistantNativeAdmission {
plan_fingerprint: Some(PLAN_DIGEST.to_string()),
adapter_backend: "lean-skeleton".to_string(),
checker_version: "tokitai-replay-skeleton-v1".to_string(),
checked_theorem_count: 1,
result_status: "accepted".to_string(),
theorem_result_fingerprints: vec![THEOREM_RESULT_DIGEST.to_string()],
admission_claim: "native checker accepted proof assistant artifact".to_string(),
evidence_digest: proof_replay_artifact_digest(&canonical_output_json),
};
let canonical_admission_json = proof_assistant_native_admission_json(&admission);
let reordered_admission_json = format!(
"{{\"evidence_digest\":\"{}\",\"admission_claim\":\"native checker accepted proof assistant artifact\",\"theorem_result_fingerprints\":[\"{THEOREM_RESULT_DIGEST}\"],\"result_status\":\"accepted\",\"checked_theorem_count\":1,\"checker_version\":\"tokitai-replay-skeleton-v1\",\"adapter_backend\":\"lean-skeleton\",\"plan_fingerprint\":\"{PLAN_DIGEST}\",\"version\":1,\"artifact\":\"tokitai-proof-assistant-native-admission\"}}",
admission.evidence_digest
);
let imported_admission =
parse_proof_assistant_native_admission_json(&reordered_admission_json).unwrap();
assert_eq!(
proof_assistant_native_admission_json(&imported_admission),
canonical_admission_json
);
assert_eq!(
proof_replay_artifact_digest(&proof_assistant_native_admission_json(&imported_admission)),
proof_replay_artifact_digest(&canonical_admission_json)
);
let bundle = proof_replay_artifact_bundle("canonical trace", &report).unwrap();
let mut manifest = proof_replay_trace_manifest("canonical trace", &bundle).unwrap();
let adapter_capability = proof_assistant_skeleton_adapter_capability();
let registry_artifact = proof_assistant_adapter_registry_artifact_for_capabilities(
"canonical trace",
Some(PLAN_DIGEST),
std::slice::from_ref(&adapter_capability),
)
.unwrap();
let certificate = ProofCertificate {
version: 1,
backend: "cpu scalar".to_string(),
proofs: vec![ProofCertificateEntry {
theorem_id: "tokitai_replay_0".to_string(),
original_id: "replay-0".to_string(),
kind: "rewrite_soundness".to_string(),
status: "proven".to_string(),
claim: "canonical replay claim".to_string(),
obligations: Vec::new(),
evidence: vec!["canonical semantic evidence".to_string()],
}],
};
let skeleton =
proof_assistant_replay_skeleton(&certificate, &report, ProofAssistantDialect::Lean)
.unwrap();
let skeleton_artifact =
proof_assistant_replay_skeleton_artifact("canonical trace", &skeleton).unwrap();
let summary = proof_assistant_replay_summary_with_adapter_registry(
&skeleton_artifact.filename,
&skeleton,
®istry_artifact,
)
.unwrap();
let summary =
proof_assistant_replay_summary_with_adapter_capability(&summary, &adapter_capability)
.unwrap();
manifest.plan_fingerprint = Some(PLAN_DIGEST.to_string());
manifest.artifacts.push(skeleton_artifact);
manifest.artifacts.push(registry_artifact);
manifest.proof_assistant = Some(summary.clone());
manifest.tuning = Some(ProofReplayTraceTuning {
backend: "cpu scalar".to_string(),
selected_strategy: "dense baseline".to_string(),
benchmark_count: 1,
enable_pointwise_fusion: true,
enable_padic_matmul_valuation_skip: false,
});
let signed_manifest =
sign_proof_replay_trace_manifest(&manifest, "canonical key", "canonical-secret").unwrap();
let canonical_manifest_json = proof_replay_trace_manifest_json(&signed_manifest);
let artifact_entries = signed_manifest
.artifacts
.iter()
.map(|artifact| {
format!(
"{{\"digest\":\"{}\",\"format\":\"{}\",\"version\":{},\"artifact\":\"{}\",\"filename\":\"{}\"}}",
artifact.digest, artifact.format, artifact.version, artifact.artifact, artifact.filename
)
})
.collect::<Vec<_>>()
.join(",");
let theorem_entries = summary
.theorems
.iter()
.map(|theorem| {
let evidence = theorem
.evidence
.iter()
.map(|item| format!("\"{}\"", item))
.collect::<Vec<_>>()
.join(",");
format!(
"{{\"adapter_capability_fingerprint\":\"{}\",\"proof_status\":\"{}\",\"checker_version\":\"{}\",\"adapter_backend\":\"{}\",\"statement_fingerprint\":\"{}\",\"evidence_count\":{},\"obligation_count\":{},\"evidence\":[{}],\"obligations\":[],\"replay_rule\":\"{}\",\"status\":\"{}\",\"kind\":\"{}\",\"original_id\":\"{}\",\"theorem_id\":\"{}\"}}",
theorem.adapter_capability_fingerprint,
theorem.proof_status,
theorem.checker_version,
theorem.adapter_backend,
theorem.statement_fingerprint,
theorem.evidence_count,
theorem.obligation_count,
evidence,
theorem.replay_rule,
theorem.status,
theorem.kind,
theorem.original_id,
theorem.theorem_id
)
})
.collect::<Vec<_>>()
.join(",");
let signature = signed_manifest.signature.as_ref().unwrap();
let reordered_manifest_json = format!(
"{{\"signature\":{{\"value\":\"{}\",\"algorithm\":\"{}\",\"key_fingerprint\":\"{}\",\"key_kind\":\"{}\",\"key_id\":\"{}\"}},\"tuning\":{{\"enable_padic_matmul_valuation_skip\":false,\"enable_pointwise_fusion\":true,\"benchmark_count\":1,\"selected_strategy\":\"dense baseline\",\"backend\":\"cpu scalar\"}},\"proof_assistant\":{{\"theorems\":[{}],\"theorem_count\":{},\"adapter_registry_digest\":\"{}\",\"adapter_registry_filename\":\"{}\",\"filename\":\"{}\",\"plan_fingerprint\":\"{}\",\"dialect\":\"lean\"}},\"artifacts\":[{}],\"plan_fingerprint\":\"{}\",\"trace_name\":\"{}\",\"version\":1,\"artifact\":\"tokitai-proof-replay-trace-manifest\"}}",
signature.value,
signature.algorithm,
signature.key_fingerprint,
signature.key_kind,
signature.key_id,
theorem_entries,
summary.theorem_count,
summary.adapter_registry_digest,
summary.adapter_registry_filename,
summary.filename,
PLAN_DIGEST,
artifact_entries,
PLAN_DIGEST,
signed_manifest.trace_name
);
let imported_manifest =
parse_proof_replay_trace_manifest_json(&reordered_manifest_json).unwrap();
assert_eq!(
proof_replay_trace_manifest_json(&imported_manifest),
canonical_manifest_json
);
assert_eq!(
proof_replay_artifact_digest(&proof_replay_trace_manifest_json(&imported_manifest)),
proof_replay_artifact_digest(&canonical_manifest_json)
);
verify_proof_replay_trace_manifest_signature(&imported_manifest, "canonical-secret").unwrap();
let canonical_registry_json = proof_assistant_adapter_registry_json_for_capabilities(
Some(PLAN_DIGEST),
std::slice::from_ref(&adapter_capability),
);
let capability_fingerprint =
proof_assistant_adapter_capability_fingerprint(&adapter_capability);
let reordered_registry_json = format!(
"{{\"capabilities\":[{{\"capability_fingerprint\":\"{}\",\"admission_artifact_digest\":null,\"native_checked\":false,\"proof_status\":\"placeholder\",\"checker_version\":\"tokitai-replay-skeleton-v1\",\"adapter_backend\":\"lean-skeleton\"}}],\"plan_fingerprint\":\"{PLAN_DIGEST}\",\"version\":1,\"artifact\":\"tokitai-proof-assistant-adapter-registry\"}}",
capability_fingerprint
);
let imported_registry =
parse_proof_assistant_adapter_registry_json(&reordered_registry_json).unwrap();
assert_eq!(
proof_assistant_adapter_registry_json_for_capabilities(
imported_registry.plan_fingerprint.as_deref(),
&imported_registry.capabilities,
),
canonical_registry_json
);
assert_eq!(
proof_replay_artifact_digest(&proof_assistant_adapter_registry_json_for_capabilities(
imported_registry.plan_fingerprint.as_deref(),
&imported_registry.capabilities,
)),
proof_replay_artifact_digest(&canonical_registry_json)
);
let tuning = ProofReplayTraceTuning {
backend: "cpu scalar".to_string(),
selected_strategy: "dense baseline".to_string(),
benchmark_count: 1,
enable_pointwise_fusion: true,
enable_padic_matmul_valuation_skip: false,
};
let canonical_tuning_json = proof_replay_trace_tuning_json(&tuning);
let reordered_tuning_json = "{\"enable_padic_matmul_valuation_skip\":false,\"enable_pointwise_fusion\":true,\"benchmark_count\":1,\"selected_strategy\":\"dense baseline\",\"backend\":\"cpu scalar\",\"version\":1,\"artifact\":\"tokitai-proof-replay-trace-tuning\"}";
let imported_tuning = parse_proof_replay_trace_tuning_json(reordered_tuning_json).unwrap();
assert_eq!(
proof_replay_trace_tuning_json(&imported_tuning),
canonical_tuning_json
);
assert_eq!(
proof_replay_artifact_digest(&proof_replay_trace_tuning_json(&imported_tuning)),
proof_replay_artifact_digest(&canonical_tuning_json)
);
let benchmarks = ProofReplayTraceBenchmarkSet {
plan_fingerprint: PLAN_DIGEST.to_string(),
backend: "cpu scalar".to_string(),
selected_strategy: "dense baseline".to_string(),
records: vec![ProofReplayTraceBenchmarkRecord {
plan_fingerprint: PLAN_DIGEST.to_string(),
backend: "cpu scalar".to_string(),
strategy: "dense baseline".to_string(),
input_description: "canonical benchmark".to_string(),
duration_ns: 42,
}],
};
let canonical_benchmark_json = proof_replay_trace_benchmark_json(&benchmarks);
let reordered_benchmark_json = format!(
"{{\"records\":[{{\"duration_ns\":42,\"input_description\":\"canonical benchmark\",\"strategy\":\"dense baseline\",\"backend\":\"cpu scalar\",\"plan_fingerprint\":\"{PLAN_DIGEST}\"}}],\"selected_strategy\":\"dense baseline\",\"backend\":\"cpu scalar\",\"plan_fingerprint\":\"{PLAN_DIGEST}\",\"version\":1,\"artifact\":\"tokitai-proof-replay-trace-benchmarks\"}}"
);
let imported_benchmarks =
parse_proof_replay_trace_benchmark_json(&reordered_benchmark_json).unwrap();
assert_eq!(
proof_replay_trace_benchmark_json(&imported_benchmarks),
canonical_benchmark_json
);
}
#[test]
fn serde_trace_metadata_fixtures_preserve_canonical_bytes_and_digests() {
let tuning = ProofReplayTraceTuning {
backend: "cpu scalar".to_string(),
selected_strategy: "dense baseline".to_string(),
benchmark_count: 1,
enable_pointwise_fusion: true,
enable_padic_matmul_valuation_skip: false,
};
let canonical_tuning_json = proof_replay_trace_tuning_json(&tuning);
let serde_tuning: SerdeTraceTuning = serde_json::from_str(&canonical_tuning_json)
.expect("trace tuning JSON should parse through serde_json");
assert_eq!(serde_tuning.artifact, "tokitai-proof-replay-trace-tuning");
assert_eq!(serde_tuning.version, 1);
assert_eq!(serde_tuning.backend, "cpu scalar");
assert_eq!(serde_tuning.selected_strategy, "dense baseline");
let serde_tuning_json =
serde_json::to_string(&serde_tuning).expect("serde tuning model should serialize");
assert_eq!(
serde_tuning_json, canonical_tuning_json,
"serde tuning struct output currently matches the fixture, but Tokitai canonical rendering remains the digest source"
);
let generic_tuning_json = serde_json::to_string(
&serde_json::from_str::<serde_json::Value>(&canonical_tuning_json)
.expect("trace tuning should parse as generic serde_json value"),
)
.expect("generic trace tuning value should serialize");
assert_ne!(
generic_tuning_json, canonical_tuning_json,
"generic serde_json Value tuning output is not Tokitai canonical bytes"
);
assert_ne!(
proof_replay_artifact_digest(&generic_tuning_json),
proof_replay_artifact_digest(&canonical_tuning_json),
"generic serde_json Value tuning output must not be a digest source"
);
let serde_tuning_canonical = canonical_serde_tuning_json(&serde_tuning);
assert_eq!(serde_tuning_canonical, canonical_tuning_json);
assert_eq!(
proof_replay_artifact_digest(&serde_tuning_canonical),
proof_replay_artifact_digest(&canonical_tuning_json)
);
for field in [
"artifact",
"version",
"backend",
"selected_strategy",
"benchmark_count",
"enable_pointwise_fusion",
"enable_padic_matmul_valuation_skip",
] {
assert!(
serde_tuning_canonical.contains(&format!("\"{field}\":")),
"serde tuning canonical fixture should preserve field {field}"
);
}
let benchmarks = ProofReplayTraceBenchmarkSet {
plan_fingerprint: PLAN_DIGEST.to_string(),
backend: "cpu scalar".to_string(),
selected_strategy: "dense baseline".to_string(),
records: vec![ProofReplayTraceBenchmarkRecord {
plan_fingerprint: PLAN_DIGEST.to_string(),
backend: "cpu scalar".to_string(),
strategy: "dense baseline".to_string(),
input_description: "canonical benchmark".to_string(),
duration_ns: 42,
}],
};
let canonical_benchmark_json = proof_replay_trace_benchmark_json(&benchmarks);
let serde_benchmarks: SerdeTraceBenchmarkSet = serde_json::from_str(&canonical_benchmark_json)
.expect("trace benchmark JSON should parse through serde_json");
assert_eq!(
serde_benchmarks.artifact,
"tokitai-proof-replay-trace-benchmarks"
);
assert_eq!(serde_benchmarks.version, 1);
assert_eq!(serde_benchmarks.plan_fingerprint, PLAN_DIGEST);
assert_eq!(serde_benchmarks.records.len(), 1);
assert_eq!(serde_benchmarks.records[0].duration_ns, 42);
let serde_benchmark_json =
serde_json::to_string(&serde_benchmarks).expect("serde benchmark model should serialize");
assert_eq!(
serde_benchmark_json, canonical_benchmark_json,
"serde benchmark struct output currently matches the fixture, but Tokitai canonical rendering remains the digest source"
);
let generic_benchmark_json = serde_json::to_string(
&serde_json::from_str::<serde_json::Value>(&canonical_benchmark_json)
.expect("trace benchmarks should parse as generic serde_json value"),
)
.expect("generic trace benchmark value should serialize");
assert_ne!(
generic_benchmark_json, canonical_benchmark_json,
"generic serde_json Value benchmark output is not Tokitai canonical bytes"
);
assert_ne!(
proof_replay_artifact_digest(&generic_benchmark_json),
proof_replay_artifact_digest(&canonical_benchmark_json),
"generic serde_json Value benchmark output must not be a digest source"
);
let serde_benchmark_canonical = canonical_serde_benchmark_json(&serde_benchmarks);
assert_eq!(serde_benchmark_canonical, canonical_benchmark_json);
assert_eq!(
proof_replay_artifact_digest(&serde_benchmark_canonical),
proof_replay_artifact_digest(&canonical_benchmark_json)
);
for field in [
"artifact",
"version",
"plan_fingerprint",
"backend",
"selected_strategy",
"records",
"strategy",
"input_description",
"duration_ns",
] {
assert!(
serde_benchmark_canonical.contains(&format!("\"{field}\":")),
"serde benchmark canonical fixture should preserve field {field}"
);
}
}
#[test]
fn serde_proof_replay_report_fixture_preserves_canonical_bytes_and_digest() {
let report = ProofReplayReport {
plan_fingerprint: Some(PLAN_DIGEST.to_string()),
checked_proofs: 1,
replayed_proofs: vec![ProofReplayEntry {
theorem_id: "tokitai_replay_0".to_string(),
original_id: "replay-0".to_string(),
kind: "rewrite_soundness".to_string(),
status: "proven".to_string(),
replayed: true,
replay_rule: "rewrite_soundness_replay".to_string(),
}],
warnings: vec!["canonical renderer keeps this warning".to_string()],
};
let canonical_report_json = proof_replay_json_report(&report);
let serde_report: SerdeProofReplayReport = serde_json::from_str(&canonical_report_json)
.expect("proof replay report JSON should parse through serde_json");
assert_eq!(serde_report.artifact, "tokitai-proof-replay-report");
assert_eq!(serde_report.version, 1);
assert_eq!(serde_report.plan_fingerprint.as_deref(), Some(PLAN_DIGEST));
assert_eq!(serde_report.checked_proofs, 1);
assert_eq!(serde_report.replayed_proofs.len(), 1);
assert_eq!(serde_report.warnings.len(), 1);
assert_eq!(
serde_report.replayed_proofs[0].theorem_id,
"tokitai_replay_0"
);
assert_eq!(
serde_report.replayed_proofs[0].replay_rule,
"rewrite_soundness_replay"
);
let serde_report_json =
serde_json::to_string(&serde_report).expect("serde proof replay report should serialize");
assert_eq!(
serde_report_json, canonical_report_json,
"serde proof replay report struct output currently matches the fixture, but proof_replay_json_report remains the digest source"
);
let generic_report_json = serde_json::to_string(
&serde_json::from_str::<serde_json::Value>(&canonical_report_json)
.expect("proof replay report should parse as generic serde_json value"),
)
.expect("generic proof replay report value should serialize");
assert_ne!(
generic_report_json, canonical_report_json,
"generic serde_json Value proof replay report output is not Tokitai canonical bytes"
);
assert_ne!(
proof_replay_artifact_digest(&generic_report_json),
proof_replay_artifact_digest(&canonical_report_json),
"generic serde_json Value proof replay report output must not be a digest source"
);
let serde_report_canonical = canonical_serde_proof_replay_report_json(&serde_report);
assert_eq!(serde_report_canonical, canonical_report_json);
assert_eq!(
proof_replay_artifact_digest(&serde_report_canonical),
proof_replay_artifact_digest(&canonical_report_json)
);
assert_eq!(
parse_proof_replay_report_json(&serde_report_canonical).unwrap(),
report
);
for field in [
"artifact",
"version",
"plan_fingerprint",
"checked_proofs",
"replayed_proofs",
"warnings",
"theorem_id",
"original_id",
"kind",
"status",
"replayed",
"replay_rule",
] {
assert!(
serde_report_canonical.contains(&format!("\"{field}\":")),
"serde proof replay report canonical fixture should preserve field {field}"
);
}
}
#[test]
fn serde_checker_artifact_fixtures_preserve_canonical_bytes_and_digests() {
let checkable_artifact = ProofReplayTraceArtifact {
filename: "serde_checker.lean-checkable.lean".to_string(),
artifact: "tokitai-proof-assistant-lean-checkable".to_string(),
version: 1,
format: "lean".to_string(),
digest: ARTIFACT_DIGEST.to_string(),
};
let transcript = proof_assistant_checker_transcript(
PLAN_DIGEST,
&checkable_artifact,
"lean serde_checker.lean-checkable.lean",
0,
"Lean accepted with spaces",
"",
"accepted",
)
.unwrap();
let canonical_transcript_json = proof_assistant_checker_transcript_json(&transcript);
let serde_transcript: SerdeCheckerTranscript = serde_json::from_str(&canonical_transcript_json)
.expect("checker transcript JSON should parse through serde_json");
assert_eq!(
serde_transcript.artifact,
"tokitai-proof-assistant-checker-transcript"
);
assert_eq!(serde_transcript.version, 1);
assert_eq!(serde_transcript.plan_fingerprint, PLAN_DIGEST);
assert_eq!(
serde_transcript.artifact_filename,
"serde_checker.lean-checkable.lean"
);
assert_eq!(serde_transcript.exit_status, 0);
assert_eq!(serde_transcript.result_status, "accepted");
let serde_transcript_json = serde_json::to_string(&serde_transcript)
.expect("serde checker transcript should serialize");
assert_eq!(
serde_transcript_json, canonical_transcript_json,
"serde checker transcript struct output currently matches the fixture, but proof_assistant_checker_transcript_json remains the digest source"
);
let generic_transcript_json = serde_json::to_string(
&serde_json::from_str::<serde_json::Value>(&canonical_transcript_json)
.expect("checker transcript should parse as generic serde_json value"),
)
.expect("generic checker transcript value should serialize");
assert_ne!(
generic_transcript_json, canonical_transcript_json,
"generic serde_json Value checker transcript output is not Tokitai canonical bytes"
);
assert_ne!(
proof_replay_artifact_digest(&generic_transcript_json),
proof_replay_artifact_digest(&canonical_transcript_json),
"generic serde_json Value checker transcript output must not be a digest source"
);
let serde_transcript_canonical = canonical_serde_checker_transcript_json(&serde_transcript);
assert_eq!(serde_transcript_canonical, canonical_transcript_json);
assert_eq!(
proof_replay_artifact_digest(&serde_transcript_canonical),
proof_replay_artifact_digest(&canonical_transcript_json)
);
assert_eq!(
parse_proof_assistant_checker_transcript_json(&serde_transcript_canonical).unwrap(),
transcript
);
for field in [
"artifact",
"version",
"plan_fingerprint",
"checker_command",
"artifact_filename",
"artifact_digest",
"exit_status",
"stdout_digest",
"stderr_digest",
"result_status",
] {
assert!(
serde_transcript_canonical.contains(&format!("\"{field}\":")),
"serde checker transcript canonical fixture should preserve field {field}"
);
}
let output = ProofAssistantCheckerOutput {
plan_fingerprint: PLAN_DIGEST.to_string(),
artifact_filename: checkable_artifact.filename.clone(),
artifact_digest: checkable_artifact.digest.clone(),
transcript_digest: proof_replay_artifact_digest(&canonical_transcript_json),
adapter_backend: "lean-skeleton".to_string(),
checker_version: "tokitai-replay-skeleton-v1".to_string(),
checked_theorem_count: 1,
result_status: "accepted".to_string(),
};
let canonical_output_json = proof_assistant_checker_output_json(&output);
let serde_output: SerdeCheckerOutput = serde_json::from_str(&canonical_output_json)
.expect("checker output JSON should parse through serde_json");
assert_eq!(
serde_output.artifact,
"tokitai-proof-assistant-checker-output"
);
assert_eq!(serde_output.version, 1);
assert_eq!(serde_output.plan_fingerprint, PLAN_DIGEST);
assert_eq!(serde_output.transcript_digest, output.transcript_digest);
assert_eq!(serde_output.checked_theorem_count, 1);
assert_eq!(serde_output.result_status, "accepted");
let serde_output_json =
serde_json::to_string(&serde_output).expect("serde checker output should serialize");
assert_eq!(
serde_output_json, canonical_output_json,
"serde checker output struct output currently matches the fixture, but proof_assistant_checker_output_json remains the digest source"
);
let generic_output_json = serde_json::to_string(
&serde_json::from_str::<serde_json::Value>(&canonical_output_json)
.expect("checker output should parse as generic serde_json value"),
)
.expect("generic checker output value should serialize");
assert_ne!(
generic_output_json, canonical_output_json,
"generic serde_json Value checker output is not Tokitai canonical bytes"
);
assert_ne!(
proof_replay_artifact_digest(&generic_output_json),
proof_replay_artifact_digest(&canonical_output_json),
"generic serde_json Value checker output must not be a digest source"
);
let serde_output_canonical = canonical_serde_checker_output_json(&serde_output);
assert_eq!(serde_output_canonical, canonical_output_json);
assert_eq!(
proof_replay_artifact_digest(&serde_output_canonical),
proof_replay_artifact_digest(&canonical_output_json)
);
assert_eq!(
parse_proof_assistant_checker_output_json(&serde_output_canonical).unwrap(),
output
);
for field in [
"artifact",
"version",
"plan_fingerprint",
"artifact_filename",
"artifact_digest",
"transcript_digest",
"adapter_backend",
"checker_version",
"checked_theorem_count",
"result_status",
] {
assert!(
serde_output_canonical.contains(&format!("\"{field}\":")),
"serde checker output canonical fixture should preserve field {field}"
);
}
}
#[test]
fn serde_high_authority_proof_artifact_fixtures_preserve_binding_bytes_and_digests() {
let admission = ProofAssistantNativeAdmission {
plan_fingerprint: Some(PLAN_DIGEST.to_string()),
adapter_backend: "lean-skeleton".to_string(),
checker_version: "tokitai-replay-skeleton-v1".to_string(),
checked_theorem_count: 1,
result_status: "accepted".to_string(),
theorem_result_fingerprints: vec![THEOREM_RESULT_DIGEST.to_string()],
admission_claim: "native checker accepted proof assistant artifact".to_string(),
evidence_digest: TRANSCRIPT_DIGEST.to_string(),
};
let canonical_admission_json = proof_assistant_native_admission_json(&admission);
let serde_admission: SerdeNativeAdmission = serde_json::from_str(&canonical_admission_json)
.expect("native admission JSON should parse through serde_json");
assert_eq!(
serde_admission.artifact,
"tokitai-proof-assistant-native-admission"
);
assert_eq!(serde_admission.version, 1);
assert_eq!(
serde_admission.plan_fingerprint.as_deref(),
Some(PLAN_DIGEST)
);
assert_eq!(serde_admission.theorem_result_fingerprints.len(), 1);
assert_eq!(
serde_admission.theorem_result_fingerprints[0],
THEOREM_RESULT_DIGEST
);
assert_eq!(serde_admission.evidence_digest, TRANSCRIPT_DIGEST);
let serde_admission_json =
serde_json::to_string(&serde_admission).expect("serde native admission should serialize");
assert_eq!(
serde_admission_json, canonical_admission_json,
"serde native admission struct output currently matches the fixture, but proof_assistant_native_admission_json remains the digest source"
);
let generic_admission_json = serde_json::to_string(
&serde_json::from_str::<serde_json::Value>(&canonical_admission_json)
.expect("native admission should parse as generic serde_json value"),
)
.expect("generic native admission value should serialize");
assert_ne!(
generic_admission_json, canonical_admission_json,
"generic serde_json Value native admission output is not Tokitai canonical bytes"
);
assert_ne!(
proof_replay_artifact_digest(&generic_admission_json),
proof_replay_artifact_digest(&canonical_admission_json),
"generic serde_json Value native admission output must not be a digest source"
);
let serde_admission_canonical = canonical_serde_native_admission_json(&serde_admission);
assert_eq!(serde_admission_canonical, canonical_admission_json);
assert_eq!(
proof_replay_artifact_digest(&serde_admission_canonical),
proof_replay_artifact_digest(&canonical_admission_json)
);
assert_eq!(
parse_proof_assistant_native_admission_json(&serde_admission_canonical).unwrap(),
admission
);
for field in [
"artifact",
"version",
"plan_fingerprint",
"adapter_backend",
"checker_version",
"checked_theorem_count",
"result_status",
"theorem_result_fingerprints",
"admission_claim",
"evidence_digest",
] {
assert!(
serde_admission_canonical.contains(&format!("\"{field}\":")),
"serde native admission canonical fixture should preserve field {field}"
);
}
let index = CheckerResultIndex {
plan_fingerprint: PLAN_DIGEST.to_string(),
entry_count: 1,
entries: vec![CheckerResultEntry {
theorem_id: "tokitai_replay_0".to_string(),
theorem_result_fingerprint: THEOREM_RESULT_DIGEST.to_string(),
adapter_capability_fingerprint: CAPABILITY_DIGEST.to_string(),
admission_artifact_digest: ADMISSION_DIGEST.to_string(),
plan_fingerprint: PLAN_DIGEST.to_string(),
}],
};
let canonical_index_json = checker_result_index_json(&index);
let serde_index: SerdeCheckerResultIndex = serde_json::from_str(&canonical_index_json)
.expect("checker result index JSON should parse through serde_json");
assert_eq!(
serde_index.artifact,
"tokitai-proof-assistant-checker-result-index"
);
assert_eq!(serde_index.version, 1);
assert_eq!(serde_index.plan_fingerprint, PLAN_DIGEST);
assert_eq!(serde_index.entry_count, 1);
assert_eq!(serde_index.entries.len(), 1);
assert_eq!(
serde_index.entries[0].theorem_result_fingerprint,
THEOREM_RESULT_DIGEST
);
assert_eq!(
serde_index.entries[0].adapter_capability_fingerprint,
CAPABILITY_DIGEST
);
assert_eq!(
serde_index.entries[0].admission_artifact_digest,
ADMISSION_DIGEST
);
let serde_index_json =
serde_json::to_string(&serde_index).expect("serde checker result index should serialize");
assert_eq!(
serde_index_json, canonical_index_json,
"serde checker result index struct output currently matches the fixture, but checker_result_index_json remains the digest source"
);
let generic_index_json = serde_json::to_string(
&serde_json::from_str::<serde_json::Value>(&canonical_index_json)
.expect("checker result index should parse as generic serde_json value"),
)
.expect("generic checker result index value should serialize");
assert_ne!(
generic_index_json, canonical_index_json,
"generic serde_json Value checker result index output is not Tokitai canonical bytes"
);
assert_ne!(
proof_replay_artifact_digest(&generic_index_json),
proof_replay_artifact_digest(&canonical_index_json),
"generic serde_json Value checker result index output must not be a digest source"
);
let serde_index_canonical = canonical_serde_checker_result_index_json(&serde_index);
assert_eq!(serde_index_canonical, canonical_index_json);
assert_eq!(
proof_replay_artifact_digest(&serde_index_canonical),
proof_replay_artifact_digest(&canonical_index_json)
);
assert_eq!(
parse_checker_result_index_json(&serde_index_canonical).unwrap(),
index
);
for field in [
"artifact",
"version",
"plan_fingerprint",
"entry_count",
"entries",
"theorem_id",
"theorem_result_fingerprint",
"adapter_capability_fingerprint",
"admission_artifact_digest",
] {
assert!(
serde_index_canonical.contains(&format!("\"{field}\":")),
"serde checker result index canonical fixture should preserve field {field}"
);
}
}
#[test]
fn serde_adapter_registry_fixture_preserves_capability_bytes_and_digests() {
let capability = tokitai_operator::verify::ProofAssistantAdapterCapability {
adapter_backend: "lean-skeleton".to_string(),
checker_version: "tokitai-replay-skeleton-v1".to_string(),
proof_status: "native_checked".to_string(),
native_checked: true,
admission_artifact_digest: Some(ADMISSION_DIGEST.to_string()),
};
let expected_capability_fingerprint =
proof_assistant_adapter_capability_fingerprint(&capability);
let canonical_registry_json = proof_assistant_adapter_registry_json_for_capabilities(
Some(PLAN_DIGEST),
std::slice::from_ref(&capability),
);
let serde_registry: SerdeAdapterRegistry = serde_json::from_str(&canonical_registry_json)
.expect("adapter registry JSON should parse through serde_json");
assert_eq!(
serde_registry.artifact,
"tokitai-proof-assistant-adapter-registry"
);
assert_eq!(serde_registry.version, 1);
assert_eq!(
serde_registry.plan_fingerprint.as_deref(),
Some(PLAN_DIGEST)
);
assert_eq!(serde_registry.capabilities.len(), 1);
assert_eq!(
serde_registry.capabilities[0].capability_fingerprint,
expected_capability_fingerprint
);
assert_eq!(
serde_registry.capabilities[0]
.admission_artifact_digest
.as_deref(),
Some(ADMISSION_DIGEST)
);
assert!(serde_registry.capabilities[0].native_checked);
let serde_registry_json =
serde_json::to_string(&serde_registry).expect("serde adapter registry should serialize");
assert_eq!(
serde_registry_json, canonical_registry_json,
"serde adapter registry struct output currently matches the fixture, but proof_assistant_adapter_registry_json_for_capabilities remains the digest source"
);
let generic_registry_json = serde_json::to_string(
&serde_json::from_str::<serde_json::Value>(&canonical_registry_json)
.expect("adapter registry should parse as generic serde_json value"),
)
.expect("generic adapter registry value should serialize");
assert_ne!(
generic_registry_json, canonical_registry_json,
"generic serde_json Value adapter registry output is not Tokitai canonical bytes"
);
assert_ne!(
proof_replay_artifact_digest(&generic_registry_json),
proof_replay_artifact_digest(&canonical_registry_json),
"generic serde_json Value adapter registry output must not be a digest source"
);
let serde_registry_canonical = canonical_serde_adapter_registry_json(&serde_registry);
assert_eq!(serde_registry_canonical, canonical_registry_json);
assert_eq!(
proof_replay_artifact_digest(&serde_registry_canonical),
proof_replay_artifact_digest(&canonical_registry_json)
);
assert_eq!(
parse_proof_assistant_adapter_registry_json(&serde_registry_canonical).unwrap(),
parse_proof_assistant_adapter_registry_json(&canonical_registry_json).unwrap()
);
for field in [
"artifact",
"version",
"plan_fingerprint",
"capabilities",
"adapter_backend",
"checker_version",
"proof_status",
"native_checked",
"admission_artifact_digest",
"capability_fingerprint",
] {
assert!(
serde_registry_canonical.contains(&format!("\"{field}\":")),
"serde adapter registry canonical fixture should preserve field {field}"
);
}
let null_admission_capability = proof_assistant_skeleton_adapter_capability();
let null_admission_registry_json = proof_assistant_adapter_registry_json_for_capabilities(
Some(PLAN_DIGEST),
std::slice::from_ref(&null_admission_capability),
);
let null_admission_registry: SerdeAdapterRegistry =
serde_json::from_str(&null_admission_registry_json)
.expect("adapter registry with null admission digest should parse through serde_json");
assert_eq!(
null_admission_registry.capabilities[0].admission_artifact_digest,
None
);
assert!(!null_admission_registry.capabilities[0].native_checked);
assert_eq!(
canonical_serde_adapter_registry_json(&null_admission_registry),
null_admission_registry_json
);
}
#[test]
fn serde_trace_manifest_fixture_preserves_signature_bytes_and_digests() {
let report = ProofReplayReport {
plan_fingerprint: Some(PLAN_DIGEST.to_string()),
checked_proofs: 1,
replayed_proofs: vec![ProofReplayEntry {
theorem_id: "tokitai_replay_0".to_string(),
original_id: "replay-0".to_string(),
kind: "rewrite_soundness".to_string(),
status: "proven".to_string(),
replayed: true,
replay_rule: "rewrite_soundness_replay".to_string(),
}],
warnings: Vec::new(),
};
let bundle = proof_replay_artifact_bundle("serde manifest trace", &report).unwrap();
let mut manifest = proof_replay_trace_manifest("serde manifest trace", &bundle).unwrap();
manifest.plan_fingerprint = Some(PLAN_DIGEST.to_string());
manifest.tuning = Some(ProofReplayTraceTuning {
backend: "cpu scalar".to_string(),
selected_strategy: "dense baseline".to_string(),
benchmark_count: 1,
enable_pointwise_fusion: true,
enable_padic_matmul_valuation_skip: false,
});
let adapter_capability = proof_assistant_skeleton_adapter_capability();
let registry_artifact = proof_assistant_adapter_registry_artifact_for_capabilities(
"serde manifest trace",
Some(PLAN_DIGEST),
std::slice::from_ref(&adapter_capability),
)
.unwrap();
let certificate = ProofCertificate {
version: 1,
backend: "cpu scalar".to_string(),
proofs: vec![ProofCertificateEntry {
theorem_id: "tokitai_replay_0".to_string(),
original_id: "replay-0".to_string(),
kind: "rewrite_soundness".to_string(),
status: "proven".to_string(),
claim: "serde manifest replay claim".to_string(),
obligations: Vec::new(),
evidence: vec!["semantic replay evidence".to_string()],
}],
};
let skeleton =
proof_assistant_replay_skeleton(&certificate, &report, ProofAssistantDialect::Lean)
.unwrap();
let skeleton_artifact =
proof_assistant_replay_skeleton_artifact("serde manifest trace", &skeleton).unwrap();
let summary = proof_assistant_replay_summary_with_adapter_registry(
&skeleton_artifact.filename,
&skeleton,
®istry_artifact,
)
.unwrap();
let summary =
proof_assistant_replay_summary_with_adapter_capability(&summary, &adapter_capability)
.unwrap();
manifest.artifacts.push(skeleton_artifact);
manifest.artifacts.push(registry_artifact);
manifest.proof_assistant = Some(summary);
let unsigned_manifest_json = proof_replay_trace_manifest_json(&manifest);
let signed_manifest =
sign_proof_replay_trace_manifest(&manifest, "serde manifest key", "serde-secret").unwrap();
let canonical_manifest_json = proof_replay_trace_manifest_json(&signed_manifest);
let serde_manifest: SerdeTraceManifest = serde_json::from_str(&canonical_manifest_json)
.expect("signed trace manifest JSON should parse through serde_json");
assert_eq!(
serde_manifest.artifact,
"tokitai-proof-replay-trace-manifest"
);
assert_eq!(serde_manifest.version, 1);
assert_eq!(serde_manifest.trace_name, signed_manifest.trace_name);
assert_eq!(
serde_manifest.plan_fingerprint.as_deref(),
Some(PLAN_DIGEST)
);
assert_eq!(
serde_manifest.artifacts.len(),
signed_manifest.artifacts.len()
);
assert_eq!(
serde_manifest
.proof_assistant
.as_ref()
.expect("serde manifest should include proof assistant summary")
.theorem_count,
1
);
assert_eq!(
serde_manifest.proof_assistant.as_ref().unwrap().theorems[0].adapter_capability_fingerprint,
proof_assistant_adapter_capability_fingerprint(&adapter_capability)
);
assert_eq!(
serde_manifest
.tuning
.as_ref()
.expect("serde manifest should include tuning")
.selected_strategy,
"dense baseline"
);
assert_eq!(
serde_manifest
.signature
.as_ref()
.expect("serde manifest should include signature")
.key_kind,
"shared-secret"
);
let serde_manifest_json =
serde_json::to_string(&serde_manifest).expect("serde trace manifest should serialize");
assert_eq!(
serde_manifest_json, canonical_manifest_json,
"serde trace manifest struct output currently matches the fixture, but proof_replay_trace_manifest_json remains the digest and signature source"
);
let generic_manifest_json = serde_json::to_string(
&serde_json::from_str::<serde_json::Value>(&canonical_manifest_json)
.expect("trace manifest should parse as generic serde_json value"),
)
.expect("generic trace manifest value should serialize");
assert_ne!(
generic_manifest_json, canonical_manifest_json,
"generic serde_json Value trace manifest output is not Tokitai canonical bytes"
);
assert_ne!(
proof_replay_artifact_digest(&generic_manifest_json),
proof_replay_artifact_digest(&canonical_manifest_json),
"generic serde_json Value trace manifest output must not be a digest source"
);
let serde_manifest_canonical = canonical_serde_trace_manifest_json(&serde_manifest);
assert_eq!(serde_manifest_canonical, canonical_manifest_json);
assert_eq!(
proof_replay_artifact_digest(&serde_manifest_canonical),
proof_replay_artifact_digest(&canonical_manifest_json)
);
assert_eq!(
parse_proof_replay_trace_manifest_json(&serde_manifest_canonical).unwrap(),
signed_manifest
);
verify_proof_replay_trace_manifest_signature(
&parse_proof_replay_trace_manifest_json(&serde_manifest_canonical).unwrap(),
"serde-secret",
)
.unwrap();
let mut unsigned_from_serde: SerdeTraceManifest =
serde_json::from_str(&serde_manifest_canonical)
.expect("serde canonical manifest should parse again");
unsigned_from_serde.signature = None;
assert_eq!(
canonical_serde_trace_manifest_json(&unsigned_from_serde),
unsigned_manifest_json,
"signature payload boundary must remain the canonical unsigned trace manifest bytes"
);
let mut generic_signed_manifest =
parse_proof_replay_trace_manifest_json(&generic_manifest_json).unwrap();
verify_proof_replay_trace_manifest_signature(&generic_signed_manifest, "serde-secret")
.expect("field-order-independent import should verify after canonical normalization");
generic_signed_manifest.signature = None;
assert_eq!(
proof_replay_trace_manifest_json(&generic_signed_manifest),
unsigned_manifest_json,
"generic serde_json Value output is importable, but the signature payload remains canonical unsigned manifest bytes"
);
for field in [
"artifact",
"version",
"trace_name",
"plan_fingerprint",
"artifacts",
"proof_assistant",
"tuning",
"signature",
"filename",
"digest",
"adapter_registry_digest",
"theorem_count",
"adapter_capability_fingerprint",
"selected_strategy",
"key_fingerprint",
"algorithm",
"value",
] {
assert!(
serde_manifest_canonical.contains(&format!("\"{field}\":")),
"serde trace manifest canonical fixture should preserve field {field}"
);
}
}