verifier: @Nat → @Int widening of a value > i64.MAX is unsound (Tier-1 proves a false postcondition)

[aallan]

Found while fixing #812 (PR #811). A distinct, more serious soundness hole than #812: this is not about literals, and it is not codegen-guarded — it silently runs and violates a proved contract.

@Nat is u64 and @Int is i64, and @Nat <: @Int. But a @Nat value in (i64.MAX, u64.MAX] reinterprets its bit pattern when widened to @Int (e.g. u64.MAX → -1), while the verifier reasons over the unbounded non-negative mathematical value. So Tier-1 proves postconditions the runtime then violates.

Repro:

public fn widen(@Nat -> @Int)
  requires(true) ensures(@Int.result >= 0) effects(pure)
{ @Nat.0 }

$ vera verify widen.vera          # ensures(@Int.result >= 0) verifies CLEAN at Tier 1
$ vera run widen.vera --fn widen -- 18446744073709551615
Error: Postcondition violation in widen(@Nat -> @Int)
  ensures(@Int.result >= 0) failed

The verifier proves result >= 0 (a @Nat is non-negative), but the runtime returns -1 for the u64.MAX input — a Tier-1/runtime divergence, exactly the #392 class.

Scope vs #812: #812 (fixed in #811) range-checks integer literals at check time. This issue is about non-literal @Nat values crossing the @Nat → @Int boundary — the subtype relation, not a literal. The negated-literal corner -18446744073709551615 (magnitude in the u64 band) is one manifestation that #812's literal check also does not cover.

Fix direction (a focused #392-style sub-task, like #798/#799): emit a verifier obligation at every @Nat → @Int coercion site that the value is <= i64.MAX — provably safe → Tier 1; provably unsafe → loud error; dynamic → runtime-guarded Tier 3 — with a codegen guard mirror and a verify-vs-run differential. (Alternatively reconsider whether @Nat <: @Int should be implicit at all.)

Parent: #392 (the smt.py/verifier↔runtime soundness audit).