From 04216e766c12ee74857c8c6f33d196e6d2e975e3 Mon Sep 17 00:00:00 2001 From: alanhc Date: Thu, 3 Sep 2026 20:41:50 +0800 Subject: [PATCH 1/5] State three shared facts once Three facts were written out in two skills each, in the shape the register warns about: a rule copied to a second place is a rule that can drift. Each now sits with the skill that owns the mechanism, and the second site names that skill. The GDB stub's refusal of x86_64 belongs beside the flag it refuses, in elfuse-debug. What check-atomics.py cannot see belongs with the atomics rules in elfuse-conventions. That a proof binds the arithmetic and not its callers belongs with the proofs in elfuse-verify, which also carries what narrows it. The security skill keeps the judgment each one supports, since a review priority is not the fact it rests on. --- .claude/skills/elfuse-guest-abi/SKILL.md | 4 ++-- .claude/skills/elfuse-security/SKILL.md | 16 +++++++--------- 2 files changed, 9 insertions(+), 11 deletions(-) diff --git a/.claude/skills/elfuse-guest-abi/SKILL.md b/.claude/skills/elfuse-guest-abi/SKILL.md index b347a33f..f6dc540c 100644 --- a/.claude/skills/elfuse-guest-abi/SKILL.md +++ b/.claude/skills/elfuse-guest-abi/SKILL.md @@ -272,8 +272,8 @@ mappings and register state, and the ways it breaks are mapping-shaped. - For dynamic x86_64 guests the host deliberately does not load segments or the interpreter. The translator reads PT_INTERP itself and mmaps the loader out of `--sysroot` through ordinary guest syscalls. -- The GDB stub is rejected for x86_64 because it would serve the translated - aarch64 view rather than the state the guest believes it has. +- The GDB stub is rejected for x86_64. `elfuse-debug` carries the reason, + beside the invocation it refuses. `docs/internals.md` section "x86_64-via-Apple-Rosetta" has the mechanism, and `docs/testing.md` has the per-host baselines the x86_64 lane compares against. diff --git a/.claude/skills/elfuse-security/SKILL.md b/.claude/skills/elfuse-security/SKILL.md index 0512fcf2..ad367dde 100644 --- a/.claude/skills/elfuse-security/SKILL.md +++ b/.claude/skills/elfuse-security/SKILL.md @@ -63,10 +63,9 @@ Cost: an out-of-bounds write that reproduces only at boundary values, which is the region hand-written tests skip. New arithmetic on a guest-chosen length belongs in `src/proved/` behind a contract, not inline. -A contract there proves the arithmetic and not its callers: they sit outside -`-wp-fct`, and for `proved/gva.h` they cannot be brought in at all, since -Frama-C does not parse `src/core/guest.c`. `elfuse-verify` carries that limit, -and it leaves the call site a review question rather than a proved one. +A contract there proves the arithmetic and not its callers, so the call site +stays a review question rather than a proved one. `elfuse-verify` carries the +limit and what narrows it from the runtime side. ### Indexes @@ -206,11 +205,10 @@ Under `make check`: restart behavior is unstated. - `scripts/check-atomics.py` fails a C11 atomic operation written without the `_explicit` form, and bans the compiler builtins, so the order is written at - the site. Its docstring names what it deliberately leaves out: plain-operator - access to an `_Atomic` object, which needs per-translation-unit declarations - and which the tree already carries a large set of. That half is a review - question, so it is the one memory-order case to spend budget on rather than - skip. + the site. What its docstring leaves out is a review question rather than a + gap to skip, and it is the memory-order case worth the budget; + `elfuse-conventions` states which access it cannot see and why a regex + cannot close it. - `scripts/check-svc-tails.py` holds every return tail to the X7 ptrace test, bar the one exception its docstring names and allowlists. - `scripts/check-syscall-coverage.py` is a best-effort audit of `dispatch.tbl` From 67e7d7a5174e10a5bf612d263dd4445840606c4a Mon Sep 17 00:00:00 2001 From: alanhc Date: Thu, 3 Sep 2026 20:42:26 +0800 Subject: [PATCH 2/5] Give the lock ordering record one owner Four skills told a contributor to record a new lock, and only one of them carried what the record actually holds. elfuse-syscall states where it lives and the three constraints that do not follow from the ordering itself, so it keeps the rule. The other three name it instead of restating it. The security skill also said it twice on its own, once in the shared-pages rule and once in the gate list beneath, where check-lock-order.py is what fails the omission. --- .claude/skills/elfuse-conventions/SKILL.md | 7 ++++--- .claude/skills/elfuse-refactor/SKILL.md | 12 ++++++------ .claude/skills/elfuse-security/SKILL.md | 6 +++--- 3 files changed, 13 insertions(+), 12 deletions(-) diff --git a/.claude/skills/elfuse-conventions/SKILL.md b/.claude/skills/elfuse-conventions/SKILL.md index 05b11a63..bc422a4c 100644 --- a/.claude/skills/elfuse-conventions/SKILL.md +++ b/.claude/skills/elfuse-conventions/SKILL.md @@ -233,9 +233,10 @@ a `bool`; a helper that forwards a page-table or syscall primitive's status should stay `int`. New code goes in the existing domain file, not a new one. New shared -declarations go in the domain's `internal.h` or an existing header. A new lock -is documented in the lock-order comment before it is used from a second -module. +declarations go in the domain's `internal.h` or an existing header, and a new +lock reaches the ordering record; `elfuse-syscall` locates that record, says +when a lock enters it, and names the three constraints in it that the +ordering alone does not give. New C tests are `tests/test-.c` and use the shared harness macros rather than rolling their own reporting. diff --git a/.claude/skills/elfuse-refactor/SKILL.md b/.claude/skills/elfuse-refactor/SKILL.md index 04c178be..7525b637 100644 --- a/.claude/skills/elfuse-refactor/SKILL.md +++ b/.claude/skills/elfuse-refactor/SKILL.md @@ -71,12 +71,12 @@ lanes are reachability paths. ## Preserve the boundaries -- A helper that acquires a lock changes lock order at every caller. The lock - order comment in `src/syscall/internal.h` is the contract. A helper that - releases one, or drops and retakes it, is the same hazard read backwards, and - the name has to carry it: `_locked` already means "call me holding it", so a - helper that hands the lock back needs a different suffix and a comment saying - the caller must not touch that lock again. +- A helper that acquires a lock changes lock order at every caller, against + the record `elfuse-syscall` reads. A helper that releases one, or drops and + retakes it, is the same hazard read backwards, and the name has to carry it: + `_locked` already means "call me holding it", so a helper that hands the + lock back needs a different suffix and a comment saying the caller must not + touch that lock again. - Moving an interruptible wait into a helper moves its restart classification. `scripts/check-eintr-contract.py` keys on the function that decides, not the syscall that returns, so the new helper takes the inventory entry and the diff --git a/.claude/skills/elfuse-security/SKILL.md b/.claude/skills/elfuse-security/SKILL.md index ad367dde..1961a3a8 100644 --- a/.claude/skills/elfuse-security/SKILL.md +++ b/.claude/skills/elfuse-security/SKILL.md @@ -160,9 +160,9 @@ than a crash at the guilty line. A guest value read twice is two values. Copy the structure in once, validate the copy, then use only the copy; validating in place and passing the original address on is the double fetch, and shared memory makes it reachable without -timing luck. A new file-scope lock goes into the ordering block at the top of -`src/syscall/internal.h` in the same change. State the memory order at every -shared access. +timing luck. A new file-scope lock enters the ordering record in the same +change, which the gate below fails for being missing. State the memory order +at every shared access. Cost: a double fetch is not a race the guest has to win. It re-runs the syscall until the two reads differ, so the window is as wide as it needs to be. From a8dec007b712ab30f1457363900d7318dbfc7758 Mon Sep 17 00:00:00 2001 From: alanhc Date: Thu, 3 Sep 2026 20:42:47 +0800 Subject: [PATCH 3/5] Route the validation table through one skill The change-area-to-command table in docs/testing.md was named and glossed in three skills. elfuse-verify opens on it and says what a failure in each lane means, so the other two ask it rather than restating the pointer. Both keep what they add: a cleanup earns the feature's command set rather than a smaller one, and a syscall change hands a failure to elfuse-debug. The tracked section stays in the authoritative sources list, which is where a skill names a file it defers to. --- .claude/skills/elfuse-refactor/SKILL.md | 7 +++---- .claude/skills/elfuse-syscall/SKILL.md | 7 +++---- 2 files changed, 6 insertions(+), 8 deletions(-) diff --git a/.claude/skills/elfuse-refactor/SKILL.md b/.claude/skills/elfuse-refactor/SKILL.md index 7525b637..68ad4d87 100644 --- a/.claude/skills/elfuse-refactor/SKILL.md +++ b/.claude/skills/elfuse-refactor/SKILL.md @@ -97,10 +97,9 @@ is not enough: the two bodies must represent the same fact. ## Work in small, evidenced steps -Read `docs/testing.md`, section "Validation Strategy By Change Type", and run -the selected baseline before a multi-step cleanup. Keep inherited failures -separate from the change. Stop when the baseline is red in the area being -changed. +Run the baseline `elfuse-verify` selects for the area touched before a +multi-step cleanup. Keep inherited failures separate from the change. Stop +when the baseline is red in the area being changed. A failure blamed on the environment earns one reproduction attempt under the condition blamed for it before it is written off. "Transient" and "the host was diff --git a/.claude/skills/elfuse-syscall/SKILL.md b/.claude/skills/elfuse-syscall/SKILL.md index 61cb2348..cacd893f 100644 --- a/.claude/skills/elfuse-syscall/SKILL.md +++ b/.claude/skills/elfuse-syscall/SKILL.md @@ -212,7 +212,6 @@ so prefer them when the two disagree: ## Verifying -`docs/testing.md`, section "Validation Strategy By Change Type", maps the area -you touched to the minimum command set. Use it rather than a habit; see -`elfuse-verify` for what the lanes mean and `elfuse-debug` for localizing a -failure in one. +`elfuse-verify` maps the area you touched to the minimum command set, which is +more specific than a habit, and says what a failure in each lane means. +`elfuse-debug` localizes a failure inside one. From 0a7c009be94cab16aa1f271483f14680daddbc96 Mon Sep 17 00:00:00 2001 From: alanhc Date: Thu, 3 Sep 2026 20:43:40 +0800 Subject: [PATCH 4/5] Report a run from one set of rules Three rules about reporting a run were written in both elfuse-verify and elfuse-refactor: recompute a number rather than quoting it from a document, take the baseline before a session rather than after, and name a lane that could not run instead of rounding it up. elfuse-verify has the section that decides what done means, so it keeps all three. The refactor skill keeps what only it can say: the one-liners that measure this tree, and which of its reds a cleanup inherits rather than causes. It also stated the lint red twice on its own, once where the gates are measured and once in the same paragraph as the baseline. --- .claude/skills/elfuse-refactor/SKILL.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/.claude/skills/elfuse-refactor/SKILL.md b/.claude/skills/elfuse-refactor/SKILL.md index 68ad4d87..c7a28761 100644 --- a/.claude/skills/elfuse-refactor/SKILL.md +++ b/.claude/skills/elfuse-refactor/SKILL.md @@ -29,8 +29,9 @@ that both moves code and changes behavior cannot be reviewed as either. Measure it first. `references/measuring.md` carries the scans for function size, duplication, and nesting, and the traps in reading each. Report a number -with the command that produced it and a judgment as a judgment; never quote a -count from a document, this one included. +with the command that produced it and a judgment as a judgment; `elfuse-verify` +carries the rest of that rule, this file included among the documents a count +must not be quoted from. Prefer deletion, an existing local helper, or a direct rewrite over a new abstraction. A parameter every caller gives the same value, a hook with one From a7f6cac4dda02340dc4555ffc90671bac3b3b466 Mon Sep 17 00:00:00 2001 From: alanhc Date: Thu, 3 Sep 2026 20:44:16 +0800 Subject: [PATCH 5/5] Ask where a new declaration goes once Both skills answered it. elfuse-conventions owns where a file, a type, and a shared declaration may go, and it is the skill a contributor reaches for that question; the syscall procedure asks it there rather than repeating the answer mid-step. What stays in the procedure is the part specific to it: which domain file a sys_ implementation belongs in, and the three examples that make the naming legible. --- .claude/skills/elfuse-syscall/SKILL.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.claude/skills/elfuse-syscall/SKILL.md b/.claude/skills/elfuse-syscall/SKILL.md index cacd893f..9a98e0bc 100644 --- a/.claude/skills/elfuse-syscall/SKILL.md +++ b/.claude/skills/elfuse-syscall/SKILL.md @@ -59,8 +59,8 @@ rules for handling one it chose badly are `elfuse-security`. 3b. The `sys_` implementation goes in the domain file whose name says so: `ls src/syscall/` is the list, and read/write/ioctl in `io.c`, brk/mmap/mprotect in `mem.c`, sockets in the `net*.c` family are - representative. New code goes in the existing domain file; shared - declarations go in `internal.h`, not a new header. + representative. `elfuse-conventions` settles where a new file or a new + shared declaration may go, and the answer is almost never a new one. Two domains sit outside `src/syscall/` because they are runtime state rather than syscall surface: clone and fork in `src/runtime/forkipc.c`,