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.
21	import Base
22	import ../../finding.bend as F
23	import ../digest.bend as Digest
24	import ../imports.bend as Imports
25	
26	# a law file and what it reaches
27	type 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
31	def 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
46	def 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
58	def 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
63	def 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
74	def 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`
83	def 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
88	def 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
104	def 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	
119	def 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
134	def 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)