verification: selfBalance escapes strict trust reporting despite documented proof/runtime bridge gap

[doomhammerhell]

Goal

finding-001-selfbalance-trust-surface-gap.md

Expr.selfBalance is already documented as compiler-supported and source-executable, but outside the current generic proof-interpreter fragment. The selected native EVMYulLean runtime path also explicitly fails closed for selfbalance until Verity’s selfBalance field is bridged into the native account map.

The trust assumption to eliminate or reduce is the unsurfaced bridge between:

Verity source/model state:
  ContractState.selfBalance

generated Yul:
  selfbalance()

native/runtime semantics:
  EVM account balance observed by the executing contract

At the moment, a contract using selfBalance can compile with all exposed strict deny flags enabled, while the generated trust report emits no named selfBalance / selfbalance obligation, no localized usage site, no assumed dependency, and no unchecked dependency.

The goal is to make this boundary fail closed: if a generated artifact depends on selfbalance(), the compiler/reporting pipeline should either prove and surface the bridge, reject the artifact under strict mode, or emit a named assumption that users must explicitly accept.

Current State

Expr.selfBalance is treated as compiler-supported and source-executable, but its runtime interpretation depends on an implicit bridge between Verity’s modeled contract state and the native/EVM account environment.

At the source level, selfBalance is evaluated from Verity state:

ContractState.selfBalance

At the generated Yul level, the same feature is lowered to:

selfbalance()

At the native/runtime level, selfbalance() observes the executing account’s EVM balance, not an ordinary contract-local field. Therefore, transporting a source-level property over ContractState.selfBalance into a native/runtime property requires an explicit account-balance bridge:

ContractState.selfBalance
  ~= 
EVM account balance observed by selfbalance()

The repository already documents this as a partial proof/runtime boundary: selfBalance is compiler-supported and source-executable, but not included in the current generic proof-interpreter fragment. The selected native EVMYulLean runtime path also fails closed for selfbalance until Verity’s selfBalance value is bridged into the native account map.

However, Contracts.Smoke.SelfBalanceSmoke currently compiles successfully with all exposed strict deny flags enabled, while the generated Yul contains selfbalance() and the generated trust report emits no named selfBalance / selfbalance obligation.

Impact:

Strict compilation can succeed for an artifact that depends on a documented partial proof/runtime feature, while the generated trust report remains assumption-empty for that feature.

Observed report surface:

Runtime introspection report:
  (no partially modeled runtime-introspection primitives used)

Low-level mechanics report:
  (no first-class low-level call or returndata primitives used)

Proof-status summary:
  proved: none
  assumed: none
  unchecked: none

Usage-site trust report:
  (no localized trust surfaces)

External assumption report:
  (no primitive assumptions, linked external assumptions, or ECM axioms)

The machine-readable trust.json similarly contains no localized mechanic, no usage site, no assumed dependency, and no unchecked dependency for selfBalance / selfbalance:

{
  "modeledLowLevelMechanics": [],
  "partiallyModeledRuntimeIntrospection": [],
  "usageSites": [],
  "hasUncheckedDependencies": false,
  "proofStatus": {
    "proved": {
      "axiomatizedPrimitives": [],
      "linkedExternals": [],
      "ecmModules": [],
      "localObligations": []
    },
    "assumed": {
      "axiomatizedPrimitives": [],
      "linkedExternals": [],
      "ecmModules": [],
      "localObligations": []
    },
    "unchecked": {
      "axiomatizedPrimitives": [],
      "linkedExternals": [],
      "ecmModules": [],
      "localObligations": []
    }
  }
}

No field names selfBalance or selfbalance are emitted, even though the generated Yul contains selfbalance().

This creates a false-negative trust report: a user can reasonably interpret strict compilation plus an empty assumption/unchecked report as meaning that the artifact is inside the mechanically covered proof fragment, while the artifact still depends on an unsurfaced account-balance bridge hypothesis.

Risk: MEDIUM

This is not a demonstrated fund-loss exploit and does not claim that selfbalance() itself behaves incorrectly at runtime.

The risk is correctness-boundary drift and user-facing overconfidence in the verification result. Strict acceptance currently does not imply that every proof/runtime bridge assumption has been surfaced, rejected, or explicitly accepted.

The violated trust-surface expectation is:

strict compilation success
  =>
all proof/runtime bridge assumptions are either proved, surfaced as named obligations, rejected by strict mode, or explicitly accepted

For SelfBalanceSmoke, that expectation does not currently hold:

generated artifact uses selfbalance()
+
selfBalance is documented as partial / unbridged for the current proof-runtime path
+
strict compilation succeeds
+
trust report emits no named obligation

This makes the issue stronger than a documentation concern: the documentation identifies the boundary, but the strict enforcement and generated reports do not reflect it. Human systems, naturally, found a way to document a dragon and then not put it on the map.

Proposed Approach

The cleanest fix is to make the selfBalance boundary explicit in the same proof/trust surface used by strict-mode enforcement.

The desired invariant is:

AcceptedStrict(P)
  =>
