Give each restated rule one owner

.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-<feature>.c` and use the shared harness macros
 rather than rolling their own reporting.

.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.

.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
@@ -71,12 +72,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
@@ -97,10 +98,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

.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
 
@@ -161,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.
@@ -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`

.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`,
@@ -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.