squin Verification Analyses

[johnzl-777]

The current rewrite approach to #19 attempted in #148 would be much better handled in terms of codegen. To that end, and to follow the proper usage pattern @Roger-luo has pointed out to me where rewrites/codegen are only attempted when equivalence is guaranteed, another analysis pass should exist to catch squin programs that are structured in a way that cannot be translated to stim.

[johnzl-777]

@weinbe58 and I had the opportunity to talk over what this would look like in more detail as well as @Roger-luo 's recommendation of a custom Error type for error handling.

Before going any further, @weinbe58 pointed out to me that it's useful to have two verification passes. One that just ensures the squin program is syntactically valid, with another one being able to build off that pass and ensure a narrower definition so Stim codegen can happen without a hitch.

For the first "is valid squin program" analysis, the structure we agreed upon for implementation goes something like this:

1. Let the standard address analysis and site analysis passes run as-is. No attempt to raise/detect errors is made at this point
2. Let the data of both analyses get injected into the hints of the program via the WrapSquinAnalysis pass in squin to stim rewrite #148
3. Have another analysis pass that can take advantage of the injected information to generate errors

The final analysis pass would have a type lattice like the following:

HasError (bottom) -> know there is error, but not where
Error (concrete info) -> know there is error, AND where it is
NoError (top) -> no error at all 

join(NoError, Error) -> Error
join(NoError, NoError) -> NoError
join(Error, Error) (diff values) -> HasError (lose the concrete info but you don't care what the info is beyond this point)
join(Error, Error) (same values) -> Error (with data plugged in)
join(Error, HasError) -> HasError

@weinbe58 has also pointed out that this idea of having a "broader" base verification pass that you can then build upon might also be worth making more generic and a feature of Kirin itself.

[weinbe58]

Oh one thing to consider about the lattice: what if we can't infer there is an error? Do we need to have an Unknown as well?

[Roger-luo]

Oh one thing to consider about the lattice: what if we can't infer there is an error? Do we need to have an Unknown as well?

do you have an example?

[Roger-luo]

I think if you cannot infer there is an error it should be NoError? Unless there is a warning.

[weinbe58]

do you have an example?

E.g. I have an OperatorType with and site analysis value of AnySites you can't infer an error. It could be bad or not.

[weinbe58]

I think if you cannot infer there is an error it should be NoError? Unless there is a warning.

I think it might make sense to have warnings here like we can enable/disable them as needed.

[weinbe58]

@johnzl-777 maybe you can think about adding a Warning value? think about how it fits into the lattice.

[johnzl-777]

Some additional discussion on subcomponents and infrastructure for the verification analyses with @weinbe58 . I'll spawn of some sub-issues to keep track of everything soon.

• There should be a shared infrastructure for the squin verification along with squin -> stim compatibility verification in the qubit and wire dialects
• @weinbe58 pointed out that it would be nice if the interpreter infrastructure in Kirin (in cases where analyses are orthogonal - that is, there is no dependency on one analysis with the other AND running a pass incurs some high resource cost) could allow for multiple methods to be called per statement as opposed to having two separate passes.
  • This whole idea spawned from the fact that, on top of the site analysis/enforcement, it would also be desirable to ensure a program doesn't contain illegal qubit usage (like applying a CX where both the target and control are the same qubit), and that you could figure both of these things simultaneously as you traverse the program

[Roger-luo]

Are we implementing this somewhere?

[johnzl-777]

@Roger-luo the shared infrastructure and all these analyses? Yes, they'll get their own PRs quite soon. I think the second bullet point from @weinbe58 is just something that could be useful for Kirin (: