feat(SendClaim): prove perfect completeness by XC0R · Pull Request #445 · Verified-zkEVM/ArkLib

XC0R · 2026-04-04T18:26:02Z

Proves SendClaim.completeness — perfect completeness for the SendClaim component of the sumcheck oracle reduction chain. This was the last remaining sorry in the four-component completeness pipeline (CheckClaim → ReduceClaim → RandomQuery → SendClaim).

What's proved

SendClaim.oracleReduction has perfect completeness: for any valid witness, the verifier accepts with probability 1 in the ideal oracle model.

Technique

The proof peels through the layered monad stack (OptionT / StateT / OracleComp) using:

simulateQ_map / simulateQ_bind / simulateQ_pure to push simulateQ through each prover and verifier bind
Option.elimM_map to bridge OptionT.run across simulateQ boundaries
StateT.run_map to convert Functor.map inside StateT to the underlying ProbComp level

The completeness event splits into two obligations: (1) the computation never returns none (failure), and (2) every output satisfies the relation. Both reduce to showing that simulateQ preserves the some <$> _ structure at each layer, then closing the oracle equality via Subsingleton.elim and Unique.uniq on the unit-indexed oracle types.

Context

Builds on the completeness chain from #444 (CheckClaim + ReduceClaim + RandomQuery) and the upstream monadLift_liftM_OptionT coherence lemma contributed in Verified-zkEVM/VCV-io#259.

chatgpt-codex-connector · 2026-04-04T18:26:08Z

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 · 2026-04-04T18:28:01Z

🤖 Gemini PR Summary

Proves SendClaim.completeness, establishing perfect completeness for the sumcheck oracle reduction chain. This resolves the final remaining sorry in the four-component completeness pipeline (CheckClaim → ReduceClaim → RandomQuery → SendClaim).

Mathematical Formalization

Established that SendClaim.oracleReduction has perfect completeness: for any valid witness, the verifier accepts with probability 1 in the ideal oracle model.
Verified that the computation never returns none (failure) and that all outputs satisfy the required relation.
Closed oracle equality obligations using Subsingleton.elim and Unique.uniq on unit-indexed oracle types.

Proof Technique

Peels through the layered monad stack (OptionT / StateT / OracleComp) by applying simulateQ_map, simulateQ_bind, and simulateQ_pure to push simulations through prover and verifier binds.
Utilized Option.elimM_map to bridge OptionT.run across simulateQ boundaries.
Used StateT.run_map to convert Functor.map operations within StateT to the underlying ProbComp level.

Status

Resolved the final sorry in the sumcheck completeness pipeline; no new sorry placeholders or admit calls were introduced.

Statistics

Metric	Count
📝 Files Changed	1
✅ Lines Added	107
❌ Lines Removed	1

Lean Declarations

No declarations were added, removed, or affected.

sorry Tracking

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

theorem completeness [Nonempty σ] : in ArkLib/ProofSystem/Component/SendClaim.lean (L113)

🎨 **Style Guide Adherence**

