qemu-model-verification

어떤 스킬인가요?

Use when existing qtest, trace, log, replay, boot, or workload evidence must be evaluated against one falsifiable QEMU device, board, TCG, or runtime claim as PASS, FAIL, or INCONCLUSIVE.

설치 방법

프로젝트 폴더에서 아래 명령어를 실행하고, 설치할 에이전트를 선택하세요.

설치 명령을 직접 실행해야 적용됩니다. 지원 에이전트와 필요한 권한·라이선스는 제작자의 안내를 확인하세요.

스킬 원문 파일

interface:
  display_name: "QEMU Model Verification"
  short_description: "Classify QEMU model evidence with explicit results."
  default_prompt: "Use $qemu-model-verification to test this QEMU model claim and classify it as PASS, FAIL, or INCONCLUSIVE."

# Claim record: <claim-id>

One claim per record. Copy it into `.oh-my-qemu/<task-slug>/audit.md` or keep
one file per claim under `output/`. Fill every placeholder before reporting a
verdict and keep the record so later rounds can re-derive it.

## Claim and gate

- Claim: <one falsifiable sentence>
- Gate: <exact command or evidence-localization method>
- Acceptance criteria: <observable condition that makes the claim PASS>
- Disconfirming evidence: <what would make it FAIL>

## Expected values and provenance

| Expected value | Meaning | Source (file:line, manual page/section, test) | Revision/date |
|---|---|---|---|
| <marker or value> | <what it proves> | <source> | <revision> |

- Re-derived when the test, image, or model changed: <yes/no and how>
- Stale literals removed: <list or none>
- User-supplied premise verified against the manual: <yes/no, page/section>

## Inputs and hashes

| Input | Path | sha256 or build ID |
|---|---|---|
| QEMU binary | `builds/build-<target>/qemu-system-<arch>` | <sha256> |
| Build directory | `builds/build-<target>/` | <configure line> |
| Image / firmware | <path> | <sha256> |
| DTB, if any | <path> | <sha256> |
| Machine options | `-M <machine> ...` | n/a |

- Required device-tree properties verified: <msi-parent/ITS, controllers,
  clocks, none>
- Environment: <host, accelerator, tool versions that affect the verdict>

## Evidence

| Artifact | Path | Decisive lines or summary |
|---|---|---|
| Log | `.oh-my-qemu/<task-slug>/logs/<file>` | <lines> |
| Trace | <path> | <counts/summary> |
| Replay | <path> | <mode/icount> |

## Verdict

- Verdict: PASS | FAIL | INCONCLUSIVE
- Gate that produced the verdict: <gate id>
- Proves: <specific claim this evidence supports>
- Does not prove: <remaining gap>
- What evidence would change the verdict: <narrow next check>
- Next blocker (FAIL/INCONCLUSIVE only): <concrete blocker and owner>

# QEMU claim review and divergence localization

Use when a review finding, bug report, or model claim must be verified before
it drives a change. Placeholders use <...>.

## Claim intake

- Restate the claim as one falsifiable sentence and keep the reviewer's cited
  evidence next to it.
- Record source, date, tree revision, and whether the reviewer is human or
  agent.
- Name the evidence class that can settle it: static code, qtest, trace, boot,
  measurement, or numeric comparison.
- If the claim cannot be falsified as stated, rewrite it or return
  INCONCLUSIVE.

## Verify against code and QOM semantics

- Locate the claim in the checked-out tree and cite `file:line` with the
  revision.
- Read the property definition (`DEFINE_PROP_*`), the realize/init path, and
  every path that can set or reach the value.
- Check QOM reachability: can a normal machine, device, or guest reach this
  state? A debug-only default, a `-global` override, or a monitor write is
  not proof of supported behavior unless the claim is about that surface.
- Reproduce with the narrowest command. If reproduction needs an unsupported
  surface, say so and treat the claim as unproven.
- Try to refute as well as confirm: state what would falsify the claim and
  check it.

A checked-out pattern: a device property declared with
`DEFINE_PROP_UINT8(..., 2)` and overridden with `-global` for one run shows
only that the property can be overridden, not that a machine or guest reaches
that value. Reject it as evidence of a supported configuration unless normal
paths reach it.

## Classify pre-existing versus introduced

