Skip to content

feat(Stir): prove out_of_dom_smpl_1 (STIR Lemma 4.5.1, out-of-domain sampling)#637

Open
aryaethn wants to merge 2 commits into
Verified-zkEVM:mainfrom
aryaethn:feat/stir-out-of-dom-smpl-1
Open

feat(Stir): prove out_of_dom_smpl_1 (STIR Lemma 4.5.1, out-of-domain sampling)#637
aryaethn wants to merge 2 commits into
Verified-zkEVM:mainfrom
aryaethn:feat/stir-out-of-dom-smpl-1

Conversation

@aryaethn

@aryaethn aryaethn commented Jul 11, 2026

Copy link
Copy Markdown
Contributor

Stacked on #634 — this PR builds on the general probability lemmas added there. Until #634 merges, this PR's diff shows two commits (the shared Data/Probability/Instances.lean additions from #634, plus the STIR proof here); once #634 lands, GitHub drops the shared commit and the diff collapses to just ProofSystem/Stir/OutOfDomSmpl.lean. Please review/merge #634 first.

What this does

Replaces the sorry in out_of_dom_smpl_1 (STIR [ACFY24stir] Lemma 4.5.1, the out-of-domain sampling collision bound) with a full proof, making OutOfDomSmpl.lean sorry-free (out_of_dom_smpl_2 already consumed it as a black box).

Proof structure

Standard union-bound × i.i.d.-product × root-count argument:

  • single_coord_bound — for two distinct codewords u ≠ u', a single uniform out-of-domain point x ∈ 𝔽 \ φ(ι) makes their decoded polynomials agree with probability ≤ (degree-1)/(|𝔽|-|ι|): the difference toPolynomial u - toPolynomial u' is nonzero (distinct codewords ⟹ distinct interpolants, via toPolynomial_eval_at_domain) of degree < degree, so it has at most degree-1 roots among the |𝔽|-|ι| out-of-domain points.
  • pair_agree_bound — extends over the s independent points via Pr_forall_eq_pow, giving ((degree-1)/(|𝔽|-|ι|))^s.
  • out_of_dom_smpl_1 — union bound (Pr_exists_le_sum) over the binom(k,2) two-element subsets of the δ-close list, where k ≤ l by list-decodability. Indexing the union by unordered pairs (Finset.powersetCard 2) is what yields the l(l-1)/2 factor (rather than l(l-1)).

Notes

aryaethn added 2 commits July 10, 2026 23:30
@aryaethn
feat(Data/Probability): add finite union bound, independence, and i.i…
188ad26 
….d. power lemmas

Three general-purpose probability lemmas over PMF sampling, proved from the
existing `prob_tsum_form_*` / `prob_split_last_uniform_sampling_of_finFun`
infrastructure in this file:

- `Pr_exists_le_sum`: finite union bound, Pr[∃ b, P b] ≤ ∑ b, Pr[P b].
- `Pr_and_indep`: independence factorization, Pr[A x ∧ B y] = Pr[A x]·Pr[B y]
  for two independent samplings.
- `Pr_forall_eq_pow`: Pr over s i.i.d. uniform samples that all satisfy Q
  equals (single-sample Pr)^s.

All three are reusable across the proximity-gap / STIR soundness proofs, which
repeatedly need union bounds and i.i.d. product bounds over uniform sampling.
@aryaethn
feat(Stir): prove out_of_dom_smpl_1 (STIR Lemma 4.5.1)
1968a12 
Replaces the sorry in `out_of_dom_smpl_1` (out-of-domain sampling collision
bound) with a full proof, making OutOfDomSmpl.lean sorry-free.

Proof outline (union bound over 2-element subsets of the list × i.i.d. product
× univariate root count):
- `single_coord_bound`: for distinct codewords, one random out-of-domain point
  makes their decoded polynomials agree with probability ≤ (degree-1)/(|F|-|ι|),
  since the difference polynomial is nonzero of degree < degree.
- `pair_agree_bound`: extend over s independent points via Pr_forall_eq_pow.
- `out_of_dom_smpl_1`: union-bound (Pr_exists_le_sum) over the binom(k,2)
  two-element subsets of the delta-close list (k ≤ l by list-decodability),
  giving the l(l-1)/2 factor.

Depends on the general probability lemmas Pr_exists_le_sum / Pr_and_indep /
Pr_forall_eq_pow (added to Data/Probability/Instances.lean).
@github-actions

github-actions Bot commented Jul 11, 2026

Copy link
Copy Markdown
Contributor

🤖 PR Summary

