guarded-continuation-checker 0.32.0

//! Canonical, source-bound artifacts for proof-carrying controller/plant batches.

use std::error::Error;
use std::fmt;

use sha2::{Digest, Sha256};

use crate::aiger_obligation::AigerTransition;
use crate::controller_mtbdd::{
    ControllerMtbddAdmissionFailure, ControllerMtbddArtifact, ControllerMtbddSummary,
    decode_controller_mtbdd, encode_controller_mtbdd, produce_controller_mtbdd,
};
use crate::controller_mtbdd_proof::{
    ControllerMtbddEquivalenceProof, decode_controller_mtbdd_equivalence_proof,
    encode_controller_mtbdd_equivalence_proof, produce_controller_mtbdd_equivalence_proof,
};
use crate::controller_plant::{
    ControllerPlantAnswer, ControllerPlantBatchInput, ControllerPlantBatchResult,
    ControllerPlantResult, ControllerPlantTraceStep, ControllerPlantWiring,
    MAX_COMPOSITION_HORIZON, compose_controller_plant_batch, compose_controller_plant_direct_batch,
    compose_verified_mtbdd_plant, reuse_verified_controller_mtbdd, verify_mtbdd_for_composition,
    verify_proof_carrying_mtbdd_for_composition,
};
use crate::controller_transducer::{
    ControllerTransducerObligation, decode_controller_transducer, encode_controller_transducer,
};

pub const CONTROLLER_PLANT_ARTIFACT_VERSION: u32 = 1;
pub const MAX_CONTROLLER_PLANT_ARTIFACT_BYTES: usize = 16 * 1024 * 1024;
pub const MAX_CONTROLLER_PLANT_ARTIFACT_MEMBERS: usize = 64;
const MAGIC: &[u8; 8] = b"GCCCPA01";
pub const MTBDD_PLANT_ARTIFACT_VERSION: u32 = 1;
const MTBDD_MAGIC: &[u8; 8] = b"GCCMPA01";
pub const PROOF_MTBDD_PLANT_ARTIFACT_VERSION: u32 = 1;
const PROOF_MTBDD_MAGIC: &[u8; 8] = b"GCCMPF01";
pub const CONTROLLER_PROOF_EVIDENCE_VERSION: u32 = 1;
const CONTROLLER_PROOF_EVIDENCE_MAGIC: &[u8; 8] = b"GCCCPE01";
pub const BOUND_PLANT_RESULTS_VERSION: u32 = 1;
const BOUND_PLANT_RESULTS_MAGIC: &[u8; 8] = b"GCCBPR01";
pub const DIRECT_PLANT_ARTIFACT_VERSION: u32 = 1;
const DIRECT_MAGIC: &[u8; 8] = b"GCCDPA01";
pub const MTBDD_PLANT_PORTFOLIO_VERSION: u32 = 1;
const PORTFOLIO_MAGIC: &[u8; 8] = b"GCCMPP01";
pub const PROOF_MTBDD_PLANT_PORTFOLIO_VERSION: u32 = 1;
const PROOF_PORTFOLIO_MAGIC: &[u8; 8] = b"GCCPGP01";
pub const CONTROLLER_PLANT_RESOURCE_ENVELOPE_VERSION: u32 = 1;
pub const CONTROLLER_PROOF_MTBDD_RESOURCE_ENVELOPE_VERSION: u32 = 1;
pub const CONTROLLER_PROOF_EVIDENCE_RESOURCE_ENVELOPE_VERSION: u32 = 1;

#[derive(Clone, Copy, Debug)]
pub struct ControllerPlantArtifactInput<'a> {
    pub plant: &'a AigerTransition,
    pub plant_source_sha256: [u8; 32],
    pub wiring: &'a ControllerPlantWiring,
    pub initial_controller_state: usize,
    pub initial_plant_state: usize,
    pub bad_plant_output: usize,
    pub horizon: usize,
}

#[derive(Clone, Debug, Eq, PartialEq)]
pub struct ControllerPlantArtifactMember {
    pub plant_source_sha256: [u8; 32],
    pub wiring: ControllerPlantWiring,
    pub initial_controller_state: usize,
    pub initial_plant_state: usize,
    pub bad_plant_output: usize,
    pub horizon: usize,
    pub result: ControllerPlantResult,
}

#[derive(Clone, Debug, Eq, PartialEq)]
pub struct ControllerPlantBatchArtifact {
    pub version: u32,
    pub controller_transducer: Vec<u8>,
    pub members: Vec<ControllerPlantArtifactMember>,
}

#[derive(Clone, Debug, Eq, PartialEq)]
pub struct ControllerMtbddPlantBatchArtifact {
    pub version: u32,
    pub controller_mtbdd: Vec<u8>,
    pub members: Vec<ControllerPlantArtifactMember>,
}

#[derive(Clone, Debug, Eq, PartialEq)]
pub struct ControllerProofMtbddPlantBatchArtifact {
    pub version: u32,
    pub controller_mtbdd_plant: Vec<u8>,
    pub equivalence_proof: Vec<u8>,
}

/// Controller-local evidence that can be cached independently of plant results.
#[derive(Clone, Debug, Eq, PartialEq)]
pub struct ControllerProofEvidenceArtifact {
    pub version: u32,
    pub controller_mtbdd: Vec<u8>,
    pub equivalence_proof: Vec<u8>,
}

/// Plant-local results bound to the digest of one canonical controller artifact.
#[derive(Clone, Debug, Eq, PartialEq)]
pub struct BoundPlantResultsArtifact {
    pub version: u32,
    pub controller_evidence_sha256: [u8; 32],
    pub members: Vec<ControllerPlantArtifactMember>,
}

/// A process-local capability proving that controller evidence was admitted.
///
/// Its fields are private so callers cannot construct a trusted session without
/// passing canonical evidence through the independent proof checker.
#[derive(Debug)]
pub struct AdmittedControllerProofEvidence {
    evidence_sha256: [u8; 32],
    controller: ControllerMtbddArtifact,
    summary: ControllerMtbddSummary,
}

/// Caller-selected limits checked before controller proof admission.
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub struct ControllerProofEvidenceResourceEnvelope {
    max_artifact_bytes: usize,
    max_unsat_proof_bytes: usize,
}

impl ControllerProofEvidenceResourceEnvelope {
    pub fn new(
        max_artifact_bytes: usize,
        max_unsat_proof_bytes: usize,
    ) -> Result<Self, ControllerPlantArtifactError> {
        if max_artifact_bytes == 0
            || max_artifact_bytes > MAX_CONTROLLER_PLANT_ARTIFACT_BYTES
            || max_unsat_proof_bytes == 0
            || max_unsat_proof_bytes > crate::unsat_proof::MAX_UNSAT_PROOF_BYTES
        {
            return Err(reject(
                "controller proof evidence resource envelope is outside static limits",
            ));
        }
        Ok(Self {
            max_artifact_bytes,
            max_unsat_proof_bytes,
        })
    }

    pub fn max_artifact_bytes(self) -> usize {
        self.max_artifact_bytes
    }

    pub fn max_unsat_proof_bytes(self) -> usize {
        self.max_unsat_proof_bytes
    }
}

#[derive(Clone, Debug, Eq, PartialEq)]
pub struct ControllerProofEvidenceResourceAssessment {
    pub version: u32,
    pub artifact_bytes: usize,
    pub mtbdd_bytes: usize,
    pub equivalence_artifact_bytes: usize,
    pub unsat_proof_bytes: usize,
}

#[derive(Debug)]
pub struct GovernedAdmittedControllerProofEvidence {
    pub resources: ControllerProofEvidenceResourceAssessment,
    pub admitted: AdmittedControllerProofEvidence,
}

#[derive(Clone, Debug, Eq, PartialEq)]
pub struct GovernedBoundPlantResultsSummary {
    pub resources: ControllerPlantResourceAssessment,
    pub verification: ControllerMtbddPlantBatchSummary,
}

impl AdmittedControllerProofEvidence {
    pub fn evidence_sha256(&self) -> [u8; 32] {
        self.evidence_sha256
    }

    pub fn summary(&self) -> &ControllerMtbddSummary {
        &self.summary
    }

    pub fn relevant_inputs(&self) -> &[usize] {
        &self.controller.relevant_inputs
    }

    pub fn observed_outputs(&self) -> &[usize] {
        &self.controller.observed_outputs
    }
}

#[derive(Clone, Debug, Eq, PartialEq)]
pub struct ControllerDirectPlantBatchArtifact {
    pub version: u32,
    pub controller_source_sha256: [u8; 32],
    pub members: Vec<ControllerPlantArtifactMember>,
}

#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub enum ControllerMtbddPlantPortfolioBackend {
    Mtbdd,
    DirectExact,
}

#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub enum ControllerMtbddPlantSelectionReason {
    MtbddAdmitted,
    BoundaryLimit,
    TerminalLimit,
    NodeLimit,
}

#[derive(Clone, Debug, Eq, PartialEq)]
pub struct ControllerMtbddPlantPortfolioArtifact {
    pub version: u32,
    pub backend: ControllerMtbddPlantPortfolioBackend,
    pub reason: ControllerMtbddPlantSelectionReason,
    pub relevant_inputs: Vec<usize>,
    pub observed_outputs: Vec<usize>,
    pub payload: Vec<u8>,
}

#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub enum ControllerProofMtbddPlantPortfolioBackend {
    ProofMtbdd,
    DirectExact,
}

#[derive(Clone, Debug, Eq, PartialEq)]
pub struct ControllerProofMtbddPlantPortfolioArtifact {
    pub version: u32,
    pub backend: ControllerProofMtbddPlantPortfolioBackend,
    pub reason: ControllerMtbddPlantSelectionReason,
    pub relevant_inputs: Vec<usize>,
    pub observed_outputs: Vec<usize>,
    pub payload: Vec<u8>,
}

#[derive(Clone, Debug, Eq, PartialEq)]
pub struct ControllerProofMtbddPlantPortfolioSummary {
    pub backend: ControllerProofMtbddPlantPortfolioBackend,
    pub reason: ControllerMtbddPlantSelectionReason,
    pub members: Vec<ControllerPlantResult>,
    pub safe: usize,
    pub unsafe_count: usize,
    pub reachable_product_states: usize,
    pub explored_transitions: usize,
    pub assignments_checked: usize,
}

#[derive(Clone, Debug, Eq, PartialEq)]
pub struct ControllerMtbddPlantPortfolioSummary {
    pub backend: ControllerMtbddPlantPortfolioBackend,
    pub reason: ControllerMtbddPlantSelectionReason,
    pub members: Vec<ControllerPlantResult>,
    pub safe: usize,
    pub unsafe_count: usize,
    pub reachable_product_states: usize,
    pub explored_transitions: usize,
}

/// Caller-selected hard bounds checked before controller/plant semantic replay.
///
/// The transition bound is a conservative upper bound over the complete product
/// state space, every requested frame, every external plant input, and, for the
/// direct backend, every omitted controller input evaluation. It is deliberately
/// independent of measured runtime and formula-specific calibration.
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub struct ControllerPlantResourceEnvelope {
    max_artifact_bytes: usize,
    max_members: usize,
    max_member_horizon: usize,
    max_product_states_per_member: usize,
    max_transition_evaluations: usize,
}

impl ControllerPlantResourceEnvelope {
    pub fn new(
        max_artifact_bytes: usize,
        max_members: usize,
        max_member_horizon: usize,
        max_product_states_per_member: usize,
        max_transition_evaluations: usize,
    ) -> Result<Self, ControllerPlantArtifactError> {
        if max_artifact_bytes == 0
            || max_artifact_bytes > MAX_CONTROLLER_PLANT_ARTIFACT_BYTES
            || max_members == 0
            || max_members > MAX_CONTROLLER_PLANT_ARTIFACT_MEMBERS
            || max_member_horizon > MAX_COMPOSITION_HORIZON
            || max_product_states_per_member == 0
            || max_product_states_per_member > crate::controller_plant::MAX_PRODUCT_STATES
            || max_transition_evaluations == 0
        {
            return Err(reject(
                "controller-plant resource envelope is outside static limits",
            ));
        }
        Ok(Self {
            max_artifact_bytes,
            max_members,
            max_member_horizon,
            max_product_states_per_member,
            max_transition_evaluations,
        })
    }

    pub fn max_artifact_bytes(self) -> usize {
        self.max_artifact_bytes
    }

    pub fn max_members(self) -> usize {
        self.max_members
    }

    pub fn max_member_horizon(self) -> usize {
        self.max_member_horizon
    }

    pub fn max_product_states_per_member(self) -> usize {
        self.max_product_states_per_member
    }

    pub fn max_transition_evaluations(self) -> usize {
        self.max_transition_evaluations
    }
}

impl Default for ControllerPlantResourceEnvelope {
    fn default() -> Self {
        Self {
            max_artifact_bytes: MAX_CONTROLLER_PLANT_ARTIFACT_BYTES,
            max_members: MAX_CONTROLLER_PLANT_ARTIFACT_MEMBERS,
            max_member_horizon: MAX_COMPOSITION_HORIZON,
            max_product_states_per_member: crate::controller_plant::MAX_PRODUCT_STATES,
            max_transition_evaluations: usize::MAX,
        }
    }
}

#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub struct ControllerPlantResourceAssessment {
    pub version: u32,
    pub backend: ControllerMtbddPlantPortfolioBackend,
    pub artifact_bytes: usize,
    pub members: usize,
    pub maximum_member_horizon: usize,
    pub maximum_product_states: usize,
    pub transition_evaluation_bound: usize,
}

#[derive(Clone, Debug, Eq, PartialEq)]
pub struct GovernedControllerMtbddPlantPortfolioSummary {
    pub resources: ControllerPlantResourceAssessment,
    pub verification: ControllerMtbddPlantPortfolioSummary,
}

/// Caller-selected limits for proof-carrying MTBDD verification.
///
/// The ordinary controller/plant envelope governs the batch and composition
/// workload. The additional bounds govern the equivalence artifact and its
/// embedded UNSAT proof before proof checking begins.
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub struct ControllerProofMtbddResourceEnvelope {
    composition: ControllerPlantResourceEnvelope,
    max_equivalence_artifact_bytes: usize,
    max_unsat_proof_bytes: usize,
}

impl ControllerProofMtbddResourceEnvelope {
    pub fn new(
        composition: ControllerPlantResourceEnvelope,
        max_equivalence_artifact_bytes: usize,
        max_unsat_proof_bytes: usize,
    ) -> Result<Self, ControllerPlantArtifactError> {
        if max_equivalence_artifact_bytes == 0
            || max_equivalence_artifact_bytes
                > crate::controller_mtbdd_proof::MAX_EQUIVALENCE_ARTIFACT_BYTES
            || max_unsat_proof_bytes == 0
            || max_unsat_proof_bytes > crate::unsat_proof::MAX_UNSAT_PROOF_BYTES
        {
            return Err(reject(
                "proof-carrying controller MTBDD resource envelope is outside static limits",
            ));
        }
        Ok(Self {
            composition,
            max_equivalence_artifact_bytes,
            max_unsat_proof_bytes,
        })
    }

