src/rules/laws/trace.bend checks

raw source on the hub · import 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/laws/trace.bend as Trace

rule trace (project-wide, opt-in): SPEC.md and the laws agree. SPEC.md, read from the directory bolt runs in, lists requirements in tables whose header is exactly | ID | Requirement | Level | Status | Law |, and trust rows in tables headed | ID | Assumption | Why it is trusted |. An ID is uppercase letters and digits in two or more segments joined by - (BOLT-CFG-1); a law proves one when a line of its comment block is exactly that ID (# BOLT-CFG-1). A Proved row, proved or pending, is a claim: a proved row's Law cell names the laws that prove it, and a pending row's may name laws that prove part of it while the row stays pending. The findings: a row that is not a well-formed requirement or trust row, an ID that does not match the pattern included; an ID listed twice; a proved row whose Law cell names no law; a Trusted row that names a law; a Law entry of a Proved row, proved or pending, whose law is missing, has no for/exs binder, or lacks the row's tag; a Trusted row with no trust row; and a tag naming an ID SPEC.md does not list as Proved, proved or pending. A Law entry is <path> <law>, the path relative to SPEC.md, entries joined by ; . Only a bolt.bend that names the rule turns it on (src/config.bend). It runs only when bolt lints the whole tree, never over files named on the line.

5 imports

import Base
import ../../finding.bend as F
import ../digest.bend as Digest
import ../imports.bend as Imports
import ../../lazy/lazy.bend as Lazy

Types

type Row source · line 30 · raw

Data

one requirement row: its ID, level and status, the Law cell's entries, and its line (0-based)

Row

@id:String -> @level:String -> @status:String -> @laws:List<&2, String> -> @line:U32 -> Row

type Mark source · line 34 · raw

Data

an ID, or a reason, at a line

Mark
```
@id:String -> @line:U32 -> Mark
```

type Mode source · line 39 · raw

Data

which table the lines are in; Head is the header row, whose | :-- | line comes next

Out
```
Mode
```
ReqHead
```
Mode
```
Reqs
```
Mode
```
TrustHead
```
Mode
```
Trusts
```
Mode
```

type Spec source · line 48 · raw

Data

what SPEC.md says: the requirement rows, the trust rows, the rows that are not well formed (why, where), each list in reverse file order while read

Spec

@mode:Mode -> @reqs:List<&2, Row> -> @trust:List<&2, Mark> -> @bad:List<&2, Mark> -> Spec

type Cells source · line 65 · raw

Data

a table line read so far: the cell being read and the cells before it, each backwards

Cells

@cur:List<&2, Char> -> @done:List<&2, String> -> Cells

Definitions

def req_head source · line 52 · raw

String

the requirement table's header

def trust_head source · line 56 · raw

String

the trust table's header

def trim source · line 60 · raw

@+ss:String -> String

a cell's text, spaces trimmed

def cells.at source · line 69 · raw

@bar:Bool -> @cc:Char -> @st:Cells -> Cells

one char onto the cells read: a bar ends the cell, any other char extends it

def cells.go source · line 81 · raw

@cs:List<&2, Char> -> @esc:Bool -> @st:Cells -> List<&2, String>

the cells of a table line, split at every | that does not follow a \ (an escaped \|); esc says the char before was a \. It matches no char pattern, so the proofs can take a char apart by what Char.is_eq says of it

def cells source · line 90 · raw

@+line:String -> List<&2, String>

the cells between a line's outer bars

def cell source · line 95 · raw

@+cs:List<&2, String> -> @ii:Nat -> String

the i-th cell, or empty

def entries.go source · line 98 · raw

@ss:List<&2, String> -> List<&2, String>

def entries source · line 107 · raw

@ss:String -> List<&2, String>

a Law cell's entries

def add_req source · line 111 · raw

@+line:String -> @+nn:U32 -> @st:Spec -> Spec

a requirement row onto the spec, or a malformed one

def add_trust source · line 119 · raw

@+line:String -> @+nn:U32 -> @st:Spec -> Spec

a trust row onto the spec, or a malformed one

def moved source · line 127 · raw

@st:Spec -> @mm:Mode -> Spec

the spec in another mode

def in_table source · line 132 · raw

@mode:Mode -> @+line:String -> @+nn:U32 -> @st:Spec -> Spec

a line inside a table: the header's | :-- | line, a row, or the end

def mode_of source · line 146 · raw

@st:Spec -> Mode

the mode a spec is in

def step source · line 151 · raw

@+line:String -> @+nn:U32 -> @+st:Spec -> Spec

one line of SPEC.md onto what it says

def parse.go source · line 158 · raw

@ls:List<&2, String> -> @+nn:U32 -> @st:Spec -> Spec

def parse source · line 166 · raw

@text:String -> Spec

what SPEC.md's text says

def id_char source · line 173 · raw

@cc:Char -> Bool

is the char an uppercase letter or a digit?

def id_chars source · line 178 · raw

@cs:List<&2, Char> -> Bool

is every char an uppercase letter or a digit?

def segment source · line 186 · raw

@+ss:String -> Bool

is every char of the segment an uppercase letter or a digit, and is there one?

def segments source · line 190 · raw

@ss:List<&2, String> -> Bool

is every segment well formed?

def lettered source · line 198 · raw

@+ss:String -> Bool

does the ID start with a letter?

def is_id source · line 204 · raw

@+ss:String -> Bool

is the text an ID: [A-Z][A-Z0-9]*(-[A-Z0-9]+)+?

def at source · line 212 · raw

@+nn:U32 -> @msg:String -> 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding

a finding in SPEC.md

def rows_with source · line 216 · raw

@rs:List<&2, Row> -> @+id:String -> Nat

how many rows have this ID (a Nat, so the count is the same in any order)

def marks_with source · line 225 · raw

@ms:List<&2, Mark> -> @+id:String -> Nat

how many trust rows have this ID

def laws_file source · line 234 · raw

@ds:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Digest> -> @+pp:String -> Maybe<&2, List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Law>>

the digest of a LAWS.bend at a path, when it was read

def law_named source · line 243 · raw

@ls:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Law> -> @+name:String -> Maybe<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Law>

the law of that name

def tagged source · line 251 · raw

@doc:List<&2, String> -> @+id:String -> Bool

is the ID one of the doc lines?

def judge_law source · line 259 · raw

@mm:Maybe<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Law> -> @+id:String -> @+entry:String -> @+nn:U32 -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

what is wrong with the law a Proved row names, found or not

def judge_file source · line 270 · raw

@mm:Maybe<&2, List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Law>> -> @+name:String -> @+id:String -> @+entry:String -> @+nn:U32 -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

the law file of an entry, then the law in it

def judge_entry source · line 284 · raw

@+ds:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Digest> -> @+id:String -> @+entry:String -> @+nn:U32 -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

one Law entry of a Proved row: <path> <law>

def judge_entries source · line 292 · raw

@es:List<&2, String> -> @+ds:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Digest> -> @+id:String -> @+nn:U32 -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

every Law entry of a Proved row

def claims source · line 300 · raw

@+lv:String -> @+st:String -> Bool

is the row a claim: Proved, and proved or pending?

def shape source · line 304 · raw

@+lv:String -> @+st:String -> @+ls:List<&2, String> -> String

what is wrong with a row's level, status and Law cell

def judge_row source · line 314 · raw

@rr:Row -> @+sp:Spec -> @+ds:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Digest> -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

every finding of one requirement row

def judge_rows source · line 327 · raw

@rs:List<&2, Row> -> @+sp:Spec -> @+ds:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Digest> -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

every finding of every requirement row

def claimed source · line 335 · raw

@rs:List<&2, Row> -> @+id:String -> Bool

is the ID a row that is a claim: Proved, and proved or pending?

def stray source · line 343 · raw

@doc:List<&2, String> -> @+rs:List<&2, Row> -> @+path:String -> @+name:String -> @+ll:U32 -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

the tags of a law SPEC.md does not list as Proved, proved or pending

def strays.laws source · line 360 · raw

@ls:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Law> -> @+rs:List<&2, Row> -> @+path:String -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

def strays source · line 368 · raw

@ds:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Digest> -> @+rs:List<&2, Row> -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

every stray tag of every law file

def malformed source · line 376 · raw

@ms:List<&2, Mark> -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

the rows that are not rows

def twins source · line 384 · raw

@ms:List<&2, Mark> -> @+all:List<&2, Mark> -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

every trust row whose ID is not an ID, or is listed twice

def check.spec source · line 395 · raw

@+sp:Spec -> @+ds:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Digest> -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

the rule over a SPEC.md that was read

def check.at source · line 401 · raw

@mm:Maybe<&2, String> -> @+ds:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Digest> -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

the rule over SPEC.md's text (None when there is none) and every file read

def check source · line 410 · raw

@whole:Bool -> @mm:Maybe<&2, String> -> @+ds:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/digest.Digest> -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

the rule, when bolt lints the whole tree; a run over the files named on the line holds only some of the laws, so it has nothing sound to check