Line 109: prover_first' := by simp - "Place by at the end of the line preceding the tactic block. Indent the tactic block."
Line 121: ... = fun x => (pure (some x) : - "Prefer fun x ↦ ... over λ x, ...." (The guideline specifies ↦ as the preferred map arrow).
Line 124: erw [simulateQ_bind]; erw [simulateQ_pure]; simp only [pure_bind] - "Avoid using ; to separate tactics unless writing short, single-line tactic sequences." (Three distinct tactics including a simp only call exceed the typical definition of a short sequence).
Line 125: erw [simulateQ_bind]; erw [simulateQ_pure]; simp only [pure_bind] - "Avoid using ; to separate tactics unless writing short, single-line tactic sequences."
Line 132: exact ⟨by { - "Place by at the end of the line preceding the tactic block. Indent the tactic block."
Line 147: erw [simulateQ_map] at hval; erw [simulateQ_map] at hval; erw [simulateQ_map] at hval - "Avoid using ; to separate tactics unless writing short, single-line tactic sequences." (Repetitive long-form tactics should be placed on new lines or use combinators like repeat).
Line 150: ... (by simp) - "Place by at the end of the line preceding the tactic block. Indent the tactic block."
Line 153: }, by { - "Place by at the end of the line preceding the tactic block. Indent the tactic block."
Line 171: erw [simulateQ_map] at hval; erw [simulateQ_map] at hval; erw [simulateQ_map] at hval - "Avoid using ; to separate tactics unless writing short, single-line tactic sequences."

📄 **Per-File Summaries**

ArkLib/ProofSystem/Component/SendClaim.lean: Replaces a sorry placeholder in the completeness theorem with a formal proof for the SendClaim component. The proof establishes the perfect completeness of the oracle reduction by unfolding the prover-verifier interaction and performing probability decomposition.

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

alexanderlhicks · 2026-04-04T22:51:01Z

ArkLib/ProofSystem/Component/SendClaim.lean

+    dsimp only [] at hx
+    -- Case split on val
+    rcases val with _ | ⟨a⟩
+    · -- val = none: contradicts hval (same as Part 1)


this blocks seems like a repetition of the one above (line 173 and down), perhaps it's worth putting this into a have?

alexanderlhicks · 2026-04-04T22:52:01Z

ArkLib/ProofSystem/Component/SendClaim.lean

+      obtain ⟨rfl, -⟩ := hx
+      -- xval (= x) is now concrete but still contains a
+      -- Peel hval to determine a (same layers as none case)
+      simp only [bind_pure_comp] at hval


This also seems to repeat the same block of steps as from line 216 and 173.

alexanderlhicks · 2026-04-04T22:53:53Z

ArkLib/ProofSystem/Component/SendClaim.lean

+This is the key missing piece for SendClaim completeness: every layer of `liftM`/`simulateQ`
+preserves the `some <$> _` structure, so `none` can never appear in the output support.
+TODO: upstream to VCVio as a general `support_simulateQ` or `none_not_mem_support_map_some`. -/
+private lemma none_not_mem_support_map_some {m : Type _ → Type _}


this doesn't seem like it's used anywhere?

alexanderlhicks · 2026-04-04T23:06:02Z

ArkLib/ProofSystem/Component/SendClaim.lean

+  rw [support_map]; rintro ⟨_, _, ⟨⟩⟩
+
+
+set_option synthInstance.maxHeartbeats 800000 in


why are these maxheartbeat/maxrecdepth values so high here?
I locally replaced the remaining simp at hval steps (lines 185, 225, 242) with simp only calls and this seems to remove the need for these (amongst other benefits).

XC0R · 2026-04-05T00:07:56Z

Commentary heeded —

Repeated blocks (216, 235): Compressed to 3 lines each. Attempted have extraction but Lean 4 hygiene renames hval → hval✝ after rcases, blocking shared reference. Open to suggestions if you have a pattern that works around this.

Unused lemma (114): Removed. Leftover from earlier approach — simp handles the contradiction via support_map + constructor discrimination.

High limits (121): Both maxHeartbeats 1600000 and maxRecDepth 2000 removed, builds within defaults. synthInstance.maxHeartbeats 800000 retained for elaboration. Cleaned unused simp args the linter flagged.

- Remove unused none_not_mem_support_map_some lemma - Remove maxHeartbeats 1600000 and maxRecDepth 2000 (builds within defaults) - Clean unused simp arguments flagged by linter - Compress repeated simulateQ/OptionT peel blocks

feat(SendClaim): prove perfect completeness — close all sorrys

0518bd8

alexanderlhicks reviewed Apr 4, 2026

View reviewed changes

alexanderlhicks self-assigned this Apr 4, 2026

refactor(SendClaim): address review feedback

5df19b8

- Remove unused none_not_mem_support_map_some lemma - Remove maxHeartbeats 1600000 and maxRecDepth 2000 (builds within defaults) - Clean unused simp arguments flagged by linter - Compress repeated simulateQ/OptionT peel blocks

XC0R force-pushed the sendclaim-completeness branch from ed6df0d to 5df19b8 Compare April 5, 2026 00:16

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(SendClaim): prove perfect completeness#445

feat(SendClaim): prove perfect completeness#445
XC0R wants to merge 2 commits intoVerified-zkEVM:mainfrom
XC0R:sendclaim-completeness

XC0R commented Apr 4, 2026

Uh oh!

chatgpt-codex-connector bot commented Apr 4, 2026

Uh oh!

github-actions bot commented Apr 4, 2026 •

edited

Loading

Uh oh!

alexanderlhicks Apr 4, 2026

Uh oh!

alexanderlhicks Apr 4, 2026

Uh oh!

alexanderlhicks Apr 4, 2026

Uh oh!

alexanderlhicks Apr 4, 2026

Uh oh!

XC0R commented Apr 5, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

		rw [support_map]; rintro ⟨_, _, ⟨⟩⟩


		set_option synthInstance.maxHeartbeats 800000 in

Conversation

XC0R commented Apr 4, 2026

What's proved

Technique

Context

Uh oh!

chatgpt-codex-connector bot commented Apr 4, 2026

Uh oh!

github-actions bot commented Apr 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 Gemini PR Summary

Mathematical Formalization

Proof Technique

Status

Uh oh!

alexanderlhicks Apr 4, 2026

Choose a reason for hiding this comment

Uh oh!

alexanderlhicks Apr 4, 2026

Choose a reason for hiding this comment

Uh oh!

alexanderlhicks Apr 4, 2026

Choose a reason for hiding this comment

Uh oh!

alexanderlhicks Apr 4, 2026

Choose a reason for hiding this comment

Uh oh!

XC0R commented Apr 5, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

github-actions bot commented Apr 4, 2026 •

edited

Loading