Towards a general proof type

Protocol Design
12

Using the data types described here, it would look roughly as follows (please excuse any potential errors in type theoretic notation, I hope this is clear enough):

Non-recursive version

type ProofRelation := ProductT [ CanonicalProofTypeV, ProductT [CanonicalAssumptionV] ]

type MultiProofT := CoproductT [ProofT]
type ProofV      := ProductT [ CanonicalProofTypeV, BasicValue ]

type CanonicalTypeV       := CoproducT [ DataValue ]
type CanonicalAssumptionV := CoproducT [ DataValue ]

Here, the DataValue in CanonicalTypeV and CanonicalAssumptionV are lists of encodings of proof types and assumptios and need to be picked at type instantiation. Then we can use content addressing to refer to any MultiProofT and need some mechanism to agree on the canonical base MultiProof. These proofs could live next to each other, and the node could just chose which ones to admit.

Recursive version

type ProofRelationAssertion := Product [ ProductT [ ProofTypeV, ProductT [AssumptionV] ],  AssertionV]
type AssertionV             := CoproductT [ MultiProofV, Nothing ]

type MultiProofT := CoproductT [Proof] 
type ProofV      := CoproductT [ ProductT [ ProofType, BasicValue ],  Nothing ]

type ProofTypeV  := CoproductT [ DataValue ]
type AssumptionV := CoproductT [ DataValue ]

(Note: ProofV and Assertion are supposed to be a specialized option type. See this question for context. ProofV might need to be a DataValue, but I’m not sure how expressive this needs to be.)

If we want to bootstrap a recursive system this way, the base ProofRelationAssertion and a base Multiproof could look something like this:

base_relation = [ "delegation proof by multisig", ["sig by ID1 exists", "sig by ID2 exists", ..., "sig by IDN exists"], Nothing ] 

base_multiproof(sigs) = {
  ProofV                = "delegation proof by multisig", sigs
}

base_relation could encode, for example, the trust assumptions of the network governance committee.

The next relation and an example proof:

next_level_of_relation = ["some new type", ["some", "new", "assumptions"], base_multiproof("sigs of ID 1 to N")]

next_level_multiproof(args) = {
  ProofV                      = "some new type", "something derived from args"
}

I’m sure this can be simplified or expressed more elegantly, but as a first approximation I think this is how we should be able to build things up recursively. Does this make sense? Please feel free to ask clarifying questions or point out errors.

1 Like