Wave Loop 575 — zero-sized-request sweep: a 2–2 policy split, and a retraction

[gHashTag]

☣️ [VERDICT]

Retraction first

Wave 574 claimed a zero-length DMA "reaches DONE without ever asserting dma_local_we, satisfying its completion contract while writing nothing". That is false.

The emitted guard was IDLE: if (start && (length != 32'd0)), and done is asserted only in DONE_ST. A zero-length request never left IDLE — it was silently dropped, which is strictly worse than completing vacuously. The claim was written from the comment sitting directly above that line, which read "A zero-length request moves no data and completes immediately": true of the intent, false of the code.

A generated file's comments are not evidence about the generated file. The standing rule is verify the artifact, not the source — a comment inside the artifact is still source.

The same table also reported two failures that were really one. dma_done is declared at line 262 and was read at line 125, so that interlock was wired to an undriven twin exactly as row 2 was, and had no effect at all.

The sweep

Rather than find this shape a fourth time by accident, formal/zero_size_props.sv measures every module that takes a count and reports completion.

module	count	verdict	policy
layer_sequencer	num_neurons	refutes	completes
weight_prefetch_ctrl	num_words	refutes	completes
multilayer_sequencer	num_layers	PROVES	dropped — host hangs
dma_controller	length	PROVES	dropped — host hangs

A 2–2 split. Neither policy is wrong alone; four modules disagreeing is the defect, because a host cannot know which to expect.

The dropping half is the dangerous half. A dropped request produces no work, no completion and no error — the one outcome a host cannot observe. The CSR write is accepted, nothing happens, and the IRQ never arrives. Both droppers now complete.

Completing must not mean pretending. Four no-work properties added, all proving. The CI gate has inverted polarity: every *_never_completes must REFUTE and every no-work property must PROVE. The first half alone permits a module that lies; the second alone permits one that hangs.

Baseline proves · 20 integration properties prove · 6 liveness witnesses as expected · Prop. 25 still gated open · 1208 passed, 0 failed · seals 496/496. Details: docs/FORMAL_FOUNDATIONS.md Prop. 26.

---

Three variants for the next wave

A — Sweep the other universal shape: the maximum-sized request. Zero was one end of every count's range; the other end is untested. num_chunks is 8 bits and chunk_id == num_chunks-1 is the terminator — what happens at 255? length is 32 bits and beats_owed = (bytes_remaining + 7) >> 3 can overflow. Same sweep method, opposite end, and boundary arithmetic is where the last three RTL defects lived.

B — Close Prop. 25 with a per-buffer written-flag. Still the one open defect. A single global bit is the wrong shape; the property asks whether the buffer being read was written. Now cheaper than last wave: the baseline gate catches a regression on the first run instead of the fourth.

C — Audit the other direction of the retraction. One wrong claim was found because a sweep happened to touch it. Prop. 25c is unlikely to be the only claim in FORMAL_FOUNDATIONS.md written from a comment or an assumption rather than a run. Re-execute every Reproduce: block in the document and mark each proposition verified-today or stale. The campaign's credibility rests on those blocks actually working.