Bytes in, leverage out

So after presenting the project proposal, I started preparing a repository — now published as pq-sap[1] — with some of the things I've learnt so far about ML-KEM[2] and ML-DSA[3]. It consists of Python scripts and vectors that I produced during the PoC of ML-KEM for the key exchange, with an almost ~1KB announcement.

During the cohort I'm going to rely extensively on AI to produce code and verify its correctness, leaving some space open to re-implement/re-write the implementation/proposal with a full understanding of what's happening.

Being wrong in an isolated environment with almost no error cost helps me iterate fast on ideas, learn fast from examples, try things out differently, and compare solutions with the collected knowledge about the domain.

So basically the leverage I have at the moment is some bytes I can send to the magic-AI-blackbox context for it to (hopefully) do what it was asked to do. The thinking and design process still remains high-level, and the recent discovery of ERC-7913[4] for key-verification abstraction — to abstract the spending part — is something that popped up among my bookmarks and not something Claude came up with.

ERC-7913 key abstraction presents verification as a tuple of (verifier, pubkey).

Signer abstraction for the spending part seems to be even more important than I originally anticipated, because there is another contributor interested in pushing for a hybrid approach: an ML-KEM exchange, but still keeping the k1 keys for spending, with 4337[5] capabilities.

Another useful link I've discovered through the Ethereum Magicians[6] mailing list (go create an account if you don't have one yet!) is ERC-8373[7] for binding pre-Q ↔ post-Q keys. It contains a useful Python spec reference as well as vectors provided along with the proposal[8]. I'd need to get more familiar with this proposal to see if there is anything useful that can be done for the PQ-spending migration — but viewing still needs to be solved.

On Lean 4 and VCVio[9] in general, I'm getting more confident with the tool choice. After reading the VCVio paper[10] a few times and staring at the formulas, I figured that the tool primarily helps me assemble a chain of oracle events (and easily replace different parts of the process, like keygen!) to produce an expected outcome over programmable rules.

For me specifically it means that I could have a generic interface for DK-SAP (which would need to be broken on purpose to compare with PQ-SAP[11]) and use the same set of tests for both schemes — as well as any new ones that might emerge.

After a quick detour to explore 8373 I took a deep dive into functional programming with Lean, and will write more about it next week!