I do not know enough about ZK proofs to say what it takes to represent them, but using (co)equality types (i.e. pushouts and pullbacks rather than just coproducts and products) as our basic types as described in Data & function encoding - #18 by terence would allow some examples of the above. In particular, for example, global elements (morphisms from the terminal object) into equalizers correspond to:
“trivial proofs” where verifying the proof requires simply computing the function