Re: Longfellow ZK (google-zk)

I guess Jaromil is busy preparing a demo for Geneva, so I take the liberty
of chiming in.

> How is the counter-signature (in the mDL transcript) of the mobile device
verified?

As you have surmised, the circuit verifies two ECDSA signatures, one from
the issuer on the hash of the MDOC, and the other from the secure element
on the transcript of the session between the relying party and the holder
(basically a nonce provided by the RP and some other stuff).

> In other words, do you know what the cost of dynamically disclosing a set
of submessages is in Longfellow ZK, or is that not supported?

The way things are currently set up is this.  Pick SZ and N in advance, say
SZ=2048 and N=3.  We generate a circuit that takes a MDOC up to SZ bytes
long and discloses up to N attributes.  The prover does not reveal the
actual length of the MDOC or how many attributes/which attributes are in
the MDOC.  "Disclosing an attribute" today means equality check: for 0 <= i
< N and given key[i], val[i] as public inputs, the circuit proves that, for
all i, some attribute exists in the mdoc that matches (key[i], val[i]).

Most of the proving cost is in the SZ term, because we have to hash SZ
bytes.  The N term is smaller, say something like 30ms for each extra
attribute.

We do equality-check only because we lack imagination.  If use cases arise
that require, e.g., less-than comparisons, we can easily add those at
negligible cost.  I think the fullness-of-time circuit will look like N
"arithmetic-logic units" that can be configured to compute a few common
operations, and N giant multiplexers that route the MDOC bytes to the input
of the ALU.  Today the ALU is just an equality check.

> ECDSA is not post-quantum.

Agree.  That's the next thing to work on---how to verify a post-quantum
signature in a circuit.  This is a hard problem.

> SD-JWT

I'll let Jaromil say what he wants to say.  I note that, from the ZKP
perspective, SD is redundant because it accomplishes the same goal as ZKP
in a less perfect way.  So it's better for us to start from plain JWT
rather than having to compute a redundant hash in SD-JWT.  MDOC is SD-only,
so it is suboptimal from our perspective.

> Circuit compression.

As you have surmised, there is a lot of redundancy in the circuit.  There
are 36 identical instances of SHA256 permutations, 2 identical ECDSA
verifications, and each SHA256 is itself multiple identical rounds, and
each round is multiple identical XORs etc.  There is redundancy at all
levels of abstraction.  Our current strategy is to flatten everything into
individual gates (the "netlist" as hardware people would call it) and
ignore the redundancy.

The redundancy manifests itself in two ways.

First, the circuit is highly compressible for the practical purpose of
distributing the circuit to all phones.  Since ZSTD was good enough we
didn't worry too much about this issue.  I am sure one can do better but
300KB is in the noise.

The second issue is more important.  It is in theory possible to exploit
the redundancy in sumcheck itself.  For example, we know how to run one
SHA256 circuit on vectors of 36 elements instead of instantiating the
SHA256 gates 36 times, and in fact this "vector sumcheck" algorithm would
be about twice as fast as the other one.  (Both versions are in the code
but the vector one is disabled.)  If the whole circuit were just repeating
SHA256 36 times we would be done, but things get much more complicated when
we have to select the N attributes, where now the attributes are misaligned
with respect to the SHA256 vector dimension.  This is kind-of analogue to
AVX programming, where you have a vector unit that performs 8 additions but
you still need to perform scalar operations.  Any attempts to exploit
vector operations leads to complexity that we are unwilling to impose to
the world at this stage.  We would also need some circuit-description
language and compiler support which we don't currently have.