Reject unsupported typed interface ABI params#1971
Open
Th0rgal wants to merge 68 commits into
Open
Conversation
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
Contributor
| \n### CI Failure Hints\n\nFailed jobs: `build`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n``` |
Th0rgal
force-pushed
the
fix/typed-interface-abi-param-guard-1962
branch
from
d0497bb to
57b2ef4
Compare
Adds the `verity-storage-layout-report` Lean executable and `scripts/generate_storage_layout_report.py` Python wrapper that together produce two committed artifacts for migration / audit review across `Compiler.Specs.allSpecs`: * `artifacts/storage_layout_report.json` — machine-readable per-contract layout (declared/canonical slots, alias slots, reserved ranges, packed subfields, mappings, dynamic arrays, opt-in EIP-7201 namespaces). * `artifacts/STORAGE_LAYOUT_SUMMARY.md` — human-readable Markdown summary. Drift is gated in two layers: `make check` runs the Python `--check --no-lean` mode (committed Markdown vs committed JSON), and `make verify-storage-layout` runs the JSON-vs-current-Lean-source check (also wired into `verify.yml` after the main `lake build`). Closes #1897.
Adds a `keccakString "<literal>"` term form that computes the Keccak-256 digest at macro-expansion time and emits a `Uint256` numeric literal. * `Verity/Macro/Syntax.lean` declares the syntax at `:max` precedence so it can appear in `verity_contract` `constants` / `immutable` right-hand sides (which require `term:max`). Non-literal arguments are rejected at parse time because the parser only accepts a `str` argument. * `Verity/Macro/KeccakString.lean` provides the macro expansion for standalone use sites (proofs, smoke tests, helpers), emitting `Verity.Core.Uint256.ofNat <digest>`. The digest is computed by the in-tree pure `Compiler.Keccak.Sponge` engine, so no new trust assumption is introduced. * `Verity/Macro/Translate/Expr.lean` pattern-matches `keccakString $s:str` in the three constant-handling layers (`validateConstantBody`, `inferPureExprType`, `translatePureExprWithTypes`) so the digest materialises as a `Compiler.CompilationModel.Expr.literal` inside contract bodies — no Lean macro expansion happens in the CompilationModel path. * `Contracts/Smoke/KeccakStringSmoke.lean` covers the macro at term position, agreement with the existing `Verity.keccak256_lit` def, and use inside a `verity_contract` `constants` block. Layer-import boundaries and Lean hygiene rules are updated alongside: `Verity/Macro/KeccakString.lean` is added to the macro-to-compiler allowlist for `Compiler.Keccak.Sponge`, and `Smoke`-stem files are explicitly added to the `native_decide` allowlist (the script's own comment already documented smokes as allowed; the code was not yet honoring it). Closes #1973.
Generalizes `Verity.Macro.Elaborate.elabVerityIntrinsic` to accept any non-zero number of comma-separated typed parameters in the `verity_intrinsic name (p1 : T1, p2 : T2, ...) : retTy where ...` command (#1977). The parser already used `sepBy(verityParam, ",")` for the parameter slot; the elaborator was the part hardcoded to a single parameter. * Records the full `paramNames` / `paramTypes` lists in the intrinsic registry (`Verity.Core.Intrinsics.IntrinsicDecl`). * Emits the wrapper as a curried function definition `def name : T1 -> T2 -> ... -> Tn -> retTy := semantics`, so the `semantics` term is supplied as an ordinary curried function value. * Fails closed on a zero-parameter declaration and on a `verbatim` Yul lowering whose declared input arity disagrees with the parameter count, mirroring how single-arg intrinsics already cross-check `1 == 1`. Smoke coverage in `Contracts.Smoke.MultiArgIntrinsicSmoke` exercises a two-arg and a three-arg intrinsic plus the obligation summary; the existing single-arg `clz` example continues to elaborate unchanged. Closes #1977.
Three fixes from the Bugbot review pass on this PR: 1. **Interface return validation removed (Medium)** — `validateExternalDeclsPublic` was only running `requireTypedInterfaceStaticParams` on interface-backed externals after the param-guard refactor, dropping the return-type executable shape check. Typed dot calls single-word-decode returndata, so an interface that declared e.g. `returns (Bytes)` or `returns (Array Uint256)` would silently truncate at the call site. Adds `requireTypedInterfaceStaticReturns` (mirroring the param guard) and wires it next to the existing param check; regression coverage in `Contracts.Smoke.InternalInterfaceSmoke` (Bytes-return and Array-return rejection). 2. **Default namespace pins wrong root (Medium)** — With `verity.storageNamespace.default` enabled and no contract-level `storage_namespace`, the auto contract-name root was eagerly seeded into `firstNamespaceOpt`. If the storage block then opened with an in-storage `storage_namespace` directive, slot offsets correctly used the in-storage root but the reported `spec.storageNamespace` (and layout/trust reports) still pointed at the auto root. Now distinguish the auto-default seed (overridable until the first field is recorded) from a contract-level seed (authoritative); the first in-storage directive replaces the provisional auto root, and a field locks the reported root in place so later directives never relabel already-declared fields. Regression: `DefaultNamespaceInStorageOverrideSmoke`. 3. **Builtin intrinsics skip arity match (Low)** — Multi-arg `verity_intrinsic` enforced that a `verbatim` lowering's declared input arity matches the parameter count, but the `builtin` path did not. Now cross-checks against `yulBuiltinArity?` for known fixed-arity builtins (`add`, `mul`, `keccak256`, …); unknown builtin names are still accepted unchecked so consumers can register novel names. Regression in `Contracts.Smoke.MultiArgIntrinsicSmoke`: a two-param intrinsic targeting `builtin "add"` compiles, a three-param one fails with the expected diagnostic. `lake build` and `make check` both pass; macro property-test artifacts regenerated.
`nonreentrant(lockField)` previously recorded metadata only; the macro accepted it, the model surfaced it, and a placeholder Lean theorem was generated, but the compiled Yul body was identical to an unguarded function. Validation enforced CEI ordering regardless, so contracts that wrote state after external calls still had to manually reorder them or escape via `allow_post_interaction_writes` (#1893). * `Compiler.CompilationModel.Dispatch.attachNonReentrantGuard` (new) prepends a transient-storage acquire prologue — `if eq(tload(lockSlot), 1) { revert(0, 0) }; tstore(lockSlot, 1)` — immediately after parameter loading for any external function whose source spec carries `nonReentrantLock = some lockField`. Transient storage (EIP-1153, Cancun+) auto-clears at end-of-transaction, so no explicit release Yul is needed on any return path — early `return`, `revert`, and panic cannot leak the lock across transactions. * Kept as a post-`compileFunctionSpec` transformation rather than inlined into the body shape, so the IR-generation proof modules continue to characterise the underlying parameter-loads + body shape without a nonReentrantLock case split. * `validateFunctionSpec` (Validation.lean) now treats `nonReentrantLock.isSome` as a CEI exemption alongside the existing `allowPostInteractionWrites` opt-out, because the synthesised guard closes the post-interaction-write reentry window at runtime. The CEI diagnostic surfaces both opt-outs to keep migration cues explicit. * `Contracts.Smoke.CEILadderSmoke` reorders `callThenStoreGuarded` so the state write follows the external call, demonstrating that the reentrancy-guarded function is no longer rejected as a CEI violation. All existing CEI-rejection `#guard_msgs` smokes are updated to match the new diagnostic wording. Trust boundary: documented in `TRUST_ASSUMPTIONS.md` and `docs/ROADMAP.md`. The guard's correctness reduces to EVM TLOAD/TSTORE semantics (already trusted) plus the macro-level invariant that the lock field is a scalar uint256 storage field used solely by the guard. Guarded functions sit outside `SupportedSpec` in this first version; proof-side guard preservation lemmas are deferred follow-up. `AUDIT.md` updated. Closes #1893.
Bugbot ("Internal nonreentrant skips guard", High) flagged that
`validateFunctionSpec` treats any `nonReentrantLock = some _` as a CEI
exemption, while `attachNonReentrantGuard` only injects the
transient-storage guard for external dispatch entries — so an internal
function carrying `nonreentrant(lock)` could compile with
post-external-call storage writes and no runtime lock.
Closed in three layers:
* **Macro layer** (`Verity/Macro/Translate.lean`): reject
user-declared `nonreentrant(<lock>)` on internal entrypoints at parse
time, with a diagnostic that names the dispatch-boundary mismatch.
* **Compilation-model layer** (`Compiler/CompilationModel/Validation.lean`):
also reject `isInternal && nonReentrantLock.isSome` here, so
consumers that build `FunctionSpec` values without going through the
macro pipeline can't silently get an unguarded post-interaction-write
window. CEI exemption now requires `!spec.isInternal`.
* **Internal helper shadow** (`Verity/Macro/Translate.lean`): the macro
emits an `internal_*` shadow spec for every user function that
inherits the public body. The shadow now drops `nonReentrantLock` to
pass the new compilation-model gate, but propagates the CEI
exemption that the public spec earned from the guard onto the shadow
as `allowPostInteractionWrites := true`. The shared body (which may
legitimately contain post-external-call writes once the public path
is guarded) therefore still validates when reused via the shadow.
Regression smoke `Contracts.Smoke.NonreentrantInternalHelperRejected`
covers the user-declared rejection path. `make check` is green.
…is now machine-checked
Adds Verity/Core/Model/Denote.lean: a denotation of the canonical deep AST (Compiler.CompilationModel) defined entirely inside the compiler-free core, mirroring Compiler.Proofs.IRGeneration.SourceSemantics decision-for-decision (evalExpr, evalExprList, execStmt/execStmtList/execForEachLoop, the storage read/write helpers, encodeStorage, and interpretFunction -> denoteFunction). The two compiler-engine dependencies are routed through a DenoteOracle structure instead of being imported: - mappingSlot : Nat -> Nat -> Nat (abstractMappingSlot / solidityMappingSlot, keccak256(abi.encode(key,slot))) - keccakMemorySlice : (Nat -> Uint256) -> Nat -> Nat -> Nat (Keccak-256 over the word-aligned memory slice, for Expr.keccak256) The proof layer will instantiate the oracle with the real Keccak engine and prove denote_eq_sourceSemantics (P4), making this the single semantic definition. Everything else (calldataloadWord, packed masks, slot alias expansion) is pure arithmetic replicated locally. Mirrors the event-less execStmt variants only; mapping writes express the IRStorageSlot/IRStorageWord round-trip directly on word-normalized Nat slots (extensionally equal). Includes native_decide smoke checks on a tiny inline CompilationModel. lake build Verity Contracts Compiler PrintAxioms green; scripts/check_lean_hygiene.py clean.
Instantiate the DenoteOracle with the real engines (abstractMappingSlot / SourceSemantics.keccakMemorySlice) and prove denote_evalExpr_eq / denote_evalExprList_eq: the compiler-free denotation's expression evaluator agrees with the proven source semantics on every expression. Equation-lemma/functional-induction realization for these ~90-arm matches exceeds the fixed realization budget, so the proof is a structural recursion whose arms close by rfl or by an Option.bind congruence helper (bindAgree) threading the induction hypotheses.
Add scripts/docsync.py: a declarative entry registry (conditional-note, snippet-sync, category-note kinds) with --check/--only/--list and a --root override for tests. Migrate the 4 Cluster B boundary-note checkers plus 2 Cluster A doc-sync checkers (layer2_boundary, interpreter_feature_boundary_catalog); legacy scripts become thin shims, Makefile check lines switch to docsync invocations, unit tests target the engine, and verify_sync_spec pins the new command list (regenerated). Output and exit codes verified byte-identical against the old checkers.
…mp set Adds the one sanctioned state-level read/write surface over the typed storage channels (readSlot/writeSlot, addr/transient/map/mapUint/map2/array variants) with read-over-write normalization lemmas tagged @[storage_simps]. The planned word-addressed representation flip (C5) becomes a swap of these lens implementations under stable names instead of another ~1400-site rewrite. No behavior change; existing accessors and proofs untouched.
Extend DenoteAgreement to the statement level: toStmtResult outcome conversion, definitional bridges for every mirrored write helper, a StorageRel fold bridge showing Denote's Nat-level mapping-write storage view tracks SourceSemantics' IRStorageSlot/IRStorageWord fold, and the mutual theorems execStmt_eq / execStmtList_eq plus execForEachLoop_agree covering every supported Stmt arm (unsupported arms agree on revert). SourceSemantics: drop 'private' from storageArraySetAt / storageArrayDropLast? / writeStorageArray so the agreement bridges can name them; no semantic change.
…perty_pipeline.py scripts/property_pipeline.py: subcommands check (manifest+coverage+lean-sync in one pass, --only per check), extract, report. The five legacy scripts become thin shims; outputs and exit codes verified byte-identical.
…e lints Dispatcher (--only/--skip/--list) over the 10 Lean structure/hygiene lint modules, generalizing the check_compiler_boundaries.py pattern. Rule modules are invoked unmodified (incl. check_lean_hygiene.py, the sorry/native_decide gate); per-rule output and exit codes verified byte-identical.
…erify sync spec Makefile check lines now invoke property_pipeline.py check (replacing 3 property lines) and lean_lint.py --only <rule> for the 10 Cluster E lints; verify_sync_spec_source.py pins updated and verify_sync_spec.json regenerated. REFERENCE.md and the consolidation inventory checklist updated.
…ds; finalize agreement artifacts - Bump maxHeartbeats for the helper-surface closure mutual block in SupportedSpec.lean: its isDefEq search is borderline at the default budget and timed out on clean (cache-cold) elaborations while passing incrementally. - Allowlist execForEachLoop_agree (58 lines): the succ case must spell out the loop-state literal inside a show-match to align the two interpreters' unfoldings. - Regenerate PrintAxioms and verification artifacts for the new DenoteAgreement theorems.
Accessors in Verity/Core.lean and state updates in Core/Model/Denote.lean now go through readSlot/writeSlot/readMap/... lenses. Until the C5 storage flip the lenses carry @[simp] so the existing raw-field proof surface keeps working; `simp only` sites and the verity_unfold/verity_spec macros gained the lens names explicitly. DenoteAgreement bridges remain rfl.
…greement Step 1: GenericInduction/DenoteSound.lean restates the two generic body/IR keystones with the compiler-free denotation (Denote.execStmtList) on the source side via DenoteAgreement.execStmtList_eq, giving denote_sound and denote_sound_with_helpers as the umbrella the per-contract _bridge instantiations will target. Step 2: DenoteFunctionAgreement.lean extends agreement to the external function boundary (denoteFunction_eq: parameter binding, transaction context, storage encoding, and result encoding all coincide on the event-free fragment). EndToEnd gains the denoteResultMatchesNativeOn surface plus its composition theorem and a SimpleStorage instantiation.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Bytes,String, array, tuple, and nested-struct typed-interface parameterssafeTransfer,safeTransferFrom, andsafeApproveselect the reusable SafeERC20 ECMs for interface-typed token parametersboundaryClassvaluesstorage_namespace, plus explicit override andstorage_namespace legacycompatibility coverageartifacts/storage_layout_report.json+artifacts/STORAGE_LAYOUT_SUMMARY.md) forCompiler.Specs.allSpecs, covering opt-in namespaces, declared/canonical slots, alias and reserved ranges, packed subfields, mappings, and dynamic-array fields, with Markdown-vs-JSON drift gated bymake checkand JSON-vs-Lean-source drift gated bymake verify-storage-layout(also wired intoverify.ymlafterlake build)keccakString "<literal>"macro-time term form (Verity.Macro.KeccakString) that computes Keccak-256 of a string literal at macro/translation time and emits aUint256literal — parser-restricted to string literals, pattern-matched directly by theverity_contractconstants-block translator, and covered byContracts.Smoke.KeccakStringSmokeverity_intrinsicto accept any non-zero number of comma-separated typed parameters: the elaborator records the full parameter list in the intrinsic registry, emits a curried wrapper definition (T1 -> T2 -> ... -> retTy), and enforces that averbatimlowering's declared input arity matches the parameter count; covered byContracts.Smoke.MultiArgIntrinsicSmoke(2-arg and 3-arg)nonreentrant(lockField)functions (Compiler.CompilationModel.Dispatch.attachNonReentrantGuard): prependsif eq(tload(lockSlot), 1) { revert(0, 0) }; tstore(lockSlot, 1)immediately after parameter loading on every external entry, exempts the function from CEI ordering enforcement (since the guard closes the post-interaction-write window at runtime), and is kept as a post-compileFunctionSpectransformation so the IR-generation proof modules are unaffected; covered byContracts.Smoke.CEILadderSmoke.callThenStoreGuarded(now writes after the external call)storageFamiliesand pairwisenonAliasClaimssections in the storage layout JSON artifact, plus a Markdown "How to discharge" preamble inartifacts/STORAGE_LAYOUT_SUMMARY.mdthat explains the three justification kinds (distinctScalarSlots,keccakDomainScalar,keccakPreimageDistinct). Replaces a global keccak-injectivity boundary with per-family local obligations plus a decidable finite subsetCompiler.Modules.CodeDataTestnow exercises empty / short / dynamicFrameLayoutpayloads (the last must be rejected to keep SSTORE2-style code-as-data static-only), anddocs/EXTERNAL_CALL_MODULES.mddocumentsCompiler.Modules.CodeDataas the canonical typed source-level facade over the CREATE2 / SSTORE2 ECMs, naming the MidnighttoId/toMarket/touchMarketround-trip pattern as the intended consumerCloses #1962
Closes #1965
Closes #1968
Closes #1896
Closes #1897
Closes #1973
Closes #1977
Closes #1747
Closes #1951
Closes #1952
Closes #1956
Closes #1893
Closes #1966
Closes #1967
Verification
lake build Contracts.Smoke.InternalInterfaceSmoke python3 scripts/check_macro_health.py python3 scripts/check_macro_property_test_generation.py lake build Compiler.CompileDriverTest lake build Contracts.Smoke python3 scripts/check_verification_status_doc.py python3 scripts/check_docs_workflow_sync.py git diff --check make verify-storage-layout python3 -m unittest discover -s scripts -p 'test_generate_storage_layout_report.py' lake build Contracts.Smoke.KeccakStringSmoke python3 -m unittest scripts.test_check_lean_hygiene lake build Contracts.Smoke.MultiArgIntrinsicSmokeNote
High Risk
Changes reentrancy semantics and compile-time fork gating (security-critical), plus broad compiler-model and CI path changes; incorrect guard or layout certificate logic could affect generated contract safety assumptions.
Overview
This PR consolidates patched Yul generation onto a single
verity-compilerbinary (--enable-patches) and drops the separateverity-compiler-patchedbuild from CI, Foundry setup, and artifact packaging.Reentrancy (#1893, #1968):
nonreentrant(lockField)now lowers to a Cancun transient-storage guard (tload/tstore) on externals, fallback, and receive, with lock release on normal fall-through; compilation fails closed whentargetForkis pre-Cancun. The guard is applied post-compileFunctionSpecviaattachNonReentrantGuard/compileGuardedFunctionSpecso IR-generation proofs stay unchanged.Storage audit (#1897, #1966, #1967): Layout JSON gains
storageFamiliesandnonAliasClaims(includingwriteSetsOverlapwhen scalar write sets intersect); alias derivation is shared via publicderivedAliasSlotsForSource. CI addsmake verify-storage-layoutinverify.yml; audit docs list the new artifacts.Model refactor (#1313): Declarative DSL types move to
Verity.Core.Model.Types;Compiler/CompilationModel/Types.leanis a shim plus IR projections.Compiler/CodegenBase.lean(no-op patch backend wrapper) is removed.Trust reporting: ECMs, linked externals, primitives, and usage sites emit stable
boundaryClassvalues in JSON reports.Other:
LogicalPurity.leanrewrites call-like / duplication-hazard checks onExpr.anyDeep/Stmt.anyDeep; Morpho-stylelegacyStringSafeTransfer*assumptions appear inAXIOMS.md.Reviewed by Cursor Bugbot for commit 4c978f4. Bugbot is set up for automated code reviews on this repo. Configure here.