feat(Sumcheck/Simple): prove perfect completeness for single-round reduction

[XC0R]

Summary

• Prove Simple.reduction_perfectCompleteness — perfect completeness for the
  non-oracle single-round sumcheck reduction (0 sorrys, was 2)
• Both branches of the probEvent proof closed:
  • No-failure: guard always passes (hValid + Fin.snoc evaluation), getM always succeeds
  • All-outputs: concrete prover output satisfies outputRelation after full simulateQ decomposition
• oracleReduction_perfectCompleteness follows once oracleVerifier_eq_verifier is resolved

Technique

Layer-by-layer simulateQ support decomposition:
erw [simulateQ_bind] → StateT.run_bind → mem_support_bind_iff for peeling,
addLift_def + simulateQ_add_liftComp_* for liftComp stripping,
norm_num after simp [Fin.snoc] for dite evaluation,
Finset.sum_map at hValid for guard matching.

[chatgpt-codex-connector]

Codex usage limits have been reached for code reviews. Please check with the admins of this repo to increase the limits by adding credits.
Credits must be used to enable repository wide code reviews.

[github-actions]

🤖 Gemini PR Summary

Core Formalization

• Proves Simple.reduction_perfectCompleteness, establishing perfect completeness for the single-round non-oracle sumcheck reduction.
• Removes 2 sorry placeholders, transitioning the proof to a fully verified state.
• Completes both branches of the probEvent proof:
  • No-failure: Verifies that the guard passes and state retrieval (getM) succeeds using Finset.sum_map and Fin.snoc.
  • All-outputs: Ensures the resulting state satisfies outputRelation through simulateQ decomposition.
• Establishes the foundation for oracleReduction_perfectCompleteness, pending the resolution of oracleVerifier_eq_verifier.

Technical Implementation

• Implements layer-by-layer simulateQ support decomposition using simulateQ_bind, StateT.run_bind, and mem_support_bind_iff.
• Handles liftComp stripping and state transformations via addLift_def and simulateQ_add_liftComp_* lemmas.
• Utilizes norm_num and Fin.snoc for evaluation of dite blocks and protocol guards.

---

Statistics

Metric	Count
📝 Files Changed	1
✅ Lines Added	189
❌ Lines Removed	46

---

Lean Declarations

• No declarations were added, removed, or affected.

---

sorry Tracking

✅ **Removed:** 1 `sorry`(s)

• theorem reduction_perfectCompleteness : in ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean (L488)

---

🎨 **Style Guide Adherence**

The code changes have several style guide violations. Because there are more than 20 violations, they are grouped by the specific rule they violate:

• Empty Lines: "Avoid empty lines inside definitions or proofs."

  • Count: 33 instances.
  • Representative Examples:
    • Line 477: Empty line immediately after the first tactic.
    • Line 485: Empty line between simp and split tactics.
    • Line 505: Empty line inside a nested tactic block (bulleted section).

• Variable Conventions (Hypotheses): "Use h, h₁, ... : Assumptions/Hypotheses"

  • Count: > 40 instances (descriptive names used across the proof).
  • Representative Examples:
    • Line 476: Use of hValid instead of h or h₁.
    • Line 483: Use of hDir0 instead of h or h₂.
    • Line 509: Use of hmem instead of h or h₃.

• Variable Conventions (Elements): "Use x, y, z, ... : Elements of a generic type"

  • Count: > 30 instances (descriptive element/state names used throughout).
  • Representative Examples:
    • Line 476: Use of target for an element of a type.
    • Line 509: Use of s for a state (generic element), which the guide reserves for Sets or Lists.
    • Line 518: Use of val and s₀ for elements of generic types.
    • Line 534: Use of chal_res and s₂ for elements of generic types.

---

📄 **Per-File Summaries**

• ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean: This change completes the proof of the reduction_perfectCompleteness theorem by replacing a sorry placeholder with a detailed formal argument. The updated proof explicitly decomposes the protocol's execution steps and uses simulation lemmas to demonstrate that a valid input relation always results in a successful verifier check and a valid output relation.

---

Last updated: 2026-04-05 18:22 UTC.