verity_contract bodies hit a Lean 4.31 do-notation elaboration failure (name-dependent) with mutable reassignments interleaved with binds

[Th0rgal]

Found while translating Pareto IdleCreditVault.prepareStopEpochWithApr0 (closure repo gap G19). This is a Lean 4 core do-elaborator issue, not a macro bug, but every verity_contract body is a Lean do block, so translators hit it and the error is opaque.

Symptom (lean4 v4.31.0, the toolchain pinned by Verity): with three let mut locals and an if whose branch interleaves let x ← e binds with reassignments, the if (and an else pure () arm) is elaborated against the word type instead of Unit:

type mismatch, result value has type
  Unit
but is expected to have type
  Uint256

It depends on the identifier names only. Plain StateM repro (no Verity import):

def step (n : Nat) : StateM Nat Nat := do
  modify (· + 1); return n + 1

-- fails
def r0 (_interest _pendingFees g fee : Nat) : StateM Nat (Nat × Nat) := do
  let mut _expInterest := _interest
  let mut _adjPendingWithdrawFees := _pendingFees
  let mut _apr0NetInterest := 0
  if g != 0 then
    let n ← step fee
    _apr0NetInterest := n
    let a2 ← step _adjPendingWithdrawFees
    _adjPendingWithdrawFees := a2
    let e2 ← step _expInterest
    _expInterest := e2
  return (_expInterest, _adjPendingWithdrawFees)

-- elaborates: only the third mutable is renamed (`_apr0NetInterest` -> `q`)
def r2 (_interest _pendingFees g fee : Nat) : StateM Nat (Nat × Nat) := do
  let mut _expInterest := _interest
  let mut _adjPendingWithdrawFees := _pendingFees
  let mut q := 0
  if g != 0 then
    let n ← step fee
    q := n
    let a2 ← step _adjPendingWithdrawFees
    _adjPendingWithdrawFees := a2
    let e2 ← step _expInterest
    _expInterest := e2
  return (_expInterest, _adjPendingWithdrawFees)

Renaming other locals (_aprNetInterest still fails, _x0y, _zzz pass), adding a type ascription, adding else pure (), or reading the third mutable afterwards do not change the outcome; hoisting the binds above the reassignments always works:

  if g != 0 then
    let n ← step fee
    let a2 ← step _adjPendingWithdrawFees
    let e2 ← step _expInterest
    _apr0NetInterest := n
    _adjPendingWithdrawFees := a2
    _expInterest := e2

Suggested Verity actions (small):

1. Document the pitfall and the binds-first workaround in docs/MODIFIERS_AND_INHERITANCE.md or the contract-authoring guide, next to the existing let mut notes.
2. Optionally have the macro detect the shape (reassignment, bind, reassignment inside one branch) and emit a hint pointing at the workaround, since the raw Lean error names no variable.
3. Report upstream to leanprover/lean4 with the repro above (I did not find an existing issue).

Context: Pareto translation review of #2413 (issues #2415-#2424, PR #2425).