Extend obligation walkers to closure / quantifier / handler-clause bodies

[aallan]

Summary

The primitive-op obligation walker (_walk_for_primitive_op_obligations in vera/verifier.py, and the sibling @Nat-binding and refinement walkers) recurse into direct-position sites, control flow (if / match / block), call arguments, array-literal elements, and assert/assume conditions — but not into the bodies of closures (AnonFn), quantifiers (ForallExpr / ExistsExpr), or handler clauses (HandleExpr). Those bodies bind fresh slots, so a trapping primitive op inside one (e.g. array_map(arr, fn(@Int -> @Int) { @Int.0 / @Int.1 }), or an index inside a forall body) carries no static obligation.

Not a soundness hole

Codegen emits the divide_by_zero / out_of_bounds runtime traps unconditionally, so such an op traps loudly at runtime — it never silently produces a wrong value. The defect is that vera verify does not report these as Tier-3 obligations (it omits them entirely), so the obligation accounting and the vera verify --json tier counts are incomplete for these positions.

Context

Surfaced in the #680 review (silent-failure-hunter). #680 closed the array-literal and assert/assume positions for division/modulo (E526) and array-index (E527) obligations; this issue tracks the remaining fresh-scope bodies.

Scope

Extend the walkers to recurse into AnonFn / ForallExpr / ExistsExpr / HandleExpr clause and body expressions, recording an obligation at each op site. Most will be Tier-3 (the fresh bindings are unconstrained, so the divisor/index can't be proven) — closure-captured array bounds specifically also need the Tier-2 work in #427. Care is needed with the fresh slot environment: a slot that mistranslates must fall to Tier-3, never produce a false E526/E527.

Affects the nat_sub (E502), nat_bind (E503), refine_bind (E505), div_zero (E526), and index_bounds (E527) obligation kinds.

[aallan]

Scope note (surfaced in the #680 review): the obligation walker also doesn't descend into contract-clause expressions — the requires / ensures / decreases predicates themselves. A trapping primitive op there (e.g. requires(@Int.0 / @Int.1 > 0)) carries no static E526/E527.

Like the fresh-scope bodies this issue already tracks, it's a reporting-completeness gap, not a soundness hole: the runtime contract check surfaces a loud precondition violation, and a concrete violating caller is rejected at the call site during verify. Folding it into this issue's scope.

Extra care when implemented: a contract walk must honour && / || short-circuit (so requires(@Int.1 != 0 && @Int.0 / @Int.1 > 0) discharges rather than false-firing) and use the right slot env per clause (ensures sees the result and old(...) bindings).