- Identify the files and hunks the change set touched.
- Reproduce on the baseline (or with the series reverted in a separate
  worktree) when available; otherwise record the missing baseline as a gap.
- Classify each finding: pre-existing, introduced by the series, pre-existing
  but newly exposed by the series, or unproven.
- Record the evidence for the classification, not only the label.

## Expected-value provenance

- Derive every expected value from the register contract, the manual page and
  section, the model source, or a checked-in test.
- Record the source and revision next to the expectation.
- Re-derive expectations when the model, image, or test changes.
- A mismatch becomes a model claim only after the expected value is verified;
  a stale literal is a known false-negative source.

## Input provenance

- Hash the QEMU binary/build directory, images, DTB, and machine options used
  by the claim.
- Check the device-tree properties the claim depends on before running (MSI:
  `msi-parent` and an ITS node; timers: clock properties and controller
  phandles).
- A stale DTB is a known false negative: rebuild it from the same tree as the
  kernel and model, or compare its hash with the recorded one.
- Record how the inputs can be re-created.

## First numerical divergence

1. Define dataflow slices in order: input capture, decode, intermediate state,
   output.
2. Compare each slice's model output against a reference (hardware trace,
   golden model, specification, or driver behavior) on identical inputs.
3. Stop at the first slice that differs and capture trace events, GDB
   register/memory state, and the exact input.
4. Re-run that slice with one variable changed to confirm causality.
5. Check the address space before declaring a bug: a model may present a
   linear view while hardware banks memory (for example separate DDR and
   global banks). Treat that as a model limitation or handoff gap.
6. Report unresolved numeric differences (for example 93 versus 96 MSI
   notifications) with counts, commands, and what would explain them. Do not
   round, average, or hide them.

## Review record

Fill one [claim record template](../assets/claim-record-template.md) per claim;
the block below is the minimum shape.

```text
Claim: <one falsifiable sentence>
Reviewer evidence: <source, date, revision>
Verification: <command, file:line, trace>
Classification: pre-existing | introduced | newly exposed | unproven
Verdict: PASS | FAIL | INCONCLUSIVE
Artifacts: <paths under .oh-my-qemu/<task-slug>/>
Gap: <what remains unexplained>
```

Unexplained numeric differences and missing baselines become handoff gaps;
record them in `audit.md` and state the next narrow check.

---
# SPDX-FileCopyrightText: Copyright (c) 2026 Process Mission
# SPDX-License-Identifier: MIT
name: qemu-model-verification
description: Use when existing qtest, trace, log, replay, boot, or workload evidence must be evaluated against one falsifiable QEMU device, board, TCG, or runtime claim as PASS, FAIL, or INCONCLUSIVE.
---

# QEMU Model Verification

## Audit workflow

For a non-trivial task that writes to the workspace, use only the needed entries under
`.oh-my-qemu/<task-slug>/`: `audit.md` (baseline, plan, decisions, evidence, verification, and
gaps), `commands.md` (redacted commands, working directories, and results), `logs/` (decisive
build, test, and runtime output), `scripts/` (probes, parsers, and harnesses), and `output/`
(generated deliverables, third-party dependencies, and non-QEMU binaries). Keep QEMU's own build
tree at source-root `builds/build-<target>/`, never an unqualified `build/`. In a Git worktree,
add `.agents/`, `.oh-my-qemu/`, and `builds/` to the file from
`git rev-parse --git-path info/exclude` before writing artifacts or configuring QEMU; preserve
existing entries and avoid duplicates. Never stage or commit these paths; stage source only when
the user explicitly requests that separate action. At handoff, reconcile `git status --short`
with the baseline and report the task directory, build directory, source changes, pre-existing
changes, and unresolved gaps.

## QEMU upstream boundary

QEMU's official GitLab and mailing lists are upstream channels. A patch becomes an upstream
contribution when it is sent to the maintainers selected through `MAINTAINERS`. Do not prepare or
send agent-generated code, documentation, commit messages, or patches for upstream submission; see
the checked-out tree's `docs/devel/code-provenance.rst`. Research, debugging, analysis, local
experiments, verification, and workflow guidance remain allowed. Local branches, commits, patch
files, pushes, and pull requests are not by themselves upstream contributions; perform those Git
actions only when requested.

## Evidence ladder

