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
A BHK style interpretation seems to me a good suggestion. Also writing explicit intro- and elim-rules for the types concerned.
Both are sensible methodologies to approach any challenge of the form “we are trying here to formalize a … proof”.
I was asked to comment here but I’m not firm on the goal, but I’ll do my best to contribute something productive. There seems to be two discussions going on here;
The first discussion pertains to the engineering problem of designing an API for nodes to send and receive assumptions and witnesses that satisfy those assumptions. I don’t have much to add here. Intuitively, this could be handled in a way that’s similar to how we agreed to handle engine types; just a big coproduct of names that can be modified over time. This was already suggested in the first post in this thread.
This would involve maintaining a public description of common assumptions and their relation to eachother. Since assumptions have a semantics (corresponding to propositions, at least), this implies structure which can be exploited to compose them.
If all we’re doing is maintaining a canonical description of assumptions + relations between these assumptions, then this should be captured by an appropriate Datalog program. I think this can be used as a guiding answer. Pick Datalog as your simple model and design the interface around that model. Assume verification is executing a specific datalog query against a database of assumptions which have been submitted by other nodes, etc.
The second discussion pertains to the theoretical problem of what the correct way to describe proofs/arguments of knowledge is in general (what would God do?). This has come up in some guise in previous discussions. In one I had with Chris he mentioned Conal Elliott’s unfinished work on “denotational ZKPs”, which would, hypothetically address this issue. Separately, the BHK interpretation was mentioned as a general description of types, but this view is rarely used when describing proof/arguments of knowledge. I don’t think anyone knows a complete answer to the question being asked. However, a recent thesis out of CMU describes a compositional framework for proofs/arguments of knowledge in terms of BHK-like computational reductions between relations between statements and witnesses. Essentially, instead of arguing that a statement is true, the arguments are that a statement must be true given a different statement.
An argument of knowledge is then a reduction to the trivial relation with one statement and one witness. Some constructs like Fiat-Shamir and folding schemes are also described in the paper.
The penultimate chapter of that thesis describes the category of such reductions and establishes that it’s a symmetric monoidal category w/ a notion of parallel reduction acting as tensor, but doesn’t establish much beyond that. I suspect that it also has coproducts, probably all finite (co)limits, and, judging by how sequential composition is described, it’s probably a category of optics of some kind. This can be used to get a list of constructs that proofs ought to support in general. This is probably the closest thing to a complete answer to the bigger, theoretical question that currently exists. But pursuing that would require original research that may be out of scope.