    pub fn composition(self) -> ControllerPlantResourceEnvelope {
        self.composition
    }

    pub fn max_equivalence_artifact_bytes(self) -> usize {
        self.max_equivalence_artifact_bytes
    }

    pub fn max_unsat_proof_bytes(self) -> usize {
        self.max_unsat_proof_bytes
    }
}

#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub struct ControllerProofMtbddResourceAssessment {
    pub version: u32,
    pub artifact_bytes: usize,
    pub equivalence_artifact_bytes: usize,
    pub unsat_proof_bytes: usize,
    pub members: usize,
    pub maximum_member_horizon: usize,
    pub maximum_product_states: usize,
    pub transition_evaluation_bound: usize,
}

#[derive(Clone, Debug, Eq, PartialEq)]
pub struct GovernedControllerProofMtbddPlantSummary {
    pub resources: ControllerProofMtbddResourceAssessment,
    pub verification: ControllerMtbddPlantBatchSummary,
}

#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub struct ControllerProofMtbddPortfolioResourceAssessment {
    pub version: u32,
    pub backend: ControllerProofMtbddPlantPortfolioBackend,
    pub artifact_bytes: usize,
    pub equivalence_artifact_bytes: usize,
    pub unsat_proof_bytes: usize,
    pub members: usize,
    pub maximum_member_horizon: usize,
    pub maximum_product_states: usize,
    pub transition_evaluation_bound: usize,
}

#[derive(Clone, Debug, Eq, PartialEq)]
pub struct GovernedControllerProofMtbddPortfolioSummary {
    pub resources: ControllerProofMtbddPortfolioResourceAssessment,
    pub verification: ControllerProofMtbddPlantPortfolioSummary,
}

#[derive(Clone, Debug, Eq, PartialEq)]
pub struct ControllerMtbddPlantBatchSummary {
    pub members: Vec<ControllerPlantResult>,
    pub safe: usize,
    pub unsafe_count: usize,
    pub mtbdd_nodes: usize,
    pub mtbdd_terminals: usize,
    pub assignments_checked: usize,
    pub reachable_product_states: usize,
    pub explored_transitions: usize,
}

#[derive(Clone, Debug, Eq, PartialEq)]
pub struct ControllerPlantArtifactError(pub String);

impl fmt::Display for ControllerPlantArtifactError {
    fn fmt(&self, formatter: &mut fmt::Formatter<'_>) -> fmt::Result {
        formatter.write_str(&self.0)
    }
}

impl Error for ControllerPlantArtifactError {}

fn reject(message: impl Into<String>) -> ControllerPlantArtifactError {
    ControllerPlantArtifactError(message.into())
}

fn narrow(value: usize, field: &str) -> Result<u32, ControllerPlantArtifactError> {
    u32::try_from(value).map_err(|_| reject(format!("{field} exceeds canonical range")))
}

fn put_vec(bytes: &mut Vec<u8>, values: &[usize]) -> Result<(), ControllerPlantArtifactError> {
    let count = u8::try_from(values.len()).map_err(|_| reject("wiring vector is too long"))?;
    bytes.push(count);
    for &value in values {
        bytes.push(u8::try_from(value).map_err(|_| reject("wiring index exceeds range"))?);
    }
    Ok(())
}

fn put_result(
    bytes: &mut Vec<u8>,
    result: &ControllerPlantResult,
) -> Result<(), ControllerPlantArtifactError> {
    bytes.push(match result.answer {
        ControllerPlantAnswer::Safe => 0,
        ControllerPlantAnswer::Unsafe => 1,
    });
    bytes.extend_from_slice(&narrow(result.horizon, "result horizon")?.to_le_bytes());
    bytes.extend_from_slice(
        &result
            .bad_frame
            .map(|value| narrow(value, "bad frame"))
            .transpose()?
            .unwrap_or(u32::MAX)
            .to_le_bytes(),
    );
    bytes.extend_from_slice(
        &narrow(result.reachable_product_states, "reachable states")?.to_le_bytes(),
    );
    bytes.extend_from_slice(
        &narrow(result.explored_transitions, "explored transitions")?.to_le_bytes(),
    );
    bytes.extend_from_slice(&narrow(result.trace.len(), "trace length")?.to_le_bytes());
    for step in &result.trace {
        for (value, field) in [
            (step.frame, "trace frame"),
            (step.controller_state, "controller state"),
            (step.plant_state, "plant state"),
            (step.sensor_pattern, "sensor pattern"),
            (step.action_pattern, "action pattern"),
        ] {
            bytes.extend_from_slice(&narrow(value, field)?.to_le_bytes());
        }
        bytes.extend_from_slice(&step.controller_input.to_le_bytes());
        bytes.extend_from_slice(&step.plant_input.to_le_bytes());
        bytes.push(u8::from(step.bad));
    }
    Ok(())
}

pub fn produce_controller_plant_artifact(
    controller_model: &AigerTransition,
    controller_source_sha256: [u8; 32],
    controller: &ControllerTransducerObligation,
    members: &[ControllerPlantArtifactInput<'_>],
) -> Result<ControllerPlantBatchArtifact, ControllerPlantArtifactError> {
    let batch_inputs = members
        .iter()
        .map(|member| ControllerPlantBatchInput {
            plant: member.plant,
            wiring: member.wiring,
            initial_controller_state: member.initial_controller_state,
            initial_plant_state: member.initial_plant_state,
            bad_plant_output: member.bad_plant_output,
            horizon: member.horizon,
        })
        .collect::<Vec<_>>();
    let batch = compose_controller_plant_batch(
        controller_model,
        controller_source_sha256,
        controller,
        &batch_inputs,
    )
    .map_err(|error| reject(error.to_string()))?;
    let artifact_members = members
        .iter()
        .zip(batch.members)
        .map(|(member, result)| ControllerPlantArtifactMember {
            plant_source_sha256: member.plant_source_sha256,
            wiring: member.wiring.clone(),
            initial_controller_state: member.initial_controller_state,
            initial_plant_state: member.initial_plant_state,
            bad_plant_output: member.bad_plant_output,
            horizon: member.horizon,
            result,
        })
        .collect();
    Ok(ControllerPlantBatchArtifact {
        version: CONTROLLER_PLANT_ARTIFACT_VERSION,
        controller_transducer: encode_controller_transducer(controller)
            .map_err(|error| reject(error.to_string()))?,
        members: artifact_members,
    })
}

pub fn encode_controller_plant_artifact(
    artifact: &ControllerPlantBatchArtifact,
) -> Result<Vec<u8>, ControllerPlantArtifactError> {
    if artifact.version != CONTROLLER_PLANT_ARTIFACT_VERSION
        || artifact.members.is_empty()
        || artifact.members.len() > MAX_CONTROLLER_PLANT_ARTIFACT_MEMBERS
    {
        return Err(reject("controller-plant artifact dimensions are invalid"));
    }
    decode_controller_transducer(&artifact.controller_transducer)
        .map_err(|error| reject(error.to_string()))?;
    let mut bytes = Vec::new();
    bytes.extend_from_slice(MAGIC);
    bytes.extend_from_slice(&artifact.version.to_le_bytes());
    bytes.extend_from_slice(
        &narrow(
            artifact.controller_transducer.len(),
            "controller artifact length",
        )?
        .to_le_bytes(),
    );
    bytes.extend_from_slice(&artifact.controller_transducer);
    bytes.push(artifact.members.len() as u8);
    for member in &artifact.members {
        bytes.extend_from_slice(&member.plant_source_sha256);
        put_vec(&mut bytes, &member.wiring.controller_sensor_inputs)?;
        put_vec(&mut bytes, &member.wiring.controller_action_outputs)?;
        put_vec(&mut bytes, &member.wiring.plant_sensor_outputs)?;
        put_vec(&mut bytes, &member.wiring.plant_action_inputs)?;
        for (value, field) in [
            (member.initial_controller_state, "initial controller state"),
            (member.initial_plant_state, "initial plant state"),
            (member.bad_plant_output, "bad plant output"),
            (member.horizon, "member horizon"),
        ] {
            bytes.extend_from_slice(&narrow(value, field)?.to_le_bytes());
        }
        put_result(&mut bytes, &member.result)?;
    }
    let integrity = Sha256::digest(&bytes);
    bytes.extend_from_slice(&integrity);
    if bytes.len() > MAX_CONTROLLER_PLANT_ARTIFACT_BYTES {
        return Err(reject("controller-plant artifact exceeds byte limit"));
    }
    Ok(bytes)
}

fn take<'a>(
    bytes: &'a [u8],
    cursor: &mut usize,
    count: usize,
) -> Result<&'a [u8], ControllerPlantArtifactError> {
    let end = cursor
        .checked_add(count)
        .ok_or_else(|| reject("controller-plant artifact cursor overflow"))?;
    let value = bytes
        .get(*cursor..end)
        .ok_or_else(|| reject("controller-plant artifact is truncated"))?;
    *cursor = end;
    Ok(value)
}

fn read_u8(bytes: &[u8], cursor: &mut usize) -> Result<u8, ControllerPlantArtifactError> {
    Ok(take(bytes, cursor, 1)?[0])
}

fn read_u32(bytes: &[u8], cursor: &mut usize) -> Result<u32, ControllerPlantArtifactError> {
    Ok(u32::from_le_bytes(
        take(bytes, cursor, 4)?
            .try_into()
            .map_err(|_| reject("controller-plant u32 decode failed"))?,
    ))
}

fn read_u64(bytes: &[u8], cursor: &mut usize) -> Result<u64, ControllerPlantArtifactError> {
    Ok(u64::from_le_bytes(
        take(bytes, cursor, 8)?
            .try_into()
            .map_err(|_| reject("controller-plant u64 decode failed"))?,
    ))
}

fn read_vec(bytes: &[u8], cursor: &mut usize) -> Result<Vec<usize>, ControllerPlantArtifactError> {
    let count = read_u8(bytes, cursor)? as usize;
    Ok(take(bytes, cursor, count)?
        .iter()
        .map(|&value| value as usize)
        .collect())
}

fn read_result(
    bytes: &[u8],
    cursor: &mut usize,
) -> Result<ControllerPlantResult, ControllerPlantArtifactError> {
    let answer = match read_u8(bytes, cursor)? {
        0 => ControllerPlantAnswer::Safe,
        1 => ControllerPlantAnswer::Unsafe,
        _ => return Err(reject("controller-plant answer is invalid")),
    };
    let horizon = read_u32(bytes, cursor)? as usize;
    let bad_raw = read_u32(bytes, cursor)?;
    let bad_frame = (bad_raw != u32::MAX).then_some(bad_raw as usize);
    let reachable_product_states = read_u32(bytes, cursor)? as usize;
    let explored_transitions = read_u32(bytes, cursor)? as usize;
    let trace_count = read_u32(bytes, cursor)? as usize;
    if horizon > MAX_COMPOSITION_HORIZON || trace_count > horizon.saturating_add(1) {
        return Err(reject("controller-plant result dimensions exceed limits"));
    }
    let mut trace = Vec::with_capacity(trace_count);
    for _ in 0..trace_count {
        let frame = read_u32(bytes, cursor)? as usize;
        let controller_state = read_u32(bytes, cursor)? as usize;
        let plant_state = read_u32(bytes, cursor)? as usize;
        let sensor_pattern = read_u32(bytes, cursor)? as usize;
        let action_pattern = read_u32(bytes, cursor)? as usize;
        let controller_input = read_u64(bytes, cursor)?;
        let plant_input = read_u64(bytes, cursor)?;
        let bad = match read_u8(bytes, cursor)? {
            0 => false,
            1 => true,
            _ => return Err(reject("controller-plant trace flag is invalid")),
        };
        trace.push(ControllerPlantTraceStep {
            frame,
            controller_state,
            plant_state,
            sensor_pattern,
            action_pattern,
            controller_input,
            plant_input,
            bad,
        });
    }
    Ok(ControllerPlantResult {
        version: crate::controller_plant::CONTROLLER_PLANT_VERSION,
        answer,
        horizon,
        bad_frame,
        reachable_product_states,
        explored_transitions,
        trace,
    })
}

pub fn decode_controller_plant_artifact(
    bytes: &[u8],
) -> Result<ControllerPlantBatchArtifact, ControllerPlantArtifactError> {
    if bytes.len() > MAX_CONTROLLER_PLANT_ARTIFACT_BYTES || bytes.len() < 32 {
        return Err(reject("controller-plant artifact size is invalid"));
    }
    let payload_len = bytes.len() - 32;
    let (payload, claimed_integrity) = bytes.split_at(payload_len);
    if Sha256::digest(payload).as_slice() != claimed_integrity {
        return Err(reject("controller-plant artifact integrity mismatch"));
    }
    let mut cursor = 0usize;
    if take(payload, &mut cursor, MAGIC.len())? != MAGIC {
        return Err(reject("controller-plant artifact magic mismatch"));
    }
    let version = read_u32(payload, &mut cursor)?;
    if version != CONTROLLER_PLANT_ARTIFACT_VERSION {
        return Err(reject("controller-plant artifact version mismatch"));
    }
    let controller_len = read_u32(payload, &mut cursor)? as usize;
    let controller_transducer = take(payload, &mut cursor, controller_len)?.to_vec();
    decode_controller_transducer(&controller_transducer)
        .map_err(|error| reject(error.to_string()))?;
    let member_count = read_u8(payload, &mut cursor)? as usize;
    if member_count == 0 || member_count > MAX_CONTROLLER_PLANT_ARTIFACT_MEMBERS {
        return Err(reject("controller-plant member count is outside limit"));
    }
    let mut members = Vec::with_capacity(member_count);
    for _ in 0..member_count {
        let plant_source_sha256 = take(payload, &mut cursor, 32)?
            .try_into()
            .map_err(|_| reject("plant digest decode failed"))?;
        let wiring = ControllerPlantWiring {
            controller_sensor_inputs: read_vec(payload, &mut cursor)?,
            controller_action_outputs: read_vec(payload, &mut cursor)?,
            plant_sensor_outputs: read_vec(payload, &mut cursor)?,
            plant_action_inputs: read_vec(payload, &mut cursor)?,
        };
        let initial_controller_state = read_u32(payload, &mut cursor)? as usize;
        let initial_plant_state = read_u32(payload, &mut cursor)? as usize;
        let bad_plant_output = read_u32(payload, &mut cursor)? as usize;
        let horizon = read_u32(payload, &mut cursor)? as usize;
        let result = read_result(payload, &mut cursor)?;
        members.push(ControllerPlantArtifactMember {
            plant_source_sha256,
            wiring,
            initial_controller_state,
            initial_plant_state,
            bad_plant_output,
            horizon,
            result,
        });
    }
    if cursor != payload.len() {
        return Err(reject("controller-plant artifact has trailing bytes"));
    }
    Ok(ControllerPlantBatchArtifact {
        version,
        controller_transducer,
        members,
    })
}

