feat(plugins): jupiter-swap-guard — verified T1 Jupiter swap builder that binds the output to the payer

[JuanMarchetto]

Existing swap plugins relay the aggregator's bytes; this one rebuilds the transaction and proves the output can only reach the user's own account and that no instruction can divert funds. The guarantee lives in the signed bytes, not in a chat summary the LLM can rewrite.

Track B · custody tier T1 (build-only): never holds a key, never signs, never broadcasts. Returns an unsigned VersionedTransaction for a human to review and sign out of band (Squads-preferred).

Complete and green — Kani proofs pass in CI and the plugin loads in the real ZeroClaw 0.8.3 host. It also survived an adversarial self-review that caught (and I fixed) every fund-diversion gap before this was opened for review. The ≤3min demo video is the one remaining piece.

The guardrails — each maps to the exploit it excludes (see PROOFS.md)

• D1 — positional destination binding. The Jupiter route's actual destination_token_account (at the discriminator's fixed ABI index — 3 for route, 6 for shared_accounts_route) must equal the payer's own ATA, derived on-device from the mint's on-chain owner (a trusted RPC read, never the aggregator response). Every ATA-create must be payer-owned.
• D2 — no smuggled fund movement. Top-level System and every top-level SPL Token / Token-2022 instruction are decoded, not trusted by program-id: Transfer/Approve/SetAuthority/Burn are refused, and a CloseAccount is allowed only when it returns to the payer — so a malicious response cannot drain the swapped tokens or the unwrapped SOL.
• D3 — on-chain amount binding. The swap instruction's own in_amount / quoted_out_amount / slippage_bps are decoded from the signed bytes and bound to what was authorized and quoted; on-chain min-out must be ≥ the floor. Closes the quote↔instructions TOCTOU; an undecodable route is refused.
• D4 — priority-fee cap. The decoded SetComputeUnitPrice fee is capped (no runaway-fee SOL drain).
• D5 — static account roles. The payer and its ATAs must be static message keys, so a malicious RPC's lookup-table contents can never fill a fund role.
• P1–P8 — mint allowlist, per-tx cap, max slippage, program allowlist, payer-only signer, and fail-closed config parsing (an unknown/misspelled key is a hard error) — enforced inside the plugin, so the model cannot talk its way past them.

Verification

• Kani proves the encoder-integrity properties exhaustively (compact-u16 malleability P6, reader crash-safety P7): CI reports Complete - 2 successfully verified harnesses, 0 failures.
• Byte-exact differential: the plugin's own parse → compile → serialize equals solana_message::v0::Message::try_compile on a real captured mainnet route (246-address ALT → 9 static keys + 1 lookup, 505 bytes). ATA derivation checked against real on-chain ATAs.
• Positive + negative controls on the real fixture: the honest route passes every check; ~11 tampered variants (attacker destination, smuggled System/Token transfer, CloseAccount-to-attacker, over-cap fee, tampered on-chain min-out, over-authorized amount, unaccountable route, wrong cluster, …) are each refused with a specific reason. 46 host tests, no network.
• The u128-division arithmetic guardrails (min-out floor, priority-fee ceil) are proptest-covered over the full domain — CBMC can't verify the divider tractably, and PROOFS.md says so plainly rather than overclaiming a proof.

Engineering / merge-readiness

• Pure-core/thin-shim; crate-type = ["cdylib","rlib"]; layout matches plugins/redact-text; permissions http_client + config_read only.
• No solana-sdk in the wasm build — hand-rolled compact-u16 + v0/ALT encoder; PDA/ATA via sha2 + curve25519-dalek (default-features=false, verified no js-sys in the wasm tree, which is a runtime landmine under wasip2). The solana-* crates are host-only dev-dependencies used purely as a byte-exact oracle.
• CI parity green: wasm32-wasip2 release build, clippy -D warnings (host + wasm), cargo fmt --check, cargo test --locked (46, no network).
• Full README (threat model incl. the load-bearing human-signer assumption + the CPI-not-enumerated caveat, custody mechanics, PR-25 compliance appendix, and a pt-BR section) and a signer guide (docs/sign-and-send.md: verify the decoded tx, not the chat).
• The Kani workflow lives on a dedicated fork branch (ci-kani) by design, so this PR touches only plugins/jupiter-swap-guard/.

Two questions I'd love maintainer input on:

1. Preferred home for a small shared Solana core (in-repo crates/ vs a published crate)?
2. For a build-only T1 tool that returns an unsigned tx, is auto_approve on the tool the pattern you'd want (the real approval being the human signature), or should it route through the host approval gate?

Feedback on the destination-binding approach and the fail-closed stance very welcome. 🦀