diff --git a/AUDIT.md b/AUDIT.md index 9b80420f40..a7c1476ee2 100644 --- a/AUDIT.md +++ b/AUDIT.md @@ -53,7 +53,9 @@ source, Lean importer, specification, execution proofs and focused acceptance tests. It is independent of the handwritten `Contracts/Vault` example. The S1 inheritance slice adds `Contracts/SolidityImportSmoke/Inheritance` with the same shape (source, import command, named-storage spec, proofs, focused Python -suite). No +suite). The S2 modifiers/structs slice adds +`Contracts/SolidityImportSmoke/Modifiers` and +`Contracts/SolidityImportSmoke/Structs` with the same shape. No Python frontend, custom serialized IR, generated Lean source, or bytecode is in the translation path: the accepted Solidity subset is the kernel-checked inductive in `Importer/Syntax.lean` and `Importer/Semantics.lean` is its single @@ -63,6 +65,13 @@ meaning. Trust and axiom scope are recorded in Evidence command for the inheritance slice: `python3 Contracts/SolidityImportSmoke/Inheritance/scripts/inheritance_test.py` (after `lake build SolidityImportSmokeInheritance`). +Evidence commands for the modifiers/structs slice: +`python3 Contracts/SolidityImportSmoke/Modifiers/scripts/modifiers_test.py` +(after `lake build SolidityImportSmokeModifiers`) and +`python3 Contracts/SolidityImportSmoke/Structs/scripts/structs_test.py` +(after `lake build SolidityImportSmokeStructs`). The structs suite also +imports a named constructor that lists `{who, amount}` out of member order +(`Expr.pairRev` evaluates source order then packs `uint256 × address`). ## Current Audit State diff --git a/AXIOMS.md b/AXIOMS.md index 518b1c9726..d3454cfdc4 100644 --- a/AXIOMS.md +++ b/AXIOMS.md @@ -15,7 +15,10 @@ and `Quot.sound`; they do not depend on `solidityMappingSlot_injective`. `solvent_invariant` is included in that audit. The inheritance-slice suite `inheritance_test.py` runs the same `#print axioms` gate on every theorem in `Contracts/SolidityImportSmoke/Inheritance/Proofs.lean` and likewise requires -only `propext` and `Quot.sound`. This does not remove the trusted Solidity frontend/translation boundary described +only `propext` and `Quot.sound`. The modifiers and structs suites +`modifiers_test.py` and `structs_test.py` run the same gate on +`Contracts/SolidityImportSmoke/Modifiers/Proofs.lean` and +`Contracts/SolidityImportSmoke/Structs/Proofs.lean`. This does not remove the trusted Solidity frontend/translation boundary described in `TRUST_ASSUMPTIONS.md`, or change the compiler axiom registry below. ## Policy diff --git a/Contracts/SolidityImportSmoke/Modifiers/Modifiers.lean b/Contracts/SolidityImportSmoke/Modifiers/Modifiers.lean new file mode 100644 index 0000000000..0738eb2da4 --- /dev/null +++ b/Contracts/SolidityImportSmoke/Modifiers/Modifiers.lean @@ -0,0 +1,7 @@ +import Contracts.VaultFromSolidity.Importer.Importer + +namespace Contracts.SolidityImportSmoke.Modifiers + +solidity_contract Child from "Modifiers.sol" + +end Contracts.SolidityImportSmoke.Modifiers diff --git a/Contracts/SolidityImportSmoke/Modifiers/Modifiers.sol b/Contracts/SolidityImportSmoke/Modifiers/Modifiers.sol new file mode 100644 index 0000000000..4f66957a90 --- /dev/null +++ b/Contracts/SolidityImportSmoke/Modifiers/Modifiers.sol @@ -0,0 +1,93 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.33; + +error NotOwner(); +error EnforcedPause(); +error ReentrancyGuardReentrantCall(); + +abstract contract OwnableLike { + address public owner; + + modifier onlyOwner() { + if (msg.sender != owner) revert NotOwner(); + _; + } +} + +abstract contract PausableLike { + uint256 public paused; + + modifier whenNotPaused() { + if (0 < paused) revert EnforcedPause(); + _; + } +} + +abstract contract ReentrancyGuardLike { + uint256 public status; + + modifier nonReentrant() { + if (1 < status) revert ReentrancyGuardReentrantCall(); + status = 2; + _; + status = 1; + } + + modifier restore() { + uint256 old = status; + _; + status = old; + } +} + +abstract contract HelperLike { + uint256 public helperValue; + + modifier bumpHelper() { + bump(); + _; + } + + function bump() private { + helperValue = 1; + } +} + +contract Child is OwnableLike, PausableLike, ReentrancyGuardLike, HelperLike { + uint256 public value; + + function setOwner(address next) external { + owner = next; + } + + function arm() external { + status = 1; + } + + function guarded(uint256 amount) external onlyOwner whenNotPaused { + value = amount; + } + + function enter(uint256 amount) external nonReentrant returns (uint256) { + value = amount; + return amount; + } + + function early(uint256 amount) external nonReentrant returns (uint256) { + value = amount; + return amount; + } + + function poison() private { + helperValue = 2; + } + + function tagged() external bumpHelper { + value = 0; + } + + function snapshot(uint256 amount) external restore returns (uint256) { + status = amount; + return amount; + } +} diff --git a/Contracts/SolidityImportSmoke/Modifiers/Proofs.lean b/Contracts/SolidityImportSmoke/Modifiers/Proofs.lean new file mode 100644 index 0000000000..62c850e97a --- /dev/null +++ b/Contracts/SolidityImportSmoke/Modifiers/Proofs.lean @@ -0,0 +1,75 @@ +import Contracts.SolidityImportSmoke.Modifiers.Spec +import Verity.Proofs.Stdlib.SolidityImport + +namespace Contracts.SolidityImportSmoke.Modifiers.Proofs +open Verity +open Verity.Proofs.Stdlib.SolidityImport +open Contracts.SolidityImportSmoke.Modifiers.Child +open Spec + +theorem status_restored (s post : ContractState) (amount : Uint256) + (h : (early amount).run s = .success amount post) : + early_spec amount (view s) (view post) := by + unfold early_spec + by_cases h0 : s.msgValue = 0 + · by_cases hst : 1 < (view s).status.val + · solidity_simp + · solidity_simp + subst h + solidity_simp + · solidity_simp + +theorem early_meets_spec (s : ContractState) (amount : Uint256) + (h0 : s.msgValue = 0) (harmed : (view s).status = 1) : + ∃ post, (early amount).run s = ContractResult.success amount post ∧ + early_spec amount (view s) (view post) := by + unfold early_spec + solidity_simp + +theorem guarded_success_spec (s post : ContractState) (amount : Uint256) + (h : (guarded amount).run s = .success () post) : + guarded_spec amount (view s) (view post) := by + unfold guarded_spec + by_cases h0 : s.msgValue = 0 + · by_cases ho : s.sender = (view s).owner + · by_cases hp : (view s).paused.val = 0 + · solidity_simp + subst h + solidity_simp + · solidity_simp + · by_cases hp : (view s).paused.val = 0 + · solidity_simp + · solidity_simp + · solidity_simp + +theorem guarded_reverts_not_owner_before_pause (s : ContractState) (amount : Uint256) + (h0 : s.msgValue = 0) + (howner : s.sender ≠ (view s).owner) + (hpaused : 0 < (view s).paused.val) : + (guarded amount).run s = ContractResult.revert "NotOwner()" s := by + by_cases ho : s.sender = (view s).owner + · exact (howner ho).elim + · have := hpaused + solidity_simp + +theorem tagged_uses_base_helper (s post : ContractState) + (h : tagged.run s = .success () post) : + tagged_spec (view s) (view post) := by + unfold tagged_spec + by_cases h0 : s.msgValue = 0 + · solidity_simp + subst h + solidity_simp + · solidity_simp + +theorem snapshot_restores_status (s post : ContractState) (amount : Uint256) + (h : (snapshot amount).run s = .success amount post) : + snapshot_spec amount (view s) (view post) := by + unfold snapshot_spec + by_cases h0 : s.msgValue = 0 + · solidity_simp + subst h + solidity_simp + · solidity_simp + +end Contracts.SolidityImportSmoke.Modifiers.Proofs diff --git a/Contracts/SolidityImportSmoke/Modifiers/Spec.lean b/Contracts/SolidityImportSmoke/Modifiers/Spec.lean new file mode 100644 index 0000000000..4b7d370096 --- /dev/null +++ b/Contracts/SolidityImportSmoke/Modifiers/Spec.lean @@ -0,0 +1,36 @@ +import Verity.EVM.Uint256 +import Contracts.SolidityImportSmoke.Modifiers.Modifiers + +namespace Contracts.SolidityImportSmoke.Modifiers.Spec + +open Verity +open Verity.EVM.Uint256 +open Contracts.SolidityImportSmoke.Modifiers.Child + +def early_spec (amount : Uint256) (pre post : Storage) : Prop := + post.status = 1 ∧ + post.value = amount ∧ + post.owner = pre.owner ∧ + post.paused = pre.paused + +def guarded_spec (amount : Uint256) (pre post : Storage) : Prop := + post.value = amount ∧ + post.status = pre.status ∧ + post.owner = pre.owner ∧ + post.paused = pre.paused + +def tagged_spec (pre post : Storage) : Prop := + post.helperValue = 1 ∧ + post.value = 0 ∧ + post.status = pre.status ∧ + post.owner = pre.owner ∧ + post.paused = pre.paused + +def snapshot_spec (_amount : Uint256) (pre post : Storage) : Prop := + post.status = pre.status ∧ + post.value = pre.value ∧ + post.owner = pre.owner ∧ + post.paused = pre.paused ∧ + post.helperValue = pre.helperValue + +end Contracts.SolidityImportSmoke.Modifiers.Spec diff --git a/Contracts/SolidityImportSmoke/Modifiers/scripts/modifiers_test.py b/Contracts/SolidityImportSmoke/Modifiers/scripts/modifiers_test.py new file mode 100755 index 0000000000..51f058736a --- /dev/null +++ b/Contracts/SolidityImportSmoke/Modifiers/scripts/modifiers_test.py @@ -0,0 +1,268 @@ +#!/usr/bin/env python3 +"""Acceptance checks for the Solidity importer modifiers slice.""" + +import hashlib +import os +from pathlib import Path +import re +import shutil +import subprocess +import tempfile + +ROOT = Path(__file__).resolve().parents[4] + + +def lake_binary() -> str: + version = (ROOT / "lean-toolchain").read_text().strip().split(":")[-1] + candidates = [ + Path.home() / ".elan/toolchains" / f"leanprover--lean4---{version}" / "bin/lake", + Path("/var/lib/opencode/.elan/toolchains") / f"leanprover--lean4---{version}" / "bin/lake", + ] + for candidate in candidates: + if candidate.is_file(): + return str(candidate) + found = shutil.which("lake") + if found: + return found + raise RuntimeError("lake executable not found") + + +LAKE = lake_binary() +ENV = dict(os.environ) +SMOKE = "Contracts/SolidityImportSmoke/Modifiers" +TARGET = "SolidityImportSmokeModifiers" +NS = "Contracts.SolidityImportSmoke.Modifiers.Child" +PROOF = f"{SMOKE}/Proofs.lean" + + +def check(ok: bool, message: str) -> None: + if not ok: + raise AssertionError(message) + print("PASS " + message, flush=True) + + +def run(root: Path, args: list[str], success: bool = True, contains: str | None = None) -> str: + process = subprocess.run( + args, cwd=root, env=ENV, text=True, capture_output=True, timeout=300 + ) + output = process.stdout + process.stderr + if (process.returncode == 0) != success or (contains and contains not in output) or "PANIC" in output: + raise AssertionError(f"{args}: exit {process.returncode}\n{output}") + return output + + +def main() -> None: + importer_path = ROOT / "Contracts/VaultFromSolidity/Importer/Importer.lean" + syntax_path = ROOT / "Contracts/VaultFromSolidity/Importer/Syntax.lean" + semantics_path = ROOT / "Contracts/VaultFromSolidity/Importer/Semantics.lean" + importer_text = importer_path.read_text() + syntax_text = syntax_path.read_text() + semantics_text = semantics_path.read_text() + check("| seq " in syntax_text and "| block " in syntax_text, + "modifier inlining uses Stmt.seq / Stmt.block") + check("Semantics.lean never sees `_`" in semantics_text or + "this file never sees `_`" in semantics_text, + "modifier placeholder is inlined at parse time") + check("wrapModifiers" in importer_text and "modifier with two placeholders" in importer_text, + "importer inlines modifiers and rejects two placeholders") + check("modifier arguments" in importer_text, + "importer rejects parameterized modifiers") + check("static.visibility == \"private\"" in importer_text and "!static.virtual" in importer_text, + "identifier calls keep private/non-virtual static binding") + check("wrapModifierParts" in importer_text and "inner.shift .uint 0" in importer_text, + "prelude locals are bound over the inlined body and postlude") + + with tempfile.TemporaryDirectory(prefix="verity-mod-check-", dir=ROOT.parent) as directory: + root = Path(directory) + for name in ("Verity", "Compiler", "Contracts", "scripts"): + shutil.copytree(ROOT / name, root / name) + for name in ("lakefile.lean", "lake-manifest.json", "lean-toolchain"): + shutil.copy2(ROOT / name, root / name) + shutil.copytree(ROOT / ".lake/build", root / ".lake/build") + (root / ".lake/solidity-import").mkdir(parents=True) + shutil.copy2(ROOT / ".lake/solidity-import/solc", root / ".lake/solidity-import/solc") + (root / ".lake/packages").symlink_to(ROOT / ".lake/packages", target_is_directory=True) + + source = root / SMOKE / "Modifiers.sol" + original = source.read_bytes() + source_stamp = source.stat() + importer = root / "Contracts/VaultFromSolidity/Importer/Importer.lean" + importer_original = importer.read_bytes() + importer_stamp = importer.stat() + proof = root / PROOF + proof_text = proof.read_text() + theorem_names = re.findall(r"^theorem\s+(\w+)", proof_text, re.M) + + def edit_source(data: bytes) -> None: + source.write_bytes(data) + os.utime(source, ns=(source_stamp.st_atime_ns, source_stamp.st_mtime_ns)) + + def build(success: bool = True, contains: str | None = None) -> str: + return run(root, [LAKE, "build", TARGET], success, contains) + + def artifacts() -> dict[str, tuple[int, str]]: + paths = list((root / ".lake/build/lib/lean/Contracts/SolidityImportSmoke/Modifiers").rglob("*.olean")) + return { + str(path.relative_to(root)): ( + path.stat().st_mtime_ns, + hashlib.sha256(path.read_bytes()).hexdigest(), + ) + for path in paths + } + + def print_names(*names: str) -> str: + probe = root / ".lake/solidity-import/ModPrint.lean" + try: + probe.write_text( + f"import {SMOKE.replace('/', '.')}.Modifiers\n" + + "".join(f"#print {NS}.{name}\n" for name in names) + ) + return run(root, [LAKE, "env", "lean", str(probe)]) + finally: + probe.unlink(missing_ok=True) + + build() + check(True, "baseline lake build SolidityImportSmokeModifiers") + + audit_file = root / ".lake/solidity-import/ModAxiomAudit.lean" + try: + audit_file.write_text( + f"import {SMOKE.replace('/', '.')}.Proofs\n" + + "\n".join( + f"#print axioms {SMOKE.replace('/', '.')}.Proofs.{name}" + for name in theorem_names + ) + + "\n" + ) + audit = run(root, [LAKE, "env", "lean", str(audit_file)]) + finally: + audit_file.unlink(missing_ok=True) + entries = re.findall( + r"'Contracts.SolidityImportSmoke.Modifiers.Proofs.(\w+)' depends on axioms: \[([^\]]*)\]", + audit, + ) + check(set(theorem_names) == {name for name, _ in entries}, + "every modifier theorem appears in #print axioms output") + axioms = {a.strip() for _, values in entries for a in values.split(",") if a.strip()} + check(axioms <= {"propext", "Quot.sound"}, + "no project axioms or sorryAx: " + ", ".join(sorted(axioms))) + + printed_early = print_names("early") + check(".seq" in printed_early and ".block" in printed_early, + "#print Child.early inlines nonReentrant as seq/block") + printed_guarded = print_names("guarded") + check(printed_guarded.find("NotOwner") < printed_guarded.find("EnforcedPause"), + "onlyOwner then whenNotPaused is declaration order") + printed_tagged = print_names("tagged") + check("HelperLike_bump" in printed_tagged and "Child_bump" not in printed_tagged, + "inherited modifier keeps the declaring contract's private helper") + printed_snapshot = print_names("snapshot") + check(".local_" in printed_snapshot and ".block" in printed_snapshot, + "#print Child.snapshot carries restore prelude local into the postlude") + + def broken_theorems(output: str) -> set[str]: + error_lines = [int(value) for value in re.findall(rf"{PROOF}:(\d+):", output)] + starts = [ + (match.group(1), line_no) + for line_no, line in enumerate(proof_text.splitlines(), 1) + if (match := re.match(r"theorem\s+([A-Za-z0-9_']+)", line.strip())) + ] + ranges = { + name: (start, starts[index + 1][1] - 1 if index + 1 < len(starts) + else len(proof_text.splitlines())) + for index, (name, start) in enumerate(starts) + } + return {name for name, (start, end) in ranges.items() + if any(start <= line <= end for line in error_lines)} + + postlude = b" status = 2;\n _;\n status = 1;" + dropped = b" status = 2;\n _;" + check(original.count(postlude) == 1, "nonReentrant postlude has one source target") + edit_source(original.replace(postlude, dropped)) + output = build(False, "Contracts.SolidityImportSmoke.Modifiers.Proofs") + check(bool({"status_restored", "early_meets_spec"} & broken_theorems(output)), + "dropping the nonReentrant postlude breaks status_restored") + edit_source(original) + build() + + swapped = original.replace(b"onlyOwner whenNotPaused", b"whenNotPaused onlyOwner") + check(original != swapped, "modifier-order mutation has a source target") + edit_source(swapped) + output = build(False, "Contracts.SolidityImportSmoke.Modifiers.Proofs") + check("guarded_reverts_not_owner_before_pause" in broken_theorems(output), + "swapping onlyOwner/whenNotPaused breaks guarded_reverts_not_owner_before_pause") + edit_source(original) + build() + + before = artifacts() + importer.write_bytes(importer_original + b"\n-- modifiers identity probe\n") + os.utime(importer, ns=(importer_stamp.st_atime_ns, importer_stamp.st_mtime_ns)) + build() + check(before != artifacts(), "Lean importer content change invalidates modifier artifacts") + importer.write_bytes(importer_original) + build() + + two_ph_old = b" if (msg.sender != owner) revert NotOwner();\n _;" + two_ph_new = b" if (msg.sender != owner) revert NotOwner();\n _;\n _;" + check(original.count(two_ph_old) == 1, "two placeholders mutation has one source target") + edit_source(original.replace(two_ph_old, two_ph_new)) + output = build(False, "modifier with two placeholders") + check(re.search(r"Contracts/SolidityImportSmoke/Modifiers/Modifiers.sol:\d+:\d+:", output) + is not None, + "two placeholders rejected with source position") + edit_source(original) + + args_src = original.replace( + b" modifier onlyOwner() {\n if (msg.sender != owner) revert NotOwner();\n _;\n }", + b" modifier onlyOwner(uint256 unused) {\n unused;\n if (msg.sender != owner) revert NotOwner();\n _;\n }", + ).replace( + b" function guarded(uint256 amount) external onlyOwner whenNotPaused {", + b" function guarded(uint256 amount) external onlyOwner(0) whenNotPaused {", + ) + check(args_src != original, "modifier arguments mutation has a source target") + edit_source(args_src) + output = build(False, "modifier arguments") + check(re.search(r"Contracts/SolidityImportSmoke/Modifiers/Modifiers.sol:\d+:\d+:", output) + is not None, + "modifier arguments rejected with source position") + edit_source(original) + build() + + restore_post = b" uint256 old = status;\n _;\n status = old;" + restore_dropped = b" uint256 old = status;\n _;" + check(original.count(restore_post) == 1, "restore postlude has one source target") + edit_source(original.replace(restore_post, restore_dropped)) + output = build(False, "Contracts.SolidityImportSmoke.Modifiers.Proofs") + check(bool({"snapshot_restores_status"} & broken_theorems(output)), + "dropping the restore postlude breaks snapshot_restores_status") + edit_source(original) + build() + + base_helper = b" function bump() private {\n helperValue = 1;\n }" + base_helper_mut = b" function bump() private {\n helperValue = 9;\n }" + check(original.count(base_helper) == 1, "base private helper has one source target") + edit_source(original.replace(base_helper, base_helper_mut)) + output = build(False, "Contracts.SolidityImportSmoke.Modifiers.Proofs") + check(bool({"tagged_uses_base_helper"} & broken_theorems(output)), + "mutating the declaring contract's private helper breaks tagged_uses_base_helper") + edit_source(original) + build() + poison = b" function poison() private {\n helperValue = 2;\n }" + poison_mut = b" function poison() private {\n helperValue = 9;\n }" + check(original.count(poison) == 1, "unrelated derived private helper has one source target") + edit_source(original.replace(poison, poison_mut)) + build() + mutated_tagged = print_names("tagged") + check("HelperLike_bump" in mutated_tagged and "Child_bump" not in mutated_tagged, + "mutating an unrelated derived private helper does not rebind the inherited modifier") + edit_source(original) + build() + + check(source.read_bytes() == original and importer.read_bytes() == importer_original, + "temporary mutations restored; final baseline passes") + print(f"PASS all modifier-slice acceptance checks ({len(theorem_names)} audited theorems)", + flush=True) + + +if __name__ == "__main__": + main() diff --git a/Contracts/SolidityImportSmoke/Structs/Proofs.lean b/Contracts/SolidityImportSmoke/Structs/Proofs.lean new file mode 100644 index 0000000000..0a77c561df --- /dev/null +++ b/Contracts/SolidityImportSmoke/Structs/Proofs.lean @@ -0,0 +1,39 @@ +import Contracts.SolidityImportSmoke.Structs.Spec +import Verity.Proofs.Stdlib.SolidityImport + +namespace Contracts.SolidityImportSmoke.Structs.Proofs +open Verity +open Verity.Proofs.Stdlib.SolidityImport +open Contracts.SolidityImportSmoke.Structs.Store +open Spec + +theorem set_then_get (s post : ContractState) (amount : Uint256) (who : Address) + (h : (set (amount, who)).run s = .success () post) : + set_spec amount who (view s) (view post) := by + unfold set_spec + cases hbeq : Nat.beq s.msgValue.val 0 + · solidity_simp + · solidity_simp + subst h + solidity_simp + +theorem other_member_unchanged_thm (s post : ContractState) (amount : Uint256) (who : Address) + (h : (set (amount, who)).run s = .success () post) : + other_member_unchanged (amount, who) (view s) (view post) := + (set_then_get s post amount who h).2.2 + +theorem get_meets_spec (s : ContractState) (h0 : s.msgValue = 0) : + ∃ post, get.run s = ContractResult.success ((view s).data_amount, (view s).data_who) post := by + solidity_simp + +theorem make_encodes (s : ContractState) (amount : Uint256) (who : Address) + (h0 : s.msgValue = 0) : + ∃ post, (make amount who).run s = ContractResult.success (amount, who) post := by + solidity_simp + +theorem makeRev_encodes (s : ContractState) (amount : Uint256) (who : Address) + (h0 : s.msgValue = 0) : + ∃ post, (makeRev amount who).run s = ContractResult.success (amount, who) post := by + solidity_simp + +end Contracts.SolidityImportSmoke.Structs.Proofs diff --git a/Contracts/SolidityImportSmoke/Structs/Spec.lean b/Contracts/SolidityImportSmoke/Structs/Spec.lean new file mode 100644 index 0000000000..47883c4fc3 --- /dev/null +++ b/Contracts/SolidityImportSmoke/Structs/Spec.lean @@ -0,0 +1,17 @@ +import Verity.EVM.Uint256 +import Contracts.SolidityImportSmoke.Structs.Structs + +namespace Contracts.SolidityImportSmoke.Structs.Spec + +open Verity +open Contracts.SolidityImportSmoke.Structs.Store + +def set_spec (amount : Uint256) (who : Address) (pre post : Storage) : Prop := + post.data_amount = amount ∧ + post.data_who = who ∧ + post.other = pre.other + +def other_member_unchanged (_a : Uint256 × Address) (pre post : Storage) : Prop := + post.other = pre.other + +end Contracts.SolidityImportSmoke.Structs.Spec diff --git a/Contracts/SolidityImportSmoke/Structs/Structs.lean b/Contracts/SolidityImportSmoke/Structs/Structs.lean new file mode 100644 index 0000000000..ba4de8e030 --- /dev/null +++ b/Contracts/SolidityImportSmoke/Structs/Structs.lean @@ -0,0 +1,7 @@ +import Contracts.VaultFromSolidity.Importer.Importer + +namespace Contracts.SolidityImportSmoke.Structs + +solidity_contract Store from "Structs.sol" + +end Contracts.SolidityImportSmoke.Structs diff --git a/Contracts/SolidityImportSmoke/Structs/Structs.sol b/Contracts/SolidityImportSmoke/Structs/Structs.sol new file mode 100644 index 0000000000..99a6ae6c55 --- /dev/null +++ b/Contracts/SolidityImportSmoke/Structs/Structs.sol @@ -0,0 +1,32 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.33; + +struct Acc { + uint256 amount; + address who; +} + +contract Store { + Acc public data; + uint256 public other; + + function set(Acc memory a) external { + data = a; + } + + function get() external view returns (Acc memory) { + return data; + } + + function setOther(uint256 n) external { + other = n; + } + + function make(uint256 amount, address who) external pure returns (Acc memory) { + return Acc({amount: amount, who: who}); + } + + function makeRev(uint256 amount, address who) external pure returns (Acc memory) { + return Acc({who: who, amount: amount}); + } +} diff --git a/Contracts/SolidityImportSmoke/Structs/scripts/structs_test.py b/Contracts/SolidityImportSmoke/Structs/scripts/structs_test.py new file mode 100755 index 0000000000..a11316103c --- /dev/null +++ b/Contracts/SolidityImportSmoke/Structs/scripts/structs_test.py @@ -0,0 +1,293 @@ +#!/usr/bin/env python3 +"""Acceptance checks for the Solidity importer structs slice.""" + +import hashlib +import os +from pathlib import Path +import re +import shutil +import subprocess +import tempfile + +ROOT = Path(__file__).resolve().parents[4] + + +def lake_binary() -> str: + version = (ROOT / "lean-toolchain").read_text().strip().split(":")[-1] + candidates = [ + Path.home() / ".elan/toolchains" / f"leanprover--lean4---{version}" / "bin/lake", + Path("/var/lib/opencode/.elan/toolchains") / f"leanprover--lean4---{version}" / "bin/lake", + ] + for candidate in candidates: + if candidate.is_file(): + return str(candidate) + found = shutil.which("lake") + if found: + return found + raise RuntimeError("lake executable not found") + + +LAKE = lake_binary() +ENV = dict(os.environ) +SMOKE = "Contracts/SolidityImportSmoke/Structs" +TARGET = "SolidityImportSmokeStructs" +NS = "Contracts.SolidityImportSmoke.Structs.Store" +PROOF = f"{SMOKE}/Proofs.lean" + + +def check(ok: bool, message: str) -> None: + if not ok: + raise AssertionError(message) + print("PASS " + message, flush=True) + + +def run(root: Path, args: list[str], success: bool = True, contains: str | None = None) -> str: + process = subprocess.run( + args, cwd=root, env=ENV, text=True, capture_output=True, timeout=300 + ) + output = process.stdout + process.stderr + if (process.returncode == 0) != success or (contains and contains not in output) or "PANIC" in output: + raise AssertionError(f"{args}: exit {process.returncode}\n{output}") + return output + + +def main() -> None: + importer_path = ROOT / "Contracts/VaultFromSolidity/Importer/Importer.lean" + syntax_path = ROOT / "Contracts/VaultFromSolidity/Importer/Syntax.lean" + importer_text = importer_path.read_text() + syntax_text = syntax_path.read_text() + check("| pair " in syntax_text and "| fst " in syntax_text and "| snd " in syntax_text, + "user structs are Expr.pair / fst / snd") + check("StructDefinition" in importer_text and "UserDefinedTypeName" in importer_text, + "importer accepts struct AST nodes") + check("structConstructorCall" in importer_text, + "importer encodes struct constructors") + check("| pairRev " in syntax_text and ".pairRev " in importer_text, + "named Acc({who, amount}) uses pairRev after source-order eval") + check(".pairRev a b =>" in (ROOT / "Contracts/VaultFromSolidity/Importer/Semantics.lean").read_text(), + "pairRev evaluates who then amount and packs uint-then-addr") + check("struct with a dynamic member" in importer_text and "mapping with struct key" in importer_text, + "importer rejects dynamic members and struct mapping keys") + + with tempfile.TemporaryDirectory(prefix="verity-struct-check-", dir=ROOT.parent) as directory: + root = Path(directory) + for name in ("Verity", "Compiler", "Contracts", "scripts"): + shutil.copytree(ROOT / name, root / name) + for name in ("lakefile.lean", "lake-manifest.json", "lean-toolchain"): + shutil.copy2(ROOT / name, root / name) + shutil.copytree(ROOT / ".lake/build", root / ".lake/build") + (root / ".lake/solidity-import").mkdir(parents=True) + shutil.copy2(ROOT / ".lake/solidity-import/solc", root / ".lake/solidity-import/solc") + (root / ".lake/packages").symlink_to(ROOT / ".lake/packages", target_is_directory=True) + + source = root / SMOKE / "Structs.sol" + original = source.read_bytes() + source_stamp = source.stat() + importer = root / "Contracts/VaultFromSolidity/Importer/Importer.lean" + importer_original = importer.read_bytes() + importer_stamp = importer.stat() + proof = root / PROOF + proof_text = proof.read_text() + theorem_names = re.findall(r"^theorem\s+(\w+)", proof_text, re.M) + + def edit_source(data: bytes) -> None: + source.write_bytes(data) + os.utime(source, ns=(source_stamp.st_atime_ns, source_stamp.st_mtime_ns)) + + def build(success: bool = True, contains: str | None = None) -> str: + return run(root, [LAKE, "build", TARGET], success, contains) + + def artifacts() -> dict[str, tuple[int, str]]: + paths = list((root / ".lake/build/lib/lean/Contracts/SolidityImportSmoke/Structs").rglob("*.olean")) + return { + str(path.relative_to(root)): ( + path.stat().st_mtime_ns, + hashlib.sha256(path.read_bytes()).hexdigest(), + ) + for path in paths + } + + def print_names(*names: str) -> str: + probe = root / ".lake/solidity-import/StructPrint.lean" + try: + probe.write_text( + f"import {SMOKE.replace('/', '.')}.Structs\n" + + "".join(f"#print {NS}.{name}\n" for name in names) + ) + return run(root, [LAKE, "env", "lean", str(probe)]) + finally: + probe.unlink(missing_ok=True) + + def slot_numbers() -> str: + slot_probe = root / ".lake/solidity-import/StructSlotProbe.lean" + try: + slot_probe.write_text( + f"import {SMOKE.replace('/', '.')}.Structs\n" + f"#eval [{NS}.data_amountSlot.slot, {NS}.data_whoSlot.slot, {NS}.otherSlot.slot]\n" + ) + found = re.findall(r"\[\d+(?:, \d+)*\]", run(root, [LAKE, "env", "lean", str(slot_probe)])) + if not found: + raise AssertionError("slot probe produced no list") + return found[0] + finally: + slot_probe.unlink(missing_ok=True) + + build() + check(True, "baseline lake build SolidityImportSmokeStructs") + + audit_file = root / ".lake/solidity-import/StructAxiomAudit.lean" + try: + audit_file.write_text( + f"import {SMOKE.replace('/', '.')}.Proofs\n" + + "\n".join( + f"#print axioms {SMOKE.replace('/', '.')}.Proofs.{name}" + for name in theorem_names + ) + + "\n" + ) + audit = run(root, [LAKE, "env", "lean", str(audit_file)]) + finally: + audit_file.unlink(missing_ok=True) + entries = re.findall( + r"'Contracts.SolidityImportSmoke.Structs.Proofs.(\w+)' depends on axioms: \[([^\]]*)\]", + audit, + ) + check(set(theorem_names) == {name for name, _ in entries}, + "every struct theorem appears in #print axioms output") + axioms = {a.strip() for _, values in entries for a in values.split(",") if a.strip()} + check(axioms <= {"propext", "Quot.sound"}, + "no project axioms or sorryAx: " + ", ".join(sorted(axioms))) + + printed = print_names("set", "get", "make", "makeRev") + check(".fst" in printed and ".snd" in printed, + "#print Store.set decodes struct members") + check(".pair" in printed, + "#print Store.make / Store.get encode the user struct") + check(".pairRev" in printed, + "#print Store.makeRev encodes named Acc({who, amount})") + check(slot_numbers() == "[0, 1, 2]", + "struct members occupy consecutive solc slots [amount, who, other]") + + def broken_theorems(output: str) -> set[str]: + error_lines = [int(value) for value in re.findall(rf"{PROOF}:(\d+):", output)] + starts = [ + (match.group(1), line_no) + for line_no, line in enumerate(proof_text.splitlines(), 1) + if (match := re.match(r"theorem\s+([A-Za-z0-9_']+)", line.strip())) + ] + ranges = { + name: (start, starts[index + 1][1] - 1 if index + 1 < len(starts) + else len(proof_text.splitlines())) + for index, (name, start) in enumerate(starts) + } + return {name for name, (start, end) in ranges.items() + if any(start <= line <= end for line in error_lines)} + + dropped_who = original.replace( + b" data = a;\n", + b" data = Acc({amount: a.amount, who: data.who});\n", + ) + check(original != dropped_who, "dropped who write has a source target") + edit_source(dropped_who) + output = build(False, "Contracts.SolidityImportSmoke.Structs.Proofs") + check("set_then_get" in broken_theorems(output), + "dropping the who write breaks set_then_get") + edit_source(original) + build() + + reordered = original.replace( + b"struct Acc {\n uint256 amount;\n address who;\n}", + b"struct Acc {\n address who;\n uint256 amount;\n}", + ) + check(original != reordered, "struct member reorder has a source target") + edit_source(reordered) + output = build(False, "unsupported struct shape") + check(re.search(r"Contracts/SolidityImportSmoke/Structs/Structs.sol:\d+:\d+:", output) + is not None, + "reordering pair members is rejected with a source position") + edit_source(original) + build() + + named_reorder = original.replace( + b" return Acc({amount: amount, who: who});", + b" return Acc({who: who, amount: amount});", + ) + check(original != named_reorder, "named constructor reorder has a source target") + edit_source(named_reorder) + build() + printed_rev = print_names("make") + check(".pairRev" in printed_rev, + "named Acc({who, amount}) imports as pairRev") + check(True, "named Acc({who: who, amount: amount}) still imports") + edit_source(original) + build() + printed_fwd = print_names("make") + check(".pair" in printed_fwd and ".pairRev" not in printed_fwd, + "named Acc({amount, who}) stays Expr.pair") + + positional = original.replace( + b" return Acc({amount: amount, who: who});", + b" return Acc(amount, who);", + ) + check(original != positional, "positional constructor has a source target") + edit_source(positional) + build() + printed_pos = print_names("make") + check(".pair" in printed_pos and ".pairRev" not in printed_pos, + "positional Acc(amount, who) stays AST/member order as Expr.pair") + edit_source(original) + build() + + before = artifacts() + importer.write_bytes(importer_original + b"\n-- structs identity probe\n") + os.utime(importer, ns=(importer_stamp.st_atime_ns, importer_stamp.st_mtime_ns)) + build() + check(before != artifacts(), "Lean importer content change invalidates struct artifacts") + importer.write_bytes(importer_original) + build() + + dyn_src = original.replace( + b" address who;\n", + b" address who;\n string note;\n", + ).replace( + b" return Acc({amount: amount, who: who});", + b" return Acc({amount: amount, who: who, note: \"\"});", + ).replace( + b" return Acc({who: who, amount: amount});", + b" return Acc({who: who, amount: amount, note: \"\"});", + ) + check(dyn_src != original, "dynamic member mutation has a source target") + edit_source(dyn_src) + output = build(False) + check( + "struct with a dynamic member" in output or "unsupported struct shape" in output, + "dynamic member is rejected", + ) + check(re.search(r"Contracts/SolidityImportSmoke/Structs/Structs.sol:\d+:\d+:", output) + is not None, + "dynamic member rejected with source position") + edit_source(original) + + key_old = b" Acc public data;\n uint256 public other;\n" + key_new = b" Acc public data;\n uint256 public other;\n mapping(Acc => uint256) private keyed;\n" + check(original.count(key_old) == 1, "struct mapping key mutation has one source target") + edit_source(original.replace(key_old, key_new)) + output = build(False) + check( + "mapping with struct key" in output or "TypeError" in output, + "mapping with struct key is rejected", + ) + check(re.search(r"Contracts/SolidityImportSmoke/Structs/Structs.sol:\d+:\d+:", output) + is not None, + "mapping with struct key rejected with source position") + edit_source(original) + build() + + check(source.read_bytes() == original and importer.read_bytes() == importer_original, + "temporary mutations restored; final baseline passes") + print(f"PASS all struct-slice acceptance checks ({len(theorem_names)} audited theorems)", + flush=True) + + +if __name__ == "__main__": + main() diff --git a/Contracts/VaultFromSolidity/Importer/Importer.lean b/Contracts/VaultFromSolidity/Importer/Importer.lean index 7269ff9629..a3bfd56460 100644 --- a/Contracts/VaultFromSolidity/Importer/Importer.lean +++ b/Contracts/VaultFromSolidity/Importer/Importer.lean @@ -38,7 +38,11 @@ a source moves every imported `sourceDigest`. -/ private def registeredSources : List (String × String) := [ ("Contracts/VaultFromSolidity/Vault.sol", "Contracts/VaultFromSolidity/Vault.sol"), ("Contracts/SolidityImportSmoke/Inheritance/Inheritance.sol", - "Contracts/SolidityImportSmoke/Inheritance/Inheritance.sol") + "Contracts/SolidityImportSmoke/Inheritance/Inheritance.sol"), + ("Contracts/SolidityImportSmoke/Modifiers/Modifiers.sol", + "Contracts/SolidityImportSmoke/Modifiers/Modifiers.sol"), + ("Contracts/SolidityImportSmoke/Structs/Structs.sol", + "Contracts/SolidityImportSmoke/Structs/Structs.sol") ] private def field (j : Json) (key : String) : MetaM Json := @@ -184,6 +188,12 @@ private def allowedNodeFields : String → Option (List String) | "IfStatement" => some ["condition", "trueBody", "falseBody"] | "RevertStatement" => some ["errorCall"] | "Return" => some ["expression", "functionReturnParameters"] + | "ModifierDefinition" => some ["body", "name", "nameLocation", "parameters", "virtual", "visibility", + "documentation"] + | "ModifierInvocation" => some ["arguments", "kind", "modifierName"] + | "PlaceholderStatement" => some ([] : List String) + | "StructDefinition" => some ["canonicalName", "members", "name", "nameLocation", "scope", "visibility"] + | "UserDefinedTypeName" => some ["pathNode", "referencedDeclaration", "typeDescriptions"] | _ => none private def requiredNodeFields : String → List String @@ -219,12 +229,18 @@ private def requiredNodeFields : String → List String | "IfStatement" => ["condition", "trueBody"] | "RevertStatement" => ["errorCall"] | "Return" => ["expression", "functionReturnParameters"] + | "ModifierDefinition" => ["name", "nameLocation", "parameters", "virtual", "visibility"] + | "ModifierInvocation" => ["kind", "modifierName"] + | "PlaceholderStatement" => [] + | "StructDefinition" => ["canonicalName", "members", "name", "nameLocation", "scope", "visibility"] + | "UserDefinedTypeName" => ["pathNode", "referencedDeclaration", "typeDescriptions"] | _ => [] private def childFields : List String := ["nodes", "baseContracts", "parameters", "returnParameters", "body", "statements", "typeName", "keyType", "valueType", "modifiers", "overrides", "storageLayout", "leftHandSide", "rightHandSide", "leftExpression", "rightExpression", "expression", "baseExpression", "indexExpression", - "arguments", "declarations", "initialValue", "condition", "trueBody", "falseBody", "errorCall", "baseName"] + "arguments", "declarations", "initialValue", "condition", "trueBody", "falseBody", "errorCall", "baseName", + "members", "modifierName", "pathNode"] private def validateTypeDescription (j : Json) : MetaM Unit := do requireKeys j ["typeIdentifier", "typeString"] "type description" @@ -312,8 +328,11 @@ private partial def validateNode (ctx : SourceContext) (j : Json) : MetaM Unit : if kind == "BinaryOperation" then needAt ctx j ((field? j "function").all Json.isNull) "user-defined operator unsupported" if kind == "FunctionCall" then - needAt ctx j ((← str (← field j "kind")) == "functionCall" && !(← bool (← field j "tryCall")) && - (← arr (← field j "names")).isEmpty) "unsupported call surface" + let k ← str (← field j "kind") + needAt ctx j ((k == "functionCall" || k == "structConstructorCall") && + !(← bool (← field j "tryCall"))) "unsupported call surface" + if k == "functionCall" then + needAt ctx j ((← arr (← field j "names")).isEmpty) "unsupported call surface" for key in childFields do if let some value := field? j key then if key == "storageLayout" && kind == "ContractDefinition" then pure () @@ -353,8 +372,13 @@ private partial def validateNode (ctx : SourceContext) (j : Json) : MetaM Unit : for p in (← arr (← field j "parameters")) do needAt ctx j ((← nodeKind p) == "VariableDeclaration") "invalid parameter declaration" | "Block" => let _ ← arr (← field j "statements") - | "VariableDeclaration" => requireKind "typeName" ["ElementaryTypeName", "Mapping"] - | "Mapping" => requireKind "keyType" ["ElementaryTypeName"]; requireKind "valueType" ["ElementaryTypeName"] + | "VariableDeclaration" => requireKind "typeName" ["ElementaryTypeName", "Mapping", "UserDefinedTypeName"] + | "Mapping" => + let keyType ← field j "keyType" + if (← nodeKind keyType) == "UserDefinedTypeName" then + failAt ctx j "mapping with struct key" + requireKind "keyType" ["ElementaryTypeName"] + requireKind "valueType" ["ElementaryTypeName", "UserDefinedTypeName"] | "ExpressionStatement" => let _ ← field j "expression" | "Assignment" => let _ ← field j "leftHandSide"; let _ ← field j "rightHandSide" | "BinaryOperation" => let _ ← field j "leftExpression"; let _ ← field j "rightExpression" @@ -365,12 +389,48 @@ private partial def validateNode (ctx : SourceContext) (j : Json) : MetaM Unit : for d in (← arr (← field j "declarations")) do needAt ctx j ((← nodeKind d) == "VariableDeclaration") "invalid local declaration" let _ ← field j "initialValue" - | "IfStatement" => requireKind "trueBody" ["Block"] + | "IfStatement" => + let trueBody ← field j "trueBody" + let tk ← nodeKind trueBody + needAt ctx j (tk == "Block" || tk == "RevertStatement") "unexpected child kind: trueBody" | "RevertStatement" => requireKind "errorCall" ["FunctionCall"] - | "Return" => let _ ← field j "expression" + | "Return" => + if let some expr := field? j "expression" then + unless expr.isNull do let _ ← field j "expression" | "ErrorDefinition" => requireKind "parameters" ["ParameterList"] + | "ModifierDefinition" => + requireKind "parameters" ["ParameterList"] + match field? j "body" with + | none => failAt ctx j "modifier missing body" + | some body => + if body.isNull then failAt ctx j "modifier missing body" + else requireKind "body" ["Block"] + | "ModifierInvocation" => + requireKind "modifierName" ["IdentifierPath"] + if let some arguments := field? j "arguments" then + unless arguments.isNull do let _ ← arr arguments + | "PlaceholderStatement" => pure () + | "StructDefinition" => + let members ← arr (← field j "members") + needAt ctx j (members.size == 2) "unsupported struct shape" + for m in members do + needAt ctx j ((← nodeKind m) == "VariableDeclaration") "invalid struct member" + let typ ← str (← field (← field m "typeDescriptions") "typeString") + unless typ == "uint256" || typ == "address" do + failAt ctx m "struct with a dynamic member" + | "UserDefinedTypeName" => requireKind "pathNode" ["IdentifierPath"] | _ => pure () +private structure StructMemberInfo where + name : String + ty : Sol.Ty + +private structure StructInfo where + id : Nat + name : String + canonicalName : String + members : List StructMemberInfo + private structure FieldInfo where id : Nat var : String @@ -378,6 +438,8 @@ private structure FieldInfo where getter : Option String slot : Nat sty : Sol.StorageTy + structId : Option Nat + memberIndex : Option Nat private structure OpaqueField where id : Nat @@ -385,6 +447,12 @@ private structure OpaqueField where slot : Nat typeLabel : String +private structure ModInfo where + id : Nat + name : String + contractId : Nat + node : Json + private structure FnInfo where id : Nat contractId : Nat @@ -398,7 +466,7 @@ private structure FnInfo where paramTys : List Sol.Ty paramIds : List (Nat × Sol.Ty × String) rets : List Sol.Ty - namedReturn : Option (Nat × String) + namedReturn : Option (Nat × Sol.Ty × String) node : Json private def FnInfo.sig (f : FnInfo) : Sol.Sig := ⟨f.paramTys.reverse, f.rets⟩ @@ -426,6 +494,8 @@ private structure Frontend where fields : List FieldInfo opaqueEntries : List OpaqueField errors : List (Nat × String) + structs : List StructInfo + modifiers : List ModInfo allFns : List FnInfo functions : List FnInfo digest : String @@ -445,19 +515,49 @@ private def identifier (ctx : SourceContext) (j : Json) : MetaM String := do private def typeString (j : Json) : MetaM String := field j "typeDescriptions" >>= (field · "typeString") >>= str -private def parseValueTy (ctx : SourceContext) (j : Json) : MetaM Sol.Ty := do +private def parseStructMembers (ctx : SourceContext) (node : Json) : MetaM (List StructMemberInfo) := do + let mut members : List StructMemberInfo := [] + for m in (← arr (← field node "members")) do + needAt ctx m (!(← bool (← field m "stateVariable")) && + !(← bool (← field m "constant")) && + (← str (← field m "mutability")) == "mutable" && + (← str (← field m "storageLocation")) == "default") "unsupported struct member" + let typ ← typeString m + let ty ← match typ with + | "uint256" => pure Sol.Ty.uint + | "address" => pure Sol.Ty.addr + | _ => failAt ctx m "struct with a dynamic member" + let name ← identifier ctx m + members := members ++ [StructMemberInfo.mk name ty] + needAt ctx node (!members.isEmpty) "empty struct unsupported" + needAt ctx node (members.map (·.ty) == [.uint, .addr]) "unsupported struct shape" + pure members + +private def lookupStruct (structs : List StructInfo) (id : Nat) : Option StructInfo := + structs.find? (·.id == id) + +private def parseValueTy (ctx : SourceContext) (structs : List StructInfo) (j : Json) : MetaM Sol.Ty := do let typ ← typeString j match typ with | "uint256" => pure .uint | "address" => pure .addr - | _ => failAt ctx j "unsupported value type" - -private def parseFnInfo (ctx : SourceContext) (contractId : Nat) (contractName : String) + | _ => + if typ.startsWith "struct " then + let some typeName := field? j "typeName" | failAt ctx j "unsupported value type" + needAt ctx j ((← nodeKind typeName) == "UserDefinedTypeName") "unsupported value type" + let rid ← int (← field typeName "referencedDeclaration") + needAt ctx j (rid >= 0) "unresolved struct" + let some info := lookupStruct structs rid.toNat | failAt ctx j "using an undeclared struct" + needAt ctx j (info.members.map (·.ty) == [.uint, .addr]) "unsupported struct shape" + pure (.pair info.id) + else failAt ctx j "unsupported value type" + +private def parseFnInfo (ctx : SourceContext) (structs : List StructInfo) + (contractId : Nat) (contractName : String) (isTarget : Bool) (node : Json) : MetaM FnInfo := do let name ← identifier ctx node let mutability ← str (← field node "stateMutability") needAt ctx node ((← str (← field node "kind")) == "function" && - (← arr (← field node "modifiers")).isEmpty && ["internal", "public", "external", "private"].contains (← str (← field node "visibility")) && ["nonpayable", "view", "pure"].contains mutability) "unsupported function surface" @@ -470,33 +570,42 @@ private def parseFnInfo (ctx : SourceContext) (contractId : Nat) (contractName : let mut paramTys : List Sol.Ty := [] let mut paramIds : List (Nat × Sol.Ty × String) := [] for p in (← arr (← field (← field node "parameters") "parameters")) do + let loc ← str (← field p "storageLocation") needAt ctx node (!(← bool (← field p "stateVariable")) && !(← bool (← field p "constant")) && (← str (← field p "mutability")) == "mutable" && - (← str (← field p "storageLocation")) == "default" && + (loc == "default" || loc == "memory") && (← str (← field p "visibility")) == "internal" && (field? p "value").all Json.isNull) "unsupported parameter declaration" - let ty ← parseValueTy ctx p + let ty ← parseValueTy ctx structs p + match ty with + | .pair _ => needAt ctx p (loc == "memory") "unsupported parameter declaration" + | _ => needAt ctx p (loc == "default") "unsupported parameter declaration" let pname ← identifier ctx p paramTys := paramTys ++ [ty] paramIds := paramIds ++ [(← nodeId p, ty, pname)] let rs ← arr (← field (← field node "returnParameters") "parameters") needAt ctx node (rs.size <= 1) "unsupported signature" let mut rets : List Sol.Ty := [] - let mut namedReturn : Option (Nat × String) := none + let mut namedReturn : Option (Nat × Sol.Ty × String) := none for r in rs do + let loc ← str (← field r "storageLocation") needAt ctx node (!(← bool (← field r "stateVariable")) && !(← bool (← field r "constant")) && (← str (← field r "mutability")) == "mutable" && - (← str (← field r "storageLocation")) == "default" && + (loc == "default" || loc == "memory") && (← str (← field r "visibility")) == "internal" && (field? r "value").all Json.isNull) "unsupported parameter declaration" - needAt ctx node ((← typeString r) == "uint256") "unsupported return type" - rets := [.uint] + let ty ← parseValueTy ctx structs r + match ty with + | .pair _ => needAt ctx r (loc == "memory") "unsupported return type" + | .uint => needAt ctx r (loc == "default") "unsupported return type" + | .addr => needAt ctx r (loc == "default") "unsupported return type" + rets := [ty] let rname ← str (← field r "name") if !rname.isEmpty then needAt ctx node (validName rname) "unsupported/reserved name" - namedReturn := some (← nodeId r, rname) + namedReturn := some (← nodeId r, ty, rname) pure { id := ← nodeId node, contractId, contractName, name, visibility := ← str (← field node "visibility"), @@ -543,6 +652,8 @@ private def parseCompilerOutput (sourcePath : System.FilePath) (logicalPath : St (← str literals[1]!) == "^" && (← str literals[2]!) == "0.8" && (← str literals[3]!) == ".33") "unsupported pragma" | "ContractDefinition" => contracts := contracts ++ [node] + | "StructDefinition" => pure () + | "ErrorDefinition" => pure () | _ => failAt ctx node "unsupported source declaration" needAt ctx ast (!contracts.isEmpty) "exactly one concrete contract required" let mut concrete : List Json := [] @@ -607,7 +718,32 @@ private def parseCompilerOutput (sourcePath : System.FilePath) (logicalPath : St let mut fields : List FieldInfo := [] let mut opaqueEntries : List OpaqueField := [] let mut errors : List (Nat × String) := [] + let mut structs : List StructInfo := [] + let mut modifiers : List ModInfo := [] let mut allFns : List FnInfo := [] + for node in (← arr (← field ast "nodes")) do + if (← nodeKind node) == "StructDefinition" then + let members ← parseStructMembers ctx node + structs := structs ++ [{ + id := ← nodeId node + name := ← identifier ctx node + canonicalName := ← str (← field node "canonicalName") + members }] + else if (← nodeKind node) == "ErrorDefinition" then + let ps ← arr (← field (← field node "parameters") "parameters") + needAt ctx node ps.isEmpty "only zero-argument custom errors" + errors := errors ++ [((← nodeId node), (← identifier ctx node))] + for cid in linearization do + let some (_, _, cnode) := contractById.find? (·.1 == cid) + | failAt ctx target "invalid contract linearization" + for node in (← arr (← field cnode "nodes")) do + if (← nodeKind node) == "StructDefinition" then + let members ← parseStructMembers ctx node + structs := structs ++ [{ + id := ← nodeId node + name := ← identifier ctx node + canonicalName := ← str (← field node "canonicalName") + members }] for cid in linearization do let some (_, cname, cnode) := contractById.find? (·.1 == cid) | failAt ctx target "invalid contract linearization" @@ -633,8 +769,8 @@ private def parseCompilerOutput (sourcePath : System.FilePath) (logicalPath : St let layoutType ← field layoutTypes typeId let slotText ← str (← field entry "slot") let some slot := slotText.toNat? | failAt ctx node "invalid storage slot" + let name ← identifier ctx node if typ == "uint256" || typ == "mapping(address => uint256)" || typ == "address" then - let name ← identifier ctx node let sty : Sol.StorageTy := if typ == "mapping(address => uint256)" then .mapping else if typ == "address" then .addr else .scalar @@ -666,7 +802,26 @@ private def parseCompilerOutput (sourcePath : System.FilePath) (logicalPath : St (← str (← field valueType "numberOfBytes")) == "32") "bad mapping layout" let vis ← str (← field node "visibility") let getter := if vis == "public" then some name else none - fields := fields ++ [FieldInfo.mk id name (name ++ "Slot") getter slot sty] + fields := fields ++ [FieldInfo.mk id name (name ++ "Slot") getter slot sty none none] + else if typ.startsWith "struct " then + let some typeName := field? node "typeName" | failAt ctx node "unsupported value type" + needAt ctx node ((← nodeKind typeName) == "UserDefinedTypeName") "unsupported value type" + let rid ← int (← field typeName "referencedDeclaration") + needAt ctx node (rid >= 0) "unresolved struct" + let some info := lookupStruct structs rid.toNat | failAt ctx node "using an undeclared struct" + requireKeys layoutType ["encoding", "label", "members", "numberOfBytes"] "storage type" + needAt ctx node ((← str (← field layoutType "encoding")) == "inplace") "bad scalar layout" + let vis ← str (← field node "visibility") + let mut i : Nat := 0 + for mem in info.members do + let sty : Sol.StorageTy := match mem.ty with + | .uint => .scalar + | .addr => .addr + | .pair _ => .scalar + let mname := name ++ "_" ++ mem.name + let getter := if vis == "public" && i == 0 then some name else none + fields := fields ++ [FieldInfo.mk id mname (mname ++ "Slot") getter (slot + i) sty (some info.id) (some i)] + i := i + 1 else let vis ← str (← field node "visibility") needAt ctx node (vis != "public") "opaque public getter unsupported" @@ -678,11 +833,20 @@ private def parseCompilerOutput (sourcePath : System.FilePath) (logicalPath : St errors := errors ++ [((← nodeId node), (← identifier ctx node))] | "FunctionDefinition" => needAt ctx node ((← nat (← field node "scope")) == cid) "function scope mismatch" - allFns := allFns ++ [← parseFnInfo ctx cid cname (cid == targetId) node] + allFns := allFns ++ [← parseFnInfo ctx structs cid cname (cid == targetId) node] + | "ModifierDefinition" => + needAt ctx node (!(← bool (← field node "virtual"))) "unsupported modifier" + let ps ← arr (← field (← field node "parameters") "parameters") + needAt ctx node ps.isEmpty "modifier arguments" + let mname ← identifier ctx node + if modifiers.any (·.name == mname) then failAt ctx node "unsupported/reserved name" + modifiers := modifiers ++ [{ id := ← nodeId node, name := mname, contractId := cid, node }] + | "StructDefinition" => pure () | _ => failAt ctx node "unsupported contract declaration" - needAt ctx target (storage.size == fields.length + opaqueEntries.length && - storage.all fun e => (field? e "astId").bind (·.getNat?.toOption) |>.any fun id => - fields.any (·.id == id) || opaqueEntries.any (·.id == id)) "unaccounted layout field" + let accounted := storage.all fun e => + (field? e "astId").bind (·.getNat?.toOption) |>.any fun id => + fields.any (·.id == id) || opaqueEntries.any (·.id == id) + needAt ctx target accounted "unaccounted layout field" let names := fields.flatMap fun f => f.name :: f.getter.toList needAt ctx target (names.length == names.eraseDups.length) "storage/generated name collision" let slots := (fields.map (·.slot)) ++ (opaqueEntries.map (·.slot)) @@ -702,7 +866,7 @@ private def parseCompilerOutput (sourcePath : System.FilePath) (logicalPath : St let digest := sha256Hex (sourceText ++ outputText ++ importerText ++ solcVersionPin).toUTF8 pure { source := ctx, ast, targetName, targetId, linearization, contractById, - fields, opaqueEntries, errors, allFns, functions, digest + fields, opaqueEntries, errors, structs, modifiers, allFns, functions, digest } private def uint := mkConst ``Verity.Core.Uint256 @@ -725,24 +889,53 @@ private def register (name : Name) (value : Expr) (type? : Option Expr := none) private def requireType (frontend : Frontend) (j : Json) (expected : String) : MetaM Unit := do let actual ← typeString j - let identifier ← str (← field (← field j "typeDescriptions") "typeIdentifier") - let expectedIdentifier := match expected with - | "uint256" => "t_uint256" - | "address" => "t_address" - | "mapping(address => uint256)" => "t_mapping$_t_address_$_t_uint256_$" - | "msg" => "t_magic_message" - | "bool" => "t_bool" - | "tuple()" => "t_tuple$__$" - | _ => "" - needAt frontend.source j (actual == expected && identifier == expectedIdentifier) ("expected " ++ expected) + if expected.startsWith "struct " then + needAt frontend.source j (actual == expected || actual == expected ++ " memory" || + actual == expected ++ " storage ref") ("expected " ++ expected) + else + let identifier ← str (← field (← field j "typeDescriptions") "typeIdentifier") + let expectedIdentifier := match expected with + | "uint256" => "t_uint256" + | "address" => "t_address" + | "mapping(address => uint256)" => "t_mapping$_t_address_$_t_uint256_$" + | "msg" => "t_magic_message" + | "bool" => "t_bool" + | "tuple()" => "t_tuple$__$" + | _ => "" + needAt frontend.source j (actual == expected && identifier == expectedIdentifier) ("expected " ++ expected) + +private def requireUintish (frontend : Frontend) (j : Json) : MetaM Unit := do + let actual ← typeString j + if actual.startsWith "int_const " then pure () + else requireType frontend j "uint256" private def valueType : Sol.Ty → Expr | .uint => uint | .addr => address + | .pair _ => mkConst ``Sol.Pair private def typeName : Sol.Ty → String | .uint => "uint256" | .addr => "address" + | .pair _ => "struct" + +private def pairTypeNameOf (info : StructInfo) : String := + "struct " ++ info.canonicalName + +private def pairTypeName (frontend : Frontend) (id : Nat) : Option String := + (lookupStruct frontend.structs id).map pairTypeNameOf + +private def isPairTypeString (frontend : Frontend) (typ : String) : Bool := + frontend.structs.any (fun s => + s.members.map (·.ty) == [.uint, .addr] && + (typ == pairTypeNameOf s || typ == pairTypeNameOf s ++ " memory" || + typ == pairTypeNameOf s ++ " storage ref")) + +private def lookupStructByTypeString (frontend : Frontend) (typ : String) : Option StructInfo := + frontend.structs.find? (fun s => + s.members.map (·.ty) == [.uint, .addr] && + (typ == pairTypeNameOf s || typ == pairTypeNameOf s ++ " memory" || + typ == pairTypeNameOf s ++ " storage ref")) private def resultType : List Sol.Ty → Expr | [] => mkConst ``Unit @@ -758,11 +951,18 @@ where | [], _ => none | f :: fs, i => if f.id == id then some i else go fs (i + 1) +private def fieldIndexAt (fields : List FieldInfo) (pos : Nat) : Option Nat := + if pos < fields.length then some pos else none + +private def svarAt (frontend : Frontend) (L : Sol.Layout) (pos : Nat) (s : Sol.StorageTy) + (j : Json) : MetaM (Sol.SVar L s) := do + let some entry := Sol.SVar.ofIndex L pos | failAt frontend.source j "unresolved declaration id" + if h : entry.1 = s then pure (h ▸ entry.2) else failAt frontend.source j "storage type mismatch" + private def svar (frontend : Frontend) (L : Sol.Layout) (id : Nat) (s : Sol.StorageTy) (j : Json) : MetaM (Sol.SVar L s) := do let some i := fieldIndex frontend.fields id | failAt frontend.source j "unresolved declaration id" - let some entry := Sol.SVar.ofIndex L i | failAt frontend.source j "unresolved declaration id" - if h : entry.1 = s then pure (h ▸ entry.2) else failAt frontend.source j "storage type mismatch" + svarAt frontend L i s j private structure Scope (Γ : Sol.Ctx) where vars : List (Nat × Σ t, Sol.Var Γ t) @@ -829,7 +1029,8 @@ private def lookupFn (frontend : Frontend) (id : Nat) : Option FnInfo := private def isErrorRef (frontend : Frontend) (id : Nat) : Bool := frontend.errors.any (·.1 == id) -private def resolveCall (frontend : Frontend) (current : FnInfo) (call : Json) : MetaM FnInfo := do +private def resolveCall (frontend : Frontend) (_current : FnInfo) (definingId : Nat) + (call : Json) : MetaM FnInfo := do let callee ← field call "expression" match ← nodeKind callee with | "Identifier" => @@ -840,9 +1041,12 @@ private def resolveCall (frontend : Frontend) (current : FnInfo) (call : Json) : let some static := lookupFn frontend id | failAt frontend.source call "unresolved function reference" needAt frontend.source call ((familyOf frontend static.name static.paramTys).any (·.id == id)) "virtual dispatch disagrees with AST" - let some resolved := mostDerived frontend static.name static.paramTys - | failAt frontend.source call "unimplemented virtual" - pure resolved + if static.visibility == "private" || !static.virtual then + pure static + else + let some resolved := mostDerived frontend static.name static.paramTys + | failAt frontend.source call "unimplemented virtual" + pure resolved | "MemberAccess" => let base ← field callee "expression" needAt frontend.source callee ((← nodeKind base) == "Identifier" && @@ -861,44 +1065,81 @@ private def resolveCall (frontend : Frontend) (current : FnInfo) (call : Json) : needAt frontend.source callee ((familyOf frontend static.name static.paramTys).any (·.id == rid.toNat)) "super dispatch family mismatch" - let some resolved := superTarget frontend current.contractId static.name static.paramTys + let some resolved := superTarget frontend definingId static.name static.paramTys | failAt frontend.source call "unresolved super target" pure resolved | _ => failAt frontend.source call "unsupported call surface" -private partial def collectCallIds (frontend : Frontend) (current : FnInfo) (j : Json) : - MetaM (List Nat) := do +private partial def collectCallIds (frontend : Frontend) (current : FnInfo) (definingId : Nat) + (j : Json) : MetaM (List Nat) := do match j with | .obj o => let walkChildren : MetaM (List Nat) := do - let rest ← o.toList.mapM fun (_, v) => collectCallIds frontend current v + let rest ← o.toList.mapM fun (_, v) => collectCallIds frontend current definingId v pure rest.flatten match field? j "nodeType" with | some nt => if (← str nt) == "FunctionCall" then - let callee ← field j "expression" - let skip ← match ← nodeKind callee with - | "Identifier" => - let rid ← int (← field callee "referencedDeclaration") - pure (rid >= 0 && isErrorRef frontend rid.toNat) - | _ => pure false - let restIds ← walkChildren - if skip then pure restIds - else - let resolved ← resolveCall frontend current j - pure (resolved.id :: restIds) + if (field? j "kind").bind (·.getStr?.toOption) == some "structConstructorCall" then + walkChildren + else do + let callee ← field j "expression" + let skip ← match ← nodeKind callee with + | "Identifier" => + let rid ← int (← field callee "referencedDeclaration") + pure (rid >= 0 && isErrorRef frontend rid.toNat) + | _ => pure false + let restIds ← walkChildren + if skip then pure restIds + else + let resolved ← resolveCall frontend current definingId j + pure (resolved.id :: restIds) else walkChildren | none => walkChildren | .arr xs => - let rest ← xs.toList.mapM (collectCallIds frontend current) + let rest ← xs.toList.mapM (collectCallIds frontend current definingId) pure rest.flatten | _ => pure [] +private def lookupMod (frontend : Frontend) (id : Nat) : Option ModInfo := + frontend.modifiers.find? (·.id == id) + +private partial def countPlaceholders (j : Json) : Nat := + match j with + | .obj o => + let here := if (j.getObjVal? "nodeType").toOption == some (Json.str "PlaceholderStatement") then 1 else 0 + o.foldl (fun acc _ v => acc + countPlaceholders v) here + | .arr xs => xs.foldl (fun acc v => acc + countPlaceholders v) 0 + | _ => 0 + +private def splitModifierBody (stmts : List Json) : MetaM (List Json × List Json) := do + let mut pre : List Json := [] + let mut post : List Json := [] + let mut seen := false + for s in stmts do + if (← nodeKind s) == "PlaceholderStatement" then + if seen then throwError "modifier with two placeholders" + seen := true + else if seen then post := post ++ [s] + else pre := pre ++ [s] + unless seen do throwError "modifier missing placeholder" + pure (pre, post) + +private def fnModifierInvocations (fn : FnInfo) : MetaM (Array Json) := do + arr (← field fn.node "modifiers") + private def topoSort (frontend : Frontend) : MetaM (List FnInfo) := do let mut deps : List (Nat × List Nat) := [] for f in frontend.functions do let body := field? f.node "body" |>.getD Json.null - let callees := (← collectCallIds frontend f body).eraseDups + let mut callees := (← collectCallIds frontend f f.contractId body).eraseDups + for inv in (← fnModifierInvocations f) do + let nameNode ← field inv "modifierName" + let rid ← int (← field nameNode "referencedDeclaration") + needAt frontend.source inv (rid >= 0) "unresolved modifier" + let some m := lookupMod frontend rid.toNat | failAt frontend.source inv "unresolved modifier" + let mbody := field? m.node "body" |>.getD Json.null + callees := (callees ++ (← collectCallIds frontend f m.contractId mbody)).eraseDups deps := deps ++ [(f.id, callees)] let mut remaining := frontend.functions let mut order : List FnInfo := [] @@ -921,6 +1162,7 @@ private structure ParseCtx where F : Sol.Fns registered : List FnInfo current : FnInfo + superFrom : Nat private def indexOfFn : List FnInfo → Nat → Nat → Option Nat | [], _, _ => none @@ -935,6 +1177,17 @@ private def fvarOf (ctx : ParseCtx) (resolved : FnInfo) (j : Json) : MetaM (Σ pure entry mutual +private partial def loadPair (ctx : ParseCtx) {Γ : Sol.Ctx} (id : Nat) (sid : Nat) (j : Json) : + MetaM (Sol.Expr ctx.L ctx.F Γ (.pair sid)) := do + let members := (List.range ctx.frontend.fields.length).zip ctx.frontend.fields |>.filter (fun p => p.2.id == id) + match members with + | (p0, m0) :: (p1, m1) :: [] => + needAt ctx.frontend.source j (m0.sty == .scalar && m1.sty == .addr) "storage type mismatch" + let a ← svarAt ctx.frontend ctx.L p0 .scalar j + let b ← svarAt ctx.frontend ctx.L p1 .addr j + pure (.pair (.load a) (.loadAddr b)) + | _ => failAt ctx.frontend.source j "storage type mismatch" + private partial def parseExpr (ctx : ParseCtx) {Γ : Sol.Ctx} (sc : Scope Γ) (t : Sol.Ty) (j : Json) : MetaM (Sol.Expr ctx.L ctx.F Γ t) := do match ← nodeKind j with @@ -943,8 +1196,19 @@ private partial def parseExpr (ctx : ParseCtx) {Γ : Sol.Ctx} (sc : Scope Γ) (t if rid < 0 then failAt ctx.frontend.source j "unresolved builtin identifier" let id := rid.toNat if let some v := sc.find? id then - requireType ctx.frontend j (typeName v.1) + match v.1 with + | .pair sid => + let some expected := pairTypeName ctx.frontend sid | failAt ctx.frontend.source j "unsupported value type" + requireType ctx.frontend j expected + | _ => requireType ctx.frontend j (typeName v.1) if h : v.1 = t then pure (.var (h ▸ v.2)) else failAt ctx.frontend.source j "local type mismatch" + else if ctx.frontend.fields.any (fun f => f.id == id && f.structId.isSome) then + match t with + | .pair sid => + let some expected := pairTypeName ctx.frontend sid | failAt ctx.frontend.source j "unsupported value type" + requireType ctx.frontend j expected + loadPair ctx id sid j + | _ => failAt ctx.frontend.source j "storage type mismatch" else if let some info := ctx.frontend.fields.find? (·.id == id) then match info.sty, t with | .scalar, .uint => @@ -960,15 +1224,33 @@ private partial def parseExpr (ctx : ParseCtx) {Γ : Sol.Ctx} (sc : Scope Γ) (t else failAt ctx.frontend.source j "unresolved declaration reference" | "MemberAccess" => let base ← field j "expression" - needAt ctx.frontend.source j ((← str (← field j "memberName")) == "sender" && - (← nodeKind base) == "Identifier" && (← str (← field base "name")) == "msg" && - (← int (← field base "referencedDeclaration")) == -15 && - (field? j "referencedDeclaration").all fun v => v.isNull) "only builtin msg.sender supported" - requireType ctx.frontend base "msg" - requireType ctx.frontend j "address" - match t with - | .addr => pure .sender - | .uint => failAt ctx.frontend.source j "address expression in uint256 position" + let member ← str (← field j "memberName") + if member == "sender" && (← nodeKind base) == "Identifier" && + (← str (← field base "name")) == "msg" && + (← int (← field base "referencedDeclaration")) == -15 && + (field? j "referencedDeclaration").all fun v => v.isNull then + requireType ctx.frontend base "msg" + requireType ctx.frontend j "address" + match t with + | .addr => pure .sender + | .uint => failAt ctx.frontend.source j "address expression in uint256 position" + | .pair _ => failAt ctx.frontend.source j "address expression in uint256 position" + else + unless isPairTypeString ctx.frontend (← typeString base) do + failAt ctx.frontend.source j "only builtin msg.sender supported" + let some info := lookupStructByTypeString ctx.frontend (← typeString base) + | failAt ctx.frontend.source j "using an undeclared struct" + let some idx := info.members.findIdx? (·.name == member) + | failAt ctx.frontend.source j "unresolved declaration reference" + let baseE ← parseExpr ctx sc (.pair info.id) base + match idx, t with + | 0, .uint => + requireType ctx.frontend j "uint256" + pure (.fst baseE) + | 1, .addr => + requireType ctx.frontend j "address" + pure (.snd baseE) + | _, _ => failAt ctx.frontend.source j "local type mismatch" | "IndexAccess" => let base ← field j "baseExpression" needAt ctx.frontend.source j ((← nodeKind base) == "Identifier") "unsupported index base" @@ -986,6 +1268,7 @@ private partial def parseExpr (ctx : ParseCtx) {Γ : Sol.Ctx} (sc : Scope Γ) (t match t with | .uint => pure (.index (← svar ctx.frontend ctx.L info.id .mapping j) key) | .addr => failAt ctx.frontend.source j "uint256 expression in address position" + | .pair _ => failAt ctx.frontend.source j "uint256 expression in address position" | "Literal" => let value ← str (← field j "value") let some n := value.toNat? | failAt ctx.frontend.source j "unsupported literal" @@ -995,6 +1278,7 @@ private partial def parseExpr (ctx : ParseCtx) {Γ : Sol.Ctx} (sc : Scope Γ) (t match t with | .uint => pure (.lit n) | .addr => failAt ctx.frontend.source j "uint256 expression in address position" + | .pair _ => failAt ctx.frontend.source j "uint256 expression in address position" | "BinaryOperation" => let op ← str (← field j "operator") needAt ctx.frontend.source j (op == "+" || op == "-") "unsupported binary operation/types" @@ -1008,18 +1292,77 @@ private partial def parseExpr (ctx : ParseCtx) {Γ : Sol.Ctx} (sc : Scope Γ) (t match t with | .uint => pure (.arith aop a b) | .addr => failAt ctx.frontend.source j "uint256 expression in address position" + | .pair _ => failAt ctx.frontend.source j "uint256 expression in address position" | "FunctionCall" => - requireType ctx.frontend j (typeName t) - let resolved ← resolveCall ctx.frontend ctx.current j - needAt ctx.frontend.source j resolved.viewOrPure - "effectful internal call in expression position" - needAt ctx.frontend.source j (resolved.rets == [t]) "function does not return the expected type" - let ⟨σ, fv⟩ ← fvarOf ctx resolved j - let argsJ := (← arr (← field j "arguments")).toList - let args ← parseArgs ctx sc resolved.paramTys argsJ j - if h : σ = ⟨resolved.paramTys.reverse, [t]⟩ then - pure (.call (h ▸ fv) args) - else failAt ctx.frontend.source j "function signature mismatch" + if (← str (← field j "kind")) == "structConstructorCall" then + let some info := lookupStructByTypeString ctx.frontend (← typeString j) + | failAt ctx.frontend.source j "using an undeclared struct" + needAt ctx.frontend.source j (t == .pair info.id) "unsupported value type" + requireType ctx.frontend j (pairTypeNameOf info) + let argsJ ← arr (← field j "arguments") + let names ← arr (← field j "names") + needAt ctx.frontend.source j (argsJ.size == 2) "argument count mismatch" + let amountName := + match info.members with + | m0 :: _ => m0.name + | [] => "" + let whoName := + match info.members with + | _ :: m1 :: _ => m1.name + | _ => "" + let e : Sol.Expr ctx.L ctx.F Γ (.pair info.id) ← + if names.isEmpty then + let a ← parseExpr ctx sc .uint argsJ[0]! + let b ← parseExpr ctx sc .addr argsJ[1]! + pure (.pair a b) + else do + needAt ctx.frontend.source j (names.size == 2) "argument count mismatch" + let some iAmt := names.findIdx? (fun n => n.getStr?.toOption == some amountName) + | failAt ctx.frontend.source j "unresolved declaration reference" + let some iWho := names.findIdx? (fun n => n.getStr?.toOption == some whoName) + | failAt ctx.frontend.source j "unresolved declaration reference" + needAt ctx.frontend.source j (iAmt != iWho) "unresolved declaration reference" + if iAmt == 0 && iWho == 1 then + let a ← parseExpr ctx sc .uint argsJ[0]! + let b ← parseExpr ctx sc .addr argsJ[1]! + pure (.pair a b) + else if iAmt == 1 && iWho == 0 then + let b ← parseExpr ctx sc .addr argsJ[0]! + let a ← parseExpr ctx sc .uint argsJ[1]! + pure (.pairRev b a) + else failAt ctx.frontend.source j "unresolved declaration reference" + if h : t = .pair info.id then pure (h ▸ e) else failAt ctx.frontend.source j "local type mismatch" + else do + let resolved ← resolveCall ctx.frontend ctx.current ctx.superFrom j + needAt ctx.frontend.source j resolved.viewOrPure + "effectful internal call in expression position" + needAt ctx.frontend.source j (resolved.rets == [t]) "function does not return the expected type" + let ⟨σ, fv⟩ ← fvarOf ctx resolved j + let argsJ := (← arr (← field j "arguments")).toList + let args ← parseArgs ctx sc resolved.paramTys argsJ j + if h : t = .uint then + requireType ctx.frontend j "uint256" + if hσ : σ = ⟨resolved.paramTys.reverse, [.uint]⟩ then + let e : Sol.Expr ctx.L ctx.F Γ .uint := .call (hσ ▸ fv) args + pure (h ▸ e) + else failAt ctx.frontend.source j "function signature mismatch" + else if h : t = .addr then + requireType ctx.frontend j "address" + if hσ : σ = ⟨resolved.paramTys.reverse, [.addr]⟩ then + let e : Sol.Expr ctx.L ctx.F Γ .addr := .call (hσ ▸ fv) args + pure (h ▸ e) + else failAt ctx.frontend.source j "function signature mismatch" + else + match t with + | .pair sid => + let some expected := pairTypeName ctx.frontend sid | failAt ctx.frontend.source j "unsupported value type" + requireType ctx.frontend j expected + if hσ : σ = ⟨resolved.paramTys.reverse, [.pair sid]⟩ then + let e : Sol.Expr ctx.L ctx.F Γ (.pair sid) := .call (hσ ▸ fv) args + if h : t = .pair sid then pure (h ▸ e) + else failAt ctx.frontend.source j "function signature mismatch" + else failAt ctx.frontend.source j "function signature mismatch" + | _ => failAt ctx.frontend.source j "function signature mismatch" | _ => failAt ctx.frontend.source j "unsupported expression" private partial def parseArgs (ctx : ParseCtx) {Γ : Sol.Ctx} (sc : Scope Γ) (ts : List Sol.Ty) @@ -1061,6 +1404,23 @@ private partial def parseLValue (ctx : ParseCtx) {Γ : Sol.Ctx} (sc : Scope Γ) pure (.mapping (← svar ctx.frontend ctx.L info.id .mapping j) key) | _ => failAt ctx.frontend.source j "only storage assignment supported" +private partial def assignStructMembers (ctx : ParseCtx) {Γ : Sol.Ctx} + (id : Nat) (sid : Nat) (rhs : Sol.Expr ctx.L ctx.F Γ (.pair sid)) + (rest : Sol.Stmt ctx.L ctx.F Γ r) + (j : Json) : MetaM (Sol.Stmt ctx.L ctx.F Γ r) := do + let members := (List.range ctx.frontend.fields.length).zip ctx.frontend.fields |>.filter (fun p => p.2.id == id) + match members with + | [(p0, m0), (p1, m1)] => + needAt ctx.frontend.source j (m0.sty == .scalar && m1.sty == .addr) "storage type mismatch" + let a ← svarAt ctx.frontend ctx.L p0 .scalar j + let b ← svarAt ctx.frontend ctx.L p1 .addr j + let shifted := rest.shift (.pair sid) 0 + let inner : Sol.Stmt ctx.L ctx.F ((.pair sid) :: Γ) r := + .assign (.scalar a) .set (.fst (.var .here)) + (.assignAddr b (.snd (.var .here)) shifted) + pure (.local_ rhs inner) + | _ => failAt ctx.frontend.source j "storage type mismatch" + private partial def parseStmts (ctx : ParseCtx) {Γ : Sol.Ctx} (sc : Scope Γ) (r : Sol.Ret) (namedReturn : Option Nat) (nodes : List Json) : MetaM (Sol.Stmt ctx.L ctx.F Γ r) := do match nodes with @@ -1077,6 +1437,7 @@ private partial def parseStmts (ctx : ParseCtx) {Γ : Sol.Ctx} (sc : Scope Γ) ( | _ => throwError "missing terminal return" | node :: rest => match ← nodeKind node with + | "PlaceholderStatement" => failAt ctx.frontend.source node "modifier with two placeholders" | "ExpressionStatement" => let expr ← field node "expression" match ← nodeKind expr with @@ -1088,6 +1449,13 @@ private partial def parseStmts (ctx : ParseCtx) {Γ : Sol.Ctx} (sc : Scope Γ) ( if rid >= 0 && ctx.frontend.opaqueEntries.any (·.id == rid.toNat) then failAt ctx.frontend.source node "opaque field" if rid >= 0 then + if ctx.frontend.fields.any (fun f => f.id == rid.toNat && f.structId.isSome) then + needAt ctx.frontend.source expr (op == "=") "unsupported assignment" + let some info := lookupStructByTypeString ctx.frontend (← typeString lhs) + | failAt ctx.frontend.source expr "using an undeclared struct" + let rhs ← parseExpr ctx sc (.pair info.id) (← field expr "rightHandSide") + let restS ← parseStmts ctx sc r namedReturn rest + return (← assignStructMembers ctx rid.toNat info.id rhs restS lhs) if let some info := ctx.frontend.fields.find? (·.id == rid.toNat) then if info.sty == .addr then needAt ctx.frontend.source expr (op == "=") "unsupported assignment" @@ -1103,7 +1471,7 @@ private partial def parseStmts (ctx : ParseCtx) {Γ : Sol.Ctx} (sc : Scope Γ) ( pure (.assign lv aop rhs (← parseStmts ctx sc r namedReturn rest)) | "FunctionCall" => requireType ctx.frontend expr "tuple()" - let resolved ← resolveCall ctx.frontend ctx.current expr + let resolved ← resolveCall ctx.frontend ctx.current ctx.superFrom expr needAt ctx.frontend.source expr resolved.rets.isEmpty "function does not return the expected type" let ⟨σ, fv⟩ ← fvarOf ctx resolved expr let argsJ := (← arr (← field expr "arguments")).toList @@ -1130,10 +1498,16 @@ private partial def parseStmts (ctx : ParseCtx) {Γ : Sol.Ctx} (sc : Scope Γ) ( | "IfStatement" => let falseBody := field? node "falseBody" let trueBody ← field node "trueBody" - let statements ← arr (← field trueBody "statements") - needAt ctx.frontend.source node (falseBody.all Json.isNull && statements.size == 1 && - (← nodeKind statements[0]!) == "RevertStatement") "only if/revert guard supported" - let call ← field statements[0]! "errorCall" + let revertNode ← match ← nodeKind trueBody with + | "Block" => + let statements ← arr (← field trueBody "statements") + needAt ctx.frontend.source node (statements.size == 1 && + (← nodeKind statements[0]!) == "RevertStatement") "only if/revert guard supported" + pure statements[0]! + | "RevertStatement" => pure trueBody + | _ => failAt ctx.frontend.source node "only if/revert guard supported" + needAt ctx.frontend.source node (falseBody.all Json.isNull) "only if/revert guard supported" + let call ← field revertNode "errorCall" let callee ← field call "expression" let rid ← int (← field callee "referencedDeclaration") let some errorName := if rid < 0 then none else ctx.frontend.errors.lookup rid.toNat @@ -1141,24 +1515,43 @@ private partial def parseStmts (ctx : ParseCtx) {Γ : Sol.Ctx} (sc : Scope Γ) ( needAt ctx.frontend.source node ((← nodeKind callee) == "Identifier" && (← arr (← field call "arguments")).isEmpty) "unsupported revert" let condition ← field node "condition" - needAt ctx.frontend.source condition ((← nodeKind condition) == "BinaryOperation" && - (← str (← field condition "operator")) == "<") "only uint256 comparison guard supported" + needAt ctx.frontend.source condition ((← nodeKind condition) == "BinaryOperation") + "only uint256 comparison guard supported" requireType ctx.frontend condition "bool" - let commonType ← field condition "commonType" - needAt ctx.frontend.source condition ((← str (← field commonType "typeString")) == "uint256" && - (← str (← field commonType "typeIdentifier")) == "t_uint256") "unsupported comparison type" + let op ← str (← field condition "operator") let left ← field condition "leftExpression" let right ← field condition "rightExpression" - requireType ctx.frontend left "uint256"; requireType ctx.frontend right "uint256" - let a ← parseExpr ctx sc .uint left - let b ← parseExpr ctx sc .uint right - pure (.guard a b (errorName ++ "()") (← parseStmts ctx sc r namedReturn rest)) + if op == "<" then + let commonType ← field condition "commonType" + needAt ctx.frontend.source condition ((← str (← field commonType "typeString")) == "uint256" && + (← str (← field commonType "typeIdentifier")) == "t_uint256") "unsupported comparison type" + requireUintish ctx.frontend left; requireUintish ctx.frontend right + let a ← parseExpr ctx sc .uint left + let b ← parseExpr ctx sc .uint right + pure (.guard a b (errorName ++ "()") (← parseStmts ctx sc r namedReturn rest)) + else if op == "!=" then + let commonType ← field condition "commonType" + needAt ctx.frontend.source condition ((← str (← field commonType "typeString")) == "address") + "unsupported comparison type" + requireType ctx.frontend left "address"; requireType ctx.frontend right "address" + let a ← parseExpr ctx sc .addr left + let b ← parseExpr ctx sc .addr right + pure (.guardAddrNe a b (errorName ++ "()") (← parseStmts ctx sc r namedReturn rest)) + else failAt ctx.frontend.source condition "only uint256 comparison guard supported" | "Return" => + needAt ctx.frontend.source node rest.isEmpty "only terminal scalar return" match r with | [t] => - needAt ctx.frontend.source node rest.isEmpty "only terminal scalar return" - let e ← parseExpr ctx sc t (← field node "expression") - pure (.ret e) + match field? node "expression" with + | some expr => + needAt ctx.frontend.source node (!expr.isNull) "only terminal scalar return" + let e ← parseExpr ctx sc t expr + pure (.ret e) + | none => failAt ctx.frontend.source node "only terminal scalar return" + | [] => + needAt ctx.frontend.source node ((field? node "expression").all fun e => e.isNull) + "only terminal scalar return" + pure .done | _ => failAt ctx.frontend.source node "only terminal scalar return" | _ => failAt ctx.frontend.source node "unsupported statement" end @@ -1229,6 +1622,69 @@ private def fnsTerm : (handles : List (Sol.Sig × Expr)) → MetaM Expr -- `FnEnv.cons` implicits are `{F : Fns}` then `{σ : Sig}`. pure (mkAppN (mkConst ``Sol.FnEnv.cons) #[toExpr tail, toExpr σ, apply, restE]) +private partial def wrapModifierParts (ctx : ParseCtx) {Γ : Sol.Ctx} (sc : Scope Γ) + (pre post : List Json) (inner : Sol.Stmt ctx.L ctx.F Γ r) : + MetaM (Sol.Stmt ctx.L ctx.F Γ r) := do + match pre with + | [] => + let postS ← parseStmts ctx sc [] none post + pure (.block inner postS) + | node :: restPre => + if (← nodeKind node) == "Return" then + failAt ctx.frontend.source node "modifier prelude return skips function body" + if (← nodeKind node) == "VariableDeclarationStatement" then + let declarations ← arr (← field node "declarations") + needAt ctx.frontend.source node (declarations.size == 1) "unsupported locals" + let declaration := declarations[0]! + needAt ctx.frontend.source declaration (!(← bool (← field declaration "stateVariable")) && + !(← bool (← field declaration "constant")) && + (← str (← field declaration "mutability")) == "mutable" && + (← str (← field declaration "storageLocation")) == "default" && + (← str (← field declaration "visibility")) == "internal") "unsupported local declaration" + requireType ctx.frontend declaration "uint256" + let id ← nodeId declaration + let _ ← identifier ctx.frontend.source declaration + let value ← parseExpr ctx sc .uint (← field node "initialValue") + let rest ← wrapModifierParts ctx (sc.push id .uint) restPre post (inner.shift .uint 0) + pure (.local_ value rest) + else + let head ← parseStmts ctx sc [] none [node] + let rest ← wrapModifierParts ctx sc restPre post inner + pure (.seq head rest) + +private def wrapModifiers (ctx : ParseCtx) {Γ : Sol.Ctx} (sc : Scope Γ) + (invs : List Json) (body : Sol.Stmt ctx.L ctx.F Γ r) : + MetaM (Sol.Stmt ctx.L ctx.F Γ r) := do + match invs with + | [] => pure body + | inv :: rest => + needAt ctx.frontend.source inv ((← str (← field inv "kind")) == "modifierInvocation") + "unsupported modifier" + if let some args := field? inv "arguments" then + unless args.isNull do + needAt ctx.frontend.source inv ((← arr args).isEmpty) "modifier arguments" + let nameNode ← field inv "modifierName" + let rid ← int (← field nameNode "referencedDeclaration") + needAt ctx.frontend.source inv (rid >= 0) "unresolved modifier" + let some m := lookupMod ctx.frontend rid.toNat | failAt ctx.frontend.source inv "unresolved modifier" + let mbody := field? m.node "body" |>.getD Json.null + let nph := countPlaceholders mbody + if nph > 1 then failAt ctx.frontend.source m.node "modifier with two placeholders" + if nph == 0 then failAt ctx.frontend.source m.node "modifier missing placeholder" + let stmts := (field? mbody "statements").bind (·.getArr?.toOption) |>.getD #[] + let (pre, post) ← splitModifierBody stmts.toList + let inner ← wrapModifiers ctx sc rest body + for s in pre do + if (← nodeKind s) == "Return" then + failAt ctx.frontend.source s "modifier prelude return skips function body" + let mctx := { ctx with superFrom := m.contractId } + if ← pre.anyM fun s => (· == "VariableDeclarationStatement") <$> nodeKind s then + wrapModifierParts mctx sc pre post inner + else + let preS ← parseStmts mctx sc [] none pre + let postS ← parseStmts mctx sc [] none post + pure (.seq preS (.block inner postS)) + private def parseBody (ctx : ParseCtx) (fn : FnInfo) : MetaM Expr := do let Γ : Sol.Ctx := fn.paramIds.reverse.map fun p => p.2.1 let sc0 := scopeOf fn.paramIds Γ @@ -1236,15 +1692,23 @@ private def parseBody (ctx : ParseCtx) (fn : FnInfo) : MetaM Expr := do match field? fn.node "body" with | some body => (field? body "statements").bind (·.getArr?.toOption) |>.getD #[] | none => #[] + let invs := (← fnModifierInvocations fn).toList match fn.namedReturn with - | some (id, _) => - let sc := sc0.push id .uint + | some (id, ty, _) => + let sc := sc0.push id ty + let defaultE : Sol.Expr ctx.L ctx.F Γ ty := + match ty with + | .uint => .lit 0 + | .addr => .zero + | .pair _ => .pair (.lit 0) .zero let inner ← parseStmts ctx sc fn.rets (some id) statements.toList - let wrapped : Sol.Stmt ctx.L ctx.F Γ fn.rets := .local_ (.lit 0) inner - pure (toExpr wrapped) + let wrapped : Sol.Stmt ctx.L ctx.F Γ fn.rets := .local_ defaultE inner + let withMods ← wrapModifiers ctx sc0 invs wrapped + pure (toExpr withMods) | none => let body ← parseStmts ctx sc0 fn.rets none statements.toList - pure (toExpr body) + let withMods ← wrapModifiers ctx sc0 invs body + pure (toExpr withMods) private def importFrontend (ns : Name) (frontend : Frontend) : MetaM Unit := do let L := layoutOf frontend.fields @@ -1285,28 +1749,46 @@ private def importFrontend (ns : Name) (frontend : Frontend) : MetaM Unit := do for h in registered do if let some getter := h.1.getter then let gname := ns ++ Name.mkSimple getter - match h.1.sty with - | .mapping => - let value ← withLocalDeclD `account address fun account => do - let getterFn ← mkAppM ``Verity.getMapping #[h.2, account] - mkLambdaFVars #[account] (← mkAppM ``Sol.nonpayable #[getterFn]) - register gname value - getterEntries := getterEntries.push (gname, [(`account, address)]) - | .addr => - let value ← mkAppM ``Sol.nonpayable #[← mkAppM ``Verity.getStorageAddr #[h.2]] - register gname value - getterEntries := getterEntries.push (gname, []) - | .scalar => - let value ← mkAppM ``Sol.nonpayable #[← mkAppM ``Verity.getStorage #[h.2]] + match h.1.structId, h.1.memberIndex with + | some _, some 0 => + let members := registered.filter (fun g => g.1.id == h.1.id && g.1.structId.isSome) + needAt frontend.source frontend.ast (members.length == 2) "storage type mismatch" + let some amountH := members.find? (fun g => g.1.memberIndex == some 0) + | throwError "unresolved struct getter" + let some whoH := members.find? (fun g => g.1.memberIndex == some 1) + | throwError "unresolved struct getter" + let amount ← mkAppM ``Verity.getStorage #[amountH.2] + let who ← mkAppM ``Verity.getStorageAddr #[whoH.2] + let value ← mkAppM ``Sol.nonpayable + #[← mkAppM ``Verity.bind #[amount, ← withLocalDeclD `x uint fun x => do + mkLambdaFVars #[x] (← mkAppM ``Verity.bind #[who, ← withLocalDeclD `y address fun y => do + mkLambdaFVars #[y] (← mkAppM ``Verity.pure #[← mkAppM ``Prod.mk #[x, y]])])]] register gname value getterEntries := getterEntries.push (gname, []) + | some _, some _ => pure () + | _, _ => + match h.1.sty with + | .mapping => + let value ← withLocalDeclD `account address fun account => do + let getterFn ← mkAppM ``Verity.getMapping #[h.2, account] + mkLambdaFVars #[account] (← mkAppM ``Sol.nonpayable #[getterFn]) + register gname value + getterEntries := getterEntries.push (gname, [(`account, address)]) + | .addr => + let value ← mkAppM ``Sol.nonpayable #[← mkAppM ``Verity.getStorageAddr #[h.2]] + register gname value + getterEntries := getterEntries.push (gname, []) + | .scalar => + let value ← mkAppM ``Sol.nonpayable #[← mkAppM ``Verity.getStorage #[h.2]] + register gname value + getterEntries := getterEntries.push (gname, []) let mut fnHandles : List (Sol.Sig × Expr) := [] let mut fnInfos : List FnInfo := [] let mut functionEntries : Array (Name × List (Name × Expr)) := #[] for fn in order do let F : Sol.Fns := fnHandles.map (·.1) let fnsE ← fnsTerm fnHandles - let ctx : ParseCtx := { frontend, L, F, registered := fnInfos, current := fn } + let ctx : ParseCtx := { frontend, L, F, registered := fnInfos, current := fn, superFrom := fn.contractId } let Γ : Sol.Ctx := fn.paramIds.reverse.map fun p => p.2.1 let bodyE ← parseBody ctx fn let meaningHead := diff --git a/Contracts/VaultFromSolidity/Importer/Semantics.lean b/Contracts/VaultFromSolidity/Importer/Semantics.lean index 43a0dcee5a..97229b4878 100644 --- a/Contracts/VaultFromSolidity/Importer/Semantics.lean +++ b/Contracts/VaultFromSolidity/Importer/Semantics.lean @@ -13,6 +13,11 @@ `Stmt.callStmt`. Pinned solc 0.8.x legacy codegen (`viaIR=false`) evaluates an effectful call before the other operand / `+=` old-read, so modelling those calls as left-to-right `Expr.call` would disagree with bytecode. + + Function modifiers are inlined at parse time; this file never sees `_`. + `Stmt.block inner post` runs `inner` and then `post`, so a function `return` + exits the block only and postludes still run. A revert anywhere aborts the + whole call. -/ import Contracts.VaultFromSolidity.Importer.Syntax @@ -23,10 +28,16 @@ namespace SolidityImporter.Sol open Lean -/-- `uint256` denotes Verity's `Uint256`, `address` its `Address`. -/ +/-- Two-member user struct as a product. Shared with the importer's Lean binder +type so `Env.cons` sees the same type as `Ty.pair.denote`. -/ +abbrev Pair := Verity.Core.Uint256 × Verity.Core.Address + +/-- `uint256` denotes Verity's `Uint256`, `address` its `Address`, two-member +user structs their product (the solc id is erased at denote). -/ @[reducible] def Ty.denote : Ty → Type | .uint => Verity.Core.Uint256 | .addr => Verity.Core.Address + | .pair _ => Pair /-- A function body returns nothing, one value, or (later) a tuple. -/ @[reducible] def Ret.denote : Ret → Type @@ -107,6 +118,7 @@ def Expr.meaning {L : Layout} {F : Fns} {Γ : Ctx} {t : Ty} match e with | .var v => Verity.pure (Env.get env v) | .sender => Verity.msgSender + | .zero => Verity.pure Verity.zeroAddress | .lit n => Verity.pure (Verity.Core.Uint256.ofNat n) | .load s => Verity.getStorage (Slots.get slots s) | .loadAddr s => Verity.getStorageAddr (Slots.get slots s) @@ -116,6 +128,16 @@ def Expr.meaning {L : Layout} {F : Fns} {Γ : Ctx} {t : Ty} | .arith op a b => Verity.bind (Expr.meaning a slots fns env) (fun x => Verity.bind (Expr.meaning b slots fns env) (fun y => checked op x y)) + | .pair a b => + Verity.bind (Expr.meaning a slots fns env) (fun x => + Verity.bind (Expr.meaning b slots fns env) (fun y => Verity.pure (x, y))) + | .pairRev a b => + Verity.bind (Expr.meaning a slots fns env) (fun y => + Verity.bind (Expr.meaning b slots fns env) (fun x => Verity.pure (x, y))) + | .fst e => + Verity.bind (Expr.meaning e slots fns env) (fun vs => Verity.pure vs.1) + | .snd e => + Verity.bind (Expr.meaning e slots fns env) (fun vs => Verity.pure vs.2) | .call fvar args => Verity.bind (Args.eval args slots fns env) (fun vals => FnEnv.get fns fvar (envOfVals vals)) @@ -177,10 +199,21 @@ def Stmt.meaning {L : Layout} {F : Fns} {Γ : Ctx} {r : Ret} Verity.bind (Expr.meaning b slots fns env) (fun y => Verity.bind (Verity.require (Nat.ble y.val x.val) msg) (fun _ => Stmt.meaning rest slots fns env))) + | .guardAddrNe a b msg rest => + Verity.bind (Expr.meaning a slots fns env) (fun x => + Verity.bind (Expr.meaning b slots fns env) (fun y => + Verity.bind (Verity.require (decide (x = y)) msg) + (fun _ => Stmt.meaning rest slots fns env))) | .callStmt fvar args rest => Verity.bind (Args.eval args slots fns env) (fun vals => Verity.bind (FnEnv.get fns fvar (envOfVals vals)) (fun _ => Stmt.meaning rest slots fns env)) + | .seq pre rest => + Verity.bind (Stmt.meaning pre slots fns env) (fun _ => + Stmt.meaning rest slots fns env) + | .block inner post => + Verity.bind (Stmt.meaning inner slots fns env) (fun v => + Verity.bind (Stmt.meaning post slots fns env) (fun _ => Verity.pure v)) end /-- Every imported entry point is non-payable. Internal calls do not re-apply diff --git a/Contracts/VaultFromSolidity/Importer/Syntax.lean b/Contracts/VaultFromSolidity/Importer/Syntax.lean index f3162c163b..d0b66e116a 100644 --- a/Contracts/VaultFromSolidity/Importer/Syntax.lean +++ b/Contracts/VaultFromSolidity/Importer/Syntax.lean @@ -21,10 +21,13 @@ open Lean namespace SolidityImporter.Sol -/-- Types of the accepted subset: `uint256` and `address`. -/ +/-- Types of the accepted subset: `uint256`, `address`, and a two-member +user struct as `uint256 × address`, indexed by the solc struct id so +distinct shapes-alike structs stay distinct in signatures. -/ inductive Ty where | uint : Ty | addr : Ty + | pair : Nat → Ty deriving DecidableEq, Repr, Inhabited, ToExpr /-- What an imported function returns. Empty is `void`; a singleton is the @@ -115,6 +118,8 @@ inductive Expr (L : Layout) (F : Fns) (Γ : Ctx) : Ty → Type where | var : Var Γ t → Expr L F Γ t /-- `msg.sender`. -/ | sender : Expr L F Γ .addr + /-- The zero address, used for named-return defaults. -/ + | zero : Expr L F Γ .addr /-- A numeric literal; the parser enforces `n < 2^256`. -/ | lit : Nat → Expr L F Γ .uint /-- `uint256` state variable read. -/ @@ -125,6 +130,17 @@ inductive Expr (L : Layout) (F : Fns) (Γ : Ctx) : Ty → Type where | index : SVar L .mapping → Expr L F Γ .addr → Expr L F Γ .uint /-- Checked `+`/`-` on `uint256`, reverting with `Panic(0x11)`. -/ | arith : ArithOp → Expr L F Γ .uint → Expr L F Γ .uint → Expr L F Γ .uint + /-- Memory struct `{amount, who}` of solc struct `id`. Evaluates amount then who + (positional `Acc(a, b)` and named `Acc({amount, who})`). -/ + | pair : {id : Nat} → Expr L F Γ .uint → Expr L F Γ .addr → Expr L F Γ (.pair id) + /-- Same packing as `pair`, but evaluates who then amount. Named + `Acc({who, amount})` uses this so source-order eval matches pinned solc 0.8.33 + before the result is packed as `uint256 × address`. -/ + | pairRev : {id : Nat} → Expr L F Γ .addr → Expr L F Γ .uint → Expr L F Γ (.pair id) + /-- First struct member (`amount`). -/ + | fst : {id : Nat} → Expr L F Γ (.pair id) → Expr L F Γ .uint + /-- Second struct member (`who`). -/ + | snd : {id : Nat} → Expr L F Γ (.pair id) → Expr L F Γ .addr /-- Internal call of an already-registered `view`/`pure` function that returns one value. Arguments are in declaration order and evaluate left to right. Effectful internals are `Stmt.callStmt` only: pinned solc 0.8.x @@ -140,6 +156,43 @@ inductive Args (L : Layout) (F : Fns) (Γ : Ctx) : List Ty → Type where deriving ToExpr end +/-- Insert `t'` at de Bruijn depth `n` (0 = innermost). -/ +def insertAt : Nat → Ty → Ctx → Ctx + | 0, t', Γ => t' :: Γ + | n + 1, t', t :: Γ => t :: insertAt n t' Γ + | _ + 1, t', [] => [t'] + +/-- Shift a variable across a binder inserted at depth `n`. -/ +def Var.shift (t' : Ty) : (n : Nat) → {Γ : Ctx} → Var Γ t → Var (insertAt n t' Γ) t + | 0, _, v => .there v + | _ + 1, _, .here => .here + | n + 1, _, .there v => .there (Var.shift t' n v) + +mutual +/-- Shift an expression across a binder inserted at depth `n`. -/ +def Expr.shift (t' : Ty) {L : Layout} {F : Fns} (n : Nat) {Γ : Ctx} {t : Ty} : + Expr L F Γ t → Expr L F (insertAt n t' Γ) t + | .var v => .var (v.shift t' n) + | .sender => .sender + | .zero => .zero + | .lit k => .lit k + | .load s => .load s + | .loadAddr s => .loadAddr s + | .index s key => .index s (key.shift t' n) + | .arith op a b => .arith op (a.shift t' n) (b.shift t' n) + | .pair a b => .pair (a.shift t' n) (b.shift t' n) + | .pairRev a b => .pairRev (a.shift t' n) (b.shift t' n) + | .fst e => .fst (e.shift t' n) + | .snd e => .snd (e.shift t' n) + | .call fv args => .call fv (args.shift t' n) + +/-- Shift call arguments across a binder inserted at depth `n`. -/ +def Args.shift (t' : Ty) {L : Layout} {F : Fns} (n : Nat) {Γ : Ctx} {ts : List Ty} : + Args L F Γ ts → Args L F (insertAt n t' Γ) ts + | .nil => .nil + | .cons e rest => .cons (e.shift t' n) (rest.shift t' n) +end + /-- Assignment targets: a `uint256` state variable or one mapping entry. Address writes use `Stmt.assignAddr`. -/ inductive LVal (L : Layout) (F : Fns) (Γ : Ctx) : Type where @@ -159,13 +212,42 @@ inductive Stmt (L : Layout) (F : Fns) : Ctx → Ret → Type where /-- `addr = rhs;` followed by the rest of the body. -/ | assignAddr : SVar L .addr → Expr L F Γ .addr → Stmt L F Γ r → Stmt L F Γ r /-- `uint256 x = e;` (or a parameter), followed by the rest of the body. -/ - | local_ : Expr L F Γ .uint → Stmt L F (.uint :: Γ) r → Stmt L F Γ r + | local_ : Expr L F Γ t → Stmt L F (t :: Γ) r → Stmt L F Γ r /-- `if (a < b) revert E();` with `E()` stored verbatim, followed by the rest of the body. -/ | guard : Expr L F Γ .uint → Expr L F Γ .uint → String → Stmt L F Γ r → Stmt L F Γ r + /-- `if (a != b) revert E();` on addresses. -/ + | guardAddrNe : Expr L F Γ .addr → Expr L F Γ .addr → String → Stmt L F Γ r → Stmt L F Γ r /-- Internal call of an already-registered void function, then the rest. -/ | callStmt : {ts : List Ty} → FVar F ⟨ts.reverse, []⟩ → Args L F Γ ts → Stmt L F Γ r → Stmt L F Γ r + /-- Run a void prefix, then the rest. Used for modifier preludes. -/ + | seq : Stmt L F Γ [] → Stmt L F Γ r → Stmt L F Γ r + /-- Run `inner`; its `ret`/`done` exits this block only. Then run void `post` + and yield `inner`'s value. Modifier postludes use this so they run after + an early return. -/ + | block : Stmt L F Γ r → Stmt L F Γ [] → Stmt L F Γ r deriving ToExpr +/-- Shift an assignment target across a binder inserted at depth `n`. -/ +def LVal.shift (t' : Ty) {L : Layout} {F : Fns} (n : Nat) {Γ : Ctx} : + LVal L F Γ → LVal L F (insertAt n t' Γ) + | .scalar s => .scalar s + | .mapping s key => .mapping s (key.shift t' n) + +/-- Shift a statement across a binder inserted at depth `n`. -/ +def Stmt.shift (t' : Ty) {L : Layout} {F : Fns} (n : Nat) {Γ : Ctx} {r : Ret} : + Stmt L F Γ r → Stmt L F (insertAt n t' Γ) r + | .done => .done + | .ret e => .ret (e.shift t' n) + | .assign lv op rhs rest => .assign (lv.shift t' n) op (rhs.shift t' n) (rest.shift t' n) + | .assignAddr s rhs rest => .assignAddr s (rhs.shift t' n) (rest.shift t' n) + | .local_ e rest => .local_ (e.shift t' n) (rest.shift t' (n + 1)) + | .guard a b msg rest => .guard (a.shift t' n) (b.shift t' n) msg (rest.shift t' n) + | .guardAddrNe a b msg rest => + .guardAddrNe (a.shift t' n) (b.shift t' n) msg (rest.shift t' n) + | .callStmt fv args rest => .callStmt fv (args.shift t' n) (rest.shift t' n) + | .seq pre rest => .seq (pre.shift t' n) (rest.shift t' n) + | .block inner post => .block (inner.shift t' n) (post.shift t' n) + end SolidityImporter.Sol diff --git a/PrintAxioms.lean b/PrintAxioms.lean index c48e2fe65b..aa7728b806 100644 --- a/PrintAxioms.lean +++ b/PrintAxioms.lean @@ -5,6 +5,8 @@ import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanNativeStepLemmas import Compiler.CompilationModel.ReservedScratchNames import Contracts.SolidityImportSmoke.Inheritance.Proofs +import Contracts.SolidityImportSmoke.Modifiers.Proofs +import Contracts.SolidityImportSmoke.Structs.Proofs import Contracts.Counter.Proofs.Basic import Contracts.Counter.Proofs.Correctness import Contracts.Counter.Proofs.Preview @@ -305,6 +307,21 @@ end Verity.AxiomAudit Contracts.SolidityImportSmoke.Inheritance.Proofs.bump_meets_spec Contracts.SolidityImportSmoke.Inheritance.Proofs.paused_invariant + -- Contracts/SolidityImportSmoke/Modifiers/Proofs.lean + Contracts.SolidityImportSmoke.Modifiers.Proofs.status_restored + Contracts.SolidityImportSmoke.Modifiers.Proofs.early_meets_spec + Contracts.SolidityImportSmoke.Modifiers.Proofs.guarded_success_spec + Contracts.SolidityImportSmoke.Modifiers.Proofs.guarded_reverts_not_owner_before_pause + Contracts.SolidityImportSmoke.Modifiers.Proofs.tagged_uses_base_helper + Contracts.SolidityImportSmoke.Modifiers.Proofs.snapshot_restores_status + + -- Contracts/SolidityImportSmoke/Structs/Proofs.lean + Contracts.SolidityImportSmoke.Structs.Proofs.set_then_get + Contracts.SolidityImportSmoke.Structs.Proofs.other_member_unchanged_thm + Contracts.SolidityImportSmoke.Structs.Proofs.get_meets_spec + Contracts.SolidityImportSmoke.Structs.Proofs.make_encodes + Contracts.SolidityImportSmoke.Structs.Proofs.makeRev_encodes + -- Contracts/Counter/Proofs/Basic.lean Contracts.Counter.Proofs.setStorage_updates_count Contracts.Counter.Proofs.getStorage_reads_count @@ -7609,4 +7626,4 @@ end Verity.AxiomAudit Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args ] --- Total: 7029 theorems/lemmas (5016 public, 2013 private, 0 sorry'd) +-- Total: 7040 theorems/lemmas (5027 public, 2013 private, 0 sorry'd) diff --git a/README.md b/README.md index 2aa433d1e0..6694d4e27b 100644 --- a/README.md +++ b/README.md @@ -73,6 +73,10 @@ lake build VaultFromSolidity python3 Contracts/VaultFromSolidity/Importer/scripts/solidity_importer_test.py lake build SolidityImportSmokeInheritance python3 Contracts/SolidityImportSmoke/Inheritance/scripts/inheritance_test.py +lake build SolidityImportSmokeModifiers +python3 Contracts/SolidityImportSmoke/Modifiers/scripts/modifiers_test.py +lake build SolidityImportSmokeStructs +python3 Contracts/SolidityImportSmoke/Structs/scripts/structs_test.py ``` The Vault acceptance script uses disposable copies for source mutations, fail-closed @@ -82,7 +86,13 @@ theorem. It never mutates the original Solidity file. The inheritance smoke (`Contracts/SolidityImportSmoke/Inheritance`) covers same-file `is` bases, C3 linearization including a diamond, virtual dispatch, `super` (target C3, not the defining-contract AST id), opaque fields, and internal calls (`Expr.call` -is view/pure only); `inheritance_test.py` is the matching focused suite. +is view/pure only); `inheritance_test.py` is the matching focused suite. The +modifiers smoke inlines argument-free modifiers in declaration order, including +`nonReentrant` postludes after an early `return` (`super` in a modifier uses +the modifier's defining contract; a prelude `return` before `_` is rejected). +The structs smoke encodes and decodes a two-member user struct used as a +parameter, storage field, and return (canonical names, one-shot RHS, zero +defaults, public product getter, struct ids in signatures). Save Solidity, rebuild this dedicated target, then reload the Lean editor: an already-open editor snapshot does not automatically watch `.sol` changes. See [the trust boundary](TRUST_ASSUMPTIONS.md#proof-only-solidity-vault-import). diff --git a/TRUST_ASSUMPTIONS.md b/TRUST_ASSUMPTIONS.md index 5b3c9f623b..4b21049252 100644 --- a/TRUST_ASSUMPTIONS.md +++ b/TRUST_ASSUMPTIONS.md @@ -59,21 +59,41 @@ never serialized. `Semantics.lean` tags its definitions into the `solidity_import` simp set, so `solidity_simp` unfolds `Fn.meaning` down to the Verity primitives exactly as it did before the split. -The accepted fragment covers the existing Vault plus the S1 inheritance slice: -full-width `uint256` scalars, `address` scalars, address-to-uint256 mappings and -public getters, straight-line reads/writes, locals, checked addition/subtraction, -comparison/custom-error guards, same-file `is` bases with solc's C3 +The accepted fragment covers the existing Vault, the S1 inheritance slice, and +the S2 modifiers/structs slice: full-width `uint256` scalars, `address` scalars, +address-to-uint256 mappings and public getters, straight-line reads/writes, +locals, checked addition/subtraction, comparison/custom-error guards (including +`address !=` for `onlyOwner`), same-file `is` bases with solc's C3 linearization (including diamonds), virtual dispatch and `super` specialized at -import time from the target's `linearizedBaseContracts` (matching 0.8.x runtime; -the AST `referencedDeclaration` on `super` follows the defining contract and is -not the dispatch key on diamonds), internal function calls (`Expr.call` is -`view`/`pure` only; effectful internals are `Stmt.callStmt`, because legacy -codegen evaluates those calls before the other operand / `+=` old-read), -abstract bases with body-less `virtual`s, -and opaque storage fields (slot reserved, not in `Storage`; a body that reads or -writes one is rejected). Unknown executable constructs are rejected; this is not -general Solidity support. Multi-file units, modifiers, packed fields, and -external calls remain out of the fragment. + import time from the target's `linearizedBaseContracts` (matching 0.8.x runtime; + the AST `referencedDeclaration` on `super` follows the defining contract and is + not the dispatch key on diamonds; `super` inside an inlined modifier starts + after that modifier's defining contract, not the function's), internal function + calls (`Expr.call` is + `view`/`pure` only; effectful internals are `Stmt.callStmt`, because legacy + codegen evaluates those calls before the other operand / `+=` old-read), + abstract bases with body-less `virtual`s, opaque storage fields (slot reserved, + not in `Storage`; a body that reads or writes one is rejected), argument-free + modifiers inlined at parse time in declaration order (`Stmt.seq` prelude plus + `Stmt.block` so a function `return` still runs the postlude; prelude `uint256` + locals scope over the inlined body and postlude; identifier calls in a + modifier body that resolve to a private or non-virtual helper stay bound to + the declaring contract even if a derived contract declares a same-name private + function; a modifier with + two `_`, with arguments, or with a prelude `return` before `_` is rejected; + `Semantics.lean` never sees `_`), named `address`/struct returns defaulting to + the zero address rather than `msg.sender`, and + user structs used as parameters, storage, and returns when they are the closed + `uint256` then `address` pair (members occupy consecutive solc slots; encode is + `Expr.pair` indexed by the solc struct id so same-shape structs stay distinct + in signatures; a public struct field registers one product getter; a storage + struct assignment binds the RHS pair once; named `Acc({...})` constructors + evaluate arguments in source order (pinned 0.8.33) then pack into the + `uint256 × address` member product — `Expr.pair` when names are already + member order, `Expr.pairRev` when they are `{who, amount}`; positional + `Acc(a, b)` stays AST/member order). Unknown executable constructs are +rejected; this is not general Solidity support. Multi-file units, packed +fields, events, and external calls remain out of the fragment. Arguments/context are already typed and decoded. `Contract.run` rolls back failed executions; errors are model strings, not verified ABI revert bytes. The storage model uses logical keys, not a proof of physical keccak layout. diff --git a/artifacts/trust_surface_report.json b/artifacts/trust_surface_report.json index f8ce7b16b4..1d4af2ff19 100644 --- a/artifacts/trust_surface_report.json +++ b/artifacts/trust_surface_report.json @@ -169,7 +169,7 @@ "mechanisms": { "@[implemented_by": 1, "native_decide": 613, - "partial def": 178 + "partial def": 182 }, "notes": "native_decide trusts Lean.ofReduceBool or Lean 4.31 generated per-proof native_decide axioms + Lean.trustCompiler. Prose registry: AXIOMS.md, TRUST_ASSUMPTIONS.md (enforced by scripts/check_trust_surface_registry.py).", "schema_version": 1 diff --git a/artifacts/verification_status.json b/artifacts/verification_status.json index 9fe885b2b1..e084577f11 100644 --- a/artifacts/verification_status.json +++ b/artifacts/verification_status.json @@ -16,10 +16,10 @@ }, "theorems": { "categories": 17, - "coverage_percent": 74, + "coverage_percent": 72, "covered": 255, - "excluded": 90, - "non_stdlib_total": 345, + "excluded": 101, + "non_stdlib_total": 356, "per_contract": { "Counter": 31, "ERC20": 22, @@ -35,13 +35,13 @@ "SafeCounter": 25, "SimpleStorage": 20, "SimpleToken": 61, - "SolidityImportSmoke": 9, + "SolidityImportSmoke": 20, "Vault": 9, "VaultFromSolidity": 7 }, - "proven": 345, + "proven": 356, "stdlib": 0, - "total": 345 + "total": 356 }, "toolchain": { "lean": "leanprover/lean4:v4.31.0", diff --git a/docs-site/public/llms.txt b/docs-site/public/llms.txt index ed61d78b29..c8a39737ff 100644 --- a/docs-site/public/llms.txt +++ b/docs-site/public/llms.txt @@ -31,11 +31,11 @@ Every transition inside the proof envelope is either fully verified or recorded - **Language**: Lean 4.31.0 -- **Core Size**: 2104 lines +- **Core Size**: 2257 lines - **Verified Contracts**: 17 (Counter, ERC20, ERC721, Ledger, LocalObligationMacroSmoke, Ownable, Owned, OwnedCounter, OwnedCounterComposed, ReentrancyExample, ReentrancyRelyGuarantee, SafeCounter, SimpleStorage, SimpleToken, SolidityImportSmoke, Vault, VaultFromSolidity) -- **Theorems**: 345 across 17 categories, 345 fully proven +- **Theorems**: 356 across 17 categories, 356 fully proven - **Axioms**: 1 documented Lean axioms (see AXIOMS.md) -- **Tests**: 528 Foundry tests, 239 property tests +- **Tests**: 532 Foundry tests, 239 property tests - **Build**: `lake build` verifies all proofs - **Repository**: https://github.com/lfglabs-dev/verity diff --git a/docs/VERIFICATION_STATUS.md b/docs/VERIFICATION_STATUS.md index af7767e4c6..7087556a80 100644 --- a/docs/VERIFICATION_STATUS.md +++ b/docs/VERIFICATION_STATUS.md @@ -40,13 +40,13 @@ EVM Bytecode | ERC721 | 11 | Baseline | `Contracts/ERC721/Proofs/` | | Vault | 9 | Baseline | `Contracts/Vault/Proofs/` | | VaultFromSolidity | 7 | Proof-only import | `Contracts/VaultFromSolidity/Proofs/` | -| SolidityImportSmoke | 9 | Proof-only import | `Contracts/SolidityImportSmoke/Inheritance/` | +| SolidityImportSmoke | 20 | Proof-only import | `Contracts/SolidityImportSmoke/` | | ReentrancyExample | 5 | Complete | `Contracts/ReentrancyExample/Contract.lean` | | ReentrancyRelyGuarantee | 10 | Semantic | `Contracts/ReentrancyRelyGuarantee/Contract.lean` | | CryptoHash | 0 | No specs | `Contracts/CryptoHash/Contract.lean` | -| **Total** | **345** | **✅ 100%** | — | +| **Total** | **356** | **✅ 100%** | — | -> **Note**: Stdlib (0 internal proof-automation properties) is excluded from the contract-spec theorem table above but included in overall coverage statistics (345 total properties). +> **Note**: Stdlib (0 internal proof-automation properties) is excluded from the contract-spec theorem table above but included in overall coverage statistics (356 total properties). Layer 1 uses macro-generated EDSL-to-`CompilationModel` bridge theorems backed by a generic typed-IR compilation-correctness theorem ([`TypedIRCompilerCorrectness.lean`](../Compiler/TypedIRCompilerCorrectness.lean)). Tuple/bytes/fixed-array/dynamic-array/string parameters now stay inside that proof path when they are carried as ABI head words/offsets. Advanced constructs beyond that typed-IR head-word surface (linked libraries, ECMs, fully custom ABI behavior) are still expressed directly in `CompilationModel` and trusted at that boundary. Higher-order internal helpers (function-pointer parameters, [#1747](https://github.com/lfglabs-dev/verity/issues/1747)) are eliminated by a compile-time monomorphization pre-pass that runs before any lowering, so the `CompilationModel` only ever contains first-order helpers: these calls are covered by the existing first-order proof path and introduce no new boundary trust. @@ -205,7 +205,7 @@ Also note that the macro-generated `*_semantic_preservation` theorems are not co | ERC20 | 86% (19/22) | 3 proof-only | | Vault | 0% (0/9) | 9 proof-only | | VaultFromSolidity | 0% (0/7) | 7 proof-only | -| SolidityImportSmoke | 0% (0/9) | 9 proof-only | +| SolidityImportSmoke | 0% (0/20) | 20 proof-only | | ERC721 | 100% (11/11) | 0 | | SafeCounter | 100% (25/25) | 0 | | ReentrancyExample | 100% (5/5) | 0 | @@ -221,11 +221,11 @@ Also note that the macro-generated `*_semantic_preservation` theorems are not co | Counter | 74% (23/31) | 8 proof-only | | Stdlib | 0% (0/0) | 0 proof-only | -**Status**: 74% coverage (255/345), 90 remaining exclusions all proof-only +**Status**: 72% coverage (255/356), 101 remaining exclusions all proof-only -- **Total Properties**: 345 +- **Total Properties**: 356 - **Covered**: 255 -- **Excluded**: 90 (all proof-only) +- **Excluded**: 101 (all proof-only) **Proof-Only Properties (74 exclusions)**: Internal proof machinery that cannot be tested in Foundry. diff --git a/lakefile.lean b/lakefile.lean index 96c5dc9416..cb41bf7d54 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -69,6 +69,28 @@ lean_lib «SolidityImportSmokeInheritance» where needs := #[inheritanceSolidity, vaultLeanImporter, vaultLeanSyntax, vaultLeanSemantics, vaultSolc, vaultBuildPolicy] +input_file modifiersSolidity where + path := "Contracts/SolidityImportSmoke/Modifiers/Modifiers.sol" + text := false + +lean_lib «SolidityImportSmokeModifiers» where + globs := #[.one `Contracts.SolidityImportSmoke.Modifiers.Modifiers, + .one `Contracts.SolidityImportSmoke.Modifiers.Spec, + .one `Contracts.SolidityImportSmoke.Modifiers.Proofs] + needs := #[modifiersSolidity, vaultLeanImporter, vaultLeanSyntax, vaultLeanSemantics, vaultSolc, + vaultBuildPolicy] + +input_file structsSolidity where + path := "Contracts/SolidityImportSmoke/Structs/Structs.sol" + text := false + +lean_lib «SolidityImportSmokeStructs» where + globs := #[.one `Contracts.SolidityImportSmoke.Structs.Structs, + .one `Contracts.SolidityImportSmoke.Structs.Spec, + .one `Contracts.SolidityImportSmoke.Structs.Proofs] + needs := #[structsSolidity, vaultLeanImporter, vaultLeanSyntax, vaultLeanSemantics, vaultSolc, + vaultBuildPolicy] + lean_lib «Contracts» where globs := #[ .one `Contracts, diff --git a/scripts/check_contract_structure.py b/scripts/check_contract_structure.py index e698a2493c..2020ff195b 100755 --- a/scripts/check_contract_structure.py +++ b/scripts/check_contract_structure.py @@ -22,7 +22,7 @@ "Ownable", # Mixin facet: named-slot proofs + footprint, no Foundry/Yul twin "OwnedCounterComposed", # Include-host acceptance example; OwnedCounter keeps Yul/difftest "VaultFromSolidity", # Proof-only imported model with its own focused structure - "SolidityImportSmoke", # Nested proof-only importer smokes (Inheritance, …) + "SolidityImportSmoke", # Nested proof-only importer smokes (Inheritance, Modifiers, Structs) } # Contracts excluded from property test check @@ -33,7 +33,7 @@ "Ownable", # Mixin proofs are reused by hosts; no compiled property harness "OwnedCounterComposed", # Proof-composition host; OwnedCounter remains the Foundry target "VaultFromSolidity", # Imported-model theorems are covered by the focused mutation suite - "SolidityImportSmoke", # Importer smoke theorems are covered by inheritance_test.py + "SolidityImportSmoke", # Importer smoke theorems are covered by focused Python suites } # Contracts excluded from differential test check diff --git a/scripts/check_spec_named_storage.py b/scripts/check_spec_named_storage.py index bb14f69347..0595ba4323 100644 --- a/scripts/check_spec_named_storage.py +++ b/scripts/check_spec_named_storage.py @@ -35,6 +35,8 @@ SPEC_FILES = ( "Contracts/VaultFromSolidity/Spec.lean", "Contracts/SolidityImportSmoke/Inheritance/Spec.lean", + "Contracts/SolidityImportSmoke/Modifiers/Spec.lean", + "Contracts/SolidityImportSmoke/Structs/Spec.lean", ) CORE_LEAN = "Verity/Core.lean" diff --git a/scripts/generate_print_axioms.py b/scripts/generate_print_axioms.py index 0bc4e4ad42..f97e21420a 100644 --- a/scripts/generate_print_axioms.py +++ b/scripts/generate_print_axioms.py @@ -22,6 +22,8 @@ TRUST_BOUNDARY_FILES = [ ROOT / "Compiler" / "CompilationModel" / "ReservedScratchNames.lean", ROOT / "Contracts" / "SolidityImportSmoke" / "Inheritance" / "Proofs.lean", + ROOT / "Contracts" / "SolidityImportSmoke" / "Modifiers" / "Proofs.lean", + ROOT / "Contracts" / "SolidityImportSmoke" / "Structs" / "Proofs.lean", ] def _collect_contract_proof_dirs() -> list[Path]: diff --git a/test/property_exclusions.json b/test/property_exclusions.json index 7b886be5ed..841b1ccc7f 100644 --- a/test/property_exclusions.json +++ b/test/property_exclusions.json @@ -28,12 +28,23 @@ "bump_meets_spec", "bump_success_spec", "dispatch_is_child", + "early_meets_spec", + "get_meets_spec", "go_meets_spec", "go_success_spec", + "guarded_reverts_not_owner_before_pause", + "guarded_success_spec", + "makeRev_encodes", + "make_encodes", + "other_member_unchanged_thm", "pause_meets_spec", "pause_success_spec", "paused_invariant", - "super_runs_parent" + "set_then_get", + "snapshot_restores_status", + "status_restored", + "super_runs_parent", + "tagged_uses_base_helper" ], "Counter": [ "getStorage_reads_count", diff --git a/test/property_manifest.json b/test/property_manifest.json index 5df20ab436..8aa30a5928 100644 --- a/test/property_manifest.json +++ b/test/property_manifest.json @@ -351,12 +351,23 @@ "bump_meets_spec", "bump_success_spec", "dispatch_is_child", + "early_meets_spec", + "get_meets_spec", "go_meets_spec", "go_success_spec", + "guarded_reverts_not_owner_before_pause", + "guarded_success_spec", + "makeRev_encodes", + "make_encodes", + "other_member_unchanged_thm", "pause_meets_spec", "pause_success_spec", "paused_invariant", - "super_runs_parent" + "set_then_get", + "snapshot_restores_status", + "status_restored", + "super_runs_parent", + "tagged_uses_base_helper" ], "Vault": [ "balanceOf_meets_spec",