Can a circuit in a zk-SNARK be reversed-engineered?

We I'm misunderstanding your question, but the circuit didn't *need* to be reverse engineered. It's publicly known and given to the verifier in plain. However in your example x would not be part of the circuit description, it is the witness, i.e. the *input* to the circuit.

Thanks, @Maeher. I meant that x shouldn't be a witness, as we don't want the prover to know x either. Is it possible to have a proof where nobody knows x but can still check if HMAC(x, witness) = s?

You can prove that for some circuit you know an input such that the output is $s$. To hide $x$ the circuit would need to be somehow obfuscated but then the question is how you verify that the obfuscated circuit really computes HMAC.

No, the zk-SNARK is a kind of NIZK, which can ensure that the witness, e.g., the secret x, is not disclosed except the proof $\pi$ and the statment s. So, for HMAC, the complier converts it to a arithmetic circuit fistly, and finally generates a QAP/QSP instance. Duo to the QAP is hard, then it is difficult to reverse to get the information of the witnesses.

I edited the problem a bit to clarify: ideally, neither the prover nor verifier knows x. The prover just needs to show they know a valid (signature, plaintext) pair. If i understand correctly, x isn't a witness in this case but rather part of the circuit

Do you mean that the prover, who only have a signature pair $(s, msg)$ but the secret signing key $x$, is just to prove that he/she own a valid signature generated from some public circuit? If so, it is just a verifiable computation problem, rather a zeroknowledge one. Furthermore, your question should be abstract as how to prove that a result correctly generated from some public function? The public function can be viewed as HMAC($x, \cdot$), which certainly can be converted into a arithmetic circuit. In this case, an adversary who get the circuit can easily reverse the secret value $x$.

That's correct; the `x` is just to prove ownership of a valid signature and should not be known by anyone except the one issuing the signature. The signing process isn't public but the verification is. So the question is how to have public verification of a HMAC signature without letting the public know `x`.

If the public function is $HMAC(k, x)$, where $k$ is a fixed key and $x$ as input, then by the technology of zkSNARKs, the $HMAC(k, x)$ can be converted into an instance of QAP firstly, However, in this step, the adversary also can recover the secret value $k$ if the degree of the polynomials is $poly(\cdot)$ size. Next, putting polynomials onto the exponent base $g$, e.g., $g^{l_i(y)}$ where $y$ is a random value, this might keep the $k$ secret due to the hardness of DL problem. Finally, public the $vk$ and $ek$ to both prover and verifier.

For the prover, it can computes $s=HMAC(k,msg)$ and therefore corresponding variables values ${w_i}, i \in [n]$. These values {$w_i$} can be viewed as witnesses. Hence, the prover performs the prove algorithm and outputs a proof $\pi$ and ${s,msg}$ to the verifier. The process I described above is unproven, especially, the method of keeping $k$ secret.

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