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