feat(OracleReduction): prove challenge-oracle append inclusions, drop admitted duplicate - #682
Open
alexanderlhicks wants to merge 3 commits into
Open
feat(OracleReduction): prove challenge-oracle append
inclusions, drop admitted duplicate#682alexanderlhicks wants to merge 3 commits into
alexanderlhicks wants to merge 3 commits into
Conversation
… 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>
Contributor
🤖 PR Summary
The PR eliminates two sorried instances and one dead lemma, reducing the total Statistics
Lean Declarations ✏️ Removed: 1 declaration(s)
✏️ Added: 19 declaration(s)
✅ Removed: 2 `sorry`(s)
📋 **Additional Analysis**No findings. 📄 **Per-File Summaries**
Last updated: 2026-08-05 14:28 UTC. |
Contributor
Build Timing Report
Incremental Rebuild Signal
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 FilesShowing 20 slowest current targets, with comparison against the selected baseline when available.
|
…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>
…ors; scope the lawfulness claim Acts on two fresh adversarial reviews, which agreed on the main gap and corrected two claims of mine. 1. Nothing pinned the transport; now something does. The previous commit's docstring said the response transport is "the *only* possible choice" and therefore canonical. That is false as stated, and a reviewer compiled the counterexample family: post-composing any fibrewise automorphism of `p.Challenge i` gives a different `onResponse` with the *same* `onQuery` that is equally `LawfulSubSpec` and equally `DisjointSubSpec`. So the three interfaces do not determine the lift, and with the only consumer (`Prover.append_run`) still `sorry`, nothing in-tree fixed the semantics. Added the `rfl`-level anchors that do, in the spirit of VCV-io's `liftM_add_left_query` / `liftM_add_right_query`: `liftM_challenge_append_inl` / `_inr` compute the lifted query, and `liftM_getChallenge_append_inl` / `_inr` the `getChallenge` shape that actually appears when a component prover's run is lifted. All four are `@[simp]` and would break if `ChallengeIdx.inl` / `inr`, `ProtocolSpec.append` or the transport lemmas were changed underneath. Docstring corrected to say what does and does not force the definition, and `challengeReindexResponse_eq_cast` records that the transport is exactly `cast`. 2. The lawfulness claim was overstated; scoped it. The comment in `Append.lean` said the `LawfulSubSpec` instances make the lifts "distribution- and support-preserving, hence usable by the security proofs below". Support: true, verified. Distribution: **not at this shape** -- `evalDist_liftComp` / `probEvent_liftComp` additionally require `IsUniformSpec` on both specs and `oSpec` is arbitrary; and the security definitions measure after `simulateQ pImpl`, so the missing ingredient is `simulateQ_liftM_eq_of_query` plus a `challengeQueryImpl`-compatibility fact across the transport, which is not proved. The comment now says exactly that, and names what is owed. 3. `DisjointSubSpec` is now built generically too (`disjointSubSpecOfChallengeReindex`, from index-level disjointness), so the section docstring's "whole package once here" is true rather than aspirational -- it was previously hand-rolled per case. The append instances are flagged as currently unconsumed. 4. Scoped the section docstring's generality claim: the construction is stated for the *default* `challengeOracleInterface`, whose `Query` is `Unit` at every index, which is what lets the query payload be reused across the reindexing. It cannot serve `challengeOracleInterfaceSR` / `..FS` (index-dependent query type); those are `def`s, not instances, so the interface is fixed at each declaration and cannot be silently swapped. One reviewer claim I checked and rejected: that at `pSpec₁ = pSpec₂` the bare `liftM`s in `Prover.append_run` would both resolve to the right-hand inclusion, making the statement wrong. Instances are resolved when the statement is elaborated, at distinct `pSpec₁` / `pSpec₂`; instantiating the elaborated statement at a single protocol still carries `..._left` for `P₁` and `..._right` for `P₂` (checked under `pp.explicit`). The documented `pSpec ++ₚ pSpec` hazard is real only for statements written directly at that shape, which is what the docstring says. Verified: `lake build` green (4135 jobs, 0 errors); `#print axioms` clean for all new declarations; all four `LawfulSubSpec` / `DisjointSubSpec` instances plus the `oSpec + ·` composites synthesise; `Prover.append_run` still resolves through `subSpec_challenge_append_left` / `_right`; no new build-linter warning or style-lint error in the changed ranges. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
alexanderlhicks
added a commit
that referenced
this pull request
Aug 5, 2026
… lift helper to ToMathlib
Acts on a fresh adversarial review that overturned a claim in the previous commit.
1. The previous commit asserted, in a code comment, that VCV-io's
`loggingOracle.fst_map_run_simulateQ` and ArkLib's `loggingOracle.map_fst_run_simulateQ` could
not be used for the verifier-logging step, and justified a hand-rolled `OracleComp.induction` on
that basis. **That was wrong.** Applying this file's own `monadLift_bind_fst` a second time --
to the verifier's lift, exactly as it is already applied to the prover's -- reduces the goal to
`loggingOracle.fst_map_run_simulateQ`'s left-hand side. The induction, its two bare `rfl`s and
the false comment are gone; the step is now
have hVerif := monadLift_bind_fst ...
exact hVerif ▸ by rw [loggingOracle.fst_map_run_simulateQ]; rfl
Net -14 lines, and the proof now uses the library instead of re-deriving it, per the repo's
reuse rule. My earlier search missed this because it only tried the logging lemmas *directly* at
the goal, never after a second application of the helper.
2. The helper moves to `ArkLib/ToMathlib/Control/MonadLift.lean` and stops being `private`. It
mentions nothing outside Lean core (it is a two-step composite of `monadLift_map` and
`bind_map_left`), so per the repo layout it belongs in `ToMathlib` as an upstreaming candidate
rather than buried in `OracleReduction/Execution.lean`. It is also generalised: the primitive is
now `monadLift_bind_map` for an arbitrary `h : α → α'` (same one-line proof), with
`monadLift_bind_fst` as the `Prod.fst` instance. Deliberately not `@[simp]` -- core's simp set
rewrites its RHS *into* its LHS, so it is anti-normal-form and must be used explicitly.
3. The docstring now records why the `▸`/`exact` spelling is forced rather than stylistic: after
`simp only` the goal is not type-correct at `instances` transparency (ArkLib's `Verifier.run` is
an `OptionT`, which `kabstract` sees as `OracleComp _ (Option _)`), so `rw` cannot operate on it
at all, for any spelling of the rewrite lemma.
Also removed a stray `#check Reduction.runWithLog` sitting in library code in `Security/Basic.lean`
(pre-existing, in a file this PR already edits).
Left alone deliberately: the zero-consumer, `stop`-admitted `fst_map_simulateQ_loggingOracle_run`
higher up in `Execution.lean`. Note `stop` expands to `repeat sorry`, so it is a `grep sorry`-
invisible admit. The companion PR #682 deletes it; removing it here too would collide.
Verified: `lake build` green (4135 jobs, 0 errors); `#print axioms` reports
[propext, Classical.choice, Quot.sound] for both theorems and for `OracleVerifier.id_soundness`;
`ArkLib.lean` regenerated via `scripts/update-lib.sh` (316 imports, `check-imports.sh` passes);
no new build-linter warning and no new style-lint error in the changed ranges.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
A validation pass over the
OracleReductionexecution/composition layer, closing threeadmitted declarations: 63 → 60
declaration uses 'sorry'inArkLib/OracleReduction/.Independent of the companion PR rebasing #491; the two touch disjoint regions of
Execution.leanand can land in either order. (Landing both takes the count to 58.)1.
Execution.lean: deletefst_map_simulateQ_loggingOracle_runIt was admitted via
stop, with a comment blaming a pendingloggingOracle/WriterTrefactor. 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 — afterwhich the file is sorry-free. On this branch alone it is still admitted.
2.
ProtocolSpec/SeqCompose.lean: prove the challenge-oracle append inclusionsAppend.leancarried two sorried anonymous instances:These were load-bearing in a way that is easy to miss.
Prover.append_run's own statementlifts along them, so the statement quantified over junk lifts rather than real ones; and
because they are anonymous
instances, typeclass resolution picked them up silentlyanywhere in scope.
Now proved, all axiom-clean:
challenge_append_inl/challenge_append_inr— the challenge-type transport factsacross
++ₚ, via the sameFin.append_left/Fin.append_rightroute thatFullTranscript.fst/.sndalready use.subSpec_challenge_append_left/..._right— built on the shape of VCVio'ssubSpec_add_left, withonResponsetransporting along the above.Placed in
SeqCompose.leanbesideChallengeIdx.inl/inr, replacing ~40 lines ofcommented-out attempts that these supersede. Those attempts stalled trying to push
simpathrough
Range/Challenge; the route that works is thatRange tis defeq toChallenge t.1, so forcing the syntactic form withshow ... fromand transporting with▸goes through. (That defeq is verified independently, not assumed.)
Also validated — no change needed
Verifier.StateRestoration.knowledgeSoundnesswas flagged in #569 as carrying the samevacuity trap that PR fixed (an always-failing extractor discharging knowledge soundness at
error
0). It has since been repaired: the extractor'sOptionTis run explicitly and theevent is
∀ extractedWitIn ∈ extractedWitIn?, ....Security/Basic.leanhas nocode-level
sorry.Verification
lake buildgreen — 4135 jobs, 0 errors#print axioms→[propext, Classical.choice, Quot.sound]for all four new declarationsinferInstanceconfirms resolution now selects the proved instancesNot in scope
Append.leanretains 14 admitted tokens, includingappend_soundness,append_knowledgeSoundness, andOracleVerifier.append— the last of which hassorryinside its definition body, which is why
OracleVerifier.append_coordinateWiseSpecialSoundinherits
sorryAxin #530. Those are materially harder than this plumbing and deserve theirown scoping.
🤖 Generated with Claude Code