Auto view-frame proof fails on require/revert and static calls, forcing view markers to be dropped

The auto-generated <fn>_view_frame theorem (Verity/Macro/Bridge.lean, mkViewFrameTheoremCommand) is proved with a fixed simp set and fails with "unsolved goals" as soon as the view body (transitively) contains require/revert or an external static call:

verity_contract F1 where
  storage
    p : Uint256 := slot 0
  function internal view r0 () : Unit := do
    let v ← getStorage p
    require (v == 0) "paused"        -- error: unsolved goals  (goal: match (if storageWords .. = 0 then success .. else revert ..) with ...)

verity_contract J3 where
  storage
    t : Address := slot 1
  interfaces
    interface IT where
      function totalSupply() view returns (Uint256)
    end
  function internal view sup (x : IT) : Uint256 := do
    let s ← x.totalSupply
    return s
  function view viewer () : Uint256 := do
    let a ← getStorageAddr t
    let s ← sup a                    -- error: unsolved goals
    return s

view functions with checked arithmetic (addPanic etc.) and Int256 do pass. Because _tranchePrice, virtualPrice, getApr, _calcInterestWithdrawRequest, _checkOnlyOwner, paused()-style guards are all view in Solidity and all contain a require or a static call, the closure translation has to drop the view marker on nearly every Solidity view (kept in comments), losing the compilation-model mutability.

Ask: make the generated proof robust (split on the if produced by require, unfold Verity.require properly, and a frame lemma for externalStaticCallContractWordsTo/externalStaticCallEffectWordsTo), or downgrade a failing auto-proof to a warning/sorry-free assumed obligation instead of failing elaboration.

Closure-side tracking: audit/VERITY-GAPS.md G11/G18.

Start in Verity/Macro/Bridge.lean at mkViewFrameTheoremCommand and reproduce the require/revert and external static-call cases described in the issue. Trace the generated proof and the relevant Verity.require and externalStaticCallContractWordsTo/externalStaticCallEffectWordsTo behavior. Done means these view bodies elaborate with a robust generated proof, or failing proofs produce a warning and an assumed obligation without failing elaboration; update audit/VERITY-GAPS.md G11/G18 if needed.