Bind proofs to the target's model and measure the parse surface by jserv · Pull Request #18 · sysprog21/frama-c-mcp

jserv · 2026-09-01T15:41:12Z

Three limits were known about driving this server against a real project's
proof targets. Two of them are now enforced by the server rather than by a
rule someone has to remember; the third is measured rather than guessed at.

The model a target declares is the model it proves under

This server's WP default is Typed+nocast. A project's proof target can
declare something else, and a goal discharged under the wrong memory model is
not evidence about that target at all. Mirroring a target meant transcribing
five values on every call with nothing checking the transcription, which is a
rule that holds until it is forgotten once.

Register what the build system says, once, and name it after that:

reload_project {verify_profiles: <json>, verify_profiles_source: "make print-verify-profiles"}
run_wp         {verify_profile: "elf"}    # model, provers, timeout
check          {verify_profile: "elf"}    # reload flags and proof config

Emit the JSON from the build system that defines the targets, so it cannot
drift from the command that decides. Each entry may carry sources,
functions, model, machdep, include_paths, defines, force_includes,
provers, timeout_seconds and reproduce.

Refusing beats repairing throughout. An unknown key is an error, because
models quietly meaning "no model declared" is the target failure with an
extra step. A profile matching nothing is refused. Naming an unregistered
profile is refused rather than silently falling back to the default. Naming a
profile also fixes the function set, since proving one function and reporting
it as evidence for a target that proves six is the same overclaim one level
down.

The end-to-end test asserts effective_wp_config, read off the process that
did the proving, not the profile echoed back. Those disagree exactly when the
feature is broken: with the model deliberately not applied, the echo still
reads caveat while the options WP ran with read Typed+nocast.

The parse surface is measured, not quoted

How much of a tree Frama-C can parse is the ceiling on what every other tool
here can say about it, and nothing measured it.

parse_surface {files, include_paths?, defines?, force_includes?, machdep?}

It separates two causes a single "did not parse" hides, because the honest
answer differs. An unmodeled_header is a gap in Frama-C's libc: a local
header declaring only what the tree calls does not close it, because the
analysis would then reason about bodies that do not exist. An
undeclared_name is what a stub can supply, declared as the platform declares
it. A path that is not a file is reported as that, rather than handed to the
front end and ranked beside real modeling gaps.

Only the first error of a run is classified, because the rest are usually its
consequences, and a tally over all of them ranks a consequence above the cause
that stopped the file. Diagnostics are read from stdout as well as stderr,
since Frama-C writes them to the former.

Run against the tree that motivated this: 60 sources, 41 parse, 19 stop, led
by sys/sysctl.h and sys/event.h at 5 files each. Its own documentation
said only a minority parse.

Two guards, because a number nobody measures drifts

MCP_TOOL_COUNT is gone. The server counts what it registered, so it cannot
disagree with the surface it describes; the declared list the lifecycle suite
pins is the one written artifact and the count comes off it. Adding a tool went
from six edit sites with three copies of the same integer, two of them inside
tests where they look like checks, to four sites with no integer at all.

src carries no panicking macro, and that is now pinned rather than true by
accident. This server holds a Frama-C child, a socket and a session's
conclusions; a panic takes all three down and answers with a closed pipe rather
than an error a caller can act on, and every failure here already has a
channel. Zero rather than a ceiling: a ceiling is a number the next person
edits to go green.

Verification

scripts/run-gates.sh 16/16 on the tree this branch was split from, which is
identical to the tip apart from comment line breaks; a confirming run on the
tip is in flight at the time of writing.

Every commit was also checked out in isolation: build, clippy and the unit
suite green at each, 429 through 434 as tests are added, so no commit borrows a
test from a later one. Both new guards are mutation-checked rather than assumed
green: injecting a panic! fails one with the file and line, and not applying
a profile's model fails the other with the options WP actually ran.

Summary by cubic

Previously, callers repeated a target’s model, sources, and WP settings without validation. The server now resolves build-system profiles for proof runs and conclusions, measures Frama-C’s parse surface, and refuses evidence that does not match its target.

Target profiles and evidence

reload_project accepts session-scoped verify_profiles JSON and its source command, with strict validation for sources, functions, models, preprocessing flags, provers, timeouts, and reproduce.
Profile-named runs require declared functions, model, provers, and timeout, and reject mismatched loads, overrides, function sets, sandbox scope, and compilation-database inputs.
Conclusions naming a profile require the function, model, and sources to match; receipts now include the complete project load alongside the AST digest.
Singular prover values now accept comma-separated lists and report the same effective configuration as plural prover input.
Projects must provide the profile JSON through reload_project; profiles are session state and are not persisted.

