vscode: redesign the proof job panel

[0xGeorgii]

Follow-up to #519; this is PR 1 of 3. The next two cover the Proof Jobs view and status bar, then the prove flow and docs.

Why

The local test of #519 against the deployed prover showed the panel was hard to read:

• A compile failure said only compile_failed: file did not compile (see build.log). The real cause (clamp already exists) took a database query to find.
• Statuses and claims were raw enums (StructuralOnly, PartialSuccess, prove), and the trust banners used internal terms ("DTOs do not agree", "persisted mode").
• The event log was one flat list of up to 2000 lines, including heartbeats.
• Every update replaced the whole page, which reset focus, open sections and scroll.

Change

• Plain verdicts. jobVerdict.ts is the single source of wording (the tree and status bar use it in the next PR). The fail-closed claim rules are unchanged; the evidence checks moved verbatim into verifierEvidence.ts. A proof is claimed only with a matching result that the independent verifier fully accepted. Raw codes now appear only under a collapsed Technical details section.
• Compile failures. The panel reads build.log and shows the first Rocq error inline, with Go to line N and Open build log. Go to line opens the local .v when it is unchanged, otherwise the uploaded copy. When the error is <stem> already exists, a hint explains the module-named-after-the-file clash.
• Run steps. Submitted › Worker › Proving › Verifying › result, built from the event history. A failed run is marked at the step where it stopped.
• Obligations. Each shows its kind and statement in plain words, whether a template or the agent closed it, its time, goal and source line. Lists of more than ten are grouped. A closed obligation is labelled "Proved" only when the run claims a proof; otherwise "Closed — not verified".
• Activity. Grouped by obligation, with a Steps / Agent / All filter and a text filter. Heartbeats are no longer listed.
• Live timer. Elapsed and remaining time against the budget. The deadline comes from the job (Inferara/inference-ai-prover#270), else the job.queued event, else submission time plus budget.
• Stable updates. The page is set once and then patched by region (ready handshake → snapshot → region diffs). Loading states make no claim. Panels are restored after a window reload (WebviewPanelSerializer, onWebviewPanel:inference.proofJob), and the tab has an icon.
• Native look. Theme colours only (the hard-coded #fff/#1e1e1e badge text is gone), inline codicon-style SVG icons, high-contrast and reduced-motion rules, focus outlines, and ARIA roles for the verdict, progress and filters.
• Visual harness. test/visual/render.ts renders every state under dark, light and both high-contrast themes. It lives under test/, so it is not packaged.

No new packaged files: the .vsix keeps the same 11 entries.

Verification

In node:24: npx tsc --noEmit -p .; npm test (482 pass); npm run "test syntax" (93 pass); npm run package, then the CI file-list check.

New tests:

• the verdict matrix, plus an exhaustive check that the success tone and claim appear only with full evidence;
• the run model;
• build-log parsing (the real clamp already exists log);
• loading and accessibility.

I also rendered all 12 states × 4 themes and reviewed the screenshots.

Risk

The webview patch protocol is new, and the full snapshot on ready keeps it recoverable. Claim rules are not edited, and the property test guards them. ProveOutcome and SubmitOutcome gain fields (vSha256, sha256) used to remember which local file a job came from.

🤖 Generated with Claude Code

Confidence Score: 5/5

The PR appears safe to merge; the remaining browser-test suggestion is non-blocking.

Findings

1.  Stable updates lack tests ▶

Diagram

sequenceDiagram
    participant Host as Extension
    participant Page as Proof-job page
    participant Server as Proof server
    Host->>Page: Set page shell
    Page->>Host: ready
    Host->>Page: snapshot (regions, activity, clock)
    Server-->>Host: Job detail and events
    Host->>Page: Changed regions
    Host->>Page: New activity
    Host->>Page: Changed clock
    Page->>Page: Restore open sections and focus

Loading

_{Reviews (3) · Last reviewed commit: "vscode: address review of the job panel" · Reviewed by Greptile}

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!