[Montana]

Fixes #1306.

Stacked on #1291. #1306 is blocked by #1291, and this branch is built on it. Until #1291 merges, this PR also shows #1291's commits. Only the last commit, cb0b874, is this PR's. Unlike #1315 and #1316, it adds no row to CHECKS, and it merges cleanly with both.

What it adds

A generator, a shrinker, and a runner that joins them. The differential checks run fixed models, so they are oracles only over the expressions those models hold. This turns the harness from checking models into searching for bugs.

• parity_checks/differential/_generate.py

  • generate(seed, fmt) draws a network of 2–4 species and 1–4 reactions whose laws are random trees over the grammar bngsim accepts:

    • arithmetic and powers;
    • exp/log/ln/log10/log2/sqrt;
    • abs/floor/ceil/round/rint/trunc/sign;
    • tanh/sin/cos/atan/erf;
    • min/max/avg/clamp;
    • if() on every comparison and on &&/||;
    • the clock;
    • and in SBML, piecewise and rateOf (of a driver species, so no law reads its own species' rate).

    It renders the model as a .net (functional rate laws) or as SBML (libsbml, parseL3Formula). A seed is its model.

  • Laws stay finite by construction, so a finding is a disagreement, not a domain error, as the issue asks:

    • logs and roots read 1 + x², powers have bases of at least 1, and quotients are guarded;
    • each law enters its reaction as k·g²/(1 + g²), which is bounded but still reads every node of g.

    The guards are squares, not abs(). bngsim declines the analytic sensitivity RHS for abs() under a call, and an abs() guard in every law kept the sensitivity checks off the analytic path in a first draft. abs is in the grammar as itself.

  • shrink(model, holds) delta-debugs: it drops reactions, then replaces each subexpression by one of its children or a constant, for as long as holds still holds. A finding's holds is "the same check gives the same status, and for an exception the same class".

• parity_checks/differential/differential_generate.py runs the seeds, each in its own process under a wall cap and a step budget (20,000, a fifth of the corpus's; a law that switches on the clock and on rateOf can crawl). It runs each model through check_all, shrinks each DIFF or EXCEPTION, and writes out every reproducer beside a JSON note. A model whose base does not run is not a finding.

First run

Seeds 0–199 in both formats: 400 models, 430 s on 8 workers locally. 389 ran, 3 had no base, 8 timed out, and there were 2 findings:

check	over 389 models
ajac_vs_fdjac, klu_vs_dense, cc_vs_interp, sparsity_covers_jacobian, backend_as_asked	all pass
sens_runs / sens_vs_plain	158 pass; 231 refused by name (laws with floor, ceil, if on the clock…)
cc_vs_mir	skip (this build has no MIR)
grid	2 diff

Both findings are genuine, judged against converged runs:

1. net seed 72, shrunk from size 20 to 10: one reaction, f1 = k1·g²/(1+g²) with g = floor(O1 + O1) − (round(O2) − O1).

   rtol	21 points vs converged	161 points vs converged
   1e-6	2.0e-6	3.4e-6
   1e-8	4.4e-8	4.9e-5
   1e-10	2.1e-9	3.4e-10

   At rtol 1e-8, asking for 8× the output points moves the answer by a thousand times the tolerance.

2. net seed 174, shrunk from size 35 to 13: two reactions, reading trunc(O2) as O2 slides up to 1 (0.99999991 at t = 10), and if(time() > 1, O1, …).

   • At rtol 1e-8, 161 points are 8.4e-3 off the converged answer, against 3.1e-8 for 21.
   • Its rtol 1e-12 run fails (CV_CONV_FAILURE at t = 8.5) on 21 points, and runs on 161.

Both are switches on the state, crossed or stepped over depending on where the output stops fall: the class #907, #1192 and #926 track. They are filed as one issue with both reproducers, for a maintainer to judge whether they are new or existing cases: #1342.

Tests (python/tests/test_differential_shapes.py, appended)

test	what it holds
test_a_seed_is_its_model	a seed renders the same model twice; two seeds differ
test_every_grammar_entry_is_one_bngsim_reads[fmt-op]	each spelling, alone in a law with a negative first argument, loads and integrates finitely (65 cases: every entry in each format it has a spelling in)
test_generated_models_load_and_stay_finite[fmt]	12 seeds per format stay finite on the window
test_the_shrinker_cuts_down_to_what_still_finds	for a predicate "has a floor()", the shrinker keeps one reaction of size ≤ 3
test_a_planted_defect_is_found_and_shrunk_to_a_reproducer	with cc_vs_interp made to read DIFF on any model containing rint(, investigate reports it and shrinks it to a one-reaction reproducer that still has the rint(
test_no_finding_is_reported_where_every_check_passes	the negative

Mutations, each caught:

• a shrinker that cuts nothing (two tests fail);
• DIFF not counted as a finding;
• an unguarded log;
• an unguarded sqrt.

The grammar test originally fed every entry positive inputs and missed the last two. Its first argument is now negative.

Suites: test_differential_shapes.py and test_differential_run.py give 239 passed, 1 xfailed. ruff 0.14.0 is clean. The branch merges cleanly with lanl main, #1315 and #1316.

Also: parity_checks/differential/.gitignore ignores runs/, where both this runner and differential_run.py write by default, as amici_parity/.gitignore does for its own.

CI notes

• Fixed: the first push failed every Python and MIR shard on the suite's skip audit. The grammar test skipped the nine .net-only entries under SBML with an undeclared reason. It is now parametrized over spelled entries only (second commit).
• Not this PR: AMICI forward-sensitivity parity failed on a wall-time alert alone. Its outcomes match the baseline exactly (82/10/2/2), and its work counters are identical (n_steps, n_rhs_evals, n_jac_evals all at ratio 1.0), but wall time was 2.15x on the same CPU model. This PR changes no engine code, and the same job passed on amici_sens: judge each sensitivity parameter on its own scale (#1261) #1303, differential: the analytic Jacobian's values against differences of the RHS (#1308) #1315 and differential: metamorphic transforms of the model file (#1305) #1316. A rerun should clear it; I don't have the rights to trigger one.

Nightly

The issue allows "nightly or on demand", and this is on demand. A run is reproducible from its seeds, and the first one took about 7 minutes. Two things would make a nightly job worth adding, as a follow-up:

• a fixed seed range;
• a baseline of its known findings.

That is why no differential.json baseline is re-recorded here: the runner adds no row to the nightly report.

Usage

python parity_checks/differential/differential_generate.py \
    --seeds 0:200 --formats net,sbml --out runs/generated.json --repro-dir runs/reproducers

No changelog fragment: this changes parity_checks/ and tests only.