Towards a general proof type

Protocol Design
6

Yes, sorry that was an error :sweat_smile:. I meant: There is a “1 proof”-to-“many assumptions” relation per proof.

Then we would bootstrap by agreeing on a set of canonical (proof, [assumption]) 1-to-many relations, e.g.

  • (trivial, [code])
  • (SNARK, [theorem1, theorem2])
  • (trusted delegation, [signature by myself])
  • etc.

For any new proof type that a node chooses to accept, it adds the assumptions to the “accepted assumptions list”, or it can add/remove assumptions explicitly, e.g. “accept signatures from this identity for trusted delegation proofs”. All this could be built on a sum type.

Yes, this would be the goal, as it seems useful for recursive multievaluation.

Then we could also do things like take assumptions of proof types and decompose them:
If I receive the relation (theorem1, [theorem3, theorem4]), including a valid proof of a type and assumptions I already accept I could include that into the hierarchy to resolve theorem1 and use proofs that either assume theorem3 or theorem4. Note: Should these relations be (optionally) bijective, or do we want to have many-to-many ([assumption], [assumption]) relations too? many-to-many ([proof type], [assumption]) seems less useful.

Or, if I want to accept delegation proofs, I add it via the canonical self delegation proof mentioned above. Doing this would generalize delegating delegation.

I think the only thing we need to do for this would be to store the (proof type, [assumption]) relations together with the proofs they came with, to reconstruct the hierarchy when needed, or just cache it.

We need to make distinctions of the type “I accept this proof type” and “I accept new relations verified by this proof type”, but this can happend on another layer, that has access to relevant information.

If we can agree on canonical bootstrapping types for the initial sum type, the dynamic fields could probably be content adressed and observer dependent, with the functions being the same everywhere.

In that sense, we would only use the canonical base multiformat as an anchor for the individual hierarchy of every node.