A second law, and the wall underneath

The previous chapter’s law compared two functions that both compute Life. This one compares two functions that both compute a string, and it is the more interesting of the two — because the thing being proved is not an optimisation detail, it is a constraint we discovered the hard way.

The setup

The animation’s renderer builds a frame backwards and reverses once at the end, because appending cell by cell in order would be O(frame²). Two levels are reversed in that one pass: the order of rows, and within a row the order of cells.

The law has to compare that against something. So the first job is to write the spec — the same frame, written the slow and obvious way, with no cleverness to get wrong:

def spec_row(+r: List<&2, Nat>) -> String:
  match r:
    case Nil{}:
      SNil{}
    case Con{h, t}:
      String.append(Anim.cell(h), spec_row(t))

def spec_rows(+rs: Anim.Rows) -> String:
  match rs:
    case Anim.RNil{}:
      SNil{}
    case Anim.RCons{r, t}:
      String.append(spec_row(r), String.append("\n", spec_rows(t)))

Two structural recursions, appended in order. Nobody would use this — it is quadratic — and that is exactly what makes it a good specification. It is obviously right.

Then the law is one line:

law frame_is_spec:
  for +rs: Anim.Rows
  {Anim.frame(rs) == String.append("\u{1B}[H", spec_rows(rs)) : String}

Fast renderer equals cursor-home escape followed by the slow renderer. This is the same shape as the previous chapter: implementation on the left, obvious specification on the right.

The palindrome constraint is a theorem

Look again at the comment in life_anim.bend:

every cell must be a palindrome. "██" and " " both are; change to "▐█" and every row flips internally (measured).

In the previous chapter that was a note in the source and a paragraph in the book. Here it is a lemma:

def pick_pal(b: Bool)
  -> {Bool.pick(String, b, "██", "  ") == String.reverse(Bool.pick(String, b, "██", "  ")) : String}:
  match b:
    case False{}:
      {==}
    case True{}:
      {==}

def cell_pal(v: Nat) -> {Anim.cell(v) == String.reverse(Anim.cell(v)) : String}:
  %pick_pal(Nat.is_eq(v, 1n)) : {Anim.cell(v) == _ : String}
  {==}

A cell is equal to its own character-reversal. The proof is two cases and both are {==}, because "██" and " " are each their own reverse — the checker just looks.

Note what this buys. Change cell to return "▐█" and cell_pal no longer holds, so frame_is_spec no longer goes through, and the program fails to prove. The constraint that was a comment for two chapters is now a compile-time obligation. It is not decoration: the break test at the end of this chapter changes exactly that one string and the gate closes.

Five of the seven lemmas are not about Life

Only two of the seven are about frames. The rest is standard library that does not exist yet, re-derived here because there was no import to reach for.

That is the honest cost of proving in Bend today, and it should be counted before choosing what to prove. The Bend README says its Lean formalisation lags the TypeScript implementation; this is what that looks like from the outside. It is not a flaw in the design — it is a young language whose lemma library has not been written.

Two things to know when writing the proofs

Accumulator functions need the accumulator spelled out. String.reverse is not a structural recursion — it calls reverse.go(s, acc). That means a goal containing reverse(x) for a variable x is stuck, and the invariant has to be generalised over the accumulator before induction will go through. Hence reverse_go_spec(s, +acc), and rowrev_spec(r, +acc), and inner(rs, +acc) which is the law generalised over the accumulator:

def inner(rs: Anim.Rows, +acc: String)
  -> {String.append(String.reverse(acc), Laws.spec_rows(rs)) == String.reverse(Anim.framerev(rs, acc)) : String}:

The law is then inner(rs, SNil{}) with the accumulator at empty, which is one line of proof.

Parameter modifiers follow use, not meaning. A parameter that appears only in the type gets -; one that is used more than once in the proof body needs +. reverse_go_spec’s acc looks erased — the type mentions it twice, which is why it is tempting to write -acc — but it appears in the recursive call, so it must be +acc. The rule is mechanical once you look at the body, and wrong every time you reason about it semantically.