sorry delta: -1 (1 removed) — net proof progress

Mathematical Formalization

  • The central result is out_of_dom_smpl_1 (STIR Lemma 4.5.1), a bound on the probability that two distinct codewords from a δ‑close list agree on all s independent uniform out‑of‑domain samples. The bound: Pr ≤ (l choose 2) * ((deg−1)/(|F|−|ι|))^s, where l is the list length and k ≤ l by list‑decodability.
  • The proof is structured as a chain of lemmas:
    • single_coord_bound: For a single sample, the agreement probability for distinct codewords is bounded by (degree−1)/(|F|−|ι|) (root‑count argument using toPolynomial_eval_at_domain).
    • pair_agree_bound: Extends to s independent samples via Pr_forall_eq_pow, yielding ((deg−1)/(|F|−|ι|))^s.
    • agree_symm: Symmetry of agreement relation.
    • The main theorem uses a union bound (Pr_exists_le_sum) over unordered pairs (Finset.powersetCard 2) of codewords, giving the binomial coefficient factor l(l−1)/2.

Proof Completion (sorries removed)

  • The sorry placeholder in out_of_dom_smpl_1 is now replaced with a full proof. All previous sorries in ArkLib/ProofSystem/Stir/OutOfDomSmpl.lean are eliminated, rendering the file sorry‑free.
  • The theorem was previously used as a black box by out_of_dom_smpl_2; now it is proved.

Probability Library Extensions

Infrastructure / CI

  • lake build passes with no new lint warnings on the modified files.

Statistics

Metric Count
📝 Files Changed 2
✅ Lines Added 242
❌ Lines Removed 1

Lean Declarations

✏️ Added: 6 declaration(s)

ArkLib/Data/Probability/Instances.lean (3)

  • theorem Pr_and_indep {α β : Type} (D₁ : PMF α) (D₂ : PMF β) (A : α → Prop) (B : β → Prop) :
  • theorem Pr_exists_le_sum {α β : Type} [Fintype β] (D : PMF α) (P : β → α → Prop) :
  • theorem Pr_forall_eq_pow {C : Type} [Fintype C] [Nonempty C] (s : ℕ) (Q : C → Prop) :

ArkLib/ProofSystem/Stir/OutOfDomSmpl.lean (3)

  • lemma agree_symm {degree s : ℕ} {φ : ι ↪ F} (a b : code φ degree)
  • lemma pair_agree_bound (φ : ι ↪ F) {degree s : ℕ} (u u' : code φ degree)
  • lemma single_coord_bound (φ : ι ↪ F) {degree : ℕ} (u u' : code φ degree)

sorry Tracking

✅ Removed: 1 `sorry`(s)

ArkLib/ProofSystem/Stir/OutOfDomSmpl.lean (1)

  • lemma out_of_dom_smpl_1 (L59)
📋 **Additional Analysis**

Style violations found (format/convention). One code correctness concern flagged (potential negative subtraction with ENNReal). No drift from roadmap or registry is detectable from the diff alone.

📄 **Per-File Summaries**
  • ArkLib/Data/Probability/Instances.lean: Added three new theorems to ArkLib/Data/Probability/Instances.lean:
  • Pr_exists_le_sum: a finite union bound stating that for any finite type β, Pr_{r ← D}[∃ b, P b r] ≤ ∑_b Pr_{r ← D}[P b r].
  • Pr_and_indep: an independence factorization stating that for independent distributions D₁ and D₂, Pr_{x←D₁; y←D₂}[A x ∧ B y] = Pr_{x←D₁}[A x] * Pr_{y←D₂}[B y].
  • Pr_forall_eq_pow: for a uniform distribution over Fin s → C where C is a nonempty fintype, Pr_{r}[∀ i, Q (r i)] = (Pr_{x←C}[Q x])^s.
  • ArkLib/ProofSystem/Stir/OutOfDomSmpl.lean: Added three lemmas: agree_symm (symmetry of codeword agreement on sampled points), single_coord_bound (probability that two distinct codewords agree on a random out‑of‑domain point ≤ (degree-1)/(|F|-|ι|)), and pair_agree_bound (probability they agree on all s independent samples ≤ ((degree-1)/(|F|-|ι|))^s). The previously sorry-filled proof of out_of_dom_smpl_1 (Lemma 4.5.1) is now completed, using the new lemmas, a union bound over unordered pairs of codewords, and combinatorial counting of two‑element subsets of the δ‑ball.

Last updated: 2026-07-11 04:41 UTC.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@aryaethn