pub fn verify_controller_plant_artifact(
    controller_model: &AigerTransition,
    controller_source_sha256: [u8; 32],
    plants: &[(&AigerTransition, [u8; 32])],
    artifact_bytes: &[u8],
) -> Result<ControllerPlantBatchResult, ControllerPlantArtifactError> {
    let artifact = decode_controller_plant_artifact(artifact_bytes)?;
    if plants.len() != artifact.members.len() {
        return Err(reject("controller-plant source count mismatch"));
    }
    let controller = decode_controller_transducer(&artifact.controller_transducer)
        .map_err(|error| reject(error.to_string()))?;
    let inputs = plants
        .iter()
        .zip(&artifact.members)
        .map(|(&(plant, digest), member)| {
            if digest != member.plant_source_sha256 {
                return Err(reject("controller-plant source digest mismatch"));
            }
            Ok(ControllerPlantBatchInput {
                plant,
                wiring: &member.wiring,
                initial_controller_state: member.initial_controller_state,
                initial_plant_state: member.initial_plant_state,
                bad_plant_output: member.bad_plant_output,
                horizon: member.horizon,
            })
        })
        .collect::<Result<Vec<_>, _>>()?;
    let verified = compose_controller_plant_batch(
        controller_model,
        controller_source_sha256,
        &controller,
        &inputs,
    )
    .map_err(|error| reject(error.to_string()))?;
    if verified
        .members
        .iter()
        .zip(&artifact.members)
        .any(|(actual, claimed)| actual != &claimed.result)
    {
        return Err(reject("controller-plant member result mismatch"));
    }
    Ok(verified)
}

