Specifying Kimchi

[mimoo]

Motivation

Read this if you’re skeptical about the need for a specification, skip it otherwise.

• We are implementing a protocol that diverges from the original PLONK paper, as such without a specification the protocol only really exists in code.
• Some people might want to analyze the protocol without having to read the code. I've run into scenarios like this, where some people wanted to analyze the protocol with formal verification tools but either gave up because they did not want to reverse engineer the code to understand the protocol, or analyzed the wrong protocol because of the lack of a spec.
• Some people might want to review the implementation based on a specification, this is very common during pentests where good value can be obtained by asking consultants to follow the specification and make sure it closely matches the specification. This is really an excellent way to find bugs
• Writing a specification is a process that often leads one to finds bugs in an implementation.
• It makes it easier to modify the protocol, when we can reason about it from a higher-level abstraction. After all, code is a noisy and verbose layer to specify a protocol.
• It makes it easier to review changes from others.
• It makes onboarding much easier.
• It makes implementing an interoperable implementation much easier.

Solutions

1. Maintain a written spec in the same repository, and update it when we make changes to the protocol

• Pros: it works
• Cons:
  • we have to be self-disciplined otherwise it can easily become outdated.
  • There’s some overhead for every change of the protocol (I would argue that this forces us to think about changing the protocol before changing code though)

2. Derive the specification from the code

• Pros: less overhead
• Cons:
  • more verbose code perhaps?
  • There’s no clear path on how to do this correctly. But that’s why we’re here
  • Perhaps it can lead to us becoming lazy (in terms of specifying the protocol clearly) and the spec can become outdated if we don’t maintain the code parts that ensures that the spec is correct. (For example we add a functionality that doesn’t generate text in the spec.)

[mimoo]

I implemented a very naive approach a while back https://github.com/mimoo/cargo-specification, it simply parses your code and look for a special type of comment (i.e. //~ like that). And you can list the files it should parse in some specification.toml file. You can also surround structs with some special comment to directly export them into the spec (so that we don’t have structures/types that become outdated in the spec). The downside is that then you have to use the code as language to specify objects (in our case Rust).
What I liked with this approach is that if we take, for example, the proof creation function, then we can use these special comments to comment on the code as well. So it doesn’t necessarily add verbosity to our codebase. At the same time you maintain the spec within your code.
I’d like to toy with the idea of having a special macro on functions that says “whenever you call me with arguments X and Y, I generate the following line in the spec”. Perhaps something like #[spec=”commit to the polynomial X”]

[mrmr1993]

Derive the specification from the code

Love this. Presumably we can use the polynomial definitions we already have

[mimoo]

BTW I'm still not convinced that this is the right path, I do think writing a separate spec forces you to write for other humans AND forces you to better understand the changes to the protocol you're making.

Some examples of good specs in our field:

• https://protocol.penumbra.zone/main/penumbra.html
• https://zcash.github.io/orchard/
• https://zcash.github.io/halo2/
• https://doc-internal.dalek.rs/bulletproofs/notes/index.html
• https://merlin.cool/

other specs that I like:

• https://strobe.sourceforge.io/specs/
• http://www.noiseprotocol.org/noise.html