feat: add verification tool

Cargo.toml

@@ -3,7 +3,7 @@ lto = "thin"
 
 [workspace]
 resolver = "2"
-members = ["impl/rs"]
+members = ["impl/rs", "tools/verifier"]
 
 [workspace.package]
 rust-version = "1.85"

impl/rs/src/reader.rs

@@ -12,11 +12,12 @@ pub mod value;
 
 pub mod optype;
 
-pub use function::{Function, FunctionId};
+pub use function::{Function, FunctionDeclaration, FunctionDefinition, FunctionId};
 pub use metadata::{HasMetadata, Metadata};
 pub use module::Module;
 pub use op::Operation;
 pub use region::Region;
+pub use value::{FunctionIOValue, ValueId, ValueTable, WireValue};
 
 use derive_more::derive::{Display, Error, From};
 

tools/verifier/Cargo.toml

@@ -0,0 +1,14 @@
+[package]
+name = "verifier"
+version = "0.1.0"
+rust-version.workspace = true
+edition.workspace = true
+homepage.workspace = true
+repository.workspace = true
+license.workspace = true
+
+[dependencies]
+jeff = { package = "jeff-format", path = "../../impl/rs" }
+
+[lints]
+workspace = true

tools/verifier/src/analysis.rs

@@ -0,0 +1,83 @@
+//! Information collection over jeff regions.
+//!
+//! This module traverses a function's dataflow graph to gather statistics
+//! used by the verification passes.
+
+use jeff::reader::optype::{ControlFlowOp, OpType};
+use jeff::reader::{ReadError, Region};
+
+/// Producer and consumer counts for a single value.
+#[derive(Debug, Default, Clone, PartialEq, Eq)]
+pub struct ValueStats {
+    /// Number of operations that produce this value.
+    pub producers: u32,
+    /// Number of operations that consume this value.
+    pub consumers: u32,
+}
+
+/// Walk `region` recursively and accumulate producer/consumer counts into `stats`.
+///
+/// The slice must be pre-allocated with one entry per value in the function's value table.
+pub fn collect_value_stats(region: Region<'_>, stats: &mut [ValueStats]) -> Result<(), ReadError> {
+    for value in region.sources() {
+        stats[value?.id() as usize].producers += 1;
+    }
+
+    for value in region.targets() {
+        stats[value?.id() as usize].consumers += 1;
+    }
+
+    for op in region.operations() {
+        for value in op.inputs() {
+            stats[value?.id() as usize].consumers += 1;
+        }
+
+        for value in op.outputs() {
+            stats[value?.id() as usize].producers += 1;
+        }
+
+        if let OpType::ControlFlowOp(cf_op) = op.op_type() {
+            collect_cf_value_stats(cf_op.as_ref(), stats)?;
+        }
+    }
+
+    Ok(())
+}
+
+fn collect_cf_value_stats(
+    cf_op: &ControlFlowOp<'_>,
+    stats: &mut [ValueStats],
+) -> Result<(), ReadError> {
+    match cf_op {
+        ControlFlowOp::For { region } => {
+            collect_value_stats(*region, stats)?;
+        }
+        ControlFlowOp::While { condition, body } => {
+            collect_value_stats(*condition, stats)?;
+            collect_value_stats(*body, stats)?;
+        }
+        ControlFlowOp::DoWhile { body, condition } => {
+            collect_value_stats(*body, stats)?;
+            collect_value_stats(*condition, stats)?;
+        }
+        ControlFlowOp::Switch(switch_op) => {
+            for branch in switch_op.branches() {
+                collect_value_stats(branch, stats)?;
+            }
+            if let Some(default) = switch_op.default_branch() {
+                collect_value_stats(default, stats)?;
+            }
+        }
+    }
+    Ok(())
+}
+
+/// Build a [`Vec<ValueStats>`] with one entry per value in the function's value table.
+pub fn build_value_stats(
+    region: Region<'_>,
+    num_values: usize,
+) -> Result<Vec<ValueStats>, ReadError> {
+    let mut stats = vec![ValueStats::default(); num_values];
+    collect_value_stats(region, &mut stats)?;
+    Ok(stats)
+}

tools/verifier/src/errors.rs

