Repository navigation
Import Solidity function slices with execution coverage and A/B/C validation - #2438
Merged
Merged
Conversation
Stmt.returnValues records source-order words and finishes as stop, so slice proofs can read the three results without a new statement outcome. Co-authored-by: Cursor <cursoragent@cursor.com>
Select the function from pinned solc 0.8.34 before validating the slice, inline the reached helpers, and reject an uncovered constructor instead of executing it. Co-authored-by: Cursor <cursoragent@cursor.com>
Contributor
| \n### CI Failure Hints\n\nFailed jobs: `foundry-patched`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n``` |
A package that depends on Verity elaborates solidity_slice_import against .lake/packages/verity, so the provenance digest has to read those sources there. The pinned solc binary stays in the elaborating package. Co-authored-by: Cursor <cursoragent@cursor.com>
An unreached loop still imports, a reached loop is rejected without leaving an olean, and helper, factor, field, return-order, and layout edits are detected by the witness. Co-authored-by: Cursor <cursoragent@cursor.com>
Th0rgal
marked this pull request as ready for review
September 23, 2026 14:53
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
Contributor
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 10 Lean file(s), 2554 changed supported line(s).
Warnings
- routing : Diff exceeded bounded packet review capability; full OCR not attempted.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 20 supported / 20 total; Lean 10, trust docs 3, workflow/scripts 4, contracts 2, docs 0
- Changed lines: 2554 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status large-lean-hotspots; comments 0; files 0; tokens 0; tool calls 0; warnings 1; duration 0s
- Largest changed files: Compiler/SoliditySlice/Import.lean (+1261/-0), Compiler/SoliditySlice/Coverage.lean (+400/-0), scripts/solidity_slice_mutations.py (+303/-0), scripts/setup_solc_slice.py (+96/-0), Contracts/SoliditySliceSmoke/Smoke.lean (+90/-0)
Packet coverage
- Packet review: not used; selected 0/8 packet(s)
- Scout: configured; status skipped_no_packets; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Diff exceeded packet budget; use top changed files and deterministic signals as required Codex/human review checklist.
- Strong packet-review blocker: OpenCodeReview 1.7.9 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
Pilot mode: advisory only. Codex Review remains the merge gate.
Contributor
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 10 Lean file(s), 2573 changed supported line(s).
Warnings
- routing : Diff exceeded bounded packet review capability; full OCR not attempted.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 23 supported / 23 total; Lean 10, trust docs 3, workflow/scripts 7, contracts 2, docs 0
- Changed lines: 2573 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status large-lean-hotspots; comments 0; files 0; tokens 0; tool calls 0; warnings 1; duration 0s
- Largest changed files: Compiler/SoliditySlice/Import.lean (+1261/-0), Compiler/SoliditySlice/Coverage.lean (+400/-0), scripts/solidity_slice_mutations.py (+303/-0), scripts/setup_solc_slice.py (+96/-0), Contracts/SoliditySliceSmoke/Smoke.lean (+90/-0)
Packet coverage
- Packet review: not used; selected 0/8 packet(s)
- Scout: configured; status skipped_no_packets; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Diff exceeded packet budget; use top changed files and deterministic signals as required Codex/human review checklist.
- Strong packet-review blocker: OpenCodeReview 1.7.9 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
Pilot mode: advisory only. Codex Review remains the merge gate.
Contributor
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 15 Lean file(s), 3713 changed supported line(s).
Warnings
- routing : Diff exceeded bounded packet review capability; full OCR not attempted.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 40 supported / 42 total; Lean 15, trust docs 3, workflow/scripts 18, contracts 3, docs 0
- Changed lines: 3713 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status large-lean-hotspots; comments 0; files 0; tokens 0; tool calls 0; warnings 1; duration 0s
- Largest changed files: Compiler/SoliditySlice/Import.lean (+1283/-0), Compiler/SoliditySlice/Coverage.lean (+400/-0), scripts/solidity_slice_mutations.py (+305/-0), scripts/solidity_differential/engine.py (+232/-0), scripts/solidity_differential/cases.py (+117/-0)
Packet coverage
- Packet review: not used; selected 0/8 packet(s)
- Scout: configured; status skipped_no_packets; model reviewer_scout
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Diff exceeded packet budget; use top changed files and deterministic signals as required Codex/human review checklist.
- Strong packet-review blocker: OpenCodeReview 1.7.9 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
Pilot mode: advisory only. Codex Review remains the merge gate.
Th0rgal
changed the title
Member
Author
|
@codex review Please review current head c134c2e, including the importer scope/hygiene fixes, nested-if compiler naming and corresponding proofs, and the A/B/C differential harness. Pay particular attention to false positives from harness failures, independence of storage/ABI construction, replay integrity, and the explicit scope limits. |
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
A mismatch between renamed/helper variants of a generated program failed the run without leaving any artifact, and --reduce then crashed on the missing case. Write metamorphic-divergence.json with the differing source rows and have the reducer reject such failures explicitly.
Contributor
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 15 Lean file(s), 3737 changed supported line(s).
Warnings
- routing : Diff exceeded bounded packet review capability; full OCR not attempted.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 40 supported / 42 total; Lean 15, trust docs 3, workflow/scripts 18, contracts 3, docs 0
- Changed lines: 3737 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status large-lean-hotspots; comments 0; files 0; tokens 0; tool calls 0; warnings 1; duration 0s
- Largest changed files: Compiler/SoliditySlice/Import.lean (+1283/-0), Compiler/SoliditySlice/Coverage.lean (+400/-0), scripts/solidity_slice_mutations.py (+305/-0), scripts/solidity_differential/engine.py (+232/-0), scripts/solidity_differential/cases.py (+117/-0)
Packet coverage
- Packet review: not used; selected 0/8 packet(s)
- Scout: configured; status skipped_no_packets; model reviewer_scout
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Diff exceeded packet budget; use top changed files and deterministic signals as required Codex/human review checklist.
- Strong packet-review blocker: OpenCodeReview 1.7.9 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
Pilot mode: advisory only. Codex Review remains the merge gate.
The `solidity_contract` importer elaborated Solidity into its own `Sol.Fn` semantics, separate from CompilationModel, so none of its theorems fed the compiler proofs. The CompilationModel slice importer (validated A/B/C against solc and the compiled model) is now the single Solidity front end. Delete Contracts/VaultFromSolidity, the SolidityImportSmoke inheritance, modifiers and structs smokes, `solidity_simp`, the 0.8.33 importer setup script and CI step, the Vault Foundry test, the Pareto import roadmap, and the now-empty named-storage spec lint. Drop the matching lakefile targets, exemptions, property manifest entries and documentation sections, and regenerate PrintAxioms and the verification status (356 -> 329 theorems).
Contributor
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 32 Lean file(s), 10381 changed supported line(s).
Warnings
- routing : Diff exceeded bounded packet review capability; full OCR not attempted.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 79 supported / 85 total; Lean 32, trust docs 3, workflow/scripts 32, contracts 8, docs 3
- Changed lines: 10381 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status large-lean-hotspots; comments 0; files 0; tokens 0; tool calls 0; warnings 1; duration 1s
- Largest changed files: Contracts/VaultFromSolidity/Importer/Importer.lean (+0/-1915), Compiler/SoliditySlice/Import.lean (+1283/-0), docs/SOLIDITY_IMPORT_ROADMAP.md (+0/-849), Contracts/VaultFromSolidity/Importer/scripts/solidity_importer_test.py (+0/-591), Compiler/SoliditySlice/Coverage.lean (+400/-0)
Packet coverage
- Packet review: not used; selected 0/8 packet(s)
- Scout: configured; status skipped_no_packets; model reviewer_scout
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Diff exceeded packet budget; use top changed files and deterministic signals as required Codex/human review checklist.
- Strong packet-review blocker: OpenCodeReview 1.7.9 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
Pilot mode: advisory only. Codex Review remains the merge gate.
Importer refactors must reproduce the imported CompilationModel exactly; solidity_slice_mutations.py now compares it with model.golden and only rewrites the snapshot with --update-golden.
Contributor
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 32 Lean file(s), 10391 changed supported line(s).
Warnings
- routing : Diff exceeded bounded packet review capability; full OCR not attempted.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 79 supported / 86 total; Lean 32, trust docs 3, workflow/scripts 32, contracts 8, docs 3
- Changed lines: 10391 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status large-lean-hotspots; comments 0; files 0; tokens 0; tool calls 0; warnings 1; duration 0s
- Largest changed files: Contracts/VaultFromSolidity/Importer/Importer.lean (+0/-1915), Compiler/SoliditySlice/Import.lean (+1283/-0), docs/SOLIDITY_IMPORT_ROADMAP.md (+0/-849), Contracts/VaultFromSolidity/Importer/scripts/solidity_importer_test.py (+0/-591), Compiler/SoliditySlice/Coverage.lean (+400/-0)
Packet coverage
- Packet review: not used; selected 0/8 packet(s)
- Scout: configured; status skipped_no_packets; model reviewer_scout
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Diff exceeded packet budget; use top changed files and deterministic signals as required Codex/human review checklist.
- Strong packet-review blocker: OpenCodeReview 1.7.9 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
Pilot mode: advisory only. Codex Review remains the merge gate.
Compiler/SoliditySlice becomes Compiler/SolidityImport and the positional
`solidity_slice_import … slice_bytecode_hash "none"` command becomes:
solidity_import x from "<root>" entry "<file>" using <profile>
contract C
function f(Market, bytes32, address)
The solc settings are an ordinary `Profile` value (named or inline), the
function is selected by its Solidity parameter types, and the generated
kernel check is `x.covered`. Report types become ImportReport,
ImportedFunction and ParamProjection; scripts become setup_solc_import.py,
solidity_import_mutations.py and solidity_import_differential.py.
The imported smoke model is byte-identical to model.golden.
Contributor
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 33 Lean file(s), 10460 changed supported line(s).
Warnings
- routing : Diff exceeded bounded packet review capability; full OCR not attempted.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 80 supported / 87 total; Lean 33, trust docs 3, workflow/scripts 32, contracts 8, docs 3
- Changed lines: 10460 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status large-lean-hotspots; comments 0; files 0; tokens 0; tool calls 0; warnings 1; duration 0s
- Largest changed files: Contracts/VaultFromSolidity/Importer/Importer.lean (+0/-1915), Compiler/SolidityImport/Import.lean (+1320/-0), docs/SOLIDITY_IMPORT_ROADMAP.md (+0/-849), Contracts/VaultFromSolidity/Importer/scripts/solidity_importer_test.py (+0/-591), Compiler/SolidityImport/Coverage.lean (+400/-0)
Packet coverage
- Packet review: not used; selected 0/8 packet(s)
- Scout: configured; status skipped_no_packets; model reviewer_scout
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Diff exceeded packet budget; use top changed files and deterministic signals as required Codex/human review checklist.
- Strong packet-review blocker: OpenCodeReview 1.7.9 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
Pilot mode: advisory only. Codex Review remains the merge gate.
The importer lowered Solidity into Lean source strings and re-parsed them with runParserCategory. Lowering now produces ordinary CompilationModel values (Expr, Stmt, Field, FunctionSpec) and Quote.lean turns the emitted fragment into syntax quotations; anything outside that fragment is an internal error. After elaboration, each import evaluates `x.model` and `x.report` back and requires them to equal the imported values. The smoke library declares its Solidity sources as a Lake `input_dir`, so editing a .sol file rebuilds the import. The imported smoke model is unchanged (model.golden), and all four A/B/C mutants are still detected.
Contributor
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 34 Lean file(s), 10603 changed supported line(s).
Warnings
- routing : Diff exceeded bounded packet review capability; full OCR not attempted.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 81 supported / 88 total; Lean 34, trust docs 3, workflow/scripts 32, contracts 8, docs 3
- Changed lines: 10603 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status large-lean-hotspots; comments 0; files 0; tokens 0; tool calls 0; warnings 1; duration 0s
- Largest changed files: Contracts/VaultFromSolidity/Importer/Importer.lean (+0/-1915), Compiler/SolidityImport/Import.lean (+1299/-0), docs/SOLIDITY_IMPORT_ROADMAP.md (+0/-849), Contracts/VaultFromSolidity/Importer/scripts/solidity_importer_test.py (+0/-591), Compiler/SolidityImport/Coverage.lean (+400/-0)
Packet coverage
- Packet review: not used; selected 0/8 packet(s)
- Scout: configured; status skipped_no_packets; model reviewer_scout
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Diff exceeded packet budget; use top changed files and deterministic signals as required Codex/human review checklist.
- Strong packet-review blocker: OpenCodeReview 1.7.9 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
Pilot mode: advisory only. Codex Review remains the merge gate.
Both now shape the elaborated model or its solc settings, so a change to either must invalidate downstream provenance like the rest of the importer.
Contributor
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 34 Lean file(s), 10607 changed supported line(s).
Warnings
- routing : Diff exceeded bounded packet review capability; full OCR not attempted.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 81 supported / 88 total; Lean 34, trust docs 3, workflow/scripts 32, contracts 8, docs 3
- Changed lines: 10607 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status large-lean-hotspots; comments 0; files 0; tokens 0; tool calls 0; warnings 1; duration 0s
- Largest changed files: Contracts/VaultFromSolidity/Importer/Importer.lean (+0/-1915), Compiler/SolidityImport/Import.lean (+1302/-0), docs/SOLIDITY_IMPORT_ROADMAP.md (+0/-849), Contracts/VaultFromSolidity/Importer/scripts/solidity_importer_test.py (+0/-591), Compiler/SolidityImport/Coverage.lean (+400/-0)
Packet coverage
- Packet review: not used; selected 0/8 packet(s)
- Scout: configured; status skipped_no_packets; model reviewer_scout
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Diff exceeded packet budget; use top changed files and deterministic signals as required Codex/human review checklist.
- Strong packet-review blocker: OpenCodeReview 1.7.9 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
Pilot mode: advisory only. Codex Review remains the merge gate.
`solidity_import` now accepts one `function` clause per root. Each root is lowered with fresh bindings, generated names and projections, so adding a root cannot change how another is lowered; all roots share one field list. The model is named after the contract (C_f_slice -> C), the report lists `roots`, and each projection records its function. The smoke contract gains `lossOf(bytes32)`. The mutation suite checks that importing f with lossOf leaves f byte-identical to importing it alone, and rejects duplicate and unknown roots; lossOf also runs A/B/C in CI.
Contributor
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 34 Lean file(s), 10691 changed supported line(s).
Warnings
- routing : Diff exceeded bounded packet review capability; full OCR not attempted.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 82 supported / 89 total; Lean 34, trust docs 3, workflow/scripts 33, contracts 8, docs 3
- Changed lines: 10691 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status large-lean-hotspots; comments 0; files 0; tokens 0; tool calls 0; warnings 1; duration 0s
- Largest changed files: Contracts/VaultFromSolidity/Importer/Importer.lean (+0/-1915), Compiler/SolidityImport/Import.lean (+1314/-0), docs/SOLIDITY_IMPORT_ROADMAP.md (+0/-849), Contracts/VaultFromSolidity/Importer/scripts/solidity_importer_test.py (+0/-591), Compiler/SolidityImport/Coverage.lean (+400/-0)
Packet coverage
- Packet review: not used; selected 0/8 packet(s)
- Scout: configured; status skipped_no_packets; model reviewer_scout
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Diff exceeded packet budget; use top changed files and deterministic signals as required Codex/human review checklist.
- Strong packet-review blocker: OpenCodeReview 1.7.9 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
Pilot mode: advisory only. Codex Review remains the merge gate.
Merge Compiler/SolidityImport/README.md and TESTING.md into docs/SOLIDITY_IMPORT.md: usage and profiles, the supported subset, the four separately established statuses (importable, runs on Denote, compiles, covered by compiler proofs), the trust boundary, and A/B/C validation. The importer folder keeps a pointer.
Contributor
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 34 Lean file(s), 10760 changed supported line(s).
Warnings
- routing : Diff exceeded bounded packet review capability; full OCR not attempted.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 83 supported / 89 total; Lean 34, trust docs 3, workflow/scripts 33, contracts 8, docs 4
- Changed lines: 10760 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status large-lean-hotspots; comments 0; files 0; tokens 0; tool calls 0; warnings 1; duration 0s
- Largest changed files: Contracts/VaultFromSolidity/Importer/Importer.lean (+0/-1915), Compiler/SolidityImport/Import.lean (+1314/-0), docs/SOLIDITY_IMPORT_ROADMAP.md (+0/-849), Contracts/VaultFromSolidity/Importer/scripts/solidity_importer_test.py (+0/-591), Compiler/SolidityImport/Coverage.lean (+400/-0)
Packet coverage
- Packet review: not used; selected 0/8 packet(s)
- Scout: configured; status skipped_no_packets; model reviewer_scout
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Diff exceeded packet budget; use top changed files and deterministic signals as required Codex/human review checklist.
- Strong packet-review blocker: OpenCodeReview 1.7.9 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
Pilot mode: advisory only. Codex Review remains the merge gate.
- Move AXIOMS.md and TRUST_ASSUMPTIONS.md into docs/ and update every check, test fixture, CI path filter, CODEOWNERS entry and link that names them. - Delete files no check reads: AUDIT.md (dated journal; history keeps it), SUPPORTEDSPEC_CONVERSION.md, Dockerfile, .gitconfig, .profile, verity.svg, one-off reports/prompts/scopes, docs/archive, docs/roadmap, docs/parity, scripts/REFERENCE.md, the finished consolidation inventory, an unused fetch script, the 27-line docsync shims and their tests, and design screenshots. - Rewrite README (46 lines: guarantees, quick start, layout, review order), CONTRIBUTING (57 lines) and CLAUDE.md. lake build and make check pass; no relative markdown link dangles.
Each imported root now has an explicit status. The import report records `importable`, `denoteCovered` (the per-root form of `x.covered`) and `compilerProof`, whose only case is `unavailable`: the importer builds no `SupportedSpec` witness and there is no decision procedure for it, so compiler-proof coverage is never claimed. `Differential.statusText` adds `compilable`, a compile attempt of the root on its own, which is not a correctness result; agreement is only sampled by A/B/C. `Differential.run` selects the root by name for `describe` and `run`, and gains `status`. `solidity_profile name where ...` defines a named `Profile`. The mutation suite checks the statuses of a two-root import and that an unsupported construct reached from the second root is rejected with that root's call path. The smoke golden model is unchanged.
The two-root check imports Compiler.SolidityImport.Differential, which `lake build SolidityImportSmoke` does not build, so CI failed on a missing olean.
Th0rgal
added a commit
to lfglabs-dev/morpho-midnight-verity
that referenced
this pull request
Sep 24, 2026
Only the importer mutation script changed; the import digest, model and per-function status are identical.
Solidity locals now keep their source name in the imported model (suffixed _1, _2, ... on collision with a parameter, projection, earlier binding, Yul keyword or builtin), so proofs refer to postSlashCredit rather than to _verity_slice_tmp_12. Expression temporaries keep the hygienic _verity_slice_tmp_N names. The smoke golden changes only by this renaming. Compiler.SolidityImport.Proofs adds runFunction, splitAfter, and the word, binding and body-splitting lemmas that were written downstream in morpho-midnight-verity.
Th0rgal
added a commit
to lfglabs-dev/morpho-midnight-verity
that referenced
this pull request
Sep 24, 2026
Import Midnight.updatePositionView with Verity's solidity_import and prove the five assertions of certora/specs/UpdatePositionView.spec on every successful call of the imported model, for any storage and any mapping-slot oracle. - Midnight/Import.lean: the declarative import. - Midnight/Spec.lean: the preciseCreditCorrect invariant, the rule's premises and its five assertions, each next to its CVL source. - Midnight/Proof.lean: the theorem; Proof/ follows the imported body statement by statement using the Solidity local names. - check/: trust boundary, re-import and provenance check, A/B/C differential vectors, and axiom audit. Verity is pinned to 2ef9c505 (lfglabs-dev/verity#2438).
solidity_import now also defines, with Solidity types: - example.f oracle world args... : Option (results), calling each imported function in world (block timestamp included); - example.field.member oracle world keys... reading a storage struct member with the imported layout, plus example.field.member_val relating it to the model's read. Key binders use the Solidity key names, now recorded in the report (`storage position keys [id, user]`). Specifications no longer name slots, bindings or packing. The wrappers go through runFunction and readMember in the new, Mathlib-free Compiler.SolidityImport.Access, which also proves that the model's own structMember reads are readMember and that a read fits its width. The imported model is unchanged (golden identical); a function named model/report/sourceDigest/covered is rejected.
Th0rgal
added a commit
to lfglabs-dev/morpho-midnight-verity
that referenced
this pull request
Sep 25, 2026
Import Midnight.updatePositionView with Verity's solidity_import and prove the five assertions of certora/specs/UpdatePositionView.spec on every successful call of the imported model, for any storage and any mapping-slot oracle. - Midnight/Import.lean: the declarative import. - Midnight/Spec.lean: the preciseCreditCorrect invariant, the rule's premises and its five assertions, each next to its CVL source. - Midnight/Proof.lean: the theorem; Proof/ follows the imported body statement by statement using the Solidity local names. - check/: trust boundary, re-import and provenance check, A/B/C differential vectors, and axiom audit. Verity is pinned to 9b472a8a (lfglabs-dev/verity#2438).
Th0rgal
added a commit
to lfglabs-dev/morpho-midnight-verity
that referenced
this pull request
Sep 25, 2026
Import Midnight.updatePositionView with Verity's solidity_import and prove the five assertions of certora/specs/UpdatePositionView.spec on every successful call of the imported model, for any storage and any mapping-slot oracle. - Midnight/Import.lean: the declarative import. - Midnight/Spec.lean: the preciseCreditCorrect invariant, the rule's premises and its five assertions, each next to its CVL source. - Midnight/Proof.lean: the theorem that the rule holds; Lemmas/ follows the imported body statement by statement using the Solidity local names. - check/: trust boundary, re-import and provenance check, A/B/C differential vectors, and axiom audit. Verity is pinned to 9b472a8a (lfglabs-dev/verity#2438).
Unused or never-built Lean: - Verity/Compiler/FromSolidity.lean: #fromSolidity scaffold shelling out to a verity-cli that does not exist; not in any lean_lib glob. - Verity/Trace.lean: not in any glob, imported nowhere. - Verity/Core/SolidityImportAttr.lean: simp attribute never used. - Contracts/Legacy.lean, Contracts/SpecAliases.lean: deprecated forwarders imported nowhere (and their feature_ownership surface). - Contracts/TypedIRTests.lean: not built by any target and no longer compiles. - PatchRulesProofs.ObjectPatchPreserves: unused placeholder `:= True`. Orphan tooling: - generate_yul_identity_diff_report.py and check_parity_pack_metrics.py (and tests): never wired into CI; issue #967 is closed. IDENTITY_CHECKER.md now says so. - check_storage_layout.py: drop the Compiler/Specs.lean layer (file gone, so the layer and the Spec-EDSL check silently checked nothing). The Spec-EDSL check now runs on every contract with both layers (smokes exempt). - check_feature_ownership.py was never run: fix the artifact's dead paths (patched compiler folded into verity-compiler, moved SourceSemantics and layout files) and run it in make check. Stale references: packages/*/lakefile.lean targets for removed modules, PrintAxioms exclusions for removed files, CODEOWNERS, ROADMAP, AXIOMS.md, generate_contract.py (Verity/All.lean -> Contracts.lean), trust surface report regenerated.
Th0rgal
added a commit
to lfglabs-dev/morpho-midnight-verity
that referenced
this pull request
Sep 25, 2026
Import Midnight.updatePositionView with Verity's solidity_import and prove the five assertions of certora/specs/UpdatePositionView.spec on every successful call of the imported model, for any storage and any mapping-slot oracle. - Midnight/Import.lean: the declarative import. - Midnight/Spec.lean: the rule updatePositionViewProperties, in the CVL vocabulary (Requires, Asserts, oldCredit, preciseCreditBefore, ...). - Midnight/Proof.lean: the theorem that the rule holds; Lemmas/ follows the imported body statement by statement using the Solidity local names. - check/: trust boundary, re-import and provenance check, A/B/C differential vectors, and axiom audit. Verity is pinned to 9b472a8a (lfglabs-dev/verity#2438).
Th0rgal
added a commit
to lfglabs-dev/morpho-midnight-verity
that referenced
this pull request
Sep 25, 2026
Import Midnight.updatePositionView with Verity's solidity_import and prove the five assertions of certora/specs/UpdatePositionView.spec on every successful call of the imported model, for any storage and any mapping-slot oracle. - Midnight/Import.lean: the declarative import. - Midnight/Spec.lean: the rule updatePositionViewProperties, in the CVL vocabulary, without the CVL ghosts; the CVL statement with ghosts is derived from it. - Midnight/Proof.lean: the theorem that the rule holds; Lemmas/ follows the imported body statement by statement using the Solidity local names. - check/: trust boundary, re-import and provenance check, A/B/C differential vectors, and axiom audit. Verity is pinned to 9b472a8a (lfglabs-dev/verity#2438).
Th0rgal
added a commit
to lfglabs-dev/morpho-midnight-verity
that referenced
this pull request
Sep 25, 2026
Import Midnight.updatePositionView with Verity's solidity_import and prove the five assertions of certora/specs/UpdatePositionView.spec on every successful call of the imported model, for any storage and any mapping-slot oracle. - Midnight/Import.lean: the declarative import. - Midnight/Spec.lean: the rule updatePositionViewProperties, in the CVL vocabulary, without the CVL ghosts (not needed for a single call). - Midnight/Proof.lean: the theorem that the rule holds; Lemmas/ follows the imported body statement by statement using the Solidity local names. - check/: trust boundary, re-import and provenance check, A/B/C differential vectors, and axiom audit. Verity is pinned to 9b472a8a (lfglabs-dev/verity#2438).
Th0rgal
added a commit
to lfglabs-dev/morpho-midnight-verity
that referenced
this pull request
Sep 25, 2026
Import Midnight.updatePositionView with Verity's solidity_import and prove the five assertions of certora/specs/UpdatePositionView.spec on every successful call of the imported model, for any storage and any mapping-slot oracle. - Midnight/Import.lean: the declarative import. - Midnight/Spec.lean: the rule updatePositionViewProperties, in the CVL vocabulary, without the CVL ghosts (not needed for a single call). - Midnight/Proof.lean: the theorem that the rule holds; Lemmas/ follows the imported body statement by statement using the Solidity local names. - check/: trust boundary, re-import and provenance check, A/B/C differential vectors, and axiom audit. Verity is pinned to 9b472a8a (lfglabs-dev/verity#2438).
Th0rgal
added a commit
to lfglabs-dev/morpho-midnight-verity
that referenced
this pull request
Sep 25, 2026
Import Midnight.updatePositionView with Verity's solidity_import and prove the five assertions of certora/specs/UpdatePositionView.spec on every successful call of the imported model, for any storage and any mapping-slot oracle. - Midnight/Import.lean: the declarative import. - Midnight/Spec.lean: the rule updatePositionViewProperties, in the CVL vocabulary, without the CVL ghosts (not needed for a single call). - Midnight/Proof.lean: the theorem that the rule holds; Lemmas/ follows the imported body statement by statement using the Solidity local names. - check/: trust boundary, re-import and provenance check, A/B/C differential vectors, and axiom audit. Verity is pinned to 9b472a8a (lfglabs-dev/verity#2438).
Th0rgal
added a commit
to lfglabs-dev/morpho-midnight-verity
that referenced
this pull request
Sep 25, 2026
Import Midnight.updatePositionView with Verity's solidity_import and prove the five assertions of certora/specs/UpdatePositionView.spec on every successful call of the imported model, for any storage and any mapping-slot oracle. - Midnight/Import.lean: the declarative import. - Midnight/Spec.lean: the rule updatePositionViewProperties, in the CVL vocabulary, without the CVL ghosts (not needed for a single call). - Midnight/Proof.lean: the theorem that the rule holds; Lemmas/ follows the imported body statement by statement using the Solidity local names. - check/: trust boundary, re-import and provenance check, A/B/C differential vectors, and axiom audit. Verity is pinned to 9b472a8a (lfglabs-dev/verity#2438).
Th0rgal
added a commit
to lfglabs-dev/morpho-midnight-verity
that referenced
this pull request
Sep 25, 2026
Import Midnight.updatePositionView with Verity's solidity_import and prove the five assertions of certora/specs/UpdatePositionView.spec on every successful call of the imported model, for any storage and any mapping-slot oracle. - Midnight/Import.lean: the declarative import. - Midnight/Spec.lean: the rule updatePositionViewProperties, in the CVL vocabulary, without the CVL ghosts (not needed for a single call). - Midnight/Proof.lean: the theorem that the rule holds; Lemmas/ follows the imported body statement by statement using the Solidity local names. - check/: trust boundary, re-import and provenance check, A/B/C differential vectors, and axiom audit. Verity is pinned to 9b472a8a (lfglabs-dev/verity#2438).
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
1 participant
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.
Import a selected Solidity function and its reached helpers into a deterministic, kernel-checked
CompilationModel, rejecting unsupported reached constructs with source locations and call chains. The current supported subset covers MidnightupdatePositionView; the generated inventory explicitly lists excluded code and scalar ABI projections.The reusable differential engine executes original Solidity in Foundry (A), the actual imported model through proof semantics
Denote.execStmtListwith real Keccak slots (B), and that model through the normal Verity→Yul→solc compiler in Foundry (C). Consumer projects supply a declarative fixture and regression inputs, without handwritten contract arithmetic.This exposed and fixes three real compilation defects: invalid temporary identifiers, checked/conditional results escaping their declaration scope, and nested if/else Yul condition locals shadowing one another. The affected compiler proofs are updated; the Midnight pilot’s five execution assertions still kernel-check.
Validation includes seeded input fuzzing, ignored ABI/storage noise, typed generated programs with renamed/helper/projection-collision variants, replay integrity checks, input/program reduction, and actual importer/Denote mutants. Compile failures, missing results and resource limits fail the harness; they never count as matching reverts or killed mutants. PRs run fixed seeds; scheduled/manual runs extend campaigns and require all four semantic mutants to be detected. Failure evidence is archived.
The source-to-model translator is not formally verified. A/B/C compare status, scalar outputs and observed storage; A/C additionally compare exact revert bytes. This first runner supports read-only calls, static scalar returns and the pinned Osaka profile. Full ABI equivalence, Denote panic payloads, gas/memory identity and a fourth EVMYulLean execution path are explicitly outside the implemented gate. See
Compiler/SoliditySlice/TESTING.mdfor reproduction and extension policy.Companion: lfglabs-dev/morpho-midnight-verity#1 (private). Its final dependency pin will be updated to the merged Verity commit.