Loop invariant operations

[0xddom]

This PR adds operations for expressing loop invariants.

Invariants are defined with the verif.invariant operation and the other operations added in this PR
are meant to be used within the body of that operation.

Also introduces two interfaces for handling contract and invariant targets. These interfaces abstract the exact operation that is
targeted by either a contract or an invariant. The contract target interface has been implemented for function.def and struct.def
while the invariant target interface has been implemented for scf.while and scf.for.

[github-actions]

Test Results

  2 files  ±0    2 suites  ±0   4m 59s ⏱️ +26s
249 tests +2  243 ✅ +2   6 💤 ±0  0 ❌ ±0 
498 runs  +4  486 ✅ +4  12 💤 ±0  0 ❌ ±0 

Results for commit 638b6f4. ± Comparison against base commit 4ed7a42.

[iangneal]

Suggested change

[iangneal]

We should add some tests here to check for mismatched loop args and init args.

[iangneal]

We should add some tests here for loops with init args

[iangneal]

I think this can be replaced with walkCollect

[iangneal]

I didn't see any tests with these inner ops added, we should add some.

[Kuhai9801]

I had one broader concern while reading through this.

The feature direction makes sense, but verif.invariant still feels under-specified as an IR construct. The op defines a loop label, argument types, and a single block, but the verifier currently seems to only resolve the loop label and check argument type compatibility. I do not see verifier rules that define what a valid invariant body must contain or what shape later passes can rely on. See the verif.invariant definition and the invariant verifier.

One thing I found confusing is the use of verif.require_compute inside verif.invariant. require_compute still implements the precondition interface, and the existing contract verifier collects nested PreconditionOpInterface ops by walking the contract. So unless this is intentional, an invariant predicate written this way is still part of the contract-precondition machinery rather than a distinct invariant predicate language. See RequireOpBase, PreconditionOpInterface, the contract verifier walk, and the current invariant test shape.

I also had questions about the structure of the new ops. Most of the invariant-related ops use ancestor checks rather than tighter placement rules. That makes it hard to tell whether nested invariants, nested steps, ranking ops inside steps, or broad verif.old usage are meant to be valid. If those are valid, it would help to spell out the semantics. If not, it seems worth rejecting them in the verifier. See the invariant inner op definitions.

The loop target binding also seems worth clarifying. The syntax looks symbol-like, for example for @loopA, but the implementation matches a string against discardable loop_label attributes found by walking the target. That could be surprising because it reads like a scoped symbol reference, but does not seem to have symbol semantics. See the loop_label lookup and the parser/printer.

Some tests that would make the intended behavior clearer: loops with init/iter args, duplicate labels in different scopes, nested invariant/step cases, misplaced inner ops, old on constants or step-local values, and an explicit test showing whether require_compute inside an invariant is intended to be valid.

Overall I like the direction. I think this would be easier to build on if the invariant sublanguage had a more precise contract before more passes start depending on it.