Add verification tool

[denialhaag]

Note

This issue is part of unitaryHACK 2026; note that you have to be registered to complete this issue. Learn more about the PR review process here. 

A message from unitaryHACK about AI Slop: "While we allow LLMs as collaborative tools, fully AI-generated PRs are prohibited. Maintainers have the right to reject any contribution that appears to be automated or lacks human oversight."

Learn more about unitaryHACK rules and opportunities here and about the usage of AI, in particular, here!

Description

The Cap'n Proto schema does not necessarily prevent the creation of invalid jeff programs. It would be nice to add a tool that can verify whether an encoded jeff program is valid.

A first version of this tool should check:

• 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?

Acceptance criteria

• The verification tool can check all of the bullet points listed above.
• Each bullet point is tested with at least one positive and one negative test.
• The tests are run in the CI.
• The verifier is implemented in either Python, Rust, or C++.
• The implementation lives at tools/verifier/.

[orisus42]

I was looking through the repository trying to understand the workflow, and wanted to confirm a few things before continuing with my implementation of the verifier. I'm building it in Rust as a library crate (if you need a binary, it only needs a wrapper for it to work). The Rust implementation files of jeff expose the reader API publicly so the verifier directly operates on that instead of the Cap'n Proto raw schema objects. It works through passes, for example, if we wanted to verify a Module there will be first an analysis pass that constructs the graph information by counting productions and consumptions of all values in a Region. Then from that AnalysisTable, it will run the other verifier passes which check for module attributes, definition and use errors, type errors and scope (region isolation).

Admittedly, there needs to be some more design logic towards it for it to work properly with region isolation as there can be nested regions from what I understood from the workflow due to control flow statements which I feel like might need to be implemented in the analysis pass itself for recursive counting in regions.

[denialhaag]

@orisus42, thanks a lot for your interest in implementing this! 🙂

I was looking through the repository trying to understand the workflow, and wanted to confirm a few things before continuing with my implementation of the verifier. I'm building it in Rust as a library crate (if you need a binary, it only needs a wrapper for it to work). The Rust implementation files of jeff expose the reader API publicly so the verifier directly operates on that instead of the Cap'n Proto raw schema objects. It works through passes, for example, if we wanted to verify a Module there will be first an analysis pass that constructs the graph information by counting productions and consumptions of all values in a Region. Then from that AnalysisTable, it will run the other verifier passes which check for module attributes, definition and use errors, type errors and scope (region isolation).

A Rust crate would be a great starting point! It also makes sense to use the reader API rather than building this on top of Cap'n Proto objects. Without having seen it, the proposed implementation sounds reasonable as well.

Admittedly, there needs to be some more design logic towards it for it to work properly with region isolation as there can be nested regions from what I understood from the workflow due to control flow statements which I feel like might need to be implemented in the analysis pass itself for recursive counting in regions.

Yes, nested regions can absolutely be a thing (e.g., consider a switch statement inside of a for loop).

[Forage409]

Opened a focused Rust verifier implementation in #65. It checks schema major version, entrypoint bounds, value resolution/use-before-definition, nested control-flow regions, and function-call targets, with tests on existing examples.