Give a record that narrows one clause of another a shape, and check it (#267)

[iderex]

The issue this belongs to

Closes #267

What changed

0001 permits a pointer to a later record that goes further on a case the earlier
one already names, and fixes nothing about where that pointer goes or what it
looks like. The one instance in the tree took the shape that reading allows: a
paragraph at line 120 of 0103, inside the section it concerns.

0267 decides the pointer is a pair of header fields instead. A record that
narrows one clause of an earlier one carries Narrows: NNNN, <clause>; the
record it narrows carries Narrowed-by: NNNN, <clause> beside its Status:
line. Each names the other, and each names the clause that moved rather than only
the record.

The record says what this asks of 0001 rather than leaving it to be inferred. It
changes clause three in two ways - the pointer takes a fixed form where the later
record narrows rather than merely goes further, and it becomes a pair, so the
narrowing record receives a field naming an earlier record, which clause three
as written says nothing about. Both halves pass clause three's own test: remove
either field and both records say exactly what they said before. Where the field
goes is read as something 0001 does not fix, and that reading is written down in
the record so it can be argued with rather than discovered.

The shape is then applied to the one instance that exists. 0103 receives
Narrowed-by: 0243, 0243 receives Narrows: 0103, and 0001 receives the first
Narrowed-by: line in the tree, naming 0267.

What failure it prevents

A reader who stops at a record's header. Today that reader opens 0103, sees
accepted with nothing beside it, and applies its fourth refused behaviour one
clause wider than the rule in force - refusing a dependency this board decided is
admissible. Nothing tells them anything is missing, which is what makes it
expensive: a wrong reading of a record reads exactly like a right one.

It has already happened in the weaker form the issue records: the narrowing is at
line 120 of a record with more than two hundred, and following a pointer is only
optional when it is possible to miss one.

The second field prevents the failure one level up. A pointer only one end
carries rots the first time a record is renumbered or withdrawn, and it rots in
silence, which is the same defect class the field exists to fix.

Evidence

The commit these were run at:

git rev-parse HEAD
a1fc0ef6793b398bb7d7710617bfc7160bdb53b5

The rule set and the fixtures behind it:

bash .github/decision-records/decision-records.sh selftest | awk '/^ok    bites/{b++} /^ok    passes/{p++} /^ok    /{t++} END{print t, b, p}'
16 9 7

Sixteen fixtures, nine of them violations the rules must refuse and seven near
misses they must not. Every one runs before the gate judges a single tracked
record, so a rule cannot pass its fixture and refuse something else in the gate.

The tree after the four fields land:

bash .github/decision-records/decision-records.sh check | grep -E '^Records:|^ok  '
Records: 62. Fields found: 4.
ok    4 field(s) name a record that exists, name a clause, and are named back

Records carrying one of the two fields:

git ls-files 'docs/decisions/*.md' | while read -r f; do grep -q '^Narrows:\|^Narrowed-by:' "$f" && echo "$f"; done | wc -l
4

Fifty-eight of the sixty-two carry neither, by subtraction from the two readings
above.

The rest of the gate, run locally at this commit:

cargo build --locked --all-targets
Finished `dev` profile [unoptimized + debuginfo] target(s) in 2.76s

cargo test --locked | grep -c '^test result: ok'
9

bash .github/doc-paths/doc-paths.sh check | tail -1
Every path these documents name resolves against the tracked set.

bash .github/invariants/invariants.sh check | tail -1
Every rule above was applied to its subject and refused nothing.

bash .github/fixture-scrub/fixture-scrub.sh check | tail -1
Every rule above was applied to its subject and refused nothing.

What a guard here refuses, and the proof it bites

.github/decision-records/decision-records.sh refuses five things: a field naming
a record that does not exist, a field naming a record and no clause, a field
written below the first heading, a record narrowing itself, and a half of a pair
with no answering half.

The nine violating fixtures are what proves each one bites in isolation. The
pairing rule was also watched failing on the real tree rather than only on a
fixture, because it is the one whose subject is the tree rather than a single
file. Deleting the line just landed on 0243:

sed -i '/^Narrows: 0103,/d' docs/decisions/0243-the-means-a-certificate-is-validated-with.md
bash .github/decision-records/decision-records.sh check
      docs/decisions/0103-what-admits-a-dependency-and-what-is-refused.md:7: names 0243 as narrowing it, and 0243 carries no Narrows: line naming 0103 back
::error::1 narrowing field(s) do not hold. Each one is printed above with its record and line.
exit 1

and the same run with the line restored:

bash .github/decision-records/decision-records.sh check | grep '^ok  '
ok    4 field(s) name a record that exists, name a clause, and are named back

The seven near misses are the other half of the proof, and they are the mistakes
somebody actually makes rather than violations that could not have passed: a
Status: line, which carries the other kind of pointer; the field quoted inside a
fenced block and inside an indented block, which is what a record arguing about
this format does; the field indented by one space; a sentence beginning with the
words and no colon at column zero; and a record carrying neither field.

The means, and why it fits

bash and awk over tracked text, matching .github/doc-paths/doc-paths.sh and
.github/invariants/invariants.sh. The subject is a line in a Markdown file, the
rules owe executed fixtures rather than a type system, and nothing here needs a
toolchain, so the check has a verdict on a tree the compiler cannot build. It
adds no language and no dependency this tree does not already carry.

It is its own script and its own workflow rather than a second rule family inside
doc-paths. That check's subject is a path that resolves, and its run prints an
accounting of what it did not read that a second family would have made false.

What this does not cover

Whether the clause a field names is the clause that actually moved. The field
either carries text after the record number or it does not; whether that text
describes the right sentence is a judgement about meaning, and no reading of the
tree makes it.

A later record that narrows an earlier one and writes no field at all. Nothing
here notices, and 0267 states that residual of itself rather than implying the
tree is covered.

Precedence between two records narrowing the same clause. 0267 fixes a pointer
and decides nothing about which narrowing wins, and names that as one of the
conditions that would reverse it.

The pointer already in 0103 is not repaired. That paragraph restates the narrowed
rule and the condition it rests on, so removing it would take something away, and
by 0001's own test that makes it an argument rather than a pointer. The
no-editing rule is what stops a landed paragraph being trimmed, so the field lands
beside it and the record keeps its text. This was found while writing 0267 and is
written into it rather than only here.

Issue #269 is not touched. It asks how a record carries a reading that has moved,
which is a stale reading rather than a narrowing, and 0267's answer does not reach
it.

No run on GitHub had happened when this body was written. Every command above ran
on a Windows machine in Git Bash, and the gate runs on ubuntu-latest; the awk
constructs the runner's mawk disagrees with are avoided for that reason and named
in the script, but no run on mawk has been taken here.

The first push of this change went out as branch
a-record-that-narrows-one-clause-267, whose commit message carried two wrong
counts. It is superseded by this branch, whose commit is identical in content, and
the old branch is left in place because deleting an unmerged branch is not
something this arrangement does.

Who has read it

Nobody other than the author. There was no second reader available for it, and
the evidence above stands in place of one rather than the question being left
open.