diff --git a/certora_autosetup/amenability/__init__.py b/certora_autosetup/amenability/__init__.py
new file mode 100644
index 0000000..710dcec
--- /dev/null
+++ b/certora_autosetup/amenability/__init__.py
@@ -0,0 +1,10 @@
+"""certora-fv-amenability: score how amenable a Solidity project is to automatic
+formal verification (autosetup) — low / medium / high — from deterministic AST
+signals (phase 1) plus an LLM judge over a versioned rubric (phase 2).
+
+See report.py for the output contract and signals/ for the individual metrics.
+"""
+
+from certora_autosetup.amenability.report import AmenabilityReport, Level
+
+__all__ = ["AmenabilityReport", "Level"]
diff --git a/certora_autosetup/amenability/cli.py b/certora_autosetup/amenability/cli.py
new file mode 100644
index 0000000..977de82
--- /dev/null
+++ b/certora_autosetup/amenability/cli.py
@@ -0,0 +1,148 @@
+"""certora-fv-amenability: score how amenable a Solidity project is to
+automatic formal verification with autosetup.
+
+JSON in/out, no side effects: clients (SaaS, CI, humans) call this and read the
+report from stdout. Exit 0 = scored (any level); exit 1 = could not score
+(most importantly: the project does not compile).
+"""
+
+import argparse
+import subprocess
+import sys
+from pathlib import Path
+
+from certora_autosetup.amenability.compile import CannotScoreError, resolve_dumps
+from certora_autosetup.amenability.context import AnalysisContext
+from certora_autosetup.amenability.report import (
+    AmenabilityReport,
+    Level,
+    Recommendation,
+    ScoringErrorReport,
+)
+from certora_autosetup.amenability.scoring import DEFAULT_WEIGHTS, ScoringConfig, aggregate
+from certora_autosetup.amenability.signals import ALL_SIGNALS
+from certora_autosetup.solidity_ast import ContractDefinition, find_all
+
+BASE_CONFIDENCE = 0.6  # static-only scoring; the phase-2 judge raises/lowers this
+
+
+def _tool_version() -> str:
+    try:
+        return subprocess.run(
+            ["git", "describe", "--always", "--dirty"],
+            cwd=Path(__file__).parent, capture_output=True, text=True, timeout=5,
+        ).stdout.strip() or "unknown"
+    except Exception:
+        return "unknown"
+
+
+def _recommendations(report_evidence) -> list[Recommendation]:
+    kinds = {e.signal for e in report_evidence}
+    recs = []
+    if "curated_summary_hits" in kinds:
+        recs.append(Recommendation(
+            kind="summary",
+            detail="Replace hand-rolled math kernels with a standard library "
+                   "(OZ Math / FullMath / prb-math) for which autosetup ships curated summaries.",
+        ))
+    if "asm_trampoline" in kinds:
+        recs.append(Recommendation(
+            kind="reference-impl",
+            detail="Replace manual calldata/delegatecall trampolines with direct calls or a "
+                   "reference implementation without the forwarding layer.",
+        ))
+    if "asm_fp_manipulation" in kinds or "storage_packing" in kinds:
+        recs.append(Recommendation(
+            kind="munge",
+            detail="Move hand-rolled memory/storage layouts behind standard declarations or "
+                   "sanctioned slot patterns (ERC-7201/StorageSlot) so the prover's storage "
+                   "and memory analyses can model them.",
+        ))
+    if "bitmask_style" in kinds or "mixed_theory" in kinds:
+        recs.append(Recommendation(
+            kind="harness",
+            detail="Extract packed-field decoding and nonlinear math into small internal pure "
+                   "functions — each becomes a summarization seam for modular proofs.",
+        ))
+    return recs
+
+
+def main() -> int:
+    parser = argparse.ArgumentParser(prog="certora-fv-amenability", description=__doc__)
+    parser.add_argument("project_root", type=Path)
+    parser.add_argument("--contract", action="append", default=[],
+                        help="restrict the contracts_analyzed listing (repeatable)")
+    parser.add_argument("--ast-dump", action="append", default=[], type=Path,
+                        help="existing certoraRun --dump_asts output (repeatable)")
+    parser.add_argument("--weights", type=Path, default=DEFAULT_WEIGHTS)
+    parser.add_argument("--judge", action="store_true",
+                        help="run the LLM judge over the static report (requires "
+                             "Anthropic credentials); default is static-only")
+    parser.add_argument("--rubric-version", default=None,
+                        help="pin a specific judge rubric version (default: latest)")
+    parser.add_argument("--no-llm", action="store_true",
+                        help="explicitly static-only (the default; kept for interface stability)")
+    parser.add_argument("--output", type=Path, default=None, help="write report here instead of stdout")
+    args = parser.parse_args()
+
+    project_root = args.project_root.resolve()
+
+    try:
+        resolution = resolve_dumps(project_root, args.ast_dump)
+    except CannotScoreError as e:
+        error = ScoringErrorReport(project=str(project_root), error=e.error, detail=e.detail)
+        print(error.model_dump_json(indent=2))
+        return 1
+
+    ctx = AnalysisContext(project_root=project_root, dumps=resolution.dumps)
+
+    config = ScoringConfig.load(args.weights)
+    results = [sig(ctx) for sig in ALL_SIGNALS]
+    static = aggregate(results, config)
+    evidence = [e for r in results for e in r.evidence]
+
+    contracts = sorted({
+        c.name for _, root in ctx.iter_sources()
+        for c in find_all(root, ContractDefinition)
+        if c.contractKind == "contract" and not c.abstract
+    })
+    if args.contract:
+        requested = set(args.contract)
+        contracts = [c for c in contracts if c in requested]
+
+    confidence = BASE_CONFIDENCE
+    if ctx.unparsed_source_count:
+        confidence = max(0.3, confidence - 0.05 * ctx.unparsed_source_count)
+
+    report = AmenabilityReport(
+        tool_version=_tool_version(),
+        project=str(project_root),
+        contracts_analyzed=contracts,
+        level=static.provisional_level,
+        confidence=round(confidence, 2),
+        static=static,
+        evidence=evidence,
+        recommendations=_recommendations(evidence),
+    )
+
+    if args.judge and not args.no_llm:
+        from certora_autosetup.amenability.judge import JudgeError, judge_report
+        try:
+            report.judge = judge_report(report, ctx, rubric_version=args.rubric_version)
+            report.level = Level(report.judge["level"])
+            report.confidence = round(
+                (confidence + report.judge["confidence"]) / 2, 2
+            )
+        except JudgeError as e:
+            print(f"judge failed, keeping static verdict: {e}", file=sys.stderr)
+
+    payload = report.model_dump_json(indent=2)
+    if args.output:
+        args.output.write_text(payload + "\n")
+    else:
+        print(payload)
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())
diff --git a/certora_autosetup/amenability/compile.py b/certora_autosetup/amenability/compile.py
new file mode 100644
index 0000000..865aeaf
--- /dev/null
+++ b/certora_autosetup/amenability/compile.py
@@ -0,0 +1,63 @@
+"""AST-dump acquisition.
+
+Compiling is the amenability floor: there is no degraded raw-source scoring
+path. The resolution order is (1) dumps passed explicitly, (2) dumps a previous
+certoraRun/autosetup run left under .certora_internal, (3) a distinct
+"cannot score" error telling the caller exactly what to run.
+"""
+
+from dataclasses import dataclass
+from pathlib import Path
+
+from certora_autosetup.solidity_ast import AstDump
+
+DUMP_BASENAMES = ("all_asts.json", ".asts.json")
+
+
+class CannotScoreError(Exception):
+    def __init__(self, error: str, detail: str):
+        super().__init__(detail)
+        self.error = error
+        self.detail = detail
+
+
+@dataclass
+class DumpResolution:
+    dumps: list[AstDump]
+    dump_paths: list[Path]
+
+
+def discover_dumps(project_root: Path) -> list[Path]:
+    """Newest-first AST dumps a previous certoraRun left in the project."""
+    internal = project_root / ".certora_internal"
+    if not internal.is_dir():
+        return []
+    candidates = [
+        p for name in DUMP_BASENAMES for p in internal.rglob(name) if p.is_file()
+    ]
+    return sorted(candidates, key=lambda p: p.stat().st_mtime, reverse=True)
+
+
+def resolve_dumps(project_root: Path, ast_dump_args: list[Path]) -> DumpResolution:
+    if ast_dump_args:
+        missing = [p for p in ast_dump_args if not p.is_file()]
+        if missing:
+            raise CannotScoreError(
+                "no-ast-dump", f"--ast-dump path(s) not found: {', '.join(map(str, missing))}"
+            )
+        return DumpResolution(
+            dumps=[AstDump.load(p) for p in ast_dump_args], dump_paths=list(ast_dump_args)
+        )
+
+    discovered = discover_dumps(project_root)
+    if discovered:
+        newest = discovered[0]
+        return DumpResolution(dumps=[AstDump.load(newest)], dump_paths=[newest])
+
+    raise CannotScoreError(
+        "does-not-compile",
+        "No AST dump found. The project must compile before it can be scored — run "
+        "`certoraRun <files...> --compilation_steps_only --dump_asts` (or a "
+        "certora-autosetup compilation analysis) in the project first, or pass an "
+        "existing dump via --ast-dump.",
+    )
diff --git a/certora_autosetup/amenability/context.py b/certora_autosetup/amenability/context.py
new file mode 100644
index 0000000..9daf6ab
--- /dev/null
+++ b/certora_autosetup/amenability/context.py
@@ -0,0 +1,130 @@
+"""AnalysisContext: the one object every signal receives.
+
+Wraps one or more AstDumps (a project may have per-contract dumps), deduplicates
+sources across them, separates project code from dependencies, and maps AST byte
+offsets to source lines for evidence.
+"""
+
+from dataclasses import dataclass, field
+from pathlib import Path
+from typing import Iterator, Optional
+
+from certora_autosetup.solidity_ast import (
+    AstDump,
+    ContractDefinition,
+    FunctionDefinition,
+    SourceUnit,
+    find_all,
+)
+
+# Path fragments that mark a source as a dependency rather than project code.
+# Signals score project code; dependencies still participate where they must
+# (e.g. curated-summary library detection).
+DEPENDENCY_MARKERS = ("node_modules/", "lib/", "dependencies/", ".deps/")
+
+# Dumps produced inside build containers key sources by the container's project
+# mount; strip these so source text resolves against the host project_root.
+CONTAINER_ROOTS = ("/workspace/project/",)
+
+
+def _strip_container_root(source_path: str) -> str:
+    for root in CONTAINER_ROOTS:
+        if source_path.startswith(root):
+            return source_path[len(root):]
+    return source_path
+
+
+def is_dependency_path(source_path: str) -> bool:
+    p = _strip_container_root(source_path).lstrip("./")
+    return any(p.startswith(m) or f"/{m}" in p for m in DEPENDENCY_MARKERS)
+
+
+@dataclass
+class AnalysisContext:
+    project_root: Path
+    dumps: list[AstDump]
+    _sources: dict[str, SourceUnit] = field(default_factory=dict, init=False)
+    _line_tables: dict[str, list[int]] = field(default_factory=dict, init=False)
+    _source_texts: dict[str, Optional[bytes]] = field(default_factory=dict, init=False)
+    unparsed_source_count: int = field(default=0, init=False)
+
+    def __post_init__(self) -> None:
+        for dump in self.dumps:
+            for _, source in dump.iter_sources():
+                if source.root is None:
+                    self.unparsed_source_count += 1
+                elif source.source_path not in self._sources:
+                    self._sources[source.source_path] = source.root
+
+    # ---- source iteration -------------------------------------------------
+
+    def iter_sources(self, *, include_dependencies: bool = False) -> Iterator[tuple[str, SourceUnit]]:
+        for path, root in self._sources.items():
+            if include_dependencies or not is_dependency_path(path):
+                yield path, root
+
+    def iter_contracts(
+        self, *, include_dependencies: bool = False
+    ) -> Iterator[tuple[str, ContractDefinition]]:
+        for path, root in self.iter_sources(include_dependencies=include_dependencies):
+            for contract in find_all(root, ContractDefinition):
+                yield path, contract
+
+    def iter_functions(
+        self, *, implemented_only: bool = True, include_dependencies: bool = False
+    ) -> Iterator[tuple[str, ContractDefinition, FunctionDefinition]]:
+        """(source_path, contract, function) over contract members (not free functions)."""
+        for path, contract in self.iter_contracts(include_dependencies=include_dependencies):
+            for node in contract.nodes:
+                if isinstance(node, FunctionDefinition) and (node.implemented or not implemented_only):
+                    yield path, contract, node
+
+    # ---- source text / line mapping --------------------------------------
+
+    def display_path(self, source_path: str) -> str:
+        """Project-relative path for reports (falls back to the raw dump path)."""
+        stripped = _strip_container_root(source_path)
+        if stripped != source_path:
+            return stripped
+        try:
+            return str(Path(source_path).resolve().relative_to(self.project_root.resolve()))
+        except ValueError:
+            return source_path
+
+    def _text(self, source_path: str) -> Optional[bytes]:
+        if source_path not in self._source_texts:
+            candidate = self.project_root / _strip_container_root(source_path)
+            self._source_texts[source_path] = (
+                candidate.read_bytes() if candidate.is_file() else None
+            )
+        return self._source_texts[source_path]
+
+    def offset_to_line(self, source_path: str, byte_offset: int) -> int:
+        """1-based line for a solc src byte offset; 0 when the source file is
+        unavailable (evidence stays usable, just without a line anchor)."""
+        text = self._text(source_path)
+        if text is None:
+            return 0
+        if source_path not in self._line_tables:
+            starts = [0]
+            for i, b in enumerate(text):
+                if b == 0x0A:
+                    starts.append(i + 1)
+            self._line_tables[source_path] = starts
+        starts = self._line_tables[source_path]
+        # binary search: number of line starts <= offset
+        lo, hi = 0, len(starts)
+        while lo < hi:
+            mid = (lo + hi) // 2
+            if starts[mid] <= byte_offset:
+                lo = mid + 1
+            else:
+                hi = mid
+        return lo
+
+    def line_span(self, source_path: str, byte_offset: int, byte_length: int) -> int:
+        """Number of source lines a node covers (0 when the source is unavailable)."""
+        text = self._text(source_path)
+        if text is None:
+            return 0
+        return text[byte_offset : byte_offset + byte_length].count(b"\n") + 1
diff --git a/certora_autosetup/amenability/judge/__init__.py b/certora_autosetup/amenability/judge/__init__.py
new file mode 100644
index 0000000..142ebfe
--- /dev/null
+++ b/certora_autosetup/amenability/judge/__init__.py
@@ -0,0 +1,6 @@
+"""Phase-2 LLM judge: a single structured call over the static report + code
+excerpts, clamped to ±1 level of the static provisional score."""
+
+from certora_autosetup.amenability.judge.agent import JudgeError, judge_report
+
+__all__ = ["judge_report", "JudgeError"]
diff --git a/certora_autosetup/amenability/judge/agent.py b/certora_autosetup/amenability/judge/agent.py
new file mode 100644
index 0000000..9a53349
--- /dev/null
+++ b/certora_autosetup/amenability/judge/agent.py
@@ -0,0 +1,178 @@
+"""LLM judge (phase 2): one structured call per project.
+
+Design choices, in order of importance:
+- Everything the judge needs is pre-assembled into the prompt (static report +
+  ±N-line excerpts around every evidence item), so a single request suffices —
+  no tool loop, which keeps cost bounded and the verdict reproducible-ish.
+- The verdict is CLAMPED in code to at most one level away from the static
+  provisional, and only moves at all with >= 2 concrete citations. The judge
+  refines, it does not override.
+- The output records model / rubric version+sha / prompt version and the request
+  usage+cost, so fleet runs can budget and audits can reproduce.
+"""
+
+import hashlib
+import re
+from pathlib import Path
+from typing import Optional
+
+from pydantic import BaseModel, Field
+
+from certora_autosetup.amenability.context import AnalysisContext
+from certora_autosetup.amenability.report import AmenabilityReport, Level
+
+JUDGE_MODEL = "claude-opus-4-8"
+# USD per 1M tokens (input, output, cache-read) — used for fleet budget tracking.
+PRICE_INPUT_PER_MTOK = 5.00
+PRICE_OUTPUT_PER_MTOK = 25.00
+PRICE_CACHE_READ_PER_MTOK = 0.50
+PROMPT_TEMPLATE_VERSION = "1"
+EXCERPT_RADIUS = 10  # lines around each evidence line
+MAX_EXCERPTS = 40
+MAX_OUTPUT_TOKENS = 2000
+
+RUBRIC_DIR = Path(__file__).parent / "rubric"
+
+LEVEL_ORDER = [Level.LOW, Level.MEDIUM, Level.HIGH]
+
+
+class JudgeCitation(BaseModel):
+    file: str
+    line: int
+    quote: str
+    signal: str
+
+
+class JudgeVerdict(BaseModel):
+    level: Level
+    confidence: float = Field(ge=0.0, le=1.0)
+    rationale: str
+    citations: list[JudgeCitation]
+
+
+class JudgeError(Exception):
+    pass
+
+
+def load_rubric(version: Optional[str] = None) -> tuple[str, str, str]:
+    """(version, sha256, text) of the requested (default: latest) rubric."""
+    rubrics = sorted(RUBRIC_DIR.glob("rubric_v*.md"))
+    if not rubrics:
+        raise JudgeError(f"no rubric files under {RUBRIC_DIR}")
+    if version:
+        path = RUBRIC_DIR / f"rubric_v{version}.md"
+        if not path.is_file():
+            raise JudgeError(f"rubric version {version} not found")
+    else:
+        path = rubrics[-1]
+    text = path.read_text()
+    match = re.search(r"rubric_v(\w+)\.md", path.name)
+    ver = match.group(1) if match else path.stem
+    return ver, hashlib.sha256(text.encode()).hexdigest(), text
+
+
+def build_excerpts(ctx: AnalysisContext, report: AmenabilityReport) -> str:
+    """±EXCERPT_RADIUS-line excerpts around each evidence item, deduplicated."""
+    seen: set[tuple[str, int]] = set()
+    chunks: list[str] = []
+    for e in report.evidence:
+        key = (e.file, e.line // (EXCERPT_RADIUS * 2))
+        if e.line == 0 or key in seen:
+            continue
+        seen.add(key)
+        source = ctx.project_root / e.file
+        if not source.is_file():
+            continue
+        lines = source.read_text(errors="replace").splitlines()
+        lo = max(0, e.line - 1 - EXCERPT_RADIUS)
+        hi = min(len(lines), e.line + EXCERPT_RADIUS)
+        body = "\n".join(f"{i + 1:5d}| {lines[i]}" for i in range(lo, hi))
+        chunks.append(f"--- {e.file}:{e.line} [{e.signal}] ---\n{body}")
+        if len(chunks) >= MAX_EXCERPTS:
+            break
+    return "\n\n".join(chunks)
+
+
+def _clamp(static_level: Level, judged: Level, citations: int) -> tuple[Level, bool]:
+    """Enforce the guardrail: >= 2 citations to move, and at most one step."""
+    if judged == static_level:
+        return judged, False
+    if citations < 2:
+        return static_level, True
+    si, ji = LEVEL_ORDER.index(static_level), LEVEL_ORDER.index(judged)
+    if abs(ji - si) > 1:
+        ji = si + (1 if ji > si else -1)
+        return LEVEL_ORDER[ji], True
+    return judged, False
+
+
+def judge_report(
+    report: AmenabilityReport,
+    ctx: AnalysisContext,
+    rubric_version: Optional[str] = None,
+    client=None,
+) -> dict:
+    """Run the judge over a static report; returns the report's `judge` dict."""
+    import anthropic  # deferred: --no-llm paths must not require the SDK
+
+    ver, sha, rubric_text = load_rubric(rubric_version)
+    if client is None:
+        client = anthropic.Anthropic()
+
+    static_json = report.model_dump_json(
+        include={"level", "static", "evidence", "contracts_analyzed"}, indent=1
+    )
+    excerpts = build_excerpts(ctx, report)
+
+    system = (
+        f"{rubric_text}\n\n"
+        "Return your verdict via the structured output schema. `level` is your "
+        "judged amenability level; `citations` must reference concrete file:line "
+        "locations from the provided evidence/excerpts with a short quote each. "
+        "You may move at most one level away from the static provisional level, "
+        "and only with at least two citations justifying the move."
+    )
+    user = (
+        f"## Static analysis report\n\n{static_json}\n\n"
+        f"## Code excerpts (around each evidence item)\n\n{excerpts or '(no excerpts available)'}"
+    )
+
+    response = client.messages.parse(
+        model=JUDGE_MODEL,
+        max_tokens=MAX_OUTPUT_TOKENS,
+        system=[{"type": "text", "text": system, "cache_control": {"type": "ephemeral"}}],
+        messages=[{"role": "user", "content": user}],
+        output_format=JudgeVerdict,
+    )
+    verdict = response.parsed_output
+    if not isinstance(verdict, JudgeVerdict):
+        raise JudgeError(f"judge returned no parseable verdict (stop_reason={response.stop_reason})")
+
+    final_level, clamped = _clamp(report.level, verdict.level, len(verdict.citations))
+
+    usage = response.usage
+    cost = (
+        usage.input_tokens * PRICE_INPUT_PER_MTOK
+        + usage.output_tokens * PRICE_OUTPUT_PER_MTOK
+        + (usage.cache_read_input_tokens or 0) * PRICE_CACHE_READ_PER_MTOK
+    ) / 1_000_000
+
+    return {
+        "level": final_level.value,
+        "raw_level": verdict.level.value,
+        "clamped": clamped,
+        "confidence": verdict.confidence,
+        "rationale": verdict.rationale,
+        "citations": [c.model_dump() for c in verdict.citations],
+        "disagrees_with_static": final_level != report.level,
+        "model": JUDGE_MODEL,
+        "rubric_version": ver,
+        "rubric_sha256": sha,
+        "prompt_template_version": PROMPT_TEMPLATE_VERSION,
+        "usage": {
+            "input_tokens": usage.input_tokens,
+            "output_tokens": usage.output_tokens,
+            "cache_read_input_tokens": usage.cache_read_input_tokens or 0,
+            "cost_usd": round(cost, 6),
+        },
+    }
diff --git a/certora_autosetup/amenability/judge/rubric/rubric_v1.md b/certora_autosetup/amenability/judge/rubric/rubric_v1.md
new file mode 100644
index 0000000..d056bb6
--- /dev/null
+++ b/certora_autosetup/amenability/judge/rubric/rubric_v1.md
@@ -0,0 +1,62 @@
+---
+version: 1
+date: 2026-07-18
+status: initial
+---
+
+# FV-Amenability Judging Rubric (v1)
+
+You judge how amenable a Solidity project is to automatic formal verification with
+Certora's autosetup pipeline. You receive a deterministic static-signal report plus
+code excerpts for each piece of evidence. Your verdict complements the static score:
+you may confirm it, or move it by at most one level when the evidence justifies it.
+
+## Levels
+
+- **low** — the project needs a full reference implementation; a small rewrite will
+  not suffice. Automatic setup will fail or produce nothing provable.
+- **medium** — scoped configuration or customization is needed (summaries, munging,
+  harnesses for specific functions), but the path to an automatic proof is visible.
+- **high** — expected to pass autosetup as-is.
+
+## What makes a project LOW
+
+These patterns defeat the prover's core analyses (pointer analysis, memory
+partitioning, storage stride inference) or make the SMT problems intractable.
+Weigh them heavily when the excerpts confirm they are load-bearing (used in core
+logic), not incidental (one utility function):
+
+1. **Delegatecall trampolines** — manual calldata assembly forwarded via
+   `delegatecall` with `returndatacopy`-style result reads. Every forwarded call is
+   unresolvable; the proxied logic is outside the verified scene.
+2. **Free-memory-pointer manipulation** — `mstore(0x40, ...)` in application code;
+   scratch memory used as a first-class data structure.
+3. **Hand-rolled storage layouts** — `sload`/`sstore` on computed slots (keccak of
+   packed keys), custom packing behind wide bit masks instead of declared mappings
+   and structs. This breaks storage analysis at the preprocessing level.
+4. **Mixed bitvector + nonlinear arithmetic in single functions** — packed-field
+   decoding interleaved with mul/div price math, with no internal-function seams to
+   summarize each part separately.
+5. **Monolithic functions** — hundreds of lines in one body: no divide-and-conquer,
+   worst-case for both static analysis and SMT splitting.
+
+## What makes a project HIGH
+
+- Standard declared storage (mappings, structs), standard libraries — especially math
+  libraries with curated summaries (OZ Math, FullMath, prb-math, solady) — small
+  focused functions, bit operations (if any) encapsulated in small internal pure
+  accessors, loops bounded by constants, external calls through typed interfaces.
+
+## Judging discipline
+
+- **Cite or don't move.** To move the level from the static provisional you must cite
+  at least two concrete file:line evidences and say what in the excerpt justifies the
+  move. Otherwise return the static level.
+- **Load-bearing vs incidental.** A single assembly block in an ERC-20 `permit` is
+  incidental; the same block in the core swap path is disqualifying. Read the
+  excerpts, not just the counts.
+- **Compilation is already guaranteed** — the project compiled, or you would not be
+  running. Do not reward mere compilation.
+- **When torn between two levels, pick the lower one.** A false "high" sends a doomed
+  project into an expensive automatic pipeline; a false "medium" merely adds a human
+  look.
diff --git a/certora_autosetup/amenability/report.py b/certora_autosetup/amenability/report.py
new file mode 100644
index 0000000..82e3179
--- /dev/null
+++ b/certora_autosetup/amenability/report.py
@@ -0,0 +1,83 @@
+"""JSON output schema of certora-fv-amenability (single source of truth).
+
+The report is the tool's whole external contract: clients (SaaS, CI, humans)
+consume this JSON and nothing else. Every evidence item carries file:line so a
+reviewer can jump straight to the code that moved the score.
+"""
+
+from enum import Enum
+from typing import Any, Optional
+
+from pydantic import BaseModel, Field
+
+SCHEMA_VERSION = "1.0"
+
+LEVEL_SEMANTICS = {
+    "low": "needs a full reference implementation; a small rewrite will not suffice",
+    "medium": "scoped configuration/customization needed to get the automatic proof going",
+    "high": "expected to pass autosetup as-is",
+}
+
+
+class Level(str, Enum):
+    LOW = "low"
+    MEDIUM = "medium"
+    HIGH = "high"
+
+
+class Severity(str, Enum):
+    HIGH = "high"
+    MEDIUM = "medium"
+    LOW = "low"
+
+
+class Evidence(BaseModel):
+    signal: str
+    severity: Severity
+    file: str
+    line: int
+    function: Optional[str] = None
+    detail: str
+
+
+class SubScore(BaseModel):
+    score: float = Field(ge=0.0, le=1.0, description="1.0 = fully amenable")
+    weight: float
+    raw: dict[str, Any] = Field(default_factory=dict)
+
+
+class StaticReport(BaseModel):
+    provisional_level: Level
+    weighted_score: float
+    sub_scores: dict[str, SubScore]
+
+
+class Recommendation(BaseModel):
+    kind: str  # summary | harness | munge | reference-impl
+    detail: str
+
+
+class AmenabilityReport(BaseModel):
+    schema_version: str = SCHEMA_VERSION
+    tool_version: str
+    project: str
+    contracts_analyzed: list[str]
+    mode: str = "ast"
+    level: Level
+    confidence: float = Field(ge=0.0, le=1.0)
+    level_semantics: dict[str, str] = Field(default_factory=lambda: dict(LEVEL_SEMANTICS))
+    static: StaticReport
+    evidence: list[Evidence]
+    judge: Optional[dict[str, Any]] = None  # populated by the phase-2 LLM judge
+    recommendations: list[Recommendation] = Field(default_factory=list)
+
+
+class ScoringErrorReport(BaseModel):
+    """Emitted (with exit code 1) when the project cannot be scored at all —
+    most importantly when it does not compile: compiling is the amenability floor,
+    so there is no degraded scoring path."""
+
+    schema_version: str = SCHEMA_VERSION
+    project: str
+    error: str  # e.g. "does-not-compile", "no-ast-dump"
+    detail: str
diff --git a/certora_autosetup/amenability/scoring.py b/certora_autosetup/amenability/scoring.py
new file mode 100644
index 0000000..a32847e
--- /dev/null
+++ b/certora_autosetup/amenability/scoring.py
@@ -0,0 +1,83 @@
+"""Aggregate signal results into a level, driven entirely by weights.yaml.
+
+Level philosophy:
+- `low` is RARE — reserved for the profile that needs a full reference
+  implementation, where a small rewrite won't suffice (the whole execution model
+  is hand-assembled: delegatecall trampolines + hand-rolled storage layouts +
+  pervasive mixed-theory monoliths, several at once). It is decided by
+  CO-OCCURRENCE of multiple severe *structural* killers, not by a low mean.
+- `medium` is the default for a project with friction that autosetup can still
+  handle with scoped config (summaries, harnesses, linking, loop_iter).
+- `high` is a clean project that should pass as-is.
+"""
+
+from dataclasses import dataclass, field
+from pathlib import Path
+
+import yaml
+
+from certora_autosetup.amenability.report import Level, StaticReport, SubScore
+from certora_autosetup.amenability.signals.base import SignalResult
+
+DEFAULT_WEIGHTS = Path(__file__).parent / "weights.yaml"
+
+
+@dataclass
+class ScoringConfig:
+    weights: dict[str, float]
+    high_min: float
+    structural_killers: set[str]
+    killer_severe_score: float
+    killers_for_low: int
+    structural_low_max: float = field(default=0.5)
+
+    @classmethod
+    def load(cls, path: Path | str = DEFAULT_WEIGHTS) -> "ScoringConfig":
+        with open(path) as f:
+            data = yaml.safe_load(f)
+        thresholds = data["thresholds"]
+        hard = data["hard_rules"]
+        return cls(
+            weights=data["weights"],
+            high_min=thresholds["high_min"],
+            structural_killers=set(hard["structural_killers"]),
+            killer_severe_score=hard["killer_severe_score"],
+            killers_for_low=hard["killers_for_low"],
+            structural_low_max=thresholds.get("structural_low_max", 0.5),
+        )
+
+
+def aggregate(results: list[SignalResult], config: ScoringConfig) -> StaticReport:
+    sub_scores: dict[str, SubScore] = {}
+    weighted_sum = 0.0
+    weight_total = 0.0
+    severe_killers = 0
+
+    for r in results:
+        weight = config.weights.get(r.signal_id, 1.0)
+        sub_scores[r.signal_id] = SubScore(score=r.score, weight=weight, raw=r.raw)
+        weighted_sum += r.score * weight
+        weight_total += weight
+        if (r.signal_id in config.structural_killers
+                and r.score <= config.killer_severe_score):
+            severe_killers += 1
+
+    weighted = weighted_sum / weight_total if weight_total else 1.0
+
+    # `low` only when several structural killers fire together AND the overall
+    # picture is genuinely weak — the reference-implementation profile.
+    # `high` means clean: a strong mean AND no structural killer firing severely
+    # (even one hand-rolled-storage or trampoline site means autosetup needs
+    # scoped config, i.e. medium). Everything in between is medium.
+    if severe_killers >= config.killers_for_low and weighted < config.structural_low_max:
+        level = Level.LOW
+    elif weighted >= config.high_min and severe_killers == 0:
+        level = Level.HIGH
+    else:
+        level = Level.MEDIUM
+
+    return StaticReport(
+        provisional_level=level,
+        weighted_score=round(weighted, 4),
+        sub_scores=sub_scores,
+    )
diff --git a/certora_autosetup/amenability/signals/__init__.py b/certora_autosetup/amenability/signals/__init__.py
new file mode 100644
index 0000000..7732994
--- /dev/null
+++ b/certora_autosetup/amenability/signals/__init__.py
@@ -0,0 +1,31 @@
+"""Signal registry: the ordered list of all deterministic amenability signals."""
+
+from certora_autosetup.amenability.signals.arithmetic import mixed_theory, unchecked_nonlinear
+from certora_autosetup.amenability.signals.assembly import (
+    asm_density,
+    asm_fp_manipulation,
+    asm_trampoline,
+)
+from certora_autosetup.amenability.signals.bitmask import bitmask_style
+from certora_autosetup.amenability.signals.calls import external_call_surface
+from certora_autosetup.amenability.signals.functions import function_length, surface_shape
+from certora_autosetup.amenability.signals.loops import dynamic_loops
+from certora_autosetup.amenability.signals.storage import storage_packing
+from certora_autosetup.amenability.signals.summaries import curated_summary_hits
+
+ALL_SIGNALS = [
+    asm_density,
+    asm_fp_manipulation,
+    asm_trampoline,
+    bitmask_style,
+    function_length,
+    unchecked_nonlinear,
+    mixed_theory,
+    curated_summary_hits,
+    storage_packing,
+    external_call_surface,
+    dynamic_loops,
+    surface_shape,
+]
+
+__all__ = ["ALL_SIGNALS"]
diff --git a/certora_autosetup/amenability/signals/arithmetic.py b/certora_autosetup/amenability/signals/arithmetic.py
new file mode 100644
index 0000000..cb7e04f
--- /dev/null
+++ b/certora_autosetup/amenability/signals/arithmetic.py
@@ -0,0 +1,129 @@
+"""Arithmetic signals: unchecked nonlinear math (S6) and mixed
+bitvector+nonlinear theory in a single function (S7).
+
+Prover impact: nonlinear integer arithmetic (mul/div chains with symbolic
+operands) is the classic SMT blowup; combining it with bitvector operations in
+the same function forces the solver to reason across theories with no clean cut,
+and prevents proving each part modularly via internal-function summaries.
+"""
+
+from certora_autosetup.amenability.context import AnalysisContext
+from certora_autosetup.amenability.report import Severity
+from certora_autosetup.amenability.signals.base import SignalResult, clamp, make_evidence, signal
+from certora_autosetup.solidity_ast import (
+    BinaryOperation,
+    FunctionCall,
+    Identifier,
+    InlineAssembly,
+    Literal,
+    UnaryOperation,
+    UncheckedBlock,
+    YulFunctionCall,
+    find_all,
+)
+
+NONLINEAR_OPS = {"*", "/", "%", "**"}
+BITVECTOR_OPS = {"&", "|", "^", "<<", ">>"}
+YUL_NONLINEAR = {"mul", "div", "sdiv", "mod", "smod", "mulmod", "exp"}
+YUL_BITVECTOR = {"and", "or", "xor", "not", "shl", "shr", "sar", "byte"}
+EVIDENCE_CAP = 10
+
+
+def _is_constant_operand(expr) -> bool:
+    """Cheap constness: literals and SCREAMING_CASE identifiers (constants by
+    convention). Full referencedDeclaration resolution is a later refinement."""
+    if isinstance(expr, Literal):
+        return True
+    if isinstance(expr, Identifier):
+        name = expr.name
+        return bool(name) and name.upper() == name and any(c.isalpha() for c in name)
+    return False
+
+
+@signal("unchecked_nonlinear")
+def unchecked_nonlinear(ctx: AnalysisContext) -> SignalResult:
+    sites = 0
+    evidence = []
+    for path, contract, fn in ctx.iter_functions():
+        if fn.body is None:
+            continue
+        for block in find_all(fn, UncheckedBlock):
+            for op in find_all(block, BinaryOperation):
+                if op.operator not in NONLINEAR_OPS:
+                    continue
+                if _is_constant_operand(op.leftExpression) or _is_constant_operand(op.rightExpression):
+                    continue
+                sites += 1
+                if len(evidence) < EVIDENCE_CAP:
+                    evidence.append(make_evidence(
+                        ctx, "unchecked_nonlinear", Severity.MEDIUM, path,
+                        op.src_location.offset,
+                        f"unchecked nonlinear `{op.operator}` with symbolic operands",
+                        function=f"{contract.name}.{fn.name or fn.kind}",
+                    ))
+    # Unchecked nonlinear arithmetic makes the SMT harder but is config/summary
+    # solvable (medium), not a rewrite trigger — floor at 0.35.
+    return SignalResult(
+        signal_id="unchecked_nonlinear",
+        score=clamp(1.0 - sites / 25.0) * 0.65 + 0.35,
+        evidence=evidence,
+        raw={"sites": sites},
+    )
+
+
+def _count_ops(fn) -> tuple[int, int]:
+    bv = 0
+    nl = 0
+    for op in find_all(fn, BinaryOperation):
+        if op.operator in BITVECTOR_OPS:
+            bv += 1
+        elif op.operator in NONLINEAR_OPS:
+            nl += 1
+    for op in find_all(fn, UnaryOperation):
+        if op.operator == "~":
+            bv += 1
+    for call in find_all(fn, FunctionCall):
+        callee = call.expression
+        if isinstance(callee, Identifier) and callee.name in ("mulmod", "addmod"):
+            nl += 1
+    for block in find_all(fn, InlineAssembly):
+        if block.AST is None:
+            continue
+        for ycall in find_all(block.AST, YulFunctionCall):
+            name = ycall.functionName.name
+            if name in YUL_BITVECTOR:
+                bv += 1
+            elif name in YUL_NONLINEAR:
+                nl += 1
+    return bv, nl
+
+
+@signal("mixed_theory")
+def mixed_theory(ctx: AnalysisContext) -> SignalResult:
+    flagged = 0
+    evidence = []
+    per_fn = {}
+    for path, contract, fn in ctx.iter_functions():
+        if fn.body is None:
+            continue
+        bv, nl = _count_ops(fn)
+        if min(bv, nl) >= 3:
+            flagged += 1
+            label = f"{contract.name}.{fn.name or fn.kind}"
+            per_fn[label] = {"bitvector_ops": bv, "nonlinear_ops": nl}
+            if len(evidence) < EVIDENCE_CAP:
+                evidence.append(make_evidence(
+                    ctx, "mixed_theory", Severity.HIGH, path, fn.src_location.offset,
+                    f"{bv} bitvector + {nl} nonlinear ops interleaved in one function "
+                    "(no internal-function seam to separate the theories)",
+                    function=label,
+                ))
+    # Mixed bitvector+nonlinear theory in one function is a real SMT hazard, but
+    # only pervasive mixing is disqualifying; a handful of such functions is
+    # medium. Floor at 0.3.
+    return SignalResult(
+        signal_id="mixed_theory",
+        score=clamp(1.0 - flagged / 12.0) * 0.7 + 0.3,
+        evidence=evidence,
+        raw={"flagged_functions": flagged, "per_function": per_fn},
+    )
diff --git a/certora_autosetup/amenability/signals/assembly.py b/certora_autosetup/amenability/signals/assembly.py
new file mode 100644
index 0000000..46be57c
--- /dev/null
+++ b/certora_autosetup/amenability/signals/assembly.py
@@ -0,0 +1,206 @@
+"""Assembly signals: density (S1), free-memory-pointer manipulation (S2),
+delegatecall trampolines (S3).
+
+Prover impact: inline assembly defeats memory partitioning and pointer analysis;
+writes to the free-memory pointer (0x40) make scratch memory a first-class object
+the analyses cannot model; delegatecall trampolines built from manual calldata +
+returndatacopy leave every forwarded call unresolvable.
+"""
+
+from certora_autosetup.amenability.context import AnalysisContext
+from certora_autosetup.amenability.report import Severity
+from certora_autosetup.amenability.signals.base import (
+    SignalResult,
+    clamp,
+    containing_function_penalty,
+    make_evidence,
+    signal,
+)
+from certora_autosetup.solidity_ast import (
+    InlineAssembly,
+    MemberAccess,
+    YulFunctionCall,
+    YulLiteralHexValue,
+    YulLiteralValue,
+    find_all,
+)
+
+FREE_MEMORY_POINTER = 0x40
+SCRATCH_SLOTS = (0x00, 0x20)
+
+EVIDENCE_CAP = 10  # per signal; raw counters always carry the full totals
+
+
+def _yul_literal_int(node) -> int | None:
+    if isinstance(node, (YulLiteralValue, YulLiteralHexValue)):
+        v = getattr(node, "value", None) or getattr(node, "hexValue", None)
+        if isinstance(v, str):
+            try:
+                return int(v, 0) if not v.startswith("0x") else int(v, 16)
+            except ValueError:
+                return None
+    return None
+
+
+@signal("asm_density")
+def asm_density(ctx: AnalysisContext) -> SignalResult:
+    total_fns = 0
+    fns_with_asm = 0
+    scoped_asm_fns = 0  # assembly living in a small internal/private helper
+    total_blocks = 0
+    untyped_blocks = 0  # solc < 0.6: no typed Yul AST, only the `operations` text
+    weighted_asm_fns = 0.0  # functions-with-asm, weighted by how interwoven they are
+    evidence = []
+    for path, contract, fn in ctx.iter_functions():
+        total_fns += 1
+        blocks = list(find_all(fn, InlineAssembly)) if fn.body is not None else []
+        if not blocks:
+            continue
+        fns_with_asm += 1
+        total_blocks += len(blocks)
+        untyped_blocks += sum(1 for b in blocks if b.AST is None)
+        penalty = containing_function_penalty(ctx, path, fn)
+        weighted_asm_fns += penalty
+        if penalty <= 0.2:
+            scoped_asm_fns += 1
+        elif len(evidence) < EVIDENCE_CAP:
+            # only surface assembly that isn't a clean scoped helper
+            evidence.append(make_evidence(
+                ctx, "asm_density", Severity.LOW, path, fn.src_location.offset,
+                f"{len(blocks)} inline-assembly block(s) interwoven with other code",
+                function=f"{contract.name}.{fn.name or fn.kind}",
+            ))
+    # Density measured on the interwoven weight, not the raw count: assembly
+    # confined to small internal/private helpers barely moves the score.
+    ratio = weighted_asm_fns / total_fns if total_fns else 0.0
+    return SignalResult(
+        signal_id="asm_density",
+        score=clamp(1.0 - 3.0 * ratio),
+        evidence=evidence,
+        raw={"functions": total_fns, "functions_with_asm": fns_with_asm,
+             "scoped_asm_helpers": scoped_asm_fns,
+             "weighted_asm_functions": round(weighted_asm_fns, 2),
+             "asm_blocks": total_blocks, "untyped_asm_blocks": untyped_blocks},
+    )
+
+
+@signal("asm_fp_manipulation")
+def asm_fp_manipulation(ctx: AnalysisContext) -> SignalResult:
+    fp_writes = 0
+    scratch_writes = 0
+    interwoven_fp_writes = 0   # fp writes NOT confined to a small scoped helper
+    evidence = []
+    for path, contract, fn in ctx.iter_functions():
+        if fn.body is None:
+            continue
+        penalty = containing_function_penalty(ctx, path, fn)
+        for block in find_all(fn, InlineAssembly):
+            if block.AST is None:
+                continue
+            for call in find_all(block.AST, YulFunctionCall):
+                if call.functionName.name != "mstore" or not call.arguments:
+                    continue
+                target = _yul_literal_int(call.arguments[0])
+                if target == FREE_MEMORY_POINTER:
+                    fp_writes += 1
+                    if penalty > 0.2:
+                        interwoven_fp_writes += 1
+                        if len(evidence) < EVIDENCE_CAP:
+                            evidence.append(make_evidence(
+                                ctx, "asm_fp_manipulation", Severity.HIGH, path,
+                                call.src_location.offset,
+                                "mstore(0x40, ...) — free-memory pointer written by hand, "
+                                "interwoven with other code",
+                                function=f"{contract.name}.{fn.name or fn.kind}",
+                            ))
+                elif target in SCRATCH_SLOTS and penalty > 0.2:
+                    scratch_writes += 1
+                    if len(evidence) < EVIDENCE_CAP:
+                        evidence.append(make_evidence(
+                            ctx, "asm_fp_manipulation", Severity.MEDIUM, path,
+                            call.src_location.offset,
+                            f"mstore({hex(target)}, ...) — scratch-space write",
+                            function=f"{contract.name}.{fn.name or fn.kind}",
+                        ))
+    # Only free-memory-pointer manipulation OUTSIDE a small scoped helper is a
+    # real hazard — the same mstore(0x40) inside a focused internal helper (the
+    # common OZ/solady pattern) is tractable. Scale with how much of it there is:
+    # a single interwoven write is medium-ish; pervasive FP surgery craters the
+    # score.
+    score = 1.0
+    if scratch_writes:
+        score = 0.7
+    if fp_writes and not interwoven_fp_writes:
+        score = 0.7   # fp writes exist but only in scoped helpers
+    if interwoven_fp_writes:
+        score = clamp(0.45 - 0.08 * (interwoven_fp_writes - 1))
+    return SignalResult(
+        signal_id="asm_fp_manipulation",
+        score=score,
+        evidence=evidence,
+        raw={"fp_writes": fp_writes, "interwoven_fp_writes": interwoven_fp_writes,
+             "scratch_writes": scratch_writes},
+    )
+
+
+@signal("asm_trampoline")
+def asm_trampoline(ctx: AnalysisContext) -> SignalResult:
+    asm_delegatecalls = 0
+    asm_calls = 0
+    solidity_delegatecalls = 0
+    # Weighted "hard forwarding": a delegatecall in a small dedicated proxy helper
+    # (the standard EIP-1967 pattern) is far more tractable than manual
+    # calldata/delegatecall interwoven with business logic in a big function.
+    weighted_hard = 0.0
+    weighted_asm_calls = 0.0
+    evidence = []
+    for path, contract, fn in ctx.iter_functions():
+        if fn.body is None:
+            continue
+        fn_label = f"{contract.name}.{fn.name or fn.kind}"
+        penalty = containing_function_penalty(ctx, path, fn)
+        for block in find_all(fn, InlineAssembly):
+            if block.AST is None:
+                continue
+            for call in find_all(block.AST, YulFunctionCall):
+                name = call.functionName.name
+                if name in ("delegatecall", "callcode"):
+                    asm_delegatecalls += 1
+                    weighted_hard += penalty
+                    if penalty > 0.2 and len(evidence) < EVIDENCE_CAP:
+                        evidence.append(make_evidence(
+                            ctx, "asm_trampoline", Severity.HIGH, path,
+                            call.src_location.offset,
+                            f"assembly {name} — manual call forwarding interwoven with "
+                            "other code, unresolvable by the prover",
+                            function=fn_label,
+                        ))
+                elif name in ("call", "staticcall"):
+                    asm_calls += 1
+                    weighted_asm_calls += penalty
+                    if penalty > 0.2 and len(evidence) < EVIDENCE_CAP:
+                        evidence.append(make_evidence(
+                            ctx, "asm_trampoline", Severity.MEDIUM, path,
+                            call.src_location.offset,
+                            f"assembly {name}", function=fn_label,
+                        ))
+        for member in find_all(fn, MemberAccess):
+            if member.memberName == "delegatecall":
+                solidity_delegatecalls += 1
+                weighted_hard += penalty
+                if penalty > 0.2 and len(evidence) < EVIDENCE_CAP:
+                    evidence.append(make_evidence(
+                        ctx, "asm_trampoline", Severity.HIGH, path,
+                        member.src_location.offset,
+                        "low-level .delegatecall — proxied logic outside the verified scene",
+                        function=fn_label,
+                    ))
+    score = clamp(1.0 - 0.4 * weighted_hard - 0.1 * weighted_asm_calls)
+    return SignalResult(
+        signal_id="asm_trampoline",
+        score=score,
+        evidence=evidence,
+        raw={"asm_delegatecalls": asm_delegatecalls, "asm_calls": asm_calls,
+             "solidity_delegatecalls": solidity_delegatecalls,
+             "weighted_hard_forwarding": round(weighted_hard, 2)},
+    )
diff --git a/certora_autosetup/amenability/signals/base.py b/certora_autosetup/amenability/signals/base.py
new file mode 100644
index 0000000..a80d194
--- /dev/null
+++ b/certora_autosetup/amenability/signals/base.py
@@ -0,0 +1,80 @@
+"""Signal protocol: each signal is a pure function over the AnalysisContext.
+
+Scores are normalized to [0, 1] with 1 = fully amenable, so aggregation is a
+plain weighted mean and weights.yaml stays the only tuning surface.
+"""
+
+from dataclasses import dataclass, field
+from typing import Any, Callable, Protocol
+
+from certora_autosetup.amenability.context import AnalysisContext
+from certora_autosetup.amenability.report import Evidence, Severity
+
+
+@dataclass
+class SignalResult:
+    signal_id: str
+    score: float  # [0,1], 1 = amenable
+    evidence: list[Evidence] = field(default_factory=list)
+    raw: dict[str, Any] = field(default_factory=dict)
+
+
+class Signal(Protocol):
+    signal_id: str
+
+    def __call__(self, ctx: AnalysisContext) -> SignalResult: ...
+
+
+def make_evidence(
+    ctx: AnalysisContext,
+    signal_id: str,
+    severity: Severity,
+    source_path: str,
+    byte_offset: int,
+    detail: str,
+    function: str | None = None,
+) -> Evidence:
+    return Evidence(
+        signal=signal_id,
+        severity=severity,
+        file=ctx.display_path(source_path),
+        line=ctx.offset_to_line(source_path, byte_offset),
+        function=function,
+        detail=detail,
+    )
+
+
+def clamp(x: float) -> float:
+    return max(0.0, min(1.0, x))
+
+
+# Assembly (and other low-level constructs) are far more tractable when scoped
+# into a small internal/private helper — a focused, summarizable seam — than when
+# interwoven with substantial other code in a large or externally-visible
+# function. This weight scales a construct's penalty by how well-scoped its
+# containing function is: ~0 for a clean helper, 1.0 for the interwoven case.
+SCOPED_HELPER_LINES = 20
+
+
+def containing_function_penalty(ctx, source_path: str, fn) -> float:
+    """Penalty multiplier in [0.15, 1.0] for a low-level construct living in `fn`,
+    based on how well-scoped the function is (visibility + size)."""
+    loc = fn.src_location
+    lines = ctx.line_span(source_path, loc.offset, loc.length)
+    small = 0 < lines <= SCOPED_HELPER_LINES
+    internal = fn.visibility in ("internal", "private")
+    if internal and small:
+        return 0.15   # the sanctioned pattern: a small scoped helper
+    if internal or small:
+        return 0.55   # one of the two — partially scoped
+    return 1.0        # large AND externally visible: interwoven with other logic
+
+
+def signal(signal_id: str) -> Callable[[Callable[[AnalysisContext], SignalResult]], Callable[[AnalysisContext], SignalResult]]:
+    """Attach the id to the function so the registry can enumerate it."""
+
+    def deco(fn: Callable[[AnalysisContext], SignalResult]) -> Callable[[AnalysisContext], SignalResult]:
+        fn.signal_id = signal_id  # type: ignore[attr-defined]
+        return fn
+
+    return deco
diff --git a/certora_autosetup/amenability/signals/bitmask.py b/certora_autosetup/amenability/signals/bitmask.py
new file mode 100644
index 0000000..3d7654f
--- /dev/null
+++ b/certora_autosetup/amenability/signals/bitmask.py
@@ -0,0 +1,85 @@
+"""Bit-mask style signal (S4): opaque mask constants and inline bit-surgery
+versus encapsulated accessor functions.
+
+Prover impact: packed fields decoded inline with wide hex masks produce deep
+bitvector terms at every use site; the same packing behind small internal pure
+accessors gives the prover (and a human summarizer) one seam per field.
+"""
+
+import re
+
+from certora_autosetup.amenability.context import AnalysisContext
+from certora_autosetup.amenability.report import Severity
+from certora_autosetup.amenability.signals.base import SignalResult, clamp, make_evidence, signal
+from certora_autosetup.solidity_ast import (
+    BinaryOperation,
+    Literal,
+    UnaryOperation,
+    walk,
+    find_all,
+)
+
+BIT_OPS = {"&", "|", "^", "<<", ">>"}
+# Mask-like: >= 16 hex digits and dominated by f/0 nibbles (bit-range masks decode
+# to runs of f/0 with at most a few partial nibbles at the boundaries).
+_HEX_RE = re.compile(r"^0x[0-9a-fA-F]{16,}$")
+ACCESSOR_MAX_NODES = 60  # node-count bound for "small accessor" classification
+EVIDENCE_CAP = 10
+
+
+def _is_mask_literal(lit: Literal) -> bool:
+    v = lit.value or ""
+    if not _HEX_RE.match(v):
+        return False
+    digits = v[2:].lower()
+    f0 = sum(1 for c in digits if c in "f0")
+    return f0 / len(digits) >= 0.7
+
+
+@signal("bitmask_style")
+def bitmask_style(ctx: AnalysisContext) -> SignalResult:
+    mask_literals = 0
+    accessor_bitops = 0
+    inline_bitops = 0
+    evidence = []
+    for path, contract, fn in ctx.iter_functions():
+        if fn.body is None:
+            continue
+        bitops = [op for op in find_all(fn, BinaryOperation) if op.operator in BIT_OPS]
+        bitops += [op for op in find_all(fn, UnaryOperation) if op.operator == "~"]
+        if not bitops:
+            continue
+        for op in find_all(fn, BinaryOperation):
+            for side in (op.leftExpression, op.rightExpression):
+                if isinstance(side, Literal) and _is_mask_literal(side):
+                    mask_literals += 1
+        is_accessor = (
+            fn.visibility in ("internal", "private")
+            and fn.stateMutability in ("pure", "view")
+            and sum(1 for _ in walk(fn.body)) <= ACCESSOR_MAX_NODES
+        )
+        if is_accessor:
+            accessor_bitops += len(bitops)
+        else:
+            inline_bitops += len(bitops)
+            if len(evidence) < EVIDENCE_CAP and len(bitops) >= 5:
+                evidence.append(make_evidence(
+                    ctx, "bitmask_style", Severity.MEDIUM, path, fn.src_location.offset,
+                    f"{len(bitops)} bit operations inline (not behind a small internal accessor)",
+                    function=f"{contract.name}.{fn.name or fn.kind}",
+                ))
+    total = accessor_bitops + inline_bitops
+    inline_ratio = inline_bitops / total if total else 0.0
+    # Bit operations are bitvector-theory work — harder but tractable (medium),
+    # even in volume, unless they're also unencapsulated. Penalize volume *
+    # inline-ness but floor at 0.35 so bit-heavy code doesn't read as a rewrite.
+    volume_factor = clamp(total / 120.0)
+    score = clamp(1.0 - inline_ratio * volume_factor) * 0.65 + 0.35
+    return SignalResult(
+        signal_id="bitmask_style",
+        score=score,
+        evidence=evidence,
+        raw={"bit_ops": total, "inline_bit_ops": inline_bitops,
+             "accessor_bit_ops": accessor_bitops, "mask_literals": mask_literals,
+             "inline_ratio": round(inline_ratio, 3)},
+    )
diff --git a/certora_autosetup/amenability/signals/calls.py b/certora_autosetup/amenability/signals/calls.py
new file mode 100644
index 0000000..d20bffe
--- /dev/null
+++ b/certora_autosetup/amenability/signals/calls.py
@@ -0,0 +1,43 @@
+"""External-call surface signal (S10): low-level calls and try/call dispatch.
+
+Prover impact: each low-level call is an unresolved callee the call-resolution
+loop must chase (or havoc); address-indexed dispatch multiplies that. Complements
+S3, which scores the delegatecall-trampoline shape specifically.
+"""
+
+from certora_autosetup.amenability.context import AnalysisContext
+from certora_autosetup.amenability.report import Severity
+from certora_autosetup.amenability.signals.base import SignalResult, clamp, make_evidence, signal
+from certora_autosetup.solidity_ast import MemberAccess, TryStatement, find_all
+
+LOW_LEVEL = {"call", "delegatecall", "staticcall"}
+EVIDENCE_CAP = 10
+
+
+@signal("external_call_surface")
+def external_call_surface(ctx: AnalysisContext) -> SignalResult:
+    low_level_calls = 0
+    try_statements = 0
+    evidence = []
+    for path, contract, fn in ctx.iter_functions():
+        if fn.body is None:
+            continue
+        for member in find_all(fn, MemberAccess):
+            # Low-level members appear as MemberAccess on an address expression.
+            if member.memberName in LOW_LEVEL:
+                low_level_calls += 1
+                if len(evidence) < EVIDENCE_CAP:
+                    evidence.append(make_evidence(
+                        ctx, "external_call_surface", Severity.LOW, path,
+                        member.src_location.offset,
+                        f"low-level .{member.memberName}",
+                        function=f"{contract.name}.{fn.name or fn.kind}",
+                    ))
+        try_statements += sum(1 for _ in find_all(fn, TryStatement))
+    score = clamp(1.0 - low_level_calls / 20.0)
+    return SignalResult(
+        signal_id="external_call_surface",
+        score=score,
+        evidence=evidence,
+        raw={"low_level_calls": low_level_calls, "try_statements": try_statements},
+    )
diff --git a/certora_autosetup/amenability/signals/functions.py b/certora_autosetup/amenability/signals/functions.py
new file mode 100644
index 0000000..fafdc41
--- /dev/null
+++ b/certora_autosetup/amenability/signals/functions.py
@@ -0,0 +1,76 @@
+"""Function-shape signals: length distribution (S5) and surface-shape
+normalizers (S12).
+
+Prover impact: a 500-line function is one giant TAC body — no divide-and-conquer
+via internal-function summaries, worst-case pattern-matching and SMT splitting.
+S12 carries scene-size counters used to normalize other signals; it does not
+judge on its own (weight 0 by default).
+"""
+
+from certora_autosetup.amenability.context import AnalysisContext
+from certora_autosetup.amenability.report import Severity
+from certora_autosetup.amenability.signals.base import SignalResult, clamp, make_evidence, signal
+
+LINES_FLAG = 150
+LINES_FLOOR = 600  # at/above this, the length score bottoms out
+EVIDENCE_CAP = 10
+
+
+@signal("function_length")
+def function_length(ctx: AnalysisContext) -> SignalResult:
+    spans = []
+    flagged = []
+    evidence = []
+    for path, contract, fn in ctx.iter_functions():
+        if fn.body is None:
+            continue
+        loc = fn.src_location
+        span = ctx.line_span(path, loc.offset, loc.length)
+        if span == 0:
+            continue  # source text unavailable
+        label = f"{contract.name}.{fn.name or fn.kind}"
+        spans.append(span)
+        if span > LINES_FLAG:
+            flagged.append({"function": label, "lines": span})
+            if len(evidence) < EVIDENCE_CAP:
+                evidence.append(make_evidence(
+                    ctx, "function_length",
+                    Severity.HIGH if span >= LINES_FLOOR / 2 else Severity.MEDIUM,
+                    path, loc.offset, f"{span}-line function", function=label,
+                ))
+    if not spans:
+        return SignalResult("function_length", 1.0, [], {"functions": 0})
+    longest = max(spans)
+    spans.sort()
+    p90 = spans[int(0.9 * (len(spans) - 1))]
+    # 1.0 while the longest fits the flag bound, 0.0 at LINES_FLOOR.
+    score = clamp(1.0 - (longest - LINES_FLAG) / (LINES_FLOOR - LINES_FLAG))
+    return SignalResult(
+        signal_id="function_length",
+        score=score,
+        evidence=evidence,
+        raw={"functions": len(spans), "max_lines": longest, "p90_lines": p90,
+             "flagged": flagged[:20]},
+    )
+
+
+@signal("surface_shape")
+def surface_shape(ctx: AnalysisContext) -> SignalResult:
+    contracts = 0
+    external_fns = 0
+    max_inheritance = 0
+    for _, contract in ctx.iter_contracts():
+        if contract.contractKind != "contract":
+            continue
+        contracts += 1
+        max_inheritance = max(max_inheritance, len(contract.linearizedBaseContracts))
+    for _, _, fn in ctx.iter_functions():
+        if fn.visibility in ("external", "public"):
+            external_fns += 1
+    return SignalResult(
+        signal_id="surface_shape",
+        score=1.0,  # informational normalizer; weight 0 in weights.yaml
+        evidence=[],
+        raw={"contracts": contracts, "external_or_public_functions": external_fns,
+             "max_inheritance_chain": max_inheritance},
+    )
diff --git a/certora_autosetup/amenability/signals/loops.py b/certora_autosetup/amenability/signals/loops.py
new file mode 100644
index 0000000..4cb40e1
--- /dev/null
+++ b/certora_autosetup/amenability/signals/loops.py
@@ -0,0 +1,81 @@
+"""Dynamic-loop signal (S11): loops whose bound is not a compile-time constant.
+
+Prover impact: every dynamic loop is unrolled to loop_iter and either loses
+soundness (optimistic) or explodes the formula; storage-length-bounded loops
+additionally drag storage reasoning into every iteration.
+"""
+
+from certora_autosetup.amenability.context import AnalysisContext
+from certora_autosetup.amenability.report import Severity
+from certora_autosetup.amenability.signals.base import SignalResult, clamp, make_evidence, signal
+from certora_autosetup.solidity_ast import (
+    DoWhileStatement,
+    ForStatement,
+    Identifier,
+    InlineAssembly,
+    MemberAccess,
+    WhileStatement,
+    YulForLoop,
+    find_all,
+    walk,
+)
+
+EVIDENCE_CAP = 10
+
+
+def _condition_is_dynamic(condition) -> tuple[bool, bool]:
+    """(dynamic, storage_length_bound) for a loop condition subtree."""
+    if condition is None:
+        return True, False  # `for(;;)` / missing condition: bounded only by breaks
+    dynamic = False
+    length_bound = False
+    for node in walk(condition):
+        if isinstance(node, MemberAccess) and node.memberName == "length":
+            dynamic = True
+            length_bound = True
+        elif isinstance(node, Identifier):
+            name = node.name or ""
+            if name.upper() != name:  # non-SCREAMING_CASE identifier = not a constant
+                dynamic = True
+        # Literals and constants keep the loop static.
+    return dynamic, length_bound
+
+
+@signal("dynamic_loops")
+def dynamic_loops(ctx: AnalysisContext) -> SignalResult:
+    dynamic = 0
+    length_bounded = 0
+    yul_loops = 0
+    evidence = []
+    for path, contract, fn in ctx.iter_functions():
+        if fn.body is None:
+            continue
+        label = f"{contract.name}.{fn.name or fn.kind}"
+        for loop in find_all(fn, (ForStatement, WhileStatement, DoWhileStatement)):
+            cond = getattr(loop, "condition", None)
+            is_dyn, is_len = _condition_is_dynamic(cond)
+            if not is_dyn:
+                continue
+            dynamic += 1
+            length_bounded += int(is_len)
+            if len(evidence) < EVIDENCE_CAP:
+                evidence.append(make_evidence(
+                    ctx, "dynamic_loops",
+                    Severity.MEDIUM if is_len else Severity.LOW,
+                    path, loop.src_location.offset,
+                    "storage-length-bounded loop" if is_len else "dynamically bounded loop",
+                    function=label,
+                ))
+        for block in find_all(fn, InlineAssembly):
+            if block.AST is not None:
+                yul_loops += sum(1 for _ in find_all(block.AST, YulForLoop))
+    # Dynamically-bounded loops are ubiquitous in real contracts and the prover
+    # handles them with loop_iter (a config knob, not a rewrite) — so this is a
+    # gentle friction signal, not a disqualifier. It floors at 0.4, never 0.
+    return SignalResult(
+        signal_id="dynamic_loops",
+        score=clamp(1.0 - dynamic / 60.0) * 0.6 + 0.4,
+        evidence=evidence,
+        raw={"dynamic_loops": dynamic, "storage_length_bounded": length_bounded,
+             "yul_for_loops": yul_loops},
+    )
diff --git a/certora_autosetup/amenability/signals/storage.py b/certora_autosetup/amenability/signals/storage.py
new file mode 100644
index 0000000..782fb4f
--- /dev/null
+++ b/certora_autosetup/amenability/signals/storage.py
@@ -0,0 +1,87 @@
+"""Storage-packing style signal (S9): standard declarations vs sanctioned slot
+patterns vs opaque hand-rolled layouts.
+
+Prover impact: the storage analysis infers a storage tree from standard
+declarations; computed-slot assembly access (hand-rolled mappings, custom
+packing behind raw sstore/sload) breaks stride inference — empirically a whole
+preprocessing-phase blowup, not just imprecision.
+"""
+
+from certora_autosetup.amenability.context import AnalysisContext
+from certora_autosetup.amenability.report import Severity
+from certora_autosetup.amenability.signals.base import SignalResult, clamp, make_evidence, signal
+from certora_autosetup.solidity_ast import (
+    InlineAssembly,
+    YulAssignment,
+    YulFunctionCall,
+    YulIdentifier,
+    YulLiteralHexValue,
+    YulLiteralValue,
+    YulVariableDeclaration,
+    find_all,
+)
+
+EVIDENCE_CAP = 10
+
+
+def _computed_yul_vars(block_ast) -> set[str]:
+    """Names of Yul variables whose (last) assigned value is a function call —
+    i.e. computed slots (keccak256, arithmetic), as opposed to `x.slot`
+    external references or plain literals."""
+    computed: set[str] = set()
+    for decl in find_all(block_ast, YulVariableDeclaration):
+        if isinstance(getattr(decl, "value", None), YulFunctionCall):
+            for var in decl.variables:
+                computed.add(var.name)
+    for assign in find_all(block_ast, YulAssignment):
+        if isinstance(assign.value, YulFunctionCall):
+            for target in assign.variableNames:
+                computed.add(target.name)
+    return computed
+
+
+@signal("storage_packing")
+def storage_packing(ctx: AnalysisContext) -> SignalResult:
+    computed_slot_accesses = 0
+    literal_slot_accesses = 0
+    evidence = []
+    for path, contract, fn in ctx.iter_functions():
+        if fn.body is None:
+            continue
+        for block in find_all(fn, InlineAssembly):
+            if block.AST is None:
+                continue
+            computed_vars = _computed_yul_vars(block.AST)
+            for call in find_all(block.AST, YulFunctionCall):
+                name = call.functionName.name
+                if name not in ("sstore", "sload", "tstore", "tload"):
+                    continue
+                slot_arg = call.arguments[0] if call.arguments else None
+                if isinstance(slot_arg, (YulLiteralValue, YulLiteralHexValue)):
+                    literal_slot_accesses += 1
+                    continue
+                # Identifier slots referencing a declared var (`x.slot` external
+                # reference) are the sanctioned pattern; anything computed
+                # (keccak output, arithmetic) — directly or via a local Yul
+                # variable — is opaque.
+                computed = isinstance(slot_arg, YulFunctionCall) or (
+                    isinstance(slot_arg, YulIdentifier) and slot_arg.name in computed_vars
+                )
+                if computed:
+                    computed_slot_accesses += 1
+                    if len(evidence) < EVIDENCE_CAP:
+                        evidence.append(make_evidence(
+                            ctx, "storage_packing", Severity.HIGH, path,
+                            call.src_location.offset,
+                            f"{name} with a computed slot expression — hand-rolled "
+                            "storage layout the storage analysis cannot model",
+                            function=f"{contract.name}.{fn.name or fn.kind}",
+                        ))
+    score = clamp(1.0 - 0.25 * computed_slot_accesses)
+    return SignalResult(
+        signal_id="storage_packing",
+        score=score,
+        evidence=evidence,
+        raw={"computed_slot_accesses": computed_slot_accesses,
+             "literal_slot_accesses": literal_slot_accesses},
+    )
diff --git a/certora_autosetup/amenability/signals/summaries.py b/certora_autosetup/amenability/signals/summaries.py
new file mode 100644
index 0000000..207f6f6
--- /dev/null
+++ b/certora_autosetup/amenability/signals/summaries.py
@@ -0,0 +1,95 @@
+"""Curated-summary signal (S8): does the project use math libraries autosetup
+already has curated CVL summaries for — or hand-rolled equivalents?
+
+Prover impact: a curated library (OZ Math, FullMath, prb-math, ...) gets its
+nonlinear kernels summarized away automatically; a hand-rolled mulDiv/sqrt is
+raw nonlinear SMT with no ready summary.
+"""
+
+import json
+from functools import lru_cache
+from pathlib import Path
+
+from certora_autosetup.amenability.context import AnalysisContext, is_dependency_path
+from certora_autosetup.amenability.report import Severity
+from certora_autosetup.amenability.signals.base import SignalResult, make_evidence, signal
+from certora_autosetup.solidity_ast import FunctionDefinition
+
+SUMMARIES_REGISTRY = (
+    Path(__file__).resolve().parents[2] / "setup" / "function_summaries.json"
+)
+# The only names whose hand-rolled reimplementation is a genuine amenability
+# signal: nonlinear fixed-point / full-precision math primitives that the prover
+# summarizes away when they come from a curated library but must reason about
+# fully when reimplemented. Everything else in the registry (toString, safeTransfer,
+# toUint*, get/set, extsload, ...) collides with unrelated helpers and is NOT
+# evidence of a hard-to-verify math kernel.
+MATH_KERNEL_NAMES = {
+    "mulDiv", "fullMulDiv", "mulDivUp", "fullMulDivUp",
+    "mulWad", "divWad", "mulWadUp", "divWadUp", "sMulWad", "sDivWad",
+    "powWad", "expWad", "lnWad", "log2", "log10", "log2Up",
+    "rpow", "rmul", "rdiv", "sqrt", "cbrt", "fixedPointMul",
+}
+EVIDENCE_CAP = 10
+
+
+@lru_cache(maxsize=1)
+def _registry() -> dict:
+    with open(SUMMARIES_REGISTRY) as f:
+        return json.load(f)
+
+
+@signal("curated_summary_hits")
+def curated_summary_hits(ctx: AnalysisContext) -> SignalResult:
+    registry = _registry()
+    curated_libraries: dict[str, set[str]] = {}
+    for entry in registry.values():
+        for lib in entry.get("library_names", []):
+            curated_libraries.setdefault(lib, set()).update(entry.get("names", []))
+
+    hits: list[str] = []
+    hand_rolled: list[str] = []
+    evidence = []
+
+    # Positive: any library in the scene (dependencies included — that is where
+    # they live) matching a curated entry by name + function overlap.
+    for path, contract in ctx.iter_contracts(include_dependencies=True):
+        if contract.contractKind != "library" or contract.name not in curated_libraries:
+            continue
+        member_names = {
+            n.name for n in contract.nodes if isinstance(n, FunctionDefinition)
+        }
+        if member_names & curated_libraries[contract.name]:
+            hits.append(f"{contract.name} ({path})")
+
+    # Negative: a genuine nonlinear-math kernel (mulDiv/sqrt/mulWad/...) hand-rolled
+    # in PROJECT code, outside any curated library. Generic-named helpers do not count.
+    for path, contract, fn in ctx.iter_functions():
+        if is_dependency_path(path):
+            continue
+        if fn.name in MATH_KERNEL_NAMES and contract.name not in curated_libraries:
+            hand_rolled.append(f"{contract.name}.{fn.name}")
+            if len(evidence) < EVIDENCE_CAP:
+                evidence.append(make_evidence(
+                    ctx, "curated_summary_hits", Severity.MEDIUM, path,
+                    fn.src_location.offset,
+                    f"hand-rolled `{fn.name}` — a curated summary exists for the "
+                    "standard-library version, but not for this implementation",
+                    function=f"{contract.name}.{fn.name}",
+                ))
+
+    # Using a curated math library is a positive; a hand-rolled kernel with no
+    # curated counterpart is a mild negative (needs a written summary — medium,
+    # not disqualifying); the common case (no heavy math) is neutral.
+    if hits:
+        score = 1.0
+    elif hand_rolled:
+        score = 0.55
+    else:
+        score = 0.85
+    return SignalResult(
+        signal_id="curated_summary_hits",
+        score=score,
+        evidence=evidence,
+        raw={"curated_hits": hits, "hand_rolled": hand_rolled},
+    )
diff --git a/certora_autosetup/amenability/weights.yaml b/certora_autosetup/amenability/weights.yaml
new file mode 100644
index 0000000..33bcfbb
--- /dev/null
+++ b/certora_autosetup/amenability/weights.yaml
@@ -0,0 +1,41 @@
+# Tuning surface of certora-fv-amenability. Calibration adjusts THIS file only —
+# scoring code never hardcodes a weight or threshold.
+#
+# score semantics: every signal emits [0,1] with 1 = fully amenable; the level is
+# derived from the weighted mean plus the co-occurrence rule below.
+
+weights:
+  # Structural killers — the patterns that can require a reference implementation.
+  # Weighted heavily; low is decided by how many of these fire together.
+  asm_trampoline: 1.6
+  asm_fp_manipulation: 1.5
+  storage_packing: 1.5
+  function_length: 1.2
+  mixed_theory: 1.2
+  # Friction — makes autosetup harder (config/summaries/harnesses) but is
+  # config-solvable, so these pull toward medium, not low. Lower weight.
+  asm_density: 0.6
+  bitmask_style: 0.7
+  unchecked_nonlinear: 0.5
+  curated_summary_hits: 0.7
+  external_call_surface: 0.4
+  dynamic_loops: 0.3
+  surface_shape: 0.0   # informational normalizers only
+
+thresholds:
+  high_min: 0.78          # weighted mean >= this AND no severe structural killer -> high
+  structural_low_max: 0.5  # low also requires the mean to be below this
+
+hard_rules:
+  # `low` requires this many structural-killer signals scoring at/below
+  # killer_severe_score simultaneously — the reference-implementation profile
+  # (trampolines + hand-rolled storage + FP surgery + monolithic mixed-theory
+  # functions all at once).
+  structural_killers:
+    - asm_trampoline
+    - asm_fp_manipulation
+    - storage_packing
+    - function_length
+    - mixed_theory
+  killer_severe_score: 0.25
+  killers_for_low: 3
diff --git a/certora_autosetup/setup/auto_munges.py b/certora_autosetup/setup/auto_munges.py
index 5aa9b68..ce37d88 100644
--- a/certora_autosetup/setup/auto_munges.py
+++ b/certora_autosetup/setup/auto_munges.py
@@ -10,9 +10,9 @@
 import traceback
 from dataclasses import asdict, dataclass
 from pathlib import Path
