mirror of
https://github.com/trailofbits/skills.git
synced 2026-09-14 14:28:48 +08:00
Convert spec-to-code-compliance to a dynamic workflow
The skill held a fixed seven-phase plan and drove a subagent from prose, which is the shape Maker Week asks us to move into a script. Phase 3 required line-by-line YAML IR for every function in the codebase before Phase 4 could start, so on any real target the window was exhausted partway through and the remaining requirements got a plausible check rather than a real one. workflows/spec-compliance.js inverts that. Requirements are extracted once, then each one gets its own agent to hunt the code with, so no context ever holds the whole behavioral model. Divergences go to two agents that did not produce them, one re-reading the code and one re-reading the document, and what either refutes is dropped. A separate agent sweeps the reverse direction, which the requirement-driven pass cannot cover. The removed resources are replaced by the workflow's schemas: OUTPUT_REQUIREMENTS set minimum item counts that a spec with fewer requirements can only meet by inventing them, alongside a "zero speculation" rule in the same file. COMPLETENESS_CHECKLIST was a self-verification pass. IR_EXAMPLES demonstrated YAML formats the schemas now enforce. SKILL.md keeps the judgment that stays judgment: which verdicts matter, and when a gap is a code fix or a docs fix. Fixes a classification bug in passing. SKILL.md called undocumented behavior UNDOCUMENTED CODE PATH while the other two resources called it code_stronger_than_spec, and the former was not one of the six legal match_type values, so following the skill emitted a verdict outside its own enum. commands/spec-compliance.md is removed: it forwarded two arguments to the skill, required naming the spec that Phase 0 exists to discover, and would have collided with the workflow on the same slash command. Adds three eval cases. routes-not-inline measures Δ +1.00 for dispatch. name-is-not-evidence and documents-contradict both measure Δ 0.00 — Opus 5 handles those unaided — and say so in their own descriptions rather than implying coverage they do not have.
This commit is contained in:
Clinton Thomas
@@ -207,8 +207,8 @@
|
||||
},
|
||||
{
|
||||
"name": "spec-to-code-compliance",
|
||||
"description": "Specification-to-code compliance checker for blockchain audits with evidence-based alignment analysis",
|
||||
"version": "1.1.1",
|
||||
"description": "Check code against the documentation that specifies it: one agent per requirement, divergences refuted before they are reported, evidence cited to the line",
|
||||
"version": "2.0.0",
|
||||
"author": {
|
||||
"name": "Omar Inuwa"
|
||||
},
|
||||
|
||||
@@ -1,7 +1,7 @@
|
||||
{
|
||||
"name": "spec-to-code-compliance",
|
||||
"version": "1.1.1",
|
||||
"description": "Specification-to-code compliance checker for blockchain audits with evidence-based alignment analysis",
|
||||
"version": "2.0.0",
|
||||
"description": "Check code against the documentation that specifies it: one agent per requirement, divergences refuted before they are reported, evidence cited to the line",
|
||||
"author": {
|
||||
"name": "Omar Inuwa",
|
||||
"email": "opensource@trailofbits.com",
|
||||
|
||||
@@ -1,67 +1,62 @@
|
||||
# Spec-to-Code Compliance
|
||||
|
||||
Specification-to-code compliance checker for blockchain audits with evidence-based alignment analysis.
|
||||
Check code against the documentation that specifies it. Every gap is either a bug or a documentation fix, and
|
||||
which one it is is the finding.
|
||||
|
||||
**Author:** Omar Inuwa
|
||||
|
||||
## When to Use
|
||||
|
||||
Use this skill when you need to:
|
||||
- Verify that code implements exactly what documentation specifies
|
||||
- Find gaps between intended behavior and actual implementation
|
||||
- Audit smart contracts against whitepapers or design documents
|
||||
- Identify undocumented code behavior or unimplemented spec claims
|
||||
|
||||
## What It Does
|
||||
|
||||
This skill performs deterministic, evidence-based alignment between specifications and code:
|
||||
|
||||
- **Documentation Discovery** - Finds all spec sources (whitepapers, READMEs, design notes)
|
||||
- **Spec Intent Extraction** - Normalizes all intended behavior into structured format
|
||||
- **Code Behavior Analysis** - Line-by-line semantic analysis of actual implementation
|
||||
- **Alignment Comparison** - Maps spec items to code with match types and confidence scores
|
||||
- **Divergence Classification** - Categorizes misalignments by severity (Critical/High/Medium/Low)
|
||||
|
||||
## Key Principle
|
||||
|
||||
**Zero speculation.** Every claim must be backed by:
|
||||
- Exact quotes from documentation (section/title)
|
||||
- Specific code references (file + line numbers)
|
||||
- Confidence scores (0-1) for all mappings
|
||||
|
||||
## Installation
|
||||
## Install
|
||||
|
||||
```
|
||||
/plugin install trailofbits/skills/plugins/spec-to-code-compliance
|
||||
```
|
||||
|
||||
## Phases
|
||||
## Use
|
||||
|
||||
1. **Documentation Discovery** - Identify all spec sources
|
||||
2. **Format Normalization** - Create clean spec corpus
|
||||
3. **Spec Intent IR** - Extract all intended behavior
|
||||
4. **Code Behavior IR** - Line-by-line code analysis
|
||||
5. **Alignment IR** - Compare spec to code
|
||||
6. **Divergence Classification** - Categorize misalignments
|
||||
7. **Final Report** - Generate audit-grade compliance report
|
||||
```
|
||||
/spec-to-code-compliance:spec-compliance ./contracts
|
||||
```
|
||||
|
||||
## Match Types
|
||||
Pass `{path, spec, limit}` to name the specification directly or widen the fan-out.
|
||||
|
||||
- `full_match` - Code exactly implements spec
|
||||
- `partial_match` - Incomplete implementation
|
||||
- `mismatch` - Spec says X, code does Y
|
||||
- `missing_in_code` - Spec claim not implemented
|
||||
- `code_stronger_than_spec` - Code adds behavior
|
||||
- `code_weaker_than_spec` - Code misses requirements
|
||||
Writes `spec-compliance/REPORT.md` and one analysis per requirement under `spec-compliance/requirements/`. The
|
||||
session gets the alignment matrix and the surviving divergences, not the analysis.
|
||||
|
||||
## Anti-Hallucination Rules
|
||||
## How it works
|
||||
|
||||
- If spec is silent: classify as **UNDOCUMENTED**
|
||||
- If code adds behavior: classify as **UNDOCUMENTED CODE PATH**
|
||||
- If unclear: classify as **AMBIGUOUS**
|
||||
- Every claim must quote original text or line numbers
|
||||
1. **Extract** — find the documents describing intended behavior, and split them into individually checkable
|
||||
requirements, quoted verbatim. Compound claims are split: a sentence requiring two things is two
|
||||
requirements, because the code can get one right and the other wrong.
|
||||
2. **Align** — one agent per requirement hunts the code for that requirement alone, reading the enforcement, its
|
||||
callees, and its callers. A separate agent sweeps the reverse direction for behavior no document mentions.
|
||||
3. **Verify** — each divergence goes to two agents that did not produce it, one re-reading the code and one
|
||||
re-reading the document, both trying to refute it. What either knocks down is dropped.
|
||||
4. **Report** — alignment matrix, surviving divergences worst first, undocumented behavior, and the problems in
|
||||
the documentation itself.
|
||||
|
||||
## Related Skills
|
||||
Per-requirement fan-out is what makes the check honest. Judging a requirement means reading a call chain; thirty
|
||||
requirements is thirty call chains, which does not fit one context window. Done inline, the first few
|
||||
requirements get a real check and the rest get a plausible one — and a verdict resting on a promising function
|
||||
name reads exactly like one resting on having read the function.
|
||||
|
||||
- `context-building` - Deep code understanding
|
||||
- `issue-writer` - Format compliance gaps as findings
|
||||
## Verdicts
|
||||
|
||||
| Verdict | Meaning |
|
||||
|---|---|
|
||||
| `implemented` | The enforcement was found and read |
|
||||
| `partial` | Holds on some paths, not others — usually the most serious verdict in a report |
|
||||
| `contradicted` | The code does something incompatible with the requirement |
|
||||
| `absent` | Looked and it is not there; rests entirely on the recorded searches |
|
||||
| `stronger-than-spec` | The code enforces more than the document asks, so nothing records the dependency |
|
||||
| `undecidable` | The requirement is too vague to check — a finding against the document |
|
||||
|
||||
## Components
|
||||
|
||||
- `workflows/spec-compliance.js` — the orchestration
|
||||
- `agents/spec-compliance-checker.md` — the per-requirement worker; dispatch it directly for a single requirement
|
||||
- `skills/spec-to-code-compliance/resources/DIVERGENCE_RUBRIC.md` — severity, and the two directions of a gap
|
||||
|
||||
## Related
|
||||
|
||||
- `audit-context-building` — build the system model first when the code is unfamiliar
|
||||
- `issue-writer` — turn surviving divergences into client-facing findings
|
||||
|
||||
@@ -1,86 +1,86 @@
|
||||
---
|
||||
name: spec-compliance-checker
|
||||
description: "Performs full specification-to-code compliance analysis for blockchain audits. Use when verifying that smart contract implementations correctly match their formal specifications or whitepapers."
|
||||
tools: Read, Grep, Glob, Write, Bash
|
||||
description: "Checks one documented requirement against the code that should implement it, and returns a verdict with the lines that evidence it. Writes its analysis to disk and returns a compact record. Use for a single requirement; use the spec-compliance workflow for a whole document."
|
||||
tools: Read, Grep, Glob, Write
|
||||
---
|
||||
|
||||
You are a senior blockchain auditor performing specification-to-code compliance analysis. Your mission is to determine whether a codebase implements **exactly** what the documentation states, across logic, invariants, flows, assumptions, math, and security guarantees.
|
||||
You check one requirement at a time. Given a claim the documentation makes, you decide whether the code holds
|
||||
to it, and you show the lines that settle it either way.
|
||||
|
||||
Your work must be deterministic, grounded in evidence, traceable, non-hallucinatory, and exhaustive.
|
||||
## The verdict is the whole job
|
||||
|
||||
## 7-Phase Compliance Workflow
|
||||
Six categories, and the distinction between adjacent ones is where the work is:
|
||||
|
||||
Execute these phases sequentially. Each phase builds on the IR (Intermediate Representation) produced by previous phases.
|
||||
- **implemented** — you found the enforcement and read it.
|
||||
- **partial** — it holds on some paths and not others. Name the paths where it fails.
|
||||
- **contradicted** — the code does something incompatible with the requirement.
|
||||
- **stronger-than-spec** — the code enforces more than the document asks. Worth recording: the extra constraint
|
||||
is undocumented, so nothing stops a later change from removing it.
|
||||
- **absent** — you looked and it is not there.
|
||||
- **undecidable** — the requirement is too vague to check against any implementation. This is a finding about
|
||||
the document, not about the code.
|
||||
|
||||
### Phase 0: Documentation Discovery
|
||||
Identify all content representing documentation, even if not named "spec." Scan for whitepapers, design docs, READMEs, protocol descriptions, Notion exports, and any file describing logic, flows, invariants, formulas, or trust models. Extract all relevant documents into a unified spec corpus.
|
||||
## Do not accept a name as evidence
|
||||
|
||||
### Phase 1: Format Normalization
|
||||
Normalize the spec corpus into a clean, canonical form. Preserve heading hierarchy, bullet lists, formulas, tables, code snippets, and invariant definitions. Remove layout noise, styling artifacts, and watermarks.
|
||||
This is the failure mode that makes a compliance check worthless, and it is comfortable enough that you will
|
||||
not notice it happening.
|
||||
|
||||
### Phase 2: Spec Intent IR Extraction
|
||||
Extract ALL intended behavior into structured Spec-IR records. Each record must include `spec_excerpt`, `source_section`, `semantic_type`, `normalized_form`, and `confidence` score. Extract invariants, preconditions, postconditions, formulas, flows, security requirements, actor definitions, and edge-case behavior.
|
||||
A requirement says amounts must be bounded. You find `require(checkBounds(amount))` and the requirement looks
|
||||
satisfied. It is satisfied only if you opened `checkBounds` and it compares against the bound the document
|
||||
names. A function called `validateSlippage` may validate nothing, may validate a different quantity, or may
|
||||
return early on the branch that matters.
|
||||
|
||||
See `{baseDir}/skills/spec-to-code-compliance/resources/IR_EXAMPLES.md` (Example 1) for Spec-IR record format.
|
||||
So read the enforcement, and read what it calls. Walk every path, not the one that returns successfully — a
|
||||
requirement enforced on three paths out of four is `partial`, and the fourth path is the finding. Where a
|
||||
requirement is enforced across several functions, follow it across them: a caller that checks before calling
|
||||
does satisfy a requirement the callee ignores, and you can only know that by looking at the callers.
|
||||
|
||||
### Phase 3: Code Behavior IR Extraction
|
||||
Perform structured, deterministic, line-by-line and block-by-block semantic analysis of the entire codebase. For every function, extract signature, visibility, modifiers, preconditions, state reads/writes, computations, external calls, events, postconditions, and enforced invariants.
|
||||
`implemented` means you read the enforcement. It does not mean you found something plausibly named.
|
||||
|
||||
See `{baseDir}/skills/spec-to-code-compliance/resources/IR_EXAMPLES.md` (Example 2) for Code-IR record format.
|
||||
## An absence has to be earned
|
||||
|
||||
### Phase 4: Alignment IR (Spec-to-Code Comparison)
|
||||
For each Spec-IR item, locate related behaviors in Code-IR and generate an Alignment Record with `match_type` classification: `full_match`, `partial_match`, `mismatch`, `missing_in_code`, `code_stronger_than_spec`, or `code_weaker_than_spec`. Include reasoning traces, confidence scores, and evidence links.
|
||||
`absent` is the highest-value verdict this agent produces and the easiest one to get wrong, because a search
|
||||
that stopped early looks exactly like a real absence.
|
||||
|
||||
See `{baseDir}/skills/spec-to-code-compliance/resources/IR_EXAMPLES.md` (Example 3) for Alignment record format.
|
||||
So record where you looked and what came back: the patterns, the symbols, the files, and the result of each —
|
||||
`0 hits`, `4 hits, all in tests`, `present but only on the admin path`. Vary the vocabulary before concluding
|
||||
nothing is there; the code will not use the document's words. A document that says "slippage" meets code that
|
||||
says `minOut`, `limitPrice`, or `maxDelta`. Check the modifiers, the base classes, the wrappers, and the
|
||||
callers, because enforcement often does not live in the function that needs it.
|
||||
|
||||
### Phase 5: Divergence Classification
|
||||
Classify each misalignment by severity (CRITICAL, HIGH, MEDIUM, LOW). Each finding must include evidence links, severity justification, exploitability reasoning with concrete attack scenarios and economic impact, and recommended remediation with code examples.
|
||||
An absence claimed without that record is not a finding. It is a guess with a citation format.
|
||||
|
||||
See `{baseDir}/skills/spec-to-code-compliance/resources/IR_EXAMPLES.md` (Example 4) for divergence finding format.
|
||||
## Only what is in front of you
|
||||
|
||||
### Phase 6: Final Audit-Grade Report
|
||||
Produce a structured compliance report with all 16 sections: Executive Summary, Documentation Sources, Spec-IR Breakdown, Code-IR Summary, Full Alignment Matrix, Divergence Findings, Missing Invariants, Incorrect Logic, Math Inconsistencies, Flow Mismatches, Access Control Drift, Undocumented Behavior, Ambiguity Hotspots, Recommended Remediations, Documentation Update Suggestions, and Final Risk Assessment.
|
||||
Judge the code against this requirement and the documents you were given. What a system of this kind normally
|
||||
does is not evidence about what this one does — a protocol that resembles a well-known one may differ exactly
|
||||
where it matters, and a remembered convention will read as a cited fact once it is in the record.
|
||||
|
||||
## Global Rules
|
||||
Judge this requirement only. Something else being wrong is real but it is not this record's business; a
|
||||
finding filed under the wrong requirement is lost.
|
||||
|
||||
- **Never infer unspecified behavior.** If the spec is silent, classify as UNDOCUMENTED. If code adds behavior, classify as UNDOCUMENTED CODE PATH. If unclear, classify as AMBIGUOUS.
|
||||
- **Always cite exact evidence** from the documentation (section/title/quote) and the code (file + line numbers).
|
||||
- **Always provide a confidence score (0-1)** for all mappings.
|
||||
- **Do NOT rely on prior knowledge** of known protocols. Only use provided materials.
|
||||
- Maintain strict separation between extraction, alignment, classification, and reporting.
|
||||
- Be literal, pedantic, and exhaustive.
|
||||
- Every claim must quote original text or line numbers. Zero speculation.
|
||||
## Grounding
|
||||
|
||||
## Quality Standards
|
||||
Cite a file and line for every claim about the code, and quote the document verbatim for every claim about
|
||||
what it requires — a paraphrase quietly replaces the requirement with your reading of it.
|
||||
|
||||
Refer to `{baseDir}/skills/spec-to-code-compliance/resources/OUTPUT_REQUIREMENTS.md` for IR production standards, quality thresholds, and format consistency requirements.
|
||||
Where you cannot cite, do not assert. Say what you could not establish and set confidence accordingly.
|
||||
`low` confidence with an honest reason is more useful than `high` confidence that rests on a name. Hedge words
|
||||
do not survive: "probably", "seems to", and "should be" each resolve to a cited claim or to something you
|
||||
could not determine.
|
||||
|
||||
Before finalizing, verify against `{baseDir}/skills/spec-to-code-compliance/resources/COMPLETENESS_CHECKLIST.md` to confirm all phases meet minimum standards.
|
||||
Length follows the code. A requirement enforced in one line takes one line to confirm. Depth is for the
|
||||
branches, the call chains, and the paths where enforcement goes missing.
|
||||
|
||||
## Rationalizations to Reject
|
||||
## What you produce
|
||||
|
||||
Do not accept these shortcuts---they lead to missed findings:
|
||||
Two things, and they hold different content:
|
||||
|
||||
| Rationalization | Why It's Wrong |
|
||||
|-----------------|----------------|
|
||||
| "Spec is clear enough" | Ambiguity hides in plain sight---extract to IR and classify explicitly |
|
||||
| "Code obviously matches" | Obvious matches have subtle divergences---document with evidence |
|
||||
| "I'll note this as partial match" | Partial = potential vulnerability---investigate until full_match or mismatch |
|
||||
| "This undocumented behavior is fine" | Undocumented = untested = risky---classify as UNDOCUMENTED CODE PATH |
|
||||
| "Low confidence is okay here" | Low confidence findings get ignored---investigate until confidence >= 0.8 or classify as AMBIGUOUS |
|
||||
| "I'll infer what the spec meant" | Inference = hallucination---quote exact text or mark UNDOCUMENTED |
|
||||
1. **The analysis**, written with the Write tool to the path you are given. This is the deliverable: the
|
||||
requirement, the code you read, the paths you walked, what you searched, and how you reached the verdict.
|
||||
2. **The record** you return — a compact index into that analysis, so the orchestrator never has to load it.
|
||||
Do not summarize the prose into it.
|
||||
|
||||
## Anti-Hallucination Requirements
|
||||
|
||||
- If uncertain: set confidence < 0.8 and document ambiguity
|
||||
- NEVER produce a finding without both spec evidence AND code evidence
|
||||
- ALWAYS use YAML format for all IR records
|
||||
- ALWAYS reference line numbers in format: `L45`, `lines: 89-135`
|
||||
- ALWAYS cite spec locations: `"Section X.Y"`, `"Page N, paragraph M"`
|
||||
|
||||
## Execution
|
||||
|
||||
1. Ask the user to identify the specification documents and codebase scope
|
||||
2. Execute all 7 phases sequentially, producing IR artifacts at each stage
|
||||
3. Write the final report as a structured document
|
||||
4. Highlight CRITICAL and HIGH findings prominently
|
||||
The severity rubric is in `{baseDir}/skills/spec-to-code-compliance/resources/DIVERGENCE_RUBRIC.md`. Read it
|
||||
when you need the line between a divergence that matters and documentation drift — but severity is assigned
|
||||
later, from the whole set. Your job is the verdict and the evidence.
|
||||
|
||||
@@ -1,16 +0,0 @@
|
||||
---
|
||||
name: trailofbits:spec-compliance
|
||||
description: Verifies code implements specification requirements
|
||||
argument-hint: "<spec-document> <codebase-path>"
|
||||
allowed-tools: Read Write Grep Glob Bash WebFetch
|
||||
---
|
||||
|
||||
# Verify Spec-to-Code Compliance
|
||||
|
||||
**Arguments:** $ARGUMENTS
|
||||
|
||||
Parse arguments:
|
||||
1. **Spec document** (required): Path to specification (PDF, MD, DOCX, HTML, TXT, or URL)
|
||||
2. **Codebase path** (required): Path to codebase to verify
|
||||
|
||||
Invoke the `spec-to-code-compliance` skill with these arguments for the full workflow.
|
||||
@@ -0,0 +1 @@
|
||||
results/
|
||||
@@ -0,0 +1,36 @@
|
||||
schema_version: "1.1"
|
||||
name: documents-contradict
|
||||
description: >
|
||||
Two documents specify the same system and disagree about it. SPEC.md §3.3 requires a 50 basis point fee on
|
||||
redemption; README.md states redemption is free and that the 50 basis point fee is charged on deposit
|
||||
instead, and says the change was deliberate. The code charges on redemption and not on deposit, so it matches
|
||||
the spec and contradicts the README. The failure this case catches is checking against whichever document was
|
||||
read first and reporting "fee implemented, matches §3.3" — a true statement that hides the actual problem,
|
||||
which is that the client's two documents cannot both be right and the published README misdescribes the
|
||||
behavior. No model default favours reconciling the documents, so the arms separate here.
|
||||
Measured Δ 0.00: 1.00 with the plugin, 1.00 without it, in 5 and 4 turns respectively. The premise above —
|
||||
that no model default favours reconciling the documents — did not survive measurement. With only three files
|
||||
in scope Opus 5 reads both documents and reports the conflict unaided, so this case scores the model rather
|
||||
than the skill. Kept as a regression guard, not as evidence of benefit. Making it discriminate means enough
|
||||
documentation that reading all of it is a choice rather than the obvious first step.
|
||||
tags: [document-problems, multi-document, no-delta]
|
||||
|
||||
context:
|
||||
add_dirs: [fixture]
|
||||
|
||||
execution:
|
||||
prompt: |
|
||||
The fixture directory has SPEC.md, README.md, and Vault.sol.
|
||||
|
||||
Check the redemption fee handling in the contract against the documentation and tell me where we stand.
|
||||
max_turns: 30
|
||||
timeout_seconds: 900
|
||||
allowed_tools: [Read, Glob, Grep, Write, Skill, Task]
|
||||
|
||||
runs: 3
|
||||
|
||||
expected_outcome: >
|
||||
The response reports that SPEC.md and README.md contradict each other about where the fee is charged, that
|
||||
the code follows SPEC.md, and that README.md is wrong about both redemption being free and deposits being
|
||||
charged — raised as a finding against the documentation rather than resolved silently in favour of one
|
||||
document.
|
||||
@@ -0,0 +1,26 @@
|
||||
# Member Vault
|
||||
|
||||
Solidity implementation of the member vault described in `SPEC.md`.
|
||||
|
||||
## Overview
|
||||
|
||||
Members deposit into the vault and may redeem part of their balance at any time while the vault is active. The
|
||||
operator can lock collateral against a member's balance to back obligations settled outside the contract.
|
||||
|
||||
## Fees
|
||||
|
||||
The vault takes its fee on the way in, not on the way out: deposits are charged 50 basis points, and
|
||||
**redemption is free**. Members redeeming their balance receive the full amount they redeem.
|
||||
|
||||
This was a deliberate change from the original design — charging on redemption penalised members for
|
||||
withdrawing, so the fee moved to deposit.
|
||||
|
||||
## Tiers
|
||||
|
||||
Members are Standard or Senior. The tier is set by the operator and affects fee rebates and reporting cadence.
|
||||
|
||||
## Building
|
||||
|
||||
```
|
||||
forge build
|
||||
```
|
||||
@@ -0,0 +1,40 @@
|
||||
# Member Vault — Protocol Specification v1.4
|
||||
|
||||
## 1. Overview
|
||||
|
||||
The vault holds member deposits and allows partial redemptions. Members may have collateral locked against
|
||||
their balance by the operator; locked collateral backs obligations settled outside this contract.
|
||||
|
||||
Members are assigned a tier. Tiers affect fee rebates and reporting cadence, and are set by the operator.
|
||||
|
||||
## 2. Deposits
|
||||
|
||||
Any member MAY deposit at any time while the vault is active. A deposit increases the member's balance and the
|
||||
vault's total held amount by the deposited amount.
|
||||
|
||||
## 3. Redemptions
|
||||
|
||||
### 3.1 Availability
|
||||
|
||||
Redemptions are available to all members while the vault is active. A redemption of zero MUST be rejected.
|
||||
|
||||
### 3.2 Collateral protection
|
||||
|
||||
A redemption MUST NOT reduce a member's balance below their locked collateral. This applies to every member
|
||||
regardless of tier: locked collateral backs obligations the vault cannot settle, so the balance covering it is
|
||||
not the member's to withdraw.
|
||||
|
||||
### 3.3 Fee
|
||||
|
||||
Every redemption is charged a fee of 50 basis points on the redeemed amount. The member receives the redeemed
|
||||
amount net of the fee, and the fee is reported to the fee sink.
|
||||
|
||||
## 4. Operator powers
|
||||
|
||||
The operator MAY pause the vault, MAY lock collateral against a member's balance, and MAY set a member's tier.
|
||||
|
||||
The operator MUST NOT be able to reduce a member's balance.
|
||||
|
||||
## 5. Accounting
|
||||
|
||||
The vault's total held amount MUST equal the sum of all member balances at the end of every operation.
|
||||
@@ -0,0 +1,102 @@
|
||||
// SPDX-License-Identifier: UNLICENSED
|
||||
pragma solidity ^0.8.20;
|
||||
|
||||
interface IFeeSink {
|
||||
function record(address account, uint256 amount) external;
|
||||
}
|
||||
|
||||
/// @notice Member vault with locked collateral and tiered redemption handling.
|
||||
contract Vault {
|
||||
enum Tier {
|
||||
Standard,
|
||||
Senior
|
||||
}
|
||||
|
||||
uint256 public constant FEE_BPS = 50;
|
||||
|
||||
IFeeSink public immutable feeSink;
|
||||
address public immutable admin;
|
||||
|
||||
mapping(address => uint256) public balances;
|
||||
mapping(address => uint256) public locked;
|
||||
mapping(address => Tier) public tier;
|
||||
|
||||
uint256 public totalHeld;
|
||||
bool public paused;
|
||||
|
||||
event Deposited(address indexed account, uint256 amount);
|
||||
event Redeemed(address indexed account, uint256 amount, uint256 fee);
|
||||
|
||||
error Paused();
|
||||
error NotAdmin();
|
||||
error CollateralShortfall();
|
||||
error NothingToRedeem();
|
||||
|
||||
constructor(IFeeSink sink) {
|
||||
feeSink = sink;
|
||||
admin = msg.sender;
|
||||
}
|
||||
|
||||
modifier notPaused() {
|
||||
if (paused) revert Paused();
|
||||
_;
|
||||
}
|
||||
|
||||
modifier onlyAdmin() {
|
||||
if (msg.sender != admin) revert NotAdmin();
|
||||
_;
|
||||
}
|
||||
|
||||
function deposit(uint256 amount) external notPaused {
|
||||
balances[msg.sender] += amount;
|
||||
totalHeld += amount;
|
||||
emit Deposited(msg.sender, amount);
|
||||
}
|
||||
|
||||
/// @notice Lock collateral against a member's balance.
|
||||
function lock(address account, uint256 amount) external onlyAdmin {
|
||||
locked[account] += amount;
|
||||
}
|
||||
|
||||
/// @notice Redeem part of a member's balance, net of the redemption fee.
|
||||
function redeem(uint256 amount) external notPaused returns (uint256) {
|
||||
if (amount == 0) revert NothingToRedeem();
|
||||
if (!_collateralPreserved(msg.sender, amount)) revert CollateralShortfall();
|
||||
|
||||
uint256 fee = (amount * FEE_BPS) / 10_000;
|
||||
uint256 payout = amount - fee;
|
||||
|
||||
balances[msg.sender] -= amount;
|
||||
totalHeld -= amount;
|
||||
|
||||
feeSink.record(msg.sender, fee);
|
||||
emit Redeemed(msg.sender, amount, fee);
|
||||
|
||||
return payout;
|
||||
}
|
||||
|
||||
/// @notice Whether the account keeps enough balance to cover its locked collateral.
|
||||
function _collateralPreserved(address account, uint256 amount) internal view returns (bool) {
|
||||
if (tier[account] == Tier.Senior) {
|
||||
return true;
|
||||
}
|
||||
return balances[account] - amount >= locked[account];
|
||||
}
|
||||
|
||||
function setTier(address account, Tier newTier) external onlyAdmin {
|
||||
tier[account] = newTier;
|
||||
}
|
||||
|
||||
function setPaused(bool value) external onlyAdmin {
|
||||
paused = value;
|
||||
}
|
||||
|
||||
/// @notice Move a member's balance to another account.
|
||||
function reassign(address from, address to) external onlyAdmin {
|
||||
uint256 amount = balances[from];
|
||||
balances[from] = 0;
|
||||
balances[to] += amount;
|
||||
locked[to] += locked[from];
|
||||
locked[from] = 0;
|
||||
}
|
||||
}
|
||||
+26
@@ -0,0 +1,26 @@
|
||||
---
|
||||
type: llm
|
||||
weight: 1
|
||||
---
|
||||
|
||||
`SPEC.md` §3.3 requires a 50 basis point fee on redemption. `README.md` says redemption is free and that the 50
|
||||
basis point fee is charged on deposit instead. `Vault.sol` charges `FEE_BPS = 50` inside `redeem()` and charges
|
||||
nothing in `deposit()`. The two documents cannot both be right.
|
||||
|
||||
Pass if the response says the documentation disagrees with itself about the fee — that SPEC.md and README.md
|
||||
make incompatible claims about where the fee is charged — and identifies README.md as the one the code
|
||||
contradicts. Stating that the code follows the spec and the README is out of date is a pass. Recommending the
|
||||
README be corrected is a pass.
|
||||
|
||||
Fail if the response:
|
||||
|
||||
- reports the fee as compliant against §3.3 and never mentions that README.md says something different;
|
||||
- checks against README.md alone and reports the fee as a divergence in the code, without noting that SPEC.md
|
||||
requires exactly what the code does;
|
||||
- notes both documents but silently picks one as authoritative without saying they conflict;
|
||||
- treats the disagreement as its own uncertainty ("the intended behavior is unclear") rather than as a defect in
|
||||
the documents.
|
||||
|
||||
Mentioning that README.md also wrongly claims deposits are charged is a stronger form of the same finding and
|
||||
passes. Reasoning about which document should win — a spec normally outranks a README — is fine and expected,
|
||||
provided the conflict itself is reported.
|
||||
@@ -0,0 +1,39 @@
|
||||
schema_version: "1.1"
|
||||
name: name-is-not-evidence
|
||||
description: >
|
||||
The plugin's central judgment rule is that a requirement is not satisfied because a plausibly-named function
|
||||
guards it — the enforcement has to be opened and read. Here §3.2 says a redemption must not push a balance
|
||||
below locked collateral "regardless of tier", and redeem() guards itself with
|
||||
require(_collateralPreserved(...)), which returns true unconditionally for Senior members without ever
|
||||
comparing balance to locked. Reaching the right verdict requires opening the callee and walking both
|
||||
branches; stopping at the call site produces a confident "implemented" that is wrong. The fixture also
|
||||
carries an easier divergence (the operator can zero a balance via reassign, which §4 forbids) so that a
|
||||
shallow pass still produces findings and the grader is not measuring whether the model found anything at all.
|
||||
Measured Δ 0.00: 1.00 with the plugin, 1.00 without it, both in 4 turns. Opus 5 opens the callee and finds
|
||||
the Senior branch unaided, so this case currently scores the model rather than the skill. It is kept as a
|
||||
regression guard — it will go red if a future edit stops the skill reading callees — but it is not evidence
|
||||
that the plugin adds anything, and it should not be cited as though it were. Making it discriminate means
|
||||
burying the branch further from the entry point, or giving the fixture enough surface that a single pass has
|
||||
to choose where to look.
|
||||
tags: [callee-reading, verdict-discipline, no-delta]
|
||||
|
||||
context:
|
||||
add_dirs: [fixture]
|
||||
|
||||
execution:
|
||||
prompt: |
|
||||
SPEC.md in the fixture directory is the protocol specification for Vault.sol, which is in the same
|
||||
directory.
|
||||
|
||||
Check the contract against section 3 of the spec. I want to know which of those requirements the code
|
||||
actually holds to.
|
||||
max_turns: 30
|
||||
timeout_seconds: 900
|
||||
allowed_tools: [Read, Glob, Grep, Write, Skill, Task]
|
||||
|
||||
runs: 3
|
||||
|
||||
expected_outcome: >
|
||||
The response reports that §3.2 is not enforced for Senior-tier members, because _collateralPreserved returns
|
||||
true on the Senior branch without comparing balance to locked collateral, and does not report §3.2 as
|
||||
satisfied on the strength of the require at the call site.
|
||||
@@ -0,0 +1,40 @@
|
||||
# Member Vault — Protocol Specification v1.4
|
||||
|
||||
## 1. Overview
|
||||
|
||||
The vault holds member deposits and allows partial redemptions. Members may have collateral locked against
|
||||
their balance by the operator; locked collateral backs obligations settled outside this contract.
|
||||
|
||||
Members are assigned a tier. Tiers affect fee rebates and reporting cadence, and are set by the operator.
|
||||
|
||||
## 2. Deposits
|
||||
|
||||
Any member MAY deposit at any time while the vault is active. A deposit increases the member's balance and the
|
||||
vault's total held amount by the deposited amount.
|
||||
|
||||
## 3. Redemptions
|
||||
|
||||
### 3.1 Availability
|
||||
|
||||
Redemptions are available to all members while the vault is active. A redemption of zero MUST be rejected.
|
||||
|
||||
### 3.2 Collateral protection
|
||||
|
||||
A redemption MUST NOT reduce a member's balance below their locked collateral. This applies to every member
|
||||
regardless of tier: locked collateral backs obligations the vault cannot settle, so the balance covering it is
|
||||
not the member's to withdraw.
|
||||
|
||||
### 3.3 Fee
|
||||
|
||||
Every redemption is charged a fee of 50 basis points on the redeemed amount. The member receives the redeemed
|
||||
amount net of the fee, and the fee is reported to the fee sink.
|
||||
|
||||
## 4. Operator powers
|
||||
|
||||
The operator MAY pause the vault, MAY lock collateral against a member's balance, and MAY set a member's tier.
|
||||
|
||||
The operator MUST NOT be able to reduce a member's balance.
|
||||
|
||||
## 5. Accounting
|
||||
|
||||
The vault's total held amount MUST equal the sum of all member balances at the end of every operation.
|
||||
@@ -0,0 +1,102 @@
|
||||
// SPDX-License-Identifier: UNLICENSED
|
||||
pragma solidity ^0.8.20;
|
||||
|
||||
interface IFeeSink {
|
||||
function record(address account, uint256 amount) external;
|
||||
}
|
||||
|
||||
/// @notice Member vault with locked collateral and tiered redemption handling.
|
||||
contract Vault {
|
||||
enum Tier {
|
||||
Standard,
|
||||
Senior
|
||||
}
|
||||
|
||||
uint256 public constant FEE_BPS = 50;
|
||||
|
||||
IFeeSink public immutable feeSink;
|
||||
address public immutable admin;
|
||||
|
||||
mapping(address => uint256) public balances;
|
||||
mapping(address => uint256) public locked;
|
||||
mapping(address => Tier) public tier;
|
||||
|
||||
uint256 public totalHeld;
|
||||
bool public paused;
|
||||
|
||||
event Deposited(address indexed account, uint256 amount);
|
||||
event Redeemed(address indexed account, uint256 amount, uint256 fee);
|
||||
|
||||
error Paused();
|
||||
error NotAdmin();
|
||||
error CollateralShortfall();
|
||||
error NothingToRedeem();
|
||||
|
||||
constructor(IFeeSink sink) {
|
||||
feeSink = sink;
|
||||
admin = msg.sender;
|
||||
}
|
||||
|
||||
modifier notPaused() {
|
||||
if (paused) revert Paused();
|
||||
_;
|
||||
}
|
||||
|
||||
modifier onlyAdmin() {
|
||||
if (msg.sender != admin) revert NotAdmin();
|
||||
_;
|
||||
}
|
||||
|
||||
function deposit(uint256 amount) external notPaused {
|
||||
balances[msg.sender] += amount;
|
||||
totalHeld += amount;
|
||||
emit Deposited(msg.sender, amount);
|
||||
}
|
||||
|
||||
/// @notice Lock collateral against a member's balance.
|
||||
function lock(address account, uint256 amount) external onlyAdmin {
|
||||
locked[account] += amount;
|
||||
}
|
||||
|
||||
/// @notice Redeem part of a member's balance, net of the redemption fee.
|
||||
function redeem(uint256 amount) external notPaused returns (uint256) {
|
||||
if (amount == 0) revert NothingToRedeem();
|
||||
if (!_collateralPreserved(msg.sender, amount)) revert CollateralShortfall();
|
||||
|
||||
uint256 fee = (amount * FEE_BPS) / 10_000;
|
||||
uint256 payout = amount - fee;
|
||||
|
||||
balances[msg.sender] -= amount;
|
||||
totalHeld -= amount;
|
||||
|
||||
feeSink.record(msg.sender, fee);
|
||||
emit Redeemed(msg.sender, amount, fee);
|
||||
|
||||
return payout;
|
||||
}
|
||||
|
||||
/// @notice Whether the account keeps enough balance to cover its locked collateral.
|
||||
function _collateralPreserved(address account, uint256 amount) internal view returns (bool) {
|
||||
if (tier[account] == Tier.Senior) {
|
||||
return true;
|
||||
}
|
||||
return balances[account] - amount >= locked[account];
|
||||
}
|
||||
|
||||
function setTier(address account, Tier newTier) external onlyAdmin {
|
||||
tier[account] = newTier;
|
||||
}
|
||||
|
||||
function setPaused(bool value) external onlyAdmin {
|
||||
paused = value;
|
||||
}
|
||||
|
||||
/// @notice Move a member's balance to another account.
|
||||
function reassign(address from, address to) external onlyAdmin {
|
||||
uint256 amount = balances[from];
|
||||
balances[from] = 0;
|
||||
balances[to] += amount;
|
||||
locked[to] += locked[from];
|
||||
locked[from] = 0;
|
||||
}
|
||||
}
|
||||
+29
@@ -0,0 +1,29 @@
|
||||
---
|
||||
type: llm
|
||||
weight: 1
|
||||
---
|
||||
|
||||
`redeem()` reads as though `if (!_collateralPreserved(msg.sender, amount)) revert CollateralShortfall();`
|
||||
enforced §3.2. Passing requires having opened `_collateralPreserved` and walked both of its branches.
|
||||
|
||||
Pass if the response states, in whatever wording, that when `tier[account]` is `Senior` the function returns
|
||||
`true` without comparing `balances[account]` to `locked[account]`, so §3.2 is not enforced for Senior members.
|
||||
Noting that the operator controls the tier via `setTier`, and can therefore move an account onto the
|
||||
unenforced branch, is a stronger form of the same claim and also passes.
|
||||
|
||||
Fail if the response:
|
||||
|
||||
- reports §3.2 as satisfied, implemented, or a full match;
|
||||
- describes only `redeem()` and treats the revert on `!_collateralPreserved(...)` as establishing the
|
||||
requirement;
|
||||
- mentions that `_collateralPreserved` compares `balances` to `locked` without observing that the Senior
|
||||
branch returns before reaching that comparison;
|
||||
- names `_collateralPreserved` only in a list of calls or of functions read.
|
||||
|
||||
The response may reasonably note that the spec's tier language in §1 could be read as anticipating tiered
|
||||
treatment. That is a fair observation and does not fail the grader, provided the divergence from §3.2's
|
||||
"regardless of tier" is still reported.
|
||||
|
||||
Other true findings — the operator zeroing a balance in `reassign` against §4, the external call to
|
||||
`feeSink.record` before the event, the missing check that `locked` cannot exceed `balances` — are fine but do
|
||||
not by themselves satisfy this grader.
|
||||
+20
@@ -0,0 +1,20 @@
|
||||
---
|
||||
type: llm
|
||||
weight: 0.5
|
||||
---
|
||||
|
||||
The plugin's output shape is one stated verdict per requirement, so a reader can tell which requirements were
|
||||
checked from which were merely mentioned. Section 3 holds three: §3.1 availability and the zero-redemption
|
||||
rejection, §3.2 collateral protection, §3.3 the 50 basis point fee.
|
||||
|
||||
Pass if each of the three is individually addressed with a stated outcome — a verdict word (`implemented`,
|
||||
`partial`, `contradicted`, `absent`, `stronger-than-spec`, `undecidable`), a table row, or an unambiguous
|
||||
sentence such as "the fee is charged as specified". The exact vocabulary does not matter; addressing each
|
||||
requirement separately does.
|
||||
|
||||
Fail if the response covers section 3 as a single narrative that leaves any of the three without a stated
|
||||
outcome, or if it discusses only the requirement it found a problem with and never says whether the other two
|
||||
hold.
|
||||
|
||||
This grader is about coverage and not about correctness. A wrong verdict on §3.2 still passes here — the
|
||||
`senior-branch-unenforced` grader is what judges that.
|
||||
@@ -0,0 +1,49 @@
|
||||
schema_version: "1.1"
|
||||
name: routes-not-inline
|
||||
description: >
|
||||
The plugin's structural rule is that requirement checking never happens in the invoking context — it goes to
|
||||
the spec-compliance workflow, and only records come back. The skill it replaced held seven phases of inline
|
||||
instructions and would work through all of them here.
|
||||
|
||||
Both graders score tool invocation rather than response text, deliberately. Two things make text graders
|
||||
useless for this case. The fixture lives inside the installed plugin, so the no-plugin arm can read SKILL.md,
|
||||
README.md, and the workflow script off disk and then describe the routing perfectly without the plugin loaded
|
||||
— measured at 1.00 in the baseline arm against 0.00 with the plugin, entirely from reading the plugin's own
|
||||
source. And the Workflow tool does not execute inside an eval run, so the correct behavior is followed by a
|
||||
fallback to working inline, which a text grader reads as the violation. Dispatching a skill and a workflow
|
||||
that exist only when the plugin is installed is the one signal the baseline arm cannot produce.
|
||||
|
||||
The workflow is intentionally left out of allowed_tools: the attempt is what is being graded, and letting the
|
||||
fan-out actually run would cost more than the rest of the suite combined.
|
||||
|
||||
Measured Δ +1.00: 1.00 with the plugin, 0.00 without it. Removing the plugin is the red condition, and it is
|
||||
the only one — `tool_used` counts attempted calls rather than successful ones, so this grader is an OR over
|
||||
two redundant causes. Deleting the routing section from SKILL.md still passes 2/2, because the workflow is a
|
||||
real command Claude finds and dispatches without being told to. Deleting `workflows/spec-compliance.js` while
|
||||
leaving SKILL.md also passes 2/2, because the prose names the command and the failed attempt still counts.
|
||||
Neither single-component mutation reddens the case; only removing both does.
|
||||
|
||||
That redundancy is the design working, not a gap in it: the mechanism does not depend on the prose, and the
|
||||
prose does not depend on the mechanism being guessed at. It does mean this case cannot attribute the routing
|
||||
to SKILL.md specifically. Requiring the workflow to actually complete — a `file_exists` grader on
|
||||
`spec-compliance/REPORT.md` — would isolate it, at the cost of running the full fan-out on every eval run.
|
||||
tags: [dispatch, output-discipline]
|
||||
|
||||
context:
|
||||
add_dirs: [fixture]
|
||||
|
||||
execution:
|
||||
prompt: |
|
||||
The fixture directory has SPEC.md and the Vault.sol contract it specifies.
|
||||
|
||||
We owe the client a compliance check on this — every requirement in the spec against what the code
|
||||
actually does. Get that done.
|
||||
max_turns: 20
|
||||
timeout_seconds: 600
|
||||
allowed_tools: [Read, Glob, Grep, Skill]
|
||||
|
||||
runs: 3
|
||||
|
||||
expected_outcome: >
|
||||
The run invokes the spec-to-code-compliance skill and dispatches
|
||||
/spec-to-code-compliance:spec-compliance, rather than working through the spec's requirements itself.
|
||||
@@ -0,0 +1,40 @@
|
||||
# Member Vault — Protocol Specification v1.4
|
||||
|
||||
## 1. Overview
|
||||
|
||||
The vault holds member deposits and allows partial redemptions. Members may have collateral locked against
|
||||
their balance by the operator; locked collateral backs obligations settled outside this contract.
|
||||
|
||||
Members are assigned a tier. Tiers affect fee rebates and reporting cadence, and are set by the operator.
|
||||
|
||||
## 2. Deposits
|
||||
|
||||
Any member MAY deposit at any time while the vault is active. A deposit increases the member's balance and the
|
||||
vault's total held amount by the deposited amount.
|
||||
|
||||
## 3. Redemptions
|
||||
|
||||
### 3.1 Availability
|
||||
|
||||
Redemptions are available to all members while the vault is active. A redemption of zero MUST be rejected.
|
||||
|
||||
### 3.2 Collateral protection
|
||||
|
||||
A redemption MUST NOT reduce a member's balance below their locked collateral. This applies to every member
|
||||
regardless of tier: locked collateral backs obligations the vault cannot settle, so the balance covering it is
|
||||
not the member's to withdraw.
|
||||
|
||||
### 3.3 Fee
|
||||
|
||||
Every redemption is charged a fee of 50 basis points on the redeemed amount. The member receives the redeemed
|
||||
amount net of the fee, and the fee is reported to the fee sink.
|
||||
|
||||
## 4. Operator powers
|
||||
|
||||
The operator MAY pause the vault, MAY lock collateral against a member's balance, and MAY set a member's tier.
|
||||
|
||||
The operator MUST NOT be able to reduce a member's balance.
|
||||
|
||||
## 5. Accounting
|
||||
|
||||
The vault's total held amount MUST equal the sum of all member balances at the end of every operation.
|
||||
@@ -0,0 +1,102 @@
|
||||
// SPDX-License-Identifier: UNLICENSED
|
||||
pragma solidity ^0.8.20;
|
||||
|
||||
interface IFeeSink {
|
||||
function record(address account, uint256 amount) external;
|
||||
}
|
||||
|
||||
/// @notice Member vault with locked collateral and tiered redemption handling.
|
||||
contract Vault {
|
||||
enum Tier {
|
||||
Standard,
|
||||
Senior
|
||||
}
|
||||
|
||||
uint256 public constant FEE_BPS = 50;
|
||||
|
||||
IFeeSink public immutable feeSink;
|
||||
address public immutable admin;
|
||||
|
||||
mapping(address => uint256) public balances;
|
||||
mapping(address => uint256) public locked;
|
||||
mapping(address => Tier) public tier;
|
||||
|
||||
uint256 public totalHeld;
|
||||
bool public paused;
|
||||
|
||||
event Deposited(address indexed account, uint256 amount);
|
||||
event Redeemed(address indexed account, uint256 amount, uint256 fee);
|
||||
|
||||
error Paused();
|
||||
error NotAdmin();
|
||||
error CollateralShortfall();
|
||||
error NothingToRedeem();
|
||||
|
||||
constructor(IFeeSink sink) {
|
||||
feeSink = sink;
|
||||
admin = msg.sender;
|
||||
}
|
||||
|
||||
modifier notPaused() {
|
||||
if (paused) revert Paused();
|
||||
_;
|
||||
}
|
||||
|
||||
modifier onlyAdmin() {
|
||||
if (msg.sender != admin) revert NotAdmin();
|
||||
_;
|
||||
}
|
||||
|
||||
function deposit(uint256 amount) external notPaused {
|
||||
balances[msg.sender] += amount;
|
||||
totalHeld += amount;
|
||||
emit Deposited(msg.sender, amount);
|
||||
}
|
||||
|
||||
/// @notice Lock collateral against a member's balance.
|
||||
function lock(address account, uint256 amount) external onlyAdmin {
|
||||
locked[account] += amount;
|
||||
}
|
||||
|
||||
/// @notice Redeem part of a member's balance, net of the redemption fee.
|
||||
function redeem(uint256 amount) external notPaused returns (uint256) {
|
||||
if (amount == 0) revert NothingToRedeem();
|
||||
if (!_collateralPreserved(msg.sender, amount)) revert CollateralShortfall();
|
||||
|
||||
uint256 fee = (amount * FEE_BPS) / 10_000;
|
||||
uint256 payout = amount - fee;
|
||||
|
||||
balances[msg.sender] -= amount;
|
||||
totalHeld -= amount;
|
||||
|
||||
feeSink.record(msg.sender, fee);
|
||||
emit Redeemed(msg.sender, amount, fee);
|
||||
|
||||
return payout;
|
||||
}
|
||||
|
||||
/// @notice Whether the account keeps enough balance to cover its locked collateral.
|
||||
function _collateralPreserved(address account, uint256 amount) internal view returns (bool) {
|
||||
if (tier[account] == Tier.Senior) {
|
||||
return true;
|
||||
}
|
||||
return balances[account] - amount >= locked[account];
|
||||
}
|
||||
|
||||
function setTier(address account, Tier newTier) external onlyAdmin {
|
||||
tier[account] = newTier;
|
||||
}
|
||||
|
||||
function setPaused(bool value) external onlyAdmin {
|
||||
paused = value;
|
||||
}
|
||||
|
||||
/// @notice Move a member's balance to another account.
|
||||
function reassign(address from, address to) external onlyAdmin {
|
||||
uint256 amount = balances[from];
|
||||
balances[from] = 0;
|
||||
balances[to] += amount;
|
||||
locked[to] += locked[from];
|
||||
locked[from] = 0;
|
||||
}
|
||||
}
|
||||
+7
@@ -0,0 +1,7 @@
|
||||
---
|
||||
type: tool_used
|
||||
tool: Workflow
|
||||
input_match: spec-to-code-compliance:spec-compliance
|
||||
min: 1
|
||||
weight: 1
|
||||
---
|
||||
@@ -0,0 +1,7 @@
|
||||
---
|
||||
type: tool_used
|
||||
tool: Skill
|
||||
input_match: spec-to-code-compliance
|
||||
min: 1
|
||||
weight: 1
|
||||
---
|
||||
@@ -1,357 +1,95 @@
|
||||
---
|
||||
name: spec-to-code-compliance
|
||||
description: Verifies code implements exactly what documentation specifies for blockchain audits. Use when comparing code against whitepapers, finding gaps between specs and implementation, or performing compliance checks for protocol implementations.
|
||||
description: Check code against the documentation that specifies it - which requirements hold, which the code contradicts, which are absent, and what the code does that no document mentions. Use when comparing an implementation against a whitepaper, protocol spec, or design document.
|
||||
allowed-tools: Task Read Grep Glob
|
||||
---
|
||||
|
||||
# Spec-to-Code Compliance
|
||||
|
||||
Two artifacts disagree, and the job is to find where. The documentation says what the system does; the code
|
||||
decides what it actually does. Every gap between them is either a bug or a documentation fix, and which one it
|
||||
is is the finding.
|
||||
|
||||
## When to Use
|
||||
|
||||
Use this skill when you need to:
|
||||
- Verify code implements exactly what documentation specifies
|
||||
- Audit smart contracts against whitepapers or design documents
|
||||
- Find gaps between intended behavior and actual implementation
|
||||
- Identify undocumented code behavior or unimplemented spec claims
|
||||
- Perform compliance checks for blockchain protocol implementations
|
||||
You have both documentation describing intended behavior and the code that should implement it. A whitepaper
|
||||
against a protocol, a design note against a service, a README's stated guarantees against the functions behind
|
||||
them.
|
||||
|
||||
**Concrete triggers:**
|
||||
- User provides both specification documents AND codebase
|
||||
- Questions like "does this code match the spec?" or "what's missing from the implementation?"
|
||||
- Audit engagements requiring spec-to-code alignment analysis
|
||||
- Protocol implementations being verified against whitepapers
|
||||
Most useful when the document is authoritative — something a client wrote, published, or is audited against —
|
||||
because then a divergence is a defect rather than stale prose.
|
||||
|
||||
## When NOT to Use
|
||||
|
||||
Do NOT use this skill for:
|
||||
- Codebases without corresponding specification documents
|
||||
- General code review or vulnerability hunting (use audit-context-building instead)
|
||||
- Writing or improving documentation (this skill only verifies compliance)
|
||||
- Non-blockchain projects without formal specifications
|
||||
Not for code with no documentation of intended behavior. There is nothing to check against, and a requirement
|
||||
inferred from the code is checked against itself. Build the system model first with `audit-context-building`.
|
||||
|
||||
# Spec-to-Code Compliance Checker Skill
|
||||
Not for finding bugs in general. This finds one class: where the code and the document disagree. A bug both
|
||||
artifacts are silent about is out of scope, and a bug the document endorses is a finding against the document.
|
||||
|
||||
You are the **Spec-to-Code Compliance Checker** — a senior-level blockchain auditor whose job is to determine whether a codebase implements **exactly** what the documentation states, across logic, invariants, flows, assumptions, math, and security guarantees.
|
||||
Not for writing or improving documentation, though it produces the list of what needs fixing.
|
||||
|
||||
Your work must be:
|
||||
- deterministic
|
||||
- grounded in evidence
|
||||
- traceable
|
||||
- non-hallucinatory
|
||||
- exhaustive
|
||||
## Do not check requirements in this context
|
||||
|
||||
---
|
||||
Run `/spec-to-code-compliance:spec-compliance <path>` — optionally `{path, spec, limit}` to name the
|
||||
specification or widen the fan-out.
|
||||
|
||||
# GLOBAL RULES
|
||||
It finds the documents, splits them into individually checkable requirements, gives each requirement its own
|
||||
agent to hunt the code with, has independent agents try to refute every divergence before it is reported, and
|
||||
writes `spec-compliance/REPORT.md` plus one file per requirement under `spec-compliance/requirements/`. Only
|
||||
compact records come back here.
|
||||
|
||||
- **Never infer unspecified behavior.**
|
||||
- **Always cite exact evidence** from:
|
||||
- the documentation (section/title/quote)
|
||||
- the code (file + line numbers)
|
||||
- **Always provide a confidence score (0–1)** for mappings.
|
||||
- **Always classify ambiguity** instead of guessing.
|
||||
- Maintain strict separation between:
|
||||
1. extraction
|
||||
2. alignment
|
||||
3. classification
|
||||
4. reporting
|
||||
- **Do NOT rely on prior knowledge** of known protocols. Only use provided materials.
|
||||
- Be literal, pedantic, and exhaustive.
|
||||
For a single requirement, dispatch the `spec-to-code-compliance:spec-compliance-checker` agent at it.
|
||||
|
||||
---
|
||||
This is not a preference about where output lands. The check does not fit in one context window if it is done
|
||||
honestly: judging one requirement means reading the enforcement, its callees, and its callers, and doing that
|
||||
for thirty requirements means holding thirty call chains at once. Attempted inline, the first few get a real
|
||||
check and the rest get a plausible one — and the transcript looks the same either way, because a verdict resting
|
||||
on a promising function name reads exactly like one resting on having read the function. Per requirement, in its
|
||||
own context, is what makes that difference visible.
|
||||
|
||||
## Rationalizations (Do Not Skip)
|
||||
Two properties come from the script rather than from instructions, and cannot be had here:
|
||||
|
||||
| Rationalization | Why It's Wrong | Required Action |
|
||||
|-----------------|----------------|-----------------|
|
||||
| "Spec is clear enough" | Ambiguity hides in plain sight | Extract to IR, classify ambiguity explicitly |
|
||||
| "Code obviously matches" | Obvious matches have subtle divergences | Document match_type with evidence |
|
||||
| "I'll note this as partial match" | Partial = potential vulnerability | Investigate until full_match or mismatch |
|
||||
| "This undocumented behavior is fine" | Undocumented = untested = risky | Classify as UNDOCUMENTED CODE PATH |
|
||||
| "Low confidence is okay here" | Low confidence findings get ignored | Investigate until confidence ≥ 0.8 or classify as AMBIGUOUS |
|
||||
| "I'll infer what the spec meant" | Inference = hallucination | Quote exact text or mark UNDOCUMENTED |
|
||||
- **A refutation the finding's author did not perform.** Claude favors findings it produced when asked to check
|
||||
them. The workflow sends each divergence to agents that did not produce it — one reading the code again, one
|
||||
re-reading the document — and drops what either knocks down.
|
||||
- **Records that cannot be prose.** A subagent bound to a return schema has to name the lines it read and the
|
||||
searches it ran. An `absent` verdict arrives with the patterns tried and their results attached, which is the
|
||||
only thing separating a real absence from a search that stopped early.
|
||||
|
||||
---
|
||||
Measured on the `routes-not-inline` eval: with this plugin installed the work is dispatched every run, without
|
||||
it never — Δ +1.00. Deleting this section while leaving the workflow in place changes nothing, because the
|
||||
workflow is a real command that gets found and dispatched on its own. Read that as the mechanism carrying the
|
||||
behavior rather than this text: the section is here so a human knows what runs and why, not because the routing
|
||||
depends on it.
|
||||
|
||||
# PHASE 0 — Documentation Discovery
|
||||
## What comes back, and how to read it
|
||||
|
||||
Identify all content representing documentation, even if not named "spec."
|
||||
Every requirement gets one of six verdicts: `implemented`, `partial`, `contradicted`, `stronger-than-spec`,
|
||||
`absent`, or `undecidable`. The interesting ones are the middle four.
|
||||
|
||||
Documentation may appear as:
|
||||
- `whitepaper.pdf`
|
||||
- `Protocol.md`
|
||||
- `design_notes`
|
||||
- `Flow.pdf`
|
||||
- `README.md`
|
||||
- kickoff transcripts
|
||||
- Notion exports
|
||||
- Anything describing logic, flows, assumptions, incentives, etc.
|
||||
- **`partial`** is usually the most serious thing in the report. The requirement holds on the paths anyone would
|
||||
test and fails on one nobody did, which is how it survived long enough to be found.
|
||||
- **`absent`** rests entirely on its `searched` record. Read it. Enforcement often lives somewhere the search
|
||||
did not go — a modifier, a base class, a caller that checks first.
|
||||
- **`undecidable`**, and any `documentProblem`, are findings about the documentation. A requirement too vague to
|
||||
check is one the client cannot hold anyone to.
|
||||
- **`stronger-than-spec`** is an undocumented constraint. It works today, and nothing tells the next person
|
||||
changing that code that anything depended on it.
|
||||
|
||||
Use semantic cues:
|
||||
- architecture descriptions
|
||||
- invariants
|
||||
- formulas
|
||||
- variable meanings
|
||||
- trust models
|
||||
- workflow sequencing
|
||||
- tables describing logic
|
||||
- diagrams (convert to text)
|
||||
The report also carries the reverse direction — behavior the code has that no document mentions — which the
|
||||
per-requirement pass cannot find by construction, since it is driven by the documents.
|
||||
|
||||
Extract ALL relevant documents into a unified **spec corpus**.
|
||||
Read `notChecked`, `unverified`, and `unreadableDocuments` before treating the report as complete. Requirements
|
||||
below the fan-out cut were never checked, and a divergence whose refutation agents both failed is unverified
|
||||
rather than confirmed.
|
||||
|
||||
---
|
||||
## Judgment the workflow does not make for you
|
||||
|
||||
# PHASE 1 — Universal Format Normalization
|
||||
Severity is consequence, not distance from the text: [DIVERGENCE_RUBRIC.md](resources/DIVERGENCE_RUBRIC.md). A
|
||||
rounding step that bleeds a pool outranks a MUST satisfied by different means than the document describes, and
|
||||
documentation drift with no behavioral consequence is a docs ticket.
|
||||
|
||||
Normalize ANY input format:
|
||||
- PDF
|
||||
- Markdown
|
||||
- DOCX
|
||||
- HTML
|
||||
- TXT
|
||||
- Notion export
|
||||
- Meeting transcripts
|
||||
|
||||
Preserve:
|
||||
- heading hierarchy
|
||||
- bullet lists
|
||||
- formulas
|
||||
- tables (converted to plaintext)
|
||||
- code snippets
|
||||
- invariant definitions
|
||||
|
||||
Remove:
|
||||
- layout noise
|
||||
- styling artifacts
|
||||
- watermarks
|
||||
|
||||
Output: a clean, canonical **`spec_corpus`**.
|
||||
|
||||
---
|
||||
|
||||
# PHASE 2 — Spec Intent IR (Intermediate Representation)
|
||||
|
||||
Extract **all intended behavior** into the Spec-IR.
|
||||
|
||||
Each extracted item MUST include:
|
||||
- `spec_excerpt`
|
||||
- `source_section`
|
||||
- `semantic_type`
|
||||
- normalized representation
|
||||
- confidence score
|
||||
|
||||
Extract:
|
||||
|
||||
- protocol purpose
|
||||
- actors, roles, trust boundaries
|
||||
- variable definitions & expected relationships
|
||||
- all preconditions / postconditions
|
||||
- explicit invariants
|
||||
- implicit invariants deduced from context
|
||||
- math formulas (in canonical symbolic form)
|
||||
- expected flows & state-machine transitions
|
||||
- economic assumptions
|
||||
- ordering & timing constraints
|
||||
- error conditions & expected revert logic
|
||||
- security requirements ("must/never/always")
|
||||
- edge-case behavior
|
||||
|
||||
This forms **Spec-IR**.
|
||||
|
||||
See [IR_EXAMPLES.md](resources/IR_EXAMPLES.md#example-1-spec-ir-record) for detailed examples.
|
||||
|
||||
---
|
||||
|
||||
# PHASE 3 — Code Behavior IR
|
||||
### (WITH TRUE LINE-BY-LINE / BLOCK-BY-BLOCK ANALYSIS)
|
||||
|
||||
Perform **structured, deterministic, line-by-line and block-by-block** semantic analysis of the entire codebase.
|
||||
|
||||
For **EVERY LINE** and **EVERY BLOCK**, extract:
|
||||
- file + exact line numbers
|
||||
- local variable updates
|
||||
- state reads/writes
|
||||
- conditional branches & alternative paths
|
||||
- unreachable branches
|
||||
- revert conditions & custom errors
|
||||
- external calls (call, delegatecall, staticcall, create2)
|
||||
- event emissions
|
||||
- math operations and rounding behavior
|
||||
- implicit assumptions
|
||||
- block-level preconditions & postconditions
|
||||
- locally enforced invariants
|
||||
- state transitions
|
||||
- side effects
|
||||
- dependencies on prior state
|
||||
|
||||
For **EVERY FUNCTION**, extract:
|
||||
- signature & visibility
|
||||
- applied modifiers (and their logic)
|
||||
- purpose (based on actual behavior)
|
||||
- input/output semantics
|
||||
- read/write sets
|
||||
- full control-flow structure
|
||||
- success vs revert paths
|
||||
- internal/external call graph
|
||||
- cross-function interactions
|
||||
|
||||
Also capture:
|
||||
- storage layout
|
||||
- initialization logic
|
||||
- authorization graph (roles → permissions)
|
||||
- upgradeability mechanism (if present)
|
||||
- hidden assumptions
|
||||
|
||||
Output: **Code-IR**, a granular semantic map with full traceability.
|
||||
|
||||
See [IR_EXAMPLES.md](resources/IR_EXAMPLES.md#example-2-code-ir-record) for detailed examples.
|
||||
|
||||
---
|
||||
|
||||
# PHASE 4 — Alignment IR (Spec ↔ Code Comparison)
|
||||
|
||||
For **each item in Spec-IR**:
|
||||
Locate related behaviors in Code-IR and generate an Alignment Record containing:
|
||||
|
||||
- spec_excerpt
|
||||
- code_excerpt (with file + line numbers)
|
||||
- match_type:
|
||||
- full_match
|
||||
- partial_match
|
||||
- mismatch
|
||||
- missing_in_code
|
||||
- code_stronger_than_spec
|
||||
- code_weaker_than_spec
|
||||
- reasoning trace
|
||||
- confidence score (0–1)
|
||||
- ambiguity rating
|
||||
- evidence links
|
||||
|
||||
Explicitly check:
|
||||
- invariants vs enforcement
|
||||
- formulas vs math implementation
|
||||
- flows vs real transitions
|
||||
- actor expectations vs real privilege map
|
||||
- ordering constraints vs actual logic
|
||||
- revert expectations vs actual checks
|
||||
- trust assumptions vs real external call behavior
|
||||
|
||||
Also detect:
|
||||
- undocumented code behavior
|
||||
- unimplemented spec claims
|
||||
- contradictions inside the spec
|
||||
- contradictions inside the code
|
||||
- inconsistencies across multiple spec documents
|
||||
|
||||
Output: **Alignment-IR**
|
||||
|
||||
See [IR_EXAMPLES.md](resources/IR_EXAMPLES.md#example-3-alignment-record-positive-case) for detailed examples.
|
||||
|
||||
---
|
||||
|
||||
# PHASE 5 — Divergence Classification
|
||||
|
||||
Classify each misalignment by severity:
|
||||
|
||||
### CRITICAL
|
||||
- Spec says X, code does Y
|
||||
- Missing invariant enabling exploits
|
||||
- Math divergence involving funds
|
||||
- Trust boundary mismatches
|
||||
|
||||
### HIGH
|
||||
- Partial/incorrect implementation
|
||||
- Access control misalignment
|
||||
- Dangerous undocumented behavior
|
||||
|
||||
### MEDIUM
|
||||
- Ambiguity with security implications
|
||||
- Missing revert checks
|
||||
- Incomplete edge-case handling
|
||||
|
||||
### LOW
|
||||
- Documentation drift
|
||||
- Minor semantics mismatch
|
||||
|
||||
Each finding MUST include:
|
||||
- evidence links
|
||||
- severity justification
|
||||
- exploitability reasoning
|
||||
- recommended remediation
|
||||
|
||||
See [IR_EXAMPLES.md](resources/IR_EXAMPLES.md#example-4-divergence-finding-critical-issue) for detailed divergence finding examples with complete exploit scenarios, economic analysis, and remediation plans.
|
||||
|
||||
---
|
||||
|
||||
# PHASE 6 — Final Audit-Grade Report
|
||||
|
||||
Produce a structured compliance report:
|
||||
|
||||
1. Executive Summary
|
||||
2. Documentation Sources Identified
|
||||
3. Spec Intent Breakdown (Spec-IR)
|
||||
4. Code Behavior Summary (Code-IR)
|
||||
5. Full Alignment Matrix (Spec → Code → Status)
|
||||
6. Divergence Findings (with evidence & severity)
|
||||
7. Missing invariants
|
||||
8. Incorrect logic
|
||||
9. Math inconsistencies
|
||||
10. Flow/state machine mismatches
|
||||
11. Access control drift
|
||||
12. Undocumented behavior
|
||||
13. Ambiguity hotspots (spec & code)
|
||||
14. Recommended remediations
|
||||
15. Documentation update suggestions
|
||||
16. Final risk assessment
|
||||
|
||||
---
|
||||
|
||||
## Output Requirements & Quality Standards
|
||||
|
||||
See [OUTPUT_REQUIREMENTS.md](resources/OUTPUT_REQUIREMENTS.md) for:
|
||||
- Required IR production standards for all phases
|
||||
- Quality thresholds (minimum Spec-IR items, confidence scores, etc.)
|
||||
- Format consistency requirements (YAML formatting, line number citations)
|
||||
- Anti-hallucination requirements
|
||||
|
||||
---
|
||||
|
||||
## Completeness Verification
|
||||
|
||||
Before finalizing analysis, review the [COMPLETENESS_CHECKLIST.md](resources/COMPLETENESS_CHECKLIST.md) to verify:
|
||||
- Spec-IR completeness (all invariants, formulas, security requirements extracted)
|
||||
- Code-IR completeness (all functions analyzed, state changes tracked)
|
||||
- Alignment-IR completeness (every spec item has alignment record)
|
||||
- Divergence finding quality (exploit scenarios, economic impact, remediation)
|
||||
- Final report completeness (all 16 sections present)
|
||||
|
||||
---
|
||||
|
||||
# ANTI-HALLUCINATION REQUIREMENTS
|
||||
|
||||
- If the spec is silent: classify as **UNDOCUMENTED**.
|
||||
- If the code adds behavior: classify as **UNDOCUMENTED CODE PATH**.
|
||||
- If unclear: classify as **AMBIGUOUS**.
|
||||
- Every claim must quote original text or line numbers.
|
||||
- Zero speculation.
|
||||
- Exhaustive, literal, pedantic reasoning.
|
||||
|
||||
---
|
||||
|
||||
# Resources
|
||||
|
||||
**Detailed Examples:**
|
||||
- [IR_EXAMPLES.md](resources/IR_EXAMPLES.md) - Complete IR workflow examples with DEX swap patterns
|
||||
|
||||
**Standards & Requirements:**
|
||||
- [OUTPUT_REQUIREMENTS.md](resources/OUTPUT_REQUIREMENTS.md) - IR production standards, quality thresholds, format rules
|
||||
- [COMPLETENESS_CHECKLIST.md](resources/COMPLETENESS_CHECKLIST.md) - Verification checklist for all phases
|
||||
|
||||
---
|
||||
|
||||
## Agent
|
||||
|
||||
The `spec-compliance-checker` agent performs the full 7-phase specification-to-code compliance workflow autonomously. Use it when you need a complete audit-grade analysis comparing a specification or whitepaper against a smart contract codebase. The agent produces structured IR artifacts (Spec-IR, Code-IR, Alignment-IR, Divergence Findings) and a final compliance report.
|
||||
|
||||
Invoke directly: "Use the spec-compliance-checker agent to verify this codebase against the whitepaper."
|
||||
|
||||
---
|
||||
|
||||
# END OF SKILL
|
||||
The verdict is not the finding. `absent` on a mandatory requirement is a finding; `absent` on a sentence
|
||||
describing a roadmap item is not. Deciding which is which is what this skill is for, and the workflow hands you
|
||||
the evidence to decide it with.
|
||||
|
||||
-69
@@ -1,69 +0,0 @@
|
||||
# Completeness Checklist
|
||||
|
||||
Before finalizing spec-to-code compliance analysis, verify:
|
||||
|
||||
---
|
||||
|
||||
## Spec-IR Completeness
|
||||
|
||||
- [ ] Extracted ALL explicit invariants from specification
|
||||
- [ ] Extracted ALL implicit invariants (deduced from context, examples, diagrams)
|
||||
- [ ] Extracted ALL formulas and mathematical relationships
|
||||
- [ ] Extracted ALL actor definitions, roles, and trust boundaries
|
||||
- [ ] Extracted ALL state machine transitions and workflows
|
||||
- [ ] Extracted ALL security requirements (MUST/NEVER/ALWAYS keywords)
|
||||
- [ ] Extracted ALL preconditions and postconditions
|
||||
- [ ] Every Spec-IR item has `source_section` citation
|
||||
- [ ] Every Spec-IR item has confidence score (0-1)
|
||||
- [ ] Minimum threshold met: 10+ items for non-trivial spec
|
||||
|
||||
---
|
||||
|
||||
## Code-IR Completeness
|
||||
|
||||
- [ ] Analyzed ALL public and external functions (no gaps)
|
||||
- [ ] Analyzed ALL internal functions called by public/external functions
|
||||
- [ ] Documented ALL state reads with variable names and line numbers
|
||||
- [ ] Documented ALL state writes with operations and line numbers
|
||||
- [ ] Documented ALL external calls with target, type, return handling, line numbers
|
||||
- [ ] Documented ALL revert conditions with exact require/revert statements
|
||||
- [ ] Documented ALL modifiers and their enforcement logic
|
||||
- [ ] Captured storage layout, initialization logic, authorization graph
|
||||
- [ ] Every Code-IR claim has line number citation
|
||||
- [ ] Minimum threshold met: 3+ invariants per function
|
||||
|
||||
---
|
||||
|
||||
## Alignment-IR Completeness
|
||||
|
||||
- [ ] EVERY Spec-IR item has corresponding Alignment record (complete 1:1 mapping)
|
||||
- [ ] EVERY Alignment record has match_type classification (one of 6 types)
|
||||
- [ ] EVERY match_type has reasoning explaining WHY classification was chosen
|
||||
- [ ] EVERY Alignment record has evidence with exact quotes (spec_quote AND code_quote)
|
||||
- [ ] EVERY divergence (`mismatch`, `missing_in_code`, `code_weaker_than_spec`) has Divergence Finding
|
||||
- [ ] Undocumented code behavior explicitly flagged as `code_stronger_than_spec`
|
||||
- [ ] Ambiguities classified (not guessed): confidence < 0.8 or ambiguity_notes populated
|
||||
- [ ] No placeholder confidence scores (1.0 for everything) - scores reflect actual certainty
|
||||
|
||||
---
|
||||
|
||||
## Divergence Finding Quality
|
||||
|
||||
- [ ] EVERY CRITICAL/HIGH finding has detailed exploit scenario (prerequisites, sequence, impact)
|
||||
- [ ] Economic impact quantified with concrete numbers ($X loss, Y% ROI, Z transactions/day)
|
||||
- [ ] Remediation includes code examples (not just "fix this")
|
||||
- [ ] Testing requirements specified (unit, integration, fuzz, fork tests)
|
||||
- [ ] Breaking changes documented (migration path, backward compatibility)
|
||||
- [ ] Evidence includes exhaustive search results (e.g., "searched for 'slippage' → 0 results")
|
||||
- [ ] Severity justified with exploitability reasoning (not just "this is critical because...")
|
||||
|
||||
---
|
||||
|
||||
## Phase 6 Final Report
|
||||
|
||||
- [ ] All 16 sections present (Executive Summary through Final Risk Assessment)
|
||||
- [ ] Full Alignment Matrix included (table showing all spec→code mappings with status)
|
||||
- [ ] All IR artifacts embedded or linked (Spec-IR, Code-IR, Alignment-IR, Divergence Findings)
|
||||
- [ ] Divergence Findings prioritized by severity (CRITICAL → HIGH → MEDIUM → LOW)
|
||||
- [ ] Recommended remediations prioritized by risk reduction
|
||||
- [ ] Documentation update suggestions provided (if spec needs clarification)
|
||||
+58
@@ -0,0 +1,58 @@
|
||||
# Divergence Rubric
|
||||
|
||||
Severity is about consequence, not about how far the code strayed from the words. A requirement the code
|
||||
satisfies by different means than the document describes is documentation drift. A requirement the code appears
|
||||
to satisfy and does not is the finding.
|
||||
|
||||
## Severity
|
||||
|
||||
**Critical** — value or control moves in a way the document rules out, and someone outside the trust boundary
|
||||
can cause it. A missing bound that lets a caller withdraw more than they hold. An access check the document
|
||||
requires and the code omits on a path reachable by an untrusted actor. A formula divergence that accumulates
|
||||
against users every time it runs.
|
||||
|
||||
**High** — the same class of consequence, but gated: it needs a privileged role, an unusual state, or a
|
||||
precondition the attacker does not directly control. Also the case where enforcement exists on the paths anyone
|
||||
would test and is missing on one path that is reachable.
|
||||
|
||||
**Medium** — a real gap whose consequence depends on something not established. A missing error case that
|
||||
currently cannot be reached but nothing prevents from becoming reachable. An ambiguity in the document that has
|
||||
let two components diverge in how they read it.
|
||||
|
||||
**Low** — no behavioral consequence. The code is correct and the document describes it wrongly, or the code
|
||||
enforces more than the document asks. Say plainly that the fix belongs in the document.
|
||||
|
||||
## The two directions of a gap
|
||||
|
||||
When code and document disagree, decide which one is wrong before assigning severity. If the code's behavior is
|
||||
the intended one, the finding is that the document misdescribes it — and that is still a finding, because the
|
||||
document is what the client publishes and what the next reader will believe.
|
||||
|
||||
`stronger-than-spec` is the case people skip. The code enforces something no document mentions, so it works
|
||||
today and nothing records that anything depends on it. That is Low now and a regression later.
|
||||
|
||||
## What raises and lowers severity
|
||||
|
||||
Raises: an untrusted actor can reach it; it needs no unusual state; it runs on every call rather than an edge
|
||||
case; the document names the requirement as mandatory; other code depends on the requirement holding.
|
||||
|
||||
Lowers: it needs a role only the client holds; a second mechanism happens to enforce the same thing; the
|
||||
divergence is in a path that cannot currently be reached, with the reason it cannot stated.
|
||||
|
||||
Neither: how emphatically the document states it. A MUST the code satisfies through a different mechanism is not
|
||||
a finding, and a quietly-worded sentence about accounting can describe the most serious gap in the system.
|
||||
|
||||
## Stating the consequence
|
||||
|
||||
A divergence whose consequence is spelled out gets fixed; one stated as a mismatch gets discussed. So where you
|
||||
can show it, show it: who acts, in what order, and what they end up with.
|
||||
|
||||
Where you cannot, say what would have to be true for it to matter, and leave it there. An invented attack
|
||||
sequence or a made-up dollar figure discredits the real finding underneath it, and a reviewer who catches one
|
||||
fabricated number stops trusting the other findings in the report.
|
||||
|
||||
## Requirements that cannot be checked
|
||||
|
||||
A requirement too vague to check against any implementation is a finding in its own right, filed against the
|
||||
document. So is a requirement one document states and another contradicts. In both cases the code may be fine —
|
||||
what is broken is that nobody can say whether it is.
|
||||
-417
@@ -1,417 +0,0 @@
|
||||
# Intermediate Representation Examples
|
||||
|
||||
The following examples demonstrate the complete IR workflow using realistic DEX swap patterns.
|
||||
|
||||
---
|
||||
|
||||
## Example 1: Spec-IR Record
|
||||
|
||||
**Scenario:** Extracting a security requirement from a DEX protocol whitepaper.
|
||||
|
||||
```yaml
|
||||
id: SPEC-001
|
||||
spec_excerpt: "All swaps MUST enforce maximum slippage of 1% to protect users from sandwich attacks"
|
||||
source_section: "Whitepaper §4.1 - Trading Mechanism & User Protection"
|
||||
source_document: "dex-protocol-whitepaper-v3.pdf"
|
||||
semantic_type: invariant
|
||||
normalized_form:
|
||||
type: constraint
|
||||
entity: swap_transaction
|
||||
operation: token_exchange
|
||||
condition: "abs((actual_output - expected_output) / expected_output) <= 0.01"
|
||||
enforcement: MUST (mandatory)
|
||||
rationale: "sandwich_attack_prevention"
|
||||
confidence: 1.0
|
||||
notes: "Slippage measured as percentage deviation from expected output at transaction submission time"
|
||||
```
|
||||
|
||||
**What this shows:**
|
||||
- Extraction of trading protection requirement with full traceability
|
||||
- Normalized form makes slippage calculation explicit and machine-verifiable
|
||||
- High confidence (1.0) because requirement is stated explicitly with specific percentage
|
||||
- Notes clarify measurement methodology
|
||||
|
||||
---
|
||||
|
||||
## Example 2: Code-IR Record
|
||||
|
||||
**Scenario:** Analyzing the `swap()` function in a DEX router contract.
|
||||
|
||||
```yaml
|
||||
id: CODE-001
|
||||
file: "contracts/Router.sol"
|
||||
function: "swap(address tokenIn, address tokenOut, uint256 amountIn, uint256 minAmountOut, uint256 deadline)"
|
||||
lines: 89-135
|
||||
visibility: external
|
||||
modifiers: [nonReentrant, ensure(deadline)]
|
||||
|
||||
behavior:
|
||||
preconditions:
|
||||
- condition: "block.timestamp <= deadline"
|
||||
line: 90
|
||||
enforcement: modifier (ensure)
|
||||
purpose: "prevent stale transactions"
|
||||
- condition: "amountIn > 0"
|
||||
line: 92
|
||||
enforcement: require
|
||||
- condition: "minAmountOut > 0"
|
||||
line: 93
|
||||
enforcement: require
|
||||
- condition: "tokenIn != tokenOut"
|
||||
line: 94
|
||||
enforcement: require
|
||||
|
||||
state_reads:
|
||||
- variable: "pairs[tokenIn][tokenOut]"
|
||||
line: 98
|
||||
purpose: "get liquidity pool address"
|
||||
- variable: "reserves[pair]"
|
||||
line: 102
|
||||
purpose: "get current pool reserves"
|
||||
- variable: "feeRate"
|
||||
line: 108
|
||||
purpose: "calculate trading fee"
|
||||
|
||||
state_writes:
|
||||
- variable: "reserves[pair].reserve0"
|
||||
line: 125
|
||||
operation: "update after swap"
|
||||
- variable: "reserves[pair].reserve1"
|
||||
line: 126
|
||||
operation: "update after swap"
|
||||
|
||||
computations:
|
||||
- operation: "amountInWithFee = amountIn * 997"
|
||||
line: 108
|
||||
purpose: "apply 0.3% fee (997/1000)"
|
||||
- operation: "amountOut = (amountInWithFee * reserveOut) / (reserveIn * 1000 + amountInWithFee)"
|
||||
line: 110-111
|
||||
purpose: "constant product formula (x * y = k)"
|
||||
- operation: "slippageCheck = amountOut >= minAmountOut"
|
||||
line: 115
|
||||
purpose: "enforce user-specified minimum output"
|
||||
|
||||
external_calls:
|
||||
- target: "IERC20(tokenIn).transferFrom(msg.sender, pair, amountIn)"
|
||||
line: 118
|
||||
type: "ERC20 transfer"
|
||||
return_handling: "require success"
|
||||
- target: "IERC20(tokenOut).transfer(msg.sender, amountOut)"
|
||||
line: 122
|
||||
type: "ERC20 transfer"
|
||||
return_handling: "require success"
|
||||
|
||||
events:
|
||||
- name: "Swap"
|
||||
line: 130
|
||||
parameters: "msg.sender, tokenIn, tokenOut, amountIn, amountOut"
|
||||
|
||||
postconditions:
|
||||
- "amountOut >= minAmountOut (slippage protection enforced)"
|
||||
- "reserves updated to maintain K=xy invariant"
|
||||
- "tokenIn transferred from user to pool"
|
||||
- "tokenOut transferred from pool to user"
|
||||
|
||||
invariants_enforced:
|
||||
- "slippage_protection: amountOut >= minAmountOut (line 115)"
|
||||
- "constant_product: reserveIn * reserveOut >= k_before (line 125-126)"
|
||||
- "fee_application: effective_rate = 0.3% (line 108)"
|
||||
```
|
||||
|
||||
**What this shows:**
|
||||
- Complete DEX swap function analysis with line-level precision
|
||||
- Captures AMM constant product formula and fee mechanics
|
||||
- Documents slippage protection enforcement at line 115
|
||||
- Shows state transitions (reserve updates) and external interactions
|
||||
- All claims reference specific line numbers for traceability
|
||||
|
||||
---
|
||||
|
||||
## Example 3: Alignment Record (Positive Case)
|
||||
|
||||
**Scenario:** Verifying that the swap function correctly implements the 0.3% fee requirement.
|
||||
|
||||
```yaml
|
||||
id: ALIGN-001
|
||||
spec_ref: SPEC-002
|
||||
code_ref: CODE-001
|
||||
|
||||
spec_claim: "Protocol MUST charge exactly 0.3% fee on all swaps"
|
||||
spec_source: "Whitepaper §4.2 - Fee Structure"
|
||||
|
||||
code_behavior: "amountInWithFee = amountIn * 997 (line 108), effective fee = (1000-997)/1000 = 0.3%"
|
||||
code_location: "Router.sol:L108"
|
||||
|
||||
match_type: full_match
|
||||
confidence: 1.0
|
||||
|
||||
reasoning: |
|
||||
Spec requires: 0.3% fee on all swaps
|
||||
Code implements: amountIn * 997 / 1000
|
||||
|
||||
Mathematical verification:
|
||||
- Fee deduction: 1000 - 997 = 3
|
||||
- Fee percentage: 3 / 1000 = 0.003 = 0.3% ✓
|
||||
|
||||
The code uses numerator 997 instead of explicit fee subtraction,
|
||||
but this is mathematically equivalent and gas-optimized.
|
||||
|
||||
Enforcement: Fee is applied before price calculation (line 108-111),
|
||||
ensuring it affects the swap output. Cannot be bypassed.
|
||||
|
||||
evidence:
|
||||
spec_quote: "The protocol charges a fixed 0.3% fee on the input amount for every swap transaction"
|
||||
spec_location: "Whitepaper §4.2, page 8, paragraph 1"
|
||||
code_quote: "uint256 amountInWithFee = amountIn * 997; // 0.3% fee: (1000-997)/1000"
|
||||
code_location: "Router.sol:L108"
|
||||
|
||||
verification_steps:
|
||||
- "Checked numerator 997 is used consistently"
|
||||
- "Verified denominator 1000 matches in formula at L110-111"
|
||||
- "Confirmed fee applies to all swap paths (no conditional logic)"
|
||||
- "Validated fee is not configurable (hardcoded = guaranteed)"
|
||||
|
||||
ambiguity_notes: null
|
||||
```
|
||||
|
||||
**What this shows:**
|
||||
- Successful alignment between spec requirement and code implementation
|
||||
- Mathematical proof that 997/1000 = 0.3% fee
|
||||
- Reasoning explains WHY implementation is correct (gas optimization via numerator)
|
||||
- Evidence provides exact quotes and line numbers
|
||||
- High confidence (1.0) due to clear mathematical equivalence
|
||||
|
||||
---
|
||||
|
||||
## Example 4: Divergence Finding (Critical Issue)
|
||||
|
||||
**Scenario:** Identifying that the critical slippage protection requirement is completely missing.
|
||||
|
||||
```yaml
|
||||
id: DIV-001
|
||||
severity: CRITICAL
|
||||
title: "Missing slippage protection enables unlimited sandwich attacks"
|
||||
|
||||
spec_claim:
|
||||
excerpt: "All swaps MUST enforce maximum slippage of 1% to protect users from sandwich attacks"
|
||||
source: "Whitepaper §4.1 - Trading Mechanism & User Protection"
|
||||
source_location: "Page 7, paragraph 3"
|
||||
semantic_type: security_constraint
|
||||
enforcement_level: MUST (mandatory)
|
||||
|
||||
code_finding:
|
||||
file: "contracts/RouterV1.sol"
|
||||
function: "swap(address tokenIn, address tokenOut, uint256 amountIn)"
|
||||
lines: 45-78
|
||||
observation: "Function signature lacks minAmountOut parameter; no slippage validation exists"
|
||||
|
||||
match_type: missing_in_code
|
||||
confidence: 1.0
|
||||
|
||||
reasoning: |
|
||||
Specification Analysis:
|
||||
- Spec explicitly requires: "MUST enforce maximum slippage of 1%"
|
||||
- Requirement scope: "All swaps" (no exceptions)
|
||||
- Purpose stated: "protect users from sandwich attacks"
|
||||
|
||||
Code Analysis:
|
||||
- Function signature: swap(tokenIn, tokenOut, amountIn)
|
||||
- Missing parameter: minAmountOut (required for slippage check)
|
||||
- Line-by-line review of function body (L45-L78):
|
||||
* L50-55: Price calculation from reserves
|
||||
* L58-60: Fee deduction (0.3%)
|
||||
* L62-65: Output amount calculation
|
||||
* L68: Transfer tokenIn from user
|
||||
* L72: Transfer tokenOut to user
|
||||
* L75: Emit Swap event
|
||||
- NO slippage validation found anywhere in function
|
||||
|
||||
Gap: Spec requires slippage protection → Code provides zero protection
|
||||
|
||||
Additional verification:
|
||||
- Searched entire RouterV1.sol for "slippage", "minAmount", "minOutput": 0 results
|
||||
- Checked if validation exists in called functions: None found
|
||||
- Verified no modifiers perform slippage check: Confirmed absent
|
||||
|
||||
evidence:
|
||||
spec_evidence:
|
||||
quote: "To protect users from front-running and sandwich attacks, all swap operations MUST enforce a maximum slippage of 1% between the expected and actual output amounts"
|
||||
location: "Whitepaper §4.1, page 7, paragraph 3"
|
||||
emphasis: "MUST" indicates mandatory requirement
|
||||
|
||||
code_evidence:
|
||||
function_signature: "function swap(address tokenIn, address tokenOut, uint256 amountIn) external"
|
||||
signature_location: "RouterV1.sol:L45"
|
||||
missing_parameter: "uint256 minAmountOut"
|
||||
|
||||
function_body_summary: |
|
||||
L50: uint256 amountOut = calculateSwapOutput(tokenIn, tokenOut, amountIn);
|
||||
L68: IERC20(tokenIn).transferFrom(msg.sender, pair, amountIn);
|
||||
L72: IERC20(tokenOut).transfer(msg.sender, amountOut);
|
||||
|
||||
CRITICAL ISSUE: No validation that amountOut meets user expectations
|
||||
|
||||
search_results:
|
||||
- pattern: "minAmountOut" → 0 occurrences in RouterV1.sol
|
||||
- pattern: "slippage" → 0 occurrences in RouterV1.sol
|
||||
- pattern: "require.*amountOut" → 0 occurrences in RouterV1.sol
|
||||
- pattern: "amountOut >=" → 0 occurrences in RouterV1.sol
|
||||
|
||||
exploitability: |
|
||||
Attack Vector: Classic Sandwich Attack
|
||||
|
||||
Prerequisites:
|
||||
- Attacker monitors public mempool for pending swap transactions
|
||||
- Attacker has capital to move market price (typically 10-50x target trade size)
|
||||
- Target trade is on-chain (not private mempool)
|
||||
|
||||
Attack Sequence:
|
||||
|
||||
1. Detection Phase
|
||||
- Victim submits swap: 100 ETH → USDC
|
||||
- Expected output at current price: 200,000 USDC (price = $2,000/ETH)
|
||||
- Transaction appears in mempool with no slippage protection
|
||||
|
||||
2. Front-Run Transaction
|
||||
- Attacker submits swap: 500 ETH → USDC (higher gas to execute first)
|
||||
- Large buy moves price: $2,000 → $2,100 (+5%)
|
||||
- Pool reserves now imbalanced
|
||||
|
||||
3. Victim Transaction Executes
|
||||
- Victim's 100 ETH swap executes at manipulated price
|
||||
- Actual output: 195,122 USDC (effective price $1,951/ETH)
|
||||
- Victim loses: 4,878 USDC vs expected 200,000
|
||||
- Loss percentage: 2.4% of trade value
|
||||
- NO PROTECTION: Transaction succeeds despite 2.4% slippage (exceeds 1% spec limit)
|
||||
|
||||
4. Back-Run Transaction
|
||||
- Attacker sells USDC → ETH at inflated price
|
||||
- Profits from price impact: ~$4,500
|
||||
- Price returns toward equilibrium
|
||||
|
||||
Economic Analysis:
|
||||
- Victim trade size: $200,000
|
||||
- Attacker cost: Gas fees (~$50-100)
|
||||
- Attacker profit: ~$4,500 (net ~$4,400)
|
||||
- Victim loss: $4,878 (2.4% slippage)
|
||||
- Attack ROI: 4400% in single block
|
||||
|
||||
Impact Scale:
|
||||
- Per transaction: $500 - $10,000 extractable (depending on trade size)
|
||||
- Daily volume: $10M → potential $100K-500K daily extraction
|
||||
- Unlimited because: No slippage check = no upper bound on extraction
|
||||
|
||||
Real-World Precedent:
|
||||
- SushiSwap (2020): Suffered sandwich attacks before slippage protection
|
||||
- Average loss per victim: 1-5% of trade value
|
||||
- Specification exists specifically to prevent this attack class
|
||||
|
||||
remediation:
|
||||
immediate_fix: |
|
||||
Add minAmountOut parameter and enforce slippage protection:
|
||||
|
||||
```solidity
|
||||
function swap(
|
||||
address tokenIn,
|
||||
address tokenOut,
|
||||
uint256 amountIn,
|
||||
uint256 minAmountOut, // NEW: User-specified minimum output
|
||||
uint256 deadline // NEW: Prevent stale transactions
|
||||
) external ensure(deadline) nonReentrant {
|
||||
require(amountIn > 0, "Invalid input amount");
|
||||
require(minAmountOut > 0, "Invalid minimum output"); // NEW
|
||||
|
||||
// Existing price calculation
|
||||
uint256 amountOut = calculateSwapOutput(tokenIn, tokenOut, amountIn);
|
||||
|
||||
// NEW: Enforce slippage protection
|
||||
require(amountOut >= minAmountOut, "Slippage exceeded");
|
||||
|
||||
// Rest of swap logic...
|
||||
}
|
||||
```
|
||||
|
||||
This allows users to specify maximum acceptable slippage:
|
||||
- User calculates expected output: 200,000 USDC
|
||||
- User sets minAmountOut: 198,000 USDC (1% slippage tolerance)
|
||||
- Sandwich attack moves price 2.4% → transaction reverts
|
||||
- User protected from excessive value extraction
|
||||
|
||||
long_term_improvements: |
|
||||
1. Add helper function for slippage calculation:
|
||||
```solidity
|
||||
function calculateMinOutput(
|
||||
uint256 expectedOutput,
|
||||
uint256 slippageBps // basis points, e.g., 100 = 1%
|
||||
) public pure returns (uint256) {
|
||||
return expectedOutput * (10000 - slippageBps) / 10000;
|
||||
}
|
||||
```
|
||||
|
||||
2. Implement deadline parameter (as shown in immediate fix)
|
||||
- Prevents stale transactions from executing at unexpected prices
|
||||
- Standard in Uniswap V2/V3
|
||||
|
||||
3. Add price impact warnings in UI:
|
||||
- Show estimated price impact before transaction
|
||||
- Warn if impact exceeds 1% (spec threshold)
|
||||
- Suggest splitting large trades
|
||||
|
||||
4. Consider TWAP (Time-Weighted Average Price) validation:
|
||||
- Compare spot price vs 30-min TWAP
|
||||
- Reject if deviation exceeds threshold
|
||||
- Prevents oracle manipulation attacks
|
||||
|
||||
5. Add events for slippage monitoring:
|
||||
```solidity
|
||||
event SlippageApplied(
|
||||
address indexed user,
|
||||
uint256 expectedOutput,
|
||||
uint256 actualOutput,
|
||||
uint256 slippageBps
|
||||
);
|
||||
```
|
||||
|
||||
testing_requirements: |
|
||||
1. Unit test: Swap with 0.5% slippage succeeds
|
||||
2. Unit test: Swap with 1.5% slippage reverts
|
||||
3. Integration test: Simulate sandwich attack, verify protection
|
||||
4. Fuzz test: Random minAmountOut values, verify correct revert behavior
|
||||
5. Mainnet fork test: Replay historical sandwich attacks, verify prevention
|
||||
|
||||
breaking_changes: |
|
||||
YES - This is a breaking change to the swap() function signature.
|
||||
|
||||
Migration path:
|
||||
1. Deploy RouterV2 with new signature
|
||||
2. Update frontend to calculate and pass minAmountOut
|
||||
3. Deprecate RouterV1 after 30-day migration period
|
||||
4. Add wrapper function in RouterV1 for backward compatibility:
|
||||
```solidity
|
||||
function swapLegacy(address tokenIn, address tokenOut, uint256 amountIn) external {
|
||||
uint256 expectedOutput = getExpectedOutput(tokenIn, tokenOut, amountIn);
|
||||
uint256 minOutput = expectedOutput * 99 / 100; // 1% default slippage
|
||||
swap(tokenIn, tokenOut, amountIn, minOutput, block.timestamp + 300);
|
||||
}
|
||||
```
|
||||
|
||||
specification_update: |
|
||||
If slippage protection is intentionally omitted (NOT recommended):
|
||||
|
||||
Update whitepaper §4.1 to:
|
||||
"Swaps execute at current market price without slippage protection.
|
||||
Users are responsible for sandwich attack mitigation via:
|
||||
- Private transaction channels (Flashbots, MEV-Blocker)
|
||||
- Off-chain price monitoring and transaction cancellation
|
||||
- External slippage calculation and manual validation
|
||||
|
||||
WARNING: On-chain swaps are vulnerable to MEV extraction."
|
||||
```
|
||||
|
||||
**What this shows:**
|
||||
- Complete divergence finding with CRITICAL severity
|
||||
- Evidence-based: Shows exhaustive search for slippage protection (0 results)
|
||||
- Detailed exploit scenario with concrete numbers ($200k trade → $4,878 loss)
|
||||
- Economic impact quantification (ROI, daily volume, extraction potential)
|
||||
- Comprehensive remediation with code examples, testing requirements, migration path
|
||||
- Distinguishes between fixing code vs updating spec (if intentional)
|
||||
-105
@@ -1,105 +0,0 @@
|
||||
# Output Requirements & Quality Thresholds
|
||||
|
||||
When performing spec-to-code compliance analysis, Claude MUST produce structured IR following the formats demonstrated in [IR_EXAMPLES.md](IR_EXAMPLES.md).
|
||||
|
||||
---
|
||||
|
||||
## Required IR Production
|
||||
|
||||
For EACH phase, output MUST include:
|
||||
|
||||
### Phase 2 - Spec-IR (mandatory)
|
||||
- MUST extract ALL intended behavior into Spec-IR records
|
||||
- Each record MUST include: `id`, `spec_excerpt`, `source_section`, `source_document`, `semantic_type`, `normalized_form`, `confidence`
|
||||
- MUST use YAML format matching Example 1
|
||||
- MUST extract minimum 10 Spec-IR items for any non-trivial specification (5+ pages of documentation)
|
||||
- MUST include confidence scores (0-1) for all extractions
|
||||
- MUST document both explicit and implicit invariants
|
||||
|
||||
### Phase 3 - Code-IR (mandatory)
|
||||
- MUST analyze EVERY function with structured extraction
|
||||
- Each record MUST include: `id`, `file`, `function`, `lines`, `visibility`, `modifiers`, `behavior` (preconditions, state_reads, state_writes, computations, external_calls, events, postconditions), `invariants_enforced`
|
||||
- MUST use YAML format matching Example 2
|
||||
- MUST document line numbers for ALL claims (every precondition, state read/write, computation, external call)
|
||||
- MUST capture full control flow (all conditional branches, revert paths)
|
||||
- MUST identify all external interactions with risk analysis
|
||||
|
||||
### Phase 4 - Alignment-IR (mandatory)
|
||||
- MUST compare EVERY Spec-IR item against Code-IR
|
||||
- Each record MUST include: `id`, `spec_ref`, `code_ref`, `spec_claim`, `code_behavior`, `match_type`, `confidence`, `reasoning`, `evidence`
|
||||
- MUST classify using exactly one of: `full_match`, `partial_match`, `mismatch`, `missing_in_code`, `code_stronger_than_spec`, `code_weaker_than_spec`
|
||||
- MUST use YAML format matching Example 3
|
||||
- MUST provide reasoning trace explaining WHY classification was chosen
|
||||
- MUST include evidence with exact quotes and locations from both spec and code
|
||||
- Every Spec-IR item MUST have corresponding Alignment record (no gaps)
|
||||
|
||||
### Phase 5 - Divergence Findings (when applicable)
|
||||
- MUST create detailed finding for EVERY `mismatch`, `missing_in_code`, or `code_weaker_than_spec`
|
||||
- Each finding MUST include: `id`, `severity`, `title`, `spec_claim`, `code_finding`, `match_type`, `confidence`, `reasoning`, `evidence`, `exploitability`, `remediation`
|
||||
- MUST use YAML format matching Example 4
|
||||
- MUST quantify impact with concrete numbers (not "could be exploited" but "attacker gains $X, victim loses $Y")
|
||||
- MUST provide exploitability analysis with attack scenarios (prerequisites, sequence, impact)
|
||||
- MUST include remediation with code examples and testing requirements
|
||||
|
||||
### Phase 6 - Final Report (mandatory)
|
||||
- MUST produce structured report following 16-section format defined in Phase 6
|
||||
- MUST include all IR artifacts (Spec-IR, Code-IR, Alignment-IR, Divergence Findings)
|
||||
- MUST provide Full Alignment Matrix showing all spec→code mappings
|
||||
- MUST quantify risk and prioritize remediations
|
||||
|
||||
---
|
||||
|
||||
## Quality Thresholds
|
||||
|
||||
A complete spec-to-code compliance analysis MUST achieve:
|
||||
|
||||
### Spec-IR minimum standards:
|
||||
- Minimum 10 Spec-IR items for non-trivial specifications
|
||||
- At least 3 invariants extracted (explicit or implicit)
|
||||
- At least 2 security requirements identified (MUST/NEVER/ALWAYS keywords)
|
||||
- At least 1 math formula or economic assumption documented
|
||||
- Confidence scores for all extractions (no missing scores)
|
||||
|
||||
### Code-IR minimum standards:
|
||||
- EVERY public/external function analyzed (no gaps in coverage)
|
||||
- Minimum 3 invariants documented per analyzed function
|
||||
- ALL external calls identified with return handling documented
|
||||
- ALL state modifications tracked (reads and writes)
|
||||
- Line number citations for ALL claims (100% traceability)
|
||||
|
||||
### Alignment-IR minimum standards:
|
||||
- EVERY Spec-IR item has corresponding Alignment record (complete matrix)
|
||||
- Reasoning provided for all match_type classifications
|
||||
- Evidence includes exact quotes from both spec and code
|
||||
- Ambiguities explicitly flagged (never guessed or inferred)
|
||||
- Confidence scores reflect actual certainty (not placeholder 1.0 for everything)
|
||||
|
||||
### Divergence Finding minimum standards:
|
||||
- EVERY CRITICAL/HIGH finding has exploit scenario with concrete attack sequence
|
||||
- Economic impact quantified with dollar amounts or percentages
|
||||
- Remediation includes code examples (not just "add validation")
|
||||
- Testing requirements specified (unit tests, integration tests, fuzz tests)
|
||||
- Breaking changes documented with migration path
|
||||
|
||||
---
|
||||
|
||||
## Format Consistency
|
||||
|
||||
- MUST use YAML for all IR records (Spec-IR, Code-IR, Alignment-IR, Divergence)
|
||||
- MUST use consistent field names across all records (e.g., `spec_excerpt` not `specification_text`)
|
||||
- MUST reference line numbers in format: `L45`, `lines: 89-135`, `line 108`
|
||||
- MUST cite spec locations: `"Section §4.1"`, `"Page 7, paragraph 3"`, `"Whitepaper section 2.3"`
|
||||
- MUST use markdown code blocks with language tags: ` ```yaml `, ` ```solidity `
|
||||
- MUST separate major sections with `---` horizontal rules
|
||||
|
||||
---
|
||||
|
||||
## Anti-Hallucination Requirements
|
||||
|
||||
- NEVER infer behavior not present in spec or code
|
||||
- ALWAYS quote exact text (spec_quote, code_quote in evidence)
|
||||
- ALWAYS provide line numbers for code claims
|
||||
- ALWAYS provide section/page for spec claims
|
||||
- If uncertain: Set confidence < 0.8 and document ambiguity
|
||||
- If spec is silent: Classify as `UNDOCUMENTED`, never guess
|
||||
- If code adds behavior: Classify as `code_stronger_than_spec`, document in Alignment-IR
|
||||
@@ -0,0 +1,529 @@
|
||||
export const meta = {
|
||||
name: 'spec-compliance',
|
||||
description: 'Check code against its specification: extract requirements, hunt each one in the code, verify divergences',
|
||||
whenToUse:
|
||||
'When you have documentation describing intended behavior and want to know where the code disagrees with it. Pass a path, or {path, spec, limit}.',
|
||||
phases: [
|
||||
{ title: 'Extract', detail: 'find the documentation; turn it into individually checkable requirements' },
|
||||
{ title: 'Align', detail: 'one agent per requirement hunts the code for it; one sweeps the reverse direction' },
|
||||
{ title: 'Verify', detail: 'independent agents try to refute each divergence before it is reported' },
|
||||
{ title: 'Report', detail: 'alignment matrix, surviving divergences, contradictions between documents' },
|
||||
],
|
||||
}
|
||||
|
||||
const target = typeof args === 'string' ? { path: args } : args ?? {}
|
||||
const root = target.path ?? '.'
|
||||
const specHint = target.spec ?? null
|
||||
const outDir = target.outDir ?? 'spec-compliance'
|
||||
|
||||
// Per-requirement analysis goes to disk. Only these records travel back through the script, which is what
|
||||
// keeps a whole-codebase behavioral model from ever having to fit in one context window.
|
||||
const DISCOVERY_SCHEMA = {
|
||||
type: 'object',
|
||||
required: ['documents', 'codePaths'],
|
||||
properties: {
|
||||
documents: {
|
||||
type: 'array',
|
||||
description: 'Files that describe intended behavior, most authoritative first.',
|
||||
items: {
|
||||
type: 'object',
|
||||
required: ['path', 'describes'],
|
||||
properties: {
|
||||
path: { type: 'string' },
|
||||
describes: { type: 'string', description: 'what part of the system this document specifies' },
|
||||
kind: {
|
||||
type: 'string',
|
||||
enum: ['whitepaper', 'design-doc', 'readme', 'inline-docs', 'transcript', 'other'],
|
||||
},
|
||||
unreadable: {
|
||||
type: 'string',
|
||||
description:
|
||||
'Set only if the file could not be read as text (e.g. a binary .docx with no converter available). Name the file and why.',
|
||||
},
|
||||
},
|
||||
},
|
||||
},
|
||||
codePaths: {
|
||||
type: 'array',
|
||||
description: 'Directories or files holding the implementation these documents describe.',
|
||||
items: { type: 'string' },
|
||||
},
|
||||
language: { type: 'string' },
|
||||
},
|
||||
}
|
||||
|
||||
const REQUIREMENTS_SCHEMA = {
|
||||
type: 'object',
|
||||
required: ['requirements'],
|
||||
properties: {
|
||||
requirements: {
|
||||
type: 'array',
|
||||
description: 'One entry per independently checkable claim. Split compound sentences into separate entries.',
|
||||
items: {
|
||||
type: 'object',
|
||||
required: ['id', 'quote', 'location', 'kind', 'force'],
|
||||
properties: {
|
||||
id: { type: 'string', description: 'stable short id, e.g. REQ-04' },
|
||||
quote: { type: 'string', description: 'the requirement verbatim from the document, not paraphrased' },
|
||||
location: { type: 'string', description: 'e.g. "§4.1" or "README.md, Fees"' },
|
||||
kind: {
|
||||
type: 'string',
|
||||
enum: [
|
||||
'invariant',
|
||||
'formula',
|
||||
'access-control',
|
||||
'state-machine',
|
||||
'error-handling',
|
||||
'ordering',
|
||||
'economic',
|
||||
'trust-boundary',
|
||||
'other',
|
||||
],
|
||||
},
|
||||
force: {
|
||||
type: 'string',
|
||||
enum: ['mandatory', 'recommended', 'optional', 'descriptive'],
|
||||
description: 'mandatory for MUST/NEVER/ALWAYS; descriptive for prose that states what the system does',
|
||||
},
|
||||
checkable: {
|
||||
type: 'string',
|
||||
description: 'what would have to be true of the code for this to hold, in one line',
|
||||
},
|
||||
},
|
||||
},
|
||||
},
|
||||
},
|
||||
}
|
||||
|
||||
const ALIGNMENT_SCHEMA = {
|
||||
type: 'object',
|
||||
required: ['requirementId', 'verdict', 'confidence', 'searched', 'reasoning'],
|
||||
properties: {
|
||||
requirementId: { type: 'string' },
|
||||
analysisFile: { type: 'string', description: 'path the full analysis was written to' },
|
||||
verdict: {
|
||||
type: 'string',
|
||||
enum: ['implemented', 'partial', 'contradicted', 'absent', 'stronger-than-spec', 'undecidable'],
|
||||
description:
|
||||
'undecidable when the requirement is too vague to check against code — that is a finding about the document',
|
||||
},
|
||||
confidence: {
|
||||
type: 'string',
|
||||
enum: ['high', 'medium', 'low'],
|
||||
description: 'how sure you are of the verdict, not how severe it is',
|
||||
},
|
||||
evidence: {
|
||||
type: 'array',
|
||||
description: 'The code that implements, contradicts, or partially covers the requirement.',
|
||||
items: {
|
||||
type: 'object',
|
||||
required: ['file', 'lines', 'quote'],
|
||||
properties: {
|
||||
file: { type: 'string' },
|
||||
lines: { type: 'string', description: 'e.g. L108 or L89-L135' },
|
||||
quote: { type: 'string' },
|
||||
role: { type: 'string', description: 'what this line does for the requirement' },
|
||||
},
|
||||
},
|
||||
},
|
||||
searched: {
|
||||
type: 'array',
|
||||
description:
|
||||
'Where you looked, and what you found. An absent verdict rests entirely on this: a reader must be able to tell a real absence from a search that stopped early.',
|
||||
items: {
|
||||
type: 'object',
|
||||
required: ['where', 'result'],
|
||||
properties: {
|
||||
where: { type: 'string', description: 'pattern, symbol, or file searched' },
|
||||
result: { type: 'string', description: 'e.g. "3 hits, all in tests" or "0 hits"' },
|
||||
},
|
||||
},
|
||||
},
|
||||
reasoning: { type: 'string', description: 'why this verdict and not the adjacent one' },
|
||||
documentProblem: {
|
||||
type: 'string',
|
||||
description: 'Set if the requirement itself is ambiguous, self-contradictory, or contradicts another document.',
|
||||
},
|
||||
},
|
||||
}
|
||||
|
||||
const UNDOCUMENTED_SCHEMA = {
|
||||
type: 'object',
|
||||
required: ['behaviors'],
|
||||
properties: {
|
||||
behaviors: {
|
||||
type: 'array',
|
||||
description: 'Externally reachable behavior the documentation does not describe. Empty is a valid answer.',
|
||||
items: {
|
||||
type: 'object',
|
||||
required: ['what', 'file', 'lines', 'whyItMatters'],
|
||||
properties: {
|
||||
what: { type: 'string' },
|
||||
file: { type: 'string' },
|
||||
lines: { type: 'string' },
|
||||
whyItMatters: {
|
||||
type: 'string',
|
||||
description: 'what a reader of the documentation alone would wrongly believe',
|
||||
},
|
||||
reachableBy: { type: 'string', description: 'which actor can trigger it' },
|
||||
},
|
||||
},
|
||||
},
|
||||
},
|
||||
}
|
||||
|
||||
const REFUTATION_SCHEMA = {
|
||||
type: 'object',
|
||||
required: ['refuted', 'reasoning'],
|
||||
properties: {
|
||||
refuted: {
|
||||
type: 'boolean',
|
||||
description: 'true if the claimed divergence does not hold up',
|
||||
},
|
||||
reasoning: { type: 'string' },
|
||||
correction: {
|
||||
type: 'string',
|
||||
description: 'If the divergence is real but described wrongly, the accurate version.',
|
||||
},
|
||||
revisedVerdict: {
|
||||
type: 'string',
|
||||
enum: ['implemented', 'partial', 'contradicted', 'absent', 'stronger-than-spec', 'undecidable'],
|
||||
description: 'Set only if the original verdict was the wrong category.',
|
||||
},
|
||||
},
|
||||
}
|
||||
|
||||
const REPORT_SCHEMA = {
|
||||
type: 'object',
|
||||
required: ['reportFile', 'divergences', 'documentProblems'],
|
||||
properties: {
|
||||
reportFile: { type: 'string' },
|
||||
divergences: {
|
||||
type: 'array',
|
||||
items: {
|
||||
type: 'object',
|
||||
required: ['requirementId', 'severity', 'title'],
|
||||
properties: {
|
||||
requirementId: { type: 'string' },
|
||||
severity: { type: 'string', enum: ['critical', 'high', 'medium', 'low'] },
|
||||
title: { type: 'string' },
|
||||
},
|
||||
},
|
||||
},
|
||||
documentProblems: {
|
||||
type: 'array',
|
||||
description: 'Ambiguities and contradictions in the documentation itself, including between documents.',
|
||||
items: { type: 'string' },
|
||||
},
|
||||
},
|
||||
}
|
||||
|
||||
const EVIDENCE_RULE = `Cite a file and line for every claim about the code, and quote the document verbatim for every
|
||||
claim about intent. Where you cannot cite, do not assert — say what you could not establish. A short answer with
|
||||
cited claims is worth more than a long one with padded ones.`
|
||||
|
||||
phase('Extract')
|
||||
|
||||
const discovery = await agent(
|
||||
`Find the documentation describing intended behavior for the codebase at ${root}, and the code it describes.
|
||||
${specHint ? `The user pointed at ${specHint} — start there, and include anything else that also specifies behavior.` : ''}
|
||||
|
||||
Documentation is whatever states what the system is supposed to do: a whitepaper, a design note, a README section,
|
||||
a protocol description, doc comments carrying real semantics. Judge by content, not filename. Skip changelogs,
|
||||
contributor guides, build instructions, and license text — they describe the project, not its behavior.
|
||||
|
||||
If a file plainly holds a specification but you cannot read it as text, record it under 'unreadable' rather than
|
||||
guessing at its contents.`,
|
||||
{ schema: DISCOVERY_SCHEMA, label: 'discover', phase: 'Extract', effort: 'low' },
|
||||
)
|
||||
|
||||
if (!discovery || discovery.documents.length === 0) {
|
||||
return {
|
||||
error: 'No documentation describing intended behavior was found, so there is nothing to check the code against.',
|
||||
root,
|
||||
}
|
||||
}
|
||||
|
||||
const unreadable = discovery.documents.filter(d => d.unreadable)
|
||||
if (unreadable.length > 0) {
|
||||
log(`Could not read ${unreadable.length} document(s): ${unreadable.map(d => `${d.path} (${d.unreadable})`).join('; ')}`)
|
||||
}
|
||||
|
||||
const readable = discovery.documents.filter(d => !d.unreadable)
|
||||
if (readable.length === 0) {
|
||||
return { error: 'Every document found was unreadable as text.', root, unreadable }
|
||||
}
|
||||
|
||||
log(`Found ${readable.length} document(s): ${readable.map(d => d.path).join(', ')}`)
|
||||
|
||||
// Barrier: the requirement set has to be whole before it can be deduplicated and before contradictions
|
||||
// between documents can be spotted at all.
|
||||
const extracted = await parallel(
|
||||
readable.map(doc => () =>
|
||||
agent(
|
||||
`Extract the checkable requirements from ${doc.path} (repo root ${root}). It specifies: ${doc.describes}
|
||||
|
||||
A requirement is any claim that could be true or false of an implementation: an invariant, a formula, who is
|
||||
allowed to do what, the order things must happen in, what must revert or error, an economic assumption. Quote each
|
||||
one verbatim — the quote is what a later agent will check the code against, so a paraphrase loses the thing being
|
||||
checked.
|
||||
|
||||
Split compound claims. "Swaps must charge 0.3% and enforce 1% maximum slippage" is two requirements, because the
|
||||
code can get one right and the other wrong.
|
||||
|
||||
Extract what the document says, however many that is. Do not pad the list to look thorough, and do not promote a
|
||||
background sentence into a requirement to reach a count. If a claim is too vague to check, extract it anyway and
|
||||
say so in 'checkable' — a requirement nobody can verify is worth reporting.
|
||||
|
||||
Set 'force' from the document's own language: mandatory for MUST/NEVER/ALWAYS, descriptive for prose that merely
|
||||
narrates what the system does.`,
|
||||
{ schema: REQUIREMENTS_SCHEMA, label: doc.path, phase: 'Extract' },
|
||||
),
|
||||
)
|
||||
)
|
||||
|
||||
// Each document was extracted by its own agent, so two of them numbering from REQ-01 is the normal case, not
|
||||
// the exceptional one. Left alone, duplicate ids collide in the report and in the on-disk filenames.
|
||||
const seenIds = new Set()
|
||||
const requirements = extracted.flatMap((result, docIndex) => {
|
||||
if (!result) return []
|
||||
const document = readable[docIndex]?.path ?? 'unknown'
|
||||
return (result.requirements ?? []).map(requirement => {
|
||||
let id = requirement.id
|
||||
if (seenIds.has(id)) {
|
||||
let suffix = 2
|
||||
while (seenIds.has(`${requirement.id}-${suffix}`)) suffix += 1
|
||||
id = `${requirement.id}-${suffix}`
|
||||
}
|
||||
seenIds.add(id)
|
||||
return { ...requirement, id, document }
|
||||
})
|
||||
})
|
||||
|
||||
if (requirements.length === 0) {
|
||||
return { error: 'No checkable requirements could be extracted from the documentation.', root, documents: readable }
|
||||
}
|
||||
|
||||
// A large budget is permission to go deeper, not a reason to check every descriptive sentence in a README.
|
||||
const DEFAULT_LIMIT = 10
|
||||
const MAX_LIMIT = 30
|
||||
const budgeted = budget.total ? Math.max(4, Math.floor(budget.remaining() / 70_000)) : DEFAULT_LIMIT
|
||||
const limit = Math.min(target.limit ?? budgeted, MAX_LIMIT)
|
||||
|
||||
// Mandatory requirements first: a MUST the code ignores is the thing this workflow exists to find.
|
||||
const forceRank = { mandatory: 0, recommended: 1, optional: 2, descriptive: 3 }
|
||||
const ranked = [...requirements].sort((a, b) => (forceRank[a.force] ?? 4) - (forceRank[b.force] ?? 4))
|
||||
const selected = ranked.slice(0, limit)
|
||||
const deferred = ranked.slice(limit)
|
||||
|
||||
log(`Extracted ${requirements.length} requirements. Checking ${selected.length}.`)
|
||||
if (deferred.length > 0) {
|
||||
log(`Not checked (${deferred.length}, ranked below the cut): ${deferred.map(r => r.id).join(', ')}`)
|
||||
}
|
||||
|
||||
phase('Align')
|
||||
|
||||
const specContext = JSON.stringify({
|
||||
language: discovery.language,
|
||||
codePaths: discovery.codePaths,
|
||||
documents: readable.map(d => ({ path: d.path, describes: d.describes })),
|
||||
})
|
||||
|
||||
const slug = id => id.replace(/[^A-Za-z0-9._-]+/g, '-').replace(/^-+|-+$/g, '').slice(0, 40) || 'req'
|
||||
|
||||
// The reverse direction. Per-requirement fan-out is driven by the documentation, so by construction it cannot
|
||||
// find behavior the documentation never mentions; this agent is the only thing covering that.
|
||||
const undocumentedPromise = agent(
|
||||
`Find behavior in the code at ${root} that the documentation does not describe.
|
||||
|
||||
Context: ${specContext}
|
||||
|
||||
These are the requirements already extracted from the documentation:
|
||||
${JSON.stringify(selected.map(r => ({ id: r.id, quote: r.quote })))}
|
||||
|
||||
Work from the code inward: look at what an outside actor can reach — entrypoints, public and external functions,
|
||||
privileged operations, upgrade and admin paths, fallbacks, anything that moves value or changes permissions. For
|
||||
each, ask whether a reader of the documentation alone would know it exists and what it does.
|
||||
|
||||
Report what is both undocumented and consequential. A helper with no external effect is not interesting; an admin
|
||||
function that can redirect funds and appears in no document is. Empty is a valid answer, and a short accurate list
|
||||
beats a long one padded with getters.
|
||||
|
||||
${EVIDENCE_RULE}`,
|
||||
{ schema: UNDOCUMENTED_SCHEMA, label: 'undocumented-behavior', phase: 'Align' },
|
||||
).catch(error => {
|
||||
// It runs concurrently with the per-requirement fan-out and is awaited after it, so an unhandled
|
||||
// rejection here would take down a run whose requirement checks had all succeeded.
|
||||
log(`Reverse-direction sweep failed, so undocumented behavior is not covered in this run: ${error.message}`)
|
||||
return null
|
||||
})
|
||||
|
||||
// Each requirement runs align -> verify independently, so a divergence found early is being refuted while other
|
||||
// requirements are still being hunted.
|
||||
const checked = await pipeline(
|
||||
selected,
|
||||
(requirement, _item, index) =>
|
||||
agent(
|
||||
`Determine whether the code at ${root} implements this one requirement.
|
||||
|
||||
Requirement ${requirement.id} (${requirement.kind}, ${requirement.force}), from ${requirement.document} ${requirement.location}:
|
||||
"${requirement.quote}"
|
||||
${requirement.checkable ? `Holds if: ${requirement.checkable}` : ''}
|
||||
|
||||
Context: ${specContext}
|
||||
|
||||
Find the code responsible for this requirement and read it. Read the functions it calls — a bound looks enforced
|
||||
when the value came back from a function whose name implies a check, and the check turns out to sit on a branch
|
||||
this path does not take. Where a requirement is enforced across several functions, follow it across them.
|
||||
|
||||
Write the full analysis to ${outDir}/requirements/${String(index + 1).padStart(2, '0')}-${slug(requirement.id)}.md
|
||||
using the Write tool, then return the record.
|
||||
|
||||
Choosing a verdict:
|
||||
- 'implemented' means you found the enforcement and read it. Not that you found a function with a promising name.
|
||||
- 'partial' means it holds on some paths and not others. Say which paths, in 'reasoning'.
|
||||
- 'contradicted' means the code does something incompatible with the requirement.
|
||||
- 'stronger-than-spec' means the code enforces more than the document asks for.
|
||||
- 'absent' means you looked and it is not there. This verdict rests entirely on 'searched': record the patterns
|
||||
and symbols you tried and what each returned, so a reader can tell a real absence from a search that stopped
|
||||
early. An absence claimed without that record is worthless.
|
||||
- 'undecidable' means the requirement is too vague to check. That is a finding about the document; put the reason
|
||||
in 'documentProblem'.
|
||||
|
||||
Judge the code against this requirement only. If you notice something else wrong, that is not this record's
|
||||
business. Use only the documentation and code in front of you — what a protocol of this kind usually does is not
|
||||
evidence about what this one does.
|
||||
|
||||
${EVIDENCE_RULE}`,
|
||||
{
|
||||
agentType: 'spec-to-code-compliance:spec-compliance-checker',
|
||||
schema: ALIGNMENT_SCHEMA,
|
||||
label: requirement.id,
|
||||
phase: 'Align',
|
||||
},
|
||||
),
|
||||
async (alignment, requirement) => {
|
||||
if (!alignment) return null
|
||||
if (alignment.verdict === 'implemented') return { requirement, alignment, refutations: [] }
|
||||
|
||||
// Independent agents, told to refute. Claude favors its own findings when asked to check them, so the
|
||||
// check has to come from an agent that did not produce the finding.
|
||||
const lenses = [
|
||||
'Read the code yourself before deciding. The most common way this verdict is wrong is that the enforcement exists somewhere the first agent did not look: a modifier, a base contract, a wrapper, a caller that checks before calling, a constructor invariant, a type that makes the case impossible.',
|
||||
'Check the reading of the document rather than the code. The most common way this verdict is wrong is that the requirement does not say what the finding claims it says: a scope limited elsewhere in the document, a definition given earlier, a sentence that recommends rather than requires, or an example that narrows it.',
|
||||
]
|
||||
|
||||
const votes = await parallel(
|
||||
lenses.map(lens => () =>
|
||||
agent(
|
||||
`Try to refute this claimed divergence between documentation and code at ${root}.
|
||||
|
||||
Requirement ${requirement.id}, from ${requirement.location}: "${requirement.quote}"
|
||||
Claimed verdict: ${alignment.verdict} (confidence: ${alignment.confidence})
|
||||
Reasoning given: ${alignment.reasoning}
|
||||
Evidence cited: ${JSON.stringify(alignment.evidence ?? [])}
|
||||
Where it searched: ${JSON.stringify(alignment.searched ?? [])}
|
||||
Full analysis: ${alignment.analysisFile ?? '(not written)'}
|
||||
|
||||
${lens}
|
||||
|
||||
Refute it if it does not hold up. If it holds up, say so — do not manufacture a refutation, and do not refute
|
||||
merely because you would have worded it differently. If the divergence is real but described inaccurately, leave
|
||||
'refuted' false and put the accurate version in 'correction'. If it is real but the wrong category — an 'absent'
|
||||
that is really a 'partial' — set 'revisedVerdict'.
|
||||
|
||||
${EVIDENCE_RULE}`,
|
||||
{ schema: REFUTATION_SCHEMA, label: `refute:${requirement.id}`, phase: 'Verify', effort: 'medium' },
|
||||
),
|
||||
),
|
||||
)
|
||||
|
||||
return { requirement, alignment, refutations: votes.filter(Boolean) }
|
||||
},
|
||||
)
|
||||
|
||||
const results = checked.filter(Boolean)
|
||||
if (results.length === 0) {
|
||||
return { error: 'Every requirement check failed.', root, selected: selected.map(r => r.id) }
|
||||
}
|
||||
|
||||
const undocumented = await undocumentedPromise
|
||||
|
||||
// Either verifier refuting is enough to drop it. A divergence nobody could confirm is not worth a client's time,
|
||||
// and both lenses have to miss for a real one to be lost.
|
||||
const survived = results.filter(r => r.alignment.verdict !== 'implemented' && !r.refutations.some(v => v.refuted))
|
||||
const dropped = results.filter(r => r.alignment.verdict !== 'implemented' && r.refutations.some(v => v.refuted))
|
||||
const unverified = results.filter(r => r.alignment.verdict !== 'implemented' && r.refutations.length === 0)
|
||||
|
||||
log(
|
||||
`Checked ${results.length}. ${survived.length} divergence(s) survived verification, ${dropped.length} refuted, ` +
|
||||
`${undocumented?.behaviors.length ?? 0} undocumented behavior(s).`,
|
||||
)
|
||||
if (unverified.length > 0) {
|
||||
log(`Unverified (both refutation agents failed): ${unverified.map(r => r.requirement.id).join(', ')}`)
|
||||
}
|
||||
|
||||
phase('Report')
|
||||
|
||||
// Genuine barrier: the matrix and the contradictions between documents need every record at once.
|
||||
const report = await agent(
|
||||
`Write the compliance report for ${root} to ${outDir}/REPORT.md using the Write tool, then return the summary.
|
||||
|
||||
Documents checked: ${JSON.stringify(readable.map(d => d.path))}
|
||||
|
||||
Requirements that hold:
|
||||
${JSON.stringify(results.filter(r => r.alignment.verdict === 'implemented').map(r => ({ id: r.requirement.id, quote: r.requirement.quote, evidence: r.alignment.evidence })))}
|
||||
|
||||
Divergences that survived refutation:
|
||||
${JSON.stringify(survived.map(r => ({ requirement: r.requirement, alignment: r.alignment, corrections: r.refutations.map(v => v.correction).filter(Boolean), revisedVerdicts: r.refutations.map(v => v.revisedVerdict).filter(Boolean) })))}
|
||||
|
||||
Divergences a refutation agent knocked down (do not report these as findings):
|
||||
${JSON.stringify(dropped.map(r => ({ id: r.requirement.id, verdict: r.alignment.verdict, whyRefuted: r.refutations.filter(v => v.refuted).map(v => v.reasoning) })))}
|
||||
|
||||
Undocumented behavior:
|
||||
${JSON.stringify(undocumented?.behaviors ?? [])}
|
||||
|
||||
Per-requirement analysis is on disk under ${outDir}/requirements/ — read any of it you need.
|
||||
|
||||
The report opens with what a reader needs first: whether the code does what the documents say, and the divergences
|
||||
that matter, worst first. Then the alignment matrix — every requirement checked, its verdict, and the line that
|
||||
evidences it. Then the undocumented behavior, then the problems in the documentation itself.
|
||||
|
||||
For each divergence: what the document requires, what the code does instead, and what follows from the gap. Where
|
||||
you can show the consequence concretely — the sequence that reaches it, who can trigger it, what they get — do,
|
||||
because a divergence whose consequence is spelled out is the one that gets fixed. Where you cannot, say what would
|
||||
have to be true for it to matter rather than inventing a scenario or a dollar figure.
|
||||
|
||||
Severity is about consequence, not about how far the code strayed. A formula off by a rounding step that drains a
|
||||
pool over time outranks a MUST the code satisfies by different means than the document describes. Documentation
|
||||
drift with no behavioral consequence is low, and say plainly that it is a documentation fix rather than a code one.
|
||||
|
||||
Carry these forward rather than smoothing them over:
|
||||
- requirements marked 'undecidable', and any 'documentProblem' recorded against a requirement — contradictions
|
||||
between two documents are a real finding, and the fix is to the documents
|
||||
- requirements not checked at all: ${deferred.length > 0 ? deferred.map(r => r.id).join(', ') : '(none)'}
|
||||
- documents that could not be read: ${unreadable.length > 0 ? unreadable.map(d => d.path).join(', ') : '(none)'}
|
||||
- divergences whose refutation agents both failed, which are unverified rather than confirmed: ${unverified.length > 0 ? unverified.map(r => r.requirement.id).join(', ') : '(none)'}
|
||||
|
||||
Cover the substance and stop. Sections with nothing in them should say so in a line, or be left out — do not pad
|
||||
the report to fill a template, and do not restate the matrix in prose after presenting it as a table.
|
||||
|
||||
${EVIDENCE_RULE}`,
|
||||
{ schema: REPORT_SCHEMA, label: 'report', phase: 'Report' },
|
||||
)
|
||||
|
||||
return {
|
||||
root,
|
||||
report: report?.reportFile ?? `${outDir}/REPORT.md`,
|
||||
documents: readable.map(d => d.path),
|
||||
requirementsExtracted: requirements.length,
|
||||
requirementsChecked: results.length,
|
||||
holds: results.filter(r => r.alignment.verdict === 'implemented').map(r => r.requirement.id),
|
||||
divergences: report?.divergences ?? survived.map(r => ({ requirementId: r.requirement.id, verdict: r.alignment.verdict })),
|
||||
refuted: dropped.map(r => ({ requirementId: r.requirement.id, verdict: r.alignment.verdict })),
|
||||
unverified: unverified.map(r => r.requirement.id),
|
||||
undocumentedBehavior: undocumented?.behaviors ?? [],
|
||||
documentProblems: report?.documentProblems ?? [],
|
||||
notChecked: deferred.map(r => r.id),
|
||||
unreadableDocuments: unreadable.map(d => ({ path: d.path, why: d.unreadable })),
|
||||
}
|
||||
Reference in New Issue
Block a user