Layer 2 follow-on: replace SupportedSpec feature exclusions with compositional proof interfaces and widen coverage toward the full EDSL image

[Th0rgal]

Summary

The generic whole-contract Layer 2 theorem is in place, but the current theorem domain is still the explicit SupportedSpec fragment rather than the effective full EDSL / full CompilationModel surface. This issue tracks the work needed to stop widening the theorem boundary by ad hoc feature exclusions and instead converge on a principled, mostly feature-complete proof interface.

This is intentionally broader than #1510.

• #1510 was about replacing the old hpost theorem spine with a real generic theorem, with an explicit supported-fragment witness and at least one auditable negative boundary.
• This issue is about what comes after that theorem exists: ranking and executing the proof-model expansion work until SupportedSpec becomes close to trivial, or is replaced by a smaller set of well-founded global side conditions.

Goal

State and prove a generic Layer 2 theorem that applies to the effective frontend-to-compiler image, not just today's narrow scalar/no-edge-surface fragment.

A rigorous end state should look like one of these:

1. verity_contract / EDSL lowering is proved to land inside a proof-complete CompilationModel subset, and the generic Layer 2 theorem covers that entire subset.
2. Or, the generic Layer 2 theorem directly covers the full CompilationModel surface used by the EDSL lowering path, with only explicit foreign/trust boundaries left as hypotheses.

The repo should avoid an unbounded "exclude one more feature in SupportedSpec" growth pattern.

Why a follow-on issue is needed beyond #1510

#1510 solved the theorem-shape problem:

• generic theorem instead of contract-specific hpost
• successful compilation mentioned directly
• theorem decomposed structurally across compiler boundaries
• explicit whole-contract witness (SupportedSpec)
• negative boundary documented

What it did not solve is theorem breadth. Today the proof boundary still excludes, wholly or partially:

• constructor semantics
• fallback / receive
• events / logs on the whole-contract path
• linked externals as fully composed proof objects
• low-level calls / returndata / proxy-upgradeability surfaces in the proof model
• helper-level compositional proof reuse across callers
• dynamic and layout-rich storage features on the whole-contract path
• local unsafe/refinement obligations as first-class discharged proof obligations

That remaining work needs an execution order, otherwise we will keep accreting exclusions case by case.

Design principle: stop proving a list of exclusions, start proving interfaces

The central shift for this issue is:

• do not keep extending SupportedSpec as a bag of feature = none side conditions
• instead, replace exclusions with compositional proof interfaces attached to the corresponding compiler boundaries

Examples:

• helper calls should be handled by a reusable helper-summary theorem interface, not by banning helper-level reuse
• external calls should be handled by explicit callee/module assumptions with proof-status tracking and composition lemmas, not by globally excluding them from whole-contract proofs
• events/errors should be handled by an output-trace/result-model interface, not by leaving them outside the theorem statement
• low-level calls/returndata should be handled by an operational semantics extension plus a trust/composition layer, not by permanently fencing them off as "supported operationally but not in proofs"

Ranked work items

P0. Define the actual theorem target precisely

Before widening feature support further, pin down the proof target.

Needed work:

• Decide whether the intended end-state claim is "full CompilationModel coverage" or "full macro-lowered EDSL image coverage".
• Document the difference explicitly in docs/ROADMAP.md, docs/VERIFICATION_STATUS.md, and the Layer 2 plan.
• If arbitrary Lean escape hatches remain available in the EDSL, define the theorem over the lowered compiler image rather than over all arbitrary Lean terms.

Why first:

• Without this, "support the whole EDSL" is underspecified and easy to overclaim.

Acceptance signal:

• the docs define the exact domain of the intended final theorem, and that domain is mechanically checkable.

P1. Replace SupportedSpec feature bans with a layered proof interface inventory

SupportedSpec is useful today, but it currently mixes:

• normalization preconditions
• selector/dispatch bookkeeping
  n- hard feature exclusions
• function/body support facts

Split these concerns.

Needed work:

• Separate persistent global invariants (layout normalization, selector uniqueness, tx-context boundedness) from feature-level support claims.
• Introduce feature-specific theorem interfaces so SupportedSpec can shrink toward:
  • structural well-formedness
  • normalization obligations
  • composition hooks for enabled features
• Audit every none/false field in SupportedSpec and classify it as either:
  • should remain a true global precondition
  • should become a dedicated proof interface
  • should be pushed down to a smaller boundary

Why high priority:

• This is the main antidote to feature-by-feature exclusion growth.

Acceptance signal:

• SupportedSpec no longer grows whenever a new feature is supported; instead, enabling a feature means instantiating a feature-local proof interface.

