feat: add verification tool

[orisus42]

This PR closes #57

The verifier is at tools/verifier. Its public API is one function:
pub fn verify_module(module: Module<'_>) -> Vec<VerificationError>

Callers can pass the decoded module from Jeff::read(...).module() and get back a list of every verification error found. An empty list means the module is valid.

Architecture

The verifier iterates over all functions in the module. For each function definition it runs sequential passes. Declarations (functions without a body) are skipped since they have no code to verify.

All passes append to the same shared Vec<VerificationError>. The verifier is non-fatal, such that it collects every error it finds rather than stopping at the first one. This lets it show the user all the invalid structures in the program.

The current passes check the following requirements as stated in the issue:

• Are all required module attributes (e.g., version and entrypoint) set?
• Is a value used before it is defined?
• Are all values used in a function's body defined in its values list?
• Are all input and output values of the expected type?
• Are the input and output values of a given integer or float operation (e.g., add or max) of the same type (i.e., the same bitwidth or float precision)?
• Is linearity respected, i.e., are all qubit and qureg values used exactly once?
• Are all regions isolated from above?

Pass 1 (Module Attributes)

Version Check - A value of 0.0.0 means the version was not set.
Entrypoint - module.entrypoint_id() must refer to an index that exists in the function list AND that function must be a definition, not a declaration. Anything else raises a verification error.

Pass 2 (Value Checks)

Out-of-bounds - The reader yields ReadError:ValueOutOfBounds which is piped to a verification error.
Use-before-defined - This checks for programs where an operator consumes a value that is produced later (or never produced at all).
Linearity - Qubits and qubit registers are linear types: they must be produced exactly once and consumed exactly once. The analysis module walks the entire region tree and increments per-value producers and consumers counters:
- A region source counts as one producer.
- An op output counts as one producer.
- A region target counts as one consumer.
- An op input counts as one consumer.

Pass 3 (Type Checks)

For each operation the verifier reads the types of its actual inputs and outputs from the value table, then checks them against the operation's expected signature. The pass recurses into all nested regions so every operation in the program is covered.

Pass 4 (Region Isolation)

It follows MLIR's IsolatedFromAbove semantics for structured control flow regions: a nested region cannot directly reference a value from an outer scope. Values must be explicitly passed in via the region's sources list.

Isolation violations no longer trigger UsedBeforeDefined.
UsedBeforeDefined is an ordering check which checks if this value was produced before it was used, within this scope. Outer-scope values ARE produced before the nested region runs, so the answer is yes.
IsolationViolation is a scoping check which asks whether it captured something from outside without going through sources.

Future changes

• Inter-function checks can be implemented
• Linearity is checked globally, it can be made branch-sensitive
• Arity of region inputs and outputs can be checked
• Similarly, arity of measurements can also be checked
• Verification errors can be made to point to the exact instruction that fails the check
• An option to stop the verifier once the first verification error occurs would be useful for debugging

Tests

Some tests that cover all the verification error codes were added. Other tests can be generated on demand using a Python or Bash script in future updates.

AI Disclosure:

The architecture and design process was completely human, GPT-5.5 was used to assist me in understanding concepts from the repository and verify my thoughts for the implementation. GPT-5.5 and Claude Sonnet 4.6 was used in writing code and generating the large set of test cases. Each section of code for the verifier was generated only after scrutiny by me. Most of the test cases generated were verified by me, and running the verifier on the complete set of test cases passed as expected. None of the above PR description was generated by any LLM.

[orisus42]

Some CI checks are failing due to me removing the tests at the end and replacing them with the scripts. I'll update the PR so that those tests aren't run by default until the generator scripts are run.

[denialhaag]

Thanks a lot for your contribution, @orisus42! This already looks really good to me! 🙂

I left some minor comments; you can find them below.

Regarding the testing, I'd be completely fine if you commit the .jeff files for now. Don't worry if it's too much of a hassle to set up a workflow that generates the .jeff files on demand. We can easily do that in a follow-up!

[denialhaag]

I'm wondering whether this should enforce something slightly stricter. Most likely, a given version of the verifier can only be used on jeff programs written for a specific version of the spec.

That said, this may be too hypothetical at this point and can be addressed when the issue arises in the future. Furthermore, if a version check is needed, it should probably already occur in lib.rs, and the verifier should immediately exit, stating that it is incompatible with the jeff program.

[orisus42]

It would make sense for the version check to actually confirm whether the right version is being used, however for this implementation what I found was that if the version is not set explicitly then it defaults to 0.0.0 which obviously isn't valid, hence that check suffices for an unset version check. You're right however, this check can be upgraded into two unique errors, MissingVersion for when the version is 0.0.0 and IncompatibleVersion for when it is anything different (although if a version is not set in that case then it would trigger both the errors, but it can be made more explicit by making sure IncompatibleVersion does not trigger on 0.0.0 which serves as an indicator of an unset version).

[denialhaag]

I agree that this should be treated as two separate errors. I would definitely keep MissingVersion as is and maybe add a separate IncompatibleVersion error.

[denialhaag]

I like how you implemented this now! 👍

[orisus42]

I would like to mention that the reader has its own version check completely separate from the verifier's. Before any verification can happen, reader validates the version against its own supported range (for now it means that if the version is above 0.2.x it returns a Err(JeffError::VersionTooNew) and never gives a Module to pass to the verifier as it returns right there. Currently for the incompatible version test it uses the version 0.1.0 which doesn't cause this panic but it might be informational to document this behavior and perhaps come up with an implementation later that kind of deals with this better.

When I tried using the version 0.3.0, our test calls .expect("failed to parse jeff file") on that result, which turns the Err into a panic. There might also be better ways for the verifier to have compatible versioning with jeff programs, might need to look into this.

[denialhaag]

Yeah, I guess the verifier could be compatible with a range of versions, for example. I'm personally fine with the current implementation. We can adjust this when the issue comes up. 🤔

[denialhaag]

Down the line, we could also define another function that accepts a path to a .jeff file. This function could catch the VersionTooNew error during reading and then return a "nicer" error. We can add this function when we make the verifier a CLI tool in a follow-up. 😌

[orisus42]

I will simplify some tests further and combine any tests that I can! Will commit the .jeff files with their corresponding .txt after cleaning the code up a bit and doing the changes as recommended.

[denialhaag]

Thanks a lot for addressing all of my comments! 🙂

Besides the one comment below, this looks good to me now. I'll approve already and leave the final review to @aborgna-q.

[aborgna-q]

It may have been cleaner to define a validation trait and implement it for each variant, but no need to change that for this PR.

[aborgna-q]

We're ignoring multiple variant here.

[denialhaag]

Ohh, yeah, I must have missed this... IntArrayOp and FloatArrayOp are missing. It's important to check that, e.g., the bitwidth of the output of IntArrayOp.getIndex must coincide with the bitwidth of the underlying intArray.

[orisus42]

Added IntArrayOp and FloatArrayOp checks (arity and type). For getIndex, setIndex and create the bitwidths coincide with the underlying array bitdwitdths. Refactored type_checks.rs pass for slightly cleaner code.

I have also fixed two examples from the examples/ directory because the verifier was using those examples as positive tests and there was an issue with setIndex in two of the examples which caused the verifier to raise errors on the unmatching bitwidths.

One operator is left to implement which is FuncOp but all it does is call another function using the function's index, I haven't implemented this because currently the TypeChecks pass only receives the Region and to type check the signature (and the arity) for an inter-function call it would require that I thread the top level Module through the pass and needs more infrastructure (I'm guessing this type check would require a lookup through some kind of table that stores function signatures and indexes them by their func_idx, making sure that the called index is not out of bounds). I thought that this might require more significant refactoring (like a seperate analytic pass which builds this signature table) and if we decide to go through that then it would also mean that we could further simplify the TypeChecks pass.

[orisus42]

Would also like to request any maintainer to assign me to this issue before merging as mentioned by the unitaryHACKS organizing team that a bot checks assigned members to collect information about the bounties.

[aborgna-q]

Ok for skipping FuncOp, but please add an explicit case with a comment explaining what we are not checking, and why.

            // ...
            OpType::FuncOp(_) => {}
            _ => {panic!("Unknown optype")}

[orisus42]

I have added the comments and the case if the verifier encounters a new OpType from a future jeff update.

[orisus42]

Hi @aborgna-q ! It's been a few days, just wanted to make sure if you could look into this once more and let me know your thoughts. Sorry for tagging after already requesting a review, but it would be awesome if we can have the verifier ready soon as the unitaryHACKS event has ended now!

[aborgna-q]

Some minor last comments

Would also like to request any maintainer to assign me to this issue before merging as mentioned by the unitaryHACKS organizing team that a bot checks assigned members to collect information about the bounties.

We'll assign you to the issue once the PR is merged. The bot will pick your name from there.

[aborgna-q]

Ok for skipping FuncOp, but please add an explicit case with a comment explaining what we are not checking, and why.

            // ...
            OpType::FuncOp(_) => {}
            _ => {panic!("Unknown optype")}

[aborgna-q]

Thanks!
CI is failing due to some unrelated dependency update. I'll merge the fix in #70 first and then update this branch.

[denialhaag]

Alright, I'll go ahead and merge this now! @orisus42, thanks a lot for your contribution! @aborgna-q, thanks a lot for the additional review! 🙂