Support constructorArg in core proof surface by Th0rgal · Pull Request #2149 · lfglabs-dev/verity

Th0rgal · 2026-07-10T18:03:07Z

Summary

Treat Expr.constructorArg as core-supported without removing any other unsupported constructor gates.
Add constructor arg alias names to constructor body scope and prove alias bindings are present.
Wire constructorArg through expression compilation/evaluation and constructor-body proof consumers.

Validation

lean-slot lake build Compiler.Proofs.IRGeneration.SupportedSpec Compiler.Proofs.IRGeneration.FunctionBody Compiler.Proofs.IRGeneration.Function Compiler.Proofs.IRGeneration.DenoteAgreement: passed.
rg -n "sorry|admit|axiom " over changed files: no proof-hole/axiom hits; only existing comment prose matched words like admit/admitted.

vercel · 2026-07-10T18:03:13Z

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
verity	Ready	Preview, Comment	Jul 11, 2026 1:47pm

github-actions · 2026-07-10T18:23:12Z

\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 · 2026-07-10T19:50:00Z

CI correction needed for head 0360db1b2a11dbda8d2979fa14d5177b75b35ce7.

The branch-head Verify proofs workflow_dispatch run failed after the main proof build passed, in step Prebuild shared audit Lean targets while building PrintAxioms:
https://github.com/lfglabs-dev/verity/actions/runs/29114717952/job/86435461155

This is not a runner flake. The audit import closure exposes stale constructor-body scope consumers after this PR changed constructor bodies to compile/support under constructorBodyScope ctor.params:

Compiler/Proofs/IRGeneration/ContractFeatureTest.lean
- around line 642: proof of compileConstructor_ok_components still simplifies with a body compile hypothesis over ctor.params.map (·.name).
- line 654: Function.compileConstructor_some_ok_of_body now expects compileStmtList ... (constructorBodyScope constructorOnlyCtor.params) ....
- lines 978 and 1045: Function.supported_constructor_body_correct_with_body_interface now expects the same constructorBodyScope compile witness.
Compiler/Proofs/EndToEnd/Base.lean
- line 5856: generatedConstructorSupportedStmtList_of_supported still returns SupportedStmtList spec.fields (ctor.params.map (·.name)) ctor.body, but the branch now has the matching supported constructor witness under constructorBodyScope ctor.params.

Suggested bounded correction scope:

Update only those stale audit consumers to use the new constructor body scope/witnesses.
Do not weaken the new constructorArg support theorem statements or reintroduce old scope assumptions.
Validate with at least:

lean-slot lake build PrintAxioms
python3 scripts/lean_lint.py --only proof_length
rg -n "sorry|admit|axiom |unsafe|allowlist" Compiler/Proofs/IRGeneration/ContractFeatureTest.lean Compiler/Proofs/EndToEnd/Base.lean Compiler/Proofs/IRGeneration/Function.lean Compiler/Proofs/IRGeneration/SupportedSpec.lean

The narrower local build already passed; this failure is specifically from the audit/PrintAxioms closure.

Th0rgal · 2026-07-10T20:20:55Z

Follow-up with local reproduction details for head 0360db1b2a11dbda8d2979fa14d5177b75b35ce7.

I reproduced the audit failure locally with:

lean-slot lake build PrintAxioms
lean-slot lake build Compiler.Proofs.EndToEnd.Base
lean-slot lake build Compiler.Proofs.IRGeneration.ContractFeatureTest

PrintAxioms fails because these two imports fail:

Compiler.Proofs.EndToEnd.Base
Compiler.Proofs.IRGeneration.ContractFeatureTest

Concrete failures:

Compiler/Proofs/EndToEnd/Base.lean:5856

The proof still expects:

SupportedStmtList spec.fields (ctor.params.map (·.name)) ctor.body

but hSupported.constructor now gives support for:

SupportedStmtList spec.fields ((constructorAsFunctionSpec ctor).params.map (·.name)) (constructorAsFunctionSpec ctor).body

This needs the same constructorAsFunctionSpec / constructorBodyScope bridge used in SupportedSpec.lean, not the old raw ctor.params.map scope.

Compiler/Proofs/IRGeneration/ContractFeatureTest.lean:978 and :1045

Both hbodyCompile witnesses still compile under:

ctor.params.map (·.name)

but Function.supported_constructor_body_correct_with_body_interface now expects:

constructorBodyScope ctor.params

So the local fix should update those body compile witnesses and the nearby bodyStmts extraction/simp blocks to use constructorBodyScope constructorOnlyCtor.params. The warning at :645 is just fallout from the mismatch (hbodyCompile becomes unused in the old simp form).

Please keep the correction scoped to these stale consumers, then re-run:

