Typed pydantic models of the Solidity compact AST (--dump_asts) + autosetup migration#76
Open
shellygr wants to merge 12 commits into
Open
Typed pydantic models of the Solidity compact AST (--dump_asts) + autosetup migration#76shellygr wants to merge 12 commits into
shellygr wants to merge 12 commits into
Conversation
Foundation for a full pydantic model of the solc compact AST as dumped by certoraRun --dump_asts. schema/schema.json is the OpenZeppelin solidity-ast 0.4.62 JSON Schema (MIT, see schema/NOTICE); models will be hand-authored and machine-verified against it. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…mance tests, fixtures 74 hand-authored pydantic v2 models (Solidity + Yul compact AST), discriminated unions with an UnknownNode fallback per union, single-point forward-ref rebuild, a loader for the 3-level --dump_asts structure (single-parse-per-source, Vyper raw passthrough, per-source degradation), traversal utilities incl. the frozen byte-compatible legacy parent-graph builder, a 151-case schema-conformance suite against the vendored schema, and real .asts.json fixtures generated via certoraRun for solc 0.6.12 / 0.7.6 / 0.8.30. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…olden test Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
setup_prover: declared-contracts and inheritance extraction go through a shared _iter_contract_declarations (typed find_all with a raw-scan fallback for sources the models cannot parse); generate_ast_graph delegates to the relocated byte-compatible parent-graph builder. auto_munges: .code detection iterates typed MemberAccess nodes (per-node raw salvage on unparsable sources) and decodes src offsets via parse_src. Parity with the legacy raw algorithms is pinned by tests/solidity_ast/test_consumer_migration.py on the real fixtures. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…enums, cached loads Review findings addressed: iter_nodes_of_type gives typed-first iteration with a raw flat-map sweep for nodes the typed walk cannot reach (e.g. under an unknown future nodeType), used by both migrated consumers so no ContractDefinition or .code MemberAccess can be hidden; InlineAssembly.evmVersion/flags are open strings (a closed fork enum would demote whole files on the next solc release — conformance test carries the allowlisted deviation); .code patches now read and target the source file the offsets refer to (not the compilation unit's main file) and are deduplicated across units; the dump is loaded once per setup run via AstDump.load_cached; union tag sets got a drift-guard test. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
roundtrip_diffs() compares a re-serialized typed tree against the exact source JSON (model_dump with exclude_unset; the internalFunctionIDs de-stamping is the one reversed normalization). Wired into the __main__ validator (with a --json machine mode for corpus sweeps) and pinned on the committed fixtures. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Corpus-driven: real certoraRun fixtures for solc 0.4.26 and 0.5.17 exposed the full legacy dialect, now handled typed (no raw-dict fallback): lenient defaults for fields that did not exist yet (mutability, virtual, tryCall, kind, abstract), string-form documentation and ElementaryTypeNameExpression.typeName, the pre-0.6 InlineAssembly shape (operations text, keyed externalReferences, no Yul AST), file-level EventDefinition (solc >= 0.8.22, missing from the vendored schema), and modeled 0.4-era FunctionDefinition flags. Every deviation from the schema is machine-tracked in the conformance test (LENIENT_REQUIRED / DELIBERATELY_OPEN / FIELD_ALLOWLIST). All five fixtures hold the same strict invariants: fully typed parse, zero unknown nodes, zero unmodeled fields, exact round-trip. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
When the producing solc version is known, a gated field absent at or above its introduction gate fails the source instead of silently reading as None (crash over wrong results); fixtures now always parse with their version so the gates stay exercised. virtual is None below 0.6 (everything was implicitly overridable — False would mislead). effective_mutability/effective_kind derive the pre-gate values faithfully from constant/isConstructor without touching the serialized form. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Empirical solc ladder over every release 0.4.24-0.8.36 pinned the exact gate boundaries: FunctionCall.tryCall from 0.6.0 and InlineAssembly.evmVersion from 0.6.2 (both previously gated later, i.e. under-enforced). solc 0.7.2 alone omits isLValue on enum-member MemberAccess nodes — a bug window, present before and after, so it is lenient (None) rather than gated. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…solidity_ast stream_ast_files's four call sites collapse into the typed layer: new AstDump.stream_units() (per-compilation-unit typed streaming with unit_filter and solc_version gates) and stream_raw_units() (raw pairs for the byte-compat parent-graph pass, which now accepts streamed units). All three consumers stream instead of whole-file loading; load_cached is gone (the memory win outweighs the shared parse), stream_ast_files removed with its purpose. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Contributor
Author
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
A new subpackage
certora_autosetup/solidity_ast/: a full, hand-authored pydantic v2 model of the solc compact AST as it appears in the.asts.jsondump produced bycertoraRun --dump_asts, plus migration of the two autosetup consumers of that dump onto it.solidity-astJSON Schema (vendored atsolidity_ast/schema/schema.json, v0.4.62, MIT — seeschema/NOTICE). The schema unions solc versions >= 0.6: version-added fields are optional, genuinely-null fields are nullable.Expression,Statement,TypeName,SourceUnitNode,ContractBodyNode,Node,YulStatement,YulExpression) onnodeType, each with anUnknownNodefallback member so an unrecognized node type from a newer solc degrades per-node instead of failing the file.AstDump.load/load_cached) for the dump's 3-level structure{original_file: {source_file: {node_id: node}}}: validates each source'sSourceUnittree exactly once (the flat id map duplicates nodes nested in ancestors), derives the id index by traversal, keeps the raw map alongside. Vyper sources pass through raw behind an explicitraw_kind="vyper"; a source the models reject entirely degrades toraw_kind="parse_failed"with the raw map retained.walk/find_all, typedbuild_parent_map,iter_nodes_of_type(typed-first + raw flat-map sweep for nodes the typed walk can't reach), andbuild_parent_graph_json— a byte-compatible relocation of the legacy parent-graph heuristic.Consumer migration (parity-pinned)
setup_prover.py: declared-contracts and inheritance/abstract extraction now go through typedContractDefinitionaccess with a raw-scan fallback;generate_ast_graphdelegates to the relocated builder — output file stays byte-identical (golden test).auto_munges.py:.codeaccess detection iterates typedMemberAccesscandidates with the raw sweep, so no access can be hidden by an unknown ancestor node or an unparsable source. Patches now read/target the source file the offsets refer to (previously a.codeaccess in an in-scope imported file produced a patch against the compilation unit's main file at foreign offsets — silent source corruption) and are deduplicated across compilation units.Guardrails
tests/solidity_ast/test_schema_conformance.py: machine-checks every model against the vendored schema — coverage in both directions, per-property presence/requiredness/nullability/enum/one-level kind (155 checks). Two deliberate, allowlisted deviations:InlineAssembly.evmVersion/flagsare open strings (a closed EVM-fork enum would demote every assembly-containing file on the first post-schema solc release).certoraRun --dump_astsfor solc 0.6.12 / 0.7.6 / 0.8.30 (path-sanitized; regeneration script included, dev-only) + a hand-written Vyper-mixed fixture. Strict parsing asserts zero unknown nodes and zero unmodeled fields — the schema-drift alarm.detect_code_accessesrun producing correct patches.Known pre-existing issue (not fixed here)
solc
srcoffsets are byte offsets, but patch extraction/application slices Python strings by character index — any non-ASCII character before a.codeaccess shifts the spans (detect and apply err consistently, so the mismatch check does not catch it). Fixing it properly touchesapply_code_access_patches/_inject_load_code_into_contractand deserves its own change.Manual validation
Point it at any existing project dump: prints per-source parse status, node counts, unknown/unmodeled fields (should be none), and contracts with resolved inheritance.
🤖 Generated with Claude Code