for every runtime-observed feature f used by P:
    f is proved
    or f is surfaced as a named assumed/unchecked obligation
    or f is rejected by strict mode
    or f is explicitly accepted through a named non-strict assumption

For selfBalance, the proof obligation is the bridge between the Verity source/model state and the native/runtime account-balance observation:

ContractState.selfBalance
  ~= 
EVM account balance observed by selfbalance()

A complete proof path would include:

Expr.selfBalance
  -> SourceSemantics reads state.world.selfBalance.val
  -> CompilationModel Expr.selfBalance
  -> generated Yul selfbalance()
  -> native EVMYulLean account-balance semantics
  -> runtime account balance for the executing contract

The proof plan should make this bridge explicit as either:

1. a discharged theorem connecting ContractState.selfBalance to the EVMYulLean account map for the executing contract;
2. a named trust assumption emitted in the generated trust report;
3. a strict-mode rejection until the bridge is implemented.

The important part is that the bridge must not remain implicit.

Validation strategy:

Add a regression test using Contracts.Smoke.SelfBalanceSmoke, since it already exercises the relevant feature and lowers to selfbalance().

The test should compile the contract with all exposed strict deny flags enabled and assert one of the following outcomes:

strict compilation rejects SelfBalanceSmoke

or:

trust.json contains a named selfBalance / selfbalance obligation

or, after the bridge is fully implemented:

trust.json identifies selfBalance as proved through the native account-balance bridge

The regression should explicitly check that this state is no longer possible:

generated Yul contains selfbalance()
+
trust.json has no selfBalance/selfbalance usage site
+
proofStatus.assumed = []
+
proofStatus.unchecked = []
+
hasUncheckedDependencies = false
+
strict compilation succeeds

A useful implementation-level validation would be to add a sync test between:

SupportedSpec.exprTouchesUnsupportedCoreSurface
TrustSurface collectors
strict deny classifiers
trust report emission
native EVMYulLean unsupported builtin list

The test should fail if a feature is marked as outside the generic proof fragment or unsupported by the selected native runtime path, but is not either denied, reported, or explicitly classified as proved.

For example:

if exprTouchesUnsupportedCoreSurface(.selfBalance) = true
or native selected runtime marks "selfbalance" unsupported
then TrustSurface must emit a named obligation
or strict mode must reject
or a proof bridge must mark the feature as discharged

This avoids future drift where proof-boundary predicates and trust-report predicates evolve independently.

Fallback path:

If the native account-balance bridge is not ready yet, the fallback should be fail-closed rather than silent.

Acceptable fallback options:

1. classify selfBalance / selfbalance as a runtime-account/environment mechanic;
2. include it in the generated trust report as an assumed or unchecked obligation;
3. add a strict deny gate for unbridged account/environment reads;
4. extend the existing runtime-introspection deny gate to include selfBalance;
5. prevent strict-mode artifacts using selfBalance from being reported as assumption-empty;
6. emit a usage-site entry for every function lowering to selfbalance().

The minimal safe fallback is:

SelfBalanceSmoke under all strict deny flags
  =>
compilation fails

until the bridge is proved or explicitly accepted.

The more user-friendly fallback is:

SelfBalanceSmoke under non-strict mode
  =>
compilation succeeds
  =>
trust.json emits named obligation:
      selfBalance / selfbalance requires account-balance bridge assumption

The long-term fix is to avoid maintaining separate unsynchronized taxonomies for proof coverage, native runtime support, trust reporting, and strict enforcement. Ideally, strict enforcement should be derived from a single proof-boundary coverage predicate, because humans maintaining parallel classifier lists is how dragons become undocumented runtime dependencies. Not our species’ finest architectural pattern.

Key References

This belongs under the native EVMYulLean / trust-reduction roadmap, specifically the work reducing the trust boundary between generated Yul, native EVMYulLean execution, and runtime environment/account-state semantics.

The relevant roadmap target is not ordinary property coverage. The issue is the missing proof/report bridge for an environment-observed account value:

Verity model state:
  ContractState.selfBalance

generated Yul:
  selfbalance()

native/runtime semantics:
  executing account balance in the EVM account map

Concrete files/modules:

• Contracts/Smoke/SelfBalanceSmoke.lean

  • Contains the minimal existing contract exercising Verity.selfBalance / selfBalance.
  • Source examples validate execution against defaultState with selfBalance := 123.

• Compiler/Proofs/IRGeneration/SourceSemantics.lean

  • Defines source-level behavior for Expr.selfBalance.
  • Expr.selfBalance evaluates from state.world.selfBalance.val.
  • Contains evalExpr_selfBalance, pinning the source-level behavior.

• Compiler/CompilationModel/ExpressionCompile.lean

  • Lowers Expr.selfBalance to generated Yul:

    YulExpr.call "selfbalance" []
    

• Compiler/Proofs/IRGeneration/SupportedSpec.lean

  • Marks .selfBalance as touching unsupported core proof surface through exprTouchesUnsupportedCoreSurface.

• Compiler/CompilationModel/TrustSurface.lean

  • Current trust-surface collectors and classifiers are assembled here.
  • collectLowLevelExprMechanics records other mechanics, but has no .selfBalance case.
  • Runtime-introspection classification includes blockNumber, contractAddress, and chainid, but not selfBalance.
  • Runtime-introspection expression collection has no .selfBalance case.
  • Trust report JSON is assembled from these collectors, so there is currently no emitted selfBalance / selfbalance obligation.

• Compiler/CompileDriverBase.lean

  • Relevant compile-driver surface for strict deny flags and report generation through compileSpecsWithOptions.

• Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeHarness.lean

  • Native selected-runtime unsupported header/account builtins include selfbalance.
  • The native harness reports that the selected runtime path uses a header/account builtin not represented in Verity’s YulTransaction bridge.

• Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeSmokeTest.lean

  • Contains smoke coverage asserting native rejection for selfbalance.

• Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeLemmas.lean

  • Relevant for checking which builtins currently have bridge agreement coverage.
  • Useful when deciding whether selfbalance has been moved into the proved/native-bridged fragment.

• docs/INTERPRETER_FEATURE_MATRIX.md

  • Documents Expr.selfBalance as partial.
  • States that selfBalance is compiler-supported and source-executable, but not included in the current generic proof-interpreter fragment.
  • Notes that address(this).balance lowers to selfbalance() and current generic proof interpreters do not yet model the balance read.

• docs/NATIVE_EVMYULLEAN_TRANSITION.md

  • Documents that selfbalance fails closed on the selected native runtime path until Verity’s selfBalance value is carried into the EVMYulLean account map.

• Generated report artifacts from the local reproduction:

  /tmp/verity-audit-selfbalance-strict/trust.json
  /tmp/verity-audit-selfbalance-strict/assumptions.json
  /tmp/verity-audit-selfbalance-strict/run.log
  /tmp/verity-audit-selfbalance-strict/out/SelfBalanceSmoke.yul
  

Validation commands:

lake build Contracts.Smoke.SelfBalanceSmoke

tmp=$(mktemp -t verity-selfbalance-check)
printf '%s\n' \
  'import Compiler.CheckContract' \
  'import Contracts.Smoke.SelfBalanceSmoke' \
  '#check_contract Contracts.Smoke.SelfBalanceSmoke' > "$tmp"
lake env lean "$tmp"

Strict compile/report reproduction:

rm -rf /tmp/verity-audit-selfbalance-strict
mkdir -p /tmp/verity-audit-selfbalance-strict

runner=$(mktemp -t verity-audit-selfbalance-strict)
printf '%s\n' \
  'import Compiler.CompileDriverBase' \
  'import Contracts.Smoke.SelfBalanceSmoke' \
  '' \
  'unsafe def main : IO Unit := do' \
  '  Compiler.Base.compileSpecsWithOptions' \
  '    [Contracts.Smoke.SelfBalanceSmoke.spec]' \
  '    "/tmp/verity-audit-selfbalance-strict/out"' \
  '    true' \
  '    []' \
  '    {}' \
  '    none' \
  '    (some "/tmp/verity-audit-selfbalance-strict/trust.json")' \
  '    (some "/tmp/verity-audit-selfbalance-strict/assumptions.json")' \
  '    none' \
  '    true true true true true true true true true none none false true' > "$runner"

lake env lean --run "$runner" 2>&1 | tee /tmp/verity-audit-selfbalance-strict/run.log
cat /tmp/verity-audit-selfbalance-strict/trust.json
rg -n "selfbalance|function currentBalance|function balancePlus" \
  /tmp/verity-audit-selfbalance-strict/out/SelfBalanceSmoke.yul

Novelty references inspected:

• Issue #1829: blobbasefee strict deny gap. Related but not duplicate. In that case the mechanic is reported but not denied; here selfBalance is absent from the trust-surface taxonomy entirely.
• Issues #1628, #1760, #1724: track selfBalance / address(this).balance feature support, not the strict-report omission.
• PR #1782: adds selfBalance support while keeping the generic proof fragment partial.
• PR #1822: retargets public correctness toward native EVMYulLean and documents the native bridge boundary.
• PR #1826: native EVMYulLean follow-up work, not a fix for this trust-report omission.
• PR #1828: CI/doc cleanup for EVMYulLean fork burn-in, not semantically relevant.

Core invariant to preserve:

AcceptedStrict(P)
  =>
for every proof/runtime feature f used by P:
    f is proved
    or f is surfaced as a named assumed/unchecked obligation
    or f is rejected by strict mode
    or f is explicitly accepted through a named non-strict assumption

Current counterexample:

P = Contracts.Smoke.SelfBalanceSmoke
f = Expr.selfBalance

generated Yul contains selfbalance()
+
selfBalance is documented as partial / unbridged for the current proof-runtime path
+
strict compilation succeeds
+
trust report emits no named obligation

Acceptance Criteria

• Trust boundary is reduced with concrete code/proof changes
• docs/ROADMAP.md is updated
• CI passes