feat(OracleReduction): prove identity verifier soundness and reduction log-discard - #681
feat(OracleReduction): prove identity verifier soundness and reduction log-discard#681alexanderlhicks wants to merge 3 commits into
Conversation
…n log-discard Rebase of #491 (by @XC0R) onto current main, keeping only the contributions that survive. The two proofs below are XC0R's work from that PR; this commit rebases them past the v4.29 -> v4.31 toolchain bump, drops one hunk that main has since superseded, and fixes a line-length lint. - `Verifier.id_soundness`: replaces a `sorry`. Three other declarations depend on it -- `OracleVerifier.id_soundness`, `Verifier.seqCompose_soundness` and `OracleVerifier.seqCompose_soundness` -- all reaching it via implicit `simp` firing, so this removes their dependence on this `sorry`. They remain `sorryAx`-tainted via the independent `append_soundness` gap. - `Reduction.runWithLog_discard_logs_eq_run`: replaces a `sorry`, plus the supporting private lemma `OptionT_liftM_bind_fst`. A whole-library scan (341601 constants, `Lean.collectAxioms` against a probe axiom substituted for the proof) finds no consumers anywhere in ArkLib. It is nonetheless worth proving: the lemma is `@[simp]`, so the admitted version sat in the default simp set ready to inject `sorryAx` into any future proof whose goal matched its LHS. Proving it disarms that, so the warning docstring is dropped. Dropped from #491: its proof of `Verifier.id_knowledgeSoundness`. That theorem was proved independently on main in #569, which also strengthened the `knowledgeSoundness` definition to close a vacuity (the always-failing extractor discharged it at error 0 for any verifier and any relations). #491's proof targets the pre-#569 event shape -- a bare `WitIn` where the definition now carries `Option WitIn` -- and no longer typechecks. Verified: `lake build` green (4135 jobs); `#print axioms` reports [propext, Classical.choice, Quot.sound] for both theorems and for `OracleVerifier.id_soundness`; no `sorryAx`. Co-authored-by: XC0R <8145037+XC0R@users.noreply.github.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
🤖 PR Summary
This PR completes two previously Mathematical Formalization
Proof Completion (sorries removed)
Infrastructure / CI
Remaining Issues
Scope NoteThe PR drops one hunk from its predecessor (#491), Statistics
Lean Declarations ✏️ Removed: 1 declaration(s)
✏️ Added: 2 declaration(s)
✅ Removed: 2 `sorry`(s)
📋 **Additional Analysis**The diff is generally well-structured and follows most of the ArkLib style guidelines. The new file 📄 **Per-File Summaries**
Last updated: 2026-08-05 14:42 UTC. |
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.
|
… and linter warnings
Addresses review findings on the identity-soundness / log-discard proofs. No statement changes;
both theorems remain axiom-clean.
1. Generalise the private helper and use core lemmas properly.
`OptionT_liftM_bind_fst` was hard-coded to `OptionT m` at `Type 0`, and proved by unfolding
`liftM` / `MonadLift.monadLift` / `OptionT.lift` / `OptionT.mk` through a goal-changing `show`
plus `congr 1` -- of whose six `simp` arguments five were unused. It is in fact the
`monadLift`-generic form of `bind_map_left`, so restate it for any
`[MonadLiftT m n] [LawfulMonadLiftT m n]` over arbitrary universes as `monadLift_bind_fst`,
proved by `rw [monadLift_map, bind_map_left]` (both Lean core). Shorter, strictly more general,
and it no longer depends on how `OptionT`'s lift happens to be implemented.
2. Dead code, in the region these changes own.
- Removed the ~20-line commented-out `calc` attempt below the now-proved theorem; the docstring
that referred to it ("a partial `calc` attempt is retained in comments") is already gone.
- Removed `private lemma Monad.map_of_prod_fst_eq_prod_fst`, which nothing references.
3. Linter warnings. The above removes all 8 that `lake build` reported inside the new code
(1 × `linter.style.show`, 7 × `linter.unusedSimpArgs`). The warnings remaining in
`Execution.lean` are pre-existing.
4. Comments. Replaced the "Remaining: ..." / "should equal" note in front of the closing `rfl`,
which read as unfinished work, with a statement of what the `rfl` discharges; and recorded why
the verifier-logging step needs an explicit induction rather than reusing VCV-io's
`loggingOracle.fst_map_run_simulateQ` or ArkLib's `loggingOracle.map_fst_run_simulateQ` (the
verifier's run sits under `liftM` inside `OptionT`, so its log is consumed by an `OptionT` bind
rather than a `Prod.fst` map -- six drop-in variants of those lemmas were tried and none
applies). Named the three anonymous shadowing `have`s at the end of `Verifier.id_soundness`.
Correction to the previous commit message: it says all three declarations that depend on
`Verifier.id_soundness` reach it by implicit `simp` firing and are invisible to a text search. Only
`OracleVerifier.id_soundness` does. `Verifier.seqCompose_soundness` names it outright
(`Composition/Sequential/General.lean`, `exact Verifier.id_soundness init impl`) and
`OracleVerifier.seqCompose_soundness` reaches it through that. The substantive claim is unaffected:
a library-wide `Lean.collectAxioms` sweep confirms exactly three declarations move from
`sorryAx`-tainted to clean -- `Verifier.id_soundness`, `OracleVerifier.id_soundness` (the one
silent dependent) and `Reduction.runWithLog_discard_logs_eq_run`.
Verified: `lake build` green (4135 jobs, 0 errors); `#print axioms` reports
[propext, Classical.choice, Quot.sound] for both theorems and for `OracleVerifier.id_soundness`;
no style-lint error and no build-linter warning inside the changed ranges.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… 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>
1 participant
Supersedes #491 by @XC0R, rebased onto current
main. The two proofs are XC0R'swork; this PR carries them past the v4.29 → v4.31 toolchain bump, drops one hunk
that
mainhas since superseded, and fixes a line-length lint.#491 could not be merged as-is: it was based on a three-month-old commit
(
37298e66), conflicted in both files, and one of its three contributions is nowinvalid rather than merely stale.
Kept
Verifier.id_soundness— replaces asorry. Three other declarations dependon it:
OracleVerifier.id_soundness,Verifier.seqCompose_soundnessandOracleVerifier.seqCompose_soundness. All three reach it through implicitsimpfiring, so none of them is visible to a text search — in particularOracleVerifier.id_soundnessis proved bysimp [OracleVerifier.soundness]andtherefore silently inherited
sorryAxonmaindespite looking proved.Reduction.runWithLog_discard_logs_eq_run— replaces asorry, plus thesupporting private lemma
OptionT_liftM_bind_fst.A whole-library scan (341,601 constants,
Lean.collectAxiomsrun against a probeaxiom substituted for the proof) finds no consumers anywhere in ArkLib. It is
still worth proving: the lemma carries
@[simp], so the admitted version sat inthe default simp set with a
sorrybehind it, ready to injectsorryAxinto anyfuture proof whose goal matched its LHS. That is the hazard the previous
docstring warned about; proving it disarms the lemma, so the warning is dropped.
The scan's positive control is
OracleVerifier.id_soundness, which reaches itsprobe only via implicit
simp— confirming the method detects exactly the kindof reach that a null result would otherwise be suspected of missing.
Dropped
Verifier.id_knowledgeSoundness. Proved independently onmainin #569,which also strengthened the
knowledgeSoundnessdefinition to close a vacuity:previously the always-failing extractor
fun _ _ _ _ _ => failuredischarged itat error
0for any verifier and any relations, becauseOptionTfailure massfalls outside
probEvent. #491's proof targets the pre-#569 event shape — a bareWitInwhere the definition now carriesOption WitIn— and no longertypechecks.
main's version is left untouched.Verification
lake buildgreen — 4135 jobs, 0 errors, on this exact commit#print axioms→[propext, Classical.choice, Quot.sound]for both theoremsand for
OracleVerifier.id_soundness; nosorryAxScope note
The two
seqComposetheorems remainsorryAx-tainted via the independentappend_soundnessgap inComposition/Sequential/Append.lean. This PR removestheir dependence on this
sorry; it does not make them axiom-clean.The only
sorryleft in either touched file is the pre-existing, unrelatedExecution.lean:123(fst_map_simulateQ_loggingOracle_run), which carries thesame
@[simp]-contamination shape one lemma upstream and is worth a follow-up.🤖 Generated with Claude Code