@@ -0,0 +1,155 @@
+use std::fmt;
+
+/// An error detected during verification of a jeff module.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum VerificationError {
+    /// The module version is unset (0.0.0).
+    MissingVersion,
+
+    /// The module version is set but does not match the version supported by this verifier.
+    IncompatibleVersion,
+
+    /// The module's entrypoint does not refer to a function definition.
+    InvalidEntrypoint,
+
+    /// An operation references a value index that is out of bounds in the function's value table.
+    ValueOutOfBounds {
+        /// The out-of-bounds value index.
+        value_id: u32,
+        /// The number of values in the table.
+        value_count: usize,
+    },
+
+    /// An operation consumes a value before any operation that produces it.
+    UsedBeforeDefined {
+        /// The value used out of order.
+        value_id: u32,
+    },
+
+    /// A value is produced by more than one operation.
+    /// In jeff's SSA value semantics, every value must have exactly one producer.
+    ValueProducedMultipleTimes {
+        /// The value produced multiple times.
+        value_id: u32,
+        /// The number of producing operations.
+        producers: u32,
+    },
+
+    /// A linear value (qubit or qureg) is consumed by more than one operation.
+    LinearValueConsumedMultipleTimes {
+        /// The value consumed multiple times.
+        value_id: u32,
+        /// The number of consuming operations.
+        consumers: u32,
+    },
+
+    /// A linear value (qubit or qureg) is produced but never consumed.
+    LinearValueNeverConsumed {
+        /// The value that is never consumed.
+        value_id: u32,
+    },
+
+    /// The input and output types of an int or float operation are not all the same bitwidth or precision.
+    TypeMismatch {
+        /// The name of the operation with mismatched types.
+        operation: &'static str,
+    },
+
+    /// An input value has a type that is not valid for the operation.
+    InvalidInputType {
+        /// The name of the operation with the invalid input.
+        operation: &'static str,
+    },
+
+    /// An output value has a type that is not valid for the operation.
+    InvalidOutputType {
+        /// The name of the operation with the invalid output.
+        operation: &'static str,
+    },
+
+    /// A gate operation has the wrong number of inputs or outputs for its declared arity.
+    WrongArity {
+        /// The name of the operation with the wrong arity.
+        operation: &'static str,
+    },
+
+    /// An operation inside a nested region directly references a value from an outer scope
+    /// without the value being explicitly passed in via the region's sources.
+    IsolationViolation {
+        /// The outer-scope value referenced directly.
+        value_id: u32,
+    },
+}
+
+impl fmt::Display for VerificationError {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            Self::MissingVersion => {
+                write!(f, "module version is unset (0.0.0)")
+            }
+            Self::IncompatibleVersion => {
+                write!(f, "module version is incompatible with the jeff program")
+            }
+            Self::InvalidEntrypoint => {
+                write!(
+                    f,
+                    "module entrypoint does not refer to a function definition"
+                )
+            }
+            Self::ValueOutOfBounds {
+                value_id,
+                value_count,
+            } => {
+                write!(
+                    f,
+                    "value {value_id} is out of bounds (function has {value_count} values)"
+                )
+            }
+            Self::UsedBeforeDefined { value_id } => {
+                write!(f, "value {value_id} is used before it is defined")
+            }
+            Self::ValueProducedMultipleTimes {
+                value_id,
+                producers,
+            } => {
+                write!(
+                    f,
+                    "value {value_id} is produced {producers} times (must be exactly once)"
+                )
+            }
+            Self::LinearValueConsumedMultipleTimes {
+                value_id,
+                consumers,
+            } => {
+                write!(
+                    f,
+                    "linear value {value_id} is consumed {consumers} times (must be exactly once)"
+                )
+            }
+            Self::LinearValueNeverConsumed { value_id } => {
+                write!(f, "linear value {value_id} is produced but never consumed")
+            }
+            Self::TypeMismatch { operation } => {
+                write!(
+                    f,
+                    "'{operation}' has inputs and outputs with mismatched types"
+                )
+            }
+            Self::InvalidInputType { operation } => {
+                write!(f, "'{operation}' has an input of an unexpected type")
+            }
+            Self::InvalidOutputType { operation } => {
+                write!(f, "'{operation}' has an output of an unexpected type")
+            }
+            Self::WrongArity { operation } => {
+                write!(f, "'{operation}' has the wrong number of inputs or outputs for its declared arity")
+            }
+            Self::IsolationViolation { value_id } => {
+                write!(
+                    f,
+                    "value {value_id} from an outer scope is used inside a nested region without being passed in via sources"
+                )
+            }
+        }
+    }
+}

tools/verifier/src/lib.rs

@@ -0,0 +1,54 @@
+//! Verifier for jeff quantum program modules.
+//!
+//! The main entry point is [`verify_module`], which checks a decoded
+//! [`jeff::reader::Module`] against all verification passes and returns
+//! a list of [`VerificationError`]s.
+
+pub mod analysis;
+/// Verification error types and their display messages.
+pub mod errors;
+pub mod passes;
+
+use jeff::reader::{Function, FunctionDefinition, Module};
+
+pub use errors::VerificationError;
+
+use passes::isolation::verify_isolation;
+use passes::module_attributes::verify_module_attributes;
+use passes::type_checks::verify_operation_types;
+use passes::value_checks::verify_value_checks;
+
+/// Verify a decoded jeff module and return all detected errors.
+///
+/// Returns an empty [`Vec`] if the module is valid.
+/// Returns immediately with a single error if the module version is missing or incompatible,
+/// since subsequent passes would produce meaningless results against an unknown schema version.
+pub fn verify_module(module: Module<'_>) -> Vec<VerificationError> {
+    let v = module.version();
+    let s = &jeff::SCHEMA_VERSION;
+
+    if v.major == 0 && v.minor == 0 && v.patch == 0 {
+        return vec![VerificationError::MissingVersion];
+    }
+    if v.major != s.major || v.minor != s.minor || v.patch != s.patch {
+        return vec![VerificationError::IncompatibleVersion];
+    }
+
+    let mut errors = Vec::new();
+
+    verify_module_attributes(module, &mut errors);
+
+    for function in module.functions() {
+        if let Function::Definition(def) = function {
+            verify_definition(def, &mut errors);
+        }
+    }
+
+    errors
+}
+
+fn verify_definition(def: FunctionDefinition<'_>, errors: &mut Vec<VerificationError>) {
+    verify_value_checks(def, errors);
+    verify_operation_types(def.body(), errors);
+    verify_isolation(def, errors);
+}