Statement/expression forms rejected in verity_contract bodies: if-without-else, mutable monadic rebinds, Int256/Bool ternaries, Bool negation

Statement/expression shapes that Solidity uses everywhere and that verity_contract rejects with "unsupported do element" / "unsupported expression in verity_contract body" (#1003). Each snippet is a minimal repro on c907fef0 (lake env lean on a file importing Contracts.Common):

1. if without else:

function t (a : Uint256) : Unit := do
  if a == 0 then
    setStorage x 1      -- unsupported do element

2. Monadic rebind of a mutable local, and typed mutable init:

let mut total := (0 : Uint256)
if a > 0 then
  total ← addPanic total a   -- unsupported (only `let t ← ...; total := t` works)
let mut g : Int256 := 0      -- unsupported do element (`let mut g := toInt256 0` works)
let mut g ← subPanic a b     -- unsupported do element

3. Pure if (ternary) restrictions:

let v := if a == 0 && b == 1 then a else b    -- unsupported (`&&` in condition)
let g := if g0 > h then g0 else h             -- unsupported (Int256 comparison / branches)
let flag := a == 0
let w := if flag then a else b                -- unsupported (Bool local as condition)

4. Bool negation and comparison:

if !flag then ...            -- unsupported
if flag == false then ...    -- unsupported
_check (not (a == 0))        -- bitwise not requires a word-like value

Pareto's _virtualPriceAux, _updateAccounting, startEpoch, _stopEpoch are full of these (int256 ternaries, if (x) return;, -_totalBBGain >= int256(_lastNAVBB)). The closure translation rewrites all of them into statement-level if/else pure () with mutable locals, which reads far from the Solidity.

Ask: desugar if c then s to if c then s else pure () (trivial), accept x ← e / let mut x ← e / let mut x : T := v, allow &&/||/! over Bool locals and pure if over Int256.

Closure-side tracking: audit/VERITY-GAPS.md G8/G9/G10.

Read audit/VERITY-GAPS.md entries G8/G9/G10, then reproduce the listed forms in a file importing Contracts.Common with lake env lean. Trace the verity_contract handling that reports the unsupported do-element and expression errors. Done means the listed statement, mutable-binding, Boolean, and Int256 conditional forms are accepted without the closure-side rewrites described in the issue.