Proof encoding¶

Proof are encoded as the pair of a natural number identifier (specifying a particular proof system) and bytes (the proof content).

type Proof := mkProof {
    proofSystemIdentifier : Natural;
    proofSystemBytes : []byte;
};

We then define the canonical proof verifier as a switch-case over these proving systems.