fix(avgpool2d): preserve pooling semantics end to end

[Kaijie-liu]

A soundness bug.

ACT previously dropped ceil_mode, count_include_pad, and divisor_override during PyTorch-to-ACT conversion. For an AvgPool2d layer using these semantics, ACT could therefore analyze a different linear operator from the source PyTorch/ONNX model. A proof about that different operator is not a sound proof about the original model.

There was also an internal inconsistency in the interval transformer: bounds were computed using PyTorch's default count_include_pad=True, while W_equiv divided by the number of valid input elements. For example, with a 3x3 input, kernel=2, stride=2, padding=1, and only the top-left input equal to 1:

• PyTorch/include-pad output: 1 / 4 = 0.25
• old W_equiv output: 1 / 1 = 1.0

One qualification: the current canonical constraint exporter does not lower the avgpool2d: equality tag and fails loudly instead. Therefore, we have not observed a false certificate caused specifically by that equality matrix. The confirmed soundness issue is the loss/inconsistent handling of source-model pooling semantics across the supported propagation paths.

When is it triggered?

The old implementation is affected by:

• padding > 0 together with count_include_pad semantics;
• ceil_mode=True when it adds a trailing pooling window;
• a non-None divisor_override;
• non-square kernel/stride/padding in the Dual backward path, which previously kept only the first tuple component.

The common configuration

padding=0, ceil_mode=False, divisor_override=None

does not expose the bug because every pooling window contains exactly the full kernel area.

Why did the previous CI runs not detect it?

The existing layer_testing_cnn_pool fixture used only:

kernel=2, stride=2, padding=0

For that case, the buggy and correct denominator formulas are identical. The code was executed, but the semantic branch that exposes the bug was not exercised.

There were two additional masking factors:

1. PyTorch-to-ACT and ACT-to-PyTorch both omitted the same pooling parameters, so a reconstructed model could repeat the same semantic loss instead of acting as an independent oracle.
2. Line coverage only shows that AvgPool code ran; it cannot distinguish padding=0 from the affected padded/ceil/divisor cases.

Influence on HyZor forzen results

We also scanned the evaluated models. Among the 475 unique models in the frozen 2213-instance suite, only the cGAN model contains AveragePool, and all ten nodes use padding=0. A scan of all 661 VNN-COMP 2025 models found no semantically affected AveragePool node. Therefore, there is no evidence that this bug changed the frozen experimental results.

Fix in this PR

This PR makes the pooling semantics explicit and consistent end to end:

1. Preserve ceil_mode, count_include_pad, and divisor_override through PyTorch-to-ACT and ACT-to-PyTorch conversion.
2. Use shared output-shape and per-window-divisor calculations matching PyTorch semantics.
3. Apply the same parameters in Interval bounds and W_equiv.
4. Align HybridZ propagation with the source operator.
5. Align Dual forward and exact transpose propagation, including non-square parameters.
6. Extend the existing pooling fixture, without adding a separate test function, to cover:
   • padded include-pad with ceil_mode=True;
   • padded exclude-pad;
   • non-square pooling parameters.

[codecov]

Codecov Report

❌ Patch coverage is 94.05941% with 6 lines in your changes missing coverage. Please review.
✅ Project coverage is 73.77%. Comparing base (09c3c6c) to head (eb2b0ba).

Files with missing lines	Patch %	Lines
act/back_end/utils.py	90.90%	4 Missing ⚠️
act/back_end/dual_tf/tf_cnn.py	94.73%	1 Missing ⚠️
act/pipeline/verification/torch2act.py	90.00%	1 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##             main     #100      +/-   ##
==========================================
+ Coverage   73.53%   73.77%   +0.24%     
==========================================
  Files          91       91              
  Lines       20372    20444      +72     
==========================================
+ Hits        14980    15083     +103     
+ Misses       5392     5361      -31     

Flag	Coverage Δ
bab	50.22% <56.43%> (+0.23%)	⬆️
backend-float32	49.44% <86.13%> (+0.11%)	⬆️
backend-float64	49.47% <86.13%> (+0.10%)	⬆️
frontend	32.98% <30.69%> (-0.01%)	⬇️
pipeline-fuzz	20.58% <7.92%> (-0.05%)	⬇️
pipeline-verify	39.45% <12.87%> (-0.10%)	⬇️

Flags with carried forward coverage won't be shown. Click here to find out more.

Files with missing lines	Coverage Δ
act/back_end/dual_tf/tf_forward.py	82.52% <100.00%> (+0.15%)	⬆️
act/back_end/hybridz_tf/tf_cnn.py	91.12% <100.00%> (+0.10%)	⬆️
act/back_end/interval_tf/tf_cnn.py	84.38% <100.00%> (+0.07%)	⬆️
act/back_end/layer_schema.py	100.00% <ø> (ø)
act/back_end/net_factory.py	86.70% <ø> (ø)
act/pipeline/verification/act2torch.py	73.90% <100.00%> (+0.18%)	⬆️
act/back_end/dual_tf/tf_cnn.py	86.15% <94.73%> (-0.02%)	⬇️
act/pipeline/verification/torch2act.py	75.01% <90.00%> (+0.15%)	⬆️
act/back_end/utils.py	82.23% <90.90%> (+3.53%)	⬆️

... and 5 files with indirect coverage changes

---

Continue to review full report in Codecov by Harness.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 09c3c6c...eb2b0ba. Read the comment docs.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

[Kaijie-liu]

a scan of all 613 ONNX models in HyZor 12 evaluated datasets found zero affected AveragePool nodes, so this PR doesn't changes benchmark result. It's a correctness fix, not a ranking score fix. ACT claims general PyTorch/ONNX support, but before this change, a perfectly legal padded AvgPool would silently yield a self-contradictory constraint.