P2. Internal helper compositional proof reuse (#1335 dependency)

This is one of the most important gaps for whole-program genericity.

Current status:

• internal helpers compile and execute operationally
• helper-level proof reuse across callers is not yet exposed as a first-class theorem interface

Needed work:

• Define helper summaries/contracts that can be composed across call sites.
• Prove a helper-level preservation theorem parameterized by pre/post state alignment and return behavior.
• Prove caller-side composition lemmas so internal-call correctness is not reproved monolithically for every caller body.
• Connect macro-generated EDSL bridge theorems to these helper summaries so helper-rich contracts do not require contract-local proof plumbing.

Implementation insight:

• treat internal helpers like miniature verified modules with explicit call summaries, not just inlined statement lists
• if fuel-based semantics remain the execution model, expose fuel-monotone helper lemmas so callers can compose them without bespoke fuel arithmetic everywhere

Why this is P2:

• without helper composition, real contracts with reusable internal structure cannot benefit from the theorem ergonomically even if the operational surface exists

Acceptance signal:

• a helper used by multiple callers is proved once and reused compositionally in the generic Layer 2 theorem path
• docs no longer describe helper reuse as an incomplete boundary

P3. Low-level calls, returndata, and proxy/upgradeability proof modeling

This is the other major breadth blocker.

Current status:

• operational/compiler support exists for several low-level mechanisms
• trust reporting and deny flags exist
• whole-contract proof modeling still treats these as outside or partial boundaries

Needed work:

• Extend the proof interpreter/state model with returndata semantics and the observable effects of call / staticcall / delegatecall.
• Make explicit what is being proved about callees:
  • closed-world verified callee
  • assumed external contract summary
  • unchecked trust boundary
• Separate two concerns that are currently easy to conflate:
  • low-level call/returndata semantics generally
  • proxy/upgradeability-specific storage/context semantics for delegatecall
• For proxy/upgradeability, define a dedicated theorem surface for layout compatibility and storage ownership assumptions instead of leaving it as a broad not-modeled bucket.

Implementation insight:

• do not wait for a perfect universal external-world semantics before proving anything
• first introduce compositional callee summaries and explicit assumption statuses, then prove closed-world cases end to end
• handle delegatecall separately from plain call/staticcall, because storage aliasing and context reuse make it a different proof problem

Why this is P3:

• these surfaces are already important in real contracts and already appear in trust reports, so the proof model should catch up to the operational/compiler surface

Acceptance signal:

• VERIFICATION_STATUS.md no longer lists low-level mechanics / proxy-upgradeability as globally outside the current proof model
• closed-world low-level call examples compile through the generic theorem path

P4. Events/logs, custom errors, and richer observable behavior

Current whole-contract statements are still too state-centric.

Needed work:

• extend the semantic result model so compiler preservation talks about:
  • return values
  • revert payloads / typed errors
  • emitted events / logs
• prove preservation of event traces and revert payload encoding, not just storage/termination behavior
• align the source-side semantic model and the IR/Yul observable outputs so event/error support is no longer treated as extra-operational only

Implementation insight:

• a trace-based small-step or big-step result envelope is likely cleaner than bolting logs/errors onto the current result type piecemeal
• model typed revert payload preservation at the ABI boundary, not just raw byte equality in ad hoc lemmas

Why this is P4:

• events/errors are core observable contract behavior; leaving them outside whole-contract proofs limits what "semantic preservation" means in practice

Acceptance signal:

• contracts whose main user-facing behavior is event emission or typed custom errors fall inside the generic theorem boundary

P5. Storage richness on the whole-contract path

Operational support has outpaced whole-contract proof support for storage-rich features.

Needed work:

• storage reads / address-based storage operations
• mappings and multi-mappings
• struct-valued storage and packed-field semantics
• dynamic arrays and storage-array operations
• richer layout controls and alias-slot semantics where they affect semantic preservation

Implementation insight:

• this likely needs a proof-layer storage model that matches the current layout metadata more directly, rather than scalarizing everything through the first narrow fragment
• packed-field proofs should be handled via a dedicated read/write mask invariant library instead of ad hoc bitvector lemmas per feature

Why this is P5:

• many standard DeFi-style contracts need this surface, but the operational/compiler path already demonstrates it is meaningful to support

Acceptance signal:

• SupportedSpec no longer excludes storage-array/address/layout-rich features that already exist in CompilationModel

P6. Constructor, fallback, and receive

Current first theorem deliberately left these out. They still need proper treatment.

Needed work:

• constructor deployment semantics and constructor-visible state/immutable materialization
• payable/non-payable behavior during deployment
• fallback / receive dispatch semantics and value-sensitive entrypoint behavior
• integration with selector dispatch correctness and default-case semantics

Why this is later than the items above:

• these matter, but helper composition and low-level/storage breadth have broader impact on real contracts and proof architecture

Acceptance signal:

• whole-contract preservation theorem covers deployment and default-dispatch entrypoints, not only selector-dispatched standard functions

P7. Local obligations and unsafe/refinement escape hatches

Current tooling already tracks local obligations and supports fail-closed modes, but the theorem boundary still treats them as exclusions.

Needed work:

• formalize a proof object interface for local obligations
• allow the generic theorem to consume discharged local obligations as explicit hypotheses instead of rejecting any presence categorically
• keep assumed / unchecked obligations visible in trust reports and theorem statements

Why this matters:

• this turns local obligations from a blanket exclusion into a managed extension point

Acceptance signal:

• a contract with discharged local obligations can still instantiate the generic theorem without being kicked out of the supported fragment wholesale

Cross-cutting engineering tasks

These are required to keep the widening effort maintainable.

1. Feature matrix for proof status, not just compiler/interpreter status

Add a machine-readable and doc-visible matrix for each major CompilationModel feature:

• parser/lowering status
• operational semantics status
• codegen status
• proof status by layer
• trust-boundary status
• issue owner/reference

This should prevent future ambiguity such as "supported operationally" vs "inside the generic theorem".

2. Contract suite ranked by proof-value

Maintain a contract ladder used as widening milestones:

• scalar/simple storage baseline
• helper-rich contract
• mapping/layout-rich contract
• event/error-heavy contract
• low-level-call contract
• proxy/upgradeability case study

Each widening PR should move at least one contract from trust/test-only coverage into generic theorem coverage.

3. Stopgap boundaries must be explicit and auditable

If a feature remains out of scope temporarily:

• document the exact theorem gap
• attach the issue number
• make CI/trust-report output reflect it
• provide one negative example so the exclusion is auditable rather than implicit

Proposed execution order

1. Pin down theorem target domain and split SupportedSpec responsibilities.
2. Finish internal helper compositional proof reuse (#1335-adjacent work).
3. Extend proof semantics for low-level calls / returndata; handle proxy/upgradeability as a dedicated follow-on track, not an afterthought.
4. Extend the result model to cover events and typed errors.
5. Widen storage/layout-rich support on the whole-contract theorem path.
6. Bring constructor / fallback / receive into the generic theorem.
7. Turn local obligations into explicit proof-carrying extensions.

Comparison with #1510

#1510 acceptance criteria were about theorem legitimacy.
This issue is about theorem completeness.

What #1510 required:

• generic theorem shape
• no contract-specific hpost
• successful compilation in theorem hypotheses
• structural decomposition
• explicit supported fragment
• at least one negative boundary example
• docs updated

What this issue adds:

• make the supported fragment shrink by principled interface design, not by accumulating exclusions
• expose internal helper composition as a reusable proof boundary
• move low-level calls / returndata / proxy-upgradeability from trust-report-only status toward actual proof interfaces
• widen observable semantics to events and typed errors
• widen storage/layout-rich support until the macro-lowered EDSL image is substantially covered

So this issue should be treated as the ranked follow-on execution plan after #1510, not as a replacement for it.

Exit criteria

This issue can close when all of the following are true:

• SupportedSpec is mostly structural/normalization-oriented rather than a long list of banned features.
• Internal helper proofs compose across callers through a reusable interface.
• Low-level calls/returndata have an explicit proof model, and proxy/upgradeability is either covered or isolated behind a dedicated theorem interface.
• Events/logs and typed errors are part of the preserved observable semantics.
• Storage/layout-rich features used by standard contracts are inside the generic theorem domain.
• The intended theorem target is documented precisely enough that "whole EDSL" is not an ambiguous claim.
• docs/ROADMAP.md, docs/VERIFICATION_STATUS.md, and the Layer 2 plan all describe the same post-#1510 widening strategy.

Related

• Layer 2: replace the theorem spine with a real generic CompilationModel→IR semantic preservation theorem #1510
• Language: first-class internal calls with compositional proof support #1335

[Th0rgal]

Update from PR #1633 (proof/body-interface-inventory): the current P1 step is now implemented as a proof-boundary refactor rather than another fragment widening.

What changed:

• SupportedSpec is split into global invariants vs temporary surface gates, and body support is split into core / state / calls / effects interfaces.
• calls is further split into helpers / foreign / lowLevel.
• calls.helpers now carries a positive direct-callee summary inventory (InternalHelperSummaryContract) plus a strictly decreasing helper-rank interface.
• SourceSemantics.lean now exposes helper-aware source semantics and proof-carrying summary-soundness wrappers (InternalHelperSummarySound, SupportedSpecHelperProofs) without widening the trusted boundary.
• artifacts/layer2_boundary_catalog.json now records the exact theorem target, the SupportedSpec split, and the current temporary helper fail-closed gate.

Why this matters for #1630:

• it completes the structural P1 move away from a monolithic list of exclusions and makes the remaining helper blocker explicit and auditable;
• the next dominating step is now to consume helper-summary soundness + decreasing helper ranks inside the body/IR preservation lemmas so calls.helpers.legacySurfaceClosed can be removed.

PR: #1633

[Th0rgal]

Closing as part of issue tracker cleanup. The work tracked here has been consolidated into new focused tracking issues. See the new issues for updated scope and status.