spec citations: five named sections their SPECs do not have, and a check so they cannot return #238
8 changed files with 216 additions and 5 deletions
45
.github/workflows/spec-refs.yml
vendored
Normal file
45
.github/workflows/spec-refs.yml
vendored
Normal file
|
|
@ -0,0 +1,45 @@
|
|||
name: spec citations resolve
|
||||
|
||||
# Every `SPEC §N` a standard's code cites is a section that standard's SPEC.md
|
||||
# has. See the header of scripts/check-spec-refs.py for why: a citation to a
|
||||
# section that does not exist reads as authority it does not have, and the three
|
||||
# instances found so far were each discovered by reading, long after they were
|
||||
# written.
|
||||
#
|
||||
# Deliberately NO `paths:` filter, for two reasons.
|
||||
#
|
||||
# The check is one Python pass over the tree — about a second, no toolchain, no
|
||||
# cargo — so running it on every change costs less than describing when to run
|
||||
# it. And a correct filter here would have to name every standard's `**/*.rs`
|
||||
# plus every `SPEC.md`; `standards-build.yml` records that `**`-prefixed globs
|
||||
# do not match on this forge the way they do elsewhere, and that a gate which
|
||||
# quietly fails to fire is worse than no gate, because it reports nothing and
|
||||
# everyone reads that as green. An unfiltered cheap check cannot fail that way.
|
||||
#
|
||||
# The self-test runs first and on its own line. A check that cannot fail is
|
||||
# decoration, and this one would be easy to break into permanent silence — a
|
||||
# regex that stops matching finds nothing and exits 0.
|
||||
|
||||
concurrency:
|
||||
group: ${{ github.workflow }}-${{ github.ref }}
|
||||
cancel-in-progress: true
|
||||
|
||||
on:
|
||||
pull_request:
|
||||
push:
|
||||
branches:
|
||||
- main
|
||||
|
||||
jobs:
|
||||
spec-refs:
|
||||
name: Code cites no section its SPEC lacks
|
||||
runs-on: linux
|
||||
steps:
|
||||
- name: Checkout
|
||||
uses: actions/checkout@v4
|
||||
|
||||
- name: The check can fail (self-test)
|
||||
run: bash scripts/check-spec-refs-selftest.sh
|
||||
|
||||
- name: Every SPEC citation resolves
|
||||
run: python3 scripts/check-spec-refs.py
|
||||
|
|
@ -33,7 +33,7 @@
|
|||
//! button (message banking), travel in the file: the photo as the button's
|
||||
//! image, the recording as its `sound`, each as a `data:` URI when the
|
||||
//! export is given their bytes ([`ObfExportOptions::media`]).
|
||||
//! - A word hidden in place (SPEC §3.3) is a button with `hidden: true`.
|
||||
//! - A word hidden in place (SPEC §2.1, §3 item 3) is a button with `hidden: true`.
|
||||
//! - AuraSense extensions: `ext_aurasense_locked` (board and button),
|
||||
//! `ext_aurasense_word_class` (the button's part of speech, from the core
|
||||
//! vocabulary) and `ext_aurasense_provenance` (where each piece came from:
|
||||
|
|
|
|||
|
|
@ -93,7 +93,7 @@ pub fn handle_cell_action(
|
|||
})
|
||||
})
|
||||
});
|
||||
// A hidden word keeps its place but cannot be chosen (SPEC §3.3), unless
|
||||
// A hidden word keeps its place but cannot be chosen (SPEC §3.1 item 3), unless
|
||||
// hidden words are shown for now: a press there does nothing at all (Help's
|
||||
// message stays, words being said go on). A word with no word in the
|
||||
// person's language yet is hidden in place too, shown or not.
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@
|
|||
//! always its words.
|
||||
//!
|
||||
//! A photo the person added takes the symbol's place (media.rs). A hidden
|
||||
//! word (SPEC §3.3) keeps its place but looks like an empty one and cannot
|
||||
//! word (SPEC §3.1 item 3) keeps its place but looks like an empty one and cannot
|
||||
//! be chosen, unless hidden words are shown for now; in Edit mode it shows
|
||||
//! faded, and every cell, and every empty place, opens the cell editor
|
||||
//! (editing.rs).
|
||||
|
|
|
|||
|
|
@ -225,7 +225,8 @@ pub struct BuildTask {
|
|||
pub steps: Vec<BuildStep>,
|
||||
}
|
||||
|
||||
/// The cascade tier that resolved a step (deterministic-first, SPEC §12.1).
|
||||
/// The cascade tier that resolved a step (deterministic-first, `spec/build.md`;
|
||||
/// the receipt that records it is SPEC §12).
|
||||
/// A build never invokes a frontier model *inside* the sandbox — execution is
|
||||
/// the deterministic verification — so the only tiers seen here are the cheap
|
||||
/// ones: a content-addressed cache hit, or a fresh deterministic execution.
|
||||
|
|
|
|||
|
|
@ -515,7 +515,8 @@ mod tests {
|
|||
.iter()
|
||||
.any(|e| matches!(e, sandbox_attest::JournalEntry::HostCall { name, .. } if name == "storage_read")));
|
||||
|
||||
// The brokered I/O is metered as a storage line (SPEC §6.5): one write +
|
||||
// The brokered I/O is metered as a storage line (`spec/receipts.md`,
|
||||
// storage activity — its own axis, outside §6.2's per-device sum): one write +
|
||||
// one read ⇒ 2 ops, 7 bytes read ("payload"), an honest estimate.
|
||||
let storage = report.storage.expect("storage activity was metered");
|
||||
assert_eq!(storage.iops, 2);
|
||||
|
|
|
|||
70
scripts/check-spec-refs-selftest.sh
Executable file
70
scripts/check-spec-refs-selftest.sh
Executable file
|
|
@ -0,0 +1,70 @@
|
|||
#!/usr/bin/env bash
|
||||
#
|
||||
# check-spec-refs-selftest.sh — check-spec-refs.py can fail.
|
||||
#
|
||||
# A check that cannot fail is decoration. This builds scratch standards under a
|
||||
# temporary root and asserts that the check
|
||||
# 1. passes when every cited section is a heading;
|
||||
# 2. fails when a cited section is not a heading (the case it exists for);
|
||||
# 3. accepts both heading spellings, `## 4.` and `## §4`;
|
||||
# 4. does NOT synthesise parents: a `## 4.10` heading alone must not satisfy a
|
||||
# `SPEC §4` citation, which is how a standard citing a section it never
|
||||
# wrote would otherwise pass;
|
||||
# 5. resolves a citation against the SPEC.md of the standard the file sits in,
|
||||
# so one standard's section cannot excuse another's citation;
|
||||
# 6. ignores `*.rs` under a `target/` directory, which is build output.
|
||||
# Nothing here reads the real tree, and nothing needs a network.
|
||||
set -uo pipefail
|
||||
|
||||
here=$(cd "$(dirname "$0")" && pwd)
|
||||
check=$here/check-spec-refs.py
|
||||
tmp=$(mktemp -d)
|
||||
trap 'rm -rf "$tmp"' EXIT
|
||||
fails=0
|
||||
|
||||
# mk <root> <standard> <spec-headings> <rs-relative-path> <rs-body>
|
||||
mk() {
|
||||
mkdir -p "$1/$2/$(dirname "$4")"
|
||||
printf '%s\n' "$3" > "$1/$2/SPEC.md"
|
||||
printf '%s\n' "$5" > "$1/$2/$4"
|
||||
}
|
||||
|
||||
want() { # want <expect-status> <root> <label>
|
||||
python3 "$check" "$2" > "$tmp/out" 2>&1
|
||||
got=$?
|
||||
if [ "$got" != "$1" ]; then
|
||||
echo "FAIL: $3 — expected exit $1, got $got"
|
||||
sed 's/^/ /' "$tmp/out"
|
||||
fails=$((fails + 1))
|
||||
else
|
||||
echo "ok: $3"
|
||||
fi
|
||||
}
|
||||
|
||||
r=$tmp/a; mk "$r" alpha '## 4. Flow
|
||||
### 4.1 Detail' src/lib.rs '/// Enforces SPEC §4.1 and SPEC §4.'
|
||||
want 0 "$r" "passes when every citation resolves"
|
||||
|
||||
r=$tmp/b; mk "$r" alpha '## 4. Flow' src/lib.rs '/// Enforces SPEC §4.10.'
|
||||
want 1 "$r" "fails on a citation with no heading"
|
||||
|
||||
r=$tmp/c; mk "$r" alpha '## §4. Flow
|
||||
### §4.1 Detail' src/lib.rs '/// Enforces SPEC §4.1.'
|
||||
want 0 "$r" "accepts the section-sign heading spelling"
|
||||
|
||||
r=$tmp/d; mk "$r" alpha '### 4.10 Child only' src/lib.rs '/// Enforces SPEC §4.'
|
||||
want 1 "$r" "does not let a child heading satisfy its parent"
|
||||
|
||||
r=$tmp/e
|
||||
mk "$r" alpha '## 7. Only in alpha' src/lib.rs '/// nothing cited here'
|
||||
mk "$r" beta '## 1. Only in beta' src/lib.rs '/// Enforces SPEC §7.'
|
||||
want 1 "$r" "does not resolve beta's citation against alpha's SPEC"
|
||||
|
||||
r=$tmp/f; mk "$r" alpha '## 4. Flow' target/debug/build.rs '/// Enforces SPEC §9.'
|
||||
want 0 "$r" "ignores .rs under target/"
|
||||
|
||||
if [ "$fails" != 0 ]; then
|
||||
echo "check-spec-refs-selftest: $fails case(s) failed."
|
||||
exit 1
|
||||
fi
|
||||
echo "check-spec-refs-selftest: all cases pass."
|
||||
94
scripts/check-spec-refs.py
Executable file
94
scripts/check-spec-refs.py
Executable file
|
|
@ -0,0 +1,94 @@
|
|||
#!/usr/bin/env python3
|
||||
"""Every `SPEC §N` a standard's code cites is a section that standard's SPEC.md has.
|
||||
|
||||
Code cites normative text to say which rule it implements or enforces. When the
|
||||
cited section does not exist, the citation reads as authority it does not have:
|
||||
the mechanism is real, gate-enforcing and tested, and nothing normative stands
|
||||
behind it. That has happened here repeatedly — `jcp-runtime` cited `SPEC §4.10`
|
||||
in six places and §4.10 did not exist (fixed by #190); `aac` cited §3.3 for a
|
||||
rule its SPEC states as "§3 item 3"; `sandbox` cited §6.5 and §12.1 for rules
|
||||
that live in `spec/receipts.md` and `spec/build.md`. Each was found by reading,
|
||||
once, long after it was written. This is that reading, done every time.
|
||||
|
||||
What it checks: in each directory holding a `SPEC.md`, every `SPEC §N` (one or
|
||||
more parts: §7, §4.10, §2.4.3) appearing in a `*.rs` file under that directory
|
||||
resolves to a numbered heading of that same `SPEC.md`. A heading counts when it
|
||||
begins `#`…, then the number, with or without `§`, as in `## 7.`, `### 6.4 `,
|
||||
`## §3.` or `### §3.1 `.
|
||||
|
||||
What it deliberately does not check:
|
||||
|
||||
- Parent numbers are not synthesised. A cited `§4` needs its own `§4` heading;
|
||||
a `§4.10` heading does not satisfy it. A standard that cites a section it
|
||||
never wrote should say so, not be excused by a child.
|
||||
- A citation is resolved against the SPEC.md of the directory the file is in.
|
||||
Every cross-standard citation in the tree today is a self-reference that
|
||||
names its own standard for the reader ("JouleClaw SPEC §1.3", inside
|
||||
jouleclaw/), so this is right for all of them. If a file ever cites another
|
||||
standard's SPEC, resolve it by naming that standard's own file instead —
|
||||
do not loosen this check, which would stop it finding anything.
|
||||
- Sections of a `spec/*.md` subfile are not sections of `SPEC.md`. Rules that
|
||||
live in a subfile should be cited by that file's name, which is what the
|
||||
sandbox fixes above do.
|
||||
- Markdown-to-markdown references are a different check, and WAI's are already
|
||||
covered by `check-wai-section-refs.py`.
|
||||
|
||||
Exit status 1, with one line per citation naming a section its SPEC does not
|
||||
have; 0 otherwise.
|
||||
|
||||
python3 scripts/check-spec-refs.py [repo-root]
|
||||
"""
|
||||
import collections
|
||||
import os
|
||||
import pathlib
|
||||
import re
|
||||
import sys
|
||||
|
||||
HEADING = re.compile(r"^#{1,6}[ \t]+§?([0-9]+(?:\.[0-9]+)*)\.?(?=[ \t])", re.M)
|
||||
CITATION = re.compile(r"SPEC[ \t]+§[ \t]*([0-9]+(?:\.[0-9]+)*)")
|
||||
|
||||
|
||||
def sections(spec: pathlib.Path) -> set:
|
||||
return set(HEADING.findall(spec.read_text(errors="replace")))
|
||||
|
||||
|
||||
def main() -> int:
|
||||
root = pathlib.Path(sys.argv[1] if len(sys.argv) > 1 else
|
||||
pathlib.Path(__file__).resolve().parent.parent).resolve()
|
||||
standards = sorted(d for d in root.iterdir()
|
||||
if d.is_dir() and not d.name.startswith(".") and (d / "SPEC.md").is_file())
|
||||
dangling = 0
|
||||
cited_total = 0
|
||||
for s in standards:
|
||||
defined = sections(s / "SPEC.md")
|
||||
found = collections.defaultdict(list)
|
||||
for f in s.rglob("*.rs"):
|
||||
if "target" in f.parts:
|
||||
continue
|
||||
try:
|
||||
text = f.read_text(errors="replace")
|
||||
except OSError:
|
||||
continue
|
||||
if "SPEC" not in text:
|
||||
continue
|
||||
for i, line in enumerate(text.splitlines(), 1):
|
||||
for m in CITATION.finditer(line):
|
||||
found[m.group(1)].append(f"{f.relative_to(root)}:{i}")
|
||||
cited_total += sum(len(v) for v in found.values())
|
||||
for n, locs in sorted(found.items(), key=lambda kv: [int(x) for x in kv[0].split(".")]):
|
||||
if n in defined:
|
||||
continue
|
||||
for loc in locs:
|
||||
print(f"{loc}: cites SPEC §{n}, which {s.name}/SPEC.md does not define")
|
||||
dangling += 1
|
||||
if dangling:
|
||||
print(f"\ncheck-spec-refs: {dangling} dangling citation(s) across {len(standards)} standards.")
|
||||
print("Either add the section, or cite where the rule actually lives "
|
||||
"(a `spec/*.md` subfile, or a numbered item of a parent section).")
|
||||
return 1
|
||||
print(f"check-spec-refs: {cited_total} citations across {len(standards)} standards, all resolve.")
|
||||
return 0
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
sys.exit(main())
|
||||
Loading…
Reference in a new issue