feat: Redefine OracleVerifier & lenses for oracle reductions

[quangvdao]

1. We re-define the oracle verifier in an IOR, to have a general way of computing the output oracle statement, instead of hard-coding them to be a subset of the oracles so far.

• This hard-coding will no longer make sense when we switch to dependent oracles / poly functors, since then there won't be an indexed family of types (for oracle statement), just a single type
• More generally, we could think of two versions:
  • The minimal version is that, we only need to specify how oracle access to the output oracle statement can be simulated by oracle access to the input oracle statement & the prover's messages. Nothing needs to be materialized. We will need to generalize everything as well, including security definition, to account for the fact that the oracle verifier has no way to "see" or derive the underlying data of the output oracle statement
  • The more integrated version is to also provide a "reification" function, which is a mapping to output oracle statement at the data level, and also a proof that this reification is actually compatible with the simulation. This is the case for all IORs we know today (where the procedure is just taking subset, linear combination, etc. which are trivially reifiable)
• We chose to do reification by default. This simplifies a lot of definitions and proofs.

[alexanderlhicks]

/review

External:

Internal:

Comments:

[github-actions]

🤖 AI Review (with external context)\n\nGenerating AI review...

Excellent, thank you for the pull request. This is a significant and well-considered refactoring of the oracle reduction framework. The changes introduce a much more principled and modular structure, especially for OracleVerifier and the context Lens definitions.

Here is my review:

High-level Summary

This pull request undertakes a major refactoring of the OracleReduction definitions to better separate concerns, particularly between the data-level ("reification") and oracle-level ("simulation") aspects of an OracleVerifier.

The key changes include:

• OracleVerifier Refactoring: The OracleVerifier structure is split into Verify, Simulate, Reify, and a LawfulReify property, making its components and correctness conditions explicit and modular.
• Lens Refactoring: The OracleContext.Lens is moved to a new file and redesigned to mirror the new OracleVerifier structure, with separate Prover (data) and Verifier (simulation) lenses and a compatibility requirement.
• Security Definition Updates: The Round-by-Round (RBR) soundness definitions, particularly Extractor.RoundByRound and KnowledgeStateFunction, have been generalized to a more standard, iterative formulation.
• API Improvements: New helper types like TrivialStatement and equivalences for composed protocols (Messages.prodEquiv, ChallengeIdx.sumEquiv) have been added, greatly improving code clarity and usability.

Overall, this is an excellent direction that significantly improves the framework's design. However, there are numerous sorry's in critical definitions and proofs that must be addressed before this can be merged.

General Feedback

• Remove commented-out code: There's a fair amount of old, commented-out code. Please remove this to keep the codebase clean.

Specific Feedback & Required Changes

I've identified several crucial parts of the implementation that are incomplete. These are blockers for the merge.

1. ArkLib/OracleReduction/Basic.lean

The new OracleVerifier.ofEmbed constructor is a great way to recover the previous, simpler functionality. However, its simulation logic is missing.

• File: ArkLib/OracleReduction/Basic.lean
• Concern: The simulate field in OracleVerifier.ofEmbed is incomplete.
• Suggestion: The sorrys need to be filled in. This will likely involve using the hData and hInterface assumptions to correctly cast the query q and response types when lifting the query to the [OStmtIn]ₒ or [pSpec.Message]ₒ specs. This can be tricky due to dependent types, but it's essential for this constructor to be usable.

-- ArkLib/OracleReduction/Basic.lean:314
def ofEmbed ... :
  OracleVerifier ... where
  verify := verify
  simulate := fun _ => {
    impl | query i q => match h : embed i with
      | Sum.inl j => sorry -- FIX: Implement simulation for input oracle statements
      | Sum.inr j => sorry -- FIX: Implement simulation for prover messages
  }
  reify := ...
  reify_simulate := sorry -- FIX: This proof will depend on the implementation of `simulate`.

2. ArkLib/OracleReduction/Composition/Sequential/Append.lean

Sequential composition is a core feature, and its implementation for oracle verifiers is currently broken due to multiple sorrys.

• File: ArkLib/OracleReduction/Composition/Sequential/Append.lean
• Concern 1: The instance instSubSpecOfProtocolSpecAppendMessage is incomplete. This instance is fundamental for allowing oracle compositions to correctly handle message oracles.
• Suggestion 1: The sorrys in the monadLift definition need to be resolved. This is a known pain point with eq.rec in Lean. You may need to carefully use cast, eq_rec_mp, or helper lemmas to satisfy the type checker. The new lemma eqRec_eqRec_eq_self might be useful here.

