Repository navigation
G29: executable constructor for ordinary verity_contract (verity#2465) - #2470
Conversation
…-20 hop lemmas (G14) - getStorage on an Int256 field binds an Int256 (ofUint256 of the word), so addPanic/subPanic on it resolve to the signed checked instance, matching the compilation model. Previously the word was Uint256 and Int256 operands were coerced, so int256 += with a negative operand panicked spuriously. - Core: hopCall_success_of_ne, hopCall_scoped_callee, hopCallView_getMapping, hopCallView_getMapping2. - Smoke: Int256 regression witnesses; Erc20BalanceHop (generated ERC-20 read and transfer through linked_contracts). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…moke state Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ty#2465, G29 part) Ordinary contracts now get an executable `constructor` definition, like mixins and include hosts already did, so a deployment boundary can run the generated constructor body. Best effort: if the body has no executable lowering, elaboration state is restored and only the compilation-model constructor is kept (no new failures for existing contracts). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…roperty artifacts Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
f6e2d4b to
e46bfba
Compare
| \n### CI Failure Hints\n\nFailed jobs: `compiler-regressions`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n``` |
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…uctor Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
![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: a02b60fa69
ℹ️ 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".
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
1 participant
Pareto G29 (verity#2465), executable-constructor part. Stacked on #2469: once #2469 merges, retarget this PR to
main.CI status: all checks green at
a02b60fa69(2026-10-05). The first run ofcompiler-regressionshit the 10-minute step timeout in "Compare Solidity, Denote and compiled models" with no mismatch reported (the differential runs it printed all passed). The rerun is green. Verity main's latest "Verify proofs" run (98533b7) is green, so no pre-existing failure is waived. Commit a02b60f fixes the earlier "Check Lean warning non-regression" failure (unused-parameter lint on the generated constructor).Exact semantics change
includes)verity_contractwith aconstructorblock now also elaboratesC.constructor : <params> → Contract Unit(Verity/Macro/Elaborate.lean). Its body is generated the same way as the existing mixin/include-host executable constructor (mkConstructorDefCommandPublic). Before this change, ordinary contracts only had the compilation-model constructor.defthrows or logs a new error (for example, a body with no executable lowering), the elaboration state is restored. The contract then keeps exactly its previous declarations, so no existing contract newly fails.Stringparameters are accepted (the tranche-shapedconstructor (name, symbol)).Contracts/ERC721/ERC721.lean: the handwritten«constructor»(same body) is removed in favour of the generated one.C.constructorafter its contract now gets "already declared". The fix is to delete the handwritten copy. lfglabs-dev/pareto-credit-vault-proof-closure has no such definitions; it uses_constructor.Soundness argument
This change only adds a definition and changes no existing definition or compiler output. The generated body uses the same executable translation as every function and as the mixin constructors, so it carries the same fidelity story. The fallback path can only remove the new
def; it cannot alter anything else. ERC721's generated constructor has the same body as the deleted handwritten one.Tests
Contracts/Smoke/ConstructorExecutable.lean:CtorExec.constructorsetsminter := msg.senderandsupply := 77(decide +kernel).CtorWithStrings.constructor : String → String → Contract Unitruns (decide +kernel).PropertyCtorExec.t.sol,PropertyCtorWithStrings.t.sol.Remaining assumptions (out of scope, written up on #2465)
keccak(rlp(sender, nonce))) is not modelled, and neither isnew C(...)CREATE lowering. Consumers must assume deployment addresses are fresh and distinct from every existing contract, that the code at those addresses is the generated contract, and that CREATE does not fail.Stringstorage andStringhelper params/results (_concat) are unsupported. Name and symbol are accepted as constructor params but not stored, and no guarantee may depend on them.No
sorry/admit/axiom/native_decideis added.🤖 Generated with Claude Code