Todo

This whole page needs to be reworked.

Questions:

- What should this type be now?
- Is everything just a provable VM?
- VM gives the semantics to interpret the function, which seems necessary.
- We have some type of assumptions \(Assumption\)
- \(prove_n\) generates the proof of type \(Proof_n\)
- \(assumptions_n\) returns the assumptions required for a proof
- \(verify_n\) verifies a proof of type \(Proof_n\)

# Proof¶

We define a set of structures required to define a proving system \(PS\) as follows:

- Proof \(\pi: PS.Proof\)
- Instance \(x: PS.Instance\) is the public input used to produce a proof.
- Witness \(w: PS.Witness\) is the private input used to produce a proof.
- Proving key \(pk: PS.ProvingKey\) contains the secret data required to produce a proof for a pair \((x, w)\).
- Verifying key \(vk: PS.VerifyingKey\) contains the data required, along with the witness \(x\), to verify a proof \(\pi\).

A **proof record** carries the components required to verify a proof. It is defined as a composite structure \(PR = (\pi, x, vk): ProofRecord\), where:

- \(ProofRecord = PS.VerifyingKey \times PS.Instance \times PS.Proof\)
- \(vk: PS.VerifyingKey\)
- \(x: PS.Instance\)
- \(\pi: PS.Proof\) is the proof of the desired statement

A proving system \(PS\) consists of a pair of algorithms, \((Prove, Verify)\):

- \(Prove(pk, x, w): PS.ProvingKey \times PS.Instance \times PS.Witness \rightarrow PS.Proof\)
- \(Verify(pr): PS.ProofRecord \rightarrow \mathbb{F}_b\)

A proving system must have the following properties:

**Completeness**: it must be possible to make a proof for a statement which is true.**Soundness**: it must not be possible to make a proof for a statement which is false.

Certain proving systems may also be **Zero-Knowledge**, meaning that the produced proofs reveal no information other than their own validity.

A proof \(\pi\) for which \(Verify(pr) = 1\) is considered valid.

For example, let's take three common instantiations:

- The
*trivial*scheme is one where computation is simply replicated. The trivial scheme is defined as`verify(a, b, predicate, _) = predicate a b`

(with proof type`()`

). It has no extra security assumptions but is not succinct.

- The
*trusted delegation*scheme is one where computation is delegated to a known, trusted party whose work is not checked. The trusted delegation scheme is defined as`verify(a, b, predicate, proof) = checkSignature (a, b, predicate) proof`

, where the trusted party is assumed to produce such a signature only if`predicate a b = 1`

. This scheme is succinct but requires a trusted party assumption (which could be generalised to a threshold quorum in the obvious way). Note that since the computation is still verifiable, a signer of`(a, b, predicate)`

where`predicate a b = 0`

could be held accountable by anyone else who later checked the predicate.

- The
*succinct proof-of-knowledge*scheme is one where the result of computation is attested to with a cryptographic proof (of the sort commonly instantiated by modern-day SNARKs & STARKs). Succint proof-of-knowledge schemes provide succinctness as well as veriability subject to the scheme-specific cryptographic assumptions. They may also possibly be*zero-knowledge*, in which the verifier learns nothing other than`predicate a b = 1`

(in this case, and in others,`a`

and`b`

will often be "hidden" with hash functions, such that the verifier knows only`hash a`

and`hash b`

but the substance of the relation obtains over the preimages).