Design: the BCS transform as a change of oracle implementation (QueryImpl), with a staged opening plan

[Abraxas1010]

Per CONTRIBUTING's blueprint-first process: a concrete design for filling the BCSTransform stub in ArkLib/OracleReduction/BCS/Basic.lean, for maintainer feedback before implementation PRs. We intend to build this in full and have validated the load-bearing elaboration against current main.

The observation the design rests on

OracleVerifier.verify already runs in OracleComp (oSpec + ([OStmtIn]ₒ + [pSpec.Message]ₒ)), and the honest adapter toVerifier (Basic.lean) is simulateQ (simOracle2 oSpec oStmt transcript.messages) (verify ...) — the verifier's access to the prover's oracle messages is already mediated by a QueryImpl. So the BCS compilation is not protocol surgery; it is a change of oracle implementation:

the compiled verifier is toVerifier with the message-side simOracle0 (answer-from-data) replaced by an opening-backed QueryImpl [pSpec.Message]ₒ (OracleComp oSpec) that runs the commitment scheme's opening procedure and refuses (OptionT failure) on rejection.

(The in-source TODO under OracleVerifier gestures at exactly this.) We have elaborated the skeleton — openingOracle, simOracleBCS (= simOracle2 with the message component opening-backed and the [OStmtIn]ₒ side pure-lifted), and toVerifierViaOpenings — against current main; it type-checks cleanly, including simulateQ through the OptionT verify computation.

Staged plan (one reviewable PR each)

1. Transform, type level + constructions: pSpec.bcsCompile via the existing renameMessage; committing prover threading (data, decommitment) state; toVerifierViaOpenings. Stage-1 restriction: direct (0-round or single-message) openings — Proof over !p[] / the NonInteractive shape — which is what Merkle vector openings are. Interactive openings are stage 2, composed via the existing append_completeness/soundness and seqCompose_* lemmas.
2. Completeness: with perfectly correct schemes, the compiled reduction inherits the IOR's completeness. Proof spine: a pointwise simulateQ-congruence between the opening-backed and data-backed implementations, anchored by one named lemma (openingImpl_answer_eq: openings on honest commitments answer exactly (Oₘ i).answer data q). We may first land the deterministic transcript-level equality and lift it, naming each honestly.
3. Binding bridge: binding_implies_committed_transcript_sound — two accepting opening responses for the same commitment+query that differ construct a BindingAdversary win. Full ROM/state-restoration soundness inheritance is deliberately out of scope and will be fenced as a named open statement referencing Security/StateRestoration.lean — we would rather ship a proven core with an honest fence than a hollow endgame.
4. Instantiation: Merkle vector commitments from the inductive Merkle tree development (feat(MerkleTree): add batch openings with completeness and uniqueness for inductive Merkle trees VCVio#473 batch openings + 🦅🦅🦅 The changes from #424 are so back 🦅🦅🦅 #474 tweaked paths), recovering the classic BCS'16 shape for vector-query IOPs.
5. If useful along the way: the fallback completeness route through the existing NonAdaptive oracle-verifier class, and small reusable simulateQ congruence lemmas upstreamed to VCV-io.

Questions for maintainers

1. Is the change-of-oracle-implementation framing acceptable as the definition of the transform, with the appended-opening-rounds presentation derived for the interactive-opening stage — or do you want the appended-rounds shape as primary?
2. Placement: extend BCS/Basic.lean in place (replacing the commented stub) vs. new sibling files per stage?
3. Any objection to the stage-1 direct-opening restriction being visible in the definition's hypotheses (an IsDirectOpening class on the scheme's opening ProtocolSpec)?
4. numQueries is currently sorry — we plan not to depend on it; flag if that's wrong.

We'll iterate here before opening PR 1.

The Institute for Ontological Mathematics (IAOM) / Equation Capital dba Apoth3osis.

[Abraxas1010]

One design point found in self-review, so it's on the table from the start: toVerifier also projects the output oracle statements through embed/hEq. After compilation, an OStmtOut index embedding into a prover message must surface as a commitment in the compiled output statement. For stage 1 we propose restricting to verifiers whose embed lands in Sum.inl (output oracles drawn from input oracles only), deferring message-derived output oracles to stage 2 together with interactive openings — this keeps the stage-1 compiled statement type simple. Flag if you'd rather have the commitment-typed output projection from day one.

[Abraxas1010]

Status + one coordination question while we build toward the plan above.

Built (in scratch, against main 5a83bfb): the full stage-1 commit-then-reveal transform — the committing prover (state transformer over the indexed PrvState family, retaining (message, decommitment, commitment) triples and challenges), the collect verifier, the single-message reveal round (on the SendWitness idiom), and the check-then-replay verifier (constructive totalization of the Option-maps, decidable opening checks, original-transcript rebuild, original-verifier replay) — composed through Reduction.append over bcsCompile ++ₚ revealSpec. Elaborates cleanly, no sorry. One design note for the record: this is the transcript-rebuild formulation, equivalent to the QueryImpl formulation for reveal-all; the QueryImpl route becomes necessary at stage-2 selective opening.

Completeness route + the question: our completeness plan is phase-wise + append_completeness, with each phase discharged by the support-level argument (perfectCompleteness_eq_prob_one → probEvent_eq_one_iff → the two-leg pattern your proven Reduction.id_perfectCompleteness uses). Working through it, we noticed SendWitness.reduction_completeness (and Verifier.id_soundness) are currently sorry on main — and our phase-2 completeness is exactly SendWitness-shaped, so we intend to prove the SendWitness case first and would happily land it as its own small PR (it should be a reusable template for other component completeness proofs). Is anyone already on those internally? If so we'll consume rather than duplicate; if not, we'll bring the proof here.

