Refuse profiled run proved less than its target

[jserv]

A profile says what a target's own build proves. Three things it could not say are what this adds, and the rest of the change is what a review and the gates found wrong with saying them.

min_goals is the floor on obligations the target requires WP to generate. "N of N discharged" is not evidence on its own: an emptied body or a dropped contract discharges 0 of 0, and every other check on the path passes it, so a build system carrying such a floor carries the only check that catches it. A floor of 0 is refused at parse time, because omitting the field already says the target declares none and a present key that checks nothing reads as a floor to whoever sees it.

The count is over the target's own obligations rather than over the goal table. fetchGoals returns everything WP holds, including goals from functions proved earlier in the session, so run_wp on one function followed by a profiled run on another would have let the first function's goals clear the second's floor. That is exactly the emptied body the floor exists to catch, cleared by goals that have nothing to do with the target. check reloads first and never saw it; a direct run_wp in a CEGIS loop is where the stale goals live.

run_wp is not the only door. store_function_conclusion takes a receipt from the caller, so a run made without the profile over a gutted target could be stored under the profile's name with the floor never having run, and the conclusion is durable. profile_evidence_error asks the floor too, but only of a receipt whose wp.functions covers the whole declared set: a receipt from check {function: "a"} is honestly scoped to a, and asking a three-function target's floor of it would refuse correct evidence and, through proof_coverage, retroactively flip conclusions already stored.

build_gates names checks the target's command runs that this server does not, echoed back as declared_build_gates_not_run_here. "Declared" is load-bearing: nothing here can verify the list, so an empty one means none were declared rather than that none exist. It bounds a verdict downward and never upward.

prop and retry_unproved join the settings a profile refuses. A filtered run attempts the obligations the filter selects and leaves the rest, so its goal count and its summary agree with each other while describing a subset. A retry re-proves at double the profile's timeout and the flipped goals replace the reported set, receipt included, while the receipt records the declared timeout. Both are the mislabelling the refusal list exists to prevent, arriving through parameters that do not look like proof settings.

Kernel -rte is gone from the main spawn, and WP's guards are generated unconditionally in its place. The two are different analyses over the same code: the kernel emits pointer_alignment assertions WP's generator does not, so a load started under it proves a strictly larger set than the -wp-rte build it claims to be. Measured on one 3-function target, -wp-rte alone generates 40 obligations and discharges all of them while -rte alongside it generates 42 and leaves the two extra open. Making the guard generation conditional on the load's rte flag moved the hole rather than closing it: with the kernel out of it nothing else generates these, so rte=false produced no runtime-error obligations at all, which two stdio tests had documented as deliberate behaviour, since generating them in place is what lets a caller ask for them without a reload that discards this session's injected annotations.

That decision is now testable. main_frama_c_args is a free function because the test asserting it pinned project_cli_args instead, which has never emitted -rte and says so in its own comment, so it passed against the code it was written to pin. The spawn argv also stopped spelling out the options-derived arguments: they were byte-identical to project_cli_args once the -rte line went, and the copy carried its own exhaustive destructure, which is two assertions that neither copy forgets a field and nothing at all that they agree on what to emit.

A goal whose verdict WP replayed from its cache no longer carries a confident reading. The fact is stated in wp_timeout_triage, which is the per-goal field a caller already reads for why a verdict is thin, rather than appended to the classification's reason: that costs 471 bytes on every classified goal, twice, and for a replayed timeout duplicates a string the same payload already carries. The stdio payload budget caught it.

self_check and context report build_commit. CARGO_PKG_VERSION has read 0.1.0 for the project's life, so an installed binary and a freshly built one describe themselves identically, and a caller comparing behaviour against source cannot tell that the server answering predates the code they are reading. build.rs stamps it, watching the tracked files from git ls-files rather than the directory listing: reading the directory watched 12,483 files and 220 MB, including the .frama-c cache every WP run writes, none of which can move a stamp computed from git, and it cost a full release recompile in the middle of a gate run. Dirtiness comes from git diff rather than diff-index, because GIT_OPTIONAL_LOCKS=0 stops git refreshing a stale index and diff-index then reports every file rewritten with identical bytes as a difference. A copy of these sources vendored elsewhere reports unknown rather than that repository's HEAD: a confident wrong sha is the value a caller compares against.

Every reader of a whole ProjectLoadOptions destructures it exhaustively, so a field added later is a compile error rather than a flag that silently never reaches Frama-C, and a guard in repo-guards stops the next reader appearing without one. The guard needed the same scrutiny it applies: it accepted a ".." rest pattern, which is the silence it exists to refuse wearing the shape it asks for, and its body window closed before the body began, because the closing paren of a multi-line signature sits at the signature's own indentation. It was checking nothing at all. It now windows by brace depth, reads the parameter name off the signature, and its fixtures run through the real window.

Caveat is accepted by Frama-C's -wp-model parser and named nowhere in -wp-h, and model names are compared case-insensitively, because a build system writes whichever spelling it likes and Frama-C does not care. Both paths read one list, and the test covers both: only the fallback was covered, and the parsed path is the one that goes stricter when a model is added to a single list.

---

Summary by cubic

Profiled runs now refuse to pass on too few, filtered, or retried goals, and the main Frama-C load generates WP's own runtime-error guards instead of kernel -rte checks, so evidence matches -wp-rte.

Profile evidence

• Adds min_goals, a required-positive floor counted over the target's own obligations, enforced for direct runs and stored receipts.
• Refuses prop and retry_unproved; echoes declared build_gates as declared_build_gates_not_run_here.

Diagnostics and safeguards

• Reports a Git-derived build_commit in self_check and context, or unknown for non-Git source trees.
• Marks cache-replayed WP verdicts as from_cache and lowers their timeout-triage confidence.
• Makes all ProjectLoadOptions readers exhaustive and accepts case-insensitive Caveat model names.

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

[cubic-dev-ai]

1 existing issue remains and 1 new issue found across 27 files

Prompt for AI agents (unresolved issues)

Check if these issues are valid — if so, understand the root cause of each and fix them. If appropriate, use sub-agents to investigate and fix each issue separately.


<file name="tests/unit/repo-guards.rs">

<violation number="1" location="tests/unit/repo-guards.rs:2428">
P3: The `function_body` doc claims a brace inside a string literal would make the window "run long," but a `}` inside a string literal or comment does the opposite: at depth 1 the line `depth = depth.saturating_sub(line.matches('}').count())` drops depth to 0, and the break condition `depth == 0 && body.len() > 1 && line.contains('}')` fires early, truncating the window before the body's field-read lines. That is a false negative for `reads_load_options_field_by_field` — the destructure guard silently misses a violating function, which is exactly the "quiet green" the guard was written to refuse. The doc's framing treats the loss as acceptable, but a short window can stop before the field read rather than merely including extra lines.</violation>
</file>

<sub>Requires human review: Auto-approval blocked because this review re-detected 1 unresolved issue already reported by Cubic.
You've manually re-run cubic several times on this PR. Each manual re-review checks the full PR again and counts toward your usage quota. To preserve your usage limits, we recommend letting cubic automatically review new commits.
Tip: cubic can generate docs of your entire codebase and keep them up to date. Try it here.

Re-trigger cubic</sub>

[cubic-dev-ai]

P3: The function_body doc claims a brace inside a string literal would make the window "run long," but a } inside a string literal or comment does the opposite: at depth 1 the line depth = depth.saturating_sub(line.matches('}').count()) drops depth to 0, and the break condition depth == 0 && body.len() > 1 && line.contains('}') fires early, truncating the window before the body's field-read lines. That is a false negative for reads_load_options_field_by_field — the destructure guard silently misses a violating function, which is exactly the "quiet green" the guard was written to refuse. The doc's framing treats the loss as acceptable, but a short window can stop before the field read rather than merely including extra lines.

Prompt for AI agents

Check if this issue is valid — if so, understand the root cause and fix it. At tests/unit/repo-guards.rs, line 2428:

<comment>The `function_body` doc claims a brace inside a string literal would make the window "run long," but a `}` inside a string literal or comment does the opposite: at depth 1 the line `depth = depth.saturating_sub(line.matches('}').count())` drops depth to 0, and the break condition `depth == 0 && body.len() > 1 && line.contains('}')` fires early, truncating the window before the body's field-read lines. That is a false negative for `reads_load_options_field_by_field` — the destructure guard silently misses a violating function, which is exactly the "quiet green" the guard was written to refuse. The doc's framing treats the loss as acceptable, but a short window can stop before the field read rather than merely including extra lines.</comment>

<file context>
@@ -2173,3 +2196,314 @@ fn jobs_running_repo_scripts_check_out_the_repo() {
+/// paren of a multi-line signature sits at exactly that column, so the window
+/// closed before the body began and the guard silently checked nothing.
+///
+/// A brace inside a string literal would throw the count off. The window would
+/// run long, which loses a finding rather than inventing one, and telling the
+/// two apart needs a lexer.
</file context>

Suggested change

	/// A brace inside a string literal would throw the count off. The window would
	/// run long, which loses a finding rather than inventing one, and telling the
	/// two apart needs a lexer.
	/// A brace inside a string literal or comment would throw the count off: a `{`
	/// runs the window long and a `}` truncates it short. Either one can drop the
	/// field-read lines from the window, so a function that reads a ProjectLoadOptions
	/// field without destructuring it could pass the guard quietly; telling the two
	/// apart needs a lexer.