Bind proofs to the target's model and measure the parse surface

README.md

@@ -245,7 +245,7 @@ The server exposes the following tool groups:
 
 | Domain | Tools | Purpose |
 |--------|-------|---------|
-| Project | `reload_project`, `list`, `context`, `self_check` | Load source, inspect declarations, navigate call relationships, and report server capabilities |
+| Project | `reload_project`, `list`, `context`, `self_check`, `parse_surface` | Load source, inspect declarations, navigate call relationships, report server capabilities, and measure how much of a file set Frama-C can parse at all |
 | EVA/WP | `check`, `run_wp`, `get_wp_goals`, `run_e_acsl` | Run verification, read what it concluded, and execute runtime counterexamples |
 | Annotations | `inject_all_annotations`, `propose_annotations` | Dry-run validate and inject ACSL annotations, and propose the frame conditions the code determines |
 | Sandbox | `create_sandbox`, `delete_sandbox` | Isolate annotation experiments |
@@ -275,6 +275,49 @@ that points out of it are all refused.
 must be `e-acsl-gcc` or `e-acsl-gcc.sh`, resolved through PATH. Both names
 exist because installs differ.
 
+### Proving what the build system proves
+
+This server's WP defaults are not what a project's proof targets use. A goal
+discharged under `Typed+nocast` says nothing about a target that declares
+`caveat`, so evidence produced under the wrong model is not evidence about that
+target at all.
+
+Register what the build system says, and name it on the same call or a later
+one. Registration happens before the load, so one call can both hand over the
+set and load under one of them:
+
+```
+reload_project {verify_profiles: <json>, verify_profiles_source: "make print-verify-profiles",
+                verify_profile: "elf"}   # registers, then loads elf's sources and cpp flags
+run_wp         {verify_profile: "elf"}   # its model, provers and timeout
+check          {verify_profile: "elf"}   # both
+reload_project {verify_profile: "gva"}   # a later target, already registered
+```
+
+Registering without naming a profile and without `files` is not a load, and a
+fresh session answers it with "no project loaded" because there is nothing to
+reparse. A malformed set is refused before anything is replaced; a set that
+parses is registered even if the load that follows it fails.
+
+Each profile may carry `sources`, `functions`, `model`, `machdep`,
+`include_paths`, `defines`, `force_includes`, `provers`, `timeout_seconds` and
+`reproduce`. Emit the JSON from the build system that defines the targets
+rather than writing it by hand, so it cannot drift from the command that
+decides. An unknown key is refused rather than ignored. A profile
+whose model key is misspelled as `models` would otherwise register with no
+model at all, and the next run would prove under this server's default and
+report it as that target's evidence, which is the failure profiles exist to
+prevent. Naming a profile nobody registered is refused too, rather than
+falling back to the default.
+
+An explicit `model`, `machdep` or include path in the same call wins over the
+profile, so deviating on purpose stays possible, and the response reports what
+came from the profile either way.
+
+`reproduce` is the command that actually decides. This server is an
+accelerator: goals discharging here are progress, and the project's own command
+is the verdict.
+
 `reload_project {include_paths, defines, force_includes}` become preprocessor
 flags, and Frama-C hands those to a shell (its `-cpp-extra-args` is "unsafe in
 sandbox mode"). Each entry is therefore restricted to `[A-Za-z0-9_./+-]`, plus

docs/agent-playbook.md

@@ -31,6 +31,32 @@ A load that fails hard never reaches this, since Frama-C exits before the
 session exists. Read `reload.error` there: it carries the process output,
 which is where an ACSL type error names its predicate and line.
 
+When several files fail that way, ask what the ceiling is before working
+around it one file at a time:
+
+```text
+parse_surface {files, include_paths?, defines?, force_includes?, machdep?, detail?}
+```
+
+It reports how many of a set parse and ranks what blocks the rest, with
+`detail: "full"` adding the per-file verdict. Recompute this rather than
+quoting a count from a document, which is the whole reason the tool exists.
+
+Two of the causes are the ones you act on, and they want opposite things. A
+`header_not_found` is either a header of this project missing from
+`include_paths`, which needs no stub at all, or a system header Frama-C's libc
+does not model, which a stub cannot honestly close: one declaring only what the
+tree calls leaves the analysis reasoning about bodies that do not exist. An
+`undeclared_name` is what a stub does answer, declared as the platform declares
+it.
+
+The rest are not about stubs. `missing_file` means the path is not there and
+nothing was measured for it, so it is evidence neither way; `timeout` means the
+front end did not finish and wants reading directly; `probe_failed` means
+Frama-C itself could not be run, so nothing was measured for that file either;
+`other` quotes the first error rather than guessing a cause for it. That quote
+is per file, so the last one wants `detail: "full"` to read at all.
+
 Call order:
 
 ```text

docs/architecture.md

@@ -25,7 +25,7 @@ The first reload_project starts the main Frama-C process.
 
 | Modules | Responsibilities |
 |---|---|
-| `mcp/*.rs` | 14 tool implementations, one `#[tool_router]` per module, split by domain below |
+| `mcp/*.rs` | 15 tool implementations, one `#[tool_router]` per module, split by domain below |
 | `mcp/server.rs` | Server state, sandbox registry, conclusion persistence, and helpers shared by the tool modules |
 | `mcp/project.rs`, `mcp/analysis.rs`, `mcp/annotations.rs`, `mcp/sandbox.rs`, `mcp/conclusions.rs` | The tool handlers themselves |
 | `mcp/wpcli.rs` | The four paths that run Frama-C as a command line rather than through the socket, because WP settings are process state |

src/error.rs

@@ -233,16 +233,28 @@ pub fn stale_marker_error(
 /// it. Searching for the first quoted token instead would return the compiler
 /// invocation's own arguments.
 pub fn missing_header_name(msg: &str) -> Option<&str> {
+    missing_file_name(msg).filter(|name| name.ends_with(".h"))
+}
+
+/// An extensionless file named by a compiler "not found" diagnostic.
+///
+/// This is not by itself enough to call the file a header: an extensionless
+/// source can produce the same wording. Parse-surface classification pairs it
+/// with the echoed `#include` before reporting it as one.
+pub(crate) fn missing_extensionless_name(msg: &str) -> Option<&str> {
+    missing_file_name(msg).filter(|name| std::path::Path::new(name).extension().is_none())
+}
+
+fn missing_file_name(msg: &str) -> Option<&str> {
     let lower = msg.to_ascii_lowercase();
 
-    // Each arm carries its own suffix filter rather than sharing one at the
-    // end. That duplication is the fall-through: a clang match on something
-    // that is not a header, a missing .c say, has to reach the gcc form below
-    // instead of short-circuiting the whole function.
+    // A clang match on something that is not a header, such as a missing .c,
+    // must still short-circuit here: otherwise the later gcc form can read a
+    // different path from the same diagnostic.
     let clang = lower.find("file not found").and_then(|at| {
         let stripped = msg[..at].trim_end().strip_suffix('\'')?;
         let name = &stripped[stripped.rfind('\'')? + 1..];
-        name.ends_with(".h").then_some(name)
+        Some(name)
     });
     if clang.is_some() {
         return clang;
@@ -252,7 +264,7 @@ pub fn missing_header_name(msg: &str) -> Option<&str> {
     let before = msg[..at].trim_end().strip_suffix(':')?.trim_end();
     // rsplit always yields at least one item, so this cannot be the None case.
     let name = before.rsplit(char::is_whitespace).next().unwrap_or(before);
-    name.ends_with(".h").then_some(name)
+    Some(name)
 }
 
 pub fn classify_server_error(msg: &str) -> (&'static str, bool, Option<serde_json::Value>) {