-from typing import Any, Callable, Dict, List, Tuple
+from typing import Callable, Dict, Iterator, List, Tuple
 
-from certora_autosetup.utils.file_utils import stream_ast_files
+from certora_autosetup.solidity_ast import AstDump, MemberAccess, SourceAst, iter_nodes_of_type, parse_src
 from certora_autosetup.utils.scope import Scope
 
 CODE_ACCESS_PATCH_FILE = ".certora_internal/code_access_patches.json"
@@ -213,6 +213,36 @@ def _load_ast_parent_graph(graph_path: Path) -> Dict[str, Dict[str, Dict[str, st
         return {}
 
 
+@dataclass(frozen=True)
+class _CodeAccessCandidate:
+    """The load-bearing fields of a `.code` MemberAccess, whether it came from the
+    typed tree or from the raw flat-map sweep of nodes the models could not reach."""
+
+    node_id: str
+    src: str
+    expr_src: str
+
+
+def _iter_code_accesses(source: SourceAst) -> Iterator[_CodeAccessCandidate]:
+    """`.code` MemberAccess candidates of one source, with exact-parity coverage:
+    typed nodes first, then raw flat-map nodes the typed walk did not reach (nested
+    under an unknown node type, or the whole source unparsable) — so a solc surprise
+    cannot hide a .code access. Vyper sources yield nothing."""
+    for node in iter_nodes_of_type(source, MemberAccess):
+        if isinstance(node, MemberAccess):
+            if node.memberName == 'code':
+                yield _CodeAccessCandidate(
+                    node_id=str(node.id), src=node.src, expr_src=node.expression.src
+                )
+        elif node.get('memberName') == 'code':
+            expression = node.get('expression', {})
+            yield _CodeAccessCandidate(
+                node_id=str(node.get('id')),
+                src=node.get('src', ''),
+                expr_src=expression.get('src', '') if isinstance(expression, dict) else '',
+            )
+
+
 def detect_code_accesses(log_func: Callable, ast_path: Path, ast_graph_path: Path, scope: Scope) -> None:
     """
     Detect .code accesses in the AST and create patches to rewrite them as loadCode(pointer) calls.
@@ -237,12 +267,14 @@ def detect_code_accesses(log_func: Callable, ast_path: Path, ast_graph_path: Pat
         patches = []
 
         # Structure: dict[relative_path: dict[absolute_path: dict[node_id: node_data]]]
-        for relative_path, path_data in stream_ast_files(ast_path):
-            # Skip files not in scope
-            if not scope.is_file_in_scope(Path(relative_path)):
-                continue
-
-            for absolute_path, nodes in path_data.items():
+        # Streamed one compilation unit at a time (the dump can be multi-GB); units
+        # whose main file is out of scope are skipped before any validation work.
+        for file_asts in AstDump.stream_units(
+            ast_path, unit_filter=lambda rel: scope.is_file_in_scope(Path(rel))
+        ):
+            relative_path = file_asts.original_file
+
+            for absolute_path, source in file_asts.sources.items():
                 # Convert absolute path to relative for scope checking
                 # The scope object works with paths relative to project_root
                 try:
@@ -261,93 +293,80 @@ def detect_code_accesses(log_func: Callable, ast_path: Path, ast_graph_path: Pat
                 if not scope.is_file_in_scope(rel_path_for_scope):
                     continue
 
-                # Iterate through all nodes (they're already flattened)
-                for _, node in nodes.items():
-                    if not isinstance(node, dict):
+                # The node's src offsets refer to THIS source file (not the unit's
+                # main file), so patches read and target it; the src file_id is not
+                # needed since the file is already known here.
+                patch_target = str(rel_path_for_scope)
+
+                # Find MemberAccess nodes with memberName="code" in this source
+                for candidate in _iter_code_accesses(source):
+                    node_id = candidate.node_id
+
+                    # Check if this .code access is used as expression in another node using parent graph
+                    # If the parent graph exists, use it for O(1) lookup
+                    if parent_graph:
+                        parent_map = parent_graph.get(relative_path, {}).get(absolute_path, {})
+                        parent_id = parent_map.get(node_id)
+
+                        if parent_id:
+                            # The raw flat map covers parsed and unparsed sources alike
+                            parent_node = source.raw.get(parent_id, {})
+                            parent_type = parent_node.get('nodeType')
+
+                            # Skip if parent is MemberAccess (like .code.length) or FunctionCall (like x.code())
+                            if parent_type in ['MemberAccess', 'FunctionCall']:
+                                continue
+                    else:
+                        # Fallback: check manually if graph not available
+                        is_chained = False
+                        for other_node in source.raw.values():
+                            if not isinstance(other_node, dict):
+                                continue
+
+                            # Check if used in MemberAccess (like .code.length) or FunctionCall (like x.code())
+                            if other_node.get('nodeType') in ['MemberAccess', 'FunctionCall']:
+                                expr = other_node.get('expression', {})
+                                if str(expr.get('id')) == node_id:
+                                    is_chained = True
+                                    break
+
+                        if is_chained:
+                            continue  # Skip this .code access, it's part of a chain or function call
+
+                    # Extract source location: "offset:length:file_id" (byte offsets)
+                    if not candidate.src or not candidate.expr_src:
+                        continue
+
+                    try:
+                        offset, length, _ = parse_src(candidate.src)
+                        expr_offset, expr_length, _ = parse_src(candidate.expr_src)
+                    except ValueError:
                         continue
 
-                    # Check if this is a MemberAccess node with memberName="code"
-                    if node.get('nodeType') == 'MemberAccess' and node.get('memberName') == 'code':
-                        node_id = str(node.get('id'))
-
-                        # Check if this .code access is used as expression in another node using parent graph
-                        # If the parent graph exists, use it for O(1) lookup
-                        if parent_graph:
-                            parent_map = parent_graph.get(relative_path, {}).get(absolute_path, {})
-                            parent_id = parent_map.get(node_id)
-
-                            if parent_id:
-                                parent_node = nodes.get(parent_id, {})
-                                parent_type = parent_node.get('nodeType')
-
-                                # Skip if parent is MemberAccess (like .code.length) or FunctionCall (like x.code())
-                                if parent_type in ['MemberAccess', 'FunctionCall']:
-                                    continue
-                        else:
-                            # Fallback: check manually if graph not available
-                            is_chained = False
-                            for _, other_node in nodes.items():
-                                if not isinstance(other_node, dict):
-                                    continue
-
-                                # Check if used in MemberAccess (like .code.length) or FunctionCall (like x.code())
-                                if other_node.get('nodeType') in ['MemberAccess', 'FunctionCall']:
-                                    expr = other_node.get('expression', {})
-                                    if str(expr.get('id')) == node_id:
-                                        is_chained = True
-                                        break
-
-                            if is_chained:
-                                continue  # Skip this .code access, it's part of a chain or function call
-
-                        # Extract source location: "offset:length:file_id"
-                        src = node.get('src', '')
-                        if not src:
-                            continue
-
-                        parts = src.split(':')
-                        if len(parts) != 3:
-                            continue
-
-                        offset = int(parts[0])
-                        length = int(parts[1])
-                        # file_id = int(parts[2])  # Not needed since we already know the file from absolute_path
-
-                        # Get the expression being accessed (e.g., "pointer" from "pointer.code")
-                        expression = node.get('expression', {})
-                        expr_src = expression.get('src', '')
-                        if not expr_src:
-                            continue
-
-                        expr_parts = expr_src.split(':')
-                        if len(expr_parts) != 3:
-                            continue
-
-                        expr_offset = int(expr_parts[0])
-                        expr_length = int(expr_parts[1])
-
-                        # Read the original expression from the source file
-                        try:
-                            with open(relative_path, 'r') as src_file:
-                                src_content = src_file.read()
-                                expr_text = src_content[expr_offset:expr_offset + expr_length]
-                                original_text = src_content[offset:offset + length]
-
-                                # Create replacement: "certora_loadCode(expression)"
-                                replacement = f"certora_loadCode({expr_text})"
-
-                                patches.append(
-                                    CodeAccessPatch(
-                                        file=relative_path,
-                                        offset=offset,
-                                        length=length,
-                                        original=original_text,
-                                        replacement=replacement,
-                                    )
-                                )
-
-                        except Exception as e:
-                            log_func(f"Warning: Failed to read source for patch at {relative_path}: {e}", "WARNING")
+                    # Read the original expression from the source file
+                    try:
+                        with open(patch_target, 'r') as src_file:
+                            src_content = src_file.read()
+                            expr_text = src_content[expr_offset:expr_offset + expr_length]
+                            original_text = src_content[offset:offset + length]
+
+                            # Create replacement: "certora_loadCode(expression)"
+                            replacement = f"certora_loadCode({expr_text})"
+
+                            patch = CodeAccessPatch(
+                                file=patch_target,
+                                offset=offset,
+                                length=length,
+                                original=original_text,
+                                replacement=replacement,
+                            )
+                            # The same source can appear under several compilation
+                            # units; apply must see each patch once
+                            if patch not in patches:
+                                patches.append(patch)
+
+                    except Exception as e:
+                        log_func(f"Warning: Failed to read source for patch at {patch_target}: {e}", "WARNING")
 
         if not patches:
             log_func("✓ No .code accesses found")
diff --git a/certora_autosetup/setup/setup_prover.py b/certora_autosetup/setup/setup_prover.py
index 63e3cd9..298fb30 100644
--- a/certora_autosetup/setup/setup_prover.py
+++ b/certora_autosetup/setup/setup_prover.py
@@ -17,7 +17,7 @@
 import traceback
 from dataclasses import dataclass
 from pathlib import Path
-from typing import TYPE_CHECKING, Any, Dict, List, Optional, Set, Tuple
+from typing import TYPE_CHECKING, Any, Dict, Iterable, Iterator, List, Optional, Set, Tuple
 
 if TYPE_CHECKING:
     from certora_autosetup.setup.setup_summaries import SummarySetup
@@ -30,10 +30,18 @@
 from certora_autosetup.setup.signature_manager import SignatureManager
 from certora_autosetup.setup.signature_types import ContractInfo
 from certora_autosetup.setup.solidity_utils import extract_definitions_from_solidity
+from certora_autosetup.solidity_ast import (
+    AstDump,
+    ContractDefinition,
+    FileAsts,
+    build_parent_graph_json,
+    iter_nodes_of_type,
+    stream_raw_units,
+)
 from packaging.version import Version
 from certora_autosetup.utils.config_manager import convert_solc_version_to_certora_format
 from certora_autosetup.cache.cache_fs import cache_path, get_fs
-from certora_autosetup.utils.file_utils import atomic_write_json_fsspec, stream_ast_files
+from certora_autosetup.utils.file_utils import atomic_write_json_fsspec
 from certora_autosetup.utils.llm_util import ledger_component
 from certora_autosetup.utils.constants import (
     DEFAULT_SOLC_VERSION,
@@ -53,6 +61,54 @@
 from certora_autosetup.utils.solc_version_resolver import VIA_IR_MIN_VERSION
 from certora_autosetup.utils.types import ContractHandle, ContractKind, TypeParseMode, parse_type_descriptor
 
+@dataclass(frozen=True)
+class _ContractDeclView:
+    """Uniform view of a ContractDefinition for declaration/inheritance scans, whether
+    it came from the typed AST or from the raw fallback of an unparsable source."""
+
+    source_path: str
+    node_id: Optional[int]
+    name: str
+    abstract: bool
+    contract_kind: str
+    linearized_base_ids: List[int]
+
+
+def _iter_contract_declarations(units: Iterable[FileAsts]) -> Iterator[_ContractDeclView]:
+    """Every contract declaration in a stream of compilation units (typically
+    ``AstDump.stream_units(...)``, so the multi-GB dump is never fully in memory):
+    typed where the models parsed, completed by a raw flat-map sweep for anything
+    the typed walk could not reach (a solc surprise cannot hide contracts from
+    setup; Vyper sources contribute nothing — no ContractDefinition nodes)."""
+    for file_asts in units:
+        for source in file_asts.sources.values():
+            yield from _unit_contract_declarations(source)
+
+
+def _unit_contract_declarations(source) -> Iterator[_ContractDeclView]:
+    for node in iter_nodes_of_type(source, ContractDefinition):
+            if isinstance(node, ContractDefinition):
+                yield _ContractDeclView(
+                    source_path=source.source_path,
+                    node_id=node.id,
+                    name=node.name,
+                    abstract=node.abstract,
+                    contract_kind=node.contractKind,
+                    linearized_base_ids=list(node.linearizedBaseContracts),
+                )
+            else:
+                yield _ContractDeclView(
+                    source_path=source.source_path,
+                    node_id=node.get("id"),
+                    name=node.get("name") or "",
+                    abstract=bool(node.get("abstract", False)),
+                    contract_kind=node.get("contractKind", "contract"),
+                    linearized_base_ids=[
+                        i for i in node.get("linearizedBaseContracts", []) if isinstance(i, int)
+                    ],
+                )
+
+
 class CompilationAnalysisError(Exception):
     """Raised when compilation analysis fails."""
 
@@ -67,27 +123,6 @@ class SummarySetupError(Exception):
 
 
 
-@dataclass
-class _ContractDef:
-    """ContractDefinition fields needed to resolve inheritance/abstract info."""
-
-    id: Optional[int]
-    name: Optional[str]
-    abstract: bool
-    contract_kind: str
-    linearized_base_contracts: List[int]
-
-    @classmethod
-    def from_ast_node(cls, node: Dict[str, Any]) -> "_ContractDef":
-        return cls(
-            id=node.get("id"),
-            name=node.get("name"),
-            abstract=node.get("abstract", False),
-            contract_kind=node.get("contractKind", "contract"),
-            linearized_base_contracts=node.get("linearizedBaseContracts", []),
-        )
-
-
 class SetupProver:
     """Class to handle setup operations for Certora Prover."""
 
@@ -743,16 +778,10 @@ def _build_declared_contracts_by_file(self) -> Dict[str, Set[str]]:
         ast_path = self._build_dir / FILE_BUILD_ASTS if self._build_dir else None
         if not ast_path or not ast_path.exists():
             return {}
-        for _relative_path, abs_path_dict in stream_ast_files(ast_path):
-            for abs_path, nodes in abs_path_dict.items():
-                rel = self.scope.get_relative_path(Path(abs_path))
-                for node in nodes.values():
-                    if (
-                        node.get("nodeType") == "ContractDefinition"
-                        and node.get("contractKind") != "interface"
-                        and node.get("name")
-                    ):
-                        contracts_by_file.setdefault(rel, set()).add(node["name"])
+        for decl in _iter_contract_declarations(AstDump.stream_units(ast_path)):
+            if decl.contract_kind != "interface" and decl.name:
+                rel = self.scope.get_relative_path(Path(decl.source_path))
+                contracts_by_file.setdefault(rel, set()).add(decl.name)
         return contracts_by_file
 
     def _sole_contract_declared_in(self, original_file: str) -> str:
@@ -1162,37 +1191,31 @@ def _extract_inheritance_and_abstract_from_ast(self, ast_file_path: Optional[Pat
         try:
             self.log(f"Extracting inheritance info from {ast_file_path}")
 
-            # Stream the (multi-GB) .asts.json once, keeping only the fields of each
-            # ContractDefinition needed below so it is never fully materialized.
-            contract_defs: List[_ContractDef] = []
-            for _file_path, abs_path_dict in stream_ast_files(ast_file_path):
-                for _abs_path, nodes in abs_path_dict.items():
-                    for _node_id, node in nodes.items():
-                        if isinstance(node, dict) and node.get("nodeType") == "ContractDefinition":
-                            contract_defs.append(_ContractDef.from_ast_node(node))
+            # Stream the (multi-GB) .asts.json once, keeping only the slim per-contract
+            # views needed below so the dump is never fully materialized.
+            declarations = list(_iter_contract_declarations(AstDump.stream_units(ast_file_path)))
 
             # Build ID to contract name mapping once
-            id_to_name = {}
-            for cd in contract_defs:
-                if cd.id and cd.name:
-                    id_to_name[cd.id] = cd.name
+            id_to_name = {
+                decl.node_id: decl.name for decl in declarations if decl.node_id and decl.name
+            }
 
             # Now process contracts and resolve inheritance using the pre-built mapping
-            for cd in contract_defs:
-                contract_name = cd.name
-                if contract_name:
-                    # Check if abstract or interface
-                    if cd.abstract or cd.contract_kind == "interface":
-                        abstract_contracts.add(contract_name)
-                        self.log(f"Identified {'abstract' if cd.abstract else 'interface'}: {contract_name}", "DEBUG")
-
-                    # Get linearized base contracts (includes self + all inherited contracts)
-                    linearized = cd.linearized_base_contracts
-                    if len(linearized) > 1:  # More than just self
-                        # Convert IDs to contract names using pre-built mapping
-                        base_contracts = [id_to_name[contract_id] for contract_id in linearized[1:] if contract_id in id_to_name]
-                        if base_contracts:
-                            inheritance_info[contract_name] = base_contracts
+            for decl in declarations:
+                if not decl.name:
+                    continue
+                # Check if abstract or interface
+                if decl.abstract or decl.contract_kind == "interface":
+                    abstract_contracts.add(decl.name)
+                    self.log(f"Identified {'abstract' if decl.abstract else 'interface'}: {decl.name}", "DEBUG")
+
+                # Get linearized base contracts (includes self + all inherited contracts)
+                linearized = decl.linearized_base_ids
+                if len(linearized) > 1:  # More than just self
+                    # Convert IDs to contract names using pre-built mapping
+                    base_contracts = [id_to_name[contract_id] for contract_id in linearized[1:] if contract_id in id_to_name]
+                    if base_contracts:
+                        inheritance_info[decl.name] = base_contracts
 
             self.log(f"Extracted inheritance for {len(inheritance_info)} contracts", "DEBUG")
             self.log(f"Found {len(abstract_contracts)} abstract/interface contracts to skip", "INFO")
@@ -1319,7 +1342,7 @@ def generate_ast_graph(self, ast_path: Path) -> None:
             ast_path: Path to the .asts.json file
 
         Output:
-            Writes to .certora_internal/.ast_graph.json with structure:
+            Writes to .certora_internal/all_ast_parent_graph.json with structure:
             {
                 "relative_path": {
                     "absolute_path": {
@@ -1331,25 +1354,10 @@ def generate_ast_graph(self, ast_path: Path) -> None:
         self.log("Building AST parent graph...")
 
         try:
-            # Build parent graph: node_id -> parent_node_id
-            parent_graph = {}
-
-            # Structure: dict[relative_path: dict[absolute_path: dict[node_id: node_data]]]
-            for relative_path, path_data in stream_ast_files(ast_path):
-                parent_graph[relative_path] = {}
-
-                for absolute_path, nodes in path_data.items():
-                    parent_graph[relative_path][absolute_path] = {}
-
-                    # For each node, find all child node IDs and map them to this parent
-                    for node_id, node in nodes.items():
-                        if not isinstance(node, dict):
-                            continue
-
-                        # Find all child node IDs referenced in this node
-                        child_ids = self._extract_child_node_ids(node)
-                        for child_id in child_ids:
-                            parent_graph[relative_path][absolute_path][str(child_id)] = str(node_id)
+            # Build parent graph: node_id -> parent_node_id (byte-compatible legacy
+            # format, streamed one compilation unit at a time — the dump can be
+            # multi-GB)
+            parent_graph = build_parent_graph_json(stream_raw_units(ast_path))
 
             # Write parent graph to JSON
             graph_path = self.getASTParentGraphPath()
@@ -1362,30 +1370,6 @@ def generate_ast_graph(self, ast_path: Path) -> None:
             self.log(f"Warning: Failed to generate AST parent graph: {e}", "WARNING")
             self.log(f"Traceback: {traceback.format_exc()}", "WARNING")
 
-    def _extract_child_node_ids(self, node: Any) -> List[int]:
-        """
-        Extract all child node IDs from an AST node.
-
-        Args:
-            node: AST node (dict or other type)
-
-        Returns:
-            List of child node IDs
-        """
-        child_ids = []
-
-        if isinstance(node, dict):
-            for key, value in node.items():
-                # Look for 'id' fields in nested structures
-                if isinstance(value, dict) and 'id' in value:
-                    child_ids.append(value['id'])
-                elif isinstance(value, list):
-                    for item in value:
-                        if isinstance(item, dict) and 'id' in item:
-                            child_ids.append(item['id'])
-
-        return child_ids
-
     def getASTPath(self) -> Path:
         return Path(".certora_internal/all_asts.json")
 
diff --git a/certora_autosetup/solidity_ast/__init__.py b/certora_autosetup/solidity_ast/__init__.py
new file mode 100644
index 0000000..8c870d1
--- /dev/null
+++ b/certora_autosetup/solidity_ast/__init__.py
@@ -0,0 +1,173 @@
+"""Typed pydantic models of the Solidity compact AST as dumped by
+``certoraRun --dump_asts`` (see ``base.py`` for the modeling conventions and
+``loader.py`` for the dump structure and degradation policy).
+
+Typical use::
+
+    from certora_autosetup.solidity_ast import AstDump, ContractDefinition, find_all
+
+    dump = AstDump.load(".certora_internal/all_asts.json")
+    for _, _, source_unit in dump.iter_parsed_roots():
+        for contract in find_all(source_unit, ContractDefinition):
+            ...
+"""
+
+__all__ = [
+    # base
+    "AstNode", "SolcNode", "YulNode", "UnknownNode", "SrcLocation", "parse_src",
+    "TypeDescriptions", "Visibility", "StateMutability", "Mutability", "StorageLocation",
+    # loader
+    "AstDump", "FileAsts", "SourceAst", "iter_nodes_of_type", "stream_raw_units",
+    # traversal
+    "iter_children", "walk", "find_all", "build_node_index", "build_parent_map",
+    "build_parent_graph_json",
+    # unions
+    "unions", "MODEL_BY_SCHEMA_DEF", "Node", "Expression", "Statement", "TypeName",
+    "SourceUnitNode", "ContractBodyNode",
+    # types
+    "ArrayTypeName", "ElementaryTypeName", "FunctionTypeName", "IdentifierPath",
+    "Mapping", "UserDefinedTypeName",
+    # expressions
+    "Assignment", "BinaryOperation", "Conditional", "ElementaryTypeNameExpression",
+    "FunctionCall", "FunctionCallOptions", "Identifier", "IndexAccess", "IndexRangeAccess",
+    "Literal", "MemberAccess", "NewExpression", "TupleExpression", "UnaryOperation",
+    # statements
+    "Block", "Break", "Continue", "DoWhileStatement", "EmitStatement", "ExpressionStatement",
+    "ForStatement", "IfStatement", "InlineAssembly", "PlaceholderStatement", "Return",
+    "RevertStatement", "TryCatchClause", "TryStatement", "UncheckedBlock",
+    "VariableDeclarationStatement", "WhileStatement",
+    # declarations
+    "ContractDefinition", "EnumDefinition", "EnumValue", "ErrorDefinition", "EventDefinition",
+    "FunctionDefinition", "ImportDirective", "InheritanceSpecifier", "ModifierDefinition",
+    "ModifierInvocation", "OverrideSpecifier", "ParameterList", "PragmaDirective", "SourceUnit",
+    "StorageLayoutSpecifier", "StructDefinition", "StructuredDocumentation",
+    "UserDefinedValueTypeDefinition", "UsingForDirective", "VariableDeclaration",
+    # yul
+    "YulAssignment", "YulBlock", "YulBreak", "YulCase", "YulContinue", "YulExpression",
+    "YulExpressionStatement", "YulForLoop", "YulFunctionCall", "YulFunctionDefinition",
+    "YulIdentifier", "YulIf", "YulLeave", "YulLiteral", "YulLiteralHexValue",
+    "YulLiteralValue", "YulStatement", "YulSwitch", "YulTypedName", "YulVariableDeclaration",
+]
+
+# Importing .unions resolves all cross-module forward references and rebuilds the
+# models; loader imports it, and the explicit re-import keeps the ordering obvious.
+from . import unions as unions
+from . import yul as yul
+from .base import (
+    AstNode,
+    Mutability,
+    SolcNode,
+    SrcLocation,
+    StateMutability,
+    StorageLocation,
+    TypeDescriptions,
+    UnknownNode,
+    Visibility,
+    YulNode,
+    parse_src,
+)
+from .declarations import (
+    ContractDefinition,
+    EnumDefinition,
+    EnumValue,
+    ErrorDefinition,
+    EventDefinition,
+    FunctionDefinition,
+    ImportDirective,
+    InheritanceSpecifier,
+    ModifierDefinition,
+    ModifierInvocation,
+    OverrideSpecifier,
+    ParameterList,
+    PragmaDirective,
+    SourceUnit,
+    StorageLayoutSpecifier,
+    StructDefinition,
+    StructuredDocumentation,
+    UserDefinedValueTypeDefinition,
+    UsingForDirective,
+    VariableDeclaration,
+)
+from .expressions import (
+    Assignment,
+    BinaryOperation,
+    Conditional,
+    ElementaryTypeNameExpression,
+    FunctionCall,
+    FunctionCallOptions,
+    Identifier,
+    IndexAccess,
+    IndexRangeAccess,
+    Literal,
+    MemberAccess,
+    NewExpression,
+    TupleExpression,
+    UnaryOperation,
+)
+from .loader import AstDump, FileAsts, SourceAst, iter_nodes_of_type, stream_raw_units
+from .statements import (
+    Block,
+    Break,
+    Continue,
+    DoWhileStatement,
+    EmitStatement,
+    ExpressionStatement,
+    ForStatement,
+    IfStatement,
+    InlineAssembly,
+    PlaceholderStatement,
+    Return,
+    RevertStatement,
+    TryCatchClause,
+    TryStatement,
+    UncheckedBlock,
+    VariableDeclarationStatement,
+    WhileStatement,
+)
+from .traversal import (
+    build_node_index,
+    build_parent_graph_json,
+    build_parent_map,
+    find_all,
+    iter_children,
+    walk,
+)
+from .types import (
+    ArrayTypeName,
+    ElementaryTypeName,
+    FunctionTypeName,
+    IdentifierPath,
+    Mapping,
+    UserDefinedTypeName,
+)
+from .unions import (
+    MODEL_BY_SCHEMA_DEF,
+    ContractBodyNode,
+    Expression,
+    Node,
+    SourceUnitNode,
+    Statement,
+    TypeName,
+)
+from .yul import (
+    YulAssignment,
+    YulBlock,
+    YulBreak,
+    YulCase,
+    YulContinue,
+    YulExpression,
+    YulExpressionStatement,
+    YulForLoop,
+    YulFunctionCall,
+    YulFunctionDefinition,
+    YulIdentifier,
+    YulIf,
+    YulLeave,
+    YulLiteral,
+    YulLiteralHexValue,
+    YulLiteralValue,
+    YulStatement,
+    YulSwitch,
+    YulTypedName,
+    YulVariableDeclaration,
+)
diff --git a/certora_autosetup/solidity_ast/__main__.py b/certora_autosetup/solidity_ast/__main__.py
new file mode 100644
index 0000000..f1009cf
--- /dev/null
+++ b/certora_autosetup/solidity_ast/__main__.py
@@ -0,0 +1,136 @@
+"""Summarize a ``.asts.json`` dump through the typed models.
+
+Usage::
+
+    python -m certora_autosetup.solidity_ast [--json] [--solc-version V] <path/to/all_asts.json>
+
+Per source file: parse status, node counts, unknown node types, unmodeled fields,
+and round-trip fidelity (does the typed tree re-serialize to the exact source
+JSON?) — a quick way to validate the models against a real project's dump. The
+dump is streamed one compilation unit at a time, so multi-GB dumps stay cheap.
+``--json`` emits one machine-readable summary object instead of text.
+"""
+
+from __future__ import annotations
+
+import argparse
+import json
+import sys
+from collections import Counter
+from typing import Any
+
+from .base import UnknownNode
+from .declarations import ContractDefinition
+from .diagnostics import roundtrip_diffs
+from .loader import AstDump, FileAsts, SourceAst
+from .traversal import find_all, walk
+
+
+def _source_report(source_ast: SourceAst) -> dict[str, Any]:
+    if source_ast.root is None:
+        return {
+            "status": source_ast.raw_kind,
+            "error": source_ast.parse_error,
+            "raw_nodes": len(source_ast.raw),
+        }
+    nodes = list(walk(source_ast.root))
+    unknown = Counter(n.nodeType for n in nodes if isinstance(n, UnknownNode))
+    extras = Counter(
+        f"{type(n).__name__}.{key}" for n in nodes for key in (n.model_extra or {})
+    )
+    diffs = roundtrip_diffs(source_ast)
+    return {
+        "status": "ok",
+        "nodes": len(nodes),
+        "indexed": len(source_ast.nodes),
+        "unknown_node_types": dict(unknown),
+        "unmodeled_fields": dict(extras),
+        "roundtrip_diffs": diffs,
+    }
+
+
+def _print_unit_text(file_asts: FileAsts, per_file: dict[str, dict[str, Any]]) -> None:
+    print(file_asts.original_file)
+    id_to_name = {
+        c.id: c.name
+        for source in file_asts.sources.values()
+        if source.root is not None
+        for c in find_all(source.root, ContractDefinition)
+    }
+    for source in file_asts.sources.values():
+        r = per_file[source.source_path]
+        if r["status"] != "ok":
+            detail = f": {r['error']}" if r.get("error") else ""
+            print(f"  {source.source_path}  [{r['status']}]{detail}")
+            continue
+        print(f"  {source.source_path}  [ok] {r['nodes']} nodes, {r['indexed']} with ids")
+        if r["unknown_node_types"]:
+            print(f"    unknown node types: {r['unknown_node_types']}")
+        if r["unmodeled_fields"]:
+            print(f"    unmodeled fields: {r['unmodeled_fields']}")
+        if r["roundtrip_diffs"]:
+            print(f"    roundtrip diffs ({len(r['roundtrip_diffs'])}):")
+            for d in r["roundtrip_diffs"][:10]:
+                print(f"      {d}")
+        assert source.root is not None
+        for contract in find_all(source.root, ContractDefinition):
+            bases = [
+                id_to_name.get(i, f"#{i}") for i in contract.linearizedBaseContracts[1:]
+            ]
+            abstract = "abstract " if contract.abstract else ""
+            inherits = f" is {', '.join(bases)}" if bases else ""
+            print(f"    {abstract}{contract.contractKind} {contract.name}{inherits}")
+
+
+def main(argv: list[str] | None = None) -> int:
+    parser = argparse.ArgumentParser(description=(__doc__ or "").partition("\n")[0])
+    parser.add_argument("dump", help="path to a .asts.json / all_asts.json file")
+    parser.add_argument("--json", action="store_true", help="machine-readable output")
+    parser.add_argument(
+        "--solc-version",
+        default=None,
+        help="compiler version that produced the dump; enables the VERSION_GATES "
+        "check (absent gated fields fail the source instead of reading as None)",
+    )
+    args = parser.parse_args(argv)
+
+    report: dict[str, dict[str, Any]] = {}
+    for file_asts in AstDump.stream_units(args.dump, solc_version=args.solc_version):
+        per_file = {
+            source.source_path: _source_report(source)
+            for source in file_asts.sources.values()
+        }
+        report[file_asts.original_file] = per_file
+        if not args.json:
+            _print_unit_text(file_asts, per_file)
+
+    flat = [r for per_file in report.values() for r in per_file.values()]
+    ok = [r for r in flat if r["status"] == "ok"]
+    clean = [
+        r
+        for r in ok
+        if not r["unknown_node_types"] and not r["unmodeled_fields"] and not r["roundtrip_diffs"]
+    ]
+    summary = {
+        "sources": len(flat),
+        "parsed": len(ok),
+        "vyper": sum(r["status"] == "vyper" for r in flat),
+        "parse_failed": sum(r["status"] == "parse_failed" for r in flat),
+        "fully_clean": len(clean),
+    }
+
+    if args.json:
+        json.dump({"summary": summary, "files": report}, sys.stdout, indent=1)
+        print()
+    else:
+        print(
+            f"\n{summary['parsed']}/{summary['sources']} sources parsed, "
+            f"{summary['fully_clean']} fully clean (no unknowns, no unmodeled fields, "
+            f"round-trip exact); vyper: {summary['vyper']}, failed: {summary['parse_failed']}"
+        )
+
+    return 0 if summary["parse_failed"] == 0 else 1
+
+
+if __name__ == "__main__":
+    sys.exit(main())
diff --git a/certora_autosetup/solidity_ast/base.py b/certora_autosetup/solidity_ast/base.py
new file mode 100644
index 0000000..9cb33a9
--- /dev/null
+++ b/certora_autosetup/solidity_ast/base.py
@@ -0,0 +1,136 @@
+"""Base classes and shared value types for the Solidity compact-AST pydantic models.
+
+The models in this subpackage describe the solc "compact AST" (the ``ast`` entry of
+solc standard-json output for each source file), as it appears inside the
+``.asts.json`` dump produced by ``certoraRun --dump_asts``. Field sets are
+transcribed from the vendored OpenZeppelin ``solidity-ast`` JSON Schema
+(see ``schema/schema.json`` and ``schema/NOTICE``), which unions solc versions
+>= 0.6 into a single schema. ``tests/solidity_ast/test_schema_conformance.py``
+machine-checks every model against that schema.
+
+Transcription conventions (uniform across all node modules):
+
+- schema-required property            -> plain annotated field, no default
+- schema-optional property (absent
+  from ``required``; version-gated)   -> ``T | None = None``
+- required-but-nullable property
+  (``anyOf [T, null]``)               -> ``T | None`` with NO default
+- ``nodeType``                        -> ``Literal["X"]`` (the union discriminator)
+- reference to a schema union helper
+  (Expression/Statement/TypeName/...) -> string forward ref to the union alias,
+                                         resolved by ``unions.model_rebuild`` wiring
+- schema enum property                -> shared ``Literal`` alias below when it matches a
+                                         helper definition, inline ``Literal[...]`` otherwise
+- python-keyword property name        -> trailing-underscore field with ``alias=`` (the only
+                                         known case is ``UsingForDirective.global``)
+"""
+
+from __future__ import annotations
+
+from typing import Callable, Literal, NamedTuple
+
+from pydantic import BaseModel, ConfigDict
+
+# Shared enum aliases, mirroring the schema's helper definitions of the same names.
+Visibility = Literal["external", "public", "internal", "private"]
+StateMutability = Literal["payable", "pure", "nonpayable", "view"]
+Mutability = Literal["mutable", "immutable", "constant"]
+StorageLocation = Literal["calldata", "default", "memory", "storage", "transient"]
+
+
+class SrcLocation(NamedTuple):
+    """Decoded solc source location ("offset:length:fileIndex", byte-based)."""
+
+    offset: int
+    length: int
+    file_index: int
+
+
+def parse_src(src: str) -> SrcLocation:
+    """Parse a solc ``src`` string ("offset:length:fileIndex") into byte offsets.
+
+    Raises ValueError on malformed input. ``fileIndex`` may be -1 for nodes solc
+    synthesizes without a source file.
+    """
+    offset, length, file_index = src.split(":")
+    return SrcLocation(int(offset), int(length), int(file_index))
+
+
+class AstNode(BaseModel):
+    """Common base of every Solidity and Yul compact-AST node.
+
+    ``extra="allow"`` keeps fields from newer solc releases (not yet in the vendored
+    schema) available via ``model_extra`` instead of failing validation.
+    """
+
+    model_config = ConfigDict(
+        extra="allow", validate_by_name=True, serialize_by_alias=True
+    )
+
+    src: str
+    # Injected by certoraRun into the dump on nodes enclosed in a ContractDefinition;
+    # never present in raw solc output.
+    certora_contract_name: str | None = None
+
+    @property
+    def src_location(self) -> SrcLocation:
+        return parse_src(self.src)
+
+
+class SolcNode(AstNode):
+    """A Solidity-language node: always carries a numeric ``id``."""
+
+    id: int
+
+
+class YulNode(AstNode):
+    """A Yul node (inside ``InlineAssembly.AST``): no ``id``; ``src`` points into the
+    original Solidity source and ``nativeSrc`` (solc >= 0.8.21) into the generated Yul.
+    """
+
+    nativeSrc: str | None = None
+
+
+class UnknownNode(AstNode):
+    """Fallback member of every node union: a node whose ``nodeType`` this model set
+    does not know (newer solc than the vendored schema, or an exotic construct).
+
+    All its fields land in ``model_extra`` and its children stay raw dicts; typed
+    queries skip it, so an unknown node degrades gracefully instead of failing the
+    whole source file.
+    """
+
+    nodeType: str
+    id: int | None = None
+    # Lenient: synthesized nodes may lack src; "" fails any src-offset use downstream
+    # the same way a missing node would.
+    src: str = ""
+
+
+UNKNOWN_TAG = "__unknown__"
+
+
+def tag_by_node_type(known: frozenset[str]) -> Callable[[object], str]:
+    """Discriminator function for a node union: returns the ``nodeType`` tag when it is
+    one of ``known``, else ``UNKNOWN_TAG`` (routing to the union's UnknownNode member).
+    Handles both dicts (validation) and model instances (serialization).
+    """
+
+    def tag(value: object) -> str:
+        node_type = (
+            value.get("nodeType")
+            if isinstance(value, dict)
+            else getattr(value, "nodeType", None)
+        )
+        return node_type if isinstance(node_type, str) and node_type in known else UNKNOWN_TAG
+
+    return tag
+
+
+class TypeDescriptions(BaseModel):
+    """The ``typeDescriptions`` object attached to expressions and type names."""
+
+    model_config = ConfigDict(extra="allow")
+
+    typeIdentifier: str | None = None
+    typeString: str | None = None
diff --git a/certora_autosetup/solidity_ast/declarations.py b/certora_autosetup/solidity_ast/declarations.py
new file mode 100644
index 0000000..cc6889e
--- /dev/null
+++ b/certora_autosetup/solidity_ast/declarations.py
@@ -0,0 +1,334 @@
+"""Declaration nodes of the Solidity compact AST (source-unit and contract-body level).
+
+Also defines ``SourceUnit`` itself, transcribed from the schema root (it is the
+schema's top-level object, not a member of ``definitions``).
+"""
+
+from __future__ import annotations
+
+from typing import TYPE_CHECKING, Literal
+
+from pydantic import BaseModel, ConfigDict, Field, field_validator
+
+from .base import (
+    Mutability,
+    SolcNode,
+    StateMutability,
+    StorageLocation,
+    TypeDescriptions,
+    Visibility,
+)
+
+if TYPE_CHECKING:
+    from .expressions import Identifier
+    from .statements import Block
+    from .types import IdentifierPath, UserDefinedTypeName
+    from .unions import ContractBodyNode, Expression, SourceUnitNode, TypeName
+
+
+class StructuredDocumentation(SolcNode):
+    """A NatSpec documentation node."""
+
+    text: str
+    nodeType: Literal["StructuredDocumentation"]
+
+
+class OverrideSpecifier(SolcNode):
+    """An ``override(...)`` specifier on a function, modifier, or state variable."""
+
+    overrides: "list[UserDefinedTypeName] | list[IdentifierPath]"
+    nodeType: Literal["OverrideSpecifier"]
+
+
+class VariableDeclaration(SolcNode):
+    """A variable declaration: state variable, parameter, struct member, or local."""
+
+    name: str
+    nameLocation: str | None = None
+    baseFunctions: list[int] | None = None
+    constant: bool
+    documentation: StructuredDocumentation | None = None
+    functionSelector: str | None = None
+    indexed: bool | None = None
+    # Absent pre-0.6.6 (only `constant` existed); LENIENT_REQUIRED.
+    mutability: Mutability | None = None
+    overrides: OverrideSpecifier | None = None
+    scope: int
+    stateVariable: bool
+    storageLocation: StorageLocation
+    typeDescriptions: TypeDescriptions
+    typeName: "TypeName | None" = None
+    value: "Expression | None" = None
+    visibility: Visibility
+    nodeType: Literal["VariableDeclaration"]
+
+    @property
+    def effective_mutability(self) -> Mutability:
+        """``mutability`` with the pre-0.6.6 case derived from ``constant`` (the only
+        mutability that existed then besides mutable) — never None."""
+        if self.mutability is not None:
+            return self.mutability
+        return "constant" if self.constant else "mutable"
+
+
+class ParameterList(SolcNode):
+    """The parenthesized list of parameters or return values."""
+
+    parameters: list[VariableDeclaration]
+    nodeType: Literal["ParameterList"]
+
+
+class EnumValue(SolcNode):
+    """A single member of an enum definition."""
+
+    name: str
+    nameLocation: str | None = None
+    documentation: StructuredDocumentation | None = None
+    nodeType: Literal["EnumValue"]
+
+
+class EnumDefinition(SolcNode):
+    """An ``enum`` definition."""
+
+    name: str
+    nameLocation: str | None = None
+    canonicalName: str
+    members: list[EnumValue]
+    documentation: StructuredDocumentation | None = None
+    nodeType: Literal["EnumDefinition"]
+
+
+class ErrorDefinition(SolcNode):
+    """A custom ``error`` definition (solc >= 0.8.4)."""
+
+    name: str
+    nameLocation: str
+    documentation: StructuredDocumentation | None = None
+    errorSelector: str | None = None
+    parameters: ParameterList
+    nodeType: Literal["ErrorDefinition"]
+
+
+class EventDefinition(SolcNode):
+    """An ``event`` definition."""
+
+    name: str
+    nameLocation: str | None = None
+    anonymous: bool
+    eventSelector: str | None = None
+    documentation: "StructuredDocumentation | str | None" = None
+    parameters: ParameterList
+    nodeType: Literal["EventDefinition"]
+
+
+class ModifierInvocation(SolcNode):
+    """A modifier (or base-constructor) invocation on a function definition."""
+
+    arguments: "list[Expression] | None" = None
+    kind: Literal["modifierInvocation", "baseConstructorSpecifier"] | None = None
+    modifierName: "Identifier | IdentifierPath"
+    nodeType: Literal["ModifierInvocation"]
+
+
+class ModifierDefinition(SolcNode):
+    """A ``modifier`` definition."""
+
+    name: str
+    nameLocation: str | None = None
+    baseModifiers: list[int] | None = None
+    body: "Block | None" = None
+    documentation: "StructuredDocumentation | str | None" = None
+    overrides: OverrideSpecifier | None = None
+    parameters: ParameterList
+    # `virtual` only exists from solc 0.6, and pre-0.6 everything was implicitly
+    # overridable — None (unknown), not False; LENIENT_REQUIRED + VERSION_GATES.
+    virtual: bool | None = None
+    visibility: Visibility
+    nodeType: Literal["ModifierDefinition"]
+
+
+class FunctionDefinition(SolcNode):
+    """A function, constructor, receive/fallback, or free-function definition."""
+
+    name: str
+    nameLocation: str | None = None
+    baseFunctions: list[int] | None = None
+    body: "Block | None" = None
+    documentation: "StructuredDocumentation | str | None" = None
+    functionSelector: str | None = None
+    implemented: bool
+    # Absent pre-0.5 (solc 0.4 marks constructors via `isConstructor`); LENIENT_REQUIRED.
+    kind: Literal["function", "receive", "constructor", "fallback", "freeFunction"] | None = None
+    modifiers: list[ModifierInvocation]
+    overrides: OverrideSpecifier | None = None
+    parameters: ParameterList
+    returnParameters: ParameterList
+    scope: int
+    stateMutability: StateMutability
+    # `virtual` only exists from solc 0.6, and pre-0.6 everything was implicitly
+    # overridable — None (unknown), not False; LENIENT_REQUIRED + VERSION_GATES.
+    virtual: bool | None = None
+    visibility: Visibility
+    # Legacy-only fields, not in the schema (FIELD_ALLOWLIST): solc 0.4 flags in
+    # place of `kind`/`stateMutability`, and the 0.4/0.5 predecessor of
+    # `baseFunctions`.
+    isConstructor: bool | None = None
+    isDeclaredConst: bool | None = None
+    payable: bool | None = None
+    superFunction: int | None = None
+    nodeType: Literal["FunctionDefinition"]
+
+    @property
+    def effective_kind(self) -> Literal["function", "receive", "constructor", "fallback", "freeFunction"]:
+        """``kind`` with the solc-0.4 case derived from ``isConstructor``/the empty
+        name (0.4's unnamed fallback function) — never None."""
+        if self.kind is not None:
+            return self.kind
+        if self.isConstructor:
+            return "constructor"
+        return "fallback" if self.name == "" else "function"
+
+
+class SymbolAlias(BaseModel):
+    """One ``{symbol as local}`` entry of an ImportDirective's symbolAliases."""
+
+    model_config = ConfigDict(extra="allow")
+
+    foreign: "Identifier"
+    local: str | None = None
+    nameLocation: str | None = None
+
+
+class ImportDirective(SolcNode):
+    """An ``import`` directive."""
+
+    absolutePath: str
+    file: str
+    nameLocation: str | None = None
+    scope: int
+    sourceUnit: int
+    symbolAliases: list[SymbolAlias]
+    unitAlias: str
+    nodeType: Literal["ImportDirective"]
+
+
+class InheritanceSpecifier(SolcNode):
+    """A base contract in a contract's inheritance list."""
+
+    arguments: "list[Expression] | None" = None
+    baseName: "UserDefinedTypeName | IdentifierPath"
+    nodeType: Literal["InheritanceSpecifier"]
+
+
+class PragmaDirective(SolcNode):
+    """A ``pragma`` directive; ``literals`` holds its tokenized pieces."""
+
+    literals: list[str]
+    nodeType: Literal["PragmaDirective"]
+
+
+class StorageLayoutSpecifier(SolcNode):
+    """A ``layout at <expr>`` storage-layout specifier (solc >= 0.8.29)."""
+
+    baseSlotExpression: "Expression"
+    nodeType: Literal["StorageLayoutSpecifier"]
+
+
+class StructDefinition(SolcNode):
+    """A ``struct`` definition."""
+
+    name: str
+    nameLocation: str | None = None
+    canonicalName: str
+    members: list[VariableDeclaration]
+    scope: int
+    visibility: Visibility
+    documentation: StructuredDocumentation | None = None
+    nodeType: Literal["StructDefinition"]
+
+
+class UserDefinedValueTypeDefinition(SolcNode):
+    """A ``type X is <elementary>`` definition (solc >= 0.8.8)."""
+
+    name: str
+    nameLocation: str | None = None
+    canonicalName: str | None = None
+    underlyingType: "TypeName"
+    nodeType: Literal["UserDefinedValueTypeDefinition"]
+
+
+class UsingForFunction(BaseModel):
+    """A plain ``{function: <path>}`` entry of a UsingForDirective's functionList."""
+
+    model_config = ConfigDict(extra="allow")
+
+    function: "IdentifierPath"
+
+
+class UsingForOperator(BaseModel):
+    """An ``{operator as <path>}`` entry of a UsingForDirective's functionList."""
+
+    model_config = ConfigDict(extra="allow")
+
+    operator: Literal[
+        "&", "|", "^", "~", "+", "-", "*", "/", "%", "==", "!=", "<", "<=", ">", ">="
+    ]
+    definition: "IdentifierPath"
+
+
+class UsingForDirective(SolcNode):
+    """A ``using ... for ...`` directive."""
+
+    functionList: list[UsingForFunction | UsingForOperator] | None = None
+    global_: bool | None = Field(default=None, alias="global")
+    libraryName: "UserDefinedTypeName | IdentifierPath | None" = None
+    typeName: "TypeName | None" = None
+    nodeType: Literal["UsingForDirective"]
+
+
+class ContractDefinition(SolcNode):
+    """A contract, interface, or library definition."""
+
+    name: str
+    nameLocation: str | None = None
+    # Schema-required, but the concept only exists from solc 0.6 — a default keeps
+    # below-floor (0.5.x) sources parseable (lenient-older policy; conformance
+    # deviation LENIENT_REQUIRED).
+    abstract: bool = False
+    baseContracts: list[InheritanceSpecifier]
+    canonicalName: str | None = None
+    contractDependencies: list[int]
+    contractKind: Literal["contract", "interface", "library"]
+    # NatSpec is a plain string in dumps from solc <= 0.5 (node form from 0.6);
+    # same widening on Function/Modifier/EventDefinition. DELIBERATELY_OPEN.
+    documentation: "StructuredDocumentation | str | None" = None
+    fullyImplemented: bool
+    linearizedBaseContracts: list[int]
+    nodes: list["ContractBodyNode"]
+    scope: int
+    usedErrors: list[int] | None = None
+    usedEvents: list[int] | None = None
+    internalFunctionIDs: dict[str, int] | None = None
+    storageLayout: StorageLayoutSpecifier | None = None
+    nodeType: Literal["ContractDefinition"]
+
+    @field_validator("internalFunctionIDs", mode="before")
+    @classmethod
+    def _drop_injected_contract_name(cls, value: object) -> object:
+        # certoraRun's certora_contract_name stamping walks every dict under a
+        # ContractDefinition, including this plain function-id map; drop the injected
+        # string entry so the values stay int-typed.
+        if isinstance(value, dict):
+            return {k: v for k, v in value.items() if k != "certora_contract_name"}
+        return value
+
+
+class SourceUnit(SolcNode):
+    """The root node of one source file's AST (the schema's top-level object)."""
+
+    absolutePath: str
+    exportedSymbols: dict[str, list[int]]
+    experimentalSolidity: bool | None = None
+    license: str | None = None
+    nodes: list["SourceUnitNode"]
+    nodeType: Literal["SourceUnit"]
diff --git a/certora_autosetup/solidity_ast/diagnostics.py b/certora_autosetup/solidity_ast/diagnostics.py
new file mode 100644
index 0000000..6bd3a1b
--- /dev/null
+++ b/certora_autosetup/solidity_ast/diagnostics.py
@@ -0,0 +1,70 @@
+"""Fidelity diagnostics: does a typed tree serialize back to the exact source JSON?
+
+Used by the round-trip tests and by ``python -m certora_autosetup.solidity_ast`` to
+validate the models against real dumps at scale.
+"""
+
+from __future__ import annotations
+
+from typing import Any
+
+from .loader import SourceAst
+
+
+def roundtrip_diffs(source: SourceAst, limit: int = 50) -> list[str]:
+    """Structural differences between ``source.root`` re-serialized and the raw
+    SourceUnit JSON it was parsed from (empty list == byte-loyal modulo key order).
+
+    ``model_dump(exclude_unset=True)`` keeps exactly the fields present in the input
+    (absent optional fields stay absent, explicit nulls stay null, unknown fields ride
+    along in ``model_extra``). The one deliberate normalization is reversed before
+    comparing: the certoraRun contract-name stamp that lands inside the plain
+    ``internalFunctionIDs`` map is dropped by the model, so it is dropped from the
+    raw side too.
+    """
+    if source.root is None:
+        return []
+    raw_root = next(
+        n
+        for n in source.raw.values()
+        if isinstance(n, dict) and n.get("nodeType") == "SourceUnit"
+    )
+    dumped = source.root.model_dump(mode="json", by_alias=True, exclude_unset=True)
+    expected = _drop_internal_function_id_stamp(raw_root)
+    diffs: list[str] = []
+    _diff(dumped, expected, "", diffs, limit)
+    return diffs
+
+
+def _drop_internal_function_id_stamp(node: Any) -> Any:
+    if isinstance(node, dict):
+        out = {}
+        for key, value in node.items():
+            if key == "internalFunctionIDs" and isinstance(value, dict):
+                value = {k: v for k, v in value.items() if k != "certora_contract_name"}
+            out[key] = _drop_internal_function_id_stamp(value)
+        return out
+    if isinstance(node, list):
+        return [_drop_internal_function_id_stamp(item) for item in node]
+    return node
+
+
+def _diff(dumped: Any, original: Any, path: str, out: list[str], limit: int) -> None:
+    if len(out) >= limit:
+        return
+    if isinstance(dumped, dict) and isinstance(original, dict):
+        for key in sorted(dumped.keys() | original.keys()):
+            if key not in original:
+                out.append(f"{path}.{key}: only in re-serialized output")
+            elif key not in dumped:
+                out.append(f"{path}.{key}: lost from the original")
+            else:
+                _diff(dumped[key], original[key], f"{path}.{key}", out, limit)
+    elif isinstance(dumped, list) and isinstance(original, list):
+        if len(dumped) != len(original):
+            out.append(f"{path}: list length {len(dumped)} != {len(original)}")
+        else:
+            for i, (d, o) in enumerate(zip(dumped, original)):
+                _diff(d, o, f"{path}[{i}]", out, limit)
+    elif dumped != original:
+        out.append(f"{path}: {dumped!r} != {original!r}")
diff --git a/certora_autosetup/solidity_ast/expressions.py b/certora_autosetup/solidity_ast/expressions.py
new file mode 100644
index 0000000..c719b19
--- /dev/null
+++ b/certora_autosetup/solidity_ast/expressions.py
@@ -0,0 +1,224 @@
+"""Expression nodes of the Solidity compact AST (members of the Expression union)."""
+
+from __future__ import annotations
+
+# The AST node class `Literal` below shadows typing.Literal, so this module uses
+# `typing.Literal[...]` for all tag/enum annotations instead of importing the name.
+import typing
+
+from .base import SolcNode, TypeDescriptions
+
+if typing.TYPE_CHECKING:
+    from .types import ElementaryTypeName
+    from .unions import Expression, TypeName
+
+
+class Assignment(SolcNode):
+    argumentTypes: list[TypeDescriptions] | None = None
+    isConstant: bool
+    isLValue: bool
+    isPure: bool
+    lValueRequested: bool
+    typeDescriptions: TypeDescriptions
+    leftHandSide: "Expression"
+    operator: typing.Literal[
+        "=", "+=", "-=", "*=", "/=", "%=", "|=", "&=", "^=", ">>=", "<<="
+    ]
+    rightHandSide: "Expression"
+    nodeType: typing.Literal["Assignment"]
+
+
+class BinaryOperation(SolcNode):
+    argumentTypes: list[TypeDescriptions] | None = None
+    isConstant: bool
+    isLValue: bool
+    isPure: bool
+    lValueRequested: bool
+    typeDescriptions: TypeDescriptions
+    commonType: TypeDescriptions
+    leftExpression: "Expression"
+    operator: typing.Literal[
+        "+", "-", "*", "/", "%", "**", "&&", "||", "!=", "==",
+        "<", "<=", ">", ">=", "^", "&", "|", "<<", ">>",
+    ]
+    rightExpression: "Expression"
+    function: int | None = None
+    nodeType: typing.Literal["BinaryOperation"]
+
+
+class Conditional(SolcNode):
+    """A ternary ``condition ? trueExpression : falseExpression``."""
+
+    argumentTypes: list[TypeDescriptions] | None = None
+    isConstant: bool
+    isLValue: bool
+    isPure: bool
+    lValueRequested: bool
+    typeDescriptions: TypeDescriptions
+    condition: "Expression"
+    falseExpression: "Expression"
+    trueExpression: "Expression"
+    nodeType: typing.Literal["Conditional"]
+
+
+class ElementaryTypeNameExpression(SolcNode):
+    """An elementary type used as an expression, e.g. the callee in ``uint256(x)``."""
+
+    argumentTypes: list[TypeDescriptions] | None = None
+    isConstant: bool
+    isLValue: bool
+    isPure: bool
+    lValueRequested: bool
+    typeDescriptions: TypeDescriptions
+    # A plain string ("uint256") in dumps from solc <= 0.5; DELIBERATELY_OPEN.
+    typeName: "ElementaryTypeName | str"
+    nodeType: typing.Literal["ElementaryTypeNameExpression"]
+
+
+class FunctionCall(SolcNode):
+    """A call, type conversion, or struct constructor call (see ``kind``)."""
+
+    argumentTypes: list[TypeDescriptions] | None = None
+    isConstant: bool
+    isLValue: bool
+    isPure: bool
+    lValueRequested: bool
+    typeDescriptions: TypeDescriptions
+    arguments: list["Expression"]
+    expression: "Expression"
+    kind: typing.Literal["functionCall", "typeConversion", "structConstructorCall"]
+    names: list[str]
+    nameLocations: list[str] | None = None
+    # try/catch only exists from solc 0.6; LENIENT_REQUIRED.
+    tryCall: bool = False
+    nodeType: typing.Literal["FunctionCall"]
+
+
+class FunctionCallOptions(SolcNode):
+    """Call options attached to a callee, e.g. ``f{value: 1, gas: 2}``."""
+
+    argumentTypes: list[TypeDescriptions] | None = None
+    isConstant: bool
+    isLValue: bool | None = None
+    isPure: bool
+    lValueRequested: bool
+    typeDescriptions: TypeDescriptions
+    expression: "Expression"
+    names: list[str]
+    options: list["Expression"]
+    nodeType: typing.Literal["FunctionCallOptions"]
+
+
+class Identifier(SolcNode):
+    argumentTypes: list[TypeDescriptions] | None = None
+    name: str
+    overloadedDeclarations: list[int]
+    referencedDeclaration: int | None = None
+    typeDescriptions: TypeDescriptions
+    nodeType: typing.Literal["Identifier"]
+
+
+class IndexAccess(SolcNode):
+    argumentTypes: list[TypeDescriptions] | None = None
+    isConstant: bool
+    isLValue: bool
+    isPure: bool
+    lValueRequested: bool
+    typeDescriptions: TypeDescriptions
+    baseExpression: "Expression"
+    indexExpression: "Expression | None" = None
+    nodeType: typing.Literal["IndexAccess"]
+
+
+class IndexRangeAccess(SolcNode):
+    """An array slice, e.g. ``arr[1:3]`` (calldata arrays only)."""
+
+    argumentTypes: list[TypeDescriptions] | None = None
+    isConstant: bool
+    isLValue: bool
+    isPure: bool
+    lValueRequested: bool
+    typeDescriptions: TypeDescriptions
+    baseExpression: "Expression"
+    endExpression: "Expression | None" = None
+    startExpression: "Expression | None" = None
+    nodeType: typing.Literal["IndexRangeAccess"]
+
+
+class Literal(SolcNode):
+    """A literal value (number, string, bool, ...); shadows ``typing.Literal`` here."""
+
+    argumentTypes: list[TypeDescriptions] | None = None
+    isConstant: bool
+    isLValue: bool
+    isPure: bool
+    lValueRequested: bool
+    typeDescriptions: TypeDescriptions
+    hexValue: str
+    kind: typing.Literal["bool", "number", "string", "hexString", "unicodeString"]
+    subdenomination: (
+        typing.Literal[
+            "seconds", "minutes", "hours", "days", "weeks",
+            "wei", "gwei", "ether", "finney", "szabo",
+        ]
+        | None
+    ) = None
+    value: str | None = None
+    nodeType: typing.Literal["Literal"]
+
+
+class MemberAccess(SolcNode):
+    argumentTypes: list[TypeDescriptions] | None = None
+    isConstant: bool
+    # solc 0.7.2 (only) omits isLValue on enum-member accesses — a compiler bug
+    # window, not an introduction gate; LENIENT_REQUIRED, no VERSION_GATES entry.
+    isLValue: bool | None = None
+    isPure: bool
+    lValueRequested: bool
+    typeDescriptions: TypeDescriptions
+    expression: "Expression"
+    memberName: str
+    memberLocation: str | None = None
+    referencedDeclaration: int | None = None
+    nodeType: typing.Literal["MemberAccess"]
+
+
+class NewExpression(SolcNode):
+    """A ``new T`` expression (contract creation or dynamic-array allocation)."""
+
+    argumentTypes: list[TypeDescriptions] | None = None
+    isConstant: bool
+    isLValue: bool | None = None
+    isPure: bool
+    lValueRequested: bool
+    typeDescriptions: TypeDescriptions
+    typeName: "TypeName"
+    nodeType: typing.Literal["NewExpression"]
+
+
+class TupleExpression(SolcNode):
+    """A tuple or inline array; ``components`` has None holes for omitted entries."""
+
+    argumentTypes: list[TypeDescriptions] | None = None
+    isConstant: bool
+    isLValue: bool
+    isPure: bool
+    lValueRequested: bool
+    typeDescriptions: TypeDescriptions
+    components: list["Expression | None"]
+    isInlineArray: bool
+    nodeType: typing.Literal["TupleExpression"]
+
+
+class UnaryOperation(SolcNode):
+    argumentTypes: list[TypeDescriptions] | None = None
+    isConstant: bool
+    isLValue: bool
+    isPure: bool
+    lValueRequested: bool
+    typeDescriptions: TypeDescriptions
+    operator: typing.Literal["++", "--", "-", "!", "delete", "~"]
+    prefix: bool
+    subExpression: "Expression"
+    function: int | None = None
+    nodeType: typing.Literal["UnaryOperation"]
diff --git a/certora_autosetup/solidity_ast/loader.py b/certora_autosetup/solidity_ast/loader.py
new file mode 100644
index 0000000..2ba51e4
--- /dev/null
+++ b/certora_autosetup/solidity_ast/loader.py
@@ -0,0 +1,264 @@
+"""Typed loader for the ``.asts.json`` dump written by ``certoraRun --dump_asts``.
+
+The dump is a three-level dict ``{original_file: {source_file: {node_id_str: node}}}``:
+the outer key is the contract file the compiler was invoked on, the middle key is every
+source in that compilation unit, and the inner map is a flat id-index whose values are
+the same nodes that also appear nested inside their parents. The loader therefore
+validates each source's SourceUnit tree exactly once and derives the id-index by
+traversal, keeping the raw flat map alongside for fallback and byte-compatible uses.
+
+Degradation policy (a project that compiles must never fail because of this loader):
+an unrecognized ``nodeType`` becomes an ``UnknownNode`` inside an otherwise-typed tree;
+a source whose shape the models reject entirely is kept raw as ``parse_failed``;
+Vyper sources (``ast_type``/``node_id`` dialect) are kept raw as ``vyper``.
+"""
+
+from __future__ import annotations
+
+import json
+import logging
+from dataclasses import dataclass, field
+from pathlib import Path
+from typing import Any, Callable, Iterator, Literal, TypeVar, get_args
+
+import ijson
+from packaging.version import Version
+from pydantic import ValidationError
+
+from . import unions as unions  # import resolves forward refs and rebuilds the models
+from .base import AstNode
+from .declarations import SourceUnit
+from .traversal import build_node_index, find_all, walk
+
+# Fields the models keep lenient (see LENIENT_REQUIRED in the conformance test) but
+# that MUST be present in dumps from the solc version that introduced them onward.
+# When the caller knows the producing version (autosetup always does), absence at or
+# above the gate is a hard error — wrong results are worse than a failed parse.
+# Gates err late where the exact introduction is unverified (never crash wrongly on
+# a version that genuinely lacked the field); tightened as fixture evidence grows.
+VERSION_GATES: dict[str, dict[str, Version]] = {
+    "ContractDefinition": {"abstract": Version("0.6.0")},
+    "FunctionDefinition": {"kind": Version("0.5.0"), "virtual": Version("0.6.0")},
+    "ModifierDefinition": {"virtual": Version("0.6.0")},
+    "FunctionCall": {"tryCall": Version("0.6.0")},
+    "VariableDeclaration": {"mutability": Version("0.6.6")},
+    "InlineAssembly": {"AST": Version("0.6.0"), "evmVersion": Version("0.6.2")},
+}
+
+
+def _version_gate_violation(root: AstNode, solc_version: Version) -> str | None:
+    """First gated field that is absent although the producing solc must emit it."""
+    for node in walk(root):
+        gates = VERSION_GATES.get(type(node).__name__)
+        if not gates:
+            continue
+        for field_name, gate in gates.items():
+            if solc_version >= gate and field_name not in node.model_fields_set:
+                return (
+                    f"{type(node).__name__}.{field_name} absent, but solc "
+                    f"{solc_version} (>= {gate}) always emits it"
+                )
+    return None
+
+logger = logging.getLogger(__name__)
+
+RawKind = Literal["solidity", "vyper", "parse_failed"]
+OnError = Literal["raw", "raise"]
+
+
+@dataclass
+class SourceAst:
+    """One source file's AST within a compilation unit."""
+
+    source_path: str
+    root: SourceUnit | None
+    nodes: dict[int, AstNode] = field(default_factory=dict)
+    raw: dict[str, Any] = field(default_factory=dict)
+    raw_kind: RawKind = "solidity"
+    parse_error: str | None = None
+
+    @property
+    def is_parsed(self) -> bool:
+        return self.root is not None
+
+
+@dataclass
+class FileAsts:
+    """All source ASTs of one compilation unit (one outer key of the dump)."""
+
+    original_file: str
+    sources: dict[str, SourceAst]
+
+
+@dataclass
+class AstDump:
+    """The full, typed view of a ``.asts.json`` dump."""
+
+    files: dict[str, FileAsts]
+
+    @classmethod
+    def load(
+        cls,
+        path: Path | str,
+        *,
+        on_error: OnError = "raw",
+        solc_version: str | Version | None = None,
+    ) -> "AstDump":
+        """``solc_version``: the compiler that produced the dump, when known —
+        enables the VERSION_GATES check (a gated field absent at or above its gate
+        fails the source instead of silently reading as None)."""
+        with open(path, "r", encoding="utf-8") as f:
+            return cls.from_dict(json.load(f), on_error=on_error, solc_version=solc_version)
+
+    @classmethod
+    def stream_units(
+        cls,
+        path: Path | str,
+        *,
+        on_error: OnError = "raw",
+        solc_version: str | Version | None = None,
+        unit_filter: Callable[[str], bool] | None = None,
+    ) -> Iterator[FileAsts]:
+        """Stream the dump one compilation unit (outer key) at a time — the dump can
+        be multi-GB, and whole-file loading OOMs constrained runs; peak memory here
+        is bounded by the largest single unit. ``unit_filter`` (on the outer key)
+        skips units before any validation work. Consumers must drop each unit before
+        taking the next.
+        """
+        version = Version(solc_version) if isinstance(solc_version, str) else solc_version
+        for original_file, per_source in stream_raw_units(path):
+            if unit_filter is not None and not unit_filter(original_file):
+                continue
+            yield FileAsts(
+                original_file=original_file,
+                sources={
+                    source_path: _load_source(source_path, flat, on_error, version)
+                    for source_path, flat in per_source.items()
+                },
+            )
+
+    @classmethod
+    def from_dict(
+        cls,
+        data: dict[str, Any],
+        *,
+        on_error: OnError = "raw",
+        solc_version: str | Version | None = None,
+    ) -> "AstDump":
+        version = Version(solc_version) if isinstance(solc_version, str) else solc_version
+        files = {
+            original_file: FileAsts(
+                original_file=original_file,
+                sources={
+                    source_path: _load_source(source_path, flat, on_error, version)
+                    for source_path, flat in per_source.items()
+                },
+            )
+            for original_file, per_source in data.items()
+        }
+        return cls(files=files)
+
+    def iter_sources(self) -> Iterator[tuple[str, SourceAst]]:
+        """(original_file, SourceAst) over every source, including vyper/failed ones."""
+        for file_asts in self.files.values():
+            for source in file_asts.sources.values():
+                yield file_asts.original_file, source
+
+    def iter_parsed_roots(self) -> Iterator[tuple[str, str, SourceUnit]]:
+        """(original_file, source_path, SourceUnit) over successfully parsed sources."""
+        for original_file, source in self.iter_sources():
+            if source.root is not None:
+                yield original_file, source.source_path, source.root
+
+    def find_node(self, source_path: str, node_id: int) -> AstNode | None:
+        for file_asts in self.files.values():
+            source = file_asts.sources.get(source_path)
+            if source is not None and node_id in source.nodes:
+                return source.nodes[node_id]
+        return None
+
+
+N = TypeVar("N", bound=AstNode)
+
+
+def iter_nodes_of_type(source: SourceAst, model: type[N]) -> Iterator[N | dict[str, Any]]:
+    """All nodes of one concrete model type in a source: typed instances from the
+    parsed tree first, then the raw flat-map dicts of matching nodeType that the
+    typed walk did not reach (nested under an UnknownNode, or the whole source
+    unparsable). Gives exact-parity coverage with a raw flat-map scan while staying
+    typed wherever the models reached; callers must accept both shapes.
+    """
+    (node_type,) = get_args(model.model_fields["nodeType"].annotation)
+    seen: set[int] = set()
+    if source.root is not None:
+        for node in find_all(source.root, model):
+            node_id = getattr(node, "id", None)  # Yul models carry no id
+            if isinstance(node_id, int):
+                seen.add(node_id)
+            yield node
+    for raw_node in source.raw.values():
+        if (
+            isinstance(raw_node, dict)
+            and raw_node.get("nodeType") == node_type
+            and raw_node.get("id") not in seen
+        ):
+            yield raw_node
+
+
+def stream_raw_units(path: Path | str) -> Iterator[tuple[str, dict[str, Any]]]:
+    """Stream raw ``(original_file, {source_path: flat_node_map})`` pairs without any
+    model validation — for raw-only passes like the legacy parent-graph builder."""
+    with open(path, "rb") as f:
+        yield from ijson.kvitems(f, "")
+
+
+def _load_source(
+    source_path: str,
+    flat: dict[str, Any],
+    on_error: OnError,
+    solc_version: Version | None = None,
+) -> SourceAst:
+    node_dicts = [n for n in flat.values() if isinstance(n, dict)]
+
+    has_solidity = any("nodeType" in n for n in node_dicts)
+    has_vyper = any("nodeType" not in n and ("ast_type" in n or "node_id" in n) for n in node_dicts)
+    if has_vyper and not has_solidity:
+        return SourceAst(source_path=source_path, root=None, raw=flat, raw_kind="vyper")
+
+    roots = [n for n in node_dicts if n.get("nodeType") == "SourceUnit"]
+    if len(roots) != 1:
+        return _failed(
+            source_path, flat, f"expected exactly one SourceUnit node, found {len(roots)}", on_error
+        )
+
+    try:
+        root = SourceUnit.model_validate(roots[0])
+    except ValidationError as e:
+        if on_error == "raise":
+            raise
+        return _failed(
+            source_path, flat, f"{e.error_count()} validation error(s): {e.errors()[0]}", on_error
+        )
+
+    if solc_version is not None:
+        violation = _version_gate_violation(root, solc_version)
+        if violation:
+            return _failed(source_path, flat, f"version-gate violation: {violation}", on_error)
+
+    nodes = build_node_index(root)
+    missing = [i for i in flat if i.isdigit() and int(i) not in nodes]
+    if missing:
+        logger.debug(
+            "%s: %d raw index ids not reached by typed traversal (first: %s)",
+            source_path, len(missing), missing[0],
+        )
+    return SourceAst(source_path=source_path, root=root, nodes=nodes, raw=flat)
+
+
+def _failed(source_path: str, flat: dict[str, Any], msg: str, on_error: OnError) -> SourceAst:
+    if on_error == "raise":
+        raise ValueError(f"failed to parse AST of {source_path}: {msg}")
+    logger.warning("falling back to raw AST for %s: %s", source_path, msg)
+    return SourceAst(
+        source_path=source_path, root=None, raw=flat, raw_kind="parse_failed", parse_error=msg
+    )
diff --git a/certora_autosetup/solidity_ast/schema/NOTICE b/certora_autosetup/solidity_ast/schema/NOTICE
new file mode 100644
index 0000000..b2a431f
--- /dev/null
+++ b/certora_autosetup/solidity_ast/schema/NOTICE
@@ -0,0 +1,17 @@
+schema.json is vendored from the OpenZeppelin `solidity-ast` npm package.
+
+  Package:  solidity-ast
+  Version:  0.4.62
+  Source:   https://unpkg.com/solidity-ast@0.4.62/schema.json
+  Project:  https://github.com/OpenZeppelin/solidity-ast
+  License:  MIT (Copyright (c) 2020 OpenZeppelin) — see the project repository
+            for the full license text.
+
+It is a JSON Schema (draft-06) of the Solidity compiler's compact JSON AST,
+unioning solc versions >= 0.6: fields added in later solc releases are optional,
+fields whose value can be null are anyOf-nullable.
+
+To refresh: pick an explicit version and run
+  curl -sL https://unpkg.com/solidity-ast@<version>/schema.json -o schema.json
+then update this NOTICE and re-run tests/solidity_ast/ (the conformance test
+will point at any model fields that need to follow).
diff --git a/certora_autosetup/solidity_ast/schema/schema.json b/certora_autosetup/solidity_ast/schema/schema.json
new file mode 100644
index 0000000..ac72844
--- /dev/null
+++ b/certora_autosetup/solidity_ast/schema/schema.json
@@ -0,0 +1,4015 @@
+{
+  "$schema": "http://json-schema.org/draft-06/schema#",
+  "title": "SourceUnit",
+  "type": "object",
+  "additionalProperties": false,
+  "properties": {
+    "id": {
+      "type": "integer"
+    },
+    "src": {
+      "$ref": "#/definitions/SourceLocation"
+    },
+    "absolutePath": {
+      "type": "string"
+    },
+    "exportedSymbols": {
+      "type": "object",
+      "additionalProperties": {
+        "type": "array",
+        "items": {
+          "type": "integer"
+        }
+      }
+    },
+    "experimentalSolidity": {
+      "type": "boolean"
+    },
+    "license": {
+      "anyOf": [
+        {
+          "type": "string"
+        },
+        {
+          "type": "null"
+        }
+      ]
+    },
+    "nodes": {
+      "type": "array",
+      "items": {
+        "anyOf": [
+          {
+            "$ref": "#/definitions/ContractDefinition"
+          },
+          {
+            "$ref": "#/definitions/EnumDefinition"
+          },
+          {
+            "$ref": "#/definitions/ErrorDefinition"
+          },
+          {
+            "$ref": "#/definitions/FunctionDefinition"
+          },
+          {
+            "$ref": "#/definitions/ImportDirective"
+          },
+          {
+            "$ref": "#/definitions/PragmaDirective"
+          },
+          {
+            "$ref": "#/definitions/StructDefinition"
+          },
+          {
+            "$ref": "#/definitions/UserDefinedValueTypeDefinition"
+          },
+          {
+            "$ref": "#/definitions/UsingForDirective"
+          },
+          {
+            "$ref": "#/definitions/VariableDeclaration"
+          }
+        ]
+      }
+    },
+    "nodeType": {
+      "enum": [
+        "SourceUnit"
+      ]
+    }
+  },
+  "required": [
+    "id",
+    "src",
+    "absolutePath",
+    "exportedSymbols",
+    "nodes",
+    "nodeType"
+  ],
+  "definitions": {
+    "SourceLocation": {
+      "type": "string",
+      "pattern": "^\\d+:\\d+:\\d+$"
+    },
+    "Mutability": {
+      "enum": [
+        "mutable",
+        "immutable",
+        "constant"
+      ]
+    },
+    "StateMutability": {
+      "enum": [
+        "payable",
+        "pure",
+        "nonpayable",
+        "view"
+      ]
+    },
+    "StorageLocation": {
+      "enum": [
+        "calldata",
+        "default",
+        "memory",
+        "storage",
+        "transient"
+      ]
+    },
+    "Visibility": {
+      "enum": [
+        "external",
+        "public",
+        "internal",
+        "private"
+      ]
+    },
+    "TypeDescriptions": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "typeIdentifier": {
+          "anyOf": [
+            {
+              "type": "string"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "typeString": {
+          "anyOf": [
+            {
+              "type": "string"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        }
+      },
+      "required": []
+    },
+    "Expression": {
+      "anyOf": [
+        {
+          "$ref": "#/definitions/Assignment"
+        },
+        {
+          "$ref": "#/definitions/BinaryOperation"
+        },
+        {
+          "$ref": "#/definitions/Conditional"
+        },
+        {
+          "$ref": "#/definitions/ElementaryTypeNameExpression"
+        },
+        {
+          "$ref": "#/definitions/FunctionCall"
+        },
+        {
+          "$ref": "#/definitions/FunctionCallOptions"
+        },
+        {
+          "$ref": "#/definitions/Identifier"
+        },
+        {
+          "$ref": "#/definitions/IndexAccess"
+        },
+        {
+          "$ref": "#/definitions/IndexRangeAccess"
+        },
+        {
+          "$ref": "#/definitions/Literal"
+        },
+        {
+          "$ref": "#/definitions/MemberAccess"
+        },
+        {
+          "$ref": "#/definitions/NewExpression"
+        },
+        {
+          "$ref": "#/definitions/TupleExpression"
+        },
+        {
+          "$ref": "#/definitions/UnaryOperation"
+        }
+      ]
+    },
+    "Statement": {
+      "anyOf": [
+        {
+          "$ref": "#/definitions/Block"
+        },
+        {
+          "$ref": "#/definitions/Break"
+        },
+        {
+          "$ref": "#/definitions/Continue"
+        },
+        {
+          "$ref": "#/definitions/DoWhileStatement"
+        },
+        {
+          "$ref": "#/definitions/EmitStatement"
+        },
+        {
+          "$ref": "#/definitions/ExpressionStatement"
+        },
+        {
+          "$ref": "#/definitions/ForStatement"
+        },
+        {
+          "$ref": "#/definitions/IfStatement"
+        },
+        {
+          "$ref": "#/definitions/InlineAssembly"
+        },
+        {
+          "$ref": "#/definitions/PlaceholderStatement"
+        },
+        {
+          "$ref": "#/definitions/Return"
+        },
+        {
+          "$ref": "#/definitions/RevertStatement"
+        },
+        {
+          "$ref": "#/definitions/TryStatement"
+        },
+        {
+          "$ref": "#/definitions/UncheckedBlock"
+        },
+        {
+          "$ref": "#/definitions/VariableDeclarationStatement"
+        },
+        {
+          "$ref": "#/definitions/WhileStatement"
+        }
+      ]
+    },
+    "TypeName": {
+      "anyOf": [
+        {
+          "$ref": "#/definitions/ArrayTypeName"
+        },
+        {
+          "$ref": "#/definitions/ElementaryTypeName"
+        },
+        {
+          "$ref": "#/definitions/FunctionTypeName"
+        },
+        {
+          "$ref": "#/definitions/Mapping"
+        },
+        {
+          "$ref": "#/definitions/UserDefinedTypeName"
+        }
+      ]
+    },
+    "ArrayTypeName": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "typeDescriptions": {
+          "$ref": "#/definitions/TypeDescriptions"
+        },
+        "baseType": {
+          "$ref": "#/definitions/TypeName"
+        },
+        "length": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/Expression"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "nodeType": {
+          "enum": [
+            "ArrayTypeName"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "typeDescriptions",
+        "baseType",
+        "nodeType"
+      ]
+    },
+    "Assignment": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "argumentTypes": {
+          "anyOf": [
+            {
+              "type": "array",
+              "items": {
+                "$ref": "#/definitions/TypeDescriptions"
+              }
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "isConstant": {
+          "type": "boolean"
+        },
+        "isLValue": {
+          "type": "boolean"
+        },
+        "isPure": {
+          "type": "boolean"
+        },
+        "lValueRequested": {
+          "type": "boolean"
+        },
+        "typeDescriptions": {
+          "$ref": "#/definitions/TypeDescriptions"
+        },
+        "leftHandSide": {
+          "$ref": "#/definitions/Expression"
+        },
+        "operator": {
+          "enum": [
+            "=",
+            "+=",
+            "-=",
+            "*=",
+            "/=",
+            "%=",
+            "|=",
+            "&=",
+            "^=",
+            ">>=",
+            "<<="
+          ]
+        },
+        "rightHandSide": {
+          "$ref": "#/definitions/Expression"
+        },
+        "nodeType": {
+          "enum": [
+            "Assignment"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "isConstant",
+        "isLValue",
+        "isPure",
+        "lValueRequested",
+        "typeDescriptions",
+        "leftHandSide",
+        "operator",
+        "rightHandSide",
+        "nodeType"
+      ]
+    },
+    "BinaryOperation": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "argumentTypes": {
+          "anyOf": [
+            {
+              "type": "array",
+              "items": {
+                "$ref": "#/definitions/TypeDescriptions"
+              }
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "isConstant": {
+          "type": "boolean"
+        },
+        "isLValue": {
+          "type": "boolean"
+        },
+        "isPure": {
+          "type": "boolean"
+        },
+        "lValueRequested": {
+          "type": "boolean"
+        },
+        "typeDescriptions": {
+          "$ref": "#/definitions/TypeDescriptions"
+        },
+        "commonType": {
+          "$ref": "#/definitions/TypeDescriptions"
+        },
+        "leftExpression": {
+          "$ref": "#/definitions/Expression"
+        },
+        "operator": {
+          "enum": [
+            "+",
+            "-",
+            "*",
+            "/",
+            "%",
+            "**",
+            "&&",
+            "||",
+            "!=",
+            "==",
+            "<",
+            "<=",
+            ">",
+            ">=",
+            "^",
+            "&",
+            "|",
+            "<<",
+            ">>"
+          ]
+        },
+        "rightExpression": {
+          "$ref": "#/definitions/Expression"
+        },
+        "function": {
+          "type": "integer"
+        },
+        "nodeType": {
+          "enum": [
+            "BinaryOperation"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "isConstant",
+        "isLValue",
+        "isPure",
+        "lValueRequested",
+        "typeDescriptions",
+        "commonType",
+        "leftExpression",
+        "operator",
+        "rightExpression",
+        "nodeType"
+      ]
+    },
+    "Block": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "documentation": {
+          "type": "string"
+        },
+        "statements": {
+          "anyOf": [
+            {
+              "type": "array",
+              "items": {
+                "$ref": "#/definitions/Statement"
+              }
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "nodeType": {
+          "enum": [
+            "Block"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "nodeType"
+      ]
+    },
+    "Break": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "documentation": {
+          "type": "string"
+        },
+        "nodeType": {
+          "enum": [
+            "Break"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "nodeType"
+      ]
+    },
+    "Conditional": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "argumentTypes": {
+          "anyOf": [
+            {
+              "type": "array",
+              "items": {
+                "$ref": "#/definitions/TypeDescriptions"
+              }
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "isConstant": {
+          "type": "boolean"
+        },
+        "isLValue": {
+          "type": "boolean"
+        },
+        "isPure": {
+          "type": "boolean"
+        },
+        "lValueRequested": {
+          "type": "boolean"
+        },
+        "typeDescriptions": {
+          "$ref": "#/definitions/TypeDescriptions"
+        },
+        "condition": {
+          "$ref": "#/definitions/Expression"
+        },
+        "falseExpression": {
+          "$ref": "#/definitions/Expression"
+        },
+        "trueExpression": {
+          "$ref": "#/definitions/Expression"
+        },
+        "nodeType": {
+          "enum": [
+            "Conditional"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "isConstant",
+        "isLValue",
+        "isPure",
+        "lValueRequested",
+        "typeDescriptions",
+        "condition",
+        "falseExpression",
+        "trueExpression",
+        "nodeType"
+      ]
+    },
+    "Continue": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "documentation": {
+          "type": "string"
+        },
+        "nodeType": {
+          "enum": [
+            "Continue"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "nodeType"
+      ]
+    },
+    "ContractDefinition": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "name": {
+          "type": "string"
+        },
+        "nameLocation": {
+          "type": "string"
+        },
+        "abstract": {
+          "type": "boolean"
+        },
+        "baseContracts": {
+          "type": "array",
+          "items": {
+            "$ref": "#/definitions/InheritanceSpecifier"
+          }
+        },
+        "canonicalName": {
+          "type": "string"
+        },
+        "contractDependencies": {
+          "type": "array",
+          "items": {
+            "type": "integer"
+          }
+        },
+        "contractKind": {
+          "enum": [
+            "contract",
+            "interface",
+            "library"
+          ]
+        },
+        "documentation": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/StructuredDocumentation"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "fullyImplemented": {
+          "type": "boolean"
+        },
+        "linearizedBaseContracts": {
+          "type": "array",
+          "items": {
+            "type": "integer"
+          }
+        },
+        "nodes": {
+          "type": "array",
+          "items": {
+            "anyOf": [
+              {
+                "$ref": "#/definitions/EnumDefinition"
+              },
+              {
+                "$ref": "#/definitions/ErrorDefinition"
+              },
+              {
+                "$ref": "#/definitions/EventDefinition"
+              },
+              {
+                "$ref": "#/definitions/FunctionDefinition"
+              },
+              {
+                "$ref": "#/definitions/ModifierDefinition"
+              },
+              {
+                "$ref": "#/definitions/StructDefinition"
+              },
+              {
+                "$ref": "#/definitions/UserDefinedValueTypeDefinition"
+              },
+              {
+                "$ref": "#/definitions/UsingForDirective"
+              },
+              {
+                "$ref": "#/definitions/VariableDeclaration"
+              }
+            ]
+          }
+        },
+        "scope": {
+          "type": "integer"
+        },
+        "usedErrors": {
+          "type": "array",
+          "items": {
+            "type": "integer"
+          }
+        },
+        "usedEvents": {
+          "type": "array",
+          "items": {
+            "type": "integer"
+          }
+        },
+        "internalFunctionIDs": {
+          "type": "object",
+          "additionalProperties": {
+            "type": "integer"
+          }
+        },
+        "storageLayout": {
+          "$ref": "#/definitions/StorageLayoutSpecifier"
+        },
+        "nodeType": {
+          "enum": [
+            "ContractDefinition"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "name",
+        "abstract",
+        "baseContracts",
+        "contractDependencies",
+        "contractKind",
+        "fullyImplemented",
+        "linearizedBaseContracts",
+        "nodes",
+        "scope",
+        "nodeType"
+      ]
+    },
+    "StorageLayoutSpecifier": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "baseSlotExpression": {
+          "$ref": "#/definitions/Expression"
+        },
+        "nodeType": {
+          "enum": [
+            "StorageLayoutSpecifier"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "baseSlotExpression",
+        "nodeType"
+      ]
+    },
+    "DoWhileStatement": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "documentation": {
+          "type": "string"
+        },
+        "body": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/Block"
+            },
+            {
+              "$ref": "#/definitions/Statement"
+            }
+          ]
+        },
+        "condition": {
+          "$ref": "#/definitions/Expression"
+        },
+        "nodeType": {
+          "enum": [
+            "DoWhileStatement"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "body",
+        "condition",
+        "nodeType"
+      ]
+    },
+    "ElementaryTypeName": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "typeDescriptions": {
+          "$ref": "#/definitions/TypeDescriptions"
+        },
+        "name": {
+          "type": "string"
+        },
+        "stateMutability": {
+          "$ref": "#/definitions/StateMutability"
+        },
+        "nodeType": {
+          "enum": [
+            "ElementaryTypeName"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "typeDescriptions",
+        "name",
+        "nodeType"
+      ]
+    },
+    "ElementaryTypeNameExpression": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "argumentTypes": {
+          "anyOf": [
+            {
+              "type": "array",
+              "items": {
+                "$ref": "#/definitions/TypeDescriptions"
+              }
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "isConstant": {
+          "type": "boolean"
+        },
+        "isLValue": {
+          "type": "boolean"
+        },
+        "isPure": {
+          "type": "boolean"
+        },
+        "lValueRequested": {
+          "type": "boolean"
+        },
+        "typeDescriptions": {
+          "$ref": "#/definitions/TypeDescriptions"
+        },
+        "typeName": {
+          "$ref": "#/definitions/ElementaryTypeName"
+        },
+        "nodeType": {
+          "enum": [
+            "ElementaryTypeNameExpression"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "isConstant",
+        "isLValue",
+        "isPure",
+        "lValueRequested",
+        "typeDescriptions",
+        "typeName",
+        "nodeType"
+      ]
+    },
+    "EmitStatement": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "documentation": {
+          "type": "string"
+        },
+        "eventCall": {
+          "$ref": "#/definitions/FunctionCall"
+        },
+        "nodeType": {
+          "enum": [
+            "EmitStatement"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "eventCall",
+        "nodeType"
+      ]
+    },
+    "EnumDefinition": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "name": {
+          "type": "string"
+        },
+        "nameLocation": {
+          "type": "string"
+        },
+        "canonicalName": {
+          "type": "string"
+        },
+        "members": {
+          "type": "array",
+          "items": {
+            "$ref": "#/definitions/EnumValue"
+          }
+        },
+        "documentation": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/StructuredDocumentation"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "nodeType": {
+          "enum": [
+            "EnumDefinition"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "name",
+        "canonicalName",
+        "members",
+        "nodeType"
+      ]
+    },
+    "EnumValue": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "name": {
+          "type": "string"
+        },
+        "nameLocation": {
+          "type": "string"
+        },
+        "documentation": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/StructuredDocumentation"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "nodeType": {
+          "enum": [
+            "EnumValue"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "name",
+        "nodeType"
+      ]
+    },
+    "ErrorDefinition": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "name": {
+          "type": "string"
+        },
+        "nameLocation": {
+          "type": "string"
+        },
+        "documentation": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/StructuredDocumentation"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "errorSelector": {
+          "type": "string"
+        },
+        "parameters": {
+          "$ref": "#/definitions/ParameterList"
+        },
+        "nodeType": {
+          "enum": [
+            "ErrorDefinition"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "name",
+        "nameLocation",
+        "parameters",
+        "nodeType"
+      ]
+    },
+    "EventDefinition": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "name": {
+          "type": "string"
+        },
+        "nameLocation": {
+          "type": "string"
+        },
+        "anonymous": {
+          "type": "boolean"
+        },
+        "eventSelector": {
+          "type": "string"
+        },
+        "documentation": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/StructuredDocumentation"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "parameters": {
+          "$ref": "#/definitions/ParameterList"
+        },
+        "nodeType": {
+          "enum": [
+            "EventDefinition"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "name",
+        "anonymous",
+        "parameters",
+        "nodeType"
+      ]
+    },
+    "ExpressionStatement": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "documentation": {
+          "type": "string"
+        },
+        "expression": {
+          "$ref": "#/definitions/Expression"
+        },
+        "nodeType": {
+          "enum": [
+            "ExpressionStatement"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "expression",
+        "nodeType"
+      ]
+    },
+    "ForStatement": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "documentation": {
+          "type": "string"
+        },
+        "body": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/Block"
+            },
+            {
+              "$ref": "#/definitions/Statement"
+            }
+          ]
+        },
+        "condition": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/Expression"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "initializationExpression": {
+          "anyOf": [
+            {
+              "anyOf": [
+                {
+                  "$ref": "#/definitions/ExpressionStatement"
+                },
+                {
+                  "$ref": "#/definitions/VariableDeclarationStatement"
+                }
+              ]
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "loopExpression": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/ExpressionStatement"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "isSimpleCounterLoop": {
+          "type": "boolean"
+        },
+        "nodeType": {
+          "enum": [
+            "ForStatement"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "body",
+        "nodeType"
+      ]
+    },
+    "FunctionCall": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "argumentTypes": {
+          "anyOf": [
+            {
+              "type": "array",
+              "items": {
+                "$ref": "#/definitions/TypeDescriptions"
+              }
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "isConstant": {
+          "type": "boolean"
+        },
+        "isLValue": {
+          "type": "boolean"
+        },
+        "isPure": {
+          "type": "boolean"
+        },
+        "lValueRequested": {
+          "type": "boolean"
+        },
+        "typeDescriptions": {
+          "$ref": "#/definitions/TypeDescriptions"
+        },
+        "arguments": {
+          "type": "array",
+          "items": {
+            "$ref": "#/definitions/Expression"
+          }
+        },
+        "expression": {
+          "$ref": "#/definitions/Expression"
+        },
+        "kind": {
+          "enum": [
+            "functionCall",
+            "typeConversion",
+            "structConstructorCall"
+          ]
+        },
+        "names": {
+          "type": "array",
+          "items": {
+            "type": "string"
+          }
+        },
+        "nameLocations": {
+          "type": "array",
+          "items": {
+            "type": "string"
+          }
+        },
+        "tryCall": {
+          "type": "boolean"
+        },
+        "nodeType": {
+          "enum": [
+            "FunctionCall"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "isConstant",
+        "isLValue",
+        "isPure",
+        "lValueRequested",
+        "typeDescriptions",
+        "arguments",
+        "expression",
+        "kind",
+        "names",
+        "tryCall",
+        "nodeType"
+      ]
+    },
+    "FunctionCallOptions": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "argumentTypes": {
+          "anyOf": [
+            {
+              "type": "array",
+              "items": {
+                "$ref": "#/definitions/TypeDescriptions"
+              }
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "isConstant": {
+          "type": "boolean"
+        },
+        "isLValue": {
+          "type": "boolean"
+        },
+        "isPure": {
+          "type": "boolean"
+        },
+        "lValueRequested": {
+          "type": "boolean"
+        },
+        "typeDescriptions": {
+          "$ref": "#/definitions/TypeDescriptions"
+        },
+        "expression": {
+          "$ref": "#/definitions/Expression"
+        },
+        "names": {
+          "type": "array",
+          "items": {
+            "type": "string"
+          }
+        },
+        "options": {
+          "type": "array",
+          "items": {
+            "$ref": "#/definitions/Expression"
+          }
+        },
+        "nodeType": {
+          "enum": [
+            "FunctionCallOptions"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "isConstant",
+        "isPure",
+        "lValueRequested",
+        "typeDescriptions",
+        "expression",
+        "names",
+        "options",
+        "nodeType"
+      ]
+    },
+    "FunctionDefinition": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "name": {
+          "type": "string"
+        },
+        "nameLocation": {
+          "type": "string"
+        },
+        "baseFunctions": {
+          "type": "array",
+          "items": {
+            "type": "integer"
+          }
+        },
+        "body": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/Block"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "documentation": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/StructuredDocumentation"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "functionSelector": {
+          "type": "string"
+        },
+        "implemented": {
+          "type": "boolean"
+        },
+        "kind": {
+          "enum": [
+            "function",
+            "receive",
+            "constructor",
+            "fallback",
+            "freeFunction"
+          ]
+        },
+        "modifiers": {
+          "type": "array",
+          "items": {
+            "$ref": "#/definitions/ModifierInvocation"
+          }
+        },
+        "overrides": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/OverrideSpecifier"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "parameters": {
+          "$ref": "#/definitions/ParameterList"
+        },
+        "returnParameters": {
+          "$ref": "#/definitions/ParameterList"
+        },
+        "scope": {
+          "type": "integer"
+        },
+        "stateMutability": {
+          "$ref": "#/definitions/StateMutability"
+        },
+        "virtual": {
+          "type": "boolean"
+        },
+        "visibility": {
+          "$ref": "#/definitions/Visibility"
+        },
+        "nodeType": {
+          "enum": [
+            "FunctionDefinition"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "name",
+        "implemented",
+        "kind",
+        "modifiers",
+        "parameters",
+        "returnParameters",
+        "scope",
+        "stateMutability",
+        "virtual",
+        "visibility",
+        "nodeType"
+      ]
+    },
+    "FunctionTypeName": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "typeDescriptions": {
+          "$ref": "#/definitions/TypeDescriptions"
+        },
+        "parameterTypes": {
+          "$ref": "#/definitions/ParameterList"
+        },
+        "returnParameterTypes": {
+          "$ref": "#/definitions/ParameterList"
+        },
+        "stateMutability": {
+          "$ref": "#/definitions/StateMutability"
+        },
+        "visibility": {
+          "$ref": "#/definitions/Visibility"
+        },
+        "nodeType": {
+          "enum": [
+            "FunctionTypeName"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "typeDescriptions",
+        "parameterTypes",
+        "returnParameterTypes",
+        "stateMutability",
+        "visibility",
+        "nodeType"
+      ]
+    },
+    "Identifier": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "argumentTypes": {
+          "anyOf": [
+            {
+              "type": "array",
+              "items": {
+                "$ref": "#/definitions/TypeDescriptions"
+              }
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "name": {
+          "type": "string"
+        },
+        "overloadedDeclarations": {
+          "type": "array",
+          "items": {
+            "type": "integer"
+          }
+        },
+        "referencedDeclaration": {
+          "anyOf": [
+            {
+              "type": "integer"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "typeDescriptions": {
+          "$ref": "#/definitions/TypeDescriptions"
+        },
+        "nodeType": {
+          "enum": [
+            "Identifier"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "name",
+        "overloadedDeclarations",
+        "typeDescriptions",
+        "nodeType"
+      ]
+    },
+    "IdentifierPath": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "name": {
+          "type": "string"
+        },
+        "nameLocations": {
+          "type": "array",
+          "items": {
+            "type": "string"
+          }
+        },
+        "referencedDeclaration": {
+          "type": "integer"
+        },
+        "nodeType": {
+          "enum": [
+            "IdentifierPath"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "name",
+        "referencedDeclaration",
+        "nodeType"
+      ]
+    },
+    "IfStatement": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "documentation": {
+          "type": "string"
+        },
+        "condition": {
+          "$ref": "#/definitions/Expression"
+        },
+        "falseBody": {
+          "anyOf": [
+            {
+              "anyOf": [
+                {
+                  "$ref": "#/definitions/Statement"
+                },
+                {
+                  "$ref": "#/definitions/Block"
+                }
+              ]
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "trueBody": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/Statement"
+            },
+            {
+              "$ref": "#/definitions/Block"
+            }
+          ]
+        },
+        "nodeType": {
+          "enum": [
+            "IfStatement"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "condition",
+        "trueBody",
+        "nodeType"
+      ]
+    },
+    "ImportDirective": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "absolutePath": {
+          "type": "string"
+        },
+        "file": {
+          "type": "string"
+        },
+        "nameLocation": {
+          "type": "string"
+        },
+        "scope": {
+          "type": "integer"
+        },
+        "sourceUnit": {
+          "type": "integer"
+        },
+        "symbolAliases": {
+          "type": "array",
+          "items": {
+            "type": "object",
+            "additionalProperties": false,
+            "properties": {
+              "foreign": {
+                "$ref": "#/definitions/Identifier"
+              },
+              "local": {
+                "anyOf": [
+                  {
+                    "type": "string"
+                  },
+                  {
+                    "type": "null"
+                  }
+                ]
+              },
+              "nameLocation": {
+                "type": "string"
+              }
+            },
+            "required": [
+              "foreign"
+            ]
+          }
+        },
+        "unitAlias": {
+          "type": "string"
+        },
+        "nodeType": {
+          "enum": [
+            "ImportDirective"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "absolutePath",
+        "file",
+        "scope",
+        "sourceUnit",
+        "symbolAliases",
+        "unitAlias",
+        "nodeType"
+      ]
+    },
+    "IndexAccess": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "argumentTypes": {
+          "anyOf": [
+            {
+              "type": "array",
+              "items": {
+                "$ref": "#/definitions/TypeDescriptions"
+              }
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "isConstant": {
+          "type": "boolean"
+        },
+        "isLValue": {
+          "type": "boolean"
+        },
+        "isPure": {
+          "type": "boolean"
+        },
+        "lValueRequested": {
+          "type": "boolean"
+        },
+        "typeDescriptions": {
+          "$ref": "#/definitions/TypeDescriptions"
+        },
+        "baseExpression": {
+          "$ref": "#/definitions/Expression"
+        },
+        "indexExpression": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/Expression"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "nodeType": {
+          "enum": [
+            "IndexAccess"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "isConstant",
+        "isLValue",
+        "isPure",
+        "lValueRequested",
+        "typeDescriptions",
+        "baseExpression",
+        "nodeType"
+      ]
+    },
+    "IndexRangeAccess": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "argumentTypes": {
+          "anyOf": [
+            {
+              "type": "array",
+              "items": {
+                "$ref": "#/definitions/TypeDescriptions"
+              }
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "isConstant": {
+          "type": "boolean"
+        },
+        "isLValue": {
+          "type": "boolean"
+        },
+        "isPure": {
+          "type": "boolean"
+        },
+        "lValueRequested": {
+          "type": "boolean"
+        },
+        "typeDescriptions": {
+          "$ref": "#/definitions/TypeDescriptions"
+        },
+        "baseExpression": {
+          "$ref": "#/definitions/Expression"
+        },
+        "endExpression": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/Expression"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "startExpression": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/Expression"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "nodeType": {
+          "enum": [
+            "IndexRangeAccess"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "isConstant",
+        "isLValue",
+        "isPure",
+        "lValueRequested",
+        "typeDescriptions",
+        "baseExpression",
+        "nodeType"
+      ]
+    },
+    "InheritanceSpecifier": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "arguments": {
+          "anyOf": [
+            {
+              "type": "array",
+              "items": {
+                "$ref": "#/definitions/Expression"
+              }
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "baseName": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/UserDefinedTypeName"
+            },
+            {
+              "$ref": "#/definitions/IdentifierPath"
+            }
+          ]
+        },
+        "nodeType": {
+          "enum": [
+            "InheritanceSpecifier"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "baseName",
+        "nodeType"
+      ]
+    },
+    "InlineAssembly": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "documentation": {
+          "type": "string"
+        },
+        "AST": {
+          "$ref": "#/definitions/YulBlock"
+        },
+        "evmVersion": {
+          "enum": [
+            "homestead",
+            "tangerineWhistle",
+            "spuriousDragon",
+            "byzantium",
+            "constantinople",
+            "petersburg",
+            "istanbul",
+            "berlin",
+            "london",
+            "paris",
+            "shanghai",
+            "cancun",
+            "prague",
+            "osaka"
+          ]
+        },
+        "externalReferences": {
+          "type": "array",
+          "items": {
+            "type": "object",
+            "additionalProperties": false,
+            "properties": {
+              "declaration": {
+                "type": "integer"
+              },
+              "isOffset": {
+                "type": "boolean"
+              },
+              "isSlot": {
+                "type": "boolean"
+              },
+              "src": {
+                "$ref": "#/definitions/SourceLocation"
+              },
+              "valueSize": {
+                "type": "integer"
+              },
+              "suffix": {
+                "enum": [
+                  "slot",
+                  "offset",
+                  "length"
+                ]
+              }
+            },
+            "required": [
+              "declaration",
+              "isOffset",
+              "isSlot",
+              "src",
+              "valueSize"
+            ]
+          }
+        },
+        "flags": {
+          "type": "array",
+          "items": {
+            "enum": [
+              "memory-safe"
+            ]
+          }
+        },
+        "nodeType": {
+          "enum": [
+            "InlineAssembly"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "AST",
+        "evmVersion",
+        "externalReferences",
+        "nodeType"
+      ]
+    },
+    "Literal": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "argumentTypes": {
+          "anyOf": [
+            {
+              "type": "array",
+              "items": {
+                "$ref": "#/definitions/TypeDescriptions"
+              }
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "isConstant": {
+          "type": "boolean"
+        },
+        "isLValue": {
+          "type": "boolean"
+        },
+        "isPure": {
+          "type": "boolean"
+        },
+        "lValueRequested": {
+          "type": "boolean"
+        },
+        "typeDescriptions": {
+          "$ref": "#/definitions/TypeDescriptions"
+        },
+        "hexValue": {
+          "type": "string",
+          "pattern": "^[0-9a-f]*$"
+        },
+        "kind": {
+          "enum": [
+            "bool",
+            "number",
+            "string",
+            "hexString",
+            "unicodeString"
+          ]
+        },
+        "subdenomination": {
+          "anyOf": [
+            {
+              "enum": [
+                "seconds",
+                "minutes",
+                "hours",
+                "days",
+                "weeks",
+                "wei",
+                "gwei",
+                "ether",
+                "finney",
+                "szabo"
+              ]
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "value": {
+          "anyOf": [
+            {
+              "type": "string"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "nodeType": {
+          "enum": [
+            "Literal"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "isConstant",
+        "isLValue",
+        "isPure",
+        "lValueRequested",
+        "typeDescriptions",
+        "hexValue",
+        "kind",
+        "nodeType"
+      ]
+    },
+    "Mapping": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "typeDescriptions": {
+          "$ref": "#/definitions/TypeDescriptions"
+        },
+        "keyType": {
+          "$ref": "#/definitions/TypeName"
+        },
+        "valueType": {
+          "$ref": "#/definitions/TypeName"
+        },
+        "keyName": {
+          "type": "string"
+        },
+        "keyNameLocation": {
+          "type": "string"
+        },
+        "valueName": {
+          "type": "string"
+        },
+        "valueNameLocation": {
+          "type": "string"
+        },
+        "nodeType": {
+          "enum": [
+            "Mapping"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "typeDescriptions",
+        "keyType",
+        "valueType",
+        "nodeType"
+      ]
+    },
+    "MemberAccess": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "argumentTypes": {
+          "anyOf": [
+            {
+              "type": "array",
+              "items": {
+                "$ref": "#/definitions/TypeDescriptions"
+              }
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "isConstant": {
+          "type": "boolean"
+        },
+        "isLValue": {
+          "type": "boolean"
+        },
+        "isPure": {
+          "type": "boolean"
+        },
+        "lValueRequested": {
+          "type": "boolean"
+        },
+        "typeDescriptions": {
+          "$ref": "#/definitions/TypeDescriptions"
+        },
+        "expression": {
+          "$ref": "#/definitions/Expression"
+        },
+        "memberName": {
+          "type": "string"
+        },
+        "memberLocation": {
+          "type": "string"
+        },
+        "referencedDeclaration": {
+          "anyOf": [
+            {
+              "type": "integer"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "nodeType": {
+          "enum": [
+            "MemberAccess"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "isConstant",
+        "isLValue",
+        "isPure",
+        "lValueRequested",
+        "typeDescriptions",
+        "expression",
+        "memberName",
+        "nodeType"
+      ]
+    },
+    "ModifierDefinition": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "name": {
+          "type": "string"
+        },
+        "nameLocation": {
+          "type": "string"
+        },
+        "baseModifiers": {
+          "anyOf": [
+            {
+              "type": "array",
+              "items": {
+                "type": "integer"
+              }
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "body": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/Block"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "documentation": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/StructuredDocumentation"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "overrides": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/OverrideSpecifier"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "parameters": {
+          "$ref": "#/definitions/ParameterList"
+        },
+        "virtual": {
+          "type": "boolean"
+        },
+        "visibility": {
+          "$ref": "#/definitions/Visibility"
+        },
+        "nodeType": {
+          "enum": [
+            "ModifierDefinition"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "name",
+        "parameters",
+        "virtual",
+        "visibility",
+        "nodeType"
+      ]
+    },
+    "ModifierInvocation": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "arguments": {
+          "anyOf": [
+            {
+              "type": "array",
+              "items": {
+                "$ref": "#/definitions/Expression"
+              }
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "kind": {
+          "enum": [
+            "modifierInvocation",
+            "baseConstructorSpecifier"
+          ]
+        },
+        "modifierName": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/Identifier"
+            },
+            {
+              "$ref": "#/definitions/IdentifierPath"
+            }
+          ]
+        },
+        "nodeType": {
+          "enum": [
+            "ModifierInvocation"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "modifierName",
+        "nodeType"
+      ]
+    },
+    "NewExpression": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "argumentTypes": {
+          "anyOf": [
+            {
+              "type": "array",
+              "items": {
+                "$ref": "#/definitions/TypeDescriptions"
+              }
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "isConstant": {
+          "type": "boolean"
+        },
+        "isLValue": {
+          "type": "boolean"
+        },
+        "isPure": {
+          "type": "boolean"
+        },
+        "lValueRequested": {
+          "type": "boolean"
+        },
+        "typeDescriptions": {
+          "$ref": "#/definitions/TypeDescriptions"
+        },
+        "typeName": {
+          "$ref": "#/definitions/TypeName"
+        },
+        "nodeType": {
+          "enum": [
+            "NewExpression"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "isConstant",
+        "isPure",
+        "lValueRequested",
+        "typeDescriptions",
+        "typeName",
+        "nodeType"
+      ]
+    },
+    "OverrideSpecifier": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "overrides": {
+          "anyOf": [
+            {
+              "type": "array",
+              "items": {
+                "$ref": "#/definitions/UserDefinedTypeName"
+              }
+            },
+            {
+              "type": "array",
+              "items": {
+                "$ref": "#/definitions/IdentifierPath"
+              }
+            }
+          ]
+        },
+        "nodeType": {
+          "enum": [
+            "OverrideSpecifier"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "overrides",
+        "nodeType"
+      ]
+    },
+    "ParameterList": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "parameters": {
+          "type": "array",
+          "items": {
+            "$ref": "#/definitions/VariableDeclaration"
+          }
+        },
+        "nodeType": {
+          "enum": [
+            "ParameterList"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "parameters",
+        "nodeType"
+      ]
+    },
+    "PlaceholderStatement": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "documentation": {
+          "type": "string"
+        },
+        "nodeType": {
+          "enum": [
+            "PlaceholderStatement"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "nodeType"
+      ]
+    },
+    "PragmaDirective": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "literals": {
+          "type": "array",
+          "items": {
+            "type": "string"
+          }
+        },
+        "nodeType": {
+          "enum": [
+            "PragmaDirective"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "literals",
+        "nodeType"
+      ]
+    },
+    "Return": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "documentation": {
+          "type": "string"
+        },
+        "expression": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/Expression"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "functionReturnParameters": {
+          "type": "integer"
+        },
+        "nodeType": {
+          "enum": [
+            "Return"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "functionReturnParameters",
+        "nodeType"
+      ]
+    },
+    "RevertStatement": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "documentation": {
+          "type": "string"
+        },
+        "errorCall": {
+          "$ref": "#/definitions/FunctionCall"
+        },
+        "nodeType": {
+          "enum": [
+            "RevertStatement"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "errorCall",
+        "nodeType"
+      ]
+    },
+    "StructDefinition": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "name": {
+          "type": "string"
+        },
+        "nameLocation": {
+          "type": "string"
+        },
+        "canonicalName": {
+          "type": "string"
+        },
+        "members": {
+          "type": "array",
+          "items": {
+            "$ref": "#/definitions/VariableDeclaration"
+          }
+        },
+        "scope": {
+          "type": "integer"
+        },
+        "visibility": {
+          "$ref": "#/definitions/Visibility"
+        },
+        "documentation": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/StructuredDocumentation"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "nodeType": {
+          "enum": [
+            "StructDefinition"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "name",
+        "canonicalName",
+        "members",
+        "scope",
+        "visibility",
+        "nodeType"
+      ]
+    },
+    "StructuredDocumentation": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "text": {
+          "type": "string"
+        },
+        "nodeType": {
+          "enum": [
+            "StructuredDocumentation"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "text",
+        "nodeType"
+      ]
+    },
+    "TryCatchClause": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "block": {
+          "$ref": "#/definitions/Block"
+        },
+        "errorName": {
+          "type": "string"
+        },
+        "parameters": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/ParameterList"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "nodeType": {
+          "enum": [
+            "TryCatchClause"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "block",
+        "errorName",
+        "nodeType"
+      ]
+    },
+    "TryStatement": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "documentation": {
+          "type": "string"
+        },
+        "clauses": {
+          "type": "array",
+          "items": {
+            "$ref": "#/definitions/TryCatchClause"
+          }
+        },
+        "externalCall": {
+          "$ref": "#/definitions/FunctionCall"
+        },
+        "nodeType": {
+          "enum": [
+            "TryStatement"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "clauses",
+        "externalCall",
+        "nodeType"
+      ]
+    },
+    "TupleExpression": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "argumentTypes": {
+          "anyOf": [
+            {
+              "type": "array",
+              "items": {
+                "$ref": "#/definitions/TypeDescriptions"
+              }
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "isConstant": {
+          "type": "boolean"
+        },
+        "isLValue": {
+          "type": "boolean"
+        },
+        "isPure": {
+          "type": "boolean"
+        },
+        "lValueRequested": {
+          "type": "boolean"
+        },
+        "typeDescriptions": {
+          "$ref": "#/definitions/TypeDescriptions"
+        },
+        "components": {
+          "type": "array",
+          "items": {
+            "anyOf": [
+              {
+                "$ref": "#/definitions/Expression"
+              },
+              {
+                "type": "null"
+              }
+            ]
+          }
+        },
+        "isInlineArray": {
+          "type": "boolean"
+        },
+        "nodeType": {
+          "enum": [
+            "TupleExpression"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "isConstant",
+        "isLValue",
+        "isPure",
+        "lValueRequested",
+        "typeDescriptions",
+        "components",
+        "isInlineArray",
+        "nodeType"
+      ]
+    },
+    "UnaryOperation": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "argumentTypes": {
+          "anyOf": [
+            {
+              "type": "array",
+              "items": {
+                "$ref": "#/definitions/TypeDescriptions"
+              }
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "isConstant": {
+          "type": "boolean"
+        },
+        "isLValue": {
+          "type": "boolean"
+        },
+        "isPure": {
+          "type": "boolean"
+        },
+        "lValueRequested": {
+          "type": "boolean"
+        },
+        "typeDescriptions": {
+          "$ref": "#/definitions/TypeDescriptions"
+        },
+        "operator": {
+          "enum": [
+            "++",
+            "--",
+            "-",
+            "!",
+            "delete",
+            "~"
+          ]
+        },
+        "prefix": {
+          "type": "boolean"
+        },
+        "subExpression": {
+          "$ref": "#/definitions/Expression"
+        },
+        "function": {
+          "type": "integer"
+        },
+        "nodeType": {
+          "enum": [
+            "UnaryOperation"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "isConstant",
+        "isLValue",
+        "isPure",
+        "lValueRequested",
+        "typeDescriptions",
+        "operator",
+        "prefix",
+        "subExpression",
+        "nodeType"
+      ]
+    },
+    "UncheckedBlock": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "documentation": {
+          "type": "string"
+        },
+        "statements": {
+          "type": "array",
+          "items": {
+            "$ref": "#/definitions/Statement"
+          }
+        },
+        "nodeType": {
+          "enum": [
+            "UncheckedBlock"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "statements",
+        "nodeType"
+      ]
+    },
+    "UserDefinedTypeName": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "typeDescriptions": {
+          "$ref": "#/definitions/TypeDescriptions"
+        },
+        "contractScope": {
+          "type": "null"
+        },
+        "name": {
+          "type": "string"
+        },
+        "pathNode": {
+          "$ref": "#/definitions/IdentifierPath"
+        },
+        "referencedDeclaration": {
+          "type": "integer"
+        },
+        "nodeType": {
+          "enum": [
+            "UserDefinedTypeName"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "typeDescriptions",
+        "referencedDeclaration",
+        "nodeType"
+      ]
+    },
+    "UserDefinedValueTypeDefinition": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "name": {
+          "type": "string"
+        },
+        "nameLocation": {
+          "type": "string"
+        },
+        "canonicalName": {
+          "type": "string"
+        },
+        "underlyingType": {
+          "$ref": "#/definitions/TypeName"
+        },
+        "nodeType": {
+          "enum": [
+            "UserDefinedValueTypeDefinition"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "name",
+        "underlyingType",
+        "nodeType"
+      ]
+    },
+    "UsingForDirective": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "functionList": {
+          "type": "array",
+          "items": {
+            "anyOf": [
+              {
+                "type": "object",
+                "additionalProperties": false,
+                "properties": {
+                  "function": {
+                    "$ref": "#/definitions/IdentifierPath"
+                  }
+                },
+                "required": [
+                  "function"
+                ]
+              },
+              {
+                "type": "object",
+                "additionalProperties": false,
+                "properties": {
+                  "operator": {
+                    "enum": [
+                      "&",
+                      "|",
+                      "^",
+                      "~",
+                      "+",
+                      "-",
+                      "*",
+                      "/",
+                      "%",
+                      "==",
+                      "!=",
+                      "<",
+                      "<=",
+                      ">",
+                      ">="
+                    ]
+                  },
+                  "definition": {
+                    "$ref": "#/definitions/IdentifierPath"
+                  }
+                },
+                "required": [
+                  "operator",
+                  "definition"
+                ]
+              }
+            ]
+          }
+        },
+        "global": {
+          "type": "boolean"
+        },
+        "libraryName": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/UserDefinedTypeName"
+            },
+            {
+              "$ref": "#/definitions/IdentifierPath"
+            }
+          ]
+        },
+        "typeName": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/TypeName"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "nodeType": {
+          "enum": [
+            "UsingForDirective"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "nodeType"
+      ]
+    },
+    "VariableDeclaration": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "name": {
+          "type": "string"
+        },
+        "nameLocation": {
+          "type": "string"
+        },
+        "baseFunctions": {
+          "anyOf": [
+            {
+              "type": "array",
+              "items": {
+                "type": "integer"
+              }
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "constant": {
+          "type": "boolean"
+        },
+        "documentation": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/StructuredDocumentation"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "functionSelector": {
+          "type": "string"
+        },
+        "indexed": {
+          "type": "boolean"
+        },
+        "mutability": {
+          "$ref": "#/definitions/Mutability"
+        },
+        "overrides": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/OverrideSpecifier"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "scope": {
+          "type": "integer"
+        },
+        "stateVariable": {
+          "type": "boolean"
+        },
+        "storageLocation": {
+          "$ref": "#/definitions/StorageLocation"
+        },
+        "typeDescriptions": {
+          "$ref": "#/definitions/TypeDescriptions"
+        },
+        "typeName": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/TypeName"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "value": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/Expression"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "visibility": {
+          "$ref": "#/definitions/Visibility"
+        },
+        "nodeType": {
+          "enum": [
+            "VariableDeclaration"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "name",
+        "constant",
+        "mutability",
+        "scope",
+        "stateVariable",
+        "storageLocation",
+        "typeDescriptions",
+        "visibility",
+        "nodeType"
+      ]
+    },
+    "VariableDeclarationStatement": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "documentation": {
+          "type": "string"
+        },
+        "assignments": {
+          "type": "array",
+          "items": {
+            "anyOf": [
+              {
+                "type": "integer"
+              },
+              {
+                "type": "null"
+              }
+            ]
+          }
+        },
+        "declarations": {
+          "type": "array",
+          "items": {
+            "anyOf": [
+              {
+                "$ref": "#/definitions/VariableDeclaration"
+              },
+              {
+                "type": "null"
+              }
+            ]
+          }
+        },
+        "initialValue": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/Expression"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "nodeType": {
+          "enum": [
+            "VariableDeclarationStatement"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "assignments",
+        "declarations",
+        "nodeType"
+      ]
+    },
+    "WhileStatement": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "id": {
+          "type": "integer"
+        },
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "documentation": {
+          "type": "string"
+        },
+        "body": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/Block"
+            },
+            {
+              "$ref": "#/definitions/Statement"
+            }
+          ]
+        },
+        "condition": {
+          "$ref": "#/definitions/Expression"
+        },
+        "nodeType": {
+          "enum": [
+            "WhileStatement"
+          ]
+        }
+      },
+      "required": [
+        "id",
+        "src",
+        "body",
+        "condition",
+        "nodeType"
+      ]
+    },
+    "YulStatement": {
+      "anyOf": [
+        {
+          "$ref": "#/definitions/YulAssignment"
+        },
+        {
+          "$ref": "#/definitions/YulBlock"
+        },
+        {
+          "$ref": "#/definitions/YulBreak"
+        },
+        {
+          "$ref": "#/definitions/YulContinue"
+        },
+        {
+          "$ref": "#/definitions/YulExpressionStatement"
+        },
+        {
+          "$ref": "#/definitions/YulLeave"
+        },
+        {
+          "$ref": "#/definitions/YulForLoop"
+        },
+        {
+          "$ref": "#/definitions/YulFunctionDefinition"
+        },
+        {
+          "$ref": "#/definitions/YulIf"
+        },
+        {
+          "$ref": "#/definitions/YulSwitch"
+        },
+        {
+          "$ref": "#/definitions/YulVariableDeclaration"
+        }
+      ]
+    },
+    "YulExpression": {
+      "anyOf": [
+        {
+          "$ref": "#/definitions/YulFunctionCall"
+        },
+        {
+          "$ref": "#/definitions/YulIdentifier"
+        },
+        {
+          "$ref": "#/definitions/YulLiteral"
+        }
+      ]
+    },
+    "YulLiteral": {
+      "anyOf": [
+        {
+          "$ref": "#/definitions/YulLiteralValue"
+        },
+        {
+          "$ref": "#/definitions/YulLiteralHexValue"
+        }
+      ]
+    },
+    "YulLiteralValue": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "value": {
+          "type": "string"
+        },
+        "kind": {
+          "enum": [
+            "number",
+            "string",
+            "bool"
+          ]
+        },
+        "type": {
+          "type": "string"
+        },
+        "nodeType": {
+          "enum": [
+            "YulLiteral"
+          ]
+        },
+        "nativeSrc": {
+          "$ref": "#/definitions/SourceLocation"
+        }
+      },
+      "required": [
+        "src",
+        "value",
+        "kind",
+        "type",
+        "nodeType"
+      ]
+    },
+    "YulLiteralHexValue": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "hexValue": {
+          "type": "string"
+        },
+        "kind": {
+          "enum": [
+            "number",
+            "string",
+            "bool"
+          ]
+        },
+        "type": {
+          "type": "string"
+        },
+        "value": {
+          "type": "string"
+        },
+        "nodeType": {
+          "enum": [
+            "YulLiteral"
+          ]
+        },
+        "nativeSrc": {
+          "$ref": "#/definitions/SourceLocation"
+        }
+      },
+      "required": [
+        "src",
+        "hexValue",
+        "kind",
+        "type",
+        "nodeType"
+      ]
+    },
+    "YulAssignment": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "value": {
+          "$ref": "#/definitions/YulExpression"
+        },
+        "variableNames": {
+          "type": "array",
+          "items": {
+            "$ref": "#/definitions/YulIdentifier"
+          }
+        },
+        "nodeType": {
+          "enum": [
+            "YulAssignment"
+          ]
+        },
+        "nativeSrc": {
+          "$ref": "#/definitions/SourceLocation"
+        }
+      },
+      "required": [
+        "src",
+        "value",
+        "variableNames",
+        "nodeType"
+      ]
+    },
+    "YulBlock": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "statements": {
+          "type": "array",
+          "items": {
+            "$ref": "#/definitions/YulStatement"
+          }
+        },
+        "nodeType": {
+          "enum": [
+            "YulBlock"
+          ]
+        },
+        "nativeSrc": {
+          "$ref": "#/definitions/SourceLocation"
+        }
+      },
+      "required": [
+        "src",
+        "statements",
+        "nodeType"
+      ]
+    },
+    "YulBreak": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "nodeType": {
+          "enum": [
+            "YulBreak"
+          ]
+        },
+        "nativeSrc": {
+          "$ref": "#/definitions/SourceLocation"
+        }
+      },
+      "required": [
+        "src",
+        "nodeType"
+      ]
+    },
+    "YulCase": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "body": {
+          "$ref": "#/definitions/YulBlock"
+        },
+        "value": {
+          "anyOf": [
+            {
+              "enum": [
+                "default"
+              ]
+            },
+            {
+              "$ref": "#/definitions/YulLiteral"
+            }
+          ]
+        },
+        "nodeType": {
+          "enum": [
+            "YulCase"
+          ]
+        },
+        "nativeSrc": {
+          "$ref": "#/definitions/SourceLocation"
+        }
+      },
+      "required": [
+        "src",
+        "body",
+        "value",
+        "nodeType"
+      ]
+    },
+    "YulContinue": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "nodeType": {
+          "enum": [
+            "YulContinue"
+          ]
+        },
+        "nativeSrc": {
+          "$ref": "#/definitions/SourceLocation"
+        }
+      },
+      "required": [
+        "src",
+        "nodeType"
+      ]
+    },
+    "YulExpressionStatement": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "expression": {
+          "$ref": "#/definitions/YulExpression"
+        },
+        "nodeType": {
+          "enum": [
+            "YulExpressionStatement"
+          ]
+        },
+        "nativeSrc": {
+          "$ref": "#/definitions/SourceLocation"
+        }
+      },
+      "required": [
+        "src",
+        "expression",
+        "nodeType"
+      ]
+    },
+    "YulFunctionCall": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "arguments": {
+          "type": "array",
+          "items": {
+            "$ref": "#/definitions/YulExpression"
+          }
+        },
+        "functionName": {
+          "$ref": "#/definitions/YulIdentifier"
+        },
+        "nodeType": {
+          "enum": [
+            "YulFunctionCall"
+          ]
+        },
+        "nativeSrc": {
+          "$ref": "#/definitions/SourceLocation"
+        }
+      },
+      "required": [
+        "src",
+        "arguments",
+        "functionName",
+        "nodeType"
+      ]
+    },
+    "YulForLoop": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "body": {
+          "$ref": "#/definitions/YulBlock"
+        },
+        "condition": {
+          "$ref": "#/definitions/YulExpression"
+        },
+        "post": {
+          "$ref": "#/definitions/YulBlock"
+        },
+        "pre": {
+          "$ref": "#/definitions/YulBlock"
+        },
+        "nodeType": {
+          "enum": [
+            "YulForLoop"
+          ]
+        },
+        "nativeSrc": {
+          "$ref": "#/definitions/SourceLocation"
+        }
+      },
+      "required": [
+        "src",
+        "body",
+        "condition",
+        "post",
+        "pre",
+        "nodeType"
+      ]
+    },
+    "YulFunctionDefinition": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "body": {
+          "$ref": "#/definitions/YulBlock"
+        },
+        "name": {
+          "type": "string"
+        },
+        "parameters": {
+          "type": "array",
+          "items": {
+            "$ref": "#/definitions/YulTypedName"
+          }
+        },
+        "returnVariables": {
+          "type": "array",
+          "items": {
+            "$ref": "#/definitions/YulTypedName"
+          }
+        },
+        "nodeType": {
+          "enum": [
+            "YulFunctionDefinition"
+          ]
+        },
+        "nativeSrc": {
+          "$ref": "#/definitions/SourceLocation"
+        }
+      },
+      "required": [
+        "src",
+        "body",
+        "name",
+        "nodeType"
+      ]
+    },
+    "YulIdentifier": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "name": {
+          "type": "string"
+        },
+        "nodeType": {
+          "enum": [
+            "YulIdentifier"
+          ]
+        },
+        "nativeSrc": {
+          "$ref": "#/definitions/SourceLocation"
+        }
+      },
+      "required": [
+        "src",
+        "name",
+        "nodeType"
+      ]
+    },
+    "YulIf": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "body": {
+          "$ref": "#/definitions/YulBlock"
+        },
+        "condition": {
+          "$ref": "#/definitions/YulExpression"
+        },
+        "nodeType": {
+          "enum": [
+            "YulIf"
+          ]
+        },
+        "nativeSrc": {
+          "$ref": "#/definitions/SourceLocation"
+        }
+      },
+      "required": [
+        "src",
+        "body",
+        "condition",
+        "nodeType"
+      ]
+    },
+    "YulLeave": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "nodeType": {
+          "enum": [
+            "YulLeave"
+          ]
+        },
+        "nativeSrc": {
+          "$ref": "#/definitions/SourceLocation"
+        }
+      },
+      "required": [
+        "src",
+        "nodeType"
+      ]
+    },
+    "YulSwitch": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "cases": {
+          "type": "array",
+          "items": {
+            "$ref": "#/definitions/YulCase"
+          }
+        },
+        "expression": {
+          "$ref": "#/definitions/YulExpression"
+        },
+        "nodeType": {
+          "enum": [
+            "YulSwitch"
+          ]
+        },
+        "nativeSrc": {
+          "$ref": "#/definitions/SourceLocation"
+        }
+      },
+      "required": [
+        "src",
+        "cases",
+        "expression",
+        "nodeType"
+      ]
+    },
+    "YulTypedName": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "name": {
+          "type": "string"
+        },
+        "type": {
+          "type": "string"
+        },
+        "nodeType": {
+          "enum": [
+            "YulTypedName"
+          ]
+        },
+        "nativeSrc": {
+          "$ref": "#/definitions/SourceLocation"
+        }
+      },
+      "required": [
+        "src",
+        "name",
+        "type",
+        "nodeType"
+      ]
+    },
+    "YulVariableDeclaration": {
+      "type": "object",
+      "additionalProperties": false,
+      "properties": {
+        "src": {
+          "$ref": "#/definitions/SourceLocation"
+        },
+        "value": {
+          "anyOf": [
+            {
+              "$ref": "#/definitions/YulExpression"
+            },
+            {
+              "type": "null"
+            }
+          ]
+        },
+        "variables": {
+          "type": "array",
+          "items": {
+            "$ref": "#/definitions/YulTypedName"
+          }
+        },
+        "nodeType": {
+          "enum": [
+            "YulVariableDeclaration"
+          ]
+        },
+        "nativeSrc": {
+          "$ref": "#/definitions/SourceLocation"
+        }
+      },
+      "required": [
+        "src",
+        "variables",
+        "nodeType"
+      ]
+    }
+  }
+}
\ No newline at end of file
diff --git a/certora_autosetup/solidity_ast/statements.py b/certora_autosetup/solidity_ast/statements.py
new file mode 100644
index 0000000..e7983e7
--- /dev/null
+++ b/certora_autosetup/solidity_ast/statements.py
@@ -0,0 +1,169 @@
+"""Statement nodes of the Solidity compact AST (members of the Statement union)."""
+
+from __future__ import annotations
+
+from typing import TYPE_CHECKING, Literal
+
+from pydantic import BaseModel, ConfigDict
+
+from .base import SolcNode
+
+if TYPE_CHECKING:
+    from .declarations import ParameterList, VariableDeclaration
+    from .expressions import FunctionCall
+    from .unions import Expression, Statement
+    from .yul import YulBlock
+
+
+class Block(SolcNode):
+    """A curly-braced statement block."""
+
+    documentation: str | None = None
+    statements: "list[Statement] | None" = None
+    nodeType: Literal["Block"]
+
+
+class Break(SolcNode):
+    documentation: str | None = None
+    nodeType: Literal["Break"]
+
+
+class Continue(SolcNode):
+    documentation: str | None = None
+    nodeType: Literal["Continue"]
+
+
+class DoWhileStatement(SolcNode):
+    documentation: str | None = None
+    body: "Block | Statement"
+    condition: "Expression"
+    nodeType: Literal["DoWhileStatement"]
+
+
+class EmitStatement(SolcNode):
+    documentation: str | None = None
+    eventCall: "FunctionCall"
+    nodeType: Literal["EmitStatement"]
+
+
+class ExpressionStatement(SolcNode):
+    documentation: str | None = None
+    expression: "Expression"
+    nodeType: Literal["ExpressionStatement"]
+
+
+class ForStatement(SolcNode):
+    documentation: str | None = None
+    body: "Block | Statement"
+    condition: "Expression | None" = None
+    initializationExpression: "ExpressionStatement | VariableDeclarationStatement | None" = None
+    loopExpression: ExpressionStatement | None = None
+    isSimpleCounterLoop: bool | None = None
+    nodeType: Literal["ForStatement"]
+
+
+class IfStatement(SolcNode):
+    documentation: str | None = None
+    condition: "Expression"
+    falseBody: "Statement | Block | None" = None
+    trueBody: "Statement | Block"
+    nodeType: Literal["IfStatement"]
+
+
+class ExternalReference(BaseModel):
+    """An entry of ``InlineAssembly.externalReferences``: a Yul identifier that refers
+    to a Solidity declaration."""
+
+    model_config = ConfigDict(extra="allow")
+
+    declaration: int
+    isOffset: bool
+    isSlot: bool
+    src: str
+    valueSize: int
+    suffix: Literal["slot", "offset", "length"] | None = None
+
+
+class InlineAssembly(SolcNode):
+    """An ``assembly { ... }`` block; its Yul body lives under the ``AST`` field.
+
+    Dumps from solc <= 0.5 use a different dialect: no ``AST``/``evmVersion``, the
+    assembly source text in ``operations``, and ``externalReferences`` items keyed
+    by identifier name (LENIENT_REQUIRED / DELIBERATELY_OPEN deviations).
+    """
+
+    documentation: str | None = None
+    AST: "YulBlock | None" = None
+    # The schema enumerates the EVM fork names, but each new fork would make every
+    # assembly-containing source fail whole-file validation until the vendored
+    # schema catches up — deliberately open (allowlisted in the conformance test).
+    evmVersion: str | None = None
+    externalReferences: list[ExternalReference | dict[str, ExternalReference]]
+    # Same reasoning: new assembly flags arrive with new solc releases.
+    flags: list[str] | None = None
+    operations: str | None = None
+    nodeType: Literal["InlineAssembly"]
+
+
+class PlaceholderStatement(SolcNode):
+    """The ``_;`` placeholder inside a modifier body."""
+
+    documentation: str | None = None
+    nodeType: Literal["PlaceholderStatement"]
+
+
+class Return(SolcNode):
+    documentation: str | None = None
+    expression: "Expression | None" = None
+    # Schema-required, but solc omits it for `return;` inside a modifier body (no
+    # function to return to) — seen in the wild on solc 0.8.x (conformance
+    # deviation LENIENT_REQUIRED).
+    functionReturnParameters: int | None = None
+    nodeType: Literal["Return"]
+
+
+class RevertStatement(SolcNode):
+    """A ``revert SomeError(...)`` statement (solc >= 0.8.4)."""
+
+    documentation: str | None = None
+    errorCall: "FunctionCall"
+    nodeType: Literal["RevertStatement"]
+
+
+class TryStatement(SolcNode):
+    documentation: str | None = None
+    clauses: "list[TryCatchClause]"
+    externalCall: "FunctionCall"
+    nodeType: Literal["TryStatement"]
+
+
+class TryCatchClause(SolcNode):
+    """A ``try``-success or ``catch`` clause of a TryStatement."""
+
+    block: Block
+    errorName: str
+    parameters: "ParameterList | None" = None
+    nodeType: Literal["TryCatchClause"]
+
+
+class UncheckedBlock(SolcNode):
+    """An ``unchecked { ... }`` block (solc >= 0.8.0)."""
+
+    documentation: str | None = None
+    statements: "list[Statement]"
+    nodeType: Literal["UncheckedBlock"]
+
+
+class VariableDeclarationStatement(SolcNode):
+    documentation: str | None = None
+    assignments: list[int | None]
+    declarations: "list[VariableDeclaration | None]"
+    initialValue: "Expression | None" = None
+    nodeType: Literal["VariableDeclarationStatement"]
+
+
+class WhileStatement(SolcNode):
+    documentation: str | None = None
+    body: "Block | Statement"
+    condition: "Expression"
+    nodeType: Literal["WhileStatement"]
diff --git a/certora_autosetup/solidity_ast/traversal.py b/certora_autosetup/solidity_ast/traversal.py
new file mode 100644
index 0000000..866045a
--- /dev/null
+++ b/certora_autosetup/solidity_ast/traversal.py
@@ -0,0 +1,119 @@
+"""Traversal utilities over typed AST nodes, plus the legacy raw parent-graph builder."""
+
+from __future__ import annotations
+
+from typing import Any, Iterable, Iterator, TypeVar, cast
+
+from pydantic import BaseModel
+
+from .base import AstNode, SolcNode
+
+N = TypeVar("N", bound=AstNode)
+
+
+def iter_children(node: AstNode) -> Iterator[AstNode]:
+    """Direct AST children of a node, in model-field declaration order.
+
+    Helper models that are not themselves AST nodes (e.g. import symbol aliases,
+    ``using``-directive function lists) are transparent containers: AST nodes found
+    inside them are yielded as direct children of ``node``. Extra fields captured by
+    ``model_extra`` (unknown to the model set) are not descended into.
+    """
+    for name in type(node).model_fields:
+        yield from _child_nodes(getattr(node, name))
+
+
+def _child_nodes(value: Any) -> Iterator[AstNode]:
+    if isinstance(value, AstNode):
+        yield value
+    elif isinstance(value, BaseModel):
+        for name in type(value).model_fields:
+            yield from _child_nodes(getattr(value, name))
+    elif isinstance(value, list):
+        for item in value:
+            yield from _child_nodes(item)
+
+
+def walk(node: AstNode) -> Iterator[AstNode]:
+    """Pre-order DFS over ``node`` and all its descendants (iterative — deep
+    expression chains cannot hit the interpreter recursion limit)."""
+    stack = [node]
+    while stack:
+        current = stack.pop()
+        yield current
+        stack.extend(reversed(list(iter_children(current))))
+
+
+def find_all(root: AstNode, node_type: type[N] | tuple[type[N], ...]) -> Iterator[N]:
+    """All nodes of the given type(s) in the subtree rooted at ``root`` (inclusive),
+    in document order. The typed replacement for ``nodeType == "X"`` scans."""
+    for node in walk(root):
+        if isinstance(node, node_type):
+            yield node
+
+
+def build_node_index(root: AstNode) -> dict[int, AstNode]:
+    """Map every id-carrying node in the subtree to its instance (Yul nodes carry
+    no id and are not indexed)."""
+    return {node.id: node for node in walk(root) if isinstance(node, SolcNode)}
+
+
+def build_parent_map(root: AstNode) -> dict[int, int]:
+    """Map child node id -> parent node id over the subtree, for id-carrying nodes.
+
+    Nodes nested inside transparent helper containers are attached to the nearest
+    id-carrying AST ancestor.
+    """
+    parent_map: dict[int, int] = {}
+    stack: list[tuple[AstNode, int | None]] = [(root, None)]
+    while stack:
+        node, parent_id = stack.pop()
+        node_id = node.id if isinstance(node, SolcNode) else None
+        if node_id is not None and parent_id is not None:
+            parent_map[node_id] = parent_id
+        enclosing = node_id if node_id is not None else parent_id
+        stack.extend((child, enclosing) for child in iter_children(node))
+    return parent_map
+
+
+def build_parent_graph_json(
+    raw_asts: dict[str, Any] | Iterable[tuple[str, Any]],
+) -> dict[str, dict[str, dict[str, str]]]:
+    """Parent graph over RAW ``.asts.json`` data (a full dict, or streamed
+    ``(relative_path, path_data)`` pairs from ``loader.stream_raw_units``), in the
+    exact legacy format written to ``all_ast_parent_graph.json``:
+    {rel_path: {abs_path: {child_id: parent_id}}} with string ids.
+
+    Deliberately operates on the raw dicts with the historical child heuristic (a child
+    is any direct dict value, or list element, carrying an ``id`` key) and preserves
+    raw key order, so ``json.dump(..., indent=2)`` output stays byte-identical to what
+    existing readers of the file expect. Use :func:`build_parent_map` for typed code.
+    """
+    units: Iterable[tuple[str, Any]]
+    if isinstance(raw_asts, dict):
+        units = cast("Iterable[tuple[str, Any]]", raw_asts.items())
+    else:
+        units = raw_asts
+    parent_graph: dict[str, dict[str, dict[str, str]]] = {}
+    for relative_path, path_data in units:
+        parent_graph[relative_path] = {}
+        for absolute_path, nodes in path_data.items():
+            parent_graph[relative_path][absolute_path] = {}
+            for node_id, node in nodes.items():
+                if not isinstance(node, dict):
+                    continue
+                for child_id in _legacy_child_ids(node):
+                    parent_graph[relative_path][absolute_path][str(child_id)] = str(node_id)
+    return parent_graph
+
+
+def _legacy_child_ids(node: dict[str, Any]) -> list[Any]:
+    child_ids = []
+    for value in node.values():
+        if isinstance(value, dict) and "id" in value:
+            child_ids.append(value["id"])
+        elif isinstance(value, list):
+            for item in value:
+                if isinstance(item, dict) and "id" in item:
+                    child_ids.append(item["id"])
+    return child_ids
diff --git a/certora_autosetup/solidity_ast/types.py b/certora_autosetup/solidity_ast/types.py
new file mode 100644
index 0000000..bcf1003
--- /dev/null
+++ b/certora_autosetup/solidity_ast/types.py
@@ -0,0 +1,73 @@
+"""Type-name nodes of the Solidity compact AST (members of the TypeName union)."""
+
+from __future__ import annotations
+
+from typing import TYPE_CHECKING, Literal
+
+from .base import SolcNode, StateMutability, TypeDescriptions, Visibility
+
+if TYPE_CHECKING:
+    from .declarations import ParameterList
+    from .unions import Expression, TypeName
+
+
+class ArrayTypeName(SolcNode):
+    """A static or dynamic array type, e.g. ``uint256[]`` or ``bytes32[4]``."""
+
+    typeDescriptions: TypeDescriptions
+    baseType: "TypeName"
+    length: "Expression | None" = None
+    nodeType: Literal["ArrayTypeName"]
+
+
+class ElementaryTypeName(SolcNode):
+    """A built-in type name, e.g. ``uint256``, ``address``, ``bytes``."""
+
+    typeDescriptions: TypeDescriptions
+    name: str
+    stateMutability: StateMutability | None = None
+    nodeType: Literal["ElementaryTypeName"]
+
+
+class FunctionTypeName(SolcNode):
+    """A function type, e.g. ``function (uint) external returns (bool)``."""
+
+    typeDescriptions: TypeDescriptions
+    parameterTypes: "ParameterList"
+    returnParameterTypes: "ParameterList"
+    stateMutability: StateMutability
+    visibility: Visibility
+    nodeType: Literal["FunctionTypeName"]
+
+
+class Mapping(SolcNode):
+    """A mapping type, e.g. ``mapping(address owner => uint256 balance)``."""
+
+    typeDescriptions: TypeDescriptions
+    keyType: "TypeName"
+    valueType: "TypeName"
+    keyName: str | None = None
+    keyNameLocation: str | None = None
+    valueName: str | None = None
+    valueNameLocation: str | None = None
+    nodeType: Literal["Mapping"]
+
+
+class IdentifierPath(SolcNode):
+    """A (possibly dotted) path referring to a declaration, e.g. ``Lib.Struct``."""
+
+    name: str
+    nameLocations: list[str] | None = None
+    referencedDeclaration: int
+    nodeType: Literal["IdentifierPath"]
+
+
+class UserDefinedTypeName(SolcNode):
+    """A reference to a user-defined type (struct, enum, contract, UDVT)."""
+
+    typeDescriptions: TypeDescriptions
+    contractScope: None = None
+    name: str | None = None
+    pathNode: IdentifierPath | None = None
+    referencedDeclaration: int
+    nodeType: Literal["UserDefinedTypeName"]
diff --git a/certora_autosetup/solidity_ast/unions.py b/certora_autosetup/solidity_ast/unions.py
new file mode 100644
index 0000000..deff4b0
--- /dev/null
+++ b/certora_autosetup/solidity_ast/unions.py
@@ -0,0 +1,407 @@
+"""Discriminated unions over the AST node models, the schema-name registry, and the
+forward-reference rebuild wiring.
+
+Import this module (or the package) before validating any node model: importing it
+resolves every cross-module forward reference and rebuilds all models. Each union
+carries an UnknownNode fallback member selected for any unrecognized ``nodeType``,
+so ASTs from solc versions newer than the vendored schema degrade per-node instead
+of failing whole-file validation.
+"""
+
+from __future__ import annotations
+
+from typing import Annotated, Union
+
+from pydantic import Discriminator, Tag
+
+from . import declarations, expressions, statements, types, yul
+from .base import UNKNOWN_TAG, AstNode, UnknownNode, tag_by_node_type
+from .yul import YulExpression, YulLiteral, YulStatement
+
+
+from .types import (
+    ArrayTypeName,
+    ElementaryTypeName,
+    FunctionTypeName,
+    IdentifierPath,
+    Mapping,
+    UserDefinedTypeName,
+)
+from .expressions import (
+    Assignment,
+    BinaryOperation,
+    Conditional,
+    ElementaryTypeNameExpression,
+    FunctionCall,
+    FunctionCallOptions,
+    Identifier,
+    IndexAccess,
+    IndexRangeAccess,
+    Literal,
+    MemberAccess,
+    NewExpression,
+    TupleExpression,
+    UnaryOperation,
+)
+from .statements import (
+    Block,
+    Break,
+    Continue,
+    DoWhileStatement,
+    EmitStatement,
+    ExpressionStatement,
+    ForStatement,
+    IfStatement,
+    InlineAssembly,
+    PlaceholderStatement,
+    Return,
+    RevertStatement,
+    TryCatchClause,
+    TryStatement,
+    UncheckedBlock,
+    VariableDeclarationStatement,
+    WhileStatement,
+)
+from .declarations import (
+    ContractDefinition,
+    EnumDefinition,
+    EnumValue,
+    ErrorDefinition,
+    EventDefinition,
+    FunctionDefinition,
+    ImportDirective,
+    InheritanceSpecifier,
+    ModifierDefinition,
+    ModifierInvocation,
+    OverrideSpecifier,
+    ParameterList,
+    PragmaDirective,
+    SourceUnit,
+    StorageLayoutSpecifier,
+    StructDefinition,
+    StructuredDocumentation,
+    UserDefinedValueTypeDefinition,
+    UsingForDirective,
+    VariableDeclaration,
+)
+from .yul import (
+    YulAssignment,
+    YulBlock,
+    YulBreak,
+    YulCase,
+    YulContinue,
+    YulExpressionStatement,
+    YulForLoop,
+    YulFunctionCall,
+    YulFunctionDefinition,
+    YulIdentifier,
+    YulIf,
+    YulLeave,
+    YulLiteralHexValue,
+    YulLiteralValue,
+    YulSwitch,
+    YulTypedName,
+    YulVariableDeclaration,
+)
+
+_EXPRESSION_TAGS = frozenset({"Assignment", "BinaryOperation", "Conditional", "ElementaryTypeNameExpression", "FunctionCall", "FunctionCallOptions", "Identifier", "IndexAccess", "IndexRangeAccess", "Literal", "MemberAccess", "NewExpression", "TupleExpression", "UnaryOperation"})
+
+Expression = Annotated[
+    Union[
+        Annotated[Assignment, Tag("Assignment")],
+        Annotated[BinaryOperation, Tag("BinaryOperation")],
+        Annotated[Conditional, Tag("Conditional")],
+        Annotated[ElementaryTypeNameExpression, Tag("ElementaryTypeNameExpression")],
+        Annotated[FunctionCall, Tag("FunctionCall")],
+        Annotated[FunctionCallOptions, Tag("FunctionCallOptions")],
+        Annotated[Identifier, Tag("Identifier")],
+        Annotated[IndexAccess, Tag("IndexAccess")],
+        Annotated[IndexRangeAccess, Tag("IndexRangeAccess")],
+        Annotated[Literal, Tag("Literal")],
+        Annotated[MemberAccess, Tag("MemberAccess")],
+        Annotated[NewExpression, Tag("NewExpression")],
+        Annotated[TupleExpression, Tag("TupleExpression")],
+        Annotated[UnaryOperation, Tag("UnaryOperation")],
+        Annotated[UnknownNode, Tag(UNKNOWN_TAG)],
+    ],
+    Discriminator(tag_by_node_type(_EXPRESSION_TAGS)),
+]
+"""Any Solidity expression node (or UnknownNode)."""
+
+_STATEMENT_TAGS = frozenset({"Block", "Break", "Continue", "DoWhileStatement", "EmitStatement", "ExpressionStatement", "ForStatement", "IfStatement", "InlineAssembly", "PlaceholderStatement", "Return", "RevertStatement", "TryStatement", "UncheckedBlock", "VariableDeclarationStatement", "WhileStatement"})
+
+Statement = Annotated[
+    Union[
+        Annotated[Block, Tag("Block")],
+        Annotated[Break, Tag("Break")],
+        Annotated[Continue, Tag("Continue")],
+        Annotated[DoWhileStatement, Tag("DoWhileStatement")],
+        Annotated[EmitStatement, Tag("EmitStatement")],
+        Annotated[ExpressionStatement, Tag("ExpressionStatement")],
+        Annotated[ForStatement, Tag("ForStatement")],
+        Annotated[IfStatement, Tag("IfStatement")],
+        Annotated[InlineAssembly, Tag("InlineAssembly")],
+        Annotated[PlaceholderStatement, Tag("PlaceholderStatement")],
+        Annotated[Return, Tag("Return")],
+        Annotated[RevertStatement, Tag("RevertStatement")],
+        Annotated[TryStatement, Tag("TryStatement")],
+        Annotated[UncheckedBlock, Tag("UncheckedBlock")],
+        Annotated[VariableDeclarationStatement, Tag("VariableDeclarationStatement")],
+        Annotated[WhileStatement, Tag("WhileStatement")],
+        Annotated[UnknownNode, Tag(UNKNOWN_TAG)],
+    ],
+    Discriminator(tag_by_node_type(_STATEMENT_TAGS)),
+]
+"""Any Solidity statement node (or UnknownNode)."""
+
+_TYPENAME_TAGS = frozenset({"ArrayTypeName", "ElementaryTypeName", "FunctionTypeName", "Mapping", "UserDefinedTypeName"})
+
+TypeName = Annotated[
+    Union[
+        Annotated[ArrayTypeName, Tag("ArrayTypeName")],
+        Annotated[ElementaryTypeName, Tag("ElementaryTypeName")],
+        Annotated[FunctionTypeName, Tag("FunctionTypeName")],
+        Annotated[Mapping, Tag("Mapping")],
+        Annotated[UserDefinedTypeName, Tag("UserDefinedTypeName")],
+        Annotated[UnknownNode, Tag(UNKNOWN_TAG)],
+    ],
+    Discriminator(tag_by_node_type(_TYPENAME_TAGS)),
+]
+"""Any type-name node (or UnknownNode)."""
+
+# EventDefinition is absent from the vendored schema's SourceUnit.nodes union, but
+# solc >= 0.8.22 allows file-level events (seen in the wild; conformance deviation
+# DELIBERATELY_OPEN on SourceUnit.nodes).
+_SOURCEUNITNODE_TAGS = frozenset({"ContractDefinition", "EnumDefinition", "ErrorDefinition", "EventDefinition", "FunctionDefinition", "ImportDirective", "PragmaDirective", "StructDefinition", "UserDefinedValueTypeDefinition", "UsingForDirective", "VariableDeclaration"})
+
+SourceUnitNode = Annotated[
+    Union[
+        Annotated[ContractDefinition, Tag("ContractDefinition")],
+        Annotated[EnumDefinition, Tag("EnumDefinition")],
+        Annotated[ErrorDefinition, Tag("ErrorDefinition")],
+        Annotated[EventDefinition, Tag("EventDefinition")],
+        Annotated[FunctionDefinition, Tag("FunctionDefinition")],
+        Annotated[ImportDirective, Tag("ImportDirective")],
+        Annotated[PragmaDirective, Tag("PragmaDirective")],
+        Annotated[StructDefinition, Tag("StructDefinition")],
+        Annotated[UserDefinedValueTypeDefinition, Tag("UserDefinedValueTypeDefinition")],
+        Annotated[UsingForDirective, Tag("UsingForDirective")],
+        Annotated[VariableDeclaration, Tag("VariableDeclaration")],
+        Annotated[UnknownNode, Tag(UNKNOWN_TAG)],
+    ],
+    Discriminator(tag_by_node_type(_SOURCEUNITNODE_TAGS)),
+]
+"""Any node that may appear directly in SourceUnit.nodes (or UnknownNode)."""
+
+_CONTRACTBODYNODE_TAGS = frozenset({"EnumDefinition", "ErrorDefinition", "EventDefinition", "FunctionDefinition", "ModifierDefinition", "StructDefinition", "UserDefinedValueTypeDefinition", "UsingForDirective", "VariableDeclaration"})
+
+ContractBodyNode = Annotated[
+    Union[
+        Annotated[EnumDefinition, Tag("EnumDefinition")],
+        Annotated[ErrorDefinition, Tag("ErrorDefinition")],
+        Annotated[EventDefinition, Tag("EventDefinition")],
+        Annotated[FunctionDefinition, Tag("FunctionDefinition")],
+        Annotated[ModifierDefinition, Tag("ModifierDefinition")],
+        Annotated[StructDefinition, Tag("StructDefinition")],
+        Annotated[UserDefinedValueTypeDefinition, Tag("UserDefinedValueTypeDefinition")],
+        Annotated[UsingForDirective, Tag("UsingForDirective")],
+        Annotated[VariableDeclaration, Tag("VariableDeclaration")],
+        Annotated[UnknownNode, Tag(UNKNOWN_TAG)],
+    ],
+    Discriminator(tag_by_node_type(_CONTRACTBODYNODE_TAGS)),
+]
+"""Any node that may appear directly in ContractDefinition.nodes (or UnknownNode)."""
+
+_NODE_TAGS = frozenset({"ArrayTypeName", "Assignment", "BinaryOperation", "Block", "Break", "Conditional", "Continue", "ContractDefinition", "DoWhileStatement", "ElementaryTypeName", "ElementaryTypeNameExpression", "EmitStatement", "EnumDefinition", "EnumValue", "ErrorDefinition", "EventDefinition", "ExpressionStatement", "ForStatement", "FunctionCall", "FunctionCallOptions", "FunctionDefinition", "FunctionTypeName", "Identifier", "IdentifierPath", "IfStatement", "ImportDirective", "IndexAccess", "IndexRangeAccess", "InheritanceSpecifier", "InlineAssembly", "Literal", "Mapping", "MemberAccess", "ModifierDefinition", "ModifierInvocation", "NewExpression", "OverrideSpecifier", "ParameterList", "PlaceholderStatement", "PragmaDirective", "Return", "RevertStatement", "SourceUnit", "StorageLayoutSpecifier", "StructDefinition", "StructuredDocumentation", "TryCatchClause", "TryStatement", "TupleExpression", "UnaryOperation", "UncheckedBlock", "UserDefinedTypeName", "UserDefinedValueTypeDefinition", "UsingForDirective", "VariableDeclaration", "VariableDeclarationStatement", "WhileStatement", "YulAssignment", "YulBlock", "YulBreak", "YulCase", "YulContinue", "YulExpressionStatement", "YulForLoop", "YulFunctionCall", "YulFunctionDefinition", "YulIdentifier", "YulIf", "YulLeave", "YulLiteral", "YulSwitch", "YulTypedName", "YulVariableDeclaration"})
+
+Node = Annotated[
+    Union[
+        Annotated[ArrayTypeName, Tag("ArrayTypeName")],
+        Annotated[Assignment, Tag("Assignment")],
+        Annotated[BinaryOperation, Tag("BinaryOperation")],
+        Annotated[Block, Tag("Block")],
+        Annotated[Break, Tag("Break")],
+        Annotated[Conditional, Tag("Conditional")],
+        Annotated[Continue, Tag("Continue")],
+        Annotated[ContractDefinition, Tag("ContractDefinition")],
+        Annotated[DoWhileStatement, Tag("DoWhileStatement")],
+        Annotated[ElementaryTypeName, Tag("ElementaryTypeName")],
+        Annotated[ElementaryTypeNameExpression, Tag("ElementaryTypeNameExpression")],
+        Annotated[EmitStatement, Tag("EmitStatement")],
+        Annotated[EnumDefinition, Tag("EnumDefinition")],
+        Annotated[EnumValue, Tag("EnumValue")],
+        Annotated[ErrorDefinition, Tag("ErrorDefinition")],
+        Annotated[EventDefinition, Tag("EventDefinition")],
+        Annotated[ExpressionStatement, Tag("ExpressionStatement")],
+        Annotated[ForStatement, Tag("ForStatement")],
+        Annotated[FunctionCall, Tag("FunctionCall")],
+        Annotated[FunctionCallOptions, Tag("FunctionCallOptions")],
+        Annotated[FunctionDefinition, Tag("FunctionDefinition")],
+        Annotated[FunctionTypeName, Tag("FunctionTypeName")],
+        Annotated[Identifier, Tag("Identifier")],
+        Annotated[IdentifierPath, Tag("IdentifierPath")],
+        Annotated[IfStatement, Tag("IfStatement")],
+        Annotated[ImportDirective, Tag("ImportDirective")],
+        Annotated[IndexAccess, Tag("IndexAccess")],
+        Annotated[IndexRangeAccess, Tag("IndexRangeAccess")],
+        Annotated[InheritanceSpecifier, Tag("InheritanceSpecifier")],
+        Annotated[InlineAssembly, Tag("InlineAssembly")],
+        Annotated[Literal, Tag("Literal")],
+        Annotated[Mapping, Tag("Mapping")],
+        Annotated[MemberAccess, Tag("MemberAccess")],
+        Annotated[ModifierDefinition, Tag("ModifierDefinition")],
+        Annotated[ModifierInvocation, Tag("ModifierInvocation")],
+        Annotated[NewExpression, Tag("NewExpression")],
+        Annotated[OverrideSpecifier, Tag("OverrideSpecifier")],
+        Annotated[ParameterList, Tag("ParameterList")],
+        Annotated[PlaceholderStatement, Tag("PlaceholderStatement")],
+        Annotated[PragmaDirective, Tag("PragmaDirective")],
+        Annotated[Return, Tag("Return")],
+        Annotated[RevertStatement, Tag("RevertStatement")],
+        Annotated[SourceUnit, Tag("SourceUnit")],
+        Annotated[StorageLayoutSpecifier, Tag("StorageLayoutSpecifier")],
+        Annotated[StructDefinition, Tag("StructDefinition")],
+        Annotated[StructuredDocumentation, Tag("StructuredDocumentation")],
+        Annotated[TryCatchClause, Tag("TryCatchClause")],
+        Annotated[TryStatement, Tag("TryStatement")],
+        Annotated[TupleExpression, Tag("TupleExpression")],
+        Annotated[UnaryOperation, Tag("UnaryOperation")],
+        Annotated[UncheckedBlock, Tag("UncheckedBlock")],
+        Annotated[UserDefinedTypeName, Tag("UserDefinedTypeName")],
+        Annotated[UserDefinedValueTypeDefinition, Tag("UserDefinedValueTypeDefinition")],
+        Annotated[UsingForDirective, Tag("UsingForDirective")],
+        Annotated[VariableDeclaration, Tag("VariableDeclaration")],
+        Annotated[VariableDeclarationStatement, Tag("VariableDeclarationStatement")],
+        Annotated[WhileStatement, Tag("WhileStatement")],
+        Annotated[YulAssignment, Tag("YulAssignment")],
+        Annotated[YulBlock, Tag("YulBlock")],
+        Annotated[YulBreak, Tag("YulBreak")],
+        Annotated[YulCase, Tag("YulCase")],
+        Annotated[YulContinue, Tag("YulContinue")],
+        Annotated[YulExpressionStatement, Tag("YulExpressionStatement")],
+        Annotated[YulForLoop, Tag("YulForLoop")],
+        Annotated[YulFunctionCall, Tag("YulFunctionCall")],
+        Annotated[YulFunctionDefinition, Tag("YulFunctionDefinition")],
+        Annotated[YulIdentifier, Tag("YulIdentifier")],
+        Annotated[YulIf, Tag("YulIf")],
+        Annotated[YulLeave, Tag("YulLeave")],
+        Annotated[YulLiteralValue | YulLiteralHexValue, Tag("YulLiteral")],
+        Annotated[YulSwitch, Tag("YulSwitch")],
+        Annotated[YulTypedName, Tag("YulTypedName")],
+        Annotated[YulVariableDeclaration, Tag("YulVariableDeclaration")],
+        Annotated[UnknownNode, Tag(UNKNOWN_TAG)],
+    ],
+    Discriminator(tag_by_node_type(_NODE_TAGS)),
+]
+"""Any concrete AST node of any kind (or UnknownNode)."""
+
+# Schema definition name -> model class ("SourceUnit" is the schema root, the two
+# YulLiteral* variants share nodeType "YulLiteral").
+MODEL_BY_SCHEMA_DEF: dict[str, type[AstNode]] = {
+    "ArrayTypeName": types.ArrayTypeName,
+    "Assignment": expressions.Assignment,
+    "BinaryOperation": expressions.BinaryOperation,
+    "Block": statements.Block,
+    "Break": statements.Break,
+    "Conditional": expressions.Conditional,
+    "Continue": statements.Continue,
+    "ContractDefinition": declarations.ContractDefinition,
+    "DoWhileStatement": statements.DoWhileStatement,
+    "ElementaryTypeName": types.ElementaryTypeName,
+    "ElementaryTypeNameExpression": expressions.ElementaryTypeNameExpression,
+    "EmitStatement": statements.EmitStatement,
+    "EnumDefinition": declarations.EnumDefinition,
+    "EnumValue": declarations.EnumValue,
+    "ErrorDefinition": declarations.ErrorDefinition,
+    "EventDefinition": declarations.EventDefinition,
+    "ExpressionStatement": statements.ExpressionStatement,
+    "ForStatement": statements.ForStatement,
+    "FunctionCall": expressions.FunctionCall,
+    "FunctionCallOptions": expressions.FunctionCallOptions,
+    "FunctionDefinition": declarations.FunctionDefinition,
+    "FunctionTypeName": types.FunctionTypeName,
+    "Identifier": expressions.Identifier,
+    "IdentifierPath": types.IdentifierPath,
+    "IfStatement": statements.IfStatement,
+    "ImportDirective": declarations.ImportDirective,
+    "IndexAccess": expressions.IndexAccess,
+    "IndexRangeAccess": expressions.IndexRangeAccess,
+    "InheritanceSpecifier": declarations.InheritanceSpecifier,
+    "InlineAssembly": statements.InlineAssembly,
+    "Literal": expressions.Literal,
+    "Mapping": types.Mapping,
+    "MemberAccess": expressions.MemberAccess,
+    "ModifierDefinition": declarations.ModifierDefinition,
+    "ModifierInvocation": declarations.ModifierInvocation,
+    "NewExpression": expressions.NewExpression,
+    "OverrideSpecifier": declarations.OverrideSpecifier,
+    "ParameterList": declarations.ParameterList,
+    "PlaceholderStatement": statements.PlaceholderStatement,
+    "PragmaDirective": declarations.PragmaDirective,
+    "Return": statements.Return,
+    "RevertStatement": statements.RevertStatement,
+    "SourceUnit": declarations.SourceUnit,
+    "StorageLayoutSpecifier": declarations.StorageLayoutSpecifier,
+    "StructDefinition": declarations.StructDefinition,
+    "StructuredDocumentation": declarations.StructuredDocumentation,
+    "TryCatchClause": statements.TryCatchClause,
+    "TryStatement": statements.TryStatement,
+    "TupleExpression": expressions.TupleExpression,
+    "UnaryOperation": expressions.UnaryOperation,
+    "UncheckedBlock": statements.UncheckedBlock,
+    "UserDefinedTypeName": types.UserDefinedTypeName,
+    "UserDefinedValueTypeDefinition": declarations.UserDefinedValueTypeDefinition,
+    "UsingForDirective": declarations.UsingForDirective,
+    "VariableDeclaration": declarations.VariableDeclaration,
+    "VariableDeclarationStatement": statements.VariableDeclarationStatement,
+    "WhileStatement": statements.WhileStatement,
+    "YulAssignment": yul.YulAssignment,
+    "YulBlock": yul.YulBlock,
+    "YulBreak": yul.YulBreak,
+    "YulCase": yul.YulCase,
+    "YulContinue": yul.YulContinue,
+    "YulExpressionStatement": yul.YulExpressionStatement,
+    "YulForLoop": yul.YulForLoop,
+    "YulFunctionCall": yul.YulFunctionCall,
+    "YulFunctionDefinition": yul.YulFunctionDefinition,
+    "YulIdentifier": yul.YulIdentifier,
+    "YulIf": yul.YulIf,
+    "YulLeave": yul.YulLeave,
+    "YulLiteralHexValue": yul.YulLiteralHexValue,
+    "YulLiteralValue": yul.YulLiteralValue,
+    "YulSwitch": yul.YulSwitch,
+    "YulTypedName": yul.YulTypedName,
+    "YulVariableDeclaration": yul.YulVariableDeclaration,
+}
+
+
+_UNION_ALIASES: dict[str, object] = {
+    "Expression": Expression,
+    "Statement": Statement,
+    "TypeName": TypeName,
+    "SourceUnitNode": SourceUnitNode,
+    "ContractBodyNode": ContractBodyNode,
+    "Node": Node,
+    "YulStatement": YulStatement,
+    "YulExpression": YulExpression,
+    "YulLiteral": YulLiteral,
+}
+
+_NAMESPACE: dict[str, object] = {
+    **{cls.__name__: cls for cls in MODEL_BY_SCHEMA_DEF.values()},
+    **_UNION_ALIASES,
+}
+
+# Node modules reference classes and unions from sibling modules as string forward
+# refs only (they import nothing from each other at runtime). Resolve everything by
+# injecting the shared namespace into each module's globals — never clobbering a
+# name the module already defines (e.g. typing.Literal vs the Literal node class) —
+# and rebuild every model once.
+for _mod in (types, expressions, statements, declarations, yul):
+    for _name, _obj in _NAMESPACE.items():
+        if not hasattr(_mod, _name):
+            setattr(_mod, _name, _obj)
+
+for _cls in {*MODEL_BY_SCHEMA_DEF.values(), UnknownNode}:
+    _cls.model_rebuild(force=True)
+
diff --git a/certora_autosetup/solidity_ast/yul.py b/certora_autosetup/solidity_ast/yul.py
new file mode 100644
index 0000000..eb39ef1
--- /dev/null
+++ b/certora_autosetup/solidity_ast/yul.py
@@ -0,0 +1,186 @@
+"""Yul AST nodes (the ``AST`` of an ``InlineAssembly`` node, solc >= 0.6).
+
+Self-contained: unlike the Solidity node modules, the union aliases
+(``YulLiteral``/``YulExpression``/``YulStatement``) are defined here and all models
+are rebuilt at import time, so this module validates on its own.
+"""
+
+from __future__ import annotations
+
+from typing import Annotated, Literal, Union
+
+from pydantic import Discriminator, Tag
+
+from .base import UNKNOWN_TAG, UnknownNode, YulNode, tag_by_node_type
+
+
+class YulAssignment(YulNode):
+    value: YulExpression
+    variableNames: list[YulIdentifier]
+    nodeType: Literal["YulAssignment"]
+
+
+class YulBlock(YulNode):
+    statements: list[YulStatement]
+    nodeType: Literal["YulBlock"]
+
+
+class YulBreak(YulNode):
+    nodeType: Literal["YulBreak"]
+
+
+class YulCase(YulNode):
+    body: YulBlock
+    value: Literal["default"] | YulLiteral
+    nodeType: Literal["YulCase"]
+
+
+class YulContinue(YulNode):
+    nodeType: Literal["YulContinue"]
+
+
+class YulExpressionStatement(YulNode):
+    expression: YulExpression
+    nodeType: Literal["YulExpressionStatement"]
+
+
+class YulForLoop(YulNode):
+    body: YulBlock
+    condition: YulExpression
+    post: YulBlock
+    pre: YulBlock
+    nodeType: Literal["YulForLoop"]
+
+
+class YulFunctionCall(YulNode):
+    arguments: list[YulExpression]
+    functionName: YulIdentifier
+    nodeType: Literal["YulFunctionCall"]
+
+
+class YulFunctionDefinition(YulNode):
+    body: YulBlock
+    name: str
+    parameters: list[YulTypedName] | None = None
+    returnVariables: list[YulTypedName] | None = None
+    nodeType: Literal["YulFunctionDefinition"]
+
+
+class YulIdentifier(YulNode):
+    name: str
+    nodeType: Literal["YulIdentifier"]
+
+
+class YulIf(YulNode):
+    body: YulBlock
+    condition: YulExpression
+    nodeType: Literal["YulIf"]
+
+
+class YulLeave(YulNode):
+    nodeType: Literal["YulLeave"]
+
+
+class YulLiteralValue(YulNode):
+    value: str
+    kind: Literal["number", "string", "bool"]
+    type: str
+    nodeType: Literal["YulLiteral"]
+
+
+class YulLiteralHexValue(YulNode):
+    hexValue: str
+    kind: Literal["number", "string", "bool"]
+    type: str
+    value: str | None = None
+    nodeType: Literal["YulLiteral"]
+
+
+class YulSwitch(YulNode):
+    cases: list[YulCase]
+    expression: YulExpression
+    nodeType: Literal["YulSwitch"]
+
+
+class YulTypedName(YulNode):
+    name: str
+    type: str
+    nodeType: Literal["YulTypedName"]
+
+
+class YulVariableDeclaration(YulNode):
+    value: YulExpression | None = None
+    variables: list[YulTypedName]
+    nodeType: Literal["YulVariableDeclaration"]
+
+
+# Union aliases mirroring the schema's helper definitions. Both YulLiteral variants
+# share the "YulLiteral" tag, so within that branch pydantic picks by fields.
+YulLiteral = YulLiteralValue | YulLiteralHexValue
+
+YulExpression = Annotated[
+    Union[
+        Annotated[YulFunctionCall, Tag("YulFunctionCall")],
+        Annotated[YulIdentifier, Tag("YulIdentifier")],
+        Annotated[YulLiteralValue | YulLiteralHexValue, Tag("YulLiteral")],
+        Annotated[UnknownNode, Tag(UNKNOWN_TAG)],
+    ],
+    Discriminator(
+        tag_by_node_type(frozenset({"YulFunctionCall", "YulIdentifier", "YulLiteral"}))
+    ),
+]
+
+YulStatement = Annotated[
+    Union[
+        Annotated[YulAssignment, Tag("YulAssignment")],
+        Annotated[YulBlock, Tag("YulBlock")],
+        Annotated[YulBreak, Tag("YulBreak")],
+        Annotated[YulContinue, Tag("YulContinue")],
+        Annotated[YulExpressionStatement, Tag("YulExpressionStatement")],
+        Annotated[YulLeave, Tag("YulLeave")],
+        Annotated[YulForLoop, Tag("YulForLoop")],
+        Annotated[YulFunctionDefinition, Tag("YulFunctionDefinition")],
+        Annotated[YulIf, Tag("YulIf")],
+        Annotated[YulSwitch, Tag("YulSwitch")],
+        Annotated[YulVariableDeclaration, Tag("YulVariableDeclaration")],
+        Annotated[UnknownNode, Tag(UNKNOWN_TAG)],
+    ],
+    Discriminator(
+        tag_by_node_type(
+            frozenset(
+                {
+                    "YulAssignment",
+                    "YulBlock",
+                    "YulBreak",
+                    "YulContinue",
+                    "YulExpressionStatement",
+                    "YulLeave",
+                    "YulForLoop",
+                    "YulFunctionDefinition",
+                    "YulIf",
+                    "YulSwitch",
+                    "YulVariableDeclaration",
+                }
+            )
+        )
+    ),
+]
+
+# The Yul namespace is fully defined above, so forward refs resolve right here.
+YulAssignment.model_rebuild()
+YulBlock.model_rebuild()
+YulBreak.model_rebuild()
+YulCase.model_rebuild()
+YulContinue.model_rebuild()
+YulExpressionStatement.model_rebuild()
+YulForLoop.model_rebuild()
+YulFunctionCall.model_rebuild()
+YulFunctionDefinition.model_rebuild()
+YulIdentifier.model_rebuild()
+YulIf.model_rebuild()
+YulLeave.model_rebuild()
+YulLiteralValue.model_rebuild()
+YulLiteralHexValue.model_rebuild()
+YulSwitch.model_rebuild()
+YulTypedName.model_rebuild()
+YulVariableDeclaration.model_rebuild()
diff --git a/certora_autosetup/utils/file_utils.py b/certora_autosetup/utils/file_utils.py
index 39b9b42..a3f3ed3 100644
--- a/certora_autosetup/utils/file_utils.py
+++ b/certora_autosetup/utils/file_utils.py
@@ -4,23 +4,9 @@
 import os
 import threading
 import uuid
-from collections.abc import Iterator
 from pathlib import Path
 from typing import Any
 
-import ijson
-
-
-def stream_ast_files(ast_path: Path) -> Iterator[tuple[str, Any]]:
-    """Yield ``(relative_path, path_data)`` pairs from a ``.asts.json``.
-
-    The file is streamed one top-level entry at a time, so only a single source
-    file's ASTs are held in memory. ``.asts.json`` is sometimes many GB.
-    Structure: ``dict[relative_path: dict[absolute_path: dict[node_id: node_data]]]``.
-    """
-    with open(ast_path, "rb") as f:
-        yield from ijson.kvitems(f, "")
-
 
 def atomic_write_json(file_path: Path, data: Any, indent: int = 2) -> None:
     """
diff --git a/pyproject.toml b/pyproject.toml
index b537406..a52783d 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -143,6 +143,7 @@ certora-parallel-autosetup = "certora_autosetup.parallel_autosetup:main"
 certora-setup-summaries = "certora_autosetup.setup.setup_summaries:main"
 certora-setup-erc7201 = "certora_autosetup.setup.setup_erc7201:main"
 certora-run-auto-solc = "certora_autosetup.certoraRunAutoSolc:main"
+certora-fv-amenability = "certora_autosetup.amenability.cli:main"
 certora-fixconf = "certora_autosetup.fixconf:main"
 autosetup = "certora_autosetup.autosetup.cli:main"
 fixconf = "certora_autosetup.fixconf:main"
diff --git a/tests/solidity_ast/__init__.py b/tests/solidity_ast/__init__.py
new file mode 100644
index 0000000..e69de29
diff --git a/tests/solidity_ast/test_lenient_parsing.py b/tests/solidity_ast/test_lenient_parsing.py
new file mode 100644
index 0000000..e809857
--- /dev/null
+++ b/tests/solidity_ast/test_lenient_parsing.py
@@ -0,0 +1,120 @@
+"""Corpus-discovered leniency cases: shapes real solc emits that the vendored schema
+does not account for (see LENIENT_REQUIRED / DELIBERATELY_OPEN in the conformance
+test). Each must parse typed — not as UnknownNode, not as a parse failure — and
+round-trip without inventing the absent fields. When the producing solc version is
+known, VERSION_GATES turns illegitimate absence into a failure instead of a None."""
+
+import pytest
+
+from certora_autosetup.solidity_ast import (
+    AstDump,
+    ContractDefinition,
+    EventDefinition,
+    FunctionDefinition,
+    Return,
+    SourceUnit,
+    VariableDeclaration,
+)
+
+
+def test_pre_06_contract_without_abstract_parses() -> None:
+    contract = ContractDefinition.model_validate(
+        {
+            "id": 1, "src": "0:10:0", "nodeType": "ContractDefinition",
+            "name": "C", "baseContracts": [], "contractDependencies": [],
+            "contractKind": "contract", "fullyImplemented": True,
+            "linearizedBaseContracts": [1], "nodes": [], "scope": 0,
+        }
+    )
+    assert contract.abstract is False
+    assert "abstract" not in contract.model_dump(exclude_unset=True)
+
+
+def test_return_inside_modifier_body_parses() -> None:
+    ret = Return.model_validate({"id": 2, "src": "0:7:0", "nodeType": "Return"})
+    assert ret.functionReturnParameters is None
+    assert "functionReturnParameters" not in ret.model_dump(exclude_unset=True)
+
+
+_BARE_CONTRACT = {
+    "id": 1, "src": "0:10:0", "nodeType": "ContractDefinition",
+    "name": "C", "baseContracts": [], "contractDependencies": [],
+    "contractKind": "contract", "fullyImplemented": True,
+    "linearizedBaseContracts": [1], "nodes": [], "scope": 0,
+}
+
+
+def _dump_with(node: dict) -> dict:
+    return {"a.sol": {"a.sol": {"1": {
+        "id": 0, "src": "0:10:0", "nodeType": "SourceUnit",
+        "absolutePath": "a.sol", "exportedSymbols": {}, "nodes": [node],
+    }}}}
+
+
+def test_version_gate_fails_absent_field_at_or_above_gate() -> None:
+    data = _dump_with(dict(_BARE_CONTRACT))  # no `abstract` (gate: 0.6.0)
+    with pytest.raises(ValueError, match="version-gate violation.*abstract"):
+        AstDump.from_dict(data, on_error="raise", solc_version="0.8.30")
+
+    dump = AstDump.from_dict(data, on_error="raw", solc_version="0.8.30")
+    [(_, source)] = list(dump.iter_sources())
+    assert source.raw_kind == "parse_failed" and "abstract" in (source.parse_error or "")
+
+
+def test_version_gate_allows_absence_below_gate() -> None:
+    data = _dump_with(dict(_BARE_CONTRACT))
+    dump = AstDump.from_dict(data, on_error="raise", solc_version="0.5.17")
+    [(_, source)] = list(dump.iter_sources())
+    assert source.is_parsed
+
+
+def test_version_gate_off_without_version() -> None:
+    dump = AstDump.from_dict(_dump_with(dict(_BARE_CONTRACT)), on_error="raise")
+    [(_, source)] = list(dump.iter_sources())
+    assert source.is_parsed
+
+
+def test_effective_mutability_derives_from_constant() -> None:
+    def var(constant: bool) -> VariableDeclaration:
+        return VariableDeclaration.model_validate({
+            "id": 5, "src": "0:1:0", "nodeType": "VariableDeclaration",
+            "name": "x", "constant": constant, "scope": 1, "stateVariable": True,
+            "storageLocation": "default", "typeDescriptions": {}, "visibility": "internal",
+        })
+
+    assert var(True).mutability is None and var(True).effective_mutability == "constant"
+    assert var(False).effective_mutability == "mutable"
+
+
+def test_effective_kind_derives_from_04_flags() -> None:
+    def fn(name: str, is_constructor: bool) -> FunctionDefinition:
+        return FunctionDefinition.model_validate({
+            "id": 6, "src": "0:1:0", "nodeType": "FunctionDefinition",
+            "name": name, "implemented": True, "isConstructor": is_constructor,
+            "modifiers": [], "scope": 1, "stateMutability": "nonpayable",
+            "visibility": "public",
+            "parameters": {"id": 7, "src": "0:0:0", "nodeType": "ParameterList", "parameters": []},
+            "returnParameters": {"id": 8, "src": "0:0:0", "nodeType": "ParameterList", "parameters": []},
+        })
+
+    assert fn("f", False).kind is None and fn("f", False).effective_kind == "function"
+    assert fn("", True).effective_kind == "constructor"
+    assert fn("", False).effective_kind == "fallback"
+    assert fn("f", False).virtual is None
+
+
+def test_file_level_event_definition_is_typed() -> None:
+    unit = SourceUnit.model_validate(
+        {
+            "id": 10, "src": "0:50:0", "nodeType": "SourceUnit",
+            "absolutePath": "a.sol", "exportedSymbols": {},
+            "nodes": [{
+                "id": 11, "src": "0:20:0", "nodeType": "EventDefinition",
+                "name": "E", "anonymous": False,
+                "parameters": {"id": 12, "src": "0:0:0", "nodeType": "ParameterList",
+                               "parameters": []},
+            }],
+        }
+    )
+    [event] = unit.nodes
+    assert isinstance(event, EventDefinition)
diff --git a/tests/solidity_ast/test_schema_conformance.py b/tests/solidity_ast/test_schema_conformance.py
new file mode 100644
index 0000000..afaec1d
--- /dev/null
+++ b/tests/solidity_ast/test_schema_conformance.py
@@ -0,0 +1,530 @@
+"""Machine-checks every solidity_ast pydantic model against the vendored JSON Schema.
+
+The vendored OpenZeppelin ``solidity-ast`` schema (``certora_autosetup/solidity_ast/
+schema/schema.json``) is the source of truth for field sets. This test asserts, per
+schema definition and property: presence, requiredness, nullability, discriminator
+value, enum values, and a one-level structural kind check of the pydantic annotation.
+
+The schema-side helpers (``load_schema``/``node_definitions``/``classify_prop``) are
+pure and importable without the model modules; everything model-side is imported
+lazily via ``models()`` so this file stays usable while the model package is being
+built.
+"""
+
+from __future__ import annotations
+
+import json
+from collections import Counter
+from dataclasses import dataclass, field as dc_field, replace
+from functools import lru_cache
+from importlib import resources
+from types import NoneType, UnionType
+from typing import Annotated, Any, Literal, Union, get_args, get_origin
+
+import pytest
+
+# ---------------------------------------------------------------------------
+# Schema side (pure: no model imports)
+# ---------------------------------------------------------------------------
+
+
+@lru_cache(maxsize=None)
+def load_schema() -> dict[str, Any]:
+    schema_file = resources.files("certora_autosetup.solidity_ast") / "schema" / "schema.json"
+    return json.loads(schema_file.read_text(encoding="utf-8"))
+
+
+@lru_cache(maxsize=None)
+def node_definitions() -> dict[str, dict[str, Any]]:
+    """Every schema definition that has a ``nodeType`` property, plus the schema
+    ROOT (the SourceUnit definition lives at the top level, not under definitions).
+    """
+    schema = load_schema()
+    defs = {
+        name: definition
+        for name, definition in schema["definitions"].items()
+        if "nodeType" in definition.get("properties", {})
+    }
+    defs["SourceUnit"] = {"properties": schema["properties"], "required": schema["required"]}
+    return defs
+
+
+@dataclass(frozen=True)
+class Shape:
+    """One classified schema property (nulls stripped out of anyOf into ``nullable``)."""
+
+    kind: str  # primitive | enum | ref | array | map | object | union | null
+    nullable: bool = False
+    py: type | None = None  # primitive
+    values: tuple[Any, ...] = ()  # enum
+    ref: str = ""  # ref (definition name)
+    item: "Shape | None" = None  # array
+    members: tuple["Shape", ...] = ()  # union
+
+
+_PRIMITIVES = {"string": str, "integer": int, "boolean": bool, "number": float}
+
+
+def classify_prop(prop: dict[str, Any]) -> Shape:
+    """Classify a schema property into a Shape; raises on any shape the schema does
+    not actually contain (so schema updates that add new shapes fail loudly).
+    """
+    if "$ref" in prop:
+        return Shape("ref", ref=prop["$ref"].rsplit("/", 1)[-1])
+    if "anyOf" in prop:
+        non_null = [m for m in prop["anyOf"] if m.get("type") != "null"]
+        nullable = len(non_null) < len(prop["anyOf"])
+        if not non_null:
+            return Shape("null", nullable=True)
+        if len(non_null) == 1:
+            inner = classify_prop(non_null[0])
+            return replace(inner, nullable=nullable or inner.nullable)
+        return Shape(
+            "union", nullable=nullable, members=tuple(classify_prop(m) for m in non_null)
+        )
+    if "enum" in prop:
+        return Shape("enum", values=tuple(prop["enum"]))
+    schema_type = prop.get("type")
+    if schema_type == "null":
+        return Shape("null", nullable=True)
+    if schema_type in _PRIMITIVES:
+        return Shape("primitive", py=_PRIMITIVES[schema_type])
+    if schema_type == "array":
+        return Shape("array", item=classify_prop(prop["items"]))
+    if schema_type == "object":
+        additional = prop.get("additionalProperties")
+        if isinstance(additional, dict):
+            return Shape("map", item=classify_prop(additional))
+        return Shape("object")
+    raise ValueError(f"unclassifiable schema property: {json.dumps(prop)[:200]}")
+
+
+def classify_all() -> Counter[str]:
+    """Classify every property of every node definition; raises if any is
+    unclassifiable. Returns kind counts ('?' suffix marks nullable shapes).
+    Runnable standalone, before the model modules exist.
+    """
+    counts: Counter[str] = Counter()
+    for definition in node_definitions().values():
+        for prop in definition["properties"].values():
+            shape = classify_prop(prop)
+            counts[shape.kind + ("?" if shape.nullable else "")] += 1
+    return counts
+
+
+# ---------------------------------------------------------------------------
+# Model side (lazy imports: unions.py wires and rebuilds all node modules)
+# ---------------------------------------------------------------------------
+
+
+class ModelInterface:
+    def __init__(self) -> None:
+        from pydantic import BaseModel
+
+        from certora_autosetup.solidity_ast import unions, yul
+        from certora_autosetup.solidity_ast.base import (
+            Mutability,
+            StateMutability,
+            StorageLocation,
+            TypeDescriptions,
+            UnknownNode,
+            Visibility,
+        )
+
+        self.base_model: type = BaseModel
+        self.registry: dict[str, type] = unions.MODEL_BY_SCHEMA_DEF
+        self.unknown_node: type = UnknownNode
+        self.type_descriptions: type = TypeDescriptions
+        # How each schema helper definition is transcribed on the python side.
+        self.ref_to_py: dict[str, Any] = {
+            "SourceLocation": str,
+            "TypeDescriptions": TypeDescriptions,
+            "Visibility": Visibility,
+            "StateMutability": StateMutability,
+            "Mutability": Mutability,
+            "StorageLocation": StorageLocation,
+            "Expression": unions.Expression,
+            "Statement": unions.Statement,
+            "TypeName": unions.TypeName,
+            "YulStatement": yul.YulStatement,
+            "YulExpression": yul.YulExpression,
+            "YulLiteral": yul.YulLiteral,
+        }
+        # Classes that legitimately appear inside field annotations; any other
+        # BaseModel subclass found there is an inline-object helper model.
+        self.known_classes: frozenset[type] = frozenset(self.registry.values()) | {
+            TypeDescriptions
+        }
+
+
+@lru_cache(maxsize=None)
+def models() -> ModelInterface:
+    return ModelInterface()
+
+
+# Model fields allowed to have no schema property backing them.
+# certoraRun injects certora_contract_name into the dump (AstNode base field);
+# the rest are the <= 0.5 dialect: InlineAssembly.operations (assembly source
+# text) and the solc-0.4/0.5 FunctionDefinition flags.
+# nativeSrc needs no entry because every Yul definition lists it in the schema.
+FIELD_ALLOWLIST = frozenset({
+    "certora_contract_name",
+    "operations",
+    "isConstructor",
+    "isDeclaredConst",
+    "payable",
+    "superFunction",
+})
+
+# Definitions whose nodeType tag differs from the registry key: solc emits
+# nodeType "YulLiteral" for both literal kinds, discriminated by hexValue/value.
+TAG_OVERRIDES = {"YulLiteralValue": "YulLiteral", "YulLiteralHexValue": "YulLiteral"}
+
+
+# ---------------------------------------------------------------------------
+# Annotation flattening / atom extraction
+# ---------------------------------------------------------------------------
+
+
+def _flat_members(ann: Any) -> list[Any]:
+    """Union members of an annotation, with Annotated wrappers (pydantic Tag /
+    Discriminator metadata) and PEP 695 TypeAliasType lazily unwrapped.
+    """
+    while True:
+        if type(ann).__name__ == "TypeAliasType" and hasattr(ann, "__value__"):
+            ann = ann.__value__
+            continue
+        if get_origin(ann) is Annotated:
+            ann = get_args(ann)[0]
+            continue
+        break
+    if get_origin(ann) in (Union, UnionType):
+        members: list[Any] = []
+        for arg in get_args(ann):
+            members.extend(_flat_members(arg))
+        return members
+    return [ann]
+
+
+@dataclass
+class Atoms:
+    """The one-level structural content of an annotation (or of a Shape)."""
+
+    classes: set[type] = dc_field(default_factory=set)  # known models / primitives
+    helpers: set[type] = dc_field(default_factory=set)  # inline-object helper models
+    literals: set[Any] = dc_field(default_factory=set)
+    lists: list[Any] = dc_field(default_factory=list)  # element annotations / Shapes
+    dicts: int = 0
+    objects: int = 0  # expected-side marker for inline-object schemas
+    has_none: bool = False
+    other: list[Any] = dc_field(default_factory=list)
+
+    def merge(self, more: "Atoms") -> None:
+        self.classes |= more.classes
+        self.helpers |= more.helpers
+        self.literals |= more.literals
+        self.lists.extend(more.lists)
+        self.dicts += more.dicts
+        self.objects += more.objects
+        self.has_none = self.has_none or more.has_none
+        self.other.extend(more.other)
+
+
+def atoms_of(ann: Any, m: ModelInterface) -> Atoms:
+    """Flatten a python annotation into Atoms. The deliberate extra UnknownNode
+    union member is dropped (it is not part of the schema contract).
+    """
+    atoms = Atoms()
+    for member in _flat_members(ann):
+        origin = get_origin(member)
+        if member is NoneType:
+            atoms.has_none = True
+        elif origin is Literal:
+            atoms.literals |= set(get_args(member))
+        elif origin is list:
+            args = get_args(member)
+            atoms.lists.append(args[0] if args else Any)
+        elif origin is dict:
+            atoms.dicts += 1
+        elif isinstance(member, type):
+            if member is m.unknown_node:
+                pass
+            elif issubclass(member, m.base_model) and member not in m.known_classes:
+                atoms.helpers.add(member)
+            else:
+                atoms.classes.add(member)
+        else:
+            atoms.other.append(member)
+    return atoms
+
+
+def expected_atoms(shape: Shape, m: ModelInterface) -> Atoms:
+    """Atoms the schema Shape demands of the annotation (nullability excluded --
+    it is checked against requiredness separately).
+    """
+    atoms = Atoms()
+    if shape.kind == "primitive":
+        assert shape.py is not None
+        atoms.classes.add(shape.py)
+    elif shape.kind == "enum":
+        atoms.literals |= set(shape.values)
+    elif shape.kind == "ref":
+        target = m.ref_to_py.get(shape.ref)
+        if target is not None:
+            resolved = atoms_of(target, m)  # alias -> literals / union members / class
+            resolved.has_none = False  # alias-internal nullability is not the field's
+            atoms.merge(resolved)
+        elif shape.ref in m.registry:
+            atoms.classes.add(m.registry[shape.ref])
+        else:
+            atoms.other.append(f"unmapped $ref {shape.ref}")
+    elif shape.kind == "union":
+        for member in shape.members:
+            atoms.merge(expected_atoms(member, m))
+    elif shape.kind == "array":
+        atoms.lists.append(shape.item)
+    elif shape.kind == "map":
+        atoms.dicts += 1
+    elif shape.kind == "object":
+        atoms.objects += 1
+    elif shape.kind == "null":
+        pass
+    return atoms
+
+
+def _compare_atoms(actual: Atoms, expected: Atoms, where: str) -> list[str]:
+    """One-level comparison; array elements are compared one level deeper, maps and
+    inline objects are not recursed into.
+    """
+    errors: list[str] = []
+    if actual.classes != expected.classes:
+        errors.append(
+            f"{where}: annotation classes {sorted(c.__name__ for c in actual.classes)} "
+            f"!= schema {sorted(c.__name__ for c in expected.classes)}"
+        )
+    if actual.literals != expected.literals:
+        errors.append(
+            f"{where}: Literal values {sorted(map(str, actual.literals))} "
+            f"!= schema enum {sorted(map(str, expected.literals))}"
+        )
+    if expected.objects and not (actual.helpers or actual.dicts):
+        errors.append(f"{where}: schema inline object needs a helper BaseModel or dict")
+    if not expected.objects and actual.helpers:
+        errors.append(
+            f"{where}: unexpected helper model(s) "
+            f"{sorted(h.__name__ for h in actual.helpers)}"
+        )
+    if expected.dicts and not actual.dicts:
+        errors.append(f"{where}: schema map needs a dict[...] annotation")
+    if actual.dicts and not (expected.dicts or expected.objects):
+        errors.append(f"{where}: unexpected dict annotation")
+    if expected.other:
+        errors.append(f"{where}: {expected.other}")
+    if actual.other:
+        errors.append(f"{where}: unrecognized annotation member(s) {actual.other}")
+    return errors
+
+
+def check_shape(shape: Shape, ann: Any, m: ModelInterface, where: str) -> list[str]:
+    actual = atoms_of(ann, m)
+    expected = expected_atoms(shape, m)
+    errors = _compare_atoms(actual, expected, where)
+
+    if expected.lists:
+        if not actual.lists:
+            errors.append(f"{where}: schema array needs a list[...] annotation")
+        else:
+            # Compare all list elements jointly, so both list[A] | list[B] and
+            # list[A | B] transcriptions of an anyOf-of-arrays are accepted.
+            elem_expected = Atoms()
+            elem_nullable = False
+            for item_shape in expected.lists:
+                assert isinstance(item_shape, Shape)
+                elem_expected.merge(expected_atoms(item_shape, m))
+                elem_nullable = elem_nullable or item_shape.nullable
+            elem_actual = Atoms()
+            for elem_ann in actual.lists:
+                elem_actual.merge(atoms_of(elem_ann, m))
+            errors += _compare_atoms(elem_actual, elem_expected, where + " (element)")
+            if elem_nullable and not elem_actual.has_none:
+                errors.append(f"{where}: array items are nullable, element lacks | None")
+            if elem_actual.has_none and not elem_nullable:
+                errors.append(f"{where}: element allows None but schema items are not nullable")
+    elif actual.lists:
+        errors.append(f"{where}: unexpected list annotation")
+    return errors
+
+
+# ---------------------------------------------------------------------------
+# Per-property check
+# ---------------------------------------------------------------------------
+
+
+def field_for(model: type, prop: str) -> Any:
+    for field_name, info in model.model_fields.items():  # type: ignore[attr-defined]
+        if field_name == prop or info.alias == prop:
+            return info
+    return None
+
+
+# Fields deliberately WIDER than the schema, all validated against real dumps
+# (fixtures for solc 0.4.26 / 0.5.17 and the project corpus sweep). Presence and
+# requiredness are still checked; only the shape check is waived:
+# - InlineAssembly.evmVersion/flags: version-freshness enums — a closed transcription
+#   would demote every assembly-containing source on the first solc release the
+#   vendored schema lags behind.
+# - SourceUnit.nodes: the schema's union lacks EventDefinition, but solc >= 0.8.22
+#   allows file-level events.
+# - documentation on Contract/Function/Modifier/EventDefinition: plain NatSpec string
+#   in dumps from solc <= 0.5 (the StructuredDocumentation node form is 0.6+).
+# - ElementaryTypeNameExpression.typeName: plain string in dumps from solc <= 0.5.
+# - InlineAssembly.externalReferences: solc <= 0.5 items are keyed by identifier name.
+DELIBERATELY_OPEN = {
+    ("InlineAssembly", "evmVersion"),
+    ("InlineAssembly", "flags"),
+    ("SourceUnit", "nodes"),
+    ("ContractDefinition", "documentation"),
+    ("FunctionDefinition", "documentation"),
+    ("ModifierDefinition", "documentation"),
+    ("EventDefinition", "documentation"),
+    ("ElementaryTypeNameExpression", "typeName"),
+    ("InlineAssembly", "externalReferences"),
+}
+
+# Schema-required fields the models default instead: solc omits them in situations
+# the schema does not account for — either below the 0.6 floor (lenient-older
+# policy: typed parsing must still work) or in corners the schema over-requires.
+# Shape is still checked. exclude_unset round-trips keep the absence loyal.
+# - ContractDefinition.abstract, {Function,Modifier}Definition.virtual,
+#   FunctionCall.tryCall, VariableDeclaration.mutability: concepts added in 0.6.x.
+# - FunctionDefinition.kind: added in 0.5 (0.4 uses isConstructor).
+# - InlineAssembly.AST/evmVersion: absent in the <= 0.5 assembly dialect.
+# - Return.functionReturnParameters: omitted for `return;` inside a modifier body.
+# - MemberAccess.isLValue: omitted by solc 0.7.2 (only) on enum-member accesses —
+#   a bug window, present both before and after, so it cannot be a version gate.
+LENIENT_REQUIRED = {
+    ("MemberAccess", "isLValue"),
+    ("ContractDefinition", "abstract"),
+    ("FunctionDefinition", "virtual"),
+    ("FunctionDefinition", "kind"),
+    ("ModifierDefinition", "virtual"),
+    ("FunctionCall", "tryCall"),
+    ("VariableDeclaration", "mutability"),
+    ("InlineAssembly", "AST"),
+    ("InlineAssembly", "evmVersion"),
+    ("Return", "functionReturnParameters"),
+}
+
+
+def check_property(
+    model: type, prop: str, spec: dict[str, Any], required: bool, m: ModelInterface
+) -> list[str]:
+    where = f"{model.__name__}.{prop}"
+    info = field_for(model, prop)
+    if info is None:
+        return [f"{where}: field missing (no field named or aliased '{prop}')"]
+
+    errors: list[str] = []
+    shape = classify_prop(spec)
+    nullable = shape.nullable or shape.kind == "null"
+    has_none = atoms_of(info.annotation, m).has_none
+
+    if required:
+        if (model.__name__, prop) in LENIENT_REQUIRED:
+            if info.is_required():
+                errors.append(f"{where}: listed in LENIENT_REQUIRED but has no default")
+        else:
+            if not info.is_required():
+                errors.append(f"{where}: schema-required but field has a default")
+            if nullable and not has_none:
+                errors.append(f"{where}: required-but-nullable, annotation lacks | None")
+            if not nullable and has_none:
+                errors.append(f"{where}: required non-nullable, annotation must not allow None")
+    else:
+        if info.is_required():
+            errors.append(f"{where}: schema-optional but field is required")
+        elif info.default is not None:
+            errors.append(f"{where}: schema-optional, default must be None (got {info.default!r})")
+        if not has_none:
+            errors.append(f"{where}: schema-optional, annotation lacks | None")
+
+    if prop == "nodeType":
+        if get_args(info.annotation) != (shape.values[0],):
+            errors.append(
+                f"{where}: get_args(annotation) == {get_args(info.annotation)!r}, "
+                f"expected ({shape.values[0]!r},)"
+            )
+    elif (model.__name__, prop) in DELIBERATELY_OPEN:
+        pass
+    elif shape.kind != "null":  # a pure-null property only constrains nullability
+        errors += check_shape(shape, info.annotation, m, where)
+    return errors
+
+
+# ---------------------------------------------------------------------------
+# Tests
+# ---------------------------------------------------------------------------
+
+DEF_NAMES = sorted(node_definitions())
+
+
+def test_classifier_covers_every_schema_shape() -> None:
+    """Pure schema test (no models): every property shape is classifiable."""
+    counts = classify_all()
+    assert sum(counts.values()) == sum(
+        len(d["properties"]) for d in node_definitions().values()
+    )
+
+
+def test_registry_coverage_both_directions() -> None:
+    m = models()
+    schema_names = set(node_definitions())
+    model_names = set(m.registry)
+    missing = schema_names - model_names
+    extra = model_names - schema_names
+    assert not missing and not extra, (
+        f"MODEL_BY_SCHEMA_DEF mismatch: missing={sorted(missing)} extra={sorted(extra)}"
+    )
+
+
+@pytest.mark.parametrize("def_name", DEF_NAMES)
+def test_definition_conforms_to_schema(def_name: str) -> None:
+    m = models()
+    model = m.registry.get(def_name)
+    assert model is not None, f"no model registered for schema definition {def_name}"
+    definition = node_definitions()[def_name]
+    required = set(definition.get("required", []))
+    errors: list[str] = []
+    for prop, spec in definition["properties"].items():
+        errors += check_property(model, prop, spec, prop in required, m)
+    assert not errors, "\n".join(errors)
+
+
+@pytest.mark.parametrize("def_name", DEF_NAMES)
+def test_no_fields_beyond_schema(def_name: str) -> None:
+    m = models()
+    model = m.registry.get(def_name)
+    assert model is not None, f"no model registered for schema definition {def_name}"
+    props = set(node_definitions()[def_name]["properties"])
+    stray = [
+        info.alias or field_name
+        for field_name, info in model.model_fields.items()
+        if (info.alias or field_name) not in props
+        and (info.alias or field_name) not in FIELD_ALLOWLIST
+    ]
+    assert not stray, f"{model.__name__}: fields with no schema property: {sorted(stray)}"
+
+
+def test_node_type_tags_match_registry_keys() -> None:
+    m = models()
+    errors: list[str] = []
+    for def_name, model in m.registry.items():
+        expected_tag = TAG_OVERRIDES.get(def_name, def_name)
+        info = model.model_fields.get("nodeType")
+        if info is None:
+            errors.append(f"{def_name}: model {model.__name__} has no nodeType field")
+            continue
+        tags = get_args(info.annotation)
+        if tags != (expected_tag,):
+            errors.append(f"{def_name}: nodeType Literal {tags!r} != ({expected_tag!r},)")
+    assert not errors, "\n".join(errors)
diff --git a/tests/solidity_ast/test_unions.py b/tests/solidity_ast/test_unions.py
new file mode 100644
index 0000000..bd127e3
--- /dev/null
+++ b/tests/solidity_ast/test_unions.py
@@ -0,0 +1,47 @@
+"""Drift guards for the hand-maintained union wiring in unions.py."""
+
+from typing import get_args
+
+from pydantic import BaseModel
+
+from certora_autosetup.solidity_ast import unions
+from certora_autosetup.solidity_ast.base import UNKNOWN_TAG, UnknownNode
+
+UNION_TO_TAGSET = {
+    "Expression": unions._EXPRESSION_TAGS,
+    "Statement": unions._STATEMENT_TAGS,
+    "TypeName": unions._TYPENAME_TAGS,
+    "SourceUnitNode": unions._SOURCEUNITNODE_TAGS,
+    "ContractBodyNode": unions._CONTRACTBODYNODE_TAGS,
+    "Node": unions._NODE_TAGS,
+}
+
+
+def _tags_of(alias: object) -> set[str]:
+    """The Tag names attached to a union alias's members (excluding the fallback)."""
+    union_type, _discriminator = get_args(alias)
+    tags = set()
+    for member in get_args(union_type):
+        _member_type, tag = get_args(member)
+        tags.add(tag.tag)
+    return tags - {UNKNOWN_TAG}
+
+
+def test_union_tag_sets_match_members() -> None:
+    """A member whose tag is missing from the discriminator's frozenset would be
+    silently routed to UnknownNode — assert the hand-written sets cannot drift."""
+    for name, tagset in UNION_TO_TAGSET.items():
+        alias = getattr(unions, name)
+        assert _tags_of(alias) == set(tagset), name
+
+
+def test_every_union_has_unknown_fallback() -> None:
+    for name in UNION_TO_TAGSET:
+        union_type, _ = get_args(getattr(unions, name))
+        members = {get_args(m)[0] for m in get_args(union_type)}
+        assert UnknownNode in members, name
+
+
+def test_registry_classes_are_models() -> None:
+    for def_name, cls in unions.MODEL_BY_SCHEMA_DEF.items():
+        assert isinstance(cls, type) and issubclass(cls, BaseModel), def_name
diff --git a/tests/test_amenability.py b/tests/test_amenability.py
new file mode 100644
index 0000000..ad3637c
--- /dev/null
+++ b/tests/test_amenability.py
@@ -0,0 +1,120 @@
+"""Unit tests for certora-fv-amenability that need no AST-dump fixture.
+
+The signal-detection tests run against a committed AST dump of a bait contract;
+that dump and the fixture-backed tests are maintained in a separate private test
+corpus (which mounts this package as a submodule).
+"""
+
+import json
+import subprocess
+import sys
+
+import pytest
+
+from certora_autosetup.amenability.compile import CannotScoreError, resolve_dumps
+from certora_autosetup.amenability.report import Level
+from certora_autosetup.amenability.scoring import ScoringConfig, aggregate
+from certora_autosetup.amenability.signals.base import SignalResult
+
+
+class TestScoring:
+    def _results(self, config, overrides: dict[str, float]) -> list[SignalResult]:
+        return [SignalResult(s, overrides.get(s, 1.0)) for s in config.weights]
+
+    def test_clean_project_scores_high(self):
+        config = ScoringConfig.load()
+        static = aggregate(self._results(config, {}), config)
+        assert static.provisional_level is Level.HIGH
+
+    def test_few_severe_killers_is_not_low(self):
+        # Fewer than killers_for_low structural killers firing → medium, never low,
+        # even though those signals are severe (config-solvable friction).
+        config = ScoringConfig.load()
+        killers = list(config.structural_killers)
+        overrides = {k: 0.1 for k in killers[: config.killers_for_low - 1]}
+        static = aggregate(self._results(config, overrides), config)
+        assert static.provisional_level is not Level.LOW
+
+    def test_killer_cooccurrence_forces_low(self):
+        # killers_for_low structural killers severe together + weak overall → low.
+        config = ScoringConfig.load()
+        killers = list(config.structural_killers)
+        overrides = {k: 0.05 for k in killers[: config.killers_for_low]}
+        # also drag the friction signals down so the mean is genuinely weak
+        overrides.update({s: 0.2 for s in config.weights
+                          if s not in config.structural_killers})
+        static = aggregate(self._results(config, overrides), config)
+        assert static.provisional_level is Level.LOW
+
+    def test_non_structural_signals_never_force_low(self):
+        # Even if every friction signal craters, without killer co-occurrence the
+        # verdict stays medium — friction is config-solvable, not a rewrite.
+        config = ScoringConfig.load()
+        overrides = {s: 0.0 for s in config.weights
+                     if s not in config.structural_killers}
+        static = aggregate(self._results(config, overrides), config)
+        assert static.provisional_level is not Level.LOW
+
+
+class TestDumpResolution:
+    def test_missing_explicit_dump(self, tmp_path):
+        with pytest.raises(CannotScoreError) as exc:
+            resolve_dumps(tmp_path, [tmp_path / "nope.json"])
+        assert exc.value.error == "no-ast-dump"
+
+    def test_no_dump_is_does_not_compile(self, tmp_path):
+        with pytest.raises(CannotScoreError) as exc:
+            resolve_dumps(tmp_path, [])
+        assert exc.value.error == "does-not-compile"
+
+
+class TestCli:
+    def _run(self, *args):
+        return subprocess.run(
+            [sys.executable, "-m", "certora_autosetup.amenability.cli", *args],
+            capture_output=True, text=True,
+        )
+
+    def test_cannot_score_without_compilation(self, tmp_path):
+        proc = self._run(str(tmp_path))
+        assert proc.returncode == 1
+        err = json.loads(proc.stdout)
+        assert err["error"] == "does-not-compile"
+
+
+class TestJudgeGuardrails:
+    def test_clamp_requires_two_citations(self):
+        from certora_autosetup.amenability.judge.agent import _clamp
+
+        level, clamped = _clamp(Level.LOW, Level.MEDIUM, citations=1)
+        assert level is Level.LOW and clamped
+
+    def test_clamp_limits_to_one_step(self):
+        from certora_autosetup.amenability.judge.agent import _clamp
+
+        level, clamped = _clamp(Level.LOW, Level.HIGH, citations=5)
+        assert level is Level.MEDIUM and clamped
+
+    def test_agreement_passes_through(self):
+        from certora_autosetup.amenability.judge.agent import _clamp
+
+        level, clamped = _clamp(Level.MEDIUM, Level.MEDIUM, citations=0)
+        assert level is Level.MEDIUM and not clamped
+
+    def test_one_step_with_citations_allowed(self):
+        from certora_autosetup.amenability.judge.agent import _clamp
+
+        level, clamped = _clamp(Level.MEDIUM, Level.HIGH, citations=2)
+        assert level is Level.HIGH and not clamped
+
+    def test_rubric_loads_with_version_and_sha(self):
+        from certora_autosetup.amenability.judge.agent import load_rubric
+
+        ver, sha, text = load_rubric()
+        assert ver == "1"
+        assert len(sha) == 64
+        assert "low" in text and "Judging discipline" in text
+
+
+if __name__ == "__main__":
+    pytest.main([__file__, "-v"])