macro: zero-argument context-taking helper called as a bare statement is not threaded (Pareto G20)

[Th0rgal]

Found while translating the Pareto Credit Vault (IdleCDOEpochVariant) into verity_contract sources on main at e53c0ef (closure repo gap G20, audit/VERITY-GAPS.md).

Symptom

A zero-argument internal helper whose body makes a mutable external call (so it "opens a reentrancy window") gets a prepended ExecutableCallContext parameter in the executable plane. When a caller invokes it as a bare statement (helper on its own line, no application node), threadAdversaryThroughExecutableSyntax does not rewrite the call (the doElem| $fn:ident $args:term* and hoistNested $name:ident($[$args],*) cases both need an application), so elaboration fails:

error: ...IdleCDOEpochVariant.lean:620:4: Type mismatch
  _skimDonatedAssets
has type
  ExecutableCallContext → Contract Unit
but is expected to have type
  Contract PUnit.{1}

The compilation-model plane accepts the bare identifier (localFunctionAppSyntax? has an .ident case), so the two planes disagree on the spelling.

Minimal repro

verity_contract BareZeroArgHelper where
  storage
    last : Uint256 := slot 0
  interfaces
    interface IToken where
      function transfer(Address, Uint256) returns (Bool)
    end
  function internal reentrancy_trusted skim (t : IToken) : Unit := do
    let ok ← t.transfer (1 : Address) 1
    require ok "transfer"
  function internal reentrancy_trusted skimAll () : Unit := do
    -- any zero-arg body with a mutable external call
    pure ()
  function reentrancy_trusted allow_post_interaction_writes run () : Unit := do
    skimAll          -- fails once skimAll takes the call context
    setStorage last 1

(Give skimAll a real mutable call, e.g. through a storage-held token wrapper as in the Pareto sources, to make it context-taking.)

Workaround

Spell the call as skimAll() (the ident noWs "(" ... ")" syntax): hoistNested matches $name:ident($[$args:term],*) with zero args and threadHelperApp? finds the helper with params.size == 0.

Suggested fix

In threadAdversaryThroughExecutableSyntax, handle a bare Syntax.ident doElem / term whose name is in adversarialHelpers with zero params, rewriting it to helperCallWithAdv name #[] adv; or reject the bare form with a message pointing at helper().