refactor(back_end): retire 13 uncollected self-tests behind two CI gates - #113
Merged
Conversation
bab.py carried 14 self-tests behind a hand-rolled `__main__` runner and
onnx_converter.py one stray `test_onnx_conversion`. Per-test coverage
attribution (each test run alone, import-only baseline subtracted, then
differenced against a 27-case e2e union built by expanding every loop
axis in act-bab.yml) showed which of them still protect anything.
Deleted -- zero residual coverage, no assertion the e2e union lacks:
test_imports, test_random_branching, test_random_bounding
Deleted -- assertion is vacuous or unreachable from production:
_test_bab_kbatch_status_parity: k=1/2/4/8 all end at nodes=32,
exhausted_budget_nodes=True. The statuses agree because the budget
ran out, not because K-batching preserves results.
test_split_subproblems: the fixture leaves incremental_alpha, eta,
split_signs and parent_margins as None, so `_clone_dict_tensors`
only ever takes its `is not None` short-circuit. Degrading the clone
to an alias would not fail this test.
test_config_yaml_roundtrip: BaBConfig.from_yaml/to_yaml have no
production caller -- BaB config is built via BaBConfig(**merged) at
config.py:606/790/861. The test was keeping dead code alive.
test_random_branching_with_mask: nothing in production passes
unstable_mask to compute_scores (bab.py:1952 passes bounds_dict and
nu_per_layer, :1964 passes none; branching.py:91 is a docstring), so
RandomBranching's neuron-split branch is unreachable.
test_subproblem_batch, test_babnode_compat: accessor smoke tests.
Migrated to CI, then deleted:
_test_bab_budget_exhaustion_returns_unknown -> "BaB soundness --
budget exhaustion returns UNKNOWN". Same two assertions against a
real torchlp solver on mlp_plain_3x8, which unlike bab_deep survives
presolve and enters BaB. Every other step in this workflow asserts
throughput; this is the first to assert the verifier does not claim
more than it proved.
_test_bab_oom_fails_loud -> an inline AST check in act-bab.yml. A
real OOM cannot be raised deterministically in CI, so the invariant
is now checked structurally: no try/except may wrap
setup_and_solve_batch or solve_batch. This covers every call site rather than the single
path the fixture reached, and guards against the
`except (ValueError, RuntimeError, ...): return None` idiom already
present at bab.py:289 spreading to the solve path. An ast-grep rule
was rejected first -- its `$$$` form missed the case where the
assignment is the last statement in the try block.
Not migrated: _test_bab_k_fluctuates asserts a performance property,
not a soundness one, and K-batch width is not exposed in metadata.
`_k_log` itself is kept: it is documented diagnostic API.
Kept: _test_check_violations_batched_per_kind and its scalar-params
sibling. Adding --bab to the range/margin/unsafe netfactory run absorbs
only 7 of their 33 residual lines; the other 26 are broadcast shapes
((1,width), (n_batch,width), batched d) that real nets never emit. Both
recompute the expected mask independently via argmax/einsum and compare
with torch.equal, so a broadcasting bug surfaces as a failed assert
rather than a silently wrong CERTIFIED.
codecov project target 74% -> 75%: deleting test_onnx_conversion drops
41 uncovered statements; the `__main__` blocks and pragma'd self-tests
were already outside the denominator, so nothing else moves.
Pure deletion in both modules (0 insertions), plus five test-only
imports (os, tempfile, BabNode, split_subproblems, RandomBranching)
dropped alongside their last callers. bab.py self-tests: 2 passed.
The inline gate was exercised by parsing the workflow and running the
extracted shell: green on bab.py and verifier.py, red on a positive
control that includes the case where the guarded call is the last
statement in the try block. lsp clean; act.back_end.bab exports unchanged.
Codecov Report❌ Patch coverage is Additional details and impacted files@@ Coverage Diff @@
## main #113 +/- ##
==========================================
- Coverage 74.97% 74.61% -0.36%
==========================================
Files 91 91
Lines 22230 22323 +93
==========================================
- Hits 16666 16657 -9
- Misses 5564 5666 +102
Flags with carried forward coverage won't be shown. Click here to find out more.
... and 14 files with indirect coverage changes Continue to review full report in Codecov by Harness.
🚀 New features to boost your workflow:
|
Two embedded self-test batteries are removed from production modules. cons_exportor's 18 are replaced by a torchlp sweep over the 59 layer_testing nets. verifier.py's 16 are dropped outright; that file was 63% test scaffolding (1363 of 2153 lines) and is now production code only. Neither dtype job runs a self-test step any more. Retiring them exposed that the gate meant to cover those paths was not actually a gate. per_neuron_bounds' check_hookable_alignment() treated hookable_layers == 0 as "aligned" rather than "nothing to verify", so a net whose kinds were all absent from _ACT_KIND_TO_MODULE ran with no hooks, checked no neurons, and printed "All 0 checks passed". 120 of 222 validation runs were green ticks over zero work. Zero-check runs are now SKIPPED and excluded from the pass tally, and the smooth activations plus the 1:1 transformer ops are mapped and emitted as real modules so their bounds are actually checked. Pre- versus post-activation is decided from the ACT layer kind rather than the traced module name, matching DualSolver's compute_forward_bounds( post_activation=False) contract: nonlinear relaxations store the incoming box, affine, shape, pooling and bilinear handlers store the outgoing one. Module names are a tracing detail and never defined which tensor a bound represented; deriving it from them compared cos(x) against the box for x and produced 87 false violations in float32. Verified by shrinking tf_sin's interval 10% toward its midpoint: the gate previously exited 0 with 0 violations, and now reports the SIN neuron violation and exits 1. Both dtypes report 0 violations across 132 checked runs with 0 zero-check runs. The solve-path exception gate is also simplified to a comprehension over Try nodes, verified to still flag both guarded call sites.
Collaborator
|
Need to fix CI coverage |
Measured +164 repo-wide executed lines in 3 seconds over the 9,085-line combined baseline of the existing pipeline-verify commands.
Conflict was in act-pipeline-verify.yml: upstream folded a hybridz combo into the vit_2023 loop, which supersedes the standalone hybridz ViT step added here. Upstream's form is kept because it also runs --validate-soundness; the standalone step is dropped as a duplicate run.
No generated network contained ATT_SCORES or ATT_MIX, and dual_tf's forward_attention/backward_attention handle only those two kinds, so the backend jobs' existing dual sweep could never reach them. MATMUL already had cover via layer_testing_matmul; the attention cores had none. layer_testing_attention lowers DENSE Q/K/V into ATT_SCORES -> CONCAT -> SOFTMAX -> ATT_MIX -> CONCAT -> LAYERNORM -> GELU. Q/K/V come from DENSE rather than an MHA_SPLIT decomposition because the dual path stubs MHA split/join and consumes the bilinear cores directly. dual_tf/tf_transformer.py goes from 72.07% to 90.4% (36 missing, was 69). Both dtypes report 0 violations and the tf_sin unsoundness probe is still caught. Picked up by the existing sweep with no workflow change.
Commit the generated attention network and manifest entry omitted from b3d3d9d. Dual-transformer coverage moved from 271/376 to 340/376 executable lines, a +69-line delta, and both dtypes complete with zero soundness violations.
Contributor
Author
To date, we deleted self-contained functional test cases, (at least) change to netfactory-composed ACT net to test. |
It was named a soundness gate but only ever flagged one syntactic shape: try/except wrapped directly around setup_and_solve_batch or solve_batch. An exception swallowed inside solve_batch's own body, or in a caller of verify_once, is equally fatal and invisible to it. It never fired, and the shape it guards is one review catches. Twenty-five lines of inline YAML Python for that is not worth carrying.
_dot_product_degenerate is documented as the closed-form box product for when there is no perturbation dimension, but both callers guarded it with dim_in == 1 rather than dim_in == 0. Since dim_in is embed_dim * perturbed_words, dim_in == 1 is one genuinely perturbed coordinate, and the helper zeroes lw/uw and multiplies only the bias terms, discarding the lw . x^r contribution entirely. Reproduction: for z1 = 2x and z2 = 3x over x in [-1, 1], dot_product returned [0, 0] while the true range of 6x^2 is [0, 6] -- the abstract bound excluded most of the reachable set. Routing dim_in == 1 through _dot_product_planes yields [-18, 6], looser but sound. Not reachable from any current end-to-end path, since attn_mode is never set in production, but it would have become a false-CERTIFIED source the moment the dual-planar route was wired up.
c56b7e4 committed layer_testing_attention.json and the manifest into act/back_end/examples/nets, which .gitignore excludes because every net there is a build product of `act.back_end --generate`. The definition already lives in act/config/gen_act_net.yaml. Tracking a generated file also disables .gitignore for it, so a later DSL edit would silently leave the committed copy stale while CI ran the regenerated one. Verified by wiping act/back_end/examples/nets entirely: --generate rebuilds all 75 nets including the attention one, byte-identical, and the dual sweep still picks it up with no --networks flag (0 violations).
32e8f0d replaced cons_exportor's self-tests with a torchlp sweep over the layer_testing nets but only wired it into the float64 job, and the verifier self-test step was later removed from both. float32 was left with neither, so nothing there exercised the LP export path. Measured locally at float32: 60 nets, 0 failures, 246s, comparable to the float64 sweep.
yuleisui
reviewed
Aug 31, 2026
Comment on lines
+234
to
+256
| # =================================================================== | ||
| # Soundness gate: a BaB run that exhausts its node budget with unproven | ||
| # sub-boxes left in the pool MUST report UNKNOWN, never CERTIFIED. Every | ||
| # other step here asserts throughput (node counts, exit codes); this is | ||
| # the only one asserting the verifier does not claim more than it proved. | ||
| # | ||
| # layer_testing_bab_deep is certified by presolve and never branches, so | ||
| # it cannot exhaust anything -- mlp_plain_3x8 is the net that survives | ||
| # presolve and enters BaB. --verbose is load-bearing: backend_cli only | ||
| # prints result.metadata under it. | ||
| # =================================================================== | ||
| - name: BaB soundness — budget exhaustion returns UNKNOWN | ||
| run: | | ||
| cd ${{ github.workspace }} | ||
| out=$(coverage run -p -m act.back_end --verify \ | ||
| --network "$ACT_NETS_DIR/mlp_plain_3x8_64x64_3962224133.json" \ | ||
| --bab --bab-max-depth 10 --bab-max-subproblems 2 --bab-max-batch-size 1 \ | ||
| --solver torchlp --device cpu --dtype float64 --verbose 2>&1) | ||
| echo "$out" | ||
| grep -q "Lane 0: VerifyStatus.UNKNOWN" <<<"$out" | ||
| grep -q "reason: budget_exhausted_with_unproven_subboxes" <<<"$out" | ||
| grep -q "exhausted_budget_nodes: True" <<<"$out" | ||
|
|
Collaborator
There was a problem hiding this comment.
this looks to be auto generated for debugging.
Contributor
Author
There was a problem hiding this comment.
yes. Now deleted.
Comment on lines
-64
to
-67
| run: | | ||
| cd ${{ github.workspace }} | ||
| coverage run -p -m act.back_end.verifier | ||
|
|
Collaborator
There was a problem hiding this comment.
be consistent with float64.yml
| @@ -0,0 +1,85 @@ | |||
| { | |||
Collaborator
There was a problem hiding this comment.
Could we remove this file as we have other json files as nets.
Collaborator
There was a problem hiding this comment.
Could you merge this into gen_act_net.yaml where necessary.
| @@ -0,0 +1,815 @@ | |||
| { | |||
Collaborator
There was a problem hiding this comment.
Need to be auto generated rather than manually added.
Refer to gen_act_net.yaml
bab.py is production code only now, matching verifier.py. The two check_violations_batched tests, the _TESTS list and the module entry point are gone, so the workflow step that ran the module goes with them, as does the budget-exhaustion gate. What this gives up, measured rather than assumed: stubbing check_violations_batched to always report "no violation" degrades a falsifiable net from FALSIFIED to UNKNOWN, and no remaining check notices -- the netfactory counterexample validation passes because it exercises verify_once, not BaB's counterexample path. Every net CI currently runs through BaB already returns UNKNOWN, so the violation-found branch has no end-to-end cover. Restoring it needs a generated net that BaB actually falsifies, plus a step asserting FALSIFIED.
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
2 participants
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.
Deleted self contained functional test cases.
codecov project target 74% -> 75%: