feat(transform): Add ProcBodyVerify transformation

[MikaelMayer]

Summary

Adds ProcBodyVerify transformation converting procedures to verification statements. Complements CallElim by providing the callee's view of verification.

Example

Input procedure:

procedure P(x: int) returns (y: int)
spec {
  modifies g;
  requires x > 0;
  ensures y > 0;
  ensures g == old g + 1;
}
{ y := x; g := g + 1; }

Output verification statement:

block "verify_P" {
  init x; init y;
  init old_g; init g := old_g;
  assume "pre_0" (x > 0);
  block "body_P" { y := x; g := g + 1; }
  assert "post_0" (y > 0);
  assert "post_1" (g == old_g + 1);
}

Implementation

• Initializes parameters and modified globals (with old/new state)
• Converts non-free preconditions to assumes
• Wraps body in labeled block
• Converts non-free postconditions to asserts
• Uses getIdentTy! for proper type lookup

Testing

DDM-based tests verify transformation output matches expected structure for:

• Procedures with modifies clauses
• Free specifications
• Multiple modified globals

[atomb]

That was a good catch! A one-identifier change can make so much difference.

It's encouraging that the proof became substantially longer.

I left a few comments (all from Kiro), but they're all minor proof style things.