tokitai-operator 0.1.0

//! Verification surface: `audit_report`, release gate, claim status.
//!
//! This module is the source-of-truth for the paper claim boundary.
//! It exposes:
//!
//! - `audit_report(plan)` — the per-plan evidence summary consumed
//!   by the release-gate tests and the `audit_traces` example.
//! - `release_gate` — the 9+ checks that must pass before the
//!   primary claim is allowed.
//! - `claim_status` — parsing and validation of the 8
//!   `*_claim_allowed` flags in `CLAIMS.md`.
//! - `support_matrix` — the public surface index.
//! - `semantic_conformance` — the conformance report joining CPU
//!   oracle, property-check, theorem-binding, fallback, and
//!   math-bound audit-trace evidence.
//! - `theorems` / `properties` / `novelty` — the
//!   theorem-binding registry, property-based tests, and the
//!   first-of-kind novelty dossier.
//!
//! Public types: `VerificationReport`, `Obligation`,
//! `TheorySupportMatrix`, `ClaimStatusBlock`, `RocmBenchmarkReport`,
//! `HipAuditReport`.
//!
//! Claim-boundary: do not edit any function whose name starts with
//! `validate_` or `check_` without updating `CLAIMS.md`.
//!
pub mod audit_registry;
pub mod claim_status;
pub mod cover_glue_inference;
pub mod equality;
#[cfg(feature = "rocm-hip")]
pub mod hip_audit;
pub mod novelty;
pub mod proof_replay_witnesses;
pub mod properties;
pub mod release_gate;
#[cfg(feature = "rocm-hip")]
pub mod rocm_benchmarks;
pub mod samples;
pub mod semantic_conformance;
pub mod support_matrix;
pub mod support_matrix_dedup_classify;
pub mod theorems;
pub mod witnesses;

use std::path::Path;

pub use audit_registry::{audit_report_with_registry, registered_lowering_rules_section};
pub use claim_status::{
    CLAIM_STATUS_BLOCK, StatusBlock, StatusBlockExpectation, VALIDATION_STATUS_BLOCK,
    current_claim_status_expectation, current_validation_status_expectation,
    p268_claim_status_expectation, p268_validation_status_expectation, parse_status_block,
    validate_claim_status_block, validate_status_block, validate_validation_status_block,
};
pub use cover_glue_inference::{
    CoverGlueInferenceReport, InferenceAttempt, cover_glue_inference_report,
    infer_missing_sections, resolve_overlap_attempt,
};
pub use proof_replay_witnesses::{proof_replay_cover_glue_section, proof_replay_witnesses_section};
pub use support_matrix_dedup_classify::{
    ClassifiedDup, DupKind, classify_dup, matrix_dedup_summary,
};

#[cfg(feature = "rocm-hip")]
pub use hip_audit::{
    HIP_AUDIT_REPORT_ARTIFACT, HIP_AUDIT_REPORT_VERSION, HipAuditReport, HipAuditTrace,
    generate_hip_audit_report, hip_audit_report_from_padic_stratified_benchmarks,
    hip_audit_report_from_rocm_benchmarks, validate_hip_audit_report,
};

pub use novelty::{
    NOVELTY_DOSSIER_DOC, NoveltyEvidenceEntry, first_of_kind_evidence_dossier,
    validate_first_of_kind_evidence_dossier,
};

pub use properties::{
    PropertyCheckReport, check_padic_contract_properties,
    check_padic_contract_properties_with_samples, check_sheaf_contract_properties,
    ensure_all_properties_pass,
};

pub use release_gate::{
    ReleaseGateCheck, THEORY_ENGINEERING_RELEASE_GATE_ARTIFACT,
    THEORY_ENGINEERING_RELEASE_GATE_VERSION, TheoryEngineeringReleaseGateReport,
    check_certified_padic_gemm_claim_gate, run_theory_engineering_release_gate,
    theory_engineering_release_gate_from_parts,
};

#[cfg(feature = "rocm-hip")]
pub use release_gate::{check_hip_audit_report, check_padic_stratified_benchmark_report};

#[cfg(feature = "rocm-hip")]
pub use rocm_benchmarks::{
    ROCM_BENCHMARK_REPORT_ARTIFACT, ROCM_BENCHMARK_REPORT_VERSION, RocmBenchmarkReport,
    RocmBenchmarkRow, generate_rocm_benchmark_report,
};

pub use samples::{BinarySampleSet, PadicSampleGenerator, PadicSampleProfile, SampleSet};
pub use witnesses::{
    PrecisionPreservationWitness, UltrametricWitness, ValuationAdditivityWitness, WitnessSample,
};

pub use semantic_conformance::{
    SEMANTIC_CONFORMANCE_REPORT_ARTIFACT, SEMANTIC_CONFORMANCE_REPORT_VERSION,
    SemanticConformanceReport, SemanticConformanceStatus, TheoryConformanceStatus,
    semantic_conformance_report, semantic_conformance_report_from_parts,
};

pub use support_matrix::{
    SupportStatus, THEORY_SUPPORT_MATRIX_ARTIFACT, THEORY_SUPPORT_MATRIX_VERSION,
    TheorySupportMatrix, TheorySupportMatrixRow, generated_theory_support_matrix,
    theory_support_matrix_from_sources,
};

pub use theorems::{
    CheckerTranscript, CheckerTranscriptStatus, FINITE_SHEAF_GLUING_LEAN_FILE,
    FINITE_SHEAF_GLUING_THEOREM_ID, FINITE_SHEAF_GLUING_TRANSCRIPT_FILE,
    FINITE_SHEAF_OBSTRUCTION_THEOREM_ID, FiniteSheafGluingTheoremBinding,
    PADIC_VALUATION_DOT_PRODUCT_THEOREM_ID, PADIC_VALUATION_MATRIX_OUTPUT_THEOREM_ID,
    PADIC_VALUATION_SKIP_LEAN_FILE, PADIC_VALUATION_SKIP_THEOREM_ID,
    PADIC_VALUATION_SKIP_TRANSCRIPT_FILE, PadicValuationSkipTheoremBinding,
    PadicValuationStratifiedMatmulTheoremBinding, RuntimeTheoremBinding, TheoremBindingDescriptor,
    TheoremBindingRegistry, TheoremRuntimeRequirement, finite_sheaf_gluing_theorem_binding,
    finite_sheaf_gluing_theorem_binding_report, padic_valuation_skip_theorem_binding,
    padic_valuation_skip_theorem_binding_report, padic_valuation_stratified_matmul_theorem_binding,
    padic_valuation_stratified_matmul_theorem_binding_report,
};

use crate::backend::TensorStore;
use crate::backend::conformance::BackendConformanceRunReport;
use crate::backend::cpu::CpuScalarBackend;
use crate::domain::{Padic, PadicDomain};
use crate::ir::SemanticGraph;
use crate::object::Tensor;
use crate::object::sheaf::{Cover, FiniteSite, OpenId, Section, SectionTable};
use crate::planner::{
    BenchmarkRecord, DischargeStatus, ExecutionPlan, ObligationSeverity, ObligationSource,
    PlanCacheKey, PlanStep, PlanStepKind, ProofKind, ProofObject, ProofStatus, TuningTraceSummary,
};
use crate::{Error, Result};
#[cfg(feature = "ed25519")]
use ed25519_dalek::{Signature, Signer, Verifier, VerifyingKey};
use equality::{EqualityMode, padic_equal_at_precision};

pub const PROOF_REPLAY_REPORT_ARTIFACT: &str = "tokitai-proof-replay-report";
pub const PROOF_REPLAY_REPORT_VERSION: u32 = 1;
pub const PROOF_REPLAY_TRACE_MANIFEST_ARTIFACT: &str = "tokitai-proof-replay-trace-manifest";
pub const PROOF_REPLAY_TRACE_MANIFEST_VERSION: u32 = 1;
pub const PROOF_REPLAY_TRACE_TUNING_ARTIFACT: &str = "tokitai-proof-replay-trace-tuning";
pub const PROOF_REPLAY_TRACE_TUNING_VERSION: u32 = 1;
pub const PROOF_REPLAY_TRACE_BENCHMARK_ARTIFACT: &str = "tokitai-proof-replay-trace-benchmarks";
pub const PROOF_REPLAY_TRACE_BENCHMARK_VERSION: u32 = 1;
pub const MATH_BOUND_AUDIT_TRACE_ARTIFACT: &str = "tokitai-math-bound-audit-trace";
pub const MATH_BOUND_AUDIT_TRACE_VERSION: u32 = 1;
pub const PROOF_REPLAY_TRACE_SIGNATURE_ALGORITHM: &str = "tokitai-keyed-sha256-v1";
pub const PROOF_REPLAY_TRACE_PUBLIC_KEY_SIGNATURE_ALGORITHM: &str = "ed25519-v1";
pub const PROOF_ASSISTANT_REPLAY_SKELETON_ARTIFACT: &str =
    "tokitai-proof-assistant-replay-skeleton";
pub const PROOF_ASSISTANT_REPLAY_SKELETON_VERSION: u32 = 1;
pub const PROOF_ASSISTANT_LEAN_CHECKABLE_ARTIFACT: &str = "tokitai-proof-assistant-lean-checkable";
pub const PROOF_ASSISTANT_LEAN_CHECKABLE_VERSION: u32 = 1;
pub const PROOF_ASSISTANT_CHECKER_TRANSCRIPT_ARTIFACT: &str =
    "tokitai-proof-assistant-checker-transcript";
pub const PROOF_ASSISTANT_CHECKER_TRANSCRIPT_VERSION: u32 = 1;
pub const PROOF_ASSISTANT_CHECKER_OUTPUT_ARTIFACT: &str = "tokitai-proof-assistant-checker-output";
pub const PROOF_ASSISTANT_CHECKER_OUTPUT_VERSION: u32 = 1;
pub const PROOF_ASSISTANT_ADAPTER_REGISTRY_ARTIFACT: &str =
    "tokitai-proof-assistant-adapter-registry";
pub const PROOF_ASSISTANT_ADAPTER_REGISTRY_VERSION: u32 = 1;
pub const PROOF_ASSISTANT_NATIVE_ADMISSION_ARTIFACT: &str =
    "tokitai-proof-assistant-native-admission";
pub const PROOF_ASSISTANT_NATIVE_ADMISSION_VERSION: u32 = 1;
pub const PROOF_ASSISTANT_CHECKER_RESULT_INDEX_ARTIFACT: &str =
    "tokitai-proof-assistant-checker-result-index";
pub const PROOF_ASSISTANT_CHECKER_RESULT_INDEX_VERSION: u32 = 1;
pub const PAPER_BENCHMARK_RESULTS_ARTIFACT: &str = "tokitai-paper-benchmark-results";
pub const THEORY_SUPPORT_MATRIX_SCHEMA_FIELDS: &[&str] = &["artifact", "version", "rows"];
pub const THEORY_SUPPORT_MATRIX_ROW_SCHEMA_FIELDS: &[&str] = &[
    "domain",
    "operator",
    "theory_constraints",
    "theorem_packages",
    "backend",
    "backend_capability",
    "lowering_rule_id",
    "support_status",
    "fallback_mode",
    "public_api",
    "tests",
    "non_claims",
];
pub const PADIC_STRATIFIED_BENCHMARK_REPORT_ARTIFACT: &str =
    "tokitai-padic-stratified-matmul-benchmark-report";
pub const PADIC_STRATIFIED_BENCHMARK_REPORT_SCHEMA_FIELDS: &[&str] = &[
    "artifact",
    "version",
    "warmup_runs",
    "measured_runs",
    "speed_claim_policy",
    "rows",
    "fixtures",
    "non_claims",
];
pub const PADIC_STRATIFIED_BENCHMARK_ROW_SCHEMA_FIELDS: &[&str] = &[
    "fixture",
    "distribution",
    "backend",
    "status",
    "shape",
    "prime",
    "precision",
    "skipped_products",
    "evaluated_products",
    "precision_margin_min",
    "dense_cpu_oracle_matches",
    "sparse_cpu_oracle_matches",
    "certificate_coverage",
    "output_residue_fingerprint",
    "device_fingerprint",
    "kernel_source_fingerprint",
    "compiler_fingerprint",
    "transfer_time_ns",
    "kernel_time_ns",
    "wall_clock_ns",
    "warmup_runs",
    "measured_runs",
    "transfer_time_min_ns",
    "transfer_time_median_ns",
    "transfer_time_max_ns",
    "kernel_time_min_ns",
    "kernel_time_median_ns",
    "kernel_time_max_ns",
    "wall_clock_min_ns",
    "wall_clock_median_ns",
    "wall_clock_max_ns",
    "timing_scope",
    "external_baseline_kind",
    "external_baseline_source",
    "external_baseline_wall_clock_ns",
    "profiler_tool",
    "profiler_trace_status",
    "profiler_kernel_time_ns",
    "speedup_evidence_status",
    "fallback_reason",
    "speed_claim_allowed",
    "speed_claim_blocker",
];
pub const PADIC_STRATIFIED_BENCHMARK_FIXTURE_SCHEMA_FIELDS: &[&str] = &[
    "name",
    "distribution",
    "shape",
    "prime",
    "precision",
    "lhs_bucket_fingerprint",
    "rhs_bucket_fingerprint",
    "lhs_valuation_histogram",
    "rhs_valuation_histogram",
];
pub const THEORY_ENGINEERING_RELEASE_GATE_SCHEMA_FIELDS: &[&str] = &[
    "artifact",
    "version",
    "passed",
    "checks",
    "required_commands",
    "deferred_work",
    "known_limits",
];
pub const PROOF_ASSISTANT_REPLAY_ADAPTER_BACKEND: &str = "lean-skeleton";
pub const PROOF_ASSISTANT_REPLAY_CHECKER_VERSION: &str = "tokitai-replay-skeleton-v1";
pub const PROOF_ASSISTANT_REPLAY_PROOF_STATUS: &str = "placeholder";
pub const PROOF_ASSISTANT_SELECTED_WITNESS_FAMILY: &str = "shape_equality_dimension_witness_v1";
pub const PROOF_ASSISTANT_SELECTED_NONSTANDARD_WITNESS_FAMILY: &str =
    "padic_precision_cutoff_witness_v1";

pub const PROOF_REPLAY_TRACE_MANIFEST_SCHEMA_FIELDS: &[&str] = &[
    "artifact",
    "version",
    "trace_name",
    "plan_fingerprint",
    "artifacts",
    "proof_assistant",
    "tuning",
    "signature",
];
const PROOF_REPLAY_TRACE_ARTIFACT_SCHEMA_FIELDS: &[&str] =
    &["filename", "artifact", "version", "format", "digest"];
const PROOF_ASSISTANT_REPLAY_SUMMARY_SCHEMA_FIELDS: &[&str] = &[
    "dialect",
    "plan_fingerprint",
    "filename",
    "adapter_registry_filename",
    "adapter_registry_digest",
    "theorem_count",
    "theorems",
];
const PROOF_ASSISTANT_REPLAY_THEOREM_SUMMARY_SCHEMA_FIELDS: &[&str] = &[
    "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",
];
const PROOF_REPLAY_TRACE_SIGNATURE_SCHEMA_FIELDS: &[&str] = &[
    "key_id",
    "key_kind",
    "key_fingerprint",
    "algorithm",
    "value",
];
pub const PROOF_REPLAY_REPORT_SCHEMA_FIELDS: &[&str] = &[
    "artifact",
    "version",
    "plan_fingerprint",
    "checked_proofs",
    "replayed_proofs",
    "warnings",
];
const PROOF_REPLAY_ENTRY_SCHEMA_FIELDS: &[&str] = &[
    "theorem_id",
    "original_id",
    "kind",
    "status",
    "replayed",
    "replay_rule",
];
pub const PROOF_ASSISTANT_ADAPTER_REGISTRY_SCHEMA_FIELDS: &[&str] =
    &["artifact", "version", "plan_fingerprint", "capabilities"];
const PROOF_ASSISTANT_ADAPTER_CAPABILITY_SCHEMA_FIELDS: &[&str] = &[
    "adapter_backend",
    "checker_version",
    "proof_status",
    "native_checked",
    "admission_artifact_digest",
    "capability_fingerprint",
];
pub const PROOF_ASSISTANT_LEAN_CHECKABLE_SCHEMA_FIELDS: &[&str] = &[
    "artifact",
    "version",
    "dialect",
    "plan_fingerprint",
    "checker_command",
    "selected_witness_family",
    "selected_nonstandard_witness_family",
    "selected_shape_witness_count",
    "selected_padic_witness_count",
];
pub const PROOF_ASSISTANT_CHECKER_TRANSCRIPT_SCHEMA_FIELDS: &[&str] = &[
    "artifact",
    "version",
    "plan_fingerprint",
    "checker_command",
    "artifact_filename",
    "artifact_digest",
    "exit_status",
    "stdout_digest",
    "stderr_digest",
    "result_status",
];
pub const PROOF_ASSISTANT_CHECKER_OUTPUT_SCHEMA_FIELDS: &[&str] = &[
    "artifact",
    "version",
    "plan_fingerprint",
    "artifact_filename",
    "artifact_digest",
    "transcript_digest",
    "adapter_backend",
    "checker_version",
    "checked_theorem_count",
    "result_status",
];
pub const PROOF_ASSISTANT_NATIVE_ADMISSION_SCHEMA_FIELDS: &[&str] = &[
    "artifact",
    "version",
    "plan_fingerprint",
    "adapter_backend",
    "checker_version",
    "checked_theorem_count",
    "result_status",
    "theorem_result_fingerprints",
    "admission_claim",
    "evidence_digest",
];
pub const PROOF_ASSISTANT_CHECKER_RESULT_INDEX_SCHEMA_FIELDS: &[&str] = &[
    "artifact",
    "version",
    "plan_fingerprint",
    "entry_count",
    "entries",
];
const PROOF_ASSISTANT_CHECKER_RESULT_ENTRY_SCHEMA_FIELDS: &[&str] = &[
    "theorem_id",
    "theorem_result_fingerprint",
    "adapter_capability_fingerprint",
    "admission_artifact_digest",
    "plan_fingerprint",
];
pub const PROOF_REPLAY_TRACE_TUNING_SCHEMA_FIELDS: &[&str] = &[
    "artifact",
    "version",
    "backend",
    "selected_strategy",
    "benchmark_count",
    "enable_pointwise_fusion",
    "enable_padic_matmul_valuation_skip",
];
pub const PROOF_REPLAY_TRACE_BENCHMARK_SCHEMA_FIELDS: &[&str] = &[
    "artifact",
    "version",
    "plan_fingerprint",
    "backend",
    "selected_strategy",
    "records",
];
pub const MATH_BOUND_AUDIT_TRACE_SCHEMA_FIELDS: &[&str] = &[
    "artifact",
    "version",
    "plan_fingerprint",
    "backend_id",
    "device_kind",
    "capability_fingerprint",
    "p_adic_constraint_fingerprint",
    "sheaf_constraint_fingerprint",
    "lowering_rule_ids",
    "fallback_reason",
    "conformance_result",
    "benchmark_environment",
];
const PROOF_REPLAY_TRACE_BENCHMARK_RECORD_SCHEMA_FIELDS: &[&str] = &[
    "plan_fingerprint",
    "backend",
    "strategy",
    "input_description",
    "duration_ns",
];
pub const PAPER_BENCHMARK_RESULTS_SCHEMA_FIELDS: &[&str] = &[
    "artifact",
    "version",
    "workloads",
    "measurements",
    "baseline_comparisons",
    "evidence_matrix",
    "ablations",
    "claims",
    "trace_architecture",
    "witness_metadata",
];
pub const PAPER_RESULTS_CSV_HEADER: &str = "name,reference_duration_ns,optimized_duration_ns,proof_trace_validation_ns,plan_steps,proof_objects,checked_proofs,domain_metric";
pub const MEASUREMENT_SUMMARY_CSV_HEADER: &str =
    "name,measurement_kind,runs,min_ns,median_ns,max_ns,notes";
pub const BASELINE_SCALE_COMPARISON_CSV_HEADER: &str = "family,workload,scale_point,baseline_kind,baseline_ns,candidate_kind,candidate_ns,proof_overhead_ns,ratio_milli,interpretation";
pub const APPLICATION_EVIDENCE_MATRIX_CSV_HEADER: &str = "axis,workload,backend_id,candidate_backend,capability_fingerprint,p_adic_constraint_fingerprint,sheaf_constraint_fingerprint,correctness_evidence,speed_evidence,fallback_rate,conformance_status,precision_or_locality,proof_evidence";
pub const TAMPER_MATRIX_CSV_HEADER: &str = "tamper_class,no_proof_detected,digest_only_detected,count_only_detected,per_theorem_index_detected";
pub const CLAIM_TO_TEST_MATRIX_CSV_HEADER: &str =
    "claim_id,paper_claim,code_artifacts,tests,experiment_artifacts";
pub const TRACE_ARCHITECTURE_CSV_HEADER: &str = "source,target,binding";

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum VerificationMode {
    Fast,
    Audited,
    Checked,
    Reference,
    Research,
}

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum TraceValidationFailureClass {
    Signature,
    Digest,
    Theorem,
    Registry,
    Admission,
    Unknown,
}

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum TraceValidationFailureBroadClass {
    Authenticity,
    Semantic,
    Unknown,
}

impl TraceValidationFailureClass {
    pub fn broad_class(self) -> TraceValidationFailureBroadClass {
        match self {
            TraceValidationFailureClass::Signature | TraceValidationFailureClass::Digest => {
                TraceValidationFailureBroadClass::Authenticity
            }
            TraceValidationFailureClass::Theorem
            | TraceValidationFailureClass::Registry
            | TraceValidationFailureClass::Admission => TraceValidationFailureBroadClass::Semantic,
            TraceValidationFailureClass::Unknown => TraceValidationFailureBroadClass::Unknown,
        }
    }
}

pub fn classify_trace_validation_error(error: &Error) -> TraceValidationFailureClass {
    let Error::Verification(message) = error else {
        return TraceValidationFailureClass::Unknown;
    };
    classify_trace_validation_message(message)
}

pub fn classify_trace_validation_message(message: &str) -> TraceValidationFailureClass {
    let message = message.to_ascii_lowercase();
    if message.contains("signature")
        || message.contains("key_id")
        || message.contains("key_fingerprint")
        || message.contains("shared-secret")
        || message.contains("shared_secret")
        || message.contains("ed25519")
    {
        return TraceValidationFailureClass::Signature;
    }
    // Registry-class failures are limited to the adapter registry's own
    // content: when the registry's declared capabilities disagree with
    // the native admission it is supposed to support, the registry
    // itself is the source of the inconsistency. The substring is unique
    // to the adapter-registry capability-fingerprint check.
    if message.contains("capability fingerprint") {
        return TraceValidationFailureClass::Registry;
    }
    // Digest-class failures are explicit cryptographic mismatches
    // (`digest mismatch`, `digest does not match`) or generic checksums.
    // Field-name substrings such as `transcript_digest` or
    // `evidence_digest` are not real digest errors and fall through to
    // the admission subsystem check below.
    if message.contains("digest mismatch")
        || message.contains("digest does not match")
        || message.contains("checksum")
    {
        return TraceValidationFailureClass::Digest;
    }
    // The native admission subsystem spans native admission, checker
    // outputs, checker transcripts, Lean checkable artifacts, the
    // checker result index, the proof assistant summary's theorems, and
    // the adapter registry's content. Any error mentioning one of these
    // subsystems is an admission-class failure: the admission is what
    // binds the evidence together, so a broken artifact in this chain is
    // an admission-side problem.
    if message.contains("admission")
        || message.contains("admissions")
        || message.contains("native")
        || message.contains("checker")
        || message.contains("transcript")
        || message.contains("checkable")
        || message.contains("lean")
        || message.contains("index")
        || message.contains("theorem")
        || message.contains("registry")
        || message.contains("adapter")
    {
        return TraceValidationFailureClass::Admission;
    }
    TraceValidationFailureClass::Unknown
}

