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	import ../../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)
31	type 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
35	type 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
40	type 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
49	type 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
53	def req_head() -> String:
54	  "| ID | Requirement | Level | Status | Law |"
55	
56	# the trust table's header
57	def trust_head() -> String:
58	  "| ID | Assumption | Why it is trusted |"
59	
60	# a cell's text, spaces trimmed
61	def 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
66	type 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
70	def 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
82	def 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
91	def 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
96	def cell(+cs: List<&2, String>, ii: Nat) -> String:
97	  Maybe.default(&2, String, List.get(&2, String, cs, ii), "")
98	
99	def 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
108	def entries(ss: String) -> List<&2, String>:
109	  entries.go(String.split(ss, ';'))
110	
111	# a requirement row onto the spec, or a malformed one
112	def 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
120	def 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
128	def 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
133	def 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
147	def 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
152	def 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	
159	def 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
167	def 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?
174	def 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?
179	def 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?
187	def 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?
191	def 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?
199	def 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]+)+`?
205	def 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
213	def 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)
217	def 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
226	def 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
235	def 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
244	def 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?
252	def 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
260	def 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
271	def 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>`
285	def 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
293	def 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?
301	def 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
305	def 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
315	def 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
328	def 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?
336	def 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
344	def 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	
361	def 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
369	def 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
377	def 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
385	def 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
396	def 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
402	def 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
411	def 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{}