Withhold WP timeout verdict the run didn't measure

[jserv]

Two things can make a run say less than its payload appears to, and neither was visible in it. A prover budget is wall clock, so on an oversubscribed host every goal grinds to it whatever its difficulty, and a timeout stops saying anything about the goal. And WP's cache defaults to update, so it replays timeout verdicts as readily as valid ones: a run whose failures all came back from the cache attempted nothing and looked identical to one that did.

run_wp now reads the host load before scheduling any proof, counts how many of its timed-out goals were replayed, and withdraws the confident verdict for either, naming both causes when both apply. The reading is taken before rather than after because a timeout-heavy run drives the one-minute average toward saturation on its own, and a reading taken at response assembly is mostly this server's own provers.

The load reaches the payload as a category and never as a number. run_wp hashes the timeout triage into the proof receipt, so a continuous environment-dependent float there would give two byte-identical runs on the same machine different digests, which is the one property a receipt exists to carry. Rounding does not save it, since 0.42 and 0.55 differ however few decimals they are printed to. The reading is reported beside the response, where nothing hashes it.

Verification profiles gain isystem_paths, nostdinc and rte, and all three join the load identity a receipt is hashed over, because each decides which declarations a file is compiled against or which obligations exist at all. A profile a run or a conclusion will name is refused without rte and nostdinc: otherwise a receipt is checked against an invented default and passes for whichever setting happened to match it. check resolves rte itself rather than leaving it to reload_project, whose fallback of false is right for a load and wrong here, since naming a target used to turn RTE off and quietly shrink the obligation set check reports against.

-nostdinc reaches Frama-C's preprocessor and not the C compiler behind E-ACSL. The modeled libc exists to be analysed rather than compiled, so dropping the real system headers from the gcc that builds the instrumented program leaves it without stdio, and a project that loads cleanly then fails to build.

run_measurement asks the goal's own verdict for whether it timed out. It asked the consolidated one, which is the verdict of the property the goal hangs off, on the line after asking the goal's own verdict for whether it was proved. A timeout under a property that consolidated valid answered "not timed out", which is how a replayed timeout hides behind a confident verdict.

---

Summary by cubic

Withholds WP timeout verdicts when the run didn't measure the goal, and closes three gaps a verdict could pass through.

Host load and cache

• run_wp reads host load before scheduling proofs and reports it as a category beside the response, not in the receipt.
• Timed-out goals replayed from the cache are counted and, with a saturated host, withdraw the confident verdict, naming the cause.
• run_measurement now reads the goal's own verdict for timeout instead of the consolidated property verdict.

Profiles and receipts

• Verification profiles gain isystem_paths, nostdinc, and rte, all hashed into the proof receipt load identity; a profile naming no isystem_paths matches only a load passing none.
• A profile named in a run or conclusion must state rte and nostdinc; otherwise it is refused.
• check resolves rte itself rather than reload_project's fallback, reports RTE_DISABLED when the profile turned RTE off, and reports PROPERTY_VACUOUS for goals proved only under an impossible hypothesis.
• -nostdinc goes to Frama-C's preprocessor only; the E-ACSL compiler keeps system headers.
• The gap logic moved from analysis.rs into checkgaps.rs unchanged, and the test harness now picks the fresher of the release build and Cargo's build.

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

[cubic-dev-ai]

1 issue found across 10 files (changes from recent commits).

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="src/mcp/checkgaps.rs">

<violation number="1" location="src/mcp/checkgaps.rs:515">
P2: For ordered-instance vacuity, `proved_goal_gap` reads `vacuity_reason` and `vacuity_dependency` from the goal, but enrichment leaves those fields only on the property row. Every `PROPERTY_VACUOUS` entry from that path therefore loses the explanation and dependency; copy the fields during goal enrichment or otherwise source them from the matched property.</violation>
</file>

<sub>Reply with feedback, questions, or to request a fix.

Re-trigger cubic</sub>

[cubic-dev-ai]

P2: For ordered-instance vacuity, proved_goal_gap reads vacuity_reason and vacuity_dependency from the goal, but enrichment leaves those fields only on the property row. Every PROPERTY_VACUOUS entry from that path therefore loses the explanation and dependency; copy the fields during goal enrichment or otherwise source them from the matched property.

Prompt for AI agents

Check if this issue is valid — if so, understand the root cause and fix it. At src/mcp/checkgaps.rs, line 515:

<comment>For ordered-instance vacuity, `proved_goal_gap` reads `vacuity_reason` and `vacuity_dependency` from the goal, but enrichment leaves those fields only on the property row. Every `PROPERTY_VACUOUS` entry from that path therefore loses the explanation and dependency; copy the fields during goal enrichment or otherwise source them from the matched property.</comment>

<file context>
@@ -479,6 +489,33 @@ fn proved_goal_gap(goal: &serde_json::Value, status: &str) -> Option<serde_json:
+            "property_status": field("normalized_property_status"),
+
+            // Why Frama-C called it vacuous, when the property row says.
+            "vacuity_reason": field("vacuity_reason"),
+            "vacuity_dependency": field("vacuity_dependency"),
+        }));
</file context>