src/rules/laws/trace.bend
bolt@1.19.0.0 · 416 lines · 0 definitions
1# rule trace (project-wide, opt-in): SPEC.md and the laws agree. SPEC.md,
2# read from the directory bolt runs in, lists requirements in tables whose
3# header is exactly `| ID | Requirement | Level | Status | Law |`, and trust
4# rows in tables headed `| ID | Assumption | Why it is trusted |`. An ID is
5# uppercase letters and digits in two or more segments joined by `-`
6# (`BOLT-CFG-1`); a law proves one when a line of its comment block is exactly
7# that ID (`# BOLT-CFG-1`). A Proved row, proved or pending, is a claim: a
8# proved row's Law cell names the laws that prove it, and a pending row's may
9# name laws that prove part of it while the row stays pending. The findings: a
10# row that is not a well-formed requirement or trust row, an ID that does not
11# match the pattern included; an ID listed twice; a proved row whose Law cell
12# names no law; a Trusted row that names a law; a Law entry of a Proved row,
13# proved or pending, whose law is missing, has no `for`/`exs` binder, or lacks
14# the row's tag; a Trusted row with no trust row; and a tag
15# naming an ID SPEC.md does not list as Proved, proved or pending. A Law entry
16# is `<path> <law>`, the path relative to SPEC.md, entries joined by `; `.
17# Only a bolt.bend that names the rule turns it on (src/config.bend). It runs
18# only when bolt lints the whole tree, never over files named on the line.
19import Base
20import bolt@1.19.0.0/src/finding.bend as F
21import bolt@1.19.0.0/src/rules/digest.bend as Digest
22import bolt@1.19.0.0/src/rules/imports.bend as Imports
23import bolt@1.19.0.0/src/lazy/lazy.bend as Lazy
24import bolt@1.19.0.0/src/rchars.bend as Rchars
25
26# reading SPEC.md
27# ---------------
28
29# one requirement row: its ID, level and status, the Law cell's entries, and
30# its line (0-based)
31type Row is Data:
32 Row{id: String, level: String, status: String, laws: List<&2, String>, line: U32}
33
34# an ID, or a reason, at a line
35type Mark is Data:
36 Mark{id: String, line: U32}
37
38# which table the lines are in; Head is the header row, whose `| :-- |` line
39# comes next
40type Mode is Data:
41 Out{}
42 ReqHead{}
43 Reqs{}
44 TrustHead{}
45 Trusts{}
46
47# what SPEC.md says: the requirement rows, the trust rows, the rows that are
48# not well formed (why, where), each list in reverse file order while read
49type Spec is Data:
50 Spec{mode: Mode, reqs: List<&2, Row>, trust: List<&2, Mark>, bad: List<&2, Mark>}
51
52# the requirement table's header
53def req_head() -> String:
54 "| ID | Requirement | Level | Status | Law |"
55
56# the trust table's header
57def trust_head() -> String:
58 "| ID | Assumption | Why it is trusted |"
59
60# a cell's text, spaces trimmed
61def trim(+ss: String) -> String:
62 String.trim(ss)
63
64# a table line read so far: the cell being read and the cells before it, each
65# backwards
66type Cells is Data:
67 Cells{cur: List<&2, Char>, done: List<&2, String>}
68
69# one char onto the cells read: a bar ends the cell, any other char extends it
70def cells.at(bar: Bool, cc: Char, st: Cells) -> Cells:
71 match bar:
72 case True{}:
73 Cells{cur, done} = st
74 Cells{[], trim(Rchars.text(cur)) <> done}
75 case False{}:
76 Cells{cur, done} = st
77 Cells{cc <> cur, done}
78
79# the cells of a table line, split at every `|` that does not follow a `\`
80# (an escaped `\|`); esc says the char before was a `\`. It matches no char
81# pattern, so the proofs can take a char apart by what Char.is_eq says of it
82def cells.go(cs: List<&2, Char>, esc: Bool, st: Cells) -> List<&2, String>:
83 match cs:
84 case Nil{}:
85 Cells{cur, done} = st
86 List.reverse(&2, String, Rchars.text(cur) <> done)
87 case Con{+c, t}:
88 cells.go(t, Char.is_eq(c, '\\'), cells.at(Bool.and(Char.is_eq(c, '|'), Bool.not(esc)), c, st))
89
90# the cells between a line's outer bars
91def cells(+line: String) -> List<&2, String>:
92 +all = cells.go(String.to_list(String.trim(line)), False{}, Cells{[], []})
93 List.take(&2, String, List.drop(&2, String, all, 1n), Nat.sub(List.length(&2, String, all), 2n))
94
95# the i-th cell, or empty
96def cell(+cs: List<&2, String>, ii: Nat) -> String:
97 Maybe.default(&2, String, List.get(&2, String, cs, ii), "")
98
99def entries.go(ss: List<&2, String>) -> List<&2, String>:
100 match ss:
101 case Nil{}:
102 Nil{}
103 case Con{+s, rest}:
104 +more = entries.go(rest)
105 Bool.pick(List<&2, String>, String.is_empty(trim(s)), more, trim(s) <> more)
106
107# a Law cell's entries
108def entries(ss: String) -> List<&2, String>:
109 entries.go(String.split(ss, ';'))
110
111# a requirement row onto the spec, or a malformed one
112def add_req(+line: String, +nn: U32, st: Spec) -> Spec:
113 Spec{+mode, +reqs, +trust, +bad} = st
114 +cs = cells(line)
115 Lazy.stop(Spec, Bool.not(Nat.is_eq(List.length(&2, String, cs), 5n)),
116 Spec{mode, reqs, trust, Mark{"a requirement row must have five cells", nn} <> bad},
117 _u => Spec{mode, Row{cell(cs, 0n), cell(cs, 2n), cell(cs, 3n), entries(cell(cs, 4n)), nn} <> reqs, trust, bad})
118
119# a trust row onto the spec, or a malformed one
120def add_trust(+line: String, +nn: U32, st: Spec) -> Spec:
121 Spec{+mode, +reqs, +trust, +bad} = st
122 +cs = cells(line)
123 Bool.pick(Spec, Nat.is_eq(List.length(&2, String, cs), 3n),
124 Spec{mode, reqs, Mark{cell(cs, 0n), nn} <> trust, bad},
125 Spec{mode, reqs, trust, Mark{"a trust row must have three cells", nn} <> bad})
126
127# the spec in another mode
128def moved(st: Spec, mm: Mode) -> Spec:
129 Spec{mode, reqs, trust, bad} = st
130 Spec{mm, reqs, trust, bad}
131
132# a line inside a table: the header's `| :-- |` line, a row, or the end
133def in_table(mode: Mode, +line: String, +nn: U32, st: Spec) -> Spec:
134 match mode:
135 case Out{}:
136 st
137 case ReqHead{}:
138 moved(st, Reqs{})
139 case Reqs{}:
140 add_req(line, nn, st)
141 case TrustHead{}:
142 moved(st, Trusts{})
143 case Trusts{}:
144 add_trust(line, nn, st)
145
146# the mode a spec is in
147def mode_of(st: Spec) -> Mode:
148 Spec{mode, reqs, trust, bad} = st
149 mode
150
151# one line of SPEC.md onto what it says
152def step(+line: String, +nn: U32, +st: Spec) -> Spec:
153 +tt = String.trim(line)
154 Bool.pick(Spec, String.eq(tt, req_head()), moved(st, ReqHead{}),
155 Bool.pick(Spec, String.eq(tt, trust_head()), moved(st, TrustHead{}),
156 Lazy.stop(Spec, Bool.not(String.starts_with(tt, "|")), moved(st, Out{}),
157 _u => in_table(mode_of(st), tt, nn, st))))
158
159def parse.go(ls: List<&2, String>, +nn: U32, st: Spec) -> Spec:
160 match ls:
161 case Nil{}:
162 st
163 case Con{l, rest}:
164 parse.go(rest, (nn + 1 : U32), step(l, nn, st))
165
166# what SPEC.md's text says
167def parse(text: String) -> Spec:
168 parse.go(String.lines(text), 0, Spec{Out{}, [], [], []})
169
170# IDs
171# ---
172
173# is the char an uppercase letter or a digit?
174def id_char(cc: Char) -> Bool:
175 +u = Char.to_u32(cc)
176 Bool.or(Bool.and(U32.is_ge(u, 65), U32.is_le(u, 90)), Bool.and(U32.is_ge(u, 48), U32.is_le(u, 57)))
177
178# is every char an uppercase letter or a digit?
179def id_chars(cs: List<&2, Char>) -> Bool:
180 match cs:
181 case Nil{}:
182 True{}
183 case Con{c, rest}:
184 Lazy.and_then(id_char(c), _u => id_chars(rest))
185
186# is every char of the segment an uppercase letter or a digit, and is there one?
187def segment(+ss: String) -> Bool:
188 Bool.and(Bool.not(String.is_empty(ss)), id_chars(String.to_list(ss)))
189
190# is every segment well formed?
191def segments(ss: List<&2, String>) -> Bool:
192 match ss:
193 case Nil{}:
194 True{}
195 case Con{s, rest}:
196 Lazy.and_then(segment(s), _u => segments(rest))
197
198# does the ID start with a letter?
199def lettered(+ss: String) -> Bool:
200 +c = Maybe.default(&2, Char, List.head(&2, Char, String.to_list(ss)), '0')
201 +u = Char.to_u32(c)
202 Bool.and(U32.is_ge(u, 65), U32.is_le(u, 90))
203
204# is the text an ID: `[A-Z][A-Z0-9]*(-[A-Z0-9]+)+`?
205def is_id(+ss: String) -> Bool:
206 +parts = String.split(ss, '-')
207 Bool.and(Bool.and(Nat.is_ge(List.length(&2, String, parts), 2n), segments(parts)), lettered(ss))
208
209# checking
210# --------
211
212# a finding in SPEC.md
213def at(+nn: U32, msg: String) -> F.Finding:
214 F.Finding{"SPEC.md", nn, 0, 0, "trace", msg}
215
216# how many rows have this ID (a Nat, so the count is the same in any order)
217def rows_with(rs: List<&2, Row>, +id: String) -> Nat:
218 match rs:
219 case Nil{}:
220 0n
221 case Con{Row{+i, lv, s, ls, n}, rest}:
222 +m = rows_with(rest, id)
223 Bool.pick(Nat, String.eq(i, id), 1n+m, m)
224
225# how many trust rows have this ID
226def marks_with(ms: List<&2, Mark>, +id: String) -> Nat:
227 match ms:
228 case Nil{}:
229 0n
230 case Con{Mark{+i, n}, rest}:
231 +m = marks_with(rest, id)
232 Bool.pick(Nat, String.eq(i, id), 1n+m, m)
233
234# the digest of a LAWS.bend at a path, when it was read
235def laws_file(ds: List<&2, Digest.Digest>, +pp: String) -> Maybe<&2, List<&2, Digest.Law>>:
236 match ds:
237 case Nil{}:
238 None{}
239 case Con{Digest.Digest{path, +norm, dir, is_laws, is_law_file, exempt, tops, says, deps, unsafes, laws}, rest}:
240 Lazy.stop(Maybe<&2, List<&2, Digest.Law>>, Bool.and(is_laws, String.eq(norm, pp)), Some{laws},
241 _u => laws_file(rest, pp))
242
243# the law of that name
244def law_named(ls: List<&2, Digest.Law>, +name: String) -> Maybe<&2, Digest.Law>:
245 match ls:
246 case Nil{}:
247 None{}
248 case Con{Digest.Law{+n, l, b, d}, rest}:
249 Lazy.stop(Maybe<&2, Digest.Law>, String.eq(n, name), Some{Digest.Law{n, l, b, d}}, _u => law_named(rest, name))
250
251# is the ID one of the doc lines?
252def tagged(doc: List<&2, String>, +id: String) -> Bool:
253 match doc:
254 case Nil{}:
255 False{}
256 case Con{d, rest}:
257 Lazy.or_else(String.eq(trim(d), id), _u => tagged(rest, id))
258
259# what is wrong with the law a Proved row names, found or not
260def judge_law(mm: Maybe<&2, Digest.Law>, +id: String, +entry: String, +nn: U32) -> List<&2, F.Finding>:
261 match mm:
262 case None{}:
263 [at(nn, id ++ " names " ++ entry ++ ", which is not a law in any LAWS.bend that bolt read.")]
264 case Some{Digest.Law{n, l, +b, +d}}:
265 List.append(&2, F.Finding,
266 Bool.pick(List<&2, F.Finding>, b, [], [at(nn, id ++ " names " ++ entry ++ ", a law with no `for` or `exs` binder.")]),
267 Bool.pick(List<&2, F.Finding>, tagged(d, id), [],
268 [at(nn, id ++ " names " ++ entry ++ ", but that law is not tagged # " ++ id ++ ".")]))
269
270# the law file of an entry, then the law in it
271def judge_file(
272 mm: Maybe<&2, List<&2, Digest.Law>>,
273 +name: String,
274 +id: String,
275 +entry: String,
276 +nn: U32
277) -> List<&2, F.Finding>:
278 match mm:
279 case None{}:
280 [at(nn, id ++ " names " ++ entry ++ ", but its file is not a LAWS.bend that bolt read.")]
281 case Some{ls}:
282 judge_law(law_named(ls, name), id, entry, nn)
283
284# one Law entry of a Proved row: `<path> <law>`
285def judge_entry(+ds: List<&2, Digest.Digest>, +id: String, +entry: String, +nn: U32) -> List<&2, F.Finding>:
286 +words = String.split(entry, ' ')
287 +path = Imports.norm(cell(words, 0n))
288 Lazy.stop(List<&2, F.Finding>, Bool.not(Nat.is_eq(List.length(&2, String, words), 2n)),
289 [at(nn, id ++ ": a Law entry must be <path> <law>, not " ++ entry ++ ".")],
290 _u => judge_file(laws_file(ds, path), cell(words, 1n), id, entry, nn))
291
292# every Law entry of a Proved row
293def judge_entries(es: List<&2, String>, +ds: List<&2, Digest.Digest>, +id: String, +nn: U32) -> List<&2, F.Finding>:
294 match es:
295 case Nil{}:
296 Nil{}
297 case Con{e, rest}:
298 List.append(&2, F.Finding, judge_entry(ds, id, e, nn), judge_entries(rest, ds, id, nn))
299
300# is the row a claim: Proved, and proved or pending?
301def claims(+lv: String, +st: String) -> Bool:
302 Bool.and(String.eq(lv, "Proved"), Bool.or(String.eq(st, "proved"), String.eq(st, "pending")))
303
304# what is wrong with a row's level, status and Law cell
305def shape(+lv: String, +st: String, +ls: List<&2, String>) -> String:
306 +proved = Bool.and(String.eq(lv, "Proved"), String.eq(st, "proved"))
307 +trusted = Bool.and(String.eq(lv, "Trusted"), String.is_empty(st))
308 +none = List.is_empty(&2, String, ls)
309 Bool.pick(String, Bool.not(Bool.or(claims(lv, st), trusted)),
310 "the level must be Proved or Trusted, and the status proved or pending for Proved, empty for Trusted",
311 Bool.pick(String, Bool.and(proved, none), "a proved row must name its law",
312 Bool.pick(String, Bool.and(trusted, Bool.not(none)), "a Trusted row must not name a law", "")))
313
314# every finding of one requirement row
315def judge_row(rr: Row, +sp: Spec, +ds: List<&2, Digest.Digest>) -> List<&2, F.Finding>:
316 Row{+id, +lv, +st, +ls, +nn} = rr
317 Spec{mode, reqs, trust, bad} = sp
318 +why = shape(lv, st, ls)
319 List.concat(&2, F.Finding, [
320 Bool.pick(List<&2, F.Finding>, is_id(id), [], [at(nn, id ++ " is not a valid ID; an ID matches [A-Z][A-Z0-9]*(-[A-Z0-9]+)+.")]),
321 Bool.pick(List<&2, F.Finding>, Nat.is_gt(rows_with(reqs, id), 1n), [at(nn, id ++ " is listed twice.")], []),
322 Bool.pick(List<&2, F.Finding>, String.is_empty(why), [], [at(nn, id ++ ": " ++ why ++ ".")]),
323 Bool.pick(List<&2, F.Finding>, Bool.and(String.eq(lv, "Trusted"), Nat.is_eq(marks_with(trust, id), 0n)),
324 [at(nn, id ++ " is Trusted but has no row in the trust boundary table.")], []),
325 Lazy.stop(List<&2, F.Finding>, Bool.not(claims(lv, st)), [], _u => judge_entries(ls, ds, id, nn))])
326
327# every finding of every requirement row
328def judge_rows(rs: List<&2, Row>, +sp: Spec, +ds: List<&2, Digest.Digest>) -> List<&2, F.Finding>:
329 match rs:
330 case Nil{}:
331 Nil{}
332 case Con{r, rest}:
333 List.append(&2, F.Finding, judge_row(r, sp, ds), judge_rows(rest, sp, ds))
334
335# is the ID a row that is a claim: Proved, and proved or pending?
336def claimed(rs: List<&2, Row>, +id: String) -> Bool:
337 match rs:
338 case Nil{}:
339 False{}
340 case Con{Row{+i, +lv, +st, ls, n}, rest}:
341 Lazy.or_else(Bool.and(claims(lv, st), String.eq(i, id)), _u => claimed(rest, id))
342
343# the tags of a law SPEC.md does not list as Proved, proved or pending
344def stray(
345 doc: List<&2, String>,
346 +rs: List<&2, Row>,
347 +path: String,
348 +name: String,
349 +ll: U32
350) -> List<&2, F.Finding>:
351 match doc:
352 case Nil{}:
353 Nil{}
354 case Con{d, rest}:
355 +tt = trim(d)
356 +more = stray(rest, rs, path, name, ll)
357 Lazy.stop(List<&2, F.Finding>, Lazy.or_else(Bool.not(is_id(tt)), _u => claimed(rs, tt)), more,
358 _u => F.Finding{path, ll, 0, 0, "trace",
359 "Law " ++ name ++ " is tagged " ++ tt ++ ", which is not a Proved row in SPEC.md with status proved or pending."} <> more)
360
361def strays.laws(ls: List<&2, Digest.Law>, +rs: List<&2, Row>, +path: String) -> List<&2, F.Finding>:
362 match ls:
363 case Nil{}:
364 Nil{}
365 case Con{Digest.Law{+n, +l, b, d}, rest}:
366 List.append(&2, F.Finding, stray(d, rs, path, n, l), strays.laws(rest, rs, path))
367
368# every stray tag of every law file
369def strays(ds: List<&2, Digest.Digest>, +rs: List<&2, Row>) -> List<&2, F.Finding>:
370 match ds:
371 case Nil{}:
372 Nil{}
373 case Con{Digest.Digest{+path, norm, dir, is_laws, is_law_file, exempt, tops, says, deps, unsafes, laws}, rest}:
374 List.append(&2, F.Finding, strays.laws(laws, rs, path), strays(rest, rs))
375
376# the rows that are not rows
377def malformed(ms: List<&2, Mark>) -> List<&2, F.Finding>:
378 match ms:
379 case Nil{}:
380 Nil{}
381 case Con{Mark{why, nn}, rest}:
382 at(nn, "Malformed row: " ++ why ++ ".") <> malformed(rest)
383
384# every trust row whose ID is not an ID, or is listed twice
385def twins(ms: List<&2, Mark>, +all: List<&2, Mark>) -> List<&2, F.Finding>:
386 match ms:
387 case Nil{}:
388 Nil{}
389 case Con{Mark{+id, +nn}, rest}:
390 +more = twins(rest, all)
391 +dup = Nat.is_gt(marks_with(all, id), 1n)
392 +twice = Bool.pick(List<&2, F.Finding>, dup, at(nn, id ++ " is listed twice.") <> more, more)
393 Bool.pick(List<&2, F.Finding>, is_id(id), twice, at(nn, id ++ " is not a valid ID; an ID matches [A-Z][A-Z0-9]*(-[A-Z0-9]+)+.") <> twice)
394
395# the rule over a SPEC.md that was read
396def check.spec(+sp: Spec, +ds: List<&2, Digest.Digest>) -> List<&2, F.Finding>:
397 Spec{mode, +reqs, +trust, bad} = sp
398 List.concat(&2, F.Finding, [malformed(List.reverse(&2, Mark, bad)),
399 judge_rows(List.reverse(&2, Row, reqs), sp, ds), twins(List.reverse(&2, Mark, trust), trust), strays(ds, reqs)])
400
401# the rule over SPEC.md's text (None when there is none) and every file read
402def check.at(mm: Maybe<&2, String>, +ds: List<&2, Digest.Digest>) -> List<&2, F.Finding>:
403 match mm:
404 case None{}:
405 [at(0, "Cannot read SPEC.md.")]
406 case Some{text}:
407 check.spec(parse(text), ds)
408
409# the rule, when bolt lints the whole tree; a run over the files named on the
410# line holds only some of the laws, so it has nothing sound to check
411def check(whole: Bool, mm: Maybe<&2, String>, +ds: List<&2, Digest.Digest>) -> List<&2, F.Finding>:
412 match whole:
413 case True{}:
414 check.at(mm, ds)
415 case False{}:
416 Nil{}