~/bend-docscommunity

src/rules/laws/unsafe.bend checks

raw source on the hub · import 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/laws/unsafe.bend as Unsafe

rule unsafe (project-wide): an @unsafe def or a foreign def (its body only import "./x.c" / import "./x.js" lines, what rule foreign reads) that a LAWS.bend or PROOF.bend reaches by relative imports, over the files bolt read. Since bend 2.0.32 a proof passes only when no def it loads, imports included, is @unsafe or foreign or names one that is: every def of every imported module counts, named by a law or not. Otherwise bend prints SOME PROOFS FAIL, then Error: N defs rely on unsafe or foreign code: and a - name list, and exits 1 (2.0.34; before 2.0.32 it printed "All terms check, but ..." and exited 0). So the gate is red, and the message names the defs that lean on the effect, not the import that brought it in: this rule names that path, law file first. @unsafe skips the termination check (a def that never returns proves anything): recurse on a shrinking argument or on fuel, and drop it. A foreign effect is fine in the program, never under a law: move it into a sibling module no law file imports, and hand the laws' code the effect as a service record (AGENTS.md; snap, ezhttp, bolt and ez were restructured that way). A def no law file reaches is not this rule's business. Hash imports (import 0x.../path, resolved through BEND_LIB) are not followed: bolt reads only the files of the run. The rule reads each file's digest (src/rules/digest.bend), and takes every closure over one import graph.

4 imports
import Base
import ../../finding.bend as F
import ../digest.bend as Digest
import ../imports.bend as Imports

Types

type Reach source · line 27 · raw

Data

a law file and what it reaches

Definitions

def reaches source · line 31 · raw

@ds:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Digest> -> @+es:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/imports.Edge> -> @+read:List<&2, String> -> @+fuel:Nat -> List<&2, Reach>

every LAWS.bend and PROOF.bend with its closure over the graph

def reacher source · line 45 · raw

@rs:List<&2, Reach> -> @+pp:String -> Maybe<&2, String>

the first law file that reaches the path

def say source · line 55 · raw

@foreign:Bool -> @+name:String -> @+origin:String -> @+via:String -> String

what a def reached from a law file along the import path via is, and what to do about it

def report source · line 66 · raw

@us:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Unsafe> -> @+origin:String -> @+via:String -> @+path:String -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

each unsafe or foreign def as a finding, at its @unsafe or its def, reached from the law file along the import path via

def via source · line 75 · raw

@es:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/imports.Edge> -> @+read:List<&2, String> -> @+fuel:Nat -> @+from:String -> @+to:String -> String

the import path from the file at from to the file at to, both normalized, as a -> b -> c

def found.some source · line 80 · raw

@us:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Unsafe> -> @+origin:String -> @+path:String -> @+norm:String -> @+es:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/imports.Edge> -> @+read:List<&2, String> -> @+fuel:Nat -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

the unsafe and foreign defs of the file at norm, reached from the law file at origin: the import path is looked for only when there is one

def found source · line 96 · raw

@mm:Maybe<&2, String> -> @us:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Unsafe> -> @+path:String -> @+norm:String -> @+es:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/imports.Edge> -> @+read:List<&2, String> -> @+fuel:Nat -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

the unsafe and foreign defs of a file, when a law file reaches it

def check.go source · line 111 · raw

@ds:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Digest> -> @+rs:List<&2, Reach> -> @+es:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/imports.Edge> -> @+read:List<&2, String> -> @+fuel:Nat -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

def check source · line 126 · raw

@+ds:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Digest> -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

the rule, over every file the linter read