Parse and safeguards

parse_surface accepts explicit files and load flags, reports parse counts, ranks first-error causes, and can include per-file results with detail: "full".
It distinguishes header_not_found, including missing project headers and Frama-C libc gaps, from undeclared_name, and handles non-files, extensionless headers, and spaced include directives.
Parse probes use a server-wide concurrency limit and kill timed-out Frama-C children.
The server derives its tool count from the registered router, and a repository guard rejects panicking macros under src.

^{Written for commit d38d0a8. Summary will update on new commits.}

How much of a tree Frama-C can parse at all is the ceiling on what any of this server's other tools can say about it, and nothing here measured it. A project working around the gap ends up with a count written in a document, quoted from there afterwards, and read as measured long after it stopped being true. parse_surface runs one front end per file, several at a time, and reports how many parsed, plus the causes ranked by how many files each blocks. It separates two causes that a single "did not parse" hides, because the honest answer to them differs. A header Frama-C's modeled libc does not have is a modeling gap: a local header declaring only what the tree calls does not close it, since the analysis would then reason about bodies that do not exist, and a proof resting on that is worth less than no proof. A name the kernel cannot resolve is a missing declaration, which a stub can supply as the platform declares it. The report says which one each file hit and phrases its advice accordingly. Only the first error of a run is classified. The errors after it are usually its consequences, so a tally over all of them counts one cause many times and ranks it above a cause that stopped a whole file on its own. Diagnostics are read from stdout as well as stderr, because Frama-C writes them to the former and a probe reading only the latter would classify every failure as unrecognized. Files are named, not globbed, so which files were measured stays visible to whoever reads the answer. The per-file verdict waits for detail full, since it is the part that makes the response large on a real tree. Measured on a tree that motivated this: 60 sources, 41 parse, 19 stop, led by sys/sysctl.h and sys/event.h at 5 files each. That tree's own documentation said only a minority parse, and told the reader to recompute the figure rather than quote it. A path that is not a file is reported as one rather than handed to the front end, because whatever came back would land in the ranking beside real modeling gaps and send someone looking for a header that was never the problem. A tool is not just a handler: the registry count, the declared surface the lifecycle suite pins, the README table, the agent playbook and the architecture table all name it, and four of those five are guarded. The cause a header failure reports is header_not_found rather than unmodeled_header, because at that point the two readings are indistinguishable: a header of this project missing from the include path looks exactly like one Frama-C's libc does not model, and only the second is a reason to write anything. The advice names both. A timed-out probe kills its child. Dropping the timeout future does not reap it on its own, so every long parse would otherwise leave a Frama-C behind.

FRAMAC_PROVERS is comma-split, and Frama-C's own -wp-prover takes the same spelling, so a caller reaches for run_wp {prover: "alt-ergo,z3"} and has every reason to expect it to work. It did not. The singular argument was wrapped whole in a one-element list, which made the entire string one prover name; that matches no identifier getProvers returns, and apply_prover_selection then refused the run rather than proving anything. The refusal names the requested list against what the server offers, so the failure was at least legible. It was still a run rejected over a spelling this tree accepts in the environment variable that means the same thing. Reporting is made consistent in the same pass. effective_wp_config echoed the singular argument verbatim, so one run reported requested as the string "alt-ergo,z3" while an identical run passing the plural argument reported an array. Every other block in that payload pairs requested with effective in one type, and a reader diffing two runs' configs should not see a difference that is only a spelling.

