From 7352294873e2c94f8ed8341bdd82719a4fa068a5 Mon Sep 17 00:00:00 2001 From: orisus42 Date: Wed, 10 Jun 2026 12:58:44 -0400 Subject: [PATCH 1/5] feat: add verification tool --- Cargo.lock | 7 + Cargo.toml | 2 +- impl/rs/src/reader.rs | 3 +- tools/verifier/Cargo.toml | 14 + tools/verifier/src/analysis.rs | 83 ++ tools/verifier/src/errors.rs | 148 +++ tools/verifier/src/lib.rs | 42 + tools/verifier/src/passes/isolation.rs | 84 ++ tools/verifier/src/passes/mod.rs | 6 + .../verifier/src/passes/module_attributes.rs | 20 + tools/verifier/src/passes/type_checks.rs | 579 +++++++++ tools/verifier/src/passes/value_checks.rs | 127 ++ tools/verifier/tests/.gitignore | 15 + tools/verifier/tests/encode_test_cases.sh | 35 + tools/verifier/tests/examples.rs | 55 + tools/verifier/tests/generate_test_cases.py | 1152 +++++++++++++++++ .../encode/bounds/nested_source_oob.txt | 32 + .../encode/bounds/nested_target_oob.txt | 32 + .../negative/encode/bounds/op_input_oob.txt | 23 + .../negative/encode/bounds/op_output_oob.txt | 19 + .../encode/bounds/region_source_oob.txt | 20 + .../encode/bounds/region_target_oob.txt | 20 + .../module/entrypoint_is_declaration.txt | 12 + .../encode/types/alloc_unexpected_input.txt | 23 + .../encode/types/free_unexpected_output.txt | 23 + .../encode/types/gate_missing_param_input.txt | 29 + .../types/gate_too_few_qubit_inputs.txt | 30 + .../encode/types/gate_wrong_output_count.txt | 33 + .../encode/types/qureg_alloc_bad_input.txt | 23 + .../encode/types/qureg_alloc_bad_output.txt | 23 + .../qureg_extract_index_bad_idx_input.txt | 32 + .../qureg_extract_index_bad_qubit_output.txt | 32 + .../qureg_extract_index_bad_reg_input.txt | 28 + .../encode/types/qureg_free_bad_input.txt | 22 + .../qureg_insert_index_bad_qubit_input.txt | 35 + .../encode/types/qureg_join_bad_input.txt | 31 + .../encode/types/qureg_length_bad_output.txt | 28 + tools/verifier/tests/negative_attrs.rs | 50 + tools/verifier/tests/negative_bounds.rs | 77 ++ tools/verifier/tests/negative_linearity.rs | 54 + tools/verifier/tests/negative_ordering.rs | 60 + tools/verifier/tests/negative_scoping.rs | 60 + tools/verifier/tests/negative_types.rs | 213 +++ tools/verifier/tests/positive.rs | 45 + 44 files changed, 3479 insertions(+), 2 deletions(-) create mode 100644 tools/verifier/Cargo.toml create mode 100644 tools/verifier/src/analysis.rs create mode 100644 tools/verifier/src/errors.rs create mode 100644 tools/verifier/src/lib.rs create mode 100644 tools/verifier/src/passes/isolation.rs create mode 100644 tools/verifier/src/passes/mod.rs create mode 100644 tools/verifier/src/passes/module_attributes.rs create mode 100644 tools/verifier/src/passes/type_checks.rs create mode 100644 tools/verifier/src/passes/value_checks.rs create mode 100644 tools/verifier/tests/.gitignore create mode 100755 tools/verifier/tests/encode_test_cases.sh create mode 100644 tools/verifier/tests/examples.rs create mode 100644 tools/verifier/tests/generate_test_cases.py create mode 100644 tools/verifier/tests/negative/encode/bounds/nested_source_oob.txt create mode 100644 tools/verifier/tests/negative/encode/bounds/nested_target_oob.txt create mode 100644 tools/verifier/tests/negative/encode/bounds/op_input_oob.txt create mode 100644 tools/verifier/tests/negative/encode/bounds/op_output_oob.txt create mode 100644 tools/verifier/tests/negative/encode/bounds/region_source_oob.txt create mode 100644 tools/verifier/tests/negative/encode/bounds/region_target_oob.txt create mode 100644 tools/verifier/tests/negative/encode/module/entrypoint_is_declaration.txt create mode 100644 tools/verifier/tests/negative/encode/types/alloc_unexpected_input.txt create mode 100644 tools/verifier/tests/negative/encode/types/free_unexpected_output.txt create mode 100644 tools/verifier/tests/negative/encode/types/gate_missing_param_input.txt create mode 100644 tools/verifier/tests/negative/encode/types/gate_too_few_qubit_inputs.txt create mode 100644 tools/verifier/tests/negative/encode/types/gate_wrong_output_count.txt create mode 100644 tools/verifier/tests/negative/encode/types/qureg_alloc_bad_input.txt create mode 100644 tools/verifier/tests/negative/encode/types/qureg_alloc_bad_output.txt create mode 100644 tools/verifier/tests/negative/encode/types/qureg_extract_index_bad_idx_input.txt create mode 100644 tools/verifier/tests/negative/encode/types/qureg_extract_index_bad_qubit_output.txt create mode 100644 tools/verifier/tests/negative/encode/types/qureg_extract_index_bad_reg_input.txt create mode 100644 tools/verifier/tests/negative/encode/types/qureg_free_bad_input.txt create mode 100644 tools/verifier/tests/negative/encode/types/qureg_insert_index_bad_qubit_input.txt create mode 100644 tools/verifier/tests/negative/encode/types/qureg_join_bad_input.txt create mode 100644 tools/verifier/tests/negative/encode/types/qureg_length_bad_output.txt create mode 100644 tools/verifier/tests/negative_attrs.rs create mode 100644 tools/verifier/tests/negative_bounds.rs create mode 100644 tools/verifier/tests/negative_linearity.rs create mode 100644 tools/verifier/tests/negative_ordering.rs create mode 100644 tools/verifier/tests/negative_scoping.rs create mode 100644 tools/verifier/tests/negative_types.rs create mode 100644 tools/verifier/tests/positive.rs diff --git a/Cargo.lock b/Cargo.lock index 2755312..f014680 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -765,6 +765,13 @@ version = "0.2.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ebc1c04c71510c7f702b52b7c350734c9ff1295c464a03335b00bb84fc54f853" +[[package]] +name = "verifier" +version = "0.1.0" +dependencies = [ + "jeff-format", +] + [[package]] name = "walkdir" version = "2.5.0" diff --git a/Cargo.toml b/Cargo.toml index 0ff8ece..fa96b93 100644 --- a/Cargo.toml +++ b/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" diff --git a/impl/rs/src/reader.rs b/impl/rs/src/reader.rs index a9a3870..32ced8f 100644 --- a/impl/rs/src/reader.rs +++ b/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}; diff --git a/tools/verifier/Cargo.toml b/tools/verifier/Cargo.toml new file mode 100644 index 0000000..86150b8 --- /dev/null +++ b/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 diff --git a/tools/verifier/src/analysis.rs b/tools/verifier/src/analysis.rs new file mode 100644 index 0000000..1b0bae0 --- /dev/null +++ b/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`] with one entry per value in the function's value table. +pub fn build_value_stats( + region: Region<'_>, + num_values: usize, +) -> Result, ReadError> { + let mut stats = vec![ValueStats::default(); num_values]; + collect_value_stats(region, &mut stats)?; + Ok(stats) +} diff --git a/tools/verifier/src/errors.rs b/tools/verifier/src/errors.rs new file mode 100644 index 0000000..ac92b2b --- /dev/null +++ b/tools/verifier/src/errors.rs @@ -0,0 +1,148 @@ +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'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 linear value (qubit or qureg) is produced by more than one operation. + LinearValueProducedMultipleTimes { + /// 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::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::LinearValueProducedMultipleTimes { + value_id, + producers, + } => { + write!( + f, + "linear 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" + ) + } + } + } +} diff --git a/tools/verifier/src/lib.rs b/tools/verifier/src/lib.rs new file mode 100644 index 0000000..033a423 --- /dev/null +++ b/tools/verifier/src/lib.rs @@ -0,0 +1,42 @@ +//! 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. +pub fn verify_module(module: Module<'_>) -> Vec { + 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) { + verify_value_checks(def, errors); + verify_operation_types(def.body(), errors); + verify_isolation(def, errors); +} diff --git a/tools/verifier/src/passes/isolation.rs b/tools/verifier/src/passes/isolation.rs new file mode 100644 index 0000000..ba7992b --- /dev/null +++ b/tools/verifier/src/passes/isolation.rs @@ -0,0 +1,84 @@ +//! Checks that nested regions are isolated from outer scopes (IsolatedFromAbove). + +use std::collections::HashSet; + +use jeff::reader::optype::{ControlFlowOp, OpType}; +use jeff::reader::{FunctionDefinition, Region, ValueId}; + +use crate::VerificationError; + +/// Check that no operation inside a nested region directly references a value from an outer scope. +pub fn verify_isolation(def: FunctionDefinition<'_>, errors: &mut Vec) { + check_region_isolation(def.body(), &HashSet::new(), errors); +} + +fn check_region_isolation( + region: Region<'_>, + outer_values: &HashSet, + errors: &mut Vec, +) { + let mut locally_defined: HashSet = region + .sources() + .filter_map(|r| r.ok()) + .map(|v| v.id()) + .collect(); + + for op in region.operations() { + for input in op.inputs().filter_map(|r| r.ok()) { + if outer_values.contains(&input.id()) && !locally_defined.contains(&input.id()) { + errors.push(VerificationError::IsolationViolation { + value_id: input.id(), + }); + } + } + + for output in op.outputs().filter_map(|r| r.ok()) { + locally_defined.insert(output.id()); + } + + if let OpType::ControlFlowOp(cf_op) = op.op_type() { + let new_outer: HashSet = outer_values + .iter() + .chain(locally_defined.iter()) + .cloned() + .collect(); + check_cf_isolation(cf_op.as_ref(), &new_outer, errors); + } + } + + for target in region.targets().filter_map(|r| r.ok()) { + if outer_values.contains(&target.id()) && !locally_defined.contains(&target.id()) { + errors.push(VerificationError::IsolationViolation { + value_id: target.id(), + }); + } + } +} + +fn check_cf_isolation( + cf_op: &ControlFlowOp<'_>, + outer_values: &HashSet, + errors: &mut Vec, +) { + match cf_op { + ControlFlowOp::For { region } => { + check_region_isolation(*region, outer_values, errors); + } + ControlFlowOp::While { condition, body } => { + check_region_isolation(*condition, outer_values, errors); + check_region_isolation(*body, outer_values, errors); + } + ControlFlowOp::DoWhile { body, condition } => { + check_region_isolation(*body, outer_values, errors); + check_region_isolation(*condition, outer_values, errors); + } + ControlFlowOp::Switch(switch_op) => { + for branch in switch_op.branches() { + check_region_isolation(branch, outer_values, errors); + } + if let Some(default) = switch_op.default_branch() { + check_region_isolation(default, outer_values, errors); + } + } + } +} diff --git a/tools/verifier/src/passes/mod.rs b/tools/verifier/src/passes/mod.rs new file mode 100644 index 0000000..f658f9c --- /dev/null +++ b/tools/verifier/src/passes/mod.rs @@ -0,0 +1,6 @@ +//! Verification passes, one per category of check. + +pub mod isolation; +pub mod module_attributes; +pub mod type_checks; +pub mod value_checks; diff --git a/tools/verifier/src/passes/module_attributes.rs b/tools/verifier/src/passes/module_attributes.rs new file mode 100644 index 0000000..e8877db --- /dev/null +++ b/tools/verifier/src/passes/module_attributes.rs @@ -0,0 +1,20 @@ +//! Checks for required module-level attributes. + +use jeff::reader::{Function, Module}; + +use crate::VerificationError; + +/// Verify that the module has a non-zero version and a valid entrypoint. +pub fn verify_module_attributes(module: Module<'_>, errors: &mut Vec) { + let v = module.version(); + if v.major == 0 && v.minor == 0 && v.patch == 0 { + errors.push(VerificationError::MissingVersion); + } + + match module.try_function(module.entrypoint_id()) { + None | Some(Function::Declaration(_)) => { + errors.push(VerificationError::InvalidEntrypoint); + } + Some(Function::Definition(_)) => {} + } +} diff --git a/tools/verifier/src/passes/type_checks.rs b/tools/verifier/src/passes/type_checks.rs new file mode 100644 index 0000000..9a3b76a --- /dev/null +++ b/tools/verifier/src/passes/type_checks.rs @@ -0,0 +1,579 @@ +//! Checks for correct input/output types and bitwidth/precision uniformity. + +use jeff::reader::optype::{ControlFlowOp, FloatOp, IntOp, OpType, QubitOp, QubitRegisterOp}; +use jeff::reader::Region; +use jeff::types::{FloatPrecision, Type}; + +use crate::VerificationError; + +/// Check that all operations in `region` (and its nested regions) have correctly typed inputs and outputs. +pub fn verify_operation_types(region: Region<'_>, errors: &mut Vec) { + check_region_types(region, errors); +} + +fn check_region_types(region: Region<'_>, errors: &mut Vec) { + for op in region.operations() { + let inputs: Vec = op.inputs().filter_map(|r| r.ok()).map(|v| v.ty()).collect(); + let outputs: Vec = op + .outputs() + .filter_map(|r| r.ok()) + .map(|v| v.ty()) + .collect(); + + match op.op_type() { + OpType::IntOp(int_op) => check_int_op(int_op, &inputs, &outputs, errors), + OpType::FloatOp(float_op) => check_float_op(float_op, &inputs, &outputs, errors), + OpType::QubitOp(qubit_op) => check_qubit_op(qubit_op, &inputs, &outputs, errors), + OpType::QubitRegisterOp(qureg_op) => { + check_qureg_op(qureg_op, &inputs, &outputs, errors); + } + OpType::ControlFlowOp(cf_op) => check_cf_region_types(cf_op.as_ref(), errors), + _ => {} + } + } +} + +fn check_cf_region_types(cf_op: &ControlFlowOp<'_>, errors: &mut Vec) { + match cf_op { + ControlFlowOp::For { region } => check_region_types(*region, errors), + ControlFlowOp::While { condition, body } => { + check_region_types(*condition, errors); + check_region_types(*body, errors); + } + ControlFlowOp::DoWhile { body, condition } => { + check_region_types(*body, errors); + check_region_types(*condition, errors); + } + ControlFlowOp::Switch(switch_op) => { + for branch in switch_op.branches() { + check_region_types(branch, errors); + } + if let Some(default) = switch_op.default_branch() { + check_region_types(default, errors); + } + } + } +} + +fn check_uniform_int( + inputs: &[Type], + outputs: &[Type], + name: &'static str, + errors: &mut Vec, +) { + for ty in inputs { + if !matches!(ty, Type::Int { .. }) { + errors.push(VerificationError::InvalidInputType { operation: name }); + return; + } + } + for ty in outputs { + if !matches!(ty, Type::Int { .. }) { + errors.push(VerificationError::InvalidOutputType { operation: name }); + return; + } + } + let mut bits: Option = None; + for ty in inputs.iter().chain(outputs.iter()) { + if let Type::Int { bits: b } = ty { + match bits { + None => bits = Some(*b), + Some(existing) if existing != *b => { + errors.push(VerificationError::TypeMismatch { operation: name }); + return; + } + _ => {} + } + } + } +} + +fn check_uniform_float( + inputs: &[Type], + outputs: &[Type], + name: &'static str, + errors: &mut Vec, +) { + for ty in inputs { + if !matches!(ty, Type::Float { .. }) { + errors.push(VerificationError::InvalidInputType { operation: name }); + return; + } + } + for ty in outputs { + if !matches!(ty, Type::Float { .. }) { + errors.push(VerificationError::InvalidOutputType { operation: name }); + return; + } + } + let mut precision: Option = None; + for ty in inputs.iter().chain(outputs.iter()) { + if let Type::Float { precision: p } = ty { + match precision { + None => precision = Some(*p), + Some(existing) if existing != *p => { + errors.push(VerificationError::TypeMismatch { operation: name }); + return; + } + _ => {} + } + } + } +} + +fn check_int_op( + int_op: IntOp, + inputs: &[Type], + outputs: &[Type], + errors: &mut Vec, +) { + match int_op { + IntOp::Const1(_) => { + if outputs + .first() + .is_some_and(|ty| *ty != (Type::Int { bits: 1 })) + { + errors.push(VerificationError::InvalidOutputType { + operation: "int const", + }); + } + } + IntOp::Const8(_) => { + if outputs + .first() + .is_some_and(|ty| *ty != (Type::Int { bits: 8 })) + { + errors.push(VerificationError::InvalidOutputType { + operation: "int const", + }); + } + } + IntOp::Const16(_) => { + if outputs + .first() + .is_some_and(|ty| *ty != (Type::Int { bits: 16 })) + { + errors.push(VerificationError::InvalidOutputType { + operation: "int const", + }); + } + } + IntOp::Const32(_) => { + if outputs + .first() + .is_some_and(|ty| *ty != (Type::Int { bits: 32 })) + { + errors.push(VerificationError::InvalidOutputType { + operation: "int const", + }); + } + } + IntOp::Const64(_) => { + if outputs + .first() + .is_some_and(|ty| *ty != (Type::Int { bits: 64 })) + { + errors.push(VerificationError::InvalidOutputType { + operation: "int const", + }); + } + } + IntOp::Add + | IntOp::Sub + | IntOp::Mul + | IntOp::DivS + | IntOp::DivU + | IntOp::Pow + | IntOp::And + | IntOp::Or + | IntOp::Xor + | IntOp::MinS + | IntOp::MinU + | IntOp::MaxS + | IntOp::MaxU + | IntOp::RemS + | IntOp::RemU + | IntOp::Shl + | IntOp::Shr + | IntOp::Not + | IntOp::Abs => { + check_uniform_int(inputs, outputs, "int arithmetic", errors); + } + IntOp::Eq | IntOp::LtS | IntOp::LteS | IntOp::LtU | IntOp::LteU => { + check_uniform_int(inputs, &[], "int comparison", errors); + if outputs + .first() + .is_some_and(|ty| *ty != (Type::Int { bits: 1 })) + { + errors.push(VerificationError::InvalidOutputType { + operation: "int comparison", + }); + } + } + _ => {} + } +} + +fn check_float_op( + float_op: FloatOp, + inputs: &[Type], + outputs: &[Type], + errors: &mut Vec, +) { + match float_op { + FloatOp::Const32(_) => { + if outputs.first().is_some_and(|ty| { + *ty != (Type::Float { + precision: FloatPrecision::Float32, + }) + }) { + errors.push(VerificationError::InvalidOutputType { + operation: "float const", + }); + } + } + FloatOp::Const64(_) => { + if outputs.first().is_some_and(|ty| { + *ty != (Type::Float { + precision: FloatPrecision::Float64, + }) + }) { + errors.push(VerificationError::InvalidOutputType { + operation: "float const", + }); + } + } + FloatOp::Add + | FloatOp::Sub + | FloatOp::Mul + | FloatOp::Pow + | FloatOp::Max + | FloatOp::Min + | FloatOp::Atan2 + | FloatOp::Sqrt + | FloatOp::Abs + | FloatOp::Ceil + | FloatOp::Floor + | FloatOp::Exp + | FloatOp::Log + | FloatOp::Sin + | FloatOp::Cos + | FloatOp::Tan + | FloatOp::Asin + | FloatOp::Acos + | FloatOp::Atan + | FloatOp::Sinh + | FloatOp::Cosh + | FloatOp::Tanh + | FloatOp::Asinh + | FloatOp::Acosh + | FloatOp::Atanh => { + check_uniform_float(inputs, outputs, "float op", errors); + } + FloatOp::Eq | FloatOp::Lt | FloatOp::Lte | FloatOp::IsNan | FloatOp::IsInf => { + check_uniform_float(inputs, &[], "float predicate", errors); + if outputs + .first() + .is_some_and(|ty| *ty != (Type::Int { bits: 1 })) + { + errors.push(VerificationError::InvalidOutputType { + operation: "float predicate", + }); + } + } + _ => {} + } +} + +fn check_qubit_op( + qubit_op: QubitOp<'_>, + inputs: &[Type], + outputs: &[Type], + errors: &mut Vec, +) { + match qubit_op { + QubitOp::Alloc => { + if !inputs.is_empty() { + errors.push(VerificationError::InvalidInputType { operation: "Alloc" }); + } + if outputs.first().is_some_and(|ty| *ty != Type::Qubit) { + errors.push(VerificationError::InvalidOutputType { operation: "Alloc" }); + } + } + QubitOp::Free | QubitOp::FreeZero | QubitOp::Reset => { + if inputs.first().is_some_and(|ty| *ty != Type::Qubit) { + errors.push(VerificationError::InvalidInputType { + operation: "qubit free/reset", + }); + } + if !outputs.is_empty() { + errors.push(VerificationError::InvalidOutputType { + operation: "qubit free/reset", + }); + } + } + QubitOp::Measure => { + if inputs.first().is_some_and(|ty| *ty != Type::Qubit) { + errors.push(VerificationError::InvalidInputType { + operation: "Measure", + }); + } + if outputs + .first() + .is_some_and(|ty| *ty != (Type::Int { bits: 1 })) + { + errors.push(VerificationError::InvalidOutputType { + operation: "Measure", + }); + } + } + QubitOp::MeasureNd => { + if inputs.first().is_some_and(|ty| *ty != Type::Qubit) { + errors.push(VerificationError::InvalidInputType { + operation: "MeasureNd", + }); + } + if outputs.len() >= 2 { + if outputs[0] != Type::Qubit { + errors.push(VerificationError::InvalidOutputType { + operation: "MeasureNd", + }); + } + if outputs[1] != (Type::Int { bits: 1 }) { + errors.push(VerificationError::InvalidOutputType { + operation: "MeasureNd", + }); + } + } + } + QubitOp::Gate(gate) => { + let num_qubits = gate.num_qubits(); + let num_params = gate.num_params(); + if inputs.len() != num_qubits + num_params { + errors.push(VerificationError::WrongArity { operation: "Gate" }); + } + if outputs.len() != num_qubits { + errors.push(VerificationError::WrongArity { operation: "Gate" }); + } + for (i, ty) in inputs.iter().enumerate() { + if i < num_qubits { + if *ty != Type::Qubit { + errors.push(VerificationError::InvalidInputType { operation: "Gate" }); + } + } else if i < num_qubits + num_params && !matches!(ty, Type::Float { .. }) { + errors.push(VerificationError::InvalidInputType { operation: "Gate" }); + } + } + for ty in outputs.iter().take(num_qubits) { + if *ty != Type::Qubit { + errors.push(VerificationError::InvalidOutputType { operation: "Gate" }); + } + } + } + _ => {} + } +} + +fn is_qureg(ty: &Type) -> bool { + matches!(ty, Type::QubitRegister { .. }) +} + +fn check_qureg_op( + qureg_op: QubitRegisterOp, + inputs: &[Type], + outputs: &[Type], + errors: &mut Vec, +) { + match qureg_op { + QubitRegisterOp::Alloc => { + if inputs + .first() + .is_some_and(|ty| *ty != (Type::Int { bits: 32 })) + { + errors.push(VerificationError::InvalidInputType { + operation: "qureg alloc", + }); + } + if outputs.first().is_some_and(|ty| !is_qureg(ty)) { + errors.push(VerificationError::InvalidOutputType { + operation: "qureg alloc", + }); + } + } + QubitRegisterOp::Free | QubitRegisterOp::FreeZero => { + if inputs.first().is_some_and(|ty| !is_qureg(ty)) { + errors.push(VerificationError::InvalidInputType { + operation: "qureg free", + }); + } + } + QubitRegisterOp::ExtractIndex => { + if inputs.first().is_some_and(|ty| !is_qureg(ty)) { + errors.push(VerificationError::InvalidInputType { + operation: "qureg extractIndex", + }); + } + if inputs + .get(1) + .is_some_and(|ty| *ty != (Type::Int { bits: 32 })) + { + errors.push(VerificationError::InvalidInputType { + operation: "qureg extractIndex", + }); + } + if outputs.first().is_some_and(|ty| !is_qureg(ty)) { + errors.push(VerificationError::InvalidOutputType { + operation: "qureg extractIndex", + }); + } + if outputs.get(1).is_some_and(|ty| *ty != Type::Qubit) { + errors.push(VerificationError::InvalidOutputType { + operation: "qureg extractIndex", + }); + } + } + QubitRegisterOp::InsertIndex => { + if inputs.first().is_some_and(|ty| !is_qureg(ty)) { + errors.push(VerificationError::InvalidInputType { + operation: "qureg insertIndex", + }); + } + if inputs + .get(1) + .is_some_and(|ty| *ty != (Type::Int { bits: 32 })) + { + errors.push(VerificationError::InvalidInputType { + operation: "qureg insertIndex", + }); + } + if inputs.get(2).is_some_and(|ty| *ty != Type::Qubit) { + errors.push(VerificationError::InvalidInputType { + operation: "qureg insertIndex", + }); + } + if outputs.first().is_some_and(|ty| !is_qureg(ty)) { + errors.push(VerificationError::InvalidOutputType { + operation: "qureg insertIndex", + }); + } + } + QubitRegisterOp::ExtractSlice => { + if inputs.first().is_some_and(|ty| !is_qureg(ty)) { + errors.push(VerificationError::InvalidInputType { + operation: "qureg extractSlice", + }); + } + for ty in inputs.iter().skip(1).take(2) { + if *ty != (Type::Int { bits: 32 }) { + errors.push(VerificationError::InvalidInputType { + operation: "qureg extractSlice", + }); + } + } + for ty in outputs.iter().take(2) { + if !is_qureg(ty) { + errors.push(VerificationError::InvalidOutputType { + operation: "qureg extractSlice", + }); + } + } + } + QubitRegisterOp::InsertSlice => { + if inputs.first().is_some_and(|ty| !is_qureg(ty)) { + errors.push(VerificationError::InvalidInputType { + operation: "qureg insertSlice", + }); + } + if inputs + .get(1) + .is_some_and(|ty| *ty != (Type::Int { bits: 32 })) + { + errors.push(VerificationError::InvalidInputType { + operation: "qureg insertSlice", + }); + } + if inputs.get(2).is_some_and(|ty| !is_qureg(ty)) { + errors.push(VerificationError::InvalidInputType { + operation: "qureg insertSlice", + }); + } + if outputs.first().is_some_and(|ty| !is_qureg(ty)) { + errors.push(VerificationError::InvalidOutputType { + operation: "qureg insertSlice", + }); + } + } + QubitRegisterOp::Length => { + if inputs.first().is_some_and(|ty| !is_qureg(ty)) { + errors.push(VerificationError::InvalidInputType { + operation: "qureg length", + }); + } + if outputs.first().is_some_and(|ty| !is_qureg(ty)) { + errors.push(VerificationError::InvalidOutputType { + operation: "qureg length", + }); + } + if outputs + .get(1) + .is_some_and(|ty| *ty != (Type::Int { bits: 32 })) + { + errors.push(VerificationError::InvalidOutputType { + operation: "qureg length", + }); + } + } + QubitRegisterOp::Split => { + if inputs.first().is_some_and(|ty| !is_qureg(ty)) { + errors.push(VerificationError::InvalidInputType { + operation: "qureg split", + }); + } + if inputs + .get(1) + .is_some_and(|ty| *ty != (Type::Int { bits: 32 })) + { + errors.push(VerificationError::InvalidInputType { + operation: "qureg split", + }); + } + for ty in outputs.iter().take(2) { + if !is_qureg(ty) { + errors.push(VerificationError::InvalidOutputType { + operation: "qureg split", + }); + } + } + } + QubitRegisterOp::Join => { + for ty in inputs.iter().take(2) { + if !is_qureg(ty) { + errors.push(VerificationError::InvalidInputType { + operation: "qureg join", + }); + } + } + if outputs.first().is_some_and(|ty| !is_qureg(ty)) { + errors.push(VerificationError::InvalidOutputType { + operation: "qureg join", + }); + } + } + QubitRegisterOp::Create => { + for ty in inputs.iter() { + if *ty != Type::Qubit { + errors.push(VerificationError::InvalidInputType { + operation: "qureg create", + }); + } + } + if outputs.first().is_some_and(|ty| !is_qureg(ty)) { + errors.push(VerificationError::InvalidOutputType { + operation: "qureg create", + }); + } + } + #[allow(unreachable_patterns)] + _ => {} + } +} diff --git a/tools/verifier/src/passes/value_checks.rs b/tools/verifier/src/passes/value_checks.rs new file mode 100644 index 0000000..7400daa --- /dev/null +++ b/tools/verifier/src/passes/value_checks.rs @@ -0,0 +1,127 @@ +//! Checks for value ordering, bounds, and linearity constraints. + +use std::collections::HashSet; + +use jeff::reader::optype::{ControlFlowOp, OpType}; +use jeff::reader::{FunctionDefinition, ReadError, Region, ValueId}; +use jeff::types::Type; + +use crate::analysis::build_value_stats; +use crate::VerificationError; + +/// Check value ordering, out-of-bounds references, and linearity for a function definition. +pub fn verify_value_checks(def: FunctionDefinition<'_>, errors: &mut Vec) { + let values = def.values(); + let num_values = values.len(); + + check_region_ordering(def.body(), errors); + + match build_value_stats(def.body(), num_values) { + Ok(stats) => { + for (id, value) in values.iter() { + if is_linear(value.ty()) { + let stat = &stats[id as usize]; + if stat.producers > 1 { + errors.push(VerificationError::LinearValueProducedMultipleTimes { + value_id: id, + producers: stat.producers, + }); + } + if stat.consumers > 1 { + errors.push(VerificationError::LinearValueConsumedMultipleTimes { + value_id: id, + consumers: stat.consumers, + }); + } + if stat.consumers == 0 && stat.producers > 0 { + errors.push(VerificationError::LinearValueNeverConsumed { value_id: id }); + } + } + } + } + Err(e) => push_oob(e, errors), + } +} + +fn is_linear(ty: Type) -> bool { + matches!(ty, Type::Qubit | Type::QubitRegister { .. }) +} + +fn push_oob(e: ReadError, errors: &mut Vec) { + if let ReadError::ValueOutOfBounds { idx, count } = e { + errors.push(VerificationError::ValueOutOfBounds { + value_id: idx, + value_count: count, + }); + } +} + +fn check_region_ordering(region: Region<'_>, errors: &mut Vec) { + let mut defined: HashSet = HashSet::new(); + + for result in region.sources() { + match result { + Ok(v) => { + defined.insert(v.id()); + } + Err(e) => push_oob(e, errors), + } + } + + for op in region.operations() { + for result in op.inputs() { + match result { + Ok(v) if !defined.contains(&v.id()) => { + errors.push(VerificationError::UsedBeforeDefined { value_id: v.id() }); + } + Ok(_) => {} + Err(e) => push_oob(e, errors), + } + } + + for result in op.outputs() { + match result { + Ok(v) => { + defined.insert(v.id()); + } + Err(e) => push_oob(e, errors), + } + } + + if let OpType::ControlFlowOp(cf_op) = op.op_type() { + check_cf_ordering(cf_op.as_ref(), errors); + } + } + + for result in region.targets() { + match result { + Ok(v) if !defined.contains(&v.id()) => { + errors.push(VerificationError::UsedBeforeDefined { value_id: v.id() }); + } + Ok(_) => {} + Err(e) => push_oob(e, errors), + } + } +} + +fn check_cf_ordering(cf_op: &ControlFlowOp<'_>, errors: &mut Vec) { + match cf_op { + ControlFlowOp::For { region } => check_region_ordering(*region, errors), + ControlFlowOp::While { condition, body } => { + check_region_ordering(*condition, errors); + check_region_ordering(*body, errors); + } + ControlFlowOp::DoWhile { body, condition } => { + check_region_ordering(*body, errors); + check_region_ordering(*condition, errors); + } + ControlFlowOp::Switch(switch_op) => { + for branch in switch_op.branches() { + check_region_ordering(branch, errors); + } + if let Some(default) = switch_op.default_branch() { + check_region_ordering(default, errors); + } + } + } +} diff --git a/tools/verifier/tests/.gitignore b/tools/verifier/tests/.gitignore new file mode 100644 index 0000000..6c3a5f4 --- /dev/null +++ b/tools/verifier/tests/.gitignore @@ -0,0 +1,15 @@ +# All .jeff files are generated — recreate with: +# .venv/bin/python tools/verifier/tests/generate_test_cases.py (python-generated) +# tools/verifier/tests/encode_test_cases.sh (hand-crafted sources) +**/*.jeff + +# .txt files produced by generate_test_cases.py (capnp decode of the generated .jeff) +positive/*.txt +negative/bounds/*.txt +negative/linearity/*.txt +negative/module/missing_version.txt +negative/module/entrypoint_oob.txt +negative/module/no_functions.txt +negative/ordering/*.txt +negative/scoping/*.txt +negative/types/*.txt diff --git a/tools/verifier/tests/encode_test_cases.sh b/tools/verifier/tests/encode_test_cases.sh new file mode 100755 index 0000000..ecd8246 --- /dev/null +++ b/tools/verifier/tests/encode_test_cases.sh @@ -0,0 +1,35 @@ +#!/usr/bin/env bash +# Encode all hand-crafted .txt fixtures in negative/encode/ to their target test directories. +# +# Run from anywhere: +# tools/verifier/tests/encode_test_cases.sh +# +# Requires the capnp CLI tool to be installed. + +set -euo pipefail + +SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" +REPO_ROOT="$(cd "$SCRIPT_DIR/../../.." && pwd)" +SCHEMA="$REPO_ROOT/impl/capnp/jeff.capnp" +ENCODED_DIR="$SCRIPT_DIR/negative/encode" + +if ! command -v capnp &>/dev/null; then + echo "error: capnp not found. Install the Cap'n Proto CLI tools." >&2 + exit 1 +fi + +echo "Encoding hand-crafted test fixtures..." + +while IFS= read -r -d '' src; do + # src is e.g. .../negative/encode/bounds/op_input_oob.txt + rel="${src#$ENCODED_DIR/}" # bounds/op_input_oob.txt + subdir="$(dirname "$rel")" # bounds + base="$(basename "$rel" .txt)" # op_input_oob + dst_dir="$SCRIPT_DIR/negative/$subdir" + dst="$dst_dir/$base.jeff" + mkdir -p "$dst_dir" + capnp encode "$SCHEMA" Module < "$src" > "$dst" + echo " encoded: negative/$subdir/$base.jeff" +done < <(find "$ENCODED_DIR" -name "*.txt" -print0 | sort -z) + +echo "Done." diff --git a/tools/verifier/tests/examples.rs b/tools/verifier/tests/examples.rs new file mode 100644 index 0000000..d340473 --- /dev/null +++ b/tools/verifier/tests/examples.rs @@ -0,0 +1,55 @@ +#![allow(missing_docs)] +//! Run the verifier against every shipped example .jeff file and print the results. +//! This is purely informational — the test always passes. +//! Run with `cargo test -p verifier examples -- --nocapture` to see the output. + +use jeff::reader::ReadJeff; +use jeff::Jeff; +use std::fs::File; +use std::path::Path; +use verifier::verify_module; + +fn run_example(name: &str) { + let path = Path::new(env!("CARGO_MANIFEST_DIR")) + .join("../../examples") + .join(name); + + print!("{name}: "); + + let file = match File::open(&path) { + Ok(f) => f, + Err(e) => { + println!("could not open file — {e}"); + return; + } + }; + + let jeff = match Jeff::read(file) { + Ok(j) => j, + Err(e) => { + println!("read error — {e:?}"); + return; + } + }; + + let errors = verify_module(jeff.module()); + if errors.is_empty() { + println!("OK"); + } else { + println!("{} error(s):", errors.len()); + for e in &errors { + println!(" - {e}"); + } + } +} + +#[test] +fn verify_examples() { + println!(); + run_example("qubits/qubits.jeff"); + run_example("entangled_qs/entangled_qs.jeff"); + run_example("entangled_calls/entangled_calls.jeff"); + run_example("catalyst_simple/catalyst_simple.jeff"); + run_example("catalyst_tket_opt/catalyst_tket_opt.jeff"); + run_example("python_optimization/python_optimization.jeff"); +} diff --git a/tools/verifier/tests/generate_test_cases.py b/tools/verifier/tests/generate_test_cases.py new file mode 100644 index 0000000..0284ab7 --- /dev/null +++ b/tools/verifier/tests/generate_test_cases.py @@ -0,0 +1,1152 @@ +"""Generate .jeff (and companion .txt) test case files for the verifier. + +Run from the repo root: + .venv/bin/python tools/verifier/tests/generate_test_cases.py + +Each call to _write() produces both a binary .jeff file and a human-readable .txt +file (via `capnp decode`) in the same directory. + +Tests implemented via hand-crafted .txt sources (not generated here): + - entrypoint_is_declaration : Python lib crashes on FunctionDecl.body in _compute_strings + - OOB value-reference tests : Python lib assigns IDs automatically; can't produce OOB refs + - Qureg op type tests : Python lib has no qureg op support + - Alloc unexpected input : same — requires manual capnp text + - Free / Reset with output : same + - Gate wrong arity tests : same + Source .txt files live in tests/negative/encode/. + Run tests/encode_test_cases.sh to produce their .jeff files. + +Deferred (not implemented, caught by the reader not the verifier): + - test_unsupported_schema_version : rejected by Jeff::read before verify_module is called +""" + +import subprocess +from pathlib import Path + +import semver + +from jeff import ( + CustomGate, + DoWhileSCF, + FunctionDef, + ForSCF, + JeffModule, + JeffOp, + JeffRegion, + JeffValue, + IntType, + FloatType, + QubitType, + SwitchSCF, + WhileSCF, + qubit_alloc, + qubit_free, + quantum_gate, +) + +POSITIVE_DIR = Path(__file__).parent / "positive" +NEG_MODULE = Path(__file__).parent / "negative" / "module" +NEG_ORDERING = Path(__file__).parent / "negative" / "ordering" +NEG_TYPES = Path(__file__).parent / "negative" / "types" +NEG_LINEARITY = Path(__file__).parent / "negative" / "linearity" +NEG_SCOPING = Path(__file__).parent / "negative" / "scoping" + +_SCHEMA = Path(__file__).parents[3] / "impl" / "capnp" / "jeff.capnp" + +VERSION = semver.Version(0, 2, 0) +VERSION_ZERO = semver.Version(0, 0, 0) + + +def _write(module: JeffModule, directory: Path, name: str) -> None: + jeff_path = directory / name + module.write_out(jeff_path) + txt_path = jeff_path.with_suffix(".txt") + with open(jeff_path, "rb") as f_in, open(txt_path, "w") as f_out: + subprocess.run( + ["capnp", "decode", str(_SCHEMA), "Module"], + stdin=f_in, + stdout=f_out, + check=True, + ) + + +# ────────────────────────────────────────────── +# Positive tests +# ────────────────────────────────────────────── + + +def generate_valid_comprehensive() -> None: + """One file that exercises every feature the verifier checks.""" + + c10 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) + c20 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 20) + iadd = JeffOp( + "int", "add", [c10.outputs[0], c20.outputs[0]], [JeffValue(IntType(32))] + ) + ieq = JeffOp("int", "eq", [c10.outputs[0], c20.outputs[0]], [JeffValue(IntType(1))]) + + f1 = JeffOp("float", "const64", [], [JeffValue(FloatType(64))], 1.0) + f2 = JeffOp("float", "const64", [], [JeffValue(FloatType(64))], 2.0) + fadd = JeffOp( + "float", "add", [f1.outputs[0], f2.outputs[0]], [JeffValue(FloatType(64))] + ) + flt = JeffOp("float", "lt", [f1.outputs[0], f2.outputs[0]], [JeffValue(IntType(1))]) + + alloc_h = qubit_alloc() + gate_h = quantum_gate("H", alloc_h.outputs[0]) + measure = JeffOp("qubit", "measure", [gate_h.outputs[0]], [JeffValue(IntType(1))]) + + alloc_rx = qubit_alloc() + gate_rx = quantum_gate("Rx", alloc_rx.outputs[0], params=[f1.outputs[0]]) + measure_nd = JeffOp( + "qubit", + "measureNd", + [gate_rx.outputs[0]], + [JeffValue(QubitType()), JeffValue(IntType(1))], + ) + free_q = qubit_free(measure_nd.outputs[0]) + + for_iter = JeffValue(IntType(32)) + for_state_in = JeffValue(IntType(32)) + for_c1 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) + for_add = JeffOp( + "int", "add", [for_state_in, for_c1.outputs[0]], [JeffValue(IntType(32))] + ) + for_body = JeffRegion( + sources=[for_iter, for_state_in], + targets=[for_add.outputs[0]], + operations=[for_c1, for_add], + ) + for_op = JeffOp( + "scf", + "for", + [c10.outputs[0], iadd.outputs[0], c10.outputs[0], c20.outputs[0]], + [JeffValue(IntType(32))], + ForSCF(for_body), + ) + + w_cond_src = JeffValue(IntType(1)) + w_cond_not = JeffOp("int", "not", [w_cond_src], [JeffValue(IntType(1))]) + while_cond = JeffRegion( + sources=[w_cond_src], targets=[w_cond_not.outputs[0]], operations=[w_cond_not] + ) + w_body_src = JeffValue(IntType(1)) + w_body_not = JeffOp("int", "not", [w_body_src], [JeffValue(IntType(1))]) + while_body = JeffRegion( + sources=[w_body_src], targets=[w_body_not.outputs[0]], operations=[w_body_not] + ) + while_op = JeffOp( + "scf", + "while", + [ieq.outputs[0]], + [JeffValue(IntType(1))], + WhileSCF(while_cond, while_body), + ) + + dw_body_src = JeffValue(IntType(32)) + dw_body_c1 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) + dw_body_add = JeffOp( + "int", "add", [dw_body_src, dw_body_c1.outputs[0]], [JeffValue(IntType(32))] + ) + dowhile_body = JeffRegion( + sources=[dw_body_src], + targets=[dw_body_add.outputs[0]], + operations=[dw_body_c1, dw_body_add], + ) + dw_cond_src = JeffValue(IntType(32)) + dw_cond_c10 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) + dw_cond_eq = JeffOp( + "int", "eq", [dw_cond_src, dw_cond_c10.outputs[0]], [JeffValue(IntType(1))] + ) + dowhile_cond = JeffRegion( + sources=[dw_cond_src], + targets=[dw_cond_eq.outputs[0]], + operations=[dw_cond_c10, dw_cond_eq], + ) + dowhile_op = JeffOp( + "scf", + "doWhile", + [iadd.outputs[0]], + [JeffValue(IntType(32))], + DoWhileSCF(dowhile_body, dowhile_cond), + ) + + sw_b0_src = JeffValue(IntType(32)) + sw_b0_c99 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 99) + sw_b0_add = JeffOp( + "int", "add", [sw_b0_src, sw_b0_c99.outputs[0]], [JeffValue(IntType(32))] + ) + sw_branch0 = JeffRegion( + sources=[sw_b0_src], + targets=[sw_b0_add.outputs[0]], + operations=[sw_b0_c99, sw_b0_add], + ) + sw_def_src = JeffValue(IntType(32)) + sw_default = JeffRegion(sources=[sw_def_src], targets=[sw_def_src], operations=[]) + switch_op = JeffOp( + "scf", + "switch", + [flt.outputs[0], iadd.outputs[0]], + [JeffValue(IntType(32))], + SwitchSCF([sw_branch0], sw_default), + ) + + body = JeffRegion( + sources=[], + targets=[], + operations=[ + c10, + c20, + iadd, + ieq, + f1, + f2, + fadd, + flt, + alloc_h, + gate_h, + measure, + alloc_rx, + gate_rx, + measure_nd, + free_q, + for_op, + while_op, + dowhile_op, + switch_op, + ], + ) + _write( + JeffModule( + [FunctionDef(name="main", body=body)], version=VERSION, entrypoint=0 + ), + POSITIVE_DIR, + "valid_comprehensive.jeff", + ) + + +def generate_valid_minimal() -> None: + """Empty-body function — the smallest valid program.""" + body = JeffRegion(sources=[], targets=[], operations=[]) + _write( + JeffModule( + [FunctionDef(name="minimal", body=body)], version=VERSION, entrypoint=0 + ), + POSITIVE_DIR, + "valid_minimal.jeff", + ) + + +def generate_valid_deeply_nested() -> None: + """For loop nested inside another for loop, both properly isolated.""" + c0 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 0) + c10 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) + c1 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) + + inner_iter = JeffValue(IntType(32)) + inner_state = JeffValue(IntType(32)) + inner_c1 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) + inner_add = JeffOp( + "int", "add", [inner_state, inner_c1.outputs[0]], [JeffValue(IntType(32))] + ) + inner_body = JeffRegion( + sources=[inner_iter, inner_state], + targets=[inner_add.outputs[0]], + operations=[inner_c1, inner_add], + ) + + outer_iter = JeffValue(IntType(32)) + outer_state = JeffValue(IntType(32)) + oc0 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 0) + oc10 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) + oc1 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) + inner_for = JeffOp( + "scf", + "for", + [oc0.outputs[0], oc10.outputs[0], oc1.outputs[0], outer_state], + [JeffValue(IntType(32))], + ForSCF(inner_body), + ) + outer_body = JeffRegion( + sources=[outer_iter, outer_state], + targets=[inner_for.outputs[0]], + operations=[oc0, oc10, oc1, inner_for], + ) + + outer_for = JeffOp( + "scf", + "for", + [c0.outputs[0], c10.outputs[0], c1.outputs[0], c0.outputs[0]], + [JeffValue(IntType(32))], + ForSCF(outer_body), + ) + body = JeffRegion(sources=[], targets=[], operations=[c0, c10, c1, outer_for]) + _write( + JeffModule( + [FunctionDef(name="main", body=body)], version=VERSION, entrypoint=0 + ), + POSITIVE_DIR, + "valid_deeply_nested.jeff", + ) + + +# ────────────────────────────────────────────── +# Negative: module attribute failures +# ────────────────────────────────────────────── + + +def _trivial_def() -> FunctionDef: + return FunctionDef(name="f", body=JeffRegion(sources=[], targets=[], operations=[])) + + +def generate_missing_version() -> None: + """Version 0.0.0 → MissingVersion.""" + _write( + JeffModule([_trivial_def()], version=VERSION_ZERO, entrypoint=0), + NEG_MODULE, + "missing_version.jeff", + ) + + +def generate_entrypoint_oob() -> None: + """Entrypoint index beyond function list → InvalidEntrypoint.""" + _write( + JeffModule([_trivial_def()], version=VERSION, entrypoint=99), + NEG_MODULE, + "entrypoint_oob.jeff", + ) + + +def generate_no_functions() -> None: + """Empty function list, version 0.0.0 → MissingVersion + InvalidEntrypoint.""" + _write( + JeffModule([], version=VERSION_ZERO, entrypoint=0), + NEG_MODULE, + "no_functions.jeff", + ) + + +# ────────────────────────────────────────────── +# Negative: used before defined +# ────────────────────────────────────────────── + + +def generate_use_before_define_outer() -> None: + """add uses c10 and c20 before they are defined in the outer region.""" + c10 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) + c20 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 20) + add = JeffOp( + "int", "add", [c10.outputs[0], c20.outputs[0]], [JeffValue(IntType(32))] + ) + body = JeffRegion(sources=[], targets=[], operations=[add, c10, c20]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_ORDERING, + "use_before_define_outer.jeff", + ) + + +def generate_use_before_define_for() -> None: + """Inside for body: add uses a constant before the constant op appears.""" + c10 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) + c20 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 20) + + for_iter = JeffValue(IntType(32)) + for_state = JeffValue(IntType(32)) + late_c = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) + bad_add = JeffOp( + "int", "add", [for_state, late_c.outputs[0]], [JeffValue(IntType(32))] + ) + for_body = JeffRegion( + sources=[for_iter, for_state], + targets=[bad_add.outputs[0]], + operations=[bad_add, late_c], + ) # bad_add before late_c + + for_op = JeffOp( + "scf", + "for", + [c10.outputs[0], c20.outputs[0], c10.outputs[0], c10.outputs[0]], + [JeffValue(IntType(32))], + ForSCF(for_body), + ) + body = JeffRegion(sources=[], targets=[], operations=[c10, c20, for_op]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_ORDERING, + "use_before_define_for.jeff", + ) + + +def generate_use_before_define_while_cond() -> None: + """Inside while condition: not uses a constant before the constant op appears.""" + c0 = JeffOp("int", "const32", [], [JeffValue(IntType(1))], 0) + + cond_src = JeffValue(IntType(1)) + late_c = JeffOp("int", "const32", [], [JeffValue(IntType(1))], 0) + bad_not = JeffOp("int", "not", [late_c.outputs[0]], [JeffValue(IntType(1))]) + cond_reg = JeffRegion( + sources=[cond_src], targets=[bad_not.outputs[0]], operations=[bad_not, late_c] + ) # bad_not before late_c + + body_src = JeffValue(IntType(1)) + body_not = JeffOp("int", "not", [body_src], [JeffValue(IntType(1))]) + body_reg = JeffRegion( + sources=[body_src], targets=[body_not.outputs[0]], operations=[body_not] + ) + + while_op = JeffOp( + "scf", + "while", + [c0.outputs[0]], + [JeffValue(IntType(1))], + WhileSCF(cond_reg, body_reg), + ) + body = JeffRegion(sources=[], targets=[], operations=[c0, while_op]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_ORDERING, + "use_before_define_while_cond.jeff", + ) + + +def generate_use_before_define_while_body() -> None: + """Inside while body: second not uses first not's output before first not appears.""" + c0 = JeffOp("int", "const32", [], [JeffValue(IntType(1))], 0) + + cond_src = JeffValue(IntType(1)) + cond_not = JeffOp("int", "not", [cond_src], [JeffValue(IntType(1))]) + cond_reg = JeffRegion( + sources=[cond_src], targets=[cond_not.outputs[0]], operations=[cond_not] + ) + + body_src = JeffValue(IntType(1)) + late_not = JeffOp("int", "not", [body_src], [JeffValue(IntType(1))]) + bad_not2 = JeffOp("int", "not", [late_not.outputs[0]], [JeffValue(IntType(1))]) + body_reg = JeffRegion( + sources=[body_src], + targets=[bad_not2.outputs[0]], + operations=[bad_not2, late_not], + ) # bad_not2 before late_not + + while_op = JeffOp( + "scf", + "while", + [c0.outputs[0]], + [JeffValue(IntType(1))], + WhileSCF(cond_reg, body_reg), + ) + body = JeffRegion(sources=[], targets=[], operations=[c0, while_op]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_ORDERING, + "use_before_define_while_body.jeff", + ) + + +def generate_use_before_define_dowhile_body() -> None: + """Inside dowhile body: add uses a constant before it appears.""" + c10 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) + + dw_src = JeffValue(IntType(32)) + late_c = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) + bad_add = JeffOp( + "int", "add", [dw_src, late_c.outputs[0]], [JeffValue(IntType(32))] + ) + dw_body = JeffRegion( + sources=[dw_src], targets=[bad_add.outputs[0]], operations=[bad_add, late_c] + ) # bad_add before late_c + + cond_src = JeffValue(IntType(32)) + cond_c = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 5) + cond_eq = JeffOp( + "int", "eq", [cond_src, cond_c.outputs[0]], [JeffValue(IntType(1))] + ) + dw_cond = JeffRegion( + sources=[cond_src], targets=[cond_eq.outputs[0]], operations=[cond_c, cond_eq] + ) + + dw_op = JeffOp( + "scf", + "doWhile", + [c10.outputs[0]], + [JeffValue(IntType(32))], + DoWhileSCF(dw_body, dw_cond), + ) + body = JeffRegion(sources=[], targets=[], operations=[c10, dw_op]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_ORDERING, + "use_before_define_dowhile_body.jeff", + ) + + +def generate_use_before_define_dowhile_cond() -> None: + """Inside dowhile condition: eq uses a constant before it appears.""" + c10 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) + + dw_src = JeffValue(IntType(32)) + dw_c1 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) + dw_add = JeffOp("int", "add", [dw_src, dw_c1.outputs[0]], [JeffValue(IntType(32))]) + dw_body = JeffRegion( + sources=[dw_src], targets=[dw_add.outputs[0]], operations=[dw_c1, dw_add] + ) + + cond_src = JeffValue(IntType(32)) + late_c = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 5) + bad_eq = JeffOp("int", "eq", [cond_src, late_c.outputs[0]], [JeffValue(IntType(1))]) + dw_cond = JeffRegion( + sources=[cond_src], targets=[bad_eq.outputs[0]], operations=[bad_eq, late_c] + ) # bad_eq before late_c + + dw_op = JeffOp( + "scf", + "doWhile", + [c10.outputs[0]], + [JeffValue(IntType(32))], + DoWhileSCF(dw_body, dw_cond), + ) + body = JeffRegion(sources=[], targets=[], operations=[c10, dw_op]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_ORDERING, + "use_before_define_dowhile_cond.jeff", + ) + + +def generate_use_before_define_switch() -> None: + """Inside a switch branch: add uses a constant before it appears.""" + c0 = JeffOp("int", "const32", [], [JeffValue(IntType(1))], 0) + c10 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) + + b0_src = JeffValue(IntType(32)) + late_c = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 99) + bad_add = JeffOp( + "int", "add", [b0_src, late_c.outputs[0]], [JeffValue(IntType(32))] + ) + branch0 = JeffRegion( + sources=[b0_src], targets=[bad_add.outputs[0]], operations=[bad_add, late_c] + ) # bad_add before late_c + + def_src = JeffValue(IntType(32)) + default = JeffRegion(sources=[def_src], targets=[def_src], operations=[]) + + sw_op = JeffOp( + "scf", + "switch", + [c0.outputs[0], c10.outputs[0]], + [JeffValue(IntType(32))], + SwitchSCF([branch0], default), + ) + body = JeffRegion(sources=[], targets=[], operations=[c0, c10, sw_op]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_ORDERING, + "use_before_define_switch.jeff", + ) + + +# ────────────────────────────────────────────── +# Negative: type check failures +# ────────────────────────────────────────────── + + +def generate_int_add_mixed_bitwidths() -> None: + """add(Int32, Int64) → TypeMismatch.""" + c32 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) + c64 = JeffOp("int", "const64", [], [JeffValue(IntType(64))], 2) + bad = JeffOp( + "int", "add", [c32.outputs[0], c64.outputs[0]], [JeffValue(IntType(32))] + ) + body = JeffRegion(sources=[], targets=[], operations=[c32, c64, bad]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_TYPES, + "int_add_mixed_bitwidths.jeff", + ) + + +def generate_int_compare_mixed_bitwidths() -> None: + """eq(Int32, Int64) → TypeMismatch for int comparison.""" + c32 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) + c64 = JeffOp("int", "const64", [], [JeffValue(IntType(64))], 2) + bad = JeffOp("int", "eq", [c32.outputs[0], c64.outputs[0]], [JeffValue(IntType(1))]) + body = JeffRegion(sources=[], targets=[], operations=[c32, c64, bad]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_TYPES, + "int_compare_mixed_bitwidths.jeff", + ) + + +def generate_int_compare_bad_output() -> None: + """eq produces Int32 instead of Int1 → InvalidOutputType.""" + c32a = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) + c32b = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 2) + bad = JeffOp( + "int", "eq", [c32a.outputs[0], c32b.outputs[0]], [JeffValue(IntType(32))] + ) + body = JeffRegion(sources=[], targets=[], operations=[c32a, c32b, bad]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_TYPES, + "int_compare_bad_output.jeff", + ) + + +def generate_int_unary_bad_output() -> None: + """not(Int32) → Int64: mismatched bitwidth → TypeMismatch.""" + c32 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 5) + bad = JeffOp("int", "not", [c32.outputs[0]], [JeffValue(IntType(64))]) + body = JeffRegion(sources=[], targets=[], operations=[c32, bad]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_TYPES, + "int_unary_bad_output.jeff", + ) + + +def generate_float_add_mixed_precisions() -> None: + """add(Float32, Float64) → TypeMismatch.""" + f32 = JeffOp("float", "const32", [], [JeffValue(FloatType(32))], 1.0) + f64 = JeffOp("float", "const64", [], [JeffValue(FloatType(64))], 2.0) + bad = JeffOp( + "float", "add", [f32.outputs[0], f64.outputs[0]], [JeffValue(FloatType(64))] + ) + body = JeffRegion(sources=[], targets=[], operations=[f32, f64, bad]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_TYPES, + "float_add_mixed_precisions.jeff", + ) + + +def generate_float_compare_mixed_precisions() -> None: + """lt(Float32, Float64) → TypeMismatch for float predicate.""" + f32 = JeffOp("float", "const32", [], [JeffValue(FloatType(32))], 1.0) + f64 = JeffOp("float", "const64", [], [JeffValue(FloatType(64))], 2.0) + bad = JeffOp( + "float", "lt", [f32.outputs[0], f64.outputs[0]], [JeffValue(IntType(1))] + ) + body = JeffRegion(sources=[], targets=[], operations=[f32, f64, bad]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_TYPES, + "float_compare_mixed_precisions.jeff", + ) + + +def generate_float_compare_bad_output() -> None: + """lt produces Float64 instead of Int1 → InvalidOutputType.""" + f64a = JeffOp("float", "const64", [], [JeffValue(FloatType(64))], 1.0) + f64b = JeffOp("float", "const64", [], [JeffValue(FloatType(64))], 2.0) + bad = JeffOp( + "float", "lt", [f64a.outputs[0], f64b.outputs[0]], [JeffValue(FloatType(64))] + ) + body = JeffRegion(sources=[], targets=[], operations=[f64a, f64b, bad]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_TYPES, + "float_compare_bad_output.jeff", + ) + + +def generate_alloc_bad_output() -> None: + """alloc produces Int32 instead of Qubit → InvalidOutputType.""" + bad = JeffOp("qubit", "alloc", [], [JeffValue(IntType(32))]) + body = JeffRegion(sources=[], targets=[], operations=[bad]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_TYPES, + "alloc_bad_output.jeff", + ) + + +def generate_measure_bad_input() -> None: + """measure takes Int32 instead of Qubit → InvalidInputType.""" + c = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 0) + bad = JeffOp("qubit", "measure", [c.outputs[0]], [JeffValue(IntType(1))]) + body = JeffRegion(sources=[], targets=[], operations=[c, bad]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_TYPES, + "measure_bad_input.jeff", + ) + + +def generate_measure_bad_output() -> None: + """measure produces Float64 instead of Int1 → InvalidOutputType.""" + alloc = qubit_alloc() + bad = JeffOp("qubit", "measure", [alloc.outputs[0]], [JeffValue(FloatType(64))]) + body = JeffRegion(sources=[], targets=[], operations=[alloc, bad]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_TYPES, + "measure_bad_output.jeff", + ) + + +def generate_measurend_bad_first_output() -> None: + """measureNd first output is Int32 instead of Qubit → InvalidOutputType.""" + alloc = qubit_alloc() + bad = JeffOp( + "qubit", + "measureNd", + [alloc.outputs[0]], + [JeffValue(IntType(32)), JeffValue(IntType(1))], + ) + body = JeffRegion(sources=[], targets=[], operations=[alloc, bad]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_TYPES, + "measurend_bad_first_output.jeff", + ) + + +def generate_measurend_bad_second_output() -> None: + """measureNd second output is Float64 instead of Int1 → InvalidOutputType.""" + alloc = qubit_alloc() + bad = JeffOp( + "qubit", + "measureNd", + [alloc.outputs[0]], + [JeffValue(QubitType()), JeffValue(FloatType(64))], + ) + free = qubit_free(bad.outputs[0]) + body = JeffRegion(sources=[], targets=[], operations=[alloc, bad, free]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_TYPES, + "measurend_bad_second_output.jeff", + ) + + +def generate_free_bad_input() -> None: + """free takes Float64 instead of Qubit → InvalidInputType.""" + f = JeffOp("float", "const64", [], [JeffValue(FloatType(64))], 0.0) + bad = JeffOp("qubit", "free", [f.outputs[0]], []) + body = JeffRegion(sources=[], targets=[], operations=[f, bad]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_TYPES, + "free_bad_input.jeff", + ) + + +def generate_gate_bad_qubit_input() -> None: + """gate first input is Float64 instead of Qubit → InvalidInputType.""" + f = JeffOp("float", "const64", [], [JeffValue(FloatType(64))], 1.0) + bad = JeffOp( + "qubit", + "gate", + [f.outputs[0]], + [JeffValue(QubitType())], + CustomGate("bad", 1, 0, 0, False, 1), + ) + body = JeffRegion(sources=[], targets=[], operations=[f, bad]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_TYPES, + "gate_bad_qubit_input.jeff", + ) + + +def generate_gate_bad_qubit_output() -> None: + """gate output is Float64 instead of Qubit → InvalidOutputType.""" + alloc = qubit_alloc() + bad = JeffOp( + "qubit", + "gate", + [alloc.outputs[0]], + [JeffValue(FloatType(64))], + CustomGate("bad", 1, 0, 0, False, 1), + ) + body = JeffRegion(sources=[], targets=[], operations=[alloc, bad]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_TYPES, + "gate_bad_qubit_output.jeff", + ) + + +def generate_gate_bad_param_type() -> None: + """gate float parameter is Int32 instead of Float → InvalidInputType.""" + alloc = qubit_alloc() + c_int = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) + bad = JeffOp( + "qubit", + "gate", + [alloc.outputs[0], c_int.outputs[0]], + [JeffValue(QubitType())], + CustomGate("bad", 1, 1, 0, False, 1), + ) + body = JeffRegion(sources=[], targets=[], operations=[alloc, c_int, bad]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_TYPES, + "gate_bad_param_type.jeff", + ) + + +# ────────────────────────────────────────────── +# Negative: linearity violations +# ────────────────────────────────────────────── + + +def generate_qubit_produced_twice() -> None: + """Same qubit value appears as both body source and op output → LinearValueProducedMultipleTimes.""" + q = JeffValue(QubitType()) + alloc = JeffOp("qubit", "alloc", [], [q]) # op produces q + free = qubit_free(q) # op consumes q + body = JeffRegion(sources=[q], targets=[], operations=[alloc, free]) + # q: producers = 2 (source + alloc output), consumers = 1 (free) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_LINEARITY, + "qubit_produced_twice.jeff", + ) + + +def generate_qubit_consumed_twice() -> None: + """Same qubit value used as input by two ops → LinearValueConsumedMultipleTimes.""" + alloc = qubit_alloc() + meas1 = JeffOp("qubit", "measure", [alloc.outputs[0]], [JeffValue(IntType(1))]) + meas2 = JeffOp("qubit", "measure", [alloc.outputs[0]], [JeffValue(IntType(1))]) + body = JeffRegion(sources=[], targets=[], operations=[alloc, meas1, meas2]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_LINEARITY, + "qubit_consumed_twice.jeff", + ) + + +def generate_qubit_never_consumed() -> None: + """Qubit allocated but never freed or measured → LinearValueNeverConsumed.""" + alloc = qubit_alloc() + body = JeffRegion(sources=[], targets=[], operations=[alloc]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_LINEARITY, + "qubit_never_consumed.jeff", + ) + + +# ────────────────────────────────────────────── +# Negative: isolation / scoping violations +# ────────────────────────────────────────────── + + +def generate_for_captures_outer() -> None: + """For body directly uses a value from the outer scope → IsolationViolation.""" + c10 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) + c20 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 20) + + for_iter = JeffValue(IntType(32)) + for_state = JeffValue(IntType(32)) + bad_add = JeffOp( + "int", "add", [for_state, c10.outputs[0]], [JeffValue(IntType(32))] + ) + # c10.outputs[0] is from the outer region — not a source of this body + for_body = JeffRegion( + sources=[for_iter, for_state], + targets=[bad_add.outputs[0]], + operations=[bad_add], + ) + + for_op = JeffOp( + "scf", + "for", + [c10.outputs[0], c20.outputs[0], c10.outputs[0], c10.outputs[0]], + [JeffValue(IntType(32))], + ForSCF(for_body), + ) + body = JeffRegion(sources=[], targets=[], operations=[c10, c20, for_op]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_SCOPING, + "for_captures_outer.jeff", + ) + + +def generate_while_cond_captures_outer() -> None: + """While condition directly uses an outer value → IsolationViolation.""" + c_outer = JeffOp("int", "const32", [], [JeffValue(IntType(1))], 0) + c_init = JeffOp("int", "const32", [], [JeffValue(IntType(1))], 0) + + cond_src = JeffValue(IntType(1)) + # bad: uses c_outer.outputs[0] which is from the outer region + bad_not = JeffOp("int", "not", [c_outer.outputs[0]], [JeffValue(IntType(1))]) + cond_reg = JeffRegion( + sources=[cond_src], targets=[bad_not.outputs[0]], operations=[bad_not] + ) + + body_src = JeffValue(IntType(1)) + body_not = JeffOp("int", "not", [body_src], [JeffValue(IntType(1))]) + body_reg = JeffRegion( + sources=[body_src], targets=[body_not.outputs[0]], operations=[body_not] + ) + + while_op = JeffOp( + "scf", + "while", + [c_init.outputs[0]], + [JeffValue(IntType(1))], + WhileSCF(cond_reg, body_reg), + ) + body = JeffRegion(sources=[], targets=[], operations=[c_outer, c_init, while_op]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_SCOPING, + "while_cond_captures_outer.jeff", + ) + + +def generate_while_body_captures_outer() -> None: + """While body directly uses an outer value → IsolationViolation.""" + c_outer = JeffOp("int", "const32", [], [JeffValue(IntType(1))], 0) + c_init = JeffOp("int", "const32", [], [JeffValue(IntType(1))], 0) + + cond_src = JeffValue(IntType(1)) + cond_not = JeffOp("int", "not", [cond_src], [JeffValue(IntType(1))]) + cond_reg = JeffRegion( + sources=[cond_src], targets=[cond_not.outputs[0]], operations=[cond_not] + ) + + body_src = JeffValue(IntType(1)) + # bad: uses c_outer.outputs[0] which is from the outer region + bad_not = JeffOp("int", "not", [c_outer.outputs[0]], [JeffValue(IntType(1))]) + body_reg = JeffRegion( + sources=[body_src], targets=[bad_not.outputs[0]], operations=[bad_not] + ) + + while_op = JeffOp( + "scf", + "while", + [c_init.outputs[0]], + [JeffValue(IntType(1))], + WhileSCF(cond_reg, body_reg), + ) + body = JeffRegion(sources=[], targets=[], operations=[c_outer, c_init, while_op]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_SCOPING, + "while_body_captures_outer.jeff", + ) + + +def generate_dowhile_body_captures_outer() -> None: + """DoWhile body directly uses an outer value → IsolationViolation.""" + c_outer = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 99) + c_init = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 0) + + dw_src = JeffValue(IntType(32)) + # bad: uses c_outer.outputs[0] which is from the outer region + bad_add = JeffOp( + "int", "add", [dw_src, c_outer.outputs[0]], [JeffValue(IntType(32))] + ) + dw_body = JeffRegion( + sources=[dw_src], targets=[bad_add.outputs[0]], operations=[bad_add] + ) + + cond_src = JeffValue(IntType(32)) + cond_c = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 5) + cond_eq = JeffOp( + "int", "eq", [cond_src, cond_c.outputs[0]], [JeffValue(IntType(1))] + ) + dw_cond = JeffRegion( + sources=[cond_src], targets=[cond_eq.outputs[0]], operations=[cond_c, cond_eq] + ) + + dw_op = JeffOp( + "scf", + "doWhile", + [c_init.outputs[0]], + [JeffValue(IntType(32))], + DoWhileSCF(dw_body, dw_cond), + ) + body = JeffRegion(sources=[], targets=[], operations=[c_outer, c_init, dw_op]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_SCOPING, + "dowhile_body_captures_outer.jeff", + ) + + +def generate_dowhile_cond_captures_outer() -> None: + """DoWhile condition directly uses an outer value → IsolationViolation.""" + c_outer = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 5) + c_init = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 0) + + dw_src = JeffValue(IntType(32)) + dw_c1 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) + dw_add = JeffOp("int", "add", [dw_src, dw_c1.outputs[0]], [JeffValue(IntType(32))]) + dw_body = JeffRegion( + sources=[dw_src], targets=[dw_add.outputs[0]], operations=[dw_c1, dw_add] + ) + + cond_src = JeffValue(IntType(32)) + # bad: uses c_outer.outputs[0] which is from the outer region + bad_eq = JeffOp( + "int", "eq", [cond_src, c_outer.outputs[0]], [JeffValue(IntType(1))] + ) + dw_cond = JeffRegion( + sources=[cond_src], targets=[bad_eq.outputs[0]], operations=[bad_eq] + ) + + dw_op = JeffOp( + "scf", + "doWhile", + [c_init.outputs[0]], + [JeffValue(IntType(32))], + DoWhileSCF(dw_body, dw_cond), + ) + body = JeffRegion(sources=[], targets=[], operations=[c_outer, c_init, dw_op]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_SCOPING, + "dowhile_cond_captures_outer.jeff", + ) + + +def generate_switch_captures_outer() -> None: + """Switch branch directly uses an outer value → IsolationViolation.""" + c_outer = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 99) + c_idx = JeffOp("int", "const32", [], [JeffValue(IntType(1))], 0) + c_state = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) + + b0_src = JeffValue(IntType(32)) + # bad: uses c_outer.outputs[0] which is from the outer region + bad_add = JeffOp( + "int", "add", [b0_src, c_outer.outputs[0]], [JeffValue(IntType(32))] + ) + branch0 = JeffRegion( + sources=[b0_src], targets=[bad_add.outputs[0]], operations=[bad_add] + ) + + def_src = JeffValue(IntType(32)) + default = JeffRegion(sources=[def_src], targets=[def_src], operations=[]) + + sw_op = JeffOp( + "scf", + "switch", + [c_idx.outputs[0], c_state.outputs[0]], + [JeffValue(IntType(32))], + SwitchSCF([branch0], default), + ) + body = JeffRegion( + sources=[], targets=[], operations=[c_outer, c_idx, c_state, sw_op] + ) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_SCOPING, + "switch_captures_outer.jeff", + ) + + +def generate_nested_captures_grandparent() -> None: + """Inner for body uses a value from the outer function scope (grandparent) → IsolationViolation.""" + c10 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) + c20 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 20) + c1 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) + + inner_iter = JeffValue(IntType(32)) + inner_state = JeffValue(IntType(32)) + # bad: c10.outputs[0] is from the grandparent scope (outer function body) + bad_add = JeffOp( + "int", "add", [inner_state, c10.outputs[0]], [JeffValue(IntType(32))] + ) + inner_body = JeffRegion( + sources=[inner_iter, inner_state], + targets=[bad_add.outputs[0]], + operations=[bad_add], + ) + + outer_iter = JeffValue(IntType(32)) + outer_state = JeffValue(IntType(32)) + oc0 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 0) + oc10 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) + oc1 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) + inner_for = JeffOp( + "scf", + "for", + [oc0.outputs[0], oc10.outputs[0], oc1.outputs[0], outer_state], + [JeffValue(IntType(32))], + ForSCF(inner_body), + ) + outer_body = JeffRegion( + sources=[outer_iter, outer_state], + targets=[inner_for.outputs[0]], + operations=[oc0, oc10, oc1, inner_for], + ) + + outer_for = JeffOp( + "scf", + "for", + [c10.outputs[0], c20.outputs[0], c1.outputs[0], c10.outputs[0]], + [JeffValue(IntType(32))], + ForSCF(outer_body), + ) + body = JeffRegion(sources=[], targets=[], operations=[c10, c20, c1, outer_for]) + _write( + JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), + NEG_SCOPING, + "nested_captures_grandparent.jeff", + ) + + +# ────────────────────────────────────────────── +# Entry point +# ────────────────────────────────────────────── + + +if __name__ == "__main__": + POSITIVE_DIR.mkdir(exist_ok=True) + for d in (NEG_MODULE, NEG_ORDERING, NEG_TYPES, NEG_LINEARITY, NEG_SCOPING): + d.mkdir(parents=True, exist_ok=True) + + generate_valid_comprehensive() + generate_valid_minimal() + generate_valid_deeply_nested() + + generate_missing_version() + generate_entrypoint_oob() + generate_no_functions() + + generate_use_before_define_outer() + generate_use_before_define_for() + generate_use_before_define_while_cond() + generate_use_before_define_while_body() + generate_use_before_define_dowhile_body() + generate_use_before_define_dowhile_cond() + generate_use_before_define_switch() + + generate_int_add_mixed_bitwidths() + generate_int_compare_mixed_bitwidths() + generate_int_compare_bad_output() + generate_int_unary_bad_output() + generate_float_add_mixed_precisions() + generate_float_compare_mixed_precisions() + generate_float_compare_bad_output() + generate_alloc_bad_output() + generate_measure_bad_input() + generate_measure_bad_output() + generate_measurend_bad_first_output() + generate_measurend_bad_second_output() + generate_free_bad_input() + generate_gate_bad_qubit_input() + generate_gate_bad_qubit_output() + generate_gate_bad_param_type() + + generate_qubit_produced_twice() + generate_qubit_consumed_twice() + generate_qubit_never_consumed() + + generate_for_captures_outer() + generate_while_cond_captures_outer() + generate_while_body_captures_outer() + generate_dowhile_body_captures_outer() + generate_dowhile_cond_captures_outer() + generate_switch_captures_outer() + generate_nested_captures_grandparent() + + print("done") diff --git a/tools/verifier/tests/negative/encode/bounds/nested_source_oob.txt b/tools/verifier/tests/negative/encode/bounds/nested_source_oob.txt new file mode 100644 index 0000000..73a1a2f --- /dev/null +++ b/tools/verifier/tests/negative/encode/bounds/nested_source_oob.txt @@ -0,0 +1,32 @@ +( version = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [], + operations = [ + ( inputs = [], + outputs = [0], + instruction = (int = (const32 = 10)) ), + ( inputs = [0, 0, 0, 0], + outputs = [1], + instruction = ( + scf = ( + for = ( + sources = [99], + targets = [2], + operations = [ + ( inputs = [], + outputs = [2], + instruction = (int = (const32 = 1)) ) ] ) ) ) ) ] ), + values = [ + (type = (int = 32)), + (type = (int = 32)), + (type = (int = 32)) ] ) ) ], + strings = ["f"], + entrypoint = 0, + tool = "", + toolVersion = "", + versionMinor = 2, + versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/bounds/nested_target_oob.txt b/tools/verifier/tests/negative/encode/bounds/nested_target_oob.txt new file mode 100644 index 0000000..e165e1e --- /dev/null +++ b/tools/verifier/tests/negative/encode/bounds/nested_target_oob.txt @@ -0,0 +1,32 @@ +( version = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [], + operations = [ + ( inputs = [], + outputs = [0], + instruction = (int = (const32 = 10)) ), + ( inputs = [0, 0, 0, 0], + outputs = [1], + instruction = ( + scf = ( + for = ( + sources = [2], + targets = [99], + operations = [ + ( inputs = [], + outputs = [2], + instruction = (int = (const32 = 1)) ) ] ) ) ) ) ] ), + values = [ + (type = (int = 32)), + (type = (int = 32)), + (type = (int = 32)) ] ) ) ], + strings = ["f"], + entrypoint = 0, + tool = "", + toolVersion = "", + versionMinor = 2, + versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/bounds/op_input_oob.txt b/tools/verifier/tests/negative/encode/bounds/op_input_oob.txt new file mode 100644 index 0000000..16f9d96 --- /dev/null +++ b/tools/verifier/tests/negative/encode/bounds/op_input_oob.txt @@ -0,0 +1,23 @@ +( version = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [], + operations = [ + ( inputs = [], + outputs = [0], + instruction = (int = (const32 = 10)) ), + ( inputs = [0, 2], + outputs = [1], + instruction = (int = (add = void)) ) ] ), + values = [ + (type = (int = 32)), + (type = (int = 32)) ] ) ) ], + strings = ["f"], + entrypoint = 0, + tool = "", + toolVersion = "", + versionMinor = 2, + versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/bounds/op_output_oob.txt b/tools/verifier/tests/negative/encode/bounds/op_output_oob.txt new file mode 100644 index 0000000..e2f6755 --- /dev/null +++ b/tools/verifier/tests/negative/encode/bounds/op_output_oob.txt @@ -0,0 +1,19 @@ +( version = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [], + operations = [ + ( inputs = [], + outputs = [1], + instruction = (int = (const32 = 10)) ) ] ), + values = [ + (type = (int = 32)) ] ) ) ], + strings = ["f"], + entrypoint = 0, + tool = "", + toolVersion = "", + versionMinor = 2, + versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/bounds/region_source_oob.txt b/tools/verifier/tests/negative/encode/bounds/region_source_oob.txt new file mode 100644 index 0000000..4c3d9a2 --- /dev/null +++ b/tools/verifier/tests/negative/encode/bounds/region_source_oob.txt @@ -0,0 +1,20 @@ +( version = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [5], + targets = [], + operations = [ + ( inputs = [], + outputs = [0], + instruction = (int = (const32 = 10)) ) ] ), + values = [ + (type = (int = 32)), + (type = (int = 32)) ] ) ) ], + strings = ["f"], + entrypoint = 0, + tool = "", + toolVersion = "", + versionMinor = 2, + versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/bounds/region_target_oob.txt b/tools/verifier/tests/negative/encode/bounds/region_target_oob.txt new file mode 100644 index 0000000..1c7b0b0 --- /dev/null +++ b/tools/verifier/tests/negative/encode/bounds/region_target_oob.txt @@ -0,0 +1,20 @@ +( version = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [5], + operations = [ + ( inputs = [], + outputs = [0], + instruction = (int = (const32 = 10)) ) ] ), + values = [ + (type = (int = 32)), + (type = (int = 32)) ] ) ) ], + strings = ["f"], + entrypoint = 0, + tool = "", + toolVersion = "", + versionMinor = 2, + versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/module/entrypoint_is_declaration.txt b/tools/verifier/tests/negative/encode/module/entrypoint_is_declaration.txt new file mode 100644 index 0000000..f194cb8 --- /dev/null +++ b/tools/verifier/tests/negative/encode/module/entrypoint_is_declaration.txt @@ -0,0 +1,12 @@ +( version = 0, + functions = [ + ( name = 0, + declaration = ( + inputs = [], + outputs = [] ) ) ], + strings = ["f"], + entrypoint = 0, + tool = "", + toolVersion = "", + versionMinor = 2, + versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/alloc_unexpected_input.txt b/tools/verifier/tests/negative/encode/types/alloc_unexpected_input.txt new file mode 100644 index 0000000..0c15883 --- /dev/null +++ b/tools/verifier/tests/negative/encode/types/alloc_unexpected_input.txt @@ -0,0 +1,23 @@ +( version = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [], + operations = [ + ( inputs = [], + outputs = [0], + instruction = (int = (const32 = 0)) ), + ( inputs = [0], + outputs = [1], + instruction = (qubit = (alloc = void)) ) ] ), + values = [ + (type = (int = 32)), + (type = (qubit = void)) ] ) ) ], + strings = ["f"], + entrypoint = 0, + tool = "", + toolVersion = "", + versionMinor = 2, + versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/free_unexpected_output.txt b/tools/verifier/tests/negative/encode/types/free_unexpected_output.txt new file mode 100644 index 0000000..7cdf88e --- /dev/null +++ b/tools/verifier/tests/negative/encode/types/free_unexpected_output.txt @@ -0,0 +1,23 @@ +( version = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [], + operations = [ + ( inputs = [], + outputs = [0], + instruction = (qubit = (alloc = void)) ), + ( inputs = [0], + outputs = [1], + instruction = (qubit = (free = void)) ) ] ), + values = [ + (type = (qubit = void)), + (type = (int = 32)) ] ) ) ], + strings = ["f"], + entrypoint = 0, + tool = "", + toolVersion = "", + versionMinor = 2, + versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/gate_missing_param_input.txt b/tools/verifier/tests/negative/encode/types/gate_missing_param_input.txt new file mode 100644 index 0000000..d7c326e --- /dev/null +++ b/tools/verifier/tests/negative/encode/types/gate_missing_param_input.txt @@ -0,0 +1,29 @@ +( version = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [], + operations = [ + ( inputs = [], + outputs = [0], + instruction = (qubit = (alloc = void)) ), + ( inputs = [0], + outputs = [1], + instruction = ( + qubit = ( + gate = ( + custom = (name = 0, numQubits = 1, numParams = 1), + controlQubits = 0, + adjoint = false, + power = 1 ) ) ) ) ] ), + values = [ + (type = (qubit = void)), + (type = (qubit = void)) ] ) ) ], + strings = ["rz"], + entrypoint = 0, + tool = "", + toolVersion = "", + versionMinor = 2, + versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/gate_too_few_qubit_inputs.txt b/tools/verifier/tests/negative/encode/types/gate_too_few_qubit_inputs.txt new file mode 100644 index 0000000..0214ed6 --- /dev/null +++ b/tools/verifier/tests/negative/encode/types/gate_too_few_qubit_inputs.txt @@ -0,0 +1,30 @@ +( version = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [], + operations = [ + ( inputs = [], + outputs = [0], + instruction = (qubit = (alloc = void)) ), + ( inputs = [0], + outputs = [1, 2], + instruction = ( + qubit = ( + gate = ( + custom = (name = 0, numQubits = 2, numParams = 0), + controlQubits = 0, + adjoint = false, + power = 1 ) ) ) ) ] ), + values = [ + (type = (qubit = void)), + (type = (qubit = void)), + (type = (qubit = void)) ] ) ) ], + strings = ["bad2q"], + entrypoint = 0, + tool = "", + toolVersion = "", + versionMinor = 2, + versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/gate_wrong_output_count.txt b/tools/verifier/tests/negative/encode/types/gate_wrong_output_count.txt new file mode 100644 index 0000000..0392aeb --- /dev/null +++ b/tools/verifier/tests/negative/encode/types/gate_wrong_output_count.txt @@ -0,0 +1,33 @@ +( version = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [], + operations = [ + ( inputs = [], + outputs = [0], + instruction = (qubit = (alloc = void)) ), + ( inputs = [], + outputs = [1], + instruction = (qubit = (alloc = void)) ), + ( inputs = [0, 1], + outputs = [2], + instruction = ( + qubit = ( + gate = ( + custom = (name = 0, numQubits = 2, numParams = 0), + controlQubits = 0, + adjoint = false, + power = 1 ) ) ) ) ] ), + values = [ + (type = (qubit = void)), + (type = (qubit = void)), + (type = (qubit = void)) ] ) ) ], + strings = ["bad2q"], + entrypoint = 0, + tool = "", + toolVersion = "", + versionMinor = 2, + versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/qureg_alloc_bad_input.txt b/tools/verifier/tests/negative/encode/types/qureg_alloc_bad_input.txt new file mode 100644 index 0000000..7148b91 --- /dev/null +++ b/tools/verifier/tests/negative/encode/types/qureg_alloc_bad_input.txt @@ -0,0 +1,23 @@ +( version = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [], + operations = [ + ( inputs = [], + outputs = [0], + instruction = (float = (const64 = 5)) ), + ( inputs = [0], + outputs = [1], + instruction = (qureg = (alloc = void)) ) ] ), + values = [ + (type = (float = float64)), + (type = (qureg = (dynamic = void))) ] ) ) ], + strings = ["f"], + entrypoint = 0, + tool = "", + toolVersion = "", + versionMinor = 2, + versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/qureg_alloc_bad_output.txt b/tools/verifier/tests/negative/encode/types/qureg_alloc_bad_output.txt new file mode 100644 index 0000000..8f127a3 --- /dev/null +++ b/tools/verifier/tests/negative/encode/types/qureg_alloc_bad_output.txt @@ -0,0 +1,23 @@ +( version = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [], + operations = [ + ( inputs = [], + outputs = [0], + instruction = (int = (const32 = 5)) ), + ( inputs = [0], + outputs = [1], + instruction = (qureg = (alloc = void)) ) ] ), + values = [ + (type = (int = 32)), + (type = (qubit = void)) ] ) ) ], + strings = ["f"], + entrypoint = 0, + tool = "", + toolVersion = "", + versionMinor = 2, + versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/qureg_extract_index_bad_idx_input.txt b/tools/verifier/tests/negative/encode/types/qureg_extract_index_bad_idx_input.txt new file mode 100644 index 0000000..c037c9f --- /dev/null +++ b/tools/verifier/tests/negative/encode/types/qureg_extract_index_bad_idx_input.txt @@ -0,0 +1,32 @@ +( version = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [], + operations = [ + ( inputs = [], + outputs = [0], + instruction = (int = (const32 = 1)) ), + ( inputs = [], + outputs = [1], + instruction = (int = (const64 = 0)) ), + ( inputs = [0], + outputs = [2], + instruction = (qureg = (alloc = void)) ), + ( inputs = [2, 1], + outputs = [3, 4], + instruction = (qureg = (extractIndex = void)) ) ] ), + values = [ + (type = (int = 32)), + (type = (int = 64)), + (type = (qureg = (dynamic = void))), + (type = (qureg = (dynamic = void))), + (type = (qubit = void)) ] ) ) ], + strings = ["f"], + entrypoint = 0, + tool = "", + toolVersion = "", + versionMinor = 2, + versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/qureg_extract_index_bad_qubit_output.txt b/tools/verifier/tests/negative/encode/types/qureg_extract_index_bad_qubit_output.txt new file mode 100644 index 0000000..fc3b414 --- /dev/null +++ b/tools/verifier/tests/negative/encode/types/qureg_extract_index_bad_qubit_output.txt @@ -0,0 +1,32 @@ +( version = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [], + operations = [ + ( inputs = [], + outputs = [0], + instruction = (int = (const32 = 1)) ), + ( inputs = [], + outputs = [1], + instruction = (int = (const32 = 0)) ), + ( inputs = [0], + outputs = [2], + instruction = (qureg = (alloc = void)) ), + ( inputs = [2, 1], + outputs = [3, 4], + instruction = (qureg = (extractIndex = void)) ) ] ), + values = [ + (type = (int = 32)), + (type = (int = 32)), + (type = (qureg = (dynamic = void))), + (type = (qureg = (dynamic = void))), + (type = (int = 32)) ] ) ) ], + strings = ["f"], + entrypoint = 0, + tool = "", + toolVersion = "", + versionMinor = 2, + versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/qureg_extract_index_bad_reg_input.txt b/tools/verifier/tests/negative/encode/types/qureg_extract_index_bad_reg_input.txt new file mode 100644 index 0000000..f5f857b --- /dev/null +++ b/tools/verifier/tests/negative/encode/types/qureg_extract_index_bad_reg_input.txt @@ -0,0 +1,28 @@ +( version = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [], + operations = [ + ( inputs = [], + outputs = [0], + instruction = (int = (const32 = 0)) ), + ( inputs = [], + outputs = [1], + instruction = (qubit = (alloc = void)) ), + ( inputs = [1, 0], + outputs = [2, 3], + instruction = (qureg = (extractIndex = void)) ) ] ), + values = [ + (type = (int = 32)), + (type = (qubit = void)), + (type = (qureg = (dynamic = void))), + (type = (qubit = void)) ] ) ) ], + strings = ["f"], + entrypoint = 0, + tool = "", + toolVersion = "", + versionMinor = 2, + versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/qureg_free_bad_input.txt b/tools/verifier/tests/negative/encode/types/qureg_free_bad_input.txt new file mode 100644 index 0000000..c19c950 --- /dev/null +++ b/tools/verifier/tests/negative/encode/types/qureg_free_bad_input.txt @@ -0,0 +1,22 @@ +( version = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [], + operations = [ + ( inputs = [], + outputs = [0], + instruction = (qubit = (alloc = void)) ), + ( inputs = [0], + outputs = [], + instruction = (qureg = (free = void)) ) ] ), + values = [ + (type = (qubit = void)) ] ) ) ], + strings = ["f"], + entrypoint = 0, + tool = "", + toolVersion = "", + versionMinor = 2, + versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/qureg_insert_index_bad_qubit_input.txt b/tools/verifier/tests/negative/encode/types/qureg_insert_index_bad_qubit_input.txt new file mode 100644 index 0000000..f1de8a5 --- /dev/null +++ b/tools/verifier/tests/negative/encode/types/qureg_insert_index_bad_qubit_input.txt @@ -0,0 +1,35 @@ +( version = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [], + operations = [ + ( inputs = [], + outputs = [0], + instruction = (int = (const32 = 1)) ), + ( inputs = [], + outputs = [1], + instruction = (int = (const32 = 0)) ), + ( inputs = [], + outputs = [2], + instruction = (int = (const32 = 42)) ), + ( inputs = [0], + outputs = [3], + instruction = (qureg = (alloc = void)) ), + ( inputs = [3, 1, 2], + outputs = [4], + instruction = (qureg = (insertIndex = void)) ) ] ), + values = [ + (type = (int = 32)), + (type = (int = 32)), + (type = (int = 32)), + (type = (qureg = (dynamic = void))), + (type = (qureg = (dynamic = void))) ] ) ) ], + strings = ["f"], + entrypoint = 0, + tool = "", + toolVersion = "", + versionMinor = 2, + versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/qureg_join_bad_input.txt b/tools/verifier/tests/negative/encode/types/qureg_join_bad_input.txt new file mode 100644 index 0000000..2312f98 --- /dev/null +++ b/tools/verifier/tests/negative/encode/types/qureg_join_bad_input.txt @@ -0,0 +1,31 @@ +( version = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [], + operations = [ + ( inputs = [], + outputs = [0], + instruction = (int = (const32 = 1)) ), + ( inputs = [0], + outputs = [1], + instruction = (qureg = (alloc = void)) ), + ( inputs = [], + outputs = [2], + instruction = (qubit = (alloc = void)) ), + ( inputs = [1, 2], + outputs = [3], + instruction = (qureg = (join = void)) ) ] ), + values = [ + (type = (int = 32)), + (type = (qureg = (dynamic = void))), + (type = (qubit = void)), + (type = (qureg = (dynamic = void))) ] ) ) ], + strings = ["f"], + entrypoint = 0, + tool = "", + toolVersion = "", + versionMinor = 2, + versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/qureg_length_bad_output.txt b/tools/verifier/tests/negative/encode/types/qureg_length_bad_output.txt new file mode 100644 index 0000000..501eab6 --- /dev/null +++ b/tools/verifier/tests/negative/encode/types/qureg_length_bad_output.txt @@ -0,0 +1,28 @@ +( version = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [], + operations = [ + ( inputs = [], + outputs = [0], + instruction = (int = (const32 = 3)) ), + ( inputs = [0], + outputs = [1], + instruction = (qureg = (alloc = void)) ), + ( inputs = [1], + outputs = [2, 3], + instruction = (qureg = (length = void)) ) ] ), + values = [ + (type = (int = 32)), + (type = (qureg = (dynamic = void))), + (type = (qureg = (dynamic = void))), + (type = (int = 64)) ] ) ) ], + strings = ["f"], + entrypoint = 0, + tool = "", + toolVersion = "", + versionMinor = 2, + versionPatch = 0 ) diff --git a/tools/verifier/tests/negative_attrs.rs b/tools/verifier/tests/negative_attrs.rs new file mode 100644 index 0000000..3789bdf --- /dev/null +++ b/tools/verifier/tests/negative_attrs.rs @@ -0,0 +1,50 @@ +#![allow(missing_docs)] +use jeff::reader::ReadJeff; +use jeff::Jeff; +use std::fs::File; +use std::path::Path; +use verifier::{verify_module, VerificationError}; + +fn load(name: &str) -> Vec { + let path = Path::new(env!("CARGO_MANIFEST_DIR")) + .join("tests/negative/module") + .join(name); + let file = File::open(&path) + .unwrap_or_else(|_| panic!("missing fixture: {path:?} — run generate_test_cases.py first")); + verify_module( + Jeff::read(file) + .expect("failed to parse jeff file") + .module(), + ) +} + +#[test] +fn missing_version() { + let errors = load("missing_version.jeff"); + assert!( + errors.contains(&VerificationError::MissingVersion), + "expected MissingVersion, got: {errors:?}" + ); +} + +#[test] +fn entrypoint_oob() { + let errors = load("entrypoint_oob.jeff"); + assert!( + errors.contains(&VerificationError::InvalidEntrypoint), + "expected InvalidEntrypoint, got: {errors:?}" + ); +} + +#[test] +fn no_functions_gives_both_errors() { + let errors = load("no_functions.jeff"); + assert!( + errors.contains(&VerificationError::MissingVersion), + "expected MissingVersion in {errors:?}" + ); + assert!( + errors.contains(&VerificationError::InvalidEntrypoint), + "expected InvalidEntrypoint in {errors:?}" + ); +} diff --git a/tools/verifier/tests/negative_bounds.rs b/tools/verifier/tests/negative_bounds.rs new file mode 100644 index 0000000..698e452 --- /dev/null +++ b/tools/verifier/tests/negative_bounds.rs @@ -0,0 +1,77 @@ +#![allow(missing_docs)] +use jeff::reader::ReadJeff; +use jeff::Jeff; +use std::fs::File; +use std::path::Path; +use verifier::{verify_module, VerificationError}; + +fn load_bounds(name: &str) -> Vec { + let path = Path::new(env!("CARGO_MANIFEST_DIR")) + .join("tests/negative/bounds") + .join(name); + let file = File::open(&path).unwrap_or_else(|_| panic!("missing fixture: {path:?}")); + verify_module( + Jeff::read(file) + .expect("failed to parse jeff file") + .module(), + ) +} + +fn load_module(name: &str) -> Vec { + let path = Path::new(env!("CARGO_MANIFEST_DIR")) + .join("tests/negative/module") + .join(name); + let file = File::open(&path).unwrap_or_else(|_| panic!("missing fixture: {path:?}")); + verify_module( + Jeff::read(file) + .expect("failed to parse jeff file") + .module(), + ) +} + +fn has_oob(errors: &[VerificationError]) -> bool { + errors + .iter() + .any(|e| matches!(e, VerificationError::ValueOutOfBounds { .. })) +} + +#[test] +fn op_input_oob() { + assert!(has_oob(&load_bounds("op_input_oob.jeff"))); +} + +#[test] +fn op_output_oob() { + assert!(has_oob(&load_bounds("op_output_oob.jeff"))); +} + +#[test] +fn region_source_oob() { + assert!(has_oob(&load_bounds("region_source_oob.jeff"))); +} + +#[test] +fn region_target_oob() { + assert!(has_oob(&load_bounds("region_target_oob.jeff"))); +} + +#[test] +fn nested_source_oob() { + assert!(has_oob(&load_bounds("nested_source_oob.jeff"))); +} + +#[test] +fn nested_target_oob() { + assert!(has_oob(&load_bounds("nested_target_oob.jeff"))); +} + +#[test] +fn entrypoint_is_declaration() { + let errors = load_module("entrypoint_is_declaration.jeff"); + assert!( + errors + .iter() + .any(|e| matches!(e, VerificationError::InvalidEntrypoint)), + "expected InvalidEntrypoint, got: {errors:?}" + ); +} diff --git a/tools/verifier/tests/negative_linearity.rs b/tools/verifier/tests/negative_linearity.rs new file mode 100644 index 0000000..896d21c --- /dev/null +++ b/tools/verifier/tests/negative_linearity.rs @@ -0,0 +1,54 @@ +#![allow(missing_docs)] +use jeff::reader::ReadJeff; +use jeff::Jeff; +use std::fs::File; +use std::path::Path; +use verifier::{verify_module, VerificationError}; + +fn load(name: &str) -> Vec { + let path = Path::new(env!("CARGO_MANIFEST_DIR")) + .join("tests/negative/linearity") + .join(name); + let file = File::open(&path) + .unwrap_or_else(|_| panic!("missing fixture: {path:?} — run generate_test_cases.py first")); + verify_module( + Jeff::read(file) + .expect("failed to parse jeff file") + .module(), + ) +} + +#[test] +fn qubit_produced_twice() { + let errors = load("qubit_produced_twice.jeff"); + assert!( + errors.iter().any(|e| matches!( + e, + VerificationError::LinearValueProducedMultipleTimes { .. } + )), + "expected LinearValueProducedMultipleTimes, got: {errors:?}" + ); +} + +#[test] +fn qubit_consumed_twice() { + let errors = load("qubit_consumed_twice.jeff"); + assert!( + errors.iter().any(|e| matches!( + e, + VerificationError::LinearValueConsumedMultipleTimes { .. } + )), + "expected LinearValueConsumedMultipleTimes, got: {errors:?}" + ); +} + +#[test] +fn qubit_never_consumed() { + let errors = load("qubit_never_consumed.jeff"); + assert!( + errors + .iter() + .any(|e| matches!(e, VerificationError::LinearValueNeverConsumed { .. })), + "expected LinearValueNeverConsumed, got: {errors:?}" + ); +} diff --git a/tools/verifier/tests/negative_ordering.rs b/tools/verifier/tests/negative_ordering.rs new file mode 100644 index 0000000..05ec6a8 --- /dev/null +++ b/tools/verifier/tests/negative_ordering.rs @@ -0,0 +1,60 @@ +#![allow(missing_docs)] +use jeff::reader::ReadJeff; +use jeff::Jeff; +use std::fs::File; +use std::path::Path; +use verifier::{verify_module, VerificationError}; + +fn load(name: &str) -> Vec { + let path = Path::new(env!("CARGO_MANIFEST_DIR")) + .join("tests/negative/ordering") + .join(name); + let file = File::open(&path) + .unwrap_or_else(|_| panic!("missing fixture: {path:?} — run generate_test_cases.py first")); + verify_module( + Jeff::read(file) + .expect("failed to parse jeff file") + .module(), + ) +} + +fn has_ubd(errors: &[VerificationError]) -> bool { + errors + .iter() + .any(|e| matches!(e, VerificationError::UsedBeforeDefined { .. })) +} + +#[test] +fn use_before_define_outer() { + assert!(has_ubd(&load("use_before_define_outer.jeff"))); +} + +#[test] +fn use_before_define_for_body() { + assert!(has_ubd(&load("use_before_define_for.jeff"))); +} + +#[test] +fn use_before_define_while_condition() { + assert!(has_ubd(&load("use_before_define_while_cond.jeff"))); +} + +#[test] +fn use_before_define_while_body() { + assert!(has_ubd(&load("use_before_define_while_body.jeff"))); +} + +#[test] +fn use_before_define_dowhile_body() { + assert!(has_ubd(&load("use_before_define_dowhile_body.jeff"))); +} + +#[test] +fn use_before_define_dowhile_condition() { + assert!(has_ubd(&load("use_before_define_dowhile_cond.jeff"))); +} + +#[test] +fn use_before_define_switch_branch() { + assert!(has_ubd(&load("use_before_define_switch.jeff"))); +} diff --git a/tools/verifier/tests/negative_scoping.rs b/tools/verifier/tests/negative_scoping.rs new file mode 100644 index 0000000..4db4196 --- /dev/null +++ b/tools/verifier/tests/negative_scoping.rs @@ -0,0 +1,60 @@ +#![allow(missing_docs)] +use jeff::reader::ReadJeff; +use jeff::Jeff; +use std::fs::File; +use std::path::Path; +use verifier::{verify_module, VerificationError}; + +fn load(name: &str) -> Vec { + let path = Path::new(env!("CARGO_MANIFEST_DIR")) + .join("tests/negative/scoping") + .join(name); + let file = File::open(&path) + .unwrap_or_else(|_| panic!("missing fixture: {path:?} — run generate_test_cases.py first")); + verify_module( + Jeff::read(file) + .expect("failed to parse jeff file") + .module(), + ) +} + +fn has_isolation(errors: &[VerificationError]) -> bool { + errors + .iter() + .any(|e| matches!(e, VerificationError::IsolationViolation { .. })) +} + +#[test] +fn for_body_captures_outer() { + assert!(has_isolation(&load("for_captures_outer.jeff"))); +} + +#[test] +fn while_condition_captures_outer() { + assert!(has_isolation(&load("while_cond_captures_outer.jeff"))); +} + +#[test] +fn while_body_captures_outer() { + assert!(has_isolation(&load("while_body_captures_outer.jeff"))); +} + +#[test] +fn dowhile_body_captures_outer() { + assert!(has_isolation(&load("dowhile_body_captures_outer.jeff"))); +} + +#[test] +fn dowhile_condition_captures_outer() { + assert!(has_isolation(&load("dowhile_cond_captures_outer.jeff"))); +} + +#[test] +fn switch_branch_captures_outer() { + assert!(has_isolation(&load("switch_captures_outer.jeff"))); +} + +#[test] +fn nested_for_captures_grandparent() { + assert!(has_isolation(&load("nested_captures_grandparent.jeff"))); +} diff --git a/tools/verifier/tests/negative_types.rs b/tools/verifier/tests/negative_types.rs new file mode 100644 index 0000000..d9394e4 --- /dev/null +++ b/tools/verifier/tests/negative_types.rs @@ -0,0 +1,213 @@ +#![allow(missing_docs)] +use jeff::reader::ReadJeff; +use jeff::Jeff; +use std::fs::File; +use std::path::Path; +use verifier::{verify_module, VerificationError}; + +fn load(name: &str) -> Vec { + let path = Path::new(env!("CARGO_MANIFEST_DIR")) + .join("tests/negative/types") + .join(name); + let file = File::open(&path) + .unwrap_or_else(|_| panic!("missing fixture: {path:?} — run generate_test_cases.py first")); + verify_module( + Jeff::read(file) + .expect("failed to parse jeff file") + .module(), + ) +} + +fn has_mismatch(errors: &[VerificationError]) -> bool { + errors + .iter() + .any(|e| matches!(e, VerificationError::TypeMismatch { .. })) +} + +fn has_bad_input(errors: &[VerificationError]) -> bool { + errors + .iter() + .any(|e| matches!(e, VerificationError::InvalidInputType { .. })) +} + +fn has_bad_output(errors: &[VerificationError]) -> bool { + errors + .iter() + .any(|e| matches!(e, VerificationError::InvalidOutputType { .. })) +} + +// ── int ────────────────────────────────────── + +#[test] +fn int_add_mixed_bitwidths() { + assert!(has_mismatch(&load("int_add_mixed_bitwidths.jeff"))); +} + +#[test] +fn int_compare_mixed_bitwidths() { + assert!(has_mismatch(&load("int_compare_mixed_bitwidths.jeff"))); +} + +#[test] +fn int_compare_bad_output_type() { + assert!(has_bad_output(&load("int_compare_bad_output.jeff"))); +} + +#[test] +fn int_unary_output_type_mismatch() { + assert!(has_mismatch(&load("int_unary_bad_output.jeff"))); +} + +// ── float ──────────────────────────────────── + +#[test] +fn float_add_mixed_precisions() { + assert!(has_mismatch(&load("float_add_mixed_precisions.jeff"))); +} + +#[test] +fn float_compare_mixed_precisions() { + assert!(has_mismatch(&load("float_compare_mixed_precisions.jeff"))); +} + +#[test] +fn float_compare_bad_output_type() { + assert!(has_bad_output(&load("float_compare_bad_output.jeff"))); +} + +// ── qubit ──────────────────────────────────── + +#[test] +fn alloc_bad_output_type() { + assert!(has_bad_output(&load("alloc_bad_output.jeff"))); +} + +#[test] +fn measure_bad_input_type() { + assert!(has_bad_input(&load("measure_bad_input.jeff"))); +} + +#[test] +fn measure_bad_output_type() { + assert!(has_bad_output(&load("measure_bad_output.jeff"))); +} + +#[test] +fn measurend_bad_first_output() { + assert!(has_bad_output(&load("measurend_bad_first_output.jeff"))); +} + +#[test] +fn measurend_bad_second_output() { + assert!(has_bad_output(&load("measurend_bad_second_output.jeff"))); +} + +#[test] +fn free_bad_input_type() { + assert!(has_bad_input(&load("free_bad_input.jeff"))); +} + +#[test] +fn gate_non_qubit_input() { + assert!(has_bad_input(&load("gate_bad_qubit_input.jeff"))); +} + +#[test] +fn gate_non_qubit_output() { + assert!(has_bad_output(&load("gate_bad_qubit_output.jeff"))); +} + +#[test] +fn gate_non_float_param() { + assert!(has_bad_input(&load("gate_bad_param_type.jeff"))); +} + +// ── qubit alloc / free / reset ──────────────── + +#[test] +fn alloc_has_unexpected_input() { + assert!(has_bad_input(&load("alloc_unexpected_input.jeff"))); +} + +#[test] +fn free_has_unexpected_output() { + assert!(has_bad_output(&load("free_unexpected_output.jeff"))); +} + +// ── gate arity ──────────────────────────────── + +fn has_wrong_arity(errors: &[VerificationError]) -> bool { + errors + .iter() + .any(|e| matches!(e, VerificationError::WrongArity { .. })) +} + +#[test] +fn gate_too_few_qubit_inputs() { + assert!(has_wrong_arity(&load("gate_too_few_qubit_inputs.jeff"))); +} + +#[test] +fn gate_wrong_output_count() { + assert!(has_wrong_arity(&load("gate_wrong_output_count.jeff"))); +} + +#[test] +fn gate_missing_param_input() { + assert!(has_wrong_arity(&load("gate_missing_param_input.jeff"))); +} + +// ── qureg ops ──────────────────────────────── + +#[test] +fn qureg_alloc_bad_input_type() { + assert!(has_bad_input(&load("qureg_alloc_bad_input.jeff"))); +} + +#[test] +fn qureg_alloc_bad_output_type() { + assert!(has_bad_output(&load("qureg_alloc_bad_output.jeff"))); +} + +#[test] +fn qureg_free_bad_input_type() { + assert!(has_bad_input(&load("qureg_free_bad_input.jeff"))); +} + +#[test] +fn qureg_extract_index_bad_reg_input() { + assert!(has_bad_input(&load( + "qureg_extract_index_bad_reg_input.jeff" + ))); +} + +#[test] +fn qureg_extract_index_bad_idx_input() { + assert!(has_bad_input(&load( + "qureg_extract_index_bad_idx_input.jeff" + ))); +} + +#[test] +fn qureg_extract_index_bad_qubit_output() { + assert!(has_bad_output(&load( + "qureg_extract_index_bad_qubit_output.jeff" + ))); +} + +#[test] +fn qureg_insert_index_bad_qubit_input() { + assert!(has_bad_input(&load( + "qureg_insert_index_bad_qubit_input.jeff" + ))); +} + +#[test] +fn qureg_length_bad_output_type() { + assert!(has_bad_output(&load("qureg_length_bad_output.jeff"))); +} + +#[test] +fn qureg_join_bad_input_type() { + assert!(has_bad_input(&load("qureg_join_bad_input.jeff"))); +} diff --git a/tools/verifier/tests/positive.rs b/tools/verifier/tests/positive.rs new file mode 100644 index 0000000..8cca687 --- /dev/null +++ b/tools/verifier/tests/positive.rs @@ -0,0 +1,45 @@ +#![allow(missing_docs)] +use jeff::reader::ReadJeff; +use jeff::Jeff; +use std::fs::File; +use std::path::Path; +use verifier::verify_module; + +fn load_positive(name: &str) -> Vec { + let path = Path::new(env!("CARGO_MANIFEST_DIR")) + .join("tests/positive") + .join(name); + let file = File::open(&path) + .unwrap_or_else(|_| panic!("missing fixture: {path:?} — run generate_test_cases.py first")); + verify_module( + Jeff::read(file) + .expect("failed to parse jeff file") + .module(), + ) +} + +#[test] +fn valid_comprehensive() { + let errors = load_positive("valid_comprehensive.jeff"); + assert!( + errors.is_empty(), + "expected no errors, got:\n{}", + errors + .iter() + .map(|e| format!(" - {e}")) + .collect::>() + .join("\n") + ); +} + +#[test] +fn valid_minimal() { + let errors = load_positive("valid_minimal.jeff"); + assert!(errors.is_empty(), "expected no errors, got: {errors:?}"); +} + +#[test] +fn valid_deeply_nested() { + let errors = load_positive("valid_deeply_nested.jeff"); + assert!(errors.is_empty(), "expected no errors, got: {errors:?}"); +} From f6376b3abfa25c82040770b33716da8bf17ac64e Mon Sep 17 00:00:00 2001 From: orisus42 Date: Thu, 11 Jun 2026 17:34:23 -0400 Subject: [PATCH 2/5] fix: updated verifier functionality and added tests --- tools/verifier/src/errors.rs | 15 +- tools/verifier/src/lib.rs | 12 + tools/verifier/src/passes/isolation.rs | 4 +- .../verifier/src/passes/module_attributes.rs | 7 +- tools/verifier/src/passes/type_checks.rs | 424 ++---- tools/verifier/src/passes/value_checks.rs | 46 +- tools/verifier/tests/.gitignore | 15 - tools/verifier/tests/encode_test_cases.sh | 35 - tools/verifier/tests/examples.rs | 55 - tools/verifier/tests/generate_test_cases.py | 1152 ----------------- tools/verifier/tests/negative.rs | 162 +++ .../encode/bounds/nested_source_oob.txt | 32 - .../encode/bounds/nested_target_oob.txt | 32 - .../negative/encode/bounds/op_input_oob.txt | 23 - .../encode/bounds/region_source_oob.txt | 20 - .../encode/bounds/region_target_oob.txt | 20 - .../module/entrypoint_is_declaration.txt | 12 - .../encode/types/free_unexpected_output.txt | 23 - .../encode/types/gate_missing_param_input.txt | 29 - .../types/gate_too_few_qubit_inputs.txt | 30 - .../encode/types/gate_wrong_output_count.txt | 33 - .../encode/types/qureg_alloc_bad_input.txt | 23 - .../encode/types/qureg_alloc_bad_output.txt | 23 - .../qureg_extract_index_bad_idx_input.txt | 32 - .../qureg_extract_index_bad_qubit_output.txt | 32 - .../qureg_extract_index_bad_reg_input.txt | 28 - .../qureg_insert_index_bad_qubit_input.txt | 35 - .../encode/types/qureg_join_bad_input.txt | 31 - .../encode/types/qureg_length_bad_output.txt | 28 - .../tests/negative/incompatible_version.jeff | Bin 0 -> 176 bytes .../tests/negative/incompatible_version.txt | 13 + .../tests/negative/invalid_entrypoint.jeff | Bin 0 -> 144 bytes .../tests/negative/invalid_entrypoint.txt | 8 + .../tests/negative/invalid_input_type.jeff | Bin 0 -> 376 bytes ...ected_input.txt => invalid_input_type.txt} | 17 +- .../tests/negative/invalid_output_type.jeff | Bin 0 -> 272 bytes ...output_oob.txt => invalid_output_type.txt} | 15 +- .../tests/negative/isolation_violation.jeff | Bin 0 -> 632 bytes .../tests/negative/isolation_violation.txt | 29 + .../tests/negative/linear_consumed_twice.jeff | Bin 0 -> 400 bytes ...ad_input.txt => linear_consumed_twice.txt} | 18 +- .../tests/negative/linear_never_consumed.jeff | Bin 0 -> 272 bytes .../tests/negative/linear_never_consumed.txt | 16 + .../tests/negative/missing_version.jeff | Bin 0 -> 176 bytes .../tests/negative/missing_version.txt | 11 + .../tests/negative/type_mismatch.jeff | Bin 0 -> 480 bytes .../verifier/tests/negative/type_mismatch.txt | 23 + .../tests/negative/used_before_defined.jeff | Bin 0 -> 376 bytes .../tests/negative/used_before_defined.txt | 20 + .../tests/negative/value_out_of_bounds.jeff | Bin 0 -> 240 bytes .../tests/negative/value_out_of_bounds.txt | 15 + .../tests/negative/value_produced_twice.jeff | Bin 0 -> 280 bytes .../tests/negative/value_produced_twice.txt | 16 + .../verifier/tests/negative/wrong_arity.jeff | Bin 0 -> 376 bytes tools/verifier/tests/negative/wrong_arity.txt | 18 + tools/verifier/tests/negative_attrs.rs | 50 - tools/verifier/tests/negative_bounds.rs | 77 -- tools/verifier/tests/negative_linearity.rs | 54 - tools/verifier/tests/negative_ordering.rs | 60 - tools/verifier/tests/negative_scoping.rs | 60 - tools/verifier/tests/negative_types.rs | 213 --- tools/verifier/tests/positive.rs | 98 +- .../positive/valid_alloc_gate_measure.jeff | Bin 0 -> 904 bytes .../positive/valid_alloc_gate_measure.txt | 36 + .../positive/valid_deep_qubit_chain.jeff | Bin 0 -> 1688 bytes .../tests/positive/valid_deep_qubit_chain.txt | 60 + .../positive/valid_for_qubit_isolation.jeff | Bin 0 -> 1056 bytes .../positive/valid_for_qubit_isolation.txt | 42 + .../tests/positive/valid_int_float_ops.jeff | Bin 0 -> 992 bytes .../tests/positive/valid_int_float_ops.txt | 41 + .../positive/valid_three_qubit_gates.jeff | Bin 0 -> 1272 bytes .../positive/valid_three_qubit_gates.txt | 48 + .../tests/positive/valid_while_isolation.jeff | Bin 0 -> 776 bytes .../tests/positive/valid_while_isolation.txt | 38 + 74 files changed, 878 insertions(+), 2631 deletions(-) delete mode 100644 tools/verifier/tests/.gitignore delete mode 100755 tools/verifier/tests/encode_test_cases.sh delete mode 100644 tools/verifier/tests/examples.rs delete mode 100644 tools/verifier/tests/generate_test_cases.py create mode 100644 tools/verifier/tests/negative.rs delete mode 100644 tools/verifier/tests/negative/encode/bounds/nested_source_oob.txt delete mode 100644 tools/verifier/tests/negative/encode/bounds/nested_target_oob.txt delete mode 100644 tools/verifier/tests/negative/encode/bounds/op_input_oob.txt delete mode 100644 tools/verifier/tests/negative/encode/bounds/region_source_oob.txt delete mode 100644 tools/verifier/tests/negative/encode/bounds/region_target_oob.txt delete mode 100644 tools/verifier/tests/negative/encode/module/entrypoint_is_declaration.txt delete mode 100644 tools/verifier/tests/negative/encode/types/free_unexpected_output.txt delete mode 100644 tools/verifier/tests/negative/encode/types/gate_missing_param_input.txt delete mode 100644 tools/verifier/tests/negative/encode/types/gate_too_few_qubit_inputs.txt delete mode 100644 tools/verifier/tests/negative/encode/types/gate_wrong_output_count.txt delete mode 100644 tools/verifier/tests/negative/encode/types/qureg_alloc_bad_input.txt delete mode 100644 tools/verifier/tests/negative/encode/types/qureg_alloc_bad_output.txt delete mode 100644 tools/verifier/tests/negative/encode/types/qureg_extract_index_bad_idx_input.txt delete mode 100644 tools/verifier/tests/negative/encode/types/qureg_extract_index_bad_qubit_output.txt delete mode 100644 tools/verifier/tests/negative/encode/types/qureg_extract_index_bad_reg_input.txt delete mode 100644 tools/verifier/tests/negative/encode/types/qureg_insert_index_bad_qubit_input.txt delete mode 100644 tools/verifier/tests/negative/encode/types/qureg_join_bad_input.txt delete mode 100644 tools/verifier/tests/negative/encode/types/qureg_length_bad_output.txt create mode 100644 tools/verifier/tests/negative/incompatible_version.jeff create mode 100644 tools/verifier/tests/negative/incompatible_version.txt create mode 100644 tools/verifier/tests/negative/invalid_entrypoint.jeff create mode 100644 tools/verifier/tests/negative/invalid_entrypoint.txt create mode 100644 tools/verifier/tests/negative/invalid_input_type.jeff rename tools/verifier/tests/negative/{encode/types/alloc_unexpected_input.txt => invalid_input_type.txt} (57%) create mode 100644 tools/verifier/tests/negative/invalid_output_type.jeff rename tools/verifier/tests/negative/{encode/bounds/op_output_oob.txt => invalid_output_type.txt} (53%) create mode 100644 tools/verifier/tests/negative/isolation_violation.jeff create mode 100644 tools/verifier/tests/negative/isolation_violation.txt create mode 100644 tools/verifier/tests/negative/linear_consumed_twice.jeff rename tools/verifier/tests/negative/{encode/types/qureg_free_bad_input.txt => linear_consumed_twice.txt} (58%) create mode 100644 tools/verifier/tests/negative/linear_never_consumed.jeff create mode 100644 tools/verifier/tests/negative/linear_never_consumed.txt create mode 100644 tools/verifier/tests/negative/missing_version.jeff create mode 100644 tools/verifier/tests/negative/missing_version.txt create mode 100644 tools/verifier/tests/negative/type_mismatch.jeff create mode 100644 tools/verifier/tests/negative/type_mismatch.txt create mode 100644 tools/verifier/tests/negative/used_before_defined.jeff create mode 100644 tools/verifier/tests/negative/used_before_defined.txt create mode 100644 tools/verifier/tests/negative/value_out_of_bounds.jeff create mode 100644 tools/verifier/tests/negative/value_out_of_bounds.txt create mode 100644 tools/verifier/tests/negative/value_produced_twice.jeff create mode 100644 tools/verifier/tests/negative/value_produced_twice.txt create mode 100644 tools/verifier/tests/negative/wrong_arity.jeff create mode 100644 tools/verifier/tests/negative/wrong_arity.txt delete mode 100644 tools/verifier/tests/negative_attrs.rs delete mode 100644 tools/verifier/tests/negative_bounds.rs delete mode 100644 tools/verifier/tests/negative_linearity.rs delete mode 100644 tools/verifier/tests/negative_ordering.rs delete mode 100644 tools/verifier/tests/negative_scoping.rs delete mode 100644 tools/verifier/tests/negative_types.rs create mode 100644 tools/verifier/tests/positive/valid_alloc_gate_measure.jeff create mode 100644 tools/verifier/tests/positive/valid_alloc_gate_measure.txt create mode 100644 tools/verifier/tests/positive/valid_deep_qubit_chain.jeff create mode 100644 tools/verifier/tests/positive/valid_deep_qubit_chain.txt create mode 100644 tools/verifier/tests/positive/valid_for_qubit_isolation.jeff create mode 100644 tools/verifier/tests/positive/valid_for_qubit_isolation.txt create mode 100644 tools/verifier/tests/positive/valid_int_float_ops.jeff create mode 100644 tools/verifier/tests/positive/valid_int_float_ops.txt create mode 100644 tools/verifier/tests/positive/valid_three_qubit_gates.jeff create mode 100644 tools/verifier/tests/positive/valid_three_qubit_gates.txt create mode 100644 tools/verifier/tests/positive/valid_while_isolation.jeff create mode 100644 tools/verifier/tests/positive/valid_while_isolation.txt diff --git a/tools/verifier/src/errors.rs b/tools/verifier/src/errors.rs index ac92b2b..b337321 100644 --- a/tools/verifier/src/errors.rs +++ b/tools/verifier/src/errors.rs @@ -6,6 +6,9 @@ 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, @@ -23,8 +26,9 @@ pub enum VerificationError { value_id: u32, }, - /// A linear value (qubit or qureg) is produced by more than one operation. - LinearValueProducedMultipleTimes { + /// 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. @@ -83,6 +87,9 @@ impl fmt::Display for VerificationError { 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, @@ -101,13 +108,13 @@ impl fmt::Display for VerificationError { Self::UsedBeforeDefined { value_id } => { write!(f, "value {value_id} is used before it is defined") } - Self::LinearValueProducedMultipleTimes { + Self::ValueProducedMultipleTimes { value_id, producers, } => { write!( f, - "linear value {value_id} is produced {producers} times (must be exactly once)" + "value {value_id} is produced {producers} times (must be exactly once)" ) } Self::LinearValueConsumedMultipleTimes { diff --git a/tools/verifier/src/lib.rs b/tools/verifier/src/lib.rs index 033a423..0ccee8b 100644 --- a/tools/verifier/src/lib.rs +++ b/tools/verifier/src/lib.rs @@ -21,7 +21,19 @@ 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 { + 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); diff --git a/tools/verifier/src/passes/isolation.rs b/tools/verifier/src/passes/isolation.rs index ba7992b..8c77ac9 100644 --- a/tools/verifier/src/passes/isolation.rs +++ b/tools/verifier/src/passes/isolation.rs @@ -25,7 +25,7 @@ fn check_region_isolation( for op in region.operations() { for input in op.inputs().filter_map(|r| r.ok()) { - if outer_values.contains(&input.id()) && !locally_defined.contains(&input.id()) { + if outer_values.contains(&input.id()) { errors.push(VerificationError::IsolationViolation { value_id: input.id(), }); @@ -47,7 +47,7 @@ fn check_region_isolation( } for target in region.targets().filter_map(|r| r.ok()) { - if outer_values.contains(&target.id()) && !locally_defined.contains(&target.id()) { + if outer_values.contains(&target.id()) { errors.push(VerificationError::IsolationViolation { value_id: target.id(), }); diff --git a/tools/verifier/src/passes/module_attributes.rs b/tools/verifier/src/passes/module_attributes.rs index e8877db..a080e16 100644 --- a/tools/verifier/src/passes/module_attributes.rs +++ b/tools/verifier/src/passes/module_attributes.rs @@ -4,13 +4,8 @@ use jeff::reader::{Function, Module}; use crate::VerificationError; -/// Verify that the module has a non-zero version and a valid entrypoint. +/// Verify that the module has a valid entrypoint. pub fn verify_module_attributes(module: Module<'_>, errors: &mut Vec) { - let v = module.version(); - if v.major == 0 && v.minor == 0 && v.patch == 0 { - errors.push(VerificationError::MissingVersion); - } - match module.try_function(module.entrypoint_id()) { None | Some(Function::Declaration(_)) => { errors.push(VerificationError::InvalidEntrypoint); diff --git a/tools/verifier/src/passes/type_checks.rs b/tools/verifier/src/passes/type_checks.rs index 9a3b76a..cecd527 100644 --- a/tools/verifier/src/passes/type_checks.rs +++ b/tools/verifier/src/passes/type_checks.rs @@ -55,6 +55,80 @@ fn check_cf_region_types(cf_op: &ControlFlowOp<'_>, errors: &mut Vec bool { + matches!(ty, Type::Int { .. }) +} + +fn is_float(ty: &Type) -> bool { + matches!(ty, Type::Float { .. }) +} + +fn is_qubit(ty: &Type) -> bool { + *ty == Type::Qubit +} + +fn is_qureg(ty: &Type) -> bool { + matches!(ty, Type::QubitRegister { .. }) +} + +fn is_i1(ty: &Type) -> bool { + *ty == (Type::Int { bits: 1 }) +} + +fn is_i32(ty: &Type) -> bool { + *ty == (Type::Int { bits: 32 }) +} + +fn expect_input( + inputs: &[Type], + idx: usize, + pred: fn(&Type) -> bool, + op: &'static str, + errors: &mut Vec, +) { + if inputs.get(idx).is_some_and(|ty| !pred(ty)) { + errors.push(VerificationError::InvalidInputType { operation: op }); + } +} + +fn expect_output( + outputs: &[Type], + idx: usize, + pred: fn(&Type) -> bool, + op: &'static str, + errors: &mut Vec, +) { + if outputs.get(idx).is_some_and(|ty| !pred(ty)) { + errors.push(VerificationError::InvalidOutputType { operation: op }); + } +} + +fn check_const_int_output(outputs: &[Type], bits: u8, errors: &mut Vec) { + if outputs + .first() + .is_some_and(|ty| *ty != (Type::Int { bits })) + { + errors.push(VerificationError::InvalidOutputType { + operation: "int const", + }); + } +} + +fn check_const_float_output( + outputs: &[Type], + precision: FloatPrecision, + errors: &mut Vec, +) { + if outputs + .first() + .is_some_and(|ty| *ty != (Type::Float { precision })) + { + errors.push(VerificationError::InvalidOutputType { + operation: "float const", + }); + } +} + fn check_uniform_int( inputs: &[Type], outputs: &[Type], @@ -62,13 +136,13 @@ fn check_uniform_int( errors: &mut Vec, ) { for ty in inputs { - if !matches!(ty, Type::Int { .. }) { + if !is_int(ty) { errors.push(VerificationError::InvalidInputType { operation: name }); return; } } for ty in outputs { - if !matches!(ty, Type::Int { .. }) { + if !is_int(ty) { errors.push(VerificationError::InvalidOutputType { operation: name }); return; } @@ -95,13 +169,13 @@ fn check_uniform_float( errors: &mut Vec, ) { for ty in inputs { - if !matches!(ty, Type::Float { .. }) { + if !is_float(ty) { errors.push(VerificationError::InvalidInputType { operation: name }); return; } } for ty in outputs { - if !matches!(ty, Type::Float { .. }) { + if !is_float(ty) { errors.push(VerificationError::InvalidOutputType { operation: name }); return; } @@ -128,56 +202,11 @@ fn check_int_op( errors: &mut Vec, ) { match int_op { - IntOp::Const1(_) => { - if outputs - .first() - .is_some_and(|ty| *ty != (Type::Int { bits: 1 })) - { - errors.push(VerificationError::InvalidOutputType { - operation: "int const", - }); - } - } - IntOp::Const8(_) => { - if outputs - .first() - .is_some_and(|ty| *ty != (Type::Int { bits: 8 })) - { - errors.push(VerificationError::InvalidOutputType { - operation: "int const", - }); - } - } - IntOp::Const16(_) => { - if outputs - .first() - .is_some_and(|ty| *ty != (Type::Int { bits: 16 })) - { - errors.push(VerificationError::InvalidOutputType { - operation: "int const", - }); - } - } - IntOp::Const32(_) => { - if outputs - .first() - .is_some_and(|ty| *ty != (Type::Int { bits: 32 })) - { - errors.push(VerificationError::InvalidOutputType { - operation: "int const", - }); - } - } - IntOp::Const64(_) => { - if outputs - .first() - .is_some_and(|ty| *ty != (Type::Int { bits: 64 })) - { - errors.push(VerificationError::InvalidOutputType { - operation: "int const", - }); - } - } + IntOp::Const1(_) => check_const_int_output(outputs, 1, errors), + IntOp::Const8(_) => check_const_int_output(outputs, 8, errors), + IntOp::Const16(_) => check_const_int_output(outputs, 16, errors), + IntOp::Const32(_) => check_const_int_output(outputs, 32, errors), + IntOp::Const64(_) => check_const_int_output(outputs, 64, errors), IntOp::Add | IntOp::Sub | IntOp::Mul @@ -201,14 +230,7 @@ fn check_int_op( } IntOp::Eq | IntOp::LtS | IntOp::LteS | IntOp::LtU | IntOp::LteU => { check_uniform_int(inputs, &[], "int comparison", errors); - if outputs - .first() - .is_some_and(|ty| *ty != (Type::Int { bits: 1 })) - { - errors.push(VerificationError::InvalidOutputType { - operation: "int comparison", - }); - } + expect_output(outputs, 0, is_i1, "int comparison", errors); } _ => {} } @@ -222,26 +244,10 @@ fn check_float_op( ) { match float_op { FloatOp::Const32(_) => { - if outputs.first().is_some_and(|ty| { - *ty != (Type::Float { - precision: FloatPrecision::Float32, - }) - }) { - errors.push(VerificationError::InvalidOutputType { - operation: "float const", - }); - } + check_const_float_output(outputs, FloatPrecision::Float32, errors); } FloatOp::Const64(_) => { - if outputs.first().is_some_and(|ty| { - *ty != (Type::Float { - precision: FloatPrecision::Float64, - }) - }) { - errors.push(VerificationError::InvalidOutputType { - operation: "float const", - }); - } + check_const_float_output(outputs, FloatPrecision::Float64, errors); } FloatOp::Add | FloatOp::Sub @@ -272,14 +278,7 @@ fn check_float_op( } FloatOp::Eq | FloatOp::Lt | FloatOp::Lte | FloatOp::IsNan | FloatOp::IsInf => { check_uniform_float(inputs, &[], "float predicate", errors); - if outputs - .first() - .is_some_and(|ty| *ty != (Type::Int { bits: 1 })) - { - errors.push(VerificationError::InvalidOutputType { - operation: "float predicate", - }); - } + expect_output(outputs, 0, is_i1, "float predicate", errors); } _ => {} } @@ -296,16 +295,10 @@ fn check_qubit_op( if !inputs.is_empty() { errors.push(VerificationError::InvalidInputType { operation: "Alloc" }); } - if outputs.first().is_some_and(|ty| *ty != Type::Qubit) { - errors.push(VerificationError::InvalidOutputType { operation: "Alloc" }); - } + expect_output(outputs, 0, is_qubit, "Alloc", errors); } QubitOp::Free | QubitOp::FreeZero | QubitOp::Reset => { - if inputs.first().is_some_and(|ty| *ty != Type::Qubit) { - errors.push(VerificationError::InvalidInputType { - operation: "qubit free/reset", - }); - } + expect_input(inputs, 0, is_qubit, "qubit free/reset", errors); if !outputs.is_empty() { errors.push(VerificationError::InvalidOutputType { operation: "qubit free/reset", @@ -313,38 +306,13 @@ fn check_qubit_op( } } QubitOp::Measure => { - if inputs.first().is_some_and(|ty| *ty != Type::Qubit) { - errors.push(VerificationError::InvalidInputType { - operation: "Measure", - }); - } - if outputs - .first() - .is_some_and(|ty| *ty != (Type::Int { bits: 1 })) - { - errors.push(VerificationError::InvalidOutputType { - operation: "Measure", - }); - } + expect_input(inputs, 0, is_qubit, "Measure", errors); + expect_output(outputs, 0, is_i1, "Measure", errors); } QubitOp::MeasureNd => { - if inputs.first().is_some_and(|ty| *ty != Type::Qubit) { - errors.push(VerificationError::InvalidInputType { - operation: "MeasureNd", - }); - } - if outputs.len() >= 2 { - if outputs[0] != Type::Qubit { - errors.push(VerificationError::InvalidOutputType { - operation: "MeasureNd", - }); - } - if outputs[1] != (Type::Int { bits: 1 }) { - errors.push(VerificationError::InvalidOutputType { - operation: "MeasureNd", - }); - } - } + expect_input(inputs, 0, is_qubit, "MeasureNd", errors); + expect_output(outputs, 0, is_qubit, "MeasureNd", errors); + expect_output(outputs, 1, is_i1, "MeasureNd", errors); } QubitOp::Gate(gate) => { let num_qubits = gate.num_qubits(); @@ -357,15 +325,15 @@ fn check_qubit_op( } for (i, ty) in inputs.iter().enumerate() { if i < num_qubits { - if *ty != Type::Qubit { + if !is_qubit(ty) { errors.push(VerificationError::InvalidInputType { operation: "Gate" }); } - } else if i < num_qubits + num_params && !matches!(ty, Type::Float { .. }) { + } else if i < num_qubits + num_params && !is_float(ty) { errors.push(VerificationError::InvalidInputType { operation: "Gate" }); } } for ty in outputs.iter().take(num_qubits) { - if *ty != Type::Qubit { + if !is_qubit(ty) { errors.push(VerificationError::InvalidOutputType { operation: "Gate" }); } } @@ -374,10 +342,6 @@ fn check_qubit_op( } } -fn is_qureg(ty: &Type) -> bool { - matches!(ty, Type::QubitRegister { .. }) -} - fn check_qureg_op( qureg_op: QubitRegisterOp, inputs: &[Type], @@ -386,192 +350,62 @@ fn check_qureg_op( ) { match qureg_op { QubitRegisterOp::Alloc => { - if inputs - .first() - .is_some_and(|ty| *ty != (Type::Int { bits: 32 })) - { - errors.push(VerificationError::InvalidInputType { - operation: "qureg alloc", - }); - } - if outputs.first().is_some_and(|ty| !is_qureg(ty)) { - errors.push(VerificationError::InvalidOutputType { - operation: "qureg alloc", - }); - } + expect_input(inputs, 0, is_i32, "qureg alloc", errors); + expect_output(outputs, 0, is_qureg, "qureg alloc", errors); } QubitRegisterOp::Free | QubitRegisterOp::FreeZero => { - if inputs.first().is_some_and(|ty| !is_qureg(ty)) { - errors.push(VerificationError::InvalidInputType { - operation: "qureg free", - }); - } + expect_input(inputs, 0, is_qureg, "qureg free", errors); } QubitRegisterOp::ExtractIndex => { - if inputs.first().is_some_and(|ty| !is_qureg(ty)) { - errors.push(VerificationError::InvalidInputType { - operation: "qureg extractIndex", - }); - } - if inputs - .get(1) - .is_some_and(|ty| *ty != (Type::Int { bits: 32 })) - { - errors.push(VerificationError::InvalidInputType { - operation: "qureg extractIndex", - }); - } - if outputs.first().is_some_and(|ty| !is_qureg(ty)) { - errors.push(VerificationError::InvalidOutputType { - operation: "qureg extractIndex", - }); - } - if outputs.get(1).is_some_and(|ty| *ty != Type::Qubit) { - errors.push(VerificationError::InvalidOutputType { - operation: "qureg extractIndex", - }); - } + expect_input(inputs, 0, is_qureg, "qureg extractIndex", errors); + expect_input(inputs, 1, is_i32, "qureg extractIndex", errors); + expect_output(outputs, 0, is_qureg, "qureg extractIndex", errors); + expect_output(outputs, 1, is_qubit, "qureg extractIndex", errors); } QubitRegisterOp::InsertIndex => { - if inputs.first().is_some_and(|ty| !is_qureg(ty)) { - errors.push(VerificationError::InvalidInputType { - operation: "qureg insertIndex", - }); - } - if inputs - .get(1) - .is_some_and(|ty| *ty != (Type::Int { bits: 32 })) - { - errors.push(VerificationError::InvalidInputType { - operation: "qureg insertIndex", - }); - } - if inputs.get(2).is_some_and(|ty| *ty != Type::Qubit) { - errors.push(VerificationError::InvalidInputType { - operation: "qureg insertIndex", - }); - } - if outputs.first().is_some_and(|ty| !is_qureg(ty)) { - errors.push(VerificationError::InvalidOutputType { - operation: "qureg insertIndex", - }); - } + expect_input(inputs, 0, is_qureg, "qureg insertIndex", errors); + expect_input(inputs, 1, is_i32, "qureg insertIndex", errors); + expect_input(inputs, 2, is_qubit, "qureg insertIndex", errors); + expect_output(outputs, 0, is_qureg, "qureg insertIndex", errors); } QubitRegisterOp::ExtractSlice => { - if inputs.first().is_some_and(|ty| !is_qureg(ty)) { - errors.push(VerificationError::InvalidInputType { - operation: "qureg extractSlice", - }); - } - for ty in inputs.iter().skip(1).take(2) { - if *ty != (Type::Int { bits: 32 }) { - errors.push(VerificationError::InvalidInputType { - operation: "qureg extractSlice", - }); - } - } - for ty in outputs.iter().take(2) { - if !is_qureg(ty) { - errors.push(VerificationError::InvalidOutputType { - operation: "qureg extractSlice", - }); - } - } + expect_input(inputs, 0, is_qureg, "qureg extractSlice", errors); + expect_input(inputs, 1, is_i32, "qureg extractSlice", errors); + expect_input(inputs, 2, is_i32, "qureg extractSlice", errors); + expect_output(outputs, 0, is_qureg, "qureg extractSlice", errors); + expect_output(outputs, 1, is_qureg, "qureg extractSlice", errors); } QubitRegisterOp::InsertSlice => { - if inputs.first().is_some_and(|ty| !is_qureg(ty)) { - errors.push(VerificationError::InvalidInputType { - operation: "qureg insertSlice", - }); - } - if inputs - .get(1) - .is_some_and(|ty| *ty != (Type::Int { bits: 32 })) - { - errors.push(VerificationError::InvalidInputType { - operation: "qureg insertSlice", - }); - } - if inputs.get(2).is_some_and(|ty| !is_qureg(ty)) { - errors.push(VerificationError::InvalidInputType { - operation: "qureg insertSlice", - }); - } - if outputs.first().is_some_and(|ty| !is_qureg(ty)) { - errors.push(VerificationError::InvalidOutputType { - operation: "qureg insertSlice", - }); - } + expect_input(inputs, 0, is_qureg, "qureg insertSlice", errors); + expect_input(inputs, 1, is_i32, "qureg insertSlice", errors); + expect_input(inputs, 2, is_qureg, "qureg insertSlice", errors); + expect_output(outputs, 0, is_qureg, "qureg insertSlice", errors); } QubitRegisterOp::Length => { - if inputs.first().is_some_and(|ty| !is_qureg(ty)) { - errors.push(VerificationError::InvalidInputType { - operation: "qureg length", - }); - } - if outputs.first().is_some_and(|ty| !is_qureg(ty)) { - errors.push(VerificationError::InvalidOutputType { - operation: "qureg length", - }); - } - if outputs - .get(1) - .is_some_and(|ty| *ty != (Type::Int { bits: 32 })) - { - errors.push(VerificationError::InvalidOutputType { - operation: "qureg length", - }); - } + expect_input(inputs, 0, is_qureg, "qureg length", errors); + expect_output(outputs, 0, is_qureg, "qureg length", errors); + expect_output(outputs, 1, is_i32, "qureg length", errors); } QubitRegisterOp::Split => { - if inputs.first().is_some_and(|ty| !is_qureg(ty)) { - errors.push(VerificationError::InvalidInputType { - operation: "qureg split", - }); - } - if inputs - .get(1) - .is_some_and(|ty| *ty != (Type::Int { bits: 32 })) - { - errors.push(VerificationError::InvalidInputType { - operation: "qureg split", - }); - } - for ty in outputs.iter().take(2) { - if !is_qureg(ty) { - errors.push(VerificationError::InvalidOutputType { - operation: "qureg split", - }); - } - } + expect_input(inputs, 0, is_qureg, "qureg split", errors); + expect_input(inputs, 1, is_i32, "qureg split", errors); + expect_output(outputs, 0, is_qureg, "qureg split", errors); + expect_output(outputs, 1, is_qureg, "qureg split", errors); } QubitRegisterOp::Join => { - for ty in inputs.iter().take(2) { - if !is_qureg(ty) { - errors.push(VerificationError::InvalidInputType { - operation: "qureg join", - }); - } - } - if outputs.first().is_some_and(|ty| !is_qureg(ty)) { - errors.push(VerificationError::InvalidOutputType { - operation: "qureg join", - }); - } + expect_input(inputs, 0, is_qureg, "qureg join", errors); + expect_input(inputs, 1, is_qureg, "qureg join", errors); + expect_output(outputs, 0, is_qureg, "qureg join", errors); } QubitRegisterOp::Create => { for ty in inputs.iter() { - if *ty != Type::Qubit { + if !is_qubit(ty) { errors.push(VerificationError::InvalidInputType { operation: "qureg create", }); } } - if outputs.first().is_some_and(|ty| !is_qureg(ty)) { - errors.push(VerificationError::InvalidOutputType { - operation: "qureg create", - }); - } + expect_output(outputs, 0, is_qureg, "qureg create", errors); } #[allow(unreachable_patterns)] _ => {} diff --git a/tools/verifier/src/passes/value_checks.rs b/tools/verifier/src/passes/value_checks.rs index 7400daa..f5fa36d 100644 --- a/tools/verifier/src/passes/value_checks.rs +++ b/tools/verifier/src/passes/value_checks.rs @@ -14,19 +14,19 @@ pub fn verify_value_checks(def: FunctionDefinition<'_>, errors: &mut Vec { for (id, value) in values.iter() { + let stat = &stats[id as usize]; + if stat.producers > 1 { + errors.push(VerificationError::ValueProducedMultipleTimes { + value_id: id, + producers: stat.producers, + }); + } if is_linear(value.ty()) { - let stat = &stats[id as usize]; - if stat.producers > 1 { - errors.push(VerificationError::LinearValueProducedMultipleTimes { - value_id: id, - producers: stat.producers, - }); - } if stat.consumers > 1 { errors.push(VerificationError::LinearValueConsumedMultipleTimes { value_id: id, @@ -56,8 +56,12 @@ fn push_oob(e: ReadError, errors: &mut Vec) { } } -fn check_region_ordering(region: Region<'_>, errors: &mut Vec) { - let mut defined: HashSet = HashSet::new(); +fn check_region_ordering( + region: Region<'_>, + outer_defined: &HashSet, + errors: &mut Vec, +) { + let mut defined: HashSet = outer_defined.clone(); for result in region.sources() { match result { @@ -89,7 +93,7 @@ fn check_region_ordering(region: Region<'_>, errors: &mut Vec } if let OpType::ControlFlowOp(cf_op) = op.op_type() { - check_cf_ordering(cf_op.as_ref(), errors); + check_cf_ordering(cf_op.as_ref(), &defined, errors); } } @@ -104,23 +108,27 @@ fn check_region_ordering(region: Region<'_>, errors: &mut Vec } } -fn check_cf_ordering(cf_op: &ControlFlowOp<'_>, errors: &mut Vec) { +fn check_cf_ordering( + cf_op: &ControlFlowOp<'_>, + outer_defined: &HashSet, + errors: &mut Vec, +) { match cf_op { - ControlFlowOp::For { region } => check_region_ordering(*region, errors), + ControlFlowOp::For { region } => check_region_ordering(*region, outer_defined, errors), ControlFlowOp::While { condition, body } => { - check_region_ordering(*condition, errors); - check_region_ordering(*body, errors); + check_region_ordering(*condition, outer_defined, errors); + check_region_ordering(*body, outer_defined, errors); } ControlFlowOp::DoWhile { body, condition } => { - check_region_ordering(*body, errors); - check_region_ordering(*condition, errors); + check_region_ordering(*body, outer_defined, errors); + check_region_ordering(*condition, outer_defined, errors); } ControlFlowOp::Switch(switch_op) => { for branch in switch_op.branches() { - check_region_ordering(branch, errors); + check_region_ordering(branch, outer_defined, errors); } if let Some(default) = switch_op.default_branch() { - check_region_ordering(default, errors); + check_region_ordering(default, outer_defined, errors); } } } diff --git a/tools/verifier/tests/.gitignore b/tools/verifier/tests/.gitignore deleted file mode 100644 index 6c3a5f4..0000000 --- a/tools/verifier/tests/.gitignore +++ /dev/null @@ -1,15 +0,0 @@ -# All .jeff files are generated — recreate with: -# .venv/bin/python tools/verifier/tests/generate_test_cases.py (python-generated) -# tools/verifier/tests/encode_test_cases.sh (hand-crafted sources) -**/*.jeff - -# .txt files produced by generate_test_cases.py (capnp decode of the generated .jeff) -positive/*.txt -negative/bounds/*.txt -negative/linearity/*.txt -negative/module/missing_version.txt -negative/module/entrypoint_oob.txt -negative/module/no_functions.txt -negative/ordering/*.txt -negative/scoping/*.txt -negative/types/*.txt diff --git a/tools/verifier/tests/encode_test_cases.sh b/tools/verifier/tests/encode_test_cases.sh deleted file mode 100755 index ecd8246..0000000 --- a/tools/verifier/tests/encode_test_cases.sh +++ /dev/null @@ -1,35 +0,0 @@ -#!/usr/bin/env bash -# Encode all hand-crafted .txt fixtures in negative/encode/ to their target test directories. -# -# Run from anywhere: -# tools/verifier/tests/encode_test_cases.sh -# -# Requires the capnp CLI tool to be installed. - -set -euo pipefail - -SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" -REPO_ROOT="$(cd "$SCRIPT_DIR/../../.." && pwd)" -SCHEMA="$REPO_ROOT/impl/capnp/jeff.capnp" -ENCODED_DIR="$SCRIPT_DIR/negative/encode" - -if ! command -v capnp &>/dev/null; then - echo "error: capnp not found. Install the Cap'n Proto CLI tools." >&2 - exit 1 -fi - -echo "Encoding hand-crafted test fixtures..." - -while IFS= read -r -d '' src; do - # src is e.g. .../negative/encode/bounds/op_input_oob.txt - rel="${src#$ENCODED_DIR/}" # bounds/op_input_oob.txt - subdir="$(dirname "$rel")" # bounds - base="$(basename "$rel" .txt)" # op_input_oob - dst_dir="$SCRIPT_DIR/negative/$subdir" - dst="$dst_dir/$base.jeff" - mkdir -p "$dst_dir" - capnp encode "$SCHEMA" Module < "$src" > "$dst" - echo " encoded: negative/$subdir/$base.jeff" -done < <(find "$ENCODED_DIR" -name "*.txt" -print0 | sort -z) - -echo "Done." diff --git a/tools/verifier/tests/examples.rs b/tools/verifier/tests/examples.rs deleted file mode 100644 index d340473..0000000 --- a/tools/verifier/tests/examples.rs +++ /dev/null @@ -1,55 +0,0 @@ -#![allow(missing_docs)] -//! Run the verifier against every shipped example .jeff file and print the results. -//! This is purely informational — the test always passes. -//! Run with `cargo test -p verifier examples -- --nocapture` to see the output. - -use jeff::reader::ReadJeff; -use jeff::Jeff; -use std::fs::File; -use std::path::Path; -use verifier::verify_module; - -fn run_example(name: &str) { - let path = Path::new(env!("CARGO_MANIFEST_DIR")) - .join("../../examples") - .join(name); - - print!("{name}: "); - - let file = match File::open(&path) { - Ok(f) => f, - Err(e) => { - println!("could not open file — {e}"); - return; - } - }; - - let jeff = match Jeff::read(file) { - Ok(j) => j, - Err(e) => { - println!("read error — {e:?}"); - return; - } - }; - - let errors = verify_module(jeff.module()); - if errors.is_empty() { - println!("OK"); - } else { - println!("{} error(s):", errors.len()); - for e in &errors { - println!(" - {e}"); - } - } -} - -#[test] -fn verify_examples() { - println!(); - run_example("qubits/qubits.jeff"); - run_example("entangled_qs/entangled_qs.jeff"); - run_example("entangled_calls/entangled_calls.jeff"); - run_example("catalyst_simple/catalyst_simple.jeff"); - run_example("catalyst_tket_opt/catalyst_tket_opt.jeff"); - run_example("python_optimization/python_optimization.jeff"); -} diff --git a/tools/verifier/tests/generate_test_cases.py b/tools/verifier/tests/generate_test_cases.py deleted file mode 100644 index 0284ab7..0000000 --- a/tools/verifier/tests/generate_test_cases.py +++ /dev/null @@ -1,1152 +0,0 @@ -"""Generate .jeff (and companion .txt) test case files for the verifier. - -Run from the repo root: - .venv/bin/python tools/verifier/tests/generate_test_cases.py - -Each call to _write() produces both a binary .jeff file and a human-readable .txt -file (via `capnp decode`) in the same directory. - -Tests implemented via hand-crafted .txt sources (not generated here): - - entrypoint_is_declaration : Python lib crashes on FunctionDecl.body in _compute_strings - - OOB value-reference tests : Python lib assigns IDs automatically; can't produce OOB refs - - Qureg op type tests : Python lib has no qureg op support - - Alloc unexpected input : same — requires manual capnp text - - Free / Reset with output : same - - Gate wrong arity tests : same - Source .txt files live in tests/negative/encode/. - Run tests/encode_test_cases.sh to produce their .jeff files. - -Deferred (not implemented, caught by the reader not the verifier): - - test_unsupported_schema_version : rejected by Jeff::read before verify_module is called -""" - -import subprocess -from pathlib import Path - -import semver - -from jeff import ( - CustomGate, - DoWhileSCF, - FunctionDef, - ForSCF, - JeffModule, - JeffOp, - JeffRegion, - JeffValue, - IntType, - FloatType, - QubitType, - SwitchSCF, - WhileSCF, - qubit_alloc, - qubit_free, - quantum_gate, -) - -POSITIVE_DIR = Path(__file__).parent / "positive" -NEG_MODULE = Path(__file__).parent / "negative" / "module" -NEG_ORDERING = Path(__file__).parent / "negative" / "ordering" -NEG_TYPES = Path(__file__).parent / "negative" / "types" -NEG_LINEARITY = Path(__file__).parent / "negative" / "linearity" -NEG_SCOPING = Path(__file__).parent / "negative" / "scoping" - -_SCHEMA = Path(__file__).parents[3] / "impl" / "capnp" / "jeff.capnp" - -VERSION = semver.Version(0, 2, 0) -VERSION_ZERO = semver.Version(0, 0, 0) - - -def _write(module: JeffModule, directory: Path, name: str) -> None: - jeff_path = directory / name - module.write_out(jeff_path) - txt_path = jeff_path.with_suffix(".txt") - with open(jeff_path, "rb") as f_in, open(txt_path, "w") as f_out: - subprocess.run( - ["capnp", "decode", str(_SCHEMA), "Module"], - stdin=f_in, - stdout=f_out, - check=True, - ) - - -# ────────────────────────────────────────────── -# Positive tests -# ────────────────────────────────────────────── - - -def generate_valid_comprehensive() -> None: - """One file that exercises every feature the verifier checks.""" - - c10 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) - c20 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 20) - iadd = JeffOp( - "int", "add", [c10.outputs[0], c20.outputs[0]], [JeffValue(IntType(32))] - ) - ieq = JeffOp("int", "eq", [c10.outputs[0], c20.outputs[0]], [JeffValue(IntType(1))]) - - f1 = JeffOp("float", "const64", [], [JeffValue(FloatType(64))], 1.0) - f2 = JeffOp("float", "const64", [], [JeffValue(FloatType(64))], 2.0) - fadd = JeffOp( - "float", "add", [f1.outputs[0], f2.outputs[0]], [JeffValue(FloatType(64))] - ) - flt = JeffOp("float", "lt", [f1.outputs[0], f2.outputs[0]], [JeffValue(IntType(1))]) - - alloc_h = qubit_alloc() - gate_h = quantum_gate("H", alloc_h.outputs[0]) - measure = JeffOp("qubit", "measure", [gate_h.outputs[0]], [JeffValue(IntType(1))]) - - alloc_rx = qubit_alloc() - gate_rx = quantum_gate("Rx", alloc_rx.outputs[0], params=[f1.outputs[0]]) - measure_nd = JeffOp( - "qubit", - "measureNd", - [gate_rx.outputs[0]], - [JeffValue(QubitType()), JeffValue(IntType(1))], - ) - free_q = qubit_free(measure_nd.outputs[0]) - - for_iter = JeffValue(IntType(32)) - for_state_in = JeffValue(IntType(32)) - for_c1 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) - for_add = JeffOp( - "int", "add", [for_state_in, for_c1.outputs[0]], [JeffValue(IntType(32))] - ) - for_body = JeffRegion( - sources=[for_iter, for_state_in], - targets=[for_add.outputs[0]], - operations=[for_c1, for_add], - ) - for_op = JeffOp( - "scf", - "for", - [c10.outputs[0], iadd.outputs[0], c10.outputs[0], c20.outputs[0]], - [JeffValue(IntType(32))], - ForSCF(for_body), - ) - - w_cond_src = JeffValue(IntType(1)) - w_cond_not = JeffOp("int", "not", [w_cond_src], [JeffValue(IntType(1))]) - while_cond = JeffRegion( - sources=[w_cond_src], targets=[w_cond_not.outputs[0]], operations=[w_cond_not] - ) - w_body_src = JeffValue(IntType(1)) - w_body_not = JeffOp("int", "not", [w_body_src], [JeffValue(IntType(1))]) - while_body = JeffRegion( - sources=[w_body_src], targets=[w_body_not.outputs[0]], operations=[w_body_not] - ) - while_op = JeffOp( - "scf", - "while", - [ieq.outputs[0]], - [JeffValue(IntType(1))], - WhileSCF(while_cond, while_body), - ) - - dw_body_src = JeffValue(IntType(32)) - dw_body_c1 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) - dw_body_add = JeffOp( - "int", "add", [dw_body_src, dw_body_c1.outputs[0]], [JeffValue(IntType(32))] - ) - dowhile_body = JeffRegion( - sources=[dw_body_src], - targets=[dw_body_add.outputs[0]], - operations=[dw_body_c1, dw_body_add], - ) - dw_cond_src = JeffValue(IntType(32)) - dw_cond_c10 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) - dw_cond_eq = JeffOp( - "int", "eq", [dw_cond_src, dw_cond_c10.outputs[0]], [JeffValue(IntType(1))] - ) - dowhile_cond = JeffRegion( - sources=[dw_cond_src], - targets=[dw_cond_eq.outputs[0]], - operations=[dw_cond_c10, dw_cond_eq], - ) - dowhile_op = JeffOp( - "scf", - "doWhile", - [iadd.outputs[0]], - [JeffValue(IntType(32))], - DoWhileSCF(dowhile_body, dowhile_cond), - ) - - sw_b0_src = JeffValue(IntType(32)) - sw_b0_c99 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 99) - sw_b0_add = JeffOp( - "int", "add", [sw_b0_src, sw_b0_c99.outputs[0]], [JeffValue(IntType(32))] - ) - sw_branch0 = JeffRegion( - sources=[sw_b0_src], - targets=[sw_b0_add.outputs[0]], - operations=[sw_b0_c99, sw_b0_add], - ) - sw_def_src = JeffValue(IntType(32)) - sw_default = JeffRegion(sources=[sw_def_src], targets=[sw_def_src], operations=[]) - switch_op = JeffOp( - "scf", - "switch", - [flt.outputs[0], iadd.outputs[0]], - [JeffValue(IntType(32))], - SwitchSCF([sw_branch0], sw_default), - ) - - body = JeffRegion( - sources=[], - targets=[], - operations=[ - c10, - c20, - iadd, - ieq, - f1, - f2, - fadd, - flt, - alloc_h, - gate_h, - measure, - alloc_rx, - gate_rx, - measure_nd, - free_q, - for_op, - while_op, - dowhile_op, - switch_op, - ], - ) - _write( - JeffModule( - [FunctionDef(name="main", body=body)], version=VERSION, entrypoint=0 - ), - POSITIVE_DIR, - "valid_comprehensive.jeff", - ) - - -def generate_valid_minimal() -> None: - """Empty-body function — the smallest valid program.""" - body = JeffRegion(sources=[], targets=[], operations=[]) - _write( - JeffModule( - [FunctionDef(name="minimal", body=body)], version=VERSION, entrypoint=0 - ), - POSITIVE_DIR, - "valid_minimal.jeff", - ) - - -def generate_valid_deeply_nested() -> None: - """For loop nested inside another for loop, both properly isolated.""" - c0 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 0) - c10 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) - c1 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) - - inner_iter = JeffValue(IntType(32)) - inner_state = JeffValue(IntType(32)) - inner_c1 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) - inner_add = JeffOp( - "int", "add", [inner_state, inner_c1.outputs[0]], [JeffValue(IntType(32))] - ) - inner_body = JeffRegion( - sources=[inner_iter, inner_state], - targets=[inner_add.outputs[0]], - operations=[inner_c1, inner_add], - ) - - outer_iter = JeffValue(IntType(32)) - outer_state = JeffValue(IntType(32)) - oc0 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 0) - oc10 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) - oc1 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) - inner_for = JeffOp( - "scf", - "for", - [oc0.outputs[0], oc10.outputs[0], oc1.outputs[0], outer_state], - [JeffValue(IntType(32))], - ForSCF(inner_body), - ) - outer_body = JeffRegion( - sources=[outer_iter, outer_state], - targets=[inner_for.outputs[0]], - operations=[oc0, oc10, oc1, inner_for], - ) - - outer_for = JeffOp( - "scf", - "for", - [c0.outputs[0], c10.outputs[0], c1.outputs[0], c0.outputs[0]], - [JeffValue(IntType(32))], - ForSCF(outer_body), - ) - body = JeffRegion(sources=[], targets=[], operations=[c0, c10, c1, outer_for]) - _write( - JeffModule( - [FunctionDef(name="main", body=body)], version=VERSION, entrypoint=0 - ), - POSITIVE_DIR, - "valid_deeply_nested.jeff", - ) - - -# ────────────────────────────────────────────── -# Negative: module attribute failures -# ────────────────────────────────────────────── - - -def _trivial_def() -> FunctionDef: - return FunctionDef(name="f", body=JeffRegion(sources=[], targets=[], operations=[])) - - -def generate_missing_version() -> None: - """Version 0.0.0 → MissingVersion.""" - _write( - JeffModule([_trivial_def()], version=VERSION_ZERO, entrypoint=0), - NEG_MODULE, - "missing_version.jeff", - ) - - -def generate_entrypoint_oob() -> None: - """Entrypoint index beyond function list → InvalidEntrypoint.""" - _write( - JeffModule([_trivial_def()], version=VERSION, entrypoint=99), - NEG_MODULE, - "entrypoint_oob.jeff", - ) - - -def generate_no_functions() -> None: - """Empty function list, version 0.0.0 → MissingVersion + InvalidEntrypoint.""" - _write( - JeffModule([], version=VERSION_ZERO, entrypoint=0), - NEG_MODULE, - "no_functions.jeff", - ) - - -# ────────────────────────────────────────────── -# Negative: used before defined -# ────────────────────────────────────────────── - - -def generate_use_before_define_outer() -> None: - """add uses c10 and c20 before they are defined in the outer region.""" - c10 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) - c20 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 20) - add = JeffOp( - "int", "add", [c10.outputs[0], c20.outputs[0]], [JeffValue(IntType(32))] - ) - body = JeffRegion(sources=[], targets=[], operations=[add, c10, c20]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_ORDERING, - "use_before_define_outer.jeff", - ) - - -def generate_use_before_define_for() -> None: - """Inside for body: add uses a constant before the constant op appears.""" - c10 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) - c20 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 20) - - for_iter = JeffValue(IntType(32)) - for_state = JeffValue(IntType(32)) - late_c = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) - bad_add = JeffOp( - "int", "add", [for_state, late_c.outputs[0]], [JeffValue(IntType(32))] - ) - for_body = JeffRegion( - sources=[for_iter, for_state], - targets=[bad_add.outputs[0]], - operations=[bad_add, late_c], - ) # bad_add before late_c - - for_op = JeffOp( - "scf", - "for", - [c10.outputs[0], c20.outputs[0], c10.outputs[0], c10.outputs[0]], - [JeffValue(IntType(32))], - ForSCF(for_body), - ) - body = JeffRegion(sources=[], targets=[], operations=[c10, c20, for_op]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_ORDERING, - "use_before_define_for.jeff", - ) - - -def generate_use_before_define_while_cond() -> None: - """Inside while condition: not uses a constant before the constant op appears.""" - c0 = JeffOp("int", "const32", [], [JeffValue(IntType(1))], 0) - - cond_src = JeffValue(IntType(1)) - late_c = JeffOp("int", "const32", [], [JeffValue(IntType(1))], 0) - bad_not = JeffOp("int", "not", [late_c.outputs[0]], [JeffValue(IntType(1))]) - cond_reg = JeffRegion( - sources=[cond_src], targets=[bad_not.outputs[0]], operations=[bad_not, late_c] - ) # bad_not before late_c - - body_src = JeffValue(IntType(1)) - body_not = JeffOp("int", "not", [body_src], [JeffValue(IntType(1))]) - body_reg = JeffRegion( - sources=[body_src], targets=[body_not.outputs[0]], operations=[body_not] - ) - - while_op = JeffOp( - "scf", - "while", - [c0.outputs[0]], - [JeffValue(IntType(1))], - WhileSCF(cond_reg, body_reg), - ) - body = JeffRegion(sources=[], targets=[], operations=[c0, while_op]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_ORDERING, - "use_before_define_while_cond.jeff", - ) - - -def generate_use_before_define_while_body() -> None: - """Inside while body: second not uses first not's output before first not appears.""" - c0 = JeffOp("int", "const32", [], [JeffValue(IntType(1))], 0) - - cond_src = JeffValue(IntType(1)) - cond_not = JeffOp("int", "not", [cond_src], [JeffValue(IntType(1))]) - cond_reg = JeffRegion( - sources=[cond_src], targets=[cond_not.outputs[0]], operations=[cond_not] - ) - - body_src = JeffValue(IntType(1)) - late_not = JeffOp("int", "not", [body_src], [JeffValue(IntType(1))]) - bad_not2 = JeffOp("int", "not", [late_not.outputs[0]], [JeffValue(IntType(1))]) - body_reg = JeffRegion( - sources=[body_src], - targets=[bad_not2.outputs[0]], - operations=[bad_not2, late_not], - ) # bad_not2 before late_not - - while_op = JeffOp( - "scf", - "while", - [c0.outputs[0]], - [JeffValue(IntType(1))], - WhileSCF(cond_reg, body_reg), - ) - body = JeffRegion(sources=[], targets=[], operations=[c0, while_op]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_ORDERING, - "use_before_define_while_body.jeff", - ) - - -def generate_use_before_define_dowhile_body() -> None: - """Inside dowhile body: add uses a constant before it appears.""" - c10 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) - - dw_src = JeffValue(IntType(32)) - late_c = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) - bad_add = JeffOp( - "int", "add", [dw_src, late_c.outputs[0]], [JeffValue(IntType(32))] - ) - dw_body = JeffRegion( - sources=[dw_src], targets=[bad_add.outputs[0]], operations=[bad_add, late_c] - ) # bad_add before late_c - - cond_src = JeffValue(IntType(32)) - cond_c = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 5) - cond_eq = JeffOp( - "int", "eq", [cond_src, cond_c.outputs[0]], [JeffValue(IntType(1))] - ) - dw_cond = JeffRegion( - sources=[cond_src], targets=[cond_eq.outputs[0]], operations=[cond_c, cond_eq] - ) - - dw_op = JeffOp( - "scf", - "doWhile", - [c10.outputs[0]], - [JeffValue(IntType(32))], - DoWhileSCF(dw_body, dw_cond), - ) - body = JeffRegion(sources=[], targets=[], operations=[c10, dw_op]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_ORDERING, - "use_before_define_dowhile_body.jeff", - ) - - -def generate_use_before_define_dowhile_cond() -> None: - """Inside dowhile condition: eq uses a constant before it appears.""" - c10 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) - - dw_src = JeffValue(IntType(32)) - dw_c1 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) - dw_add = JeffOp("int", "add", [dw_src, dw_c1.outputs[0]], [JeffValue(IntType(32))]) - dw_body = JeffRegion( - sources=[dw_src], targets=[dw_add.outputs[0]], operations=[dw_c1, dw_add] - ) - - cond_src = JeffValue(IntType(32)) - late_c = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 5) - bad_eq = JeffOp("int", "eq", [cond_src, late_c.outputs[0]], [JeffValue(IntType(1))]) - dw_cond = JeffRegion( - sources=[cond_src], targets=[bad_eq.outputs[0]], operations=[bad_eq, late_c] - ) # bad_eq before late_c - - dw_op = JeffOp( - "scf", - "doWhile", - [c10.outputs[0]], - [JeffValue(IntType(32))], - DoWhileSCF(dw_body, dw_cond), - ) - body = JeffRegion(sources=[], targets=[], operations=[c10, dw_op]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_ORDERING, - "use_before_define_dowhile_cond.jeff", - ) - - -def generate_use_before_define_switch() -> None: - """Inside a switch branch: add uses a constant before it appears.""" - c0 = JeffOp("int", "const32", [], [JeffValue(IntType(1))], 0) - c10 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) - - b0_src = JeffValue(IntType(32)) - late_c = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 99) - bad_add = JeffOp( - "int", "add", [b0_src, late_c.outputs[0]], [JeffValue(IntType(32))] - ) - branch0 = JeffRegion( - sources=[b0_src], targets=[bad_add.outputs[0]], operations=[bad_add, late_c] - ) # bad_add before late_c - - def_src = JeffValue(IntType(32)) - default = JeffRegion(sources=[def_src], targets=[def_src], operations=[]) - - sw_op = JeffOp( - "scf", - "switch", - [c0.outputs[0], c10.outputs[0]], - [JeffValue(IntType(32))], - SwitchSCF([branch0], default), - ) - body = JeffRegion(sources=[], targets=[], operations=[c0, c10, sw_op]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_ORDERING, - "use_before_define_switch.jeff", - ) - - -# ────────────────────────────────────────────── -# Negative: type check failures -# ────────────────────────────────────────────── - - -def generate_int_add_mixed_bitwidths() -> None: - """add(Int32, Int64) → TypeMismatch.""" - c32 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) - c64 = JeffOp("int", "const64", [], [JeffValue(IntType(64))], 2) - bad = JeffOp( - "int", "add", [c32.outputs[0], c64.outputs[0]], [JeffValue(IntType(32))] - ) - body = JeffRegion(sources=[], targets=[], operations=[c32, c64, bad]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_TYPES, - "int_add_mixed_bitwidths.jeff", - ) - - -def generate_int_compare_mixed_bitwidths() -> None: - """eq(Int32, Int64) → TypeMismatch for int comparison.""" - c32 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) - c64 = JeffOp("int", "const64", [], [JeffValue(IntType(64))], 2) - bad = JeffOp("int", "eq", [c32.outputs[0], c64.outputs[0]], [JeffValue(IntType(1))]) - body = JeffRegion(sources=[], targets=[], operations=[c32, c64, bad]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_TYPES, - "int_compare_mixed_bitwidths.jeff", - ) - - -def generate_int_compare_bad_output() -> None: - """eq produces Int32 instead of Int1 → InvalidOutputType.""" - c32a = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) - c32b = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 2) - bad = JeffOp( - "int", "eq", [c32a.outputs[0], c32b.outputs[0]], [JeffValue(IntType(32))] - ) - body = JeffRegion(sources=[], targets=[], operations=[c32a, c32b, bad]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_TYPES, - "int_compare_bad_output.jeff", - ) - - -def generate_int_unary_bad_output() -> None: - """not(Int32) → Int64: mismatched bitwidth → TypeMismatch.""" - c32 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 5) - bad = JeffOp("int", "not", [c32.outputs[0]], [JeffValue(IntType(64))]) - body = JeffRegion(sources=[], targets=[], operations=[c32, bad]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_TYPES, - "int_unary_bad_output.jeff", - ) - - -def generate_float_add_mixed_precisions() -> None: - """add(Float32, Float64) → TypeMismatch.""" - f32 = JeffOp("float", "const32", [], [JeffValue(FloatType(32))], 1.0) - f64 = JeffOp("float", "const64", [], [JeffValue(FloatType(64))], 2.0) - bad = JeffOp( - "float", "add", [f32.outputs[0], f64.outputs[0]], [JeffValue(FloatType(64))] - ) - body = JeffRegion(sources=[], targets=[], operations=[f32, f64, bad]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_TYPES, - "float_add_mixed_precisions.jeff", - ) - - -def generate_float_compare_mixed_precisions() -> None: - """lt(Float32, Float64) → TypeMismatch for float predicate.""" - f32 = JeffOp("float", "const32", [], [JeffValue(FloatType(32))], 1.0) - f64 = JeffOp("float", "const64", [], [JeffValue(FloatType(64))], 2.0) - bad = JeffOp( - "float", "lt", [f32.outputs[0], f64.outputs[0]], [JeffValue(IntType(1))] - ) - body = JeffRegion(sources=[], targets=[], operations=[f32, f64, bad]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_TYPES, - "float_compare_mixed_precisions.jeff", - ) - - -def generate_float_compare_bad_output() -> None: - """lt produces Float64 instead of Int1 → InvalidOutputType.""" - f64a = JeffOp("float", "const64", [], [JeffValue(FloatType(64))], 1.0) - f64b = JeffOp("float", "const64", [], [JeffValue(FloatType(64))], 2.0) - bad = JeffOp( - "float", "lt", [f64a.outputs[0], f64b.outputs[0]], [JeffValue(FloatType(64))] - ) - body = JeffRegion(sources=[], targets=[], operations=[f64a, f64b, bad]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_TYPES, - "float_compare_bad_output.jeff", - ) - - -def generate_alloc_bad_output() -> None: - """alloc produces Int32 instead of Qubit → InvalidOutputType.""" - bad = JeffOp("qubit", "alloc", [], [JeffValue(IntType(32))]) - body = JeffRegion(sources=[], targets=[], operations=[bad]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_TYPES, - "alloc_bad_output.jeff", - ) - - -def generate_measure_bad_input() -> None: - """measure takes Int32 instead of Qubit → InvalidInputType.""" - c = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 0) - bad = JeffOp("qubit", "measure", [c.outputs[0]], [JeffValue(IntType(1))]) - body = JeffRegion(sources=[], targets=[], operations=[c, bad]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_TYPES, - "measure_bad_input.jeff", - ) - - -def generate_measure_bad_output() -> None: - """measure produces Float64 instead of Int1 → InvalidOutputType.""" - alloc = qubit_alloc() - bad = JeffOp("qubit", "measure", [alloc.outputs[0]], [JeffValue(FloatType(64))]) - body = JeffRegion(sources=[], targets=[], operations=[alloc, bad]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_TYPES, - "measure_bad_output.jeff", - ) - - -def generate_measurend_bad_first_output() -> None: - """measureNd first output is Int32 instead of Qubit → InvalidOutputType.""" - alloc = qubit_alloc() - bad = JeffOp( - "qubit", - "measureNd", - [alloc.outputs[0]], - [JeffValue(IntType(32)), JeffValue(IntType(1))], - ) - body = JeffRegion(sources=[], targets=[], operations=[alloc, bad]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_TYPES, - "measurend_bad_first_output.jeff", - ) - - -def generate_measurend_bad_second_output() -> None: - """measureNd second output is Float64 instead of Int1 → InvalidOutputType.""" - alloc = qubit_alloc() - bad = JeffOp( - "qubit", - "measureNd", - [alloc.outputs[0]], - [JeffValue(QubitType()), JeffValue(FloatType(64))], - ) - free = qubit_free(bad.outputs[0]) - body = JeffRegion(sources=[], targets=[], operations=[alloc, bad, free]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_TYPES, - "measurend_bad_second_output.jeff", - ) - - -def generate_free_bad_input() -> None: - """free takes Float64 instead of Qubit → InvalidInputType.""" - f = JeffOp("float", "const64", [], [JeffValue(FloatType(64))], 0.0) - bad = JeffOp("qubit", "free", [f.outputs[0]], []) - body = JeffRegion(sources=[], targets=[], operations=[f, bad]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_TYPES, - "free_bad_input.jeff", - ) - - -def generate_gate_bad_qubit_input() -> None: - """gate first input is Float64 instead of Qubit → InvalidInputType.""" - f = JeffOp("float", "const64", [], [JeffValue(FloatType(64))], 1.0) - bad = JeffOp( - "qubit", - "gate", - [f.outputs[0]], - [JeffValue(QubitType())], - CustomGate("bad", 1, 0, 0, False, 1), - ) - body = JeffRegion(sources=[], targets=[], operations=[f, bad]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_TYPES, - "gate_bad_qubit_input.jeff", - ) - - -def generate_gate_bad_qubit_output() -> None: - """gate output is Float64 instead of Qubit → InvalidOutputType.""" - alloc = qubit_alloc() - bad = JeffOp( - "qubit", - "gate", - [alloc.outputs[0]], - [JeffValue(FloatType(64))], - CustomGate("bad", 1, 0, 0, False, 1), - ) - body = JeffRegion(sources=[], targets=[], operations=[alloc, bad]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_TYPES, - "gate_bad_qubit_output.jeff", - ) - - -def generate_gate_bad_param_type() -> None: - """gate float parameter is Int32 instead of Float → InvalidInputType.""" - alloc = qubit_alloc() - c_int = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) - bad = JeffOp( - "qubit", - "gate", - [alloc.outputs[0], c_int.outputs[0]], - [JeffValue(QubitType())], - CustomGate("bad", 1, 1, 0, False, 1), - ) - body = JeffRegion(sources=[], targets=[], operations=[alloc, c_int, bad]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_TYPES, - "gate_bad_param_type.jeff", - ) - - -# ────────────────────────────────────────────── -# Negative: linearity violations -# ────────────────────────────────────────────── - - -def generate_qubit_produced_twice() -> None: - """Same qubit value appears as both body source and op output → LinearValueProducedMultipleTimes.""" - q = JeffValue(QubitType()) - alloc = JeffOp("qubit", "alloc", [], [q]) # op produces q - free = qubit_free(q) # op consumes q - body = JeffRegion(sources=[q], targets=[], operations=[alloc, free]) - # q: producers = 2 (source + alloc output), consumers = 1 (free) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_LINEARITY, - "qubit_produced_twice.jeff", - ) - - -def generate_qubit_consumed_twice() -> None: - """Same qubit value used as input by two ops → LinearValueConsumedMultipleTimes.""" - alloc = qubit_alloc() - meas1 = JeffOp("qubit", "measure", [alloc.outputs[0]], [JeffValue(IntType(1))]) - meas2 = JeffOp("qubit", "measure", [alloc.outputs[0]], [JeffValue(IntType(1))]) - body = JeffRegion(sources=[], targets=[], operations=[alloc, meas1, meas2]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_LINEARITY, - "qubit_consumed_twice.jeff", - ) - - -def generate_qubit_never_consumed() -> None: - """Qubit allocated but never freed or measured → LinearValueNeverConsumed.""" - alloc = qubit_alloc() - body = JeffRegion(sources=[], targets=[], operations=[alloc]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_LINEARITY, - "qubit_never_consumed.jeff", - ) - - -# ────────────────────────────────────────────── -# Negative: isolation / scoping violations -# ────────────────────────────────────────────── - - -def generate_for_captures_outer() -> None: - """For body directly uses a value from the outer scope → IsolationViolation.""" - c10 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) - c20 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 20) - - for_iter = JeffValue(IntType(32)) - for_state = JeffValue(IntType(32)) - bad_add = JeffOp( - "int", "add", [for_state, c10.outputs[0]], [JeffValue(IntType(32))] - ) - # c10.outputs[0] is from the outer region — not a source of this body - for_body = JeffRegion( - sources=[for_iter, for_state], - targets=[bad_add.outputs[0]], - operations=[bad_add], - ) - - for_op = JeffOp( - "scf", - "for", - [c10.outputs[0], c20.outputs[0], c10.outputs[0], c10.outputs[0]], - [JeffValue(IntType(32))], - ForSCF(for_body), - ) - body = JeffRegion(sources=[], targets=[], operations=[c10, c20, for_op]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_SCOPING, - "for_captures_outer.jeff", - ) - - -def generate_while_cond_captures_outer() -> None: - """While condition directly uses an outer value → IsolationViolation.""" - c_outer = JeffOp("int", "const32", [], [JeffValue(IntType(1))], 0) - c_init = JeffOp("int", "const32", [], [JeffValue(IntType(1))], 0) - - cond_src = JeffValue(IntType(1)) - # bad: uses c_outer.outputs[0] which is from the outer region - bad_not = JeffOp("int", "not", [c_outer.outputs[0]], [JeffValue(IntType(1))]) - cond_reg = JeffRegion( - sources=[cond_src], targets=[bad_not.outputs[0]], operations=[bad_not] - ) - - body_src = JeffValue(IntType(1)) - body_not = JeffOp("int", "not", [body_src], [JeffValue(IntType(1))]) - body_reg = JeffRegion( - sources=[body_src], targets=[body_not.outputs[0]], operations=[body_not] - ) - - while_op = JeffOp( - "scf", - "while", - [c_init.outputs[0]], - [JeffValue(IntType(1))], - WhileSCF(cond_reg, body_reg), - ) - body = JeffRegion(sources=[], targets=[], operations=[c_outer, c_init, while_op]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_SCOPING, - "while_cond_captures_outer.jeff", - ) - - -def generate_while_body_captures_outer() -> None: - """While body directly uses an outer value → IsolationViolation.""" - c_outer = JeffOp("int", "const32", [], [JeffValue(IntType(1))], 0) - c_init = JeffOp("int", "const32", [], [JeffValue(IntType(1))], 0) - - cond_src = JeffValue(IntType(1)) - cond_not = JeffOp("int", "not", [cond_src], [JeffValue(IntType(1))]) - cond_reg = JeffRegion( - sources=[cond_src], targets=[cond_not.outputs[0]], operations=[cond_not] - ) - - body_src = JeffValue(IntType(1)) - # bad: uses c_outer.outputs[0] which is from the outer region - bad_not = JeffOp("int", "not", [c_outer.outputs[0]], [JeffValue(IntType(1))]) - body_reg = JeffRegion( - sources=[body_src], targets=[bad_not.outputs[0]], operations=[bad_not] - ) - - while_op = JeffOp( - "scf", - "while", - [c_init.outputs[0]], - [JeffValue(IntType(1))], - WhileSCF(cond_reg, body_reg), - ) - body = JeffRegion(sources=[], targets=[], operations=[c_outer, c_init, while_op]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_SCOPING, - "while_body_captures_outer.jeff", - ) - - -def generate_dowhile_body_captures_outer() -> None: - """DoWhile body directly uses an outer value → IsolationViolation.""" - c_outer = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 99) - c_init = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 0) - - dw_src = JeffValue(IntType(32)) - # bad: uses c_outer.outputs[0] which is from the outer region - bad_add = JeffOp( - "int", "add", [dw_src, c_outer.outputs[0]], [JeffValue(IntType(32))] - ) - dw_body = JeffRegion( - sources=[dw_src], targets=[bad_add.outputs[0]], operations=[bad_add] - ) - - cond_src = JeffValue(IntType(32)) - cond_c = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 5) - cond_eq = JeffOp( - "int", "eq", [cond_src, cond_c.outputs[0]], [JeffValue(IntType(1))] - ) - dw_cond = JeffRegion( - sources=[cond_src], targets=[cond_eq.outputs[0]], operations=[cond_c, cond_eq] - ) - - dw_op = JeffOp( - "scf", - "doWhile", - [c_init.outputs[0]], - [JeffValue(IntType(32))], - DoWhileSCF(dw_body, dw_cond), - ) - body = JeffRegion(sources=[], targets=[], operations=[c_outer, c_init, dw_op]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_SCOPING, - "dowhile_body_captures_outer.jeff", - ) - - -def generate_dowhile_cond_captures_outer() -> None: - """DoWhile condition directly uses an outer value → IsolationViolation.""" - c_outer = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 5) - c_init = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 0) - - dw_src = JeffValue(IntType(32)) - dw_c1 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) - dw_add = JeffOp("int", "add", [dw_src, dw_c1.outputs[0]], [JeffValue(IntType(32))]) - dw_body = JeffRegion( - sources=[dw_src], targets=[dw_add.outputs[0]], operations=[dw_c1, dw_add] - ) - - cond_src = JeffValue(IntType(32)) - # bad: uses c_outer.outputs[0] which is from the outer region - bad_eq = JeffOp( - "int", "eq", [cond_src, c_outer.outputs[0]], [JeffValue(IntType(1))] - ) - dw_cond = JeffRegion( - sources=[cond_src], targets=[bad_eq.outputs[0]], operations=[bad_eq] - ) - - dw_op = JeffOp( - "scf", - "doWhile", - [c_init.outputs[0]], - [JeffValue(IntType(32))], - DoWhileSCF(dw_body, dw_cond), - ) - body = JeffRegion(sources=[], targets=[], operations=[c_outer, c_init, dw_op]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_SCOPING, - "dowhile_cond_captures_outer.jeff", - ) - - -def generate_switch_captures_outer() -> None: - """Switch branch directly uses an outer value → IsolationViolation.""" - c_outer = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 99) - c_idx = JeffOp("int", "const32", [], [JeffValue(IntType(1))], 0) - c_state = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) - - b0_src = JeffValue(IntType(32)) - # bad: uses c_outer.outputs[0] which is from the outer region - bad_add = JeffOp( - "int", "add", [b0_src, c_outer.outputs[0]], [JeffValue(IntType(32))] - ) - branch0 = JeffRegion( - sources=[b0_src], targets=[bad_add.outputs[0]], operations=[bad_add] - ) - - def_src = JeffValue(IntType(32)) - default = JeffRegion(sources=[def_src], targets=[def_src], operations=[]) - - sw_op = JeffOp( - "scf", - "switch", - [c_idx.outputs[0], c_state.outputs[0]], - [JeffValue(IntType(32))], - SwitchSCF([branch0], default), - ) - body = JeffRegion( - sources=[], targets=[], operations=[c_outer, c_idx, c_state, sw_op] - ) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_SCOPING, - "switch_captures_outer.jeff", - ) - - -def generate_nested_captures_grandparent() -> None: - """Inner for body uses a value from the outer function scope (grandparent) → IsolationViolation.""" - c10 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) - c20 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 20) - c1 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) - - inner_iter = JeffValue(IntType(32)) - inner_state = JeffValue(IntType(32)) - # bad: c10.outputs[0] is from the grandparent scope (outer function body) - bad_add = JeffOp( - "int", "add", [inner_state, c10.outputs[0]], [JeffValue(IntType(32))] - ) - inner_body = JeffRegion( - sources=[inner_iter, inner_state], - targets=[bad_add.outputs[0]], - operations=[bad_add], - ) - - outer_iter = JeffValue(IntType(32)) - outer_state = JeffValue(IntType(32)) - oc0 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 0) - oc10 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 10) - oc1 = JeffOp("int", "const32", [], [JeffValue(IntType(32))], 1) - inner_for = JeffOp( - "scf", - "for", - [oc0.outputs[0], oc10.outputs[0], oc1.outputs[0], outer_state], - [JeffValue(IntType(32))], - ForSCF(inner_body), - ) - outer_body = JeffRegion( - sources=[outer_iter, outer_state], - targets=[inner_for.outputs[0]], - operations=[oc0, oc10, oc1, inner_for], - ) - - outer_for = JeffOp( - "scf", - "for", - [c10.outputs[0], c20.outputs[0], c1.outputs[0], c10.outputs[0]], - [JeffValue(IntType(32))], - ForSCF(outer_body), - ) - body = JeffRegion(sources=[], targets=[], operations=[c10, c20, c1, outer_for]) - _write( - JeffModule([FunctionDef(name="f", body=body)], version=VERSION, entrypoint=0), - NEG_SCOPING, - "nested_captures_grandparent.jeff", - ) - - -# ────────────────────────────────────────────── -# Entry point -# ────────────────────────────────────────────── - - -if __name__ == "__main__": - POSITIVE_DIR.mkdir(exist_ok=True) - for d in (NEG_MODULE, NEG_ORDERING, NEG_TYPES, NEG_LINEARITY, NEG_SCOPING): - d.mkdir(parents=True, exist_ok=True) - - generate_valid_comprehensive() - generate_valid_minimal() - generate_valid_deeply_nested() - - generate_missing_version() - generate_entrypoint_oob() - generate_no_functions() - - generate_use_before_define_outer() - generate_use_before_define_for() - generate_use_before_define_while_cond() - generate_use_before_define_while_body() - generate_use_before_define_dowhile_body() - generate_use_before_define_dowhile_cond() - generate_use_before_define_switch() - - generate_int_add_mixed_bitwidths() - generate_int_compare_mixed_bitwidths() - generate_int_compare_bad_output() - generate_int_unary_bad_output() - generate_float_add_mixed_precisions() - generate_float_compare_mixed_precisions() - generate_float_compare_bad_output() - generate_alloc_bad_output() - generate_measure_bad_input() - generate_measure_bad_output() - generate_measurend_bad_first_output() - generate_measurend_bad_second_output() - generate_free_bad_input() - generate_gate_bad_qubit_input() - generate_gate_bad_qubit_output() - generate_gate_bad_param_type() - - generate_qubit_produced_twice() - generate_qubit_consumed_twice() - generate_qubit_never_consumed() - - generate_for_captures_outer() - generate_while_cond_captures_outer() - generate_while_body_captures_outer() - generate_dowhile_body_captures_outer() - generate_dowhile_cond_captures_outer() - generate_switch_captures_outer() - generate_nested_captures_grandparent() - - print("done") diff --git a/tools/verifier/tests/negative.rs b/tools/verifier/tests/negative.rs new file mode 100644 index 0000000..8f3adac --- /dev/null +++ b/tools/verifier/tests/negative.rs @@ -0,0 +1,162 @@ +#![allow(missing_docs)] +use jeff::reader::ReadJeff; +use jeff::Jeff; +use std::fs::File; +use std::path::Path; +use verifier::{verify_module, VerificationError}; + +fn load_negative(name: &str) -> Vec { + let path = Path::new(env!("CARGO_MANIFEST_DIR")) + .join("tests/negative") + .join(name); + let file = File::open(&path).unwrap_or_else(|_| panic!("missing fixture: {path:?}")); + verify_module( + Jeff::read(file) + .expect("failed to parse jeff file") + .module(), + ) +} + +#[test] +fn missing_version() { + let errors = load_negative("missing_version.jeff"); + assert!( + errors + .iter() + .any(|e| matches!(e, VerificationError::MissingVersion)), + "expected MissingVersion, got: {errors:?}" + ); +} + +#[test] +fn incompatible_version() { + let errors = load_negative("incompatible_version.jeff"); + assert!( + errors + .iter() + .any(|e| matches!(e, VerificationError::IncompatibleVersion)), + "expected IncompatibleVersion, got: {errors:?}" + ); +} + +#[test] +fn invalid_entrypoint() { + let errors = load_negative("invalid_entrypoint.jeff"); + assert!( + errors + .iter() + .any(|e| matches!(e, VerificationError::InvalidEntrypoint)), + "expected InvalidEntrypoint, got: {errors:?}" + ); +} + +#[test] +fn value_out_of_bounds() { + let errors = load_negative("value_out_of_bounds.jeff"); + assert!( + errors + .iter() + .any(|e| matches!(e, VerificationError::ValueOutOfBounds { .. })), + "expected ValueOutOfBounds, got: {errors:?}" + ); +} + +#[test] +fn used_before_defined() { + let errors = load_negative("used_before_defined.jeff"); + assert!( + errors + .iter() + .any(|e| matches!(e, VerificationError::UsedBeforeDefined { .. })), + "expected UsedBeforeDefined, got: {errors:?}" + ); +} + +#[test] +fn value_produced_twice() { + let errors = load_negative("value_produced_twice.jeff"); + assert!( + errors + .iter() + .any(|e| matches!(e, VerificationError::ValueProducedMultipleTimes { .. })), + "expected ValueProducedMultipleTimes, got: {errors:?}" + ); +} + +#[test] +fn linear_never_consumed() { + let errors = load_negative("linear_never_consumed.jeff"); + assert!( + errors + .iter() + .any(|e| matches!(e, VerificationError::LinearValueNeverConsumed { .. })), + "expected LinearValueNeverConsumed, got: {errors:?}" + ); +} + +#[test] +fn linear_consumed_twice() { + let errors = load_negative("linear_consumed_twice.jeff"); + assert!( + errors.iter().any(|e| matches!( + e, + VerificationError::LinearValueConsumedMultipleTimes { .. } + )), + "expected LinearValueConsumedMultipleTimes, got: {errors:?}" + ); +} + +#[test] +fn type_mismatch() { + let errors = load_negative("type_mismatch.jeff"); + assert!( + errors + .iter() + .any(|e| matches!(e, VerificationError::TypeMismatch { .. })), + "expected TypeMismatch, got: {errors:?}" + ); +} + +#[test] +fn invalid_input_type() { + let errors = load_negative("invalid_input_type.jeff"); + assert!( + errors + .iter() + .any(|e| matches!(e, VerificationError::InvalidInputType { .. })), + "expected InvalidInputType, got: {errors:?}" + ); +} + +#[test] +fn invalid_output_type() { + let errors = load_negative("invalid_output_type.jeff"); + assert!( + errors + .iter() + .any(|e| matches!(e, VerificationError::InvalidOutputType { .. })), + "expected InvalidOutputType, got: {errors:?}" + ); +} + +#[test] +fn wrong_arity() { + let errors = load_negative("wrong_arity.jeff"); + assert!( + errors + .iter() + .any(|e| matches!(e, VerificationError::WrongArity { .. })), + "expected WrongArity, got: {errors:?}" + ); +} + +#[test] +fn isolation_violation() { + let errors = load_negative("isolation_violation.jeff"); + assert!( + errors + .iter() + .any(|e| matches!(e, VerificationError::IsolationViolation { .. })), + "expected IsolationViolation, got: {errors:?}" + ); +} diff --git a/tools/verifier/tests/negative/encode/bounds/nested_source_oob.txt b/tools/verifier/tests/negative/encode/bounds/nested_source_oob.txt deleted file mode 100644 index 73a1a2f..0000000 --- a/tools/verifier/tests/negative/encode/bounds/nested_source_oob.txt +++ /dev/null @@ -1,32 +0,0 @@ -( version = 0, - functions = [ - ( name = 0, - definition = ( - body = ( - sources = [], - targets = [], - operations = [ - ( inputs = [], - outputs = [0], - instruction = (int = (const32 = 10)) ), - ( inputs = [0, 0, 0, 0], - outputs = [1], - instruction = ( - scf = ( - for = ( - sources = [99], - targets = [2], - operations = [ - ( inputs = [], - outputs = [2], - instruction = (int = (const32 = 1)) ) ] ) ) ) ) ] ), - values = [ - (type = (int = 32)), - (type = (int = 32)), - (type = (int = 32)) ] ) ) ], - strings = ["f"], - entrypoint = 0, - tool = "", - toolVersion = "", - versionMinor = 2, - versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/bounds/nested_target_oob.txt b/tools/verifier/tests/negative/encode/bounds/nested_target_oob.txt deleted file mode 100644 index e165e1e..0000000 --- a/tools/verifier/tests/negative/encode/bounds/nested_target_oob.txt +++ /dev/null @@ -1,32 +0,0 @@ -( version = 0, - functions = [ - ( name = 0, - definition = ( - body = ( - sources = [], - targets = [], - operations = [ - ( inputs = [], - outputs = [0], - instruction = (int = (const32 = 10)) ), - ( inputs = [0, 0, 0, 0], - outputs = [1], - instruction = ( - scf = ( - for = ( - sources = [2], - targets = [99], - operations = [ - ( inputs = [], - outputs = [2], - instruction = (int = (const32 = 1)) ) ] ) ) ) ) ] ), - values = [ - (type = (int = 32)), - (type = (int = 32)), - (type = (int = 32)) ] ) ) ], - strings = ["f"], - entrypoint = 0, - tool = "", - toolVersion = "", - versionMinor = 2, - versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/bounds/op_input_oob.txt b/tools/verifier/tests/negative/encode/bounds/op_input_oob.txt deleted file mode 100644 index 16f9d96..0000000 --- a/tools/verifier/tests/negative/encode/bounds/op_input_oob.txt +++ /dev/null @@ -1,23 +0,0 @@ -( version = 0, - functions = [ - ( name = 0, - definition = ( - body = ( - sources = [], - targets = [], - operations = [ - ( inputs = [], - outputs = [0], - instruction = (int = (const32 = 10)) ), - ( inputs = [0, 2], - outputs = [1], - instruction = (int = (add = void)) ) ] ), - values = [ - (type = (int = 32)), - (type = (int = 32)) ] ) ) ], - strings = ["f"], - entrypoint = 0, - tool = "", - toolVersion = "", - versionMinor = 2, - versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/bounds/region_source_oob.txt b/tools/verifier/tests/negative/encode/bounds/region_source_oob.txt deleted file mode 100644 index 4c3d9a2..0000000 --- a/tools/verifier/tests/negative/encode/bounds/region_source_oob.txt +++ /dev/null @@ -1,20 +0,0 @@ -( version = 0, - functions = [ - ( name = 0, - definition = ( - body = ( - sources = [5], - targets = [], - operations = [ - ( inputs = [], - outputs = [0], - instruction = (int = (const32 = 10)) ) ] ), - values = [ - (type = (int = 32)), - (type = (int = 32)) ] ) ) ], - strings = ["f"], - entrypoint = 0, - tool = "", - toolVersion = "", - versionMinor = 2, - versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/bounds/region_target_oob.txt b/tools/verifier/tests/negative/encode/bounds/region_target_oob.txt deleted file mode 100644 index 1c7b0b0..0000000 --- a/tools/verifier/tests/negative/encode/bounds/region_target_oob.txt +++ /dev/null @@ -1,20 +0,0 @@ -( version = 0, - functions = [ - ( name = 0, - definition = ( - body = ( - sources = [], - targets = [5], - operations = [ - ( inputs = [], - outputs = [0], - instruction = (int = (const32 = 10)) ) ] ), - values = [ - (type = (int = 32)), - (type = (int = 32)) ] ) ) ], - strings = ["f"], - entrypoint = 0, - tool = "", - toolVersion = "", - versionMinor = 2, - versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/module/entrypoint_is_declaration.txt b/tools/verifier/tests/negative/encode/module/entrypoint_is_declaration.txt deleted file mode 100644 index f194cb8..0000000 --- a/tools/verifier/tests/negative/encode/module/entrypoint_is_declaration.txt +++ /dev/null @@ -1,12 +0,0 @@ -( version = 0, - functions = [ - ( name = 0, - declaration = ( - inputs = [], - outputs = [] ) ) ], - strings = ["f"], - entrypoint = 0, - tool = "", - toolVersion = "", - versionMinor = 2, - versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/free_unexpected_output.txt b/tools/verifier/tests/negative/encode/types/free_unexpected_output.txt deleted file mode 100644 index 7cdf88e..0000000 --- a/tools/verifier/tests/negative/encode/types/free_unexpected_output.txt +++ /dev/null @@ -1,23 +0,0 @@ -( version = 0, - functions = [ - ( name = 0, - definition = ( - body = ( - sources = [], - targets = [], - operations = [ - ( inputs = [], - outputs = [0], - instruction = (qubit = (alloc = void)) ), - ( inputs = [0], - outputs = [1], - instruction = (qubit = (free = void)) ) ] ), - values = [ - (type = (qubit = void)), - (type = (int = 32)) ] ) ) ], - strings = ["f"], - entrypoint = 0, - tool = "", - toolVersion = "", - versionMinor = 2, - versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/gate_missing_param_input.txt b/tools/verifier/tests/negative/encode/types/gate_missing_param_input.txt deleted file mode 100644 index d7c326e..0000000 --- a/tools/verifier/tests/negative/encode/types/gate_missing_param_input.txt +++ /dev/null @@ -1,29 +0,0 @@ -( version = 0, - functions = [ - ( name = 0, - definition = ( - body = ( - sources = [], - targets = [], - operations = [ - ( inputs = [], - outputs = [0], - instruction = (qubit = (alloc = void)) ), - ( inputs = [0], - outputs = [1], - instruction = ( - qubit = ( - gate = ( - custom = (name = 0, numQubits = 1, numParams = 1), - controlQubits = 0, - adjoint = false, - power = 1 ) ) ) ) ] ), - values = [ - (type = (qubit = void)), - (type = (qubit = void)) ] ) ) ], - strings = ["rz"], - entrypoint = 0, - tool = "", - toolVersion = "", - versionMinor = 2, - versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/gate_too_few_qubit_inputs.txt b/tools/verifier/tests/negative/encode/types/gate_too_few_qubit_inputs.txt deleted file mode 100644 index 0214ed6..0000000 --- a/tools/verifier/tests/negative/encode/types/gate_too_few_qubit_inputs.txt +++ /dev/null @@ -1,30 +0,0 @@ -( version = 0, - functions = [ - ( name = 0, - definition = ( - body = ( - sources = [], - targets = [], - operations = [ - ( inputs = [], - outputs = [0], - instruction = (qubit = (alloc = void)) ), - ( inputs = [0], - outputs = [1, 2], - instruction = ( - qubit = ( - gate = ( - custom = (name = 0, numQubits = 2, numParams = 0), - controlQubits = 0, - adjoint = false, - power = 1 ) ) ) ) ] ), - values = [ - (type = (qubit = void)), - (type = (qubit = void)), - (type = (qubit = void)) ] ) ) ], - strings = ["bad2q"], - entrypoint = 0, - tool = "", - toolVersion = "", - versionMinor = 2, - versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/gate_wrong_output_count.txt b/tools/verifier/tests/negative/encode/types/gate_wrong_output_count.txt deleted file mode 100644 index 0392aeb..0000000 --- a/tools/verifier/tests/negative/encode/types/gate_wrong_output_count.txt +++ /dev/null @@ -1,33 +0,0 @@ -( version = 0, - functions = [ - ( name = 0, - definition = ( - body = ( - sources = [], - targets = [], - operations = [ - ( inputs = [], - outputs = [0], - instruction = (qubit = (alloc = void)) ), - ( inputs = [], - outputs = [1], - instruction = (qubit = (alloc = void)) ), - ( inputs = [0, 1], - outputs = [2], - instruction = ( - qubit = ( - gate = ( - custom = (name = 0, numQubits = 2, numParams = 0), - controlQubits = 0, - adjoint = false, - power = 1 ) ) ) ) ] ), - values = [ - (type = (qubit = void)), - (type = (qubit = void)), - (type = (qubit = void)) ] ) ) ], - strings = ["bad2q"], - entrypoint = 0, - tool = "", - toolVersion = "", - versionMinor = 2, - versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/qureg_alloc_bad_input.txt b/tools/verifier/tests/negative/encode/types/qureg_alloc_bad_input.txt deleted file mode 100644 index 7148b91..0000000 --- a/tools/verifier/tests/negative/encode/types/qureg_alloc_bad_input.txt +++ /dev/null @@ -1,23 +0,0 @@ -( version = 0, - functions = [ - ( name = 0, - definition = ( - body = ( - sources = [], - targets = [], - operations = [ - ( inputs = [], - outputs = [0], - instruction = (float = (const64 = 5)) ), - ( inputs = [0], - outputs = [1], - instruction = (qureg = (alloc = void)) ) ] ), - values = [ - (type = (float = float64)), - (type = (qureg = (dynamic = void))) ] ) ) ], - strings = ["f"], - entrypoint = 0, - tool = "", - toolVersion = "", - versionMinor = 2, - versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/qureg_alloc_bad_output.txt b/tools/verifier/tests/negative/encode/types/qureg_alloc_bad_output.txt deleted file mode 100644 index 8f127a3..0000000 --- a/tools/verifier/tests/negative/encode/types/qureg_alloc_bad_output.txt +++ /dev/null @@ -1,23 +0,0 @@ -( version = 0, - functions = [ - ( name = 0, - definition = ( - body = ( - sources = [], - targets = [], - operations = [ - ( inputs = [], - outputs = [0], - instruction = (int = (const32 = 5)) ), - ( inputs = [0], - outputs = [1], - instruction = (qureg = (alloc = void)) ) ] ), - values = [ - (type = (int = 32)), - (type = (qubit = void)) ] ) ) ], - strings = ["f"], - entrypoint = 0, - tool = "", - toolVersion = "", - versionMinor = 2, - versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/qureg_extract_index_bad_idx_input.txt b/tools/verifier/tests/negative/encode/types/qureg_extract_index_bad_idx_input.txt deleted file mode 100644 index c037c9f..0000000 --- a/tools/verifier/tests/negative/encode/types/qureg_extract_index_bad_idx_input.txt +++ /dev/null @@ -1,32 +0,0 @@ -( version = 0, - functions = [ - ( name = 0, - definition = ( - body = ( - sources = [], - targets = [], - operations = [ - ( inputs = [], - outputs = [0], - instruction = (int = (const32 = 1)) ), - ( inputs = [], - outputs = [1], - instruction = (int = (const64 = 0)) ), - ( inputs = [0], - outputs = [2], - instruction = (qureg = (alloc = void)) ), - ( inputs = [2, 1], - outputs = [3, 4], - instruction = (qureg = (extractIndex = void)) ) ] ), - values = [ - (type = (int = 32)), - (type = (int = 64)), - (type = (qureg = (dynamic = void))), - (type = (qureg = (dynamic = void))), - (type = (qubit = void)) ] ) ) ], - strings = ["f"], - entrypoint = 0, - tool = "", - toolVersion = "", - versionMinor = 2, - versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/qureg_extract_index_bad_qubit_output.txt b/tools/verifier/tests/negative/encode/types/qureg_extract_index_bad_qubit_output.txt deleted file mode 100644 index fc3b414..0000000 --- a/tools/verifier/tests/negative/encode/types/qureg_extract_index_bad_qubit_output.txt +++ /dev/null @@ -1,32 +0,0 @@ -( version = 0, - functions = [ - ( name = 0, - definition = ( - body = ( - sources = [], - targets = [], - operations = [ - ( inputs = [], - outputs = [0], - instruction = (int = (const32 = 1)) ), - ( inputs = [], - outputs = [1], - instruction = (int = (const32 = 0)) ), - ( inputs = [0], - outputs = [2], - instruction = (qureg = (alloc = void)) ), - ( inputs = [2, 1], - outputs = [3, 4], - instruction = (qureg = (extractIndex = void)) ) ] ), - values = [ - (type = (int = 32)), - (type = (int = 32)), - (type = (qureg = (dynamic = void))), - (type = (qureg = (dynamic = void))), - (type = (int = 32)) ] ) ) ], - strings = ["f"], - entrypoint = 0, - tool = "", - toolVersion = "", - versionMinor = 2, - versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/qureg_extract_index_bad_reg_input.txt b/tools/verifier/tests/negative/encode/types/qureg_extract_index_bad_reg_input.txt deleted file mode 100644 index f5f857b..0000000 --- a/tools/verifier/tests/negative/encode/types/qureg_extract_index_bad_reg_input.txt +++ /dev/null @@ -1,28 +0,0 @@ -( version = 0, - functions = [ - ( name = 0, - definition = ( - body = ( - sources = [], - targets = [], - operations = [ - ( inputs = [], - outputs = [0], - instruction = (int = (const32 = 0)) ), - ( inputs = [], - outputs = [1], - instruction = (qubit = (alloc = void)) ), - ( inputs = [1, 0], - outputs = [2, 3], - instruction = (qureg = (extractIndex = void)) ) ] ), - values = [ - (type = (int = 32)), - (type = (qubit = void)), - (type = (qureg = (dynamic = void))), - (type = (qubit = void)) ] ) ) ], - strings = ["f"], - entrypoint = 0, - tool = "", - toolVersion = "", - versionMinor = 2, - versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/qureg_insert_index_bad_qubit_input.txt b/tools/verifier/tests/negative/encode/types/qureg_insert_index_bad_qubit_input.txt deleted file mode 100644 index f1de8a5..0000000 --- a/tools/verifier/tests/negative/encode/types/qureg_insert_index_bad_qubit_input.txt +++ /dev/null @@ -1,35 +0,0 @@ -( version = 0, - functions = [ - ( name = 0, - definition = ( - body = ( - sources = [], - targets = [], - operations = [ - ( inputs = [], - outputs = [0], - instruction = (int = (const32 = 1)) ), - ( inputs = [], - outputs = [1], - instruction = (int = (const32 = 0)) ), - ( inputs = [], - outputs = [2], - instruction = (int = (const32 = 42)) ), - ( inputs = [0], - outputs = [3], - instruction = (qureg = (alloc = void)) ), - ( inputs = [3, 1, 2], - outputs = [4], - instruction = (qureg = (insertIndex = void)) ) ] ), - values = [ - (type = (int = 32)), - (type = (int = 32)), - (type = (int = 32)), - (type = (qureg = (dynamic = void))), - (type = (qureg = (dynamic = void))) ] ) ) ], - strings = ["f"], - entrypoint = 0, - tool = "", - toolVersion = "", - versionMinor = 2, - versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/qureg_join_bad_input.txt b/tools/verifier/tests/negative/encode/types/qureg_join_bad_input.txt deleted file mode 100644 index 2312f98..0000000 --- a/tools/verifier/tests/negative/encode/types/qureg_join_bad_input.txt +++ /dev/null @@ -1,31 +0,0 @@ -( version = 0, - functions = [ - ( name = 0, - definition = ( - body = ( - sources = [], - targets = [], - operations = [ - ( inputs = [], - outputs = [0], - instruction = (int = (const32 = 1)) ), - ( inputs = [0], - outputs = [1], - instruction = (qureg = (alloc = void)) ), - ( inputs = [], - outputs = [2], - instruction = (qubit = (alloc = void)) ), - ( inputs = [1, 2], - outputs = [3], - instruction = (qureg = (join = void)) ) ] ), - values = [ - (type = (int = 32)), - (type = (qureg = (dynamic = void))), - (type = (qubit = void)), - (type = (qureg = (dynamic = void))) ] ) ) ], - strings = ["f"], - entrypoint = 0, - tool = "", - toolVersion = "", - versionMinor = 2, - versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/encode/types/qureg_length_bad_output.txt b/tools/verifier/tests/negative/encode/types/qureg_length_bad_output.txt deleted file mode 100644 index 501eab6..0000000 --- a/tools/verifier/tests/negative/encode/types/qureg_length_bad_output.txt +++ /dev/null @@ -1,28 +0,0 @@ -( version = 0, - functions = [ - ( name = 0, - definition = ( - body = ( - sources = [], - targets = [], - operations = [ - ( inputs = [], - outputs = [0], - instruction = (int = (const32 = 3)) ), - ( inputs = [0], - outputs = [1], - instruction = (qureg = (alloc = void)) ), - ( inputs = [1], - outputs = [2, 3], - instruction = (qureg = (length = void)) ) ] ), - values = [ - (type = (int = 32)), - (type = (qureg = (dynamic = void))), - (type = (qureg = (dynamic = void))), - (type = (int = 64)) ] ) ) ], - strings = ["f"], - entrypoint = 0, - tool = "", - toolVersion = "", - versionMinor = 2, - versionPatch = 0 ) diff --git a/tools/verifier/tests/negative/incompatible_version.jeff b/tools/verifier/tests/negative/incompatible_version.jeff new file mode 100644 index 0000000000000000000000000000000000000000..e09ed965bb2d7e6c4dab040ab3e5a4d68e01f0cb GIT binary patch literal 176 zcmZQzU|>YY($m^a)IW6RDb{z*d1CxR&HWu9!LZLf5!sS literal 0 HcmV?d00001 diff --git a/tools/verifier/tests/negative/incompatible_version.txt b/tools/verifier/tests/negative/incompatible_version.txt new file mode 100644 index 0000000..64f9786 --- /dev/null +++ b/tools/verifier/tests/negative/incompatible_version.txt @@ -0,0 +1,13 @@ +( version = 0, + versionMinor = 1, + versionPatch = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [], + operations = [] ), + values = [] ) ) ], + strings = ["main"], + entrypoint = 0 ) diff --git a/tools/verifier/tests/negative/invalid_entrypoint.jeff b/tools/verifier/tests/negative/invalid_entrypoint.jeff new file mode 100644 index 0000000000000000000000000000000000000000..b26298f3cd7382f7924127895790d45a4635a36c GIT binary patch literal 144 zcmZQzU|Lj>0`y9s(`v1{OqooB8E_c0zqyVsx3PEiqdb1;CB?CEF z^jkeshbr}&=sXVUlv1Fl*V*<}y||MfY>(CwI^SiH&ABWot!l#BVW6&$Q+p5Y07+K3wN6V1TdmEQobN_=5_)g z=bLvxujFkLXN*kS!PkoVp+Ol2+cF38lU3klBX(!kXVhp)6{v20SE>JOBaN=Z?wIwH w@6VOGcwc{p3-aare`(1fnABYI|E*)EOc!ETV<5$0?UyhDt0Vk*f4tcF0DnveEC2ui literal 0 HcmV?d00001 diff --git a/tools/verifier/tests/negative/isolation_violation.txt b/tools/verifier/tests/negative/isolation_violation.txt new file mode 100644 index 0000000..998c2c6 --- /dev/null +++ b/tools/verifier/tests/negative/isolation_violation.txt @@ -0,0 +1,29 @@ +( version = 0, + versionMinor = 2, + versionPatch = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [], + operations = [ + ( outputs = [0], + instruction = (int = (const1 = false)) ), + ( outputs = [1], + instruction = (int = (const32 = 1)) ), + ( inputs = [1, 1, 1], + instruction = (scf = (for = ( + sources = [2], + targets = [], + operations = [ + ( inputs = [0], + outputs = [3], + instruction = (int = (not = void)) ) ] ) )) ) ] ), + values = [ + (type = (int = 1)), + (type = (int = 32)), + (type = (int = 32)), + (type = (int = 1)) ] ) ) ], + strings = ["main"], + entrypoint = 0 ) diff --git a/tools/verifier/tests/negative/linear_consumed_twice.jeff b/tools/verifier/tests/negative/linear_consumed_twice.jeff new file mode 100644 index 0000000000000000000000000000000000000000..6c1b2a70ecbcad704b7ad50cbf82a0bdf4244994 GIT binary patch literal 400 zcmZQzU|=u=Vh~_rV1+QiYzR{jNT~zyN+9Ng2w^2zfTD~H%y2mlFpGtu5=e`~MHv`) zfozakPACnsu^xzFfCtE61gn6FKxmK~L2@vl17t7)Aq?mO8OZW5aTOo~S)D2lbuwt` kVEWN%gpH^&=;9zhf)LVh~_rV1+QiYzR{jNT~yHCJ^&Mgs_qzio@F_6Bzm&~sKa3zI+ zxrwMvZdeZFmt5QE=eOpx!Yp}|~dSh|B=XOQ9la zl`UulHlR`K_6%^HJdR!&Rge#u@2#E?%vOoH@eNqL8eLW*mI}&3|8m`VSvx=DWBfzx&IE>z(r_VEO)5PTm1d7zF(Q literal 0 HcmV?d00001 diff --git a/tools/verifier/tests/negative/used_before_defined.txt b/tools/verifier/tests/negative/used_before_defined.txt new file mode 100644 index 0000000..29f38f3 --- /dev/null +++ b/tools/verifier/tests/negative/used_before_defined.txt @@ -0,0 +1,20 @@ +( version = 0, + versionMinor = 2, + versionPatch = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [], + operations = [ + ( inputs = [1], + outputs = [0], + instruction = (int = (not = void)) ), + ( outputs = [1], + instruction = (int = (const1 = false)) ) ] ), + values = [ + (type = (int = 1)), + (type = (int = 1)) ] ) ) ], + strings = ["main"], + entrypoint = 0 ) diff --git a/tools/verifier/tests/negative/value_out_of_bounds.jeff b/tools/verifier/tests/negative/value_out_of_bounds.jeff new file mode 100644 index 0000000000000000000000000000000000000000..91ac7af0b7d5d7a0b889ffb91e7e4e14c5be9fe9 GIT binary patch literal 240 zcmZQzU|^61Vh~_rV1+QiYzR{jNT~yHBoOmKgs_qR{< F?9pPcm?o^Iv#n8uo_?89peAc}H@a@@s3`3vn~22yPTLpJm7MrQ-3aA* q Vec { - let path = Path::new(env!("CARGO_MANIFEST_DIR")) - .join("tests/negative/module") - .join(name); - let file = File::open(&path) - .unwrap_or_else(|_| panic!("missing fixture: {path:?} — run generate_test_cases.py first")); - verify_module( - Jeff::read(file) - .expect("failed to parse jeff file") - .module(), - ) -} - -#[test] -fn missing_version() { - let errors = load("missing_version.jeff"); - assert!( - errors.contains(&VerificationError::MissingVersion), - "expected MissingVersion, got: {errors:?}" - ); -} - -#[test] -fn entrypoint_oob() { - let errors = load("entrypoint_oob.jeff"); - assert!( - errors.contains(&VerificationError::InvalidEntrypoint), - "expected InvalidEntrypoint, got: {errors:?}" - ); -} - -#[test] -fn no_functions_gives_both_errors() { - let errors = load("no_functions.jeff"); - assert!( - errors.contains(&VerificationError::MissingVersion), - "expected MissingVersion in {errors:?}" - ); - assert!( - errors.contains(&VerificationError::InvalidEntrypoint), - "expected InvalidEntrypoint in {errors:?}" - ); -} diff --git a/tools/verifier/tests/negative_bounds.rs b/tools/verifier/tests/negative_bounds.rs deleted file mode 100644 index 698e452..0000000 --- a/tools/verifier/tests/negative_bounds.rs +++ /dev/null @@ -1,77 +0,0 @@ -#![allow(missing_docs)] -use jeff::reader::ReadJeff; -use jeff::Jeff; -use std::fs::File; -use std::path::Path; -use verifier::{verify_module, VerificationError}; - -fn load_bounds(name: &str) -> Vec { - let path = Path::new(env!("CARGO_MANIFEST_DIR")) - .join("tests/negative/bounds") - .join(name); - let file = File::open(&path).unwrap_or_else(|_| panic!("missing fixture: {path:?}")); - verify_module( - Jeff::read(file) - .expect("failed to parse jeff file") - .module(), - ) -} - -fn load_module(name: &str) -> Vec { - let path = Path::new(env!("CARGO_MANIFEST_DIR")) - .join("tests/negative/module") - .join(name); - let file = File::open(&path).unwrap_or_else(|_| panic!("missing fixture: {path:?}")); - verify_module( - Jeff::read(file) - .expect("failed to parse jeff file") - .module(), - ) -} - -fn has_oob(errors: &[VerificationError]) -> bool { - errors - .iter() - .any(|e| matches!(e, VerificationError::ValueOutOfBounds { .. })) -} - -#[test] -fn op_input_oob() { - assert!(has_oob(&load_bounds("op_input_oob.jeff"))); -} - -#[test] -fn op_output_oob() { - assert!(has_oob(&load_bounds("op_output_oob.jeff"))); -} - -#[test] -fn region_source_oob() { - assert!(has_oob(&load_bounds("region_source_oob.jeff"))); -} - -#[test] -fn region_target_oob() { - assert!(has_oob(&load_bounds("region_target_oob.jeff"))); -} - -#[test] -fn nested_source_oob() { - assert!(has_oob(&load_bounds("nested_source_oob.jeff"))); -} - -#[test] -fn nested_target_oob() { - assert!(has_oob(&load_bounds("nested_target_oob.jeff"))); -} - -#[test] -fn entrypoint_is_declaration() { - let errors = load_module("entrypoint_is_declaration.jeff"); - assert!( - errors - .iter() - .any(|e| matches!(e, VerificationError::InvalidEntrypoint)), - "expected InvalidEntrypoint, got: {errors:?}" - ); -} diff --git a/tools/verifier/tests/negative_linearity.rs b/tools/verifier/tests/negative_linearity.rs deleted file mode 100644 index 896d21c..0000000 --- a/tools/verifier/tests/negative_linearity.rs +++ /dev/null @@ -1,54 +0,0 @@ -#![allow(missing_docs)] -use jeff::reader::ReadJeff; -use jeff::Jeff; -use std::fs::File; -use std::path::Path; -use verifier::{verify_module, VerificationError}; - -fn load(name: &str) -> Vec { - let path = Path::new(env!("CARGO_MANIFEST_DIR")) - .join("tests/negative/linearity") - .join(name); - let file = File::open(&path) - .unwrap_or_else(|_| panic!("missing fixture: {path:?} — run generate_test_cases.py first")); - verify_module( - Jeff::read(file) - .expect("failed to parse jeff file") - .module(), - ) -} - -#[test] -fn qubit_produced_twice() { - let errors = load("qubit_produced_twice.jeff"); - assert!( - errors.iter().any(|e| matches!( - e, - VerificationError::LinearValueProducedMultipleTimes { .. } - )), - "expected LinearValueProducedMultipleTimes, got: {errors:?}" - ); -} - -#[test] -fn qubit_consumed_twice() { - let errors = load("qubit_consumed_twice.jeff"); - assert!( - errors.iter().any(|e| matches!( - e, - VerificationError::LinearValueConsumedMultipleTimes { .. } - )), - "expected LinearValueConsumedMultipleTimes, got: {errors:?}" - ); -} - -#[test] -fn qubit_never_consumed() { - let errors = load("qubit_never_consumed.jeff"); - assert!( - errors - .iter() - .any(|e| matches!(e, VerificationError::LinearValueNeverConsumed { .. })), - "expected LinearValueNeverConsumed, got: {errors:?}" - ); -} diff --git a/tools/verifier/tests/negative_ordering.rs b/tools/verifier/tests/negative_ordering.rs deleted file mode 100644 index 05ec6a8..0000000 --- a/tools/verifier/tests/negative_ordering.rs +++ /dev/null @@ -1,60 +0,0 @@ -#![allow(missing_docs)] -use jeff::reader::ReadJeff; -use jeff::Jeff; -use std::fs::File; -use std::path::Path; -use verifier::{verify_module, VerificationError}; - -fn load(name: &str) -> Vec { - let path = Path::new(env!("CARGO_MANIFEST_DIR")) - .join("tests/negative/ordering") - .join(name); - let file = File::open(&path) - .unwrap_or_else(|_| panic!("missing fixture: {path:?} — run generate_test_cases.py first")); - verify_module( - Jeff::read(file) - .expect("failed to parse jeff file") - .module(), - ) -} - -fn has_ubd(errors: &[VerificationError]) -> bool { - errors - .iter() - .any(|e| matches!(e, VerificationError::UsedBeforeDefined { .. })) -} - -#[test] -fn use_before_define_outer() { - assert!(has_ubd(&load("use_before_define_outer.jeff"))); -} - -#[test] -fn use_before_define_for_body() { - assert!(has_ubd(&load("use_before_define_for.jeff"))); -} - -#[test] -fn use_before_define_while_condition() { - assert!(has_ubd(&load("use_before_define_while_cond.jeff"))); -} - -#[test] -fn use_before_define_while_body() { - assert!(has_ubd(&load("use_before_define_while_body.jeff"))); -} - -#[test] -fn use_before_define_dowhile_body() { - assert!(has_ubd(&load("use_before_define_dowhile_body.jeff"))); -} - -#[test] -fn use_before_define_dowhile_condition() { - assert!(has_ubd(&load("use_before_define_dowhile_cond.jeff"))); -} - -#[test] -fn use_before_define_switch_branch() { - assert!(has_ubd(&load("use_before_define_switch.jeff"))); -} diff --git a/tools/verifier/tests/negative_scoping.rs b/tools/verifier/tests/negative_scoping.rs deleted file mode 100644 index 4db4196..0000000 --- a/tools/verifier/tests/negative_scoping.rs +++ /dev/null @@ -1,60 +0,0 @@ -#![allow(missing_docs)] -use jeff::reader::ReadJeff; -use jeff::Jeff; -use std::fs::File; -use std::path::Path; -use verifier::{verify_module, VerificationError}; - -fn load(name: &str) -> Vec { - let path = Path::new(env!("CARGO_MANIFEST_DIR")) - .join("tests/negative/scoping") - .join(name); - let file = File::open(&path) - .unwrap_or_else(|_| panic!("missing fixture: {path:?} — run generate_test_cases.py first")); - verify_module( - Jeff::read(file) - .expect("failed to parse jeff file") - .module(), - ) -} - -fn has_isolation(errors: &[VerificationError]) -> bool { - errors - .iter() - .any(|e| matches!(e, VerificationError::IsolationViolation { .. })) -} - -#[test] -fn for_body_captures_outer() { - assert!(has_isolation(&load("for_captures_outer.jeff"))); -} - -#[test] -fn while_condition_captures_outer() { - assert!(has_isolation(&load("while_cond_captures_outer.jeff"))); -} - -#[test] -fn while_body_captures_outer() { - assert!(has_isolation(&load("while_body_captures_outer.jeff"))); -} - -#[test] -fn dowhile_body_captures_outer() { - assert!(has_isolation(&load("dowhile_body_captures_outer.jeff"))); -} - -#[test] -fn dowhile_condition_captures_outer() { - assert!(has_isolation(&load("dowhile_cond_captures_outer.jeff"))); -} - -#[test] -fn switch_branch_captures_outer() { - assert!(has_isolation(&load("switch_captures_outer.jeff"))); -} - -#[test] -fn nested_for_captures_grandparent() { - assert!(has_isolation(&load("nested_captures_grandparent.jeff"))); -} diff --git a/tools/verifier/tests/negative_types.rs b/tools/verifier/tests/negative_types.rs deleted file mode 100644 index d9394e4..0000000 --- a/tools/verifier/tests/negative_types.rs +++ /dev/null @@ -1,213 +0,0 @@ -#![allow(missing_docs)] -use jeff::reader::ReadJeff; -use jeff::Jeff; -use std::fs::File; -use std::path::Path; -use verifier::{verify_module, VerificationError}; - -fn load(name: &str) -> Vec { - let path = Path::new(env!("CARGO_MANIFEST_DIR")) - .join("tests/negative/types") - .join(name); - let file = File::open(&path) - .unwrap_or_else(|_| panic!("missing fixture: {path:?} — run generate_test_cases.py first")); - verify_module( - Jeff::read(file) - .expect("failed to parse jeff file") - .module(), - ) -} - -fn has_mismatch(errors: &[VerificationError]) -> bool { - errors - .iter() - .any(|e| matches!(e, VerificationError::TypeMismatch { .. })) -} - -fn has_bad_input(errors: &[VerificationError]) -> bool { - errors - .iter() - .any(|e| matches!(e, VerificationError::InvalidInputType { .. })) -} - -fn has_bad_output(errors: &[VerificationError]) -> bool { - errors - .iter() - .any(|e| matches!(e, VerificationError::InvalidOutputType { .. })) -} - -// ── int ────────────────────────────────────── - -#[test] -fn int_add_mixed_bitwidths() { - assert!(has_mismatch(&load("int_add_mixed_bitwidths.jeff"))); -} - -#[test] -fn int_compare_mixed_bitwidths() { - assert!(has_mismatch(&load("int_compare_mixed_bitwidths.jeff"))); -} - -#[test] -fn int_compare_bad_output_type() { - assert!(has_bad_output(&load("int_compare_bad_output.jeff"))); -} - -#[test] -fn int_unary_output_type_mismatch() { - assert!(has_mismatch(&load("int_unary_bad_output.jeff"))); -} - -// ── float ──────────────────────────────────── - -#[test] -fn float_add_mixed_precisions() { - assert!(has_mismatch(&load("float_add_mixed_precisions.jeff"))); -} - -#[test] -fn float_compare_mixed_precisions() { - assert!(has_mismatch(&load("float_compare_mixed_precisions.jeff"))); -} - -#[test] -fn float_compare_bad_output_type() { - assert!(has_bad_output(&load("float_compare_bad_output.jeff"))); -} - -// ── qubit ──────────────────────────────────── - -#[test] -fn alloc_bad_output_type() { - assert!(has_bad_output(&load("alloc_bad_output.jeff"))); -} - -#[test] -fn measure_bad_input_type() { - assert!(has_bad_input(&load("measure_bad_input.jeff"))); -} - -#[test] -fn measure_bad_output_type() { - assert!(has_bad_output(&load("measure_bad_output.jeff"))); -} - -#[test] -fn measurend_bad_first_output() { - assert!(has_bad_output(&load("measurend_bad_first_output.jeff"))); -} - -#[test] -fn measurend_bad_second_output() { - assert!(has_bad_output(&load("measurend_bad_second_output.jeff"))); -} - -#[test] -fn free_bad_input_type() { - assert!(has_bad_input(&load("free_bad_input.jeff"))); -} - -#[test] -fn gate_non_qubit_input() { - assert!(has_bad_input(&load("gate_bad_qubit_input.jeff"))); -} - -#[test] -fn gate_non_qubit_output() { - assert!(has_bad_output(&load("gate_bad_qubit_output.jeff"))); -} - -#[test] -fn gate_non_float_param() { - assert!(has_bad_input(&load("gate_bad_param_type.jeff"))); -} - -// ── qubit alloc / free / reset ──────────────── - -#[test] -fn alloc_has_unexpected_input() { - assert!(has_bad_input(&load("alloc_unexpected_input.jeff"))); -} - -#[test] -fn free_has_unexpected_output() { - assert!(has_bad_output(&load("free_unexpected_output.jeff"))); -} - -// ── gate arity ──────────────────────────────── - -fn has_wrong_arity(errors: &[VerificationError]) -> bool { - errors - .iter() - .any(|e| matches!(e, VerificationError::WrongArity { .. })) -} - -#[test] -fn gate_too_few_qubit_inputs() { - assert!(has_wrong_arity(&load("gate_too_few_qubit_inputs.jeff"))); -} - -#[test] -fn gate_wrong_output_count() { - assert!(has_wrong_arity(&load("gate_wrong_output_count.jeff"))); -} - -#[test] -fn gate_missing_param_input() { - assert!(has_wrong_arity(&load("gate_missing_param_input.jeff"))); -} - -// ── qureg ops ──────────────────────────────── - -#[test] -fn qureg_alloc_bad_input_type() { - assert!(has_bad_input(&load("qureg_alloc_bad_input.jeff"))); -} - -#[test] -fn qureg_alloc_bad_output_type() { - assert!(has_bad_output(&load("qureg_alloc_bad_output.jeff"))); -} - -#[test] -fn qureg_free_bad_input_type() { - assert!(has_bad_input(&load("qureg_free_bad_input.jeff"))); -} - -#[test] -fn qureg_extract_index_bad_reg_input() { - assert!(has_bad_input(&load( - "qureg_extract_index_bad_reg_input.jeff" - ))); -} - -#[test] -fn qureg_extract_index_bad_idx_input() { - assert!(has_bad_input(&load( - "qureg_extract_index_bad_idx_input.jeff" - ))); -} - -#[test] -fn qureg_extract_index_bad_qubit_output() { - assert!(has_bad_output(&load( - "qureg_extract_index_bad_qubit_output.jeff" - ))); -} - -#[test] -fn qureg_insert_index_bad_qubit_input() { - assert!(has_bad_input(&load( - "qureg_insert_index_bad_qubit_input.jeff" - ))); -} - -#[test] -fn qureg_length_bad_output_type() { - assert!(has_bad_output(&load("qureg_length_bad_output.jeff"))); -} - -#[test] -fn qureg_join_bad_input_type() { - assert!(has_bad_input(&load("qureg_join_bad_input.jeff"))); -} diff --git a/tools/verifier/tests/positive.rs b/tools/verifier/tests/positive.rs index 8cca687..9f52bbd 100644 --- a/tools/verifier/tests/positive.rs +++ b/tools/verifier/tests/positive.rs @@ -3,14 +3,13 @@ use jeff::reader::ReadJeff; use jeff::Jeff; use std::fs::File; use std::path::Path; -use verifier::verify_module; +use verifier::{verify_module, VerificationError}; -fn load_positive(name: &str) -> Vec { +fn load_positive(name: &str) -> Vec { let path = Path::new(env!("CARGO_MANIFEST_DIR")) .join("tests/positive") .join(name); - let file = File::open(&path) - .unwrap_or_else(|_| panic!("missing fixture: {path:?} — run generate_test_cases.py first")); + let file = File::open(&path).unwrap_or_else(|_| panic!("missing fixture: {path:?}")); verify_module( Jeff::read(file) .expect("failed to parse jeff file") @@ -18,28 +17,89 @@ fn load_positive(name: &str) -> Vec { ) } +fn load_example(rel: &str) -> Vec { + let path = Path::new(env!("CARGO_MANIFEST_DIR")) + .join("../../examples") + .join(rel); + let file = File::open(&path).unwrap_or_else(|_| panic!("missing example: {path:?}")); + verify_module( + Jeff::read(file) + .expect("failed to parse jeff file") + .module(), + ) +} + +// positive tests + +#[test] +fn valid_alloc_gate_measure() { + let errors = load_positive("valid_alloc_gate_measure.jeff"); + assert!(errors.is_empty(), "expected no errors, got: {errors:?}"); +} + +#[test] +fn valid_deep_qubit_chain() { + let errors = load_positive("valid_deep_qubit_chain.jeff"); + assert!(errors.is_empty(), "expected no errors, got: {errors:?}"); +} + +#[test] +fn valid_for_qubit_isolation() { + let errors = load_positive("valid_for_qubit_isolation.jeff"); + assert!(errors.is_empty(), "expected no errors, got: {errors:?}"); +} + +#[test] +fn valid_int_float_ops() { + let errors = load_positive("valid_int_float_ops.jeff"); + assert!(errors.is_empty(), "expected no errors, got: {errors:?}"); +} + +#[test] +fn valid_while_isolation() { + let errors = load_positive("valid_while_isolation.jeff"); + assert!(errors.is_empty(), "expected no errors, got: {errors:?}"); +} + #[test] -fn valid_comprehensive() { - let errors = load_positive("valid_comprehensive.jeff"); - assert!( - errors.is_empty(), - "expected no errors, got:\n{}", - errors - .iter() - .map(|e| format!(" - {e}")) - .collect::>() - .join("\n") - ); +fn valid_three_qubit_gates() { + let errors = load_positive("valid_three_qubit_gates.jeff"); + assert!(errors.is_empty(), "expected no errors, got: {errors:?}"); +} + +// examples +#[test] +fn example_qubits() { + let errors = load_example("qubits/qubits.jeff"); + assert!(errors.is_empty(), "expected no errors, got: {errors:?}"); +} + +#[test] +fn example_entangled_qs() { + let errors = load_example("entangled_qs/entangled_qs.jeff"); + assert!(errors.is_empty(), "expected no errors, got: {errors:?}"); +} + +#[test] +fn example_entangled_calls() { + let errors = load_example("entangled_calls/entangled_calls.jeff"); + assert!(errors.is_empty(), "expected no errors, got: {errors:?}"); +} + +#[test] +fn example_catalyst_simple() { + let errors = load_example("catalyst_simple/catalyst_simple.jeff"); + assert!(errors.is_empty(), "expected no errors, got: {errors:?}"); } #[test] -fn valid_minimal() { - let errors = load_positive("valid_minimal.jeff"); +fn example_catalyst_tket_opt() { + let errors = load_example("catalyst_tket_opt/catalyst_tket_opt.jeff"); assert!(errors.is_empty(), "expected no errors, got: {errors:?}"); } #[test] -fn valid_deeply_nested() { - let errors = load_positive("valid_deeply_nested.jeff"); +fn example_python_optimization() { + let errors = load_example("python_optimization/python_optimization.jeff"); assert!(errors.is_empty(), "expected no errors, got: {errors:?}"); } diff --git a/tools/verifier/tests/positive/valid_alloc_gate_measure.jeff b/tools/verifier/tests/positive/valid_alloc_gate_measure.jeff new file mode 100644 index 0000000000000000000000000000000000000000..37e351ec3389bbcdcf4694d0dc82534198e982be GIT binary patch literal 904 zcmcIi%MJlS5bRx#kZ>RlBH}7>_6IIL!NGxqgaqN_OMI)Vs-CIMWN@Q4-PMnp$IgtI z*%d~V)(C;eA?$&sut#Aw38jy|j%s1Gs@L+UZVimPS5>nvVrtv4LF6Y`;0~IwA*^tv zI)TriPEtA`F7V~pqmb%0$Wz@m_QgmYYxq=mM9zJRT?Ds-rMeq(t|vz5IKihn?Oz;a z_U%8^fB!>u0+%u6*$Jhu99GZAQ_mW2jQ5d`<5+3XuAm#%OHnQX=OQ#;-XD9nv^iLN jX6fI#FZ)Bs^GT8CeBUz|xgU81K5vf~kS*ze#VYU%jua0! literal 0 HcmV?d00001 diff --git a/tools/verifier/tests/positive/valid_alloc_gate_measure.txt b/tools/verifier/tests/positive/valid_alloc_gate_measure.txt new file mode 100644 index 0000000..58bd5a7 --- /dev/null +++ b/tools/verifier/tests/positive/valid_alloc_gate_measure.txt @@ -0,0 +1,36 @@ +( version = 0, + versionMinor = 2, + versionPatch = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [5, 6], + operations = [ + ( outputs = [0], + instruction = (qubit = (alloc = void)) ), + ( outputs = [1], + instruction = (qubit = (alloc = void)) ), + ( inputs = [0], + outputs = [2], + instruction = (qubit = (gate = (custom = (name = 1, numQubits = 1, numParams = 0), controlQubits = 0, adjoint = false, power = 1))) ), + ( inputs = [2, 1], + outputs = [3, 4], + instruction = (qubit = (gate = (custom = (name = 2, numQubits = 2, numParams = 0), controlQubits = 0, adjoint = false, power = 1))) ), + ( inputs = [3], + outputs = [5], + instruction = (qubit = (measure = void)) ), + ( inputs = [4], + outputs = [6], + instruction = (qubit = (measure = void)) ) ] ), + values = [ + (type = (qubit = void)), + (type = (qubit = void)), + (type = (qubit = void)), + (type = (qubit = void)), + (type = (qubit = void)), + (type = (int = 1)), + (type = (int = 1)) ] ) ) ], + strings = ["main", "H", "CX"], + entrypoint = 0 ) diff --git a/tools/verifier/tests/positive/valid_deep_qubit_chain.jeff b/tools/verifier/tests/positive/valid_deep_qubit_chain.jeff new file mode 100644 index 0000000000000000000000000000000000000000..aaaece9e1efd727f08407b4e229ee4351dd52ab4 GIT binary patch literal 1688 zcmds0Jxc^Z49(uHAE$0{VkP#1g;?6#_!Gp=Qc!=Xg^GfLf`W1iS_n3FzL(59huK{a zD=|m%@-i=z+1nj6vkN$FU^9_;9_bjc4sV8Ln^EeFHL8_Clx*Iywq{^9Q4!d{sU5-B z5}#B^lCi!3r;fG-ue`(QG&~_&nliI{h3>4-ou_pnsM{%GKKBNE z1uk?E!X-S{J%CduMCx{nnCo7^d48db5FX*V?j4*uAyT(j#9a3VPMy$22+#0br+Gr@ zemnOQ8*r{r`+XqE=c+DjztLF1XVq!a>r0%?R0E$B)1=cf_1u%+CT~I6$6l_NeJFVk z^>gr__DL7_q}|6;a#lG{`VrP>dd^^R2Ijm&v~pcHd@+_==NrBe^dAL zNw51{o@bjIV22}*PCWcK{{3WsBjY>Et>pPyS6=GJ5N*JT%L!Kt&ie7e;R(QY8DKkm KfeCCssC@xq|1Gxw literal 0 HcmV?d00001 diff --git a/tools/verifier/tests/positive/valid_deep_qubit_chain.txt b/tools/verifier/tests/positive/valid_deep_qubit_chain.txt new file mode 100644 index 0000000..fac04df --- /dev/null +++ b/tools/verifier/tests/positive/valid_deep_qubit_chain.txt @@ -0,0 +1,60 @@ +( version = 0, + versionMinor = 2, + versionPatch = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [9, 10, 13], + operations = [ + ( outputs = [0], + instruction = (qubit = (alloc = void)) ), + ( outputs = [1], + instruction = (qubit = (alloc = void)) ), + ( outputs = [2], + instruction = (qubit = (alloc = void)) ), + ( inputs = [1], + outputs = [3], + instruction = (qubit = (gate = (custom = (name = 1, numQubits = 1, numParams = 0), controlQubits = 0, adjoint = false, power = 1))) ), + ( inputs = [3, 2], + outputs = [4, 5], + instruction = (qubit = (gate = (custom = (name = 2, numQubits = 2, numParams = 0), controlQubits = 0, adjoint = false, power = 1))) ), + ( inputs = [0, 4], + outputs = [6, 7], + instruction = (qubit = (gate = (custom = (name = 2, numQubits = 2, numParams = 0), controlQubits = 0, adjoint = false, power = 1))) ), + ( inputs = [6], + outputs = [8], + instruction = (qubit = (gate = (custom = (name = 1, numQubits = 1, numParams = 0), controlQubits = 0, adjoint = false, power = 1))) ), + ( inputs = [8], + outputs = [9], + instruction = (qubit = (measure = void)) ), + ( inputs = [7], + outputs = [10], + instruction = (qubit = (measure = void)) ), + ( inputs = [5], + outputs = [11], + instruction = (qubit = (gate = (custom = (name = 3, numQubits = 1, numParams = 0), controlQubits = 0, adjoint = false, power = 1))) ), + ( inputs = [11], + outputs = [12], + instruction = (qubit = (gate = (custom = (name = 4, numQubits = 1, numParams = 0), controlQubits = 0, adjoint = false, power = 1))) ), + ( inputs = [12], + outputs = [13], + instruction = (qubit = (measure = void)) ) ] ), + values = [ + (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 = (int = 1)), + (type = (int = 1)), + (type = (qubit = void)), + (type = (qubit = void)), + (type = (int = 1)) ] ) ) ], + strings = ["main", "H", "CX", "X", "Z"], + entrypoint = 0 ) diff --git a/tools/verifier/tests/positive/valid_for_qubit_isolation.jeff b/tools/verifier/tests/positive/valid_for_qubit_isolation.jeff new file mode 100644 index 0000000000000000000000000000000000000000..6f66d42182c882d5370ed99cd8db58511b36f5a0 GIT binary patch literal 1056 zcmc&yyKcfj5L_F=Lka~EiYQYcMWRWao`MpJNNJFuKnjKViF^bNO+GJQkTx^79^cur zMaiJO+1s79_I5Ed`-Ty@J-8Emcc-9N*l%X`?4j1Pk7#DSDmMyV-`-JosiI~R_|%SJ zk0t+s1$8h-APY)moC^@^gfBQ5ez^iAAHk_^k2^I@-L9eg?9hEQbemE)025o-0@kKW zyZeELeTm@)TygRpU5J@DV`}4jdbR4Ps>k^q)+o3tBv literal 0 HcmV?d00001 diff --git a/tools/verifier/tests/positive/valid_for_qubit_isolation.txt b/tools/verifier/tests/positive/valid_for_qubit_isolation.txt new file mode 100644 index 0000000..c025a57 --- /dev/null +++ b/tools/verifier/tests/positive/valid_for_qubit_isolation.txt @@ -0,0 +1,42 @@ +( version = 0, + versionMinor = 2, + versionPatch = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [5], + operations = [ + ( outputs = [0], + instruction = (qubit = (alloc = void)) ), + ( outputs = [1], + instruction = (int = (const32 = 0)) ), + ( outputs = [2], + instruction = (int = (const32 = 1)) ), + ( outputs = [3], + instruction = (int = (const32 = 1)) ), + ( inputs = [1, 2, 3, 0], + outputs = [4], + instruction = (scf = (for = ( + sources = [6, 7], + targets = [8], + operations = [ + ( inputs = [7], + outputs = [8], + instruction = (qubit = (gate = (custom = (name = 1, numQubits = 1, numParams = 0), controlQubits = 0, adjoint = false, power = 1))) ) ] ) )) ), + ( inputs = [4], + outputs = [5], + instruction = (qubit = (measure = void)) ) ] ), + values = [ + (type = (qubit = void)), + (type = (int = 32)), + (type = (int = 32)), + (type = (int = 32)), + (type = (qubit = void)), + (type = (int = 1)), + (type = (int = 32)), + (type = (qubit = void)), + (type = (qubit = void)) ] ) ) ], + strings = ["main", "H"], + entrypoint = 0 ) diff --git a/tools/verifier/tests/positive/valid_int_float_ops.jeff b/tools/verifier/tests/positive/valid_int_float_ops.jeff new file mode 100644 index 0000000000000000000000000000000000000000..5ec52b76c89d0f7f6f13195a51c97a873d40a163 GIT binary patch literal 992 zcmchVyJ|u~5QgXMIq?z_LG%GE1i{WekaRwWT>??G5CjRNP}D-O@xk&oDf9n(afd;O zl>>9;_RZ{`-4zj8Ln%%kg5&+*wqXX)pF*S+QdhqfvW1kFTElyljL^5cWJR9glWju# zP{w00NgNzbsX^<|9<)FQ^IFabo>bxlpN!>>hT9wNfVc~#)$=xn+eVI7bKjBUKWX_w zpt%)d?#*&b!_5u1K+OHo>Up1rn?{aSbMKLZiBigAa$)n)mwp{p^0j=P`E4YIz4^vF zDebNP&%DO(tDchc)f;)%c<)K_+Tq+-=bK2P{hm)cd4bh^_l})}o%rqez5EyFQ(#Y} SZseBO8J^RI(COr3#{NI(k`x~R literal 0 HcmV?d00001 diff --git a/tools/verifier/tests/positive/valid_int_float_ops.txt b/tools/verifier/tests/positive/valid_int_float_ops.txt new file mode 100644 index 0000000..46b1104 --- /dev/null +++ b/tools/verifier/tests/positive/valid_int_float_ops.txt @@ -0,0 +1,41 @@ +( version = 0, + versionMinor = 2, + versionPatch = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [2, 3, 6, 7], + operations = [ + ( outputs = [0], + instruction = (int = (const32 = 10)) ), + ( outputs = [1], + instruction = (int = (const32 = 20)) ), + ( inputs = [0, 1], + outputs = [2], + instruction = (int = (add = void)) ), + ( inputs = [0, 1], + outputs = [3], + instruction = (int = (eq = void)) ), + ( outputs = [4], + instruction = (float = (const64 = 1.5)) ), + ( outputs = [5], + instruction = (float = (const64 = 2.5)) ), + ( inputs = [4, 5], + outputs = [6], + instruction = (float = (add = void)) ), + ( inputs = [4, 5], + outputs = [7], + instruction = (float = (lt = void)) ) ] ), + values = [ + (type = (int = 32)), + (type = (int = 32)), + (type = (int = 32)), + (type = (int = 1)), + (type = (float = float64)), + (type = (float = float64)), + (type = (float = float64)), + (type = (int = 1)) ] ) ) ], + strings = ["main"], + entrypoint = 0 ) diff --git a/tools/verifier/tests/positive/valid_three_qubit_gates.jeff b/tools/verifier/tests/positive/valid_three_qubit_gates.jeff new file mode 100644 index 0000000000000000000000000000000000000000..e67fb6e87a8d1914425f6d096eea324fee3d97a9 GIT binary patch literal 1272 zcmd5)u}VWx3_b7JS}i&#PDPvwg7hz3T-+R79UZJ+;6FGhC}^pm&<@W2p64VtC0yG& z>M6-da!+1f?+XA-XhMsw2Nrv{M>?jRx4@B?mii8>4K@~MTNZV2*8pFODzM8~+HKk) zP5CV~0rlyuUkXEVV;!YXXinZqrFX^+e>L7%$hwymy5~ywQ0X4ac`#GMJ$;`0%KU&9 zY$CcRTGo9qmoAv0VM?EMpUn0C!3+&E`mBrl2re?z_o8`vUU2B94D$1$9{lrW{e)|= z7O@eVN!8jUpH@FtdeyWeU0U6zUd^ogq*Yz|USX2KdzSZUj^O)>w837F`PxY#{*Pxq wOL6RLeLgZ_iwknTtN)(cYyY9sH_P}f*Y`Q0iT4W+$TwHlV-n8fh|^2wZ&*kg>i_@% literal 0 HcmV?d00001 diff --git a/tools/verifier/tests/positive/valid_three_qubit_gates.txt b/tools/verifier/tests/positive/valid_three_qubit_gates.txt new file mode 100644 index 0000000..db0aa40 --- /dev/null +++ b/tools/verifier/tests/positive/valid_three_qubit_gates.txt @@ -0,0 +1,48 @@ +( version = 0, + versionMinor = 2, + versionPatch = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [8, 9, 10], + operations = [ + ( outputs = [0], + instruction = (qubit = (alloc = void)) ), + ( outputs = [1], + instruction = (qubit = (alloc = void)) ), + ( outputs = [2], + instruction = (qubit = (alloc = void)) ), + ( inputs = [0], + outputs = [3], + instruction = (qubit = (gate = (custom = (name = 1, numQubits = 1, numParams = 0), controlQubits = 0, adjoint = false, power = 1))) ), + ( inputs = [3, 1], + outputs = [4, 5], + instruction = (qubit = (gate = (custom = (name = 2, numQubits = 2, numParams = 0), controlQubits = 0, adjoint = false, power = 1))) ), + ( inputs = [5, 2], + outputs = [6, 7], + instruction = (qubit = (gate = (custom = (name = 2, numQubits = 2, numParams = 0), controlQubits = 0, adjoint = false, power = 1))) ), + ( inputs = [4], + outputs = [8], + instruction = (qubit = (measure = void)) ), + ( inputs = [6], + outputs = [9], + instruction = (qubit = (measure = void)) ), + ( inputs = [7], + outputs = [10], + instruction = (qubit = (measure = void)) ) ] ), + values = [ + (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 = (int = 1)), + (type = (int = 1)), + (type = (int = 1)) ] ) ) ], + strings = ["main", "H", "CX"], + entrypoint = 0 ) diff --git a/tools/verifier/tests/positive/valid_while_isolation.jeff b/tools/verifier/tests/positive/valid_while_isolation.jeff new file mode 100644 index 0000000000000000000000000000000000000000..0939019d67ee94b7119f0a5d3fb0335e533ce58a GIT binary patch literal 776 zcmb_Z%L)Q944l?g6jTsA=)tofg1_Kjc-4c52mNdRV`tK4w^T2}29n96)1)Z?T&a?X zadOO0?uxLd-UF~qsh_rCHel4%rsg&H5FcF@SkTwm8FilVLUdsp6Y&F2#vD8B=!oaC zp`$aCoY)docg$(5>4dM_yxODp_r97{6Q46`e%)W<$!f_s&o`0w(!ZnRmG97d#jW}E s)@#1vvVWQv-B148zvkEdwQo&%G;4vGq2tKkDrM+cw;!ml+w-kHEssG6w*UYD literal 0 HcmV?d00001 diff --git a/tools/verifier/tests/positive/valid_while_isolation.txt b/tools/verifier/tests/positive/valid_while_isolation.txt new file mode 100644 index 0000000..bb93e48 --- /dev/null +++ b/tools/verifier/tests/positive/valid_while_isolation.txt @@ -0,0 +1,38 @@ +( version = 0, + versionMinor = 2, + versionPatch = 0, + functions = [ + ( name = 0, + definition = ( + body = ( + sources = [], + targets = [1], + operations = [ + ( outputs = [0], + instruction = (int = (const1 = false)) ), + ( inputs = [0], + outputs = [1], + instruction = (scf = (while = ( + condition = ( + sources = [2], + targets = [3], + operations = [ + ( inputs = [2], + outputs = [3], + instruction = (int = (not = void)) ) ] ), + body = ( + sources = [4], + targets = [5], + operations = [ + ( inputs = [4], + outputs = [5], + instruction = (int = (not = void)) ) ] ) ) )) ) ] ), + values = [ + (type = (int = 1)), + (type = (int = 1)), + (type = (int = 1)), + (type = (int = 1)), + (type = (int = 1)), + (type = (int = 1)) ] ) ) ], + strings = ["main"], + entrypoint = 0 ) From ef691a1a572cbcc8ec3bba5918af11e470f7b277 Mon Sep 17 00:00:00 2001 From: orisus42 Date: Thu, 11 Jun 2026 18:22:03 -0400 Subject: [PATCH 3/5] chore: add encode_tests.sh helper script --- tools/verifier/tests/encode_tests.sh | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100755 tools/verifier/tests/encode_tests.sh diff --git a/tools/verifier/tests/encode_tests.sh b/tools/verifier/tests/encode_tests.sh new file mode 100755 index 0000000..be2d0d1 --- /dev/null +++ b/tools/verifier/tests/encode_tests.sh @@ -0,0 +1,17 @@ +#!/bin/bash +set -e + +if [ $# -ne 1 ]; then + echo "Usage: $0 " >&2 + exit 1 +fi + +dir="$1" +schema="$(dirname "$0")/../../../impl/capnp/jeff.capnp" + +find "$dir" -name "*.txt" -type f | while read -r txt; do + jeff="${txt%.txt}.jeff" + if ! capnp encode "$schema" Module < "$txt" > "$jeff"; then + echo "Error encoding $txt" >&2 + fi +done From d5e457b7e775b95b97e9c15688b0018c21a14d79 Mon Sep 17 00:00:00 2001 From: orisus42 Date: Mon, 15 Jun 2026 13:07:18 -0400 Subject: [PATCH 4/5] fix: refactor type_checks and fix example bitwidth mismatches --- examples/entangled_calls/entangled_calls.jeff | Bin 5752 -> 5752 bytes examples/entangled_calls/entangled_calls.txt | 34 +- examples/entangled_qs/entangled_qs.jeff | Bin 3120 -> 3120 bytes examples/entangled_qs/entangled_qs.txt | 14 +- tools/verifier/src/errors.rs | 2 +- tools/verifier/src/passes/type_checks.rs | 472 +++++++++++++++--- 6 files changed, 422 insertions(+), 100 deletions(-) diff --git a/examples/entangled_calls/entangled_calls.jeff b/examples/entangled_calls/entangled_calls.jeff index a506f32db800cbfb7dfd7f0a647874288a52ea0f..b58979e5db468eb3576d5a1a9a9e24de139c3c37 100644 GIT binary patch delta 160 zcmeyN^FwEY6~|;R4!+3;I5;*3a7QFHTKPG9!PRziG}{RD4KbYNpsEIf>wn|;}~vM@4EX6Dw%Lw@GA1psOK3$*|M delta 62 mcmdlWu|Z;k0~;?R0|bC*t, errors: &mut Vec) { .filter_map(|r| r.ok()) .map(|v| v.ty()) .collect(); - match op.op_type() { OpType::IntOp(int_op) => check_int_op(int_op, &inputs, &outputs, errors), OpType::FloatOp(float_op) => check_float_op(float_op, &inputs, &outputs, errors), @@ -28,6 +29,12 @@ fn check_region_types(region: Region<'_>, errors: &mut Vec) { check_qureg_op(qureg_op, &inputs, &outputs, errors); } OpType::ControlFlowOp(cf_op) => check_cf_region_types(cf_op.as_ref(), errors), + OpType::IntArrayOp(int_array_op) => { + check_int_array_op(int_array_op, &inputs, &outputs, errors); + } + OpType::FloatArrayOp(float_array_op) => { + check_float_array_op(float_array_op, &inputs, &outputs, errors); + } _ => {} } } @@ -55,34 +62,40 @@ fn check_cf_region_types(cf_op: &ControlFlowOp<'_>, errors: &mut Vec bool { - matches!(ty, Type::Int { .. }) +fn is_int(ty: &Type, bits: impl Into>) -> bool { + match bits.into() { + Some(b) => matches!(ty, Type::Int { bits: x } if *x == b), + None => matches!(ty, Type::Int { .. }), + } } -fn is_float(ty: &Type) -> bool { - matches!(ty, Type::Float { .. }) +fn is_float(ty: &Type, precision: impl Into>) -> bool { + match precision.into() { + Some(p) => matches!(ty, Type::Float { precision: x } if *x == p), + None => matches!(ty, Type::Float { .. }), + } } fn is_qubit(ty: &Type) -> bool { - *ty == Type::Qubit + matches!(ty, Type::Qubit) } fn is_qureg(ty: &Type) -> bool { matches!(ty, Type::QubitRegister { .. }) } -fn is_i1(ty: &Type) -> bool { - *ty == (Type::Int { bits: 1 }) +fn is_int_array(ty: &Type) -> bool { + matches!(ty, Type::IntArray { .. }) } -fn is_i32(ty: &Type) -> bool { - *ty == (Type::Int { bits: 32 }) +fn is_float_array(ty: &Type) -> bool { + matches!(ty, Type::FloatArray { .. }) } fn expect_input( inputs: &[Type], idx: usize, - pred: fn(&Type) -> bool, + pred: impl Fn(&Type) -> bool, op: &'static str, errors: &mut Vec, ) { @@ -94,7 +107,7 @@ fn expect_input( fn expect_output( outputs: &[Type], idx: usize, - pred: fn(&Type) -> bool, + pred: impl Fn(&Type) -> bool, op: &'static str, errors: &mut Vec, ) { @@ -103,29 +116,16 @@ fn expect_output( } } -fn check_const_int_output(outputs: &[Type], bits: u8, errors: &mut Vec) { - if outputs - .first() - .is_some_and(|ty| *ty != (Type::Int { bits })) - { - errors.push(VerificationError::InvalidOutputType { - operation: "int const", - }); - } -} - -fn check_const_float_output( +fn check_arity( + inputs: &[Type], + expected_inputs: usize, outputs: &[Type], - precision: FloatPrecision, + expected_outputs: usize, + op: &'static str, errors: &mut Vec, ) { - if outputs - .first() - .is_some_and(|ty| *ty != (Type::Float { precision })) - { - errors.push(VerificationError::InvalidOutputType { - operation: "float const", - }); + if inputs.len() != expected_inputs || outputs.len() != expected_outputs { + errors.push(VerificationError::WrongArity { operation: op }); } } @@ -136,13 +136,13 @@ fn check_uniform_int( errors: &mut Vec, ) { for ty in inputs { - if !is_int(ty) { + if !is_int(ty, None) { errors.push(VerificationError::InvalidInputType { operation: name }); return; } } for ty in outputs { - if !is_int(ty) { + if !is_int(ty, None) { errors.push(VerificationError::InvalidOutputType { operation: name }); return; } @@ -169,13 +169,13 @@ fn check_uniform_float( errors: &mut Vec, ) { for ty in inputs { - if !is_float(ty) { + if !is_float(ty, None) { errors.push(VerificationError::InvalidInputType { operation: name }); return; } } for ty in outputs { - if !is_float(ty) { + if !is_float(ty, None) { errors.push(VerificationError::InvalidOutputType { operation: name }); return; } @@ -202,11 +202,26 @@ fn check_int_op( errors: &mut Vec, ) { match int_op { - IntOp::Const1(_) => check_const_int_output(outputs, 1, errors), - IntOp::Const8(_) => check_const_int_output(outputs, 8, errors), - IntOp::Const16(_) => check_const_int_output(outputs, 16, errors), - IntOp::Const32(_) => check_const_int_output(outputs, 32, errors), - IntOp::Const64(_) => check_const_int_output(outputs, 64, errors), + IntOp::Const1(_) => { + check_arity(inputs, 0, outputs, 1, "int const", errors); + expect_output(outputs, 0, |ty| is_int(ty, 1), "int const", errors); + } + IntOp::Const8(_) => { + check_arity(inputs, 0, outputs, 1, "int const", errors); + expect_output(outputs, 0, |ty| is_int(ty, 8), "int const", errors); + } + IntOp::Const16(_) => { + check_arity(inputs, 0, outputs, 1, "int const", errors); + expect_output(outputs, 0, |ty| is_int(ty, 16), "int const", errors); + } + IntOp::Const32(_) => { + check_arity(inputs, 0, outputs, 1, "int const", errors); + expect_output(outputs, 0, |ty| is_int(ty, 32), "int const", errors); + } + IntOp::Const64(_) => { + check_arity(inputs, 0, outputs, 1, "int const", errors); + expect_output(outputs, 0, |ty| is_int(ty, 64), "int const", errors); + } IntOp::Add | IntOp::Sub | IntOp::Mul @@ -223,14 +238,18 @@ fn check_int_op( | IntOp::RemS | IntOp::RemU | IntOp::Shl - | IntOp::Shr - | IntOp::Not - | IntOp::Abs => { + | IntOp::Shr => { + check_arity(inputs, 2, outputs, 1, "int arithmetic", errors); + check_uniform_int(inputs, outputs, "int arithmetic", errors); + } + IntOp::Not | IntOp::Abs => { + check_arity(inputs, 1, outputs, 1, "int arithmetic", errors); check_uniform_int(inputs, outputs, "int arithmetic", errors); } IntOp::Eq | IntOp::LtS | IntOp::LteS | IntOp::LtU | IntOp::LteU => { + check_arity(inputs, 2, outputs, 1, "int comparison", errors); check_uniform_int(inputs, &[], "int comparison", errors); - expect_output(outputs, 0, is_i1, "int comparison", errors); + expect_output(outputs, 0, |ty| is_int(ty, 1), "int comparison", errors); } _ => {} } @@ -244,19 +263,36 @@ fn check_float_op( ) { match float_op { FloatOp::Const32(_) => { - check_const_float_output(outputs, FloatPrecision::Float32, errors); + check_arity(inputs, 0, outputs, 1, "float const", errors); + expect_output( + outputs, + 0, + |ty| is_float(ty, FloatPrecision::Float32), + "float const", + errors, + ); } FloatOp::Const64(_) => { - check_const_float_output(outputs, FloatPrecision::Float64, errors); + check_arity(inputs, 0, outputs, 1, "float const", errors); + expect_output( + outputs, + 0, + |ty| is_float(ty, FloatPrecision::Float64), + "float const", + errors, + ); } FloatOp::Add | FloatOp::Sub | FloatOp::Mul | FloatOp::Pow - | FloatOp::Max - | FloatOp::Min | FloatOp::Atan2 - | FloatOp::Sqrt + | FloatOp::Max + | FloatOp::Min => { + check_arity(inputs, 2, outputs, 1, "float op", errors); + check_uniform_float(inputs, outputs, "float op", errors); + } + FloatOp::Sqrt | FloatOp::Abs | FloatOp::Ceil | FloatOp::Floor @@ -274,11 +310,18 @@ fn check_float_op( | FloatOp::Asinh | FloatOp::Acosh | FloatOp::Atanh => { + check_arity(inputs, 1, outputs, 1, "float op", errors); check_uniform_float(inputs, outputs, "float op", errors); } - FloatOp::Eq | FloatOp::Lt | FloatOp::Lte | FloatOp::IsNan | FloatOp::IsInf => { + FloatOp::Eq | FloatOp::Lt | FloatOp::Lte => { + check_arity(inputs, 2, outputs, 1, "float predicate", errors); + check_uniform_float(inputs, &[], "float predicate", errors); + expect_output(outputs, 0, |ty| is_int(ty, 1), "float predicate", errors); + } + FloatOp::IsNan | FloatOp::IsInf => { + check_arity(inputs, 1, outputs, 1, "float predicate", errors); check_uniform_float(inputs, &[], "float predicate", errors); - expect_output(outputs, 0, is_i1, "float predicate", errors); + expect_output(outputs, 0, |ty| is_int(ty, 1), "float predicate", errors); } _ => {} } @@ -292,27 +335,28 @@ fn check_qubit_op( ) { match qubit_op { QubitOp::Alloc => { - if !inputs.is_empty() { - errors.push(VerificationError::InvalidInputType { operation: "Alloc" }); - } + check_arity(inputs, 0, outputs, 1, "Alloc", errors); expect_output(outputs, 0, is_qubit, "Alloc", errors); } - QubitOp::Free | QubitOp::FreeZero | QubitOp::Reset => { - expect_input(inputs, 0, is_qubit, "qubit free/reset", errors); - if !outputs.is_empty() { - errors.push(VerificationError::InvalidOutputType { - operation: "qubit free/reset", - }); - } + QubitOp::Free | QubitOp::FreeZero => { + check_arity(inputs, 1, outputs, 0, "qubit free", errors); + expect_input(inputs, 0, is_qubit, "qubit free", errors); + } + QubitOp::Reset => { + check_arity(inputs, 1, outputs, 1, "Reset", errors); + expect_input(inputs, 0, is_qubit, "Reset", errors); + expect_output(outputs, 0, is_qubit, "Reset", errors); } QubitOp::Measure => { + check_arity(inputs, 1, outputs, 1, "Measure", errors); expect_input(inputs, 0, is_qubit, "Measure", errors); - expect_output(outputs, 0, is_i1, "Measure", errors); + expect_output(outputs, 0, |ty| is_int(ty, 1), "Measure", errors); } QubitOp::MeasureNd => { + check_arity(inputs, 1, outputs, 2, "MeasureNd", errors); expect_input(inputs, 0, is_qubit, "MeasureNd", errors); expect_output(outputs, 0, is_qubit, "MeasureNd", errors); - expect_output(outputs, 1, is_i1, "MeasureNd", errors); + expect_output(outputs, 1, |ty| is_int(ty, 1), "MeasureNd", errors); } QubitOp::Gate(gate) => { let num_qubits = gate.num_qubits(); @@ -328,7 +372,7 @@ fn check_qubit_op( if !is_qubit(ty) { errors.push(VerificationError::InvalidInputType { operation: "Gate" }); } - } else if i < num_qubits + num_params && !is_float(ty) { + } else if i < num_qubits + num_params && !is_float(ty, None) { errors.push(VerificationError::InvalidInputType { operation: "Gate" }); } } @@ -350,54 +394,68 @@ fn check_qureg_op( ) { match qureg_op { QubitRegisterOp::Alloc => { - expect_input(inputs, 0, is_i32, "qureg alloc", errors); + check_arity(inputs, 1, outputs, 1, "qureg alloc", errors); + expect_input(inputs, 0, |ty| is_int(ty, 32), "qureg alloc", errors); expect_output(outputs, 0, is_qureg, "qureg alloc", errors); } QubitRegisterOp::Free | QubitRegisterOp::FreeZero => { + check_arity(inputs, 1, outputs, 0, "qureg free", errors); expect_input(inputs, 0, is_qureg, "qureg free", errors); } QubitRegisterOp::ExtractIndex => { + check_arity(inputs, 2, outputs, 2, "qureg extractIndex", errors); expect_input(inputs, 0, is_qureg, "qureg extractIndex", errors); - expect_input(inputs, 1, is_i32, "qureg extractIndex", errors); + expect_input(inputs, 1, |ty| is_int(ty, 32), "qureg extractIndex", errors); expect_output(outputs, 0, is_qureg, "qureg extractIndex", errors); expect_output(outputs, 1, is_qubit, "qureg extractIndex", errors); } QubitRegisterOp::InsertIndex => { + check_arity(inputs, 3, outputs, 1, "qureg insertIndex", errors); expect_input(inputs, 0, is_qureg, "qureg insertIndex", errors); - expect_input(inputs, 1, is_i32, "qureg insertIndex", errors); + expect_input(inputs, 1, |ty| is_int(ty, 32), "qureg insertIndex", errors); expect_input(inputs, 2, is_qubit, "qureg insertIndex", errors); expect_output(outputs, 0, is_qureg, "qureg insertIndex", errors); } QubitRegisterOp::ExtractSlice => { + check_arity(inputs, 3, outputs, 2, "qureg extractSlice", errors); expect_input(inputs, 0, is_qureg, "qureg extractSlice", errors); - expect_input(inputs, 1, is_i32, "qureg extractSlice", errors); - expect_input(inputs, 2, is_i32, "qureg extractSlice", errors); + expect_input(inputs, 1, |ty| is_int(ty, 32), "qureg extractSlice", errors); + expect_input(inputs, 2, |ty| is_int(ty, 32), "qureg extractSlice", errors); expect_output(outputs, 0, is_qureg, "qureg extractSlice", errors); expect_output(outputs, 1, is_qureg, "qureg extractSlice", errors); } QubitRegisterOp::InsertSlice => { + check_arity(inputs, 3, outputs, 1, "qureg insertSlice", errors); expect_input(inputs, 0, is_qureg, "qureg insertSlice", errors); - expect_input(inputs, 1, is_i32, "qureg insertSlice", errors); + expect_input(inputs, 1, |ty| is_int(ty, 32), "qureg insertSlice", errors); expect_input(inputs, 2, is_qureg, "qureg insertSlice", errors); expect_output(outputs, 0, is_qureg, "qureg insertSlice", errors); } QubitRegisterOp::Length => { + check_arity(inputs, 1, outputs, 2, "qureg length", errors); expect_input(inputs, 0, is_qureg, "qureg length", errors); expect_output(outputs, 0, is_qureg, "qureg length", errors); - expect_output(outputs, 1, is_i32, "qureg length", errors); + expect_output(outputs, 1, |ty| is_int(ty, 32), "qureg length", errors); } QubitRegisterOp::Split => { + check_arity(inputs, 2, outputs, 2, "qureg split", errors); expect_input(inputs, 0, is_qureg, "qureg split", errors); - expect_input(inputs, 1, is_i32, "qureg split", errors); + expect_input(inputs, 1, |ty| is_int(ty, 32), "qureg split", errors); expect_output(outputs, 0, is_qureg, "qureg split", errors); expect_output(outputs, 1, is_qureg, "qureg split", errors); } QubitRegisterOp::Join => { + check_arity(inputs, 2, outputs, 1, "qureg join", errors); expect_input(inputs, 0, is_qureg, "qureg join", errors); expect_input(inputs, 1, is_qureg, "qureg join", errors); expect_output(outputs, 0, is_qureg, "qureg join", errors); } QubitRegisterOp::Create => { + if outputs.len() != 1 { + errors.push(VerificationError::WrongArity { + operation: "qureg create", + }); + } for ty in inputs.iter() { if !is_qubit(ty) { errors.push(VerificationError::InvalidInputType { @@ -407,7 +465,271 @@ fn check_qureg_op( } expect_output(outputs, 0, is_qureg, "qureg create", errors); } - #[allow(unreachable_patterns)] + _ => {} + } +} + +fn check_int_array_op( + int_array_op: IntArrayOp<'_>, + inputs: &[Type], + outputs: &[Type], + errors: &mut Vec, +) { + match int_array_op { + IntArrayOp::ConstArray1(_) => { + check_arity(inputs, 0, outputs, 1, "int array const", errors); + expect_output( + outputs, + 0, + |ty| matches!(ty, Type::IntArray { bits: 1, .. }), + "int array const", + errors, + ); + } + IntArrayOp::ConstArray8(_) => { + check_arity(inputs, 0, outputs, 1, "int array const", errors); + expect_output( + outputs, + 0, + |ty| matches!(ty, Type::IntArray { bits: 8, .. }), + "int array const", + errors, + ); + } + IntArrayOp::ConstArray16(_) => { + check_arity(inputs, 0, outputs, 1, "int array const", errors); + expect_output( + outputs, + 0, + |ty| matches!(ty, Type::IntArray { bits: 16, .. }), + "int array const", + errors, + ); + } + IntArrayOp::ConstArray32(_) => { + check_arity(inputs, 0, outputs, 1, "int array const", errors); + expect_output( + outputs, + 0, + |ty| matches!(ty, Type::IntArray { bits: 32, .. }), + "int array const", + errors, + ); + } + IntArrayOp::ConstArray64(_) => { + check_arity(inputs, 0, outputs, 1, "int array const", errors); + expect_output( + outputs, + 0, + |ty| matches!(ty, Type::IntArray { bits: 64, .. }), + "int array const", + errors, + ); + } + IntArrayOp::Zero { bits } => { + check_arity(inputs, 1, outputs, 1, "int array zero", errors); + expect_input(inputs, 0, |ty| is_int(ty, 32), "int array zero", errors); + expect_output( + outputs, + 0, + |ty| matches!(ty, Type::IntArray { bits: b, .. } if *b == bits), + "int array zero", + errors, + ); + } + IntArrayOp::GetIndex => { + check_arity(inputs, 2, outputs, 1, "int array getIndex", errors); + expect_input(inputs, 0, is_int_array, "int array getIndex", errors); + expect_input(inputs, 1, |ty| is_int(ty, 32), "int array getIndex", errors); + if let (Some(Type::IntArray { bits, .. }), Some(out_ty)) = + (inputs.first(), outputs.first()) + { + if !is_int(out_ty, *bits) { + errors.push(VerificationError::TypeMismatch { + operation: "int array getIndex", + }); + } + } + } + IntArrayOp::SetIndex => { + check_arity(inputs, 3, outputs, 1, "int array setIndex", errors); + expect_input(inputs, 0, is_int_array, "int array setIndex", errors); + expect_input(inputs, 1, |ty| is_int(ty, 32), "int array setIndex", errors); + if let Some(Type::IntArray { bits, .. }) = inputs.first() { + let bits = *bits; + if inputs.get(2).is_some_and(|ty| !is_int(ty, bits)) { + errors.push(VerificationError::TypeMismatch { + operation: "int array setIndex", + }); + } + if outputs + .first() + .is_some_and(|ty| !matches!(ty, Type::IntArray { bits: b, .. } if *b == bits)) + { + errors.push(VerificationError::TypeMismatch { + operation: "int array setIndex", + }); + } + } + } + IntArrayOp::Length => { + check_arity(inputs, 1, outputs, 1, "int array length", errors); + expect_input(inputs, 0, is_int_array, "int array length", errors); + expect_output(outputs, 0, |ty| is_int(ty, 32), "int array length", errors); + } + IntArrayOp::Create => { + if outputs.len() != 1 { + errors.push(VerificationError::WrongArity { + operation: "int array create", + }); + } + expect_output(outputs, 0, is_int_array, "int array create", errors); + if let Some(Type::IntArray { bits, .. }) = outputs.first() { + let bits = *bits; + for ty in inputs.iter() { + if !is_int(ty, bits) { + errors.push(VerificationError::TypeMismatch { + operation: "int array create", + }); + break; + } + } + } + } + _ => {} + } +} + +fn check_float_array_op( + float_array_op: FloatArrayOp<'_>, + inputs: &[Type], + outputs: &[Type], + errors: &mut Vec, +) { + match float_array_op { + FloatArrayOp::Const32(_) => { + check_arity(inputs, 0, outputs, 1, "float array const", errors); + expect_output( + outputs, + 0, + |ty| { + matches!( + ty, + Type::FloatArray { + precision: FloatPrecision::Float32, + .. + } + ) + }, + "float array const", + errors, + ); + } + FloatArrayOp::Const64(_) => { + check_arity(inputs, 0, outputs, 1, "float array const", errors); + expect_output( + outputs, + 0, + |ty| { + matches!( + ty, + Type::FloatArray { + precision: FloatPrecision::Float64, + .. + } + ) + }, + "float array const", + errors, + ); + } + FloatArrayOp::Zero { precision } => { + check_arity(inputs, 1, outputs, 1, "float array zero", errors); + expect_input(inputs, 0, |ty| is_int(ty, 32), "float array zero", errors); + expect_output( + outputs, + 0, + |ty| matches!(ty, Type::FloatArray { precision: p, .. } if *p == precision), + "float array zero", + errors, + ); + } + FloatArrayOp::GetIndex => { + check_arity(inputs, 2, outputs, 1, "float array getIndex", errors); + expect_input(inputs, 0, is_float_array, "float array getIndex", errors); + expect_input( + inputs, + 1, + |ty| is_int(ty, 32), + "float array getIndex", + errors, + ); + if let (Some(Type::FloatArray { precision, .. }), Some(out_ty)) = + (inputs.first(), outputs.first()) + { + if !is_float(out_ty, *precision) { + errors.push(VerificationError::TypeMismatch { + operation: "float array getIndex", + }); + } + } + } + FloatArrayOp::SetIndex => { + check_arity(inputs, 3, outputs, 1, "float array setIndex", errors); + expect_input(inputs, 0, is_float_array, "float array setIndex", errors); + expect_input( + inputs, + 1, + |ty| is_int(ty, 32), + "float array setIndex", + errors, + ); + if let Some(Type::FloatArray { precision, .. }) = inputs.first() { + let precision = *precision; + if inputs.get(2).is_some_and(|ty| !is_float(ty, precision)) { + errors.push(VerificationError::TypeMismatch { + operation: "float array setIndex", + }); + } + if outputs.first().is_some_and( + |ty| !matches!(ty, Type::FloatArray { precision: p, .. } if *p == precision), + ) { + errors.push(VerificationError::TypeMismatch { + operation: "float array setIndex", + }); + } + } + } + FloatArrayOp::Length => { + check_arity(inputs, 1, outputs, 1, "float array length", errors); + expect_input(inputs, 0, is_float_array, "float array length", errors); + expect_output( + outputs, + 0, + |ty| is_int(ty, 32), + "float array length", + errors, + ); + } + FloatArrayOp::Create => { + if outputs.len() != 1 { + errors.push(VerificationError::WrongArity { + operation: "float array create", + }); + } + expect_output(outputs, 0, is_float_array, "float array create", errors); + if let Some(Type::FloatArray { precision, .. }) = outputs.first() { + let precision = *precision; + for ty in inputs.iter() { + if !is_float(ty, precision) { + errors.push(VerificationError::TypeMismatch { + operation: "float array create", + }); + break; + } + } + } + } _ => {} } } From ee17a64b79707afcf5c04671e61b8a0ac8fb0bc0 Mon Sep 17 00:00:00 2001 From: orisus42 Date: Thu, 18 Jun 2026 12:03:54 -0400 Subject: [PATCH 5/5] fix: add FuncOp, unknown optype case and SCF TODO --- tools/verifier/src/passes/type_checks.rs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/tools/verifier/src/passes/type_checks.rs b/tools/verifier/src/passes/type_checks.rs index bd50179..38a83c0 100644 --- a/tools/verifier/src/passes/type_checks.rs +++ b/tools/verifier/src/passes/type_checks.rs @@ -35,12 +35,18 @@ fn check_region_types(region: Region<'_>, errors: &mut Vec) { OpType::FloatArrayOp(float_array_op) => { check_float_array_op(float_array_op, &inputs, &outputs, errors); } - _ => {} + // FuncOp only has a function index so type checking calls require to find the + // callee signature at Module level, but this pass is only scoped to a Region. + // TODO: Scope Module into this pass / add a helper pass to build a + // function table for a signature lookup and check out of bounds index + OpType::FuncOp(_) => {} + _ => panic!("Unknown optype"), } } } fn check_cf_region_types(cf_op: &ControlFlowOp<'_>, errors: &mut Vec) { + // TODO: Verify that SCF node input/output types. match cf_op { ControlFlowOp::For { region } => check_region_types(*region, errors), ControlFlowOp::While { condition, body } => {