-- ArkLib/OracleReduction/Composition/Sequential/Append.lean:133
instance instSubSpecOfProtocolSpecAppendMessage : ... where
  monadLift | query i t => match i with
    | Sum.inl j => by
        ...
        sorry -- FIX
        ...
        sorry -- FIX
    | Sum.inr j => by sorry -- FIX

• Concern 2: The definition for OracleVerifier.append is missing its core logic and correctness proof.
• Suggestion 2:
  1. Implement the verify field. This should involve running V₁.verify and then using its StmtOut to run V₂.verify. This will require carefully handling the oracle specs using simulateQ and the SubSpec instances.
  2. Implement the reify_simulate proof. This is the crucial correctness guarantee for the composed verifier, proving that the composed reify and simulate fields are compatible. This will be a complex proof, likely involving the reify_simulate properties of V₁ and V₂.

-- ArkLib/OracleReduction/Composition/Sequential/Append.lean:233
def OracleVerifier.append ... where
  verify := fun stmt challenges => by
    ...
    sorry -- FIX: Implement verification logic.

  simulate := ... -- This part looks plausible.

  reify := ... -- This part looks plausible.

  reify_simulate := sorry -- FIX: Implement this crucial proof.

3. ArkLib/OracleReduction/LiftContext/OracleReduction.lean

The framework for lifting an oracle reduction to a new context is also incomplete.

• File: ArkLib/OracleReduction/LiftContext/OracleReduction.lean
• Concern: The implementation of OracleVerifier.liftContext has missing logic, and its key correctness proof (liftContext_toVerifier_comm) is missing. Without these, the entire context-lifting mechanism for oracle reductions is unusable.
• Suggestion:
  1. Fix the sorry within the verify field of liftContext.
  2. Implement the reify_simulate proof, which ensures the lifted verifier is lawful.
  3. Prove liftContext_toVerifier_comm. This theorem is essential, as all the lifted security proofs (liftContext_completeness, liftContext_soundness, etc.) depend on it.

-- ArkLib/OracleReduction/LiftContext/OracleReduction.lean:55
def OracleVerifier.liftContext ... where
  verify := fun outerStmtIn challenges => do
    ...
    let outerStmtOut ← simulateQ sorry (lens.verifier.liftStmt outerStmtIn innerStmtOut) -- FIX
    return outerStmtOut

  ...

  reify_simulate := by
    ...
    sorry -- FIX

-- ArkLib/OracleReduction/LiftContext/OracleReduction.lean:80
theorem OracleVerifier.liftContext_toVerifier_comm ... :
      (V.liftContext lens).toVerifier = V.toVerifier.liftContext lens.toStatement := by
  sorry -- FIX

4. ArkLib/OracleReduction/Security/RoundByRound.lean

The refactoring of RBR soundness is a great improvement, but the connection to the old definition needs to be established.

• File: ArkLib/OracleReduction/Security/RoundByRound.lean
• Concern: The proof of rbrKnowledgeSoundnessOneShot_implies_rbrKnowledgeSoundness is sorry.
• Suggestion: Please provide this proof. It's an important result to show that the new, more general definition of RBR soundness is a strict generalization of the previous one, ensuring backward compatibility of security results.

-- ArkLib/OracleReduction/Security/RoundByRound.lean:222
theorem rbrKnowledgeSoundnessOneShot_implies_rbrKnowledgeSoundness ...
    (h : verifier.rbrKnowledgeSoundnessOneShot relIn relOut rbrKnowledgeError) :
    verifier.rbrKnowledgeSoundness relIn relOut rbrKnowledgeError := by
  ...
  sorry -- FIX

Positive Notes

Despite the required changes, I want to reiterate that the design direction is excellent.

• The rfl proofs for run_eq_run_verifier and run_eq_run_reduction are fantastic and show the power of the new design.
• The new prodEquiv and sumEquiv helpers for composed protocols in ProtocolSpec.lean will make working with composition much cleaner.
• The use of TrivialStatement and TrivialWitness is a great clean-up.

This is a high-quality refactoring. Once the sorry's are addressed, this will be a fantastic improvement to the library.

[quangvdao]

Note: this PR is stale and will be scrapped & rewritten once the new VCVio refactor is ready.

[alexanderlhicks]

Yep no worries, just running the review bot on more or less everything to test it out.