Reading a failed proof

When a rewrite does not apply, the error prints expected and observed as fully unfolded terms. cellnext alone unfolds to thousands of characters, so the part that actually differs is somewhere in a wall of text. Measured, on a deliberately miscalled lemma:

The script in the directory folds those runs down to CELL:

bend LIFE_PAR_PROOF.bend 2>&1 | python3 elide_errors.py

This is a papercut rather than a language feature — the error is complete and correct, it is just rendered in a form no human can diff. Worth knowing before you spend an hour staring at one.

The break tests

Every one of these is a change to the implementation life_anim.bend:

The second entry is the one to look at twice. The bug that was found by eye, after it had already shipped into a working animation, is now caught at compile time — by a law whose proof takes 0.09 seconds.

That is the whole claim of this part of the book, and it is worth stating without inflation: the law does not make the renderer correct. It makes one specific property of it something you cannot break by accident and not notice.

Why we stopped here

The obvious next law was index safety for at() — “every index stays within 0 .. w*h”. It is a good law, it is the kind the Bend README advertises (array_set() may never be called out-of-bounds), and we did not write it.

Here is the wall. Both laws needed library lemmas that Base does not have. But the difficulty of the two taxes is not comparable:

The String lemmas were all structural: append matches on its first argument, so induction over that argument closes the proof. The arithmetic lemmas have to go through Nat.cmp, whose recursion compares two numbers and therefore needs induction over a pair. Same wall, two different heights — one is an afternoon, the other is not obviously finishable in one.

So the choice of which law to prove is not free, and it is not about how interesting the law is. It is about how far the lemma you need is from a structural recursion. Prefer laws whose proof obligation reduces to structural induction.

The law and its proof

# The law of the animated frame.
#
# `frame` builds the whole screen with ONE String.reverse at the end: rows are
# accumulated backwards (framerev), each row's *cells* backwards (rowrev), and
# the single char-level reverse undoes both at once. That is what makes it
# O(frame length) instead of O(n^2) with an append chain.
#
# The spec below is the same frame written the slow, obvious, append-heavy
# way. The law says the fast one equals it.
#
# The catch -- and the reason this law is not just a restatement -- is that
# the two levels disagree about what a "unit" is. rowrev reverses CELLS and
# leaves each cell's characters alone; String.reverse reverses CHARACTERS.
# Composing them gives
#
#     reverse (rowrev r) == map reverse (map cell r)
#
# so a row only comes out right if every cell is its own character-reversal,
# i.e. a palindrome. `cell` returns "██" or "  ", and both are. Change it to
# "▐█" and every row comes out mirrored -- measured, not reasoned: the 4x4
# glider renders as `OXOX][][` / `][][OX][` instead of `[]XO[][]` / `[][]XO[]`.
# That is the exact shape of the bug this repository already hit once.
#
# Written by hand, not by the AI. LIFE_ANIM_PROOF.bend proves it.
import Base
import ./life_anim.bend as Anim

# ---- the spec: what a frame should be, written the slow obvious way ----
def spec_row(+r: List<&2, Nat>) -> String:
  match r:
    case Nil{}:
      SNil{}
    case Con{h, t}:
      String.append(Anim.cell(h), spec_row(t))

def spec_rows(+rs: Anim.Rows) -> String:
  match rs:
    case Anim.RNil{}:
      SNil{}
    case Anim.RCons{r, t}:
      String.append(spec_row(r), String.append("\n", spec_rows(t)))

# LAW: the frame is the cursor-home escape, then the rows in order, each row's
# cells in order, each row followed by a newline.
law frame_is_spec:
  for +rs: Anim.Rows
  {Anim.frame(rs) == String.append("\u{1B}[H", spec_rows(rs)) : String}

# The proof of LIFE_ANIM_LAWS.bend's frame_is_spec.
#
# Same shape as LIFE_PAR_PROOF.bend: the goal is {impl == spec}, and every
# `%lem(args) : P` moves one side into the other's shape. P is the goal AFTER
# the rewrite, with `_` at the position the lemma's LEFT side was put in. So a
# lemma is written {target == what-is-there-now}: its right side is the form
# the goal currently holds, its left side is the form that replaces it.
#
# The first five lemmas are library gaps -- Base has no String lemmas at all.
import Base
import ./life_anim.bend as Anim
import ./LIFE_ANIM_LAWS.bend as Laws

# ---- library: append ----

# String.append matches on its FIRST argument, so append(a, SNil{}) is stuck
# when a is a variable. This is the only reason the lemma exists.
def append_nil2(a: String) -> {a == String.append(a, SNil{}) : String}:
  match a:
    case SNil{}:
      {==}
    case SCon{+h, +t}:
      %append_nil2(t) : {SCon{h, t} == SCon{h, _} : String}
      {==}

def append_assoc2(a: String, -b: String, -c: String)
  -> {String.append(a, String.append(b, c)) == String.append(String.append(a, b), c) : String}:
  match a:
    case SNil{}:
      {==}
    case SCon{+h, +t}:
      %append_assoc2(t, b, c) : {SCon{h, String.append(t, String.append(b, c))} == SCon{h, _} : String}
      {==}

# ---- library: reverse ----

# reverse.go carries an accumulator, so it is stuck on a variable. Its
# invariant: the reversed prefix comes first, then the accumulator.
def reverse_go_spec(s: String, +acc: String)
  -> {String.append(String.reverse(s), acc) == String.reverse.go(s, acc) : String}:
  match s:
    case SNil{}:
      {==}
    case SCon{+h, +t}:
      %reverse_go_spec(t, SCon{h, SNil{}}) : {String.append(_, acc) == String.reverse.go(t, SCon{h, acc}) : String}
      %append_assoc2(String.reverse(t), SCon{h, SNil{}}, acc) : {_ == String.reverse.go(t, SCon{h, acc}) : String}
      %reverse_go_spec(t, SCon{h, acc}) : {String.append(String.reverse(t), SCon{h, acc}) == _ : String}
      {==}

# reverse(append(a, b)) == append(reverse(b), reverse(a)).
def reverse_append2(a: String, +b: String)
  -> {String.append(String.reverse(b), String.reverse(a)) == String.reverse(String.append(a, b)) : String}:
  match a:
    case SNil{}:
      %append_nil2(String.reverse(b)) : {_ == String.reverse(b) : String}
      {==}
    case SCon{+h, +t}:
      %reverse_go_spec(t, SCon{h, SNil{}}) : {String.append(String.reverse(b), _) == String.reverse.go(String.append(t, b), SCon{h, SNil{}}) : String}
      %reverse_go_spec(String.append(t, b), SCon{h, SNil{}}) : {String.append(String.reverse(b), String.append(String.reverse(t), SCon{h, SNil{}})) == _ : String}
      %reverse_append2(t, b) : {String.append(String.reverse(b), String.append(String.reverse(t), SCon{h, SNil{}})) == String.append(_, SCon{h, SNil{}}) : String}
      %append_assoc2(String.reverse(b), String.reverse(t), SCon{h, SNil{}}) : {String.append(String.reverse(b), String.append(String.reverse(t), SCon{h, SNil{}})) == _ : String}
      {==}

# ---- library: cell ----

# WHY THIS LEMMA IS THE WHOLE POINT. rowrev reverses CELLS; String.reverse
# reverses CHARACTERS. A row survives the one-reverse trick only because each
# cell is restored by a character reversal, i.e. is a palindrome.
def pick_pal(b: Bool)
  -> {Bool.pick(String, b, "██", "  ") == String.reverse(Bool.pick(String, b, "██", "  ")) : String}:
  match b:
    case False{}:
      {==}
    case True{}:
      {==}

def cell_pal(v: Nat) -> {Anim.cell(v) == String.reverse(Anim.cell(v)) : String}:
  %pick_pal(Nat.is_eq(v, 1n)) : {Anim.cell(v) == _ : String}
  {==}

# ---- the row ----

