bend PROOF.bend fails over foreign defs that no law depends on #1463

What Bend should do

bend PROOF.bend should fail only when a law's statement or proof relies on unsafe or foreign code. Other unsafe or foreign defs that happen to be in the import graph should be listed as a note, not turned into a failure.

Today, one foreign def anywhere in the graph fails every law. With the four files below, the only law is about core.greet, a pure function:

$ bend PROOF.bend
SOME PROOFS FAIL
Error: 2 defs rely on unsafe or foreign code:
- main.tty
- main.main
$ echo $?
1

Neither listed def is used by the law. Remove import ./main.bend as M from LAWS.bend and PROOF.bend, and the same law passes (ALL PROOFS CHECK, exit 0). tty.c doesn't need to exist for the check.

# core.bend
import Base

def greet(name: String) -> String:
  "hi " ++ name

# main.bend
import Base
import ./core.bend as C

def tty(fd: U32) -> IO(U32):
  import "./tty.c"

def main() -> IO(Unit):
  do IO<Unit>:
    t : U32 <- tty(1)
    IO.print(C.greet(U32.show(t)))

# LAWS.bend
import Base
import ./core.bend as C
import ./main.bend as M

law greets:
  {C.greet("x") == "hi x" : String}

# PROOF.bend
import Base
import ./core.bend as C
import ./main.bend as M
import ./LAWS.bend as Laws

def Laws.greets():
  {==}

Why

A program's laws usually import its modules, including the one that holds main. demos/io_hello_world/LAWS.bend does import ./main.bend as Hello. As soon as main uses a single foreign effect, for example isatty, which Base doesn't have, every law about the program fails, however pure the law is.

The only workaround is to split each program into a pure module, which the laws import, and a main module, which they must never import, even indirectly. Nothing enforces that rule except the failure itself.

This keeps what #776 and #966 asked for: a non-zero exit when a law rests on unchecked code. It only stops failing over code that sits next to the laws without being used by them.

bend 2.0.36 · Darwin arm64