Development of Interactive (Oracle) Reductions

[quangvdao]

This issue hosts all development of interactive (oracle) reductions and their composition.

The following are immediate targets to work on:

• Definition of OracleVerifier.append for composing two oracle verifiers.
• Definitions for composing multiple (oracle) reductions. This requires development of a general API for Fin.fold, together with other missing Mathlib theorems.
• Proofs that composition of two (oracle) reductions preserve completenes & all notions of soundness.

Some nice-to-have things that are not actively worked on:

• Definition of state-restoration (knowledge) soundness
• Definition of rewinding (knowledge) soundness
• Definition of honest-verifier zero-knowledge