Skip to content

Wave Loop 576 — the document recording these proofs was itself unchecked evidence #1998

Description

@gHashTag

☣️ [VERDICT]

Wave 575 found one published claim written from a comment rather than a run. That made the implicit claim behind all 26 propositions — their reproduction blocks work — the least-tested thing in the repository, and the one everything else stands on. This wave tested it.

14 of 19 shell blocks were transcripts

class count what it is
runnable 3 a command a reader can run
template 2 contains <placeholders>
transcript 14 a result, formatted identically to a command

A ```bash fence reads as "run this". Fourteen were showing output. Same failure shape this campaign keeps finding — a form that reads as stronger evidence than it is — this time in its own documentation. All fourteen are now ```text.

Both blocks a reader could actually run were broken

The two runnable blocks added in waves 574 and 575 both begin:

t27c gen-bitnet-bundle --output-dir build/rtl

which t27c returns nothing — the binary is at ./target/release/t27c. Prop. 3's own lesson 6 states that evidence citing a command that does not exist is not weak evidence, it is not evidence. Both blocks were written after that lesson was recorded, in the same file, by the same author, and neither was ever executed.

A rule with no gate is a preference.

All 27 propositions now name their gate

Mapped mechanically — identifiers each proposition cites, matched against the workflows and formal/*.sv. Six matched nothing and were checked by hand rather than declared ungated, which is how four false negatives of my own heuristic were caught (it could not see prose probe labels like 'DMA can start').

One proposition has no gate, and now says so: Prop. 5 measured sv2v behaviour; CI does not install sv2v. Correctly historical rather than standing.

Enforced going forward: CI fails if a proposition lacks a **Gate:** line, if a ```bash block calls bare t27c, or if a ```bash block contains no command at all.

What this does not establish: that each gate is sufficient for its claim. Prop. 4's gate counts conformance files without measuring vector sufficiency, and says so.

27 propositions · 27 gates · every bash block verified to execute · 1208 passed, 0 failed · seals 496/496. Details: docs/FORMAL_FOUNDATIONS.md Prop. 27.


Three variants for the next wave

A — Gate adequacy, claim by claim. Prop. 27c establishes every claim has a check; it does not establish the check is sufficient. Prop. 4's gate counts files without measuring vector sufficiency — how many others are like that? For each proposition, break its gate deliberately and confirm the proposition's own claim goes red. That is the vacuity oracle (Prop. 12a) applied to the gate map instead of to properties.

B — Sweep the maximum-sized request. Still unexecuted from wave 575, and still where the arithmetic lives: num_chunks is 8 bits with a num_chunks-1 terminator, and beats_owed = (bytes_remaining + 7) >> 3 can overflow. Zero was one end of every range; nothing has tested the other.

C — Close Prop. 25 with a per-buffer written-flag. The one open RTL defect. Cheaper now than at any prior point: the baseline gate catches a regression on the first run instead of the fourth, which is exactly what cost wave 574 three withdrawn attempts.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions