Cancellation in Doomformer's Plane Guards

Starting at 14,000 and adding 100 followed by -100 returns to 14,000. Doomformer's plane guard still reports a bound of 14,100, above its 14,018 limit. Cancellation in the final answer does not cancel the intermediate requirement.

That is a synthetic numeric replay, not a failed game execution. I ran the unchanged guard functions at revision 9d3acae475b6f3c2351ae7d1b6eb0c323796ffbd with Python 3.12.14 and NumPy 2.3.5 on Linux. ViZDoom was unavailable; I did not invoke ACC, compile a map, run a network in the engine, or reproduce the project's engine measurements.

The useful engineering detail is how the guard separates different obligations. Final values, accumulation order, move direction, and reset positions are distinct constraints. Its static interval analysis adds another conservative approximation on top.

An Integer Backend With Physical Constraints

Doomformer lowers integer neural networks into game-map mechanisms: threshold gates, moving floor or ceiling planes, and light accumulators. Python builds the map, supplies inputs, and compares readback with an integer reference. The repository includes a compiler, scheduling checks, quantization code, readback validation, engine probes, and tests. Its contribution is a concrete execution backend with explicit numeric contracts.

The package configuration declares version 0.7.1, Python >=3.11, and an exact ViZDoom 1.3.2 dependency. The toolkit implementation distinguishes agreement with its integer reference from agreement with an original floating-point model. Quantization can change the model before the game backend executes it.

My subject is the smaller planes.py guard. It imports the configured move speed and ceiling height from tile.py. The examined source computes:

PLANE_MAX = 32768 - 150000 // 8 = 14018
START_MIN = -15000
START_MAX = 16000

The source documents a fixed-point mover problem: beyond particular starting heights, a move can occupy the mover longer and cause a subsequent request to be dropped. Those engine observations belong to the project's probes and tests; my replay checks the guard's calculation, not the underlying engine claim.

Bound the Path, Not Just the Result

terms_peak() separates positive and negative terms. If their totals are P and N, the relevant directional endpoints are bias + P for a plane that rises and N - bias for one that falls. A direction with no corresponding terms contributes zero.

That treatment accounts for arbitrary crossing order. Positive terms may arrive before the negative terms that eventually cancel them. Checking only abs(bias + sum(terms)) would miss that excursion.

The replay returned:

Bias	Terms	Final sum	Guard bound	Move predicate rejects?	Start predicate rejects?
14,000	100, -100	14,000	14,100	Yes	No
14,000	10, 10, -10, -10	14,000	14,020	Yes	No
15,000	-2000	13,000	0	No	No
16,001	-2000	14,001	0	No	Yes

The third row is easy to misread. A bound of zero does not mean the plane has height zero. There is no raise to evaluate, and the lower moves away from the positive extreme. The directional endpoint measure contributes zero while the separate start-range predicate accepts 15,000.

The fourth row makes the separation necessary. Its decreasing move passes the move predicate, but its initial position exceeds the permitted reset range. A safe-looking final value cannot repair that initial condition.

These fixtures exercise helper predicates only. They are not claims that complete neural networks with those values satisfy every compiler constraint.

The Helper Is Conservative About Move Starts

The name and explanatory comments discuss where a move starts, but the guard uses the directional endpoint after all same-sign contributions. The source explicitly allows this conservative treatment.

For bias=14000 and terms [10, 10, -10, -10], I enumerated every ordering. The largest positive-direction move start was 14,010; the guard returned 14,020. Thus the guard rejected the fixture even though this enumeration's directional starts stayed below 14,018. That does not establish engine safety: timing, geometry, reset behavior, and other constraints were not simulated.

To check the calculation independently, the probe walked every permutation of four terms drawn from [-3, -1, 0, 1, 3], at seven biases. It recorded post-move endpoints by direction and compared them with the production helper. All 4,375 fixtures matched, with all 24 positional orderings evaluated for each fixture. Repeated terms produce duplicate orderings; this is a finite exhaustive check over the stated fixture space, not a proof for arbitrary arrays or integer sizes.

The edge predicates also behaved as written: 14,018 passed the move comparison; 14,019 failed it. Starts at -15,000 and 16,000 passed their separate range check; -15,001 and 16,001 failed.

Interval Analysis Can Lose Hidden Correlations

The same module's mlp_static_peaks() propagates activation intervals through hidden layers. It can reject a model before any particular input is supplied. The MLP caller exposes this as plane_errors(), while check(x) evaluates bounds for the activations produced by a supplied input.

I supplied a shape-only synthetic fixture with one signed input count, x ∈ {-1, 0, 1}. Its first hidden pair was ReLU-count(x) and ReLU-count(-x), each using threshold [1]. Each output ranges independently over [0,1], but both cannot be one for the same input.

The next hidden row had weights [255,255] and bias 13550. The interval calculation admitted both contributions simultaneously and reported 14,060. Exhausting all three input counts produced a maximum per-input guard bound of 13,805. The difference was 255, one impossible simultaneous contribution.

This is an observed limitation of interval precision. The fixture was passed directly to the guard's data interface and was not validated or compiled as a full model. It illustrates why a static rejection and a particular input's numeric result can disagree without either calculation being internally inconsistent.

Replay the Guard Boundary

The probe checks SHA-256 digests for six pinned source files. It bypasses the public package initializer with a namespace container, then imports the original modules normally. No guard or reference function is replaced. The imported ACC helper is never invoked.

With the source checkout at the pinned revision, run python plane-probe.py /path/to/doomformer-checkout. My actual cloud command was:

python public/blog/plane-bound-before-final-sum/plane-probe.py /tmp/doom-note31

It exited 0. Selected terminal output:

PLANE_MAX=14018; start=[-15000,16000]
ordered_endpoint_oracle: 4375 fixtures passed (all 24 orderings each)
correlated_hidden_fixture: static_h2=14060; exhaustive_input_peak=13805; inputs=3
bound_edges: 14018 accepted by move predicate; 14019 rejected; start edges checked
PASS: numeric guards only; no ViZDoom, ACC invocation, map compilation, or engine result

The project's plane tests also contain engine sweeps, repeated-pass reset checks, and comparisons with compiled models. I inspected them but did not run them. These local results support the guard arithmetic and its conservatism; they do not independently establish bit-exact game execution.

For this backend, a successful sum is only one piece of evidence. A compiler also has to bound the route to that sum and preserve a valid starting state for the next pass. Doomformer's separate predicates make those obligations inspectable, including the precision they give up to stay conservative.