feat(OracleReduction): prove challenge-oracle append inclusions, drop admitted duplicate by alexanderlhicks · Pull Request #682 · Verified-zkEVM/ArkLib

alexanderlhicks · 2026-08-05T00:10:41Z

A validation pass over the OracleReduction execution/composition layer, closing three
admitted declarations: 63 → 60 declaration uses 'sorry' in ArkLib/OracleReduction/.

Independent of the companion PR rebasing #491; the two touch disjoint regions of
Execution.lean and can land in either order. (Landing both takes the count to 58.)

1. `Execution.lean`: delete `fst_map_simulateQ_loggingOracle_run`

It was admitted via stop, with a comment blaming a pending loggingOracle/WriterT
refactor. But it states exactly VCVio's loggingOracle.fst_map_run_simulateQ —
Prod.fst <$> (simulateQ spec.loggingOracle oa).run = oa, same universes — which is
@[simp] and axiom-clean upstream. It also had zero consumers.

So this needed deleting rather than proving: reuse the upstream lemma instead of carrying a
local admitted fork.

This clears one of the two admitted declarations in Execution.lean. The other,
Reduction.runWithLog_discard_logs_eq_run, is closed by the companion #491 rebase — after
which the file is sorry-free. On this branch alone it is still admitted.

2. `ProtocolSpec/SeqCompose.lean`: prove the challenge-oracle append inclusions

Append.lean carried two sorried anonymous instances:

