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