Zero Knowledge Proof of Brainf*ck program execution

Graviton

1/6/24, 6:25 AM

I have been trying to follow this paper for zk-SNARKs to create Zero Knowledge Proofs (ZKPs) for verifying computations. Specifically, given a public program $F$, a public input $x$, I would like to create a proof $\pi$ which "proves" that there exists some private input $w$ such that, $$F(x,w)=z,$$ without revealing what $w$ is. However, as I am new to cryptography, although I have a decent background in math with some recreational programming abilities, much of this paper goes over my head.

My restrictions:

So, I thought it might be easier to restrict myself from a universal construction (which is what that paper describes), to an easier case; namely, the Brainf*ck programming language (which I will denote as BF). Also, I will assume that $x=\emptyset$ (i.e; the program $F$ takes only $w$ as an input). Furthermore, the I/O of BF is quite limited, so I will assume that $w$ is simply a string of bytes to initialize the memory, and that the output $z$ is a boolean $\text{True}$.

How would I begin to create a protocol that creates a ZKP for a given public BF program $F$, to "prove" that there exists some private $w$ such that $F(w)=\text{True}$?

How I see myself continuing depends on what exactly $F(\cdot)$ represents. I see a few options

$F(w)=\text{True} \iff$ the program outputs a non-zero byte,
$F(w)=\text{True} \iff$ the program outputs anything at all,
$F(w)=\text{True} \iff$ the program does not halt,
$F(w)=\text{True} \iff$ the program ends with the bytes in memory in a certain configuration.

They all seem to have various pros and cons. Option 1 and 2 are "natural", but rely on direct outputs of the program. Option 3 and 4 read no outputs, but 3 runs into the halting problem, and 4 reads the memory. These are all effectively isomorphic in the sense that it is trivial to rewrite a program to reproduce any of these results, but I would like to know your opinion on which of these options (if any) makes ZKPs easier. Maybe I'm over thinking this part.

In any case, after this I'm not confident on how to continue. Theoretically, I need some way of generating some notion of a certificate which could only come from a successful evaluation of $F(w)=\text{True}$ and uniquely corresponds to an input $w$, without revealing what $w$ is.

Any and all advice would be greatly appreciated.

P.S. I've asked a related question over at the MathematicsSE here, in which I'm looking for general reference requests for introductions to ZKPs which are more friendly to those with little cryptography background but decent math backgrounds. I figured that there are probably more people here that'd know the answer, despite it being more of a math-oriented question.

0 + 4

zero-knowledge-proofs

yyyyyyy

1/6/24, 8:46 AM

Brainfuck is Turing-complete, so your "easier case" actually *is* the general case.

Graviton

1/6/24, 9:12 AM

@yyyyyyy that's a good point, which somehow leaves me more confused, haha. The paper I was reading was a universal , protocol for any language, so by restricting myself to one language, does this not make my problem any easier? Surely proving the execution of a BF program is easier than something like python, as we can leverage its simple source code, despite both being Turing complete. On the contrary, perhaps I have got it backwards, in that higher level languages are actually easier to verify...

Marc Ilunga

1/6/24, 9:32 AM

That task doesn't see too trivial. Have a look into Circom https://docs.circom.io/. It's a language that lets you write zk circuits and later generates provers and verifier code. Alternatively, you can restrict to simple programs like arithmetic circuit and find a suitable proof system to work with.

Lev

1/18/24, 8:01 PM

To be honest, understanding generic proof systems is a difficult task. You're best off starting with traditional ZKP constructions to understand the definitions better (See Schnorr's protocol for discrete log, for example).

Elon Musk

I sit in a Tesla and translated this thread with Ai:

EN: Zero Knowledge Proof of Brainf*ck program execution

Post an answer

Most people don’t grasp that asking a lot of questions unlocks learning and improves interpersonal bonding. In Alison’s studies, for example, though people could accurately recall how many questions had been asked in their conversations, they didn’t intuit the link between questions and liking. Across four studies, in which participants were engaged in conversations themselves or read transcripts of others’ conversations, people tended not to realize that question asking would influence—or had influenced—the level of amity between the conversationalists.