pub struct AuditDocument {
    pub backend: String,
    pub math_bound: MathBoundAuditTrace,
    pub steps: Vec<AuditStep>,
    pub obligations: Vec<AuditObligation>,
    pub rewrites: Vec<AuditRewrite>,
    pub proof_objects: Vec<AuditProofObject>,
    pub evidence: Vec<String>,
    pub cost: AuditCost,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct MathBoundAuditTrace {
    pub plan_fingerprint: String,
    pub backend_id: String,
    pub device_kind: String,
    pub capability_fingerprint: String,
    pub p_adic_constraint_fingerprint: String,
    pub sheaf_constraint_fingerprint: String,
    pub lowering_rule_ids: Vec<String>,
    pub fallback_reason: Option<String>,
    pub conformance_result: Option<String>,
    pub benchmark_environment: Option<String>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct AuditStep {
    pub node_id: usize,
    pub op_name: String,
    pub backend: String,
    pub domain: String,
    pub representation: String,
    pub lowering_rule_id: Option<String>,
    pub kind: String,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct AuditObligation {
    pub source: String,
    pub severity: String,
    pub status: String,
    pub condition: String,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct AuditRewrite {
    pub source: String,
    pub rule: String,
    pub discharged_conditions: usize,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct AuditProofObject {
    pub id: String,
    pub kind: String,
    pub claim: String,
    pub status: String,
    pub obligations: Vec<String>,
    pub evidence: Vec<String>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct AuditCost {
    pub runtime_ns: Option<u64>,
    pub memory_bytes: Option<u64>,
    pub precision_loss: Option<u32>,
    pub unresolved_obligations: usize,
    pub semantic: Vec<String>,
}

impl AuditDocument {
    pub fn from_plan(plan: &ExecutionPlan) -> Self {
        let math_bound = MathBoundAuditTrace::from_plan(plan, None, None);
        Self {
            backend: plan.backend.clone(),
            math_bound,
            steps: plan.steps.iter().map(AuditStep::from_step).collect(),
            obligations: plan
                .obligations
                .iter()
                .map(|obligation| AuditObligation {
                    source: format_obligation_source(&obligation.source),
                    severity: format_obligation_severity(&obligation.severity),
                    status: format_discharge_status(&obligation.status),
                    condition: obligation.condition.clone(),
                })
                .collect(),
            rewrites: plan
                .rewrites
                .iter()
                .map(|rewrite| AuditRewrite {
                    source: format!("{:?}", rewrite.source),
                    rule: rewrite.rule.clone(),
                    discharged_conditions: rewrite.discharged_conditions.len(),
                })
                .collect(),
            proof_objects: plan
                .proof_objects
                .iter()
                .map(AuditProofObject::from_proof_object)
                .collect(),
            evidence: plan.evidence_log.entries.clone(),
            cost: AuditCost::from_plan(plan),
        }
    }

    pub fn from_plan_with_conformance(
        plan: &ExecutionPlan,
        conformance: &BackendConformanceRunReport,
    ) -> Self {
        let mut document = Self::from_plan(plan);
        document.math_bound.conformance_result = Some(format_conformance_result(conformance));
        document
    }

    pub fn to_json(&self) -> String {
        let steps = self
            .steps
            .iter()
            .map(AuditStep::to_json)
            .collect::<Vec<_>>()
            .join(",");
        let obligations = self
            .obligations
            .iter()
            .map(AuditObligation::to_json)
            .collect::<Vec<_>>()
            .join(",");
        let rewrites = self
            .rewrites
            .iter()
            .map(AuditRewrite::to_json)
            .collect::<Vec<_>>()
            .join(",");
        let proof_objects = self
            .proof_objects
            .iter()
            .map(AuditProofObject::to_json)
            .collect::<Vec<_>>()
            .join(",");
        let evidence = self
            .evidence
            .iter()
            .map(|entry| json_string(entry))
            .collect::<Vec<_>>()
            .join(",");
        format!(
            "{{\"backend\":{},\"math_bound\":{},\"steps\":[{}],\"obligations\":[{}],\"rewrites\":[{}],\"proof_objects\":[{}],\"evidence\":[{}],\"cost\":{}}}",
            json_string(&self.backend),
            self.math_bound.to_json(),
            steps,
            obligations,
            rewrites,
            proof_objects,
            evidence,
            self.cost.to_json()
        )
    }
}

pub fn audit_json_report(plan: &ExecutionPlan) -> String {
    AuditDocument::from_plan(plan).to_json()
}

pub fn audit_json_report_with_conformance(
    plan: &ExecutionPlan,
    conformance: &BackendConformanceRunReport,
) -> String {
    AuditDocument::from_plan_with_conformance(plan, conformance).to_json()
}

pub fn math_bound_audit_trace_from_plan(
    plan: &ExecutionPlan,
    plan_fingerprint: &str,
) -> Result<MathBoundAuditTrace> {
    if !is_valid_artifact_digest(plan_fingerprint) {
        return Err(Error::verification(
            "math-bound audit trace plan_fingerprint must be a sha256 digest",
        ));
    }
    let mut trace = MathBoundAuditTrace::from_plan(plan, None, None);
    trace.plan_fingerprint = plan_fingerprint.to_string();
    Ok(trace)
}

pub fn math_bound_audit_trace_from_plan_with_conformance(
    plan: &ExecutionPlan,
    plan_fingerprint: &str,
    conformance: &BackendConformanceRunReport,
    benchmark_environment: Option<String>,
) -> Result<MathBoundAuditTrace> {
    let mut trace = math_bound_audit_trace_from_plan(plan, plan_fingerprint)?;
    trace.conformance_result = Some(format_conformance_result(conformance));
    trace.benchmark_environment = benchmark_environment;
    Ok(trace)
}

pub fn math_bound_audit_trace_json(trace: &MathBoundAuditTrace) -> String {
    trace.to_json()
}

pub fn math_bound_audit_trace_artifact(
    stem: &str,
    trace: &MathBoundAuditTrace,
) -> Result<ProofReplayTraceArtifact> {
    let stem = sanitize_artifact_stem(stem)?;
    let filename = format!("{stem}.math-bound-audit.json");
    let contents = trace.to_json();
    Ok(ProofReplayTraceArtifact {
        filename,
        artifact: MATH_BOUND_AUDIT_TRACE_ARTIFACT.to_string(),
        version: MATH_BOUND_AUDIT_TRACE_VERSION,
        format: "json".to_string(),
        digest: proof_replay_artifact_digest(&contents),
    })
}

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum ProofCertificateFormat {
    SExpression,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ProofCertificate {
    pub version: u32,
    pub backend: String,
    pub proofs: Vec<ProofCertificateEntry>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ProofCertificateEntry {
    pub theorem_id: String,
    pub original_id: String,
    pub kind: String,
    pub status: String,
    pub claim: String,
    pub obligations: Vec<String>,
    pub evidence: Vec<String>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ProofCertificateCheckReport {
    pub checked_proofs: usize,
    pub warnings: Vec<String>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ProofReplayReport {
    pub plan_fingerprint: Option<String>,
    pub checked_proofs: usize,
    pub replayed_proofs: Vec<ProofReplayEntry>,
    pub warnings: Vec<String>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ProofReplayEntry {
    pub theorem_id: String,
    pub original_id: String,
    pub kind: String,
    pub status: String,
    pub replayed: bool,
    pub replay_rule: String,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ProofReplayArtifactBundle {
    pub text_filename: String,
    pub text: String,
    pub json_filename: String,
    pub json: String,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ProofReplayTraceManifest {
    pub trace_name: String,
    pub plan_fingerprint: Option<String>,
    pub artifacts: Vec<ProofReplayTraceArtifact>,
    pub proof_assistant: Option<ProofAssistantReplaySummary>,
    pub tuning: Option<ProofReplayTraceTuning>,
    pub signature: Option<ProofReplayTraceSignature>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ProofAssistantReplaySummary {
    pub dialect: String,
    pub plan_fingerprint: Option<String>,
    pub filename: String,
    pub adapter_registry_filename: String,
    pub adapter_registry_digest: String,
    pub theorem_count: usize,
    pub theorems: Vec<ProofAssistantReplayTheoremSummary>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ProofAssistantReplayTheoremSummary {
    pub theorem_id: String,
    pub original_id: String,
    pub kind: String,
    pub status: String,
    pub replay_rule: String,
    pub obligations: Vec<String>,
    pub evidence: Vec<String>,
    pub obligation_count: usize,
    pub evidence_count: usize,
    pub statement_fingerprint: String,
    pub adapter_backend: String,
    pub checker_version: String,
    pub proof_status: String,
    pub adapter_capability_fingerprint: String,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ProofAssistantAdapterCapability {
    pub adapter_backend: String,
    pub checker_version: String,
    pub proof_status: String,
    pub native_checked: bool,
    pub admission_artifact_digest: Option<String>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ProofAssistantAdapterRegistry {
    pub plan_fingerprint: Option<String>,
    pub capabilities: Vec<ProofAssistantAdapterCapability>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ProofAssistantNativeAdmission {
    pub plan_fingerprint: Option<String>,
    pub adapter_backend: String,
    pub checker_version: String,
    pub checked_theorem_count: usize,
    pub result_status: String,
    pub theorem_result_fingerprints: Vec<String>,
    pub admission_claim: String,
    pub evidence_digest: String,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ProofAssistantCheckerOutput {
    pub plan_fingerprint: String,
    pub artifact_filename: String,
    pub artifact_digest: String,
    pub transcript_digest: String,
    pub adapter_backend: String,
    pub checker_version: String,
    pub checked_theorem_count: usize,
    pub result_status: String,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ProofAssistantCheckerTranscript {
    pub plan_fingerprint: String,
    pub checker_command: String,
    pub artifact_filename: String,
    pub artifact_digest: String,
    pub exit_status: i32,
    pub stdout_digest: String,
    pub stderr_digest: String,
    pub result_status: String,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct CheckerResultEntry {
    pub theorem_id: String,
    pub theorem_result_fingerprint: String,
    pub adapter_capability_fingerprint: String,
    pub admission_artifact_digest: String,
    pub plan_fingerprint: String,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct CheckerResultIndex {
    pub plan_fingerprint: String,
    pub entry_count: usize,
    pub entries: Vec<CheckerResultEntry>,
}

impl ProofAssistantAdapterCapability {
    fn to_json(&self) -> String {
        format!(
            "{{\"adapter_backend\":{},\"checker_version\":{},\"proof_status\":{},\"native_checked\":{},\"admission_artifact_digest\":{},\"capability_fingerprint\":{}}}",
            json_string(&self.adapter_backend),
            json_string(&self.checker_version),
            json_string(&self.proof_status),
            self.native_checked,
            json_option_string(&self.admission_artifact_digest),
            json_string(&proof_assistant_adapter_capability_fingerprint(self))
        )
    }
}

impl ProofAssistantNativeAdmission {
    pub fn to_json(&self) -> String {
        let theorem_result_fingerprints = self
            .theorem_result_fingerprints
            .iter()
            .map(|fingerprint| json_string(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\":{}}}",
            json_string(PROOF_ASSISTANT_NATIVE_ADMISSION_ARTIFACT),
            PROOF_ASSISTANT_NATIVE_ADMISSION_VERSION,
            json_option_string(&self.plan_fingerprint),
            json_string(&self.adapter_backend),
            json_string(&self.checker_version),
            self.checked_theorem_count,
            json_string(&self.result_status),
            theorem_result_fingerprints,
            json_string(&self.admission_claim),
            json_string(&self.evidence_digest)
        )
    }
}

impl ProofAssistantCheckerOutput {
    pub fn to_json(&self) -> String {
        format!(
            "{{\"artifact\":{},\"version\":{},\"plan_fingerprint\":{},\"artifact_filename\":{},\"artifact_digest\":{},\"transcript_digest\":{},\"adapter_backend\":{},\"checker_version\":{},\"checked_theorem_count\":{},\"result_status\":{}}}",
            json_string(PROOF_ASSISTANT_CHECKER_OUTPUT_ARTIFACT),
            PROOF_ASSISTANT_CHECKER_OUTPUT_VERSION,
            json_string(&self.plan_fingerprint),
            json_string(&self.artifact_filename),
            json_string(&self.artifact_digest),
            json_string(&self.transcript_digest),
            json_string(&self.adapter_backend),
            json_string(&self.checker_version),
            self.checked_theorem_count,
            json_string(&self.result_status)
        )
    }
}

impl ProofAssistantCheckerTranscript {
    pub fn to_json(&self) -> String {
        format!(
            "{{\"artifact\":{},\"version\":{},\"plan_fingerprint\":{},\"checker_command\":{},\"artifact_filename\":{},\"artifact_digest\":{},\"exit_status\":{},\"stdout_digest\":{},\"stderr_digest\":{},\"result_status\":{}}}",
            json_string(PROOF_ASSISTANT_CHECKER_TRANSCRIPT_ARTIFACT),
            PROOF_ASSISTANT_CHECKER_TRANSCRIPT_VERSION,
            json_string(&self.plan_fingerprint),
            json_string(&self.checker_command),
            json_string(&self.artifact_filename),
            json_string(&self.artifact_digest),
            self.exit_status,
            json_string(&self.stdout_digest),
            json_string(&self.stderr_digest),
            json_string(&self.result_status)
        )
    }
}

impl CheckerResultEntry {
    fn to_json(&self) -> String {
        format!(
            "{{\"theorem_id\":{},\"theorem_result_fingerprint\":{},\"adapter_capability_fingerprint\":{},\"admission_artifact_digest\":{},\"plan_fingerprint\":{}}}",
            json_string(&self.theorem_id),
            json_string(&self.theorem_result_fingerprint),
            json_string(&self.adapter_capability_fingerprint),
            json_string(&self.admission_artifact_digest),
            json_string(&self.plan_fingerprint)
        )
    }
}

impl CheckerResultIndex {
    pub fn to_json(&self) -> String {
        let entries = self
            .entries
            .iter()
            .map(CheckerResultEntry::to_json)
            .collect::<Vec<_>>()
            .join(",");
        format!(
            "{{\"artifact\":{},\"version\":{},\"plan_fingerprint\":{},\"entry_count\":{},\"entries\":[{}]}}",
            json_string(PROOF_ASSISTANT_CHECKER_RESULT_INDEX_ARTIFACT),
            PROOF_ASSISTANT_CHECKER_RESULT_INDEX_VERSION,
            json_string(&self.plan_fingerprint),
            self.entry_count,
            entries
        )
    }
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ProofReplayTraceArtifact {
    pub filename: String,
    pub artifact: String,
    pub version: u32,
    pub format: String,
    pub digest: String,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ProofReplayTraceSignature {
    pub key_id: String,
    pub key_kind: String,
    pub key_fingerprint: String,
    pub algorithm: String,
    pub value: String,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub enum ProofReplayTraceVerificationKey {
    SharedSecret {
        key_id: String,
        secret: String,
    },
    Ed25519PublicKey {
        key_id: String,
        public_key_fingerprint: String,
        public_key_hex: String,
    },
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ProofReplayTraceTuning {
    pub backend: String,
    pub selected_strategy: String,
    pub benchmark_count: usize,
    pub enable_pointwise_fusion: bool,
    pub enable_padic_matmul_valuation_skip: bool,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ProofReplayTraceBenchmarkSet {
    pub plan_fingerprint: String,
    pub backend: String,
    pub selected_strategy: String,
    pub records: Vec<ProofReplayTraceBenchmarkRecord>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ProofReplayTraceBenchmarkRecord {
    pub plan_fingerprint: String,
    pub backend: String,
    pub strategy: String,
    pub input_description: String,
    pub duration_ns: u64,
}

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum ProofAssistantDialect {
    Lean,
}

impl ProofReplayTraceTuning {
    pub fn to_json(&self) -> String {
        format!(
            "{{\"artifact\":{},\"version\":{},\"backend\":{},\"selected_strategy\":{},\"benchmark_count\":{},\"enable_pointwise_fusion\":{},\"enable_padic_matmul_valuation_skip\":{}}}",
            json_string(PROOF_REPLAY_TRACE_TUNING_ARTIFACT),
            PROOF_REPLAY_TRACE_TUNING_VERSION,
            json_string(&self.backend),
            json_string(&self.selected_strategy),
            self.benchmark_count,
            self.enable_pointwise_fusion,
            self.enable_padic_matmul_valuation_skip
        )
    }

    fn to_manifest_json(&self) -> String {
        format!(
            "{{\"backend\":{},\"selected_strategy\":{},\"benchmark_count\":{},\"enable_pointwise_fusion\":{},\"enable_padic_matmul_valuation_skip\":{}}}",
            json_string(&self.backend),
            json_string(&self.selected_strategy),
            self.benchmark_count,
            self.enable_pointwise_fusion,
            self.enable_padic_matmul_valuation_skip
        )
    }
}

impl From<TuningTraceSummary> for ProofReplayTraceTuning {
    fn from(value: TuningTraceSummary) -> Self {
        Self {
            backend: value.backend,
            selected_strategy: value.selected_strategy,
            benchmark_count: value.benchmark_count,
            enable_pointwise_fusion: value.enable_pointwise_fusion,
            enable_padic_matmul_valuation_skip: value.enable_padic_matmul_valuation_skip,
        }
    }
}

impl ProofReplayTraceBenchmarkSet {
    pub fn from_benchmark_records(
        plan_fingerprint: impl Into<String>,
        backend: impl Into<String>,
        selected_strategy: impl Into<String>,
        records: &[BenchmarkRecord],
    ) -> Self {
        let backend = backend.into();
        let plan_fingerprint = plan_fingerprint.into();
        Self {
            plan_fingerprint: plan_fingerprint.clone(),
            backend: backend.clone(),
            selected_strategy: selected_strategy.into(),
            records: records
                .iter()
                .filter(|record| {
                    record.backend == backend
                        && proof_replay_plan_fingerprint(&record.plan_key) == plan_fingerprint
                })
                .map(|record| {
                    ProofReplayTraceBenchmarkRecord::from_record(record, &plan_fingerprint)
                })
                .collect(),
        }
    }

    pub fn to_json(&self) -> String {
        let records = self
            .records
            .iter()
            .map(ProofReplayTraceBenchmarkRecord::to_json)
            .collect::<Vec<_>>()
            .join(",");
        format!(
            "{{\"artifact\":{},\"version\":{},\"plan_fingerprint\":{},\"backend\":{},\"selected_strategy\":{},\"records\":[{}]}}",
            json_string(PROOF_REPLAY_TRACE_BENCHMARK_ARTIFACT),
            PROOF_REPLAY_TRACE_BENCHMARK_VERSION,
            json_string(&self.plan_fingerprint),
            json_string(&self.backend),
            json_string(&self.selected_strategy),
            records
        )
    }

    fn fastest_strategy(&self) -> Option<&str> {
        self.records
            .iter()
            .min_by_key(|record| record.duration_ns)
            .map(|record| record.strategy.as_str())
    }
}

impl ProofReplayTraceBenchmarkRecord {
    fn to_json(&self) -> String {
        format!(
            "{{\"plan_fingerprint\":{},\"backend\":{},\"strategy\":{},\"input_description\":{},\"duration_ns\":{}}}",
            json_string(&self.plan_fingerprint),
            json_string(&self.backend),
            json_string(&self.strategy),
            json_string(&self.input_description),
            self.duration_ns
        )
    }
}

impl ProofReplayTraceBenchmarkRecord {
    fn from_record(value: &BenchmarkRecord, plan_fingerprint: &str) -> Self {
        Self {
            plan_fingerprint: plan_fingerprint.to_string(),
            backend: value.backend.clone(),
            strategy: value.strategy.clone(),
            input_description: value.input_description.clone(),
            duration_ns: value.duration_ns,
        }
    }
}

impl ProofReplayReport {
    pub fn to_json(&self) -> String {
        let replayed_proofs = self
            .replayed_proofs
            .iter()
            .map(ProofReplayEntry::to_json)
            .collect::<Vec<_>>()
            .join(",");
        let warnings = self
            .warnings
            .iter()
            .map(|warning| json_string(warning))
            .collect::<Vec<_>>()
            .join(",");
        format!(
            "{{\"artifact\":{},\"version\":{},\"plan_fingerprint\":{},\"checked_proofs\":{},\"replayed_proofs\":[{}],\"warnings\":[{}]}}",
            json_string(PROOF_REPLAY_REPORT_ARTIFACT),
            PROOF_REPLAY_REPORT_VERSION,
            json_option_string(&self.plan_fingerprint),
            self.checked_proofs,
            replayed_proofs,
            warnings
        )
    }
}

impl ProofReplayTraceManifest {
    pub fn to_json(&self) -> String {
        let artifacts = self
            .artifacts
            .iter()
            .map(ProofReplayTraceArtifact::to_json)
            .collect::<Vec<_>>()
            .join(",");
        format!(
            "{{\"artifact\":{},\"version\":{},\"trace_name\":{},\"plan_fingerprint\":{},\"artifacts\":[{}],\"proof_assistant\":{},\"tuning\":{},\"signature\":{}}}",
            json_string(PROOF_REPLAY_TRACE_MANIFEST_ARTIFACT),
            PROOF_REPLAY_TRACE_MANIFEST_VERSION,
            json_string(&self.trace_name),
            json_option_string(&self.plan_fingerprint),
            artifacts,
            json_option_proof_assistant_summary(&self.proof_assistant),
            json_option_tuning(&self.tuning),
            json_option_signature(&self.signature)
        )
    }
}

impl ProofAssistantReplaySummary {
    fn to_json(&self) -> String {
        let theorems = self
            .theorems
            .iter()
            .map(ProofAssistantReplayTheoremSummary::to_json)
            .collect::<Vec<_>>()
            .join(",");
        format!(
            "{{\"dialect\":{},\"plan_fingerprint\":{},\"filename\":{},\"adapter_registry_filename\":{},\"adapter_registry_digest\":{},\"theorem_count\":{},\"theorems\":[{}]}}",
            json_string(&self.dialect),
            json_option_string(&self.plan_fingerprint),
            json_string(&self.filename),
            json_string(&self.adapter_registry_filename),
            json_string(&self.adapter_registry_digest),
            self.theorem_count,
            theorems
        )
    }
}

impl ProofAssistantReplayTheoremSummary {
    fn to_json(&self) -> String {
        let obligations = self
            .obligations
            .iter()
            .map(|entry| json_string(entry))
            .collect::<Vec<_>>()
            .join(",");
        let evidence = self
            .evidence
            .iter()
            .map(|entry| json_string(entry))
            .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\":{}}}",
            json_string(&self.theorem_id),
            json_string(&self.original_id),
            json_string(&self.kind),
            json_string(&self.status),
            json_string(&self.replay_rule),
            obligations,
            evidence,
            self.obligation_count,
            self.evidence_count,
            json_string(&self.statement_fingerprint),
            json_string(&self.adapter_backend),
            json_string(&self.checker_version),
            json_string(&self.proof_status),
            json_string(&self.adapter_capability_fingerprint)
        )
    }
}

impl ProofReplayTraceSignature {
    fn to_json(&self) -> String {
        format!(
            "{{\"key_id\":{},\"key_kind\":{},\"key_fingerprint\":{},\"algorithm\":{},\"value\":{}}}",
            json_string(&self.key_id),
            json_string(&self.key_kind),
            json_string(&self.key_fingerprint),
            json_string(&self.algorithm),
            json_string(&self.value)
        )
    }
}

impl ProofReplayTraceArtifact {
    fn to_json(&self) -> String {
        format!(
            "{{\"filename\":{},\"artifact\":{},\"version\":{},\"format\":{},\"digest\":{}}}",
            json_string(&self.filename),
            json_string(&self.artifact),
            self.version,
            json_string(&self.format),
            json_string(&self.digest)
        )
    }
}

impl ProofReplayEntry {
    fn to_json(&self) -> String {
        format!(
            "{{\"theorem_id\":{},\"original_id\":{},\"kind\":{},\"status\":{},\"replayed\":{},\"replay_rule\":{}}}",
            json_string(&self.theorem_id),
            json_string(&self.original_id),
            json_string(&self.kind),
            json_string(&self.status),
            self.replayed,
            json_string(&self.replay_rule)
        )
    }
}

impl ProofCertificate {
    pub fn from_plan(plan: &ExecutionPlan) -> Self {
        Self {
            version: 1,
            backend: plan.backend.clone(),
            proofs: plan
                .proof_objects
                .iter()
                .map(ProofCertificateEntry::from_proof_object)
                .collect(),
        }
    }

    pub fn to_format(&self, format: ProofCertificateFormat) -> String {
        match format {
            ProofCertificateFormat::SExpression => self.to_s_expression(),
        }
    }

    pub fn to_s_expression(&self) -> String {
        let mut lines = Vec::new();
        lines.push("(tokitai-proof-certificate".to_string());
        lines.push(format!("  (version {})", self.version));
        lines.push(format!("  (backend {})", sexp_string(&self.backend)));
        for proof in &self.proofs {
            lines.push("  (proof".to_string());
            lines.push(format!("    (theorem {})", proof.theorem_id));
            lines.push(format!(
                "    (original-id {})",
                sexp_string(&proof.original_id)
            ));
            lines.push(format!("    (kind {})", proof.kind));
            lines.push(format!("    (status {})", proof.status));
            lines.push(format!("    (claim {})", sexp_string(&proof.claim)));
            lines.push("    (obligations".to_string());
            for obligation in &proof.obligations {
                lines.push(format!("      {}", sexp_string(obligation)));
            }
            lines.push("    )".to_string());
            lines.push("    (evidence".to_string());
            for evidence in &proof.evidence {
                lines.push(format!("      {}", sexp_string(evidence)));
            }
            lines.push("    )".to_string());
            lines.push("  )".to_string());
        }
        lines.push(")".to_string());
        lines.join("\n")
    }

    pub fn from_s_expression(input: &str) -> Result<Self> {
        parse_proof_certificate_s_expression(input)
    }
}

pub fn parse_proof_certificate_report(input: &str) -> Result<ProofCertificate> {
    ProofCertificate::from_s_expression(input)
}

pub fn verify_proof_certificate(
    certificate: &ProofCertificate,
) -> Result<ProofCertificateCheckReport> {
    if certificate.version != 1 {
        return Err(Error::verification(format!(
            "unsupported proof certificate version {}",
            certificate.version
        )));
    }
    if certificate.backend.trim().is_empty() {
        return Err(Error::verification(
            "proof certificate backend must not be empty",
        ));
    }
    let mut warnings = Vec::new();
    for proof in &certificate.proofs {
        verify_certificate_entry(proof)?;
        if proof.status == "pending" {
            warnings.push(format!("proof {} is pending", proof.theorem_id));
        }
        if proof.status == "assumed" {
            warnings.push(format!(
                "proof {} relies on an assumption",
                proof.theorem_id
            ));
        }
    }
    Ok(ProofCertificateCheckReport {
        checked_proofs: certificate.proofs.len(),
        warnings,
    })
}

pub fn verify_plan_proof_certificate(plan: &ExecutionPlan) -> Result<ProofCertificateCheckReport> {
    verify_proof_certificate(&ProofCertificate::from_plan(plan))
}

pub fn verify_plan_bound_proof_certificate(
    plan: &ExecutionPlan,
    certificate: &ProofCertificate,
) -> Result<ProofCertificateCheckReport> {
    let report = verify_proof_certificate(certificate)?;
    let expected = ProofCertificate::from_plan(plan);
    if certificate.backend != expected.backend {
        return Err(Error::verification(format!(
            "proof certificate backend mismatch: expected {}, got {}",
            expected.backend, certificate.backend
        )));
    }
    if certificate.proofs.len() != expected.proofs.len() {
        return Err(Error::verification(format!(
            "proof certificate proof count mismatch: expected {}, got {}",
            expected.proofs.len(),
            certificate.proofs.len()
        )));
    }
    for expected_proof in &expected.proofs {
        let Some(actual) = certificate
            .proofs
            .iter()
            .find(|proof| proof.original_id == expected_proof.original_id)
        else {
            return Err(Error::verification(format!(
                "proof certificate missing plan proof {}",
                expected_proof.original_id
            )));
        };
        if actual != expected_proof {
            return Err(Error::verification(format!(
                "proof certificate entry {} does not match plan proof object",
                expected_proof.original_id
            )));
        }
    }
    Ok(report)
}

pub fn verify_plan_certificate_semantics(
    plan: &ExecutionPlan,
    certificate: &ProofCertificate,
) -> Result<ProofCertificateCheckReport> {
    let report = verify_plan_certificate_semantics_report(plan, certificate)?;
    Ok(ProofCertificateCheckReport {
        checked_proofs: report.checked_proofs,
        warnings: report.warnings,
    })
}

pub fn verify_plan_certificate_semantics_report(
    plan: &ExecutionPlan,
    certificate: &ProofCertificate,
) -> Result<ProofReplayReport> {
    let report = verify_plan_bound_proof_certificate(plan, certificate)?;
    let mut replayed_proofs = Vec::new();
    for proof in &certificate.proofs {
        if proof.kind == "shape_equality" {
            replay_shape_equality_proof(plan, proof)?;
        } else if proof.kind == "valuation_cutoff" {
            replay_valuation_cutoff_proof(plan, proof)?;
        } else if proof.kind == "lowering_semantic_preservation" {
            replay_lowering_semantic_preservation_proof(plan, proof)?;
        } else if proof.kind == "rewrite_soundness" {
            replay_rewrite_soundness_proof(plan, proof)?;
        }
        replayed_proofs.push(ProofReplayEntry {
            theorem_id: proof.theorem_id.clone(),
            original_id: proof.original_id.clone(),
            kind: proof.kind.clone(),
            status: proof.status.clone(),
            replayed: is_semantically_replayed_kind(&proof.kind),
            replay_rule: semantic_replay_rule(&proof.kind).to_string(),
        });
    }
    Ok(ProofReplayReport {
        plan_fingerprint: None,
        checked_proofs: report.checked_proofs,
        replayed_proofs,
        warnings: report.warnings,
    })
}

impl ProofCertificateEntry {
    fn from_proof_object(proof: &ProofObject) -> Self {
        Self {
            theorem_id: proof_theorem_id(&proof.id),
            original_id: proof.id.clone(),
            kind: format_proof_kind(&proof.kind),
            status: format_proof_status(&proof.status),
            claim: proof.claim.clone(),
            obligations: proof.obligations.clone(),
            evidence: proof.evidence.clone(),
        }
    }
}

pub fn proof_certificate_report(plan: &ExecutionPlan) -> String {
    ProofCertificate::from_plan(plan).to_format(ProofCertificateFormat::SExpression)
}

pub fn proof_replay_report(report: &ProofReplayReport) -> String {
    let mut lines = Vec::new();
    lines.push(format!("artifact: {PROOF_REPLAY_REPORT_ARTIFACT}"));
    lines.push(format!("version: {PROOF_REPLAY_REPORT_VERSION}"));
    lines.push(format!(
        "plan fingerprint: {}",
        report.plan_fingerprint.as_deref().unwrap_or("null")
    ));
    lines.push(format!("checked proofs: {}", report.checked_proofs));
    lines.push(format!("replayed proofs: {}", report.replayed_proofs.len()));
    for entry in &report.replayed_proofs {
        lines.push(format!(
            "proof replay: theorem={}, original={}, kind={}, status={}, replayed={}, rule={}",
            entry.theorem_id,
            entry.original_id,
            entry.kind,
            entry.status,
            entry.replayed,
            entry.replay_rule
        ));
    }
    lines.push(format!("warnings: {}", report.warnings.len()));
    for warning in &report.warnings {
        lines.push(format!("warning: {warning}"));
    }
    lines.join("\n")
}

pub fn proof_replay_json_report(report: &ProofReplayReport) -> String {
    report.to_json()
}

pub fn proof_assistant_replay_skeleton(
    certificate: &ProofCertificate,
    report: &ProofReplayReport,
    dialect: ProofAssistantDialect,
) -> Result<String> {
    match dialect {
        ProofAssistantDialect::Lean => lean_replay_skeleton(certificate, report),
    }
}

pub fn proof_assistant_lean_checkable_artifact_contents(
    summary: &ProofAssistantReplaySummary,
) -> Result<String> {
    verify_proof_assistant_replay_summary(summary)?;
    let selected_shape_witness_count = summary
        .theorems
        .iter()
        .filter(|theorem| theorem.kind == "shape_equality")
        .count();
    let selected_padic_witness_count = summary
        .theorems
        .iter()
        .filter(|theorem| padic_precision_cutoff_witness_statement(theorem).is_ok())
        .count();
    let mut lines = Vec::new();
    lines.push("/-".to_string());
    lines.push(format!(
        "artifact: {PROOF_ASSISTANT_LEAN_CHECKABLE_ARTIFACT}"
    ));
    lines.push(format!("version: {PROOF_ASSISTANT_LEAN_CHECKABLE_VERSION}"));
    lines.push("dialect: lean".to_string());
    lines.push(format!(
        "plan_fingerprint: {}",
        summary.plan_fingerprint.as_deref().unwrap_or("null")
    ));
    lines.push("checker_command: lean <artifact>.lean-checkable.lean".to_string());
    lines.push("This file is a minimally checkable Tokitai Lean smoke artifact.".to_string());
    lines.push(format!(
        "selected_witness_family: {PROOF_ASSISTANT_SELECTED_WITNESS_FAMILY}"
    ));
    lines.push(format!(
        "selected_nonstandard_witness_family: {PROOF_ASSISTANT_SELECTED_NONSTANDARD_WITNESS_FAMILY}"
    ));
    lines.push(format!(
        "selected_shape_witness_count: {selected_shape_witness_count}"
    ));
    lines.push(format!(
        "selected_padic_witness_count: {selected_padic_witness_count}"
    ));
    lines.push("-/".to_string());
    lines.push(String::new());
    lines.push("namespace TokitaiCheckable".to_string());
    for theorem in &summary.theorems {
        let theorem_ident = lean_identifier(&format!("{}_checkable", theorem.theorem_id))?;
        lines.push(String::new());
        lines.push(format!(
            "/-- Tokitai checkable theorem: {} -/",
            theorem.theorem_id
        ));
        lines.push(format!("-- original_id: {}", theorem.original_id));
        lines.push(format!("-- kind: {}", theorem.kind));
        lines.push(format!("-- status: {}", theorem.status));
        lines.push(format!("-- replay_rule: {}", theorem.replay_rule));
        lines.push(format!(
            "-- statement_fingerprint: {}",
            theorem.statement_fingerprint
        ));
        lines.push(format!("-- adapter_backend: {}", theorem.adapter_backend));
        lines.push(format!("-- checker_version: {}", theorem.checker_version));
        lines.push(format!("-- proof_status: {}", theorem.proof_status));
        lines.push(format!(
            "-- adapter_capability_fingerprint: {}",
            theorem.adapter_capability_fingerprint
        ));
        lines.push(format!("theorem {theorem_ident} : True := by"));
        lines.push("  trivial".to_string());
        if theorem.kind == "shape_equality" {
            let witness_ident =
                lean_identifier(&format!("{}_shape_equality_witness", theorem.theorem_id))?;
            lines.push(format!(
                "theorem {witness_ident} : {} := by",
                lean_shape_equality_witness_statement(theorem)?
            ));
            lines.push("  rfl".to_string());
        }
        if let Ok(statement) = padic_precision_cutoff_witness_statement(theorem) {
            let witness_ident = lean_identifier(&format!(
                "{}_padic_precision_cutoff_witness",
                theorem.theorem_id
            ))?;
            lines.push(format!("theorem {witness_ident} : {statement} := by"));
            lines.push("  rfl".to_string());
        }
    }
    lines.push(String::new());
    lines.push("end TokitaiCheckable".to_string());
    Ok(lines.join("\n"))
}

pub fn proof_replay_report_with_plan_fingerprint(
    report: &ProofReplayReport,
    plan_fingerprint: &str,
) -> Result<ProofReplayReport> {
    if !is_valid_artifact_digest(plan_fingerprint) {
        return Err(Error::verification(
            "proof replay report plan_fingerprint must be a sha256 digest",
        ));
    }
    let mut report = report.clone();
    report.plan_fingerprint = Some(plan_fingerprint.to_string());
    Ok(report)
}

fn lean_replay_skeleton(
    certificate: &ProofCertificate,
    report: &ProofReplayReport,
) -> Result<String> {
    verify_proof_replay_report(report)?;
    let mut lines = Vec::new();
    lines.push("/-".to_string());
    lines.push(format!(
        "artifact: {PROOF_ASSISTANT_REPLAY_SKELETON_ARTIFACT}"
    ));
    lines.push(format!(
        "version: {PROOF_ASSISTANT_REPLAY_SKELETON_VERSION}"
    ));
    lines.push("dialect: lean".to_string());
    lines.push(format!("backend: {}", certificate.backend));
    lines.push(format!(
        "plan_fingerprint: {}",
        report.plan_fingerprint.as_deref().unwrap_or("null")
    ));
    lines.push(
        "This file is an interchange skeleton generated from Tokitai semantic replay.".to_string(),
    );
    lines.push("The theorem declarations are replay entry points; obligation and evidence declarations expose machine-checker-oriented proof goals for later native discharge.".to_string());
    lines.push("-/".to_string());
    lines.push(String::new());
    lines.push("namespace TokitaiReplay".to_string());
    let adapter_capability_fingerprint = proof_assistant_adapter_capability_fingerprint(
        &proof_assistant_skeleton_adapter_capability(),
    );
    for proof in &certificate.proofs {
        let Some(entry) = report
            .replayed_proofs
            .iter()
            .find(|entry| entry.original_id == proof.original_id)
        else {
            return Err(Error::verification(format!(
                "proof assistant replay skeleton missing replay entry for {}",
                proof.original_id
            )));
        };
        if entry.theorem_id != proof.theorem_id
            || entry.kind != proof.kind
            || entry.status != proof.status
            || !entry.replayed
        {
            return Err(Error::verification(format!(
                "proof assistant replay skeleton cannot bind inconsistent replay entry {}",
                proof.theorem_id
            )));
        }
        lines.push(String::new());
        lines.push(format!("/-- Tokitai theorem: {} -/", proof.theorem_id));
        lines.push(format!(
            "-- original_id: {}",
            lean_comment_text(&proof.original_id)
        ));
        lines.push(format!("-- kind: {}", proof.kind));
        lines.push(format!("-- status: {}", proof.status));
        lines.push(format!("-- replay_rule: {}", entry.replay_rule));
        lines.push(format!(
            "-- adapter_backend: {PROOF_ASSISTANT_REPLAY_ADAPTER_BACKEND}"
        ));
        lines.push(format!(
            "-- checker_version: {PROOF_ASSISTANT_REPLAY_CHECKER_VERSION}"
        ));
        lines.push(format!(
            "-- proof_status: {PROOF_ASSISTANT_REPLAY_PROOF_STATUS}"
        ));
        lines.push(format!(
            "-- adapter_capability_fingerprint: {adapter_capability_fingerprint}"
        ));
        lines.push(format!("-- claim: {}", lean_comment_text(&proof.claim)));
        let theorem_ident = lean_identifier(&proof.theorem_id)?;
        for obligation in &proof.obligations {
            lines.push(format!("-- obligation: {}", lean_comment_text(obligation)));
        }
        for evidence in &proof.evidence {
            lines.push(format!("-- evidence: {}", lean_comment_text(evidence)));
        }
        for index in 0..proof.obligations.len() {
            lines.push(format!(
                "def {theorem_ident}_obligation_{index} : Prop := True"
            ));
        }
        for index in 0..proof.evidence.len() {
            lines.push(format!(
                "def {theorem_ident}_evidence_{index} : Prop := True"
            ));
        }
        lines.push(format!(
            "axiom {theorem_ident} : {}",
            lean_replay_theorem_statement(
                &theorem_ident,
                proof.obligations.len(),
                proof.evidence.len()
            )
        ));
    }
    lines.push(String::new());
    lines.push("end TokitaiReplay".to_string());
    Ok(lines.join("\n"))
}

fn lean_identifier(value: &str) -> Result<String> {
    if value.is_empty() {
        return Err(Error::verification("Lean identifier must not be empty"));
    }
    let mut ident = String::new();
    for ch in value.chars() {
        if ch.is_ascii_alphanumeric() || ch == '_' {
            ident.push(ch);
        } else {
            ident.push('_');
        }
    }
    if ident.chars().next().is_some_and(|ch| ch.is_ascii_digit()) {
        ident.insert(0, '_');
    }
    if ident.chars().all(|ch| ch == '_') {
        return Err(Error::verification(format!(
            "Lean identifier {} has no usable symbol characters",
            value
        )));
    }
    Ok(ident)
}

fn lean_replay_theorem_statement(
    theorem_ident: &str,
    obligation_count: usize,
    evidence_count: usize,
) -> String {
    let mut goals = Vec::new();
    for index in 0..obligation_count {
        goals.push(format!("{theorem_ident}_obligation_{index}"));
    }
    for index in 0..evidence_count {
        goals.push(format!("{theorem_ident}_evidence_{index}"));
    }
    if goals.is_empty() {
        "True".to_string()
    } else {
        goals.join(" ∧ ")
    }
}

fn proof_assistant_statement_fingerprint(statement: &str) -> String {
    proof_replay_artifact_digest(statement)
}

fn lean_shape_equality_witness_statement(
    theorem: &ProofAssistantReplayTheoremSummary,
) -> Result<String> {
    if theorem.kind != "shape_equality" {
        return Err(Error::verification(
            "Lean shape equality witness requires a shape_equality theorem",
        ));
    }
    let Some(output_shape) = theorem
        .evidence
        .iter()
        .find_map(|entry| entry.strip_prefix("output_shape="))
    else {
        return Err(Error::verification(format!(
            "shape equality theorem {} missing output_shape evidence for Lean witness",
            theorem.theorem_id
        )));
    };
    let shape_len = lean_shape_evidence_length(output_shape).ok_or_else(|| {
        Error::verification(format!(
            "shape equality theorem {} has unsupported output_shape evidence {}",
            theorem.theorem_id, output_shape
        ))
    })?;
    Ok(format!("{shape_len} = {shape_len}"))
}

fn lean_shape_evidence_length(output_shape: &str) -> Option<usize> {
    let inner = output_shape.strip_prefix('[')?.strip_suffix(']')?;
    let trimmed = inner.trim();
    if trimmed.is_empty() {
        return Some(0);
    }
    Some(trimmed.split(',').count())
}

fn padic_precision_cutoff_witness_statement(
    theorem: &ProofAssistantReplayTheoremSummary,
) -> Result<String> {
    if theorem.kind != "valuation_cutoff" {
        return Err(Error::verification(
            "Lean p-adic precision cutoff witness requires a valuation_cutoff theorem",
        ));
    }
    if !theorem.claim_or_evidence_mentions_padic() {
        return Err(Error::verification(format!(
            "valuation theorem {} is not a p-adic cutoff witness candidate",
            theorem.theorem_id
        )));
    }
    let Some(precision) = theorem
        .evidence
        .iter()
        .find_map(|entry| extract_numeric_metadata(entry, "precision"))
        .or_else(|| {
            theorem
                .evidence
                .iter()
                .find_map(|entry| extract_numeric_metadata(entry, "cutoff"))
        })
    else {
        return Err(Error::verification(format!(
            "p-adic valuation theorem {} missing precision or cutoff evidence for Lean witness",
            theorem.theorem_id
        )));
    };
    Ok(format!("{precision} = {precision}"))
}

trait ProofAssistantReplayTheoremSummaryExt {
    fn claim_or_evidence_mentions_padic(&self) -> bool;
}

impl ProofAssistantReplayTheoremSummaryExt for ProofAssistantReplayTheoremSummary {
    fn claim_or_evidence_mentions_padic(&self) -> bool {
        self.obligations
            .iter()
            .chain(self.evidence.iter())
            .any(|entry| entry.contains("p-adic") || entry.contains("prime="))
    }
}

fn extract_numeric_metadata(entry: &str, key: &str) -> Option<usize> {
    let offset = entry.find(&format!("{key}="))? + key.len() + 1;
    let value = entry[offset..]
        .chars()
        .take_while(|ch| ch.is_ascii_digit())
        .collect::<String>();
    if value.is_empty() {
        return None;
    }
    value.parse().ok()
}

fn lean_comment_text(value: &str) -> String {
    value
        .replace("-/", "- /")
        .replace('\n', "\\n")
        .replace('\r', "\\r")
}

pub fn parse_proof_replay_report_json(input: &str) -> Result<ProofReplayReport> {
    let fields = parse_json_object_fields(input, "proof replay report JSON")?;
    validate_json_object_field_set(
        &fields,
        PROOF_REPLAY_REPORT_SCHEMA_FIELDS,
        "proof replay report",
    )?;
    let artifact_literal = json_field_string(&fields, "artifact", "proof replay report")?;
    if artifact_literal != PROOF_REPLAY_REPORT_ARTIFACT {
        return Err(Error::verification(format!(
            "unexpected proof replay report artifact {}",
            artifact_literal
        )));
    }
    let version = json_field_u32(&fields, "version", "proof replay report")?;
    if version != PROOF_REPLAY_REPORT_VERSION {
        return Err(Error::verification(format!(
            "unsupported proof replay report version {}",
            version
        )));
    }
    let plan_fingerprint =
        json_field_option_string(&fields, "plan_fingerprint", "proof replay report")?;
    let checked_proofs = json_field_usize(&fields, "checked_proofs", "proof replay report")?;
    let replayed_proofs = parse_proof_replay_entries_from_array(json_field(
        &fields,
        "replayed_proofs",
        "proof replay report",
    )?)?;
    let warnings = json_field_string_array(&fields, "warnings", "proof replay report")?;
    let report = ProofReplayReport {
        plan_fingerprint,
        checked_proofs,
        replayed_proofs,
        warnings,
    };
    verify_proof_replay_report(&report)?;
    Ok(report)
}

pub fn proof_replay_artifact_bundle(
    stem: &str,
    report: &ProofReplayReport,
) -> Result<ProofReplayArtifactBundle> {
    let stem = sanitize_artifact_stem(stem)?;
    Ok(ProofReplayArtifactBundle {
        text_filename: format!("{stem}.proof-replay.txt"),
        text: proof_replay_report(report),
        json_filename: format!("{stem}.proof-replay.json"),
        json: proof_replay_json_report(report),
    })
}

pub fn proof_replay_artifact_bundle_with_plan_fingerprint(
    stem: &str,
    report: &ProofReplayReport,
    plan_fingerprint: &str,
) -> Result<ProofReplayArtifactBundle> {
    let report = proof_replay_report_with_plan_fingerprint(report, plan_fingerprint)?;
    proof_replay_artifact_bundle(stem, &report)
}

pub fn verify_proof_replay_report(report: &ProofReplayReport) -> Result<()> {
    if report.checked_proofs != report.replayed_proofs.len() {
        return Err(Error::verification(format!(
            "proof replay report checked_proofs {} does not match replayed proof count {}",
            report.checked_proofs,
            report.replayed_proofs.len()
        )));
    }
    if let Some(fingerprint) = &report.plan_fingerprint {
        if !is_valid_artifact_digest(fingerprint) {
            return Err(Error::verification(
                "proof replay report plan_fingerprint must be a sha256 digest",
            ));
        }
    }
    for entry in &report.replayed_proofs {
        verify_proof_replay_entry(entry)?;
    }
    Ok(())
}

pub fn proof_replay_trace_manifest(
    trace_name: &str,
    bundle: &ProofReplayArtifactBundle,
) -> Result<ProofReplayTraceManifest> {
    proof_replay_trace_manifest_with_tuning(trace_name, bundle, None)
}

pub fn proof_replay_trace_manifest_with_tuning(
    trace_name: &str,
    bundle: &ProofReplayArtifactBundle,
    tuning: Option<ProofReplayTraceTuning>,
) -> Result<ProofReplayTraceManifest> {
    proof_replay_trace_manifest_with_plan_fingerprint(trace_name, bundle, tuning, None)
}

pub fn proof_replay_trace_manifest_with_plan_fingerprint(
    trace_name: &str,
    bundle: &ProofReplayArtifactBundle,
    tuning: Option<ProofReplayTraceTuning>,
    plan_fingerprint: Option<String>,
) -> Result<ProofReplayTraceManifest> {
    let trace_name = sanitize_artifact_stem(trace_name)?;
    if let Some(fingerprint) = &plan_fingerprint {
        if !is_valid_artifact_digest(fingerprint) {
            return Err(Error::verification(
                "proof replay trace manifest plan_fingerprint must be a sha256 digest",
            ));
        }
    }
    Ok(ProofReplayTraceManifest {
        trace_name,
        plan_fingerprint,
        artifacts: vec![
            ProofReplayTraceArtifact {
                filename: bundle.text_filename.clone(),
                artifact: PROOF_REPLAY_REPORT_ARTIFACT.to_string(),
                version: PROOF_REPLAY_REPORT_VERSION,
                format: "text".to_string(),
                digest: proof_replay_artifact_digest(&bundle.text),
            },
            ProofReplayTraceArtifact {
                filename: bundle.json_filename.clone(),
                artifact: PROOF_REPLAY_REPORT_ARTIFACT.to_string(),
                version: PROOF_REPLAY_REPORT_VERSION,
                format: "json".to_string(),
                digest: proof_replay_artifact_digest(&bundle.json),
            },
        ],
        proof_assistant: None,
        tuning,
        signature: None,
    })
}

pub fn proof_replay_trace_tuning_artifact(
    stem: &str,
    tuning: &ProofReplayTraceTuning,
) -> Result<ProofReplayTraceArtifact> {
    let stem = sanitize_artifact_stem(stem)?;
    let filename = format!("{stem}.trace-tuning.json");
    let contents = tuning.to_json();
    Ok(ProofReplayTraceArtifact {
        filename,
        artifact: PROOF_REPLAY_TRACE_TUNING_ARTIFACT.to_string(),
        version: PROOF_REPLAY_TRACE_TUNING_VERSION,
        format: "json".to_string(),
        digest: proof_replay_artifact_digest(&contents),
    })
}

pub fn proof_replay_trace_tuning_json(tuning: &ProofReplayTraceTuning) -> String {
    tuning.to_json()
}

pub fn proof_replay_trace_benchmark_artifact(
    stem: &str,
    benchmarks: &ProofReplayTraceBenchmarkSet,
) -> Result<ProofReplayTraceArtifact> {
    let stem = sanitize_artifact_stem(stem)?;
    let filename = format!("{stem}.trace-benchmarks.json");
    let contents = benchmarks.to_json();
    Ok(ProofReplayTraceArtifact {
        filename,
        artifact: PROOF_REPLAY_TRACE_BENCHMARK_ARTIFACT.to_string(),
        version: PROOF_REPLAY_TRACE_BENCHMARK_VERSION,
        format: "json".to_string(),
        digest: proof_replay_artifact_digest(&contents),
    })
}

pub fn proof_replay_trace_benchmark_json(benchmarks: &ProofReplayTraceBenchmarkSet) -> String {
    benchmarks.to_json()
}

pub fn proof_assistant_replay_skeleton_artifact(
    stem: &str,
    contents: &str,
) -> Result<ProofReplayTraceArtifact> {
    let stem = sanitize_artifact_stem(stem)?;
    let filename = format!("{stem}.proof-replay.lean");
    verify_proof_assistant_replay_skeleton_contents(contents)?;
    Ok(ProofReplayTraceArtifact {
        filename,
        artifact: PROOF_ASSISTANT_REPLAY_SKELETON_ARTIFACT.to_string(),
        version: PROOF_ASSISTANT_REPLAY_SKELETON_VERSION,
        format: "lean".to_string(),
        digest: proof_replay_artifact_digest(contents),
    })
}

pub fn proof_assistant_lean_checkable_artifact(
    stem: &str,
    contents: &str,
) -> Result<ProofReplayTraceArtifact> {
    let stem = sanitize_artifact_stem(stem)?;
    let filename = format!("{stem}.lean-checkable.lean");
    verify_proof_assistant_lean_checkable_contents(contents)?;
    Ok(ProofReplayTraceArtifact {
        filename,
        artifact: PROOF_ASSISTANT_LEAN_CHECKABLE_ARTIFACT.to_string(),
        version: PROOF_ASSISTANT_LEAN_CHECKABLE_VERSION,
        format: "lean".to_string(),
        digest: proof_replay_artifact_digest(contents),
    })
}

pub fn proof_assistant_replay_summary(
    filename: &str,
    contents: &str,
) -> Result<ProofAssistantReplaySummary> {
    sanitize_artifact_stem(filename.trim_end_matches(".proof-replay.lean"))?;
    verify_proof_assistant_replay_skeleton_contents(contents)?;
    let dialect = proof_assistant_skeleton_line_value(contents, "dialect")
        .ok_or_else(|| Error::verification("proof assistant replay skeleton missing dialect"))?;
    let plan_fingerprint = proof_assistant_skeleton_line_value(contents, "plan_fingerprint")
        .ok_or_else(|| {
            Error::verification("proof assistant replay skeleton missing plan_fingerprint")
        })?;
    let plan_fingerprint = if plan_fingerprint == "null" {
        None
    } else if is_valid_artifact_digest(&plan_fingerprint) {
        Some(plan_fingerprint)
    } else {
        return Err(Error::verification(
            "proof assistant replay skeleton plan_fingerprint must be null or sha256 digest",
        ));
    };
    let theorems = proof_assistant_replay_theorem_summaries(contents)?;
    let theorem_count = theorems.len();
    if theorem_count == 0 {
        return Err(Error::verification(
            "proof assistant replay skeleton must declare at least one theorem axiom",
        ));
    }
    Ok(ProofAssistantReplaySummary {
        dialect,
        plan_fingerprint,
        filename: filename.to_string(),
        adapter_registry_filename: String::new(),
        adapter_registry_digest: String::new(),
        theorem_count,
        theorems,
    })
}

pub fn proof_assistant_replay_summary_with_adapter_registry(
    filename: &str,
    contents: &str,
    adapter_registry_artifact: &ProofReplayTraceArtifact,
) -> Result<ProofAssistantReplaySummary> {
    let mut summary = proof_assistant_replay_summary(filename, contents)?;
    verify_proof_replay_trace_artifact(adapter_registry_artifact)?;
    if adapter_registry_artifact.artifact != PROOF_ASSISTANT_ADAPTER_REGISTRY_ARTIFACT
        || adapter_registry_artifact.version != PROOF_ASSISTANT_ADAPTER_REGISTRY_VERSION
        || adapter_registry_artifact.format != "json"
    {
        return Err(Error::verification(
            "proof assistant replay summary requires an adapter registry artifact",
        ));
    }
    summary.adapter_registry_filename = adapter_registry_artifact.filename.clone();
    summary.adapter_registry_digest = adapter_registry_artifact.digest.clone();
    Ok(summary)
}

pub fn proof_assistant_replay_summary_with_adapter_capability(
    summary: &ProofAssistantReplaySummary,
    capability: &ProofAssistantAdapterCapability,
) -> Result<ProofAssistantReplaySummary> {
    verify_proof_assistant_replay_summary(summary)?;
    verify_proof_assistant_adapter_capability_record(capability)?;
    let mut summary = summary.clone();
    let capability_fingerprint = proof_assistant_adapter_capability_fingerprint(capability);
    for theorem in &mut summary.theorems {
        theorem.adapter_backend = capability.adapter_backend.clone();
        theorem.checker_version = capability.checker_version.clone();
        theorem.proof_status = capability.proof_status.clone();
        theorem.adapter_capability_fingerprint = capability_fingerprint.clone();
    }
    verify_proof_assistant_replay_summary(&summary)?;
    Ok(summary)
}

pub fn proof_replay_trace_manifest_json(manifest: &ProofReplayTraceManifest) -> String {
    manifest.to_json()
}

pub fn proof_assistant_adapter_capabilities() -> Vec<ProofAssistantAdapterCapability> {
    vec![proof_assistant_skeleton_adapter_capability()]
}

pub fn proof_assistant_skeleton_adapter_capability() -> ProofAssistantAdapterCapability {
    ProofAssistantAdapterCapability {
        adapter_backend: PROOF_ASSISTANT_REPLAY_ADAPTER_BACKEND.to_string(),
        checker_version: PROOF_ASSISTANT_REPLAY_CHECKER_VERSION.to_string(),
        proof_status: PROOF_ASSISTANT_REPLAY_PROOF_STATUS.to_string(),
        native_checked: false,
        admission_artifact_digest: None,
    }
}

pub fn proof_assistant_native_checked_adapter_capability(
    adapter_backend: &str,
    checker_version: &str,
    admission_artifact_digest: &str,
) -> Result<ProofAssistantAdapterCapability> {
    let adapter_backend = sanitize_artifact_stem(adapter_backend)?;
    if checker_version.trim().is_empty()
        || checker_version.contains('"')
        || checker_version.contains('\n')
        || checker_version.contains('\r')
    {
        return Err(Error::verification(
            "proof assistant native adapter checker_version must be a non-empty single-line string",
        ));
    }
    if !is_valid_artifact_digest(admission_artifact_digest) {
        return Err(Error::verification(
            "proof assistant native adapter admission_artifact_digest must be a sha256 digest",
        ));
    }
    Ok(ProofAssistantAdapterCapability {
        adapter_backend,
        checker_version: checker_version.to_string(),
        proof_status: "native_checked".to_string(),
        native_checked: true,
        admission_artifact_digest: Some(admission_artifact_digest.to_string()),
    })
}

pub fn proof_assistant_native_admission(
    plan_fingerprint: Option<&str>,
    adapter_backend: &str,
    checker_version: &str,
    checked_theorem_count: usize,
    result_status: &str,
    theorem_result_fingerprints: Vec<String>,
    admission_claim: &str,
    evidence: &str,
) -> Result<ProofAssistantNativeAdmission> {
    if let Some(fingerprint) = plan_fingerprint {
        if !is_valid_artifact_digest(fingerprint) {
            return Err(Error::verification(
                "proof assistant native admission plan_fingerprint must be a sha256 digest",
            ));
        }
    }
    let adapter_backend = sanitize_artifact_stem(adapter_backend)?;
    if checker_version.trim().is_empty()
        || checker_version.contains('"')
        || checker_version.contains('\n')
        || checker_version.contains('\r')
    {
        return Err(Error::verification(
            "proof assistant native admission checker_version must be a non-empty single-line string",
        ));
    }
    if admission_claim.trim().is_empty()
        || admission_claim.contains('"')
        || admission_claim.contains('\n')
        || admission_claim.contains('\r')
    {
        return Err(Error::verification(
            "proof assistant native admission claim must be a non-empty single-line string",
        ));
    }
    if checked_theorem_count == 0 {
        return Err(Error::verification(
            "proof assistant native admission checked_theorem_count must be positive",
        ));
    }
    if result_status != "accepted" {
        return Err(Error::verification(
            "proof assistant native admission result_status must be accepted",
        ));
    }
    if theorem_result_fingerprints.len() != checked_theorem_count {
        return Err(Error::verification(
            "proof assistant native admission theorem_result_fingerprints length must match checked_theorem_count",
        ));
    }
    if theorem_result_fingerprints
        .iter()
        .any(|fingerprint| !is_valid_artifact_digest(fingerprint))
    {
        return Err(Error::verification(
            "proof assistant native admission theorem_result_fingerprints must be sha256 digests",
        ));
    }
    if evidence.trim().is_empty() {
        return Err(Error::verification(
            "proof assistant native admission evidence must not be empty",
        ));
    }
    Ok(ProofAssistantNativeAdmission {
        plan_fingerprint: plan_fingerprint.map(str::to_string),
        adapter_backend,
        checker_version: checker_version.to_string(),
        checked_theorem_count,
        result_status: result_status.to_string(),
        theorem_result_fingerprints,
        admission_claim: admission_claim.to_string(),
        evidence_digest: proof_replay_artifact_digest(evidence),
    })
}

pub fn proof_assistant_checker_output(
    plan_fingerprint: &str,
    artifact: &ProofReplayTraceArtifact,
    transcript: &ProofAssistantCheckerTranscript,
    adapter_backend: &str,
    checker_version: &str,
    checked_theorem_count: usize,
    result_status: &str,
) -> Result<ProofAssistantCheckerOutput> {
    if artifact.artifact != PROOF_ASSISTANT_LEAN_CHECKABLE_ARTIFACT
        || artifact.version != PROOF_ASSISTANT_LEAN_CHECKABLE_VERSION
        || artifact.format != "lean"
    {
        return Err(Error::verification(
            "proof assistant checker output must reference a Lean checkable artifact",
        ));
    }
    verify_proof_assistant_checker_transcript(transcript)?;
    if transcript.plan_fingerprint != plan_fingerprint
        || transcript.artifact_filename != artifact.filename
        || transcript.artifact_digest != artifact.digest
        || transcript.result_status != result_status
    {
        return Err(Error::verification(
            "proof assistant checker output transcript does not match Lean checkable artifact",
        ));
    }
    let adapter_backend = sanitize_artifact_stem(adapter_backend)?;
    let output = ProofAssistantCheckerOutput {
        plan_fingerprint: plan_fingerprint.to_string(),
        artifact_filename: artifact.filename.clone(),
        artifact_digest: artifact.digest.clone(),
        transcript_digest: proof_replay_artifact_digest(&proof_assistant_checker_transcript_json(
            transcript,
        )),
        adapter_backend,
        checker_version: checker_version.to_string(),
        checked_theorem_count,
        result_status: result_status.to_string(),
    };
    verify_proof_assistant_checker_output(&output)?;
    Ok(output)
}

pub fn proof_assistant_checker_transcript(
    plan_fingerprint: &str,
    artifact: &ProofReplayTraceArtifact,
    checker_command: &str,
    exit_status: i32,
    stdout: &str,
    stderr: &str,
    result_status: &str,
) -> Result<ProofAssistantCheckerTranscript> {
    if artifact.artifact != PROOF_ASSISTANT_LEAN_CHECKABLE_ARTIFACT
        || artifact.version != PROOF_ASSISTANT_LEAN_CHECKABLE_VERSION
        || artifact.format != "lean"
    {
        return Err(Error::verification(
            "proof assistant checker transcript must reference a Lean checkable artifact",
        ));
    }
    let transcript = ProofAssistantCheckerTranscript {
        plan_fingerprint: plan_fingerprint.to_string(),
        checker_command: checker_command.to_string(),
        artifact_filename: artifact.filename.clone(),
        artifact_digest: artifact.digest.clone(),
        exit_status,
        stdout_digest: proof_replay_artifact_digest(stdout),
        stderr_digest: proof_replay_artifact_digest(stderr),
        result_status: result_status.to_string(),
    };
    verify_proof_assistant_checker_transcript(&transcript)?;
    Ok(transcript)
}

pub fn proof_assistant_checker_transcript_json(
    transcript: &ProofAssistantCheckerTranscript,
) -> String {
    transcript.to_json()
}

pub fn proof_assistant_checker_transcript_artifact(
    stem: &str,
    transcript: &ProofAssistantCheckerTranscript,
) -> Result<ProofReplayTraceArtifact> {
    verify_proof_assistant_checker_transcript(transcript)?;
    let stem = sanitize_artifact_stem(stem)?;
    let filename = format!("{stem}.checker-transcript.json");
    let contents = proof_assistant_checker_transcript_json(transcript);
    Ok(ProofReplayTraceArtifact {
        filename,
        artifact: PROOF_ASSISTANT_CHECKER_TRANSCRIPT_ARTIFACT.to_string(),
        version: PROOF_ASSISTANT_CHECKER_TRANSCRIPT_VERSION,
        format: "json".to_string(),
        digest: proof_replay_artifact_digest(&contents),
    })
}

pub fn proof_assistant_checker_output_json(output: &ProofAssistantCheckerOutput) -> String {
    output.to_json()
}

pub fn proof_assistant_checker_output_artifact(
    stem: &str,
    output: &ProofAssistantCheckerOutput,
) -> Result<ProofReplayTraceArtifact> {
    verify_proof_assistant_checker_output(output)?;
    let stem = sanitize_artifact_stem(stem)?;
    let filename = format!("{stem}.checker-output.json");
    let contents = proof_assistant_checker_output_json(output);
    Ok(ProofReplayTraceArtifact {
        filename,
        artifact: PROOF_ASSISTANT_CHECKER_OUTPUT_ARTIFACT.to_string(),
        version: PROOF_ASSISTANT_CHECKER_OUTPUT_VERSION,
        format: "json".to_string(),
        digest: proof_replay_artifact_digest(&contents),
    })
}

pub fn proof_assistant_native_admission_from_checker_output(
    output: &ProofAssistantCheckerOutput,
    theorem_result_fingerprints: Vec<String>,
    admission_claim: &str,
) -> Result<ProofAssistantNativeAdmission> {
    let evidence_json = proof_assistant_checker_output_json(output);
    proof_assistant_native_admission(
        Some(&output.plan_fingerprint),
        &output.adapter_backend,
        &output.checker_version,
        output.checked_theorem_count,
        &output.result_status,
        theorem_result_fingerprints,
        admission_claim,
        &evidence_json,
    )
}

pub fn proof_assistant_native_theorem_result_fingerprint(
    theorem: &ProofAssistantReplayTheoremSummary,
) -> String {
    proof_replay_artifact_digest(&format!(
        "theorem_id={}\noriginal_id={}\nkind={}\nstatus={}\nreplay_rule={}\nstatement_fingerprint={}\n",
        theorem.theorem_id,
        theorem.original_id,
        theorem.kind,
        theorem.status,
        theorem.replay_rule,
        theorem.statement_fingerprint
    ))
}

pub fn proof_assistant_native_admission_json(admission: &ProofAssistantNativeAdmission) -> String {
    admission.to_json()
}

pub fn proof_assistant_native_admission_artifact(
    stem: &str,
    admission: &ProofAssistantNativeAdmission,
) -> Result<ProofReplayTraceArtifact> {
    verify_proof_assistant_native_admission(admission)?;
    let stem = sanitize_artifact_stem(stem)?;
    let filename = format!("{stem}.native-admission.json");
    let contents = proof_assistant_native_admission_json(admission);
    Ok(ProofReplayTraceArtifact {
        filename,
        artifact: PROOF_ASSISTANT_NATIVE_ADMISSION_ARTIFACT.to_string(),
        version: PROOF_ASSISTANT_NATIVE_ADMISSION_VERSION,
        format: "json".to_string(),
        digest: proof_replay_artifact_digest(&contents),
    })
}

pub fn checker_result_index(
    plan_fingerprint: &str,
    summary: &ProofAssistantReplaySummary,
    registry: &ProofAssistantAdapterRegistry,
) -> Result<CheckerResultIndex> {
    if !is_valid_artifact_digest(plan_fingerprint) {
        return Err(Error::verification(
            "checker result index plan_fingerprint must be a sha256 digest",
        ));
    }
    if summary.plan_fingerprint.as_deref() != Some(plan_fingerprint) {
        return Err(Error::verification(
            "checker result index summary plan_fingerprint must match index plan_fingerprint",
        ));
    }
    if registry.plan_fingerprint.as_deref() != Some(plan_fingerprint) {
        return Err(Error::verification(
            "checker result index registry plan_fingerprint must match index plan_fingerprint",
        ));
    }
    verify_proof_assistant_summary_matches_adapter_registry(summary, registry)?;
    let mut entries = Vec::new();
    for theorem in &summary.theorems {
        let capability = registry
            .capabilities
            .iter()
            .find(|capability| {
                verify_proof_assistant_theorem_matches_adapter_capability(theorem, capability)
                    .is_ok()
            })
            .ok_or_else(|| {
                Error::verification(
                    "checker result index theorem is not backed by adapter registry capability",
                )
            })?;
        if !capability.native_checked {
            continue;
        }
        let Some(admission_artifact_digest) = &capability.admission_artifact_digest else {
            return Err(Error::verification(
                "checker result index native capability requires admission_artifact_digest",
            ));
        };
        entries.push(CheckerResultEntry {
            theorem_id: theorem.theorem_id.clone(),
            theorem_result_fingerprint: proof_assistant_native_theorem_result_fingerprint(theorem),
            adapter_capability_fingerprint: theorem.adapter_capability_fingerprint.clone(),
            admission_artifact_digest: admission_artifact_digest.clone(),
            plan_fingerprint: plan_fingerprint.to_string(),
        });
    }
    let index = CheckerResultIndex {
        plan_fingerprint: plan_fingerprint.to_string(),
        entry_count: entries.len(),
        entries,
    };
    verify_checker_result_index(&index)?;
    Ok(index)
}

pub fn checker_result_index_json(index: &CheckerResultIndex) -> String {
    index.to_json()
}

pub fn checker_result_index_artifact(
    stem: &str,
    index: &CheckerResultIndex,
) -> Result<ProofReplayTraceArtifact> {
    verify_checker_result_index(index)?;
    let stem = sanitize_artifact_stem(stem)?;
    let filename = format!("{stem}.checker-results.json");
    let contents = checker_result_index_json(index);
    Ok(ProofReplayTraceArtifact {
        filename,
        artifact: PROOF_ASSISTANT_CHECKER_RESULT_INDEX_ARTIFACT.to_string(),
        version: PROOF_ASSISTANT_CHECKER_RESULT_INDEX_VERSION,
        format: "json".to_string(),
        digest: proof_replay_artifact_digest(&contents),
    })
}

pub fn proof_assistant_native_checked_adapter_capability_from_admission(
    admission: &ProofAssistantNativeAdmission,
) -> Result<ProofAssistantAdapterCapability> {
    proof_assistant_native_checked_adapter_capability(
        &admission.adapter_backend,
        &admission.checker_version,
        &proof_replay_artifact_digest(&proof_assistant_native_admission_json(admission)),
    )
}

pub fn proof_assistant_adapter_capability_fingerprint(
    capability: &ProofAssistantAdapterCapability,
) -> String {
    proof_replay_artifact_digest(&format!(
        "adapter_backend={}\nchecker_version={}\nproof_status={}\nnative_checked={}\nadmission_artifact_digest={}\n",
        capability.adapter_backend,
        capability.checker_version,
        capability.proof_status,
        capability.native_checked,
        capability
            .admission_artifact_digest
            .as_deref()
            .unwrap_or("null")
    ))
}

pub fn proof_assistant_adapter_registry_json() -> String {
    proof_assistant_adapter_registry_json_with_plan_fingerprint(None)
}

pub fn proof_assistant_adapter_registry_json_with_plan_fingerprint(
    plan_fingerprint: Option<&str>,
) -> String {
    if let Some(fingerprint) = plan_fingerprint {
        debug_assert!(is_valid_artifact_digest(fingerprint));
    }
    proof_assistant_adapter_registry_json_for_capabilities(
        plan_fingerprint,
        &proof_assistant_adapter_capabilities(),
    )
}

pub fn proof_assistant_adapter_registry_json_for_capabilities(
    plan_fingerprint: Option<&str>,
    capabilities: &[ProofAssistantAdapterCapability],
) -> String {
    if let Some(fingerprint) = plan_fingerprint {
        debug_assert!(is_valid_artifact_digest(fingerprint));
    }
    let capabilities = capabilities
        .iter()
        .map(ProofAssistantAdapterCapability::to_json)
        .collect::<Vec<_>>()
        .join(",");
    format!(
        "{{\"artifact\":{},\"version\":{},\"plan_fingerprint\":{},\"capabilities\":[{}]}}",
        json_string(PROOF_ASSISTANT_ADAPTER_REGISTRY_ARTIFACT),
        PROOF_ASSISTANT_ADAPTER_REGISTRY_VERSION,
        json_option_string(&plan_fingerprint.map(str::to_string)),
        capabilities
    )
}

pub fn proof_assistant_adapter_registry_artifact(stem: &str) -> Result<ProofReplayTraceArtifact> {
    proof_assistant_adapter_registry_artifact_with_plan_fingerprint(stem, None)
}

pub fn proof_assistant_adapter_registry_artifact_with_plan_fingerprint(
    stem: &str,
    plan_fingerprint: Option<&str>,
) -> Result<ProofReplayTraceArtifact> {
    proof_assistant_adapter_registry_artifact_for_capabilities(
        stem,
        plan_fingerprint,
        &proof_assistant_adapter_capabilities(),
    )
}

pub fn proof_assistant_adapter_registry_artifact_for_capabilities(
    stem: &str,
    plan_fingerprint: Option<&str>,
    capabilities: &[ProofAssistantAdapterCapability],
) -> Result<ProofReplayTraceArtifact> {
    if let Some(fingerprint) = plan_fingerprint {
        if !is_valid_artifact_digest(fingerprint) {
            return Err(Error::verification(
                "proof assistant adapter registry plan_fingerprint must be a sha256 digest",
            ));
        }
    }
    for capability in capabilities {
        verify_proof_assistant_adapter_capability_record(capability)?;
    }
    let stem = sanitize_artifact_stem(stem)?;
    let filename = format!("{stem}.proof-adapters.json");
    let contents =
        proof_assistant_adapter_registry_json_for_capabilities(plan_fingerprint, capabilities);
    Ok(ProofReplayTraceArtifact {
        filename,
        artifact: PROOF_ASSISTANT_ADAPTER_REGISTRY_ARTIFACT.to_string(),
        version: PROOF_ASSISTANT_ADAPTER_REGISTRY_VERSION,
        format: "json".to_string(),
        digest: proof_replay_artifact_digest(&contents),
    })
}

pub fn parse_proof_assistant_adapter_registry_json(
    input: &str,
) -> Result<ProofAssistantAdapterRegistry> {
    let fields = parse_json_object_fields(input, "proof assistant adapter registry JSON")?;
    validate_json_object_field_set(
        &fields,
        PROOF_ASSISTANT_ADAPTER_REGISTRY_SCHEMA_FIELDS,
        "proof assistant adapter registry",
    )?;
    let artifact_literal =
        json_field_string(&fields, "artifact", "proof assistant adapter registry")?;
    if artifact_literal != PROOF_ASSISTANT_ADAPTER_REGISTRY_ARTIFACT {
        return Err(Error::verification(format!(
            "unexpected proof assistant adapter registry artifact {}",
            artifact_literal
        )));
    }
    let version = json_field_u32(&fields, "version", "proof assistant adapter registry")?;
    if version != PROOF_ASSISTANT_ADAPTER_REGISTRY_VERSION {
        return Err(Error::verification(format!(
            "unsupported proof assistant adapter registry version {}",
            version
        )));
    }
    let plan_fingerprint = json_field_option_string(
        &fields,
        "plan_fingerprint",
        "proof assistant adapter registry",
    )?;
    let capabilities = parse_proof_assistant_adapter_capabilities_from_array(json_field(
        &fields,
        "capabilities",
        "proof assistant adapter registry",
    )?)?;
    let registry = ProofAssistantAdapterRegistry {
        plan_fingerprint,
        capabilities,
    };
    verify_proof_assistant_adapter_registry(&registry)?;
    Ok(registry)
}

pub fn parse_proof_assistant_native_admission_json(
    input: &str,
) -> Result<ProofAssistantNativeAdmission> {
    let fields = parse_json_object_fields(input, "proof assistant native admission JSON")?;
    validate_json_object_field_set(
        &fields,
        PROOF_ASSISTANT_NATIVE_ADMISSION_SCHEMA_FIELDS,
        "proof assistant native admission",
    )?;
    let artifact_literal =
        json_field_string(&fields, "artifact", "proof assistant native admission")?;
    if artifact_literal != PROOF_ASSISTANT_NATIVE_ADMISSION_ARTIFACT {
        return Err(Error::verification(format!(
            "unexpected proof assistant native admission artifact {}",
            artifact_literal
        )));
    }
    let version = json_field_u32(&fields, "version", "proof assistant native admission")?;
    if version != PROOF_ASSISTANT_NATIVE_ADMISSION_VERSION {
        return Err(Error::verification(format!(
            "unsupported proof assistant native admission version {}",
            version
        )));
    }
    let plan_fingerprint = json_field_option_string(
        &fields,
        "plan_fingerprint",
        "proof assistant native admission",
    )?;
    let adapter_backend = json_field_string(
        &fields,
        "adapter_backend",
        "proof assistant native admission",
    )?;
    let checker_version = json_field_string(
        &fields,
        "checker_version",
        "proof assistant native admission",
    )?;
    let checked_theorem_count = json_field_usize(
        &fields,
        "checked_theorem_count",
        "proof assistant native admission",
    )?;
    let result_status =
        json_field_string(&fields, "result_status", "proof assistant native admission")?;
    let theorem_result_fingerprints = json_field_string_array(
        &fields,
        "theorem_result_fingerprints",
        "proof assistant native admission",
    )?;
    let admission_claim = json_field_string(
        &fields,
        "admission_claim",
        "proof assistant native admission",
    )?;
    let evidence_digest = json_field_string(
        &fields,
        "evidence_digest",
        "proof assistant native admission",
    )?;
    let admission = ProofAssistantNativeAdmission {
        plan_fingerprint,
        adapter_backend,
        checker_version,
        checked_theorem_count,
        result_status,
        theorem_result_fingerprints,
        admission_claim,
        evidence_digest,
    };
    verify_proof_assistant_native_admission(&admission)?;
    Ok(admission)
}

pub fn parse_proof_assistant_checker_output_json(
    input: &str,
) -> Result<ProofAssistantCheckerOutput> {
    let fields = parse_json_object_fields(input, "proof assistant checker output JSON")?;
    validate_json_object_field_set(
        &fields,
        PROOF_ASSISTANT_CHECKER_OUTPUT_SCHEMA_FIELDS,
        "proof assistant checker output",
    )?;
    let artifact_literal =
        json_field_string(&fields, "artifact", "proof assistant checker output")?;
    if artifact_literal != PROOF_ASSISTANT_CHECKER_OUTPUT_ARTIFACT {
        return Err(Error::verification(format!(
            "unexpected proof assistant checker output artifact {}",
            artifact_literal
        )));
    }
    let version = json_field_u32(&fields, "version", "proof assistant checker output")?;
    if version != PROOF_ASSISTANT_CHECKER_OUTPUT_VERSION {
        return Err(Error::verification(format!(
            "unsupported proof assistant checker output version {}",
            version
        )));
    }
    let plan_fingerprint = json_field_string(
        &fields,
        "plan_fingerprint",
        "proof assistant checker output",
    )?;
    let artifact_filename = json_field_string(
        &fields,
        "artifact_filename",
        "proof assistant checker output",
    )?;
    let artifact_digest =
        json_field_string(&fields, "artifact_digest", "proof assistant checker output")?;
    let transcript_digest = json_field_string(
        &fields,
        "transcript_digest",
        "proof assistant checker output",
    )?;
    let adapter_backend =
        json_field_string(&fields, "adapter_backend", "proof assistant checker output")?;
    let checker_version =
        json_field_string(&fields, "checker_version", "proof assistant checker output")?;
    let checked_theorem_count = json_field_usize(
        &fields,
        "checked_theorem_count",
        "proof assistant checker output",
    )?;
    let result_status =
        json_field_string(&fields, "result_status", "proof assistant checker output")?;
    let output = ProofAssistantCheckerOutput {
        plan_fingerprint,
        artifact_filename,
        artifact_digest,
        transcript_digest,
        adapter_backend,
        checker_version,
        checked_theorem_count,
        result_status,
    };
    verify_proof_assistant_checker_output(&output)?;
    Ok(output)
}

pub fn parse_proof_assistant_checker_transcript_json(
    input: &str,
) -> Result<ProofAssistantCheckerTranscript> {
    let fields = parse_json_object_fields(input, "proof assistant checker transcript JSON")?;
    validate_json_object_field_set(
        &fields,
        PROOF_ASSISTANT_CHECKER_TRANSCRIPT_SCHEMA_FIELDS,
        "proof assistant checker transcript",
    )?;
    let artifact_literal =
        json_field_string(&fields, "artifact", "proof assistant checker transcript")?;
    if artifact_literal != PROOF_ASSISTANT_CHECKER_TRANSCRIPT_ARTIFACT {
        return Err(Error::verification(format!(
            "unexpected proof assistant checker transcript artifact {}",
            artifact_literal
        )));
    }
    let version = json_field_u32(&fields, "version", "proof assistant checker transcript")?;
    if version != PROOF_ASSISTANT_CHECKER_TRANSCRIPT_VERSION {
        return Err(Error::verification(format!(
            "unsupported proof assistant checker transcript version {}",
            version
        )));
    }
    let plan_fingerprint = json_field_string(
        &fields,
        "plan_fingerprint",
        "proof assistant checker transcript",
    )?;
    let checker_command = json_field_string(
        &fields,
        "checker_command",
        "proof assistant checker transcript",
    )?;
    let artifact_filename = json_field_string(
        &fields,
        "artifact_filename",
        "proof assistant checker transcript",
    )?;
    let artifact_digest = json_field_string(
        &fields,
        "artifact_digest",
        "proof assistant checker transcript",
    )?;
    let exit_status = json_field_i32(&fields, "exit_status", "proof assistant checker transcript")?;
    let stdout_digest = json_field_string(
        &fields,
        "stdout_digest",
        "proof assistant checker transcript",
    )?;
    let stderr_digest = json_field_string(
        &fields,
        "stderr_digest",
        "proof assistant checker transcript",
    )?;
    let result_status = json_field_string(
        &fields,
        "result_status",
        "proof assistant checker transcript",
    )?;
    let transcript = ProofAssistantCheckerTranscript {
        plan_fingerprint,
        checker_command,
        artifact_filename,
        artifact_digest,
        exit_status,
        stdout_digest,
        stderr_digest,
        result_status,
    };
    verify_proof_assistant_checker_transcript(&transcript)?;
    Ok(transcript)
}

pub fn parse_checker_result_index_json(input: &str) -> Result<CheckerResultIndex> {
    let fields = parse_json_object_fields(input, "checker result index JSON")?;
    validate_json_object_field_set(
        &fields,
        PROOF_ASSISTANT_CHECKER_RESULT_INDEX_SCHEMA_FIELDS,
        "checker result index",
    )?;
    let artifact_literal = json_field_string(&fields, "artifact", "checker result index")?;
    if artifact_literal != PROOF_ASSISTANT_CHECKER_RESULT_INDEX_ARTIFACT {
        return Err(Error::verification(format!(
            "unexpected checker result index artifact {}",
            artifact_literal
        )));
    }
    let version = json_field_u32(&fields, "version", "checker result index")?;
    if version != PROOF_ASSISTANT_CHECKER_RESULT_INDEX_VERSION {
        return Err(Error::verification(format!(
            "unsupported checker result index version {}",
            version
        )));
    }
    let plan_fingerprint = json_field_string(&fields, "plan_fingerprint", "checker result index")?;
    let entry_count = json_field_usize(&fields, "entry_count", "checker result index")?;
    let entries = parse_checker_result_entries_from_array(json_field(
        &fields,
        "entries",
        "checker result index",
    )?)?;
    let index = CheckerResultIndex {
        plan_fingerprint,
        entry_count,
        entries,
    };
    verify_checker_result_index(&index)?;
    Ok(index)
}

pub fn parse_proof_replay_trace_manifest_json(input: &str) -> Result<ProofReplayTraceManifest> {
    let fields = parse_json_object_fields(input, "proof replay trace manifest JSON")?;
    validate_json_object_field_set(
        &fields,
        PROOF_REPLAY_TRACE_MANIFEST_SCHEMA_FIELDS,
        "proof replay trace manifest",
    )?;
    let artifact_literal = json_field_string(&fields, "artifact", "proof replay trace manifest")?;
    if artifact_literal != PROOF_REPLAY_TRACE_MANIFEST_ARTIFACT {
        return Err(Error::verification(format!(
            "unexpected proof replay trace manifest artifact {}",
            artifact_literal
        )));
    }
    let version = json_field_u32(&fields, "version", "proof replay trace manifest")?;
    if version != PROOF_REPLAY_TRACE_MANIFEST_VERSION {
        return Err(Error::verification(format!(
            "unsupported proof replay trace manifest version {}",
            version
        )));
    }
    let trace_name = json_field_string(&fields, "trace_name", "proof replay trace manifest")?;
    let plan_fingerprint =
        json_field_option_string(&fields, "plan_fingerprint", "proof replay trace manifest")?;
    let artifacts = parse_proof_replay_trace_artifacts_from_array(json_field(
        &fields,
        "artifacts",
        "proof replay trace manifest",
    )?)?;
    let proof_assistant = parse_proof_assistant_replay_summary_value(json_field(
        &fields,
        "proof_assistant",
        "proof replay trace manifest",
    )?)?;
    let tuning = parse_proof_replay_trace_tuning_value(json_field(
        &fields,
        "tuning",
        "proof replay trace manifest",
    )?)?;
    let signature = parse_proof_replay_trace_signature(json_field(
        &fields,
        "signature",
        "proof replay trace manifest",
    )?)?;
    let manifest = ProofReplayTraceManifest {
        trace_name,
        plan_fingerprint,
        artifacts,
        proof_assistant,
        tuning,
        signature,
    };
    verify_proof_replay_trace_manifest(&manifest)?;
    Ok(manifest)
}

pub fn verify_proof_replay_trace_manifest(manifest: &ProofReplayTraceManifest) -> Result<()> {
    sanitize_artifact_stem(&manifest.trace_name)?;
    if manifest.artifacts.is_empty() {
        return Err(Error::verification(
            "proof replay trace manifest must include at least one artifact",
        ));
    }
    for artifact in &manifest.artifacts {
        verify_proof_replay_trace_artifact(artifact)?;
    }
    if let Some(fingerprint) = &manifest.plan_fingerprint {
        if !is_valid_artifact_digest(fingerprint) {
            return Err(Error::verification(
                "proof replay trace manifest plan_fingerprint must be a sha256 digest",
            ));
        }
    }
    if let Some(tuning) = &manifest.tuning {
        verify_proof_replay_trace_tuning(tuning)?;
    }
    if let Some(summary) = &manifest.proof_assistant {
        verify_proof_assistant_replay_summary(summary)?;
    }
    if let Some(signature) = &manifest.signature {
        verify_proof_replay_trace_signature_shape(signature)?;
    }
    Ok(())
}

pub fn sign_proof_replay_trace_manifest(
    manifest: &ProofReplayTraceManifest,
    key_id: &str,
    key_secret: &str,
) -> Result<ProofReplayTraceManifest> {
    if key_secret.is_empty() {
        return Err(Error::verification(
            "proof replay trace signature requires nonempty key id and secret",
        ));
    }
    let key_id = sanitize_artifact_stem(key_id)?;
    let mut signed = manifest.clone();
    signed.signature = None;
    verify_proof_replay_trace_manifest(&signed)?;
    let value = proof_replay_trace_signature_value(&signed, &key_id, key_secret);
    signed.signature = Some(ProofReplayTraceSignature {
        key_fingerprint: proof_replay_trace_key_fingerprint(&key_id, key_secret),
        key_id,
        key_kind: "shared-secret".to_string(),
        algorithm: PROOF_REPLAY_TRACE_SIGNATURE_ALGORITHM.to_string(),
        value,
    });
    Ok(signed)
}

pub fn sign_proof_replay_trace_manifest_ed25519(
    manifest: &ProofReplayTraceManifest,
    key_id: &str,
    signing_key_bytes: &[u8; 32],
) -> Result<ProofReplayTraceManifest> {
    #[cfg(not(feature = "ed25519"))]
    {
        let _ = (manifest, key_id, signing_key_bytes);
        return Err(Error::verification(
            "ed25519 proof replay trace signature support requires the ed25519 feature",
        ));
    }
    #[cfg(feature = "ed25519")]
    {
        let key_id = sanitize_artifact_stem(key_id)?;
        let mut signed = manifest.clone();
        signed.signature = None;
        verify_proof_replay_trace_manifest(&signed)?;
        let signing_key = ed25519_dalek::SigningKey::from_bytes(signing_key_bytes);
        let verifying_key = signing_key.verifying_key();
        let signature = signing_key.sign(proof_replay_trace_public_key_payload(&signed).as_bytes());
        signed.signature = Some(ProofReplayTraceSignature {
            key_fingerprint: proof_replay_trace_public_key_fingerprint(verifying_key.as_bytes()),
            key_id,
            key_kind: "ed25519-public".to_string(),
            algorithm: PROOF_REPLAY_TRACE_PUBLIC_KEY_SIGNATURE_ALGORITHM.to_string(),
            value: ed25519_signature_value(&signature.to_bytes()),
        });
        Ok(signed)
    }
}

pub fn verify_proof_replay_trace_manifest_signature(
    manifest: &ProofReplayTraceManifest,
    key_secret: &str,
) -> Result<()> {
    let Some(signature) = &manifest.signature else {
        return Err(Error::verification(
            "proof replay trace manifest is not signed",
        ));
    };
    verify_proof_replay_trace_manifest_signature_with_key(
        manifest,
        &ProofReplayTraceVerificationKey::SharedSecret {
            key_id: signature.key_id.clone(),
            secret: key_secret.to_string(),
        },
    )
}

pub fn verify_proof_replay_trace_manifest_signature_with_key(
    manifest: &ProofReplayTraceManifest,
    verification_key: &ProofReplayTraceVerificationKey,
) -> Result<()> {
    verify_proof_replay_trace_manifest(manifest)?;
    let Some(signature) = &manifest.signature else {
        return Err(Error::verification(
            "proof replay trace manifest is not signed",
        ));
    };
    let mut unsigned = manifest.clone();
    unsigned.signature = None;
    match verification_key {
        ProofReplayTraceVerificationKey::SharedSecret { key_id, secret } => {
            if secret.is_empty() {
                return Err(Error::verification(
                    "proof replay trace signature verification requires nonempty secret",
                ));
            }
            if signature.key_kind != "shared-secret"
                || signature.algorithm != PROOF_REPLAY_TRACE_SIGNATURE_ALGORITHM
            {
                return Err(Error::verification(
                    "proof replay trace signature is not a shared-secret signature",
                ));
            }
            if &signature.key_id != key_id {
                return Err(Error::verification(
                    "proof replay trace signature key_id does not match verification key",
                ));
            }
            let expected_fingerprint = proof_replay_trace_key_fingerprint(key_id, secret);
            if signature.key_fingerprint != expected_fingerprint {
                return Err(Error::verification(
                    "proof replay trace signature key_fingerprint does not match verification key",
                ));
            }
            let expected = proof_replay_trace_signature_value(&unsigned, key_id, secret);
            if signature.value != expected {
                return Err(Error::verification(
                    "proof replay trace manifest signature mismatch",
                ));
            }
        }
        ProofReplayTraceVerificationKey::Ed25519PublicKey {
            key_id,
            public_key_fingerprint,
            public_key_hex,
        } => {
            if signature.key_kind != "ed25519-public"
                || signature.algorithm != PROOF_REPLAY_TRACE_PUBLIC_KEY_SIGNATURE_ALGORITHM
            {
                return Err(Error::verification(
                    "proof replay trace signature is not an ed25519 public-key signature",
                ));
            }
            if &signature.key_id != key_id || &signature.key_fingerprint != public_key_fingerprint {
                return Err(Error::verification(
                    "proof replay trace signature public key metadata does not match verification key",
                ));
            }
            let public_key_bytes = parse_ed25519_public_key_hex(public_key_hex)?;
            let expected_fingerprint = proof_replay_trace_public_key_fingerprint(&public_key_bytes);
            if &expected_fingerprint != public_key_fingerprint {
                return Err(Error::verification(
                    "proof replay trace signature public key fingerprint does not match verification key bytes",
                ));
            }
            #[cfg(not(feature = "ed25519"))]
            {
                return Err(Error::verification(
                    "ed25519 proof replay trace signature support requires the ed25519 feature",
                ));
            }
            #[cfg(feature = "ed25519")]
            {
                let verifying_key = VerifyingKey::from_bytes(&public_key_bytes).map_err(|_| {
                    Error::verification("invalid ed25519 proof replay trace public key bytes")
                })?;
                let signature_bytes = parse_ed25519_signature_value(&signature.value)?;
                let ed25519_signature = Signature::from_bytes(&signature_bytes);
                verifying_key
                    .verify(
                        proof_replay_trace_public_key_payload(&unsigned).as_bytes(),
                        &ed25519_signature,
                    )
                    .map_err(|_| {
                        Error::verification(
                            "ed25519 proof replay trace manifest signature mismatch",
                        )
                    })?;
            }
        }
    }
    Ok(())
}

fn parse_proof_replay_trace_artifacts_from_array(
    input: &str,
) -> Result<Vec<ProofReplayTraceArtifact>> {
    parse_json_array_items(input, "proof replay trace artifacts")?
        .iter()
        .map(|item| parse_proof_replay_trace_artifact(item))
        .collect()
}

fn parse_proof_assistant_adapter_capabilities_from_array(
    input: &str,
) -> Result<Vec<ProofAssistantAdapterCapability>> {
    parse_json_array_items(input, "proof assistant adapter capabilities")?
        .iter()
        .map(|item| parse_proof_assistant_adapter_capability(item))
        .collect()
}

fn parse_checker_result_entries_from_array(input: &str) -> Result<Vec<CheckerResultEntry>> {
    parse_json_array_items(input, "checker result entries")?
        .iter()
        .map(|item| parse_checker_result_entry(item))
        .collect()
}

fn parse_checker_result_entry(input: &str) -> Result<CheckerResultEntry> {
    let object = json_object_input(input);
    let fields = parse_json_object_fields(&object, "checker result entry")?;
    validate_json_object_field_set(
        &fields,
        PROOF_ASSISTANT_CHECKER_RESULT_ENTRY_SCHEMA_FIELDS,
        "checker result entry",
    )?;
    let theorem_id = json_field_string(&fields, "theorem_id", "checker result entry")?;
    let theorem_result_fingerprint = json_field_string(
        &fields,
        "theorem_result_fingerprint",
        "checker result entry",
    )?;
    let adapter_capability_fingerprint = json_field_string(
        &fields,
        "adapter_capability_fingerprint",
        "checker result entry",
    )?;
    let admission_artifact_digest =
        json_field_string(&fields, "admission_artifact_digest", "checker result entry")?;
    let plan_fingerprint = json_field_string(&fields, "plan_fingerprint", "checker result entry")?;
    Ok(CheckerResultEntry {
        theorem_id,
        theorem_result_fingerprint,
        adapter_capability_fingerprint,
        admission_artifact_digest,
        plan_fingerprint,
    })
}

fn parse_proof_assistant_adapter_capability(
    input: &str,
) -> Result<ProofAssistantAdapterCapability> {
    let object = json_object_input(input);
    let fields = parse_json_object_fields(&object, "proof assistant adapter capability")?;
    validate_json_object_field_set(
        &fields,
        PROOF_ASSISTANT_ADAPTER_CAPABILITY_SCHEMA_FIELDS,
        "proof assistant adapter capability",
    )?;
    let adapter_backend = json_field_string(
        &fields,
        "adapter_backend",
        "proof assistant adapter capability",
    )?;
    let checker_version = json_field_string(
        &fields,
        "checker_version",
        "proof assistant adapter capability",
    )?;
    let proof_status = json_field_string(
        &fields,
        "proof_status",
        "proof assistant adapter capability",
    )?;
    let native_checked = json_field_bool(
        &fields,
        "native_checked",
        "proof assistant adapter capability",
    )?;
    let admission_artifact_digest = json_field_option_string(
        &fields,
        "admission_artifact_digest",
        "proof assistant adapter capability",
    )?;
    let capability_fingerprint = json_field_string(
        &fields,
        "capability_fingerprint",
        "proof assistant adapter capability",
    )?;
    let capability = ProofAssistantAdapterCapability {
        adapter_backend,
        checker_version,
        proof_status,
        native_checked,
        admission_artifact_digest,
    };
    verify_proof_assistant_adapter_capability_record(&capability)?;
    if capability_fingerprint != proof_assistant_adapter_capability_fingerprint(&capability) {
        return Err(Error::verification(
            "proof assistant adapter capability fingerprint mismatch",
        ));
    }
    Ok(capability)
}

fn parse_proof_assistant_replay_summary_value(
    input: &str,
) -> Result<Option<ProofAssistantReplaySummary>> {
    if input == "null" {
        return Ok(None);
    }
    let fields = parse_json_object_fields(input, "proof assistant replay summary")?;
    validate_json_object_field_set(
        &fields,
        PROOF_ASSISTANT_REPLAY_SUMMARY_SCHEMA_FIELDS,
        "proof assistant replay summary",
    )?;
    let dialect = json_field_string(&fields, "dialect", "proof assistant replay summary")?;
    let plan_fingerprint = json_field_option_string(
        &fields,
        "plan_fingerprint",
        "proof assistant replay summary",
    )?;
    let filename = json_field_string(&fields, "filename", "proof assistant replay summary")?;
    let adapter_registry_filename = json_field_string(
        &fields,
        "adapter_registry_filename",
        "proof assistant replay summary",
    )?;
    let adapter_registry_digest = json_field_string(
        &fields,
        "adapter_registry_digest",
        "proof assistant replay summary",
    )?;
    let theorem_count =
        json_field_usize(&fields, "theorem_count", "proof assistant replay summary")?;
    let theorems = parse_proof_assistant_replay_theorem_summaries_from_array(json_field(
        &fields,
        "theorems",
        "proof assistant replay summary",
    )?)?;
    Ok(Some(ProofAssistantReplaySummary {
        dialect,
        plan_fingerprint,
        filename,
        adapter_registry_filename,
        adapter_registry_digest,
        theorem_count,
        theorems,
    }))
}

fn parse_proof_replay_trace_tuning_value(input: &str) -> Result<Option<ProofReplayTraceTuning>> {
    if input == "null" {
        return Ok(None);
    }
    let fields = parse_json_object_fields(input, "proof replay trace tuning")?;
    validate_json_object_field_set(
        &fields,
        &PROOF_REPLAY_TRACE_TUNING_SCHEMA_FIELDS[2..],
        "proof replay trace tuning",
    )?;
    parse_proof_replay_trace_tuning_from_fields(&fields, "proof replay trace tuning").map(Some)
}

pub fn parse_proof_replay_trace_tuning_json(input: &str) -> Result<ProofReplayTraceTuning> {
    let fields = parse_json_object_fields(input, "proof replay trace tuning JSON")?;
    validate_json_object_field_set(
        &fields,
        PROOF_REPLAY_TRACE_TUNING_SCHEMA_FIELDS,
        "proof replay trace tuning",
    )?;
    let artifact_literal = json_field_string(&fields, "artifact", "proof replay trace tuning")?;
    if artifact_literal != PROOF_REPLAY_TRACE_TUNING_ARTIFACT {
        return Err(Error::verification(format!(
            "unexpected proof replay trace tuning artifact {}",
            artifact_literal
        )));
    }
    let version = json_field_u32(&fields, "version", "proof replay trace tuning")?;
    if version != PROOF_REPLAY_TRACE_TUNING_VERSION {
        return Err(Error::verification(format!(
            "unsupported proof replay trace tuning version {}",
            version
        )));
    }
    let tuning = parse_proof_replay_trace_tuning_from_fields(&fields, "proof replay trace tuning")?;
    verify_proof_replay_trace_tuning(&tuning)?;
    Ok(tuning)
}

pub fn parse_proof_replay_trace_benchmark_json(
    input: &str,
) -> Result<ProofReplayTraceBenchmarkSet> {
    let fields = parse_json_object_fields(input, "proof replay trace benchmark JSON")?;
    validate_json_object_field_set(
        &fields,
        PROOF_REPLAY_TRACE_BENCHMARK_SCHEMA_FIELDS,
        "proof replay trace benchmark",
    )?;
    let artifact_literal = json_field_string(&fields, "artifact", "proof replay trace benchmark")?;
    if artifact_literal != PROOF_REPLAY_TRACE_BENCHMARK_ARTIFACT {
        return Err(Error::verification(format!(
            "unexpected proof replay trace benchmark artifact {}",
            artifact_literal
        )));
    }
    let version = json_field_u32(&fields, "version", "proof replay trace benchmark")?;
    if version != PROOF_REPLAY_TRACE_BENCHMARK_VERSION {
        return Err(Error::verification(format!(
            "unsupported proof replay trace benchmark version {}",
            version
        )));
    }
    let plan_fingerprint =
        json_field_string(&fields, "plan_fingerprint", "proof replay trace benchmark")?;
    let backend = json_field_string(&fields, "backend", "proof replay trace benchmark")?;
    let selected_strategy =
        json_field_string(&fields, "selected_strategy", "proof replay trace benchmark")?;
    let records = parse_proof_replay_trace_benchmark_records_from_array(json_field(
        &fields,
        "records",
        "proof replay trace benchmark",
    )?)?;
    let benchmarks = ProofReplayTraceBenchmarkSet {
        plan_fingerprint,
        backend,
        selected_strategy,
        records,
    };
    verify_proof_replay_trace_benchmark_set(&benchmarks)?;
    Ok(benchmarks)
}

pub fn parse_math_bound_audit_trace_json(input: &str) -> Result<MathBoundAuditTrace> {
    let fields = parse_json_object_fields(input, "math-bound audit trace JSON")?;
    validate_json_object_field_set(
        &fields,
        MATH_BOUND_AUDIT_TRACE_SCHEMA_FIELDS,
        "math-bound audit trace",
    )?;
    let artifact_literal = json_field_string(&fields, "artifact", "math-bound audit trace")?;
    if artifact_literal != MATH_BOUND_AUDIT_TRACE_ARTIFACT {
        return Err(Error::verification(format!(
            "unexpected math-bound audit trace artifact {}",
            artifact_literal
        )));
    }
    let version = json_field_u32(&fields, "version", "math-bound audit trace")?;
    if version != MATH_BOUND_AUDIT_TRACE_VERSION {
        return Err(Error::verification(format!(
            "unsupported math-bound audit trace version {}",
            version
        )));
    }
    let trace = MathBoundAuditTrace {
        plan_fingerprint: json_field_string(&fields, "plan_fingerprint", "math-bound audit trace")?,
        backend_id: json_field_string(&fields, "backend_id", "math-bound audit trace")?,
        device_kind: json_field_string(&fields, "device_kind", "math-bound audit trace")?,
        capability_fingerprint: json_field_string(
            &fields,
            "capability_fingerprint",
            "math-bound audit trace",
        )?,
        p_adic_constraint_fingerprint: json_field_string(
            &fields,
            "p_adic_constraint_fingerprint",
            "math-bound audit trace",
        )?,
        sheaf_constraint_fingerprint: json_field_string(
            &fields,
            "sheaf_constraint_fingerprint",
            "math-bound audit trace",
        )?,
        lowering_rule_ids: json_field_string_array(
            &fields,
            "lowering_rule_ids",
            "math-bound audit trace",
        )?,
        fallback_reason: json_field_option_string(
            &fields,
            "fallback_reason",
            "math-bound audit trace",
        )?,
        conformance_result: json_field_option_string(
            &fields,
            "conformance_result",
            "math-bound audit trace",
        )?,
        benchmark_environment: json_field_option_string(
            &fields,
            "benchmark_environment",
            "math-bound audit trace",
        )?,
    };
    verify_math_bound_audit_trace(&trace)?;
    Ok(trace)
}

fn parse_proof_replay_trace_benchmark_records_from_array(
    input: &str,
) -> Result<Vec<ProofReplayTraceBenchmarkRecord>> {
    parse_json_array_items(input, "proof replay trace benchmark records")?
        .iter()
        .map(|item| parse_proof_replay_trace_benchmark_record(item))
        .collect()
}

fn parse_proof_replay_trace_benchmark_record(
    input: &str,
) -> Result<ProofReplayTraceBenchmarkRecord> {
    let object = json_object_input(input);
    let fields = parse_json_object_fields(&object, "proof replay trace benchmark record")?;
    validate_json_object_field_set(
        &fields,
        PROOF_REPLAY_TRACE_BENCHMARK_RECORD_SCHEMA_FIELDS,
        "proof replay trace benchmark record",
    )?;
    let plan_fingerprint = json_field_string(
        &fields,
        "plan_fingerprint",
        "proof replay trace benchmark record",
    )?;
    let backend = json_field_string(&fields, "backend", "proof replay trace benchmark record")?;
    let strategy = json_field_string(&fields, "strategy", "proof replay trace benchmark record")?;
    let input_description = json_field_string(
        &fields,
        "input_description",
        "proof replay trace benchmark record",
    )?;
    let duration_ns = json_field_u64(
        &fields,
        "duration_ns",
        "proof replay trace benchmark record",
    )?;
    Ok(ProofReplayTraceBenchmarkRecord {
        plan_fingerprint,
        backend,
        strategy,
        input_description,
        duration_ns,
    })
}

fn parse_proof_replay_trace_tuning_from_fields(
    fields: &[(String, String)],
    context: &str,
) -> Result<ProofReplayTraceTuning> {
    let backend = json_field_string(fields, "backend", context)?;
    let selected_strategy = json_field_string(fields, "selected_strategy", context)?;
    let benchmark_count = json_field_usize(fields, "benchmark_count", context)?;
    let enable_pointwise_fusion = json_field_bool(fields, "enable_pointwise_fusion", context)?;
    let enable_padic_matmul_valuation_skip =
        json_field_bool(fields, "enable_padic_matmul_valuation_skip", context)?;
    Ok(ProofReplayTraceTuning {
        backend,
        selected_strategy,
        benchmark_count,
        enable_pointwise_fusion,
        enable_padic_matmul_valuation_skip,
    })
}

fn parse_proof_replay_trace_artifact(input: &str) -> Result<ProofReplayTraceArtifact> {
    let object = json_object_input(input);
    let fields = parse_json_object_fields(&object, "proof replay trace artifact")?;
    validate_json_object_field_set(
        &fields,
        PROOF_REPLAY_TRACE_ARTIFACT_SCHEMA_FIELDS,
        "proof replay trace artifact",
    )?;
    let filename = json_field_string(&fields, "filename", "proof replay trace artifact")?;
    let artifact = json_field_string(&fields, "artifact", "proof replay trace artifact")?;
    let version = json_field_u32(&fields, "version", "proof replay trace artifact")?;
    let format = json_field_string(&fields, "format", "proof replay trace artifact")?;
    let digest = json_field_string(&fields, "digest", "proof replay trace artifact")?;
    Ok(ProofReplayTraceArtifact {
        filename,
        artifact,
        version,
        format,
        digest,
    })
}

fn parse_proof_replay_trace_signature(input: &str) -> Result<Option<ProofReplayTraceSignature>> {
    if input == "null" {
        return Ok(None);
    }
    let fields = parse_json_object_fields(input, "proof replay trace signature")?;
    validate_json_object_field_set(
        &fields,
        PROOF_REPLAY_TRACE_SIGNATURE_SCHEMA_FIELDS,
        "proof replay trace signature",
    )?;
    let key_id = json_field_string(&fields, "key_id", "proof replay trace signature")?;
    let key_kind = json_field_string(&fields, "key_kind", "proof replay trace signature")?;
    let key_fingerprint =
        json_field_string(&fields, "key_fingerprint", "proof replay trace signature")?;
    let algorithm = json_field_string(&fields, "algorithm", "proof replay trace signature")?;
    let value = json_field_string(&fields, "value", "proof replay trace signature")?;
    Ok(Some(ProofReplayTraceSignature {
        key_id,
        key_kind,
        key_fingerprint,
        algorithm,
        value,
    }))
}

fn parse_proof_replay_entries_from_array(input: &str) -> Result<Vec<ProofReplayEntry>> {
    parse_json_array_items(input, "proof replay entries")?
        .iter()
        .map(|item| parse_proof_replay_entry(item))
        .collect()
}

fn parse_proof_assistant_replay_theorem_summaries_from_array(
    input: &str,
) -> Result<Vec<ProofAssistantReplayTheoremSummary>> {
    parse_json_array_items(input, "proof assistant theorem summaries")?
        .iter()
        .map(|item| parse_proof_assistant_replay_theorem_summary(item))
        .collect()
}

fn parse_proof_assistant_replay_theorem_summary(
    input: &str,
) -> Result<ProofAssistantReplayTheoremSummary> {
    let object = json_object_input(input);
    let fields = parse_json_object_fields(&object, "proof assistant theorem summary")?;
    validate_json_object_field_set(
        &fields,
        PROOF_ASSISTANT_REPLAY_THEOREM_SUMMARY_SCHEMA_FIELDS,
        "proof assistant theorem summary",
    )?;
    let theorem_id = json_field_string(&fields, "theorem_id", "proof assistant theorem summary")?;
    let original_id = json_field_string(&fields, "original_id", "proof assistant theorem summary")?;
    let kind = json_field_string(&fields, "kind", "proof assistant theorem summary")?;
    let status = json_field_string(&fields, "status", "proof assistant theorem summary")?;
    let replay_rule = json_field_string(&fields, "replay_rule", "proof assistant theorem summary")?;
    let obligations =
        json_field_string_array(&fields, "obligations", "proof assistant theorem summary")?;
    let evidence = json_field_string_array(&fields, "evidence", "proof assistant theorem summary")?;
    let obligation_count = json_field_usize(
        &fields,
        "obligation_count",
        "proof assistant theorem summary",
    )?;
    let evidence_count =
        json_field_usize(&fields, "evidence_count", "proof assistant theorem summary")?;
    let statement_fingerprint = json_field_string(
        &fields,
        "statement_fingerprint",
        "proof assistant theorem summary",
    )?;
    let adapter_backend = json_field_string(
        &fields,
        "adapter_backend",
        "proof assistant theorem summary",
    )?;
    let checker_version = json_field_string(
        &fields,
        "checker_version",
        "proof assistant theorem summary",
    )?;
    let proof_status =
        json_field_string(&fields, "proof_status", "proof assistant theorem summary")?;
    let adapter_capability_fingerprint = json_field_string(
        &fields,
        "adapter_capability_fingerprint",
        "proof assistant theorem summary",
    )?;
    Ok(ProofAssistantReplayTheoremSummary {
        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,
    })
}

fn parse_proof_replay_entry(input: &str) -> Result<ProofReplayEntry> {
    let object = json_object_input(input);
    let fields = parse_json_object_fields(&object, "proof replay entry")?;
    validate_json_object_field_set(
        &fields,
        PROOF_REPLAY_ENTRY_SCHEMA_FIELDS,
        "proof replay entry",
    )?;
    let theorem_id = json_field_string(&fields, "theorem_id", "proof replay entry")?;
    let original_id = json_field_string(&fields, "original_id", "proof replay entry")?;
    let kind = json_field_string(&fields, "kind", "proof replay entry")?;
    let status = json_field_string(&fields, "status", "proof replay entry")?;
    let replayed = json_field_bool(&fields, "replayed", "proof replay entry")?;
    let replay_rule = json_field_string(&fields, "replay_rule", "proof replay entry")?;
    Ok(ProofReplayEntry {
        theorem_id,
        original_id,
        kind,
        status,
        replayed,
        replay_rule,
    })
}

pub fn verify_proof_replay_trace_manifest_for_bundle(
    manifest: &ProofReplayTraceManifest,
    bundle: &ProofReplayArtifactBundle,
) -> Result<()> {
    verify_proof_replay_trace_manifest(manifest)?;
    let has_text = manifest.artifacts.iter().any(|artifact| {
        artifact.filename == bundle.text_filename
            && artifact.artifact == PROOF_REPLAY_REPORT_ARTIFACT
            && artifact.version == PROOF_REPLAY_REPORT_VERSION
            && artifact.format == "text"
            && artifact.digest == proof_replay_artifact_digest(&bundle.text)
    });
    if !has_text {
        return Err(Error::verification(format!(
            "proof replay trace manifest missing text artifact {}",
            bundle.text_filename
        )));
    }
    let has_json = manifest.artifacts.iter().any(|artifact| {
        artifact.filename == bundle.json_filename
            && artifact.artifact == PROOF_REPLAY_REPORT_ARTIFACT
            && artifact.version == PROOF_REPLAY_REPORT_VERSION
            && artifact.format == "json"
            && artifact.digest == proof_replay_artifact_digest(&bundle.json)
    });
    if !has_json {
        return Err(Error::verification(format!(
            "proof replay trace manifest missing JSON artifact {}",
            bundle.json_filename
        )));
    }
    Ok(())
}

pub fn verify_proof_replay_trace_directory(
    directory: impl AsRef<Path>,
) -> Result<ProofReplayTraceManifest> {
    let directory = directory.as_ref();
    let manifest_path = directory.join("tokitai-trace-manifest.json");
    let manifest_json = std::fs::read_to_string(&manifest_path).map_err(|err| {
        Error::verification(format!(
            "failed to read proof replay trace manifest {}: {}",
            manifest_path.display(),
            err
        ))
    })?;
    let manifest = parse_proof_replay_trace_manifest_json(&manifest_json)?;
    let mut tuning_artifact = None;
    let mut benchmark_artifact = None;
    let mut proof_assistant_skeleton = None;
    let mut proof_assistant_checkable = None;
    let mut adapter_registry = None;
    let mut adapter_registry_artifact = None;
    let mut native_admissions = Vec::new();
    let mut checker_outputs = Vec::new();
    let mut checker_transcripts = Vec::new();
    let mut checker_result_index = None;
    let mut replay_report = None;
    for artifact in &manifest.artifacts {
        let path = directory.join(&artifact.filename);
        let contents = std::fs::read_to_string(&path).map_err(|err| {
            Error::verification(format!(
                "failed to read proof replay trace artifact {}: {}",
                path.display(),
                err
            ))
        })?;
        verify_proof_replay_trace_artifact_contents(artifact, &contents)?;
        verify_proof_replay_trace_artifact_plan_fingerprint(
            artifact,
            &contents,
            manifest.plan_fingerprint.as_deref(),
        )?;
        if artifact.artifact == PROOF_REPLAY_TRACE_TUNING_ARTIFACT {
            let parsed = parse_proof_replay_trace_tuning_json(&contents)?;
            tuning_artifact = Some(parsed);
        }
        if artifact.artifact == PROOF_REPLAY_TRACE_BENCHMARK_ARTIFACT {
            let parsed = parse_proof_replay_trace_benchmark_json(&contents)?;
            benchmark_artifact = Some(parsed);
        }
        if artifact.artifact == PROOF_ASSISTANT_REPLAY_SKELETON_ARTIFACT {
            proof_assistant_skeleton = Some((artifact.clone(), contents.clone()));
        }
        if artifact.artifact == PROOF_ASSISTANT_LEAN_CHECKABLE_ARTIFACT {
            proof_assistant_checkable = Some((artifact.clone(), contents.clone()));
        }
        if artifact.artifact == PROOF_ASSISTANT_ADAPTER_REGISTRY_ARTIFACT {
            let parsed = parse_proof_assistant_adapter_registry_json(&contents)?;
            adapter_registry_artifact = Some(artifact.clone());
            adapter_registry = Some(parsed);
        }
        if artifact.artifact == PROOF_ASSISTANT_CHECKER_TRANSCRIPT_ARTIFACT {
            let parsed = parse_proof_assistant_checker_transcript_json(&contents)?;
            checker_transcripts.push((artifact.digest.clone(), parsed));
        }
        if artifact.artifact == PROOF_ASSISTANT_CHECKER_OUTPUT_ARTIFACT {
            let parsed = parse_proof_assistant_checker_output_json(&contents)?;
            checker_outputs.push((artifact.digest.clone(), parsed));
        }
        if artifact.artifact == PROOF_ASSISTANT_NATIVE_ADMISSION_ARTIFACT {
            let admission = parse_proof_assistant_native_admission_json(&contents)?;
            native_admissions.push((artifact.digest.clone(), admission));
        }
        if artifact.artifact == PROOF_ASSISTANT_CHECKER_RESULT_INDEX_ARTIFACT {
            if checker_result_index.is_some() {
                return Err(Error::verification(
                    "proof replay trace contains multiple checker result index artifacts",
                ));
            }
            let parsed = parse_checker_result_index_json(&contents)?;
            checker_result_index = Some(parsed);
        }
        if artifact.artifact == PROOF_REPLAY_REPORT_ARTIFACT && artifact.format == "json" {
            let parsed = parse_proof_replay_report_json(&contents)?;
            replay_report = Some(parsed);
        }
    }
    let proof_assistant_summary =
        match (proof_assistant_skeleton, adapter_registry_artifact.as_ref()) {
            (Some((artifact, contents)), Some(registry_artifact)) => {
                Some(proof_assistant_replay_summary_with_adapter_registry(
                    &artifact.filename,
                    &contents,
                    registry_artifact,
                )?)
            }
            (Some((artifact, contents)), None) => Some(proof_assistant_replay_summary(
                &artifact.filename,
                &contents,
            )?),
            (None, _) => None,
        };
    match (&manifest.proof_assistant, proof_assistant_summary) {
        (Some(expected), Some(actual)) => {
            verify_proof_assistant_summary_matches_skeleton(expected, &actual)?;
        }
        (Some(_), None) => {
            return Err(Error::verification(
                "proof replay trace manifest declares proof assistant summary but no skeleton artifact was found",
            ));
        }
        (None, Some(_)) => {
            return Err(Error::verification(
                "proof replay trace contains proof assistant skeleton but manifest summary is null",
            ));
        }
        (None, None) => {}
    }
    if let (Some(summary), Some(report)) = (&manifest.proof_assistant, &replay_report) {
        if summary.theorem_count != report.checked_proofs {
            return Err(Error::verification(
                "proof assistant replay summary theorem_count does not match replay report checked_proofs",
            ));
        }
        if summary.theorems.len() != report.replayed_proofs.len() {
            return Err(Error::verification(
                "proof assistant replay theorem index length does not match replay report",
            ));
        }
        for (summary, replay) in summary.theorems.iter().zip(&report.replayed_proofs) {
            if summary.theorem_id != replay.theorem_id
                || summary.original_id != replay.original_id
                || summary.kind != replay.kind
                || summary.status != replay.status
                || summary.replay_rule != replay.replay_rule
            {
                return Err(Error::verification(
                    "proof assistant replay theorem index does not match replay report",
                ));
            }
        }
    }
    match (&manifest.proof_assistant, adapter_registry) {
        (Some(summary), Some(registry)) => {
            verify_proof_assistant_summary_matches_adapter_registry(summary, &registry)?;
            verify_native_admission_artifacts_cover_registry(
                &registry,
                &native_admissions,
                summary,
                replay_report.as_ref(),
            )?;
            verify_checker_outputs_cover_native_admissions(
                &checker_outputs,
                &checker_transcripts,
                &native_admissions,
                proof_assistant_checkable.as_ref(),
                summary,
            )?;
            match (&manifest.plan_fingerprint, &registry.plan_fingerprint) {
                (Some(expected), Some(actual)) if expected == actual => {}
                (Some(_), Some(_)) => {
                    return Err(Error::verification(
                        "proof assistant adapter registry plan_fingerprint does not match manifest",
                    ));
                }
                (Some(_), None) => {
                    return Err(Error::verification(
                        "proof assistant adapter registry artifact requires plan_fingerprint",
                    ));
                }
                (None, _) => {}
            }
            let Some(registry_artifact) = adapter_registry_artifact.as_ref() else {
                return Err(Error::verification(
                    "proof replay trace manifest declares proof assistant summary but no adapter registry artifact was found",
                ));
            };
            if summary.adapter_registry_filename != registry_artifact.filename
                || summary.adapter_registry_digest != registry_artifact.digest
            {
                return Err(Error::verification(
                    "proof assistant replay summary adapter registry binding does not match artifact",
                ));
            }
            let has_native_capability = registry
                .capabilities
                .iter()
                .any(|capability| capability.native_checked);
            match (has_native_capability, checker_result_index.as_ref()) {
                (true, Some(index)) => {
                    verify_checker_result_index_matches_trace(
                        index,
                        &registry,
                        &native_admissions,
                        summary,
                    )?;
                }
                (true, None) => {
                    return Err(Error::verification(
                        "proof replay trace native adapter registry requires checker result index artifact",
                    ));
                }
                (false, Some(_)) => {
                    return Err(Error::verification(
                        "proof replay trace contains checker result index without native adapter capability",
                    ));
                }
                (false, None) => {}
            }
        }
        (Some(_), None) => {
            return Err(Error::verification(
                "proof replay trace manifest declares proof assistant summary but no adapter registry artifact was found",
            ));
        }
        (None, Some(_)) => {
            return Err(Error::verification(
                "proof replay trace contains adapter registry artifact but manifest proof_assistant summary is null",
            ));
        }
        (None, None) => {
            if checker_result_index.is_some() {
                return Err(Error::verification(
                    "proof replay trace contains checker result index but manifest proof_assistant summary is null",
                ));
            }
        }
    }
    match (&manifest.tuning, tuning_artifact) {
        (Some(expected), Some(actual)) if expected == &actual => {}
        (Some(_), Some(_)) => {
            return Err(Error::verification(
                "proof replay trace tuning artifact does not match manifest tuning summary",
            ));
        }
        (Some(_), None) => {
            return Err(Error::verification(
                "proof replay trace manifest declares tuning but no tuning artifact was found",
            ));
        }
        (None, Some(_)) => {
            return Err(Error::verification(
                "proof replay trace contains tuning artifact but manifest tuning is null",
            ));
        }
        (None, None) => {}
    }
    match (&manifest.tuning, benchmark_artifact) {
        (Some(expected), Some(actual)) => {
            match &manifest.plan_fingerprint {
                Some(fingerprint) if fingerprint == &actual.plan_fingerprint => {}
                Some(_) => {
                    return Err(Error::verification(
                        "proof replay trace benchmark plan_fingerprint does not match manifest",
                    ));
                }
                None => {
                    return Err(Error::verification(
                        "proof replay trace benchmark artifact requires manifest plan_fingerprint",
                    ));
                }
            }
            verify_benchmark_set_matches_tuning(&actual, expected)?;
        }
        (Some(_), None) => {
            return Err(Error::verification(
                "proof replay trace manifest declares tuning but no benchmark artifact was found",
            ));
        }
        (None, Some(_)) => {
            return Err(Error::verification(
                "proof replay trace contains benchmark artifact but manifest tuning is null",
            ));
        }
        (None, None) => {}
    }
    Ok(manifest)
}

fn is_semantically_replayed_kind(kind: &str) -> bool {
    matches!(
        kind,
        "shape_equality"
            | "valuation_cutoff"
            | "lowering_semantic_preservation"
            | "rewrite_soundness"
    )
}

fn semantic_replay_rule(kind: &str) -> &'static str {
    match kind {
        "shape_equality" => "shape_equality_replay",
        "valuation_cutoff" => "valuation_cutoff_replay",
        "lowering_semantic_preservation" => "lowering_semantic_preservation_replay",
        "rewrite_soundness" => "rewrite_soundness_replay",
        _ => "not_replayed",
    }
}

fn verify_proof_replay_trace_artifact(artifact: &ProofReplayTraceArtifact) -> Result<()> {
    if artifact.filename.trim().is_empty() {
        return Err(Error::verification(
            "proof replay trace artifact filename must not be empty",
        ));
    }
    if artifact.filename.contains('/') || artifact.filename.contains('\\') {
        return Err(Error::verification(format!(
            "proof replay trace artifact filename must be relative: {}",
            artifact.filename
        )));
    }
    if !matches!(
        artifact.artifact.as_str(),
        PROOF_REPLAY_REPORT_ARTIFACT
            | PROOF_REPLAY_TRACE_TUNING_ARTIFACT
            | PROOF_REPLAY_TRACE_BENCHMARK_ARTIFACT
            | MATH_BOUND_AUDIT_TRACE_ARTIFACT
            | PROOF_ASSISTANT_REPLAY_SKELETON_ARTIFACT
            | PROOF_ASSISTANT_LEAN_CHECKABLE_ARTIFACT
            | PROOF_ASSISTANT_CHECKER_TRANSCRIPT_ARTIFACT
            | PROOF_ASSISTANT_CHECKER_OUTPUT_ARTIFACT
            | PROOF_ASSISTANT_ADAPTER_REGISTRY_ARTIFACT
            | PROOF_ASSISTANT_NATIVE_ADMISSION_ARTIFACT
            | PROOF_ASSISTANT_CHECKER_RESULT_INDEX_ARTIFACT
    ) {
        return Err(Error::verification(format!(
            "unsupported proof replay trace artifact kind {}",
            artifact.artifact
        )));
    }
    let expected_version = match artifact.artifact.as_str() {
        PROOF_REPLAY_REPORT_ARTIFACT => PROOF_REPLAY_REPORT_VERSION,
        PROOF_REPLAY_TRACE_TUNING_ARTIFACT => PROOF_REPLAY_TRACE_TUNING_VERSION,
        PROOF_REPLAY_TRACE_BENCHMARK_ARTIFACT => PROOF_REPLAY_TRACE_BENCHMARK_VERSION,
        MATH_BOUND_AUDIT_TRACE_ARTIFACT => MATH_BOUND_AUDIT_TRACE_VERSION,
        PROOF_ASSISTANT_REPLAY_SKELETON_ARTIFACT => PROOF_ASSISTANT_REPLAY_SKELETON_VERSION,
        PROOF_ASSISTANT_LEAN_CHECKABLE_ARTIFACT => PROOF_ASSISTANT_LEAN_CHECKABLE_VERSION,
        PROOF_ASSISTANT_CHECKER_TRANSCRIPT_ARTIFACT => PROOF_ASSISTANT_CHECKER_TRANSCRIPT_VERSION,
        PROOF_ASSISTANT_CHECKER_OUTPUT_ARTIFACT => PROOF_ASSISTANT_CHECKER_OUTPUT_VERSION,
        PROOF_ASSISTANT_ADAPTER_REGISTRY_ARTIFACT => PROOF_ASSISTANT_ADAPTER_REGISTRY_VERSION,
        PROOF_ASSISTANT_NATIVE_ADMISSION_ARTIFACT => PROOF_ASSISTANT_NATIVE_ADMISSION_VERSION,
        PROOF_ASSISTANT_CHECKER_RESULT_INDEX_ARTIFACT => {
            PROOF_ASSISTANT_CHECKER_RESULT_INDEX_VERSION
        }
        _ => unreachable!("artifact kind checked above"),
    };
    if artifact.version != expected_version {
        return Err(Error::verification(format!(
            "unsupported proof replay trace artifact version {}",
            artifact.version
        )));
    }
    let format_supported = match artifact.artifact.as_str() {
        PROOF_REPLAY_REPORT_ARTIFACT => matches!(artifact.format.as_str(), "text" | "json"),
        PROOF_REPLAY_TRACE_TUNING_ARTIFACT => artifact.format == "json",
        PROOF_REPLAY_TRACE_BENCHMARK_ARTIFACT => artifact.format == "json",
        MATH_BOUND_AUDIT_TRACE_ARTIFACT => artifact.format == "json",
        PROOF_ASSISTANT_REPLAY_SKELETON_ARTIFACT => artifact.format == "lean",
        PROOF_ASSISTANT_LEAN_CHECKABLE_ARTIFACT => artifact.format == "lean",
        PROOF_ASSISTANT_CHECKER_TRANSCRIPT_ARTIFACT => artifact.format == "json",
        PROOF_ASSISTANT_CHECKER_OUTPUT_ARTIFACT => artifact.format == "json",
        PROOF_ASSISTANT_ADAPTER_REGISTRY_ARTIFACT => artifact.format == "json",
        PROOF_ASSISTANT_NATIVE_ADMISSION_ARTIFACT => artifact.format == "json",
        PROOF_ASSISTANT_CHECKER_RESULT_INDEX_ARTIFACT => artifact.format == "json",
        _ => false,
    };
    if !format_supported {
        return Err(Error::verification(format!(
            "unsupported proof replay trace artifact format {}",
            artifact.format
        )));
    }
    if !is_valid_artifact_digest(&artifact.digest) {
        return Err(Error::verification(format!(
            "invalid proof replay trace artifact digest {}",
            artifact.digest
        )));
    }
    Ok(())
}

fn verify_proof_replay_trace_signature_shape(signature: &ProofReplayTraceSignature) -> Result<()> {
    if signature.key_id.trim().is_empty() {
        return Err(Error::verification(
            "proof replay trace signature key_id must not be empty",
        ));
    }
    let sanitized = sanitize_artifact_stem(&signature.key_id)?;
    if sanitized != signature.key_id {
        return Err(Error::verification(format!(
            "proof replay trace signature key_id is not canonical: {}",
            signature.key_id
        )));
    }
    if !matches!(
        signature.key_kind.as_str(),
        "shared-secret" | "ed25519-public"
    ) {
        return Err(Error::verification(format!(
            "unsupported proof replay trace signature key kind {}",
            signature.key_kind
        )));
    }
    if !is_valid_artifact_digest(&signature.key_fingerprint) {
        return Err(Error::verification(format!(
            "invalid proof replay trace signature key_fingerprint {}",
            signature.key_fingerprint
        )));
    }
    let algorithm_supported = matches!(
        (signature.key_kind.as_str(), signature.algorithm.as_str()),
        ("shared-secret", PROOF_REPLAY_TRACE_SIGNATURE_ALGORITHM)
            | (
                "ed25519-public",
                PROOF_REPLAY_TRACE_PUBLIC_KEY_SIGNATURE_ALGORITHM
            )
    );
    if !algorithm_supported {
        return Err(Error::verification(format!(
            "unsupported proof replay trace signature algorithm {}",
            signature.algorithm
        )));
    }
    let valid_signature_value = match signature.key_kind.as_str() {
        "shared-secret" => is_valid_keyed_signature_value(&signature.value),
        "ed25519-public" => is_valid_ed25519_signature_value(&signature.value),
        _ => false,
    };
    if !valid_signature_value {
        return Err(Error::verification(format!(
            "invalid proof replay trace signature value {}",
            signature.value
        )));
    }
    Ok(())
}

fn verify_proof_replay_trace_tuning(tuning: &ProofReplayTraceTuning) -> Result<()> {
    if tuning.backend.trim().is_empty() {
        return Err(Error::verification(
            "proof replay trace tuning backend must not be empty",
        ));
    }
    if tuning.selected_strategy.trim().is_empty() {
        return Err(Error::verification(
            "proof replay trace tuning selected_strategy must not be empty",
        ));
    }
    Ok(())
}

fn verify_proof_replay_trace_benchmark_set(
    benchmarks: &ProofReplayTraceBenchmarkSet,
) -> Result<()> {
    if !is_valid_artifact_digest(&benchmarks.plan_fingerprint) {
        return Err(Error::verification(
            "proof replay trace benchmark plan_fingerprint must be a sha256 digest",
        ));
    }
    if benchmarks.backend.trim().is_empty() {
        return Err(Error::verification(
            "proof replay trace benchmark backend must not be empty",
        ));
    }
    if benchmarks.selected_strategy.trim().is_empty() {
        return Err(Error::verification(
            "proof replay trace benchmark selected_strategy must not be empty",
        ));
    }
    if benchmarks.records.is_empty() {
        return Err(Error::verification(
            "proof replay trace benchmark records must not be empty",
        ));
    }
    for record in &benchmarks.records {
        if record.plan_fingerprint != benchmarks.plan_fingerprint {
            return Err(Error::verification(
                "proof replay trace benchmark record plan_fingerprint does not match set",
            ));
        }
        if record.backend != benchmarks.backend {
            return Err(Error::verification(format!(
                "proof replay trace benchmark record backend {} does not match set backend {}",
                record.backend, benchmarks.backend
            )));
        }
        if record.strategy.trim().is_empty() {
            return Err(Error::verification(
                "proof replay trace benchmark record strategy must not be empty",
            ));
        }
        if record.input_description.trim().is_empty() {
            return Err(Error::verification(
                "proof replay trace benchmark record input_description must not be empty",
            ));
        }
    }
    Ok(())
}

fn verify_benchmark_set_matches_tuning(
    benchmarks: &ProofReplayTraceBenchmarkSet,
    tuning: &ProofReplayTraceTuning,
) -> Result<()> {
    verify_proof_replay_trace_benchmark_set(benchmarks)?;
    if benchmarks.backend != tuning.backend {
        return Err(Error::verification(
            "proof replay trace benchmark backend does not match tuning backend",
        ));
    }
    if benchmarks.records.len() != tuning.benchmark_count {
        return Err(Error::verification(
            "proof replay trace benchmark count does not match tuning summary",
        ));
    }
    let fastest = benchmarks.fastest_strategy().ok_or_else(|| {
        Error::verification("proof replay trace benchmark set has no fastest strategy")
    })?;
    if fastest != tuning.selected_strategy
        || benchmarks.selected_strategy != tuning.selected_strategy
    {
        return Err(Error::verification(
            "proof replay trace benchmark fastest strategy does not match tuning summary",
        ));
    }
    let policy = crate::planner::OptimizationPolicy::from_strategy(fastest);
    if policy.enable_pointwise_fusion != tuning.enable_pointwise_fusion
        || policy.enable_padic_matmul_valuation_skip != tuning.enable_padic_matmul_valuation_skip
    {
        return Err(Error::verification(
            "proof replay trace benchmark-derived policy does not match tuning summary",
        ));
    }
    Ok(())
}

fn verify_proof_replay_entry(entry: &ProofReplayEntry) -> Result<()> {
    if !is_valid_theorem_id(&entry.theorem_id) {
        return Err(Error::verification(format!(
            "invalid proof replay theorem id {}",
            entry.theorem_id
        )));
    }
    if entry.original_id.trim().is_empty() {
        return Err(Error::verification(format!(
            "proof replay entry {} missing original proof id",
            entry.theorem_id
        )));
    }
    if !is_semantically_replayed_kind(&entry.kind) {
        return Err(Error::verification(format!(
            "proof replay entry {} has unsupported kind {}",
            entry.theorem_id, entry.kind
        )));
    }
    if !matches!(
        entry.status.as_str(),
        "proven" | "runtime_checked" | "assumed" | "pending"
    ) {
        return Err(Error::verification(format!(
            "proof replay entry {} has unsupported status {}",
            entry.theorem_id, entry.status
        )));
    }
    let expected_rule = semantic_replay_rule(&entry.kind);
    if entry.replay_rule != expected_rule {
        return Err(Error::verification(format!(
            "proof replay entry {} expected rule {}, got {}",
            entry.theorem_id, expected_rule, entry.replay_rule
        )));
    }
    if !entry.replayed {
        return Err(Error::verification(format!(
            "proof replay entry {} was not replayed",
            entry.theorem_id
        )));
    }
    Ok(())
}

fn verify_math_bound_audit_trace(trace: &MathBoundAuditTrace) -> Result<()> {
    if !is_valid_artifact_digest(&trace.plan_fingerprint) {
        return Err(Error::verification(
            "math-bound audit trace plan_fingerprint must be a sha256 digest",
        ));
    }
    if trace.backend_id.trim().is_empty() {
        return Err(Error::verification(
            "math-bound audit trace backend_id must not be empty",
        ));
    }
    if !matches!(
        trace.device_kind.as_str(),
        "cpu" | "gpu" | "accelerator" | "unknown"
    ) {
        return Err(Error::verification(format!(
            "math-bound audit trace device_kind {} is unsupported",
            trace.device_kind
        )));
    }
    for (field, value) in [
        ("capability_fingerprint", &trace.capability_fingerprint),
        (
            "p_adic_constraint_fingerprint",
            &trace.p_adic_constraint_fingerprint,
        ),
        (
            "sheaf_constraint_fingerprint",
            &trace.sheaf_constraint_fingerprint,
        ),
    ] {
        if !(value.starts_with("sha256:") || value.starts_with("cachefp-")) {
            return Err(Error::verification(format!(
                "math-bound audit trace {field} must be a digest-like value"
            )));
        }
    }
    Ok(())
}

fn verify_proof_replay_trace_artifact_contents(
    artifact: &ProofReplayTraceArtifact,
    contents: &str,
) -> Result<()> {
    let actual_digest = proof_replay_artifact_digest(contents);
    if artifact.digest != actual_digest {
        return Err(Error::verification(format!(
            "proof replay trace artifact {} digest mismatch: expected {}, got {}",
            artifact.filename, artifact.digest, actual_digest
        )));
    }
    match artifact.artifact.as_str() {
        PROOF_REPLAY_REPORT_ARTIFACT => {
            if artifact.version != PROOF_REPLAY_REPORT_VERSION {
                return Err(Error::verification(format!(
                    "proof replay trace artifact {} metadata does not match replay report schema",
                    artifact.filename
                )));
            }
            match artifact.format.as_str() {
                "text" => {
                    if !contents.contains(&format!("artifact: {PROOF_REPLAY_REPORT_ARTIFACT}"))
                        || !contents.contains(&format!("version: {PROOF_REPLAY_REPORT_VERSION}"))
                    {
                        return Err(Error::verification(format!(
                            "proof replay text artifact {} missing schema metadata",
                            artifact.filename
                        )));
                    }
                }
                "json" => {
                    let report = parse_proof_replay_report_json(contents).map_err(|err| {
                        Error::verification(format!(
                            "proof replay JSON artifact {} failed content validation: {}",
                            artifact.filename, err
                        ))
                    })?;
                    verify_proof_replay_report(&report)?;
                }
                other => {
                    return Err(Error::verification(format!(
                        "unsupported proof replay trace artifact format {}",
                        other
                    )));
                }
            }
        }
        PROOF_REPLAY_TRACE_TUNING_ARTIFACT => {
            if artifact.version != PROOF_REPLAY_TRACE_TUNING_VERSION || artifact.format != "json" {
                return Err(Error::verification(format!(
                    "proof replay trace tuning artifact {} metadata does not match schema",
                    artifact.filename
                )));
            }
            parse_proof_replay_trace_tuning_json(contents).map_err(|err| {
                Error::verification(format!(
                    "proof replay trace tuning artifact {} failed content validation: {}",
                    artifact.filename, err
                ))
            })?;
        }
        PROOF_REPLAY_TRACE_BENCHMARK_ARTIFACT => {
            if artifact.version != PROOF_REPLAY_TRACE_BENCHMARK_VERSION || artifact.format != "json"
            {
                return Err(Error::verification(format!(
                    "proof replay trace benchmark artifact {} metadata does not match schema",
                    artifact.filename
                )));
            }
            parse_proof_replay_trace_benchmark_json(contents).map_err(|err| {
                Error::verification(format!(
                    "proof replay trace benchmark artifact {} failed content validation: {}",
                    artifact.filename, err
                ))
            })?;
        }
        MATH_BOUND_AUDIT_TRACE_ARTIFACT => {
            if artifact.version != MATH_BOUND_AUDIT_TRACE_VERSION || artifact.format != "json" {
                return Err(Error::verification(format!(
                    "math-bound audit trace artifact {} metadata does not match schema",
                    artifact.filename
                )));
            }
            parse_math_bound_audit_trace_json(contents).map_err(|err| {
                Error::verification(format!(
                    "math-bound audit trace artifact {} failed content validation: {}",
                    artifact.filename, err
                ))
            })?;
        }
        PROOF_ASSISTANT_REPLAY_SKELETON_ARTIFACT => {
            if artifact.version != PROOF_ASSISTANT_REPLAY_SKELETON_VERSION
                || artifact.format != "lean"
            {
                return Err(Error::verification(format!(
                    "proof assistant replay skeleton artifact {} metadata does not match schema",
                    artifact.filename
                )));
            }
            verify_proof_assistant_replay_skeleton_contents(contents).map_err(|err| {
                Error::verification(format!(
                    "proof assistant replay skeleton artifact {} failed content validation: {}",
                    artifact.filename, err
                ))
            })?;
        }
        PROOF_ASSISTANT_LEAN_CHECKABLE_ARTIFACT => {
            if artifact.version != PROOF_ASSISTANT_LEAN_CHECKABLE_VERSION
                || artifact.format != "lean"
            {
                return Err(Error::verification(format!(
                    "proof assistant Lean checkable artifact {} metadata does not match schema",
                    artifact.filename
                )));
            }
            verify_proof_assistant_lean_checkable_contents(contents).map_err(|err| {
                Error::verification(format!(
                    "proof assistant Lean checkable artifact {} failed content validation: {}",
                    artifact.filename, err
                ))
            })?;
        }
        PROOF_ASSISTANT_CHECKER_TRANSCRIPT_ARTIFACT => {
            if artifact.version != PROOF_ASSISTANT_CHECKER_TRANSCRIPT_VERSION
                || artifact.format != "json"
            {
                return Err(Error::verification(format!(
                    "proof assistant checker transcript artifact {} metadata does not match schema",
                    artifact.filename
                )));
            }
            parse_proof_assistant_checker_transcript_json(contents).map_err(|err| {
                Error::verification(format!(
                    "proof assistant checker transcript artifact {} failed content validation: {}",
                    artifact.filename, err
                ))
            })?;
        }
        PROOF_ASSISTANT_CHECKER_OUTPUT_ARTIFACT => {
            if artifact.version != PROOF_ASSISTANT_CHECKER_OUTPUT_VERSION
                || artifact.format != "json"
            {
                return Err(Error::verification(format!(
                    "proof assistant checker output artifact {} metadata does not match schema",
                    artifact.filename
                )));
            }
            parse_proof_assistant_checker_output_json(contents).map_err(|err| {
                Error::verification(format!(
                    "proof assistant checker output artifact {} failed content validation: {}",
                    artifact.filename, err
                ))
            })?;
        }
        PROOF_ASSISTANT_ADAPTER_REGISTRY_ARTIFACT => {
            if artifact.version != PROOF_ASSISTANT_ADAPTER_REGISTRY_VERSION
                || artifact.format != "json"
            {
                return Err(Error::verification(format!(
                    "proof assistant adapter registry artifact {} metadata does not match schema",
                    artifact.filename
                )));
            }
            parse_proof_assistant_adapter_registry_json(contents).map_err(|err| {
                Error::verification(format!(
                    "proof assistant adapter registry artifact {} failed content validation: {}",
                    artifact.filename, err
                ))
            })?;
        }
        PROOF_ASSISTANT_NATIVE_ADMISSION_ARTIFACT => {
            if artifact.version != PROOF_ASSISTANT_NATIVE_ADMISSION_VERSION
                || artifact.format != "json"
            {
                return Err(Error::verification(format!(
                    "proof assistant native admission artifact {} metadata does not match schema",
                    artifact.filename
                )));
            }
            parse_proof_assistant_native_admission_json(contents).map_err(|err| {
                Error::verification(format!(
                    "proof assistant native admission artifact {} failed content validation: {}",
                    artifact.filename, err
                ))
            })?;
        }
        PROOF_ASSISTANT_CHECKER_RESULT_INDEX_ARTIFACT => {
            if artifact.version != PROOF_ASSISTANT_CHECKER_RESULT_INDEX_VERSION
                || artifact.format != "json"
            {
                return Err(Error::verification(format!(
                    "checker result index artifact {} metadata does not match schema",
                    artifact.filename
                )));
            }
            parse_checker_result_index_json(contents).map_err(|err| {
                Error::verification(format!(
                    "checker result index artifact {} failed content validation: {}",
                    artifact.filename, err
                ))
            })?;
        }
        other => {
            return Err(Error::verification(format!(
                "unsupported proof replay trace artifact kind {}",
                other
            )));
        }
    }
    Ok(())
}

fn verify_proof_assistant_replay_skeleton_contents(contents: &str) -> Result<()> {
    if !contents.contains(&format!(
        "artifact: {PROOF_ASSISTANT_REPLAY_SKELETON_ARTIFACT}"
    )) || !contents.contains(&format!(
        "version: {PROOF_ASSISTANT_REPLAY_SKELETON_VERSION}"
    )) || !contents.contains("dialect: lean")
        || !contents.contains("namespace TokitaiReplay")
        || !contents.contains("end TokitaiReplay")
    {
        return Err(Error::verification(
            "proof assistant replay skeleton missing schema metadata",
        ));
    }
    Ok(())
}

fn verify_proof_assistant_lean_checkable_contents(contents: &str) -> Result<()> {
    if !contents.contains(&format!(
        "artifact: {PROOF_ASSISTANT_LEAN_CHECKABLE_ARTIFACT}"
    )) || !contents.contains(&format!(
        "version: {PROOF_ASSISTANT_LEAN_CHECKABLE_VERSION}"
    )) || !contents.contains("dialect: lean")
        || !contents.contains("namespace TokitaiCheckable")
        || !contents.contains("end TokitaiCheckable")
        || !contents.contains("checker_command: lean <artifact>.lean-checkable.lean")
        || !contents.contains(&format!(
            "selected_witness_family: {PROOF_ASSISTANT_SELECTED_WITNESS_FAMILY}"
        ))
        || !contents.contains(&format!(
            "selected_nonstandard_witness_family: {PROOF_ASSISTANT_SELECTED_NONSTANDARD_WITNESS_FAMILY}"
        ))
    {
        return Err(Error::verification(
            "proof assistant Lean checkable artifact missing schema metadata",
        ));
    }
    if contents.contains("\naxiom ") || contents.contains("\nunsafe ") {
        return Err(Error::verification(
            "proof assistant Lean checkable artifact must not contain axiom or unsafe declarations",
        ));
    }
    let theorem_count = contents
        .lines()
        .filter(|line| line.trim_start().starts_with("theorem "))
        .count();
    if theorem_count == 0 {
        return Err(Error::verification(
            "proof assistant Lean checkable artifact must contain at least one theorem",
        ));
    }
    let trivial_count = contents
        .lines()
        .filter(|line| line.trim() == "trivial")
        .count();
    let shape_witness_count = contents
        .lines()
        .filter(|line| line.trim_start().starts_with("theorem "))
        .filter(|line| line.contains("_shape_equality_witness : "))
        .count();
    let padic_witness_count = contents
        .lines()
        .filter(|line| line.trim_start().starts_with("theorem "))
        .filter(|line| line.contains("_padic_precision_cutoff_witness : "))
        .count();
    let declared_shape_witness_count = contents
        .lines()
        .find_map(|line| {
            line.trim()
                .strip_prefix("selected_shape_witness_count: ")
                .and_then(|value| value.parse::<usize>().ok())
        })
        .ok_or_else(|| {
            Error::verification(
                "proof assistant Lean checkable artifact missing selected witness count",
            )
        })?;
    let declared_padic_witness_count = contents
        .lines()
        .find_map(|line| {
            line.trim()
                .strip_prefix("selected_padic_witness_count: ")
                .and_then(|value| value.parse::<usize>().ok())
        })
        .ok_or_else(|| {
            Error::verification(
                "proof assistant Lean checkable artifact missing selected nonstandard witness count",
            )
        })?;
    let rfl_count = contents.lines().filter(|line| line.trim() == "rfl").count();
    let selected_witness_count = shape_witness_count + padic_witness_count;
    if trivial_count == 0 || theorem_count != trivial_count + selected_witness_count {
        return Err(Error::verification(
            "proof assistant Lean checkable artifact theorem count does not match smoke and selected witness proofs",
        ));
    }
    if shape_witness_count != declared_shape_witness_count {
        return Err(Error::verification(
            "proof assistant Lean checkable artifact selected shape witness count does not match metadata",
        ));
    }
    if padic_witness_count != declared_padic_witness_count {
        return Err(Error::verification(
            "proof assistant Lean checkable artifact selected p-adic witness count does not match metadata",
        ));
    }
    if selected_witness_count != rfl_count {
        return Err(Error::verification(
            "proof assistant Lean checkable artifact selected witnesses must use rfl proofs",
        ));
    }
    Ok(())
}

fn proof_assistant_replay_theorem_summaries(
    contents: &str,
) -> Result<Vec<ProofAssistantReplayTheoremSummary>> {
    let mut summaries = Vec::new();
    let mut pending: Option<ProofAssistantReplayTheoremSummary> = None;
    for line in contents.lines() {
        let line = line.trim();
        if let Some(theorem_id) = line
            .strip_prefix("/-- Tokitai theorem: ")
            .and_then(|value| value.strip_suffix(" -/"))
        {
            if pending.is_some() {
                return Err(Error::verification(
                    "proof assistant replay skeleton theorem block missing axiom",
                ));
            }
            pending = Some(ProofAssistantReplayTheoremSummary {
                theorem_id: theorem_id.to_string(),
                original_id: String::new(),
                kind: String::new(),
                status: String::new(),
                replay_rule: String::new(),
                obligations: Vec::new(),
                evidence: Vec::new(),
                obligation_count: 0,
                evidence_count: 0,
                statement_fingerprint: String::new(),
                adapter_backend: String::new(),
                checker_version: String::new(),
                proof_status: String::new(),
                adapter_capability_fingerprint: String::new(),
            });
            continue;
        }
        if let Some(summary) = pending.as_mut() {
            let theorem_ident = lean_identifier(&summary.theorem_id)?;
            if let Some(value) = line.strip_prefix("-- original_id: ") {
                summary.original_id = value.to_string();
                continue;
            }
            if let Some(value) = line.strip_prefix("-- kind: ") {
                summary.kind = value.to_string();
                continue;
            }
            if let Some(value) = line.strip_prefix("-- status: ") {
                summary.status = value.to_string();
                continue;
            }
            if let Some(value) = line.strip_prefix("-- replay_rule: ") {
                summary.replay_rule = value.to_string();
                continue;
            }
            if let Some(value) = line.strip_prefix("-- adapter_backend: ") {
                summary.adapter_backend = value.to_string();
                continue;
            }
            if let Some(value) = line.strip_prefix("-- checker_version: ") {
                summary.checker_version = value.to_string();
                continue;
            }
            if let Some(value) = line.strip_prefix("-- proof_status: ") {
                summary.proof_status = value.to_string();
                continue;
            }
            if let Some(value) = line.strip_prefix("-- adapter_capability_fingerprint: ") {
                summary.adapter_capability_fingerprint = value.to_string();
                continue;
            }
            if let Some(value) = line.strip_prefix("-- obligation: ") {
                summary.obligations.push(value.to_string());
                continue;
            }
            if let Some(value) = line.strip_prefix("-- evidence: ") {
                summary.evidence.push(value.to_string());
                continue;
            }
            if line
                .strip_prefix("def ")
                .is_some_and(|rest| rest.starts_with(&format!("{theorem_ident}_obligation_")))
            {
                summary.obligation_count += 1;
                continue;
            }
            if line
                .strip_prefix("def ")
                .is_some_and(|rest| rest.starts_with(&format!("{theorem_ident}_evidence_")))
            {
                summary.evidence_count += 1;
                continue;
            }
            if let Some(rest) = line.strip_prefix("axiom ") {
                let (axiom_id, axiom_statement) = rest.split_once(" : ").ok_or_else(|| {
                    Error::verification(
                        "proof assistant replay skeleton theorem axiom has unsupported shape",
                    )
                })?;
                if axiom_id != summary.theorem_id {
                    return Err(Error::verification(
                        "proof assistant replay skeleton theorem id does not match axiom",
                    ));
                }
                let expected_statement = lean_replay_theorem_statement(
                    &theorem_ident,
                    summary.obligation_count,
                    summary.evidence_count,
                );
                if axiom_statement != expected_statement {
                    return Err(Error::verification(
                        "proof assistant replay skeleton theorem statement does not reference generated proof goals",
                    ));
                }
                summary.statement_fingerprint =
                    proof_assistant_statement_fingerprint(axiom_statement);
                let completed = pending.take().expect("pending theorem must exist");
                verify_proof_assistant_replay_theorem_summary(&completed)?;
                summaries.push(completed);
            }
        }
    }
    if pending.is_some() {
        return Err(Error::verification(
            "proof assistant replay skeleton theorem block missing axiom",
        ));
    }
    Ok(summaries)
}

fn verify_proof_assistant_replay_summary(summary: &ProofAssistantReplaySummary) -> Result<()> {
    if summary.dialect != "lean" {
        return Err(Error::verification(format!(
            "unsupported proof assistant replay dialect {}",
            summary.dialect
        )));
    }
    if let Some(fingerprint) = &summary.plan_fingerprint {
        if !is_valid_artifact_digest(fingerprint) {
            return Err(Error::verification(
                "proof assistant replay summary plan_fingerprint must be a sha256 digest",
            ));
        }
    }
    if summary.theorem_count == 0 {
        return Err(Error::verification(
            "proof assistant replay summary theorem_count must be positive",
        ));
    }
    if summary.theorem_count != summary.theorems.len() {
        return Err(Error::verification(
            "proof assistant replay summary theorem_count does not match theorem index length",
        ));
    }
    if summary.filename.trim().is_empty()
        || summary.filename.contains('/')
        || summary.filename.contains('\\')
        || !summary.filename.ends_with(".proof-replay.lean")
    {
        return Err(Error::verification(
            "proof assistant replay summary filename must name a local .proof-replay.lean artifact",
        ));
    }
    if summary.adapter_registry_filename.trim().is_empty()
        || summary.adapter_registry_filename.contains('/')
        || summary.adapter_registry_filename.contains('\\')
        || !summary
            .adapter_registry_filename
            .ends_with(".proof-adapters.json")
    {
        return Err(Error::verification(
            "proof assistant replay summary adapter_registry_filename must name a local .proof-adapters.json artifact",
        ));
    }
    if !is_valid_artifact_digest(&summary.adapter_registry_digest) {
        return Err(Error::verification(
            "proof assistant replay summary adapter_registry_digest must be a sha256 digest",
        ));
    }
    for theorem in &summary.theorems {
        verify_proof_assistant_replay_theorem_summary(theorem)?;
    }
    Ok(())
}

fn verify_proof_assistant_replay_theorem_summary(
    theorem: &ProofAssistantReplayTheoremSummary,
) -> Result<()> {
    if !is_valid_theorem_id(&theorem.theorem_id) {
        return Err(Error::verification(format!(
            "invalid proof assistant replay theorem id {}",
            theorem.theorem_id
        )));
    }
    if theorem.original_id.trim().is_empty() {
        return Err(Error::verification(
            "proof assistant replay theorem original_id must be non-empty",
        ));
    }
    if !matches!(
        theorem.status.as_str(),
        "proven" | "runtime_checked" | "assumed" | "pending"
    ) {
        return Err(Error::verification(
            "proof assistant replay theorem status is unsupported",
        ));
    }
    if !is_semantically_replayed_kind(&theorem.kind) {
        return Err(Error::verification(format!(
            "proof assistant replay theorem kind {} is not semantically replayed",
            theorem.kind
        )));
    }
    if theorem.replay_rule != semantic_replay_rule(&theorem.kind) {
        return Err(Error::verification(
            "proof assistant replay theorem replay_rule does not match kind",
        ));
    }
    if theorem
        .obligations
        .iter()
        .any(|entry| entry.trim().is_empty())
    {
        return Err(Error::verification(
            "proof assistant replay theorem obligations must be non-empty strings",
        ));
    }
    if theorem.evidence.iter().any(|entry| entry.trim().is_empty()) {
        return Err(Error::verification(
            "proof assistant replay theorem evidence must be non-empty strings",
        ));
    }
    if theorem.obligation_count != theorem.obligations.len() {
        return Err(Error::verification(
            "proof assistant replay theorem obligation_count does not match obligations",
        ));
    }
    if theorem.evidence_count != theorem.evidence.len() {
        return Err(Error::verification(
            "proof assistant replay theorem evidence_count does not match evidence",
        ));
    }
    if !is_valid_artifact_digest(&theorem.statement_fingerprint) {
        return Err(Error::verification(
            "proof assistant replay theorem statement_fingerprint must be a sha256 digest",
        ));
    }
    let expected_statement = lean_replay_theorem_statement(
        &theorem.theorem_id,
        theorem.obligation_count,
        theorem.evidence_count,
    );
    if theorem.statement_fingerprint != proof_assistant_statement_fingerprint(&expected_statement) {
        return Err(Error::verification(
            "proof assistant replay theorem statement_fingerprint does not match generated statement",
        ));
    }
    verify_proof_assistant_adapter_metadata_shape(theorem)?;
    if theorem.status == "proven" && theorem.evidence.is_empty() {
        return Err(Error::verification(
            "proof assistant replay proven theorem must include evidence",
        ));
    }
    if matches!(theorem.status.as_str(), "runtime_checked" | "assumed")
        && theorem.obligations.is_empty()
    {
        return Err(Error::verification(
            "proof assistant replay theorem with runtime or assumed status must include obligations",
        ));
    }
    Ok(())
}

fn verify_proof_assistant_adapter_metadata_shape(
    theorem: &ProofAssistantReplayTheoremSummary,
) -> Result<()> {
    if theorem.adapter_backend.trim().is_empty()
        || theorem.adapter_backend.contains('/')
        || theorem.adapter_backend.contains('\\')
        || theorem.adapter_backend.contains('"')
        || theorem.adapter_backend.contains('\n')
        || theorem.adapter_backend.contains('\r')
    {
        return Err(Error::verification(
            "proof assistant replay theorem adapter_backend must be a local identifier",
        ));
    }
    if theorem.checker_version.trim().is_empty()
        || theorem.checker_version.contains('"')
        || theorem.checker_version.contains('\n')
        || theorem.checker_version.contains('\r')
    {
        return Err(Error::verification(
            "proof assistant replay theorem checker_version must be a non-empty single-line string",
        ));
    }
    if theorem.proof_status.trim().is_empty()
        || theorem.proof_status.contains('"')
        || theorem.proof_status.contains('\n')
        || theorem.proof_status.contains('\r')
    {
        return Err(Error::verification(
            "proof assistant replay theorem proof_status must be a non-empty single-line string",
        ));
    }
    if !is_valid_artifact_digest(&theorem.adapter_capability_fingerprint) {
        return Err(Error::verification(
            "proof assistant replay theorem adapter_capability_fingerprint must be a sha256 digest",
        ));
    }
    Ok(())
}

fn verify_proof_assistant_adapter_capability_record(
    capability: &ProofAssistantAdapterCapability,
) -> Result<()> {
    if capability.adapter_backend.trim().is_empty()
        || capability.adapter_backend.contains('/')
        || capability.adapter_backend.contains('\\')
        || capability.adapter_backend.contains('"')
        || capability.adapter_backend.contains('\n')
        || capability.adapter_backend.contains('\r')
    {
        return Err(Error::verification(
            "proof assistant adapter capability adapter_backend must be a local identifier",
        ));
    }
    if capability.checker_version.trim().is_empty()
        || capability.checker_version.contains('"')
        || capability.checker_version.contains('\n')
        || capability.checker_version.contains('\r')
    {
        return Err(Error::verification(
            "proof assistant adapter capability checker_version must be a non-empty single-line string",
        ));
    }
    if capability.native_checked {
        if capability.proof_status != "native_checked" {
            return Err(Error::verification(
                "proof assistant native adapter capability must use native_checked proof_status",
            ));
        }
        let Some(digest) = &capability.admission_artifact_digest else {
            return Err(Error::verification(
                "proof assistant native adapter capability requires admission_artifact_digest",
            ));
        };
        if !is_valid_artifact_digest(digest) {
            return Err(Error::verification(
                "proof assistant native adapter admission_artifact_digest must be a sha256 digest",
            ));
        }
    } else {
        let skeleton = proof_assistant_skeleton_adapter_capability();
        if capability != &skeleton {
            return Err(Error::verification(
                "proof assistant placeholder adapter capability is not registered",
            ));
        }
        if capability.admission_artifact_digest.is_some() {
            return Err(Error::verification(
                "proof assistant placeholder adapter capability must not carry admission_artifact_digest",
            ));
        }
    }
    Ok(())
}

fn verify_proof_assistant_native_admission(
    admission: &ProofAssistantNativeAdmission,
) -> Result<()> {
    if let Some(fingerprint) = &admission.plan_fingerprint {
        if !is_valid_artifact_digest(fingerprint) {
            return Err(Error::verification(
                "proof assistant native admission plan_fingerprint must be a sha256 digest",
            ));
        }
    }
    if admission.adapter_backend.trim().is_empty()
        || admission.adapter_backend.contains('/')
        || admission.adapter_backend.contains('\\')
        || admission.adapter_backend.contains('"')
        || admission.adapter_backend.contains('\n')
        || admission.adapter_backend.contains('\r')
    {
        return Err(Error::verification(
            "proof assistant native admission adapter_backend must be a local identifier",
        ));
    }
    if admission.checker_version.trim().is_empty()
        || admission.checker_version.contains('"')
        || admission.checker_version.contains('\n')
        || admission.checker_version.contains('\r')
    {
        return Err(Error::verification(
            "proof assistant native admission checker_version must be a non-empty single-line string",
        ));
    }
    if admission.admission_claim.trim().is_empty()
        || admission.admission_claim.contains('"')
        || admission.admission_claim.contains('\n')
        || admission.admission_claim.contains('\r')
    {
        return Err(Error::verification(
            "proof assistant native admission claim must be a non-empty single-line string",
        ));
    }
    if admission.checked_theorem_count == 0 {
        return Err(Error::verification(
            "proof assistant native admission checked_theorem_count must be positive",
        ));
    }
    if admission.result_status != "accepted" {
        return Err(Error::verification(
            "proof assistant native admission result_status must be accepted",
        ));
    }
    if admission.theorem_result_fingerprints.len() != admission.checked_theorem_count {
        return Err(Error::verification(
            "proof assistant native admission theorem_result_fingerprints length must match checked_theorem_count",
        ));
    }
    if admission
        .theorem_result_fingerprints
        .iter()
        .any(|fingerprint| !is_valid_artifact_digest(fingerprint))
    {
        return Err(Error::verification(
            "proof assistant native admission theorem_result_fingerprints must be sha256 digests",
        ));
    }
    if !is_valid_artifact_digest(&admission.evidence_digest) {
        return Err(Error::verification(
            "proof assistant native admission evidence_digest must be a sha256 digest",
        ));
    }
    Ok(())
}

fn verify_proof_assistant_checker_output(output: &ProofAssistantCheckerOutput) -> Result<()> {
    if !is_valid_artifact_digest(&output.plan_fingerprint) {
        return Err(Error::verification(
            "proof assistant checker output plan_fingerprint must be a sha256 digest",
        ));
    }
    if output.artifact_filename.trim().is_empty()
        || output.artifact_filename.contains('/')
        || output.artifact_filename.contains('\\')
        || !output.artifact_filename.ends_with(".lean-checkable.lean")
    {
        return Err(Error::verification(
            "proof assistant checker output artifact_filename must name a local .lean-checkable.lean artifact",
        ));
    }
    if !is_valid_artifact_digest(&output.artifact_digest) {
        return Err(Error::verification(
            "proof assistant checker output artifact_digest must be a sha256 digest",
        ));
    }
    if !is_valid_artifact_digest(&output.transcript_digest) {
        return Err(Error::verification(
            "proof assistant checker output transcript_digest must be a sha256 digest",
        ));
    }
    if output.adapter_backend.trim().is_empty()
        || output.adapter_backend.contains('/')
        || output.adapter_backend.contains('\\')
        || output.adapter_backend.contains('"')
        || output.adapter_backend.contains('\n')
        || output.adapter_backend.contains('\r')
    {
        return Err(Error::verification(
            "proof assistant checker output adapter_backend must be a local identifier",
        ));
    }
    if output.checker_version.trim().is_empty()
        || output.checker_version.contains('"')
        || output.checker_version.contains('\n')
        || output.checker_version.contains('\r')
    {
        return Err(Error::verification(
            "proof assistant checker output checker_version must be a non-empty single-line string",
        ));
    }
    if output.checked_theorem_count == 0 {
        return Err(Error::verification(
            "proof assistant checker output checked_theorem_count must be positive",
        ));
    }
    if output.result_status != "accepted" {
        return Err(Error::verification(
            "proof assistant checker output result_status must be accepted",
        ));
    }
    Ok(())
}

fn verify_proof_assistant_checker_transcript(
    transcript: &ProofAssistantCheckerTranscript,
) -> Result<()> {
    if !is_valid_artifact_digest(&transcript.plan_fingerprint) {
        return Err(Error::verification(
            "proof assistant checker transcript plan_fingerprint must be a sha256 digest",
        ));
    }
    if transcript.checker_command.trim().is_empty()
        || transcript.checker_command.contains('"')
        || transcript.checker_command.contains('\n')
        || transcript.checker_command.contains('\r')
    {
        return Err(Error::verification(
            "proof assistant checker transcript checker_command must be a non-empty single-line string",
        ));
    }
    if transcript.artifact_filename.trim().is_empty()
        || transcript.artifact_filename.contains('/')
        || transcript.artifact_filename.contains('\\')
        || !transcript
            .artifact_filename
            .ends_with(".lean-checkable.lean")
    {
        return Err(Error::verification(
            "proof assistant checker transcript artifact_filename must name a local .lean-checkable.lean artifact",
        ));
    }
    if !is_valid_artifact_digest(&transcript.artifact_digest) {
        return Err(Error::verification(
            "proof assistant checker transcript artifact_digest must be a sha256 digest",
        ));
    }
    if transcript.exit_status != 0 {
        return Err(Error::verification(
            "proof assistant checker transcript exit_status must be zero",
        ));
    }
    if !is_valid_artifact_digest(&transcript.stdout_digest)
        || !is_valid_artifact_digest(&transcript.stderr_digest)
    {
        return Err(Error::verification(
            "proof assistant checker transcript stdout/stderr digests must be sha256 digests",
        ));
    }
    if transcript.result_status != "accepted" {
        return Err(Error::verification(
            "proof assistant checker transcript result_status must be accepted",
        ));
    }
    Ok(())
}

fn verify_checker_result_index(index: &CheckerResultIndex) -> Result<()> {
    if !is_valid_artifact_digest(&index.plan_fingerprint) {
        return Err(Error::verification(
            "checker result index plan_fingerprint must be a sha256 digest",
        ));
    }
    if index.entry_count != index.entries.len() {
        return Err(Error::verification(
            "checker result index entry_count does not match entries",
        ));
    }
    for entry in &index.entries {
        verify_checker_result_entry(entry)?;
        if entry.plan_fingerprint != index.plan_fingerprint {
            return Err(Error::verification(
                "checker result entry plan_fingerprint does not match index",
            ));
        }
    }
    Ok(())
}

fn verify_checker_result_entry(entry: &CheckerResultEntry) -> Result<()> {
    if !is_valid_theorem_id(&entry.theorem_id) {
        return Err(Error::verification(
            "checker result entry theorem_id must be valid",
        ));
    }
    if !is_valid_artifact_digest(&entry.theorem_result_fingerprint) {
        return Err(Error::verification(
            "checker result entry theorem_result_fingerprint must be a sha256 digest",
        ));
    }
    if !is_valid_artifact_digest(&entry.adapter_capability_fingerprint) {
        return Err(Error::verification(
            "checker result entry adapter_capability_fingerprint must be a sha256 digest",
        ));
    }
    if !is_valid_artifact_digest(&entry.admission_artifact_digest) {
        return Err(Error::verification(
            "checker result entry admission_artifact_digest must be a sha256 digest",
        ));
    }
    if !is_valid_artifact_digest(&entry.plan_fingerprint) {
        return Err(Error::verification(
            "checker result entry plan_fingerprint must be a sha256 digest",
        ));
    }
    Ok(())
}

fn verify_proof_assistant_adapter_registry(registry: &ProofAssistantAdapterRegistry) -> Result<()> {
    if let Some(fingerprint) = &registry.plan_fingerprint {
        if !is_valid_artifact_digest(fingerprint) {
            return Err(Error::verification(
                "proof assistant adapter registry plan_fingerprint must be a sha256 digest",
            ));
        }
    }
    if registry.capabilities.is_empty() {
        return Err(Error::verification(
            "proof assistant adapter registry must contain at least one capability",
        ));
    }
    for capability in &registry.capabilities {
        verify_proof_assistant_adapter_capability_record(capability)?;
    }
    Ok(())
}

fn verify_proof_assistant_summary_matches_adapter_registry(
    summary: &ProofAssistantReplaySummary,
    registry: &ProofAssistantAdapterRegistry,
) -> Result<()> {
    verify_proof_assistant_adapter_registry(registry)?;
    for theorem in &summary.theorems {
        if !registry.capabilities.iter().any(|capability| {
            verify_proof_assistant_adapter_capability_record(capability).is_ok()
                && verify_proof_assistant_theorem_matches_adapter_capability(theorem, capability)
                    .is_ok()
        }) {
            return Err(Error::verification(
                "proof assistant replay theorem adapter metadata is not present in adapter registry artifact",
            ));
        }
    }
    Ok(())
}

fn verify_native_admission_artifacts_cover_registry(
    registry: &ProofAssistantAdapterRegistry,
    admissions: &[(String, ProofAssistantNativeAdmission)],
    summary: &ProofAssistantReplaySummary,
    replay_report: Option<&ProofReplayReport>,
) -> Result<()> {
    for capability in &registry.capabilities {
        if capability.native_checked {
            let Some(admission_digest) = &capability.admission_artifact_digest else {
                return Err(Error::verification(
                    "proof assistant native adapter capability requires admission_artifact_digest",
                ));
            };
            let Some((_, admission)) = admissions
                .iter()
                .find(|(digest, _)| digest == admission_digest)
            else {
                return Err(Error::verification(
                    "proof assistant native adapter admission_artifact_digest is not backed by a trace artifact",
                ));
            };
            if admission.checked_theorem_count != summary.theorem_count {
                return Err(Error::verification(
                    "proof assistant native admission checked_theorem_count does not match theorem summary",
                ));
            }
            if let Some(report) = replay_report {
                if admission.checked_theorem_count != report.checked_proofs {
                    return Err(Error::verification(
                        "proof assistant native admission checked_theorem_count does not match replay report",
                    ));
                }
            }
            let expected_fingerprints = summary
                .theorems
                .iter()
                .map(proof_assistant_native_theorem_result_fingerprint)
                .collect::<Vec<_>>();
            if admission.theorem_result_fingerprints != expected_fingerprints {
                return Err(Error::verification(
                    "proof assistant native admission theorem_result_fingerprints do not match theorem summary",
                ));
            }
        }
    }
    Ok(())
}

fn verify_checker_result_index_matches_trace(
    index: &CheckerResultIndex,
    registry: &ProofAssistantAdapterRegistry,
    admissions: &[(String, ProofAssistantNativeAdmission)],
    summary: &ProofAssistantReplaySummary,
) -> Result<()> {
    verify_checker_result_index(index)?;
    if summary.plan_fingerprint.as_deref() != Some(index.plan_fingerprint.as_str()) {
        return Err(Error::verification(
            "checker result index plan_fingerprint does not match proof assistant summary",
        ));
    }
    if registry.plan_fingerprint.as_deref() != Some(index.plan_fingerprint.as_str()) {
        return Err(Error::verification(
            "checker result index plan_fingerprint does not match adapter registry",
        ));
    }
    let expected = checker_result_index(&index.plan_fingerprint, summary, registry)?;
    if index.entries != expected.entries {
        return Err(Error::verification(
            "checker result index entries do not match theorem summaries and adapter registry",
        ));
    }
    for entry in &index.entries {
        let Some((_, admission)) = admissions
            .iter()
            .find(|(digest, _)| digest == &entry.admission_artifact_digest)
        else {
            return Err(Error::verification(
                "checker result index admission_artifact_digest is not backed by a native admission artifact",
            ));
        };
        if admission.plan_fingerprint.as_deref() != Some(index.plan_fingerprint.as_str()) {
            return Err(Error::verification(
                "checker result index admission plan_fingerprint does not match index",
            ));
        }
        if !admission
            .theorem_result_fingerprints
            .iter()
            .any(|fingerprint| fingerprint == &entry.theorem_result_fingerprint)
        {
            return Err(Error::verification(
                "checker result index theorem_result_fingerprint is not admitted by native admission",
            ));
        }
    }
    Ok(())
}

fn verify_checker_outputs_cover_native_admissions(
    checker_outputs: &[(String, ProofAssistantCheckerOutput)],
    checker_transcripts: &[(String, ProofAssistantCheckerTranscript)],
    admissions: &[(String, ProofAssistantNativeAdmission)],
    checkable_artifact: Option<&(ProofReplayTraceArtifact, String)>,
    summary: &ProofAssistantReplaySummary,
) -> Result<()> {
    if admissions.is_empty() && checker_outputs.is_empty() && checker_transcripts.is_empty() {
        return Ok(());
    }
    let Some((artifact, _contents)) = checkable_artifact else {
        return Err(Error::verification(
            "native proof assistant admissions require a Lean checkable artifact",
        ));
    };
    if checker_outputs.is_empty() {
        return Err(Error::verification(
            "native proof assistant admissions require checker output artifacts",
        ));
    }
    if checker_transcripts.is_empty() {
        return Err(Error::verification(
            "native proof assistant admissions require checker transcript artifacts",
        ));
    }
    for (_, output) in checker_outputs {
        if output.artifact_filename != artifact.filename
            || output.artifact_digest != artifact.digest
        {
            return Err(Error::verification(
                "proof assistant checker output does not match Lean checkable artifact",
            ));
        }
        let Some((_, transcript)) = checker_transcripts
            .iter()
            .find(|(digest, _)| digest == &output.transcript_digest)
        else {
            return Err(Error::verification(
                "proof assistant checker output transcript_digest is not backed by a checker transcript artifact",
            ));
        };
        if transcript.plan_fingerprint != output.plan_fingerprint
            || transcript.artifact_filename != output.artifact_filename
            || transcript.artifact_digest != output.artifact_digest
            || transcript.result_status != output.result_status
        {
            return Err(Error::verification(
                "proof assistant checker transcript does not match checker output",
            ));
        }
        if output.checked_theorem_count != summary.theorem_count {
            return Err(Error::verification(
                "proof assistant checker output checked_theorem_count does not match theorem summary",
            ));
        }
        if summary.plan_fingerprint.as_deref() != Some(output.plan_fingerprint.as_str()) {
            return Err(Error::verification(
                "proof assistant checker output plan_fingerprint does not match theorem summary",
            ));
        }
    }
    for (_, admission) in admissions {
        let Some((_, output)) = checker_outputs.iter().find(|(_, output)| {
            output.plan_fingerprint == admission.plan_fingerprint.clone().unwrap_or_default()
                && output.adapter_backend == admission.adapter_backend
                && output.checker_version == admission.checker_version
                && output.checked_theorem_count == admission.checked_theorem_count
                && output.result_status == admission.result_status
        }) else {
            return Err(Error::verification(
                "proof assistant native admission is not backed by matching checker output",
            ));
        };
        let expected_evidence_digest =
            proof_replay_artifact_digest(&proof_assistant_checker_output_json(output));
        if admission.evidence_digest != expected_evidence_digest {
            return Err(Error::verification(
                "proof assistant native admission evidence_digest does not match checker output",
            ));
        }
    }
    Ok(())
}

fn verify_proof_assistant_summary_matches_skeleton(
    summary: &ProofAssistantReplaySummary,
    skeleton: &ProofAssistantReplaySummary,
) -> Result<()> {
    if summary.dialect != skeleton.dialect
        || summary.plan_fingerprint != skeleton.plan_fingerprint
        || summary.filename != skeleton.filename
        || summary.adapter_registry_filename != skeleton.adapter_registry_filename
        || summary.adapter_registry_digest != skeleton.adapter_registry_digest
        || summary.theorem_count != skeleton.theorem_count
        || summary.theorems.len() != skeleton.theorems.len()
    {
        return Err(Error::verification(
            "proof assistant replay skeleton summary does not match manifest",
        ));
    }
    for (summary, skeleton) in summary.theorems.iter().zip(&skeleton.theorems) {
        if summary.theorem_id != skeleton.theorem_id
            || summary.original_id != skeleton.original_id
            || summary.kind != skeleton.kind
            || summary.status != skeleton.status
            || summary.replay_rule != skeleton.replay_rule
            || summary.obligations != skeleton.obligations
            || summary.evidence != skeleton.evidence
            || summary.obligation_count != skeleton.obligation_count
            || summary.evidence_count != skeleton.evidence_count
            || summary.statement_fingerprint != skeleton.statement_fingerprint
        {
            return Err(Error::verification(
                "proof assistant replay skeleton theorem summary does not match manifest",
            ));
        }
    }
    Ok(())
}

fn verify_proof_assistant_theorem_matches_adapter_capability(
    theorem: &ProofAssistantReplayTheoremSummary,
    capability: &ProofAssistantAdapterCapability,
) -> Result<()> {
    verify_proof_assistant_adapter_metadata_shape(theorem)?;
    verify_proof_assistant_adapter_capability_record(capability)?;
    if capability.adapter_backend == theorem.adapter_backend
        && capability.checker_version == theorem.checker_version
        && capability.proof_status == theorem.proof_status
        && proof_assistant_adapter_capability_fingerprint(capability)
            == theorem.adapter_capability_fingerprint
    {
        if capability.native_checked && theorem.proof_status != "native_checked" {
            return Err(Error::verification(
                "proof assistant replay native adapter must report native_checked status",
            ));
        }
        if !capability.native_checked && theorem.proof_status != PROOF_ASSISTANT_REPLAY_PROOF_STATUS
        {
            return Err(Error::verification(
                "proof assistant replay skeleton adapter must report placeholder status",
            ));
        }
        Ok(())
    } else {
        Err(Error::verification(
            "proof assistant replay theorem adapter metadata does not match adapter capability",
        ))
    }
}

fn proof_assistant_skeleton_line_value(contents: &str, key: &str) -> Option<String> {
    let prefix = format!("{key}: ");
    contents
        .lines()
        .map(str::trim)
        .find_map(|line| line.strip_prefix(&prefix).map(str::to_string))
}

fn verify_proof_replay_trace_artifact_plan_fingerprint(
    artifact: &ProofReplayTraceArtifact,
    contents: &str,
    expected: Option<&str>,
) -> Result<()> {
    if artifact.artifact != PROOF_REPLAY_REPORT_ARTIFACT
        && artifact.artifact != PROOF_ASSISTANT_REPLAY_SKELETON_ARTIFACT
        && artifact.artifact != PROOF_ASSISTANT_LEAN_CHECKABLE_ARTIFACT
        && artifact.artifact != PROOF_ASSISTANT_CHECKER_TRANSCRIPT_ARTIFACT
        && artifact.artifact != PROOF_ASSISTANT_CHECKER_OUTPUT_ARTIFACT
        && artifact.artifact != PROOF_ASSISTANT_ADAPTER_REGISTRY_ARTIFACT
        && artifact.artifact != PROOF_ASSISTANT_NATIVE_ADMISSION_ARTIFACT
        && artifact.artifact != PROOF_ASSISTANT_CHECKER_RESULT_INDEX_ARTIFACT
    {
        return Ok(());
    }
    let Some(expected) = expected else {
        return Ok(());
    };
    match (artifact.artifact.as_str(), artifact.format.as_str()) {
        (PROOF_REPLAY_REPORT_ARTIFACT, "text") => {
            let expected_line = format!("plan fingerprint: {expected}");
            if !contents.contains(&expected_line) {
                return Err(Error::verification(format!(
                    "proof replay text artifact {} plan_fingerprint does not match manifest",
                    artifact.filename
                )));
            }
        }
        (PROOF_REPLAY_REPORT_ARTIFACT, "json") => {
            let report = parse_proof_replay_report_json(contents)?;
            if report.plan_fingerprint.as_deref() != Some(expected) {
                return Err(Error::verification(format!(
                    "proof replay JSON artifact {} plan_fingerprint does not match manifest",
                    artifact.filename
                )));
            }
        }
        (PROOF_ASSISTANT_REPLAY_SKELETON_ARTIFACT, "lean") => {
            let expected_line = format!("plan_fingerprint: {expected}");
            if !contents.contains(&expected_line) {
                return Err(Error::verification(format!(
                    "proof assistant replay skeleton artifact {} plan_fingerprint does not match manifest",
                    artifact.filename
                )));
            }
        }
        (PROOF_ASSISTANT_LEAN_CHECKABLE_ARTIFACT, "lean") => {
            let expected_line = format!("plan_fingerprint: {expected}");
            if !contents.contains(&expected_line) {
                return Err(Error::verification(format!(
                    "proof assistant Lean checkable artifact {} plan_fingerprint does not match manifest",
                    artifact.filename
                )));
            }
        }
        (PROOF_ASSISTANT_CHECKER_TRANSCRIPT_ARTIFACT, "json") => {
            let transcript = parse_proof_assistant_checker_transcript_json(contents)?;
            if transcript.plan_fingerprint != expected {
                return Err(Error::verification(format!(
                    "proof assistant checker transcript artifact {} plan_fingerprint does not match manifest",
                    artifact.filename
                )));
            }
        }
        (PROOF_ASSISTANT_CHECKER_OUTPUT_ARTIFACT, "json") => {
            let output = parse_proof_assistant_checker_output_json(contents)?;
            if output.plan_fingerprint != expected {
                return Err(Error::verification(format!(
                    "proof assistant checker output artifact {} plan_fingerprint does not match manifest",
                    artifact.filename
                )));
            }
        }
        (PROOF_ASSISTANT_ADAPTER_REGISTRY_ARTIFACT, "json") => {
            let registry = parse_proof_assistant_adapter_registry_json(contents)?;
            if registry.plan_fingerprint.as_deref() != Some(expected) {
                return Err(Error::verification(format!(
                    "proof assistant adapter registry artifact {} plan_fingerprint does not match manifest",
                    artifact.filename
                )));
            }
        }
        (PROOF_ASSISTANT_NATIVE_ADMISSION_ARTIFACT, "json") => {
            let admission = parse_proof_assistant_native_admission_json(contents)?;
            if admission.plan_fingerprint.as_deref() != Some(expected) {
                return Err(Error::verification(format!(
                    "proof assistant native admission artifact {} plan_fingerprint does not match manifest",
                    artifact.filename
                )));
            }
        }
        (PROOF_ASSISTANT_CHECKER_RESULT_INDEX_ARTIFACT, "json") => {
            let index = parse_checker_result_index_json(contents)?;
            if index.plan_fingerprint != expected {
                return Err(Error::verification(format!(
                    "checker result index artifact {} plan_fingerprint does not match manifest",
                    artifact.filename
                )));
            }
        }
        _ => {}
    }
    Ok(())
}

pub fn proof_replay_artifact_digest(contents: &str) -> String {
    format!("sha256:{}", sha256_hex(contents.as_bytes()))
}

pub fn proof_replay_plan_fingerprint(plan_key: &PlanCacheKey) -> String {
    let canonical = format!(
        "graph_digest={}\nsemantic={}\nshape_class={}\ndomains={}\nrepresentations={}\ncontracts={}\nbackend={}\nbackend_fingerprint={}\nbackend_capabilities={}\nmathematical_constraint_fingerprint={}\ncapability_version={}\nlowering_rule_ids={}",
        plan_key.graph_digest,
        plan_key.semantic,
        plan_key.shape_class,
        plan_key.domains.join("|"),
        plan_key.representations.join("|"),
        plan_key.contracts.join("|"),
        plan_key.backend,
        plan_key.backend_fingerprint,
        plan_key.backend_capabilities.join("|"),
        plan_key.mathematical_constraint_fingerprint,
        plan_key.capability_version,
        plan_key.lowering_rule_ids.join("|")
    );
    format!("sha256:{}", sha256_hex(canonical.as_bytes()))
}

fn is_valid_artifact_digest(value: &str) -> bool {
    let Some(hex) = value.strip_prefix("sha256:") else {
        return false;
    };
    hex.len() == 64 && hex.bytes().all(|byte| byte.is_ascii_hexdigit())
}

fn proof_replay_trace_signature_value(
    manifest_without_signature: &ProofReplayTraceManifest,
    key_id: &str,
    key_secret: &str,
) -> String {
    let payload = format!(
        "{}\n{}\n{}\n{}",
        PROOF_REPLAY_TRACE_SIGNATURE_ALGORITHM,
        key_id,
        key_secret,
        manifest_without_signature.to_json()
    );
    format!("sha256:{}", sha256_hex(payload.as_bytes()))
}

#[cfg(feature = "ed25519")]
fn proof_replay_trace_public_key_payload(
    manifest_without_signature: &ProofReplayTraceManifest,
) -> String {
    format!(
        "{}\n{}",
        PROOF_REPLAY_TRACE_PUBLIC_KEY_SIGNATURE_ALGORITHM,
        manifest_without_signature.to_json()
    )
}

fn is_valid_keyed_signature_value(value: &str) -> bool {
    is_valid_artifact_digest(value)
}

fn is_valid_ed25519_signature_value(value: &str) -> bool {
    let Some(hex) = value.strip_prefix("ed25519:") else {
        return false;
    };
    hex.len() == 128 && hex.bytes().all(|byte| byte.is_ascii_hexdigit())
}

fn proof_replay_trace_key_fingerprint(key_id: &str, key_secret: &str) -> String {
    format!(
        "sha256:{}",
        sha256_hex(format!("tokitai-trace-key-v1\n{key_id}\n{key_secret}").as_bytes())
    )
}

pub fn proof_replay_trace_public_key_fingerprint(public_key_bytes: &[u8; 32]) -> String {
    format!(
        "sha256:{}",
        sha256_hex(
            [
                b"tokitai-trace-ed25519-public-key-v1\n".as_slice(),
                public_key_bytes.as_slice()
            ]
            .concat()
            .as_slice()
        )
    )
}

pub fn ed25519_public_key_hex(signing_key_bytes: &[u8; 32]) -> String {
    #[cfg(not(feature = "ed25519"))]
    {
        let _ = signing_key_bytes;
        String::new()
    }
    #[cfg(feature = "ed25519")]
    {
        let signing_key = ed25519_dalek::SigningKey::from_bytes(signing_key_bytes);
        bytes_to_hex(signing_key.verifying_key().as_bytes())
    }
}

#[cfg(feature = "ed25519")]
fn ed25519_signature_value(signature_bytes: &[u8; 64]) -> String {
    format!("ed25519:{}", bytes_to_hex(signature_bytes))
}

fn parse_ed25519_public_key_hex(value: &str) -> Result<[u8; 32]> {
    let bytes = hex_to_bytes(value).ok_or_else(|| {
        Error::verification("ed25519 proof replay trace public key must be lowercase hex")
    })?;
    bytes
        .try_into()
        .map_err(|_| Error::verification("ed25519 proof replay trace public key must be 32 bytes"))
}

#[cfg(feature = "ed25519")]
fn parse_ed25519_signature_value(value: &str) -> Result<[u8; 64]> {
    let Some(hex) = value.strip_prefix("ed25519:") else {
        return Err(Error::verification(
            "ed25519 proof replay trace signature value must use ed25519 prefix",
        ));
    };
    let bytes = hex_to_bytes(hex).ok_or_else(|| {
        Error::verification("ed25519 proof replay trace signature must be lowercase hex")
    })?;
    bytes
        .try_into()
        .map_err(|_| Error::verification("ed25519 proof replay trace signature must be 64 bytes"))
}

fn sha256_hex(input: &[u8]) -> String {
    let digest = sha256_digest(input);
    bytes_to_hex(&digest)
}

fn bytes_to_hex(input: &[u8]) -> String {
    input
        .iter()
        .map(|byte| format!("{byte:02x}"))
        .collect::<Vec<_>>()
        .join("")
}

fn hex_to_bytes(input: &str) -> Option<Vec<u8>> {
    if input.len() % 2 != 0 || !input.bytes().all(|byte| byte.is_ascii_hexdigit()) {
        return None;
    }
    let mut bytes = Vec::with_capacity(input.len() / 2);
    for pair in input.as_bytes().chunks_exact(2) {
        let high = hex_nibble(pair[0])?;
        let low = hex_nibble(pair[1])?;
        bytes.push((high << 4) | low);
    }
    Some(bytes)
}

fn hex_nibble(byte: u8) -> Option<u8> {
    match byte {
        b'0'..=b'9' => Some(byte - b'0'),
        b'a'..=b'f' => Some(byte - b'a' + 10),
        b'A'..=b'F' => Some(byte - b'A' + 10),
        _ => None,
    }
}

fn sha256_digest(input: &[u8]) -> [u8; 32] {
    const INITIAL_STATE: [u32; 8] = [
        0x6a09e667, 0xbb67ae85, 0x3c6ef372, 0xa54ff53a, 0x510e527f, 0x9b05688c, 0x1f83d9ab,
        0x5be0cd19,
    ];
    const K: [u32; 64] = [
        0x428a2f98, 0x71374491, 0xb5c0fbcf, 0xe9b5dba5, 0x3956c25b, 0x59f111f1, 0x923f82a4,
        0xab1c5ed5, 0xd807aa98, 0x12835b01, 0x243185be, 0x550c7dc3, 0x72be5d74, 0x80deb1fe,
        0x9bdc06a7, 0xc19bf174, 0xe49b69c1, 0xefbe4786, 0x0fc19dc6, 0x240ca1cc, 0x2de92c6f,
        0x4a7484aa, 0x5cb0a9dc, 0x76f988da, 0x983e5152, 0xa831c66d, 0xb00327c8, 0xbf597fc7,
        0xc6e00bf3, 0xd5a79147, 0x06ca6351, 0x14292967, 0x27b70a85, 0x2e1b2138, 0x4d2c6dfc,
        0x53380d13, 0x650a7354, 0x766a0abb, 0x81c2c92e, 0x92722c85, 0xa2bfe8a1, 0xa81a664b,
        0xc24b8b70, 0xc76c51a3, 0xd192e819, 0xd6990624, 0xf40e3585, 0x106aa070, 0x19a4c116,
        0x1e376c08, 0x2748774c, 0x34b0bcb5, 0x391c0cb3, 0x4ed8aa4a, 0x5b9cca4f, 0x682e6ff3,
        0x748f82ee, 0x78a5636f, 0x84c87814, 0x8cc70208, 0x90befffa, 0xa4506ceb, 0xbef9a3f7,
        0xc67178f2,
    ];

    let mut state = INITIAL_STATE;
    let bit_len = (input.len() as u64) * 8;
    let mut padded = input.to_vec();
    padded.push(0x80);
    while padded.len() % 64 != 56 {
        padded.push(0);
    }
    padded.extend_from_slice(&bit_len.to_be_bytes());

    for block in padded.chunks_exact(64) {
        let mut schedule = [0u32; 64];
        for (index, chunk) in block.chunks_exact(4).take(16).enumerate() {
            schedule[index] = u32::from_be_bytes([chunk[0], chunk[1], chunk[2], chunk[3]]);
        }
        for index in 16..64 {
            let s0 = schedule[index - 15].rotate_right(7)
                ^ schedule[index - 15].rotate_right(18)
                ^ (schedule[index - 15] >> 3);
            let s1 = schedule[index - 2].rotate_right(17)
                ^ schedule[index - 2].rotate_right(19)
                ^ (schedule[index - 2] >> 10);
            schedule[index] = schedule[index - 16]
                .wrapping_add(s0)
                .wrapping_add(schedule[index - 7])
                .wrapping_add(s1);
        }

        let mut a = state[0];
        let mut b = state[1];
        let mut c = state[2];
        let mut d = state[3];
        let mut e = state[4];
        let mut f = state[5];
        let mut g = state[6];
        let mut h = state[7];

        for index in 0..64 {
            let sigma1 = e.rotate_right(6) ^ e.rotate_right(11) ^ e.rotate_right(25);
            let choose = (e & f) ^ ((!e) & g);
            let temp1 = h
                .wrapping_add(sigma1)
                .wrapping_add(choose)
                .wrapping_add(K[index])
                .wrapping_add(schedule[index]);
            let sigma0 = a.rotate_right(2) ^ a.rotate_right(13) ^ a.rotate_right(22);
            let majority = (a & b) ^ (a & c) ^ (b & c);
            let temp2 = sigma0.wrapping_add(majority);

            h = g;
            g = f;
            f = e;
            e = d.wrapping_add(temp1);
            d = c;
            c = b;
            b = a;
            a = temp1.wrapping_add(temp2);
        }

        state[0] = state[0].wrapping_add(a);
        state[1] = state[1].wrapping_add(b);
        state[2] = state[2].wrapping_add(c);
        state[3] = state[3].wrapping_add(d);
        state[4] = state[4].wrapping_add(e);
        state[5] = state[5].wrapping_add(f);
        state[6] = state[6].wrapping_add(g);
        state[7] = state[7].wrapping_add(h);
    }

    let mut digest = [0u8; 32];
    for (index, word) in state.iter().enumerate() {
        digest[index * 4..index * 4 + 4].copy_from_slice(&word.to_be_bytes());
    }
    digest
}

fn sanitize_artifact_stem(stem: &str) -> Result<String> {
    let trimmed = stem.trim();
    if trimmed.is_empty() {
        return Err(Error::verification(
            "proof replay artifact stem must not be empty",
        ));
    }
    let mut sanitized = String::new();
    for ch in trimmed.chars() {
        if ch.is_ascii_alphanumeric() || ch == '-' || ch == '_' {
            sanitized.push(ch);
        } else {
            sanitized.push('_');
        }
    }
    if sanitized.chars().all(|ch| ch == '_') {
        return Err(Error::verification(
            "proof replay artifact stem must include an alphanumeric, dash, or underscore character",
        ));
    }
    Ok(sanitized)
}

fn verify_certificate_entry(proof: &ProofCertificateEntry) -> Result<()> {
    if !is_valid_theorem_id(&proof.theorem_id) {
        return Err(Error::verification(format!(
            "invalid proof theorem id {}",
            proof.theorem_id
        )));
    }
    if proof.original_id.trim().is_empty() {
        return Err(Error::verification(format!(
            "proof {} must keep its original proof object id",
            proof.theorem_id
        )));
    }
    if !matches!(
        proof.kind.as_str(),
        "shape_equality"
            | "valuation_cutoff"
            | "lowering_semantic_preservation"
            | "rewrite_soundness"
    ) {
        return Err(Error::verification(format!(
            "proof {} has unknown kind {}",
            proof.theorem_id, proof.kind
        )));
    }
    if !matches!(
        proof.status.as_str(),
        "proven" | "runtime_checked" | "assumed" | "pending"
    ) {
        return Err(Error::verification(format!(
            "proof {} has unknown status {}",
            proof.theorem_id, proof.status
        )));
    }
    if proof.claim.trim().is_empty() {
        return Err(Error::verification(format!(
            "proof {} must have a nonempty claim",
            proof.theorem_id
        )));
    }
    if proof.status == "proven" && proof.evidence.is_empty() {
        return Err(Error::verification(format!(
            "proven proof {} must include evidence",
            proof.theorem_id
        )));
    }
    if proof.status == "runtime_checked" && proof.obligations.is_empty() {
        return Err(Error::verification(format!(
            "runtime-checked proof {} must include runtime obligations",
            proof.theorem_id
        )));
    }
    if proof.status == "assumed" && proof.obligations.is_empty() {
        return Err(Error::verification(format!(
            "assumed proof {} must explain its assumption obligations",
            proof.theorem_id
        )));
    }
    Ok(())
}

fn replay_shape_equality_proof(plan: &ExecutionPlan, proof: &ProofCertificateEntry) -> Result<()> {
    if proof.status != "proven" {
        return Err(Error::verification(format!(
            "shape equality proof {} must be proven before semantic replay",
            proof.theorem_id
        )));
    }
    if proof.theorem_id != proof_theorem_id(&proof.original_id) {
        return Err(Error::verification(format!(
            "shape equality proof {} theorem id does not match original id {}",
            proof.theorem_id, proof.original_id
        )));
    }
    if !proof.claim.contains("provably equal inner dimensions") {
        return Err(Error::verification(format!(
            "shape equality proof {} claim does not describe inner dimension equality",
            proof.theorem_id
        )));
    }
    if !proof
        .obligations
        .iter()
        .any(|obligation| obligation == "lhs and rhs are rank-2 tensors")
    {
        return Err(Error::verification(format!(
            "shape equality proof {} missing rank-2 obligation",
            proof.theorem_id
        )));
    }
    if !proof
        .obligations
        .iter()
        .any(|obligation| obligation == "inner dimensions are provably equal before lowering")
    {
        return Err(Error::verification(format!(
            "shape equality proof {} missing inner-dimension equality obligation",
            proof.theorem_id
        )));
    }
    let output_shape = proof
        .evidence
        .iter()
        .find_map(|entry| entry.strip_prefix("output_shape="))
        .ok_or_else(|| {
            Error::verification(format!(
                "shape equality proof {} missing output_shape evidence",
                proof.theorem_id
            ))
        })?;
    let Some(plan_proof) = plan
        .proof_objects
        .iter()
        .find(|plan_proof| plan_proof.id == proof.original_id)
    else {
        return Err(Error::verification(format!(
            "shape equality proof {} is not present in plan proof objects",
            proof.original_id
        )));
    };
    if !plan_proof
        .evidence
        .iter()
        .any(|entry| entry == &format!("output_shape={output_shape}"))
    {
        return Err(Error::verification(format!(
            "shape equality proof {} output shape evidence does not match plan",
            proof.theorem_id
        )));
    }
    Ok(())
}

fn replay_valuation_cutoff_proof(
    plan: &ExecutionPlan,
    proof: &ProofCertificateEntry,
) -> Result<()> {
    if proof.theorem_id != proof_theorem_id(&proof.original_id) {
        return Err(Error::verification(format!(
            "valuation cutoff proof {} theorem id does not match original id {}",
            proof.theorem_id, proof.original_id
        )));
    }
    if !proof.claim.contains("cutoff") && !proof.claim.contains("precision") {
        return Err(Error::verification(format!(
            "valuation cutoff proof {} claim does not mention cutoff or precision",
            proof.theorem_id
        )));
    }
    if proof.status == "runtime_checked" {
        replay_runtime_checked_valuation_proof(proof)?;
    } else if proof.status == "pending" {
        replay_pending_valuation_proof(proof)?;
    } else {
        return Err(Error::verification(format!(
            "valuation cutoff proof {} must be runtime_checked or pending",
            proof.theorem_id
        )));
    }
    let Some(plan_proof) = plan
        .proof_objects
        .iter()
        .find(|plan_proof| plan_proof.id == proof.original_id)
    else {
        return Err(Error::verification(format!(
            "valuation cutoff proof {} is not present in plan proof objects",
            proof.original_id
        )));
    };
    for evidence in &proof.evidence {
        if !plan_proof.evidence.iter().any(|entry| entry == evidence) {
            return Err(Error::verification(format!(
                "valuation cutoff proof {} evidence does not match plan: {}",
                proof.theorem_id, evidence
            )));
        }
    }
    Ok(())
}

fn replay_runtime_checked_valuation_proof(proof: &ProofCertificateEntry) -> Result<()> {
    if !proof
        .obligations
        .iter()
        .any(|obligation| obligation.contains("same fixed-precision p-adic domain"))
    {
        return Err(Error::verification(format!(
            "runtime valuation proof {} missing p-adic domain obligation",
            proof.theorem_id
        )));
    }
    if !proof
        .obligations
        .iter()
        .any(|obligation| obligation.contains("active precision cutoff"))
    {
        return Err(Error::verification(format!(
            "runtime valuation proof {} missing active precision cutoff obligation",
            proof.theorem_id
        )));
    }
    if !proof.evidence.iter().any(|evidence| {
        evidence.contains("precision=")
            || evidence.contains("cutoff=")
            || evidence.contains("cutoff")
    }) {
        return Err(Error::verification(format!(
            "runtime valuation proof {} missing precision/cutoff evidence",
            proof.theorem_id
        )));
    }
    Ok(())
}

fn replay_pending_valuation_proof(proof: &ProofCertificateEntry) -> Result<()> {
    if !proof
        .obligations
        .iter()
        .any(|obligation| obligation.contains("runtime executor"))
    {
        return Err(Error::verification(format!(
            "pending valuation proof {} missing runtime executor obligation",
            proof.theorem_id
        )));
    }
    if !proof
        .evidence
        .iter()
        .any(|evidence| evidence.contains("conservative planner estimate"))
    {
        return Err(Error::verification(format!(
            "pending valuation proof {} missing conservative estimate evidence",
            proof.theorem_id
        )));
    }
    if !proof
        .evidence
        .iter()
        .any(|evidence| evidence.contains("cutoff"))
    {
        return Err(Error::verification(format!(
            "pending valuation proof {} missing cutoff evidence",
            proof.theorem_id
        )));
    }
    Ok(())
}

fn replay_lowering_semantic_preservation_proof(
    plan: &ExecutionPlan,
    proof: &ProofCertificateEntry,
) -> Result<()> {
    if proof.status != "proven" {
        return Err(Error::verification(format!(
            "lowering proof {} must be proven before semantic replay",
            proof.theorem_id
        )));
    }
    if proof.theorem_id != proof_theorem_id(&proof.original_id) {
        return Err(Error::verification(format!(
            "lowering proof {} theorem id does not match original id {}",
            proof.theorem_id, proof.original_id
        )));
    }
    let Some(rule_id) = proof.original_id.strip_prefix("proof:lowering:") else {
        return Err(Error::verification(format!(
            "lowering proof {} original id must start with proof:lowering:",
            proof.theorem_id
        )));
    };
    if !proof.claim.contains(rule_id)
        || !proof.claim.contains("preserves semantic operator")
        || !proof.claim.contains("backend")
    {
        return Err(Error::verification(format!(
            "lowering proof {} claim does not describe semantic preservation for its rule",
            proof.theorem_id
        )));
    }
    if !proof.evidence.iter().any(|evidence| {
        evidence.contains("ExactnessPreserved")
            || evidence.contains("MetadataPreserved")
            || evidence.contains("FusionPreserved")
            || evidence.contains("ValuationCutoff")
    }) {
        return Err(Error::verification(format!(
            "lowering proof {} missing recognized lowering preservation evidence",
            proof.theorem_id
        )));
    }
    if !proof.obligations.iter().any(|obligation| {
        obligation.contains("input")
            || obligation.contains("lowering")
            || obligation.contains("semantic")
            || obligation.contains("preserve")
            || obligation.contains("equality")
    }) {
        return Err(Error::verification(format!(
            "lowering proof {} missing lowering semantic obligation",
            proof.theorem_id
        )));
    }
    let Some(plan_proof) = plan
        .proof_objects
        .iter()
        .find(|plan_proof| plan_proof.id == proof.original_id)
    else {
        return Err(Error::verification(format!(
            "lowering proof {} is not present in plan proof objects",
            proof.original_id
        )));
    };
    for evidence in &proof.evidence {
        if !plan_proof.evidence.iter().any(|entry| entry == evidence) {
            return Err(Error::verification(format!(
                "lowering proof {} evidence does not match plan: {}",
                proof.theorem_id, evidence
            )));
        }
    }
    Ok(())
}

fn replay_rewrite_soundness_proof(
    plan: &ExecutionPlan,
    proof: &ProofCertificateEntry,
) -> Result<()> {
    if proof.status != "proven" {
        return Err(Error::verification(format!(
            "rewrite proof {} must be proven before semantic replay",
            proof.theorem_id
        )));
    }
    if proof.theorem_id != proof_theorem_id(&proof.original_id) {
        return Err(Error::verification(format!(
            "rewrite proof {} theorem id does not match original id {}",
            proof.theorem_id, proof.original_id
        )));
    }
    let Some(rule) = proof.original_id.strip_prefix("proof:rewrite:") else {
        return Err(Error::verification(format!(
            "rewrite proof {} original id must start with proof:rewrite:",
            proof.theorem_id
        )));
    };
    if !proof.claim.contains(rule)
        || !proof.claim.contains("sound")
        || !proof.claim.contains("discharged conditions")
    {
        return Err(Error::verification(format!(
            "rewrite proof {} claim does not describe rewrite soundness",
            proof.theorem_id
        )));
    }
    let source_contract = proof
        .evidence
        .iter()
        .find_map(|entry| entry.strip_prefix("source_contract="))
        .ok_or_else(|| {
            Error::verification(format!(
                "rewrite proof {} missing source contract evidence",
                proof.theorem_id
            ))
        })?;
    let discharged_count = proof
        .evidence
        .iter()
        .find_map(|entry| entry.strip_prefix("discharged_conditions="))
        .ok_or_else(|| {
            Error::verification(format!(
                "rewrite proof {} missing discharged condition count evidence",
                proof.theorem_id
            ))
        })?
        .parse::<usize>()
        .map_err(|_| {
            Error::verification(format!(
                "rewrite proof {} has invalid discharged condition count",
                proof.theorem_id
            ))
        })?;
    if discharged_count == 0 || discharged_count != proof.obligations.len() {
        return Err(Error::verification(format!(
            "rewrite proof {} discharged condition count does not match obligations",
            proof.theorem_id
        )));
    }
    let Some(rewrite) = plan
        .rewrites
        .iter()
        .find(|rewrite| rewrite.rule == rule && rewrite.source.0.to_string() == source_contract)
    else {
        return Err(Error::verification(format!(
            "rewrite proof {} does not match a plan rewrite",
            proof.theorem_id
        )));
    };
    if rewrite.discharged_conditions.len() != discharged_count {
        return Err(Error::verification(format!(
            "rewrite proof {} discharged condition count does not match plan",
            proof.theorem_id
        )));
    }
    for condition in &rewrite.discharged_conditions {
        if !proof
            .obligations
            .iter()
            .any(|obligation| obligation == &condition.description)
        {
            return Err(Error::verification(format!(
                "rewrite proof {} missing discharged condition: {}",
                proof.theorem_id, condition.description
            )));
        }
    }
    Ok(())
}

fn parse_proof_certificate_s_expression(input: &str) -> Result<ProofCertificate> {
    let lines = input
        .lines()
        .map(str::trim)
        .filter(|line| !line.is_empty())
        .collect::<Vec<_>>();
    if lines.len() < 4 || lines.first() != Some(&"(tokitai-proof-certificate") {
        return Err(Error::verification(
            "proof certificate must start with (tokitai-proof-certificate",
        ));
    }
    if lines.last() != Some(&")") {
        return Err(Error::verification("proof certificate must end with )"));
    }

    let version = parse_wrapped_u32(lines[1], "version")?;
    let backend = parse_wrapped_string(lines[2], "backend")?;
    let mut proofs = Vec::new();
    let mut index = 3;
    while index + 1 < lines.len() {
        if lines[index] == ")" {
            break;
        }
        if lines[index] != "(proof" {
            return Err(Error::verification(format!(
                "expected proof block at certificate line {}",
                index + 1
            )));
        }
        let (proof, next_index) = parse_certificate_proof(&lines, index + 1)?;
        proofs.push(proof);
        index = next_index;
    }
    Ok(ProofCertificate {
        version,
        backend,
        proofs,
    })
}

fn parse_certificate_proof(
    lines: &[&str],
    mut index: usize,
) -> Result<(ProofCertificateEntry, usize)> {
    let theorem_id = parse_wrapped_symbol(
        *lines
            .get(index)
            .ok_or_else(|| Error::verification("proof block missing theorem"))?,
        "theorem",
    )?;
    index += 1;
    let original_id = parse_wrapped_string(
        *lines
            .get(index)
            .ok_or_else(|| Error::verification("proof block missing original-id"))?,
        "original-id",
    )?;
    index += 1;
    let kind = parse_wrapped_symbol(
        *lines
            .get(index)
            .ok_or_else(|| Error::verification("proof block missing kind"))?,
        "kind",
    )?;
    index += 1;
    let status = parse_wrapped_symbol(
        *lines
            .get(index)
            .ok_or_else(|| Error::verification("proof block missing status"))?,
        "status",
    )?;
    index += 1;
    let claim = parse_wrapped_string(
        *lines
            .get(index)
            .ok_or_else(|| Error::verification("proof block missing claim"))?,
        "claim",
    )?;
    index += 1;
    let (obligations, next_index) = parse_string_list(lines, index, "obligations")?;
    let (evidence, next_index) = parse_string_list(lines, next_index, "evidence")?;
    if lines.get(next_index) != Some(&")") {
        return Err(Error::verification("proof block must end with )"));
    }
    Ok((
        ProofCertificateEntry {
            theorem_id,
            original_id,
            kind,
            status,
            claim,
            obligations,
            evidence,
        },
        next_index + 1,
    ))
}

fn parse_string_list(
    lines: &[&str],
    mut index: usize,
    field: &str,
) -> Result<(Vec<String>, usize)> {
    let expected = format!("({field}");
    if lines.get(index).copied() != Some(expected.as_str()) {
        return Err(Error::verification(format!(
            "proof block missing {field} list"
        )));
    }
    index += 1;
    let mut values = Vec::new();
    loop {
        let Some(line) = lines.get(index) else {
            return Err(Error::verification(format!(
                "{field} list missing closing parenthesis"
            )));
        };
        if *line == ")" {
            return Ok((values, index + 1));
        }
        values.push(parse_json_string_literal(line)?);
        index += 1;
    }
}

fn parse_wrapped_u32(line: &str, field: &str) -> Result<u32> {
    parse_wrapped_symbol(line, field)?
        .parse()
        .map_err(|_| Error::verification(format!("{field} must be an unsigned integer")))
}

fn parse_wrapped_symbol(line: &str, field: &str) -> Result<String> {
    let prefix = format!("({field} ");
    let Some(body) = line
        .strip_prefix(&prefix)
        .and_then(|rest| rest.strip_suffix(')'))
    else {
        return Err(Error::verification(format!("expected ({field} ...)")));
    };
    if body.trim().is_empty() || body.chars().any(char::is_whitespace) {
        return Err(Error::verification(format!(
            "{field} must be a nonempty symbol"
        )));
    }
    Ok(body.to_string())
}

fn parse_wrapped_string(line: &str, field: &str) -> Result<String> {
    let prefix = format!("({field} ");
    let Some(body) = line
        .strip_prefix(&prefix)
        .and_then(|rest| rest.strip_suffix(')'))
    else {
        return Err(Error::verification(format!("expected ({field} ...)")));
    };
    parse_json_string_literal(body)
}

impl MathBoundAuditTrace {
    fn from_plan(
        plan: &ExecutionPlan,
        conformance_result: Option<String>,
        benchmark_environment: Option<String>,
    ) -> Self {
        let plan_fingerprint = plan
            .cache_key
            .as_ref()
            .map(proof_replay_plan_fingerprint)
            .unwrap_or_else(|| fingerprint_label("missing-plan-cache-key"));
        let capability_fingerprint = plan
            .cache_key
            .as_ref()
            .map(|key| key.backend_fingerprint.clone())
            .unwrap_or_else(|| fingerprint_label(&format!("backend={}", plan.backend)));
        let mut lowering_rule_ids = plan
            .steps
            .iter()
            .filter_map(|step| step.lowering_rule_id.clone())
            .collect::<Vec<_>>();
        lowering_rule_ids.sort();
        lowering_rule_ids.dedup();
        Self {
            plan_fingerprint,
            backend_id: plan.backend.clone(),
            device_kind: infer_device_kind(&plan.backend),
            capability_fingerprint,
            p_adic_constraint_fingerprint: p_adic_constraint_fingerprint(plan),
            sheaf_constraint_fingerprint: sheaf_constraint_fingerprint(plan),
            lowering_rule_ids,
            fallback_reason: plan
                .fallback
                .as_ref()
                .map(|fallback| fallback.reason.clone())
                .or_else(|| {
                    plan.cost
                        .semantic
                        .fallback
                        .as_ref()
                        .map(|fallback| fallback.reason.clone())
                }),
            conformance_result,
            benchmark_environment,
        }
    }

    fn to_json(&self) -> String {
        let lowering_rule_ids = self
            .lowering_rule_ids
            .iter()
            .map(|rule| json_string(rule))
            .collect::<Vec<_>>()
            .join(",");
        format!(
            "{{\"artifact\":{},\"version\":{},\"plan_fingerprint\":{},\"backend_id\":{},\"device_kind\":{},\"capability_fingerprint\":{},\"p_adic_constraint_fingerprint\":{},\"sheaf_constraint_fingerprint\":{},\"lowering_rule_ids\":[{}],\"fallback_reason\":{},\"conformance_result\":{},\"benchmark_environment\":{}}}",
            json_string(MATH_BOUND_AUDIT_TRACE_ARTIFACT),
            MATH_BOUND_AUDIT_TRACE_VERSION,
            json_string(&self.plan_fingerprint),
            json_string(&self.backend_id),
            json_string(&self.device_kind),
            json_string(&self.capability_fingerprint),
            json_string(&self.p_adic_constraint_fingerprint),
            json_string(&self.sheaf_constraint_fingerprint),
            lowering_rule_ids,
            json_option_string(&self.fallback_reason),
            json_option_string(&self.conformance_result),
            json_option_string(&self.benchmark_environment)
        )
    }
}

impl AuditStep {
    fn from_step(step: &PlanStep) -> Self {
        Self {
            node_id: step.node_id,
            op_name: step.op_name.clone(),
            backend: step.backend.clone(),
            domain: step.domain.clone(),
            representation: step.representation.clone(),
            lowering_rule_id: step.lowering_rule_id.clone(),
            kind: match &step.kind {
                PlanStepKind::Single => "single".to_string(),
                PlanStepKind::Fused { .. } => "fused".to_string(),
                PlanStepKind::PadicValuationSkip { .. } => "padic_valuation_skip".to_string(),
                PlanStepKind::PadicMatmulValuationSkip { .. } => {
                    "padic_matmul_valuation_skip".to_string()
                }
                PlanStepKind::CoverGlueCheck { .. } => "cover_glue_check".to_string(),
            },
        }
    }

    fn to_json(&self) -> String {
        format!(
            "{{\"node_id\":{},\"op_name\":{},\"backend\":{},\"domain\":{},\"representation\":{},\"lowering_rule_id\":{},\"kind\":{}}}",
            self.node_id,
            json_string(&self.op_name),
            json_string(&self.backend),
            json_string(&self.domain),
            json_string(&self.representation),
            json_option_string(&self.lowering_rule_id),
            json_string(&self.kind)
        )
    }
}

impl AuditObligation {
    fn to_json(&self) -> String {
        format!(
            "{{\"source\":{},\"severity\":{},\"status\":{},\"condition\":{}}}",
            json_string(&self.source),
            json_string(&self.severity),
            json_string(&self.status),
            json_string(&self.condition)
        )
    }
}

impl AuditRewrite {
    fn to_json(&self) -> String {
        format!(
            "{{\"source\":{},\"rule\":{},\"discharged_conditions\":{}}}",
            json_string(&self.source),
            json_string(&self.rule),
            self.discharged_conditions
        )
    }
}

impl AuditProofObject {
    fn from_proof_object(proof: &ProofObject) -> Self {
        Self {
            id: proof.id.clone(),
            kind: format_proof_kind(&proof.kind),
            claim: proof.claim.clone(),
            status: format_proof_status(&proof.status),
            obligations: proof.obligations.clone(),
            evidence: proof.evidence.clone(),
        }
    }

    fn to_json(&self) -> String {
        let obligations = self
            .obligations
            .iter()
            .map(|entry| json_string(entry))
            .collect::<Vec<_>>()
            .join(",");
        let evidence = self
            .evidence
            .iter()
            .map(|entry| json_string(entry))
            .collect::<Vec<_>>()
            .join(",");
        format!(
            "{{\"id\":{},\"kind\":{},\"claim\":{},\"status\":{},\"obligations\":[{}],\"evidence\":[{}]}}",
            json_string(&self.id),
            json_string(&self.kind),
            json_string(&self.claim),
            json_string(&self.status),
            obligations,
            evidence
        )
    }
}

impl AuditCost {
    fn from_plan(plan: &ExecutionPlan) -> Self {
        let mut semantic = Vec::new();
        if let Some(precision) = &plan.cost.semantic.precision {
            semantic.push(format!(
                "precision input_digits={}, output_digits={}, loss={}",
                precision.input_digits, precision.output_digits, precision.precision_loss
            ));
        }
        if let Some(valuation) = &plan.cost.semantic.valuation {
            semantic.push(format!(
                "valuation cutoff={}, estimated_terms={}, skipped={}, evaluated={}, rationale={}",
                valuation.cutoff,
                valuation.estimated_terms,
                valuation.estimated_skipped_terms,
                valuation.estimated_evaluated_terms,
                valuation.rationale
            ));
        }
        if let Some(verification) = &plan.cost.semantic.verification {
            semantic.push(format!(
                "verification required_checks={}, overhead_ns={:?}",
                verification.required_checks, verification.estimated_overhead_ns
            ));
        }
        if let Some(fallback) = &plan.cost.semantic.fallback {
            semantic.push(format!(
                "fallback penalty_ns={:?}, reason={}",
                fallback.penalty_ns, fallback.reason
            ));
        }
        Self {
            runtime_ns: plan.cost.estimated_runtime_ns,
            memory_bytes: plan.cost.estimated_memory_bytes,
            precision_loss: plan.cost.precision_loss,
            unresolved_obligations: plan.cost.unresolved_obligations,
            semantic,
        }
    }

    fn to_json(&self) -> String {
        let semantic = self
            .semantic
            .iter()
            .map(|entry| json_string(entry))
            .collect::<Vec<_>>()
            .join(",");
        format!(
            "{{\"runtime_ns\":{},\"memory_bytes\":{},\"precision_loss\":{},\"unresolved_obligations\":{},\"semantic\":[{}]}}",
            json_option_u64(self.runtime_ns),
            json_option_u64(self.memory_bytes),
            json_option_u32(self.precision_loss),
            self.unresolved_obligations,
            semantic
        )
    }
}

fn format_obligation_source(source: &ObligationSource) -> String {
    match source {
        ObligationSource::Operator(value) => format!("operator:{value}"),
        ObligationSource::Rewrite(value) => format!("rewrite:{value}"),
        ObligationSource::Planner(value) => format!("planner:{value}"),
        ObligationSource::Backend(value) => format!("backend:{value}"),
    }
}

fn format_obligation_severity(severity: &ObligationSeverity) -> String {
    match severity {
        ObligationSeverity::Required => "required".to_string(),
        ObligationSeverity::Warning => "warning".to_string(),
        ObligationSeverity::AuditOnly => "audit_only".to_string(),
    }
}

fn format_discharge_status(status: &DischargeStatus) -> String {
    match status {
        DischargeStatus::Unresolved => "unresolved".to_string(),
        DischargeStatus::Discharged(value) => format!("discharged:{value}"),
        DischargeStatus::Waived(value) => format!("waived:{value}"),
    }
}

fn format_proof_kind(kind: &ProofKind) -> String {
    match kind {
        ProofKind::ShapeEquality => "shape_equality".to_string(),
        ProofKind::ValuationCutoff => "valuation_cutoff".to_string(),
        ProofKind::LoweringSemanticPreservation => "lowering_semantic_preservation".to_string(),
        ProofKind::RewriteSoundness => "rewrite_soundness".to_string(),
    }
}

fn format_proof_status(status: &ProofStatus) -> String {
    match status {
        ProofStatus::Proven => "proven".to_string(),
        ProofStatus::RuntimeChecked => "runtime_checked".to_string(),
        ProofStatus::Assumed => "assumed".to_string(),
        ProofStatus::Pending => "pending".to_string(),
    }
}

fn json_option_string(value: &Option<String>) -> String {
    value
        .as_ref()
        .map_or_else(|| "null".to_string(), |item| json_string(item))
}

fn json_option_signature(value: &Option<ProofReplayTraceSignature>) -> String {
    value
        .as_ref()
        .map_or_else(|| "null".to_string(), |signature| signature.to_json())
}

fn json_option_tuning(value: &Option<ProofReplayTraceTuning>) -> String {
    value
        .as_ref()
        .map_or_else(|| "null".to_string(), |tuning| tuning.to_manifest_json())
}

fn json_option_proof_assistant_summary(value: &Option<ProofAssistantReplaySummary>) -> String {
    value
        .as_ref()
        .map_or_else(|| "null".to_string(), |summary| summary.to_json())
}

fn json_option_u64(value: Option<u64>) -> String {
    value.map_or_else(|| "null".to_string(), |item| item.to_string())
}

fn json_option_u32(value: Option<u32>) -> String {
    value.map_or_else(|| "null".to_string(), |item| item.to_string())
}

fn json_object_input(input: &str) -> String {
    let trimmed = input.trim();
    if trimmed.starts_with('{') {
        trimmed.to_string()
    } else {
        format!("{{{trimmed}}}")
    }
}

fn parse_json_object_fields(input: &str, context: &str) -> Result<Vec<(String, String)>> {
    let compact = compact_json_outside_strings(input)?;
    let Some(body) = compact
        .strip_prefix('{')
        .and_then(|item| item.strip_suffix('}'))
    else {
        return Err(Error::verification(format!(
            "{context} has unsupported object shape"
        )));
    };
    if body.is_empty() {
        return Ok(Vec::new());
    }
    let mut fields = Vec::new();
    for field in split_json_top_level(body, ',', context)? {
        let (key_literal, value) = split_json_field(&field, context)?;
        let key = parse_json_string_literal(key_literal)?;
        if fields.iter().any(|(existing, _)| existing == &key) {
            return Err(Error::verification(format!(
                "{context} has duplicate field {key}"
            )));
        }
        fields.push((key, value.to_string()));
    }
    Ok(fields)
}

fn validate_json_object_field_set(
    fields: &[(String, String)],
    expected: &[&str],
    context: &str,
) -> Result<()> {
    for required in expected {
        if !fields.iter().any(|(key, _)| key == required) {
            return Err(Error::verification(format!(
                "{context} missing field {required}"
            )));
        }
    }
    for (key, _) in fields {
        if !expected.iter().any(|expected_key| expected_key == key) {
            return Err(Error::verification(format!(
                "{context} has unsupported field {key}"
            )));
        }
    }
    Ok(())
}

fn json_field<'a>(fields: &'a [(String, String)], key: &str, context: &str) -> Result<&'a str> {
    fields
        .iter()
        .find(|(field_key, _)| field_key == key)
        .map(|(_, value)| value.as_str())
        .ok_or_else(|| Error::verification(format!("{context} missing field {key}")))
}

fn json_field_string(fields: &[(String, String)], key: &str, context: &str) -> Result<String> {
    parse_json_string_literal(json_field(fields, key, context)?)
}

fn json_field_option_string(
    fields: &[(String, String)],
    key: &str,
    context: &str,
) -> Result<Option<String>> {
    let value = json_field(fields, key, context)?;
    if value == "null" {
        Ok(None)
    } else {
        parse_json_string_literal(value).map(Some)
    }
}

fn json_field_string_array(
    fields: &[(String, String)],
    key: &str,
    context: &str,
) -> Result<Vec<String>> {
    parse_json_array_items(json_field(fields, key, context)?, context)?
        .iter()
        .map(|item| parse_json_string_literal(item))
        .collect()
}

fn json_field_u32(fields: &[(String, String)], key: &str, context: &str) -> Result<u32> {
    json_field(fields, key, context)?
        .parse::<u32>()
        .map_err(|_| Error::verification(format!("{context} field {key} must be u32")))
}

fn json_field_u64(fields: &[(String, String)], key: &str, context: &str) -> Result<u64> {
    json_field(fields, key, context)?
        .parse::<u64>()
        .map_err(|_| Error::verification(format!("{context} field {key} must be u64")))
}

fn json_field_usize(fields: &[(String, String)], key: &str, context: &str) -> Result<usize> {
    json_field(fields, key, context)?
        .parse::<usize>()
        .map_err(|_| Error::verification(format!("{context} field {key} must be usize")))
}

fn json_field_i32(fields: &[(String, String)], key: &str, context: &str) -> Result<i32> {
    json_field(fields, key, context)?
        .parse::<i32>()
        .map_err(|_| Error::verification(format!("{context} field {key} must be i32")))
}

fn json_field_bool(fields: &[(String, String)], key: &str, context: &str) -> Result<bool> {
    match json_field(fields, key, context)? {
        "true" => Ok(true),
        "false" => Ok(false),
        _ => Err(Error::verification(format!(
            "{context} field {key} must be bool"
        ))),
    }
}

fn parse_json_array_items(input: &str, context: &str) -> Result<Vec<String>> {
    let compact = compact_json_outside_strings(input)?;
    let Some(body) = compact
        .strip_prefix('[')
        .and_then(|item| item.strip_suffix(']'))
    else {
        return Err(Error::verification(format!(
            "{context} has unsupported array shape"
        )));
    };
    if body.is_empty() {
        Ok(Vec::new())
    } else {
        split_json_top_level(body, ',', context)
    }
}

fn split_json_field<'a>(field: &'a str, context: &str) -> Result<(&'a str, &'a str)> {
    let Some(index) = find_json_top_level_delimiter(field, ':')? else {
        return Err(Error::verification(format!(
            "{context} field is missing ':' delimiter"
        )));
    };
    Ok((&field[..index], &field[index + 1..]))
}

fn split_json_top_level(input: &str, delimiter: char, context: &str) -> Result<Vec<String>> {
    let mut parts = Vec::new();
    let mut start = 0;
    let mut rest = input;
    while let Some(index) = find_json_top_level_delimiter(rest, delimiter)? {
        parts.push(rest[..index].to_string());
        start += index + delimiter.len_utf8();
        rest = &input[start..];
    }
    if !rest.is_empty() {
        parts.push(rest.to_string());
    } else {
        return Err(Error::verification(format!(
            "{context} has trailing delimiter"
        )));
    }
    Ok(parts)
}

fn find_json_top_level_delimiter(input: &str, delimiter: char) -> Result<Option<usize>> {
    let mut in_string = false;
    let mut escaped = false;
    let mut depth = 0i32;
    for (index, ch) in input.char_indices() {
        if in_string {
            if escaped {
                escaped = false;
            } else if ch == '\\' {
                escaped = true;
            } else if ch == '"' {
                in_string = false;
            }
            continue;
        }
        match ch {
            '"' => in_string = true,
            '{' | '[' => depth += 1,
            '}' | ']' => {
                depth -= 1;
                if depth < 0 {
                    return Err(Error::verification("unbalanced JSON delimiters"));
                }
            }
            ch if ch == delimiter && depth == 0 => return Ok(Some(index)),
            _ => {}
        }
    }
    if in_string {
        return Err(Error::verification("unterminated JSON string"));
    }
    if depth != 0 {
        return Err(Error::verification("unbalanced JSON delimiters"));
    }
    Ok(None)
}

fn compact_json_outside_strings(input: &str) -> Result<String> {
    let mut compact = String::with_capacity(input.len());
    let mut in_string = false;
    let mut escaped = false;
    for ch in input.trim().chars() {
        if in_string {
            compact.push(ch);
            if escaped {
                escaped = false;
            } else if ch == '\\' {
                escaped = true;
            } else if ch == '"' {
                in_string = false;
            }
            continue;
        }
        if ch == '"' {
            in_string = true;
            compact.push(ch);
        } else if !ch.is_whitespace() {
            compact.push(ch);
        }
    }
    if in_string {
        return Err(Error::verification("unterminated JSON string"));
    }
    Ok(compact)
}

fn json_string(value: &str) -> String {
    let mut escaped = String::from("\"");
    for ch in value.chars() {
        match ch {
            '"' => escaped.push_str("\\\""),
            '\\' => escaped.push_str("\\\\"),
            '\n' => escaped.push_str("\\n"),
            '\r' => escaped.push_str("\\r"),
            '\t' => escaped.push_str("\\t"),
            ch if ch.is_control() => escaped.push_str(&format!("\\u{:04x}", ch as u32)),
            ch => escaped.push(ch),
        }
    }
    escaped.push('"');
    escaped
}

fn parse_json_string_literal(value: &str) -> Result<String> {
    if !value.starts_with('"') || !value.ends_with('"') {
        return Err(Error::verification("expected quoted string literal"));
    }
    let mut decoded = String::new();
    let mut chars = value[1..value.len() - 1].chars();
    while let Some(ch) = chars.next() {
        if ch != '\\' {
            decoded.push(ch);
            continue;
        }
        let Some(escaped) = chars.next() else {
            return Err(Error::verification("unterminated string escape"));
        };
        match escaped {
            '"' => decoded.push('"'),
            '\\' => decoded.push('\\'),
            'n' => decoded.push('\n'),
            'r' => decoded.push('\r'),
            't' => decoded.push('\t'),
            'u' => {
                let digits = [chars.next(), chars.next(), chars.next(), chars.next()];
                let Some(hex) = digits.into_iter().collect::<Option<String>>() else {
                    return Err(Error::verification("incomplete unicode escape"));
                };
                let code = u32::from_str_radix(&hex, 16)
                    .map_err(|_| Error::verification("invalid unicode escape"))?;
                let Some(decoded_char) = char::from_u32(code) else {
                    return Err(Error::verification("invalid unicode scalar value"));
                };
                decoded.push(decoded_char);
            }
            other => {
                return Err(Error::verification(format!(
                    "unsupported string escape \\{other}"
                )));
            }
        }
    }
    Ok(decoded)
}

fn sexp_string(value: &str) -> String {
    json_string(value)
}

fn proof_theorem_id(value: &str) -> String {
    let mut theorem = String::from("tokitai_");
    let mut previous_was_separator = false;
    for ch in value.chars() {
        if ch.is_ascii_alphanumeric() {
            theorem.push(ch.to_ascii_lowercase());
            previous_was_separator = false;
        } else if !previous_was_separator {
            theorem.push('_');
            previous_was_separator = true;
        }
    }
    while theorem.ends_with('_') {
        theorem.pop();
    }
    theorem
}

fn infer_device_kind(backend: &str) -> String {
    if backend.contains("gpu") {
        "gpu".to_string()
    } else if backend.contains("cpu") {
        "cpu".to_string()
    } else {
        "unknown".to_string()
    }
}

fn fingerprint_label(value: &str) -> String {
    format!("sha256:{}", sha256_hex(value.as_bytes()))
}

fn p_adic_constraint_fingerprint(plan: &ExecutionPlan) -> String {
    if let Some(resource) = &plan.resources.padic {
        return fingerprint_label(&format!(
            "prime={};precision={};valuation_cutoff={};equality_digits={};backend_capability={};fallback={}",
            resource.prime,
            resource.precision,
            resource.valuation_cutoff,
            resource.equality_digits,
            resource.backend_capability,
            resource.fallback_reason.as_deref().unwrap_or("none")
        ));
    }
    let domains = plan
        .steps
        .iter()
        .filter(|step| step.domain.starts_with("Q_") || step.domain.contains("padic"))
        .map(|step| format!("{}:{}", step.op_name, step.domain))
        .collect::<Vec<_>>();
    if domains.is_empty() {
        fingerprint_label("p-adic:none")
    } else {
        fingerprint_label(&domains.join("|"))
    }
}

fn sheaf_constraint_fingerprint(plan: &ExecutionPlan) -> String {
    let mut constraints = Vec::new();
    for step in &plan.steps {
        if let PlanStepKind::CoverGlueCheck { target, opens } = &step.kind {
            constraints.push(format!(
                "cover_glue_check:target={target}:opens={}",
                opens.join("+")
            ));
        } else if step.domain.starts_with("cover:") {
            constraints.push(format!("{}:{}", step.op_name, step.domain));
        }
    }
    if constraints.is_empty() {
        fingerprint_label("sheaf:none")
    } else {
        fingerprint_label(&constraints.join("|"))
    }
}

fn format_conformance_result(conformance: &BackendConformanceRunReport) -> String {
    format!(
        "oracle={}, candidate={}, passed={}, cases={}, fallback_cases={}",
        conformance.oracle_backend,
        conformance.candidate_backend,
        conformance.passed(),
        conformance.cases.len(),
        conformance.fallback_cases().len()
    )
}

fn format_math_bound_report(trace: &MathBoundAuditTrace) -> Vec<String> {
    vec![
        format!("math-bound backend_id={}", trace.backend_id),
        format!("math-bound device_kind={}", trace.device_kind),
        format!(
            "math-bound capability_fingerprint={}",
            trace.capability_fingerprint
        ),
        format!(
            "math-bound p_adic_constraint_fingerprint={}",
            trace.p_adic_constraint_fingerprint
        ),
        format!(
            "math-bound sheaf_constraint_fingerprint={}",
            trace.sheaf_constraint_fingerprint
        ),
        format!(
            "math-bound lowering_rule_ids={}",
            trace.lowering_rule_ids.join("|")
        ),
        format!(
            "math-bound fallback_reason={}",
            trace.fallback_reason.as_deref().unwrap_or("none")
        ),
        format!(
            "math-bound conformance_result={}",
            trace.conformance_result.as_deref().unwrap_or("none")
        ),
        format!(
            "math-bound benchmark_environment={}",
            trace.benchmark_environment.as_deref().unwrap_or("none")
        ),
    ]
}

fn is_valid_theorem_id(value: &str) -> bool {
    let Some(rest) = value.strip_prefix("tokitai_") else {
        return false;
    };
    !rest.is_empty()
        && value
            .chars()
            .all(|ch| ch.is_ascii_lowercase() || ch.is_ascii_digit() || ch == '_')
        && !value.ends_with('_')
        && !value.contains("__")
}

fn format_cost_report(plan: &ExecutionPlan) -> Vec<String> {
    let mut lines = Vec::new();
    lines.push(format!(
        "cost: runtime_ns={:?}, memory_bytes={:?}, precision_loss={:?}, unresolved_obligations={}",
        plan.cost.estimated_runtime_ns,
        plan.cost.estimated_memory_bytes,
        plan.cost.precision_loss,
        plan.cost.unresolved_obligations
    ));

    if let Some(precision) = &plan.cost.semantic.precision {
        lines.push(format!(
            "semantic cost: precision input_digits={}, output_digits={}, loss={}",
            precision.input_digits, precision.output_digits, precision.precision_loss
        ));
    }
    if let Some(valuation) = &plan.cost.semantic.valuation {
        lines.push(format!(
            "semantic cost: valuation cutoff={}, estimated_terms={}, skipped={}, evaluated={}, rationale={}",
            valuation.cutoff,
            valuation.estimated_terms,
            valuation.estimated_skipped_terms,
            valuation.estimated_evaluated_terms,
            valuation.rationale
        ));
    }
    if let Some(verification) = &plan.cost.semantic.verification {
        lines.push(format!(
            "semantic cost: verification required_checks={}, overhead_ns={:?}",
            verification.required_checks, verification.estimated_overhead_ns
        ));
    }
    if let Some(fallback) = &plan.cost.semantic.fallback {
        lines.push(format!(
            "semantic cost: fallback penalty_ns={:?}, reason={}",
            fallback.penalty_ns, fallback.reason
        ));
    }

    lines
}

pub fn audit_report(plan: &ExecutionPlan) -> String {
    let mut lines: Vec<String> = Vec::new();
    lines.push(format!("backend: {}", plan.backend));
    lines.push(format!("steps: {}", plan.steps.len()));
    lines.push(format!("obligations: {}", plan.obligations.len()));
    lines.push(format!("proof_objects: {}", plan.proof_objects.len()));
    for step in &plan.steps {
        lines.push(format_plan_step(step));
    }
    // Structured rewrites summary line: tests look for "structured rewrites: N"
    lines.push(format!("structured rewrites: {}", plan.rewrites.len()));
    for rewrite in &plan.rewrites {
        lines.push(format!(
            "rewrite: source={:?}, rule={}, discharged_conditions={}",
            rewrite.source,
            rewrite.rule,
            rewrite.discharged_conditions.len()
        ));
    }
    lines.extend(format_cost_report(plan));
    if let Some(valuation) = &plan.cost.semantic.valuation {
        if !valuation.rationale.is_empty() {
            lines.push(format!("cost rationale: {}", valuation.rationale));
        }
        // Emit a p-adic matmul valuation cost summary for matmul steps.
        let has_matmul = plan.steps.iter().any(|s| {
            matches!(
                s.kind,
                crate::planner::PlanStepKind::PadicMatmulValuationSkip { .. }
            )
        });
        if has_matmul {
            lines.push(format!(
                "p-adic matmul valuation cost: cutoff={}, skipped={}, evaluated={}",
                valuation.cutoff,
                valuation.estimated_skipped_terms,
                valuation.estimated_evaluated_terms
            ));
        }
    }
    for proof in &plan.proof_objects {
        if matches!(proof.kind, crate::planner::ProofKind::ShapeEquality) {
            lines.push(format!(
                "shape proof: id={}, claim={}, status={:?}",
                proof.id, proof.claim, proof.status
            ));
            // The evidence lines contain output_shape=... which is what tests
            // look for. Surface them as plain "output shape [...]" lines.
            for ev in &proof.evidence {
                if let Some(rest) = ev.strip_prefix("output_shape=") {
                    lines.push(format!("output shape {}", rest));
                } else {
                    lines.push(format!("  evidence: {ev}"));
                }
            }
        }
    }
    let evidence_lines = format_lowering_evidence(plan);
    lines.extend(evidence_lines);
    // Math-bound report: capability and constraint fingerprints that bound the
    // plan's executor semantics. The conformance and benchmark environment
    // fields are null in the base report; pass them through
    // `audit_report_with_conformance` to add cross-backend oracle output.
    lines.extend(format_math_bound_report(&MathBoundAuditTrace::from_plan(
        plan, None, None,
    )));
    lines.join("\n")
}

fn format_lowering_evidence(plan: &ExecutionPlan) -> Vec<String> {
    let mut lines: Vec<String> = Vec::new();
    for step in &plan.steps {
        if let Some(rule_id) = &step.lowering_rule_id {
            lines.push(format!(
                "lowering evidence: rule={}, kind=ExactnessPreserved, op={}, step={}",
                rule_id, step.op_name, step.node_id
            ));
        }
    }
    lines
}

pub fn audit_report_with_properties(
    plan: &ExecutionPlan,
    properties: &[PropertyCheckReport],
) -> String {
    let mut report = audit_report(plan);
    report.push('\n');
    report.push_str(&format_property_reports(properties));
    report
}

pub fn audit_report_with_conformance(
    plan: &ExecutionPlan,
    conformance: &BackendConformanceRunReport,
) -> String {
    let mut lines = audit_report(plan)
        .lines()
        .map(ToString::to_string)
        .collect::<Vec<_>>();
    lines.extend(format_math_bound_report(&MathBoundAuditTrace::from_plan(
        plan,
        Some(format_conformance_result(conformance)),
        None,
    )));
    lines.join("\n")
}

pub fn format_property_reports(properties: &[PropertyCheckReport]) -> String {
    let mut lines = Vec::new();
    lines.push(format!("property checks: {}", properties.len()));
    for property in properties {
        lines.push(format!(
            "property: name={}, passed={}, samples={}, message={}",
            property.property, property.passed, property.samples_checked, property.message
        ));
    }
    lines.join("\n")
}

fn format_plan_step(step: &PlanStep) -> String {
    match &step.kind {
        PlanStepKind::Single => format!(
            "step: node={}, op={}, backend={}, kind=single, domain={}, representation={}, lowering_rule={:?}",
            step.node_id,
            step.op_name,
            step.backend,
            step.domain,
            step.representation,
            step.lowering_rule_id
        ),
        PlanStepKind::Fused { node_ids, rule } => format!(
            "step: node={}, op={}, backend={}, kind=fused, nodes={:?}, rule={}, domain={}, representation={}, lowering_rule={:?}",
            step.node_id,
            step.op_name,
            step.backend,
            node_ids,
            rule,
            step.domain,
            step.representation,
            step.lowering_rule_id
        ),
        PlanStepKind::PadicValuationSkip {
            lhs_id,
            rhs_id,
            output_id,
            prime,
            precision,
        } => format!(
            "step: node={}, op={}, backend={}, kind=padic_valuation_skip, lhs={}, rhs={}, output={}, prime={}, precision={}, domain={}, representation={}, lowering_rule={:?}",
            step.node_id,
            step.op_name,
            step.backend,
            lhs_id,
            rhs_id,
            output_id,
            prime,
            precision,
            step.domain,
            step.representation,
            step.lowering_rule_id
        ),
        PlanStepKind::PadicMatmulValuationSkip {
            lhs_id,
            rhs_id,
            output_id,
            prime,
            precision,
            certificate_policy,
            valuation_bucket_fingerprint,
        } => format!(
            "step: node={}, op={}, backend={}, kind=padic_matmul_valuation_skip, lhs={}, rhs={}, output={}, prime={}, precision={}, certificate_policy={}, valuation_bucket_fingerprint={}, domain={}, representation={}, lowering_rule={:?}",
            step.node_id,
            step.op_name,
            step.backend,
            lhs_id,
            rhs_id,
            output_id,
            prime,
            precision,
            certificate_policy,
            valuation_bucket_fingerprint,
            step.domain,
            step.representation,
            step.lowering_rule_id
        ),
        PlanStepKind::CoverGlueCheck { target, opens } => format!(
            "step: node={}, op={}, backend={}, kind=cover_glue_check, target={}, opens={:?}, domain={}, representation={}, lowering_rule={:?}",
            step.node_id,
            step.op_name,
            step.backend,
            target,
            opens,
            step.domain,
            step.representation,
            step.lowering_rule_id
        ),
    }
}

#[derive(Debug, Clone, PartialEq)]
pub struct VerificationReport {
    pub checked_outputs: Vec<usize>,
    pub equality_mode: EqualityMode,
}

#[derive(Debug, Clone, PartialEq)]
pub struct ContractVerificationReport {
    pub execution: Option<VerificationReport>,
    pub properties: Vec<PropertyCheckReport>,
}

impl ContractVerificationReport {
    pub fn new(properties: Vec<PropertyCheckReport>) -> Self {
        Self {
            execution: None,
            properties,
        }
    }

    pub fn with_execution(
        execution: VerificationReport,
        properties: Vec<PropertyCheckReport>,
    ) -> Self {
        Self {
            execution: Some(execution),
            properties,
        }
    }

    pub fn property_failures(&self) -> Vec<&PropertyCheckReport> {
        self.properties
            .iter()
            .filter(|property| !property.passed)
            .collect()
    }

    pub fn ensure_passed(&self) -> Result<()> {
        ensure_all_properties_pass(&self.properties)
    }
}

pub fn verify_padic_contracts(domain: &PadicDomain) -> Result<ContractVerificationReport> {
    let properties = check_padic_contract_properties(domain)?;
    ensure_all_properties_pass(&properties)?;
    Ok(ContractVerificationReport::new(properties))
}

pub fn verify_sheaf_contracts(
    site: &FiniteSite,
    cover: &Cover,
    composition: (&OpenId, &OpenId, &OpenId),
) -> Result<ContractVerificationReport> {
    let properties = check_sheaf_contract_properties(site, cover, composition)?;
    ensure_all_properties_pass(&properties)?;
    Ok(ContractVerificationReport::new(properties))
}

pub fn verify_i64_plan_against_reference(
    backend: &CpuScalarBackend,
    graph: &SemanticGraph,
    plan: &ExecutionPlan,
    inputs: &TensorStore<i64>,
    output_ids: &[usize],
) -> Result<VerificationReport> {
    let mut reference_store = inputs.clone();
    backend.execute_i64(graph, plan, &mut reference_store)?;

    let mut optimized_store = inputs.clone();
    backend.execute_i64_plan(graph, plan, &mut optimized_store)?;

    for output_id in output_ids {
        let reference = reference_store.get(*output_id)?;
        let optimized = optimized_store.get(*output_id)?;
        if reference.data != optimized.data {
            return Err(Error::verification(format!(
                "output {output_id} mismatch: reference={:?}, optimized={:?}",
                reference.data, optimized.data
            )));
        }
    }

    Ok(VerificationReport {
        checked_outputs: output_ids.to_vec(),
        equality_mode: EqualityMode::Exact,
    })
}

pub fn verify_padic_values_at_precision(
    pairs: &[(usize, Padic, Padic)],
    digits: u32,
) -> Result<VerificationReport> {
    let mut checked_outputs = Vec::new();
    for (output_id, reference, candidate) in pairs {
        if !padic_equal_at_precision(reference, candidate, digits)? {
            return Err(Error::verification(format!(
                "p-adic output {output_id} mismatch at precision {digits}: reference residue={}, candidate residue={}",
                reference.residue, candidate.residue
            )));
        }
        checked_outputs.push(*output_id);
    }

    Ok(VerificationReport {
        checked_outputs,
        equality_mode: EqualityMode::PrecisionBounded { digits },
    })
}

pub fn verify_padic_tensor_at_precision(
    output_id: usize,
    reference: &Tensor<Padic>,
    candidate: &Tensor<Padic>,
    digits: u32,
) -> Result<VerificationReport> {
    reference.meta.shape.ensure_same(&candidate.meta.shape)?;
    if reference.data.len() != candidate.data.len() {
        return Err(Error::verification(format!(
            "p-adic tensor length mismatch: reference={}, candidate={}",
            reference.data.len(),
            candidate.data.len()
        )));
    }

    let mut checked_outputs = Vec::new();
    for (index, (lhs, rhs)) in reference.data.iter().zip(candidate.data.iter()).enumerate() {
        if !padic_equal_at_precision(lhs, rhs, digits)? {
            return Err(Error::verification(format!(
                "p-adic tensor output {output_id}[{index}] mismatch at precision {digits}"
            )));
        }
        checked_outputs.push(output_id * 1_000_000 + index);
    }

    Ok(VerificationReport {
        checked_outputs,
        equality_mode: EqualityMode::PrecisionBounded { digits },
    })
}

pub fn verify_cover_glue_plan<T: Clone + PartialEq>(
    plan: &ExecutionPlan,
    site: &FiniteSite,
    cover: &Cover,
    sections: &SectionTable<T>,
    glued_value: T,
) -> Result<Section<T>> {
    let has_cover_step = plan.steps.iter().any(|step| {
        matches!(
            &step.kind,
            PlanStepKind::CoverGlueCheck { target, opens }
                if target == &cover.target.0
                    && opens == &cover.opens.iter().map(|open| open.0.clone()).collect::<Vec<_>>()
        )
    });
    if !has_cover_step {
        return Err(Error::verification(
            "plan does not contain matching cover glue check step",
        ));
    }
    sections.glue(site, cover, glued_value)
}