From aa6345e18489d1e38c6cfc53f730adfd56f018f7 Mon Sep 17 00:00:00 2001 From: Jim Huang Date: Wed, 30 Sep 2026 01:35:04 +0800 Subject: [PATCH 1/5] Correct the claims the skill files outgrew The skills drift in ways check-skill-refs cannot see. It resolves paths, targets and section anchors, so a wrong count, a stale enumeration or a banned identifier passes it untouched. elfuse-guest-abi named the __ATOMIC_* order constants for calls the source writes as atomic_fetch_or_explicit and atomic_fetch_and_explicit. check-atomics rejects that spelling, so an agent following the skill wrote code the build refuses. The same file omitted HVC 13 and the X7 ptrace request, and said the shim_data cache decides whether a syscall takes HVC 5 at all rather than whether a call with an EL1 fast path can skip one. Its list of those paths stopped at identity and urandom; the shim also serves getpgid(0), getsid(0), getrandom and two futex shapes inline, and gettid reads CONTEXTIDR_EL1 rather than a cached slot. usbdevfs had no coverage anywhere: the second largest source file in the tree, two make check gates, a generated ioctl table and four lock-ordering entries, reachable from no skill and no routing row. It now has a bullet in elfuse-syscall and an entry in the elfuse-security boundary list. elfuse-verify pinned six counts inside the bullet that tells the reader to recompute counts, called only a minority of src parsable when most of it parses, listed sys/sysctl.h among the headers no stub can supply beside the stub the tree carries for it, and described check-proof-targets as a CI job when make check runs it too. It also told the reader every scanner runs with no arguments, which for the generator behind check-usbdev-departed writes its header. Two skills restated a source comment in the sentence that cited it, and both copies had already diverged from it. They cite it now. The frama-c MCP material moves to references/frama-c-mcp.md. It was 291 of 738 lines behind a conditional most triggers never take, and a body is a cost paid every time the skill fires. --- .claude/skills/elfuse-conventions/SKILL.md | 21 +- .claude/skills/elfuse-debug/SKILL.md | 7 +- .claude/skills/elfuse-guest-abi/SKILL.md | 38 +- .claude/skills/elfuse-security/SKILL.md | 17 +- .claude/skills/elfuse-syscall/SKILL.md | 23 +- .claude/skills/elfuse-verify/SKILL.md | 364 ++++-------------- .../elfuse-verify/references/frama-c-mcp.md | 293 ++++++++++++++ 7 files changed, 437 insertions(+), 326 deletions(-) create mode 100644 .claude/skills/elfuse-verify/references/frama-c-mcp.md diff --git a/.claude/skills/elfuse-conventions/SKILL.md b/.claude/skills/elfuse-conventions/SKILL.md index 08228a69..8f1d7e45 100644 --- a/.claude/skills/elfuse-conventions/SKILL.md +++ b/.claude/skills/elfuse-conventions/SKILL.md @@ -130,10 +130,9 @@ coverage. Both fail rather than skip when their tool is missing. `make indent` is a no-op on a clean tree, in both halves: every file clang-format selects already formats to itself, and every file commentflow selects already -reflows to itself. That was not free. The tree's comments were wrapped by hand -before the tool existed, and the one-time reflow rewrote 142 of the 353 C and -header files, both assembly files, and 36 of the 41 shell scripts. It landed as -its own commit, under the rule the commit section states. +reflows to itself. The tree's comments were wrapped by hand before the tool +existed, and the one-time reflow landed as its own commit, under the rule the +commit section states. The gate is what keeps it a no-op. If `make indent` ever hands you a diff in a file you did not touch, something reintroduced hand-wrapping, or your @@ -169,8 +168,8 @@ is a sequentially-consistent read-modify-write, and a site already holding the lock that serializes it pays for ordering it does not need while saying nothing about the ordering it does. Where a file has many such sites, name the discipline once in helpers rather than spelling the order out at each: the -`pending_load` / `pending_or` / `pending_clear` group at the top of -`src/syscall/signal.c` is the shape. +`pending_load` / `pending_or` / `pending_clear` group in +`src/syscall/signal.h` is the shape. Never hand an `_Atomic` object to `memcpy` or to a guest read/write helper. That copies the object representation, which is not an atomic read of it. Load into a @@ -265,9 +264,13 @@ flag, or helper is named for its operation, not the manner. Not in `src/`: attribution, dates, commented-out code, issue-tracker numbers (barred from `docs/` and README prose too, PR#40, PR#223; they belong in a -commit trailer), or `TODO`/`FIXME`; incomplete work belongs in the commit -message or PR. Editing part of a comment re-opens all of it: re-read the -block and rewrite what no longer reads cleanly. +commit trailer), or a bare `TODO`/`FIXME`; incomplete work belongs in the +commit message or PR. `CONTRIBUTING.md` carries the marker rule, which asks a +`TODO` to say what remains and to carry an all-caps owner ahead of the word +when one applies. What `src/` writes instead is the stage or the condition the +work waits on, as a parenthesis (`grep -rn 'TODO(' src/`). Editing part of a +comment re-opens all of it: re-read the block and rewrite what no longer reads +cleanly. Mechanics: `/* */` only in `.c`, `.h`, and `.S`, no `//`, no Doxygen tags; multi-line blocks align on ` * `, close with `*/` on its own line, indented diff --git a/.claude/skills/elfuse-debug/SKILL.md b/.claude/skills/elfuse-debug/SKILL.md index 214e2423..b20c5923 100644 --- a/.claude/skills/elfuse-debug/SKILL.md +++ b/.claude/skills/elfuse-debug/SKILL.md @@ -32,6 +32,7 @@ classification is the first bisection, and it is free: | `CRASH_UNEXPECTED_HVC` / `CRASH_UNEXPECTED_EC` | The shim and the host dispatcher disagree about the protocol. Usually a half-landed HVC change. | | `CRASH_HV_CHECK` | Hypervisor.framework refused a call. Host-side: a mapping or permission elfuse asked for is not one HVF allows. | | `CRASH_ELR_ZERO` | Register state after exec is not what the host wrote. A return-to-EL0 path problem, not a loader problem. | +| `CRASH_UNEXPECTED_EXIT` | `hv_vcpu_run()` returned an exit reason the loop does not handle. Host-side: HVF or the run loop, not the guest. | | `CRASH_TIMEOUT` | One `hv_vcpu_run()` iteration exceeded the `--timeout` watchdog. | `CRASH_TIMEOUT` is the one that gets misread. The watchdog bounds a single run @@ -198,6 +199,8 @@ so prefer them when the two disagree: `--timeout`, `--fakeroot`, and `ELFUSE_FAKEROOT_EXEC`. - `docs/internals.md`, section "GDB Stub" - the snapshot protocol and the `src/debug/` split. -- The header comments in `src/core/startup-trace.h`, `src/debug/syscall-hist.h`, - and `src/debug/crashreport.h` - each states its env var's accepted values and +- The header comments in `src/core/startup-trace.h` and + `src/debug/syscall-hist.h` - each states its env var's accepted values and what it costs when disabled. +- `src/debug/crashreport.h` for the crash-type enum and the report layout. + The report is unconditional. diff --git a/.claude/skills/elfuse-guest-abi/SKILL.md b/.claude/skills/elfuse-guest-abi/SKILL.md index 94d743ef..c673d9a4 100644 --- a/.claude/skills/elfuse-guest-abi/SKILL.md +++ b/.claude/skills/elfuse-guest-abi/SKILL.md @@ -43,9 +43,13 @@ Only `bad_exception` vectors may clobber X5, because they halt. | #12 | System instruction trap | cache maintenance logging | | #13 | Ptrace stop | taken after the shim restores the HVC #5 saved frame | -The register contract per HVC, including which return values each one accepts, -is the header comment in `src/core/shim.S`. That comment is the specification; -this table is an index into it. +The register contract per shim HVC, including which return values each one +accepts, is the header comment in `src/core/shim.S`. That comment is the +specification; this table is an index into it. HVC #6 is the exception: it +never reaches the shim, so the header does not list it. Its contract is the +`hvc6_handler` comment in `src/core/guest.h`, which names both routes into it; +they are dispatched from `case 6` in `src/syscall/proc.c` and from the private +pseudo-syscall in `src/syscall/syscall.c`. Changing the protocol is never a one-file change. The shim, the host dispatcher, the crash and debug paths that decode HVCs, and the documentation @@ -208,11 +212,20 @@ Two rules survive any layout change: ## shim_data integrity shim_data is `MEM_PERM_RW_EL1_ONLY` and holds a host-published cache the EL1 -shim serves inline: identity slots (pid/ppid/uid/euid/gid/egid/tid), the -urandom-eligible fd bitmap, a urandom ring, and an attention bitmask -(`ATTN_BIT_SIGTIMER`, `ATTN_BIT_CRED`, `ATTN_BIT_TRACE`). HVC #5 is taken only -when attention is raised, the fd is not in the bitmap, or the ring needs a -refill. +shim serves inline: identity slots (pid/ppid/uid/euid/gid/egid, plus pgid +and sid), per-bucket futex waiter counts, the urandom-eligible fd bitmap, a +urandom ring, and an attention bitmask +(`ATTN_BIT_SIGTIMER`, `ATTN_BIT_CRED`, `ATTN_BIT_TRACE`, `ATTN_BIT_PTRACE`; +`src/core/shim-globals.h` is the list). This governs the inline fast paths +only: the identity calls, getpgid(0) and getsid(0), read on a urandom fd, +getrandom, a futex wait whose word moves during the EL1 spin (answered EAGAIN, +or EFAULT when the word cannot be read), and a futex wake whose bucket holds +no waiter (answered 0). gettid needs no slot: it reads CONTEXTIDR_EL1, which +the host sets to the tid per vCPU. Every other syscall forwards as HVC #5, and +so does a fast-path call the shim cannot settle: attention raised, the fd not +in the urandom bitmap, the ring short, a futex word that still matches, a +bucket with a waiter. The dispatch and bail labels in `src/core/shim.S` are +the full list. Four things keep EL0 out of it, and a change that weakens any one of them is a guest-readable host cache: @@ -226,9 +239,12 @@ guest-readable host cache: - `/proc/self/maps` reports the span as PROT_NONE. Publishing into the cache is bracketed rather than ordered by luck: -`shim_globals_attn_or` (`__ATOMIC_SEQ_CST`) raises the attention bit before -the mutator's stores, so a weakly-ordered ARM64 reader cannot observe the -publish without the bit; the clear is `__ATOMIC_RELEASE`. +`shim_globals_attn_or` raises the attention bit before the mutator's stores +with `atomic_fetch_or_explicit(..., memory_order_seq_cst)`, so a +weakly-ordered ARM64 reader cannot observe the publish without the bit; +`shim_globals_attn_and` clears it with +`atomic_fetch_and_explicit(..., memory_order_release)`. Both are C11; the +atomics rule and its gate are `elfuse-conventions`. ## Stack construction diff --git a/.claude/skills/elfuse-security/SKILL.md b/.claude/skills/elfuse-security/SKILL.md index 0512fcf2..2e0d82c7 100644 --- a/.claude/skills/elfuse-security/SKILL.md +++ b/.claude/skills/elfuse-security/SKILL.md @@ -25,7 +25,7 @@ which lanes prove it. ## Where the boundary runs -Five surfaces, ordered by what one bad value reaches: +The surfaces, ordered by what one bad value reaches: - Syscall arguments. X0-X5 and X8 arrive from EL0 with no host filter in front, so every wrapper reached from `src/syscall/dispatch.tbl` is on the @@ -34,12 +34,17 @@ Five surfaces, ordered by what one bad value reaches: translator, and the permission half is the security half. - Formats the host parses for the guest: the ELF the loader reads, netlink messages, FUSE frames, control messages, sigframes, sockaddrs, iovecs, - dirents. Each carries lengths, offsets, or counts the guest supplies, but - what the guest owns differs per format, so answer that per format rather - than assuming it. The ELF is read by offset, a sockaddr length arrives as a - separate syscall argument, and a sigframe is built by the host and then left - where the guest can rewrite it before `rt_sigreturn` reads it back. + dirents, and the usbdevfs URB structures (`usbdevfs_urb`, + `usbdevfs_ctrltransfer`, `usbdevfs_bulktransfer`). Each carries lengths, + offsets, or counts the guest supplies, but what the guest owns differs per + format, so answer that per format rather than assuming it. The ELF is read + by offset, a sockaddr length arrives as a separate syscall argument, and a + sigframe is built by the host and then left where the guest can rewrite it + before `rt_sigreturn` reads it back. - Paths. Every name the guest supplies, absolute ones included. +- Raw USB descriptor blobs, walked by `src/runtime/usb-desc.c`. The one + input here the guest does not author; the header comment in + `src/runtime/usb-desc.h` says why it is untrusted anyway. - Shared pages. The guest and the host see the same memory, so a structure validated in guest memory and then passed on by address was not validated. diff --git a/.claude/skills/elfuse-syscall/SKILL.md b/.claude/skills/elfuse-syscall/SKILL.md index aae739de..2a909a37 100644 --- a/.claude/skills/elfuse-syscall/SKILL.md +++ b/.claude/skills/elfuse-syscall/SKILL.md @@ -152,9 +152,9 @@ target. See the `elfuse-verify` skill. ## FDs and locks Guest fds are not host fds. Allocate through the bitmap allocator in -`fdtable.c`; classify with the helpers in `fd.c` and `fd.h` (socket, pidfd, -eventfd, timerfd, signalfd). A class check that reads the raw fd number is wrong after -a `dup`. +`fdtable.c`. The `FD_*` type constants live in `linux-wire.h`; the class +predicates live in `fd.c`, `fd.h` and `internal.h`. A class check that reads +the raw fd number is wrong after a `dup`. The lock order is the comment at the top of `internal.h`. Acquire in the order it lists, and add a new lock to that comment as soon as it exists, whether or @@ -169,7 +169,7 @@ the ordering: ## Subsystems with rules of their own -Three areas under `src/syscall/` are not ordinary domain files, and a change +Some areas under `src/syscall/` are not ordinary domain files, and a change that treats them as such tends to compile and then deadlock or leak: - FUSE (`fuse.c`) runs a whole filesystem transport inside the guest. Sessions @@ -185,6 +185,21 @@ that treats them as such tends to compile and then deadlock or leak: - Abstract Unix sockets, SCM_RIGHTS, and netlink each carry their own serialization format over guest-supplied lengths, which is why several of them have proof targets. +- usbdevfs (`usbdev.c`, with `src/runtime/usb-sysfs.c` and `usb-desc.c`): + `/dev/bus/usb/BBB/DDD` character devices over IOKit, asynchronous URBs, and + a synthetic `/sys/bus/usb` tree that goes through the same intercept layer + as procfs. Its locks do not nest the way the rest of the ordered list does, + and the `usbdev_table_lock` entry in `internal.h` is where that is written + down. The IOKit calls sit behind a COM seam, and `ELFUSE_USB_FIXTURE` stands + modeled devices in front of it so the fd contract runs with no hardware. A + device that answers a transfer needs both `ELFUSE_USB_FIXTURE=loopback` at + run time and a binary built with `USB_LOOPBACK_FIXTURE=1`: the env var picks + the device, the build flavor decides whether the fixture is linked in at all. + `mk/config.mk` owns the split and says why the two flavors write separate + binaries. + `scripts/gen-usbdev-ioctl-departed.py` generates + build/usbdev-ioctl-departed-vectors.h from + `tests/usbdev-ioctl-departed.tbl`: edit the table, not the header. `docs/internals.md` has a section for each. diff --git a/.claude/skills/elfuse-verify/SKILL.md b/.claude/skills/elfuse-verify/SKILL.md index f5bdbb90..c88eb4ce 100644 --- a/.claude/skills/elfuse-verify/SKILL.md +++ b/.claude/skills/elfuse-verify/SKILL.md @@ -23,20 +23,25 @@ a regression you can act on, and a serial re-run is the only thing that tells you whether it was real. The pure source scanners are the exception, and they are the cheap early -signal while something long is in flight: `check-lock-order`, -`check-eintr-contract`, `check-atomics`, `check-proof-targets`, -`check-stub-shadow` and `check-syscall-coverage` read the tree, cost seconds, -and fail long before a full lane would. Five of the six are on `make check`; -`check-stub-shadow` is a prerequisite of every `verify-*` target instead, so it -is not reached by `make check` alone. Running one directly with -`python3 scripts/.py` costs nothing and needs no arguments. - -Five of the six write nothing. `check-proof-targets` is the one that does: -it shells out to `make print-verify-targets` rather than reading -`mk/verify.mk`, and a sub-make evaluates the build-flavor guard while it reads -the makefiles. `print-%` goals are skipped by that guard for exactly this -reason (`mk/common.mk`), so the scanner is safe to run beside a build; if you -add a scanner that invokes make on some other goal, it is not. +signal while something long is in flight: they read the tree, cost seconds, +and fail long before a full lane would. The `check:` prerequisite line in +`mk/tests.mk` is the live roster; `check-stub-shadow` is the one that hangs +off every `verify-*` target instead, so `make check` alone does not reach it. +Beside a build in flight, run the script directly with the flags its recipe +passes, not through its make target: any goal outside `print-%` evaluates the +build-flavor guard (`mk/common.mk`), which can wipe a build made with other +CFLAGS. Read the recipe first. `scripts/gen-usbdev-ioctl-departed.py`, behind +`check-usbdev-departed`, is a generator that writes its header unless given +`--check`, and `make check-usbdev-departed` rebuilds that header under +`build/` when it is stale before comparing. + +None of them writes to the source tree. Three invoke make, each on a `print-%` +goal: `check-proof-targets` and `check-skill-refs` ask +`make print-verify-targets` for the proof list rather than reading +`mk/verify.mk`, and `check-usb-fixture-bin` asks for the binary path of both +build flavors. `print-%` goals skip the flavor guard, which is what keeps those +sub-makes safe beside a build. A scanner that invoked make on some other goal +would not be. ## Choosing what to run @@ -128,18 +133,16 @@ Apple's 3.81. `MUTANT_SINCE=` for a changed-only run, and `MUTANT_ESCALATE=` (see the exhaustion section below). -Read past the "N mutations, N caught" line. It also prints the proved functions -that have no mutation yet, and that list, not the caught count, is the honest -measure of what the gate covers: all-caught alongside a handful of functions -nobody has tried to break says the gate is green and that those proofs have -never been asked whether they would reject a broken source. They are not -failures, and they are not covered either. +Read past the "N mutations, N caught" line. It also reports two coverage gaps: +proved functions with no mutation under any target, and functions mutated +under one target but not another target that proves them. The first asks +whether a proved function has any mutation. The second asks whether each target +that proves an already-mutated function has its own mutation. Both matter +because targets can use different models and header environments, so a +mutation under one does not exercise another target's proof. These reports are +advisory, but each entry is uncovered under the metric that reports it. -Recompute that list before quoting it, and read what it counts. It counts -distinct functions now; it used to count `(target, function)` pairs, so a -function proved by two targets showed up twice and read as uncovered under its -second target even though the first mutates it. That inflated the gap fourfold -the last time it was checked - twelve listings, three functions. +Recompute both gaps before quoting them and name the denominator used. A function can also sit in a `_FCTS` list with no ACSL contract at all, proved only for absence of runtime errors. Nothing there can reject a mutation, so @@ -245,8 +248,9 @@ honest. ### Adding to src/proved/ Nothing lands there without a proof target - -`scripts/check-proof-targets.py` (a CI job in `.github/workflows/lint.yml`) -fails otherwise. Callers include the header as `proved/.h`. +`scripts/check-proof-targets.py`, run by `make check` and by +`.github/workflows/lint.yml`, fails otherwise. Callers include the header as +`proved/.h`. The routine: @@ -347,279 +351,53 @@ contract writing into a loop instead of a guess. Start with `self_check`, because the optional pieces degrade independently, then reload the target's sources plus `FRAMAC_STUB_DIR`, run WP one function at a time, and use `get_wp_goals` and `context` to find which obligation is unproved rather than -rewriting a contract on suspicion. Retrying the unproved goals distinguishes -"not proved" from "not proved yet", so check that before rewriting a contract -that only needed a longer timeout. `create_sandbox` is the honest way to try a +rewriting a contract on suspicion. `create_sandbox` is the honest way to try a strengthening without touching the real source. -Read the `self_check` result rather than the absence of an error: a degraded -server still answers, and the answer looks like a normal response. -`frama_c.status: ok` says only that the binary runs. The fields that decide -whether the interactive path works at all are `socket_spawn`, and -`wp.available` / `eva.available` under `capabilities`. - -Do not read a failed `socket_spawn` as a missing `ast_utils` plugin without -checking. Its probes are time-bounded, so on a loaded host they time out and -report `error` or `unknown` for a plugin that is installed and works. Seen -here at load 75 on 8 cores: `socket_spawn` reported "the probe process exited -or never created one" and `ast_utils` came back `unknown`, while -`frama-c -load-module ast_utils_plugin -print-libc` succeeded immediately and -the plugin sat in Frama-C's plugin directory the whole time. `opam_switch_hint` -timing out in the same report is the tell. Confirm with that one-line load -before concluding anything, and re-run `self_check` on a quiet machine; only -if the plugin is genuinely absent is the install -`cd ast-utils && dune install` in the frama-c-mcp checkout. - -`reload_project` does not take a raw preprocessor string. It takes structured -flags, and an unknown key is accepted and dropped rather than refused, so a -call carrying `cpp_extra_args` parses with none of them and then fails on a -header that is on the real include path. Mirror `FRAMAC_CPP_ARGS` field by -field instead; for this tree that is +The MCP is an accelerator, never the gate. A change lands on `make verify` +plus `make verify-mutants`, run from the Makefile, because that is what CI +runs and what a contributor without the server can reproduce. Never report a +proof as done on MCP evidence alone, and never add a workflow step, script, or +CI job that depends on the server being connected. -``` -include_paths: ["frama-c-stubs", "src", "build"] -force_includes: ["prelude.h", "macos-libc.h"] -machdep: "gcc_x86_64" -``` - -Those three lines are `FRAMAC_INCLUDE_DIRS`, `FRAMAC_FORCE_INCLUDES` and -`FRAMAC_DATA_MODEL` from `mk/verify.mk`, and they are reproduced here only to -show the shape; take the live values from `make print-verify-profiles` below -rather than from this block, which nothing gates. - -`nostdinc` and `isystem_paths` are fields, and they are not optional detail on -this platform: without them the real macOS headers win over the modeled libc, -and a file whose parse depends on that shadowing loads as a different program. -Two measurements from when they could not be expressed, both worth knowing -because they are what a load under the wrong headers looks like. -`src/syscall/sys.c` parsed under the `mk/verify.mk` flags and failed without -them, on a `_Static_assert` over `struct rusage` that only holds against the -modeled header, which put it and six others in `parse_surface`'s blocked set: -39 of 60 reported against 46 of 60 true. - -The flags are not the only way the two can differ, and the other way cost me a -wrong diagnosis. On `src/syscall/net.c` the server reported `recv_at`'s -`pointer_alignment` obligation unproved, surviving `retry_unproved` at double -the budget, which is its own strongest test for a goal that is unprovable -rather than slow. Under `mk/verify.mk` the same three functions discharge 6 of -6 and that obligation is never generated. I recorded that here as a header -artifact; it was not. The cause was RTE: the kernel's generator and WP's own -are different analyses, the kernel emits `pointer_alignment` assertions and -WP's does not, and the server was starting Frama-C with `-rte` where the recipe -passes `-wp-rte`. Fixed upstream, but the shape is worth keeping: a -`pointer_alignment` goal the build never generates is the signature of the -wrong RTE generator, not of a hard proof. - -So the rule is not "distrust the server", it is "pass the flags". A profile -from `make print-verify-profiles` carries both, and `nostdinc` must be stated -for a profile to be proof evidence at all. When you load by hand instead, pass -`nostdinc` and `isystem_paths` yourself, or you are measuring another program. - -Two rules about what any of that proves: - -- The MCP's default WP model is not what every target uses. A goal that - discharges under defaults says nothing about whether `make verify-` - passes. Always mirror the target's own `VERIFY__MODEL`. -- A prover budget is wall-clock, so on a saturated machine a goal can reach it - whatever its difficulty. Read `wp_timeout_triage` before believing a timeout - verdict: it carries `host_load_per_cpu` in its evidence and drops to - `confidence: low` above one runnable thread per CPU, and again when the - reading is `"unavailable"`, since an unread host is not a quiet one. Only a - measured quiet host earns `confidence: high`. -- Re-running is not re-measuring, and this is the trap. WP's cache defaults to - `update`, so it stores timeout verdicts too and replays them. Measured here: - the same six functions, run under load (one-minute average 40 to 61 on 8 - cores) and again at load 3.3, produced the identical `proof_receipt` sha256, - with every timeout goal carrying `from_cache: true`. The second run proved - nothing and looked exactly like the first. - - The response says so now. `measurement` reports `replayed`, `unproved` and - `unproved_replayed`, and `every_unproved_goal_was_replayed` is the one to - read: when it is true the run attempted none of its own failures, and - `wp_timeout_triage` drops to `confidence: low` saying so. Pass - `cache: "None"` to prove everything in the run. It is the same distinction - `proof_coverage` draws between `fresh_valid` and `cached_valid`, and it - costs a re-prove, so spend it when a verdict is about to become a decision. -- `retry_unproved` settles slow against unprovable, and nothing else. It - re-runs the timed-out goals at double the budget and reports which flip, so - an empty `flipped` means more time is not the fix. It does not check that the - program under it is the one you meant: on `src/syscall/net.c` a goal survived - it and was still an artifact of the wrong header environment. Rule out the - load, the cache, and the flags before reading it as a property of the code. -- The connected server is whatever binary is installed, which can lag the - source tree. A behavior described here that the running server does not show - means the installed binary predates it, not that the description is wrong; - `self_check` reports the server version. -- The MCP is an accelerator, never the gate. A change lands on `make verify` - plus `make verify-mutants`, run from the Makefile, because that is what CI - runs and what a contributor without the server can reproduce. Never report a - proof as done on MCP evidence alone, and never add a workflow step, script, - or CI job that depends on the server being connected. - -It also answers the coverage question rather than just the green/red one, -which is how you find a target that passes because it is proving less than you -thought. `proof_coverage` is the tool for that: - -``` -# denominator: every defined function of the loaded project -proof_coverage {} - -# denominator: the function set that target declares -proof_coverage {verify_profile: "", detail: "full"} -``` - -It measures stored conclusions, not the last run, so it reports nothing until -`store_function_conclusion` has filed a receipt from a `run_wp` on the real -project. With nothing loaded and nothing stored it answers `0 of 0`, -`incomplete`, and an empty function list rather than an error, which is easy to -skim as a clean report. Check the denominator before reading the percent. - -Sandbox receipts are refused on purpose: a sandbox proves an extracted copy -whose uncontracted callees are stubs. Merge the annotations back, re-run WP on -the main project, and store that receipt. - -Read a row's `reason` as the instruction, and treat an empty one as the only -thing that counts. Three of them come up here more than the others: - -- `stale_source` after a single edit. A receipt hashes the whole loaded file - set, not the one file its function lives in, so touching any source reds the - entire report. Expect it; it is not a signal about the function you edited. -- `unverified_callee`, propagated through the call chain. Fix what - `blocking_callees` names first. -- `proved_under_a_goal_filter`, meaning the run passed `prop` and left the - unselected obligations unattempted. That is the "proving less than you - thought" case caught by name. - -One limit on the number, on top of the two rules above. It reads WP only, so -`complete` is a statement about proof obligations generated by the ACSL, RTE -and WP configuration that produced those receipts. A requirement no contract -states is not an uncovered row, it is absent from the denominator entirely, so -coverage cannot tell you the property table is complete. - -### Calibrate the server before trusting a number from it - -Run one already-green target through it and compare the obligation count with -what the matching `make verify-` reports. Use `iov`: three functions, one -header, and a known answer of 40 of 40. - -``` -make verify- # the answer, for name=iov -reload_project {verify_profiles: , - verify_profile: "iov"} -run_wp {verify_profile: "iov", cache: "None"} -``` - -The counts must match exactly. Every wrong conclusion this file records came -from skipping that check, and each was invisible without it: - -- The server refused 20 of the 21 targets outright with - `invalid WP model 'typed'`, comparing the name case-sensitively where - Frama-C does not care. A profile emitted faithfully from the recipe was - rejected by the tool whose whole purpose is to run that recipe's proof. -- With that fixed it answered 42 obligations to the recipe's 40, both extras - `pointer_alignment` on one function, because it started Frama-C with kernel - `-rte` where the recipe passes `-wp-rte`. Those are different analyses and - the larger one is not the target's. -- `caveat`, which one target is proved under, is accepted by Frama-C and named - nowhere in `-wp-h`, so a list built from that help text called it invalid. - -None of those announced themselves. Each produced a confident, well-formatted -answer about a program the build system does not prove, and `retry_unproved` -confirmed one of them. Two numbers side by side is the cheapest thing that -catches the whole class, and it costs one target. - -### Making the MCP prove what the Makefile proves - -`make print-verify-profiles` emits the `verify_profiles` JSON for all of -`mk/verify.mk`, one entry per target, carrying the sources, functions, model, -machdep, include paths, defines, provers, timeout and a `reproduce` command. -It comes from the same variables the `verify-` recipe consumes, so a -profile and a Makefile run cannot disagree about what a target proves. Emit -it, never hand-write it: a hand-written function set is the drift the whole -mechanism exists to prevent. - -That property is only as good as the sharing. The two lists the profile and the -recipe both need, include directories and force-includes, live in -`FRAMAC_INCLUDE_DIRS` and `FRAMAC_FORCE_INCLUDES`; `FRAMAC_CPP_ARGS` turns them -into `-I` and `-include` flags with `patsubst`, and the emitter passes them -through as the bare directories and headers the schema wants. Spelling either -list twice is the bug this arrangement exists to prevent, and it is not -hypothetical: they were duplicated at first, under a comment claiming they -could not drift. If you add an include path, add it there and check both sides -move: - -``` -make print-verify-profiles FRAMAC_INCLUDE_DIRS="... extra" | grep extra -make -n verify-align FRAMAC_INCLUDE_DIRS="... extra" | grep -- -Iextra -``` - -The emitter refuses rather than emitting a profile that cannot be used: no -sources, no functions, an empty or blank model, no provers, a non-positive -timeout, a `CPP_DEFS` token that is not a `-D`, or no targets at all. Each -names the make variable to look at. That matters because the server's own -refusal comes much later and names none of them: a profile missing one required -field is accepted for loading and then rejected by every `run_wp` and every -`store_function_conclusion` that names it, which reads as a broken target -rather than as an empty variable on the command line that produced it. - -That closes the loop between the two tools: - -``` -make print-verify-profiles # from the build system -reload_project {verify_profiles: , verify_profile: ""} -run_wp {verify_profile: ""} -store_function_conclusion {function, status: "verified", - proof_receipt_sha256, verify_profile: ""} -proof_coverage {verify_profile: "", detail: "full"} -``` - -The JSON goes in as the object or as its text: the `verify_profiles` parameter -is untyped, so a client that stringifies it is not making a mistake, and the -server decodes either. Naming the profile is what makes each step mean the -target rather than the server's defaults. A run that deviated from the profile -is refused as that target's evidence rather than quietly accepted, and a -conclusion stored without one records what was proved but not what it settles. - -Three things to know when feeding it in. The profile carries `nostdinc` and -`isystem_paths` alongside the include paths, all four from the same -`mk/verify.mk` variables the recipe uses, so the load the server makes is the -one the recipe makes. The model strings are the -Makefile's own spelling (`typed`, `caveat`, `Bytes`), which is the point: -normalizing them here would make the profile prove something the recipe does -not. And every profile carries `rte: true`, because every `verify-` -recipe passes `-wp-rte`: that flag decides which obligations exist at all, so a -load without it gives a strictly smaller set. The server treats it as part of -the load identity, so a non-RTE load is refused as that target's evidence -rather than quietly accepted, and a profile that omits it can load sources but -cannot be proof evidence. - -`rte: true` means WP's generator specifically, not Frama-C's kernel one. They -are different analyses over the same code and the kernel's is larger: it emits -`pointer_alignment` assertions WP's does not. The server used to start Frama-C -with kernel `-rte` here, which is how a profiled `iov` run answered 42 -obligations to the recipe's 40 with both extras unproved. Worth knowing because -the field cannot express the difference, so the only way to see it is the -calibration above. +The server reports more confidently than it measures, and the ways it can be +wrong are specific: a verdict that rests on a filtered goal set, a cached +replay read as a fresh run, a model or flag set that is not the target's, a +timeout on a loaded host. `references/frama-c-mcp.md` carries the whole of it, +including the shapes its `check` codes name, how to calibrate against a known +target before trusting a number, and how to make the server prove what the +Makefile proves. Read it before quoting anything the server prints. ### frama-c-stubs/ -Declarations the analyzer needs that the compiler or macOS supplies: -`Hypervisor/Hypervisor.h` and `macos-libc.h` for Darwin constants the modeled -libc omits, plus `prelude.h`, which declares nothing of its own and instead -force-includes the two headers Frama-C ships but never reaches on its own: its -gcc-builtins model, and its stdatomic.h for the `_Atomic` qualifier its front -end cannot parse and for the C11 atomics vocabulary the tree calls. +Declarations the analyzer needs that the compiler or macOS supplies. +`ls -R frama-c-stubs/` is the list, and three kinds live there: whole Darwin +headers Frama-C has no model of, constants the modeled libc omits, and Darwin +structure shapes it declares in the Linux spelling. `prelude.h` is the odd +one, declaring nothing of its own and instead force-including the two headers +Frama-C ships but never reaches on its own: its gcc-builtins model, and its +stdatomic.h for the `_Atomic` qualifier its front end cannot parse and for the +C11 atomics vocabulary the tree calls. + +A stub of the third kind may take the modeled header whole through +`#include_next` and rename one name inside it. `scripts/check-stub-shadow.py`, +a prerequisite of every `verify-*` target, holds that to exactly one +declaration, because a second would follow the rename into a prototype and +change a signature the proofs reason about. It sits outside `src/` on purpose so a real compile, which resolves through `-Isrc`, cannot reach it. Only `FRAMAC_STUB_DIR` in `mk/verify.mk` does. It is tracked in git because every proof target needs it to parse. A missing declaration fails with "Cannot resolve variable" - that is how the -next one gets found. Only a minority of `src/`'s `.c` files parse today; the -rest stop on macOS headers Frama-C's libc genuinely does not model -(`sys/mount.h`, `sys/event.h`, `sys/sysctl.h`, `sys/xattr.h`, `sys/attr.h`, -`sys/spawn.h`). That is a real modeling gap. Do not paper over it with a fake -stub, and do not quote a parse count without recomputing it. +next one gets found. Most of `src/`'s `.c` files parse; the rest stop on macOS +headers Frama-C's libc does not model (`sys/mount.h`, `sys/event.h`, +`sys/xattr.h`, `sys/attr.h`, `sys/spawn.h`). That is a real modeling gap, and +a stub that invents a body for one is how a proof comes to reason about a +program nobody runs. A declarations-only stub is a different thing and is +legitimate: `frama-c-stubs/sys/sysctl.h` is the worked case, and its own +header comment argues why sysctl left the blocked list. Recompute the parse +count before quoting it; the probe above is how. ## Other checks @@ -652,12 +430,10 @@ which have shipped before: stops at the first failing step and the suites after it never print. - A count, a latency, or a coverage figure is recomputed before it is quoted, including from this file and from `CLAUDE.md`, whose counts drift because - nothing gates them. Measured in one session: 21 verify targets against its - 20, 32 file-scope locks against its 31, 17 files under `src/proved/` against - the 15 it lists. The gates print the live number, so take it from - `make print-verify-targets` and from what `check-lock-order` and - `check-proof-targets` report. A number carried forward from a document reads - as measured and is not. + nothing gates them. The gates print the live number: take the target count + from `make print-verify-targets`, the lock split from `check-lock-order`, + and the `src/proved/` count from `check-proof-targets`. A number carried + forward from a document reads as measured and is not. - The `PROVED n of n` line is not in `build/verify-.log`, which carries Frama-C's own `[wp] Proved goals: N / N` instead. It is check-wp-result.py's console output, colorized unconditionally, with the escape sitting between diff --git a/.claude/skills/elfuse-verify/references/frama-c-mcp.md b/.claude/skills/elfuse-verify/references/frama-c-mcp.md new file mode 100644 index 00000000..836c1ee4 --- /dev/null +++ b/.claude/skills/elfuse-verify/references/frama-c-mcp.md @@ -0,0 +1,293 @@ +# Driving the frama-c MCP server + +Loaded from `elfuse-verify` when the `frama-c` MCP server is connected and a +proof needs to be worked goal by goal. Everything here is about reading a +result from that server correctly. None of it changes what makes a proof +land: that is `make verify` plus `make verify-mutants`, from the Makefile. + +## Using the server + +`make verify-` is a batch run: it either discharges or it does not, and +a failure tells you little about which obligation is stuck. If the `frama-c` +MCP server is connected, it drives the same Frama-C interactively, which turns +contract writing into a loop instead of a guess. Start with `self_check`, +because the optional pieces degrade independently, then reload the target's +sources plus `FRAMAC_STUB_DIR`, run WP one function at a time, and use +`get_wp_goals` and `context` to find which obligation is unproved rather than +rewriting a contract on suspicion. Retrying the unproved goals distinguishes +"not proved" from "not proved yet", so check that before rewriting a contract +that only needed a longer timeout. `create_sandbox` is the honest way to try a +strengthening without touching the real source. + +Three of the server's behaviors are worth knowing before you read a result +from it: + +- `check` gates its verdict on evidence the run actually read, not on an + empty `incomplete[]`. It carries codes for the shapes that pass silently + otherwise: a statement contract or generalized + invariant dropped as "not yet supported (skipped)", a union write proved + "might be unsound", an undefined logic function "interpreted as reads + nothing", a postcondition that got no goal because the function has a + caller, and a dead branch only WP's smoke tests see. A verdict that arrives + with one of those codes is not the proof you asked for. +- Per-goal WP cache provenance comes from `ast-utils`, not from the summary + line. The "(Cached)" word is printed for every cacheable goal in an updating + cache mode, hit or miss, so it does not say a verdict was replayed. When it + matters whether a number is fresh, read the provenance or run with + `cache: "None"` as the calibration below does. +- `analyze_concurrency` screens loaded sources for race and lock-order + candidates. That is directly useful here, because the ordering block in + `src/syscall/internal.h` is prose and nothing proves the tree obeys it. Read + the level honestly: the scan is syntactic, a candidate is evidence and not a + race, and an absent candidate is not a proof of safety, because the + strongest thing a lexical lockset supports is that two accesses name one + lock. It is also bounded. `max_events` defaults to 10,000 and clamps at + 100,000, `max_candidates` defaults to 2,000 and clamps at 20,000, and the + scan has its own time budget that can stop it mid-file; `scan_complete` + reports that last one. An enumeration that hit any of those is partial, and + reading it as complete is the one way this tool produces a wrong answer. + +Read the `self_check` result rather than the absence of an error: a degraded +server still answers, and the answer looks like a normal response. +`frama_c.status: ok` says only that the binary runs. The fields that decide +whether the interactive path works at all are `socket_spawn`, and +`wp.available` / `eva.available` under `capabilities`. + +Do not read a failed `socket_spawn` as a missing `ast_utils` plugin without +checking. Its probes are time-bounded, so on a loaded host they time out and +report `error` or `unknown` for a plugin that is installed and works. Seen +here at load 75 on 8 cores: `socket_spawn` reported "the probe process exited +or never created one" and `ast_utils` came back `unknown`, while +`frama-c -load-module ast_utils_plugin -print-libc` succeeded immediately and +the plugin sat in Frama-C's plugin directory the whole time. `opam_switch_hint` +timing out in the same report is the tell. Confirm with that one-line load +before concluding anything, and re-run `self_check` on a quiet machine; only +if the plugin is genuinely absent is the install +`cd ast-utils && dune install` in the frama-c-mcp checkout. + +`reload_project` does not take a raw preprocessor string. It takes structured +flags, and an unknown key is accepted and dropped rather than refused, so a +call carrying `cpp_extra_args` parses with none of them and then fails on a +header that is on the real include path. Mirror `FRAMAC_CPP_ARGS` field by +field instead; for this tree that is + +``` +include_paths: ["frama-c-stubs", "src", "build"] +force_includes: ["prelude.h", "macos-libc.h"] +machdep: "gcc_x86_64" +``` + +Those three lines are `FRAMAC_INCLUDE_DIRS`, `FRAMAC_FORCE_INCLUDES` and +`FRAMAC_DATA_MODEL` from `mk/verify.mk`, and they are reproduced here only to +show the shape; take the live values from `make print-verify-profiles` below +rather than from this block, which nothing gates. + +`nostdinc` and `isystem_paths` are fields, and they are not optional detail on +this platform: without them the real macOS headers win over the modeled libc, +and a file whose parse depends on that shadowing loads as a different program. +Two measurements from when they could not be expressed, both worth knowing +because they are what a load under the wrong headers looks like. +`src/syscall/sys.c` parsed under the `mk/verify.mk` flags and failed without +them, on a `_Static_assert` over `struct rusage` that only holds against the +modeled header, which put it and six others in `parse_surface`'s blocked set. +The tool reports fewer files parsing than actually do, so take the number from +the probe rather than from it. + +The flags are not the only way the two can differ, and the other way reads as +a hard proof failure. On `src/syscall/net.c` the server reported `recv_at`'s +`pointer_alignment` obligation unproved, surviving `retry_unproved` at double +the budget, which is its own strongest test for a goal that is unprovable +rather than slow. Under `mk/verify.mk` the same three functions discharge 6 of +6 and that obligation is never generated. The cause is RTE, not the header: +the kernel's generator and WP's own are different analyses, the kernel emits +`pointer_alignment` assertions and WP's does not, and the server was starting +Frama-C with `-rte` where the recipe passes `-wp-rte`. Fixed upstream, but the +shape is worth keeping: a `pointer_alignment` goal the build never generates +is the signature of the wrong RTE generator, not of a hard proof. + +So the rule is not "distrust the server", it is "pass the flags". A profile +from `make print-verify-profiles` carries both, and `nostdinc` must be stated +for a profile to be proof evidence at all. When you load by hand instead, pass +`nostdinc` and `isystem_paths` yourself, or you are measuring another program. + +Two rules about what any of that proves: + +- The MCP's default WP model is not what every target uses. A goal that + discharges under defaults says nothing about whether `make verify-` + passes. Always mirror the target's own `VERIFY__MODEL`. +- A prover budget is wall-clock, so on a saturated machine a goal can reach it + whatever its difficulty. Read `wp_timeout_triage` before believing a timeout + verdict: it carries `host_load_per_cpu` in its evidence and drops to + `confidence: low` above one runnable thread per CPU, and again when the + reading is `"unavailable"`, since an unread host is not a quiet one. Only a + measured quiet host earns `confidence: high`. +- Re-running is not re-measuring, and this is the trap. WP's cache defaults to + `update`, so it stores timeout verdicts too and replays them. Measured here: + the same six functions, run under load (one-minute average 40 to 61 on 8 + cores) and again at load 3.3, produced the identical `proof_receipt` sha256, + with every timeout goal carrying `from_cache: true`. The second run proved + nothing and looked exactly like the first. + + The response says so now. `measurement` reports `replayed`, `unproved` and + `unproved_replayed`, and `every_unproved_goal_was_replayed` is the one to + read: when it is true the run attempted none of its own failures, and + `wp_timeout_triage` drops to `confidence: low` saying so. Pass + `cache: "None"` to prove everything in the run. It is the same distinction + `proof_coverage` draws between `fresh_valid` and `cached_valid`, and it + costs a re-prove, so spend it when a verdict is about to become a decision. +- `retry_unproved` settles slow against unprovable, and nothing else. It + re-runs the timed-out goals at double the budget and reports which flip, so + an empty `flipped` means more time is not the fix. It does not check that the + program under it is the one you meant: on `src/syscall/net.c` a goal survived + it and was still an artifact of the wrong header environment. Rule out the + load, the cache, and the flags before reading it as a property of the code. +- The connected server is whatever binary is installed, which can lag the + source tree. A behavior described here that the running server does not show + means the installed binary predates it, not that the description is wrong; + `self_check` reports the server version. +- The MCP is an accelerator, never the gate. A change lands on `make verify` + plus `make verify-mutants`, run from the Makefile, because that is what CI + runs and what a contributor without the server can reproduce. Never report a + proof as done on MCP evidence alone, and never add a workflow step, script, + or CI job that depends on the server being connected. + +It also answers the coverage question rather than just the green/red one, +which is how you find a target that passes because it is proving less than you +thought. `proof_coverage` is the tool for that: + +``` +# denominator: every defined function of the loaded project +proof_coverage {} + +# denominator: the function set that target declares +proof_coverage {verify_profile: "", detail: "full"} +``` + +It measures stored conclusions, not the last run, so it reports nothing until +`store_function_conclusion` has filed a receipt from a `run_wp` on the real +project. With nothing loaded and nothing stored it answers `0 of 0`, +`incomplete`, and an empty function list rather than an error, which is easy to +skim as a clean report. Check the denominator before reading the percent. + +Sandbox receipts are refused on purpose: a sandbox proves an extracted copy +whose uncontracted callees are stubs. Merge the annotations back, re-run WP on +the main project, and store that receipt. + +Read a row's `reason` as the instruction, and treat an empty one as the only +thing that counts. Three of them come up here more than the others: + +- `stale_source` after a single edit. A receipt hashes the whole loaded file + set, not the one file its function lives in, so touching any source reds the + entire report. Expect it; it is not a signal about the function you edited. +- `unverified_callee`, propagated through the call chain. Fix what + `blocking_callees` names first. +- `proved_under_a_goal_filter`, meaning the run passed `prop` and left the + unselected obligations unattempted. That is the "proving less than you + thought" case caught by name. + +One limit on the number, on top of the two rules above. It reads WP only, so +`complete` is a statement about proof obligations generated by the ACSL, RTE +and WP configuration that produced those receipts. A requirement no contract +states is not an uncovered row, it is absent from the denominator entirely, so +coverage cannot tell you the property table is complete. + +## Calibrate the server before trusting a number from it + +Run one already-green target through it and compare the obligation count with +what the matching `make verify-` reports. Use `iov`: three functions, one +header, and a known answer of 40 of 40. + +``` +make verify- # the answer, for name=iov +reload_project {verify_profiles: , + verify_profile: "iov"} +run_wp {verify_profile: "iov", cache: "None"} +``` + +The counts must match exactly. Every wrong conclusion this file records came +from skipping that check, and each was invisible without it: + +- The server refused all but one target outright with + `invalid WP model 'typed'`, comparing the name case-sensitively where + Frama-C does not care. A profile emitted faithfully from the recipe was + rejected by the tool whose whole purpose is to run that recipe's proof. +- With that fixed it answered 42 obligations to the recipe's 40, both extras + `pointer_alignment` on one function, because it started Frama-C with kernel + `-rte` where the recipe passes `-wp-rte`. Those are different analyses and + the larger one is not the target's. +- `caveat`, which one target is proved under, is accepted by Frama-C and named + nowhere in `-wp-h`, so a list built from that help text called it invalid. + +None of those announced themselves. Each produced a confident, well-formatted +answer about a program the build system does not prove, and `retry_unproved` +confirmed one of them. Two numbers side by side is the cheapest thing that +catches the whole class, and it costs one target. + +## Making the MCP prove what the Makefile proves + +`make print-verify-profiles` emits the `verify_profiles` JSON for all of +`mk/verify.mk`, one entry per target, carrying the sources, functions, model, +machdep, include paths, defines, provers, timeout and a `reproduce` command. +It comes from the same variables the `verify-` recipe consumes, so a +profile and a Makefile run cannot disagree about what a target proves. Emit +it, never hand-write it: a hand-written function set is the drift the whole +mechanism exists to prevent. + +That property is only as good as the sharing. The two lists the profile and the +recipe both need, include directories and force-includes, live in +`FRAMAC_INCLUDE_DIRS` and `FRAMAC_FORCE_INCLUDES`; `FRAMAC_CPP_ARGS` turns them +into `-I` and `-include` flags with `patsubst`, and the emitter passes them +through as the bare directories and headers the schema wants. Spelling either +list twice is the bug this arrangement exists to prevent, and it is not +hypothetical: they were duplicated at first, under a comment claiming they +could not drift. If you add an include path, add it there and check both sides +move: + +``` +make print-verify-profiles FRAMAC_INCLUDE_DIRS="... extra" | grep extra +make -n verify-align FRAMAC_INCLUDE_DIRS="... extra" | grep -- -Iextra +``` + +The emitter refuses rather than emitting a profile that cannot be used: no +sources, no functions, an empty or blank model, no provers, a non-positive +timeout, a `CPP_DEFS` token that is not a `-D`, or no targets at all. Each +names the make variable to look at. That matters because the server's own +refusal comes much later and names none of them: a profile missing one required +field is accepted for loading and then rejected by every `run_wp` and every +`store_function_conclusion` that names it, which reads as a broken target +rather than as an empty variable on the command line that produced it. + +That closes the loop between the two tools: + +``` +make print-verify-profiles # from the build system +reload_project {verify_profiles: , verify_profile: ""} +run_wp {verify_profile: ""} +store_function_conclusion {function, status: "verified", + proof_receipt_sha256, verify_profile: ""} +proof_coverage {verify_profile: "", detail: "full"} +``` + +The JSON goes in as the object or as its text: the `verify_profiles` parameter +is untyped, so a client that stringifies it is not making a mistake, and the +server decodes either. Naming the profile is what makes each step mean the +target rather than the server's defaults. A run that deviated from the profile +is refused as that target's evidence rather than quietly accepted, and a +conclusion stored without one records what was proved but not what it settles. + +Three things to know when feeding it in. The profile carries `nostdinc` and +`isystem_paths` alongside the include paths, all four from the same +`mk/verify.mk` variables the recipe uses, so the load the server makes is the +one the recipe makes. The model strings are the +Makefile's own spelling (`typed`, `caveat`, `Bytes`), which is the point: +normalizing them here would make the profile prove something the recipe does +not. And every profile carries `rte: true`, because every `verify-` +recipe passes `-wp-rte`: that flag decides which obligations exist at all, so a +load without it gives a strictly smaller set. The server treats it as part of +the load identity, so a non-RTE load is refused as that target's evidence +rather than quietly accepted, and a profile that omits it can load sources but +cannot be proof evidence. + +`rte: true` means WP's generator specifically, not Frama-C's kernel one. The +difference and what it costs are under "Using the server" above; the field +cannot express it, so the calibration above is the only way to see it. From 3e012de8105ca50ad6596215d6c9de6f554c7792 Mon Sep 17 00:00:00 2001 From: Jim Huang Date: Wed, 30 Sep 2026 01:35:04 +0800 Subject: [PATCH 2/5] Gate the banned atomic spelling in the skills check-atomics read src only, and its builtin pattern required a call paren, so it caught __atomic_load_n but never a bare order constant. Both gaps met in the skill files, where elfuse-guest-abi named __ATOMIC_SEQ_CST for a call the source writes in C11 and nothing objected. The skills are what a fresh clone carries, so they earn the same gate the source has. Only the banned-spelling half applies to prose: a skill explaining why a bare atomic_load is wrong has to be able to write one, while the builtin vocabulary hands the next reader the wrong spelling for an operation the tree writes in C11. The order constants are gated in prose rather than in C, where every real use sits inside a call the builtin rule already catches. The paren requirement was the same hole from the other side. A bare __atomic_fetch_or named in prose teaches the spelling whether or not a call follows it, so the prose path takes a pattern of its own that does not require one. The star form the rule is stated with stays legal, because the star is not a word character. The skill files are enumerated the way check-ascii.py enumerates its sources, tracked plus untracked and not ignored, so a skill still being drafted is gated while an ignored scratch file is not. A directory walk would have failed the build on the latter. A gate nothing reaches is not a gate. check-atomics ran only under make check, and that lane ignores paths matching **.md and .claude/**, so the pull request this half was written for reached no run of it. It now runs in lint.yml, which carries no path filter. Negative control: reinjecting the original defect fails at its line and removing it passes. Eight prose self-test cases cover both directions, including the three forms prose must keep, and the failure path prints which pattern stopped matching instead of raising. --- .claude/skills/elfuse-conventions/SKILL.md | 10 +- .github/workflows/lint.yml | 12 ++- mk/tests.mk | 2 +- scripts/check-atomics.py | 110 +++++++++++++++++++-- 4 files changed, 120 insertions(+), 14 deletions(-) diff --git a/.claude/skills/elfuse-conventions/SKILL.md b/.claude/skills/elfuse-conventions/SKILL.md index 8f1d7e45..43e9f947 100644 --- a/.claude/skills/elfuse-conventions/SKILL.md +++ b/.claude/skills/elfuse-conventions/SKILL.md @@ -191,9 +191,13 @@ states no more about the ordering than the plain operator does. `scripts/check-atomics.py` holds the two halves a regex can settle: no `__atomic_*` or `__sync_*`, and no C11 atomic call without its `_explicit` -form. It does not check plain-operator access to an `_Atomic` object, because -finding those needs the declarations resolved and the tree still carries a large -pre-existing set of them; that half stays a review question. +form. It reads these skill files too, under the banned-spelling half only, so +prose may quote a bare `atomic_load` but not a concrete `__atomic_*` name or an +`__ATOMIC_*` order constant; write either family with the star, as this +paragraph does. The script does not check plain-operator access to an +`_Atomic` object, because finding those needs the declarations resolved and the +tree still carries a large pre-existing set of them; that half stays a review +question. State the order and name what it pairs with. Relaxed is right under a lock that already serializes the access. Release and acquire are for a publish a lock-free diff --git a/.github/workflows/lint.yml b/.github/workflows/lint.yml index 90ef219e..260f9e6e 100644 --- a/.github/workflows/lint.yml +++ b/.github/workflows/lint.yml @@ -179,12 +179,22 @@ jobs: if: ${{ !cancelled() }} run: python3 scripts/check-skill-refs.py + - name: Atomic spelling + # Reads src/ and the .claude/ skills, nothing built, so it belongs in + # the lane with no path filter. The documentation half in particular: + # build.yml ignores '**.md' and '.claude/**', so the pull request this + # half was written for is exactly the one that reaches no `make check`. + if: ${{ !cancelled() }} + run: | + python3 scripts/check-atomics.py --self-test + python3 scripts/check-atomics.py + # What follows needs LINT_PKGS, and the three checks that use it read # only C sources, the style file, and the .ci scripts that implement # them. cppcheck alone is 50 of this job's 85 seconds and the install is # another 12, so a pull request touching none of those would otherwise # pay about 70 seconds for three checks with nothing to look at. - # The six checks above still run on everything, which is what lets this + # The checks above still run on everything, which is what lets this # workflow carry no path filter at all. # # Whenever the answer is not certain (a push, a merge queue, a base that diff --git a/mk/tests.mk b/mk/tests.mk index a428e7ab..f5ba5b0d 100644 --- a/mk/tests.mk +++ b/mk/tests.mk @@ -105,7 +105,7 @@ check-lock-order: ## Fail when an atomic access states no memory order check-atomics: - @echo " ATOMICS src/" + @echo " ATOMICS src/ .claude/skills/" @python3 scripts/check-atomics.py --self-test @python3 scripts/check-atomics.py diff --git a/scripts/check-atomics.py b/scripts/check-atomics.py index 595b4ed9..cd97b968 100644 --- a/scripts/check-atomics.py +++ b/scripts/check-atomics.py @@ -21,6 +21,14 @@ `atomic_thread_fence` and `atomic_init` are exempt: the fence takes its order as its only argument, and `atomic_init` has no order to state. +The skill files under `.claude/skills/` are read too, under the banned-spelling +half only. The order constants are gated there rather than in C, where every +real use sits inside a `__atomic_*` call the builtin rule already catches. Prose +has to be able to quote a bare `atomic_load` to say why it is wrong, but naming +the builtins' `__ATOMIC_*` order constants for an operation written in C11 hands +the next reader the wrong spelling. Write either family with the star; a +concrete builtin name or a literal order constant trips the gate. + Usage: check-atomics.py [--self-test] """ @@ -34,6 +42,18 @@ # Builtins the conventions ban outright. BUILTIN_RE = re.compile(r"\b(__atomic_\w+|__sync_\w+)\s*\(") +# The builtins' order constants. A call is caught by BUILTIN_RE, but the +# constants also travel alone, most often into prose describing what a C11 +# call does. That reading is what the conventions ban: naming the builtin +# vocabulary for an operation written in C11 tells the next reader to use it. +ORDER_CONST_RE = re.compile(r"\b__ATOMIC_[A-Z_]+\b") + +# The banned families named without a call. Prose states the rule as +# `__atomic_*`, which stays legal because `*` is not a word character, but a +# concrete builtin name teaches the spelling whether or not a paren follows it, +# so the prose rule does not require one the way BUILTIN_RE does. +PROSE_BUILTIN_RE = re.compile(r"\b(__atomic_\w+|__sync_\w+)\b") + # A C11 atomic call whose name does not end in _explicit. The exempt names take # no order argument at all. EXEMPT = { @@ -151,6 +171,21 @@ def scan(text): yield lines[m.start()], name, "implicit-order" +def scan_prose(text): + """Yield (lineno, symbol, rule) for banned atomic spellings in prose. + + Documentation is not C, so the implicit-order rule does not apply: a skill + explaining why `atomic_load` is wrong has to be able to write it. What + does apply is the banned vocabulary, because a reader copies the spelling + a document uses. + """ + for lineno, line in enumerate(text.split("\n"), 1): + for m in PROSE_BUILTIN_RE.finditer(line): + yield lineno, m.group(1), "builtin" + for m in ORDER_CONST_RE.finditer(line): + yield lineno, m.group(0), "order-constant" + + def self_test(): cases = [ ("__atomic_load_n(&x, __ATOMIC_RELAXED);", 1, "builtin"), @@ -202,12 +237,47 @@ def self_test(): % (src, got, want_line) ) failures += 1 + prose_cases = [ + ("the clear is `__ATOMIC_RELEASE`", 1, "order-constant"), + ("`shim_globals_attn_or` (`__ATOMIC_SEQ_CST`) raises the bit", 1, + "order-constant"), + ("__atomic_load_n(&x, 0);", 1, "builtin"), + # A concrete builtin name teaches the spelling with no call around it. + ("`shim_globals_attn_or` is an `__atomic_fetch_or`", 1, "builtin"), + ("a `__sync_synchronize` where a fence belongs", 1, "builtin"), + # Naming the banned family without calling it is how the rule is + # stated, so it must stay legal. + ("bans the `__atomic_*` and `__sync_*` builtins", 0, None), + # The C11 spellings are what documents are supposed to use. + ("`atomic_fetch_or_explicit(..., memory_order_seq_cst)`", 0, None), + # Prose may quote a bare C11 call as the thing it is warning about. + ("a bare `atomic_load(x)` defaults to seq_cst", 0, None), + ] + for text, want, rule in prose_cases: + got = list(scan_prose(text)) + if len(got) != want or (want and got[0][2] != rule): + print(" self-test FAIL (prose): %r -> %r" % (text, got)) + failures += 1 + if failures: return 1 - print(" self-test: %d cases, all pass" % (len(cases) + len(line_cases))) + print(" self-test: %d cases, all pass" + % (len(cases) + len(line_cases) + len(prose_cases))) return 0 +def git_ls(root, *args): + """Paths git lists under root, NUL-delimited so a space survives.""" + out = subprocess.run( + ["git", "ls-files", "-z", *args], + cwd=root, + capture_output=True, + text=True, + check=True, + ).stdout + return [rel for rel in out.split("\0") if rel] + + def main(): ap = argparse.ArgumentParser() ap.add_argument("--self-test", action="store_true") @@ -217,13 +287,7 @@ def main(): return self_test() root = pathlib.Path(__file__).resolve().parent.parent - files = subprocess.run( - ["git", "ls-files", "src/*.c", "src/*.h"], - cwd=root, - capture_output=True, - text=True, - check=True, - ).stdout.split() + files = git_ls(root, "src/*.c", "src/*.h") bad = [] for rel in files: @@ -239,7 +303,35 @@ def main(): print(" See .claude/skills/elfuse-conventions/SKILL.md") return 1 - print(" %d source file(s), every atomic states its memory order" % len(files)) + # Enumerated the way check-ascii.py enumerates its sources: tracked, plus + # anything untracked that is not ignored, since a skill file is untracked + # for as long as it takes to write it. A plain directory walk would instead + # fail the build on an ignored scratch file that is not part of the tree. + # The is_file test drops a tracked file deleted from the worktree. + doc_bad = [] + skills = sorted( + rel + for rel in git_ls(root, "--cached", "--others", "--exclude-standard", + ".claude/skills/*.md") + if (root / rel).is_file() + ) + for rel in skills: + text = (root / rel).read_text(encoding="utf-8", errors="replace") + for lineno, sym, rule in scan_prose(text): + doc_bad.append((rel, lineno, sym, rule)) + + if doc_bad: + print(" %d banned atomic spelling(s) in documentation:" % len(doc_bad)) + for rel, lineno, sym, rule in doc_bad: + hint = ("banned builtin" if rule == "builtin" + else "banned order constant, write the family with a star") + print(" %s:%d: %s (%s)" % (rel, lineno, sym, hint)) + print(" See .claude/skills/elfuse-conventions/SKILL.md") + return 1 + + print(" %d source file(s), every atomic states its memory order; " + "%d skill file(s), no banned atomic spelling" + % (len(files), len(skills))) return 0 From 89347f5738dae2b6e5a472bf56aa091cc3400cc1 Mon Sep 17 00:00:00 2001 From: Jim Huang Date: Wed, 30 Sep 2026 01:35:21 +0800 Subject: [PATCH 3/5] Correct the loopback fixture claim in the docs docs/testing.md and docs/internals.md each introduce the IOKit COM seam substitution with ELFUSE_USB_FIXTURE=loopback alone, and place the build flavor that supplies it 55 to 60 lines below in the same section with no reference tying the two. Read in order, the first sentence says the env var is sufficient, and it is not: a default build links usbdev-fixture-stub.c, whose usbdev_fixture_loopback returns false, so the env var yields a modeled device with no service behind it. The device that answers a transfer needs USB_LOOPBACK_FIXTURE=1 as well, and the loopback lanes set both. Both files now name the flavor in the sentence that introduces the substitution. Measured rather than read: nm finds _usbdev_fixture_lock zero times in build/elfuse and once in build/elfuse-loopback, which is the invariant docs/internals.md pins its dated byte counts to. The two skill descriptions gain the routing vocabulary for this material. Both bodies already covered usbdevfs URBs and raw descriptor blobs, and neither description named USB, so work on it reached neither skill by the words the model matches on. --- .claude/skills/elfuse-security/SKILL.md | 2 +- .claude/skills/elfuse-syscall/SKILL.md | 2 +- docs/internals.md | 7 ++++--- docs/testing.md | 5 +++-- 4 files changed, 9 insertions(+), 7 deletions(-) diff --git a/.claude/skills/elfuse-security/SKILL.md b/.claude/skills/elfuse-security/SKILL.md index 2e0d82c7..b4568640 100644 --- a/.claude/skills/elfuse-security/SKILL.md +++ b/.claude/skills/elfuse-security/SKILL.md @@ -1,6 +1,6 @@ --- name: elfuse-security -description: The guest as an attacker - where the trust boundary runs, the rules a handler on it obeys, what the gates already catch, and what is out of scope. Use when a change parses a guest-chosen length, translates a guest address, resolves a guest path, allocates on the guest's behalf, or blocks holding shared state, and when auditing a diff or writing a finding up. +description: The guest as an attacker - where the trust boundary runs, the rules a handler on it obeys, what the gates already catch, and what is out of scope. Use when a change parses a guest-chosen length, translates a guest address, resolves a guest path, walks a raw USB descriptor blob, allocates on the guest's behalf, or blocks holding shared state, and when auditing a diff or writing a finding up. --- # Security at the guest boundary diff --git a/.claude/skills/elfuse-syscall/SKILL.md b/.claude/skills/elfuse-syscall/SKILL.md index 2a909a37..ec5367ed 100644 --- a/.claude/skills/elfuse-syscall/SKILL.md +++ b/.claude/skills/elfuse-syscall/SKILL.md @@ -1,6 +1,6 @@ --- name: elfuse-syscall -description: Adding or changing a Linux syscall in elfuse. Covers dispatch.tbl, sc_ wrappers, the translation boundary, path and filename resolution, fd classes, lock order, and the coverage gate. Use when touching src/syscall/ or the syscall side of src/runtime/, adding a syscall number, or debugging a guest ENOSYS/EINVAL/EPERM. If the change also alters what the guest observes on return (registers, page permissions, the EL0 return path), read elfuse-guest-abi as well. +description: Adding or changing a Linux syscall in elfuse. Covers dispatch.tbl, sc_ wrappers, the translation boundary, path and filename resolution, fd classes, lock order, usbdevfs, and the coverage gate. Use when touching src/syscall/ or the syscall side of src/runtime/, working on a USB descriptor blob, adding a syscall number, or debugging a guest ENOSYS/EINVAL/EPERM. If the change also alters what the guest observes on return (registers, page permissions, the EL0 return path), read elfuse-guest-abi as well. --- # Adding a syscall to elfuse diff --git a/docs/internals.md b/docs/internals.md index 86526868..26895585 100644 --- a/docs/internals.md +++ b/docs/internals.md @@ -1361,9 +1361,10 @@ fork. IOKit publishes no loopback device, so the async engine had no in-tree lane at all: `ELFUSE_USB_FIXTURE`'s devices have no IOKit service behind them and stop at `SUBMITURB`'s argument gate. `ELFUSE_USB_FIXTURE=loopback` adds one that -does, by substituting at the narrowest place that leaves every layer above it -real: the two COM vtables. Every wire call in `usbdev.c` goes through -`IOUSBDeviceInterface650 **` or `IOUSBInterfaceInterface800 **` as +does, in the `USB_LOOPBACK_FIXTURE=1` build that links the model rather than +the stub (below), by substituting at the narrowest place that leaves every +layer above it real: the two COM vtables. Every wire call in `usbdev.c` goes +through `IOUSBDeviceInterface650 **` or `IOUSBInterfaceInterface800 **` as `(*h)->Method(h, ...)`, so `src/syscall/usbdev-fixture.c` hands back an object whose first member is a vtable of the same shape and nothing above it changes. The URB records, the per-endpoint FIFO, the completion callback, `urb_status`, diff --git a/docs/testing.md b/docs/testing.md index ba71560e..f0285c35 100644 --- a/docs/testing.md +++ b/docs/testing.md @@ -564,8 +564,9 @@ argument gate: the async engine's first review found five defects in code no lane executed, and the arithmetic half of it is testable on any machine. `test-usbdev-urb-loopback` covers the other half. IOKit publishes no loopback -device, so the fixture becomes one: `ELFUSE_USB_FIXTURE=loopback` substitutes -for the two IOKit COM vtables and for nothing above them (see +device, so the fixture becomes one: in the `USB_LOOPBACK_FIXTURE=1` build that +links it (below), `ELFUSE_USB_FIXTURE=loopback` substitutes for the two IOKit +COM vtables and for nothing above them (see [internals.md](internals.md#testing-the-engine-without-hardware)), which puts submit, the per-endpoint queue, the completion callback on the event thread, `DISCARDURB`, `REAPURB` blocking and non-blocking, poll and epoll readiness, From 817dc1e4644d5285b9617c2b635b93e7bd0e09eb Mon Sep 17 00:00:00 2001 From: Jim Huang Date: Wed, 30 Sep 2026 01:35:32 +0800 Subject: [PATCH 4/5] Give the atomics carve-out one home The reason check-atomics leaves plain-operator access to an _Atomic object unchecked was written out three times: in the script's module docstring, in elfuse-conventions, and in elfuse-security. The three had already drifted apart in wording, and one commit rewrapped the docstring copy without touching the other two. The docstring wins, because it sits at the code that implements the rule, and because elfuse-skills already sets that pattern for check-skill-refs.py. Both skills now state what is unchecked and point there for why. What each keeps is the part only it says: elfuse-conventions the spelling rule it demonstrates in its own paragraph, elfuse-security the judgment that this is the one memory-order case worth an auditor's budget rather than a skip. elfuse-conventions was the only skill of eight ending without an Authoritative sources section. It has one now, in the shape its seven siblings use. Two entries carry facts the body does not: that check-ascii reads only .c, .h and .S under src, tests and frama-c-stubs, so the markdown half of the em dash ban has no gate behind it, and that the installed hooks run check-format.sh and check-commentflow.sh at commit time and the commit-log check at push time, none of the gates listed above among them. --- .claude/skills/elfuse-conventions/SKILL.md | 22 ++++++++++++++++++---- .claude/skills/elfuse-security/SKILL.md | 6 ++---- 2 files changed, 20 insertions(+), 8 deletions(-) diff --git a/.claude/skills/elfuse-conventions/SKILL.md b/.claude/skills/elfuse-conventions/SKILL.md index 43e9f947..12f73f39 100644 --- a/.claude/skills/elfuse-conventions/SKILL.md +++ b/.claude/skills/elfuse-conventions/SKILL.md @@ -194,10 +194,8 @@ states no more about the ordering than the plain operator does. form. It reads these skill files too, under the banned-spelling half only, so prose may quote a bare `atomic_load` but not a concrete `__atomic_*` name or an `__ATOMIC_*` order constant; write either family with the star, as this -paragraph does. The script does not check plain-operator access to an -`_Atomic` object, because finding those needs the declarations resolved and the -tree still carries a large pre-existing set of them; that half stays a review -question. +paragraph does. That script's module docstring carries the reasoning, and why +plain-operator access to an `_Atomic` object is left a review question. State the order and name what it pairs with. Relaxed is right under a lock that already serializes the access. Release and acquire are for a publish a lock-free @@ -424,3 +422,19 @@ would push one person's habit onto everybody. Build and toolchain requirements are in `docs/testing.md`, section "Build Requirements". They belong to a machine, not to this convention set. + +## Authoritative sources + +- `CONTRIBUTING.md` for C style, the formatter, and the commit-message rules; + it wins where both files speak. +- `scripts/check-atomics.py`, its module docstring, for what the atomics gate + checks and what it deliberately leaves to review. +- `scripts/check-ascii.py` for the character-set gate, which reads only `.c`, + `.h` and `.S` under `src`, `tests` and `frama-c-stubs`: the markdown half of + the em dash ban has no gate behind it and stays a review question. +- `scripts/check-skill-refs.py` for how a path, target, or section named in + these files is resolved. +- `scripts/install-git-hooks.sh` for the hooks a fresh clone installs. They + run `.ci/check-format.sh` and `.ci/check-commentflow.sh` at commit time and + the commit-log check at push time; none of the gates above is among them, so + those first fail at `make check` or in CI. diff --git a/.claude/skills/elfuse-security/SKILL.md b/.claude/skills/elfuse-security/SKILL.md index b4568640..9c109edd 100644 --- a/.claude/skills/elfuse-security/SKILL.md +++ b/.claude/skills/elfuse-security/SKILL.md @@ -212,10 +212,8 @@ Under `make check`: - `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. + access to an `_Atomic` object. That half is a review question, so it is the + one memory-order case to spend budget on rather than skip. - `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 c216b2899d896bb0cf52d7785c8d17e5aba07c1e Mon Sep 17 00:00:00 2001 From: Jim Huang Date: Wed, 30 Sep 2026 01:35:32 +0800 Subject: [PATCH 5/5] Run the skill gates where they can fail check-skill-refs.py was built to take a routing document on the command line, and the makefile never passed one, so the skill paths in the untracked AGENTS.md routing table went unchecked. The target now passes $(wildcard AGENTS.md), which covers the table where it exists and leaves a fresh clone that has none with the bare invocation it had before. The wildcard is required rather than tidy: the script exits 1 on a file argument that does not exist. The same target ran its self-test locally and not in CI, where the step invoked the checker bare. A regression in the checker's own logic would have passed CI while failing on any developer machine. It now runs its self-test in both places, as check-atomics already does. --- .github/workflows/lint.yml | 4 +++- mk/tests.mk | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/.github/workflows/lint.yml b/.github/workflows/lint.yml index 260f9e6e..03ec67ab 100644 --- a/.github/workflows/lint.yml +++ b/.github/workflows/lint.yml @@ -177,7 +177,9 @@ jobs: # current. This found two dead references to a workflow and a makefile # that the CI split had already removed. if: ${{ !cancelled() }} - run: python3 scripts/check-skill-refs.py + run: | + python3 scripts/check-skill-refs.py --self-test + python3 scripts/check-skill-refs.py - name: Atomic spelling # Reads src/ and the .claude/ skills, nothing built, so it belongs in diff --git a/mk/tests.mk b/mk/tests.mk index f5ba5b0d..069972eb 100644 --- a/mk/tests.mk +++ b/mk/tests.mk @@ -123,7 +123,7 @@ check-svc-tails: ## Verify every path, target, and section the skills name still resolves check-skill-refs: @python3 scripts/check-skill-refs.py --self-test - @python3 scripts/check-skill-refs.py + @python3 scripts/check-skill-refs.py $(wildcard AGENTS.md) define RUN_OPTIONAL_SKIP77 @set -e; \