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
45	def 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
55	def 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
66	def 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`
75	def 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
80	def 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
96	def 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	
111	def 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
126	def 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)