A project's proof targets each declare a memory model, and this server's default is not it. 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. Mirroring a target by hand meant transcribing five values on every call with nothing checking the transcription, which is a rule a caller follows until it forgets once. The values are registered once, from the build system that defines them, and named afterwards. reload_project takes them and applies a profile's sources, machdep and preprocessor flags; run_wp applies its model, provers and timeout; check applies both. What the caller states explicitly still wins, so deviating on purpose stays possible, and the response reports which values came from the profile. Refusing beats repairing throughout. An unknown key in a profile is an error rather than an ignored field, because "models" quietly meaning no model was declared is the same failure with an extra step. A profile naming neither functions nor sources is refused, since nothing could ever be matched to it. Naming a profile nobody registered is refused rather than quietly falling back to the default, which would prove something under a model the caller did not ask for and report it as that target's evidence. Profiles are session state rather than persisted. They describe a build system as it is now, and a stale copy on disk is the drift they exist to prevent. A profile's prover list becomes one comma-separated prover string, which is Frama-C's own "-wp-prover alt-ergo,z3". It is deliberately not routed through this tool's plural provers argument, which runs a separate process per prover: that would silently change which execution path a run took. The end-to-end test asserts effective_wp_config, read off the process that did the proving, rather than the profile echoed back in the response. With the model deliberately not applied, the echo still reads caveat while the options WP ran with read Typed+nocast, so the echo is exactly the field that would keep looking right. run_wp has three exits and the profile applies to all of them: the sandbox scope, the isolated per-prover retries, and the main path. A response that omitted it would leave the model a caller proved under recorded nowhere they will look. Naming a profile also fixes the function set. Proving one function and reporting it as evidence for a target that proves six is the same class of overclaim as proving under the wrong model, so a different set is refused and the profile's order, which is the target's proof identity, is what runs. Resolution happens after the cancel path, not before it. Cancelling is the way out of a run rather than a run, so a caller abandoning one should not be refused over the config of the thing it is abandoning. Registration and resolution happen under one guard. Dropping it between the two leaves a window where a second caller replaces the set, and the first then loads another target's model or is refused over a name it registered itself. The function set is compared on bare names. A sandbox target is written "exp42:foo" while a profile names the function rather than the experiment holding it, so comparing the qualified form would refuse every sandbox run, and rewriting the caller's list to bare names would leave the sandbox unable to resolve them. The comparison is its own function because it needs a test and the method around it needs a live server. Function and prover names are trimmed at registration, and one that is nothing but padding is refused. A name is compared for equality later, so " elf_phdr_fetch " would register, match nothing all session, and then print a refusal against the name it differs from by two spaces.

Adding one tool meant editing six places, three of which held the same integer: a constant the server reported, a literal in the lifecycle suite's scraper, and a literal in the README guard. Two of those three are inside tests, which makes them look like checks. They are not. A number a person edits to make a build green reads as a check and is one only until the first time somebody bumps it without reading what it describes, and this repository already makes that argument about its own published-surface counts. The server counts what it registered, so it cannot disagree with the surface it is describing. The declared list the lifecycle suite pins becomes the one written artifact and the count is taken from it. The README guard compares against the router. Adding a tool now touches four places and none of them is an integer: the declared list, the README table, a playbook workflow, and the architecture table, the last of which is still checked against the registry rather than believed.

This server holds a Frama-C child, a socket and a session's conclusions. A panic takes all three down and answers the caller with a closed pipe rather than an error they can act on, and every failure here already has a channel: McpError upstream, FramaCError downstream. So reaching for a panicking macro is a decision rather than an accident, and the decision is no. There were none to remove. The guard pins that rather than reporting it, because a property nothing measures is one that drifts, which is the same reason the nesting rule stopped being a comment. Zero rather than a ceiling. A ceiling is a measurement, and a guard carrying one is a number the next person edits to go green; zero is a policy, so there is nothing to bump and a new panic has to argue with the comment above the test. unwrap and expect stay out of it. They panic too, and the eight in src are each either a literal regex behind a OnceLock or a stated invariant, which is a judgement per site rather than a number, so they remain a review question.

Whitespace only, split out rather than folded into a commit that changes behavior, so a reader of either does not have to tell the two apart.

A header with no suffix, "#include <config>", produced a diagnostic the parse-surface report could not classify, so the file landed in "other" with the error quoted and no subject. That is the one cause the report cannot rank or group, which for a whole-tree sweep is the difference between a list of things to fix and a list of files to read. The suffix test moves off the parser and onto its callers. missing_file_name reads the name out of either preprocessor voice, and the two filters over it say what the caller means: a header by suffix, or a name with no extension at all. The second is not enough on its own, since an extensionless source produces the same wording, so classification pairs it with the echoed #include on the following lines before calling it a header. The clang arm now short-circuits on any match rather than only on one ending in ".h". Falling through let the gcc form read a different path out of the same diagnostic, which is a worse answer than none.

