Frequently Asked Questions (FAQ)

Caveats

This page is a best-effort attempt at listing common questions people have when trying to use ArkLib. The source of these Q&As are conversations I've had with other people, which are then passed to an AI and re-generated below. I make no guarantees about the correctness of the responses. If you find that some information is not accurate, feel free to contact me (Quang Dao).

---

Q: How can I use ArkLib in my own Lean project? Is it possible to add it as a Git submodule or use lake dependencies?

A: We have introduced a tag / versioning system, and thus you should be able to build on specific tags without worries of ArkLib breaking in the future.

---

Q: I'm familiar with a specific interactive protocol definition from a paper (e.g., IOPP from STIR). How does this relate to the structures defined in ArkLib, such as OracleReduction and OracleProof?

A: ArkLib provides generalized structures for interactive protocols. Specific protocols from the literature are often instances or specializations of these structures, augmented with specific security guarantees:

• ArkLib.OracleReduction.OracleReduction: This is the most general definition, capturing the interactive structure (messages, challenges, oracle access) between a prover and a verifier over a specified ProtocolSpec.
• ArkLib.OracleReduction.OracleProof: This is a specialization of OracleReduction typically used for decision or verification problems, where the verifier's final output (StmtOut) is constrained to be Bool and the prover's output witness (WitOut) is Unit.
• Specific protocols from the literature, like IOPP, can be seen as instances of these general structures (OracleProof in the case of IOPP). The key difference lies in the specific security guarantees (e.g., completeness, knowledge soundness) that are proven about such an instance, which are defined separately.

---

Q: How should I represent a specific protocol like IOPP, which has particular completeness and soundness properties, using ArkLib?

A: One approach is to define a new structure for your specific protocol that extends OracleProof (or OracleReduction if the output types differ). Then, add fields to this new structure to hold the proofs or statements of the required security guarantees.

For example:

import ArkLib.OracleReduction.Security.Basic -- ... and other relevant imports

structure IOPP (pSpec : ProtocolSpec n) -- ... other type parameters
  extends OracleProof pSpec oSpec Statement Witness OStatement where
  completeness : PerfectCompleteness prover verifier exact_relation -- Fix notation as needed
  proximity_soundness : knowledgeSoundness verifier extractor proximity_relation -- Fix notation as needed
  -- ... other properties if needed

This approach effectively bundles the protocol's interactive interface (inherited from OracleProof) with its defining security properties.

---

Key Concepts & Potential Points of Confusion

• Separation of Concerns: Protocol Interface vs. Security Guarantees: It's important to distinguish between:

  1. The definition of the interactive protocol's structure: This includes the types of statements, witnesses, messages, the number of rounds, the prover/verifier computations, and oracle access patterns. This is what structures like OracleReduction, OracleProof, Prover, and Verifier in ArkLib.OracleReduction are designed to capture.
  2. The security properties proven about a protocol instance: These are mathematical guarantees like completeness, soundness (various forms), zero-knowledge, etc. They are properties about a specific protocol constructed using the ArkLib framework and are typically defined and proven in terms of relations involving the protocol's inputs and outputs.

  While often discussed together, ArkLib primarily provides the tools to define the structure (1), upon which security guarantees (2) can be formally stated and proven.