bend-laws

When proving changed behavior or maintaining verification, read the Poteto adaptation.

A law is an acceptance criterion that a proof must meet for every input. Bend checks the proofs against a reference model of the rule. A table generated from that model ties the shipped code to the laws.

Fit

Use laws for rules that decide money, access, or safety and are finite or integer arithmetic: modes, permissions, statuses, thresholds, time windows, rounding. Route strings, parsers, JSON, floats (Bend's F32 is axiomatic and there is no F64), and UI to property tests (fast-check, rapid) instead; proving them costs more than it catches.

Ownership

Workflow

1. Read the shipped rule and its tests. List every input and the decision it returns. Done when the input domain is enumerated (finite) or its boundaries are named.
2. Draft the laws in a scratch directory as LAWS_draft.bend (import paths allow only letters, digits, _ and -), and prove them there. Give each law one plain-English comment. Done when the human has reviewed the draft and committed it as LAWS.bend.
   • Call only the functions under test. Define every helper a law uses inside LAWS.bend, so the model cannot weaken a law by redefining its vocabulary.
   • State what must hold. Anything a law leaves open is whatever the model does, so pair each prohibition ("never runs X") with the requirement ("runs only what declares Y").
   • Write imported constructors qualified and braced: case P.Yes{}:. A bare case Yes: on an imported type binds every value and the law passes vacuously (bendlang/bend#1328); check.sh and the hook reject it.
3. Model the rule in policy.bend, mirroring the shipped code's branch order, and prove each law in PROOF.bend as def Laws.<law>(...). Done when bend PROOF.bend prints ALL PROOFS CHECK.
4. Mutate the model once per law: change a branch the law guards and confirm bend PROOF.bend prints SOME PROOFS FAIL at that law; then revert. Done when every law has rejected a mutant. A law no mutant fails is vacuous.
5. Write oracle.bend, whose main prints the # @generated header and one <inputs> <decision> line per input, then run laws/check.sh --write.
6. Compare the shipped code: a unit test parses decisions.txt and asserts the shipped function returns every row. For a finite domain, also assert each input appears once, with the domain derived from the code's types so a new value breaks the build. For an unbounded domain, generate inputs with property tests, seed the law boundaries, and compare against the model compiled with bend -o model.mjs. Done when a mutant in the shipped code fails the test.
7. Copy templates/install-bend.sh and templates/check.sh into laws/, then add a required CI job that runs both. Add CODEOWNERS for laws/**/LAWS.bend and laws/**/decisions.txt. Done when the job fails on a missing LAWS.bend and passes once it lands.

To change a rule: the human edits the law, the agent updates the model and proofs, runs check.sh --write, then changes the shipped code until its unit test matches. Review every decisions.txt diff as a behavior change.

Before writing Bend, run bend guide; read REFERENCE.md for the syntax traps, proof patterns, --verdict setup and upgrades.

Guardrails

• Propose law changes to the human; never edit LAWS.bend or work around the hook.
• Keep @unsafe, def f? and foreign code out of law directories: they switch off the soundness a proof relies on. Bend's gate and check.sh both reject them.
• Keep the Bend version pinned in install-bend.sh; upgrade deliberately and re-prove.
• Keep source on the machine: sending code to BendAI or publishing to the Bend hub needs explicit approval.