Auto-enable dynamic_bound/dynamic_dispatch when contract creation is detected

[shellygr]

SG: The standard way we dealt with Clones.clone and others in the past is NONDET'ing them. However there are cases where this solution limits the verification scope too much. In such cases it can be better to enable dynamic dispatch. If callers know they don't need to call the cloned contracts and reason about them it is possible to go back to NONDET. Opting for the more precise option here.

TODO: Consider if to move this to call_resolution, as it already gives out info about contract creation

---

Summary

• Dynamically created contracts are only resolvable by the Prover with dynamic_bound set; without it, calls on a freshly created instance may fail with ASSUME false[optimistic dispatcher] and every path through the creating function reverts.
• Detection is by creation instruction: per compilation unit, every FunctionDefinition/ModifierDefinition/ContractDefinition subtree of the already-parsed solc AST is scanned for Yul create/create2 and typed new C(), and creation kinds are propagated up the intra-unit call graph (referencedDeclaration edges from call sites, FunctionCallOptions-wrapped calls, and modifier invocations) to a fixpoint. Roots are nodes in in-scope files plus every base contract an in-scope contract linearizes over. This covers OpenZeppelin Clones, Solady LibClone, clones-with-immutable-args, CREATE3 wrappers, and hand-rolled factories with one mechanism — including creation living outside any function (state-variable initializers, inheritance-specifier base-constructor arguments) and creation reachable only through out-of-scope library code.
• Kind-aware gating: any reachable creation defaults dynamic_bound=1; only runtime-assembled bytecode (assembly create/create2, i.e. proxy/clone patterns) additionally defaults dynamic_dispatch — a typed new C() instance resolves to a clone of C under dynamic_bound alone, keeping the more precise static call resolution.
• Each key is still skipped independently if the user already controls it (pre-populated config dict entry, or a raw --dynamic_bound/--dynamic_dispatch token in --extra-args, both space and = forms).
• all_asts.json is parsed once and shared by the AST-parent-graph builder and the detector.

Known limitations (documented in the module docstring)

• Calls through internal function pointers carry no referencedDeclaration, so creation reachable only that way is missed (inherent to a static reference-based call graph).
• solc < 0.6 emits inline assembly as a raw source string (no structured Yul AST); raw creates there are invisible and a loud warning is logged. A conservative substring check on the legacy operations string is possible if desired — left out pending maintainer sign-off.

[shellygr]

why would it succeed in this case as opposed to failing in generate_ast_graph?

[shellygr]

Claude answers: You were right that it wouldn't — a JSON re-parse of the same file would fail exactly like generate_ast_graph's own parse did; the only cases the fallback actually covered were post-parse failures inside generate_ast_graph (parent-graph build or the graph-file write). Restructured in 24e9019: all_asts.json is parsed once in process_certora_build_json and the parsed dict is passed to both generate_ast_graph (signature now takes the dict) and creation detection, so the fallback is gone entirely. A parse failure now degrades both consumers to a single warning; a parent-graph build/write failure no longer affects detection at all.

[shellygr]

alternatively, we could make this part of call resolution, add a hook on CREATE and CREATE2 opcodes that asserts and match on that in order to enable the flags, instead of relying on brittle AST parsing