The Institute for Ontological Mathematics (IAOM) / Equation Capital dba Apoth3osis.

[Abraxas1010]

Progress update on the BCS staging (all in our staging clone, PR-able in whatever order maintainers prefer):

1. SendWitness completeness — filled and PR'd as feat(SendWitness): prove reduction completeness; add Prover.runToRound_succ #631 (plus Prover.runToRound_succ as the general round-unfolding brick).
2. Reveal-round (phase 2) perfect completeness — proven for the commit-then-reveal design above: honest reveal relation (totalized maps + verified openings + replay agreement) → output relation, for any init/impl.
3. End-to-end commit-and-open completeness — the BCS compilation of SendWitness as a concrete 2-round protocol (commitment message, reveal message), proven perfectly complete with an effectful commit : OracleComp oSpec (C × D) and a single hypothesis: every commitment in commit's support verifies against its own opening. Axioms: [propext, Classical.choice, Quot.sound].

One observation that may be useful for the open TODO in Composition/Sequential/Append.lean ("when do these theorems hold?"): the obstruction with StateT implementations is that R₂'s completeness premise quantifies from init, while in the appended run R₂ starts from whatever state R₁ left. For perfect completeness the fix seems to be requiring R₂'s completeness uniformly in the initial state (∀ init', not a fixed init) — which component completeness proofs (SendWitness, our phase 2/3 above) already satisfy, since they're proven for arbitrary init/impl. Happy to attempt append_perfectCompleteness under that side condition if useful.

— The Institute for Ontological Mathematics (IAOM) / Equation Capital dba Apoth3osis

[Abraxas1010]

Follow-through on the append-completeness offer above — the composition theorem is now proven in our staging (zero sorries, axioms [propext, Classical.choice, Quot.sound]):

theorem append_perfectCompleteness_of_proverFactorization
    (hf₁ : ∀ stmt td, R₁.verifier.verify stmt td = pure (f₁ stmt td))
    (hf₂ : ∀ stmt td, R₂.verifier.verify stmt td = pure (f₂ stmt td))
    (hfact : /- prover-level simulated factorization: the distributional shadow of Prover.append_run -/)
    (h₁ : R₁.perfectCompleteness init impl rel₁ rel₂)
    (h₂ : ∀ init' : ProbComp σ, R₂.perfectCompleteness init' impl rel₂ rel₃) :
    (R₁.append R₂).perfectCompleteness init impl rel₁ rel₃

Three findings worth recording for the Append.lean TODO ("when do these theorems hold?"):

1. The side condition is init-uniformity of R₂ (h₂ over all initial states) — the appended run hands R₂ the state R₁'s prover left, so a fixed-init premise cannot apply. Component completeness proofs (SendWitness/feat(SendWitness): prove reduction completeness; add Prover.runToRound_succ #631 included) already satisfy this, since they hold for arbitrary init/impl.
2. A run-level factorization through R₂.run is false pointwise: the appended verifier chains V₁'s output statement while the appended prover chains P₁'s output statement — these agree only on honest supports (via completeness's prvStmtOut = stmtOut). The unconditional factorization is prover-level (Prover.append_run), and that is the only remaining obligation the theorem hypothesizes.
3. En route we proved a small reusable lemma, Reduction.run_pure_verifier: for any reduction with a pure verifier f, (R.run stmt wit).run = liftM (R.prover.run stmt wit) >>= fun r => pure (some ((r.1, r.2), f stmt r.1)) — the run characterization your support_run_pure_verifier premise pattern suggests.

Happy to PR any packaging of this you'd prefer (new theorem alongside the existing sorried append_completeness, or replacing it under the documented side conditions), building on #633's SubSpec instances.

— The Institute for Ontological Mathematics (IAOM) / Equation Capital dba Apoth3osis

[Abraxas1010]

Milestone for this thread: the composition is now fully proven in our staging for the 1-message ++ 1-message case (the commit-then-reveal shape) — zero sorries, axioms [propext, Classical.choice, Quot.sound]:

theorem append_perfectCompleteness_oneMsg
    (hf₁ : R₁'s verifier pure) (hf₂ : R₂'s verifier pure)
    (h₁ : R₁.perfectCompleteness init impl rel₁ rel₂)
    (h₂ : ∀ init', R₂.perfectCompleteness init' impl rel₂ rel₃) :
    (R₁.append R₂).perfectCompleteness init impl rel₁ rel₃

Unconditional — the prover-level factorization from my previous comment is no longer a hypothesis: we proved it (hfact) through Prover.append's definition, via per-field equation lemmas at the embedded indices (the Eq.mpr casts from the tactic-mode field definitions fall to an eq_mpr_eq_cast/cast_heq/congr recipe), a run characterization of the appended prover in component operations, and simulated-level bridge lemmas showing the direct challenge-sum lifts wash out under any QueryImpl.

Two practical notes for whoever tackles the general Prover.append_run:

1. The lift-instance routes matter: a restated liftM can elect a two-hop path through a component's challenge-sum (opened by the feat(Append): construct the challenge-oracle SubSpec embeddings #633 SubSpec instances) that is semantically but not definitionally equal to processRound's direct lift — pin the chain explicitly.
2. On current toolchains the simulateQ_bind/StateT.run_bind rewrites refuse to fire on these goals via rw/simp — erw (or term-level congrArg+Eq.trans) is required.

Combined with #631 (SendWitness) and the reveal-round completeness from earlier in this thread, the stage-1 BCS completeness now assembles end-to-end. Happy to PR in whatever increments suit — the natural units are: the composition theorem + Reduction.run_pure_verifier; the append field-equation lemmas + run characterization; hfact + the 1+1 instance.

— The Institute for Ontological Mathematics (IAOM) / Equation Capital dba Apoth3osis