Naming a profile applied its model, provers and timeout, and checked nothing about what was loaded. So a caller could load one file, prove it under another target's memory model, and get a response labelling the result as that target's evidence. The wrong sources defeat the claim as squarely as the wrong model does, and only one of the two was being caught. A profiled run now compares the loaded sources and preprocessor settings against what the profile declares, and refuses when they differ rather than answering with a label it cannot support. An empty source list means the profile does not constrain sources; every other field is exactly what reload_project would have applied from it, so the ordinary path of loading under a profile and then proving under it always matches. The WP lock is taken before that comparison and held across the run. Without it the project can be reloaded between deciding that the profile fits and proving anything under it, which is the same gap one level up: a check whose answer stops being true before it is used.

The probe pool was created inside the call that used it, so it composed with nothing. Two concurrent sweeps ran twice as many Frama-C front ends, and a session already holding its sandbox limit paid for both on top. Each front end is a few hundred megabytes, so what matters is how many exist at once, not how many one request asked for. The semaphore lives on the server now. The number is unchanged for a single sweep, which is the common case; what changes is that a second one waits rather than doubling the machine's load. This is a resource limit the server already states elsewhere, through --max-sandboxes, and the pool was quietly outside it.

An extensionless header is only recognised when the lines after the diagnostic echo the include that names it, and that echo was matched by searching for the literal "#include". C allows whitespace between the hash and the directive, so "# include" and a tab-separated form are both legal and both appear in real source. Either one fell through to "other", which is the bucket that names no cause at all and so ranks nothing and suggests nothing. The hash is located rather than anchored at the start of the line. Anchoring was the first attempt and it broke the ordinary case: Frama-C echoes the offending source with a line number and a bar in front of it, so the directive is mid-line, and a check that required the line to begin with a hash traded the common spelling for the rare one. The test covers all three.

Naming a profile applied its settings and checked almost nothing else, so a run could carry a target's name while being about something else entirely: proved under an overriding model, over sources the target does not name, for a subset of its functions, in a sandbox, or under a profile that declared no model at all and quietly fell back to this server's default. Each of those reports the target's name over a result that is not the target's. A named run is now refused unless the profile declares functions, model, provers and timeout_seconds; the call passes none of model, prover, provers or timeout; the loaded sources and preprocessor settings are the ones the profile declares; the functions are exactly the target's set; and the scope is the main project, since a sandbox proof is never a target's evidence. A load through a compilation database is refused too: the database supplies per-file flags this server never sees, so no field the profile declares can describe it. The same bar applies where the verdict is recorded. A conclusion may name the target it settles, and is refused unless the profile proves that function and the receipt agrees on model and sources. That check runs against the merged conclusion rather than one call's arguments, because the tool is incremental: attaching a name to a receipt stored earlier, or replacing the receipt under a name stored earlier, both ask the same question and both used to bypass it. What survives is a verdict that names its target and the command that decides it, which is what this server being an accelerator rather than the gate requires in order to mean anything past a single call. The receipt records the load itself: the preprocessor and target settings the sources were parsed under, separately from the AST digest, because they distinguish configuration changes that select identical code. The format identifier is derived from the receipt's key set, so it moves on its own; only the historical record needed the entry. The lock is held from before the profile is validated until the run completes, so the project cannot be reloaded between deciding that a profile fits and proving anything under it.

This comment was marked as resolved.

Sign in to view

jserv force-pushed the verify-profiles branch 2 times, most recently from 841fdec to 1bbbeb7 Compare September 1, 2026 22:47

This comment was marked as resolved.

Sign in to view

jserv added 11 commits September 2, 2026 14:30

Format the test harness with cargo fmt

ccea308

Whitespace only, split out rather than folded into a commit that changes behavior, so a reader of either does not have to tell the two apart.

jserv force-pushed the verify-profiles branch from 3c00cd2 to d38d0a8 Compare September 2, 2026 06:31

jserv merged commit 8b984dc into main Sep 2, 2026
9 checks passed

jserv deleted the verify-profiles branch September 2, 2026 06:48

Navigation Menu

Uh oh!

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

Bind proofs to the target's model and measure the parse surface#18
jserv merged 11 commits into
mainfrom
verify-profiles

jserv commented Sep 1, 2026 •

edited by cubic-dev-ai Bot

Loading

Uh oh!

This comment was marked as resolved.

Uh oh!

This comment was marked as resolved.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

jserv commented Sep 1, 2026 • edited by cubic-dev-ai Bot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

The model a target declares is the model it proves under

The parse surface is measured, not quoted

Two guards, because a number nobody measures drifts

Verification

Summary by cubic

Uh oh!

This comment was marked as resolved.

Uh oh!

This comment was marked as resolved.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

jserv commented Sep 1, 2026 •

edited by cubic-dev-ai Bot

Loading