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 2 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
Proof Completion (sorries removed)
Infrastructure / Refactoring
Dropped Proof The proof Remaining Sorries One pre‑existing Verification
The two Statistics
Lean Declarations ✏️ Removed: 1 declaration(s)
✏️ Added: 1 declaration(s)
✅ Removed: 2 `sorry`(s)
📋 **Additional Analysis**Style guide review of the PR diff reveals several violations of the ArkLib contribution guidelines, particularly in naming conventions and documentation standards. The PR resolves a previously admitted lemma and adds a new proof, but the new code does not fully adhere to the specified style. 📄 **Per-File Summaries**
Last updated: 2026-08-05 02:40 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>
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