src/rules/laws/unsafe.bend
bolt@1.24.0.0 · 138 lines · 0 definitions
1# rule unsafe (project-wide): an `@unsafe def` or a foreign def (its body
2# only `import "./x.c"` / `import "./x.js"` lines, what rule foreign reads)
3# that a LAWS.bend or PROOF.bend reaches by relative imports, over the files
4# bolt read. Since bend 2.0.32 a proof passes only when no def it loads,
5# imports included, is `@unsafe` or foreign or names one that is: every def
6# of every imported module counts, named by a law or not. Otherwise `bend`
7# prints `SOME PROOFS FAIL`, then `Error: N defs rely on unsafe or foreign
8# code:` and a `- name` list, and exits 1 (2.0.34; before 2.0.32 it printed
9# "All terms check, but ..." and exited 0). So the gate is red, and the
10# message names the defs that lean on the effect, not the import that
11# brought it in: this rule names that path, law file first. `@unsafe` skips
12# the termination check (a def that never returns proves anything): recurse
13# on a shrinking argument or on fuel, and drop it. A foreign effect is fine
14# in the program, never under a law: move it into a sibling module no law
15# file imports, and hand the laws' code the effect as a service record
16# (AGENTS.md; snap, ezhttp, bolt and ez were restructured that way). A def no
17# law file reaches is not this rule's business. Hash imports (`import
18# 0x.../path`, resolved through BEND_LIB) are not followed: bolt reads only
19# the files of the run. The rule reads each file's digest
20# (src/rules/digest.bend), and takes every closure over one import graph.
21import Base
22import bolt@1.24.0.0/src/finding.bend as F
23import bolt@1.24.0.0/src/rules/digest.bend as Digest
24import bolt@1.24.0.0/src/rules/imports.bend as Imports
25
26# a law file and what it reaches
27type Reach is Data:
28 Reach{origin: String, files: List<&2, String>}
29
30# every LAWS.bend and PROOF.bend with its closure over the graph
31def reaches(
32 ds: List<&2, Digest.Digest>,
33 +es: List<&2, Imports.Edge>,
34 +read: List<&2, String>,
35 +fuel: Nat
36) -> List<&2, Reach>:
37 match ds:
38 case Nil{}:
39 Nil{}
40 case Con{Digest.Digest{path, norm, dir, is_laws, is_law_file, exempt, tops, says, deps, unsafes, laws}, rest}:
41 +more = reaches(rest, es, read, fuel)
42 Bool.pick(List<&2, Reach>, is_law_file, Reach{path, Imports.closure.go(es, read, fuel, norm)} <> more, more)
43
44# the first law file that reaches the path; hit: the one before rs did, so
45# the search stops there
46def reacher.go(rs: List<&2, Reach>, +pp: String, hit: Maybe<&2, String>) -> Maybe<&2, String>:
47 match rs:
48 case Nil{}:
49 hit
50 case Con{Reach{origin, ps}, rest}:
51 match hit:
52 case Some{x}:
53 Some{x}
54 case None{}:
55 reacher.go(rest, pp, Bool.pick(Maybe<&2, String>, Imports.has(ps, pp), Some{origin}, None{}))
56
57# the first law file that reaches the path
58def reacher(rs: List<&2, Reach>, +pp: String) -> Maybe<&2, String>:
59 reacher.go(rs, pp, None{})
60
61# what a def reached from a law file along the import path via is, and what
62# to do about it
63def say(foreign: Bool, +name: String, +origin: String, +via: String) -> String:
64 match foreign:
65 case True{}:
66 "foreign def " ++ name ++ " is reachable from " ++ origin ++ " (" ++ via
67 ++ "), so bend fails that proof: SOME PROOFS FAIL, defs rely on unsafe or foreign code; move the effect into a sibling module no law file imports, and pass it in as a service."
68 case False{}:
69 "@unsafe def " ++ name ++ " is reachable from " ++ origin ++ " (" ++ via
70 ++ "), so bend fails that proof: SOME PROOFS FAIL, defs rely on unsafe or foreign code; recurse on a shrinking argument or on fuel and drop @unsafe, or move it into a sibling module no law file imports."
71
72# each unsafe or foreign def as a finding, at its `@unsafe` or its `def`,
73# reached from the law file along the import path via
74def report(us: List<&2, Digest.Unsafe>, +origin: String, +via: String, +path: String) -> List<&2, F.Finding>:
75 match us:
76 case Nil{}:
77 Nil{}
78 case Con{Digest.Unsafe{n, l, c, +fo}, rest}:
79 F.Finding{path, l, c, Bool.pick(U32, fo, 3, 7), "unsafe", say(fo, n, origin, via)} <> report(rest, origin, via, path)
80
81# the import path from the file at from to the file at to, both normalized,
82# as `a -> b -> c`
83def via(es: List<&2, Imports.Edge>, +read: List<&2, String>, +fuel: Nat, +from: String, +to: String) -> String:
84 String.join(Imports.trail(es, read, fuel, from, to), " -> ")
85
86# the unsafe and foreign defs of the file at norm, reached from the law file
87# at origin: the import path is looked for only when there is one
88def found.some(
89 us: List<&2, Digest.Unsafe>,
90 +origin: String,
91 +path: String,
92 +norm: String,
93 +es: List<&2, Imports.Edge>,
94 +read: List<&2, String>,
95 +fuel: Nat
96) -> List<&2, F.Finding>:
97 match us:
98 case Nil{}:
99 Nil{}
100 case Con{u, rest}:
101 report(u <> rest, origin, via(es, read, fuel, Imports.norm(origin), norm), path)
102
103# the unsafe and foreign defs of a file, when a law file reaches it
104def found(
105 mm: Maybe<&2, String>,
106 us: List<&2, Digest.Unsafe>,
107 +path: String,
108 +norm: String,
109 +es: List<&2, Imports.Edge>,
110 +read: List<&2, String>,
111 +fuel: Nat
112) -> List<&2, F.Finding>:
113 match mm:
114 case None{}:
115 Nil{}
116 case Some{origin}:
117 found.some(us, origin, path, norm, es, read, fuel)
118
119def check.go(
120 ds: List<&2, Digest.Digest>,
121 +rs: List<&2, Reach>,
122 +es: List<&2, Imports.Edge>,
123 +read: List<&2, String>,
124 +fuel: Nat
125) -> List<&2, F.Finding>:
126 match ds:
127 case Nil{}:
128 Nil{}
129 case Con{Digest.Digest{path, +norm, dir, is_laws, is_law_file, exempt, tops, says, deps, unsafes, laws}, rest}:
130 List.append(&2, F.Finding, found(reacher(rs, norm), unsafes, path, norm, es, read, fuel),
131 check.go(rest, rs, es, read, fuel))
132
133# the rule, over every file the linter read
134def check(+ds: List<&2, Digest.Digest>) -> List<&2, F.Finding>:
135 +es = Digest.edges(ds)
136 +read = Imports.paths(es)
137 +fuel = List.length(&2, Digest.Digest, ds)
138 check.go(ds, reaches(ds, es, read, fuel), es, read, fuel)