Hedronite Lesson · Polyglot-Dev / Bend · Wed 2026-09-30 · T8

Encode one new rust-tops clause as a fail-closed law — Bend s08

Pick a Forbidden clause absent from NAMES. Write Refuse. Break Allow on purpose.

Lesson Class: Asr (Bend T8 Verification & AI ops)

Focus: Clause Pick · Law Shape · Deliberate Break · mutants_skip_needs_reason

Done-criteria: one new law; deliberate break; gate fails closed; lesson only no push

Grounding: AGENTS.md Forbidden · LAWS.bend Verdict pattern · NAMES absence · BEND2 sketch

Note: Experiment lane · not spike bank · not musl body · not primary stack · no repo push

Clause Pick

#[mutants::skip] without reason; absent from NAMES (53).

Law Shape

MutantsSkip → Refuse on SkipNoReason; parallel evidence_not_self_served.

Deliberate Break

Allow on SkipNoReason opens the gate; keep Refuse.

Quote the Forbidden bullet. Keep the teaching law in the lesson. Do not push NAMES.

Write one law for a clause not yet in the catalog. Break it on purpose. Show Refuse.

§I. Frame

Asr session 08 for Bend. Topic T8 Verification & AI ops. Eighth live fire; third rust-tops encode row. Home: . Corpus: ~/projects/rust-tops/AGENTS.md, laws/LAWS.bend, laws/NAMES (vault mirror under foundry/rust-tops/repo/rust-tops/). Protocol: ·

Session 06 read the triad. Session 07 named Catalog Emit and the names-only floor. Today the unmarked row asks you to encode one new clause as a fail-closed law: pick something absent from NAMES, write the Bend shape, break it deliberately, and show Refuse.

Host reminder: Bend CLI work stays on tower or Bot-VM only. This lesson authors the law in the lesson file. Do not push edits to rust-tops. Do not run gen-laws.rs to insert the name. Do not weaken an existing catalog law.

Done-criteria: write one law for a clause not yet in the catalog, break it deliberately, and show the gate fails closed. Lesson only; no push to the rust-tops repo.

§II. Clause Pick (named technique)

Clause Pick: Forbidden text that NAMES does not already cover.

laws/NAMES has 53 lines (H-01..H-53 harvest). Grep shows no mutants_skip name. AGENTS.md Forbidden states, quoted:

#[mutants::skip] without an equivalent-mutant reason.

BEND2-INTEGRATION.md already sketches the duty under Mutation on diff: refuse unexplained survivors; #[mutants::skip] needs equivalent-mutant reason. That sketch is not yet a catalog law. Closest existing names (baseline_green_before_mutants, mutant_kill_without_scar) cover baseline skip and scar-split kills, not skip-without-reason.

Teaching name: mutants_skip_needs_reason.

Yagyu: quote the Forbidden bullet. Musashi: one absent clause, one snake_name.

§III. Law Shape (named technique)

Law Shape: copy the Verdict / Refuse pattern from an existing law. Parallel: evidence_not_self_served in LAWS.bend.

type Verdict is Data:
  Refuse{}
  Ack{}
  Allow{}

type MutantsSkip is Data:
  SkipNoReason{}
  SkipWithReason{}

def mutants_skip_verdict(x: MutantsSkip) -> Verdict:
  match x:
    case SkipNoReason{}:
      Refuse{}
    case SkipWithReason{}:
      Allow{}

law mutants_skip_needs_reason:
  {mutants_skip_verdict(SkipNoReason{}) == Refuse{} : Verdict}

def mutants_skip_needs_reason():
  {==}

Read the parallel in the corpus:

law evidence_not_self_served:
  {evidence_verdict(FromImpl{}) == Refuse{} : Verdict}

Same skeleton: bad ctor → Refuse{}; good ctor → Allow{}; law pins the bad ctor to Refuse. SkipWithReason{} means a tight-scope skip plus an equivalent-mutant reason (RUST_TOPS §8.3). SkipNoReason{} is the Forbidden bare skip.

