diff --git a/editors/vscode/package.json b/editors/vscode/package.json index 07a809b0..eccf3f9d 100644 --- a/editors/vscode/package.json +++ b/editors/vscode/package.json @@ -29,7 +29,8 @@ "workspaceContains:**/*.inf", "onLanguage:inference", "onView:inference.configView", - "onView:inference.proofJobsView" + "onView:inference.proofJobsView", + "onWebviewPanel:inference.proofJob" ], "contributes": { "viewsContainers": { diff --git a/editors/vscode/src/prover/buildLog.ts b/editors/vscode/src/prover/buildLog.ts new file mode 100644 index 00000000..99525cd1 --- /dev/null +++ b/editors/vscode/src/prover/buildLog.ts @@ -0,0 +1,98 @@ +/** + * The first error in a server build log (`build.log`, Rocq output). Pure — no + * `vscode` import. + * + * Rocq reports `File "", line N, characters A-B:` followed by the + * message. The server compiles the uploaded file in place (only the proof + * terminators change), so line N is line N of the submitted `.v`. + */ + +export interface BuildError { + /** 1-based line in the compiled file, when the log names one. */ + line?: number; + /** 0-based character range on that line. */ + startChar?: number; + endChar?: number; + /** The message without its `Error:` prefix, at most 600 characters. */ + message: string; +} + +const LOCATION = /^File "[^"]*", line (\d+), characters (\d+)-(\d+):\s*$/; + +function clean(lines: string[]): string { + const text = lines + .join('\n') + .replace(/^\s*Error:\s*/, '') + .trim(); + return text.length > 600 ? `${text.slice(0, 600)}…` : text; +} + +/** + * First located error, else the first `Error:` block, else null. Warnings use + * the same location header, so a located block counts only when its message + * is an error. + */ +export function firstBuildError(log: string): BuildError | null { + const lines = log.replace(/\r\n?/g, '\n').split('\n'); + for (let i = 0; i < lines.length; i++) { + const m = LOCATION.exec(lines[i]); + if (!m) { + continue; + } + const body: string[] = []; + for (let j = i + 1; j < lines.length; j++) { + if (LOCATION.test(lines[j]) || (lines[j].trim() === '' && body.length > 0)) { + break; + } + body.push(lines[j]); + } + if (!/^\s*Error:/.test(body.find((l) => l.trim() !== '') ?? '')) { + continue; + } + const message = clean(body); + if (message) { + return { + line: Number(m[1]), + startChar: Number(m[2]), + endChar: Number(m[3]), + message, + }; + } + } + const errorAt = lines.findIndex((l) => /^\s*Error:/.test(l)); + if (errorAt >= 0) { + const body: string[] = []; + for (let j = errorAt; j < lines.length && (j === errorAt || lines[j].trim() !== ''); j++) { + body.push(lines[j]); + } + const message = clean(body); + return message ? { message } : null; + } + return null; +} + +/** + * A hint for ` already exists`: the compiler names the module after the + * file, so a function with the file's name defines it twice. + */ +export function duplicateNameHint(message: string, fileStems: readonly string[]): string | null { + const m = /^(\S+) already exists\.?$/.exec(message.split('\n')[0].trim()); + if (!m) { + return null; + } + const name = m[1]; + if (fileStems.includes(name)) { + return `The compiler names the module after the file, so a function also named “${name}” defines “${name}” twice. Rename the file or the function, then prove again.`; + } + return `“${name}” is defined twice in the generated file.`; +} + +/** File name without directory and final extension. */ +export function fileStem(name: string | null | undefined): string | null { + if (!name) { + return null; + } + const base = name.split(/[\\/]/).pop() ?? name; + const dot = base.lastIndexOf('.'); + return dot > 0 ? base.slice(0, dot) : base; +} diff --git a/editors/vscode/src/prover/eventFormat.ts b/editors/vscode/src/prover/eventFormat.ts index 184bb76e..52539ddf 100644 --- a/editors/vscode/src/prover/eventFormat.ts +++ b/editors/vscode/src/prover/eventFormat.ts @@ -17,7 +17,7 @@ const MAX_PAYLOAD_CHARS = 160; const MAX_ACTIVITY_CHARS = 240; /** Server-originated agent limits (`agent.limited.code`), as the portal words them. */ -const AGENT_LIMIT_MESSAGES: Readonly> = { +export const AGENT_LIMIT_MESSAGES: Readonly> = { AGENT_REQUEST_LIMIT: 'Agent request limit reached. No further model requests are allowed for this job.', AGENT_PROVIDER_RATE_LIMITED: @@ -69,7 +69,7 @@ function clip(text: string, max: number): string { * One `agent.activity` payload as a readable line. The kinds mirror the * portal's transcript (`portal/src/lib/store.ts::applyActivity`). */ -function summarizeActivity(p: Record): string { +export function summarizeActivity(p: Record): string { const kind = str(p.kind) ?? ''; const detail = str(p.detail) ?? ''; if (kind === 'truncated') { @@ -110,7 +110,7 @@ function activityScope(p: Record): string { } /** Per-type human summary of an event payload ('' = type alone suffices). */ -function summarize(env: EventEnvelope): string { +export function summarize(env: EventEnvelope): string { const p = asRecord(env.payload); const name = str(p.name); const attempt = num(p.attempt); diff --git a/editors/vscode/src/prover/index.ts b/editors/vscode/src/prover/index.ts index bfaef652..2a1644a0 100644 --- a/editors/vscode/src/prover/index.ts +++ b/editors/vscode/src/prover/index.ts @@ -1,6 +1,6 @@ import * as vscode from 'vscode'; -import { hasApiKey, SERVER_URL_SETTING, updateConfiguredContext } from './config'; +import { hasApiKey, resolveConfig, SERVER_URL_SETTING, updateConfiguredContext } from './config'; import { cancelJobInteractive, compareProof, @@ -8,7 +8,8 @@ import { openInPortal, resubmitJob, } from './jobActions'; -import { JobDetailViewManager } from './jobDetailView'; +import { JOB_PANEL_VIEW_TYPE, JobDetailViewManager } from './jobDetailView'; +import { JobOrigins, type JobOrigin } from './jobOrigins'; import { FILTER_STATUSES } from './jobList'; import { JobTreeItem, ProofJobsProvider } from './jobsTree'; import { ProofDocuments } from './proofDocuments'; @@ -40,21 +41,53 @@ export function registerProver( const jobs = new ProofJobsProvider(secrets, log); const view = vscode.window.createTreeView('inference.proofJobsView', { treeDataProvider: jobs }); const documents = new ProofDocuments(secrets); - const panels = new JobDetailViewManager(secrets, log, documents, () => void jobs.refresh()); - disposables.push(jobs, view, documents, panels); + const origins = new JobOrigins(context.workspaceState); + /** The local files a job was uploaded from, when this workspace knows them. */ + const originOf = async (jobId: string): Promise => { + const config = await resolveConfig(secrets).catch(() => null); + return config ? origins.get(config.serverUrl, jobId) : undefined; + }; + const runAgain = async (job: JobResponse) => { + const fresh = await resubmitJob(secrets, log, job); + if (fresh) { + await showJob(fresh, await originOf(job.id)); + } + }; + const panels = new JobDetailViewManager( + context.extensionUri, + secrets, + log, + documents, + origins, + () => void jobs.refresh(), + runAgain, + ); + disposables.push( + jobs, + view, + documents, + panels, + vscode.window.registerWebviewPanelSerializer(JOB_PANEL_VIEW_TYPE, panels), + ); disposables.push(view.onDidChangeVisibility((e) => jobs.setVisible(e.visible))); if (view.visible) { jobs.setVisible(true); } - const showJob: SubmitHooks['showJob'] = async (job, source) => { + const showJob: SubmitHooks['showJob'] = async (job, origin) => { + if (origin) { + const config = await resolveConfig(secrets).catch(() => null); + if (config) { + await origins.set(config.serverUrl, job.id, origin); + } + } await jobs.refresh(); const node = jobs.findNode(job.id); if (node && view.visible) { await view.reveal(node, { select: true, focus: false }); } - await panels.open(job, source); + await panels.open(job, origin); }; const jobOf = (arg: unknown): JobResponse | undefined => arg instanceof JobTreeItem ? arg.job : undefined; @@ -96,9 +129,8 @@ export function registerProver( }); command('inference.resubmitProofJob', async (arg) => { const job = jobOf(arg); - const fresh = job && (await resubmitJob(secrets, log, job)); - if (fresh) { - await showJob(fresh); + if (job) { + await runAgain(job); } }); command('inference.copyProofJobId', async (arg) => { diff --git a/editors/vscode/src/prover/jobActions.ts b/editors/vscode/src/prover/jobActions.ts index aab9c75b..586a6de2 100644 --- a/editors/vscode/src/prover/jobActions.ts +++ b/editors/vscode/src/prover/jobActions.ts @@ -160,10 +160,11 @@ export async function compareProof( export async function openInPortal( secrets: vscode.SecretStorage, job: JobRef, - tab: 'certificate' | undefined = 'certificate', + page: 'certificate' | 'job' = 'certificate', ): Promise { const config = await requireConfig(secrets); if (config) { + const tab = page === 'certificate' ? 'certificate' : undefined; await vscode.env.openExternal(vscode.Uri.parse(portalJobUrl(config.serverUrl, job.id, tab))); } } diff --git a/editors/vscode/src/prover/jobDetailHtml.ts b/editors/vscode/src/prover/jobDetailHtml.ts index a0bbc37b..da29c63f 100644 --- a/editors/vscode/src/prover/jobDetailHtml.ts +++ b/editors/vscode/src/prover/jobDetailHtml.ts @@ -1,128 +1,37 @@ /** - * Pure HTML renderer for the proof-job detail webview. + * Pure HTML renderer for the proof-job panel. * - * Deliberately free of any `vscode` import so it can be unit-tested under - * plain node. All server-originated strings are HTML-escaped here — the - * webview must never interpolate them raw. Styling uses VS Code theme - * variables (`--vscode-*`) so the view follows the user's theme. - */ - -import { isProvedSuccess } from './jobPresentation'; -import type { - AssumptionReport, - JobResponse, - JobResultResponse, - ObligationDto, -} from './types'; - -/** Statuses the control plane treats as terminal (mirrors the server). */ -const TERMINAL_STATUSES: ReadonlySet = new Set([ - 'Succeeded', - 'CompileGoals', - 'PartialSuccess', - 'Failed', - 'TimedOut', - 'Lost', - 'Canceled', - 'ProvisionFailed', -]); - -/** - * Statuses `POST /jobs/{id}/cancel` accepts (mirrors the server's switch); - * everything else — including Verifying and Canceling — is 409 NOT_CANCELABLE. - */ -const CANCELABLE_STATUSES: ReadonlySet = new Set([ - 'Accepted', - 'Queued', - 'Provisioning', - 'Booting', - 'Running', -]); - -/** Event-log lines kept per job, in the host and in the webview DOM. */ -export const EVENT_LOG_CAP = 2000; - -/** Artifact kinds that are text and open as read-only documents. */ -const TEXT_ARTIFACT_KINDS: ReadonlySet = new Set([ - 'InputV', - 'CompletedV', - 'Report', - 'Goals', - 'BuildLog', - 'AgentLog', - 'RefutationV', - 'RefutationMd', -]); - -export function isTextArtifactKind(kind: string): boolean { - return TEXT_ARTIFACT_KINDS.has(kind); -} - -/** The run phases in order; the last chip is the terminal result. */ -const PHASES = ['Accepted', 'Queued', 'Provisioning', 'Booting', 'Running', 'Verifying'] as const; - -export type PhaseState = 'done' | 'active' | 'todo' | 'past' | 'ok' | 'warn' | 'err'; - -/** - * Phase ribbon chips for a status. A live job marks earlier phases done and - * its own active. A finished job does not record which phases it reached - * (ProvisionFailed never booted), so earlier chips are neutral and only the - * result chip carries a tone. - */ -export function phaseRibbon( - status: string, - provedSuccess: boolean, -): Array<{ name: string; state: PhaseState }> { - const index = (PHASES as readonly string[]).indexOf(status); - if (index >= 0) { - return [ - ...PHASES.map((name, i) => ({ - name, - state: (i < index ? 'done' : i === index ? 'active' : 'todo') as PhaseState, - })), - { name: 'Result', state: 'todo' }, - ]; - } - if (status === 'Canceling') { - return [ - ...PHASES.map((name) => ({ name, state: 'past' as PhaseState })), - { name: 'Canceling', state: 'active' }, - ]; - } - const tone = statusClass(status, provedSuccess); - return [ - ...PHASES.map((name) => ({ name, state: 'past' as PhaseState })), - { name: status, state: tone === 'active' ? 'warn' : tone }, - ]; -} - -function fmtBudget(seconds: number): string { - const h = Math.floor(seconds / 3600); - const m = Math.floor((seconds % 3600) / 60); - const s = seconds % 60; - return [h ? `${h}h` : '', m ? `${m}m` : '', s || (!h && !m) ? `${s}s` : ''] - .filter(Boolean) - .join(' '); -} - -export function isTerminalStatus(status: string): boolean { - return TERMINAL_STATUSES.has(status); -} - -/** - * Statuses that end the server's event stream. `Lost` is soft-terminal: the - * reaper re-queues it (bounded retry, Lost → Queued) and `StreamEvents` - * deliberately keeps the SSE stream open without an `end` frame — so the - * client must keep its transport (stream + polls) alive on Lost too, or it - * freezes on a job that is actively being rerun. + * Free of any `vscode` import so it is unit-tested under plain node. Every + * server-originated string is HTML-escaped here; the webview script never + * interpolates data into markup (activity rows use textContent). + * + * The page is a fixed shell (`renderShell`) with named regions the host + * patches in place (`renderRegions`), so updates keep focus, open sections + * and scroll positions. `renderJobDetailHtml` returns shell + regions in one + * document for tests and the visual harness. */ -export function isStreamTerminalStatus(status: string): boolean { - return TERMINAL_STATUSES.has(status) && status !== 'Lost'; -} -export function isCancelableStatus(status: string): boolean { - return CANCELABLE_STATUSES.has(status); -} +import { jobDetailScript } from './jobDetailScript'; +import { + buildJobView, + type ActionView, + type CheckView, + type EvidenceView, + type JobView, + type JobViewInput, + type LiveMode, + type ObligationView, + type StepView, +} from './jobDetailModel'; +import { JOB_DETAIL_STYLES } from './jobDetailStyles'; +import type { Tone, VerdictIcon } from './jobVerdict'; +import { EVENT_LOG_CAP, type ActivityRow } from './runModel'; +import type { JobResponse } from './types'; +import { icon, type IconName } from './webviewIcons'; + +export { isCancelableStatus, isStreamTerminalStatus, isTerminalStatus, isTextArtifactKind } from './jobStatus'; +export { EVENT_LOG_CAP } from './runModel'; +export type { LiveMode } from './jobDetailModel'; export function escapeHtml(value: string): string { return value @@ -133,695 +42,426 @@ export function escapeHtml(value: string): string { .replace(/'/g, '''); } -/** Map a job status onto one of the badge color classes defined in the CSS. */ -function statusClass( - status: string, - provedSuccess: boolean, -): 'ok' | 'warn' | 'err' | 'active' { - switch (status) { - case 'Succeeded': - return provedSuccess ? 'ok' : 'warn'; - case 'CompileGoals': - case 'PartialSuccess': - case 'Canceled': - return 'warn'; - case 'Failed': - case 'TimedOut': - case 'Lost': - case 'ProvisionFailed': - return 'err'; - default: - return 'active'; - } +const esc = escapeHtml; + +export const REGION_IDS = [ + 'banner', + 'header', + 'steps', + 'verdict', + 'progress', + 'obligations', + 'evidence', + 'files', + 'tech', +] as const; + +export type RegionId = (typeof REGION_IDS)[number]; +export type Regions = Record; + +const VERDICT_ICONS: Record = { + pass: 'pass', + warning: 'warning', + error: 'error', + refuted: 'refuted', + running: 'running', + waiting: 'waiting', + verifying: 'verifying', + canceled: 'canceled', + loading: 'loading', +}; + +function verdictIcon(name: VerdictIcon): string { + return icon(VERDICT_ICONS[name], name === 'running' || name === 'loading' ? 'spin' : ''); } -function obligationStatusClass(status: string | null | undefined): string { - switch (status) { - case 'proved': - return 'ok'; - case 'failed': +function toneIcon(tone: Tone): IconName { + switch (tone) { + case 'ok': + return 'pass'; + case 'err': + return 'error'; case 'refuted': - return 'err'; - case 'skipped': - return 'warn'; + return 'refuted'; + case 'warn': + return 'warning'; + case 'active': + return 'running'; default: - return 'active'; + return 'dot'; } } -function fmtDuration(ms: number | null | undefined): string { - if (ms === null || ms === undefined) { - return '—'; - } - if (ms < 1000) { - return `${ms} ms`; - } - const s = ms / 1000; - return s < 60 ? `${s.toFixed(1)} s` : `${Math.floor(s / 60)}m ${Math.round(s % 60)}s`; +function dataAttrs(data: Record | undefined): string { + return Object.entries(data ?? {}) + .map(([k, v]) => ` data-${k.replace(/[^a-z0-9-]/g, '')}="${esc(v)}"`) + .join(''); } -function fmtBytes(bytes: number): string { - if (bytes < 1024) { - return `${bytes} B`; - } - const kib = bytes / 1024; - return kib < 1024 ? `${kib.toFixed(1)} KiB` : `${(kib / 1024).toFixed(2)} MiB`; +function button(a: ActionView, extraClass = ''): string { + const cls = [a.style ?? 'secondary', extraClass].filter(Boolean).join(' '); + const focusKey = `${a.action}:${a.data?.artifact ?? ''}:${a.data?.line ?? ''}:${a.data?.obligation ?? ''}`; + return ``; } -function fmtTimestamp(iso: string | null | undefined): string { - if (!iso) { - return '—'; +// ── Regions ───────────────────────────────────────────────────────────── + +function bannerRegion(view: JobView): string { + if (!view.banner) { + return ''; } - const d = new Date(iso); - return Number.isNaN(d.getTime()) ? escapeHtml(iso) : d.toLocaleString(); + const tone = view.banner.tone; + return ``; } -function metaRow(label: string, valueHtml: string): string { - return `
${escapeHtml(label)}
${valueHtml}
`; +function liveIndicator(live: LiveMode): string { + switch (live) { + case 'sse': + return `${icon('dot')}Live`; + case 'poll': + return `${icon('dot')}Polling`; + default: + return ''; + } } -function obligationRow(o: ObligationDto): string { - const status = o.status ?? 'pending'; - const content = o.content ?? 'unknown'; - const main = ` - ${escapeHtml(o.name)} - ${escapeHtml(o.kind)} - ${escapeHtml(content)} - ${escapeHtml(status)} - ${o.attempts ?? '—'} - ${fmtDuration(o.durationMs)} - ${o.lastError ? escapeHtml(o.lastError) : ''} - `; - // The goal state at this obligation's `Proof.` (compile-goals flow) — shown - // as a full-width sub-row beneath the obligation so multi-line goals are readable. - const goalRow = o.goal - ? `
goal
${escapeHtml(o.goal)}
` - : ''; - return main + goalRow; +function headerRegion(view: JobView): string { + const v = view.verdict; + return `
+
+
${verdictIcon(v.icon)}

${esc(view.title)}

${esc(v.badge)}
+ ${view.subtitle ? `
Uploaded as ${esc(view.subtitle)}
` : ''} +
+
${liveIndicator(view.live)}${view.headerActions.map((a) => button(a)).join('')}
+
`; } -/** ✓/✗ badge for a verifier verdict flag (null = verifier did not report). */ -function verdictFlag( - label: string, - value: boolean | null | undefined, - goodWhen: boolean, - unexpectedTone: 'warn' | 'err' = 'err', -): string { - if (value === null || value === undefined) { - return metaRow(label, '—'); +const STEP_SR: Record = { + done: 'done', + active: 'in progress', + todo: 'not started', + unknown: 'not recorded', + stopped: 'stopped here', + final: 'result', +}; + +function stepIcon(step: StepView, verdict: JobView['verdict']): string { + switch (step.state) { + case 'done': + return icon('pass'); + case 'active': + return step.key === 'result' ? verdictIcon(verdict.icon) + : step.key === 'worker' || step.key === 'submitted' ? icon('waiting') : icon('running', 'spin'); + case 'todo': + return icon('todo'); + case 'unknown': + return icon('dot'); + case 'stopped': + return icon(step.tone === 'muted' ? 'canceled' : toneIcon(step.tone ?? 'err')); + case 'final': + return verdictIcon(verdict.icon); } - const good = value === goodWhen; - return metaRow( - label, - `${value ? 'yes' : 'no'}`, - ); } -function markersFlag(value: number | null | undefined): string { - if (value === null || value === undefined) { - return metaRow('Proof markers remaining', '—'); - } - return metaRow( - 'Proof markers remaining', - `${value}`, - ); +function stepsRegion(view: JobView): string { + const items = view.steps.map((step, i) => { + const tone = step.tone ? ` tone-${step.tone}` : ''; + const title = step.at ? ` title="Started ${esc(new Date(step.at).toLocaleTimeString())}"` : ''; + return `
  • ${ + i > 0 ? `` : '' + }${stepIcon(step, view.verdict)}${esc(step.label)}, ${STEP_SR[step.state]}
    • `; + }); + return `
      ${items.join('')}
    `; } -function normalizedVerifierOutcome( - result: JobResultResponse | null | undefined, -): string | null { - const value = result?.verificationOutcome?.trim().toLowerCase(); - return value || null; +function verdictRegion(view: JobView): string { + const v = view.verdict; + const code = (v.kind === 'compile-error' || v.kind === 'completed-compile-error') && view.verdictBodyIsCode; + return `
    +

    ${verdictIcon(v.icon)}${esc(v.headline)}

    + ${code ? `
    ${esc(v.body)}
    ` : `

    ${esc(v.body)}

    `} + ${v.caveats.length ? `
      ${v.caveats.map((c) => `
    • ${esc(c)}
      • `).join('')}
    ` : ''} + ${view.actions.length ? `
    ${view.actions.map((a) => button(a)).join('')}
    ` : ''} +
    `; } -function normalizedAssumptionReports( - result: JobResultResponse, -): AssumptionReport[] | null { - const reports = result.assumptionReports; - if (!Array.isArray(reports)) return null; - for (const report of reports) { - if (!report || typeof report.target !== 'string' || !report.target || - typeof report.kernelOutput !== 'string' || !report.kernelOutput || - typeof report.policyPassed !== 'boolean' || - !Array.isArray(report.assumptions)) { - return null; - } - for (const assumption of report.assumptions) { - if (!assumption || typeof assumption.name !== 'string' || !assumption.name || - typeof assumption.type !== 'string' || !assumption.type || - (assumption.kind !== 'axiom' && assumption.kind !== 'sectionVariable')) { - return null; - } - } +function clockFallback(view: JobView): string { + const budget = view.clock.budgetSeconds; + if (!budget) { + return ''; } - return reports; + const h = Math.floor(budget / 3600); + const m = Math.floor((budget % 3600) / 60); + return `Time budget ${h ? `${h}h${m ? ` ${m}m` : ''}` : m ? `${m}m` : `${budget}s`}`; } -function hasCompleteAssumptionEvidence( - result: JobResultResponse, - expectedTargets: string[], -): boolean { - const reports = normalizedAssumptionReports(result); - if (!result.assumptionPolicyId?.trim() || !reports) return false; - const names = new Set(reports.map((report) => report.target)); - const expected = new Set(expectedTargets); - return reports.length === result.holesClosed - && names.size === reports.length - && expected.size === expectedTargets.length - && expected.size === result.holesClosed - && reports.every((report) => expected.has(report.target)) - && reports.every((report) => report.policyPassed); +function progressRegion(view: JobView): string { + const p = view.progress; + const clock = ``; + if (!p.known) { + return `

    Obligations

    ${clock}
    `; + } + const pct = (n: number) => (p.total > 0 ? Math.min(100, Math.round((n / p.total) * 1000) / 10) : 0); + return `
    +

    Obligations ${p.closed}/${p.total}

    ${ + p.failed > 0 ? `${p.failed} not closed` : '' + }${clock}
    +
    +
    `; } -function verifierAcceptedFull( - result: JobResultResponse, - expectedTargets: string[], -): boolean { - return ( - normalizedVerifierOutcome(result) === 'succeeded' && - result.compileOk === true && - result.assumptionsClosed === true && - result.verifiedClean === true && - result.admitsDetected === false && - result.statementsImmutable === true && - result.markersRemaining === 0 && - hasCompleteAssumptionEvidence(result, expectedTargets) - ); +function obligationDetails(o: ObligationView): string { + const key = `obl:${o.name}`; + const meta = [ + o.by ? `${o.by === 'template' ? 'template' : `agent${o.attempts && o.attempts > 0 ? ` #${o.attempts}` : ''}`}` : '', + o.duration ? `${esc(o.duration)}` : '', + `${esc(o.statusLabel)}`, + ].join(''); + const facts = [ + `
    Theorem
    ${esc(o.name)}
    `, + `
    Statement
    ${esc(o.contentLabel)}
    `, + o.specList ? `
    Specification
    ${esc(o.specList)}
    ` : '', + o.attempts ? `
    Attempts
    ${o.attempts}
    ` : '', + ].join(''); + const goto = o.goto.target === 'proof' + ? button({ + action: 'gotoTheorem', label: 'Go to proof', icon: 'goto', data: { obligation: o.name, artifact: o.goto.artifact }, + ariaLabel: `Show the proof of ${o.shortName} in the completed file`, + }, 'link') + : button({ + action: 'gotoTheorem', label: 'Go to theorem', icon: 'goto', + data: { obligation: o.name, ...(o.goto.line !== undefined ? { line: String(o.goto.line) } : {}) }, + ariaLabel: `Go to ${o.shortName} in the submitted file`, + }, 'link'); + const actions = [ + goto, + ``, + ].join(''); + return `
    + ${o.status === 'pending' || o.statusLabel === 'Not attempted' ? icon('todo') : icon(toneIcon(o.tone), o.status === 'running' ? 'spin' : '')}${esc(o.shortName)}${esc(o.kindLabel)}${meta}${icon('chevron')} +
    +
    ${facts}
    + ${o.lastError ? `
    ${icon('error')}${esc(o.lastError)}
    ` : ''} + ${o.goal ? `
    Goal
    ${esc(o.goal)}
    ` : ''} +
    ${actions}
    +
    +
    `; } -function verifierAcceptedPartial( - result: JobResultResponse, - expectedTargets: string[], -): boolean { - // Partial verification intentionally leaves the unfilled obligations - // admitted, so verifiedClean=false/admitsDetected=true are expected here. - return ( - normalizedVerifierOutcome(result) === 'partial' && - result.compileOk === true && - result.assumptionsClosed === true && - result.verifiedClean === false && - result.admitsDetected === true && - result.statementsImmutable === true && - result.markersRemaining === 0 && - hasCompleteAssumptionEvidence(result, expectedTargets) - ); +const GROUP_TITLES: Record = { + active: 'Working', + problem: 'Not closed', + waiting: 'Waiting', + done: 'Closed', +}; + +/** + * The closed group is titled like its rows ("Proved" only when the run's + * verdict claims a proof; else "Closed" or "Closed — not verified"). + */ +function groupTitle(group: ObligationView['group'], items: readonly ObligationView[]): string { + return group === 'done' && items[0] ? items[0].statusLabel : GROUP_TITLES[group]; } -function assumptionEvidenceHtml(result: JobResultResponse): string { - const reports = normalizedAssumptionReports(result); - if (!reports || !result.assumptionPolicyId?.trim()) { - return '

    Kernel-reported assumptions

    Per-theorem Print Assumptions evidence is unavailable.

    '; +function obligationsRegion(view: JobView): string { + const list = view.obligations; + if (list === null) { + return `
    Loading obligations…
    `; } - const renderedReports = reports.map((report) => { - const rows = report.assumptions.length - ? report.assumptions.map((assumption) => ` - ${escapeHtml(assumption.kind)} - ${escapeHtml(assumption.name)} - ${escapeHtml(assumption.type)} - `).join('') - : 'Closed under the global context; no assumptions reported.'; - return `

    ${escapeHtml(report.target)} ${report.policyPassed ? 'policy passed' : 'policy rejected'}

    - ${rows}
    KindDependencyKernel type
    -
    Normalized Print Assumptions output
    ${escapeHtml(report.kernelOutput)}
    `; - }).join(''); - return `

    Kernel-reported assumptions

    -

    Reviewed policy: ${escapeHtml(result.assumptionPolicyId)}

    ${renderedReports}`; + if (list.length === 0) { + const text = view.terminal || view.verdict.kind === 'canceling' + ? 'No obligations were reported for this run.' + : 'Obligations appear once the worker has compiled the file.'; + return `

    ${text}

    `; + } + if (list.length <= 10) { + return `
    ${list.map(obligationDetails).join('')}
    `; + } + const groups = (['active', 'problem', 'waiting', 'done'] as const) + .map((g) => [g, list.filter((o) => o.group === g)] as const) + .filter(([, items]) => items.length > 0) + .map(([g, items]) => `
    ${icon('chevron')}${esc(groupTitle(g, items))} (${items.length})${items.map(obligationDetails).join('')}
    `); + return `
    ${groups.join('')}
    `; } -function artifactRow(a: JobResultResponse['artifacts'][number]): string { - const open = isTextArtifactKind(a.kind) - ? ` ` - : ''; - return ` - ${escapeHtml(a.filename)} - ${escapeHtml(a.kind)} - ${fmtBytes(a.sizeBytes)} - ${open} - `; -} +const CHECK_ICONS: Record = { pass: 'pass', fail: 'error', warn: 'warning', unknown: 'dot' }; +const CHECK_SR: Record = { pass: 'passed', fail: 'failed', warn: 'partial', unknown: 'not reported' }; -/** - * Result actions: open the proof or refutation, compare it with the input, - * and open the exportable certificate in the portal (the claim rules have one - * implementation, the portal's certificate builder). - */ -function resultActions(result: JobResultResponse, terminal: boolean): string { - const kinds = new Set(result.artifacts.map((a) => a.kind)); - const buttons: string[] = []; - const completed = result.artifacts.find((a) => a.kind === 'CompletedV'); - if (completed) { - buttons.push(``); - if (kinds.has('InputV')) { - buttons.push(''); - } +function evidenceBody(e: EvidenceView): string { + if (e.kind === 'worker-only') { + return '

    Not independently verified — this result was checked only inside the worker.

    '; } - const refutation = result.artifacts.find((a) => a.kind === 'RefutationV'); - if (refutation) { - buttons.push(``); + if (e.kind === 'not-applicable') { + return '

    Not applicable — this run only compiled the file.

    '; } - if (terminal) { - buttons.push(''); + const checks = e.checks + .map((c) => `
  • ${icon(CHECK_ICONS[c.state])}${esc(c.label)}${c.detail ? ` — ${esc(c.detail)}` : ''}: ${CHECK_SR[c.state]}
    • `) + .join(''); + const reports = e.reports + ? e.reports + .map((r) => { + const rows = r.assumptions.length + ? r.assumptions + .map((a) => `${a.kind === 'axiom' ? 'axiom' : 'section variable'}${esc(a.name)}${esc(a.type)}`) + .join('') + : 'Closed under the global context; no assumptions.'; + return `
    ${icon('chevron')}${icon(r.policyPassed ? 'pass' : 'error')}${esc(r.target)}— ${r.policyPassed ? 'policy passed' : 'policy rejected'} · ${r.assumptions.length} ${r.assumptions.length === 1 ? 'assumption' : 'assumptions'} +${rows}
    KindDependencyKernel type
    +
    ${icon('chevron')}Normalized Print Assumptions output
    ${esc(r.kernelOutput)}
    `; + }) + .join('') + : '

    Per-theorem Print Assumptions evidence is unavailable.

    '; + return `

    Independent verifier: ${esc(e.outcome ?? '')}${e.verifiedAt ? ` · ${esc(e.verifiedAt)}` : ''}

    +
      ${checks}
    +

    Kernel-reported assumptions

    +${e.policyId ? `

    Reviewed policy ${esc(e.policyId)}

    ` : ''} +${reports}`; +} + +function section(key: string, title: string, body: string, open = false): string { + return `
    ${icon('chevron')}

    ${title}

    ${body}
    `; +} + +function evidenceRegion(view: JobView): string { + if (!view.evidence) { + return ''; } - return buttons.length > 0 ? `
    ${buttons.join('')}
    ` : ''; + return section('sec:evidence', 'How this was verified', evidenceBody(view.evidence), view.verdict.kind === 'rejected'); } -/** Live-update mode the hosting view is currently in. */ -export type LiveMode = 'sse' | 'poll' | 'terminal'; +function filesRegion(view: JobView): string { + if (!view.files) { + return ''; + } + const body = view.files.length + ? `
      ${view.files + .map((f) => `
    • ${icon('file')}${esc(f.filename)}${esc(f.kindLabel)} · ${esc(f.size)}${ + f.text + ? button({ action: 'openArtifact', label: 'Open', data: { artifact: f.id }, ariaLabel: `Open ${f.filename}` }, 'link') + : '' + }${button({ action: 'downloadArtifact', label: 'Download', icon: 'download', data: { artifact: f.id }, ariaLabel: `Download ${f.filename}` }, 'link')}
      • `) + .join('')}
    ` + : '

    No files were stored for this run.

    '; + return section('sec:files', `Files (${view.files.length})`, body); +} -function liveNote(mode: LiveMode): string { - switch (mode) { - case 'sse': - return 'Live — streaming events from the server.'; - case 'poll': - return 'Polling every 5 s (live stream unavailable).'; - case 'terminal': - return 'Job is terminal — auto-refresh stopped.'; +function techRegion(view: JobView): string { + const rows = view.tech + .map((r) => `
    ${esc(r.label)}
    ${r.mono ? `${esc(r.value)}` : esc(r.value)}
    `) + .join(''); + return section('sec:tech', 'Technical details', `
    ${rows}
    ${button({ action: 'copyJobId', label: 'Copy job ID', icon: 'copy' }, 'link')}
    `); +} + +/** Every region of the panel for one view, as escaped HTML. */ +export function renderRegions(view: JobView): Regions { + return { + banner: bannerRegion(view), + header: headerRegion(view), + steps: stepsRegion(view), + verdict: verdictRegion(view), + progress: progressRegion(view), + obligations: obligationsRegion(view), + evidence: evidenceRegion(view), + files: filesRegion(view), + tech: techRegion(view), + }; +} + +/** Activity rows as markup identical to what the webview script builds. */ +export function renderActivityRows(rows: readonly ActivityRow[]): string { + if (rows.length === 0) { + return '
    No activity yet.
    '; + } + let last: string | null = null; + const out: string[] = []; + for (const r of rows) { + const key = r.obligation ?? ''; + if (key !== last && (key || last)) { + const short = key ? key.slice(key.lastIndexOf('__') > 0 ? key.lastIndexOf('__') + 2 : 0) || key : 'Run'; + out.push(`
    ${esc(short)}
    `); + } + last = key; + const d = new Date(r.ts); + const p = (n: number) => String(n).padStart(2, '0'); + const clock = Number.isNaN(d.getTime()) ? '' : `${p(d.getHours())}:${p(d.getMinutes())}:${p(d.getSeconds())}`; + out.push(`
    ${ + r.attempt ? `#${r.attempt}` : '' + }${esc(r.text)}
    `); } + return out.join(''); } -export interface RenderOptions { - /** Name of the source `.inf`, when this extension compiled the upload. */ - source?: string | null; - /** CSP nonce for the inline script. */ +export interface ShellOptions { nonce: string; - /** `webview.cspSource` of the hosting panel. */ cspSource: string; - /** Fetch-failure banner (stale data below stays visible), or null. */ - error?: string | null; - /** Current update mode, shown next to the Refresh button. */ - live: LiveMode; - /** Pre-formatted event log lines (oldest first); escaped at render. */ - eventLog: readonly string[]; - /** Show the Cancel button (status must be server-cancelable). */ - canCancel: boolean; - /** Terminal result metadata and artifacts, once fetched. */ - result?: JobResultResponse | null; + /** Regions to render inline (tests, harness); empty placeholders otherwise. */ + regions?: Partial; + rows?: readonly ActivityRow[]; } -/** Render the full webview HTML document for one job. */ -export function renderJobDetailHtml(job: JobResponse, opts: RenderOptions): string { - const status = job.status ?? 'Unknown'; - const total = job.holesTotal ?? 0; - const closed = job.holesClosed ?? 0; - const failed = job.holesFailed ?? 0; - const pct = total > 0 ? Math.round((closed / total) * 100) : 0; - const obligations = job.obligations ?? []; - const provedTargets = obligations - .filter((obligation) => obligation.status === 'proved') - .map((obligation) => obligation.name); - const jobHasCompleteProofs = - job.status === 'Succeeded' && - job.mode === 'prove' && - typeof job.holesTotal === 'number' && - job.holesTotal > 0 && - typeof job.holesClosed === 'number' && - job.holesClosed === job.holesTotal; - const jobClaimsProof = isProvedSuccess( - job.status, - job.mode, - job.holesTotal, - job.holesClosed, - job.claimClass, - ); - const jobClaimsPartialProof = - job.status === 'PartialSuccess' && - job.mode === 'prove' && - total > 0 && - closed > 0 && - closed < total; - const verifierOutcome = normalizedVerifierOutcome(opts.result); - const hasVerifierVerdict = verifierOutcome !== null; - const fullVerifierAccepted = Boolean( - opts.result && verifierAcceptedFull(opts.result, provedTargets), - ); - const partialVerifierAccepted = Boolean( - opts.result && verifierAcceptedPartial(opts.result, provedTargets), - ); - const resultMatchesJob = Boolean( - opts.result && - opts.result.id === job.id && - opts.result.status === job.status && - opts.result.mode === job.mode && - opts.result.holesTotal === job.holesTotal && - opts.result.holesClosed === job.holesClosed && - opts.result.claimClass === job.claimClass, - ); - const resultAgreesWithProof = Boolean( - opts.result && - resultMatchesJob && - isProvedSuccess( - opts.result.status, - opts.result.mode, - opts.result.holesTotal, - opts.result.holesClosed, - opts.result.claimClass, - ) && - hasVerifierVerdict && - fullVerifierAccepted, - ); - const provedSuccess = jobClaimsProof && resultAgreesWithProof; - - const ribbon = `
    ${phaseRibbon(status, provedSuccess) - .map((chip) => `${escapeHtml(chip.name)}`) - .join('›')}
    `; - - const budget = typeof job.maxWallClockSeconds === 'number' && job.maxWallClockSeconds > 0 - ? job.maxWallClockSeconds - : null; - const created = job.createdAt ? new Date(job.createdAt) : null; - const deadline = budget !== null && created && !Number.isNaN(created.getTime()) - ? new Date(created.getTime() + budget * 1000).toISOString() - : null; - - const errorBanner = opts.error - ? `` - : ''; - - const verdictBlock = - job.errorCode || job.errorReason - ? `` - : ''; - - const compileGoalsNotice = - job.status === 'CompileGoals' - ? '' - : job.mode === 'compile-goals' && job.status !== 'Succeeded' - ? '' - : ''; - - const structuralOnlyNotice = - job.status === 'Succeeded' && job.claimClass === 'StructuralOnly' - ? '' - : ''; - - const succeededTrustNotice = - job.status !== 'Succeeded' - ? '' - : job.mode === 'compile-goals' - ? '' - : job.mode !== 'prove' - ? `` - : !jobHasCompleteProofs - ? '' - : opts.result && !resultMatchesJob - ? `` - : hasVerifierVerdict && !fullVerifierAccepted - ? '' - : job.claimClass === 'StructuralOnly' - ? '' - : job.claimClass !== 'Verified' - ? `` - : !opts.result - ? '' - : !hasVerifierVerdict - ? '' - : ''; - - const partialTrustNotice = - job.status !== 'PartialSuccess' - ? '' - : !jobClaimsPartialProof - ? '' - : opts.result && !resultMatchesJob - ? '' - : job.claimClass !== 'PartialVerified' - ? '' - : !opts.result || !hasVerifierVerdict - ? '' - : partialVerifierAccepted - ? '' - : ''; - - const proofTrustNotice = - structuralOnlyNotice + succeededTrustNotice + partialTrustNotice; - - const obligationsTable = - obligations.length > 0 - ? ` - - ${obligations.map(obligationRow).join('\n')} -
    ObligationKindContentStatusAttemptsDurationLast error
    ` - : '

    No obligations reported yet.

    '; - - const eventLogHtml = - opts.eventLog.length > 0 - ? opts.eventLog - .map((line) => `
    ${escapeHtml(line)}
    `) - .join('') - : '
    No events yet.
    '; - - const verificationSection = opts.result - ? hasVerifierVerdict - ? `

    Independent verifier verdict

    -
    - ${metaRow('Outcome', `${escapeHtml(verifierOutcome!)}`)} - ${metaRow('Result claim class', `${escapeHtml(opts.result.claimClass ?? 'missing')}`)} - ${metaRow('Verified at', fmtTimestamp(opts.result.verifiedAt))} - ${verdictFlag('Compilation passed', opts.result.compileOk, true)} - ${verdictFlag('Assumption policy passed', opts.result.assumptionsClosed, true)} - ${verdictFlag('Verified clean (all holes closed, no admits)', opts.result.verifiedClean, true, partialVerifierAccepted ? 'warn' : 'err')} - ${verdictFlag('Admits detected', opts.result.admitsDetected, false, partialVerifierAccepted ? 'warn' : 'err')} - ${verdictFlag('Statements immutable', opts.result.statementsImmutable, true)} - ${markersFlag(opts.result.markersRemaining)} -
    ` - : '

    Verification

    No independent verifier provenance is available; this is a worker-reported legacy result.

    ' - : ''; - - const resultSection = opts.result - ? `${resultActions(opts.result, isTerminalStatus(status))} - ${verificationSection} - ${hasVerifierVerdict ? assumptionEvidenceHtml(opts.result) : ''} -

    Artifacts

    - ${ - opts.result.artifacts.length > 0 - ? ` - - ${opts.result.artifacts.map(artifactRow).join('\n')} -
    FileKindSize
    ` - : '

    No artifacts stored.

    ' - }` - : ''; - - const cancelButton = opts.canCancel - ? '' - : ''; - +/** The page: regions, the activity section and the script. */ +export function renderShell(opts: ShellOptions): string { + const region = (id: RegionId, fallback = '') => `
    ${opts.regions?.[id] ?? fallback}
    `; + const loading = '
    '; return ` - + + - ${errorBanner} -

    ${escapeHtml(job.filename ?? job.id)} ${escapeHtml(status)}

    - ${ribbon} - -
    - ${metaRow('Job ID', `${escapeHtml(job.id)}`)} - ${opts.source ? metaRow('Source', `${escapeHtml(opts.source)}`) : ''} - ${metaRow('Submitted', fmtTimestamp(job.createdAt))} - ${budget !== null ? metaRow('Time budget', escapeHtml(fmtBudget(budget))) : ''} - ${deadline ? metaRow('Deadline', fmtTimestamp(deadline)) : ''} - ${metaRow('Mode', escapeHtml(job.mode ?? '—'))} - ${metaRow('Outcome', escapeHtml(job.outcome ?? '—'))} - ${metaRow('Claim class', `${escapeHtml(job.claimClass ?? 'missing')}`)} -
    - - ${compileGoalsNotice} - ${proofTrustNotice} - -

    Proof holes: ${closed}/${total} closed${failed > 0 ? `, ${failed} failed` : ''}

    -
    - - ${verdictBlock} - -

    Obligations

    - ${obligationsTable} - - ${resultSection} - -

    Events

    -
    ${eventLogHtml}
    - -
    - - ${cancelButton} - ${escapeHtml(liveNote(opts.live))} - -
    - - +
    + ${region('banner')} + ${region('header', loading)} + ${region('steps')} + ${region('verdict', loading)} + ${region('progress')} + ${region('obligations')} + ${region('evidence')} + ${region('files')} + ${region('tech')} +
    +
    +

    Activity

    +
    +
    + + + +
    + +
    +
    +
    ${renderActivityRows(opts.rows ?? [])}
    +
    +
    +
    + `; } + +export interface RenderOptions extends Omit { + /** CSP nonce for the inline script. */ + nonce: string; + /** `webview.cspSource` of the hosting panel. */ + cspSource: string; +} + +/** One complete document (shell + regions + activity) for a job. */ +export function renderJobDetailHtml(job: JobResponse, opts: RenderOptions): string { + const view = buildJobView({ ...opts, job }); + return renderShell({ + nonce: opts.nonce, + cspSource: opts.cspSource, + regions: renderRegions(view), + rows: opts.run?.rows ?? [], + }); +} diff --git a/editors/vscode/src/prover/jobDetailModel.ts b/editors/vscode/src/prover/jobDetailModel.ts new file mode 100644 index 00000000..7acbf5ba --- /dev/null +++ b/editors/vscode/src/prover/jobDetailModel.ts @@ -0,0 +1,558 @@ +/** + * The job panel's view model: everything the panel shows, worked out from the + * job, its result and its event history. Pure — no `vscode` import, no HTML. + */ + +import { fileStem, type BuildError } from './buildLog'; +import { isCancelableStatus, isStreamTerminalStatus, isTerminalStatus, isTextArtifactKind } from './jobStatus'; +import { jobVerdict, type ResultState, type Tone, type Verdict } from './jobVerdict'; + +/** Shown until a restored panel has fetched its job. */ +const LOADING_JOB: Verdict = { + kind: 'loading', + tone: 'muted', + icon: 'loading', + badge: 'Loading…', + headline: 'Loading this proof job…', + body: 'The job is shown once the proof server has answered.', + caveats: [], + claim: 'none', +}; +import { newRunModel, type RunModel, type RunStep } from './runModel'; +import type { ArtifactInfo, AssumptionReport, JobResponse, JobResultResponse, ObligationDto } from './types'; +import { normalizedAssumptionReports, normalizedVerifierOutcome, verifierAcceptedPartial } from './verifierEvidence'; + +/** Live-update transport the hosting view is in. */ +export type LiveMode = 'sse' | 'poll' | 'terminal'; + +export interface JobViewInput { + job: JobResponse; + result?: JobResultResponse | null; + /** Defaults: `loaded` with a result, `loading` for a finished job without one. */ + resultState?: ResultState; + /** False until the job detail (not just a list row) has been fetched. */ + detailLoaded?: boolean; + /** False for a panel restored after a reload, before its first fetch. */ + statusKnown?: boolean; + run?: RunModel; + buildError?: BuildError | null; + /** The `.inf` the user proved, when this extension compiled the upload. */ + source?: string | null; + /** Fetch-failure text; stale data stays visible below it. */ + error?: string | null; + live: LiveMode; +} + +export interface ActionView { + /** `data-action` the webview posts back. */ + action: string; + label: string; + icon?: 'file' | 'diff' | 'linkExternal' | 'log' | 'goto' | 'rerun' | 'refresh' | 'stop' | 'copy' | 'download'; + /** Accessible name when the label alone is ambiguous. */ + ariaLabel?: string; + /** Extra `data-*` attributes (escaped at render). */ + data?: Record; + style?: 'primary' | 'secondary' | 'danger'; +} + +/** `stopped`: the step a finished run ended in without completing it. */ +export type StepState = 'done' | 'active' | 'todo' | 'unknown' | 'stopped' | 'final'; + +export interface StepView { + key: RunStep | 'result'; + label: string; + state: StepState; + tone?: Tone; + /** When the step started (done/active), for the tooltip. */ + at?: string; +} + +export interface ObligationView { + name: string; + shortName: string; + status: string; + statusLabel: string; + tone: Tone; + kindLabel: string; + contentLabel: string; + by?: 'template' | 'agent'; + attempts?: number; + duration?: string; + goal?: string; + lastError?: string; + specList?: string; + /** + * Where "Go to" leads: the theorem's proof in the returned file once the + * obligation is proved, else its statement in the submitted file. The host + * finds the theorem by name; `line` (the proof hole the server reported) + * is the fallback for the submitted file. + */ + goto: { target: 'proof'; artifact: string } | { target: 'source'; line?: number }; + group: 'active' | 'problem' | 'waiting' | 'done'; +} + +export interface CheckView { + label: string; + state: 'pass' | 'fail' | 'warn' | 'unknown'; + detail?: string; +} + +export interface EvidenceView { + kind: 'verdict' | 'worker-only' | 'not-applicable'; + outcome?: string; + verifiedAt?: string; + checks: CheckView[]; + policyId?: string; + /** Null when the per-theorem evidence is missing or malformed. */ + reports: AssumptionReport[] | null; +} + +export interface FileView { + id: string; + kind: string; + kindLabel: string; + filename: string; + size: string; + text: boolean; +} + +export interface TechRow { + field: string; + label: string; + value: string; + mono?: boolean; +} + +export interface ClockView { + /** Budget start (submission; queue time counts). */ + start?: string; + deadline?: string; + /** When the run ended, for finished jobs whose history says so. */ + end?: string; + budgetSeconds?: number; + running: boolean; +} + +export interface JobView { + jobId: string; + title: string; + /** The uploaded `.v` name, shown under an `.inf` title. */ + subtitle?: string; + verdict: Verdict; + /** The verdict body is compiler output (shown as code). */ + verdictBodyIsCode: boolean; + steps: StepView[]; + progress: { known: boolean; total: number; closed: number; failed: number }; + clock: ClockView; + /** Null while the job detail is loading. */ + obligations: ObligationView[] | null; + actions: ActionView[]; + headerActions: ActionView[]; + /** Null for runs that have not finished (or whose result is loading). */ + evidence: EvidenceView | null; + files: FileView[] | null; + tech: TechRow[]; + banner: { tone: 'err' | 'warn'; text: string } | null; + live: LiveMode; + terminal: boolean; +} + +const KIND_LABELS: Record = { + module: 'structure', + spec: 'behavior', + exists_spec: 'existence', + unique_spec: 'uniqueness', +}; + +const CONTENT_LABELS: Record = { + grounded: 'States a behavioral property of the compiled module', + structural: 'Structural (module typing)', + empty: 'Empty specification', + tautology: 'Tautology — true for any program', + unguarded: 'Not tied to the compiled module', +}; + +const STATUS_LABELS: Record = { + pending: ['Waiting', 'muted'], + running: ['Working', 'active'], + proved: ['Proved', 'ok'], + failed: ['Not closed', 'err'], + skipped: ['Skipped — out of time', 'warn'], + refuted: ['Refuted', 'refuted'], +}; + +const ARTIFACT_LABELS: Record = { + InputV: 'Submitted file', + CompletedV: 'Completed proof', + Report: 'Run report', + Goals: 'Proof goals', + BuildLog: 'Build log', + AgentLog: 'Agent log', + RefutationV: 'Refutation', + RefutationMd: 'Refutation notes', +}; + +export function fmtDuration(ms: number | null | undefined): string | undefined { + if (ms === null || ms === undefined || !Number.isFinite(ms)) { + return undefined; + } + if (ms < 1000) { + return `${ms} ms`; + } + const s = ms / 1000; + return s < 60 ? `${s.toFixed(1)} s` : `${Math.floor(s / 60)}m ${Math.round(s % 60)}s`; +} + +export function fmtBudget(seconds: number): string { + const h = Math.floor(seconds / 3600); + const m = Math.floor((seconds % 3600) / 60); + const s = seconds % 60; + return [h ? `${h}h` : '', m ? `${m}m` : '', s || (!h && !m) ? `${s}s` : ''] + .filter(Boolean) + .join(' '); +} + +export function fmtBytes(bytes: number): string { + if (bytes < 1024) { + return `${bytes} B`; + } + const kib = bytes / 1024; + return kib < 1024 ? `${kib.toFixed(1)} KiB` : `${(kib / 1024).toFixed(2)} MiB`; +} + +function fmtTimestamp(iso: string | null | undefined): string { + if (!iso) { + return '—'; + } + const d = new Date(iso); + return Number.isNaN(d.getTime()) ? iso : d.toLocaleString(); +} + +/** `valid_main__Comm` → `Comm`; names without a `__` part stay whole. */ +export function shortObligationName(name: string): string { + const i = name.lastIndexOf('__'); + return i > 0 && i + 2 < name.length ? name.slice(i + 2) : name; +} + +const GROUP_ORDER: Record = { active: 0, problem: 1, waiting: 2, done: 3 }; + +/** + * An obligation closed by the worker is "Proved" only once the run's verdict + * claims a proof; while running it is "Closed", and in a finished run without + * a claim it is "Closed — not verified". + */ +function obligationView( + o: ObligationDto, + run: RunModel, + finished: boolean, + claimed: boolean, + completedId: string | undefined, +): ObligationView { + const status = o.status ?? 'pending'; + const [statusLabel, tone]: [string, Tone] = + finished && (status === 'pending' || status === 'running') + ? ['Not attempted', 'muted'] + : status === 'proved' && !claimed + ? finished ? ['Closed — not verified', 'warn'] : ['Closed', 'ok'] + : STATUS_LABELS[status] ?? [status, 'muted']; + const group: ObligationView['group'] = + status === 'running' ? 'active' + : status === 'failed' || status === 'refuted' ? 'problem' + : status === 'proved' ? 'done' : 'waiting'; + const view: ObligationView = { + name: o.name, + shortName: shortObligationName(o.name), + status, + statusLabel, + tone, + kindLabel: KIND_LABELS[o.kind] ?? 'other', + contentLabel: CONTENT_LABELS[o.content ?? 'unknown'] ?? 'Not classified', + goto: { target: 'source' }, + group, + }; + const by = status === 'proved' ? run.provedBy[o.name] : undefined; + if (by) view.by = by; + const attempts = o.attempts ?? run.attempts[o.name]; + if (typeof attempts === 'number' && attempts > 0) view.attempts = attempts; + const duration = fmtDuration(o.durationMs); + if (duration) view.duration = duration; + if (o.goal) view.goal = o.goal; + if (o.lastError) view.lastError = o.lastError; + if (o.specList) view.specList = o.specList; + const line = o.sourceLine ?? run.sourceLines[o.name]; + if (status === 'proved' && completedId) { + view.goto = { target: 'proof', artifact: completedId }; + } else if (typeof line === 'number' && line > 0) { + view.goto = { target: 'source', line }; + } + return view; +} + +function steps(job: JobResponse, run: RunModel, verdict: Verdict): StepView[] { + const order: Array<[RunStep, string]> = [ + ['submitted', 'Submitted'], + ['worker', 'Worker'], + ['proving', 'Proving'], + ['verifying', 'Verifying'], + ]; + const activeIndex: Record = { + Accepted: 0, + Queued: 1, + Provisioning: 1, + Booting: 1, + Running: 2, + Verifying: 3, + }; + const at = (key: RunStep) => run.reached[key]; + const live = activeIndex[job.status]; + if (live !== undefined) { + return [ + ...order.map(([key, label], i): StepView => ({ + key, + label, + state: i < live ? 'done' : i === live ? 'active' : 'todo', + ...(at(key) ? { at: at(key) } : {}), + })), + { key: 'result', label: 'Result', state: 'todo' }, + ]; + } + // Finished or canceling: a step counts as done only when the history shows + // it (a run that never got a worker did not "prove"). Submitted always was. + // A run that did not succeed stopped in the last step it reached. + const reached = order.map(([key]) => key === 'submitted' || Boolean(run.reached[key])); + const last = reached.lastIndexOf(true); + const stoppedAt = + verdict.claim === 'none' && last > 0 && !run.finished[order[last][0]] ? last : -1; + return [ + ...order.map(([key, label], i): StepView => ({ + key, + label, + state: i === stoppedAt ? 'stopped' : reached[i] ? 'done' : 'unknown', + ...(i === stoppedAt ? { tone: verdict.tone } : {}), + ...(at(key) ? { at: at(key) } : {}), + })), + { + key: 'result', + label: verdict.badge, + state: job.status === 'Canceling' ? 'active' : 'final', + tone: verdict.tone, + }, + ]; +} + +function evidence(job: JobResponse, result: JobResultResponse): EvidenceView { + const outcome = normalizedVerifierOutcome(result); + if (outcome === null) { + return { + kind: job.mode === 'compile-goals' || job.status === 'CompileGoals' ? 'not-applicable' : 'worker-only', + checks: [], + reports: null, + }; + } + const provedTargets = (job.obligations ?? []).filter((o) => o.status === 'proved').map((o) => o.name); + const partial = job.status === 'PartialSuccess' && verifierAcceptedPartial(result, provedTargets); + const flag = (value: boolean | null | undefined, good: boolean): CheckView['state'] => + value === null || value === undefined ? 'unknown' : value === good ? 'pass' : 'fail'; + const reports = normalizedAssumptionReports(result); + const complete = result.verifiedClean === true && result.admitsDetected === false; + const admitted = Math.max(0, (result.holesTotal ?? 0) - (result.holesClosed ?? 0)); + const checks: CheckView[] = [ + { label: 'The returned file compiles', state: flag(result.compileOk, true) }, + partial + ? { + label: 'Every closed proof is complete', + state: 'warn', + detail: `${admitted} unproved ${admitted === 1 ? 'obligation remains' : 'obligations remain'} admitted, as expected for a partial result.`, + } + : { + label: 'Every proof is complete (no admits)', + state: result.verifiedClean === null || result.verifiedClean === undefined || + result.admitsDetected === null || result.admitsDetected === undefined + ? 'unknown' + : complete ? 'pass' : 'fail', + }, + { label: 'Theorem statements are unchanged', state: flag(result.statementsImmutable, true) }, + { + label: 'No proof markers left', + state: result.markersRemaining === null || result.markersRemaining === undefined + ? 'unknown' + : result.markersRemaining === 0 ? 'pass' : 'fail', + ...(typeof result.markersRemaining === 'number' && result.markersRemaining > 0 + ? { detail: `${result.markersRemaining} left` } + : {}), + }, + { + label: 'Only approved assumptions are used', + state: result.assumptionsClosed !== true + ? flag(result.assumptionsClosed, true) + : reports && reports.every((r) => r.policyPassed) ? 'pass' : 'fail', + }, + ]; + return { + kind: 'verdict', + outcome, + ...(result.verifiedAt ? { verifiedAt: fmtTimestamp(result.verifiedAt) } : {}), + checks, + ...(result.assumptionPolicyId?.trim() ? { policyId: result.assumptionPolicyId } : {}), + reports: result.assumptionPolicyId?.trim() ? reports : null, + }; +} + +function verdictActions(job: JobResponse, result: JobResultResponse | null, verdict: Verdict, buildError: BuildError | null | undefined): ActionView[] { + const actions: ActionView[] = []; + const artifacts = result?.artifacts ?? []; + const find = (kind: string) => artifacts.find((a) => a.kind === kind); + const completed = find('CompletedV'); + if (completed) { + actions.push({ + action: 'openArtifact', label: 'Open proof', icon: 'file', style: 'primary', + ariaLabel: `Open the completed proof ${completed.filename}`, data: { artifact: completed.id }, + }); + if (find('InputV')) { + actions.push({ action: 'compare', label: 'Compare with input', icon: 'diff', ariaLabel: 'Compare the completed proof with the submitted file' }); + } + } + const refutation = find('RefutationV'); + if (refutation) { + actions.push({ + action: 'openArtifact', label: 'Open refutation', icon: 'file', style: completed ? 'secondary' : 'primary', + ariaLabel: `Open the refutation ${refutation.filename}`, data: { artifact: refutation.id }, + }); + } + if (verdict.kind === 'compile-error' || verdict.kind === 'completed-compile-error') { + const input = find(verdict.kind === 'compile-error' ? 'InputV' : 'CompletedV'); + if (buildError?.line !== undefined && input) { + actions.push({ + action: 'gotoLine', label: `Go to line ${buildError.line}`, icon: 'goto', style: 'primary', + ariaLabel: `Go to line ${buildError.line} of ${input.filename}`, + data: { artifact: input.id, line: String(buildError.line) }, + }); + } + const log = find('BuildLog'); + if (log) { + actions.push({ action: 'openArtifact', label: 'Open build log', icon: 'log', ariaLabel: 'Open the build log', data: { artifact: log.id } }); + } + } + if (isTerminalStatus(job.status)) { + const proofLike = job.status === 'Succeeded' || job.status === 'PartialSuccess' || job.status === 'CompileGoals'; + actions.push(proofLike + ? { action: 'openCertificate', label: 'Certificate', icon: 'linkExternal', ariaLabel: 'Open the certificate in the portal' } + : { action: 'openPortal', label: 'Open in portal', icon: 'linkExternal', ariaLabel: 'Open this job in the portal' }); + } + if (['failed', 'timed-out', 'provision-failed', 'lost', 'canceled'].includes(verdict.kind)) { + actions.push({ action: 'resubmit', label: 'Run Again', icon: 'rerun', ariaLabel: 'Run this proof job again' }); + } + return actions; +} + +function techRows(job: JobResponse, clock: ClockView, live: LiveMode): TechRow[] { + const rows: TechRow[] = [ + { field: 'id', label: 'Job ID', value: job.id, mono: true }, + { field: 'submitted', label: 'Submitted', value: fmtTimestamp(job.createdAt) }, + ]; + if (clock.budgetSeconds) rows.push({ field: 'budget', label: 'Time budget', value: fmtBudget(clock.budgetSeconds) }); + if (clock.deadline) rows.push({ field: 'deadline', label: 'Deadline', value: fmtTimestamp(clock.deadline) }); + rows.push({ field: 'status', label: 'Status', value: job.status, mono: true }); + rows.push({ field: 'mode', label: 'Mode', value: job.mode ?? '—', mono: true }); + if (job.outcome) rows.push({ field: 'outcome', label: 'Outcome', value: job.outcome, mono: true }); + rows.push({ field: 'claimClass', label: 'Claim class', value: job.claimClass ?? 'missing', mono: true }); + if (job.errorCode) rows.push({ field: 'errorCode', label: 'Error code', value: job.errorCode, mono: true }); + if (job.errorReason) rows.push({ field: 'errorReason', label: 'Error detail', value: job.errorReason }); + rows.push({ + field: 'updates', + label: 'Updates', + value: live === 'sse' ? 'Live — streaming events' : live === 'poll' ? 'Polling every 5 s (live stream unavailable)' : 'Finished — auto-refresh stopped', + }); + return rows; +} + +export function buildJobView(input: JobViewInput): JobView { + const { job } = input; + const run = input.run ?? newRunModel(); + const result = input.result ?? null; + const terminal = isTerminalStatus(job.status); + const resultState: ResultState = + input.resultState ?? (result ? 'loaded' : isStreamTerminalStatus(job.status) ? 'loading' : 'n/a'); + const detailLoaded = input.detailLoaded ?? true; + const fileStems = [fileStem(input.source), fileStem(job.filename)].filter((s): s is string => Boolean(s)); + const statusKnown = input.statusKnown ?? true; + const verdict = statusKnown + ? jobVerdict({ job, result, resultState, buildError: input.buildError, fileStems }) + : LOADING_JOB; + + const budget = typeof job.maxWallClockSeconds === 'number' && job.maxWallClockSeconds > 0 + ? job.maxWallClockSeconds + : undefined; + const created = job.createdAt ? Date.parse(job.createdAt) : NaN; + const deadline = job.deadlineUtc ?? run.deadlineUtc ?? + (budget !== undefined && !Number.isNaN(created) ? new Date(created + budget * 1000).toISOString() : undefined); + const clock: ClockView = { + ...(job.createdAt ? { start: job.createdAt } : {}), + ...(deadline ? { deadline } : {}), + ...(terminal && run.endedAt ? { end: run.endedAt } : {}), + ...(budget !== undefined ? { budgetSeconds: budget } : {}), + running: !terminal, + }; + + const completedId = result?.artifacts.find((a) => a.kind === 'CompletedV')?.id; + const obligations = detailLoaded && statusKnown + ? (job.obligations ?? []) + .map((o) => obligationView(o, run, terminal, verdict.claim !== 'none', completedId)) + .map((view, index) => ({ view, index })) + .sort((a, b) => GROUP_ORDER[a.view.group] - GROUP_ORDER[b.view.group] || a.index - b.index) + .map(({ view }) => view) + : null; + + const headerActions: ActionView[] = [ + { action: 'refresh', label: 'Refresh', icon: 'refresh', style: 'secondary', ariaLabel: 'Refresh this job' }, + ]; + if (statusKnown && isCancelableStatus(job.status)) { + headerActions.push({ action: 'cancel', label: 'Cancel Job', icon: 'stop', style: 'danger' }); + } + + const title = input.source ?? job.filename ?? job.id; + const banner = input.error + ? { tone: 'err' as const, text: input.error } + : run.integrityWarnings.length > 0 + ? { tone: 'warn' as const, text: `Integrity warning: ${run.integrityWarnings[run.integrityWarnings.length - 1]} This run needs review.` } + : null; + + return { + jobId: job.id, + title, + ...(input.source && job.filename && job.filename !== input.source ? { subtitle: job.filename } : {}), + verdict, + verdictBodyIsCode: Boolean(input.buildError) && + (verdict.kind === 'compile-error' || verdict.kind === 'completed-compile-error'), + steps: statusKnown + ? steps(job, run, verdict) + : steps({ ...job, status: 'Accepted' }, run, verdict).map((s) => ({ ...s, state: 'todo' as const })), + progress: { + known: detailLoaded && typeof job.holesTotal === 'number', + total: job.holesTotal ?? 0, + closed: job.holesClosed ?? 0, + failed: job.holesFailed ?? 0, + }, + clock, + obligations, + actions: statusKnown ? verdictActions(job, result, verdict, input.buildError) : [], + headerActions, + evidence: result && ['Succeeded', 'PartialSuccess', 'CompileGoals'].includes(job.status) + ? evidence(job, result) + : null, + files: result + ? result.artifacts.map((a: ArtifactInfo) => ({ + id: a.id, + kind: a.kind, + kindLabel: ARTIFACT_LABELS[a.kind] ?? a.kind, + filename: a.filename, + size: fmtBytes(a.sizeBytes), + text: isTextArtifactKind(a.kind), + })) + : null, + tech: techRows(job, clock, input.live), + banner, + live: input.live, + terminal, + }; +} diff --git a/editors/vscode/src/prover/jobDetailScript.ts b/editors/vscode/src/prover/jobDetailScript.ts new file mode 100644 index 00000000..319a174d --- /dev/null +++ b/editors/vscode/src/prover/jobDetailScript.ts @@ -0,0 +1,312 @@ +/** + * The job panel's in-webview script (one nonce'd inline script). + * + * The host sets the page once; afterwards it sends messages and this script + * patches the page in place, so focus, open sections, the activity filter and + * scroll positions survive every update: + * + * - `snapshot` {regions, rows, clock, jobId}: full state (after `ready`). + * - `regions` {regions}: changed regions only, as HTML the host escaped. + * - `activity` {rows, reset?}: activity rows, built here with textContent. + * - `clock` {clock}: budget start/deadline/end for the live timer. + * - `checked` {at}: a refresh found nothing new. + * + * Posts `ready` once, and `{command: , ...}` for every action. + */ + +export function jobDetailScript(rowCap: number): string { + return ` +(function () { + 'use strict'; + const vscode = acquireVsCodeApi(); + const CAP = ${Math.max(1, Math.floor(rowCap))}; + const saved = vscode.getState() || {}; + let filter = ['steps', 'agent', 'all'].indexOf(saved.filter) >= 0 ? saved.filter : 'steps'; + let query = typeof saved.query === 'string' ? saved.query : ''; + const openKeys = new Set(Array.isArray(saved.open) ? saved.open : []); + const closedKeys = new Set(Array.isArray(saved.closed) ? saved.closed : []); + let jobId = typeof saved.jobId === 'string' ? saved.jobId : null; + let clock = null; + const log = document.getElementById('log'); + const search = document.getElementById('activity-search'); + let lastGroup = null; + + function save() { + vscode.setState({ + jobId: jobId, filter: filter, query: query, + open: Array.from(openKeys).slice(-200), closed: Array.from(closedKeys).slice(-200), + }); + } + + // ── Details open/closed memory ────────────────────────────────────── + document.addEventListener('toggle', function (e) { + const d = e.target; + if (!d || !d.dataset || !d.dataset.key) return; + if (d.open) { openKeys.add(d.dataset.key); closedKeys.delete(d.dataset.key); } + else { closedKeys.add(d.dataset.key); openKeys.delete(d.dataset.key); } + save(); + }, true); + + function restoreDetails(root) { + root.querySelectorAll('details[data-key]').forEach(function (d) { + if (openKeys.has(d.dataset.key)) d.open = true; + else if (closedKeys.has(d.dataset.key)) d.open = false; + }); + } + + // ── Region patches ────────────────────────────────────────────────── + function patch(regions) { + const active = document.activeElement; + const focusKey = active && active.getAttribute ? active.getAttribute('data-focus-key') : null; + const scrollY = window.scrollY; + Object.keys(regions || {}).forEach(function (id) { + const el = document.getElementById('region-' + id); + if (el && typeof regions[id] === 'string') { + el.innerHTML = regions[id]; + restoreDetails(el); + } + }); + if (focusKey && (!document.activeElement || document.activeElement === document.body)) { + const target = document.querySelector('[data-focus-key="' + CSS.escape(focusKey) + '"]'); + if (target) target.focus({ preventScroll: true }); + } + window.scrollTo(0, scrollY); + tick(); + } + + // ── Activity ──────────────────────────────────────────────────────── + function clockText(iso) { + const d = new Date(iso); + if (isNaN(d.getTime())) return ''; + const p = function (n) { return String(n).padStart(2, '0'); }; + return p(d.getHours()) + ':' + p(d.getMinutes()) + ':' + p(d.getSeconds()); + } + function shortName(name) { + const i = name.lastIndexOf('__'); + return i > 0 && i + 2 < name.length ? name.slice(i + 2) : name; + } + function catVisible(cat) { + if (filter === 'steps') return cat !== 'agent' && cat !== 'detail'; + if (filter === 'agent') return cat === 'agent' || cat === 'warn' || cat === 'error'; + return true; + } + function matches(row) { + if (!query) return true; + const q = query.toLowerCase(); + return row.textContent.toLowerCase().indexOf(q) >= 0 || + (row.dataset.obligation || '').toLowerCase().indexOf(q) >= 0; + } + function updateGroups() { + let header = null; + let any = false; + Array.prototype.forEach.call(log.children, function (el) { + if (el.classList.contains('grp')) { + if (header) header.hidden = !any; + header = el; + any = false; + } else if (el.classList.contains('row') && !el.hidden && catVisible(el.dataset.cat)) { + any = true; + } + }); + if (header) header.hidden = !any; + const empty = log.querySelector('.empty'); + const visible = Array.prototype.some.call(log.querySelectorAll('.row'), function (r) { + return !r.hidden && catVisible(r.dataset.cat); + }); + if (!visible && !empty) { + const p = document.createElement('div'); + p.className = 'empty'; + p.textContent = log.querySelector('.row') ? 'No matching activity.' : 'No activity yet.'; + log.appendChild(p); + } else if (visible && empty) { + empty.remove(); + } else if (empty) { + empty.textContent = log.querySelector('.row') ? 'No matching activity.' : 'No activity yet.'; + } + } + function rowElement(r) { + const div = document.createElement('div'); + div.className = 'row'; + div.dataset.cat = r.cat; + div.dataset.seq = String(r.seq); + if (r.obligation) div.dataset.obligation = r.obligation; + const t = document.createElement('time'); + t.dateTime = r.ts; + t.textContent = clockText(r.ts); + const s = document.createElement('span'); + s.className = 'text'; + if (r.attempt) { + const a = document.createElement('span'); + a.className = 'att'; + a.textContent = '#' + r.attempt; + s.appendChild(a); + } + s.appendChild(document.createTextNode(r.text)); + div.appendChild(t); + div.appendChild(s); + div.hidden = !matches(div); + return div; + } + function groupElement(name) { + const g = document.createElement('div'); + g.className = 'grp'; + g.textContent = name ? shortName(name) : 'Run'; + if (name) g.title = name; + return g; + } + function appendRows(rows, reset) { + if (reset) { + log.textContent = ''; + lastGroup = null; + } + const stick = reset || log.scrollTop + log.clientHeight >= log.scrollHeight - 8; + const frag = document.createDocumentFragment(); + (rows || []).forEach(function (r) { + const key = r.obligation || ''; + if (key !== lastGroup && (key || lastGroup)) { + frag.appendChild(groupElement(key)); + } + lastGroup = key; + frag.appendChild(rowElement(r)); + }); + log.appendChild(frag); + let count = log.querySelectorAll('.row').length; + while (count > CAP && log.firstElementChild) { + if (log.firstElementChild.classList.contains('row')) count--; + log.removeChild(log.firstElementChild); + } + updateGroups(); + if (stick) log.scrollTop = log.scrollHeight; + } + function applyFilter() { + log.dataset.filter = filter; + document.querySelectorAll('[data-action="filter"]').forEach(function (b) { + const on = b.dataset.value === filter; + b.setAttribute('aria-checked', on ? 'true' : 'false'); + b.tabIndex = on ? 0 : -1; + }); + log.querySelectorAll('.row').forEach(function (r) { r.hidden = !matches(r); }); + updateGroups(); + } + + // ── Timer ─────────────────────────────────────────────────────────── + function fmt(sec) { + sec = Math.max(0, Math.round(sec)); + const h = Math.floor(sec / 3600), m = Math.floor((sec % 3600) / 60), s = sec % 60; + return h ? h + 'h ' + m + 'm' : m ? m + 'm ' + s + 's' : s + 's'; + } + function fmtBudget(sec) { + const h = Math.floor(sec / 3600), m = Math.floor((sec % 3600) / 60); + return h ? h + 'h' + (m ? ' ' + m + 'm' : '') : m ? m + 'm' : sec + 's'; + } + function tick() { + const el = document.querySelector('[data-clock]'); + if (!el || !clock || !clock.start) return; + const start = Date.parse(clock.start); + if (isNaN(start)) return; + const now = Date.now(); + let text = ''; + if (clock.running) { + text = fmt((now - start) / 1000) + ' elapsed'; + const deadline = clock.deadline ? Date.parse(clock.deadline) : NaN; + if (!isNaN(deadline)) { + text += deadline > now ? ' · ' + fmt((deadline - now) / 1000) + ' left' : ' · time budget used'; + } + } else if (clock.end && !isNaN(Date.parse(clock.end))) { + text = 'Took ' + fmt((Date.parse(clock.end) - start) / 1000) + + (clock.budgetSeconds ? ' of ' + fmtBudget(clock.budgetSeconds) : ''); + } else if (clock.budgetSeconds) { + text = 'Time budget ' + fmtBudget(clock.budgetSeconds); + } + el.textContent = text; + } + setInterval(function () { if (clock && clock.running) tick(); }, 1000); + + // ── Actions ───────────────────────────────────────────────────────── + document.addEventListener('click', function (e) { + const el = e.target && e.target.closest ? e.target.closest('[data-action]') : null; + if (!el) return; + const action = el.dataset.action; + if (action === 'filter') { + filter = el.dataset.value; + applyFilter(); + save(); + return; + } + if (action === 'show-activity') { + query = el.dataset.obligation || ''; + search.value = query; + filter = 'all'; + applyFilter(); + save(); + document.getElementById('activity').scrollIntoView({ block: 'start' }); + return; + } + const message = { command: action }; + if (el.dataset.artifact) message.artifactId = el.dataset.artifact; + if (el.dataset.line) message.line = Number(el.dataset.line); + if (el.dataset.obligation) message.obligation = el.dataset.obligation; + vscode.postMessage(message); + }); + document.addEventListener('keydown', function (e) { + const el = e.target; + if (!el || !el.dataset || el.dataset.action !== 'filter') return; + if (e.key !== 'ArrowRight' && e.key !== 'ArrowLeft' && e.key !== 'ArrowDown' && e.key !== 'ArrowUp') return; + const radios = Array.prototype.slice.call(document.querySelectorAll('[data-action="filter"]')); + const i = radios.indexOf(el); + const next = radios[(i + (e.key === 'ArrowRight' || e.key === 'ArrowDown' ? 1 : radios.length - 1)) % radios.length]; + filter = next.dataset.value; + applyFilter(); + save(); + next.focus(); + e.preventDefault(); + }); + search.addEventListener('input', function () { + query = search.value.trim(); + applyFilter(); + save(); + }); + + // ── Host messages ─────────────────────────────────────────────────── + window.addEventListener('message', function (event) { + const m = event.data; + if (!m || typeof m.command !== 'string') return; + switch (m.command) { + case 'snapshot': + if (typeof m.jobId === 'string') jobId = m.jobId; + clock = m.clock || null; + patch(m.regions); + appendRows(m.rows, true); + document.getElementById('checked').textContent = ''; + save(); + break; + case 'regions': + patch(m.regions); + break; + case 'activity': + appendRows(m.rows, Boolean(m.reset)); + break; + case 'clock': + clock = m.clock || null; + tick(); + break; + case 'checked': + document.getElementById('checked').textContent = + 'Checked at ' + m.at + ' — no changes.'; + break; + } + }); + + // Initial page state: restore the saved filter and sections, then ask + // the host for the current data. + search.value = query; + restoreDetails(document); + lastGroup = (function () { + const rows = log.querySelectorAll('.row'); + return rows.length ? rows[rows.length - 1].dataset.obligation || '' : null; + })(); + applyFilter(); + vscode.postMessage({ command: 'ready' }); +})(); +`; +} diff --git a/editors/vscode/src/prover/jobDetailStyles.ts b/editors/vscode/src/prover/jobDetailStyles.ts new file mode 100644 index 00000000..d0359a86 --- /dev/null +++ b/editors/vscode/src/prover/jobDetailStyles.ts @@ -0,0 +1,289 @@ +/** + * Job panel stylesheet. Every colour comes from the VS Code theme + * (`--vscode-*`), so the panel follows light, dark and high-contrast themes; + * tone colours are never the only signal (each has a label or icon shape). + */ +export const JOB_DETAIL_STYLES = ` +:root { + --ok: var(--vscode-testing-iconPassed, #73c991); + --err: var(--vscode-testing-iconFailed, var(--vscode-errorForeground, #f14c4c)); + --warn: var(--vscode-editorWarning-foreground, #cca700); + --refuted: var(--vscode-charts-purple, #b180d7); + --active: var(--vscode-progressBar-background, #0e70c0); + --muted: var(--vscode-descriptionForeground, #8b8b8b); + --border: var(--vscode-widget-border, var(--vscode-panel-border, rgba(128, 128, 128, 0.35))); + --code-bg: var(--vscode-textCodeBlock-background, rgba(128, 128, 128, 0.12)); + --focus: var(--vscode-focusBorder, #007fd4); + --tone: var(--muted); +} +.tone-ok { --tone: var(--ok); } +.tone-err { --tone: var(--err); } +.tone-warn { --tone: var(--warn); } +.tone-refuted { --tone: var(--refuted); } +.tone-active { --tone: var(--active); } +.tone-muted { --tone: var(--muted); } + +body { + font-family: var(--vscode-font-family); + font-size: var(--vscode-font-size, 13px); + color: var(--vscode-foreground); + line-height: 1.5; + margin: 0; + padding: 16px 24px 40px; +} +main { max-width: 980px; } +code, pre { font-family: var(--vscode-editor-font-family); font-size: 0.95em; } +h1, h2, h3 { font-weight: 600; margin: 0; } +h1 { font-size: 1.4em; line-height: 1.3; overflow-wrap: anywhere; } +h2 { font-size: 1.05em; } +h3 { font-size: 1em; margin: 14px 0 6px; } +p { margin: 0; } +.muted { color: var(--muted); } +.sr-only { + position: absolute; width: 1px; height: 1px; overflow: hidden; + clip: rect(0 0 0 0); clip-path: inset(50%); white-space: nowrap; +} +.icon { width: 16px; height: 16px; flex: none; vertical-align: -3px; } +.spin { animation: spin 1.2s linear infinite; transform-origin: 50% 50%; } +@keyframes spin { to { transform: rotate(360deg); } } +@media (prefers-reduced-motion: reduce) { .spin { animation: none; } } +:focus-visible { outline: 1px solid var(--focus); outline-offset: 2px; } + +/* Buttons follow VS Code's button tokens. */ +button { + font: inherit; line-height: 18px; + display: inline-flex; align-items: center; gap: 6px; + padding: 4px 12px; border-radius: 2px; cursor: pointer; + border: 1px solid var(--vscode-button-border, transparent); + background: var(--vscode-button-background); + color: var(--vscode-button-foreground); +} +button:hover { background: var(--vscode-button-hoverBackground); } +button .icon { width: 14px; height: 14px; vertical-align: 0; } +button.secondary { + background: var(--vscode-button-secondaryBackground, transparent); + color: var(--vscode-button-secondaryForeground, var(--vscode-foreground)); +} +button.secondary:hover { background: var(--vscode-button-secondaryHoverBackground, var(--vscode-toolbar-hoverBackground)); } +button.danger { + background: transparent; color: var(--vscode-foreground); + border-color: color-mix(in srgb, var(--err) 65%, transparent); +} +button.danger .icon { color: var(--err); } +button.danger:hover { background: color-mix(in srgb, var(--err) 14%, transparent); } +button.link { + background: none; border-color: transparent; padding: 2px 4px; + color: var(--vscode-textLink-foreground); +} +button.link:hover { background: none; color: var(--vscode-textLink-activeForeground); text-decoration: underline; } +.actions { display: flex; flex-wrap: wrap; gap: 8px; margin-top: 12px; } +.actions.small { gap: 4px 12px; margin-top: 8px; } + +.banner { + display: flex; gap: 8px; align-items: flex-start; + padding: 8px 12px; margin: 0 0 14px; border-radius: 4px; + border: 1px solid var(--tone); + background: color-mix(in srgb, var(--tone) 10%, transparent); +} +.banner .icon { color: var(--tone); margin-top: 2px; } + +.header { + display: flex; justify-content: space-between; align-items: flex-start; + flex-wrap: wrap; gap: 8px 16px; +} +.title { display: flex; align-items: center; gap: 8px; flex-wrap: wrap; min-width: 0; } +.title > .icon { width: 20px; height: 20px; color: var(--tone); } +.subtitle { color: var(--muted); margin: 2px 0 0 28px; } +.header-actions { display: flex; align-items: center; gap: 8px; flex-wrap: wrap; } +.badge { + display: inline-flex; align-items: center; white-space: nowrap; + padding: 0 8px; border-radius: 10px; font-size: 0.85em; font-weight: 600; line-height: 20px; + color: var(--vscode-foreground); + background: color-mix(in srgb, var(--tone) 16%, transparent); + border: 1px solid color-mix(in srgb, var(--tone) 60%, transparent); +} +.live { display: inline-flex; align-items: center; gap: 2px; color: var(--muted); font-size: 0.9em; } +.live .icon { color: var(--active); } + +.steps { + list-style: none; padding: 0; margin: 14px 0 16px; + display: flex; flex-wrap: wrap; align-items: center; gap: 4px 0; +} +.step { display: inline-flex; align-items: center; gap: 6px; color: var(--muted); } +.step .sep { display: inline-flex; margin: 0 6px; opacity: 0.6; } +.step .sep .icon { width: 12px; height: 12px; } +.step.done { color: var(--vscode-foreground); } +.step.done > .icon { color: var(--ok); } +.step.active { color: var(--vscode-foreground); font-weight: 600; } +.step.active > .icon { color: var(--active); } +.step.unknown > .icon { opacity: 0.7; } +.step.stopped { color: var(--vscode-foreground); } +.step.stopped > .icon { color: var(--tone); } +.step.final { color: var(--vscode-foreground); font-weight: 600; } +.step.final > .icon { color: var(--tone); } + +.verdict { + margin: 0 0 20px; padding: 12px 16px; border-radius: 4px; + border: 1px solid var(--border); border-left: 3px solid var(--tone); + background: color-mix(in srgb, var(--tone) 7%, transparent); +} +.verdict h2 { display: flex; align-items: center; gap: 8px; font-size: 1.1em; margin-bottom: 4px; } +.verdict h2 .icon { color: var(--tone); } +.verdict .caveats { margin: 8px 0 0; padding-left: 20px; } +.verdict .caveats li + li { margin-top: 2px; } +pre.excerpt { + margin: 6px 0 0; padding: 8px 12px; border-radius: 3px; + background: var(--code-bg); white-space: pre-wrap; overflow-wrap: anywhere; +} + +.progress { margin-bottom: 10px; } +.progress-head { display: flex; align-items: baseline; gap: 6px 14px; flex-wrap: wrap; } +.progress-head .count { font-variant-numeric: tabular-nums; } +.progress-head .failed-note { color: var(--err); } +.clock { margin-left: auto; color: var(--muted); font-variant-numeric: tabular-nums; } +.bar { + display: flex; height: 6px; margin: 8px 0 14px; border-radius: 3px; overflow: hidden; + background: color-mix(in srgb, var(--muted) 22%, transparent); +} +.bar .closed { background: var(--ok); } +.bar .failed { background: var(--err); } +.bar.loading { opacity: 0.6; } + +.obligations { border: 1px solid var(--border); border-radius: 4px; overflow: hidden; } +.empty { color: var(--muted); padding: 8px 0; } +details > summary { list-style: none; cursor: pointer; } +details > summary::-webkit-details-marker { display: none; } +.chev { display: inline-flex; transition: transform 0.1s; color: var(--muted); } +details[open] > summary .chev { transform: rotate(90deg); } +@media (prefers-reduced-motion: reduce) { .chev { transition: none; } } +details.group > summary { + display: flex; align-items: center; gap: 6px; padding: 6px 10px; + font-weight: 600; background: color-mix(in srgb, var(--muted) 8%, transparent); + border-top: 1px solid var(--border); +} +details.group:first-child > summary { border-top: none; } +details.obl { border-top: 1px solid var(--border); } +.obligations > details.obl:first-child { border-top: none; } +details.obl > summary { + display: grid; grid-template-columns: 16px minmax(0, 1fr) auto 12px; + align-items: center; gap: 10px; padding: 6px 10px; +} +details.obl > summary:hover { background: var(--vscode-list-hoverBackground); } +.obl-icon { display: inline-flex; color: var(--tone); } +.obl-main { display: flex; align-items: center; gap: 8px; min-width: 0; } +.obl-name { font-family: var(--vscode-editor-font-family); overflow: hidden; text-overflow: ellipsis; white-space: nowrap; } +.chip { + flex: none; font-size: 0.85em; color: var(--muted); padding: 0 6px; border-radius: 8px; + border: 1px solid var(--border); +} +.obl-meta { display: flex; gap: 12px; color: var(--muted); white-space: nowrap; font-variant-numeric: tabular-nums; } +.obl-status { color: var(--vscode-foreground); } +.obl-body { padding: 4px 14px 12px 36px; } +.facts { display: grid; grid-template-columns: max-content minmax(0, 1fr); gap: 2px 14px; margin: 4px 0 0; } +.facts dt { color: var(--muted); } +.facts dd { margin: 0; overflow-wrap: anywhere; } +.obl-error { display: flex; gap: 6px; margin-top: 8px; color: var(--vscode-foreground); } +.obl-error .icon { color: var(--err); margin-top: 2px; } +.goal-label { margin-top: 10px; color: var(--muted); font-size: 0.85em; } +pre.goal { + margin: 2px 0 0; padding: 8px 12px; border-radius: 3px; background: var(--code-bg); + white-space: pre-wrap; overflow-wrap: anywhere; line-height: 1.45; +} +@media (max-width: 560px) { + details.obl > summary { grid-template-columns: 16px minmax(0, 1fr) 12px; } + .obl-meta { grid-column: 2 / 3; } + .obl-body { padding-left: 14px; } +} + +details.section { margin-top: 16px; border-top: 1px solid var(--border); padding-top: 10px; } +details.section > summary { display: flex; align-items: center; gap: 6px; } +details.section > summary h2 { display: inline; } +.section-body { padding: 8px 0 0 20px; } +.checks { list-style: none; padding: 0; margin: 8px 0 0; } +.checks li { display: flex; gap: 8px; align-items: flex-start; padding: 2px 0; } +.checks li .icon { margin-top: 2px; } +.checks .pass .icon { color: var(--ok); } +.checks .fail .icon { color: var(--err); } +.checks .warn .icon { color: var(--warn); } +.checks .unknown .icon { color: var(--muted); } +details.assume { margin-top: 6px; } +details.assume > summary { display: flex; align-items: center; gap: 6px; } +table { border-collapse: collapse; width: 100%; margin: 6px 0; } +th, td { text-align: left; padding: 4px 12px 4px 0; vertical-align: top; } +th { color: var(--muted); font-weight: 600; border-bottom: 1px solid var(--border); } +.files { list-style: none; padding: 0; margin: 4px 0 0; } +.files li { + display: grid; grid-template-columns: 16px minmax(0, 1fr) auto; gap: 10px; align-items: center; + padding: 4px 0; border-bottom: 1px solid var(--border); +} +.files li:last-child { border-bottom: none; } +.file-name { display: flex; flex-wrap: wrap; gap: 0 10px; min-width: 0; } +.file-actions { display: flex; gap: 4px; } +dl.tech { display: grid; grid-template-columns: max-content minmax(0, 1fr); gap: 4px 16px; margin: 4px 0 0; } +dl.tech dt { color: var(--muted); } +dl.tech dd { margin: 0; overflow-wrap: anywhere; } + +.activity { margin-top: 24px; } +.activity-head { display: flex; justify-content: space-between; align-items: center; flex-wrap: wrap; gap: 8px; } +.activity-tools { display: flex; align-items: center; gap: 8px; flex-wrap: wrap; } +.segmented { display: inline-flex; border: 1px solid var(--border); border-radius: 3px; overflow: hidden; } +.segmented button { + background: transparent; color: var(--vscode-foreground); border: none; border-radius: 0; padding: 2px 10px; +} +.segmented button + button { border-left: 1px solid var(--border); } +.segmented button[aria-checked="true"] { + background: var(--vscode-button-secondaryBackground, color-mix(in srgb, var(--muted) 25%, transparent)); + color: var(--vscode-button-secondaryForeground, var(--vscode-foreground)); +} +.search { + display: inline-flex; align-items: center; gap: 6px; padding: 2px 6px; border-radius: 2px; + border: 1px solid var(--vscode-input-border, var(--border)); + background: var(--vscode-input-background); color: var(--vscode-input-foreground); +} +.search:focus-within { outline: 1px solid var(--focus); outline-offset: -1px; } +.search .icon { color: var(--muted); width: 14px; height: 14px; } +.search input { border: none; outline: none; background: transparent; color: inherit; font: inherit; width: 14em; } +.log { + margin-top: 8px; padding: 6px 0; border-radius: 4px; max-height: 28em; overflow: auto; + font-family: var(--vscode-editor-font-family); font-size: var(--vscode-editor-font-size, 12px); line-height: 1.6; + background: var(--code-bg); +} +.log .row { display: grid; grid-template-columns: 5.6em minmax(0, 1fr); gap: 10px; padding: 0 12px; } +.log .row time { color: var(--muted); font-variant-numeric: tabular-nums; } +.log .row .text { white-space: pre-wrap; overflow-wrap: anywhere; } +.log .row .att { color: var(--muted); margin-right: 6px; } +.log .row[data-cat="agent"] .text { color: color-mix(in srgb, var(--vscode-foreground) 82%, transparent); } +.log .row[data-cat="warn"] .text { color: var(--warn); } +.log .row[data-cat="error"] .text { color: var(--err); } +.log .grp { + padding: 8px 12px 2px; font-family: var(--vscode-font-family); font-size: 0.92em; + font-weight: 600; color: var(--muted); +} +.log .empty { padding: 0 12px; } +.log[data-filter="steps"] .row[data-cat="agent"], +.log[data-filter="steps"] .row[data-cat="detail"], +.log[data-filter="agent"] .row[data-cat="step"], +.log[data-filter="agent"] .row[data-cat="detail"], +.log [hidden] { display: none; } +.footer { margin-top: 16px; min-height: 1.5em; color: var(--muted); } +.skeleton { + height: 12px; margin: 10px; border-radius: 3px; + background: color-mix(in srgb, var(--muted) 18%, transparent); +} + +body.vscode-high-contrast, body.vscode-high-contrast-light { + --border: var(--vscode-contrastBorder, currentColor); +} +body.vscode-high-contrast .log, body.vscode-high-contrast-light .log { border: 1px solid var(--border); } +body.vscode-high-contrast .badge, body.vscode-high-contrast-light .badge, +body.vscode-high-contrast .verdict, body.vscode-high-contrast-light .verdict, +body.vscode-high-contrast .banner, body.vscode-high-contrast-light .banner { + background: transparent; + border-color: var(--vscode-contrastBorder, currentColor); +} +body.vscode-high-contrast .verdict, body.vscode-high-contrast-light .verdict { border-left: 3px solid var(--tone); } +body.vscode-high-contrast .bar, body.vscode-high-contrast-light .bar { outline: 1px solid var(--vscode-contrastBorder, currentColor); } +body.vscode-high-contrast :focus-visible, body.vscode-high-contrast-light :focus-visible { + outline: 1px solid var(--vscode-contrastActiveBorder, var(--focus)); +} +`; diff --git a/editors/vscode/src/prover/jobDetailView.ts b/editors/vscode/src/prover/jobDetailView.ts index 6fae4850..81b9dbcf 100644 --- a/editors/vscode/src/prover/jobDetailView.ts +++ b/editors/vscode/src/prover/jobDetailView.ts @@ -1,26 +1,25 @@ import * as crypto from 'crypto'; import * as os from 'os'; +import * as path from 'path'; import * as vscode from 'vscode'; import { ApiError, ProverApi, buildUrl } from './api'; +import { firstBuildError, type BuildError } from './buildLog'; import { describeError, resolveConfig, type ProverConfig } from './config'; -import { formatEventLine } from './eventFormat'; import { cancelJobInteractive, compareProof, openInPortal } from './jobActions'; -import { - EVENT_LOG_CAP, - isCancelableStatus, - isStreamTerminalStatus, - isTextArtifactKind, - renderJobDetailHtml, - type LiveMode, -} from './jobDetailHtml'; -import { fetchVerified, safeArtifactName, type ProofDocuments } from './proofDocuments'; +import { buildJobView, type LiveMode } from './jobDetailModel'; +import { REGION_IDS, renderRegions, renderShell, type Regions } from './jobDetailHtml'; +import { JobOrigins, type JobOrigin } from './jobOrigins'; +import { isStreamTerminalStatus, isTextArtifactKind } from './jobStatus'; +import type { ResultState } from './jobVerdict'; +import { fetchVerified, safeArtifactName, showAtLine, type ProofDocuments } from './proofDocuments'; +import { declarationLine } from './rocqSource'; +import { applyEvent, changesSummary, EVENT_LOG_CAP, newRunModel, type ActivityRow, type RunModel } from './runModel'; import { openEventStream, type SseMessage } from './sse'; -import type { - EventEnvelope, - JobResponse, - JobResultResponse, -} from './types'; +import type { ArtifactInfo, EventEnvelope, JobResponse, JobResultResponse } from './types'; + +/** The panel's webview type, also used to restore panels after a reload. */ +export const JOB_PANEL_VIEW_TYPE = 'inference.proofJob'; /** Poll cadence when the SSE stream is unavailable. */ const POLL_MS = 5_000; @@ -29,7 +28,7 @@ const POLL_MS = 5_000; const SLOW_POLL_MS = 30_000; /** Debounce for event-driven detail re-fetches. */ const REFRESH_DEBOUNCE_MS = 1_200; -/** Event types that never change the rendered job detail. Agent activity is +/** Event types that never change the job detail. Agent activity is * high-volume transcript; re-fetching the job per line would flood the server. */ const DETAIL_NEUTRAL_TYPES: ReadonlySet = new Set([ 'heartbeat', @@ -42,17 +41,18 @@ const EVENTS_PAGE = 500; /** Bound on history pages fetched for a finished job. */ const MAX_HISTORY_PAGES = 40; +/** What the webview saves (`vscode.setState`) and a restored panel gets back. */ +interface SavedPanelState { + jobId?: unknown; +} + interface PanelState { panel: vscode.WebviewPanel; job: JobResponse; - /** Source `.inf` name when this extension compiled the upload. */ - source: string | null; - /** Last rendered error banner (null = clean render). */ + origin?: JobOrigin; + /** Fetch-error banner (null = clean). */ error: string | null; - /** Formatted event-log lines, oldest first, capped. */ - log: string[]; - /** Highest event `seq` seen (SSE id / envelope seq / polled events). */ - lastSeq: number; + run: RunModel; /** Current live-update transport. */ liveMode: 'sse' | 'poll'; stream?: { dispose(): void }; @@ -60,37 +60,51 @@ interface PanelState { refreshDebounce?: NodeJS.Timeout; /** A detail fetch is in flight — coalesces timer/reveal/Refresh races. */ inflight: boolean; - /** A load was requested while one was in flight — re-run when it ends - * (e.g. the stream's `end` frame racing an event-debounced fetch). */ + /** A load was requested while one was in flight — re-run when it ends. */ reloadRequested: boolean; - /** Result metadata + artifacts, fetched once the job is terminal. */ + /** The job detail (not just a list row) has been fetched once. */ + detailLoaded: boolean; + /** False for a restored panel until its first fetch. */ + statusKnown: boolean; result: JobResultResponse | null; - resultFetched: boolean; + resultState: ResultState; /** The finished job's remaining event history has been read. */ historyFetched: boolean; + buildError: BuildError | null; + buildLogFetched: boolean; + /** The webview script has said `ready` since it last (re)loaded. */ + ready: boolean; + /** Regions last sent to the webview. */ + sent: Partial; + /** The clock last sent to the webview (JSON). */ + sentClock: string; } /** * Manages the "Proof Job" webview panels — one per job, reused on re-open. * - * Live updates are SSE-first: while the panel is visible and the job is - * non-terminal, an event stream (`/api/v1/jobs/{id}/stream`) feeds the event - * log incrementally and triggers debounced detail re-fetches; a slow safety - * poll runs alongside. When the stream is down the view falls back to 5 s - * polling plus `/events?after=` catch-up, resuming the stream with - * `Last-Event-ID` once it reconnects — the server replays missed events - * gap-free from its durable log. Hidden panels release their stream and - * timers; revealing re-attaches from the saved cursor. + * The page is set once; afterwards the host sends region patches and + * activity rows, so focus, open sections and the activity filter survive + * every update. Live updates are SSE-first: while the panel is visible and + * the job is non-terminal, an event stream feeds the activity list and + * triggers debounced detail re-fetches; a slow safety poll runs alongside. + * When the stream is down the view falls back to 5 s polling plus + * `/events?after=` catch-up. Hidden panels release their stream and timers; + * when the webview reloads (reveal, window reload) it asks for a snapshot. */ -export class JobDetailViewManager implements vscode.Disposable { +export class JobDetailViewManager implements vscode.Disposable, vscode.WebviewPanelSerializer { private readonly states = new Map(); constructor( + private readonly extensionUri: vscode.Uri, private readonly secrets: vscode.SecretStorage, private readonly log: vscode.LogOutputChannel, private readonly documents: ProofDocuments, + private readonly origins: JobOrigins, /** Called after an action here changed a job (the tree refreshes). */ private readonly onJobChanged: () => void, + /** Run a finished job again (the caller opens the new job). */ + private readonly onRunAgain: (job: JobResponse) => Promise, ) {} /** Close every panel: the server or the account changed. */ @@ -101,95 +115,108 @@ export class JobDetailViewManager implements vscode.Disposable { } /** Open (or reveal) the detail panel for `job`, then fetch fresh data. */ - async open(job: JobResponse, source?: string): Promise { + async open(job: JobResponse, origin?: JobOrigin): Promise { const existing = this.states.get(job.id); if (existing) { - existing.source = source ?? existing.source; + existing.origin = origin ?? existing.origin; existing.panel.reveal(); await this.load(job.id); return; } - const panel = vscode.window.createWebviewPanel( - 'inference.proofJob', - this.title(job), + JOB_PANEL_VIEW_TYPE, + this.title(job, origin), vscode.ViewColumn.Active, - { - enableScripts: true, - // The view is fully self-contained: no local resources at all. - localResourceRoots: [], - }, + this.webviewOptions(), ); + await this.adopt(panel, job, origin); + } + + /** Restore a panel VS Code kept across a window reload. */ + async deserializeWebviewPanel(panel: vscode.WebviewPanel, saved: unknown): Promise { + const jobId = (saved as SavedPanelState | undefined)?.jobId; + if (typeof jobId !== 'string' || !jobId || this.states.has(jobId)) { + panel.dispose(); + return; + } + panel.webview.options = this.webviewOptions(); + await this.adopt(panel, { id: jobId, status: 'Accepted' }, undefined, false); + } + + private webviewOptions(): vscode.WebviewOptions & vscode.WebviewPanelOptions { + // The page is self-contained: inline styles, inline SVG, one nonce'd + // script. No local resources are loaded. + return { enableScripts: true, localResourceRoots: [] }; + } + + private async adopt( + panel: vscode.WebviewPanel, + job: JobResponse, + origin?: JobOrigin, + known = true, + ): Promise { + const id = job.id; const state: PanelState = { panel, job, - source: source ?? null, + origin, error: null, - log: [], - lastSeq: 0, + run: newRunModel(), liveMode: 'poll', inflight: false, reloadRequested: false, + detailLoaded: false, + statusKnown: known, result: null, - resultFetched: false, + resultState: 'n/a', historyFetched: false, + buildError: null, + buildLogFetched: false, + ready: false, + sent: {}, + sentClock: '', }; - this.states.set(job.id, state); + this.states.set(id, state); + panel.iconPath = vscode.Uri.joinPath(this.extensionUri, 'icons', 'file_icon.svg'); + if (!origin) { + const config = await this.config(); + state.origin = config ? this.origins.get(config.serverUrl, id) : undefined; + } + panel.title = this.title(job, state.origin); panel.onDidDispose(() => { - this.suspend(job.id); - this.states.delete(job.id); + this.suspend(id); + this.states.delete(id); }); - panel.webview.onDidReceiveMessage( - (message: { command?: string; artifactId?: string }) => { - switch (message?.command) { - case 'refresh': - void this.load(job.id); - break; - case 'cancel': - void this.cancel(job.id); - break; - case 'downloadArtifact': - if (typeof message.artifactId === 'string') { - void this.downloadArtifact( - job.id, - message.artifactId, - ); - } - break; - case 'openArtifact': - if (typeof message.artifactId === 'string') { - void this.openArtifact(job.id, message.artifactId); - } - break; - case 'compare': - void compareProof(this.secrets, this.log, this.documents, job); - break; - case 'openCertificate': - void openInPortal(this.secrets, job); - break; - } - }, - ); - // Hidden panels hold no stream or timers; reveal re-attaches and the - // stream resumes from the saved cursor (missed events are replayed). + panel.webview.onDidReceiveMessage((message: unknown) => this.onMessage(id, message)); + // Hidden panels hold no stream or timers; the webview reloads on reveal + // and asks for a snapshot (`ready`). panel.onDidChangeViewState((e) => { + const fresh = this.states.get(id); + if (!fresh) { + return; + } if (e.webviewPanel.visible) { - this.render(job.id); - this.ensureLive(job.id); - void this.load(job.id); + this.ensureLive(id); + void this.load(id); } else { - this.suspend(job.id); + fresh.ready = false; + this.suspend(id); } }); - this.render(job.id); - this.ensureLive(job.id); - await this.load(job.id); + panel.webview.html = renderShell({ + nonce: crypto.randomBytes(16).toString('hex'), + cspSource: panel.webview.cspSource, + }); + if (known) { + this.ensureLive(id); + } + await this.load(id); } - private title(job: JobResponse): string { - return `Proof: ${job.filename ?? job.id}`; + private title(job: JobResponse, origin?: JobOrigin): string { + return `Proof: ${JobOrigins.displayName(origin) ?? job.filename ?? job.id}`; } /** Resolved config, or null (missing key or invalid URL) — never throws. */ @@ -201,6 +228,60 @@ export class JobDetailViewManager implements vscode.Disposable { } } + // ── Webview messages ──────────────────────────────────────────────────── + + private onMessage(id: string, raw: unknown): void { + const state = this.states.get(id); + const message = (raw ?? {}) as { command?: unknown; artifactId?: unknown; line?: unknown; obligation?: unknown }; + if (!state || typeof message.command !== 'string') { + return; + } + const artifactId = typeof message.artifactId === 'string' ? message.artifactId : undefined; + const line = typeof message.line === 'number' && Number.isInteger(message.line) ? message.line : undefined; + const obligation = typeof message.obligation === 'string' && message.obligation ? message.obligation : undefined; + switch (message.command) { + case 'ready': + state.ready = true; + this.sendSnapshot(id); + break; + case 'refresh': + void this.load(id); + break; + case 'cancel': + void this.cancel(id); + break; + case 'downloadArtifact': + if (artifactId) void this.downloadArtifact(id, artifactId); + break; + case 'openArtifact': + if (artifactId) void this.openArtifact(id, artifactId); + break; + case 'gotoLine': + if (line !== undefined) void this.gotoLine(id, line, artifactId); + break; + case 'gotoTheorem': + if (obligation) void this.gotoTheorem(id, obligation, artifactId, line); + break; + case 'compare': + void compareProof(this.secrets, this.log, this.documents, state.job); + break; + case 'openCertificate': + void openInPortal(this.secrets, state.job, 'certificate'); + break; + case 'openPortal': + void openInPortal(this.secrets, state.job, 'job'); + break; + case 'copyJobId': + void vscode.env.clipboard.writeText(id).then(() => + vscode.window.setStatusBarMessage(`Copied job ID ${id}`, 3000), + ); + break; + case 'resubmit': + void this.onRunAgain(state.job); + break; + } + } + // ── Live stream ───────────────────────────────────────────────────────── /** Start the SSE stream if the panel is visible and the job can move. */ @@ -225,13 +306,12 @@ export class JobDetailViewManager implements vscode.Disposable { `/api/v1/jobs/${encodeURIComponent(id)}/stream`, ), apiKey: config.apiKey, - // Deliberately not seeded from JobResponse.lastEventSeq: a - // fresh panel connects from seq 0 so the durable history - // replays into the event log (bounded — 200/batch on the - // server, EVENT_LOG_CAP lines kept). Hide/reveal resumes - // from the cursor whose events the log already holds. + // A fresh panel connects from seq 0 so the durable history + // replays into the activity list (bounded — 200/batch on the + // server, EVENT_LOG_CAP rows kept). Hide/reveal resumes from + // the cursor whose events the model already holds. lastEventId: - fresh.lastSeq > 0 ? String(fresh.lastSeq) : undefined, + fresh.run.lastSeq > 0 ? String(fresh.run.lastSeq) : undefined, onMessage: (msg) => this.onStreamMessage(id, msg), onStateChange: (s, detail) => { const st = this.states.get(id); @@ -270,28 +350,40 @@ export class JobDetailViewManager implements vscode.Disposable { this.log.warn(`Job ${id}: unparseable SSE frame (${msg.event})`); return; } - // Advance-then-append: state.lastSeq is the single dedupe authority. - // The stream and the poll fallback can overlap (the SSE client - // reconnects with its own Last-Event-ID while a poll already moved - // the cursor) — anything at or below the cursor is a replay. - if (typeof envelope.seq === 'number') { - if (envelope.seq <= state.lastSeq) { - return; - } - state.lastSeq = envelope.seq; - } - this.appendLogLine(state, formatEventLine(envelope)); + this.ingest(id, [envelope]); if (!DETAIL_NEUTRAL_TYPES.has(envelope.type)) { this.scheduleDetailRefresh(id); } } - private appendLogLine(state: PanelState, line: string): void { - state.log.push(line); - if (state.log.length > EVENT_LOG_CAP) { - state.log.splice(0, state.log.length - EVENT_LOG_CAP); + /** + * Apply events to the run model (it dedupes replays: the stream and the + * poll fallback overlap), send the new activity rows, and re-render the + * summary when an event can change it. + */ + private ingest(id: string, events: readonly EventEnvelope[]): void { + const state = this.states.get(id); + if (!state) { + return; + } + const rows: ActivityRow[] = []; + let summaryChanged = false; + for (const env of events) { + const { applied, row } = applyEvent(state.run, env); + if (!applied) { + continue; + } + if (row) { + rows.push(row); + } + summaryChanged ||= changesSummary(env.type); + } + if (rows.length > 0 && state.ready) { + void state.panel.webview.postMessage({ command: 'activity', rows }); + } + if (summaryChanged) { + this.render(id); } - void state.panel.webview.postMessage({ command: 'event', line }); } private setLiveMode(id: string, mode: 'sse' | 'poll'): void { @@ -300,10 +392,7 @@ export class JobDetailViewManager implements vscode.Disposable { return; } state.liveMode = mode; - const uiMode: LiveMode = isStreamTerminalStatus(state.job.status) - ? 'terminal' - : mode; - void state.panel.webview.postMessage({ command: 'mode', mode: uiMode }); + this.render(id); this.schedule(id); // re-arm the poll at the cadence the mode implies } @@ -341,40 +430,42 @@ export class JobDetailViewManager implements vscode.Disposable { try { const config = await resolveConfig(this.secrets); if (!config) { - this.renderError(id, 'Proof server API key is not set.'); + this.renderError(id, 'The proof server API key is not set. Run “Inference: Set Proof Server API Key”.'); return; } const api = new ProverApi(config.serverUrl, config.apiKey); const fresh = await api.getJob(id); - if (!this.states.get(id)) { + const current = this.states.get(id); + if (!current) { return; // panel closed while the fetch was in flight } + const wasKnown = current.detailLoaded; + current.job = fresh; + current.detailLoaded = true; + current.statusKnown = true; + current.error = null; + current.panel.title = this.title(fresh, current.origin); + if (!wasKnown) { + this.ensureLive(id); // a restored panel learns its status here + } // Stream-terminal, not display-terminal: on `Lost` the server // keeps the stream open and may re-queue the job — keep ours too. - const terminal = isStreamTerminalStatus(fresh.status); - let auxChanged = false; - if (terminal) { - // No more movement: release the stream, fetch the verdict and - // (when opened post-mortem) backfill the event history. - state.stream?.dispose(); - state.stream = undefined; - auxChanged = await this.fetchResultOnce(id, api); - auxChanged = - (await this.catchUpHistoryOnce(id, api)) || auxChanged; - } else if (state.liveMode !== 'sse') { + if (isStreamTerminalStatus(fresh.status)) { + current.stream?.dispose(); + current.stream = undefined; + if (current.resultState !== 'loaded') { + current.resultState = 'loading'; + } + this.render(id); + await this.fetchResultOnce(id, api); + await this.catchUpHistoryOnce(id, api); + await this.fetchBuildErrorOnce(id, api); + } else if (current.liveMode !== 'sse') { await this.pollEvents(id, api); } - - const changed = - JSON.stringify(fresh) !== JSON.stringify(state.job); - const hadError = state.error !== null; - state.error = null; - state.job = fresh; - if (changed || hadError || auxChanged) { - this.render(id); - } else { - // Acknowledge a no-op refresh without an HTML swap. + const changed = this.render(id); + if (!changed && state.ready) { void state.panel.webview.postMessage({ command: 'checked', at: new Date().toLocaleTimeString(), @@ -403,61 +494,49 @@ export class JobDetailViewManager implements vscode.Disposable { } } - /** - * Fetch result metadata + artifacts once (terminal jobs only). - * Returns true when new data landed (the caller must re-render). - */ - private async fetchResultOnce(id: string, api: ProverApi): Promise { + /** Fetch result metadata + artifacts once (terminal jobs only). */ + private async fetchResultOnce(id: string, api: ProverApi): Promise { const state = this.states.get(id); - if (!state || state.resultFetched) { - return false; + if (!state || state.resultState === 'loaded') { + return; } try { - state.result = await api.getResult(id); - state.resultFetched = true; - return true; + const result = await api.getResult(id); + const fresh = this.states.get(id); + if (fresh) { + fresh.result = result; + fresh.resultState = 'loaded'; + } } catch (err) { // 409 NOT_TERMINAL = raced a transition; retry on next refresh. - if (!(err instanceof ApiError && err.status === 409)) { - this.log.warn( - `Job ${id} result: ${err instanceof Error ? err.message : err}`, - ); + const fresh = this.states.get(id); + if (fresh && !(err instanceof ApiError && err.status === 409)) { + fresh.resultState = 'failed'; + this.log.warn(`Job ${id} result: ${err instanceof Error ? err.message : err}`); } - return false; } } /** - * Once a job has finished, read every event past the panel's cursor: the - * whole history for a panel opened afterwards, or the tail a polling - * panel had not fetched yet when the job ended. Reads until a short page - * (bounded) and keeps the newest {@link EVENT_LOG_CAP} lines — the tail - * holds the verdict. Returns true when lines were added. + * Once a job has finished, read every event past the model's cursor: the + * whole history for a panel opened afterwards, or the tail a polling panel + * had not fetched yet. Reads until a short page (bounded). */ - private async catchUpHistoryOnce( - id: string, - api: ProverApi, - ): Promise { + private async catchUpHistoryOnce(id: string, api: ProverApi): Promise { const state = this.states.get(id); if (!state || state.historyFetched) { - return false; + return; } try { - const lines: string[] = []; - let cursor = state.lastSeq; + const events: EventEnvelope[] = []; + let cursor = state.run.lastSeq; for (let page = 0; page < MAX_HISTORY_PAGES; page++) { const res = await api.getEvents(id, cursor); for (const env of res.events) { - if (typeof env.seq === 'number') { - if (env.seq <= cursor) { - continue; - } + events.push(env); + if (typeof env.seq === 'number' && env.seq > cursor) { cursor = env.seq; } - lines.push(formatEventLine(env)); - } - if (lines.length > EVENT_LOG_CAP) { - lines.splice(0, lines.length - EVENT_LOG_CAP); } if (res.events.length < EVENTS_PAGE) { break; @@ -465,50 +544,63 @@ export class JobDetailViewManager implements vscode.Disposable { } const fresh = this.states.get(id); if (!fresh) { - return false; - } - fresh.log.push(...lines); - if (fresh.log.length > EVENT_LOG_CAP) { - fresh.log.splice(0, fresh.log.length - EVENT_LOG_CAP); + return; } - fresh.lastSeq = Math.max(fresh.lastSeq, cursor); fresh.historyFetched = true; - return lines.length > 0; + // At the row cap new rows replace old ones, so count additions. + let added = 0; + for (const env of events) { + if (applyEvent(fresh.run, env).row) { + added++; + } + } + if (fresh.ready && added > 0) { + void fresh.panel.webview.postMessage({ command: 'activity', rows: fresh.run.rows, reset: true }); + } } catch (err) { - this.log.warn( - `Job ${id} event history: ${err instanceof Error ? err.message : err}`, - ); - return false; + this.log.warn(`Job ${id} event history: ${err instanceof Error ? err.message : err}`); } } - /** Poll-mode event catch-up: replay anything past the cursor. */ - private async pollEvents(id: string, api: ProverApi): Promise { + /** For a compile failure, read the build log once and keep its first error. */ + private async fetchBuildErrorOnce(id: string, api: ProverApi): Promise { const state = this.states.get(id); - if (!state) { + const code = state?.job.errorCode; + if (!state || state.buildLogFetched || (code !== 'compile_failed' && code !== 'completed_compile_failed')) { + return; + } + const info = state.result?.artifacts.find((a) => a.kind === 'BuildLog'); + if (!info) { return; } + state.buildLogFetched = true; try { - const res = await api.getEvents(id, state.lastSeq); + const text = await this.documents.text(api, id, info); const fresh = this.states.get(id); - if (!fresh) { - return; + if (fresh) { + fresh.buildError = firstBuildError(text); } - for (const env of res.events) { - // Same advance-then-append dedupe as the stream path: a - // reconnecting stream may already have shown these. - if (typeof env.seq === 'number') { - if (env.seq <= fresh.lastSeq) { - continue; - } - fresh.lastSeq = env.seq; - } - this.appendLogLine(fresh, formatEventLine(env)); + } catch (err) { + // Let the next refresh try again. + const fresh = this.states.get(id); + if (fresh) { + fresh.buildLogFetched = false; } + this.log.warn(`Job ${id} build log: ${err instanceof Error ? err.message : err}`); + } + } + + /** Poll-mode event catch-up: replay anything past the cursor. */ + private async pollEvents(id: string, api: ProverApi): Promise { + const state = this.states.get(id); + if (!state) { + return; + } + try { + const res = await api.getEvents(id, state.run.lastSeq); + this.ingest(id, res.events); } catch (err) { - this.log.warn( - `Job ${id} event poll: ${err instanceof Error ? err.message : err}`, - ); + this.log.warn(`Job ${id} event poll: ${err instanceof Error ? err.message : err}`); } } @@ -518,7 +610,7 @@ export class JobDetailViewManager implements vscode.Disposable { if ( !state || !state.panel.visible || - isStreamTerminalStatus(state.job.status) + (state.detailLoaded && isStreamTerminalStatus(state.job.status)) ) { return; } @@ -558,7 +650,7 @@ export class JobDetailViewManager implements vscode.Disposable { } const acted = await cancelJobInteractive(this.secrets, this.log, { id, - filename: state.job.filename, + filename: JobOrigins.displayName(state.origin) ?? state.job.filename, }); if (acted) { this.onJobChanged(); @@ -566,25 +658,30 @@ export class JobDetailViewManager implements vscode.Disposable { } } - private async downloadArtifact( - id: string, - artifactId: string, - ): Promise { - const state = this.states.get(id); - // The artifact id from the webview is only trusted as a lookup key - // into the server-provided list. - const info = state?.result?.artifacts.find((a) => a.id === artifactId); + /** The artifact list: the result's when loaded, else fetched. */ + private async artifacts(id: string, api: ProverApi): Promise { + return this.states.get(id)?.result?.artifacts ?? (await api.listArtifacts(id)); + } + + private async downloadArtifact(id: string, artifactId: string): Promise { const config = await this.config(); - if (!state || !info || !config) { + if (!config) { return; } + const api = new ProverApi(config.serverUrl, config.apiKey); try { + // The artifact id from the webview is only a lookup key into the + // server-provided list. + const info = (await this.artifacts(id, api)).find((a) => a.id === artifactId); + if (!info) { + return; + } const content = await vscode.window.withProgress( { location: vscode.ProgressLocation.Notification, title: `Downloading ${info.filename}…`, }, - () => fetchVerified(new ProverApi(config.serverUrl, config.apiKey), id, info), + () => fetchVerified(api, id, info), ); const target = await vscode.window.showSaveDialog({ defaultUri: vscode.Uri.joinPath( @@ -599,7 +696,7 @@ export class JobDetailViewManager implements vscode.Disposable { await vscode.workspace.fs.writeFile(target, content); const openable = /\.(v|json|log|txt|md)$/i.test(target.path); const action = await vscode.window.showInformationMessage( - `Inference: saved ${info.filename}.`, + `Inference: saved ${path.basename(target.fsPath)}.`, ...(openable ? ['Open File'] : []), ); if (action === 'Open File') { @@ -616,14 +713,18 @@ export class JobDetailViewManager implements vscode.Disposable { } /** Show a text artifact as a read-only document (SHA-256-checked). */ - private async openArtifact(id: string, artifactId: string): Promise { - const info = this.states.get(id)?.result?.artifacts.find((a) => a.id === artifactId); + private async openArtifact(id: string, artifactId: string, line?: number): Promise { const config = await this.config(); - if (!info || !config || !isTextArtifactKind(info.kind)) { + if (!config) { return; } + const api = new ProverApi(config.serverUrl, config.apiKey); try { - await this.documents.open(new ProverApi(config.serverUrl, config.apiKey), id, info); + const info = (await this.artifacts(id, api)).find((a) => a.id === artifactId); + if (!info || !isTextArtifactKind(info.kind)) { + return; + } + await this.documents.open(api, id, info, line); } catch (err) { this.log.error( `Artifact ${artifactId} of job ${id}: ${err instanceof Error ? err.message : err}`, @@ -632,6 +733,86 @@ export class JobDetailViewManager implements vscode.Disposable { } } + /** + * Jump to a line of the submitted file: the local `.v` when it is still + * byte-identical to the upload, else the uploaded copy (read-only). An + * explicit artifact (e.g. the returned proof) opens that one instead. + */ + private async gotoLine(id: string, line: number, artifactId?: string): Promise { + const state = this.states.get(id); + const config = await this.config(); + if (!state || !config) { + return; + } + const api = new ProverApi(config.serverUrl, config.apiKey); + try { + const artifacts = await this.artifacts(id, api); + const target = artifactId + ? artifacts.find((a) => a.id === artifactId) + : artifacts.find((a) => a.kind === 'InputV'); + if (target?.kind === 'InputV' && state.origin) { + const local = vscode.Uri.file(state.origin.vPath); + try { + const bytes = await vscode.workspace.fs.readFile(local); + const sha = target.sha256.toLowerCase(); + if (crypto.createHash('sha256').update(bytes).digest('hex') === sha) { + // An open editor may hold unsaved edits that move lines. + const doc = await vscode.workspace.openTextDocument(local); + const text = Buffer.from(doc.getText(), 'utf-8'); + if (!doc.isDirty || crypto.createHash('sha256').update(text).digest('hex') === sha) { + await showAtLine(doc, line); + return; + } + } + } catch { + // The local file is gone; fall back to the uploaded copy. + } + } + if (target) { + await this.openArtifact(id, target.id, line); + } + } catch (err) { + this.log.error(`Job ${id} go to line ${line}: ${err instanceof Error ? err.message : err}`); + vscode.window.showErrorMessage(`Inference: ${describeError(err)}`); + } + } + + /** + * Jump to an obligation's theorem: its proof in the returned file when + * `artifactId` names it, else its statement in the submitted file. The + * theorem is found by name; `fallbackLine` (the proof hole the server + * reported) is used when the submitted file does not declare it. + */ + private async gotoTheorem(id: string, name: string, artifactId?: string, fallbackLine?: number): Promise { + const config = await this.config(); + if (!this.states.has(id) || !config) { + return; + } + const api = new ProverApi(config.serverUrl, config.apiKey); + try { + const artifacts = await this.artifacts(id, api); + const target = artifactId + ? artifacts.find((a) => a.id === artifactId) + : artifacts.find((a) => a.kind === 'InputV'); + if (!target || !isTextArtifactKind(target.kind)) { + return; + } + const found = declarationLine(await this.documents.text(api, id, target), name); + const line = found ?? (target.kind === 'InputV' ? fallbackLine : undefined); + if (line === undefined) { + void vscode.window.showInformationMessage(`Inference: ${name} was not found in ${target.filename}.`); + } + if (target.kind === 'InputV') { + await this.gotoLine(id, line ?? 1); + } else { + await this.openArtifact(id, target.id, line); + } + } catch (err) { + this.log.error(`Job ${id} go to ${name}: ${err instanceof Error ? err.message : err}`); + vscode.window.showErrorMessage(`Inference: ${describeError(err)}`); + } + } + // ── Rendering ─────────────────────────────────────────────────────────── private renderError(id: string, message: string): void { @@ -643,22 +824,82 @@ export class JobDetailViewManager implements vscode.Disposable { this.render(id); } - private render(id: string): void { + private liveMode(state: PanelState): LiveMode { + return state.detailLoaded && isStreamTerminalStatus(state.job.status) ? 'terminal' : state.liveMode; + } + + private regions(state: PanelState): Regions { + const source = state.origin?.infPath ? path.basename(state.origin.infPath) : null; + return renderRegions( + buildJobView({ + job: state.job, + result: state.result, + resultState: state.resultState, + detailLoaded: state.detailLoaded, + statusKnown: state.statusKnown, + run: state.run, + buildError: state.buildError, + source, + error: state.error, + live: this.liveMode(state), + }), + ); + } + + private clock(state: PanelState): unknown { + const view = buildJobView({ + job: state.job, + detailLoaded: state.detailLoaded, + run: state.run, + live: this.liveMode(state), + }); + return view.clock; + } + + /** Send the regions that changed; returns whether anything did. */ + private render(id: string): boolean { + const state = this.states.get(id); + if (!state || !state.ready) { + return false; + } + const regions = this.regions(state); + const changed: Partial = {}; + for (const key of REGION_IDS) { + if (state.sent[key] !== regions[key]) { + changed[key] = regions[key]; + } + } + const clock = this.clock(state); + const clockJson = JSON.stringify(clock); + const regionsChanged = Object.keys(changed).length > 0; + if (regionsChanged) { + state.sent = { ...state.sent, ...changed }; + void state.panel.webview.postMessage({ command: 'regions', regions: changed }); + } + // The clock can change on its own (an end time from a late event). + if (clockJson !== state.sentClock) { + state.sentClock = clockJson; + void state.panel.webview.postMessage({ command: 'clock', clock }); + } + return regionsChanged; + } + + /** Full state for a webview that (re)loaded. */ + private sendSnapshot(id: string): void { const state = this.states.get(id); if (!state) { return; } - state.panel.title = this.title(state.job); - const terminal = isStreamTerminalStatus(state.job.status); - state.panel.webview.html = renderJobDetailHtml(state.job, { - nonce: crypto.randomBytes(16).toString('hex'), - cspSource: state.panel.webview.cspSource, - error: state.error, - live: terminal ? 'terminal' : state.liveMode, - eventLog: state.log, - canCancel: isCancelableStatus(state.job.status), - result: state.result, - source: state.source, + const regions = this.regions(state); + const clock = this.clock(state); + state.sent = regions; + state.sentClock = JSON.stringify(clock); + void state.panel.webview.postMessage({ + command: 'snapshot', + jobId: id, + regions, + rows: state.run.rows.slice(-EVENT_LOG_CAP), + clock, }); } diff --git a/editors/vscode/src/prover/jobOrigins.ts b/editors/vscode/src/prover/jobOrigins.ts new file mode 100644 index 00000000..1ab016d7 --- /dev/null +++ b/editors/vscode/src/prover/jobOrigins.ts @@ -0,0 +1,65 @@ +import * as path from 'path'; +import type * as vscode from 'vscode'; + +/** Where a job's upload came from on this machine. */ +export interface JobOrigin { + /** The `.inf` that was compiled, for Prove This File. */ + infPath?: string; + /** The `.v` that was uploaded. */ + vPath: string; + /** SHA-256 (hex) of the uploaded bytes, to tell whether `vPath` changed since. */ + vSha256: string; +} + +interface StoredOrigin extends JobOrigin { + at: number; +} + +const KEY = 'inference.prover.jobOrigins'; +/** Origins kept per workspace; the oldest are dropped first. */ +export const ORIGIN_CAP = 200; + +/** Keep the newest `cap` entries (pure, for tests). */ +export function pruneOrigins( + entries: Record, + cap: number, +): Record { + const sorted = Object.entries(entries).sort(([, a], [, b]) => b.at - a.at); + return Object.fromEntries(sorted.slice(0, cap)); +} + +/** + * Remembers which local files each submitted job came from, per workspace, + * so the job panel can name the `.inf` and jump to lines in the local `.v`. + */ +export class JobOrigins { + constructor(private readonly memento: vscode.Memento) {} + + private key(serverUrl: string, jobId: string): string { + return `${serverUrl}|${jobId}`; + } + + get(serverUrl: string, jobId: string): JobOrigin | undefined { + const all = this.memento.get>(KEY) ?? {}; + const found = all[this.key(serverUrl, jobId)]; + if (!found || typeof found.vPath !== 'string' || typeof found.vSha256 !== 'string') { + return undefined; + } + const { at: _at, ...origin } = found; + return origin; + } + + async set(serverUrl: string, jobId: string, origin: JobOrigin): Promise { + const all = this.memento.get>(KEY) ?? {}; + all[this.key(serverUrl, jobId)] = { ...origin, at: Date.now() }; + await this.memento.update(KEY, pruneOrigins(all, ORIGIN_CAP)); + } + + /** The name the user knows the job by: the `.inf`, else the `.v`. */ + static displayName(origin: JobOrigin | undefined): string | undefined { + if (!origin) { + return undefined; + } + return path.basename(origin.infPath ?? origin.vPath); + } +} diff --git a/editors/vscode/src/prover/jobStatus.ts b/editors/vscode/src/prover/jobStatus.ts new file mode 100644 index 00000000..10008b08 --- /dev/null +++ b/editors/vscode/src/prover/jobStatus.ts @@ -0,0 +1,63 @@ +/** + * Job status sets mirrored from the server's state machine. Pure — no + * `vscode` import. + */ + +/** Statuses the control plane treats as terminal (mirrors the server). */ +const TERMINAL_STATUSES: ReadonlySet = new Set([ + 'Succeeded', + 'CompileGoals', + 'PartialSuccess', + 'Failed', + 'TimedOut', + 'Lost', + 'Canceled', + 'ProvisionFailed', +]); + +/** + * Statuses `POST /jobs/{id}/cancel` accepts (mirrors the server's switch); + * everything else — including Verifying and Canceling — is 409 NOT_CANCELABLE. + */ +const CANCELABLE_STATUSES: ReadonlySet = new Set([ + 'Accepted', + 'Queued', + 'Provisioning', + 'Booting', + 'Running', +]); + +/** Artifact kinds that are text and open as read-only documents. */ +const TEXT_ARTIFACT_KINDS: ReadonlySet = new Set([ + 'InputV', + 'CompletedV', + 'Report', + 'Goals', + 'BuildLog', + 'AgentLog', + 'RefutationV', + 'RefutationMd', +]); + +export function isTerminalStatus(status: string): boolean { + return TERMINAL_STATUSES.has(status); +} + +/** + * Statuses that end the server's event stream. `Lost` is soft-terminal: the + * reaper re-queues it (bounded retry, Lost → Queued) and `StreamEvents` + * deliberately keeps the SSE stream open without an `end` frame — so the + * client must keep its transport (stream + polls) alive on Lost too, or it + * freezes on a job that is actively being rerun. + */ +export function isStreamTerminalStatus(status: string): boolean { + return TERMINAL_STATUSES.has(status) && status !== 'Lost'; +} + +export function isCancelableStatus(status: string): boolean { + return CANCELABLE_STATUSES.has(status); +} + +export function isTextArtifactKind(kind: string): boolean { + return TEXT_ARTIFACT_KINDS.has(kind); +} diff --git a/editors/vscode/src/prover/jobVerdict.ts b/editors/vscode/src/prover/jobVerdict.ts new file mode 100644 index 00000000..96053145 --- /dev/null +++ b/editors/vscode/src/prover/jobVerdict.ts @@ -0,0 +1,421 @@ +/** + * What a job's result means, in plain words — the single wording source for + * the job panel, the Proof Jobs view, the status bar and notifications. + * Pure — no `vscode` import. + * + * The claim rules are fail-closed and unchanged from the portal's certificate + * (`portal/src/lib/certificate.ts`): a positive claim needs a Succeeded + * prove-mode run with every hole closed, claim class Verified, a result that + * matches the job, and the independent verifier's full acceptance. Anything + * short of that is worded as "not verified", never as a proof. + */ + +import { duplicateNameHint, type BuildError } from './buildLog'; +import { isProvedSuccess } from './jobPresentation'; +import { errorCodeText } from './runModel'; +import type { ClaimClass, JobResponse, JobResultResponse, ObligationDto } from './types'; +import { + hasCompleteAssumptionEvidence, + normalizedVerifierOutcome, + resultMatchesJob, + verifierAcceptedFull, + verifierAcceptedPartial, +} from './verifierEvidence'; + +export type Tone = 'ok' | 'warn' | 'err' | 'refuted' | 'active' | 'muted'; + +/** Icon keys shared by the webview glyphs and the tree's codicons. */ +export type VerdictIcon = + | 'pass' + | 'warning' + | 'error' + | 'refuted' + | 'running' + | 'waiting' + | 'verifying' + | 'canceled' + | 'loading'; + +export type VerdictKind = + | 'queued' + | 'starting' + | 'proving' + | 'verifying' + | 'canceling' + | 'loading' + | 'verified' + | 'structural' + | 'partial' + | 'compile-only' + | 'unverified' + | 'conflict' + | 'rejected' + | 'compile-error' + | 'completed-compile-error' + | 'refuted' + | 'failed' + | 'timed-out' + | 'provision-failed' + | 'lost' + | 'canceled'; + +export interface Verdict { + kind: VerdictKind; + tone: Tone; + icon: VerdictIcon; + /** One or two words for badges and list rows. */ + badge: string; + headline: string; + body: string; + /** Further plain-language notes, most important first. */ + caveats: string[]; + /** The strongest claim this verdict makes; `none` for everything else. */ + claim: 'proved' | 'partial' | 'structural' | 'none'; +} + +/** Whether the terminal result (`GET /result`) is loaded. */ +export type ResultState = 'n/a' | 'loading' | 'loaded' | 'failed'; + +export interface VerdictInput { + job: JobResponse; + result?: JobResultResponse | null; + resultState?: ResultState; + /** First error of the server's build log, when the run failed to compile. */ + buildError?: BuildError | null; + /** File stems the user knows the job by (`clamp` for clamp.inf / clamp.v). */ + fileStems?: readonly string[]; +} + +function plural(n: number, one: string, many = `${one}s`): string { + return `${n} ${n === 1 ? one : many}`; +} + +function verdict( + kind: VerdictKind, + tone: Tone, + icon: VerdictIcon, + badge: string, + headline: string, + body: string, + caveats: string[] = [], + claim: Verdict['claim'] = 'none', +): Verdict { + return { kind, tone, icon, badge, headline, body, caveats, claim }; +} + +/** Verdicts of a job that is still moving (status alone decides). */ +function liveVerdict(job: JobResponse): Verdict | null { + switch (job.status) { + case 'Accepted': + return verdict('queued', 'active', 'waiting', 'Accepted', 'Accepted', + 'The proof server accepted the file and is queuing it.'); + case 'Queued': + return verdict('queued', 'active', 'waiting', 'Queued', 'Waiting for a worker', + 'The job waits until an isolated worker is free. Waiting time counts toward its time budget.'); + case 'Provisioning': + case 'Booting': + return verdict('starting', 'active', 'waiting', 'Starting', 'Preparing an isolated worker', + 'A fresh worker is starting for this job. This usually takes a minute or two.'); + case 'Running': + return verdict('proving', 'active', 'running', 'Proving', 'Proving obligations', + 'The worker compiles the file and closes its proof holes one by one.'); + case 'Verifying': + return verdict('verifying', 'active', 'verifying', 'Verifying', + 'Independently verifying the returned proof', + 'A separate verifier re-checks the completed file before any proof is claimed.'); + case 'Canceling': + return verdict('canceling', 'muted', 'canceled', 'Canceling…', 'Canceling', + 'The server is stopping this job. While its worker is still starting this can take up to about 90 seconds.'); + default: + return null; + } +} + +/** Plain notes about obligations whose statement says little. */ +function contentCaveats(obligations: readonly ObligationDto[]): string[] { + const count = (content: string) => + obligations.filter((o) => (o.content ?? 'unknown') === content).length; + const notes: string[] = []; + const empty = count('empty'); + const tautology = count('tautology'); + const unguarded = count('unguarded'); + const unknown = count('unknown'); + if (empty) { + notes.push(`${plural(empty, 'obligation has', 'obligations have')} an empty specification.`); + } + if (tautology) { + notes.push(`${plural(tautology, 'obligation is a tautology', 'obligations are tautologies')}: true for any program.`); + } + if (unguarded) { + notes.push(`${plural(unguarded, 'obligation is', 'obligations are')} not tied to the compiled module.`); + } + if (unknown) { + notes.push(`${plural(unknown, 'obligation', 'obligations')} could not be classified.`); + } + return notes; +} + +/** Why the verifier's evidence does not support the claim. */ +export function verifierRejections( + result: JobResultResponse, + expectedTargets: string[], + partial: boolean, +): string[] { + const reasons: string[] = []; + const outcome = normalizedVerifierOutcome(result); + const expectedOutcome = partial ? 'partial' : 'succeeded'; + if (outcome !== expectedOutcome) { + reasons.push(`The verifier's outcome is “${outcome ?? 'missing'}”, not “${expectedOutcome}”.`); + } + if (result.compileOk !== true) { + reasons.push('The returned file did not compile.'); + } + if (!partial && (result.verifiedClean !== true || result.admitsDetected !== false)) { + reasons.push('Some proofs are incomplete (still admitted).'); + } + if (partial && (result.verifiedClean !== false || result.admitsDetected !== true)) { + reasons.push('The admitted obligations do not match a partial result.'); + } + if (result.statementsImmutable !== true) { + reasons.push('Theorem statements were changed.'); + } + if (result.markersRemaining !== 0) { + reasons.push( + typeof result.markersRemaining === 'number' + ? `${plural(result.markersRemaining, 'proof marker remains', 'proof markers remain')}.` + : 'Remaining proof markers were not reported.', + ); + } + if (result.assumptionsClosed !== true) { + reasons.push('The proof relies on assumptions the policy does not allow.'); + } else if (!hasCompleteAssumptionEvidence(result, expectedTargets)) { + reasons.push('The per-theorem assumption evidence is incomplete or rejected.'); + } + return reasons; +} + +function terminalFailure(job: JobResponse, input: VerdictInput): Verdict { + const code = job.errorCode ?? null; + const compileOnlyNote = + job.mode === 'compile-goals' ? ['This was a compile-only run; no proof was accepted or returned.'] : []; + if (code === 'spec_refuted') { + return verdict('refuted', 'refuted', 'refuted', 'Refuted', 'Specification refuted', + 'The prover produced a machine-checked demonstration that an obligation cannot hold. This is a formal negative result, not an error.'); + } + if (code === 'compile_failed' || code === 'completed_compile_failed') { + const returned = code === 'completed_compile_failed'; + const error = input.buildError; + const body = error + ? `${error.line !== undefined ? `Line ${error.line}: ` : ''}${error.message}` + : returned + ? 'The completed file the worker returned did not compile. Open the build log for the compiler output.' + : 'The submitted file did not compile on the proof server. Open the build log for the compiler output.'; + const hint = error ? duplicateNameHint(error.message, input.fileStems ?? []) : null; + return returned + ? verdict('completed-compile-error', 'err', 'error', 'Failed', 'The returned proof did not compile', body, + hint ? [hint] : []) + : verdict('compile-error', 'err', 'error', 'Compile error', 'The prover could not compile your file', body, + hint ? [hint] : []); + } + switch (job.status) { + case 'TimedOut': { + const total = job.holesTotal ?? 0; + const closed = job.holesClosed ?? 0; + const body = code === 'QUEUE_TIMEOUT' + ? 'No worker became free before the time budget ran out.' + : 'The run used its whole time budget before it finished.'; + const caveats = total > 0 && code !== 'QUEUE_TIMEOUT' + ? [`${closed} of ${plural(total, 'obligation')} were closed before the limit; none is claimed as proved.`] + : []; + return verdict('timed-out', 'err', 'error', 'Timed out', 'Time limit reached', body, caveats); + } + case 'ProvisionFailed': + return verdict('provision-failed', 'err', 'error', "Couldn't start", "Couldn't start a worker", + 'This is a problem on the proof server, not with your file. Run it again later.', + job.errorReason ? [job.errorReason] : []); + case 'Lost': + return verdict('lost', 'warn', 'warning', 'Worker lost', 'Worker lost', + 'The worker stopped responding. The server retries lost jobs automatically; if this one stays lost, run it again.'); + case 'Canceled': + return verdict('canceled', 'muted', 'canceled', 'Canceled', 'Canceled', + 'The run was canceled before it finished.'); + default: + return verdict('failed', 'err', 'error', 'Failed', 'Not proved', + errorCodeText(code) ?? job.errorReason ?? 'No proof was produced for this run.', + compileOnlyNote); + } +} + +const COMPILE_ONLY = (): Verdict => + verdict('compile-only', 'warn', 'warning', 'Compiled only', 'Compiled — nothing was proved', + 'The file compiled with every proof hole admitted and its goals were extracted. No proof was accepted or returned.'); + +/** + * The verdict for the job panel: the job detail plus, for finished runs, the + * terminal result and its verifier evidence. + */ +export function jobVerdict(input: VerdictInput): Verdict { + const { job } = input; + const live = liveVerdict(job); + if (live) { + return live; + } + const result = input.result ?? null; + const resultState: ResultState = input.resultState ?? (result ? 'loaded' : 'n/a'); + const obligations = job.obligations ?? []; + const total = job.holesTotal ?? 0; + const closed = job.holesClosed ?? 0; + const provedTargets = obligations.filter((o) => o.status === 'proved').map((o) => o.name); + const outcome = normalizedVerifierOutcome(result); + const hasVerifierVerdict = outcome !== null; + const matches = result ? resultMatchesJob(job, result) : false; + + if (job.status === 'CompileGoals') { + return COMPILE_ONLY(); + } + + if (job.status === 'Succeeded') { + if (job.mode === 'compile-goals') { + return COMPILE_ONLY(); + } + if (job.mode !== 'prove') { + return verdict('unverified', 'warn', 'warning', 'Not verified', 'Not a proof result', + 'This run was not recorded as a proof run, so no proof is claimed.'); + } + const complete = + typeof job.holesTotal === 'number' && job.holesTotal > 0 && + typeof job.holesClosed === 'number' && job.holesClosed === job.holesTotal; + if (!complete) { + return verdict('unverified', 'warn', 'warning', 'Not verified', 'Not proved', + 'The record does not show every proof hole closed, so no proof is claimed.'); + } + if (result && !matches) { + return verdict('conflict', 'warn', 'warning', 'Inconsistent', 'Inconsistent record', + 'The job record and its result disagree, so this view makes no proof claim.'); + } + if (result && hasVerifierVerdict && !verifierAcceptedFull(result, provedTargets)) { + return verdict('rejected', 'err', 'error', 'Rejected', 'Independent verification failed', + 'The independent verifier did not accept this result, so no proof is claimed.', + verifierRejections(result, provedTargets, false)); + } + if (job.claimClass !== 'Verified' && job.claimClass !== 'StructuralOnly') { + return verdict('unverified', 'warn', 'warning', 'Not verified', 'Behavior not verified', + job.claimClass + ? 'The server did not classify this result as a behavioral proof, so the closed obligations are not shown as proved behavior.' + : 'The server did not provide a claim class, so the closed obligations are not shown as proved behavior.'); + } + // Structural and behavioral claims need the same evidence: a matching + // result the independent verifier fully accepted (as in the portal). + if (!result) { + return resultState === 'failed' + ? verdict('unverified', 'warn', 'warning', 'Not verified', 'Verifier evidence unavailable', + "The verifier's verdict could not be loaded, so this view makes no proof claim. Refresh to try again.") + : verdict('loading', 'muted', 'loading', 'Loading…', "Loading the verifier's verdict…", + 'The result is shown once the independent verifier evidence has loaded.'); + } + if (!hasVerifierVerdict) { + return verdict('unverified', 'warn', 'warning', 'Not verified', 'Not independently verified', + 'This result was checked only inside the worker; no independent verification is recorded, so no proof is claimed.'); + } + const structural = job.claimClass === 'StructuralOnly'; + // isProvedSuccess checks the status, mode and counts; a structural run + // carries its own claim class, which resultMatchesJob compares. + const claimFor = (claimClass: ClaimClass | null | undefined) => (structural ? 'Verified' : claimClass); + const proved = + isProvedSuccess(job.status, job.mode, job.holesTotal, job.holesClosed, claimFor(job.claimClass)) && + isProvedSuccess(result.status, result.mode, result.holesTotal, result.holesClosed, claimFor(result.claimClass)) && + matches && + verifierAcceptedFull(result, provedTargets); + if (!proved) { + return verdict('unverified', 'warn', 'warning', 'Not verified', 'Not proved', + 'This view cannot confirm a proof for this run.'); + } + if (structural) { + return verdict('structural', 'warn', 'warning', 'Structural only', 'Structural validity only', + `All ${plural(total, 'obligation')} closed and independently re-verified. They establish structural validity (Wasm module typing) only — this is not a functional-correctness result.`, + contentCaveats(obligations), 'structural'); + } + const grounded = obligations.filter((o) => o.content === 'grounded').length; + return verdict('verified', 'ok', 'pass', 'Verified', 'Proved and independently verified', + `All ${plural(total, 'obligation')} closed and re-checked by the independent verifier.${grounded > 0 ? ` ${grounded} ${grounded === 1 ? 'states a behavioral property' : 'state behavioral properties'} of the compiled Wasm.` : ''}`, + contentCaveats(obligations), 'proved'); + } + + if (job.status === 'PartialSuccess') { + const partialCounts = job.mode === 'prove' && total > 0 && closed > 0 && closed < total; + if (!partialCounts) { + return verdict('unverified', 'warn', 'warning', 'Not verified', 'Not a valid partial proof', + 'A partial proof needs some, but not all, obligations closed in a proof run, so no proof is claimed.'); + } + if (result && !matches) { + return verdict('conflict', 'warn', 'warning', 'Inconsistent', 'Inconsistent record', + 'The job record and its result disagree, so this view makes no proof claim.'); + } + if (job.claimClass !== 'PartialVerified') { + return verdict('unverified', 'warn', 'warning', 'Not verified', 'Partial result not verified', + 'The server did not classify this as a verified partial result, so no proof is claimed.'); + } + if (!result) { + return resultState === 'failed' + ? verdict('unverified', 'warn', 'warning', 'Not verified', 'Verifier evidence unavailable', + "The verifier's verdict could not be loaded, so this view makes no proof claim. Refresh to try again.") + : verdict('loading', 'muted', 'loading', 'Loading…', "Loading the verifier's verdict…", + 'The result is shown once the independent verifier evidence has loaded.'); + } + if (!hasVerifierVerdict) { + return verdict('unverified', 'warn', 'warning', 'Not verified', 'Not independently verified', + 'This partial result was checked only inside the worker; no independent verification is recorded.'); + } + if (verifierAcceptedPartial(result, provedTargets)) { + return verdict('partial', 'warn', 'warning', 'Partially proved', 'Partially proved', + `${closed} of ${plural(total, 'obligation')} closed and independently re-verified; the other ${total - closed} remain admitted (unproved).`, + contentCaveats(obligations.filter((o) => o.status === 'proved')), 'partial'); + } + return verdict('rejected', 'err', 'error', 'Rejected', 'Independent verification failed', + 'The independent verifier did not accept this partial result, so no proof is claimed.', + verifierRejections(result, provedTargets, true)); + } + + return terminalFailure(job, input); +} + +/** + * The verdict for a job list row (no result, no events). The list DTO carries + * the server's claim class, which the server sets to Verified only after the + * independent verifier accepted the run. + */ +export function listVerdict(job: JobResponse): Verdict { + const live = liveVerdict(job); + if (live) { + return live; + } + const total = job.holesTotal ?? 0; + const closed = job.holesClosed ?? 0; + if (job.status === 'CompileGoals' || (job.status === 'Succeeded' && job.mode === 'compile-goals')) { + return COMPILE_ONLY(); + } + if (job.status === 'Succeeded') { + if (isProvedSuccess(job.status, job.mode, job.holesTotal, job.holesClosed, job.claimClass)) { + return verdict('verified', 'ok', 'pass', 'Verified', 'Proved and independently verified', + `All ${plural(total, 'obligation')} closed and re-checked by the independent verifier.`, [], 'proved'); + } + const complete = job.mode === 'prove' && total > 0 && closed === total; + if (complete && job.claimClass === 'StructuralOnly') { + return verdict('structural', 'warn', 'warning', 'Structural only', 'Structural validity only', + `All ${plural(total, 'obligation')} closed. They establish structural validity only — not functional correctness.`, + [], 'structural'); + } + return verdict('unverified', 'warn', 'warning', 'Not verified', 'Not verified', + 'This result is not shown as a proof. Open it for details.'); + } + if (job.status === 'PartialSuccess') { + if (job.mode === 'prove' && job.claimClass === 'PartialVerified' && closed > 0 && closed < total) { + return verdict('partial', 'warn', 'warning', 'Partially proved', 'Partially proved', + `${closed} of ${plural(total, 'obligation')} closed and independently re-verified; the rest remain admitted.`, + [], 'partial'); + } + return verdict('unverified', 'warn', 'warning', 'Not verified', 'Not verified', + 'This partial result is not shown as a proof. Open it for details.'); + } + return terminalFailure(job, { job }); +} diff --git a/editors/vscode/src/prover/proofDocuments.ts b/editors/vscode/src/prover/proofDocuments.ts index 4cb428d9..1f164f33 100644 --- a/editors/vscode/src/prover/proofDocuments.ts +++ b/editors/vscode/src/prover/proofDocuments.ts @@ -47,6 +47,20 @@ function artifactUri(jobId: string, info: ArtifactInfo): vscode.Uri { }); } +/** Show a document with the cursor on a 1-based line (clamped), revealed in the centre. */ +export async function showAtLine(doc: vscode.TextDocument, line?: number): Promise { + const options: vscode.TextDocumentShowOptions = { preview: false }; + if (line !== undefined && Number.isInteger(line) && line > 0) { + const target = Math.min(line, doc.lineCount) - 1; + const range = doc.lineAt(target).range; + options.selection = new vscode.Range(range.start, range.start); + } + const editor = await vscode.window.showTextDocument(doc, options); + if (options.selection) { + editor.revealRange(options.selection, vscode.TextEditorRevealType.InCenter); + } +} + /** * Read-only documents for job artifacts (`inference-proof:///`). * @@ -90,12 +104,17 @@ export class ProofDocuments implements vscode.TextDocumentContentProvider, vscod return text; } - /** Download (verified) and show one artifact read-only. */ - async open(api: ProverApi, jobId: string, info: ArtifactInfo): Promise { + /** Download (verified) and show one artifact read-only, optionally at a 1-based line. */ + async open(api: ProverApi, jobId: string, info: ArtifactInfo, line?: number): Promise { const uri = artifactUri(jobId, info); await this.load(api, jobId, info, uri); const doc = await vscode.workspace.openTextDocument(uri); - await vscode.window.showTextDocument(doc, { preview: false }); + await showAtLine(doc, line); + } + + /** The text of an artifact (verified), for parsing in the host. */ + async text(api: ProverApi, jobId: string, info: ArtifactInfo): Promise { + return this.load(api, jobId, info); } /** Diff the submitted input against the completed proof. */ diff --git a/editors/vscode/src/prover/proveFile.ts b/editors/vscode/src/prover/proveFile.ts index b97b916e..185a8ef8 100644 --- a/editors/vscode/src/prover/proveFile.ts +++ b/editors/vscode/src/prover/proveFile.ts @@ -90,7 +90,7 @@ export function registerProveFileCommand( }); }, ); - await report(outcome, source, log, hooks, onCompilerCheck); + await report(outcome, uri.fsPath, log, hooks, onCompilerCheck); } catch (err) { log.error(`Prover: prove ${source}: ${err instanceof Error ? err.message : err}`); vscode.window.showErrorMessage(`Inference: ${submitErrorMessage(err)}`); @@ -102,11 +102,12 @@ export function registerProveFileCommand( async function report( outcome: ProveOutcome, - source: string, + infPath: string, log: vscode.LogOutputChannel, hooks: SubmitHooks, onCompilerCheck: (check: CompilerCheck) => void, ): Promise { + const source = path.basename(infPath); const showOutput = async (message: string, error = true) => { const show = error ? vscode.window.showErrorMessage(message, 'Show Output') @@ -123,7 +124,7 @@ async function report( : { state: 'unchecked', detail: 'server does not publish an accepted compiler' }, ); log.info(`Prover: ${source} → ${outcome.vPath} (${outcome.holes} holes) → job ${outcome.job.id}`); - await hooks.showJob(outcome.job, source); + await hooks.showJob(outcome.job, { infPath, vPath: outcome.vPath, vSha256: outcome.vSha256 }); return; } case 'no-infs': { diff --git a/editors/vscode/src/prover/proveFlow.ts b/editors/vscode/src/prover/proveFlow.ts index 195da69e..a5e61991 100644 --- a/editors/vscode/src/prover/proveFlow.ts +++ b/editors/vscode/src/prover/proveFlow.ts @@ -53,7 +53,7 @@ export interface ProveDeps { } export type ProveOutcome = - | { kind: 'submitted'; job: JobResponse; vPath: string; holes: number; checked: boolean } + | { kind: 'submitted'; job: JobResponse; vPath: string; vSha256: string; holes: number; checked: boolean } | { kind: 'no-infs' } | { kind: 'no-infc' } | { @@ -156,6 +156,7 @@ export async function proveInfFile(infPath: string, deps: ProveDeps): Promise (c === '\n' || c === '\r' ? c : ' '); + for (let i = 0; i < text.length; i++) { + const c = text[i]; + const next = text[i + 1]; + if (inString) { + if (c === '"' && next === '"') { + out += ' '; + i++; + } else if (c === '"') { + inString = false; + out += depth > 0 ? ' ' : c; + } else { + out += blank(c); + } + } else if (c === '(' && next === '*') { + depth++; + out += ' '; + i++; + } else if (depth > 0 && c === '*' && next === ')') { + depth--; + out += ' '; + i++; + } else if (c === '"') { + inString = true; + out += depth > 0 ? ' ' : c; + } else { + out += depth > 0 ? blank(c) : c; + } + } + return out; +} + +/** + * The 1-based line declaring `name` (or, for a qualified name, its last + * segment), or undefined when the text has no such declaration. Comments and + * strings are ignored. + */ +export function declarationLine(text: string, name: string): number | undefined { + const last = name.split('.').pop() ?? name; + const names = last && last !== name ? [name, last] : [name]; + const lines = maskCommentsAndStrings(text).split(/\r\n?|\n/); + for (const candidate of names) { + if (!candidate) { + continue; + } + const declaration = new RegExp( + `^\\s*(?:#\\[[^\\]]*\\]\\s*)?(?:(?:Local|Global|Polymorphic|Program)\\s+)*(?:${KEYWORDS})\\s+${escapeRegExp(candidate)}(?![\\w'])`, + ); + const index = lines.findIndex((line) => declaration.test(line)); + if (index >= 0) { + return index + 1; + } + } + return undefined; +} diff --git a/editors/vscode/src/prover/runModel.ts b/editors/vscode/src/prover/runModel.ts new file mode 100644 index 00000000..68f44b96 --- /dev/null +++ b/editors/vscode/src/prover/runModel.ts @@ -0,0 +1,395 @@ +/** + * What a job's event history says about its run: when each step started and + * finished, how each obligation was closed, and a readable activity list. + * Pure — no `vscode` import. + * + * Event types and payloads per docs/CONTRACTS.md ("Event types"). The job + * DTO stays the authority for status and counts; this model only adds what + * the DTO does not carry (step times, `by`, source lines, the deadline). + */ + +import { AGENT_LIMIT_MESSAGES, summarize, summarizeActivity } from './eventFormat'; +import type { EventEnvelope } from './types'; + +/** Activity rows kept per job, in the host and in the webview. */ +export const EVENT_LOG_CAP = 2000; + +/** Steps: lifecycle (step), agent transcript (agent), problems, diagnostics. */ +export type ActivityCategory = 'step' | 'agent' | 'warn' | 'error' | 'detail'; + +export interface ActivityRow { + seq: number; + /** RFC 3339 event time. */ + ts: string; + cat: ActivityCategory; + /** Obligation the row belongs to, when the event names one. */ + obligation?: string; + attempt?: number; + text: string; +} + +export type RunStep = 'submitted' | 'worker' | 'proving' | 'verifying'; + +export interface RunModel { + /** Highest event `seq` applied (the dedupe cursor). */ + lastSeq: number; + /** When each step started / finished, from event times. */ + reached: Partial>; + finished: Partial>; + /** From `job.queued` (older servers do not put it on the job). */ + deadlineUtc?: string; + /** Time of the event that ended the run, when one did. */ + endedAt?: string; + /** Time of the newest event, heartbeats included. */ + lastSignalAt?: string; + /** 1-based line of each obligation in the submitted `.v`. */ + sourceLines: Record; + provedBy: Record; + attempts: Record; + integrityWarnings: string[]; + rows: ActivityRow[]; +} + +export function newRunModel(): RunModel { + return { + lastSeq: 0, + reached: {}, + finished: {}, + sourceLines: {}, + provedBy: {}, + attempts: {}, + integrityWarnings: [], + rows: [], + }; +} + +function asRecord(payload: unknown): Record { + return typeof payload === 'object' && payload !== null + ? (payload as Record) + : {}; +} + +function str(v: unknown): string | undefined { + return typeof v === 'string' && v.trim().length > 0 ? v : undefined; +} + +function num(v: unknown): number | undefined { + return typeof v === 'number' && Number.isFinite(v) ? v : undefined; +} + +function plural(n: number, one: string, many = `${one}s`): string { + return `${n} ${n === 1 ? one : many}`; +} + +function fmtMs(ms: number): string { + if (ms < 1000) { + return `${ms} ms`; + } + const s = ms / 1000; + return s < 60 ? `${s.toFixed(1)} s` : `${Math.floor(s / 60)}m ${Math.round(s % 60)}s`; +} + +/** Plain-language reason for a server error code; null when it has none. */ +export function errorCodeText(code: string | null | undefined): string | null { + switch (code) { + case 'compile_failed': + return 'The submitted file did not compile on the proof server.'; + case 'completed_compile_failed': + return 'The returned proof did not compile.'; + case 'spec_refuted': + return 'A specification was refuted.'; + case 'harness_error': + return 'The proof worker hit an internal error. This is not a problem with your file.'; + case 'worker_terminated': + return 'The worker was stopped before it finished.'; + case 'WORKER_LOST': + return 'The worker stopped responding too many times.'; + case 'QUEUE_TIMEOUT': + return 'No worker became free before the time budget ran out.'; + case 'TIMED_OUT': + return 'The time budget ran out.'; + case 'VERIFIER_UNAVAILABLE': + return 'The independent verifier was unavailable, so the result could not be checked.'; + case 'VERIFIER_ERROR': + return 'The independent verifier failed, so the result could not be checked.'; + default: + return null; + } +} + +function markReached(run: RunModel, step: RunStep, ts: string): void { + run.reached[step] ??= ts; +} + +function markFinished(run: RunModel, step: RunStep, ts: string): void { + markReached(run, step, ts); + run.finished[step] ??= ts; +} + +/** The step and timing side of one event. */ +function applyTiming(run: RunModel, env: EventEnvelope, p: Record): void { + const ts = env.ts; + switch (env.type) { + case 'job.accepted': + markFinished(run, 'submitted', ts); + break; + case 'job.queued': + markFinished(run, 'submitted', ts); + run.deadlineUtc = str(p.deadlineUtc) ?? run.deadlineUtc; + break; + case 'job.provisioning': + case 'vm.booting': + markFinished(run, 'submitted', ts); + markReached(run, 'worker', ts); + break; + case 'vm.online': + markFinished(run, 'submitted', ts); + markFinished(run, 'worker', ts); + break; + case 'job.compiling': + case 'obligations.discovered': + case 'job.proving': + case 'obligation.started': + case 'obligation.attempt': + case 'obligation.proved': + case 'obligation.failed': + case 'obligation.refuted': + case 'agent.activity': + markFinished(run, 'submitted', ts); + markFinished(run, 'worker', ts); + markReached(run, 'proving', ts); + break; + case 'job.verifying': + markFinished(run, 'proving', ts); + markReached(run, 'verifying', ts); + break; + case 'job.completed': + if (run.reached.verifying) { + markFinished(run, 'verifying', ts); + } else if (run.reached.proving) { + markFinished(run, 'proving', ts); + } + run.endedAt = ts; + break; + case 'job.errored': + case 'job.cancelled': + run.endedAt = ts; + break; + } +} + +/** Obligation facts the job DTO does not carry. */ +function applyObligation(run: RunModel, env: EventEnvelope, p: Record): void { + const name = str(p.name); + switch (env.type) { + case 'obligations.discovered': { + const list = Array.isArray(p.obligations) ? p.obligations : []; + for (const item of list) { + const o = asRecord(item); + const oName = str(o.name); + const line = num(o.sourceLine); + if (oName && line !== undefined && line > 0) { + run.sourceLines[oName] = line; + } + } + break; + } + case 'obligation.attempt': { + const attempt = num(p.attempt); + if (name && attempt !== undefined) { + run.attempts[name] = attempt; + } + break; + } + case 'obligation.proved': { + if (name) { + const attempt = num(p.attempt); + // Template proofs say so (`by: "template"`, attempt 0); agent + // proofs carry no `by`. + run.provedBy[name] = p.by === 'template' || attempt === 0 ? 'template' : 'agent'; + if (attempt !== undefined && attempt > 0) { + run.attempts[name] = attempt; + } + } + break; + } + } +} + +/** The activity row for one event, or null when it adds nothing to read. */ +function rowFor(env: EventEnvelope, p: Record): Omit | null { + const name = str(p.name); + const attempt = num(p.attempt); + switch (env.type) { + case 'heartbeat': + case 'usage.tick': + return null; + case 'job.accepted': { + const holes = num(p.holes); + return { + cat: 'step', + text: `Accepted${holes !== undefined ? ` — ${plural(holes, 'proof hole')}` : ''}`, + }; + } + case 'job.queued': + return { cat: 'step', text: 'Waiting for a worker' }; + case 'job.provisioning': { + const n = num(p.attempt); + return { + cat: 'step', + text: n !== undefined && n > 1 + ? `Preparing an isolated worker (attempt ${n})` + : 'Preparing an isolated worker', + }; + } + case 'vm.booting': + return { cat: 'step', text: 'Worker is starting' }; + case 'vm.online': + return { cat: 'step', text: 'Worker ready' }; + case 'job.compiling': + return { cat: 'step', text: 'Checking that the submitted file compiles' }; + case 'obligations.discovered': { + const n = Array.isArray(p.obligations) ? p.obligations.length : undefined; + return { + cat: 'step', + text: n !== undefined ? `Found ${plural(n, 'proof obligation')}` : 'Proof obligations identified', + }; + } + case 'job.proving': { + const holes = num(p.holes); + return { + cat: 'step', + text: holes !== undefined ? `Proving ${plural(holes, 'obligation')}` : 'Proving obligations', + }; + } + case 'obligation.started': + return { cat: 'step', obligation: name, text: 'Started' }; + case 'obligation.attempt': + return { + cat: 'step', + obligation: name, + text: attempt !== undefined ? `Attempt ${attempt}` : 'New attempt', + }; + case 'obligation.proved': { + const duration = num(p.durationMs); + const byTemplate = p.by === 'template' || attempt === 0; + const how = byTemplate ? 'Proved by a built-in template' : 'Proved'; + const extra = [ + !byTemplate && attempt !== undefined ? `attempt ${attempt}` : undefined, + duration !== undefined ? fmtMs(duration) : undefined, + ].filter(Boolean); + return { + cat: 'step', + obligation: name, + text: extra.length ? `${how} (${extra.join(', ')})` : how, + }; + } + case 'obligation.failed': + return { + cat: 'warn', + obligation: name, + text: `Not closed${str(p.error) ? ` — ${str(p.error)}` : ''}`, + }; + case 'obligation.refuted': + return { + cat: 'warn', + obligation: name, + text: 'Refuted — a machine-checked counterexample was accepted', + }; + case 'job.verifying': + return { cat: 'step', text: 'Independently verifying the returned proof' }; + case 'job.completed': + return { cat: 'step', text: 'Run finished' }; + case 'job.cancelling': + return { cat: 'step', text: 'Cancellation requested' }; + case 'job.cancelled': + return { cat: 'step', text: 'Canceled' }; + case 'job.errored': { + const code = str(p.errorCode); + const reason = errorCodeText(code) ?? str(p.errorReason) ?? 'The run ended with an error.'; + return { cat: 'error', text: reason }; + } + case 'integrity.warning': + return { + cat: 'warn', + text: `Integrity warning — ${str(p.detail) ?? str(p.message) ?? 'this run needs review'}`, + }; + case 'agent.limited': { + const code = str(p.code); + return { + cat: 'warn', + text: (code && AGENT_LIMIT_MESSAGES[code]) ?? 'A generation limit was reported.', + }; + } + case 'agent.activity': { + const theorem = str(p.theorem); + return { + cat: 'agent', + obligation: theorem, + attempt, + text: summarizeActivity(p), + }; + } + case 'setup.progress': + case 'log': { + const message = str(p.message) ?? str(p.step); + return message ? { cat: 'detail', text: message } : null; + } + default: { + const summary = summarize(env); + return { cat: 'detail', text: summary ? `${env.type} — ${summary}` : env.type }; + } + } +} + +/** + * Apply one event. Events at or below the cursor are replays (the stream and + * the poll fallback overlap) and change nothing. Returns whether the event was + * new and the activity row it added, if any. + */ +export function applyEvent( + run: RunModel, + env: EventEnvelope, +): { applied: boolean; row: ActivityRow | null } { + if (typeof env.seq === 'number') { + if (env.seq <= run.lastSeq) { + return { applied: false, row: null }; + } + run.lastSeq = env.seq; + } + const p = asRecord(env.payload); + if (typeof env.ts === 'string' && !Number.isNaN(Date.parse(env.ts))) { + run.lastSignalAt = env.ts; + applyTiming(run, env, p); + } + applyObligation(run, env, p); + if (env.type === 'integrity.warning') { + run.integrityWarnings.push(str(p.detail) ?? str(p.message) ?? 'This run needs review.'); + } + const partial = rowFor(env, p); + if (!partial) { + return { applied: true, row: null }; + } + const row: ActivityRow = { + seq: typeof env.seq === 'number' ? env.seq : run.lastSeq, + ts: env.ts, + ...partial, + text: partial.text.length > 600 ? `${partial.text.slice(0, 600)}…` : partial.text, + }; + if (!row.obligation) { + delete row.obligation; + } + if (row.attempt === undefined) { + delete row.attempt; + } + run.rows.push(row); + if (run.rows.length > EVENT_LOG_CAP) { + run.rows.splice(0, run.rows.length - EVENT_LOG_CAP); + } + return { applied: true, row }; +} + +/** Whether an event can change what the panel shows above the activity list. */ +export function changesSummary(type: string): boolean { + return type !== 'agent.activity' && type !== 'heartbeat' && type !== 'usage.tick' && type !== 'log'; +} diff --git a/editors/vscode/src/prover/submission.ts b/editors/vscode/src/prover/submission.ts index c1abba97..6222e51c 100644 --- a/editors/vscode/src/prover/submission.ts +++ b/editors/vscode/src/prover/submission.ts @@ -91,7 +91,7 @@ export function generatedVPath(stdout: string, cwd: string): string | null { } export type SubmitOutcome = - | { kind: 'submitted'; job: JobResponse; holes: number } + | { kind: 'submitted'; job: JobResponse; holes: number; sha256: string } | { kind: 'preflight-failed'; problem: string }; /** Preflight, then submit with the content-derived key. API errors propagate. */ @@ -107,5 +107,6 @@ export async function submitVFile( } // No options: the server picks provider, agent and budget. const job = await api.submitJob(filename, bytes, {}, idempotencyKey(checked.text)); - return { kind: 'submitted', job, holes: checked.holes }; + const sha256 = crypto.createHash('sha256').update(bytes).digest('hex'); + return { kind: 'submitted', job, holes: checked.holes, sha256 }; } diff --git a/editors/vscode/src/prover/submitProof.ts b/editors/vscode/src/prover/submitProof.ts index c96fdc78..4250cecc 100644 --- a/editors/vscode/src/prover/submitProof.ts +++ b/editors/vscode/src/prover/submitProof.ts @@ -3,13 +3,14 @@ import * as vscode from 'vscode'; import { ApiError, AuthError, ProverApi } from './api'; import { describeError, requireConfig, type ProverConfig } from './config'; +import type { JobOrigin } from './jobOrigins'; import { DEFAULT_MAX_UPLOAD_BYTES, submitVFile } from './submission'; import type { JobResponse } from './types'; /** What a finished submission hands to the views. */ export interface SubmitHooks { /** Refresh the jobs view, reveal the job and open its panel. */ - showJob(job: JobResponse, source?: string): Promise; + showJob(job: JobResponse, origin?: JobOrigin): Promise; } const UPLOAD_NOTICE_KEY = 'inference.prover.uploadNotice'; @@ -139,7 +140,7 @@ export function registerSubmitProofCommand( return; } log.info(`Prover: submitted ${filename} (${outcome.holes} holes) → job ${outcome.job.id}`); - await hooks.showJob(outcome.job); + await hooks.showJob(outcome.job, { vPath: uri.fsPath, vSha256: outcome.sha256 }); } catch (err) { log.error(`Prover: submit ${filename}: ${err instanceof Error ? err.message : err}`); vscode.window.showErrorMessage(`Inference: ${submitErrorMessage(err)}`); diff --git a/editors/vscode/src/prover/types.ts b/editors/vscode/src/prover/types.ts index 34416b9e..2c1cc424 100644 --- a/editors/vscode/src/prover/types.ts +++ b/editors/vscode/src/prover/types.ts @@ -102,6 +102,8 @@ export interface ObligationDto { lastError?: string | null; /** Goal state Rocq shows at this theorem's `Proof.` (compile-goals flow). */ goal?: string | null; + /** 1-based line of the theorem in the submitted `.v`; absent on older servers. */ + sourceLine?: number | null; } /** @@ -139,6 +141,11 @@ export interface JobResponse { claimClass?: ClaimClass | null; errorCode?: string | null; errorReason?: string | null; + /** + * When the time budget ends (submission + budget; queue time counts). + * Absent on older servers: `job.queued` carries it, or derive it. + */ + deadlineUtc?: string | null; } /** Paged list response for `GET /api/v1/jobs`. */ diff --git a/editors/vscode/src/prover/verifierEvidence.ts b/editors/vscode/src/prover/verifierEvidence.ts new file mode 100644 index 00000000..b56b0585 --- /dev/null +++ b/editors/vscode/src/prover/verifierEvidence.ts @@ -0,0 +1,102 @@ +/** + * Fail-closed checks over the independent verifier's evidence. Pure — no + * `vscode` import. A positive claim needs every check here to pass; the + * wording built on top of them lives in ./jobVerdict.ts. + */ + +import type { AssumptionReport, JobResponse, JobResultResponse } from './types'; + +/** The verifier's outcome, lowercased; null when the verifier did not report. */ +export function normalizedVerifierOutcome( + result: JobResultResponse | null | undefined, +): string | null { + const value = result?.verificationOutcome?.trim().toLowerCase(); + return value || null; +} + +/** Well-formed per-target reports, or null when any is malformed. */ +export function normalizedAssumptionReports( + result: JobResultResponse, +): AssumptionReport[] | null { + const reports = result.assumptionReports; + if (!Array.isArray(reports)) return null; + for (const report of reports) { + if (!report || typeof report.target !== 'string' || !report.target || + typeof report.kernelOutput !== 'string' || !report.kernelOutput || + typeof report.policyPassed !== 'boolean' || + !Array.isArray(report.assumptions)) { + return null; + } + for (const assumption of report.assumptions) { + if (!assumption || typeof assumption.name !== 'string' || !assumption.name || + typeof assumption.type !== 'string' || !assumption.type || + (assumption.kind !== 'axiom' && assumption.kind !== 'sectionVariable')) { + return null; + } + } + } + return reports; +} + +/** One passing report per closed target, and only for the expected targets. */ +export function hasCompleteAssumptionEvidence( + result: JobResultResponse, + expectedTargets: string[], +): boolean { + const reports = normalizedAssumptionReports(result); + if (!result.assumptionPolicyId?.trim() || !reports) return false; + const names = new Set(reports.map((report) => report.target)); + const expected = new Set(expectedTargets); + return reports.length === result.holesClosed + && names.size === reports.length + && expected.size === expectedTargets.length + && expected.size === result.holesClosed + && reports.every((report) => expected.has(report.target)) + && reports.every((report) => report.policyPassed); +} + +export function verifierAcceptedFull( + result: JobResultResponse, + expectedTargets: string[], +): boolean { + return ( + normalizedVerifierOutcome(result) === 'succeeded' && + result.compileOk === true && + result.assumptionsClosed === true && + result.verifiedClean === true && + result.admitsDetected === false && + result.statementsImmutable === true && + result.markersRemaining === 0 && + hasCompleteAssumptionEvidence(result, expectedTargets) + ); +} + +export function verifierAcceptedPartial( + result: JobResultResponse, + expectedTargets: string[], +): boolean { + // Partial verification intentionally leaves the unfilled obligations + // admitted, so verifiedClean=false/admitsDetected=true are expected here. + return ( + normalizedVerifierOutcome(result) === 'partial' && + result.compileOk === true && + result.assumptionsClosed === true && + result.verifiedClean === false && + result.admitsDetected === true && + result.statementsImmutable === true && + result.markersRemaining === 0 && + hasCompleteAssumptionEvidence(result, expectedTargets) + ); +} + +/** The job detail and its result describe the same run. */ +export function resultMatchesJob(job: JobResponse, result: JobResultResponse): boolean { + return ( + result.id === job.id && + result.status === job.status && + result.mode === job.mode && + result.holesTotal === job.holesTotal && + result.holesClosed === job.holesClosed && + result.claimClass === job.claimClass + ); +} diff --git a/editors/vscode/src/prover/webviewIcons.ts b/editors/vscode/src/prover/webviewIcons.ts new file mode 100644 index 00000000..01eda536 --- /dev/null +++ b/editors/vscode/src/prover/webviewIcons.ts @@ -0,0 +1,40 @@ +/** + * Small 16px line icons for the job panel, drawn in the style of VS Code's + * codicons. Inline SVG in `currentColor`: no packaged font, no CSP change, + * and every icon follows the theme. Always decorative (`aria-hidden`) — + * meaning is carried by adjacent text. + */ + +const PATHS = { + pass: '', + error: '', + warning: '', + refuted: '', + running: '', + loading: '', + waiting: '', + verifying: '', + canceled: '', + todo: '', + dot: '', + chevron: '', + linkExternal: '', + file: '', + diff: '', + copy: '', + stop: '', + refresh: '', + search: '', + download: '', + rerun: '', + goto: '', + log: '', +} as const; + +export type IconName = keyof typeof PATHS; + +/** An inline, decorative icon. */ +export function icon(name: IconName, extraClass = ''): string { + const cls = extraClass ? `icon ${extraClass}` : 'icon'; + return ``; +} diff --git a/editors/vscode/src/test/prover-build-log.test.ts b/editors/vscode/src/test/prover-build-log.test.ts new file mode 100644 index 00000000..45104b7b --- /dev/null +++ b/editors/vscode/src/test/prover-build-log.test.ts @@ -0,0 +1,67 @@ +import * as assert from 'node:assert'; +import { describe, it } from 'node:test'; + +import { duplicateNameHint, fileStem, firstBuildError } from '../prover/buildLog'; +import { pruneOrigins } from '../prover/jobOrigins'; + +describe('firstBuildError', () => { + it('reads the located error Rocq prints (real server build.log)', () => { + const log = 'File "/work/compiled.v", line 53, characters 11-16:\nError: clamp already exists.\n\n'; + assert.deepStrictEqual(firstBuildError(log), { + line: 53, startChar: 11, endChar: 16, message: 'clamp already exists.', + }); + }); + + it('keeps a multi-line message and stops at the next location', () => { + const log = [ + 'File "/work/compiled.v", line 9, characters 2-10:', + 'Error:', + 'In environment', + 'x : nat', + 'File "/work/compiled.v", line 12, characters 0-1:', + 'Error: later', + ].join('\n'); + const error = firstBuildError(log); + assert.strictEqual(error?.line, 9); + assert.strictEqual(error?.message, 'In environment\nx : nat'); + }); + + it('skips located warnings before the error', () => { + const log = [ + 'File "/work/compiled.v", line 3, characters 0-20:', + 'Warning: Notation "_ + _" was already used. [notation-overridden,parsing,default]', + '', + 'File "/work/compiled.v", line 53, characters 11-16:', + 'Error: clamp already exists.', + '', + ].join('\n'); + assert.deepStrictEqual(firstBuildError(log), { line: 53, startChar: 11, endChar: 16, message: 'clamp already exists.' }); + assert.strictEqual(firstBuildError(log.split('\n').slice(0, 3).join('\n')), null); + }); + + it('falls back to an unlocated Error block, and to null', () => { + assert.deepStrictEqual(firstBuildError('noise\nError: Cannot find library Foo.\n'), { message: 'Cannot find library Foo.' }); + assert.strictEqual(firstBuildError('all good\n'), null); + }); +}); + +describe('duplicateNameHint', () => { + it('explains the module-named-after-the-file clash', () => { + assert.ok(duplicateNameHint('clamp already exists.', ['clamp'])?.includes('names the module after the file')); + assert.ok(duplicateNameHint('foo already exists.', ['clamp'])?.includes('defined twice')); + assert.strictEqual(duplicateNameHint('Syntax error', ['clamp']), null); + }); + + it('takes stems from paths and names', () => { + assert.strictEqual(fileStem('/a/b/clamp.inf'), 'clamp'); + assert.strictEqual(fileStem('clamp.v'), 'clamp'); + assert.strictEqual(fileStem(null), null); + }); +}); + +describe('pruneOrigins', () => { + it('keeps the newest entries', () => { + const kept = pruneOrigins({ a: { at: 1 }, b: { at: 3 }, c: { at: 2 } }, 2); + assert.deepStrictEqual(Object.keys(kept).sort(), ['b', 'c']); + }); +}); diff --git a/editors/vscode/src/test/prover-job-detail-actions.test.ts b/editors/vscode/src/test/prover-job-detail-actions.test.ts index fd650c85..1a827473 100644 --- a/editors/vscode/src/test/prover-job-detail-actions.test.ts +++ b/editors/vscode/src/test/prover-job-detail-actions.test.ts @@ -1,10 +1,12 @@ import * as assert from 'node:assert'; import { describe, it } from 'node:test'; -import { EVENT_LOG_CAP, phaseRibbon, renderJobDetailHtml, type RenderOptions } from '../prover/jobDetailHtml'; -import type { JobResponse, JobResultResponse } from '../prover/types'; +import { buildJobView } from '../prover/jobDetailModel'; +import { EVENT_LOG_CAP, renderJobDetailHtml, type RenderOptions } from '../prover/jobDetailHtml'; +import { applyEvent, newRunModel } from '../prover/runModel'; +import type { EventEnvelope, JobResponse, JobResultResponse } from '../prover/types'; -const OPTS: RenderOptions = { nonce: 'n', cspSource: 'csp', live: 'terminal', eventLog: [], canCancel: false }; +const OPTS: RenderOptions = { nonce: 'n', cspSource: 'csp', live: 'terminal' }; const JOB: JobResponse = { id: 'job-1', status: 'Succeeded', filename: 'm.v', createdAt: '2026-10-07T00:00:00Z', maxWallClockSeconds: 900, holesTotal: 1, holesClosed: 1, mode: 'prove', claimClass: 'Verified', @@ -15,53 +17,120 @@ const RESULT = (kinds: string[]): JobResultResponse => ({ id: 'job-1', status: 'Succeeded', holesTotal: 1, holesClosed: 1, artifacts: kinds.map((k, i) => artifact(`a${i}`, k)), }); +const event = (seq: number, type: string, payload: unknown = {}): EventEnvelope => ({ + schemaVersion: 1, jobId: 'job-1', seq, type, ts: `2026-10-07T00:00:${String(seq).padStart(2, '0')}Z`, payload, +}); -describe('phaseRibbon', () => { +describe('run steps', () => { it('marks a live job done/active/todo', () => { - assert.deepStrictEqual(phaseRibbon('Running', false).map((c) => c.state), - ['done', 'done', 'done', 'done', 'active', 'todo', 'todo']); + const view = buildJobView({ job: { ...JOB, status: 'Running' }, live: 'sse' }); + assert.deepStrictEqual(view.steps.map((s) => [s.key, s.state]), [ + ['submitted', 'done'], ['worker', 'done'], ['proving', 'active'], ['verifying', 'todo'], ['result', 'todo'], + ]); + }); + + it('does not claim steps a finished job never reached', () => { + const view = buildJobView({ job: { ...JOB, status: 'ProvisionFailed' }, live: 'terminal' }); + assert.deepStrictEqual(view.steps.map((s) => s.state), ['done', 'unknown', 'unknown', 'unknown', 'final']); + assert.deepStrictEqual(view.steps.at(-1), { key: 'result', label: "Couldn't start", state: 'final', tone: 'err' }); }); - it('does not claim phases a finished job may never have reached', () => { - const chips = phaseRibbon('ProvisionFailed', false); - assert.ok(chips.slice(0, -1).every((c) => c.state === 'past')); - assert.deepStrictEqual(chips.at(-1), { name: 'ProvisionFailed', state: 'err' }); - assert.deepStrictEqual(phaseRibbon('Succeeded', true).at(-1), { name: 'Succeeded', state: 'ok' }); - assert.deepStrictEqual(phaseRibbon('Succeeded', false).at(-1), { name: 'Succeeded', state: 'warn' }); + it('marks the steps the event history shows', () => { + const run = newRunModel(); + for (const [seq, type] of [[1, 'job.accepted'], [2, 'vm.online'], [3, 'job.compiling'], [4, 'job.verifying'], [5, 'job.completed']] as const) { + applyEvent(run, event(seq, type)); + } + const view = buildJobView({ job: JOB, run, live: 'terminal' }); + assert.deepStrictEqual(view.steps.map((s) => s.state), ['done', 'done', 'done', 'done', 'final']); + assert.strictEqual(view.clock.end, '2026-10-07T00:00:05Z'); }); }); -describe('job detail actions', () => { +describe('job panel actions', () => { it('offers open/compare/certificate for a completed proof', () => { const html = renderJobDetailHtml(JOB, { ...OPTS, result: RESULT(['InputV', 'CompletedV', 'BuildLog']) }); - assert.ok(html.includes('Open completed proof')); - assert.ok(html.includes('id="compare"')); - assert.ok(html.includes('Open certificate in portal')); - // Every text artifact can open read-only; binary ones only download. - assert.strictEqual(html.match(/class="open-artifact"/g)?.length, 4); + assert.ok(html.includes('Open proof')); + assert.ok(html.includes('data-action="compare"')); + assert.ok(html.includes('aria-label="Open the certificate in the portal"')); + // Every text artifact opens read-only (3 files + the proof button). + assert.strictEqual(html.match(/data-action="openArtifact"/g)?.length, 4); }); - it('offers the refutation and no comparison when there is no completed proof', () => { - const html = renderJobDetailHtml({ ...JOB, status: 'Failed' }, { ...OPTS, result: RESULT(['InputV', 'RefutationV']) }); + it('offers the refutation and the portal page when there is no completed proof', () => { + const html = renderJobDetailHtml( + { ...JOB, status: 'Failed', errorCode: 'spec_refuted' }, + { ...OPTS, result: RESULT(['InputV', 'RefutationV']) }, + ); assert.ok(html.includes('Open refutation')); - assert.ok(!html.includes('id="compare"')); + assert.ok(html.includes('Specification refuted')); + assert.ok(!html.includes('data-action="compare"')); + assert.ok(html.includes('data-action="openPortal"')); + assert.ok(!html.includes('data-action="openCertificate"')); }); - it('styles a refuted obligation as a failure', () => { - assert.ok(renderJobDetailHtml(JOB, OPTS).includes('refuted')); + it('styles a refuted obligation distinctly', () => { + const html = renderJobDetailHtml(JOB, OPTS); + assert.ok(html.includes('class="obl tone-refuted"')); + assert.ok(html.includes('data-status="refuted"')); + assert.ok(html.includes('>Refuted')); }); it('shows the time budget, deadline and source, escaped', () => { const html = renderJobDetailHtml(JOB, { ...OPTS, source: '.inf' }); - assert.ok(html.includes('15m')); - assert.ok(/Deadline/.test(html)); + assert.ok(html.includes('data-field="budget">15m')); + assert.ok(html.includes('data-field="deadline"')); assert.ok(html.includes('<x>.inf')); + assert.ok(html.includes('Uploaded as m.v')); + }); + + it('prefers the deadline the server or the event history gives', () => { + const fromJob = buildJobView({ job: { ...JOB, deadlineUtc: '2026-10-07T01:00:00Z' }, live: 'terminal' }); + assert.strictEqual(fromJob.clock.deadline, '2026-10-07T01:00:00Z'); + const run = newRunModel(); + applyEvent(run, event(1, 'job.queued', { deadlineUtc: '2026-10-07T02:00:00Z' })); + assert.strictEqual(buildJobView({ job: JOB, run, live: 'terminal' }).clock.deadline, '2026-10-07T02:00:00Z'); + assert.strictEqual(buildJobView({ job: JOB, live: 'terminal' }).clock.deadline, '2026-10-07T00:15:00.000Z'); + }); + + it('links an open obligation to its theorem in the submitted file, with the reported line as fallback', () => { + const run = newRunModel(); + applyEvent(run, event(1, 'obligations.discovered', { obligations: [{ name: 't', sourceLine: 98 }] })); + const [fromEvents] = buildJobView({ job: JOB, run, live: 'terminal' }).obligations ?? []; + assert.deepStrictEqual(fromEvents.goto, { target: 'source', line: 98 }); + const html = renderJobDetailHtml(JOB, { ...OPTS, run }); + assert.ok(html.includes('data-action="gotoTheorem" data-obligation="t" data-line="98"')); + assert.ok(html.includes('Go to theorem')); + assert.ok(!html.includes('Go to line')); + const [unknown] = buildJobView({ job: JOB, live: 'terminal' }).obligations ?? []; + assert.deepStrictEqual(unknown.goto, { target: 'source' }); + }); + + it('titles the closed group like its rows, never "Proved" without a claim', () => { + const obligations = Array.from({ length: 11 }, (_, i) => ({ name: `t${i}`, kind: 'spec' as const, status: 'proved' as const })); + const unverified = renderJobDetailHtml({ ...JOB, holesTotal: 11, holesClosed: 11, obligations }, { ...OPTS, resultState: 'failed' }); + assert.ok(unverified.includes('Closed — not verified (11)')); + assert.ok(!unverified.includes('Proved (11)')); + const running = renderJobDetailHtml({ ...JOB, status: 'Running', holesTotal: 12, holesClosed: 11, obligations }, { ...OPTS, live: 'sse' }); + assert.ok(running.includes('Closed (11)')); + }); + + it('links a proved obligation to its proof in the returned file', () => { + const job: JobResponse = { ...JOB, obligations: [{ name: 't', kind: 'spec', status: 'proved', sourceLine: 7 }] }; + const result = RESULT(['InputV', 'CompletedV']); + const [proved] = buildJobView({ job, result, live: 'terminal' }).obligations ?? []; + assert.deepStrictEqual(proved.goto, { target: 'proof', artifact: 'a1' }); + const html = renderJobDetailHtml(job, { ...OPTS, result }); + assert.ok(html.includes('data-action="gotoTheorem" data-obligation="t" data-artifact="a1"')); + assert.ok(html.includes('Go to proof')); + // Without a returned file it points at the submitted one. + const [noProof] = buildJobView({ job, result: RESULT(['InputV']), live: 'terminal' }).obligations ?? []; + assert.deepStrictEqual(noProof.goto, { target: 'source', line: 7 }); }); - it('keeps one nonce-bound script and the larger log cap', () => { + it('keeps one nonce-bound script and the activity cap', () => { const html = renderJobDetailHtml(JOB, { ...OPTS, result: RESULT(['CompletedV']) }); assert.strictEqual(html.match(/]/g)?.length, 1); - assert.ok(html.includes(`MAX_LOG_NODES = ${EVENT_LOG_CAP}`)); + assert.ok(html.includes(`const CAP = ${EVENT_LOG_CAP};`)); assert.strictEqual(EVENT_LOG_CAP, 2000); }); }); diff --git a/editors/vscode/src/test/prover-job-detail-html.test.ts b/editors/vscode/src/test/prover-job-detail-html.test.ts index da58c2f3..96ab1391 100644 --- a/editors/vscode/src/test/prover-job-detail-html.test.ts +++ b/editors/vscode/src/test/prover-job-detail-html.test.ts @@ -9,6 +9,8 @@ import { renderJobDetailHtml, type RenderOptions, } from '../prover/jobDetailHtml'; +import { JOB_DETAIL_STYLES } from '../prover/jobDetailStyles'; +import { applyEvent, newRunModel } from '../prover/runModel'; import type { JobResponse, JobResultResponse, @@ -20,8 +22,6 @@ const BASE_OPTS: RenderOptions = { cspSource: 'vscode-webview://test-source', error: null, live: 'terminal', - eventLog: [], - canCancel: false, }; const JOB: JobResponse = { @@ -117,6 +117,21 @@ const RESULT: JobResultResponse = { ], }; +/** The verdict the panel shows (`#verdict` data attributes). */ +function verdictOf(html: string): { kind: string; tone: string; claim: string } { + const m = /id="verdict" data-verdict="([^"]+)" data-tone="([^"]+)" data-claim="([^"]+)"/.exec(html); + assert.ok(m, 'the panel renders a verdict'); + return { kind: m[1], tone: m[2], claim: m[3] }; +} + +/** No positive claim and no success tone. */ +function assertNoProofClaim(html: string, message?: string): void { + const v = verdictOf(html); + assert.notStrictEqual(v.tone, 'ok', message); + assert.strictEqual(v.claim, 'none', message); + assert.ok(!html.includes('data-verdict="verified"'), message); +} + describe('escapeHtml', () => { it('escapes all five HTML metacharacters', () => { assert.strictEqual( @@ -204,46 +219,48 @@ describe('isCancelableStatus', () => { }); describe('renderJobDetailHtml', () => { - it('renders the core job facts', () => { + it('renders the core job facts in plain words, raw values only under Technical details', () => { const html = renderJobDetailHtml(JOB, BASE_OPTS); assert.ok(html.includes('fixture-stdlib.v')); - assert.ok(html.includes('Succeeded')); - assert.ok(!html.includes('Succeeded')); - assert.ok(html.includes('Certificate evidence unavailable')); - assert.ok( - html.includes( - '
    Mode
    prove
    ', - ), - ); - assert.ok(html.includes('2/2 closed')); - assert.ok(html.includes('valid_fixture__Add')); - assert.ok(html.includes('valid_fixture__Comm')); - assert.ok(html.includes('Content')); - assert.ok(html.includes('grounded')); - assert.ok(html.includes('Claim class')); - assert.ok(html.includes('Verified')); - assert.ok(html.includes('4200 ms') || html.includes('4.2 s')); + assert.ok(html.includes('data-field="mode">prove')); + assert.ok(html.includes('data-field="claimClass">Verified')); + assert.ok(html.includes('data-field="status">Succeeded')); + assert.ok(html.includes('aria-valuenow="2"')); + assert.ok(html.includes('aria-valuemax="2"')); + assert.ok(html.includes('2 of 2 obligations closed')); + // Short names in the list, full theorem names in the details. + assert.ok(html.includes('>Add')); + assert.ok(html.includes('valid_fixture__Comm')); + assert.ok(html.includes('>behavior')); + assert.ok(html.includes('States a behavioral property of the compiled module')); + assert.ok(html.includes('4.2 s')); assert.ok(html.includes('1m 1s')); }); + it('makes no claim while the verifier verdict is loading, and says so when it failed', () => { + const loading = renderJobDetailHtml(JOB, BASE_OPTS); + assertNoProofClaim(loading); + assert.strictEqual(verdictOf(loading).kind, 'loading'); + + const failed = renderJobDetailHtml(JOB, { ...BASE_OPTS, resultState: 'failed' }); + assertNoProofClaim(failed); + assert.ok(failed.includes('Verifier evidence unavailable')); + }); + it('fails closed for Succeeded records without durable prove mode', () => { for (const mode of [ undefined, null, 'unknown', - 'compile-goals', ] satisfies Array) { - const html = renderJobDetailHtml({ ...JOB, mode }, BASE_OPTS); - assert.ok( - html.includes('Succeeded'), - `mode ${String(mode)} should be warning`, - ); - assert.ok( - !html.includes('Succeeded'), - `mode ${String(mode)} must not be green`, - ); - assert.ok(html.includes('Not proven.')); + const html = renderJobDetailHtml({ ...JOB, mode }, { ...BASE_OPTS, result: { ...RESULT, mode } }); + assertNoProofClaim(html, `mode ${String(mode)} must not be a proof`); + assert.strictEqual(verdictOf(html).tone, 'warn'); + assert.ok(html.includes('was not recorded as a proof run')); } + const compileGoals = renderJobDetailHtml({ ...JOB, mode: 'compile-goals' }, BASE_OPTS); + assertNoProofClaim(compileGoals); + assert.strictEqual(verdictOf(compileGoals).kind, 'compile-only'); }); it('fails closed when job and result proof modes disagree', () => { @@ -251,10 +268,9 @@ describe('renderJobDetailHtml', () => { ...BASE_OPTS, result: { ...RESULT, mode: 'compile-goals' }, }); - assert.ok(html.includes('Succeeded')); - assert.ok(!html.includes('Succeeded')); - assert.ok(html.includes('Not proven.')); - assert.ok(html.includes('Job detail and result DTOs do not agree')); + assertNoProofClaim(html); + assert.strictEqual(verdictOf(html).kind, 'conflict'); + assert.ok(html.includes('The job record and its result disagree')); }); it('fails closed when Succeeded proof counts are incomplete', () => { @@ -262,9 +278,8 @@ describe('renderJobDetailHtml', () => { { ...JOB, holesTotal: 2, holesClosed: 1 }, BASE_OPTS, ); - assert.ok(html.includes('Succeeded')); - assert.ok(!html.includes('Succeeded')); - assert.ok(html.includes('every hole closed')); + assertNoProofClaim(html); + assert.ok(html.includes('does not show every proof hole closed')); }); it('fails closed when job and result proof counts disagree', () => { @@ -272,9 +287,8 @@ describe('renderJobDetailHtml', () => { ...BASE_OPTS, result: { ...RESULT, holesClosed: 1 }, }); - assert.ok(html.includes('Succeeded')); - assert.ok(!html.includes('Succeeded')); - assert.ok(html.includes('Job detail and result DTOs do not agree')); + assertNoProofClaim(html); + assert.strictEqual(verdictOf(html).kind, 'conflict'); }); it('fails closed when independent verifier flags reject Succeeded', () => { @@ -282,9 +296,10 @@ describe('renderJobDetailHtml', () => { ...BASE_OPTS, result: { ...RESULT, verifiedClean: false, admitsDetected: true }, }); - assert.ok(html.includes('Succeeded')); - assert.ok(!html.includes('Succeeded')); - assert.ok(html.includes('independent verifier evidence rejects')); + assertNoProofClaim(html); + assert.deepStrictEqual(verdictOf(html), { kind: 'rejected', tone: 'err', claim: 'none' }); + assert.ok(html.includes('Independent verification failed')); + assert.ok(html.includes('Some proofs are incomplete (still admitted).')); }); it('fails closed when a target fails the assumption policy', () => { @@ -298,10 +313,11 @@ describe('renderJobDetailHtml', () => { index === 0 ? { ...report, policyPassed: false } : report), }, }); - assert.ok(!html.includes('Succeeded')); - assert.ok(html.includes('independent verifier evidence rejects')); - assert.ok(html.includes('Assumption policy passed')); + assertNoProofClaim(html); + assert.strictEqual(verdictOf(html).kind, 'rejected'); + assert.ok(html.includes('Only approved assumptions are used')); assert.ok(html.includes('policy rejected')); + assert.ok(html.includes('relies on assumptions the policy does not allow')); }); it('fails closed when verifier outcome disagrees with Succeeded', () => { @@ -314,12 +330,12 @@ describe('renderJobDetailHtml', () => { admitsDetected: true, }, }); - assert.ok(html.includes('Succeeded')); - assert.ok(!html.includes('Succeeded')); - assert.ok(html.includes('independent verifier evidence rejects')); + assertNoProofClaim(html); + assert.strictEqual(verdictOf(html).kind, 'rejected'); + assert.ok(html.includes('outcome is “partial”, not “succeeded”')); }); - it('renders CompileGoals as a terminal warning, never a green success', () => { + it('renders CompileGoals as compiled-only, never a success', () => { const mode: RunMode = 'compile-goals'; const compileGoals: JobResponse = { ...JOB, @@ -332,15 +348,11 @@ describe('renderJobDetailHtml', () => { const html = renderJobDetailHtml(compileGoals, BASE_OPTS); assert.ok(isTerminalStatus(compileGoals.status)); assert.ok(isStreamTerminalStatus(compileGoals.status)); - assert.ok(html.includes('CompileGoals')); - assert.ok(!html.includes('CompileGoals')); - assert.ok( - html.includes( - '
    Mode
    compile-goals
    ', - ), - ); - assert.ok(html.includes('Compile-only result.')); - assert.ok(html.includes('no proof was accepted or returned')); + assertNoProofClaim(html); + assert.deepStrictEqual(verdictOf(html), { kind: 'compile-only', tone: 'warn', claim: 'none' }); + assert.ok(html.includes('data-field="mode">compile-goals')); + assert.ok(html.includes('Compiled — nothing was proved')); + assert.ok(html.includes('No proof was accepted or returned.')); const failedCompile = renderJobDetailHtml( { @@ -351,7 +363,8 @@ describe('renderJobDetailHtml', () => { }, BASE_OPTS, ); - assert.ok(failedCompile.includes('Compile-only run.')); + assertNoProofClaim(failedCompile); + assert.ok(failedCompile.includes('This was a compile-only run')); assert.ok(!failedCompile.includes('The file compiled')); }); @@ -383,14 +396,9 @@ describe('renderJobDetailHtml', () => { ...BASE_OPTS, result: compileResult, }); - assert.ok(html.includes('

    Verification

    ')); - assert.ok( - html.includes( - 'No independent verifier provenance is available; this is a worker-reported legacy result.', - ), - ); - assert.ok(!html.includes('Independent verifier verdict')); - assert.ok(!html.includes('Verified clean (compiles, no admits)')); + assert.ok(html.includes('How this was verified')); + assert.ok(html.includes('Not applicable — this run only compiled the file.')); + assert.ok(!html.includes('class="checks"')); }); it('renders the per-obligation goal state', () => { @@ -400,7 +408,7 @@ describe('renderJobDetailHtml', () => { assert.ok(html.includes('pre class="goal"')); }); - it('fails closed to unknown when legacy obligation content is missing', () => { + it('fails closed to "not classified" when legacy obligation content is missing', () => { const html = renderJobDetailHtml( { ...JOB, @@ -409,7 +417,7 @@ describe('renderJobDetailHtml', () => { BASE_OPTS, ); assert.ok(html.includes('legacy_obligation')); - assert.ok(html.includes('unknown')); + assert.ok(html.includes('Not classified')); }); it('escapes goal text (server-originated)', () => { @@ -437,15 +445,15 @@ describe('renderJobDetailHtml', () => { assert.ok(!html.includes('claude-code')); assert.ok(!html.includes('kubernetes')); assert.ok(!/>\s*Provider\s*\s*Agent\s* { const hostile: JobResponse = { ...JOB, + status: 'Failed', filename: '.v', errorCode: 'Xsteal()', @@ -463,15 +471,19 @@ describe('renderJobDetailHtml', () => { assert.ok(!html.includes('steal')); assert.ok(!html.includes('valid_')); + assert.ok(!html.includes('X { - const html = renderJobDetailHtml(JOB, { - ...BASE_OPTS, - eventLog: ['12:00:00 log — '], + it('escapes activity rows', () => { + const run = newRunModel(); + applyEvent(run, { + schemaVersion: 1, jobId: JOB.id, seq: 1, type: 'log', ts: '2026-06-05T10:00:01Z', + payload: { message: '' }, }); + const html = renderJobDetailHtml(JOB, { ...BASE_OPTS, run }); assert.ok(!html.includes('`; + return html + .replace('\n