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.