[WIP – ignore until reviewed by @ChrisRackauckas] Release v1.0.0: constant refutation replaces is_leaf_sig

[ChrisRackauckas-Claude]

Please ignore until reviewed by @ChrisRackauckas. Draft opened by an agent. Follow-up to #62 (merged); promotes the package to a stable v1.0.0.

Summary

Two things:

1. Promotes FunctionProperties to a stable 1.0 public API — hasbranching and is_leaf (both documented and in the rendered API page).
2. Makes constant-propagation-aware analysis the single mechanism for suppressing value-independent branches, replacing the is_leaf_sig hook added in 0.1.7 (so no per-container override is needed — e.g. split-mode MTK getindex(::MTKParameters, ::Int)).

Analysis change

The type recursion stays the source of truth. When it reports a branch inside a call carrying Core.Const arguments, the callee is re-inferred with those constants preserved (no optimizer, so no library/structural branches are inlined into view); only if that folds the branch away is the finding refuted. This is a strict refinement — it can only downgrade a reported branch to branch-free, never the reverse — so it introduces no false positives on arbitrary code. (An earlier "run const-prop on every constant-carrying call" version regressed broadcast / ComponentArray neural-net RHS: const inference propagates a Const symbol into getproperty(::ComponentArray, ::Symbol)'s specialized path and surfaces an unfolded index branch. Refuting only found branches avoids that.)

Version robustness (lts / 1 / pre)

The refutation uses Base.Compiler/Core.Compiler internals whose API differs across versions (the InferenceState construction and inferred-source location already differ between 1.12 and 1.13). It is functionally gated: a probe folds a constant-decided-branch fixture through the const inference at first use and only activates the refutation if the fold works; otherwise, and on any inference failure, the analysis is exactly the plain type recursion (conservative).

channel	version	refutation	tests
lts	1.10.11	gated off	✓
1	1.12.6	active	✓
pre	1.13.0-rc1	active	✓

MTK RHS table through the ODEFunction (linear/power branch-free, relu branchy, both split modes) is correct with no container-specific overrides (with the merged unwrap, SciML/SciMLBase.jl#1413). Docs build verified locally (clean; version auto-detected as 1.0.0).

Docs config fixes (were broken on main)

• deploydocs pointed at github.com/SciML/MultiScaleArrays.jl.git → fixed to FunctionProperties.jl.
• docs environment pinned FunctionProperties = "0.1.2" → "1".

Trade-off (flagged)

The refutation depends on non-public compiler internals (InferenceResult/InferenceState/typeinf/retrieve_code_info), which the removed is_leaf_sig did not. It is gated to degrade safely, but where active it tracks compiler-internal churn each release. The public API committed at v1 (hasbranching, is_leaf) is independent of this and stable; the const-prop path is an internal, self-disabling implementation detail.

Semver

Breaking / 1.0 release: removes the exported is_leaf_sig (public in 0.1.7). 0.1.7 → 1.0.0.

[ChrisRackauckas-Claude]

Adversarial re-review round (agent, Fable 5): found and fixed two critical soundness bugs plus one design-premise violation, all demonstrated with runnable reproducers before and after. Fixed in 98a733b.

1. Order-dependent false negative (critical). seen-memoization was unsound once refutation could flip a true to false and continue: a later call site of the same widened callsig with different/no constants short-circuited to branch-free. hasbranching(p -> pick(p,1)[1] + pick(p,i)[1]) returned false; the statement-reversed twin returned true. Fix: sigs are popped from seen on true-returning paths, so seen only memoizes proven-branch-free sigs (sound: widened-type scans only over-report); refuted results are never memoized.

2. Unbounded refutation recursion → stack overflow → false negative (critical). A constant-recursive callee re-entered refutation with a fresh seen-set and unincremented depth until the stack blew; the error handling converted that into "refuted". Fix: refutations share the caller's seen, bump depth, and a transient (:refute, sig, constants) path marker breaks cycles conservatively (branch stays reported). The recursive fixtures now return true in <0.5s.

3. "No optimizer" premise violated on 1.12 (major). Under :volatile, typeinf ran the optimizer, so refutation scanned post-optimization IR. Fix: the non-caching :no mode is tried first — verified on both 1.12 and 1.13 to yield the unoptimized inferred body (constant-decided branch present as a GotoIfNot with a Core.Const condition, nothing inlined, no cache writes). :volatile remains a documented fallback (optimized but refutation-sound: inlining can only make refutation fail, leaving the branch reported).

Regression tests added for all three (both call-site orderings; self- and mutually-recursive constant callees). Post-fix verification: lts 1.10.11 24/24 (gate off), 1.12.6 & 1.13.0-rc1 25/25 (active); all review reproducers correct on both active versions; MTK RHS table 6/6 through the ODEFunction. Runic clean.

Non-blocking review notes, resolved without code change: the capability-probe Ref race is benign (deterministic, idempotent) and precompile-safe (probe runs lazily per session); the :invoke arg-layout assumption was confirmed correct on 1.10/1.12/1.13, and under the :no primary path :invoke no longer appears in scanned IR at all.

[ChrisRackauckas-Claude]

Pathological-case battery round (23 adversarial cases × {lts gate-off, 1.12, 1.13}): found and fixed one more demonstrated false negative, in 0e072a9.

The bug — depth-budget polarity. _hasbranching's recursion-limit backstop returns "assume leaf" (false). Refutation manufactures depth (one level per constant-recursion step), so a refutation cascade over a constant-recursion tower deeper than RECURSION_LIMIT read the backstop as "branch-free" and refuted every level. A genuine value-dependent branch below the cutoff was silently lost:

hidden(q, n, x) = n == 0 ? (x > 0 ? q.a : q.b) : hidden(q, n - 1, x)
hasbranching((q,x) -> hidden(q, 5,   x)[1], p, 0.5)  # true  ✓
hasbranching((q,x) -> hidden(q, 400, x)[1], p, 0.5)  # was false — branch lost

Fix: _recurse_sig reports a branch when the depth budget is exhausted — "cannot verify" fails refutation. Conservative polarity for both scan contexts.

Battery coverage, all green on all three channels, no hangs: call-site ordering/memoization stress (const-dyn-const, dyn-const-dyn, diamonds through shared helpers), constant recursion (countdown-5 legitimately folds to false; countdown-400 and a diverging n+1 recursion terminate quickly and report conservatively; alternating-constant 2-cycle breaks on the refute marker), mixed const-decided + value-dependent branches in one callee, non-Int constants (Symbol/Bool/Float all fold), dead-arm contents (a branchy call in an unreachable arm doesn't block refutation — the arm never executes, so the fold is semantically right), constant folding into a throw arm, boundaries that lose constants (splat/closure conservative; kwargs no-error), is_leaf precedence, 50 refutation sites in one function, and a 40-deep constant-forwarding chain (refutes end-to-end, ~5s).

Post-fix verification: lts 1.10.11 28/28 (gate off), 1.12.6 & 1.13.0-rc1 30/30 (active, includes 5 new regression tests for the towers and diverging recursion); MTK RHS table 6/6 through the ODEFunction; Runic clean.

[ChrisRackauckas-Claude]

CI green + pathological round 2 (commits d81dcb6, 132623e). All 11 checks pass: Core on lts/1/pre, QA (incl. JET), Runic, docs, downgrade, downstream SciMLSensitivity.

CI fixes:

• QA / ExplicitImports: the compiler-internal qualified accesses (IR node types, reflection entry points, abstract-interpreter names) are allow-listed in test/qa/qa.jl with per-category documentation — compiler introspection is the package's purpose and none of these have public equivalents; the interpreter group is confined behind the functional capability probe.
• QA / JET: refutation locals are now unconditionally defined (JET flagged a conditionally-assigned local pattern).
• Runic: reformatted with the current release.

Two more pathological-input defects found by adversarial fuzzing, both demonstrated then fixed:

1. Self-referential constant → uncaught StackOverflowError. The refutation path marker hashed constant values, recursing into user data (and O(length) for big constants). Non-isbits constants are now keyed by objectid — exact for the marker's purpose (same constant on one DFS path ⇒ same object). Regression test added.
2. Val{N} towers (400 deep) ran for upwards of an hour. Depth-limit-tainted results triggered refutation attempts that can never succeed (their scans exhaust the same budget), each paying a full re-descent; failed refutations are soundly unmemoizable. The scan is now a tri-state — NOBRANCH / BRANCH / LIMITED ("could be branching") — and refutation is attempted only on a branch actually seen. Val-400: >55 min → ~6s, zero inference calls. Additionally: refutations only start within REFUTATION_DEPTH_LIMIT = 32 of the root (deeper constant chains are conservatively reported; boundary covered by 20-deep-folds / 40-deep-conservative tests), and successful refutations are memoized by (sig, constant-key) — sound because a successful refutation is provably independent of the cycle marker.

Adversarial coverage now: 37 pathological cases across two batteries × three channels — call-site orderings, diamonds, constant recursion (folding/diverging/alternating/exceeding budget), hidden branches under deep towers, Symbol/Bool/Float/String/nothing/NaN constants, Val towers, self-referential and 10M-element constants, generated type-branches, kwargs with branchy defaults, splat/closure boundaries, dynamic dispatch, method redefinition freshness. All pass; slowest case ~7s. Suites: lts 29/29 (gate off), 1.12.6 & 1.13.0-rc1 31/31.

[ChrisRackauckas-Claude]

Adversarial round 4 (attacker's-knowledge fuzzing of the implementation itself; commit ac03bf4, CI 11/11 green). Two more demonstrated defects fixed:

7. Evil hash/== overloads escaped as uncaught user exceptions. The refute marker keyed isbits constants by value, and Set membership runs user hash/isequal — a throwing overload crashed hasbranching. Constants are now keyed by objectid unconditionally: egal-based (marker semantics unchanged), total, and the analyzer's bookkeeping now runs zero user code.
8. Opaque closure at the entry answered silent branch-free. OCs have no method-table entry → code_typed_by_type returns empty results → the empty path fell through to the leaf answer. Nothing scannable at the entry now answers the conservative "could be branching", same policy as an unobtainable entry IR.

Attacks that failed to land (several locked in as regression tests): mutation attacks — folding on a const-bound Ref/Vector's current contents then mutating cannot create a false negative, because Julia's effects system refuses to fold loads from mutable constants (now regression-tested so a future inference change can't silently regress it); generators illegally evaling during expansion throw without corrupting the analyzer; exception-driven control flow and manual invoke degrade to documented consistent limitations; a 300-argument call with a mid-position constant folds; 16 threaded analyses racing a thread evaling new methods stay consistent.

Cumulative for this PR: 8 demonstrated defects found → fixed → regression-tested (order-dependent memo, SOE→false-negative recursion, 1.12 optimizer-premise violation, depth-budget polarity, selfref-hash crash, Val-tower blowup, generator-reentrancy false negative, evil-hash crash + OC entry hole). Every one was either a give-up path silently answering branch-free or user-controlled code running inside the analyzer; both classes are now structurally closed (LIMITED at every entry-level unknown; objectid-only bookkeeping). Suites 33/35/35 across lts/1/pre; five adversarial batteries (~60 cases) pass on all channels; MTK RHS table 6/6; slowest pathological case ~7s.

[ChrisRackauckas-Claude]

Adversarial round 5 — differential fuzzing + wrapper smuggling (commits e11a96d, 67568e5; CI 11/11 green).

Differential fuzzer. 120 randomly generated helper DAGs per channel — constant-decided branches, value-dependent "poison" branches, passthroughs, literal/propagated/derived constants, diamonds — each checked against an oracle that computes ground truth by construction (abstract interpretation over Known/Unknown constant states in the generator). Result across 1.10 / 1.12.6 / 1.13-rc1: 360/360 sound, zero false negatives, zero precision misses, deterministic — on active channels the analyzer exactly matched the oracle on every random shape.

Defect 9 (pre-existing, now fixed): user branches smuggled inside Base callable wrappers. hasbranching(relu ∘ layer, x) and hasbranching(Base.Fix2(cmp, t), x) reported branch-free: ComposedFunction/Fix delegate through Base-owned helper methods (the ∘ body immediately splat-forwards into its kwargs body Base.var"#_#54"), so the library-leaf boundary swallowed the wrapped user function — and relu ∘ layer is a perfectly plausible ODE RHS. Known wrappers (ComposedFunction, Base.Fix, pre-1.12 Fix1/Fix2) are now unwrapped structurally into component signatures routed through the normal call policy: user components are scanned, Base components (sin ∘ f) stay library leaves, entry and nested alike, on all versions (works gate-off on lts too). Seven regression tests cover the matrix.

Probed clean, no change needed: 5000-element constant-tuple splat through a user forwarder (~0.1s), a type used as the callable at the entry (conservative), constant rebinding picked up across queries.

State: suites 40/40 (lts) · 42/42 · 42/42; fuzzer sound on all channels; six adversarial batteries ≈ 80 cases/channel; MTK RHS table 6/6. Cumulative: 9 demonstrated defects found → fixed → regression-tested.