bend PROOF.bend fails only when a law or its proof relies on unsafe or foreign code (#1463)

[viridale]

Fixes #1463.

Until now, bend PROOF.bend failed every law if any def in the import graph relied on unsafe or foreign code, for example an effect in the module that holds main. With this change, a PROOF.bend's claims are its own defs and its LAWS.bend's. A def outside them that relies on a promise is listed in a note, and the run passes:

$ bend PROOF.bend          # the issue's four files
ALL PROOFS CHECK
Note: 2 defs rely on unsafe or foreign code, but no law or proof does:
- main.tty
- main.main
Use --verdict for mathematical validity.
$ echo $?
0

A law still fails when its statement or proof relies on a promise, directly or through anything it names. The walk is the same book_promises flood as before; only the split into a failure and a note is new. An unsafe fill of a law counts too, because it sets u on the law's own def. Roots other than PROOF.bend keep #1001's rule: every def outside Base is a claim. The unsafe_* import tests are unchanged.

• bend2/main.ts: cli_verdict takes the root file and splits book_promises into the failure and the note. A new helper, relies, formats both lists. The failure text is byte-for-byte the same as before.
• bend2/safe.ts: safe_check takes the noted defs and lets them be out of the kernel's scope. Without this, --verdict would answer an unused @unsafe def with the MISMATCH message. Everything else it checks is unchanged.
• guide/GUIDE.md: the --verdict paragraph now says "every law and proof" instead of "every def outside Base".

Tests (a test runs its file as the root, so each PROOF.bend has its own directory):

• tests/proof/PROOF.bend: a law about a pure greet, beside an imported main that loops by an @unsafe def. It passes with the note. Before this change it failed and listed app/main.serve and app/main.main.
• tests/import/PROOF.bend: a false law, proved by an @unsafe def of the PROOF.bend's own. It still fails, listing the law and that def, but no longer the unrelated unsafe-law/safe.spin it also imports.
• Each LAWS.bend run alone is an open claim, which the test pins.

How I checked it, all locally:

• The proof, import and check suites, run as one gate shard does: 414 / 414.
• gates/repo.ts: 54 / 54.
• --verdict with the Lean kernel on both the issue's files and tests/proof/PROOF.bend: ALL PROOFS CHECK plus the note.
• Every demo's PROOF.bend: the four that failed (app_slash_boss_3d, io_http_server, io_tcp_echos, pure_hvm5_mini) now pass with a note. In each, the noted defs belong to the module that holds main, and no law names them. The others are unchanged.