From 7e53affcdef019d8f5d7d82fbba3958e70c9327e Mon Sep 17 00:00:00 2001 From: speak-agent Date: Sun, 20 Sep 2026 18:36:43 +0800 Subject: [PATCH 1/3] the interface list an implementation provides is derived from its artefact `provides-interfaces` in a package manifest is a declaration, and a declaration is checked rather than trusted. The check available to it already exists: clause 9's surface comparison walks SURFACE.txt group by group and decides, for each, whether the artefact exports it whole, in part, or not at all. "Which interfaces does this implementation provide" is that walk stopped one step earlier. `check-surface.sh` gains `--interfaces` and `--toml` rather than a second script, because a second derivation of the same walk would go stale the first time a group was added. `--toml` prints the array a manifest carries, so a package's declaration is GENERATED FROM THE ARTEFACT: a declaration derived from the thing it describes cannot disagree with it, and an implementation that gains an interface cannot forget to say so. `openkal.version` is excluded. SURFACE.txt says in its own header that it is not an interface --- it provides no resource --- and every conforming implementation exports it, so listing it would put a name that answers nothing in every package. A group exported in PART is not listed. An interface is provided in whole or not at all (clause 3), so half of one is not a smaller claim but a different and false one. CI asserts both directions against a real implementation: the list contains openkal.stream, and removing one of that group's definitions takes it out. Without the second leg the first passes against a script that prints every group in SURFACE.txt and reads no artefact at all. Co-authored-by: Claude Code --- .github/workflows/ci.yml | 49 ++++++++++++++++++++++++ README.md | 36 ++++++++++++++++++ tools/check-surface.sh | 82 +++++++++++++++++++++++++++++++++++++++- 3 files changed, 165 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 27ad1f2..3714f70 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -571,6 +571,55 @@ jobs: fi rm -f src/extra.cpp + - name: The interface list is derived from the artefact + working-directory: examples/substitution/impl-fd + run: | + # `provides-interfaces` in a package manifest is a declaration, and a + # declaration is checked rather than trusted. The check available to + # it is clause 9's surface comparison, stopped one step earlier: the + # walk that decides whether each group is exported whole already + # answers "which interfaces does this implementation provide". This + # step asserts that the answer comes from the artefact and moves with + # it. + mcpp build > /dev/null + objs="$(find target -name '*.o' | tr '\n' ' ')" + bash ../../../tools/check-surface.sh --interfaces \ + ../../../SURFACE.txt $objs > provided.txt + grep -qx 'openkal.stream' provided.txt || { + echo "the implementation exports openkal.stream whole and it was not listed" + cat provided.txt; exit 1 + } + # `openkal.version` is exported by every conforming implementation + # and is not an interface --- SURFACE.txt says so in its own header. + # Listing it would put a name that answers nothing in every package. + if grep -qx 'openkal.version' provided.txt; then + echo "openkal.version is not an interface and must not be listed"; exit 1 + fi + + # REMOVE ONE DEFINITION AND THE INTERFACE MUST LEAVE THE LIST. An + # interface is provided in whole or not at all (clause 3), so a group + # exported in part is not a smaller claim but a different and false + # one. Without this leg the step above passes against a script that + # lists every group in SURFACE.txt and reads no artefact at all. + # `sed -i` reports success when it changes nothing, so the edit is + # asserted rather than assumed: an edit that silently missed would + # rebuild the same artefact and this leg would pass for the one + # reason it exists to rule out. + sed -i 's/^int kal_stream_flush/int kal_stream_flush_removed/' src/stream.cpp + grep -q 'kal_stream_flush_removed' src/stream.cpp || { + echo "the edit that removes one definition did not apply"; exit 1 + } + rm -rf target + mcpp build > /dev/null + objs="$(find target -name '*.o' | tr '\n' ' ')" + bash ../../../tools/check-surface.sh --interfaces \ + ../../../SURFACE.txt $objs > partial.txt || true + if grep -qx 'openkal.stream' partial.txt; then + echo "half an interface was reported as provided" + cat partial.txt; exit 1 + fi + git checkout -- src/stream.cpp + # --------------------------------------------------------------------------- # The suite, against the implementation for each system. # diff --git a/README.md b/README.md index 7420082..c110d34 100644 --- a/README.md +++ b/README.md @@ -179,6 +179,42 @@ Clause 9 has two halves, and both are here. names against `SURFACE.txt`. It detects the one freedom an implementation retains after the language has removed the others: the addition of names. +**Which interfaces an implementation provides, derived rather than declared.** +`tools/check-surface.sh --interfaces` prints the interfaces the artefact exports +whole; `--toml` prints them as the array a package manifest carries: + +```bash +bash tools/check-surface.sh --toml SURFACE.txt $(find target -name '*.o') +``` + +```toml +provides-interfaces = [ + "openkal.abort", + "openkal.stream", + "openkal.memory", +] +``` + +It is a mode of the surface comparison rather than a second script because it is +that comparison stopped one step earlier: clause 9 already walks `SURFACE.txt` +group by group and decides, for each, whether the artefact exports it whole, in +part, or not at all. A second derivation of the same walk would go stale the +first time a group was added. + +A package's `provides-interfaces` is therefore generated from the artefact and +not written by hand. A declaration derived from the thing it describes cannot +disagree with it, and an implementation that gains an interface cannot forget to +say so. A group exported in part is not listed: an interface is provided in whole +or not at all (clause 3), so half of one is not a smaller claim but a different +and false one. + +A build tool reads that array at dependency resolution, against the +`requires-interfaces` a consumer states in its own package, and refuses a +combination before anything is compiled. That is the first of the three times +clause 6.2 tabulates, and the earliest at which the question can be answered — +source that asks the same question with `#ifdef` asks it during preprocessing, +which is earlier than any answer exists. + **The behaviour.** [`conformance/`](conformance/) is a program an implementation runs against itself — 193 observations across fifteen interfaces, in four kinds: behaviour, ABI, stability and cost. diff --git a/tools/check-surface.sh b/tools/check-surface.sh index ff5305e..5159e22 100755 --- a/tools/check-surface.sh +++ b/tools/check-surface.sh @@ -6,16 +6,43 @@ # incomplete coverage, and it detects the one freedom an implementation retains # after the language has removed the others: the addition of names. # -# check-surface.sh [--complete] ... +# check-surface.sh [--complete] [--interfaces|--toml] ... # # Without --complete, an absent name denotes an interface the implementation # does not provide, which clause 3 permits. With --complete, every name in the # list is required, which is what an implementation claiming the whole # specification asserts. +# +# --interfaces WRITES THE ANSWER THE COMPARISON ALREADY REACHES, AND THAT IS +# WHY IT IS A MODE OF THIS SCRIPT RATHER THAN A SECOND ONE. Clause 9's surface +# comparison walks SURFACE.txt group by group and decides, for each, whether +# the artefact exports it whole, in part, or not at all. "Which interfaces does +# this implementation provide" is that same walk, stopped one step earlier. +# Deriving it anywhere else would be the same decision written twice, and the +# copy would go stale the first time a group was added. +# +# --interfaces prints one interface name per line. --toml prints the array a +# manifest carries, so that a package's `[kernel-abi] provides-interfaces` is +# GENERATED FROM THE ARTEFACT rather than written by hand: a declaration +# derived from the thing it describes cannot disagree with it, and a package +# that gains an interface cannot forget to say so. +# +# A group exported in PART is a defect under --complete and is reported as +# such; under --interfaces it is simply not listed, because an interface is +# provided in whole or not at all (clause 3) and half of one is not a smaller +# claim but a different, false one. set -euo pipefail complete=0 -if [ "${1:-}" = "--complete" ]; then complete=1; shift; fi +emit='' +while :; do + case "${1:-}" in + --complete) complete=1; shift ;; + --interfaces) emit=lines; shift ;; + --toml) emit=toml; shift ;; + *) break ;; + esac +done list="${1:?usage: check-surface.sh [--complete] ...}" shift @@ -93,6 +120,57 @@ done <<< "$found" # implementation does not provide and is not a deviation". A group none of whose # names is exported is an interface not provided. A group SOME of whose names # are exported is the thing this check exists to catch: half an interface. +# --interfaces / --toml: the same group walk, reporting which interfaces the +# artefact provides WHOLE. Written before the --complete block so that a caller +# asking for both gets the list and the verdict from one reading of the list. +if [ -n "$emit" ]; then + provided='' + group=''; want='' + emit_group() { + [ -n "$group" ] && [ -n "$want" ] || return 0 + # `openkal.version` is not an interface (SURFACE.txt says so in its own + # header: it provides no resource). Every conforming implementation + # exports it, so listing it would put a name in every package's + # declaration that answers nothing. + [ "$group" != "openkal.version" ] || return 0 + local present=0 absent=0 + while read -r name; do + [ -n "$name" ] || continue + if grep -qxF -- "$name" <<< "$found"; then present=$((present+1)) + else absent=$((absent+1)); fi + done <<< "$want" + if [ "$present" -gt 0 ] && [ "$absent" -eq 0 ]; then + provided="$provided$group +" + fi + } + while IFS= read -r line; do + case "$line" in + # The heading may carry prose after the name --- SURFACE.txt's + # `openkal.version` row explains there why it is spelled as a group + # and is not an interface --- so the name is the first word of it + # and not the rest of the line. + '# openkal.'*) emit_group; group="${line#\# }"; group="${group%% *}"; want='' ;; + '#'*|'') ;; + *) want="$want$line +" ;; + esac + done < "$list" + emit_group + if [ -z "$provided" ]; then + echo "no interface is exported whole; refusing to write an empty declaration" >&2 + exit 1 + fi + if [ "$emit" = toml ]; then + echo "provides-interfaces = [" + while read -r g; do [ -n "$g" ] && printf ' "%s",\n' "$g"; done <<< "$provided" + echo "]" + else + printf '%s' "$provided" + fi + exit 0 +fi + if [ "$complete" -eq 1 ]; then group=''; want='' check_group() { From de92cf4bd28065ef02b4f51f01866e2b41fb0a67 Mon Sep 17 00:00:00 2001 From: speak-agent Date: Sun, 20 Sep 2026 18:55:08 +0800 Subject: [PATCH 2/3] the interface step builds clean, because the step before it leaves an object behind The step that requires the surface checker to reject an unspecified name removes `src/extra.cpp` and not the object it produced, so a `find` over `target/` still reports `kal_vendor_extension` and the next step examines an artefact no source in the tree describes. It now starts from a clean build, and refuses to run against an empty object list. Co-authored-by: Claude Code --- .github/workflows/ci.yml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3714f70..0e125a0 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -581,8 +581,14 @@ jobs: # answers "which interfaces does this implementation provide". This # step asserts that the answer comes from the artefact and moves with # it. - mcpp build > /dev/null + # FROM A CLEAN BUILD. The step before this one introduces an + # unspecified name, requires the checker to reject it, and removes + # the source -- without removing the object it produced. A `find` + # over `target/` therefore still reports that name, and this step + # would be examining an artefact no source in the tree describes. + rm -rf target && mcpp build > /dev/null objs="$(find target -name '*.o' | tr '\n' ' ')" + [ -n "$objs" ] || { echo "no objects to examine"; exit 1; } bash ../../../tools/check-surface.sh --interfaces \ ../../../SURFACE.txt $objs > provided.txt grep -qx 'openkal.stream' provided.txt || { From 0d0b120f6b1b8e3c5c7e044dd06c2d75fdf12098 Mon Sep 17 00:00:00 2001 From: speak-agent Date: Sun, 20 Sep 2026 19:16:34 +0800 Subject: [PATCH 3/3] the interface step measures a synthetic artefact, because impl-fd claims nothing impl-fd exists to show substitution, not conformance: it defines six of openkal.stream's seven names and none of any other group, so no interface is exported whole and every leg of the step was measuring an implementation that claims nothing --- which is why it reported 'no interface is exported whole' rather than a list. The subject is now an object built from SURFACE.txt in the step, with three groups whole and two names of a fourth. The answer is known in advance, which is what lets the check fail for the one reason it exists to catch: a group exported in part must not be listed, because an interface is provided in whole or not at all. Co-authored-by: Claude Code --- .github/workflows/ci.yml | 94 ++++++++++++++++++++++------------------ 1 file changed, 53 insertions(+), 41 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 0e125a0..7a2a4c0 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -574,57 +574,69 @@ jobs: - name: The interface list is derived from the artefact working-directory: examples/substitution/impl-fd run: | + set -euo pipefail # `provides-interfaces` in a package manifest is a declaration, and a # declaration is checked rather than trusted. The check available to - # it is clause 9's surface comparison, stopped one step earlier: the + # it is clause 9's surface comparison stopped one step earlier: the # walk that decides whether each group is exported whole already - # answers "which interfaces does this implementation provide". This - # step asserts that the answer comes from the artefact and moves with - # it. - # FROM A CLEAN BUILD. The step before this one introduces an - # unspecified name, requires the checker to reject it, and removes - # the source -- without removing the object it produced. A `find` - # over `target/` therefore still reports that name, and this step - # would be examining an artefact no source in the tree describes. - rm -rf target && mcpp build > /dev/null - objs="$(find target -name '*.o' | tr '\n' ' ')" - [ -n "$objs" ] || { echo "no objects to examine"; exit 1; } + # answers which interfaces an implementation provides. + # + # THE SUBJECT IS A SYNTHETIC OBJECT BUILT FROM SURFACE.txt, AND NOT + # THIS EXAMPLE. `impl-fd` exists to show substitution, not + # conformance: it defines six of openkal.stream's seven names and + # none of the other groups, so no interface is exported whole and + # every leg below would be measuring an implementation that claims + # nothing. The object here is constructed so that the answer is known + # in advance, which is what lets the check fail for the one reason it + # exists to catch. + python3 - ../../../SURFACE.txt > fake.c <<'PY' + import sys + groups, cur = {}, None + for line in open(sys.argv[1], encoding='utf-8'): + line = line.rstrip('\n') + if line.startswith('# openkal.'): + cur = line[2:].split(' ')[0]; groups[cur] = [] + elif line.startswith('#') or not line.strip(): + continue + elif cur: + groups[cur].append(line.strip()) + # Three groups whole, and two names of a fourth: an interface is + # provided in whole or not at all, so the fourth must not be listed. + for g in ('openkal.version', 'openkal.abort', 'openkal.stream', 'openkal.memory'): + for n in groups.get(g, []): + print(f'int {n}(void);\nint {n}(void) {{ return 0; }}') + for n in groups.get('openkal.fs', [])[:2]: + print(f'int {n}(void);\nint {n}(void) {{ return 0; }}') + PY + cc -c fake.c -o fake.o bash ../../../tools/check-surface.sh --interfaces \ - ../../../SURFACE.txt $objs > provided.txt - grep -qx 'openkal.stream' provided.txt || { - echo "the implementation exports openkal.stream whole and it was not listed" - cat provided.txt; exit 1 - } + ../../../SURFACE.txt fake.o > provided.txt + cat provided.txt + + for want in openkal.abort openkal.stream openkal.memory; do + grep -qx "$want" provided.txt || { + echo "::error::$want is exported whole and was not listed"; exit 1; } + done # `openkal.version` is exported by every conforming implementation # and is not an interface --- SURFACE.txt says so in its own header. # Listing it would put a name that answers nothing in every package. if grep -qx 'openkal.version' provided.txt; then - echo "openkal.version is not an interface and must not be listed"; exit 1 + echo "::error::openkal.version is not an interface and must not be listed"; exit 1 fi - - # REMOVE ONE DEFINITION AND THE INTERFACE MUST LEAVE THE LIST. An - # interface is provided in whole or not at all (clause 3), so a group - # exported in part is not a smaller claim but a different and false - # one. Without this leg the step above passes against a script that - # lists every group in SURFACE.txt and reads no artefact at all. - # `sed -i` reports success when it changes nothing, so the edit is - # asserted rather than assumed: an edit that silently missed would - # rebuild the same artefact and this leg would pass for the one - # reason it exists to rule out. - sed -i 's/^int kal_stream_flush/int kal_stream_flush_removed/' src/stream.cpp - grep -q 'kal_stream_flush_removed' src/stream.cpp || { - echo "the edit that removes one definition did not apply"; exit 1 - } - rm -rf target - mcpp build > /dev/null - objs="$(find target -name '*.o' | tr '\n' ' ')" - bash ../../../tools/check-surface.sh --interfaces \ - ../../../SURFACE.txt $objs > partial.txt || true - if grep -qx 'openkal.stream' partial.txt; then - echo "half an interface was reported as provided" - cat partial.txt; exit 1 + # HALF AN INTERFACE IS NOT A SMALLER CLAIM. Without this leg the + # checks above pass against a script that prints every group in + # SURFACE.txt and reads no artefact at all. + if grep -qx 'openkal.fs' provided.txt; then + echo "::error::a group exported in part was reported as provided"; exit 1 fi - git checkout -- src/stream.cpp + # And the --toml spelling is the same answer in the shape a manifest + # carries, because a package's declaration is generated from it. + bash ../../../tools/check-surface.sh --toml \ + ../../../SURFACE.txt fake.o > provided.toml + grep -qx 'provides-interfaces = \[' provided.toml + grep -qx ' "openkal.stream",' provided.toml + rm -f fake.c fake.o provided.txt provided.toml + echo " ok the list is the artefact's own answer" # --------------------------------------------------------------------------- # The suite, against the implementation for each system.