Can Zk-SNARKs verify the results of turing-complete computations? My understanding is that Zk-SNARKs (and zero-knowledge proofs in general) can be used to prove that a polynomial-time computation has a certain output, while keeping one or more of the inputs to that computation hidden.

For example, say you have a string h which is the output of a fixed hash function. If you know an input x which hashes to h, you could use a Zk-SNARK to prove you know x in zero knowledge (i.e. without revealing x). Equivalently, given a verification function like this:

verify(x,h):
    return hash(x) == h


you're essentially proving that you know inputs to verify which make it return true, without revealing all of those inputs.

So, here's my question. Suppose you have a secret poly-time, single-argument function f. Given a public input x and a public output y, could you use a Zk-SNARK to prove in zero knowledge that f(x)=y? I.e., given the function

verify(f,x,y):
    return f(x) == y


could you still construct a proof showing that verify returns true while keeping f secret? The difference between this situation and the above one is that now you're proving something about a verify function that is itself running an arbitrary function, rather than one which simply does some fixed calculations to check things--and this seems like a pretty significant difference to me. 

It seems like this should be possible in theory, because if f is poly-time then f(x)=y is still an NP statement (although I may be wrong about that)--but I'm wondering if it's possible in practice with today's Zk-SNARKs.

The way I phrased my question, I guess knowledge of such a function is trivial, because if the prover knew y in advance, they could just define f to return y. So to make things more interesting, you could imagine a situation where the prover commits to f in advance, and the proof is expanded to verify that the f used to compute y matches the commitment.
Yes. Express $f$ as a (say, Boolean) circuit. If $f$ is poly-time it will have a number of gates that is polynomial in the input size. A universal circuit $U$ is a Boolean circuit that evaluates any circuit up to bounded size (see e.g. this eprint from 2017 by Günther, Kiss and Schneider). The input to $U$ will be bits representing the structure of the circuit of $f$. Since $U$ is just another Boolean circuit, it can also be represented as a QAP as in the Pinocchio paper, or whatever the zk-SNARK uses.