pub fn produce_controller_mtbdd_plant_artifact(
    controller_model: &AigerTransition,
    controller_source_sha256: [u8; 32],
    controller: &ControllerMtbddArtifact,
    members: &[ControllerPlantArtifactInput<'_>],
) -> Result<ControllerMtbddPlantBatchArtifact, ControllerPlantArtifactError> {
    if members.is_empty() || members.len() > MAX_CONTROLLER_PLANT_ARTIFACT_MEMBERS {
        return Err(reject(
            "controller MTBDD plant member count is outside limit",
        ));
    }
    let verified =
        verify_mtbdd_for_composition(controller_model, controller_source_sha256, controller)
            .map_err(|error| reject(error.to_string()))?;
    let artifact_members = members
        .iter()
        .map(|member| {
            let result = compose_verified_mtbdd_plant(
                &verified,
                member.plant,
                member.wiring,
                member.initial_controller_state,
                member.initial_plant_state,
                member.bad_plant_output,
                member.horizon,
            )
            .map_err(|error| reject(error.to_string()))?;
            Ok(ControllerPlantArtifactMember {
                plant_source_sha256: member.plant_source_sha256,
                wiring: member.wiring.clone(),
                initial_controller_state: member.initial_controller_state,
                initial_plant_state: member.initial_plant_state,
                bad_plant_output: member.bad_plant_output,
                horizon: member.horizon,
                result,
            })
        })
        .collect::<Result<Vec<_>, ControllerPlantArtifactError>>()?;
    Ok(ControllerMtbddPlantBatchArtifact {
        version: MTBDD_PLANT_ARTIFACT_VERSION,
        controller_mtbdd: encode_controller_mtbdd(controller)
            .map_err(|error| reject(error.to_string()))?,
        members: artifact_members,
    })
}

pub fn encode_controller_mtbdd_plant_artifact(
    artifact: &ControllerMtbddPlantBatchArtifact,
) -> Result<Vec<u8>, ControllerPlantArtifactError> {
    if artifact.version != MTBDD_PLANT_ARTIFACT_VERSION
        || artifact.members.is_empty()
        || artifact.members.len() > MAX_CONTROLLER_PLANT_ARTIFACT_MEMBERS
    {
        return Err(reject(
            "controller MTBDD plant artifact dimensions are invalid",
        ));
    }
    decode_controller_mtbdd(&artifact.controller_mtbdd)
        .map_err(|error| reject(error.to_string()))?;
    let mut bytes = Vec::new();
    bytes.extend_from_slice(MTBDD_MAGIC);
    bytes.extend_from_slice(&artifact.version.to_le_bytes());
    bytes.extend_from_slice(
        &narrow(artifact.controller_mtbdd.len(), "controller MTBDD length")?.to_le_bytes(),
    );
    bytes.extend_from_slice(&artifact.controller_mtbdd);
    bytes.push(artifact.members.len() as u8);
    for member in &artifact.members {
        bytes.extend_from_slice(&member.plant_source_sha256);
        put_vec(&mut bytes, &member.wiring.controller_sensor_inputs)?;
        put_vec(&mut bytes, &member.wiring.controller_action_outputs)?;
        put_vec(&mut bytes, &member.wiring.plant_sensor_outputs)?;
        put_vec(&mut bytes, &member.wiring.plant_action_inputs)?;
        for (value, field) in [
            (member.initial_controller_state, "initial controller state"),
            (member.initial_plant_state, "initial plant state"),
            (member.bad_plant_output, "bad plant output"),
            (member.horizon, "member horizon"),
        ] {
            bytes.extend_from_slice(&narrow(value, field)?.to_le_bytes());
        }
        put_result(&mut bytes, &member.result)?;
    }
    let integrity = Sha256::digest(&bytes);
    bytes.extend_from_slice(&integrity);
    if bytes.len() > MAX_CONTROLLER_PLANT_ARTIFACT_BYTES {
        return Err(reject("controller MTBDD plant artifact exceeds byte limit"));
    }
    Ok(bytes)
}

pub fn decode_controller_mtbdd_plant_artifact(
    bytes: &[u8],
) -> Result<ControllerMtbddPlantBatchArtifact, ControllerPlantArtifactError> {
    if bytes.len() > MAX_CONTROLLER_PLANT_ARTIFACT_BYTES || bytes.len() < 32 {
        return Err(reject("controller MTBDD plant artifact size is invalid"));
    }
    let payload_len = bytes.len() - 32;
    let (payload, claimed_integrity) = bytes.split_at(payload_len);
    if Sha256::digest(payload).as_slice() != claimed_integrity {
        return Err(reject("controller MTBDD plant artifact integrity mismatch"));
    }
    let mut cursor = 0usize;
    if take(payload, &mut cursor, MTBDD_MAGIC.len())? != MTBDD_MAGIC {
        return Err(reject("controller MTBDD plant artifact magic mismatch"));
    }
    let version = read_u32(payload, &mut cursor)?;
    if version != MTBDD_PLANT_ARTIFACT_VERSION {
        return Err(reject("controller MTBDD plant artifact version mismatch"));
    }
    let controller_len = read_u32(payload, &mut cursor)? as usize;
    let controller_mtbdd = take(payload, &mut cursor, controller_len)?.to_vec();
    decode_controller_mtbdd(&controller_mtbdd).map_err(|error| reject(error.to_string()))?;
    let member_count = read_u8(payload, &mut cursor)? as usize;
    if member_count == 0 || member_count > MAX_CONTROLLER_PLANT_ARTIFACT_MEMBERS {
        return Err(reject(
            "controller MTBDD plant member count is outside limit",
        ));
    }
    let mut members = Vec::with_capacity(member_count);
    for _ in 0..member_count {
        let plant_source_sha256 = take(payload, &mut cursor, 32)?
            .try_into()
            .map_err(|_| reject("plant digest decode failed"))?;
        let wiring = ControllerPlantWiring {
            controller_sensor_inputs: read_vec(payload, &mut cursor)?,
            controller_action_outputs: read_vec(payload, &mut cursor)?,
            plant_sensor_outputs: read_vec(payload, &mut cursor)?,
            plant_action_inputs: read_vec(payload, &mut cursor)?,
        };
        let initial_controller_state = read_u32(payload, &mut cursor)? as usize;
        let initial_plant_state = read_u32(payload, &mut cursor)? as usize;
        let bad_plant_output = read_u32(payload, &mut cursor)? as usize;
        let horizon = read_u32(payload, &mut cursor)? as usize;
        let result = read_result(payload, &mut cursor)?;
        members.push(ControllerPlantArtifactMember {
            plant_source_sha256,
            wiring,
            initial_controller_state,
            initial_plant_state,
            bad_plant_output,
            horizon,
            result,
        });
    }
    if cursor != payload.len() {
        return Err(reject("controller MTBDD plant artifact has trailing bytes"));
    }
    Ok(ControllerMtbddPlantBatchArtifact {
        version,
        controller_mtbdd,
        members,
    })
}

pub fn verify_controller_mtbdd_plant_artifact(
    controller_model: &AigerTransition,
    controller_source_sha256: [u8; 32],
    plants: &[(&AigerTransition, [u8; 32])],
    artifact_bytes: &[u8],
) -> Result<ControllerMtbddPlantBatchSummary, ControllerPlantArtifactError> {
    let artifact = decode_controller_mtbdd_plant_artifact(artifact_bytes)?;
    if plants.len() != artifact.members.len() {
        return Err(reject("controller MTBDD plant source count mismatch"));
    }
    let controller = decode_controller_mtbdd(&artifact.controller_mtbdd)
        .map_err(|error| reject(error.to_string()))?;
    let verified =
        verify_mtbdd_for_composition(controller_model, controller_source_sha256, &controller)
            .map_err(|error| reject(error.to_string()))?;
    let mut members = Vec::with_capacity(plants.len());
    let mut safe = 0usize;
    let mut unsafe_count = 0usize;
    let mut reachable_product_states = 0usize;
    let mut explored_transitions = 0usize;
    for ((plant, digest), claimed) in plants.iter().copied().zip(&artifact.members) {
        if digest != claimed.plant_source_sha256 {
            return Err(reject("controller MTBDD plant source digest mismatch"));
        }
        let result = compose_verified_mtbdd_plant(
            &verified,
            plant,
            &claimed.wiring,
            claimed.initial_controller_state,
            claimed.initial_plant_state,
            claimed.bad_plant_output,
            claimed.horizon,
        )
        .map_err(|error| reject(error.to_string()))?;
        if result != claimed.result {
            return Err(reject("controller MTBDD plant member result mismatch"));
        }
        match result.answer {
            ControllerPlantAnswer::Safe => safe += 1,
            ControllerPlantAnswer::Unsafe => unsafe_count += 1,
        }
        reachable_product_states = reachable_product_states
            .checked_add(result.reachable_product_states)
            .ok_or_else(|| reject("controller MTBDD plant reachable count overflow"))?;
        explored_transitions = explored_transitions
            .checked_add(result.explored_transitions)
            .ok_or_else(|| reject("controller MTBDD plant transition count overflow"))?;
        members.push(result);
    }
    Ok(ControllerMtbddPlantBatchSummary {
        members,
        safe,
        unsafe_count,
        mtbdd_nodes: verified.summary().nodes,
        mtbdd_terminals: verified.summary().terminals,
        assignments_checked: verified.summary().assignments_checked,
        reachable_product_states,
        explored_transitions,
    })
}

pub fn produce_controller_proof_mtbdd_plant_artifact(
    controller_model: &AigerTransition,
    controller_source_sha256: [u8; 32],
    controller: &ControllerMtbddArtifact,
    members: &[ControllerPlantArtifactInput<'_>],
) -> Result<ControllerProofMtbddPlantBatchArtifact, ControllerPlantArtifactError> {
    if members.is_empty() || members.len() > MAX_CONTROLLER_PLANT_ARTIFACT_MEMBERS {
        return Err(reject(
            "proof-carrying controller MTBDD plant member count is outside limit",
        ));
    }
    let proof = produce_controller_mtbdd_equivalence_proof(
        controller_model,
        controller_source_sha256,
        controller,
    )
    .map_err(|error| reject(error.to_string()))?;
    let verified = verify_proof_carrying_mtbdd_for_composition(
        controller_model,
        controller_source_sha256,
        controller,
        &proof,
    )
    .map_err(|error| reject(error.to_string()))?;
    let artifact_members = members
        .iter()
        .map(|member| {
            let result = compose_verified_mtbdd_plant(
                &verified,
                member.plant,
                member.wiring,
                member.initial_controller_state,
                member.initial_plant_state,
                member.bad_plant_output,
                member.horizon,
            )
            .map_err(|error| reject(error.to_string()))?;
            Ok(ControllerPlantArtifactMember {
                plant_source_sha256: member.plant_source_sha256,
                wiring: member.wiring.clone(),
                initial_controller_state: member.initial_controller_state,
                initial_plant_state: member.initial_plant_state,
                bad_plant_output: member.bad_plant_output,
                horizon: member.horizon,
                result,
            })
        })
        .collect::<Result<Vec<_>, ControllerPlantArtifactError>>()?;
    let inner = ControllerMtbddPlantBatchArtifact {
        version: MTBDD_PLANT_ARTIFACT_VERSION,
        controller_mtbdd: encode_controller_mtbdd(controller)
            .map_err(|error| reject(error.to_string()))?,
        members: artifact_members,
    };
    Ok(ControllerProofMtbddPlantBatchArtifact {
        version: PROOF_MTBDD_PLANT_ARTIFACT_VERSION,
        controller_mtbdd_plant: encode_controller_mtbdd_plant_artifact(&inner)?,
        equivalence_proof: encode_controller_mtbdd_equivalence_proof(&proof)
            .map_err(|error| reject(error.to_string()))?,
    })
}

pub fn encode_controller_proof_mtbdd_plant_artifact(
    artifact: &ControllerProofMtbddPlantBatchArtifact,
) -> Result<Vec<u8>, ControllerPlantArtifactError> {
    if artifact.version != PROOF_MTBDD_PLANT_ARTIFACT_VERSION {
        return Err(reject(
            "proof-carrying controller MTBDD plant artifact version mismatch",
        ));
    }
    decode_controller_mtbdd_plant_artifact(&artifact.controller_mtbdd_plant)?;
    decode_controller_mtbdd_equivalence_proof(&artifact.equivalence_proof)
        .map_err(|error| reject(error.to_string()))?;
    let mut bytes = Vec::new();
    bytes.extend_from_slice(PROOF_MTBDD_MAGIC);
    bytes.extend_from_slice(&artifact.version.to_le_bytes());
    bytes.extend_from_slice(
        &narrow(
            artifact.controller_mtbdd_plant.len(),
            "controller MTBDD plant length",
        )?
        .to_le_bytes(),
    );
    bytes.extend_from_slice(&artifact.controller_mtbdd_plant);
    bytes.extend_from_slice(
        &narrow(
            artifact.equivalence_proof.len(),
            "controller MTBDD equivalence proof length",
        )?
        .to_le_bytes(),
    );
    bytes.extend_from_slice(&artifact.equivalence_proof);
    bytes.extend_from_slice(&Sha256::digest(&bytes));
    if bytes.len() > MAX_CONTROLLER_PLANT_ARTIFACT_BYTES {
        return Err(reject(
            "proof-carrying controller MTBDD plant artifact exceeds byte limit",
        ));
    }
    Ok(bytes)
}

pub fn decode_controller_proof_mtbdd_plant_artifact(
    bytes: &[u8],
) -> Result<ControllerProofMtbddPlantBatchArtifact, ControllerPlantArtifactError> {
    if bytes.len() < 8 + 4 + 4 + 4 + 32 || bytes.len() > MAX_CONTROLLER_PLANT_ARTIFACT_BYTES {
        return Err(reject(
            "proof-carrying controller MTBDD plant artifact size is invalid",
        ));
    }
    let payload_len = bytes.len() - 32;
    let (payload, integrity) = bytes.split_at(payload_len);
    if Sha256::digest(payload).as_slice() != integrity {
        return Err(reject(
            "proof-carrying controller MTBDD plant artifact integrity mismatch",
        ));
    }
    let mut cursor = 0usize;
    if take(payload, &mut cursor, 8)? != PROOF_MTBDD_MAGIC {
        return Err(reject(
            "proof-carrying controller MTBDD plant artifact magic mismatch",
        ));
    }
    let version = read_u32(payload, &mut cursor)?;
    if version != PROOF_MTBDD_PLANT_ARTIFACT_VERSION {
        return Err(reject(
            "proof-carrying controller MTBDD plant artifact version mismatch",
        ));
    }
    let inner_len = read_u32(payload, &mut cursor)? as usize;
    let controller_mtbdd_plant = take(payload, &mut cursor, inner_len)?.to_vec();
    decode_controller_mtbdd_plant_artifact(&controller_mtbdd_plant)?;
    let proof_len = read_u32(payload, &mut cursor)? as usize;
    let equivalence_proof = take(payload, &mut cursor, proof_len)?.to_vec();
    decode_controller_mtbdd_equivalence_proof(&equivalence_proof)
        .map_err(|error| reject(error.to_string()))?;
    if cursor != payload.len() {
        return Err(reject(
            "proof-carrying controller MTBDD plant artifact has trailing bytes",
        ));
    }
    Ok(ControllerProofMtbddPlantBatchArtifact {
        version,
        controller_mtbdd_plant,
        equivalence_proof,
    })
}

pub fn verify_controller_proof_mtbdd_plant_artifact(
    controller_model: &AigerTransition,
    controller_source_sha256: [u8; 32],
    plants: &[(&AigerTransition, [u8; 32])],
    artifact_bytes: &[u8],
) -> Result<ControllerMtbddPlantBatchSummary, ControllerPlantArtifactError> {
    let outer = decode_controller_proof_mtbdd_plant_artifact(artifact_bytes)?;
    let artifact = decode_controller_mtbdd_plant_artifact(&outer.controller_mtbdd_plant)?;
    if plants.len() != artifact.members.len() {
        return Err(reject(
            "proof-carrying controller MTBDD plant source count mismatch",
        ));
    }
    let controller = decode_controller_mtbdd(&artifact.controller_mtbdd)
        .map_err(|error| reject(error.to_string()))?;
    let proof: ControllerMtbddEquivalenceProof =
        decode_controller_mtbdd_equivalence_proof(&outer.equivalence_proof)
            .map_err(|error| reject(error.to_string()))?;
    let verified = verify_proof_carrying_mtbdd_for_composition(
        controller_model,
        controller_source_sha256,
        &controller,
        &proof,
    )
    .map_err(|error| reject(error.to_string()))?;
    let mut members = Vec::with_capacity(plants.len());
    let mut safe = 0usize;
    let mut unsafe_count = 0usize;
    let mut reachable_product_states = 0usize;
    let mut explored_transitions = 0usize;
    for ((plant, digest), claimed) in plants.iter().copied().zip(&artifact.members) {
        if digest != claimed.plant_source_sha256 {
            return Err(reject(
                "proof-carrying controller MTBDD plant source digest mismatch",
            ));
        }
        let result = compose_verified_mtbdd_plant(
            &verified,
            plant,
            &claimed.wiring,
            claimed.initial_controller_state,
            claimed.initial_plant_state,
            claimed.bad_plant_output,
            claimed.horizon,
        )
        .map_err(|error| reject(error.to_string()))?;
        if result != claimed.result {
            return Err(reject(
                "proof-carrying controller MTBDD plant member result mismatch",
            ));
        }
        match result.answer {
            ControllerPlantAnswer::Safe => safe += 1,
            ControllerPlantAnswer::Unsafe => unsafe_count += 1,
        }
        reachable_product_states = reachable_product_states
            .checked_add(result.reachable_product_states)
            .ok_or_else(|| reject("proof-carrying reachable count overflow"))?;
        explored_transitions = explored_transitions
            .checked_add(result.explored_transitions)
            .ok_or_else(|| reject("proof-carrying transition count overflow"))?;
        members.push(result);
    }
    Ok(ControllerMtbddPlantBatchSummary {
        members,
        safe,
        unsafe_count,
        mtbdd_nodes: verified.summary().nodes,
        mtbdd_terminals: verified.summary().terminals,
        assignments_checked: verified.summary().assignments_checked,
        reachable_product_states,
        explored_transitions,
    })
}

/// Produce controller-local proof evidence without embedding any plant result.
pub fn produce_controller_proof_evidence_artifact(
    controller_model: &AigerTransition,
    controller_source_sha256: [u8; 32],
    controller: &ControllerMtbddArtifact,
) -> Result<ControllerProofEvidenceArtifact, ControllerPlantArtifactError> {
    let proof = produce_controller_mtbdd_equivalence_proof(
        controller_model,
        controller_source_sha256,
        controller,
    )
    .map_err(|error| reject(error.to_string()))?;
    verify_proof_carrying_mtbdd_for_composition(
        controller_model,
        controller_source_sha256,
        controller,
        &proof,
    )
    .map_err(|error| reject(error.to_string()))?;
    Ok(ControllerProofEvidenceArtifact {
        version: CONTROLLER_PROOF_EVIDENCE_VERSION,
        controller_mtbdd: encode_controller_mtbdd(controller)
            .map_err(|error| reject(error.to_string()))?,
        equivalence_proof: encode_controller_mtbdd_equivalence_proof(&proof)
            .map_err(|error| reject(error.to_string()))?,
    })
}

/// Encode one canonical, content-addressable controller evidence object.
pub fn encode_controller_proof_evidence_artifact(
    artifact: &ControllerProofEvidenceArtifact,
) -> Result<Vec<u8>, ControllerPlantArtifactError> {
    if artifact.version != CONTROLLER_PROOF_EVIDENCE_VERSION {
        return Err(reject("controller proof evidence version mismatch"));
    }
    decode_controller_mtbdd(&artifact.controller_mtbdd)
        .map_err(|error| reject(error.to_string()))?;
    decode_controller_mtbdd_equivalence_proof(&artifact.equivalence_proof)
        .map_err(|error| reject(error.to_string()))?;
    let mut bytes = Vec::new();
    bytes.extend_from_slice(CONTROLLER_PROOF_EVIDENCE_MAGIC);
    bytes.extend_from_slice(&artifact.version.to_le_bytes());
    bytes.extend_from_slice(
        &narrow(artifact.controller_mtbdd.len(), "controller MTBDD length")?.to_le_bytes(),
    );
    bytes.extend_from_slice(&artifact.controller_mtbdd);
    bytes.extend_from_slice(
        &narrow(
            artifact.equivalence_proof.len(),
            "controller equivalence proof length",
        )?
        .to_le_bytes(),
    );
    bytes.extend_from_slice(&artifact.equivalence_proof);
    bytes.extend_from_slice(&Sha256::digest(&bytes));
    if bytes.len() > MAX_CONTROLLER_PLANT_ARTIFACT_BYTES {
        return Err(reject("controller proof evidence exceeds byte limit"));
    }
    Ok(bytes)
}

/// Decode a controller evidence object without trusting its internal payloads.
pub fn decode_controller_proof_evidence_artifact(
    bytes: &[u8],
) -> Result<ControllerProofEvidenceArtifact, ControllerPlantArtifactError> {
    if bytes.len() < 8 + 4 + 4 + 4 + 32 || bytes.len() > MAX_CONTROLLER_PLANT_ARTIFACT_BYTES {
        return Err(reject("controller proof evidence size is invalid"));
    }
    let (payload, integrity) = bytes.split_at(bytes.len() - 32);
    if Sha256::digest(payload).as_slice() != integrity {
        return Err(reject("controller proof evidence integrity mismatch"));
    }
    let mut cursor = 0usize;
    if take(payload, &mut cursor, 8)? != CONTROLLER_PROOF_EVIDENCE_MAGIC {
        return Err(reject("controller proof evidence magic mismatch"));
    }
    let version = read_u32(payload, &mut cursor)?;
    if version != CONTROLLER_PROOF_EVIDENCE_VERSION {
        return Err(reject("controller proof evidence version mismatch"));
    }
    let mtbdd_len = read_u32(payload, &mut cursor)? as usize;
    let controller_mtbdd = take(payload, &mut cursor, mtbdd_len)?.to_vec();
    decode_controller_mtbdd(&controller_mtbdd).map_err(|error| reject(error.to_string()))?;
    let proof_len = read_u32(payload, &mut cursor)? as usize;
    let equivalence_proof = take(payload, &mut cursor, proof_len)?.to_vec();
    decode_controller_mtbdd_equivalence_proof(&equivalence_proof)
        .map_err(|error| reject(error.to_string()))?;
    if cursor != payload.len() {
        return Err(reject("controller proof evidence has trailing bytes"));
    }
    Ok(ControllerProofEvidenceArtifact {
        version,
        controller_mtbdd,
        equivalence_proof,
    })
}

fn put_artifact_member(
    bytes: &mut Vec<u8>,
    member: &ControllerPlantArtifactMember,
) -> Result<(), ControllerPlantArtifactError> {
    bytes.extend_from_slice(&member.plant_source_sha256);
    put_vec(bytes, &member.wiring.controller_sensor_inputs)?;
    put_vec(bytes, &member.wiring.controller_action_outputs)?;
    put_vec(bytes, &member.wiring.plant_sensor_outputs)?;
    put_vec(bytes, &member.wiring.plant_action_inputs)?;
    for (value, field) in [
        (member.initial_controller_state, "initial controller state"),
        (member.initial_plant_state, "initial plant state"),
        (member.bad_plant_output, "bad plant output"),
        (member.horizon, "member horizon"),
    ] {
        bytes.extend_from_slice(&narrow(value, field)?.to_le_bytes());
    }
    put_result(bytes, &member.result)
}

fn read_artifact_member(
    bytes: &[u8],
    cursor: &mut usize,
) -> Result<ControllerPlantArtifactMember, ControllerPlantArtifactError> {
    let plant_source_sha256 = take(bytes, cursor, 32)?
        .try_into()
        .map_err(|_| reject("plant digest decode failed"))?;
    let wiring = ControllerPlantWiring {
        controller_sensor_inputs: read_vec(bytes, cursor)?,
        controller_action_outputs: read_vec(bytes, cursor)?,
        plant_sensor_outputs: read_vec(bytes, cursor)?,
        plant_action_inputs: read_vec(bytes, cursor)?,
    };
    let initial_controller_state = read_u32(bytes, cursor)? as usize;
    let initial_plant_state = read_u32(bytes, cursor)? as usize;
    let bad_plant_output = read_u32(bytes, cursor)? as usize;
    let horizon = read_u32(bytes, cursor)? as usize;
    let result = read_result(bytes, cursor)?;
    Ok(ControllerPlantArtifactMember {
        plant_source_sha256,
        wiring,
        initial_controller_state,
        initial_plant_state,
        bad_plant_output,
        horizon,
        result,
    })
}

/// Produce plant-local results bound to canonical controller evidence bytes.
pub fn produce_bound_plant_results_artifact(
    controller_model: &AigerTransition,
    controller_source_sha256: [u8; 32],
    controller_evidence_bytes: &[u8],
    members: &[ControllerPlantArtifactInput<'_>],
) -> Result<BoundPlantResultsArtifact, ControllerPlantArtifactError> {
    let admitted = admit_controller_proof_evidence(
        controller_model,
        controller_source_sha256,
        controller_evidence_bytes,
    )?;
    produce_bound_plant_results_with_admitted_controller(&admitted, members)
}

/// Produce replaceable plant results after admitting controller evidence once.
pub fn produce_bound_plant_results_with_admitted_controller(
    admitted: &AdmittedControllerProofEvidence,
    members: &[ControllerPlantArtifactInput<'_>],
) -> Result<BoundPlantResultsArtifact, ControllerPlantArtifactError> {
    if members.is_empty() || members.len() > MAX_CONTROLLER_PLANT_ARTIFACT_MEMBERS {
        return Err(reject("bound plant result member count is outside limit"));
    }
    let verified = reuse_verified_controller_mtbdd(&admitted.controller, admitted.summary.clone());
    let members = members
        .iter()
        .map(|member| {
            let result = compose_verified_mtbdd_plant(
                &verified,
                member.plant,
                member.wiring,
                member.initial_controller_state,
                member.initial_plant_state,
                member.bad_plant_output,
                member.horizon,
            )
            .map_err(|error| reject(error.to_string()))?;
            Ok(ControllerPlantArtifactMember {
                plant_source_sha256: member.plant_source_sha256,
                wiring: member.wiring.clone(),
                initial_controller_state: member.initial_controller_state,
                initial_plant_state: member.initial_plant_state,
                bad_plant_output: member.bad_plant_output,
                horizon: member.horizon,
                result,
            })
        })
        .collect::<Result<Vec<_>, ControllerPlantArtifactError>>()?;
    Ok(BoundPlantResultsArtifact {
        version: BOUND_PLANT_RESULTS_VERSION,
        controller_evidence_sha256: admitted.evidence_sha256,
        members,
    })
}

pub fn encode_bound_plant_results_artifact(
    artifact: &BoundPlantResultsArtifact,
) -> Result<Vec<u8>, ControllerPlantArtifactError> {
    if artifact.version != BOUND_PLANT_RESULTS_VERSION
        || artifact.members.is_empty()
        || artifact.members.len() > MAX_CONTROLLER_PLANT_ARTIFACT_MEMBERS
    {
        return Err(reject("bound plant result dimensions are invalid"));
    }
    let mut bytes = Vec::new();
    bytes.extend_from_slice(BOUND_PLANT_RESULTS_MAGIC);
    bytes.extend_from_slice(&artifact.version.to_le_bytes());
    bytes.extend_from_slice(&artifact.controller_evidence_sha256);
    bytes.push(artifact.members.len() as u8);
    for member in &artifact.members {
        put_artifact_member(&mut bytes, member)?;
    }
    bytes.extend_from_slice(&Sha256::digest(&bytes));
    if bytes.len() > MAX_CONTROLLER_PLANT_ARTIFACT_BYTES {
        return Err(reject("bound plant result artifact exceeds byte limit"));
    }
    Ok(bytes)
}

pub fn decode_bound_plant_results_artifact(
    bytes: &[u8],
) -> Result<BoundPlantResultsArtifact, ControllerPlantArtifactError> {
    if bytes.len() < 8 + 4 + 32 + 1 + 32 || bytes.len() > MAX_CONTROLLER_PLANT_ARTIFACT_BYTES {
        return Err(reject("bound plant result artifact size is invalid"));
    }
    let (payload, integrity) = bytes.split_at(bytes.len() - 32);
    if Sha256::digest(payload).as_slice() != integrity {
        return Err(reject("bound plant result artifact integrity mismatch"));
    }
    let mut cursor = 0usize;
    if take(payload, &mut cursor, 8)? != BOUND_PLANT_RESULTS_MAGIC {
        return Err(reject("bound plant result artifact magic mismatch"));
    }
    let version = read_u32(payload, &mut cursor)?;
    if version != BOUND_PLANT_RESULTS_VERSION {
        return Err(reject("bound plant result artifact version mismatch"));
    }
    let controller_evidence_sha256 = take(payload, &mut cursor, 32)?
        .try_into()
        .map_err(|_| reject("controller evidence digest decode failed"))?;
    let member_count = read_u8(payload, &mut cursor)? as usize;
    if member_count == 0 || member_count > MAX_CONTROLLER_PLANT_ARTIFACT_MEMBERS {
        return Err(reject("bound plant result member count is outside limit"));
    }
    let mut members = Vec::with_capacity(member_count);
    for _ in 0..member_count {
        members.push(read_artifact_member(payload, &mut cursor)?);
    }
    if cursor != payload.len() {
        return Err(reject("bound plant result artifact has trailing bytes"));
    }
    Ok(BoundPlantResultsArtifact {
        version,
        controller_evidence_sha256,
        members,
    })
}

/// Check controller evidence once and return a non-forgeable process-local capability.
pub fn admit_controller_proof_evidence(
    controller_model: &AigerTransition,
    controller_source_sha256: [u8; 32],
    controller_evidence_bytes: &[u8],
) -> Result<AdmittedControllerProofEvidence, ControllerPlantArtifactError> {
    let evidence = decode_controller_proof_evidence_artifact(controller_evidence_bytes)?;
    let controller = decode_controller_mtbdd(&evidence.controller_mtbdd)
        .map_err(|error| reject(error.to_string()))?;
    let proof = decode_controller_mtbdd_equivalence_proof(&evidence.equivalence_proof)
        .map_err(|error| reject(error.to_string()))?;
    let summary = verify_proof_carrying_mtbdd_for_composition(
        controller_model,
        controller_source_sha256,
        &controller,
        &proof,
    )
    .map_err(|error| reject(error.to_string()))?
    .summary()
    .clone();
    Ok(AdmittedControllerProofEvidence {
        evidence_sha256: Sha256::digest(controller_evidence_bytes).into(),
        controller,
        summary,
    })
}

/// Preflight controller evidence byte and embedded proof limits without
/// checking the proof or admitting a trusted controller capability.
pub fn assess_controller_proof_evidence_resources(
    controller_evidence_bytes: &[u8],
    envelope: ControllerProofEvidenceResourceEnvelope,
) -> Result<ControllerProofEvidenceResourceAssessment, ControllerPlantArtifactError> {
    if controller_evidence_bytes.len() > envelope.max_artifact_bytes {
        return Err(reject(
            "controller proof evidence resource artifact-byte limit exceeded",
        ));
    }
    let evidence = decode_controller_proof_evidence_artifact(controller_evidence_bytes)?;
    let proof = decode_controller_mtbdd_equivalence_proof(&evidence.equivalence_proof)
        .map_err(|error| reject(error.to_string()))?;
    if proof.proof.len() > envelope.max_unsat_proof_bytes {
        return Err(reject(
            "controller proof evidence resource UNSAT-proof limit exceeded",
        ));
    }
    Ok(ControllerProofEvidenceResourceAssessment {
        version: CONTROLLER_PROOF_EVIDENCE_RESOURCE_ENVELOPE_VERSION,
        artifact_bytes: controller_evidence_bytes.len(),
        mtbdd_bytes: evidence.controller_mtbdd.len(),
        equivalence_artifact_bytes: evidence.equivalence_proof.len(),
        unsat_proof_bytes: proof.proof.len(),
    })
}

/// Admit controller evidence only after it fits every caller-selected proof
/// resource limit.
pub fn admit_controller_proof_evidence_with_resources(
    controller_model: &AigerTransition,
    controller_source_sha256: [u8; 32],
    controller_evidence_bytes: &[u8],
    envelope: ControllerProofEvidenceResourceEnvelope,
) -> Result<GovernedAdmittedControllerProofEvidence, ControllerPlantArtifactError> {
    let resources =
        assess_controller_proof_evidence_resources(controller_evidence_bytes, envelope)?;
    let admitted = admit_controller_proof_evidence(
        controller_model,
        controller_source_sha256,
        controller_evidence_bytes,
    )?;
    Ok(GovernedAdmittedControllerProofEvidence {
        resources,
        admitted,
    })
}

/// Conservatively preflight a replaceable plant batch before semantic replay.
pub fn assess_bound_plant_results_resources(
    controller_model: &AigerTransition,
    members: &[ControllerPlantArtifactInput<'_>],
    plant_results_bytes: &[u8],
    envelope: ControllerPlantResourceEnvelope,
) -> Result<ControllerPlantResourceAssessment, ControllerPlantArtifactError> {
    if plant_results_bytes.len() > envelope.max_artifact_bytes {
        return Err(reject(
            "bound plant result resource artifact-byte limit exceeded",
        ));
    }
    if members.is_empty() || members.len() > envelope.max_members {
        return Err(reject("bound plant result resource member limit exceeded"));
    }
    let artifact = decode_bound_plant_results_artifact(plant_results_bytes)?;
    if members.len() != artifact.members.len() {
        return Err(reject("bound plant result resource member count mismatch"));
    }
    let controller_states = bounded_state_count(controller_model.latches.len())?;
    let mut maximum_member_horizon = 0usize;
    let mut maximum_product_states = 0usize;
    let mut transition_evaluation_bound = 0usize;
    for (member, claimed) in members.iter().zip(&artifact.members) {
        if member.plant_source_sha256 != claimed.plant_source_sha256
            || member.wiring != &claimed.wiring
            || member.initial_controller_state != claimed.initial_controller_state
            || member.initial_plant_state != claimed.initial_plant_state
            || member.bad_plant_output != claimed.bad_plant_output
            || member.horizon != claimed.horizon
        {
            return Err(reject("bound plant result resource obligation mismatch"));
        }
        if member.horizon > envelope.max_member_horizon {
            return Err(reject("bound plant result resource horizon limit exceeded"));
        }
        maximum_member_horizon = maximum_member_horizon.max(member.horizon);
        let plant_states = bounded_state_count(member.plant.latches.len())?;
        let product_states = controller_states
            .checked_mul(plant_states)
            .ok_or_else(|| reject("bound plant result product-state bound overflow"))?;
        if product_states > envelope.max_product_states_per_member {
            return Err(reject(
                "bound plant result resource product-state limit exceeded",
            ));
        }
        maximum_product_states = maximum_product_states.max(product_states);
        let external_inputs = member
            .plant
            .inputs
            .len()
            .checked_sub(member.wiring.plant_action_inputs.len())
            .ok_or_else(|| reject("bound plant result resource wiring is invalid"))?;
        let external_patterns = 1usize
            .checked_shl(
                u32::try_from(external_inputs)
                    .map_err(|_| reject("bound plant result input width exceeds range"))?,
            )
            .ok_or_else(|| reject("bound plant result input width exceeds range"))?;
        let member_bound = product_states
            .checked_mul(member.horizon.saturating_add(1))
            .and_then(|value| value.checked_mul(external_patterns))
            .ok_or_else(|| reject("bound plant result transition bound overflow"))?;
        transition_evaluation_bound = transition_evaluation_bound
            .checked_add(member_bound)
            .ok_or_else(|| reject("bound plant result transition bound overflow"))?;
        if transition_evaluation_bound > envelope.max_transition_evaluations {
            return Err(reject(
                "bound plant result resource transition limit exceeded",
            ));
        }
    }
    Ok(ControllerPlantResourceAssessment {
        version: CONTROLLER_PLANT_RESOURCE_ENVELOPE_VERSION,
        backend: ControllerMtbddPlantPortfolioBackend::Mtbdd,
        artifact_bytes: plant_results_bytes.len(),
        members: members.len(),
        maximum_member_horizon,
        maximum_product_states,
        transition_evaluation_bound,
    })
}

/// Check a plant-result batch using previously admitted controller evidence.
pub fn verify_bound_plant_results_with_admitted_controller(
    admitted: &AdmittedControllerProofEvidence,
    members: &[ControllerPlantArtifactInput<'_>],
    plant_results_bytes: &[u8],
) -> Result<ControllerMtbddPlantBatchSummary, ControllerPlantArtifactError> {
    let results = decode_bound_plant_results_artifact(plant_results_bytes)?;
    if results.controller_evidence_sha256 != admitted.evidence_sha256 {
        return Err(reject("bound plant result controller evidence mismatch"));
    }
    if members.len() != results.members.len() {
        return Err(reject("bound plant result source count mismatch"));
    }
    let verified = reuse_verified_controller_mtbdd(&admitted.controller, admitted.summary.clone());
    let mut verified_members = Vec::with_capacity(members.len());
    let mut safe = 0usize;
    let mut unsafe_count = 0usize;
    let mut reachable_product_states = 0usize;
    let mut explored_transitions = 0usize;
    for (member, claimed) in members.iter().zip(&results.members) {
        if member.plant_source_sha256 != claimed.plant_source_sha256
            || member.wiring != &claimed.wiring
            || member.initial_controller_state != claimed.initial_controller_state
            || member.initial_plant_state != claimed.initial_plant_state
            || member.bad_plant_output != claimed.bad_plant_output
            || member.horizon != claimed.horizon
        {
            return Err(reject("bound plant result obligation mismatch"));
        }
        let result = compose_verified_mtbdd_plant(
            &verified,
            member.plant,
            member.wiring,
            member.initial_controller_state,
            member.initial_plant_state,
            member.bad_plant_output,
            member.horizon,
        )
        .map_err(|error| reject(error.to_string()))?;
        if result != claimed.result {
            return Err(reject("bound plant result mismatch"));
        }
        match result.answer {
            ControllerPlantAnswer::Safe => safe += 1,
            ControllerPlantAnswer::Unsafe => unsafe_count += 1,
        }
        reachable_product_states = reachable_product_states
            .checked_add(result.reachable_product_states)
            .ok_or_else(|| reject("bound plant reachable count overflow"))?;
        explored_transitions = explored_transitions
            .checked_add(result.explored_transitions)
            .ok_or_else(|| reject("bound plant transition count overflow"))?;
        verified_members.push(result);
    }
    Ok(ControllerMtbddPlantBatchSummary {
        members: verified_members,
        safe,
        unsafe_count,
        mtbdd_nodes: verified.summary().nodes,
        mtbdd_terminals: verified.summary().terminals,
        assignments_checked: verified.summary().assignments_checked,
        reachable_product_states,
        explored_transitions,
    })
}

/// Verify a replaceable plant batch only after every caller-selected
/// composition limit fits.
pub fn verify_bound_plant_results_with_resources(
    admitted: &AdmittedControllerProofEvidence,
    controller_model: &AigerTransition,
    members: &[ControllerPlantArtifactInput<'_>],
    plant_results_bytes: &[u8],
    envelope: ControllerPlantResourceEnvelope,
) -> Result<GovernedBoundPlantResultsSummary, ControllerPlantArtifactError> {
    let resources = assess_bound_plant_results_resources(
        controller_model,
        members,
        plant_results_bytes,
        envelope,
    )?;
    let verification = verify_bound_plant_results_with_admitted_controller(
        admitted,
        members,
        plant_results_bytes,
    )?;
    Ok(GovernedBoundPlantResultsSummary {
        resources,
        verification,
    })
}

/// Stateless convenience path that admits controller evidence before checking
/// every separately supplied plant result.
pub fn verify_bound_plant_results_artifact(
    controller_model: &AigerTransition,
    controller_source_sha256: [u8; 32],
    controller_evidence_bytes: &[u8],
    members: &[ControllerPlantArtifactInput<'_>],
    plant_results_bytes: &[u8],
) -> Result<ControllerMtbddPlantBatchSummary, ControllerPlantArtifactError> {
    let admitted = admit_controller_proof_evidence(
        controller_model,
        controller_source_sha256,
        controller_evidence_bytes,
    )?;
    verify_bound_plant_results_with_admitted_controller(&admitted, members, plant_results_bytes)
}

pub fn produce_controller_direct_plant_artifact(
    controller_model: &AigerTransition,
    controller_source_sha256: [u8; 32],
    members: &[ControllerPlantArtifactInput<'_>],
) -> Result<ControllerDirectPlantBatchArtifact, ControllerPlantArtifactError> {
    let inputs = members
        .iter()
        .map(|member| ControllerPlantBatchInput {
            plant: member.plant,
            wiring: member.wiring,
            initial_controller_state: member.initial_controller_state,
            initial_plant_state: member.initial_plant_state,
            bad_plant_output: member.bad_plant_output,
            horizon: member.horizon,
        })
        .collect::<Vec<_>>();
    let batch = compose_controller_plant_direct_batch(controller_model, &inputs)
        .map_err(|error| reject(error.to_string()))?;
    let artifact_members = members
        .iter()
        .zip(batch.members)
        .map(|(member, result)| ControllerPlantArtifactMember {
            plant_source_sha256: member.plant_source_sha256,
            wiring: member.wiring.clone(),
            initial_controller_state: member.initial_controller_state,
            initial_plant_state: member.initial_plant_state,
            bad_plant_output: member.bad_plant_output,
            horizon: member.horizon,
            result,
        })
        .collect();
    Ok(ControllerDirectPlantBatchArtifact {
        version: DIRECT_PLANT_ARTIFACT_VERSION,
        controller_source_sha256,
        members: artifact_members,
    })
}

pub fn encode_controller_direct_plant_artifact(
    artifact: &ControllerDirectPlantBatchArtifact,
) -> Result<Vec<u8>, ControllerPlantArtifactError> {
    if artifact.version != DIRECT_PLANT_ARTIFACT_VERSION
        || artifact.members.is_empty()
        || artifact.members.len() > MAX_CONTROLLER_PLANT_ARTIFACT_MEMBERS
    {
        return Err(reject(
            "controller direct plant artifact dimensions are invalid",
        ));
    }
    let mut bytes = Vec::new();
    bytes.extend_from_slice(DIRECT_MAGIC);
    bytes.extend_from_slice(&artifact.version.to_le_bytes());
    bytes.extend_from_slice(&artifact.controller_source_sha256);
    bytes.push(artifact.members.len() as u8);
    for member in &artifact.members {
        bytes.extend_from_slice(&member.plant_source_sha256);
        put_vec(&mut bytes, &member.wiring.controller_sensor_inputs)?;
        put_vec(&mut bytes, &member.wiring.controller_action_outputs)?;
        put_vec(&mut bytes, &member.wiring.plant_sensor_outputs)?;
        put_vec(&mut bytes, &member.wiring.plant_action_inputs)?;
        for (value, field) in [
            (member.initial_controller_state, "initial controller state"),
            (member.initial_plant_state, "initial plant state"),
            (member.bad_plant_output, "bad plant output"),
            (member.horizon, "member horizon"),
        ] {
            bytes.extend_from_slice(&narrow(value, field)?.to_le_bytes());
        }
        put_result(&mut bytes, &member.result)?;
    }
    let integrity = Sha256::digest(&bytes);
    bytes.extend_from_slice(&integrity);
    if bytes.len() > MAX_CONTROLLER_PLANT_ARTIFACT_BYTES {
        return Err(reject(
            "controller direct plant artifact exceeds byte limit",
        ));
    }
    Ok(bytes)
}

pub fn decode_controller_direct_plant_artifact(
    bytes: &[u8],
) -> Result<ControllerDirectPlantBatchArtifact, ControllerPlantArtifactError> {
    if bytes.len() > MAX_CONTROLLER_PLANT_ARTIFACT_BYTES || bytes.len() < 77 {
        return Err(reject("controller direct plant artifact size is invalid"));
    }
    let payload_len = bytes.len() - 32;
    let (payload, claimed_integrity) = bytes.split_at(payload_len);
    if Sha256::digest(payload).as_slice() != claimed_integrity {
        return Err(reject(
            "controller direct plant artifact integrity mismatch",
        ));
    }
    let mut cursor = 0usize;
    if take(payload, &mut cursor, DIRECT_MAGIC.len())? != DIRECT_MAGIC {
        return Err(reject("controller direct plant artifact magic mismatch"));
    }
    let version = read_u32(payload, &mut cursor)?;
    if version != DIRECT_PLANT_ARTIFACT_VERSION {
        return Err(reject("controller direct plant artifact version mismatch"));
    }
    let controller_source_sha256 = take(payload, &mut cursor, 32)?
        .try_into()
        .map_err(|_| reject("controller digest decode failed"))?;
    let member_count = read_u8(payload, &mut cursor)? as usize;
    if member_count == 0 || member_count > MAX_CONTROLLER_PLANT_ARTIFACT_MEMBERS {
        return Err(reject(
            "controller direct plant member count is outside limit",
        ));
    }
    let mut members = Vec::with_capacity(member_count);
    for _ in 0..member_count {
        let plant_source_sha256 = take(payload, &mut cursor, 32)?
            .try_into()
            .map_err(|_| reject("plant digest decode failed"))?;
        let wiring = ControllerPlantWiring {
            controller_sensor_inputs: read_vec(payload, &mut cursor)?,
            controller_action_outputs: read_vec(payload, &mut cursor)?,
            plant_sensor_outputs: read_vec(payload, &mut cursor)?,
            plant_action_inputs: read_vec(payload, &mut cursor)?,
        };
        let initial_controller_state = read_u32(payload, &mut cursor)? as usize;
        let initial_plant_state = read_u32(payload, &mut cursor)? as usize;
        let bad_plant_output = read_u32(payload, &mut cursor)? as usize;
        let horizon = read_u32(payload, &mut cursor)? as usize;
        let result = read_result(payload, &mut cursor)?;
        members.push(ControllerPlantArtifactMember {
            plant_source_sha256,
            wiring,
            initial_controller_state,
            initial_plant_state,
            bad_plant_output,
            horizon,
            result,
        });
    }
    if cursor != payload.len() {
        return Err(reject(
            "controller direct plant artifact has trailing bytes",
        ));
    }
    Ok(ControllerDirectPlantBatchArtifact {
        version,
        controller_source_sha256,
        members,
    })
}

pub fn verify_controller_direct_plant_artifact(
    controller_model: &AigerTransition,
    controller_source_sha256: [u8; 32],
    plants: &[(&AigerTransition, [u8; 32])],
    artifact_bytes: &[u8],
) -> Result<ControllerPlantBatchResult, ControllerPlantArtifactError> {
    let artifact = decode_controller_direct_plant_artifact(artifact_bytes)?;
    if artifact.controller_source_sha256 != controller_source_sha256
        || plants.len() != artifact.members.len()
    {
        return Err(reject("controller direct plant source binding mismatch"));
    }
    let inputs = plants
        .iter()
        .zip(&artifact.members)
        .map(|(&(plant, digest), member)| {
            if digest != member.plant_source_sha256 {
                return Err(reject("controller direct plant source digest mismatch"));
            }
            Ok(ControllerPlantBatchInput {
                plant,
                wiring: &member.wiring,
                initial_controller_state: member.initial_controller_state,
                initial_plant_state: member.initial_plant_state,
                bad_plant_output: member.bad_plant_output,
                horizon: member.horizon,
            })
        })
        .collect::<Result<Vec<_>, _>>()?;
    let verified = compose_controller_plant_direct_batch(controller_model, &inputs)
        .map_err(|error| reject(error.to_string()))?;
    if verified
        .members
        .iter()
        .zip(&artifact.members)
        .any(|(actual, claimed)| actual != &claimed.result)
    {
        return Err(reject("controller direct plant member result mismatch"));
    }
    Ok(verified)
}

fn portfolio_reason_from_failure(
    failure: ControllerMtbddAdmissionFailure,
) -> ControllerMtbddPlantSelectionReason {
    match failure {
        ControllerMtbddAdmissionFailure::BoundaryLimit => {
            ControllerMtbddPlantSelectionReason::BoundaryLimit
        }
        ControllerMtbddAdmissionFailure::TerminalLimit => {
            ControllerMtbddPlantSelectionReason::TerminalLimit
        }
        ControllerMtbddAdmissionFailure::NodeLimit => {
            ControllerMtbddPlantSelectionReason::NodeLimit
        }
    }
}

fn portfolio_backend_tag(backend: ControllerMtbddPlantPortfolioBackend) -> u8 {
    match backend {
        ControllerMtbddPlantPortfolioBackend::Mtbdd => 0,
        ControllerMtbddPlantPortfolioBackend::DirectExact => 1,
    }
}

fn portfolio_reason_tag(reason: ControllerMtbddPlantSelectionReason) -> u8 {
    match reason {
        ControllerMtbddPlantSelectionReason::MtbddAdmitted => 0,
        ControllerMtbddPlantSelectionReason::BoundaryLimit => 1,
        ControllerMtbddPlantSelectionReason::TerminalLimit => 2,
        ControllerMtbddPlantSelectionReason::NodeLimit => 3,
    }
}

pub fn encode_controller_mtbdd_plant_portfolio(
    artifact: &ControllerMtbddPlantPortfolioArtifact,
) -> Result<Vec<u8>, ControllerPlantArtifactError> {
    let route_is_valid = matches!(
        (artifact.backend, artifact.reason),
        (
            ControllerMtbddPlantPortfolioBackend::Mtbdd,
            ControllerMtbddPlantSelectionReason::MtbddAdmitted
        ) | (
            ControllerMtbddPlantPortfolioBackend::DirectExact,
            ControllerMtbddPlantSelectionReason::BoundaryLimit
                | ControllerMtbddPlantSelectionReason::TerminalLimit
                | ControllerMtbddPlantSelectionReason::NodeLimit
        )
    );
    if artifact.version != MTBDD_PLANT_PORTFOLIO_VERSION
        || !route_is_valid
        || artifact.relevant_inputs.is_empty()
        || artifact.observed_outputs.is_empty()
        || artifact.payload.is_empty()
    {
        return Err(reject("controller MTBDD portfolio dimensions are invalid"));
    }
    match artifact.backend {
        ControllerMtbddPlantPortfolioBackend::Mtbdd => {
            decode_controller_mtbdd_plant_artifact(&artifact.payload)?;
        }
        ControllerMtbddPlantPortfolioBackend::DirectExact => {
            decode_controller_direct_plant_artifact(&artifact.payload)?;
        }
    }
    let mut bytes = Vec::new();
    bytes.extend_from_slice(PORTFOLIO_MAGIC);
    bytes.extend_from_slice(&artifact.version.to_le_bytes());
    bytes.push(portfolio_backend_tag(artifact.backend));
    bytes.push(portfolio_reason_tag(artifact.reason));
    put_vec(&mut bytes, &artifact.relevant_inputs)?;
    put_vec(&mut bytes, &artifact.observed_outputs)?;
    bytes.extend_from_slice(
        &narrow(artifact.payload.len(), "portfolio payload length")?.to_le_bytes(),
    );
    bytes.extend_from_slice(&artifact.payload);
    let integrity = Sha256::digest(&bytes);
    bytes.extend_from_slice(&integrity);
    if bytes.len() > MAX_CONTROLLER_PLANT_ARTIFACT_BYTES {
        return Err(reject("controller MTBDD portfolio exceeds byte limit"));
    }
    Ok(bytes)
}

pub fn decode_controller_mtbdd_plant_portfolio(
    bytes: &[u8],
) -> Result<ControllerMtbddPlantPortfolioArtifact, ControllerPlantArtifactError> {
    if bytes.len() > MAX_CONTROLLER_PLANT_ARTIFACT_BYTES || bytes.len() < 52 {
        return Err(reject("controller MTBDD portfolio size is invalid"));
    }
    let payload_len = bytes.len() - 32;
    let (payload, claimed_integrity) = bytes.split_at(payload_len);
    if Sha256::digest(payload).as_slice() != claimed_integrity {
        return Err(reject("controller MTBDD portfolio integrity mismatch"));
    }
    let mut cursor = 0usize;
    if take(payload, &mut cursor, PORTFOLIO_MAGIC.len())? != PORTFOLIO_MAGIC {
        return Err(reject("controller MTBDD portfolio magic mismatch"));
    }
    let version = read_u32(payload, &mut cursor)?;
    if version != MTBDD_PLANT_PORTFOLIO_VERSION {
        return Err(reject("controller MTBDD portfolio version mismatch"));
    }
    let backend = match read_u8(payload, &mut cursor)? {
        0 => ControllerMtbddPlantPortfolioBackend::Mtbdd,
        1 => ControllerMtbddPlantPortfolioBackend::DirectExact,
        _ => return Err(reject("controller MTBDD portfolio backend is invalid")),
    };
    let reason = match read_u8(payload, &mut cursor)? {
        0 => ControllerMtbddPlantSelectionReason::MtbddAdmitted,
        1 => ControllerMtbddPlantSelectionReason::BoundaryLimit,
        2 => ControllerMtbddPlantSelectionReason::TerminalLimit,
        3 => ControllerMtbddPlantSelectionReason::NodeLimit,
        _ => return Err(reject("controller MTBDD portfolio reason is invalid")),
    };
    let relevant_inputs = read_vec(payload, &mut cursor)?;
    let observed_outputs = read_vec(payload, &mut cursor)?;
    let embedded_len = read_u32(payload, &mut cursor)? as usize;
    let embedded = take(payload, &mut cursor, embedded_len)?.to_vec();
    if cursor != payload.len() {
        return Err(reject("controller MTBDD portfolio has trailing bytes"));
    }
    let artifact = ControllerMtbddPlantPortfolioArtifact {
        version,
        backend,
        reason,
        relevant_inputs,
        observed_outputs,
        payload: embedded,
    };
    encode_controller_mtbdd_plant_portfolio(&artifact)?;
    Ok(artifact)
}

pub fn produce_controller_mtbdd_plant_portfolio(
    controller_model: &AigerTransition,
    controller_source_sha256: [u8; 32],
    relevant_inputs: &[usize],
    observed_outputs: &[usize],
    members: &[ControllerPlantArtifactInput<'_>],
) -> Result<Vec<u8>, ControllerPlantArtifactError> {
    if !portfolio_boundary_matches_members(relevant_inputs, observed_outputs, members) {
        return Err(reject(
            "controller MTBDD portfolio member boundary mismatch",
        ));
    }
    let (backend, reason, payload) = match produce_controller_mtbdd(
        controller_model,
        controller_source_sha256,
        relevant_inputs,
        observed_outputs,
    ) {
        Ok(mtbdd) => {
            let artifact = produce_controller_mtbdd_plant_artifact(
                controller_model,
                controller_source_sha256,
                &mtbdd,
                members,
            )?;
            (
                ControllerMtbddPlantPortfolioBackend::Mtbdd,
                ControllerMtbddPlantSelectionReason::MtbddAdmitted,
                encode_controller_mtbdd_plant_artifact(&artifact)?,
            )
        }
        Err(error) => {
            let failure = error
                .admission_failure()
                .ok_or_else(|| reject(error.to_string()))?;
            let artifact = produce_controller_direct_plant_artifact(
                controller_model,
                controller_source_sha256,
                members,
            )?;
            (
                ControllerMtbddPlantPortfolioBackend::DirectExact,
                portfolio_reason_from_failure(failure),
                encode_controller_direct_plant_artifact(&artifact)?,
            )
        }
    };
    encode_controller_mtbdd_plant_portfolio(&ControllerMtbddPlantPortfolioArtifact {
        version: MTBDD_PLANT_PORTFOLIO_VERSION,
        backend,
        reason,
        relevant_inputs: relevant_inputs.to_vec(),
        observed_outputs: observed_outputs.to_vec(),
        payload,
    })
}

fn proof_portfolio_backend_tag(backend: ControllerProofMtbddPlantPortfolioBackend) -> u8 {
    match backend {
        ControllerProofMtbddPlantPortfolioBackend::ProofMtbdd => 0,
        ControllerProofMtbddPlantPortfolioBackend::DirectExact => 1,
    }
}

pub fn encode_controller_proof_mtbdd_plant_portfolio(
    artifact: &ControllerProofMtbddPlantPortfolioArtifact,
) -> Result<Vec<u8>, ControllerPlantArtifactError> {
    let route_is_valid = matches!(
        (artifact.backend, artifact.reason),
        (
            ControllerProofMtbddPlantPortfolioBackend::ProofMtbdd,
            ControllerMtbddPlantSelectionReason::MtbddAdmitted
        ) | (
            ControllerProofMtbddPlantPortfolioBackend::DirectExact,
            ControllerMtbddPlantSelectionReason::BoundaryLimit
                | ControllerMtbddPlantSelectionReason::TerminalLimit
                | ControllerMtbddPlantSelectionReason::NodeLimit
        )
    );
    if artifact.version != PROOF_MTBDD_PLANT_PORTFOLIO_VERSION
        || !route_is_valid
        || artifact.relevant_inputs.is_empty()
        || artifact.observed_outputs.is_empty()
        || artifact.payload.is_empty()
    {
        return Err(reject(
            "proof-carrying controller MTBDD portfolio dimensions are invalid",
        ));
    }
    match artifact.backend {
        ControllerProofMtbddPlantPortfolioBackend::ProofMtbdd => {
            decode_controller_proof_mtbdd_plant_artifact(&artifact.payload)?;
        }
        ControllerProofMtbddPlantPortfolioBackend::DirectExact => {
            decode_controller_direct_plant_artifact(&artifact.payload)?;
        }
    }
    let mut bytes = Vec::new();
    bytes.extend_from_slice(PROOF_PORTFOLIO_MAGIC);
    bytes.extend_from_slice(&artifact.version.to_le_bytes());
    bytes.push(proof_portfolio_backend_tag(artifact.backend));
    bytes.push(portfolio_reason_tag(artifact.reason));
    put_vec(&mut bytes, &artifact.relevant_inputs)?;
    put_vec(&mut bytes, &artifact.observed_outputs)?;
    bytes.extend_from_slice(
        &narrow(artifact.payload.len(), "proof portfolio payload length")?.to_le_bytes(),
    );
    bytes.extend_from_slice(&artifact.payload);
    bytes.extend_from_slice(&Sha256::digest(&bytes));
    if bytes.len() > MAX_CONTROLLER_PLANT_ARTIFACT_BYTES {
        return Err(reject(
            "proof-carrying controller MTBDD portfolio exceeds byte limit",
        ));
    }
    Ok(bytes)
}

pub fn decode_controller_proof_mtbdd_plant_portfolio(
    bytes: &[u8],
) -> Result<ControllerProofMtbddPlantPortfolioArtifact, ControllerPlantArtifactError> {
    if bytes.len() > MAX_CONTROLLER_PLANT_ARTIFACT_BYTES || bytes.len() < 52 {
        return Err(reject(
            "proof-carrying controller MTBDD portfolio size is invalid",
        ));
    }
    let payload_len = bytes.len() - 32;
    let (payload, integrity) = bytes.split_at(payload_len);
    if Sha256::digest(payload).as_slice() != integrity {
        return Err(reject(
            "proof-carrying controller MTBDD portfolio integrity mismatch",
        ));
    }
    let mut cursor = 0usize;
    if take(payload, &mut cursor, PROOF_PORTFOLIO_MAGIC.len())? != PROOF_PORTFOLIO_MAGIC {
        return Err(reject(
            "proof-carrying controller MTBDD portfolio magic mismatch",
        ));
    }
    let version = read_u32(payload, &mut cursor)?;
    if version != PROOF_MTBDD_PLANT_PORTFOLIO_VERSION {
        return Err(reject(
            "proof-carrying controller MTBDD portfolio version mismatch",
        ));
    }
    let backend = match read_u8(payload, &mut cursor)? {
        0 => ControllerProofMtbddPlantPortfolioBackend::ProofMtbdd,
        1 => ControllerProofMtbddPlantPortfolioBackend::DirectExact,
        _ => {
            return Err(reject(
                "proof-carrying controller MTBDD portfolio backend is invalid",
            ));
        }
    };
    let reason = match read_u8(payload, &mut cursor)? {
        0 => ControllerMtbddPlantSelectionReason::MtbddAdmitted,
        1 => ControllerMtbddPlantSelectionReason::BoundaryLimit,
        2 => ControllerMtbddPlantSelectionReason::TerminalLimit,
        3 => ControllerMtbddPlantSelectionReason::NodeLimit,
        _ => {
            return Err(reject(
                "proof-carrying controller MTBDD portfolio reason is invalid",
            ));
        }
    };
    let relevant_inputs = read_vec(payload, &mut cursor)?;
    let observed_outputs = read_vec(payload, &mut cursor)?;
    let embedded_len = read_u32(payload, &mut cursor)? as usize;
    let embedded = take(payload, &mut cursor, embedded_len)?.to_vec();
    if cursor != payload.len() {
        return Err(reject(
            "proof-carrying controller MTBDD portfolio has trailing bytes",
        ));
    }
    let artifact = ControllerProofMtbddPlantPortfolioArtifact {
        version,
        backend,
        reason,
        relevant_inputs,
        observed_outputs,
        payload: embedded,
    };
    encode_controller_proof_mtbdd_plant_portfolio(&artifact)?;
    Ok(artifact)
}

/// Produce a proof-carrying MTBDD portfolio when the exact MTBDD boundary is
/// statically admitted. Only a narrow MTBDD admission failure selects direct
/// exact fallback; proof production and encoding failures propagate.
pub fn produce_controller_proof_mtbdd_plant_portfolio(
    controller_model: &AigerTransition,
    controller_source_sha256: [u8; 32],
    relevant_inputs: &[usize],
    observed_outputs: &[usize],
    members: &[ControllerPlantArtifactInput<'_>],
) -> Result<Vec<u8>, ControllerPlantArtifactError> {
    if !portfolio_boundary_matches_members(relevant_inputs, observed_outputs, members) {
        return Err(reject(
            "proof-carrying controller MTBDD portfolio member boundary mismatch",
        ));
    }
    let (backend, reason, payload) = match produce_controller_mtbdd(
        controller_model,
        controller_source_sha256,
        relevant_inputs,
        observed_outputs,
    ) {
        Ok(mtbdd) => {
            let artifact = produce_controller_proof_mtbdd_plant_artifact(
                controller_model,
                controller_source_sha256,
                &mtbdd,
                members,
            )?;
            (
                ControllerProofMtbddPlantPortfolioBackend::ProofMtbdd,
                ControllerMtbddPlantSelectionReason::MtbddAdmitted,
                encode_controller_proof_mtbdd_plant_artifact(&artifact)?,
            )
        }
        Err(error) => {
            let failure = error
                .admission_failure()
                .ok_or_else(|| reject(error.to_string()))?;
            let artifact = produce_controller_direct_plant_artifact(
                controller_model,
                controller_source_sha256,
                members,
            )?;
            (
                ControllerProofMtbddPlantPortfolioBackend::DirectExact,
                portfolio_reason_from_failure(failure),
                encode_controller_direct_plant_artifact(&artifact)?,
            )
        }
    };
    encode_controller_proof_mtbdd_plant_portfolio(&ControllerProofMtbddPlantPortfolioArtifact {
        version: PROOF_MTBDD_PLANT_PORTFOLIO_VERSION,
        backend,
        reason,
        relevant_inputs: relevant_inputs.to_vec(),
        observed_outputs: observed_outputs.to_vec(),
        payload,
    })
}

fn portfolio_boundary_matches_members(
    relevant_inputs: &[usize],
    observed_outputs: &[usize],
    members: &[ControllerPlantArtifactInput<'_>],
) -> bool {
    !members.is_empty()
        && members.iter().all(|member| {
            member.wiring.controller_sensor_inputs == relevant_inputs
                && member.wiring.controller_action_outputs == observed_outputs
        })
}

fn portfolio_members_match(
    claimed: &[ControllerPlantArtifactMember],
    expected: &[ControllerPlantArtifactInput<'_>],
) -> bool {
    claimed.len() == expected.len()
        && claimed.iter().zip(expected).all(|(claimed, expected)| {
            claimed.plant_source_sha256 == expected.plant_source_sha256
                && claimed.wiring == *expected.wiring
                && claimed.initial_controller_state == expected.initial_controller_state
                && claimed.initial_plant_state == expected.initial_plant_state
                && claimed.bad_plant_output == expected.bad_plant_output
                && claimed.horizon == expected.horizon
        })
}

fn bounded_state_count(latches: usize) -> Result<usize, ControllerPlantArtifactError> {
    1usize
        .checked_shl(
            u32::try_from(latches)
                .map_err(|_| reject("controller-plant resource state width exceeds range"))?,
        )
        .ok_or_else(|| reject("controller-plant resource state width exceeds range"))
}

/// Conservatively preflight a proof-carrying MTBDD batch before checking its
/// equivalence proof or replaying controller/plant reachability.
pub fn assess_controller_proof_mtbdd_plant_resources(
    controller_model: &AigerTransition,
    members: &[ControllerPlantArtifactInput<'_>],
    bytes: &[u8],
    envelope: ControllerProofMtbddResourceEnvelope,
) -> Result<ControllerProofMtbddResourceAssessment, ControllerPlantArtifactError> {
    let composition = envelope.composition;
    if bytes.len() > composition.max_artifact_bytes {
        return Err(reject(
            "proof-carrying controller MTBDD resource artifact-byte limit exceeded",
        ));
    }
    if members.is_empty() || members.len() > composition.max_members {
        return Err(reject(
            "proof-carrying controller MTBDD resource member limit exceeded",
        ));
    }
    let outer = decode_controller_proof_mtbdd_plant_artifact(bytes)?;
    if outer.equivalence_proof.len() > envelope.max_equivalence_artifact_bytes {
        return Err(reject(
            "proof-carrying controller MTBDD resource equivalence-artifact limit exceeded",
        ));
    }
    let proof = decode_controller_mtbdd_equivalence_proof(&outer.equivalence_proof)
        .map_err(|error| reject(error.to_string()))?;
    if proof.proof.len() > envelope.max_unsat_proof_bytes {
        return Err(reject(
            "proof-carrying controller MTBDD resource UNSAT-proof limit exceeded",
        ));
    }
    let inner = decode_controller_mtbdd_plant_artifact(&outer.controller_mtbdd_plant)?;
    if members.len() != inner.members.len() {
        return Err(reject(
            "proof-carrying controller MTBDD resource member count mismatch",
        ));
    }
    let controller_states = bounded_state_count(controller_model.latches.len())?;
    let mut maximum_member_horizon = 0usize;
    let mut maximum_product_states = 0usize;
    let mut transition_evaluation_bound = 0usize;
    for (member, claimed) in members.iter().zip(&inner.members) {
        if member.plant_source_sha256 != claimed.plant_source_sha256
            || member.wiring != &claimed.wiring
            || member.initial_controller_state != claimed.initial_controller_state
            || member.initial_plant_state != claimed.initial_plant_state
            || member.bad_plant_output != claimed.bad_plant_output
            || member.horizon != claimed.horizon
        {
            return Err(reject(
                "proof-carrying controller MTBDD resource member mismatch",
            ));
        }
        if member.horizon > composition.max_member_horizon {
            return Err(reject(
                "proof-carrying controller MTBDD resource horizon limit exceeded",
            ));
        }
        maximum_member_horizon = maximum_member_horizon.max(member.horizon);
        let plant_states = bounded_state_count(member.plant.latches.len())?;
        let product_states = controller_states
            .checked_mul(plant_states)
            .ok_or_else(|| reject("proof-carrying product-state bound overflow"))?;
        if product_states > composition.max_product_states_per_member {
            return Err(reject(
                "proof-carrying controller MTBDD resource product-state limit exceeded",
            ));
        }
        maximum_product_states = maximum_product_states.max(product_states);
        let external_inputs = member
            .plant
            .inputs
            .len()
            .checked_sub(member.wiring.plant_action_inputs.len())
            .ok_or_else(|| reject("proof-carrying controller MTBDD resource wiring is invalid"))?;
        let external_patterns = 1usize
            .checked_shl(
                u32::try_from(external_inputs)
                    .map_err(|_| reject("proof-carrying input width exceeds range"))?,
            )
            .ok_or_else(|| reject("proof-carrying input width exceeds range"))?;
        let member_bound = product_states
            .checked_mul(member.horizon.saturating_add(1))
            .and_then(|value| value.checked_mul(external_patterns))
            .ok_or_else(|| reject("proof-carrying transition bound overflow"))?;
        transition_evaluation_bound = transition_evaluation_bound
            .checked_add(member_bound)
            .ok_or_else(|| reject("proof-carrying transition bound overflow"))?;
        if transition_evaluation_bound > composition.max_transition_evaluations {
            return Err(reject(
                "proof-carrying controller MTBDD resource transition limit exceeded",
            ));
        }
    }
    Ok(ControllerProofMtbddResourceAssessment {
        version: CONTROLLER_PROOF_MTBDD_RESOURCE_ENVELOPE_VERSION,
        artifact_bytes: bytes.len(),
        equivalence_artifact_bytes: outer.equivalence_proof.len(),
        unsat_proof_bytes: proof.proof.len(),
        members: members.len(),
        maximum_member_horizon,
        maximum_product_states,
        transition_evaluation_bound,
    })
}

/// Verify a proof-carrying MTBDD batch only after every caller-selected proof
/// and composition limit fits.
pub fn verify_controller_proof_mtbdd_plant_artifact_with_resources(
    controller_model: &AigerTransition,
    controller_source_sha256: [u8; 32],
    members: &[ControllerPlantArtifactInput<'_>],
    bytes: &[u8],
    envelope: ControllerProofMtbddResourceEnvelope,
) -> Result<GovernedControllerProofMtbddPlantSummary, ControllerPlantArtifactError> {
    let resources =
        assess_controller_proof_mtbdd_plant_resources(controller_model, members, bytes, envelope)?;
    let plants = members
        .iter()
        .map(|member| (member.plant, member.plant_source_sha256))
        .collect::<Vec<_>>();
    let verification = verify_controller_proof_mtbdd_plant_artifact(
        controller_model,
        controller_source_sha256,
        &plants,
        bytes,
    )?;
    Ok(GovernedControllerProofMtbddPlantSummary {
        resources,
        verification,
    })
}

pub fn assess_controller_proof_mtbdd_plant_portfolio_resources(
    controller_model: &AigerTransition,
    relevant_inputs: &[usize],
    observed_outputs: &[usize],
    members: &[ControllerPlantArtifactInput<'_>],
    bytes: &[u8],
    envelope: ControllerProofMtbddResourceEnvelope,
) -> Result<ControllerProofMtbddPortfolioResourceAssessment, ControllerPlantArtifactError> {
    let composition = envelope.composition;
    if bytes.len() > composition.max_artifact_bytes {
        return Err(reject(
            "proof-carrying controller MTBDD portfolio resource artifact-byte limit exceeded",
        ));
    }
    if members.is_empty() || members.len() > composition.max_members {
        return Err(reject(
            "proof-carrying controller MTBDD portfolio resource member limit exceeded",
        ));
    }
    let portfolio = decode_controller_proof_mtbdd_plant_portfolio(bytes)?;
    if portfolio.relevant_inputs != relevant_inputs
        || portfolio.observed_outputs != observed_outputs
    {
        return Err(reject(
            "proof-carrying controller MTBDD portfolio resource boundary mismatch",
        ));
    }
    if !portfolio_boundary_matches_members(relevant_inputs, observed_outputs, members) {
        return Err(reject(
            "proof-carrying controller MTBDD portfolio resource member boundary mismatch",
        ));
    }
    match portfolio.backend {
        ControllerProofMtbddPlantPortfolioBackend::ProofMtbdd => {
            let assessment = assess_controller_proof_mtbdd_plant_resources(
                controller_model,
                members,
                &portfolio.payload,
                envelope,
            )?;
            Ok(ControllerProofMtbddPortfolioResourceAssessment {
                version: CONTROLLER_PROOF_MTBDD_RESOURCE_ENVELOPE_VERSION,
                backend: portfolio.backend,
                artifact_bytes: bytes.len(),
                equivalence_artifact_bytes: assessment.equivalence_artifact_bytes,
                unsat_proof_bytes: assessment.unsat_proof_bytes,
                members: assessment.members,
                maximum_member_horizon: assessment.maximum_member_horizon,
                maximum_product_states: assessment.maximum_product_states,
                transition_evaluation_bound: assessment.transition_evaluation_bound,
            })
        }
        ControllerProofMtbddPlantPortfolioBackend::DirectExact => {
            let artifact = decode_controller_direct_plant_artifact(&portfolio.payload)?;
            if !portfolio_members_match(&artifact.members, members) {
                return Err(reject(
                    "proof-carrying controller MTBDD portfolio resource member mismatch",
                ));
            }
            let controller_states = bounded_state_count(controller_model.latches.len())?;
            let omitted_controller_inputs = controller_model
                .inputs
                .len()
                .checked_sub(relevant_inputs.len())
                .ok_or_else(|| reject("proof-carrying portfolio resource boundary is invalid"))?;
            let direct_multiplier = 1usize
                .checked_shl(
                    u32::try_from(omitted_controller_inputs)
                        .map_err(|_| reject("proof-carrying input width exceeds range"))?,
                )
                .ok_or_else(|| reject("proof-carrying input width exceeds range"))?;
            let mut maximum_member_horizon = 0usize;
            let mut maximum_product_states = 0usize;
            let mut transition_evaluation_bound = 0usize;
            for member in members {
                if member.horizon > composition.max_member_horizon {
                    return Err(reject(
                        "proof-carrying controller MTBDD portfolio resource horizon limit exceeded",
                    ));
                }
                maximum_member_horizon = maximum_member_horizon.max(member.horizon);
                let plant_states = bounded_state_count(member.plant.latches.len())?;
                let product_states = controller_states
                    .checked_mul(plant_states)
                    .ok_or_else(|| reject("proof-carrying product-state bound overflow"))?;
                if product_states > composition.max_product_states_per_member {
                    return Err(reject(
                        "proof-carrying controller MTBDD portfolio resource product-state limit exceeded",
                    ));
                }
                maximum_product_states = maximum_product_states.max(product_states);
                let external_inputs = member
                    .plant
                    .inputs
                    .len()
                    .checked_sub(member.wiring.plant_action_inputs.len())
                    .ok_or_else(|| reject("proof-carrying portfolio resource wiring is invalid"))?;
                let external_patterns = 1usize
                    .checked_shl(
                        u32::try_from(external_inputs)
                            .map_err(|_| reject("proof-carrying input width exceeds range"))?,
                    )
                    .ok_or_else(|| reject("proof-carrying input width exceeds range"))?;
                let member_bound = product_states
                    .checked_mul(member.horizon.saturating_add(1))
                    .and_then(|value| value.checked_mul(external_patterns))
                    .and_then(|value| value.checked_mul(direct_multiplier))
                    .ok_or_else(|| reject("proof-carrying transition bound overflow"))?;
                transition_evaluation_bound = transition_evaluation_bound
                    .checked_add(member_bound)
                    .ok_or_else(|| reject("proof-carrying transition bound overflow"))?;
                if transition_evaluation_bound > composition.max_transition_evaluations {
                    return Err(reject(
                        "proof-carrying controller MTBDD portfolio resource transition limit exceeded",
                    ));
                }
            }
            Ok(ControllerProofMtbddPortfolioResourceAssessment {
                version: CONTROLLER_PROOF_MTBDD_RESOURCE_ENVELOPE_VERSION,
                backend: portfolio.backend,
                artifact_bytes: bytes.len(),
                equivalence_artifact_bytes: 0,
                unsat_proof_bytes: 0,
                members: members.len(),
                maximum_member_horizon,
                maximum_product_states,
                transition_evaluation_bound,
            })
        }
    }
}

#[allow(clippy::too_many_arguments)]
pub fn verify_controller_proof_mtbdd_plant_portfolio_with_resources(
    controller_model: &AigerTransition,
    controller_source_sha256: [u8; 32],
    relevant_inputs: &[usize],
    observed_outputs: &[usize],
    members: &[ControllerPlantArtifactInput<'_>],
    bytes: &[u8],
    envelope: ControllerProofMtbddResourceEnvelope,
) -> Result<GovernedControllerProofMtbddPortfolioSummary, ControllerPlantArtifactError> {
    let resources = assess_controller_proof_mtbdd_plant_portfolio_resources(
        controller_model,
        relevant_inputs,
        observed_outputs,
        members,
        bytes,
        envelope,
    )?;
    let verification = verify_controller_proof_mtbdd_plant_portfolio(
        controller_model,
        controller_source_sha256,
        relevant_inputs,
        observed_outputs,
        members,
        bytes,
    )?;
    Ok(GovernedControllerProofMtbddPortfolioSummary {
        resources,
        verification,
    })
}

/// Conservatively preflight one portfolio verification against caller-selected
/// resource bounds. This validates the canonical outer artifact but performs no
/// controller/plant reachability replay.
pub fn assess_controller_mtbdd_plant_portfolio_resources(
    controller_model: &AigerTransition,
    members: &[ControllerPlantArtifactInput<'_>],
    bytes: &[u8],
    envelope: ControllerPlantResourceEnvelope,
) -> Result<ControllerPlantResourceAssessment, ControllerPlantArtifactError> {
    if bytes.len() > envelope.max_artifact_bytes {
        return Err(reject(
            "controller-plant resource envelope artifact-byte limit exceeded",
        ));
    }
    if members.is_empty() || members.len() > envelope.max_members {
        return Err(reject(
            "controller-plant resource envelope member limit exceeded",
        ));
    }
    let artifact = decode_controller_mtbdd_plant_portfolio(bytes)?;
    let controller_states = bounded_state_count(controller_model.latches.len())?;
    let omitted_controller_inputs = controller_model
        .inputs
        .len()
        .checked_sub(artifact.relevant_inputs.len())
        .ok_or_else(|| reject("controller-plant resource boundary is invalid"))?;
    let direct_multiplier = match artifact.backend {
        ControllerMtbddPlantPortfolioBackend::Mtbdd => 1,
        ControllerMtbddPlantPortfolioBackend::DirectExact => 1usize
            .checked_shl(
                u32::try_from(omitted_controller_inputs)
                    .map_err(|_| reject("controller-plant resource input width exceeds range"))?,
            )
            .ok_or_else(|| reject("controller-plant resource input width exceeds range"))?,
    };
    let mut maximum_member_horizon = 0usize;
    let mut maximum_product_states = 0usize;
    let mut transition_evaluation_bound = 0usize;
    for member in members {
        if member.horizon > envelope.max_member_horizon {
            return Err(reject(
                "controller-plant resource envelope horizon limit exceeded",
            ));
        }
        maximum_member_horizon = maximum_member_horizon.max(member.horizon);
        let plant_states = bounded_state_count(member.plant.latches.len())?;
        let product_states = controller_states
            .checked_mul(plant_states)
            .ok_or_else(|| reject("controller-plant resource product-state bound overflow"))?;
        if product_states > envelope.max_product_states_per_member {
            return Err(reject(
                "controller-plant resource envelope product-state limit exceeded",
            ));
        }
        maximum_product_states = maximum_product_states.max(product_states);
        let external_inputs = member
            .plant
            .inputs
            .len()
            .checked_sub(member.wiring.plant_action_inputs.len())
            .ok_or_else(|| reject("controller-plant resource wiring is invalid"))?;
        let external_patterns = 1usize
            .checked_shl(
                u32::try_from(external_inputs)
                    .map_err(|_| reject("controller-plant resource input width exceeds range"))?,
            )
            .ok_or_else(|| reject("controller-plant resource input width exceeds range"))?;
        let member_bound = product_states
            .checked_mul(member.horizon.saturating_add(1))
            .and_then(|value| value.checked_mul(external_patterns))
            .and_then(|value| value.checked_mul(direct_multiplier))
            .ok_or_else(|| reject("controller-plant resource transition bound overflow"))?;
        transition_evaluation_bound = transition_evaluation_bound
            .checked_add(member_bound)
            .ok_or_else(|| reject("controller-plant resource transition bound overflow"))?;
        if transition_evaluation_bound > envelope.max_transition_evaluations {
            return Err(reject(
                "controller-plant resource envelope transition limit exceeded",
            ));
        }
    }
    Ok(ControllerPlantResourceAssessment {
        version: CONTROLLER_PLANT_RESOURCE_ENVELOPE_VERSION,
        backend: artifact.backend,
        artifact_bytes: bytes.len(),
        members: members.len(),
        maximum_member_horizon,
        maximum_product_states,
        transition_evaluation_bound,
    })
}

/// Verify through the existing exact portfolio only after its conservative
/// workload fits the supplied resource envelope.
#[allow(clippy::too_many_arguments)]
pub fn verify_controller_mtbdd_plant_portfolio_with_resources(
    controller_model: &AigerTransition,
    controller_source_sha256: [u8; 32],
    relevant_inputs: &[usize],
    observed_outputs: &[usize],
    members: &[ControllerPlantArtifactInput<'_>],
    bytes: &[u8],
    envelope: ControllerPlantResourceEnvelope,
) -> Result<GovernedControllerMtbddPlantPortfolioSummary, ControllerPlantArtifactError> {
    let resources = assess_controller_mtbdd_plant_portfolio_resources(
        controller_model,
        members,
        bytes,
        envelope,
    )?;
    let verification = verify_controller_mtbdd_plant_portfolio(
        controller_model,
        controller_source_sha256,
        relevant_inputs,
        observed_outputs,
        members,
        bytes,
    )?;
    Ok(GovernedControllerMtbddPlantPortfolioSummary {
        resources,
        verification,
    })
}

pub fn verify_controller_mtbdd_plant_portfolio(
    controller_model: &AigerTransition,
    controller_source_sha256: [u8; 32],
    relevant_inputs: &[usize],
    observed_outputs: &[usize],
    members: &[ControllerPlantArtifactInput<'_>],
    bytes: &[u8],
) -> Result<ControllerMtbddPlantPortfolioSummary, ControllerPlantArtifactError> {
    let artifact = decode_controller_mtbdd_plant_portfolio(bytes)?;
    if artifact.relevant_inputs != relevant_inputs || artifact.observed_outputs != observed_outputs
    {
        return Err(reject("controller MTBDD portfolio boundary mismatch"));
    }
    if !portfolio_boundary_matches_members(relevant_inputs, observed_outputs, members) {
        return Err(reject(
            "controller MTBDD portfolio member boundary mismatch",
        ));
    }
    let plants = members
        .iter()
        .map(|member| (member.plant, member.plant_source_sha256))
        .collect::<Vec<_>>();
    let (results, safe, unsafe_count, reachable_product_states, explored_transitions) =
        match artifact.backend {
            ControllerMtbddPlantPortfolioBackend::Mtbdd => {
                let decoded = decode_controller_mtbdd_plant_artifact(&artifact.payload)?;
                if !portfolio_members_match(&decoded.members, members) {
                    return Err(reject("controller MTBDD portfolio member mismatch"));
                }
                let summary = verify_controller_mtbdd_plant_artifact(
                    controller_model,
                    controller_source_sha256,
                    &plants,
                    &artifact.payload,
                )?;
                (
                    summary.members,
                    summary.safe,
                    summary.unsafe_count,
                    summary.reachable_product_states,
                    summary.explored_transitions,
                )
            }
            ControllerMtbddPlantPortfolioBackend::DirectExact => {
                let expected_reason = match produce_controller_mtbdd(
                    controller_model,
                    controller_source_sha256,
                    relevant_inputs,
                    observed_outputs,
                ) {
                    Ok(_) => return Err(reject("controller MTBDD portfolio downgrade detected")),
                    Err(error) => error
                        .admission_failure()
                        .map(portfolio_reason_from_failure)
                        .ok_or_else(|| reject(error.to_string()))?,
                };
                if artifact.reason != expected_reason {
                    return Err(reject("controller MTBDD portfolio reason mismatch"));
                }
                let decoded = decode_controller_direct_plant_artifact(&artifact.payload)?;
                if !portfolio_members_match(&decoded.members, members) {
                    return Err(reject("controller MTBDD portfolio member mismatch"));
                }
                let summary = verify_controller_direct_plant_artifact(
                    controller_model,
                    controller_source_sha256,
                    &plants,
                    &artifact.payload,
                )?;
                (
                    summary.members,
                    summary.safe,
                    summary.unsafe_count,
                    summary.reachable_product_states,
                    summary.explored_transitions,
                )
            }
        };
    Ok(ControllerMtbddPlantPortfolioSummary {
        backend: artifact.backend,
        reason: artifact.reason,
        members: results,
        safe,
        unsafe_count,
        reachable_product_states,
        explored_transitions,
    })
}

pub fn verify_controller_proof_mtbdd_plant_portfolio(
    controller_model: &AigerTransition,
    controller_source_sha256: [u8; 32],
    relevant_inputs: &[usize],
    observed_outputs: &[usize],
    members: &[ControllerPlantArtifactInput<'_>],
    bytes: &[u8],
) -> Result<ControllerProofMtbddPlantPortfolioSummary, ControllerPlantArtifactError> {
    let artifact = decode_controller_proof_mtbdd_plant_portfolio(bytes)?;
    if artifact.relevant_inputs != relevant_inputs || artifact.observed_outputs != observed_outputs
    {
        return Err(reject(
            "proof-carrying controller MTBDD portfolio boundary mismatch",
        ));
    }
    if !portfolio_boundary_matches_members(relevant_inputs, observed_outputs, members) {
        return Err(reject(
            "proof-carrying controller MTBDD portfolio member boundary mismatch",
        ));
    }
    let plants = members
        .iter()
        .map(|member| (member.plant, member.plant_source_sha256))
        .collect::<Vec<_>>();
    let (results, safe, unsafe_count, reachable, explored, assignments_checked) =
        match artifact.backend {
            ControllerProofMtbddPlantPortfolioBackend::ProofMtbdd => {
                let outer = decode_controller_proof_mtbdd_plant_artifact(&artifact.payload)?;
                let inner = decode_controller_mtbdd_plant_artifact(&outer.controller_mtbdd_plant)?;
                if !portfolio_members_match(&inner.members, members) {
                    return Err(reject(
                        "proof-carrying controller MTBDD portfolio member mismatch",
                    ));
                }
                let summary = verify_controller_proof_mtbdd_plant_artifact(
                    controller_model,
                    controller_source_sha256,
                    &plants,
                    &artifact.payload,
                )?;
                (
                    summary.members,
                    summary.safe,
                    summary.unsafe_count,
                    summary.reachable_product_states,
                    summary.explored_transitions,
                    summary.assignments_checked,
                )
            }
            ControllerProofMtbddPlantPortfolioBackend::DirectExact => {
                let expected_reason = match produce_controller_mtbdd(
                    controller_model,
                    controller_source_sha256,
                    relevant_inputs,
                    observed_outputs,
                ) {
                    Ok(_) => {
                        return Err(reject(
                            "proof-carrying controller MTBDD portfolio downgrade detected",
                        ));
                    }
                    Err(error) => error
                        .admission_failure()
                        .map(portfolio_reason_from_failure)
                        .ok_or_else(|| reject(error.to_string()))?,
                };
                if artifact.reason != expected_reason {
                    return Err(reject(
                        "proof-carrying controller MTBDD portfolio reason mismatch",
                    ));
                }
                let decoded = decode_controller_direct_plant_artifact(&artifact.payload)?;
                if !portfolio_members_match(&decoded.members, members) {
                    return Err(reject(
                        "proof-carrying controller MTBDD portfolio member mismatch",
                    ));
                }
                let summary = verify_controller_direct_plant_artifact(
                    controller_model,
                    controller_source_sha256,
                    &plants,
                    &artifact.payload,
                )?;
                (
                    summary.members,
                    summary.safe,
                    summary.unsafe_count,
                    summary.reachable_product_states,
                    summary.explored_transitions,
                    0,
                )
            }
        };
    Ok(ControllerProofMtbddPlantPortfolioSummary {
        backend: artifact.backend,
        reason: artifact.reason,
        members: results,
        safe,
        unsafe_count,
        reachable_product_states: reachable,
        explored_transitions: explored,
        assignments_checked,
    })
}