Skip to content

test(zeronym): model the divert protocol in Quint and check it in CI - #82

Open
aphelionz wants to merge 4 commits into
mainfrom
test/zeronym-divert-quint
Open

test(zeronym): model the divert protocol in Quint and check it in CI#82
aphelionz wants to merge 4 commits into
mainfrom
test/zeronym-divert-quint

Conversation

@aphelionz

@aphelionz aphelionz commented Sep 23, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

Adds a Quint model of the shim <-> hub divert protocol, plus a cheap CI job that checks it.

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.

zeronym/spec/check.sh simulates ten module/invariant pairs and asserts each outcome, classified by Quint's verdict line so a crash or misspelt invariant fails the gate. It runs as a new spec job in zeronym-guards (ubuntu-latest, Quint pinned at 0.32.0).

  • Holds against any hub (shim claims): the L4 guard, and an honest queue hit reading as pending.
  • Holds against an honest hub (hub claims): queued bytes staying in the hub, bytes only after publication.
  • Reproduced with the fix switched off: the queue-hit sentinel bug fixed in fix(zeronym): the shim discarded the hub's queue-hit sentinel #80 (found in 31 ms) and the 45e408f byte leak.
  • Known gaps, kept visible as expected failures: silent refusal over Nym, a lying hub faking pending or releasing a queued migration early (attestation is the defense), and the flush-window flip from pending to NOT_FOUND. If one of these starts holding, the code or the model changed and the spec needs a look.

Rebased onto #80, so current matches main. Simulation samples random traces; a bounded quint verify (Apalache) pass is a possible follow-up.

Verification

  • sh zeronym/spec/check.sh: 10/10 outcomes as expected (TypeScript backend locally)
  • sh zeronym/guards.sh green

🤖 Generated with Claude Code

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

Copilot AI left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 High severity

Open (2)
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.

Comment thread zeronym/spec/check.sh Outdated
Comment thread zeronym/spec/divert.qnt Outdated
aphelionz pushed a commit that referenced this pull request Sep 23, 2026
Mark Henderson @claude
test(zeronym): scope the divert invariants by hub honesty; verdict-aw…
768e476 
…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 AI review requested due to automatic review settings September 23, 2026 15:24
Copilot AI reviewed Sep 23, 2026
View reviewed changes

Copilot AI left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 High severity

Open (1)
Resolved since last review (2)

Comment thread zeronym/spec/divert.qnt
Mark Henderson and others added 2 commits September 23, 2026 13:00
Mark Henderson @claude
test(zeronym): model the divert protocol in Quint and check it in CI
80648df 
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>
Mark Henderson @claude
test(zeronym): scope the divert invariants by hub honesty; verdict-aw…
4a456c9 
…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 AI review requested due to automatic review settings September 23, 2026 17:00
@aphelionz
aphelionz force-pushed the test/zeronym-divert-quint branch from 768e476 to 4a456c9 Compare September 23, 2026 17:00
Copilot AI reviewed Sep 23, 2026
View reviewed changes

Copilot AI left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 High severity

Open (2)

Comment thread .github/workflows/zeronym-guards.yml Outdated
Mark Henderson @claude
ci(zeronym): pin the spec job's checkout and give it a read-only token
2e90d6f 
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 AI review requested due to automatic review settings September 23, 2026 20:26
Copilot AI reviewed Sep 23, 2026
View reviewed changes

Copilot AI left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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)

Mark Henderson @claude
test(zeronym): assert the lying-hub noQueuedBytes counterexample
262bd78 
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 AI review requested due to automatic review settings September 23, 2026 21:52
Copilot AI reviewed Sep 23, 2026
View reviewed changes

Copilot AI left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Copilot review overview

🔵 Needs a closer look

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

Review effort: Lite
Findings: None

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

Copilot code review Copilot
Copilot review effort
Applies to this pull request for everyone.Learn more about Copilot code review.
Copilot left review comments

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@aphelionz