Laws depth (property ownership) — Bend s02

Humans own invariants in LAWS.bend. Agents fill PROOF.bend. Green covers stated laws only.

<!-- hal:authoritative:yaml -->

Name who owns the invariants. Name who owns the proofs. Treat a green proof as coverage of stated laws only, never as blanket product safety.

§I — Frame

Asr session 02 for Bend. Second live fire of the Bend experiment track. Week 1 fire 2. Home folder: . Primary live cite: https://bend-lang.com/. Vendor org: https://higherorderco.com/. On-disk hub (path for citations): .

Session 01 shipped the fail-closed gate: install, guide, one trivial law, deliberate break refuses, one named incompleteness gap. That folder stays closed for re-teaching install. A teammate §4 DoD remains the prior shape; this session does not walk the curl installer again.

Done-criteria: you can say which properties humans (or operators) own in LAWS.bend versus which proofs the agent fills in PROOF.bend; you can state that a green proof only covers stated laws.

Still experiment lane. Primary stack law stands: Rust + TypeScript for full-stack work; Python + Nix for ops and config. Bend does not join that daily clock.

§II — Two files, two owners

Vendor contract on bend-lang.com splits the surface:

1. LAWS.bend — declared invariants. Property ownership lives here.
2. PROOF.bend — proofs written to satisfy those laws.
3. Checker — bend PROOF.bend (or the documented check command of the day) verifies the stated laws only.

Musashi declarative: the law file is the contract; the proof file is the discharge; the checker is the refuse.

If you merge a green proof without reading the laws, you accepted a discharge you cannot name. That is still wrong even when CI is green.

§III — Property ownership (named technique: Law Own)

Yagyu names the cut once. Law Own: the human or operator authors the properties that must never break; the agent (or junior author) authors proofs that claim those properties hold.

Own in LAWS.bend:

• Game invariant: you_cant_win (no move sequence leads to victory).
• Sorted-output invariant: sorted_nondecreasing.
• Any host policy you actually wrote as a law (rare on day one; usually absent).

Do not pretend the agent owns those properties because it typed the proof. Typing a proof does not transfer ownership of the invariant. Ownership is authorship of the statement.

Own in PROOF.bend:

• The discharging argument the model (or you) writes.
• Tactic structure, lemmas, and rebuilds after a law edit.

If-then-thus: if the operator did not write the law, then a green proof only discharges whatever happened to be in the file, thus silent policy gaps remain free to rot.

§IV — Stated laws only (named technique: Cover Bound)

Cover Bound: a green PROOF.bend covers the properties written in LAWS.bend and nothing else.

Session 01 incompleteness list still applies as ownership gaps, not as a second install drill:

1. Host / OS — files, permissions, packaging, PATH, launchd, containers.
2. IO / network / secrets — TLS, sockets, wallets, API keys.
3. **@unsafe / FFI** — escape hatches outside the law surface.
4. Renderer / JS edge — UI side effects outside board laws.
5. Install / maturity friction — young toolchain; prove-on-spike.

Example: you_cant_win owns board victory. It does not own filesystem writes. A green proof of you_cant_win still allows a bad host write unless a separate law says otherwise.

§V — Worked ownership split (game law)

Vendor-shaped law (from bend-lang.com demo):

# LAW: no move sequence leads to victory.
law you_cant_win:
  for moves: List<Move>
  board = replay(start(), moves)
  is_won(board) == False{}

Ownership table for this spike:

Change the law without updating the proof: expect fail. Change the implementation so victory becomes possible: expect fail. Change nothing in laws and ship a host-side delete: checker may stay green. That third case is Cover Bound, not a toolchain mystery.

§VI — Why green-without-reading is still wrong

CI green means stated laws held under the checker’s current semantics. It does not mean:

• the laws match product intent,
• unstated security policy holds,
• primary-stack crates should adopt Bend,
• you can skip reading LAWS.bend before merge.

Review order for Hedronite spikes: read laws first, skim proof second, run checker third. Invert that order and you rubber-stamp a discharge of unknown properties.

§VIb — Operator vs agent in one sentence each

Operator sentence: I own every property written in LAWS.bend, including you_cant_win, and I own the decision that host/IO gaps stay unstated today.

Agent sentence: I own the text in PROOF.bend that claims those properties hold, and I do not own product policy that never appeared as a law.

Say both aloud before merge. If you cannot say the operator sentence, stop and open the law file.

§VII — Common mistakes

1. Treating proof authorship as property ownership.
2. Merging green proofs without opening LAWS.bend.
3. Re-running session 01 install steps as if ownership were an install lesson.
4. Claiming host/IO gaps are “covered” because the board law is green.
5. Reseating Rust/TS or Python/Nix clocks toward Bend after one green spike.

§VIII — Boundaries

• Not install tutorial (session 01 already).
• Not Lean tactics training.
• Not CUDA/Metal performance theater.
• Not curriculum clock reseat.
• Not Maghrib quiz×4 (Maghrib stays quiz×3 on the Dhuhr trio).

§IX — Close

Session 01 showed refuse. Session 02 assigns ownership: Law Own for invariants, Cover Bound for green proofs, incompleteness gaps remaining unowned until written. Next unmarked: session 03, incompleteness checklist drill.

Related:

Open yesterday’s LAWS.bend (or the vendor you_cant_win shape). Write one sentence naming the property owner and one sentence naming what the green proof does not cover, then stop.