use std::fs;
use std::path::Path;
use std::process::Command;
use tokitai_operator::verify::{
TraceValidationFailureBroadClass, TraceValidationFailureClass, checker_result_index,
checker_result_index_artifact, checker_result_index_json, classify_trace_validation_error,
parse_math_bound_audit_trace_json, parse_proof_assistant_adapter_registry_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_json_for_capabilities, proof_assistant_checker_output,
proof_assistant_checker_output_artifact, proof_assistant_checker_output_json,
proof_assistant_checker_transcript, proof_assistant_checker_transcript_artifact,
proof_assistant_checker_transcript_json, proof_assistant_lean_checkable_artifact,
proof_assistant_lean_checkable_artifact_contents, proof_assistant_native_admission_artifact,
proof_assistant_native_admission_from_checker_output, proof_assistant_native_admission_json,
proof_assistant_native_checked_adapter_capability_from_admission,
proof_assistant_native_theorem_result_fingerprint, proof_replay_artifact_digest,
proof_replay_trace_manifest_json, verify_proof_replay_report,
verify_proof_replay_trace_directory, verify_proof_replay_trace_manifest,
verify_proof_replay_trace_manifest_signature,
};
fn assert_directory_failure_class(
artifact_dir: &Path,
class: TraceValidationFailureClass,
broad_class: TraceValidationFailureBroadClass,
) {
let error = verify_proof_replay_trace_directory(artifact_dir).unwrap_err();
let actual_class = classify_trace_validation_error(&error);
assert_eq!(actual_class, class, "unexpected validation error: {error}");
assert_eq!(actual_class.broad_class(), broad_class);
}
#[test]
fn audit_traces_example_prints_proof_replay_artifacts() {
let artifact_dir =
std::env::temp_dir().join(format!("tokitai-audit-traces-{}", std::process::id()));
let _ = fs::remove_dir_all(&artifact_dir);
let output = Command::new(env!("CARGO"))
.args(["run", "--quiet", "--example", "audit_traces"])
.env("TOKITAI_AUDIT_TRACE_DIR", &artifact_dir)
.env("TOKITAI_AUDIT_TRACE_KEY_ID", "test key")
.env("TOKITAI_AUDIT_TRACE_SECRET", "trace-secret")
.output()
.expect("audit_traces example should run");
assert!(
output.status.success(),
"audit_traces example failed: {}",
String::from_utf8_lossy(&output.stderr)
);
let stdout = String::from_utf8(output.stdout).expect("example output should be utf8");
assert!(stdout.contains("== proof replay report =="));
assert!(stdout.contains("artifact: tokitai-proof-replay-report"));
assert!(stdout.contains("version: 1"));
assert!(stdout.contains("plan fingerprint: sha256:"));
assert!(stdout.contains("proof replay: theorem=tokitai_proof_matmul_shape_0"));
assert!(stdout.contains("rule=shape_equality_replay"));
assert!(stdout.contains("== proof replay json =="));
assert!(stdout.contains("== math-bound audit =="));
assert!(stdout.contains("math-bound capability_fingerprint="));
assert!(stdout.contains("math-bound conformance_result=oracle=cpu_scalar"));
assert!(stdout.contains("\"artifact\":\"tokitai-proof-replay-report\""));
assert!(stdout.contains("\"version\":1"));
assert!(stdout.contains("\"plan_fingerprint\":\"sha256:"));
assert!(stdout.contains("\"kind\":\"shape_equality\""));
assert!(stdout.contains("\"replay_rule\":\"shape_equality_replay\""));
assert!(stdout.contains("== proof replay files =="));
assert!(stdout.contains("matmul.proof-replay.txt"));
assert!(stdout.contains("matmul.proof-replay.json"));
assert!(stdout.contains("matmul.proof-replay.lean"));
assert!(stdout.contains("matmul.proof-adapters.json"));
assert!(stdout.contains("matmul.trace-tuning.json"));
assert!(stdout.contains("matmul.trace-benchmarks.json"));
assert!(stdout.contains("matmul.math-bound-audit.json"));
assert!(stdout.contains("tokitai-trace-manifest.json"));
let replay_text = fs::read_to_string(artifact_dir.join("matmul.proof-replay.txt")).unwrap();
let replay_json = fs::read_to_string(artifact_dir.join("matmul.proof-replay.json")).unwrap();
let replay_lean = fs::read_to_string(artifact_dir.join("matmul.proof-replay.lean")).unwrap();
let adapter_registry_json =
fs::read_to_string(artifact_dir.join("matmul.proof-adapters.json")).unwrap();
let tuning_json = fs::read_to_string(artifact_dir.join("matmul.trace-tuning.json")).unwrap();
let benchmark_json =
fs::read_to_string(artifact_dir.join("matmul.trace-benchmarks.json")).unwrap();
let math_bound_json =
fs::read_to_string(artifact_dir.join("matmul.math-bound-audit.json")).unwrap();
let manifest_json =
fs::read_to_string(artifact_dir.join("tokitai-trace-manifest.json")).unwrap();
assert!(replay_text.contains("artifact: tokitai-proof-replay-report"));
assert!(replay_text.contains("plan fingerprint: sha256:"));
assert!(replay_text.contains("proof replay: theorem=tokitai_proof_matmul_shape_0"));
assert!(replay_json.contains("\"artifact\":\"tokitai-proof-replay-report\""));
assert!(replay_json.contains("\"plan_fingerprint\":\"sha256:"));
assert!(replay_json.contains("\"replay_rule\":\"shape_equality_replay\""));
assert!(replay_lean.contains("artifact: tokitai-proof-assistant-replay-skeleton"));
assert!(replay_lean.contains("dialect: lean"));
assert!(replay_lean.contains("namespace TokitaiReplay"));
assert!(replay_lean.contains("-- replay_rule: shape_equality_replay"));
assert!(replay_lean.contains("-- adapter_backend: lean-skeleton"));
assert!(replay_lean.contains("-- checker_version: tokitai-replay-skeleton-v1"));
assert!(replay_lean.contains("-- proof_status: placeholder"));
assert!(replay_lean.contains("-- adapter_capability_fingerprint: sha256:"));
assert!(replay_lean.contains("def tokitai_proof_matmul_shape_0_evidence_0 : Prop := True"));
assert!(replay_lean.contains(
"axiom tokitai_proof_matmul_shape_0 : tokitai_proof_matmul_shape_0_obligation_0"
));
assert!(replay_lean.contains("∧ tokitai_proof_matmul_shape_0_evidence_0"));
let replay_report = parse_proof_replay_report_json(&replay_json).unwrap();
verify_proof_replay_report(&replay_report).unwrap();
assert!(manifest_json.contains("\"artifact\":\"tokitai-proof-replay-trace-manifest\""));
assert!(manifest_json.contains("\"trace_name\":\"audit_traces\""));
assert!(manifest_json.contains("\"filename\":\"matmul.proof-replay.txt\""));
assert!(manifest_json.contains("\"filename\":\"matmul.proof-replay.json\""));
assert!(manifest_json.contains("\"filename\":\"matmul.proof-replay.lean\""));
assert!(manifest_json.contains("\"filename\":\"matmul.proof-adapters.json\""));
assert!(manifest_json.contains("\"filename\":\"matmul.trace-tuning.json\""));
assert!(manifest_json.contains("\"filename\":\"matmul.trace-benchmarks.json\""));
assert!(manifest_json.contains("\"filename\":\"matmul.math-bound-audit.json\""));
assert!(manifest_json.contains("\"artifact\":\"tokitai-proof-replay-trace-tuning\""));
assert!(manifest_json.contains("\"artifact\":\"tokitai-proof-replay-trace-benchmarks\""));
assert!(manifest_json.contains("\"artifact\":\"tokitai-math-bound-audit-trace\""));
assert!(manifest_json.contains("\"artifact\":\"tokitai-proof-assistant-replay-skeleton\""));
assert!(manifest_json.contains("\"artifact\":\"tokitai-proof-assistant-adapter-registry\""));
assert!(manifest_json.contains("\"proof_assistant\":{\"dialect\":\"lean\""));
assert!(manifest_json.contains("\"filename\":\"matmul.proof-replay.lean\""));
assert!(manifest_json.contains("\"adapter_registry_filename\":\"matmul.proof-adapters.json\""));
assert!(manifest_json.contains("\"adapter_registry_digest\":\"sha256:"));
assert!(manifest_json.contains("\"theorem_count\":"));
assert!(manifest_json.contains("\"theorems\":["));
assert!(manifest_json.contains("\"theorem_id\":\"tokitai_proof_matmul_shape_0\""));
assert!(manifest_json.contains("\"replay_rule\":\"shape_equality_replay\""));
assert!(manifest_json.contains("\"obligations\":["));
assert!(manifest_json.contains("\"evidence\":["));
assert!(manifest_json.contains("\"obligation_count\":"));
assert!(manifest_json.contains("\"evidence_count\":"));
assert!(manifest_json.contains("\"statement_fingerprint\":\"sha256:"));
assert!(manifest_json.contains("\"adapter_backend\":\"lean-skeleton\""));
assert!(manifest_json.contains("\"checker_version\":\"tokitai-replay-skeleton-v1\""));
assert!(manifest_json.contains("\"proof_status\":\"placeholder\""));
assert!(manifest_json.contains("\"adapter_capability_fingerprint\":\"sha256:"));
assert!(
adapter_registry_json.contains("\"artifact\":\"tokitai-proof-assistant-adapter-registry\"")
);
assert!(adapter_registry_json.contains("\"plan_fingerprint\":\"sha256:"));
assert!(adapter_registry_json.contains("\"adapter_backend\":\"lean-skeleton\""));
assert!(adapter_registry_json.contains("\"checker_version\":\"tokitai-replay-skeleton-v1\""));
assert!(adapter_registry_json.contains("\"proof_status\":\"placeholder\""));
assert!(adapter_registry_json.contains("\"capability_fingerprint\":\"sha256:"));
let adapter_registry =
parse_proof_assistant_adapter_registry_json(&adapter_registry_json).unwrap();
assert!(
adapter_registry
.plan_fingerprint
.as_ref()
.is_some_and(|fingerprint| fingerprint.starts_with("sha256:"))
);
assert_eq!(adapter_registry.capabilities.len(), 1);
assert_eq!(
adapter_registry.capabilities[0].adapter_backend,
"lean-skeleton"
);
assert!(manifest_json.contains("\"plan_fingerprint\":\"sha256:"));
assert!(manifest_json.contains("\"digest\":\"sha256:"));
assert!(manifest_json.contains("\"tuning\":{\"backend\":\"cpu_scalar\""));
assert!(manifest_json.contains("\"selected_strategy\":\"dense-baseline\""));
assert!(manifest_json.contains("\"benchmark_count\":2"));
assert!(manifest_json.contains("\"signature\":{\"key_id\":\"test_key\""));
assert!(manifest_json.contains("\"key_kind\":\"shared-secret\""));
assert!(manifest_json.contains("\"key_fingerprint\":\"sha256:"));
assert!(manifest_json.contains("\"algorithm\":\"tokitai-keyed-sha256-v1\""));
assert!(manifest_json.contains("\"value\":\"sha256:"));
let manifest = parse_proof_replay_trace_manifest_json(&manifest_json).unwrap();
verify_proof_replay_trace_manifest(&manifest).unwrap();
let math_bound_trace = parse_math_bound_audit_trace_json(&math_bound_json).unwrap();
assert_eq!(math_bound_trace.backend_id, "cpu_scalar");
assert_eq!(math_bound_trace.device_kind, "cpu");
assert!(
math_bound_trace
.capability_fingerprint
.starts_with("cachefp-")
);
assert!(
math_bound_trace
.p_adic_constraint_fingerprint
.starts_with("sha256:")
);
assert!(
math_bound_trace
.sheaf_constraint_fingerprint
.starts_with("sha256:")
);
assert!(
math_bound_trace
.lowering_rule_ids
.contains(&"cpu.matmul.dense".to_string())
);
assert!(
math_bound_trace
.conformance_result
.as_ref()
.is_some_and(|result| result.contains("candidate=gpu_scaffold"))
);
assert_eq!(
math_bound_trace.benchmark_environment.as_deref(),
Some("example:audit_traces")
);
assert_eq!(
replay_report.plan_fingerprint.as_ref(),
manifest.plan_fingerprint.as_ref()
);
assert_eq!(
adapter_registry.plan_fingerprint.as_ref(),
manifest.plan_fingerprint.as_ref()
);
let proof_assistant = manifest.proof_assistant.as_ref().unwrap();
assert_eq!(proof_assistant.dialect, "lean");
assert_eq!(
proof_assistant.plan_fingerprint.as_ref(),
manifest.plan_fingerprint.as_ref()
);
assert_eq!(proof_assistant.filename, "matmul.proof-replay.lean");
assert_eq!(
proof_assistant.adapter_registry_filename,
"matmul.proof-adapters.json"
);
assert!(
proof_assistant
.adapter_registry_digest
.starts_with("sha256:")
);
assert_eq!(proof_assistant.theorem_count, replay_report.checked_proofs);
assert_eq!(
proof_assistant.theorems.len(),
replay_report.replayed_proofs.len()
);
assert_eq!(
proof_assistant.theorems[0].theorem_id,
replay_report.replayed_proofs[0].theorem_id
);
assert_eq!(
proof_assistant.theorems[0].replay_rule,
replay_report.replayed_proofs[0].replay_rule
);
assert!(!proof_assistant.theorems[0].evidence.is_empty());
assert_eq!(
proof_assistant.theorems[0].evidence_count,
proof_assistant.theorems[0].evidence.len()
);
assert!(
proof_assistant.theorems[0]
.statement_fingerprint
.starts_with("sha256:")
);
assert_eq!(proof_assistant.theorems[0].adapter_backend, "lean-skeleton");
assert_eq!(
proof_assistant.theorems[0].checker_version,
"tokitai-replay-skeleton-v1"
);
assert_eq!(proof_assistant.theorems[0].proof_status, "placeholder");
assert!(
proof_assistant.theorems[0]
.adapter_capability_fingerprint
.starts_with("sha256:")
);
let tuning = manifest.tuning.as_ref().unwrap();
assert_eq!(tuning.backend, "cpu_scalar");
assert_eq!(tuning.selected_strategy, "dense-baseline");
assert_eq!(tuning.benchmark_count, 2);
assert!(!tuning.enable_pointwise_fusion);
assert!(!tuning.enable_padic_matmul_valuation_skip);
let tuning_artifact = parse_proof_replay_trace_tuning_json(&tuning_json).unwrap();
assert_eq!(&tuning_artifact, tuning);
let benchmark_artifact = parse_proof_replay_trace_benchmark_json(&benchmark_json).unwrap();
assert!(benchmark_artifact.plan_fingerprint.starts_with("sha256:"));
assert_eq!(
manifest.plan_fingerprint.as_ref(),
Some(&benchmark_artifact.plan_fingerprint)
);
assert_eq!(benchmark_artifact.backend, "cpu_scalar");
assert_eq!(benchmark_artifact.selected_strategy, "dense-baseline");
assert_eq!(benchmark_artifact.records.len(), 2);
assert!(
benchmark_artifact
.records
.iter()
.all(|record| record.plan_fingerprint == benchmark_artifact.plan_fingerprint)
);
verify_proof_replay_trace_manifest_signature(&manifest, "trace-secret").unwrap();
let wrong_secret_error =
verify_proof_replay_trace_manifest_signature(&manifest, "wrong-secret").unwrap_err();
let wrong_secret_class = classify_trace_validation_error(&wrong_secret_error);
assert_eq!(wrong_secret_class, TraceValidationFailureClass::Signature);
assert_eq!(
wrong_secret_class.broad_class(),
TraceValidationFailureBroadClass::Authenticity
);
let directory_manifest = verify_proof_replay_trace_directory(&artifact_dir).unwrap();
assert_eq!(directory_manifest.trace_name, "audit_traces");
let mut native_summary_for_check = manifest.proof_assistant.as_ref().unwrap().clone();
for theorem in &mut native_summary_for_check.theorems {
theorem.adapter_backend = "lean_native".to_string();
theorem.checker_version = "lean-4.15-native".to_string();
theorem.proof_status = "native_checked".to_string();
}
let checkable_contents =
proof_assistant_lean_checkable_artifact_contents(&native_summary_for_check).unwrap();
assert!(checkable_contents.contains("theorem tokitai_proof_matmul_shape_0_checkable"));
assert!(
checkable_contents.contains("selected_witness_family: shape_equality_dimension_witness_v1")
);
assert!(
checkable_contents.contains("theorem tokitai_proof_matmul_shape_0_shape_equality_witness")
);
assert!(checkable_contents.contains(" rfl"));
assert!(!checkable_contents.contains("\naxiom "));
let checkable_artifact =
proof_assistant_lean_checkable_artifact("lean-native", &checkable_contents).unwrap();
let checker_transcript = proof_assistant_checker_transcript(
manifest.plan_fingerprint.as_deref().unwrap(),
&checkable_artifact,
"lean lean-native.lean-checkable.lean",
0,
"Lean accepted",
"",
"accepted",
)
.unwrap();
let checker_transcript_artifact =
proof_assistant_checker_transcript_artifact("lean-native", &checker_transcript).unwrap();
let checker_transcript_json = proof_assistant_checker_transcript_json(&checker_transcript);
let checker_output = proof_assistant_checker_output(
manifest.plan_fingerprint.as_deref().unwrap(),
&checkable_artifact,
&checker_transcript,
"lean_native",
"lean-4.15-native",
manifest.proof_assistant.as_ref().unwrap().theorem_count,
"accepted",
)
.unwrap();
let checker_output_artifact =
proof_assistant_checker_output_artifact("lean-native", &checker_output).unwrap();
let checker_output_json = proof_assistant_checker_output_json(&checker_output);
let native_admission = proof_assistant_native_admission_from_checker_output(
&checker_output,
manifest
.proof_assistant
.as_ref()
.unwrap()
.theorems
.iter()
.map(proof_assistant_native_theorem_result_fingerprint)
.collect(),
"native Lean checker replay accepted",
)
.unwrap();
let native_admission_artifact =
proof_assistant_native_admission_artifact("lean-native", &native_admission).unwrap();
let native_admission_json = proof_assistant_native_admission_json(&native_admission);
let native_capability =
proof_assistant_native_checked_adapter_capability_from_admission(&native_admission)
.unwrap();
let native_registry_json = proof_assistant_adapter_registry_json_for_capabilities(
manifest.plan_fingerprint.as_deref(),
&[native_capability.clone()],
);
let mut native_manifest = manifest.clone();
let native_registry_digest = proof_replay_artifact_digest(&native_registry_json);
let native_registry_artifact = native_manifest
.artifacts
.iter_mut()
.find(|artifact| artifact.filename == "matmul.proof-adapters.json")
.unwrap();
native_registry_artifact.digest = native_registry_digest.clone();
native_manifest.artifacts.push(checkable_artifact.clone());
native_manifest
.artifacts
.push(checker_transcript_artifact.clone());
native_manifest
.artifacts
.push(checker_output_artifact.clone());
native_manifest
.artifacts
.push(native_admission_artifact.clone());
let native_summary = native_manifest.proof_assistant.as_mut().unwrap();
native_summary.adapter_registry_digest = native_registry_digest;
for theorem in &mut native_summary.theorems {
theorem.adapter_backend = native_capability.adapter_backend.clone();
theorem.checker_version = native_capability.checker_version.clone();
theorem.proof_status = native_capability.proof_status.clone();
theorem.adapter_capability_fingerprint =
proof_assistant_adapter_capability_fingerprint(&native_capability);
}
let native_registry =
parse_proof_assistant_adapter_registry_json(&native_registry_json).unwrap();
let checker_index = checker_result_index(
native_manifest.plan_fingerprint.as_deref().unwrap(),
native_manifest.proof_assistant.as_ref().unwrap(),
&native_registry,
)
.unwrap();
let checker_index_artifact = checker_result_index_artifact("lean-native", &checker_index)
.expect("checker result index artifact");
let checker_index_json = checker_result_index_json(&checker_index);
assert_eq!(
checker_index.entry_count,
native_admission.checked_theorem_count
);
assert_eq!(
checker_index.entries[0].theorem_result_fingerprint,
native_admission.theorem_result_fingerprints[0]
);
assert_eq!(
checker_index.entries[0].admission_artifact_digest,
native_admission_artifact.digest
);
native_manifest
.artifacts
.push(checker_index_artifact.clone());
assert!(
proof_replay_trace_manifest_json(&native_manifest)
.contains("\"artifact\":\"tokitai-proof-assistant-checker-result-index\"")
);
fs::write(
artifact_dir.join("matmul.proof-adapters.json"),
&native_registry_json,
)
.unwrap();
fs::write(
artifact_dir.join(&native_admission_artifact.filename),
&native_admission_json,
)
.unwrap();
fs::write(
artifact_dir.join(&checkable_artifact.filename),
&checkable_contents,
)
.unwrap();
fs::write(
artifact_dir.join(&checker_output_artifact.filename),
&checker_output_json,
)
.unwrap();
fs::write(
artifact_dir.join(&checker_transcript_artifact.filename),
&checker_transcript_json,
)
.unwrap();
fs::write(
artifact_dir.join(&checker_index_artifact.filename),
&checker_index_json,
)
.unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&native_manifest),
)
.unwrap();
let native_directory_manifest = verify_proof_replay_trace_directory(&artifact_dir).unwrap();
assert_eq!(
native_directory_manifest
.proof_assistant
.as_ref()
.unwrap()
.theorems[0]
.proof_status,
"native_checked"
);
let mut missing_checker_transcript_manifest = native_manifest.clone();
missing_checker_transcript_manifest
.artifacts
.retain(|artifact| artifact.artifact != "tokitai-proof-assistant-checker-transcript");
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&missing_checker_transcript_manifest),
)
.unwrap();
assert_directory_failure_class(
&artifact_dir,
TraceValidationFailureClass::Admission,
TraceValidationFailureBroadClass::Semantic,
);
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&native_manifest),
)
.unwrap();
let stale_checker_transcript_json = checker_transcript_json.replace(
&checkable_artifact.digest,
"sha256:aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa",
);
let mut stale_checker_transcript_manifest = native_manifest.clone();
let stale_checker_transcript_artifact = stale_checker_transcript_manifest
.artifacts
.iter_mut()
.find(|artifact| artifact.filename == checker_transcript_artifact.filename)
.unwrap();
stale_checker_transcript_artifact.digest =
proof_replay_artifact_digest(&stale_checker_transcript_json);
fs::write(
artifact_dir.join(&checker_transcript_artifact.filename),
stale_checker_transcript_json,
)
.unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&stale_checker_transcript_manifest),
)
.unwrap();
assert_directory_failure_class(
&artifact_dir,
TraceValidationFailureClass::Admission,
TraceValidationFailureBroadClass::Semantic,
);
fs::write(
artifact_dir.join(&checker_transcript_artifact.filename),
&checker_transcript_json,
)
.unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&native_manifest),
)
.unwrap();
let failed_checker_transcript_json =
checker_transcript_json.replace("\"exit_status\":0", "\"exit_status\":1");
let mut failed_checker_transcript_manifest = native_manifest.clone();
let failed_checker_transcript_artifact = failed_checker_transcript_manifest
.artifacts
.iter_mut()
.find(|artifact| artifact.filename == checker_transcript_artifact.filename)
.unwrap();
failed_checker_transcript_artifact.digest =
proof_replay_artifact_digest(&failed_checker_transcript_json);
fs::write(
artifact_dir.join(&checker_transcript_artifact.filename),
failed_checker_transcript_json,
)
.unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&failed_checker_transcript_manifest),
)
.unwrap();
assert_directory_failure_class(
&artifact_dir,
TraceValidationFailureClass::Admission,
TraceValidationFailureBroadClass::Semantic,
);
fs::write(
artifact_dir.join(&checker_transcript_artifact.filename),
&checker_transcript_json,
)
.unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&native_manifest),
)
.unwrap();
let mut missing_checker_index_manifest = native_manifest.clone();
missing_checker_index_manifest
.artifacts
.retain(|artifact| artifact.artifact != "tokitai-proof-assistant-checker-result-index");
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&missing_checker_index_manifest),
)
.unwrap();
assert_directory_failure_class(
&artifact_dir,
TraceValidationFailureClass::Admission,
TraceValidationFailureBroadClass::Semantic,
);
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&native_manifest),
)
.unwrap();
let wrong_index_capability_fingerprint =
"sha256:3333333333333333333333333333333333333333333333333333333333333333";
let wrong_index_capability_json = checker_index_json.replace(
&checker_index.entries[0].adapter_capability_fingerprint,
wrong_index_capability_fingerprint,
);
let mut wrong_index_capability_manifest = native_manifest.clone();
let wrong_index_capability_artifact = wrong_index_capability_manifest
.artifacts
.iter_mut()
.find(|artifact| artifact.filename == checker_index_artifact.filename)
.unwrap();
wrong_index_capability_artifact.digest =
proof_replay_artifact_digest(&wrong_index_capability_json);
fs::write(
artifact_dir.join(&checker_index_artifact.filename),
wrong_index_capability_json,
)
.unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&wrong_index_capability_manifest),
)
.unwrap();
assert_directory_failure_class(
&artifact_dir,
TraceValidationFailureClass::Admission,
TraceValidationFailureBroadClass::Semantic,
);
fs::write(
artifact_dir.join(&checker_index_artifact.filename),
&checker_index_json,
)
.unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&native_manifest),
)
.unwrap();
let wrong_index_admission_digest =
"sha256:5555555555555555555555555555555555555555555555555555555555555555";
let wrong_index_admission_json = checker_index_json.replace(
&checker_index.entries[0].admission_artifact_digest,
wrong_index_admission_digest,
);
let mut wrong_index_admission_manifest = native_manifest.clone();
let wrong_index_admission_artifact = wrong_index_admission_manifest
.artifacts
.iter_mut()
.find(|artifact| artifact.filename == checker_index_artifact.filename)
.unwrap();
wrong_index_admission_artifact.digest =
proof_replay_artifact_digest(&wrong_index_admission_json);
fs::write(
artifact_dir.join(&checker_index_artifact.filename),
wrong_index_admission_json,
)
.unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&wrong_index_admission_manifest),
)
.unwrap();
assert_directory_failure_class(
&artifact_dir,
TraceValidationFailureClass::Admission,
TraceValidationFailureBroadClass::Semantic,
);
fs::write(
artifact_dir.join(&checker_index_artifact.filename),
&checker_index_json,
)
.unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&native_manifest),
)
.unwrap();
let stale_checkable_contents = checkable_contents.replace(
"theorem tokitai_proof_matmul_shape_0_shape_equality_witness : 2 = 2",
"theorem tokitai_proof_matmul_shape_0_shape_equality_witness_changed : 2 = 2",
);
let mut stale_checkable_manifest = native_manifest.clone();
let stale_checkable_artifact = stale_checkable_manifest
.artifacts
.iter_mut()
.find(|artifact| artifact.filename == checkable_artifact.filename)
.unwrap();
stale_checkable_artifact.digest = proof_replay_artifact_digest(&stale_checkable_contents);
fs::write(
artifact_dir.join(&checkable_artifact.filename),
stale_checkable_contents,
)
.unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&stale_checkable_manifest),
)
.unwrap();
assert_directory_failure_class(
&artifact_dir,
TraceValidationFailureClass::Admission,
TraceValidationFailureBroadClass::Semantic,
);
fs::write(
artifact_dir.join(&checkable_artifact.filename),
&checkable_contents,
)
.unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&native_manifest),
)
.unwrap();
let stale_checker_output_json = checker_output_json.replace(
&checkable_artifact.digest,
"sha256:9999999999999999999999999999999999999999999999999999999999999999",
);
let mut stale_checker_output_manifest = native_manifest.clone();
let stale_checker_output_artifact = stale_checker_output_manifest
.artifacts
.iter_mut()
.find(|artifact| artifact.filename == checker_output_artifact.filename)
.unwrap();
stale_checker_output_artifact.digest = proof_replay_artifact_digest(&stale_checker_output_json);
fs::write(
artifact_dir.join(&checker_output_artifact.filename),
stale_checker_output_json,
)
.unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&stale_checker_output_manifest),
)
.unwrap();
assert_directory_failure_class(
&artifact_dir,
TraceValidationFailureClass::Admission,
TraceValidationFailureBroadClass::Semantic,
);
fs::write(
artifact_dir.join(&checker_output_artifact.filename),
&checker_output_json,
)
.unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&native_manifest),
)
.unwrap();
let wrong_native_admission_json = native_admission_json.replace(
&format!(
"\"checked_theorem_count\":{}",
native_admission.checked_theorem_count
),
&format!(
"\"checked_theorem_count\":{}",
native_admission.checked_theorem_count + 1
),
);
let wrong_admission_digest = proof_replay_artifact_digest(&wrong_native_admission_json);
let wrong_native_registry_json =
native_registry_json.replace(&native_admission_artifact.digest, &wrong_admission_digest);
let mut wrong_count_manifest = native_manifest.clone();
let wrong_registry_digest = proof_replay_artifact_digest(&wrong_native_registry_json);
let wrong_registry_artifact = wrong_count_manifest
.artifacts
.iter_mut()
.find(|artifact| artifact.filename == "matmul.proof-adapters.json")
.unwrap();
wrong_registry_artifact.digest = wrong_registry_digest.clone();
let wrong_admission_artifact = wrong_count_manifest
.artifacts
.iter_mut()
.find(|artifact| artifact.filename == native_admission_artifact.filename)
.unwrap();
wrong_admission_artifact.digest = wrong_admission_digest;
wrong_count_manifest
.proof_assistant
.as_mut()
.unwrap()
.adapter_registry_digest = wrong_registry_digest;
fs::write(
artifact_dir.join("matmul.proof-adapters.json"),
wrong_native_registry_json,
)
.unwrap();
fs::write(
artifact_dir.join(&native_admission_artifact.filename),
wrong_native_admission_json,
)
.unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&wrong_count_manifest),
)
.unwrap();
assert_directory_failure_class(
&artifact_dir,
TraceValidationFailureClass::Registry,
TraceValidationFailureBroadClass::Semantic,
);
fs::write(
artifact_dir.join("matmul.proof-adapters.json"),
&native_registry_json,
)
.unwrap();
fs::write(
artifact_dir.join(&native_admission_artifact.filename),
&native_admission_json,
)
.unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&native_manifest),
)
.unwrap();
let wrong_result_fingerprint =
"sha256:4444444444444444444444444444444444444444444444444444444444444444";
let wrong_result_admission_json = native_admission_json.replace(
&native_admission.theorem_result_fingerprints[0],
wrong_result_fingerprint,
);
let wrong_result_admission_digest = proof_replay_artifact_digest(&wrong_result_admission_json);
let wrong_result_registry_json = native_registry_json.replace(
&native_admission_artifact.digest,
&wrong_result_admission_digest,
);
let mut wrong_result_manifest = native_manifest.clone();
let wrong_result_registry_digest = proof_replay_artifact_digest(&wrong_result_registry_json);
let wrong_result_registry_artifact = wrong_result_manifest
.artifacts
.iter_mut()
.find(|artifact| artifact.filename == "matmul.proof-adapters.json")
.unwrap();
wrong_result_registry_artifact.digest = wrong_result_registry_digest.clone();
let wrong_result_admission_artifact = wrong_result_manifest
.artifacts
.iter_mut()
.find(|artifact| artifact.filename == native_admission_artifact.filename)
.unwrap();
wrong_result_admission_artifact.digest = wrong_result_admission_digest;
wrong_result_manifest
.proof_assistant
.as_mut()
.unwrap()
.adapter_registry_digest = wrong_result_registry_digest;
fs::write(
artifact_dir.join("matmul.proof-adapters.json"),
wrong_result_registry_json,
)
.unwrap();
fs::write(
artifact_dir.join(&native_admission_artifact.filename),
wrong_result_admission_json,
)
.unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&wrong_result_manifest),
)
.unwrap();
assert_directory_failure_class(
&artifact_dir,
TraceValidationFailureClass::Registry,
TraceValidationFailureBroadClass::Semantic,
);
fs::write(
artifact_dir.join("matmul.proof-adapters.json"),
&native_registry_json,
)
.unwrap();
fs::write(
artifact_dir.join(&native_admission_artifact.filename),
&native_admission_json,
)
.unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&native_manifest),
)
.unwrap();
let mut missing_admission_manifest = native_manifest.clone();
missing_admission_manifest
.artifacts
.retain(|artifact| artifact.artifact != "tokitai-proof-assistant-native-admission");
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&missing_admission_manifest),
)
.unwrap();
assert!(verify_proof_replay_trace_directory(&artifact_dir).is_err());
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&native_manifest),
)
.unwrap();
fs::write(
artifact_dir.join(&native_admission_artifact.filename),
native_admission_json.replace(
"native Lean checker replay accepted",
"native Lean checker replay changed",
),
)
.unwrap();
assert!(verify_proof_replay_trace_directory(&artifact_dir).is_err());
fs::write(
artifact_dir.join(&native_admission_artifact.filename),
&native_admission_json,
)
.unwrap();
fs::write(
artifact_dir.join("matmul.proof-adapters.json"),
&adapter_registry_json,
)
.unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&native_manifest),
)
.unwrap();
assert!(verify_proof_replay_trace_directory(&artifact_dir).is_err());
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
&manifest_json,
)
.unwrap();
let wrong_registry_json = adapter_registry_json.replace(
"\"checker_version\":\"tokitai-replay-skeleton-v1\"",
"\"checker_version\":\"lean-unknown\"",
);
let mut registry_tampered_manifest = manifest.clone();
let registry_artifact = registry_tampered_manifest
.artifacts
.iter_mut()
.find(|artifact| artifact.filename == "matmul.proof-adapters.json")
.unwrap();
registry_artifact.digest = proof_replay_artifact_digest(&wrong_registry_json);
fs::write(
artifact_dir.join("matmul.proof-adapters.json"),
wrong_registry_json,
)
.unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(®istry_tampered_manifest),
)
.unwrap();
assert!(verify_proof_replay_trace_directory(&artifact_dir).is_err());
fs::write(
artifact_dir.join("matmul.proof-adapters.json"),
&adapter_registry_json,
)
.unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
&manifest_json,
)
.unwrap();
let manifest_fingerprint = manifest.plan_fingerprint.as_ref().unwrap();
let wrong_fingerprint =
"sha256:0000000000000000000000000000000000000000000000000000000000000000";
let wrong_registry_fingerprint_json =
adapter_registry_json.replace(manifest_fingerprint, wrong_fingerprint);
let mut registry_fingerprint_tampered_manifest = manifest.clone();
let registry_artifact = registry_fingerprint_tampered_manifest
.artifacts
.iter_mut()
.find(|artifact| artifact.filename == "matmul.proof-adapters.json")
.unwrap();
registry_artifact.digest = proof_replay_artifact_digest(&wrong_registry_fingerprint_json);
registry_fingerprint_tampered_manifest
.proof_assistant
.as_mut()
.unwrap()
.adapter_registry_digest = registry_artifact.digest.clone();
fs::write(
artifact_dir.join("matmul.proof-adapters.json"),
wrong_registry_fingerprint_json,
)
.unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(®istry_fingerprint_tampered_manifest),
)
.unwrap();
assert!(verify_proof_replay_trace_directory(&artifact_dir).is_err());
fs::write(
artifact_dir.join("matmul.proof-adapters.json"),
&adapter_registry_json,
)
.unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
&manifest_json,
)
.unwrap();
let wrong_capability_fingerprint =
"sha256:1111111111111111111111111111111111111111111111111111111111111111";
let wrong_registry_capability_json = adapter_registry_json.replace(
adapter_registry
.capabilities
.iter()
.map(tokitai_operator::verify::proof_assistant_adapter_capability_fingerprint)
.next()
.unwrap()
.as_str(),
wrong_capability_fingerprint,
);
let mut registry_capability_tampered_manifest = manifest.clone();
let registry_artifact = registry_capability_tampered_manifest
.artifacts
.iter_mut()
.find(|artifact| artifact.filename == "matmul.proof-adapters.json")
.unwrap();
registry_artifact.digest = proof_replay_artifact_digest(&wrong_registry_capability_json);
registry_capability_tampered_manifest
.proof_assistant
.as_mut()
.unwrap()
.adapter_registry_digest = registry_artifact.digest.clone();
fs::write(
artifact_dir.join("matmul.proof-adapters.json"),
wrong_registry_capability_json,
)
.unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(®istry_capability_tampered_manifest),
)
.unwrap();
assert!(verify_proof_replay_trace_directory(&artifact_dir).is_err());
fs::write(
artifact_dir.join("matmul.proof-adapters.json"),
&adapter_registry_json,
)
.unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
&manifest_json,
)
.unwrap();
let mut registry_binding_tampered_manifest = manifest.clone();
registry_binding_tampered_manifest
.proof_assistant
.as_mut()
.unwrap()
.adapter_registry_digest =
"sha256:0000000000000000000000000000000000000000000000000000000000000000".to_string();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(®istry_binding_tampered_manifest),
)
.unwrap();
assert!(verify_proof_replay_trace_directory(&artifact_dir).is_err());
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
&manifest_json,
)
.unwrap();
fs::write(
artifact_dir.join("matmul.proof-replay.json"),
replay_json.replace("shape_equality_replay", "rewrite_soundness_replay"),
)
.unwrap();
assert!(verify_proof_replay_trace_directory(&artifact_dir).is_err());
fs::write(artifact_dir.join("matmul.proof-replay.json"), replay_json).unwrap();
let mut summary_tampered_manifest = manifest.clone();
summary_tampered_manifest
.proof_assistant
.as_mut()
.unwrap()
.theorem_count += 1;
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&summary_tampered_manifest),
)
.unwrap();
assert!(verify_proof_replay_trace_directory(&artifact_dir).is_err());
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
&manifest_json,
)
.unwrap();
let mut theorem_index_tampered_manifest = manifest.clone();
theorem_index_tampered_manifest
.proof_assistant
.as_mut()
.unwrap()
.theorems[0]
.replay_rule = "rewrite_soundness_replay".to_string();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&theorem_index_tampered_manifest),
)
.unwrap();
assert!(verify_proof_replay_trace_directory(&artifact_dir).is_err());
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
&manifest_json,
)
.unwrap();
let mut theorem_evidence_tampered_manifest = manifest.clone();
theorem_evidence_tampered_manifest
.proof_assistant
.as_mut()
.unwrap()
.theorems[0]
.evidence
.clear();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&theorem_evidence_tampered_manifest),
)
.unwrap();
assert!(verify_proof_replay_trace_directory(&artifact_dir).is_err());
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
&manifest_json,
)
.unwrap();
let mut theorem_count_tampered_manifest = manifest.clone();
theorem_count_tampered_manifest
.proof_assistant
.as_mut()
.unwrap()
.theorems[0]
.evidence_count += 1;
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&theorem_count_tampered_manifest),
)
.unwrap();
assert!(verify_proof_replay_trace_directory(&artifact_dir).is_err());
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
&manifest_json,
)
.unwrap();
let mut theorem_statement_fingerprint_tampered_manifest = manifest.clone();
theorem_statement_fingerprint_tampered_manifest
.proof_assistant
.as_mut()
.unwrap()
.theorems[0]
.statement_fingerprint =
"sha256:0000000000000000000000000000000000000000000000000000000000000000".to_string();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&theorem_statement_fingerprint_tampered_manifest),
)
.unwrap();
assert!(verify_proof_replay_trace_directory(&artifact_dir).is_err());
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
&manifest_json,
)
.unwrap();
let mut theorem_adapter_tampered_manifest = manifest.clone();
theorem_adapter_tampered_manifest
.proof_assistant
.as_mut()
.unwrap()
.theorems[0]
.proof_status = "native_checked".to_string();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&theorem_adapter_tampered_manifest),
)
.unwrap();
assert!(verify_proof_replay_trace_directory(&artifact_dir).is_err());
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
&manifest_json,
)
.unwrap();
let mut theorem_checker_tampered_manifest = manifest.clone();
theorem_checker_tampered_manifest
.proof_assistant
.as_mut()
.unwrap()
.theorems[0]
.checker_version = "lean-unknown".to_string();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&theorem_checker_tampered_manifest),
)
.unwrap();
assert!(verify_proof_replay_trace_directory(&artifact_dir).is_err());
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
&manifest_json,
)
.unwrap();
let mut theorem_capability_tampered_manifest = manifest.clone();
theorem_capability_tampered_manifest
.proof_assistant
.as_mut()
.unwrap()
.theorems[0]
.adapter_capability_fingerprint =
"sha256:2222222222222222222222222222222222222222222222222222222222222222".to_string();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&theorem_capability_tampered_manifest),
)
.unwrap();
assert!(verify_proof_replay_trace_directory(&artifact_dir).is_err());
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
&manifest_json,
)
.unwrap();
let mut summary_filename_tampered_manifest = manifest.clone();
summary_filename_tampered_manifest
.proof_assistant
.as_mut()
.unwrap()
.filename = "other.proof-replay.lean".to_string();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&summary_filename_tampered_manifest),
)
.unwrap();
assert!(verify_proof_replay_trace_directory(&artifact_dir).is_err());
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
&manifest_json,
)
.unwrap();
let wrong_fingerprint_lean = replay_lean.replace(manifest_fingerprint, wrong_fingerprint);
let mut fingerprint_tampered_manifest = manifest.clone();
let lean_artifact = fingerprint_tampered_manifest
.artifacts
.iter_mut()
.find(|artifact| artifact.filename == "matmul.proof-replay.lean")
.unwrap();
lean_artifact.digest = proof_replay_artifact_digest(&wrong_fingerprint_lean);
fs::write(
artifact_dir.join("matmul.proof-replay.lean"),
wrong_fingerprint_lean,
)
.unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&fingerprint_tampered_manifest),
)
.unwrap();
assert!(verify_proof_replay_trace_directory(&artifact_dir).is_err());
fs::write(artifact_dir.join("matmul.proof-replay.lean"), &replay_lean).unwrap();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
&manifest_json,
)
.unwrap();
fs::write(
artifact_dir.join("matmul.proof-replay.lean"),
replay_lean.replace("dialect: lean", "dialect: bad"),
)
.unwrap();
assert!(verify_proof_replay_trace_directory(&artifact_dir).is_err());
fs::write(artifact_dir.join("matmul.proof-replay.lean"), &replay_lean).unwrap();
fs::write(
artifact_dir.join("matmul.proof-replay.lean"),
replay_lean.replace(
"axiom tokitai_proof_matmul_shape_0 : tokitai_proof_matmul_shape_0_obligation_0 ∧ tokitai_proof_matmul_shape_0_obligation_1 ∧ tokitai_proof_matmul_shape_0_evidence_0",
"axiom tokitai_proof_matmul_shape_0 : True",
),
)
.unwrap();
assert!(verify_proof_replay_trace_directory(&artifact_dir).is_err());
fs::write(artifact_dir.join("matmul.proof-replay.lean"), replay_lean).unwrap();
fs::write(
artifact_dir.join("matmul.trace-tuning.json"),
tuning_json.replace("\"benchmark_count\":2", "\"benchmark_count\":3"),
)
.unwrap();
assert!(verify_proof_replay_trace_directory(&artifact_dir).is_err());
fs::write(artifact_dir.join("matmul.trace-tuning.json"), tuning_json).unwrap();
fs::write(
artifact_dir.join("matmul.trace-benchmarks.json"),
benchmark_json.replace("\"duration_ns\":10", "\"duration_ns\":99"),
)
.unwrap();
assert!(verify_proof_replay_trace_directory(&artifact_dir).is_err());
fs::write(
artifact_dir.join("matmul.trace-benchmarks.json"),
benchmark_json.replacen("sha256:", "sha256:bad", 1),
)
.unwrap();
assert!(verify_proof_replay_trace_directory(&artifact_dir).is_err());
fs::write(
artifact_dir.join("matmul.trace-benchmarks.json"),
benchmark_json,
)
.unwrap();
let mut format_tampered_manifest = manifest.clone();
let json_artifact = format_tampered_manifest
.artifacts
.iter_mut()
.find(|artifact| artifact.filename == "matmul.proof-replay.json")
.unwrap();
json_artifact.format = "text".to_string();
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
proof_replay_trace_manifest_json(&format_tampered_manifest),
)
.unwrap();
assert!(verify_proof_replay_trace_directory(&artifact_dir).is_err());
fs::write(
artifact_dir.join("tokitai-trace-manifest.json"),
manifest_json,
)
.unwrap();
fs::remove_file(artifact_dir.join("matmul.proof-replay.json")).unwrap();
assert!(verify_proof_replay_trace_directory(&artifact_dir).is_err());
fs::remove_dir_all(artifact_dir).unwrap();
}