instance : [(pSpec₁).Challenge]ₒ ⊂ₒ [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ := sorry
instance : [(pSpec₂).Challenge]ₒ ⊂ₒ [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ := sorry

These were load-bearing in a way that is easy to miss. Prover.append_run's own statement
lifts along them, so the statement quantified over junk lifts rather than real ones; and
because they are anonymous instances, typeclass resolution picked them up silently
anywhere in scope.

Now proved, all axiom-clean:

challenge_append_inl / challenge_append_inr — the challenge-type transport facts
across ++ₚ, via the same Fin.append_left / Fin.append_right route that
FullTranscript.fst / .snd already use.
subSpec_challenge_append_left / ..._right — built on the shape of VCVio's
subSpec_add_left, with onResponse transporting along the above.

Placed in SeqCompose.lean beside ChallengeIdx.inl/inr, replacing ~40 lines of
commented-out attempts that these supersede. Those attempts stalled trying to push simpa
through Range/Challenge; the route that works is that Range t is defeq to
Challenge t.1, so forcing the syntactic form with show ... from and transporting with ▸
goes through. (That defeq is verified independently, not assumed.)

Also validated — no change needed

Verifier.StateRestoration.knowledgeSoundness was flagged in #569 as carrying the same
vacuity trap that PR fixed (an always-failing extractor discharging knowledge soundness at
error 0). It has since been repaired: the extractor's OptionT is run explicitly and the
event is ∀ extractedWitIn ∈ extractedWitIn?, .... Security/Basic.lean has no
code-level sorry.

Verification

lake build green — 4135 jobs, 0 errors
#print axioms → [propext, Classical.choice, Quot.sound] for all four new declarations
inferInstance confirms resolution now selects the proved instances
no new lint warnings in the touched files

Not in scope

Append.lean retains 14 admitted tokens, including append_soundness,
append_knowledgeSoundness, and OracleVerifier.append — the last of which has sorry
inside its definition body, which is why OracleVerifier.append_coordinateWiseSpecialSound
inherits sorryAx in #530. Those are materially harder than this plumbing and deserve their
own scoping.

🤖 Generated with Claude Code

… admitted duplicate Validation pass over the `OracleReduction` execution/composition layer, closing three admitted declarations: 63 -> 60 `declaration uses 'sorry'` in `ArkLib/OracleReduction/`. Independent of the companion PR that rebases #491; the two touch disjoint regions of `Execution.lean` and can land in either order. 1. `Execution.lean`: delete `fst_map_simulateQ_loggingOracle_run`. It was admitted (via `stop`, with a comment blaming a pending `loggingOracle`/`WriterT` refactor) and states *exactly* VCVio's `loggingOracle.fst_map_run_simulateQ` -- `Prod.fst <$> (simulateQ spec.loggingOracle oa).run = oa`, same universes -- which is `@[simp]` and axiom-clean upstream. It had zero consumers. So it wanted deleting rather than proving: reuse the upstream lemma instead of carrying a local admitted fork. This clears one of the two admitted declarations in `Execution.lean`; the other, `Reduction.runWithLog_discard_logs_eq_run`, is closed by the companion #491 rebase, after which the file is sorry-free. 2. `ProtocolSpec/SeqCompose.lean`: prove the challenge-oracle append inclusions. `Append.lean` carried two *sorried anonymous instances* `[pSpecᵢ.Challenge]ₒ ⊂ₒ [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ`. These were load-bearing in a way that is easy to miss: `Prover.append_run`'s own statement lifts along them, so the statement quantified over junk lifts, and being anonymous instances they were picked up silently by typeclass resolution anywhere in scope. Now proved, axiom-clean: - `challenge_append_inl` / `challenge_append_inr`: the challenge-type transport facts across `++ₚ`, via the same `Fin.append_left` / `Fin.append_right` route that `FullTranscript.fst` / `.snd` already use. - `subSpec_challenge_append_left` / `..._right`: built on the shape of VCVio's `subSpec_add_left`, with `onResponse` transporting along the above. Placed in `SeqCompose.lean` next to `ChallengeIdx.inl`/`inr`, replacing ~40 lines of commented-out attempts that this supersedes. Those attempts stalled trying to push `simpa` through `Range`/`Challenge`; the working route is that `Range t` is *defeq* to `Challenge t.1`, so forcing the syntactic form with `show ... from` and transporting with `▸` goes through. Also validated, no change needed: `StateRestoration.knowledgeSoundness` (flagged in #569 as carrying the same vacuity trap) has since been repaired -- it runs the extractor's `OptionT` explicitly with the `∀ extractedWitIn ∈ extractedWitIn?` event shape. Verified on this branch standalone: `lake build` green (4135 jobs, 0 errors); `#print axioms` reports [propext, Classical.choice, Quot.sound] for all four new declarations; `inferInstance` confirms resolution selects the proved instances; no new lint warnings. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

github-actions · 2026-08-05T00:13:05Z

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: feat(OracleReduction): prove challenge-oracle append inclusions, drop admitted duplicate

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

This PR completes a validation pass over the OracleReduction execution/composition layer, closing three of 63 admitted sorry declarations in ArkLib/OracleReduction/ down to 60. The work is split across two fronts: deleting an obsolete admitted lemma that duplicates an upstream axiom-clean result, and proving the previously-sorried challenge-oracle append inclusions that underpin sequential composition. While one admitted declaration remains in Execution.lean on this branch (resolved by a companion PR), the core append-inclusion proofs are all axiom-clean and the proofs have architectural weight beyond mere placeholder-filling: they establish canonical, lawfully-distributing embeddings of component challenge oracles into the appended challenge interface. These are now the load-bearing facts for composing oracle queries across sequential protocols, replacing dead code and silent typeclass-junk lifts. The PR also introduces a reusable ChallengeReindex construction that generalizes the transport mechanism for future composition operators.

Mathematical Formalization

Proved challenge-oracle append inclusions (ArkLib/OracleReduction/ProtocolSpec/SeqCompose.lean): The two sorried anonymous instances embedding each component's challenge oracle into [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ are now formalized as explicit theorems and proofs:
- challenge_append_inl / challenge_append_inr establish the challenge‑type transport across ++ₚ via append_Type_castAdd/append_Type_natAdd, following the Fin.append_left/Fin.append_right route already used by FullTranscript.fst/.snd.
- Six new instances provide subSpec with lawfulSubSpec for left/right inclusions and OracleSpec.DisjointSubSpec in both orderings. These ensure the embeddings preserve distribution and support, making them suitable for the security proofs below.
- The key technical insight is that Range t is definitionally equal to Challenge t.1; forcing the syntactic form with show ... from and transporting with ▸ goes through where earlier simpa-based attempts stalled (those attempts are now superseded by the proved lemmas).
New canonical ChallengeReindex API (ArkLib/OracleReduction/ProtocolSpec/Basic.lean): Introduced a reusable section defining challengeReindexQuery, challengeReindexResponse, and subSpecOfChallengeReindex — a SubSpec inclusion that lifts a [p.Challenge]ₒ oracle into [q.Challenge]ₒ given an index map f and type-transport proof hf. The theorems challengeReindexResponse_bijective and lawfulSubSpecOfChallengeReindex guarantee the reindexed oracle remains uniform, giving a canonical construction to avoid case-by-case repetition in future composition operators.

Proof Completion (sorries removed)

Removed one of three target sorrys: The private lemma fst_map_simulateQ_loggingOracle_run in Execution.lean is deleted. It stated exactly VCVio's axiom-clean loggingOracle.fst_map_run_simulateQ (with zero consumers), so the project reuses the upstream @[simp] lemma rather than carrying a local admitted fork. This clears the file's load-bearing block caused by the abandoned proof.
Proved the two append inclusions: The anonymous sorried instances in Append.lean are removed and replaced by the proved instances above. These were load-bearing beyond their own statements — Prover.append_run's statement quantifies over them, and anonymous instances were silently picked up by typeclass resolution.
Remaining sorry on this branch: Reduction.runWithLog_discard_logs_eq_run in Execution.lean is still admitted on this branch alone (closed by a companion PR); the file is fully sorry-free only after that rebase.

Protocols / Soundness

No code-level sorry in Security/Basic.lean: The Verifier.StateRestoration.knowledgeSoundness concern flagged in fix(oracle-reduction): close vacuity in straightline knowledge soundness #569 has already been addressed via explicit OptionT execution and the ∀ extractedWitIn ∈ extractedWitIn?, ... quantification; no further change here.
Refined coercion steps in CoordinateWiseSpecialSoundness/SeqCompose.lean: The theorems append_nodeOk_inl and append_nodeOk_inr now use the dedicated ProtocolSpec.challenge_append_inl/challenge_append_inr lemmas in their cast expressions, replacing inline simp blocks. This makes the type-coercion step match the challenge type from the appended tree to the component protocol's type explicit and robust.
Append.lean retains admitted content: 14 admitted tokens remain, including append_soundness, append_knowledgeSoundness, and OracleVerifier.append — the last has sorry inside its definition body, which propagates sorryAx into OracleVerifier.append_coordinateWiseSpecialSound. These are scoped out as materially harder than this plumbing.

Infrastructure / CI

Merging strategy: The PR is independent of companion feat(OracleReduction): prove identity verifier soundness and knowledge soundness #491 (which rebases Execution.lean); the two touch disjoint regions and can land in any order. Landing both brings total sorry count to 58.
Verification: lake build green (4135 jobs, 0 errors); #print axioms confirms [propext, Classical.choice, Quot.sound] for all four new declarations; inferInstance confirms resolution selects the proved instances; no new lint warnings in touched files.

Statistics

Metric	Count
📝 Files Changed	5
✅ Lines Added	130
❌ Lines Removed	61

Lean Declarations

✏️ Removed: 1 declaration(s)

ArkLib/OracleReduction/Execution.lean (1)

private lemma fst_map_simulateQ_loggingOracle_run {ι : Type} {spec : OracleSpec ι} {α : Type}

✏️ Added: 13 declaration(s)

ArkLib/OracleReduction/ProtocolSpec/Basic.lean (5)

@[reducible] def challengeReindexQuery (t : [p.Challenge]ₒ.Domain) : [q.Challenge]ₒ.Domain
@[reducible] def challengeReindexResponse (t : [p.Challenge]ₒ.Domain)
@[reducible] def subSpecOfChallengeReindex : [p.Challenge]ₒ ⊂ₒ [q.Challenge]ₒ where
theorem challengeReindexResponse_bijective (t : [p.Challenge]ₒ.Domain) :
theorem lawfulSubSpecOfChallengeReindex :

ArkLib/OracleReduction/ProtocolSpec/SeqCompose.lean (8)

instance disjointSubSpec_challenge_append_left_right :
instance disjointSubSpec_challenge_append_right_left :
instance lawfulSubSpec_challenge_append_left :
instance lawfulSubSpec_challenge_append_right :
instance subSpec_challenge_append_left :
instance subSpec_challenge_append_right :
theorem challenge_append_inl (i : ChallengeIdx pSpec₁) :
theorem challenge_append_inr (i : ChallengeIdx pSpec₂) :

sorry Tracking

✅ Removed: 2 `sorry`(s)

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

def StateFunction.append (L334)
def StateFunction.append (L335)

📋 **Additional Analysis**

The diff introduces several naming and documentation violations against the project's style guide. The most significant issues are inconsistent naming of instances (mixing camelCase and snake_case) and missing docstrings on key definitions.

📄 **Per-File Summaries**

ArkLib/OracleReduction/Composition/Sequential/Append.lean: Removed two sorry-filled instance declarations [(pSpec₁).Challenge]ₒ ⊂ₒ [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ and [(pSpec₂).Challenge]ₒ ⊂ₒ [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ that were previously left incomplete. Replaced them with a comment explaining that the needed challenge-oracle inclusions are now proved by ProtocolSpec.subSpec_challenge_append_left / ..._right in ProtocolSpec/SeqCompose.lean, together with their LawfulSubSpec instances, which make the lifts distribution- and support-preserving for the security proofs below.
ArkLib/OracleReduction/Execution.lean: Removed the private lemma fst_map_simulateQ_loggingOracle_run, which attempted to prove that applying WriterT.run with the logging oracle and then discarding the log equals the original computation. The lemma was incomplete (it ended with stop and contained a show block citing a broken refactor). Its deletion cleans up dead code and resolves a compilation block caused by the abandoned proof.
ArkLib/OracleReduction/ProtocolSpec/Basic.lean: The diff adds a ChallengeReindex section defining challengeReindexQuery, challengeReindexResponse, subSpecOfChallengeReindex (a SubSpec inclusion between challenge oracles), and theorems challengeReindexResponse_bijective and lawfulSubSpecOfChallengeReindex. These provide a canonical, reusable construction—given an index map f and type‑transport proof hf—that lifts a [p.Challenge]ₒ oracle into [q.Challenge]ₒ while preserving the uniform distribution on challenges, avoiding case‑by‑case repetition in composition operators.
ArkLib/OracleReduction/ProtocolSpec/SeqCompose.lean: In the Append section of SeqCompose.lean, two previously commented-out blocks (a set of @[simp] lemmas and SubSpec instances for the challenge oracle of pSpec₁ ++ₚ pSpec₂) were replaced by formalized equivalents: the theorems challenge_append_inl and challenge_append_inr use append_Type_castAdd/append_Type_natAdd to equate the challenge type at a left‑/right‑injected index with that of the component; six new instances provide subSpec (embedding) with lawfulSubSpec for left and right inclusions and OracleSpec.DisjointSubSpec in both orderings. These establish that the two component challenge oracles embed lawfully and disjointly into the appended challenge interface, which is required for composing oracle queries in the sequential composition protocol.
ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/SeqCompose.lean: The diff adjusts two theorems append_nodeOk_inl and append_nodeOk_inr in SeqCompose.lean. In each theorem the expression used inside the cast for the challenge function argument is changed from a simp block referencing ProtocolSpec.append and ChallengeIdx.inl/inr to a direct call to the dedicated lemma ProtocolSpec.challenge_append_inl i₁ or ProtocolSpec.challenge_append_inr i₂, respectively. This refines the type-coercion step that matches the challenges from the appended challenge tree to the original sub‑protocol’s challenge type, replacing an inline simp proof with the explicit lemma. No other changes occur in the file; the two theorems remain otherwise identical in their statements and in the rest of their proof bodies.

Last updated: 2026-08-05 03:51 UTC.

github-actions · 2026-08-05T00:22:37Z

Build Timing Report

Commit: 11cbb52
Message: feat(OracleReduction): prove challenge-oracle append inclusions, drop admitted duplicate
Ref: feat/append-challenge-subspec
Comparison baseline: 4397764 from the previous successful PR update.
Measured on ubuntu-latest with /usr/bin/time -p.
Commands: clean build rm -rf .lake/build && lake build; warm rebuild lake build; validation wrapper ./scripts/validate.sh.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	570.83	770.76	+199.93	ok
Warm rebuild	2.27	2.29	+0.02	ok
Validation wrapper	2.10	2.49	+0.39	ok

Incremental Rebuild Signal

Warm rebuild saved 768.47s vs clean (336.58x faster).

This compares a clean project build against an incremental rebuild in the same CI job; it is a lightweight variability signal, not a full cross-run benchmark.

Slowest Current Clean-Build Files

Showing 20 slowest current targets, with comparison against the selected baseline when available.

Current (s)	Baseline (s)	Delta (s)	Path
69.00	43.00	+26.00	`ArkLib/Data/CodingTheory/ProximityGap/DG25/MainResults.lean`
69.00	48.00	+21.00	`ArkLib/ProofSystem/Stir/Combine.lean`
63.00	41.00	+22.00	`ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean`
59.00	45.00	+14.00	`ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineSpaces.lean`
53.00	33.00	+20.00	`ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/BWMatrix.lean`
52.00	39.00	+13.00	`ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean`
43.00	36.00	+7.00	`ArkLib/OracleReduction/LiftContext/Reduction.lean`
42.00	31.00	+11.00	`ArkLib/Data/CodingTheory/BerlekampWelch/Condition.lean`
41.00	37.00	+4.00	`ArkLib/Data/CodingTheory/ProximityGap/AHIV22.lean`
40.00	31.00	+9.00	`ArkLib/Data/CodingTheory/ProximityGap/Folding.lean`
35.00	26.00	+9.00	`ArkLib/ProofSystem/Binius/BinaryBasefold/Prelude.lean`
34.00	22.00	+12.00	`ArkLib/Commitments/Functional/KZG/Binding.lean`
33.00	21.00	+12.00	`ArkLib/OracleReduction/Security/RoundByRound.lean`
33.00	19.00	+14.00	`ArkLib/Commitments/Functional/KZG/FunctionBinding/EvaluationBindingConflict.lean`
33.00	23.00	+10.00	`ArkLib/Data/CodingTheory/JohnsonBound/Basic.lean`
33.00	15.00	+18.00	`ArkLib/ProofSystem/Sumcheck/Domain.lean`
28.00	19.00	+9.00	`ArkLib/Data/CodingTheory/DivergenceOfSets.lean`
28.00	15.00	+13.00	`ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/JointAgreement.lean`
26.00	17.00	+9.00	`ArkLib/ToCompPoly/Univariate/Basic.lean`
25.00	19.00	+6.00	`ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean`

…awful + disjoint append inclusions Addresses review findings on the challenge-oracle append inclusions. 1. Right abstraction instead of two bespoke copies. The two inclusions were built from four hand-written helper defs (`challengeInl/InrOn Query/Response`) that differed only in which index map and transport lemma they used. Replace them with one construction in `ProtocolSpec/Basic.lean`, beside `challengeOracleInterface`: an index map `f : p.ChallengeIdx → q.ChallengeIdx` plus a transport `∀ i, q.Challenge (f i) = p.Challenge i` induces `subSpecOfChallengeReindex`. That data determines the lift uniquely (the transport is an equality of types), which is what makes the induced inclusion canonical rather than merely well-typed. `seqCompose` is the intended second client; it is not instantiated here since nothing consumes it yet. 2. `LawfulSubSpec` (the substantive gap). `SubSpec` is pure data: on its own it does not force the lift to preserve the uniform distribution on challenges. `LawfulSubSpec` -- `onResponse` bijective on every fibre, i.e. a cartesian lens -- is what VCV-io requires for `evalDist_liftComp`, `probEvent_liftComp`, `probOutput_liftComp` and `support_liftComp`, and for `lawfulSubSpec_right_add_right_add` to carry lawfulness through the `oSpec + .` layer that `Prover.append_run` actually lifts across. Neither inclusion had it, so `append_run` could not have fed the security proofs even once proved. Now provided generically (`lawfulSubSpecOfChallengeReindex`, from `challengeReindexResponse_bijective`) and instantiated on both sides; verified that `(oSpec + [pSpecᵢ.Challenge]ₒ) ˡ⊂ₒ (oSpec + [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ)` now synthesises. 3. `DisjointSubSpec`, both orientations, matching VCV-io's `disjointSubSpec_add_left_right` / `..._right_left`: a left-injected round index is `< m` and a right-injected one is `≥ m`, so the two components' challenge queries cannot alias. 4. Deduplication. `challenge_append_inl` / `_inr` re-derived by `simp` what `append_Type_castAdd` / `append_Type_natAdd` already state 320 lines up in the same file; they are now those lemmas at the underlying round index. Conversely `CoordinateWiseSpecialSoundness/SeqCompose.lean` was re-deriving the same transport inline as `cast (by simp [...])`; it now cites `challenge_append_inl` / `_inr`, removing a fourth copy and giving the lemmas real consumers. Also: dropped the `SampleableType` `variable` line left dangling with no declarations after it, and documented the `pSpec ++ₚ pSpec` instance-overlap (resolution picks `..._right`, as upstream does for `spec + spec`). Verified: `lake build` green (4135 jobs, 0 errors); `#print axioms` reports [propext, Classical.choice, Quot.sound] for all 11 new/changed declarations; `Prover.append_run` still resolves through `subSpec_challenge_append_left` / `_right` under `pp.explicit`; no style-lint error and no build-linter warning inside the changed ranges. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Navigation Menu

Uh oh!

feat(OracleReduction): prove challenge-oracle append inclusions, drop admitted duplicate - #682

feat(OracleReduction): prove challenge-oracle append inclusions, drop admitted duplicate#682
alexanderlhicks wants to merge 2 commits into
mainfrom
feat/append-challenge-subspec

alexanderlhicks commented Aug 5, 2026

Uh oh!

github-actions Bot commented Aug 5, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Aug 5, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

alexanderlhicks commented Aug 5, 2026

1. Execution.lean: delete fst_map_simulateQ_loggingOracle_run

2. ProtocolSpec/SeqCompose.lean: prove the challenge-oracle append inclusions

Also validated — no change needed

Verification

Not in scope

Uh oh!

github-actions Bot commented Aug 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 PR Summary

Mathematical Formalization

Proof Completion (sorries removed)

Protocols / Soundness

Infrastructure / CI

Uh oh!

github-actions Bot commented Aug 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Build Timing Report

Incremental Rebuild Signal

Slowest Current Clean-Build Files

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

1. `Execution.lean`: delete `fst_map_simulateQ_loggingOracle_run`

2. `ProtocolSpec/SeqCompose.lean`: prove the challenge-oracle append inclusions

github-actions Bot commented Aug 5, 2026 •

edited

Loading

github-actions Bot commented Aug 5, 2026 •

edited

Loading