This block lives in the lesson. It is not appended to laws/LAWS.bend today.

§IV. Deliberate Break (named technique)

Deliberate Break: show Ack/Allow temptation vs Refuse on the bad path.

Path	Input	Verdict	Meaning
Fail closed	`SkipNoReason{}`	`Refuse{}`	bare `#[mutants::skip]` — Forbidden
Pass	`SkipWithReason{}`	`Allow{}`	skip + equivalent-mutant reason
False green (break)	treat `SkipNoReason{}` as `Allow{}`	wrong	gate opened; lesson failed

Deliberate break for study: rewrite the match so SkipNoReason{} returns Allow{} (or change the law to assert Allow). The proof obligation then no longer encodes the Forbidden clause. Fail closed means that rewrite is rejected: the law must keep SkipNoReason{} == Refuse{}.

Ack{} exists on Verdict in the catalog import. Do not use Ack as a soft pass for Forbidden skips. This teaching law stays binary for the bad ctor: Refuse or you opened the gate.

On a Bend host (tower / Bot-VM), the drill is: install → trivial law green → flip the bad ctor to Allow → proof/law check fails. On vault-only lab Mac, the drill is the table above plus the corpus parallel. Do not claim a mesh PATH bend run from this Mac lesson.

Chozanshi: if the skip has no equivalent-mutant reason, then Verdict is Refuse; thus the agent may not wrap the function to silence survivors.

§V. Why this encode seat

Bend2 at Asr exists so AI ops can turn protocol Forbidden lines into fail-closed laws before they land in the generator. Session 06/07 stay honest about the catalog that already ships. Session 08 practices the encode move on a real gap (mutants_skip_needs_reason) without polluting NAMES from class.

RUST_TOPS section 8.3 already states when a survivor is explained: equivalent mutant, one-line reason, tight-scope #[mutants::skip] with that same reason. The teaching law does not reimplement cargo mutants. It refuses the skip that lacks the reason. Halos still run the tool; Bend refuses progress that skips required evidence (BEND2 encode rule of thumb).

When this clause graduates for real, a human runs Catalog Emit (session 07) on host and lands it through gen-laws.rs. That is a product change. This lesson stops at the teaching law.

§VI. Done-criteria check

Say aloud without looking:

Clause Pick: Forbidden #[mutants::skip] without reason; absent from NAMES (53).
Law Shape: MutantsSkip / mutants_skip_verdict / law mutants_skip_needs_reason pinning Refuse.
Deliberate Break: Allow on SkipNoReason{} opens the gate; keep Refuse.
Lesson boundary: no push, no hand-edit of LAWS.bend, no fake NAMES insert.

§VII. Common mistakes

Picking a clause already in NAMES (e.g. re-teaching baseline_green_before_mutants).
Pushing the teaching law into rust-tops from Asr.
Editing LAWS.bend by hand instead of later Catalog Emit.
Confusing names-only floor parity with proof of this new law.
Treating Nix musl cross (peer today) as the encode seat.
Scoring success by inventing Halo apply from this lesson.

§VIII. Boundaries

Not Catalog Emit / regenerate re-teach as the whole lesson (session 07).
Not spike bank review (session 09).
Not Halo mutants/CRAP grind on product code.
Not Maghrib quiz×4.
Not mesh PATH Bend on the lab Mac.
Not Nix static musl body (Asr Nix #18 peer).
Not primary-stack adoption of Bend.

§IX. Close

Session 07 named emit and floor gate. Session 08 encodes mutants_skip_needs_reason from AGENTS.md Forbidden, parallel to evidence_not_self_served, with a deliberate Allow-break that must Refuse. Next unmarked: session 09, spike bank review against laws from #6 to #8.

Related: ·

Quote the Forbidden bullet. Keep the teaching law in the lesson. Stop.