[Lorenzobattistela]

Closes #1463.

A file checked as proofs (--verdict, or a file with no main) still fails when any def outside Base relies on unsafe or foreign code, including defs it imports but never uses. That rule doesn't change. What changes is the error: when none of those defs is a law or a def of the checked file, no law or proof uses them, and the error now ends with a hint that names them:

SOME PROOFS FAIL
Error: 2 defs rely on unsafe or foreign code:
defs that depend on @unsafe: app/main.serve, app/main.main
Hint: no law or proof uses these defs. Move them to a file this proof does not import, and the proofs will check: app/main.serve, app/main.main

The rule is the same for every file. There's no special case for PROOF.bend. Laws are now marked when parsed (Def.l), so a law filled by unsafe code in an imported file doesn't get the hint (unsafe_law_fill, unsafe_law_own, unsafe_law_derived stay as they were).

Tests: tests/proof/PROOF.bend (hint) and tests/import/PROOF.bend (a law relies on unsafe, no hint) come from #1472, with expectations updated. unsafe_unused and unsafe_law_unused now show the hint.

Gates on top of main 15a336c: repo 54/54, test 1630/1630, perf 124/124, ping 58/58, safe 1643 files with 0 !/t/e, exit 0. Not run: Linux, Windows, CUDA.