name: midnight-verify:verify-ledger
description: >-
Ledger/protocol claim classification and method routing. Determines what kind
of ledger claim is being verified and which verification methods apply:
source investigation (primary), type-checking (pre-flight for TypeScript API),
compilation/execution (secondary for testable claims), or ledger-v8 execution
(secondary for API behavioral claims). Handles claims about transaction
structure, token mechanics (Night/Zswap/Dust), cost model, on-chain VM,
contract execution, cryptographic primitives, well-formedness rules, and the
@midnight-ntwrk/ledger-v8 TypeScript API. Loaded by the /midnight-verify:verify command
alongside the hub skill.
version: 0.1.0
Ledger/Protocol Claim Classification
This skill classifies ledger and protocol claims and determines which verification method to use. The /midnight-verify:verify command loads this alongside the midnight-verify:verify-correctness hub skill.
Verification Flow
Ledger claims have a richer verification hierarchy than other domains because the ledger crates produce the compiled output that the contract-writer and zkir-checker already work with.
- Type-check (pre-flight) — for TypeScript API claims only. Dispatch @"midnight-verify:type-checker (agent)" against the existing sdk-workspace (ledger-v8 is already installed). Pre-flight only, never a standalone verdict.
- Source investigation (primary) — always runs for protocol claims. Dispatch @"midnight-verify:source-investigator (agent)", which loads
verify-by-ledger-source for Rust crate-level routing.
- Compilation/execution (secondary) — for claims testable via Compact contracts. Dispatch @"midnight-verify:contract-writer (agent)" (compile + execute, extract ledger-level evidence) or @"midnight-verify:zkir-checker (agent)" (inspect compiled circuits).
- Ledger-v8 execution (secondary) — for claims about TypeScript API behavioral output. Write a script that calls ledger-v8 functions and observes output.
Claim Type → Method Routing
Claims About Protocol Structure
| Claim Type |
Example |
Pre-flight |
Primary |
Secondary |
| Transaction format |
"Transactions contain intents, offers, and binding randomness" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
| Segment ordering |
"Segment 0 is guaranteed, executes first" |
— |
@"midnight-verify:source-investigator (agent)" |
@"midnight-verify:contract-writer (agent)" (negative test) |
| Causal precedence |
"Contract A calling B means A causally precedes B" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
| Replay protection |
"Intent hashes stored in TimeFilterMap" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
| Well-formedness |
"Disjoint check prevents input/output overlap" |
— |
@"midnight-verify:source-investigator (agent)" |
@"midnight-verify:contract-writer (agent)" (build invalid tx) |
| Proof staging |
"UnprovenTransaction transitions to Proven via prove()" |
— |
@"midnight-verify:source-investigator (agent)" |
ledger-v8 execution |
Claims About Token Mechanics
| Claim Type |
Example |
Pre-flight |
Primary |
Secondary |
| Night UTXO |
"UTXO uniqueness from (intent_hash, output_no)" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
| Zswap commitments |
"CoinCommitment = Hash<(CoinInfo, CoinPublicKey)>" |
— |
@"midnight-verify:source-investigator (agent)" |
ledger-v8 execution (call coinCommitment) |
| Zswap nullifiers |
"CoinNullifier = Hash<(CoinInfo, CoinSecretKey)>" |
— |
@"midnight-verify:source-investigator (agent)" |
ledger-v8 execution (call coinNullifier) |
| Zswap transients |
"Transients use ephemeral single-leaf Merkle tree" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
| Dust generation |
"Dust generates proportional to backing Night value" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
| Dust spending |
"Dust spend requires ZK proof of generation chain" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
| Token types |
"NIGHT is TokenType::Unshielded with raw [0u8; 32]" |
— |
@"midnight-verify:source-investigator (agent)" |
ledger-v8 execution (call nativeToken) |
Claims About Cost Model
| Claim Type |
Example |
Pre-flight |
Primary |
Secondary |
| Cost dimensions |
"SyntheticCost has 5 dimensions: read, compute, block, write, churn" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
| Fee formula |
"Fee = max(read, compute, block) + write + churn" |
— |
@"midnight-verify:source-investigator (agent)" |
@"midnight-verify:contract-writer (agent)" (compile, measure cost) |
| Block limits |
"Block usage limit is 200,000 bytes" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
| Price adjustment |
"Per-dimension price targets 50% block fullness" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
| Guaranteed limits |
"Guaranteed section has separate cost bounds" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
Claims About On-Chain VM
| Claim Type |
Example |
Pre-flight |
Primary |
Secondary |
| Opcode semantics |
"idx loads from Map by key" |
— |
@"midnight-verify:source-investigator (agent)" |
@"midnight-verify:zkir-checker (agent)" (inspect compiled) |
| StateValue types |
"5 types: Null, Cell, Map, Array, BoundedMerkleTree" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
| Stack machine |
"VM is a stack machine, always exactly 1 item initially" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
| Cached reads |
"idxc requires value to be cached in memory" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
Claims About Contract Execution
| Claim Type |
Example |
Pre-flight |
Primary |
Secondary |
| Contract address |
"ContractAddress = Hash" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
| Effects system |
"Effects declare claimed nullifiers, commitments, calls" |
— |
@"midnight-verify:source-investigator (agent)" |
@"midnight-verify:contract-writer (agent)" (compile + execute) |
| Caller determination |
"Caller is calling contract, then single UTXO owner, then None" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
| Transcripts |
"Guaranteed transcript executes before fees are taken" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
Claims About Cryptographic Primitives
| Claim Type |
Example |
Pre-flight |
Primary |
Secondary |
| Pedersen commitments |
"Value commitment = gr + hv where h = hash(type, segment)" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
| Fiat-Shamir binding |
"Binding uses challenge c = hash(ErasedIntent, gr, gs)" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
| Signatures |
"Schnorr over Secp256k1 per BIP 340" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
| Hashing |
"field::hash uses Poseidon" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
| Merkle trees |
"Commitment tree uses persistent Merkle tree" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
Claims About Ledger TypeScript API
| Claim Type |
Example |
Pre-flight |
Primary |
Secondary |
| Type/export existence |
"ledger-v8 exports Transaction class" |
@"midnight-verify:type-checker (agent)" |
@"midnight-verify:source-investigator (agent)" |
— |
| Function signature |
"coinCommitment takes (coin, coinPublicKey)" |
@"midnight-verify:type-checker (agent)" |
@"midnight-verify:source-investigator (agent)" |
— |
| Function behavior |
"nativeToken() returns the NIGHT raw token type" |
@"midnight-verify:type-checker (agent)" |
@"midnight-verify:source-investigator (agent)" |
ledger-v8 execution |
| Class API |
"ZswapLocalState has spend() method" |
@"midnight-verify:type-checker (agent)" |
@"midnight-verify:source-investigator (agent)" |
— |
| CostModel API |
"CostModel.initialCostModel() returns default fee config" |
@"midnight-verify:type-checker (agent)" |
@"midnight-verify:source-investigator (agent)" |
ledger-v8 execution |
Claims About Formal Properties
| Claim Type |
Example |
Pre-flight |
Primary |
Secondary |
| Balance preservation |
"Total funds preserved except mints, dust, and treasury" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
| Transaction binding |
"Assembled transaction cannot be disassembled" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
| Infragility |
"Defensively-created tx survives malicious merge" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
| Causality |
"Contract call A → B implies A success ⟹ B success" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
| Self-determination |
"User cannot spend another user's funds" |
— |
@"midnight-verify:source-investigator (agent)" |
— |
Routing Rules
When in doubt:
- Protocol structure, token mechanics, crypto primitives → @"midnight-verify:source-investigator (agent)" (Rust source is authoritative)
- TypeScript API surface → @"midnight-verify:type-checker (agent)" pre-flight + @"midnight-verify:source-investigator (agent)" (trace WASM binding to Rust)
- Testable behavior (cost, well-formedness, token operations) → @"midnight-verify:source-investigator (agent)" + @"midnight-verify:contract-writer (agent)" or ledger-v8 execution as secondary
- Formal properties → @"midnight-verify:source-investigator (agent)" only (these are about the proof structure in code)
Source investigation is always primary. Secondary methods (compilation, execution) provide corroborating evidence but are not required for a verdict.
Hints from Existing Skills
Sub-agents may load these skills for context. They are hints only — never cite skill content as evidence.
compact-core:compact-standard-library skill — stdlib functions that map to ledger primitivesmidnight-tooling:compact-cli skill — how Compact compiles to ZKIR (relevant for VM claims)midnight-tooling:compact-cli skill — compiler behavior and flags
By