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"

examples/entangled_calls/entangled_calls.txt

@@ -10,7 +10,7 @@
                     sources = [],
                     targets = [49],
                     operations = [
-                        (outputs = [0], instruction = (int = (const8 = 1))),
+                        (outputs = [0], instruction = (int = (const1 = true))),
                         (outputs = [1], instruction = (qubit = (alloc = void))),
                         (outputs = [2], instruction = (qubit = (alloc = void))),
                         (outputs = [3], instruction = (qubit = (alloc = void))),
@@ -21,7 +21,7 @@
                         (inputs = [8, 3], outputs = [9, 10], instruction = (qubit = (gate = (custom = (name = 5, numQubits = 1), controlQubits = 1)))),
                         (inputs = [10, 4], outputs = [11, 12], instruction = (qubit = (gate = (custom = (name = 5, numQubits = 1), controlQubits = 1)))),
                         (inputs = [12, 5], outputs = [13, 14], instruction = (qubit = (gate = (custom = (name = 5, numQubits = 1), controlQubits = 1)))),
-                        (outputs = [15], instruction = (intArray = (const8 = [0, 0, 0, 0, 0]))),
+                        (outputs = [15], instruction = (intArray = (const1 = [false, false, false, false, false]))),
                         (inputs = [7], outputs = [16], instruction = (qubit = (measure = void))),
                         (outputs = [17], instruction = (int = (const32 = 0))),
                         (inputs = [15, 17, 16], outputs = [18], instruction = (intArray = (setIndex = void))),
@@ -59,23 +59,23 @@
                     ]
                 ),
                 values = [
-                    (type = (int = 8)), (type = (qubit = void)), (type = (qubit = void)),
+                    (type = (int = 1)), (type = (qubit = void)), (type = (qubit = void)),
                     (type = (qubit = void)), (type = (qubit = void)), (type = (qubit = void)),
                     (type = (qubit = void)), (type = (qubit = void)), (type = (qubit = void)),
                     (type = (qubit = void)), (type = (qubit = void)), (type = (qubit = void)),
                     (type = (qubit = void)), (type = (qubit = void)), (type = (qubit = void)),
-                    (type = (intArray = (bitwidth = 8, length = (static = 5)))), (type = (int = 1)), (type = (int = 32)),
-                    (type = (intArray = (bitwidth = 8, length = (static = 5)))), (type = (int = 1)), (type = (int = 32)),
-                    (type = (intArray = (bitwidth = 8, length = (static = 5)))), (type = (int = 1)), (type = (int = 32)),
-                    (type = (intArray = (bitwidth = 8, length = (static = 5)))), (type = (int = 1)), (type = (int = 32)),
-                    (type = (intArray = (bitwidth = 8, length = (static = 5)))), (type = (int = 1)), (type = (int = 32)),
-                    (type = (intArray = (bitwidth = 8, length = (static = 5)))), (type = (int = 32)), (type = (int = 8)),
-                    (type = (int = 8)), (type = (int = 32)), (type = (int = 8)),
-                    (type = (int = 8)), (type = (int = 8)), (type = (int = 32)),
-                    (type = (int = 8)), (type = (int = 8)), (type = (int = 8)),
-                    (type = (int = 32)), (type = (int = 8)), (type = (int = 8)),
-                    (type = (int = 8)), (type = (int = 32)), (type = (int = 8)),
-                    (type = (int = 8)), (type = (int = 8))
+                    (type = (intArray = (bitwidth = 1, length = (static = 5)))), (type = (int = 1)), (type = (int = 32)),
+                    (type = (intArray = (bitwidth = 1, length = (static = 5)))), (type = (int = 1)), (type = (int = 32)),
+                    (type = (intArray = (bitwidth = 1, length = (static = 5)))), (type = (int = 1)), (type = (int = 32)),
+                    (type = (intArray = (bitwidth = 1, length = (static = 5)))), (type = (int = 1)), (type = (int = 32)),
+                    (type = (intArray = (bitwidth = 1, length = (static = 5)))), (type = (int = 1)), (type = (int = 32)),
+                    (type = (intArray = (bitwidth = 1, length = (static = 5)))), (type = (int = 32)), (type = (int = 1)),
+                    (type = (int = 1)), (type = (int = 32)), (type = (int = 1)),
+                    (type = (int = 1)), (type = (int = 1)), (type = (int = 32)),
+                    (type = (int = 1)), (type = (int = 1)), (type = (int = 1)),
+                    (type = (int = 32)), (type = (int = 1)), (type = (int = 1)),
+                    (type = (int = 1)), (type = (int = 32)), (type = (int = 1)),
+                    (type = (int = 1)), (type = (int = 1))
                 ]
             ),
         ),
