doc(oracle-reduction): add conceptual documentation for Basic.lean

[Sfgangloff]

Hi,

While reading through OracleReduction/Basic.lean, I found that the core abstractions (prover, verifier, oracle verifier) are quite rich but not easy to parse at a conceptual level.

I would like to contribute a conceptual documentation for this file, making the mathematical structure more explicit. The plan is to:

• describe the prover/verifier interaction model (states, messages, challenges)
• explain the role of oracle access and the embed mechanism
• clarify the separation between interaction, execution, and security

The goal is to complement existing docstrings with a higher-level explanation of the design.
I can either:

• extend the module docstring in Basic.lean, or
• write a separate markdown-style document, including schema

I would start with Basic.lean, and potentially extend to other files if useful.

Does this direction and format sound good?

[quangvdao]

Thanks! I agree more documentation is helpful. We have a very outdated blueprint, and I'm doing a rewrite of the core IOR layer at #433 . I expect this to be merged some time next month, which will come with better documentation.

[Sfgangloff]

Thanks, that makes sense. Since the core layer is being rewritten in #433, is there any area in the current repo where contributions would still be useful in the meantime (e.g. tests, examples, documentation, or small refactors), or should I just wait for the new structure to stabilize?

[quangvdao]

Thanks for following up. I think it would be better not to spend effort documenting the current OracleReduction/Basic.lean API directly while #433 is still rewriting the core interaction/IOR layer.

One useful direction in the meantime would be documentation that is less tied to the exact current API surface. In particular, #457 is adding a repository knowledge base under docs/kb/, with concept pages, paper pages, and audit-style notes. A good contribution could be to add or improve KB material around interactive oracle proofs / oracle reductions: e.g. explain the conceptual roles of prover, verifier, oracle access, execution, and security, and link that to the relevant ArkLib modules and references.

That way the work can survive the API rewrite better than a detailed module-docstring pass on the old core file. Once #457 lands, I’d suggest starting with a focused KB/concept page rather than modifying OracleReduction/Basic.lean directly.

Posted by Cursor assistant (model: GPT-5.5) on behalf of the user (Quang Dao) with approval.

[lekt9]

Heads-up in case it helps scope this: OracleReduction/Basic.lean already carries a fairly complete conceptual overview in its module docstring (currently lines 9–201), and it covers the three points in your plan quite directly:

• Prover/verifier interaction model (states, messages, challenges): sections ## The Prover and ## The Verifier.
• Oracle access and the embed mechanism: sections ## The Oracle Verifier, ### OracleInterface, and ## The embed Mechanism.
• Separation of interaction / execution / security: section ## Interaction, Execution, and Security: The Three Layers (with explicit 1. Interaction (syntax) / 2. Execution (semantics) / 3. Security (properties) subsections).

It also includes a File Scope schema table and a Quick Reference: Key Definitions section.

So the direction you proposed largely already exists in-tree. If you were planning additional depth (e.g. worked examples, a separate markdown design doc, or extending the same treatment to other files), that could still be valuable — but the core conceptual overview for Basic.lean itself looks done. Maintainers may want to close or re-scope accordingly.