Conversation
…ith-payout, epoch seals Amended revision of the PULSE spec from PR #45, relocated to research/pulse/ (the docs/ tree was removed in the project restructure). Key changes vs revision 1: - Analyze the current-state exit race left unexamined: A16 (live-Operator exit denial, previously evidence-free) and A17 (current-root broadcast griefing, superseding A7's full-root case) - New §7.5: exit notices + eviction-with-payout — displacing an in-flight exit is conforming only with a full on-chain payout, upgrading the exit guarantee to exit-or-payout against any Operator, live or dark - Per-pulse finality via off-chain epoch seals (k-of-n DA receipts) instead of on-chain h_k gating, removing the pulse-per-batch throughput ceiling - 'Checkpoint' deliberately avoided for the seal role: Arkade already uses checkpoint transactions for offchain VTXO spends (anti-griefing) - Threshold continuity attestation promoted to the primary model default - Anchor topology revised (A6): keyless P2A per node + TRUC sibling eviction; per-claimant anchors at slot level only - §2/§11 rewritten for the current compiler surface (tapscript leaves, grouped ABI; options block and serverVariant no longer exist) - Margins include virtual-chain depth and stampede fees; slot-CSV rationale stated Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DyA8J3GnnE55mvBWX4wHnT
…ntified capital requirements - §9.2: self-enforcing equivocation bonds (Babylon-style EOTS with pre-committed per-epoch nonces); corrects the §9 nonce-reuse rejection, which is valid for transaction signatures only — protocol artifacts can pin nonces, so double-signing A_k/sigma_k/h_k leaks the key and lets anyone execute a pre-signed burn: judge-free, token-free slashing of the double-sign class - §9.3: token-free distributed-systems hardening — SUNDR fork-linearizability as the design ceiling, witness-cosigned transparency log (1-of-N split-view detection), proactive FROST share refresh on heartbeat cadence, erasure-coded DA with sampling - §9.4: capital requirements quantified per adversary class, with a worked example, per-identity bond aggregation rule, fee-floor formula, and renewal-ladder liquidity schedule; corrects revision 2's requiredCoverage claim (heartbeat cadence does not bound the lie-once drain — only the signing threshold does) - Six new red-team findings A18–A23 (accidental self-slash, nonce withholding, burn-tx pinning, DA sampling eclipse, reshare capture, correlated per-identity bonds); evidence lists, §12.2, §13.1, §13.4, and the trust statement updated Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DyA8J3GnnE55mvBWX4wHnT
…four claim-precision defects Corrections arising from an independent formal-verification pass over revision 2.1 (TLA+ ceremony/exit models, Lean proofs of the §9.2 algebra). Protocol change: - A24 (new, CRITICAL): revision 2.1 indexed nonce commitments per epoch, but the operator threshold signs two artifacts per epoch (A_k and h_k). Distinct messages under one committed nonce is the EOTS extraction condition, so a correct implementation of 2.1 would leak its own key and burn its own bond during honest operation. Nonce index is now the (epoch, artifact role) pair; message-level role separation is not a fix. Distinct from A18, which is a crash/restart fault — this fires on the specified happy path. Claim-precision fixes: - §9.2: extraction requires distinct challenges, not merely distinct messages; the implication holds only under collision resistance. - §7.1: abandonment is clean only through step 4; a signed transition is broadcastable and cannot be recalled. - §7.1a: auto-exit on k−1 names the epoch clients select, not a promise that its input is unspent. - §7.5: only enclave/threshold refusal prevents an unlawful eviction; client non-finality, seal refusal and bond slashing are after-the-fact. - Vocabulary (EOTS, nonce chain) realigned with the corrected §9.2. Verification gaps recorded in §0 so they are not mistaken for results: the A4 ordering invariant is enforced by construction rather than independently falsified, the §7.4 timelock inequality is a property of the chosen parameters, and §13.2 remains unformalized. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DyA8J3GnnE55mvBWX4wHnT
|
Important Draft PR not reviewedDraft PRs are not automatically reviewed by default.
To automatically review draft PRs, update your CodeRabbit configuration: reviews:
auto_review:
drafts: trueThanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
Contributor
Playground PreviewA live preview of this PR's playground is available at:
|
…nsion pass The payout obligation of §7.5 was keyed to the moment a notice is sealed, and the only leg that actually prevents a spend — refusal by the signing threshold — was gated on that same condition. The interval between filing a notice and the seal set receipting it was therefore unprotected: an Operator can evict paying zero with an intact signing policy and a healthy seal set, and can widen the window by stalling the sealers. The obligation now attaches on the validly signed notice presented to the signing threshold, which can verify that signature without anyone's receipt. The seal governs third-party adjudication — dispute halt, slashing, compensation — not the refusal that prevents the spend. Found and its fix verified by an expansion of the formal models, which also: - gave A24 and A18 executable models (the honest-operation self-slash reproduces in three states with no adversary and no crash), plus four dependency-free Lean theorems stating the side condition that separates extraction-as-a-defence from extraction-as-a-liability; - made the A4 ordering invariant independently falsifiable, where it had been enforced by the model's own construction; - demoted the §7.4 timelock inequality to an assumption, since it tested the chosen parameters rather than the protocol. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DyA8J3GnnE55mvBWX4wHnT
The TLA+ models and Lean proofs behind findings A24 and A25 existed only as a loose bundle; the spec cited them for provenance but the repository had no copy. This adds them, so a reader can run what the document claims. Contents: three TLA+ modules (Ceremony, Exit, Nonce) with 15 configurations — five that hold and ten mutants that must each lose their named property — plus two Lean files, and verify.py to re-run everything and reject unexpected results. Negative cases must fail for their named property, never for a syntax or runtime error. Nonce.tla and NonceSchedule.lean are the executable evidence for A24: the honest-operation self-slash reproduces in three states with no adversary and no crash, and four dependency-free Lean theorems compile with no axioms at all, stating the side condition that separates extraction-as-a-defence from extraction-as-a-liability. Also reconciles what committing these made stale: - the bundle README is marked superseded in part by VERIFICATION-2.2.md, and its two invalidated ledger rows are corrected in place (LatticeBeforeTransition was unfalsifiable as first written; TimelockOrdering tested the parameters, not the protocol, and is now an ASSUME); - the VERIFICATION-2.2 manifest notes Pulse.lean, which sits alongside unchanged and was not re-run in that pass; - the spec's §0 no longer says the formalization is outside this repository. No compiler behaviour changes; these are research artifacts. tla2tools.jar and the Lean toolchain are not vendored — verify.py takes their paths. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DyA8J3GnnE55mvBWX4wHnT
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Design specification for PULSE (Pooled Unilateral-exit via Lattice State Epochs): a way to give open-membership pool contracts — AMMs, lending pools, vaults — the same standing unilateral exit that ordinary Arkade VTXOs already have. Documentation only, no compiler changes. Supersedes #45.
The problem
An ordinary Arkade contract gives you a way out on your own. You write a
tapscriptleaf naming your key behind a CSV, and if the Operator disappears you broadcast it, wait out the timelock, and your funds land on L1. Nobody's permission required.That construction needs to name its keys when the contract is instantiated — and a pool's membership is dynamic and unbounded, so there are no keys to name. In practice pool contracts ship with either no unilateral leaf at all, or one gated on a curator, which is custodial by another name. Pool exits today are transient: a cooperative redemption drains funds to per-holder VTXOs that each have a clean exit, but only while the Operator plays along.
So the gap is specific: a passive pool member — someone whose balance hasn't moved in weeks — has no standing way out. Their money is only as safe as the Operator's continued cooperation.
The idea
Keep a complete, fully pre-signed fire escape for every member at all times, and refresh it whenever anyone transacts.
The pool is one shared VTXO holding aggregate funds, plus a balance table. Each time someone deposits, withdraws, or trades, the parties actually involved — typically one or two, plus the Operator — run a short ceremony that re-signs an exit lattice: a tree of pre-signed transactions splitting the pool UTXO into one output per member at their current balance. Every member holds their own branch. Passive members sign nothing, ever, after joining. Whoever moves funds pays the coordination cost.
The trick that makes this safe without a covenant opcode: the pool's exit leaf is a single constant-size key plus a CSV, and the keys behind it are ephemeral and deleted once the lattice is signed. The lattice is then the only thing that can ever spend that leaf — a de facto covenant, built the same way Arkade's own VTXO trees are built. Operator vanishes, you broadcast your branch and walk out.
Two consequences shape everything else. Exit costs are bounded by how far the off-chain chain has run, so the pool periodically re-anchors on-chain (the heartbeat) — many cheap off-chain pulses between on-chain heartbeats, which is where "recurrent" comes from. And since a stale lattice would pay out old balances, exits sit behind a delay while ordinary transitions don't: anyone holding a newer state can always outrun an old one.
The parts that are actually hard
Who checks the numbers for people who weren't in the room? Every pulse publishes a signed attestation over the entire balance table, not just the parties transacting, and anyone at all can recompute two things from public data: that the lattice's outputs sum to the pool's value, and that they match the attested table. Fail either and conforming software treats the pulse as non-final and falls back to the last good one. A malformed or over-allocating lattice becomes a visible halt instead of a silent loss.
Can a live Operator simply stall your exit forever? This was the sharpest finding in review. Delayed exits versus undelayed transitions cuts both ways: a live Operator could keep displacing your exit indefinitely, carrying balances forward correctly each time so no fraud evidence ever exists. The fix is exit notices and eviction-with-payout — once you file a notice, the only valid way to displace your exit is a transaction that pays your full balance on-chain. Exit or payout; there is no third option, and refusing to do either is a visible stall that trips everyone else's auto-exit. This also defuses the mirror-image griefing attack, since broadcasting the current lattice now just means requesting your own payout.
What stops the Operator signing two contradictory histories? Signing nonces are pre-committed per epoch and role, so signing twice in one slot leaks the signer's key by plain Schnorr algebra — which lets anyone complete a pre-signed transaction that burns that signer's bond. Self-executing, no judges, no token, ordinary Bitcoin.
What it honestly does not give you
The document is explicit about this rather than burying it, and a reader should know before evaluating:
That split is deliberate, and §13.2 states why it's unavoidable: with non-interactive passive members and no covenant opcode, amount safety must rest on a trusted layer. Covenant-grade trustlessness needs a fork (§12.2 sketches what changes under the Great Script Restoration). Absent one, trustless-mechanism / enforced-amount is the end state.
What formal verification caught
An independent pass built TLA+ models of the ceremony and the timed exit race and Lean proofs of the signature algebra. It surfaced A24, a CRITICAL flaw in the spec as previously written: nonce commitments were indexed per epoch, but the Operator threshold signs two artifacts per epoch. Two messages under one nonce is exactly the key-extraction condition, so a faithful implementation would have leaked its own key and burned its own bond during entirely honest operation — no attacker, no crash. Nonces are now indexed per (epoch, role). Four further claims were tightened where the prose said slightly more than it could support.
That pass's own limits are recorded in §0 too, so nothing reads as more verified than it is: one ordering invariant is enforced by the model's construction rather than independently falsified, the timelock inequality is a property of the chosen parameters rather than of the protocol, and the trilemma remains unformalized.
Reading order
§1 is a plain-language walkthrough with no math. §7 is the protocol proper. §10 is the 24-finding adversarial table, which is the fastest way to judge whether the design has been pushed on hard enough. §13 is the honest security accounting. §0 logs how the document evolved.
Draft, and intended as input to a whitepaper. The compiler-surface section (§11) is explicitly future work and touches no supervised zones.
🤖 Generated with Claude Code
https://claude.ai/code/session_01DyA8J3GnnE55mvBWX4wHnT