lean-slot lake build Compiler.Proofs.EndToEnd.Base
lean-slot lake build Compiler.Proofs.IRGeneration.ContractFeatureTest
lean-slot lake build PrintAxioms
python3 scripts/lean_lint.py --only proof_length
rg -n "sorry|admit|axiom |unsafe|allowlist" Compiler/Proofs/IRGeneration/ContractFeatureTest.lean Compiler/Proofs/EndToEnd/Base.lean Compiler/Proofs/IRGeneration/Function.lean Compiler/Proofs/IRGeneration/SupportedSpec.lean

Th0rgal · 2026-07-11T10:30:37Z

@codex review

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 9d260c4c53

ℹ️ 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".

Th0rgal · 2026-07-11T10:57:56Z

@codex review

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 3a05390a9c

ℹ️ 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".

Th0rgal · 2026-07-11T11:14:49Z

@codex review

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 1056f078a2

ℹ️ 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".

chatgpt-codex-connector · 2026-07-11T11:20:15Z

+private def validateConstructorArgAliasNameCollisions (params : List Param) :
+    Except String Unit := do
+  let generated := constructorArgAliasNames params
+  match params.find? (fun param => generated.contains param.name) with


Reject locals that shadow constructor arg aliases

For constructors that declare a local/binder named arg<i> (for example Stmt.letVar "arg0" ...) this check still passes because it only scans formal parameter names, while genConstructorArgLoads now reserves those same arg<i> identifiers and Expr.constructorArg i lowers to them. That lets a constructor body shadow the generated alias (or emit duplicate Yul let declarations) so later constructorArg reads the local instead of the deploy argument; mirror the ADT collision check by including collectStmtListBindNames body or pass the alias names into constructor scope validation.

Useful? React with 👍 / 👎.

Th0rgal · 2026-07-11T11:24:35Z

@codex review

chatgpt-codex-connector · 2026-07-11T11:30:07Z

Codex Review: Didn't find any major issues. More of your lovely PRs please.

Reviewed commit: 082dd8c08d

ℹ️ 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/2083-constructor-arg

Th0rgal · 2026-07-11T13:47:55Z

@codex review

chatgpt-codex-connector · 2026-07-11T13:54:36Z

Codex Review: Didn't find any major issues. Another round soon, please!

Reviewed commit: c057821775

ℹ️ 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".

Support constructor arg core proofs

9e9f73b

chore: auto-refresh derived artifacts

2ed542a

vercel Bot deployed to Preview July 10, 2026 18:03 View deployment

Split constructor arg alias bound proof

6143d68

vercel Bot deployed to Preview July 10, 2026 18:22 View deployment

chore: auto-refresh derived artifacts

0360db1

vercel Bot deployed to Preview July 10, 2026 18:22 View deployment

Fix constructor body audit consumers

e66e27a

vercel Bot deployed to Preview July 10, 2026 23:00 View deployment

Merge main into constructor arg proof branch

9a3c885

vercel Bot deployed to Preview July 11, 2026 09:51 View deployment

Merge latest main into constructor arg proof branch

9d260c4

vercel Bot deployed to Preview July 11, 2026 09:57 View deployment

chatgpt-codex-connector Bot reviewed Jul 11, 2026

View reviewed changes

Comment thread Compiler/Proofs/EndToEnd/Base.lean

Align constructor body bridge scope

3a05390

vercel Bot deployed to Preview July 11, 2026 10:57 View deployment

chatgpt-codex-connector Bot reviewed Jul 11, 2026

View reviewed changes

Comment thread Compiler/Proofs/IRGeneration/SourceSemantics.lean

Reject constructor arg alias collisions

1056f07

vercel Bot deployed to Preview July 11, 2026 11:14 View deployment

chatgpt-codex-connector Bot reviewed Jul 11, 2026

View reviewed changes

Reject constructor arg alias local collisions

082dd8c

vercel Bot deployed to Preview July 11, 2026 11:24 View deployment

Th0rgal added 2 commits July 11, 2026 15:43

Merge latest main into constructor arg proof branch

dc2b299

Merge remote-tracking branch 'origin/codex/2083-constructor-arg' into…

c057821

… codex/2083-constructor-arg

vercel Bot deployed to Preview July 11, 2026 13:47 View deployment

Uh oh!

Conversation

Th0rgal commented Jul 10, 2026

Uh oh!

vercel Bot commented Jul 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jul 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Th0rgal commented Jul 10, 2026

Uh oh!

Th0rgal commented Jul 10, 2026

Uh oh!

Th0rgal commented Jul 11, 2026

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

Th0rgal commented Jul 11, 2026

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

Th0rgal commented Jul 11, 2026

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

chatgpt-codex-connector Bot Jul 11, 2026

Choose a reason for hiding this comment

Uh oh!

Th0rgal commented Jul 11, 2026

Uh oh!

chatgpt-codex-connector Bot commented Jul 11, 2026

Uh oh!

Th0rgal commented Jul 11, 2026

Uh oh!

chatgpt-codex-connector Bot commented Jul 11, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

vercel Bot commented Jul 10, 2026 •

edited

Loading

github-actions Bot commented Jul 10, 2026 •

edited

Loading