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-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-refactor/SKILL.md b/.claude/skills/elfuse-refactor/SKILL.md index 04c178be..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 @@ -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 diff --git a/.claude/skills/elfuse-security/SKILL.md b/.claude/skills/elfuse-security/SKILL.md index 0512fcf2..1961a3a8 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 @@ -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` diff --git a/.claude/skills/elfuse-syscall/SKILL.md b/.claude/skills/elfuse-syscall/SKILL.md index 61cb2348..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`, @@ -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.