Given one falsifiable claim and existing evidence, report PASS, FAIL, or
INCONCLUSIVE without inventing evidence. Use the lowest rung that proves the
claim; a boot banner alone does not prove device correctness:

1. **Static inspection**: source/docs establish a fact.
2. **Build**: the touched target compiles.
3. **Unit/qtest**: register, IRQ, timer, memory, or board contract holds.
4. **Trace/log**: the expected runtime path executes and the bad path does not.
5. **Boot smoke**: firmware/kernel reaches a named milestone.
6. **Workload**: guest output proves the modeled hardware was consumed.
7. **Replay/reproduction**: the failure is deterministic or captured.

## Evidence provenance

Derive every expected marker, status value, count, or numeric bound from the
same evidence class as the artifact under test: register contract, model
source, or a checked-in test. Record the source and re-derive it when the test,
image, or model changes. A stale literal is a known false-negative source (an
old SHUTDOWN status, a DTB without required properties); do not edit an
expected literal to force a pass until its provenance is restored.

Record and compare hashes of the QEMU binary/build directory, images, DTB, and
machine options. Verify the device-tree properties the claim depends on (MSI:
`msi-parent` and an ITS node; timers/interrupts: controller and clock
properties) and decode the DTB when in doubt; a stale DTB is a known false
negative, not model evidence.

## Claim and acceptance criteria

Record one claim per gate in the
[claim record template](assets/claim-record-template.md): claim, gate, expected
values with provenance, inputs and hashes, evidence paths, verdict, proves and
does-not-prove, next blocker.

## INCONCLUSIVE sufficiency

A verdict is sufficient only when it names the evidence that would change it.
INCONCLUSIVE must state the gate, evidence collected, missing evidence, and
the next narrow command that could obtain it.

## Reviewer claims

Treat external review findings, human or agent, as hypotheses. Verify each
against the checked-out code and QOM semantics with `file:line`, classify it as
pre-existing or introduced by the change set, and reject unsupported debug
surfaces (for example a `-global` override unreachable from normal machine or
guest paths) as proof. Record the classification and evidence:
[claim review](references/claim-review.md).

## First divergence

For numeric mismatches, localize the first diverging slice: compare slice by
slice against a reference model or expected trace, capture trace/GDB state at
the first difference, and check whether banked or multiple address spaces hide
the difference.

## Failure classification

Classify before changing model code: environment/toolchain/build directory;
stale image; boot ABI; board topology; device register/IRQ/timer/DMA semantics;
TCG frontend/backend; guest/application. Usually only topology,
model-semantics, and TCG categories justify source changes.

## Register model structure check

Reconstruct the register-framework decision from current evidence (workspace
policy, compatible explicit user direction, maintained nearby convention, with
`RegisterInfo` as the fallback default) and verify the implementation matches
it. Register offsets, field macros, backing storage, framework tables, and
register-local callbacks must live in the device `.c` file, not a header or
board file. Report FAIL when current evidence does not justify the
implementation or a record contradicts it; do not fail only because no
historical record exists. Record the decision in `audit.md`; a successful
build, boot, or probe does not override this check.

## Device and board checklist

Use the qemu-peripheral-modeling and qemu-board-modeling checklists when
installed; otherwise verify directly: reset state, read/write masks and
reserved bits, W1C/status clear, IRQ raise/clear route, virtual-clock timer,
DMA guest-memory effect, machine creation, memory-map probes, reset after
dirty state.

## Trace validation

- count events and inspect semantic summaries; check skipped or unknown
  descriptor counts;
- verify command-memory and DMA ranges, and that the running image is the one
  intended;
- correlate trace milestones with UART or workload output.

## Reporting format

```text
PASS|FAIL|INCONCLUSIVE: <gate>
Command: <exact command>
Artifacts: <paths under .oh-my-qemu/<task-slug>/>
Evidence: <decisive lines or summary>
Proves / does not prove: <claim> / <remaining gap>
```

## Upstream references

- QEMU code provenance and AI policy: `docs/devel/code-provenance.rst`.
- Testing overview: `docs/devel/testing/main.rst`.
- QTest docs: `docs/devel/testing/qtest.rst`.
- Tracing: `docs/devel/tracing.rst`.
- Replay: `docs/system/replay.rst`.

Paths can differ between QEMU versions; locate them in the checked-out tree.