src/rules/laws/unsafe.bend
bolt@1.18.0.0 · 130 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.18.0.0/src/finding.bend as F
23import bolt@1.18.0.0/src/rules/digest.bend as Digest
24import bolt@1.18.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
45def reacher(rs: List<&2, Reach>, +pp: String) -> Maybe<&2, String>:
46 match rs:
47 case Nil{}:
48 None{}
49 case Con{Reach{origin, ps}, rest}:
50 +more = reacher(rest, pp)
51 Bool.pick(Maybe<&2, String>, Imports.has(ps, pp), Some{origin}, more)
52
53# what a def reached from a law file along the import path via is, and what
54# to do about it
55def say(foreign: Bool, +name: String, +origin: String, +via: String) -> String:
56 match foreign:
57 case True{}:
58 "foreign def " ++ name ++ " is reachable from " ++ origin ++ " (" ++ via
59 ++ "), 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."
60 case False{}:
61 "@unsafe def " ++ name ++ " is reachable from " ++ origin ++ " (" ++ via
62 ++ "), 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."
63
64# each unsafe or foreign def as a finding, at its `@unsafe` or its `def`,
65# reached from the law file along the import path via
66def report(us: List<&2, Digest.Unsafe>, +origin: String, +via: String, +path: String) -> List<&2, F.Finding>:
67 match us:
68 case Nil{}:
69 Nil{}
70 case Con{Digest.Unsafe{n, l, c, +fo}, rest}:
71 F.Finding{path, l, c, Bool.pick(U32, fo, 3, 7), "unsafe", say(fo, n, origin, via)} <> report(rest, origin, via, path)
72
73# the import path from the file at from to the file at to, both normalized,
74# as `a -> b -> c`
75def via(es: List<&2, Imports.Edge>, +read: List<&2, String>, +fuel: Nat, +from: String, +to: String) -> String:
76 String.join(Imports.trail(es, read, fuel, from, to), " -> ")
77
78# the unsafe and foreign defs of the file at norm, reached from the law file
79# at origin: the import path is looked for only when there is one
80def found.some(
81 us: List<&2, Digest.Unsafe>,
82 +origin: String,
83 +path: String,
84 +norm: String,
85 +es: List<&2, Imports.Edge>,
86 +read: List<&2, String>,
87 +fuel: Nat
88) -> List<&2, F.Finding>:
89 match us:
90 case Nil{}:
91 Nil{}
92 case Con{u, rest}:
93 report(u <> rest, origin, via(es, read, fuel, Imports.norm(origin), norm), path)
94
95# the unsafe and foreign defs of a file, when a law file reaches it
96def found(
97 mm: Maybe<&2, String>,
98 us: List<&2, Digest.Unsafe>,
99 +path: String,
100 +norm: String,
101 +es: List<&2, Imports.Edge>,
102 +read: List<&2, String>,
103 +fuel: Nat
104) -> List<&2, F.Finding>:
105 match mm:
106 case None{}:
107 Nil{}
108 case Some{origin}:
109 found.some(us, origin, path, norm, es, read, fuel)
110
111def check.go(
112 ds: List<&2, Digest.Digest>,
113 +rs: List<&2, Reach>,
114 +es: List<&2, Imports.Edge>,
115 +read: List<&2, String>,
116 +fuel: Nat
117) -> List<&2, F.Finding>:
118 match ds:
119 case Nil{}:
120 Nil{}
121 case Con{Digest.Digest{path, +norm, dir, is_laws, is_law_file, exempt, tops, says, deps, unsafes, laws}, rest}:
122 List.append(&2, F.Finding, found(reacher(rs, norm), unsafes, path, norm, es, read, fuel),
123 check.go(rest, rs, es, read, fuel))
124
125# the rule, over every file the linter read
126def check(+ds: List<&2, Digest.Digest>) -> List<&2, F.Finding>:
127 +es = Digest.edges(ds)
128 +read = Imports.paths(es)
129 +fuel = List.length(&2, Digest.Digest, ds)
130 check.go(ds, reaches(ds, es, read, fuel), es, read, fuel)