# reverse(rowrev(r, acc)) is the row's cells in order, then the reversed acc.
# Inducting on r needs the accumulator spelled out, hence the -acc.
def rowrev_spec(r: List<&2, Nat>, +acc: String)
  -> {String.append(String.reverse(acc), Laws.spec_row(r)) == String.reverse(Anim.rowrev(r, acc)) : String}:
  match r:
    case Nil{}:
      %append_nil2(String.reverse(acc)) : {_ == String.reverse(acc) : String}
      {==}
    case Con{+h, +t}:
      %rowrev_spec(t, String.append(Anim.cell(h), acc)) : {String.append(String.reverse(acc), String.append(Anim.cell(h), Laws.spec_row(t))) == _ : String}
      %reverse_append2(Anim.cell(h), acc) : {String.append(String.reverse(acc), String.append(Anim.cell(h), Laws.spec_row(t))) == String.append(_, Laws.spec_row(t)) : String}
      %cell_pal(h) : {String.append(String.reverse(acc), String.append(Anim.cell(h), Laws.spec_row(t))) == String.append(String.append(String.reverse(acc), _), Laws.spec_row(t)) : String}
      %append_assoc2(String.reverse(acc), Anim.cell(h), Laws.spec_row(t)) : {String.append(String.reverse(acc), String.append(Anim.cell(h), Laws.spec_row(t))) == _ : String}
      {==}

# ---- the frame ----

# The accumulator invariant over Rows: reverse(framerev(rs, acc)) is the
# reversed acc, then the spec's frame. At acc = SNil that is exactly the law.
def inner(rs: Anim.Rows, +acc: String)
  -> {String.append(String.reverse(acc), Laws.spec_rows(rs)) == String.reverse(Anim.framerev(rs, acc)) : String}:
  match rs:
    case Anim.RNil{}:
      %append_nil2(String.reverse(acc)) : {_ == String.reverse(acc) : String}
      {==}
    case Anim.RCons{+r, +t}:
      %inner(t, String.append("\n", String.append(Anim.rowrev(r, SNil{}), acc))) : {String.append(String.reverse(acc), String.append(Laws.spec_row(r), String.append("\n", Laws.spec_rows(t)))) == _ : String}
      %reverse_append2("\n", String.append(Anim.rowrev(r, SNil{}), acc)) : {String.append(String.reverse(acc), String.append(Laws.spec_row(r), String.append("\n", Laws.spec_rows(t)))) == String.append(_, Laws.spec_rows(t)) : String}
      %reverse_append2(Anim.rowrev(r, SNil{}), acc) : {String.append(String.reverse(acc), String.append(Laws.spec_row(r), String.append("\n", Laws.spec_rows(t)))) == String.append(String.append(_, "\n"), Laws.spec_rows(t)) : String}
      %rowrev_spec(r, SNil{}) : {String.append(String.reverse(acc), String.append(Laws.spec_row(r), String.append("\n", Laws.spec_rows(t)))) == String.append(String.append(String.append(String.reverse(acc), _), "\n"), Laws.spec_rows(t)) : String}
      %append_assoc2(String.reverse(acc), Laws.spec_row(r), "\n") : {String.append(String.reverse(acc), String.append(Laws.spec_row(r), String.append("\n", Laws.spec_rows(t)))) == String.append(_, Laws.spec_rows(t)) : String}
      %append_assoc2(String.reverse(acc), String.append(Laws.spec_row(r), "\n"), Laws.spec_rows(t)) : {String.append(String.reverse(acc), String.append(Laws.spec_row(r), String.append("\n", Laws.spec_rows(t)))) == _ : String}
      %append_assoc2(Laws.spec_row(r), "\n", Laws.spec_rows(t)) : {String.append(String.reverse(acc), String.append(Laws.spec_row(r), String.append("\n", Laws.spec_rows(t)))) == String.append(String.reverse(acc), _) : String}
      {==}

# ---- the law ----

def Laws.frame_is_spec(rs):
  %inner(rs, SNil{}) : {String.append("\u{1B}[H", _) == String.append("\u{1B}[H", Laws.spec_rows(rs)) : String}
  {==}