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.
19	import Base
20	import ../../finding.bend as F
21	import ../digest.bend as Digest
22	import ../imports.bend as Imports
23	import ../../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)
30	type 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
34	type 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
39	type 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
48	type 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
52	def req_head() -> String:
53	  "| ID | Requirement | Level | Status | Law |"
54	
55	# the trust table's header
56	def trust_head() -> String:
57	  "| ID | Assumption | Why it is trusted |"
58	
59	# a cell's text, spaces trimmed
60	def 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
65	type 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
69	def 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
81	def 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
90	def 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
95	def cell(+cs: List<&2, String>, ii: Nat) -> String:
96	  Maybe.default(&2, String, List.get(&2, String, cs, ii), "")
97	
98	def 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
107	def entries(ss: String) -> List<&2, String>:
108	  entries.go(String.split(ss, ';'))
109	
110	# a requirement row onto the spec, or a malformed one
111	def 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
119	def 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
127	def 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
132	def 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
146	def 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
151	def 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	
158	def 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
166	def 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?
173	def 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?
178	def 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?
186	def 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?
190	def 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?
198	def 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]+)+`?
204	def 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
212	def 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)
216	def 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
225	def 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
234	def 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
243	def 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?
251	def 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
259	def 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
270	def 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>`
284	def 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
292	def 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?
300	def 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
304	def 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
314	def 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
327	def 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?
335	def 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
343	def 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	
360	def 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
368	def 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
376	def 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
384	def 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
395	def 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
401	def 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
410	def 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{}