@@ -90,7 +90,7 @@
                     ]
                 ),
                 values = [
-                    (type = (int = 8))
+                    (type = (int = 1))
                 ]
             ),
         ),
@@ -118,7 +118,7 @@
                     operations = []
                 ),
                 values = [
-                    (type = (int = 8))
+                    (type = (int = 1))
                 ]
             ),
         ),

examples/entangled_qs/entangled_qs.txt

@@ -18,7 +18,7 @@
                         (inputs = [7, 2], outputs = [8, 9], instruction = (qubit = (gate = (custom = (name = 2, numQubits = 1), controlQubits = 1)))),
                         (inputs = [9, 3], outputs = [10, 11], instruction = (qubit = (gate = (custom = (name = 2, numQubits = 1), controlQubits = 1)))),
                         (inputs = [11, 4], outputs = [12, 13], instruction = (qubit = (gate = (custom = (name = 2, numQubits = 1), controlQubits = 1)))),
-                        (outputs = [14], instruction = (intArray = (const8 = [0, 0, 0, 0, 0]))),
+                        (outputs = [14], instruction = (intArray = (const1 = [false, false, false, false, false]))),
                         (inputs = [6], outputs = [15], instruction = (qubit = (measure = void))),
                         (outputs = [16], instruction = (int = (const32 = 0))),
                         (inputs = [14, 16, 15], outputs = [17], instruction = (intArray = (setIndex = void))),
@@ -41,12 +41,12 @@
                     (type = (qubit = void)), (type = (qubit = void)), (type = (qubit = void)),
                     (type = (qubit = void)), (type = (qubit = void)), (type = (qubit = void)),
                     (type = (qubit = void)), (type = (qubit = void)), (type = (qubit = void)),
-                    (type = (qubit = void)), (type = (qubit = void)), (type = (intArray = (bitwidth = 8, length = (static = 5)))),
-                    (type = (int = 1)), (type = (int = 32)), (type = (intArray = (bitwidth = 8, length = (static = 5)))),
-                    (type = (int = 1)), (type = (int = 32)), (type = (intArray = (bitwidth = 8, length = (static = 5)))),
-                    (type = (int = 1)), (type = (int = 32)), (type = (intArray = (bitwidth = 8, length = (static = 5)))),
-                    (type = (int = 1)), (type = (int = 32)), (type = (intArray = (bitwidth = 8, length = (static = 5)))),
-                    (type = (int = 1)), (type = (int = 32)), (type = (intArray = (bitwidth = 8, length = (static = 5))))
+                    (type = (qubit = void)), (type = (qubit = void)), (type = (intArray = (bitwidth = 1, length = (static = 5)))),
+                    (type = (int = 1)), (type = (int = 32)), (type = (intArray = (bitwidth = 1, length = (static = 5)))),
+                    (type = (int = 1)), (type = (int = 32)), (type = (intArray = (bitwidth = 1, length = (static = 5)))),
+                    (type = (int = 1)), (type = (int = 32)), (type = (intArray = (bitwidth = 1, length = (static = 5)))),
+                    (type = (int = 1)), (type = (int = 32)), (type = (intArray = (bitwidth = 1, length = (static = 5)))),
+                    (type = (int = 1)), (type = (int = 32)), (type = (intArray = (bitwidth = 1, length = (static = 5))))
                 ]
             ),
         )

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,
+    },
+
+    /// An 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"
+                )
+            }
+        }
+    }
+}