diff --git a/.claude/skills/elfuse-conventions/SKILL.md b/.claude/skills/elfuse-conventions/SKILL.md index 08228a69..12f73f39 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 @@ -192,9 +191,11 @@ 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. 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 @@ -265,9 +266,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 @@ -417,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-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..9c109edd 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 @@ -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. @@ -207,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` diff --git a/.claude/skills/elfuse-syscall/SKILL.md b/.claude/skills/elfuse-syscall/SKILL.md index aae739de..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 @@ -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. diff --git a/.github/workflows/lint.yml b/.github/workflows/lint.yml index 90ef219e..03ec67ab 100644 --- a/.github/workflows/lint.yml +++ b/.github/workflows/lint.yml @@ -177,14 +177,26 @@ 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 + # 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/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, diff --git a/mk/tests.mk b/mk/tests.mk index a428e7ab..069972eb 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 @@ -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; \ 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