feat: Add verification tool for jeff programs#66
Conversation
Checks all 7 requirements from issue #57: - Required module attributes (entrypoint bounds) - SSA validity (values defined before use) - Type consistency for all operations - Int/float operand type consistency (bitwidth/precision) - Qubit linearity (consumed at most once) - Region isolation (nested regions don't bypass boundaries) Tests: 9 integration tests (3 positive + 6 negative) covering all checks.
This comment was marked as low quality.
This comment was marked as low quality.
denialhaag
left a comment
denialhaag
left a comment
There was a problem hiding this comment.
Thanks for also working on the verifier, @kawacukennedy! 🙂
I had an initial look at your implementation, and you can find some feedback below. This is already going in the right direction!
| fn check(&self, module: &Module<'_>) -> Vec<CheckError> { | ||
| let mut errors = vec![]; | ||
|
|
||
| let entry_id = module.entrypoint_id() as usize; | ||
| let func_count = module.function_count(); | ||
| if entry_id >= func_count { | ||
| errors.push(CheckError { | ||
| check_name: self.name(), | ||
| message: format!( | ||
| "Entrypoint index {entry_id} is out of bounds: module has {func_count} function(s)." | ||
| ), | ||
| }); | ||
| } | ||
|
|
||
| errors | ||
| } |
There was a problem hiding this comment.
This should probably raise an error if entrypoint is not specified (see, e.g., entangled_qs.txt)
There was a problem hiding this comment.
It looks like this is not tested.
| //! - Required module attributes (entrypoint, tool name/version) | ||
| //! - SSA validity (all values defined before use) | ||
| //! - Type consistency for operations | ||
| //! - Qubit linearity (qubits consumed at most once) |
There was a problem hiding this comment.
Qubits must be used exactly once. Every qubit must be either destructively measured or freed. The respective check should be adapted and tested accordingly.
| //! Verification tool for jeff programs. | ||
| //! | ||
| //! Checks a jeff file for common issues including: | ||
| //! - Required module attributes (entrypoint, tool name/version) |
There was a problem hiding this comment.
Strictly speaking, the tool name and version are not required attributes.
There was a problem hiding this comment.
The checks here look pretty good already, but it would be nice to improve the test coverage beyond the add operations.
…n, test coverage, doc fix - attributes: Error when entrypoint not specified (entrypoint_id == 0 with functions) - linearity: Add qubit leak detection (every qubit must be consumed exactly once) - isolation: Add region isolation test fixture and integration test - types: Add int_sub_bitwidth and float_mul_mismatch test coverage - main: Fix doc comment (tool name/version not required) - All fixtures updated with explicit entrypoint for multi-function modules
This comment was marked as low quality.
This comment was marked as low quality.
2 participants
Closes #57.
Adds verification tool at
tools/verifier/that checks all 7 requirements from the issue:Implementation
tools/verifier/using the reader API (jeff::reader)clapfor command-line verificationattributes,ssa,types,linearity,isolationcargo test -p jeff-verifyCI integration
tools/verifier/**added to the Rust change filter so CI triggers on verifier changesCargo.tomlupdated to includetools/verifierNotes
matches!for array type length wildcards (avoids false positives on intArray/FloatArray length mismatches)qubits,entangled_qs, andentangled_callsall pass cleanly