feat(edsl): journal linked external calls in the executable plane - #2334
feat(edsl): journal linked external calls in the executable plane#2334Th0rgal wants to merge 2 commits into
Conversation
The EDSL executable plane's linked-call primitives (externalCallBind, callResultWords, tryExternalCallWords, and the safeTransfer family) were pure no-ops, so executable-plane theorems quantified over ContractState.calls could not observe whether a call happened at all — double-send, omission, reorder, rename, and argument mutants were all indistinguishable at run level. Each primitive now appends a name-keyed ExternalCall entry (exact argument words as calldata, success/failure control, stub returndata) to ContractState.calls, with @[simp] run-lemmas proved by rfl. A new smoke module runs the programs and separates every mutant class from the original in an arbitrary pre-state, and shows monadic revert rolls the journal back through Contract.run's snapshot semantics. The pure externalCallWords form remains non-journaling and is documented as a trust boundary in TRUST_ASSUMPTIONS.md; AUDIT.md records the new axiom-free surface. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_4484e748-16b6-481b-8dd2-fb145e606116) |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 4a45b12c4e
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| let entry := linkedCallEntry name args | ||
| (if success then .success else .failure) | ||
| (if success then [(externalCallStubWord name args : Nat)] else []) | ||
| ContractResult.success (success, (Inhabited.default : α)) |
There was a problem hiding this comment.
For every non-"fail" callee whose stub word is nonzero, this returns a successful result with the wrong payload. For example, tryExternalCall "echo" [7] now returns (true, 0) while journaling successful returndata [7]; consequently TryExternalCallSmoke.tryEcho follows its success branch but stores 0 instead of 7, unlike both externalCallWords and callResultWords. The successful branch should decode externalCallStubWord through ExternalResult rather than always returning Inhabited.default.
Useful? React with 👍 / 👎.
| { state with calls := state.calls ++ [entry] } | ||
| def externalCallBind {α : Type} [ExternalArg α] (names : List String) (name : String) (args : List α) : Contract Unit := | ||
| fun state => | ||
| let argWords := args.map ExternalArg.toWord |
There was a problem hiding this comment.
When args contains an Array or ByteArray, this conversion is lossy because the existing ExternalArg instances encode only .size. Thus calls such as externalCallBind [] "notifyArray" [#[1]] and the same call with #[2] produce identical journal entries, despite the commit's stated invariant that altered arguments are observable; the dynamic linked-call forms exercised in ExternalCalls.lean are therefore still unable to reject same-length payload mutations. The journal encoding needs to retain the dynamic contents or their complete ABI representation.
Useful? React with 👍 / 👎.
| def safeTransfer (token toAddr : Address) (amount : Uint256) : Contract Unit := | ||
| recordLinkedCall (linkedCallEntry "safeTransfer" | ||
| [Verity.addressToWord token, Verity.addressToWord toAddr, amount]) |
There was a problem hiding this comment.
For safeTransfer token toAddr amount, the emitted ERC-20 module calls token and supplies toAddr and amount as the transfer calldata, but this entry inherits target := 0 and instead places token in calldata. Unlike ordinary linked externals, this helper's target is dynamic rather than bound by name, so executable proofs inspecting the shared ExternalCall.target or calldata fields observe a wrapper invocation rather than the actual external-call boundary; the safe-transfer family should construct entries with the token address as the target and the ERC-20 arguments as calldata.
Useful? React with 👍 / 👎.
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_fc9cb2d0-4e51-4f4a-9420-6fdc3657fc60) |
|
@codex review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 9847597736
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| def safeTransfer (token toAddr : Address) (amount : Uint256) : Contract Unit := | ||
| recordLinkedCall (erc20WriteEntry "safeTransfer" token | ||
| [Verity.addressToWord toAddr, amount]) |
There was a problem hiding this comment.
This adds observability only to the ERC-20 write wrappers, while the adjacent balanceOf, allowance, and totalSupply helpers still return pure stub results without appending to calls. Consequently executable contracts such as ERC20HelperSmoke.snapshotBalance in Contracts/Smoke/ExternalCalls.lean can have these external reads omitted, duplicated, or reordered without the journal detecting the mutation, despite these helpers being monadic external-call crossings. Record entries for the read helpers too, including the token target, arguments, and stub returndata.
Useful? React with 👍 / 👎.
1 participant
Summary
The EDSL executable plane's linked-call primitives (
externalCallBind,callResultWords,tryExternalCallWords, and thesafeTransferfamily) werepure ()no-ops: executable-plane theorems quantified overContractState.callscould not observe whether a call happened at all, so double-send, omission, reorder, rename, and argument mutants were indistinguishable at run level.This PR makes each primitive append a name-keyed
ExternalCallentry toContractState.calls:Verity.Core.ExternalCallgains a defaultedname : String := ""field (existing address-keyed model-plane entries unaffected).Contracts.linkedCallEntrybuilds the entry: exact argument words as calldata,.success/.failurecontrol, in-band stub returndata;externalCallStubWordis now public andexternalCallStubSuccessreserves the"fail"callee for the failure path.@[simp] … := rfl; the compiler pipeline consumes model bodies (IR constructors), so Yul generation and difftests are unaffected.Contracts/Smoke/ExternalCallObservability.leanruns the programs and separates every mutant class from the original over an arbitrary pre-state: duplicated call, omitted call, reordered calls, renamed callee, zeroed argument, and thesafeTransferdouble-send form. It also proves a monadic revert rolls the journal entry back throughContract.run's snapshot semantics (EVM top-level revert observability).TRUST_ASSUMPTIONS.mddocuments the remaining boundary (stub-not-adversary; the pureexternalCallWordsform stays non-journaling; unmodeledcallExternal/mapping stubs);AUDIT.mdrecords the new axiom-free surface.Adopted from an abandoned unpushed WIP based on
0fd1c2f8(= current main), completed with compile fixes:tois a reserved token in the Lean grammar (binders renamedtoAddr), a no-progresssimp onlyremoved, and the"fail"-callee example restated as a fullContractResultequality to avoid a missingInhabited (Call.Result Uint256)instance.Campaign context: continues the bounded Verity→Lido closure campaign from milestone minimal-11
25c82e13, with the Lido model pinned to Verity main04729a9(Lido PR #69 remains review-first and unmerged). A vacuousexternalCallBind := pure ()was explicitly ruled out as a TX close; this PR is the non-vacuous repair.Test Plan
lake build— exit 0 (2471 jobs)lake build Contracts PrintAxioms Compiler.CompilationModelFeatureTest— exit 0 (2695 jobs); zerosorryin the log; no warnings in touched filesgit diff | grep -E '^\+.*(sorry|admit|\baxiom\b|unsafe|native_decide|@\[implemented_by)'→ no matches (also checked the new smoke file)make check— green excepttest_profile_ci_resources(container lacks GNU/usr/bin/time; environmental, unrelated to this diff)artifacts/verification_status.jsonregenerated (core_lines 1098→1103)FOUNDRY_PROFILE=difftest forge test) — forge unavailable in this container; deferred to CIRelated Issues
Addresses part of #2084 (Tier 4 — external calls & low-level mechanics): run-level observability of the executable linked-call family.
🤖 Generated with Claude Code
Note
Medium Risk
Changes executable-plane semantics and
ExternalCallshape used by proofs and stubs, but the denotational model plane is untouched and behavior is bounded by deterministic stubs plus documented trust boundaries.Overview
Linked external calls in the EDSL executable plane now append to
ContractState.calls, so run-level specs can see whether calls happened, in what order, and with what arguments—instead of the previouspure ()no-ops that made double-send, omission, reorder, rename, and argument mutants indistinguishable.ExternalCallgains a defaultednamefield for name-keyed linked callees;linkedCallEntry,recordLinkedCall, and publicexternalCallStubWord/externalCallStubSuccess(reserved"fail"callee) build journal entries with control, returndata, andExternalArg.toWordsencoding (length-prefixed arrays/bytes, not full EVM ABI). MonadicexternalCallBind,callResultWords,tryExternalCallWords, andsafeTransfer/safeApprovewrappers journal; ERC-20 writes settargetto the token. PureexternalCallWordsstill does not journal (documented inTRUST_ASSUMPTIONS.md).@[simp]run lemmas and new smokeExternalCallObservability.leanseparate mutant classes over arbitrary pre-states and pin revert rolling back the journal viaContract.run. Model plane unchanged;AUDIT.mdupdated;verification_status.jsoncore line count bumped.Reviewed by Cursor Bugbot for commit 9847597. Bugbot is set up for automated code reviews on this repo. Configure here.