test(zeronym): model the protocol in Quint and check it in CI by aphelionz · Pull Request #82 · ShieldedLabs/zero

aphelionz · 2026-09-23T14:28:10Z

Adds a Quint specification of the zeronym protocol (wallet, shim, hub, indexer and chain, over a mixnet that loses, duplicates and reorders messages) and checks it in CI. No Rust is changed.

zeronym/spec/quint/ has two layers:

Protocol spec (protocol.qnt): the components as pure functions, the hub abstract, one Byzantine component at a time. Checked by quint test and seeded simulation.
Hub spec (hubMachine.qnt): the real hub function on a chain clock, checked exhaustively with TLC for the schedule guarantees (G6b, G6c) and known gaps.

zeronym/spec/quint/README.md has the threat model, guarantees, trust matrix, known gaps and findings against the Rust.

CI (zeronym-guards): spec-protocol runs tiers 1 to 3b (typecheck, tests, simulation); spec-protocol-tlc runs tiers 1 and 4 (TLC, Java 21). Quint 0.33.0 and Apalache 0.62.1 are pinned.

What it found

Eleven findings against the Rust, listed with their evidence in the README. Five are classed as code bugs: one HIGH (a single indexer endpoint reporting a far-ahead tip pins the hub's tip), three MEDIUM (two of which share a root cause) and one LOW. None is fixed here. Each was matched to the code by reading; nothing was reproduced against it.

What "checked" means

The hub spec is exhaustive under TLC for small, scaled-down configurations. The protocol spec's guarantees are bounded random simulation, not proof. One hub and the mixnet transport only.

Verification

CI: spec-protocol and spec-protocol-tlc pass
sh zeronym/spec/quint/check.sh: all tiers green locally (Quint 0.33.0, Rust evaluator, OpenJDK 27)
sh zeronym/guards.sh green

🤖 Generated with Claude Code

Copilot

Copilot review overview

🟡 Changes recommended

Critical model and harness issues remain, along with a moderate invariant concern.

Get a fresh assessment by requesting another Copilot review.

Review effort: Lite
Findings: 2

Open (2)

Non-zero Quint exits are incorrectly treated as counterexamples · New
Lying hub can mask early bytes as a valid transaction · New

What changed in this PR

Adds a Quint model of the Zeronym divert protocol and runs its checks in CI.

Changes:

Models queueing, lookup, publication, and unreliable network behavior.
Checks known fixes and documented protocol gaps.
Adds a dedicated Quint specification CI job.

File	Summary	Review findings
`zeronym/spec/divert.qnt`	Protocol model and invariants	Critical (3 votes): A lying hub can expose queued or absent data as `tx`, allowing `noEarlyBytes` to pass despite early bytes. Moderate (1 vote): The L4 invariant is tautological and cannot detect a guard violation.
`zeronym/spec/check.sh`	Simulation and expected-outcome checks	Critical (3 votes): Every non-zero Quint exit is treated as an expected counterexample, allowing execution failures to pass silently.
`.github/workflows/zeronym-guards.yml`	CI job for the model	No specific findings.

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

…are check.sh From review on #82. Lying replies were tagged hubSaw "lie", which exempted them from noQueuedBytes and noEarlyBytes, so a lying hub releasing a queued migration's bytes passed as safe. Replies now carry the hub's real state plus an `honest` ghost flag. The shim's claims (guardHolds, pendingVisible) are checked against a lying hub as shimSafety; the hub's claims (noQueuedBytes, noEarlyBytes) are checked against an honest hub, and current.noEarlyBytes is a new expected failure recording that attestation is what stands between a queued migration and early release. check.sh read every nonzero exit as a counterexample, so a crash, a download failure or a misspelt invariant passed each "fails" row. It now classifies runs by Quint's [ok] / [violation] line and fails the gate on anything else. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Copilot

Copilot review overview

🟡 Changes recommended

The model currently masks an unresolved #80 regression, and the verification count is inaccurate.

Get a fresh assessment by requesting another Copilot review.

Review effort: Lite
Findings: 1

Open (1)

Sentinel check can miss the #80 regression · New

Resolved since last review (2)

Lying hub can mask early bytes as a valid transaction
Non-zero Quint exits are incorrectly treated as counterexamples

zeronym/spec/divert.qnt models the wallet, shim and hub over a mixnet that loses, duplicates and reorders messages, with a hub that can be set to lie. It mirrors the get_transaction reply arms in intercept.rs, the queue-first lookup in server.rs, admission in queue.rs and the epoch flush in batcher.rs. check.sh simulates eight module/invariant pairs and asserts each outcome: - the four safety claims hold for the current code (L4 guard, queued bytes stay in the hub, a queue hit reads as pending, bytes only after publish); - ecb4641 and 45e408f reappear with their fixes switched off; - three known gaps stay visible: silent refusal over Nym, a lying hub faking pending, and the flush-window pending -> NOT_FOUND flip. It runs as a cheap-tier job in zeronym-guards. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…are check.sh From review on #82. Lying replies were tagged hubSaw "lie", which exempted them from noQueuedBytes and noEarlyBytes, so a lying hub releasing a queued migration's bytes passed as safe. Replies now carry the hub's real state plus an `honest` ghost flag. The shim's claims (guardHolds, pendingVisible) are checked against a lying hub as shimSafety; the hub's claims (noQueuedBytes, noEarlyBytes) are checked against an honest hub, and current.noEarlyBytes is a new expected failure recording that attestation is what stands between a queued migration and early release. check.sh read every nonzero exit as a counterexample, so a crash, a download failure or a misspelt invariant passed each "fails" row. It now classifies runs by Quint's [ok] / [violation] line and fails the gate on anything else. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Copilot

Copilot review overview

🟡 Changes recommended

Pin actions/checkout to a known commit SHA and ensure the job is read-only.

Get a fresh assessment by requesting another Copilot review.

Review effort: Lite
Findings: 2

Open (2)

Pin actions/checkout to a commit SHA and restrict token permissions · New
Sentinel check can miss the #80 regression

From review on #82: the job runs code fetched at run time (npx, Quint's evaluator), so it should run with a SHA-pinned checkout, no persisted credentials, and contents: read. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Copilot

Copilot review overview

🔵 Needs a closer look

The CI matrix omits the documented lying-hub noQueuedBytes counterexample, allowing an expected failure to disappear without failing the gate.

Review effort: Lite
Findings: None

Resolved since last review (2)

Pin actions/checkout to a commit SHA and restrict token permissions
Sentinel check can miss the #80 regression

From review on #82: divert.qnt documents that a lying hub breaks both hub claims, but check.sh asserted only noEarlyBytes, so the noQueuedBytes gap could disappear without failing the gate. Ten rows now. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Copilot

Copilot review overview

🔵 Needs a closer look

The protocol model and expected-failure CI gate warrant final human review.

Review effort: Lite
Findings: None

An honest hub forwards a Found with an empty body and height 0, and the shim renders pending. A conforming indexer does not send that image; the model now can, and pendingIsTrue fails when it does. Co-authored-by: Cursor <cursoragent@cursor.com>

pendingVisible ignores every reply the hub was not following its code to send, so it is not a claim about an arbitrary hub. The any-reply bundle no longer includes it. Co-authored-by: Cursor <cursoragent@cursor.com>

guardHolds repeated the only assignment of status tx, so a hub could not falsify it. The mismatch arm and the queue-hit sentinel are now runs. Co-authored-by: Cursor <cursoragent@cursor.com>

The lie was only a found reply. It can now be not-found or error, and a queued migration reported not-found is an expected failure. Co-authored-by: Cursor <cursoragent@cursor.com>

Once the wallet has seen a transaction's bytes, a later pending or not-found is a regression. Reorder, a resend after publication, and the other hub's not-found each reach it. The seeded sample does not, so the runs are the check. Co-authored-by: Cursor <cursoragent@cursor.com>

find_by_txid matches a queue entry only when its txid is the query. An unparseable body stays queued and answers not-found, and pending is only claimed for a body that has a txid. Co-authored-by: Cursor <cursoragent@cursor.com>

This reverts commit 62ec0d9.

L4 turns a mismatched found into status not-found. The suppression check follows the reply's disposition, so that mismatch is not the witness. Co-authored-by: Cursor <cursoragent@cursor.com>

This reverts commit c22aa12.

Copilot

🔵 Needs a closer look

A moderate active finding remains because check.sh can treat a child command that exits nonzero as successful, violating the script’s fail-closed behavior.

1 open issue

Prevent overlapping abstract flushes while a batch is held

_{Review effort: Lite}

Co-authored-by: Shoaib Ahmed <sufialhussaini@gmail.com>

spec(zeronym): record the free junk burst as finding 13

Copilot

🔵 Needs a closer look

A critical mismatch between the specification and the checked-in classifier means the tests may pass without validating the shipped behavior, requiring human assessment.

1 open issue

Prevent overlapping abstract flushes while a batch is held

_{Review effort: Lite}

…claude/spec-hub-substitution # Conflicts: # zeronym/spec/quint/README.md

docs(zeronym/spec): add the hub-hop and lookup threats from the third report

Copilot

🔵 Needs a closer look

The protocol model permits a new flush to begin while retryable entries from the previous batch remain in flight, misrepresenting the hub’s queue and verdict ordering.

1 open issue

Prevent overlapping abstract flushes while a batch is held

_{Review effort: Lite}

…assumptions

…able

…mptions

…re work

Copilot

🟡 Changes recommended

A critical issue remains in zeronym/spec/quint/check.sh because nonzero background-check exit statuses can be treated as successes, allowing the gate to pass despite failed verification.

2 open issues

_{Review effort: Lite}

A rejection or a mined verdict burns the txid, refuses a later signing of it, and drops every queued entry that carries it. The burn set's bound stays unmodelled. Co-authored-by: Cursor <cursoragent@cursor.com>

Copilot

🟡 Changes recommended

A moderate active finding remains in zeronym/spec/quint/wire.qnt: the lookup arm can return an unparseable payload when its txid matches, diverging from the Rust behavior and lacking the requested regression coverage.

3 open issues

_{Review effort: Lite}

…t flush only when idle

Copilot

🔵 Needs a closer look

Human assessment is needed because the evidence indicates a critical mismatch between the modeled burn/nullifier behavior and the shipped Rust admission logic, making the apparent verification coverage unreliable.

1 open issue

Reject unparseable payloads when interpreting lookup replies

2 resolved since last review

_{Review effort: Lite}

Copilot AI lite review requested due to automatic review settings September 23, 2026 14:28

Copilot started reviewing on behalf of aphelionz September 23, 2026 14:28

View session