X-Wing, Frames, ecrecover, SPHINCS⁻ and VCVio

Hey all, last week of summer — people are slowly coming back from vacations and work is getting back to full speed.

With all the work up to this point I think that in the next few upcoming weeks I'd probably wrap the proposal up, kick off the ethresear.ch[1] post and start discussing the scheme extensions.

Circle's ecrecover fix

Part of the week I spent analyzing whether it would make sense (or even be possible) to use a hash-based commitment scheme for the key-exchange part, and looking for a better interface for hybrid pre-quantum/post-quantum signatures.

Previously the state of the art for hybrid signatures, to me, seemed to be a zk-nox 4337[2] PQ account that checked an ECDSA signature and then a PQ signature right after it.

During PQ-signatures breakout #13, Mira from Circle shared their idea of how to incorporate hybrid signatures by re-defining the ecrecover byte layout[3] without breaking its pure semantics. The pair (v = 27, s = 0) becomes the sentinel — a valid ECDSA signature never has s = 0 — and r is repurposed:

• 0x00 — leading byte, keeps r < n
• bytes11 signatureIndex — index into the frame transaction's tx.signature[] array
• bytes20 verificationFunctionId — either a fixed enum for a pure verification function, or a lookup into a key-registration precompile

So the same 65 bytes point at a PQ signature (and its public key) carried by an EIP-8141[4] frame transaction instead of encoding a curve point. It works natively with frames, where one frame may register a PQ key and the very next frame reads it — the registration mechanism itself is left open between EIP-8164, EIP-7932 and EIP-8130.

That idea sounds very interesting, and I went and adjusted the existing PoC codebase to use this trick instead of ERC-7913[5] as I had planned. Because the spending part is only an implementation detail, most of the code stayed in place with minor diffs.

This solution is great because it opens a way to not deprecate existing contracts that use ecrecover — the Stealth Meta-Address Registry[6] being the one I care about.

Office hours #11

The office hours this week were extremely inspiring. Huge thanks to everyone. All of my questions were mysteriously asked and answered before I got to them — including machine proofs and the post-quantum internet.

By the way, w.r.t. PQ-TLS I learnt about X-Wing[7], and Arc uses it for TLS 1.3[8].

Lean 4 de-slopping

Inspired by the advice to trust the process and not be afraid of making mistakes, I started a close analysis of the Lean 4 code produced by the machine — ideally wanting to de-slop it and understand what needs to be contributed upstream.

I ended up creating two PRs for relatively small things in ML-KEM, which is not as actively used and maintained in VCVio[10] as ML-DSA, and was missing a couple of small utilities that my coding agent had produced and flagged as unnecessary.

VCVio PRs

• #583 — expose concrete ML-KEM encoding facts[11] (merged) — DecidableEq on the encoded types and public encoder sizes, so the concrete scheme elaborates without downstream workarounds.
• #582 — generic SampleableType instances for ring carriers[12] — improved sampling that lets downstream code drop the instances it had to carry as hypotheses on every statement.

Proofs overview

To review proofs I've tweaked my Neovim setup with lean.nvim[9], which is handy for following the theorems — but reading with my own eyes is what I mostly need at this point. So I decided to put together a wiki with script-generated proof pages that explain each proof and display its parts.

Going to host it on pq-sap.gwei.domains next week or so.

Hash-based commitments for key exchange

I already did some exploration of Merkle trees and Poseidon2 usage, and the new information about ML-KEM[13]-powered X-Wing got me prototyping again. As I figured, X-Wing is basically X25519 + ML-KEM-768:

• If a quantum computer breaks X25519, ML-KEM carries.
• If Module-LWE falls to classical cryptanalysis, X25519 carries.

Hash-based key exchange itself is quite tricky. Merkle Puzzles achieve it with hashed leaves, where Bob would need to find the same pre-image and, having done so, prove that to Alice.

With 128-bit security an attacker would need 2^64 hashes per party. But against Grover's algorithm, unfortunately, it doesn't stand.

So even if research backed by Cloudflare concludes that cryptographic agility and fallbacks for both X25519 and ML-KEM are a good approach in general, I should probably chill and move on.

EIP-8304 and Native UTXOs

This one is pretty exciting as well. A few days ago a new post appeared on ethresear.ch with the results of "An Evaluation of Authenticated UTXO Discovery with EIP-8304 and UTXO Proof Tables"[14], which I had hinted at in the original Native UTXOs thread[15].

Frame transactions

After exploring a few links I found out that Nethermind is championing[16] frame transaction prototypes and spec edits, and perhaps I could spend next week looking deeper into what's available there and whether it would be enough for a demo. Promising sign: their integration branch already runs a shielded pool end-to-end on a two-client devnet.

For those who aren't chronically on CT: there's a small drama going on around 8130 and 8141. However, on ACDE it was agreed to proceed with some form of AA in Hegota (~yay). Trusting my gut and my understanding of both specs, I'd probably commit to also researching what interesting SAP designs we can unlock — and ideally test them.

The justification for including 8141[4] in the pq-sap ERC scope would be to not drag in the AA stack (previously highlighted as needed to solve issues like ownership, recovery, automations, etc.), as well as to be a good reference for developers who would want to get into frame transactions earlier.

SPHINCS⁻

Randomly and unexpectedly, I see a post from Nico[17] in my CT feed about SPHINCS⁻, which I'd heard about a few months ago at EthPrague. And it just clicked: why not consider it as one of the spending schemes? It's legitimately a cheaper gas option with even more conservative security assumptions (hash-only, no lattice). It turned out to be

~77× cheaper than the ML-DSA 7913 route (14.97M gas)

with an interesting observation that one long-term hash-based pk links payments.

Demo app

I'm such a visual person, and seeing how everything comes together through a UI is one of the best feelings in the world for me. So I started working on a prototype app that would allow using the hybrid PQ stealth address protocol with ML-KEM for the exchange and something else for spending — with all the fancy stuff like relayers, paymasters and scan functionality.

Next

Overall the week was fun — onto the next things.