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.
20	import Base
21	import ../../finding.bend as F
22	import ../digest.bend as Digest
23	import ../imports.bend as Imports
24	import ../../lazy/lazy.bend as Lazy
25	import ../../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)
32	type 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
36	type 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
41	type 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
50	type 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
54	def req_head() -> String:
55	  "| ID | Requirement | Level | Status | Law |"
56	
57	# the trust table's header
58	def trust_head() -> String:
59	  "| ID | Assumption | Why it is trusted |"
60	
61	# a cell's text, spaces trimmed
62	def 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
67	type 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
71	def 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
83	def 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
92	def 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
97	def cell(+cs: List<&2, String>, ii: Nat) -> String:
98	  Maybe.default(&2, String, List.get(&2, String, cs, ii), "")
99	
100	def 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
109	def entries(ss: String) -> List<&2, String>:
110	  entries.go(String.split(ss, ';'))
111	
112	# a requirement row onto the spec, or a malformed one
113	def 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
121	def 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
129	def 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
134	def 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
148	def 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
153	def 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	
160	def 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
168	def 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?
175	def 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?
180	def 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?
188	def 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?
192	def 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?
200	def 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]+)+`?
206	def 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
214	def 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)
218	def 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
227	def 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
236	def 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
245	def 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?
253	def 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
261	def 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
272	def 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>`
286	def 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
294	def 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?
302	def 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
306	def 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
316	def 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
329	def 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?
337	def 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
345	def 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	
362	def 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
370	def 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
378	def 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
386	def 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
397	def 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
403	def 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
412	def 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{}