refactor(OracleReduction): generic challenge-oracle reindexing; add lawful + 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>

Author: alexanderlhicks

ArkLib/OracleReduction/Composition/Sequential/Append.lean

@@ -331,8 +331,10 @@ variable {P₁ : Prover oSpec Stmt₁ Wit₁ Stmt₂ Wit₂ pSpec₁}
 
 -- theorem append_runToRound
 
--- The challenge-oracle inclusions used below are now provided (proved) by
--- `ProtocolSpec.subSpec_challenge_append_left` / `..._right` in `ProtocolSpec/SeqCompose.lean`.
+-- The challenge-oracle inclusions that `append_run`'s statement lifts along are provided (proved)
+-- by `ProtocolSpec.subSpec_challenge_append_left` / `..._right` in `ProtocolSpec/SeqCompose.lean`,
+-- together with their `LawfulSubSpec` instances — the latter are what make the lifts distribution-
+-- and support-preserving, hence usable by the security proofs below.
 
 /--
 States that running an appended prover `P₁.append P₂` with an initial statement `stmt₁` and

ArkLib/OracleReduction/ProtocolSpec/Basic.lean

@@ -681,6 +681,64 @@ def challengeQueryImpl {pSpec : ProtocolSpec n} [∀ i, SampleableType (pSpec.Ch
     QueryImpl ([pSpec.Challenge]ₒ'challengeOracleInterface) ProbComp :=
   fun q => $ᵗ (pSpec.Challenge q.1)
 
+section ChallengeReindex
+
+/-! ### Reindexing challenge oracles
+
+A protocol's challenge oracles embed into another's whenever challenge *indices* embed in a way
+that preserves the challenge *types*. That data — an index map `f` together with the transport
+`∀ i, q.Challenge (f i) = p.Challenge i` — is all a `SubSpec` needs, and it determines the lift
+uniquely, so we build the whole `SubSpec` / `LawfulSubSpec` / `DisjointSubSpec` package from it
+once here rather than case by case.
+
+Clients are the composition operators, each of which supplies an index map and a transport lemma.
+`++ₚ` supplies `ChallengeIdx.inl` / `ChallengeIdx.inr` with `challenge_append_inl` /
+`challenge_append_inr`; `seqCompose` would supply `sigmaChallengeIdxToSeqCompose`, whose transport
+follows from `seqCompose_challenge_eq` and `seqComposeChallengeEquiv.left_inv` (not instantiated
+here, as nothing consumes it yet). -/
+
+variable {k l : ℕ} {p : ProtocolSpec k} {q : ProtocolSpec l}
+  (f : p.ChallengeIdx → q.ChallengeIdx) (hf : ∀ i, q.Challenge (f i) = p.Challenge i)
+
+/-- Forward map on challenge queries induced by an index map: reindex, keep the (trivial) query. -/
+@[reducible] def challengeReindexQuery (t : [p.Challenge]ₒ.Domain) : [q.Challenge]ₒ.Domain :=
+  ⟨f t.1, t.2⟩
+
+/-- Backward map on challenge responses induced by an index map with matching challenge types:
+transport the response along `hf`. Note that this is the *only* possible choice, since `hf` is an
+equality of types — which is what makes `subSpecOfChallengeReindex` canonical. -/
+@[reducible] def challengeReindexResponse (t : [p.Challenge]ₒ.Domain)
+    (r : [q.Challenge]ₒ.Range (challengeReindexQuery f t)) : [p.Challenge]ₒ.Range t :=
+  show p.Challenge t.1 from (hf t.1) ▸ (show q.Challenge (f t.1) from r)
+
+/-- Transporting a challenge response along an equality of challenge types is a bijection.
+This is what makes the induced inclusion *lawful*, i.e. uniform-challenge preserving. -/
+theorem challengeReindexResponse_bijective (t : [p.Challenge]ₒ.Domain) :
+    Function.Bijective (challengeReindexResponse f hf t) :=
+  (Equiv.cast (hf t.1)).bijective
+
+/-- An embedding of challenge indices that preserves challenge types induces an inclusion of
+challenge oracles.
+
+`monadLift` is spelled out in lens form (rather than left to the class default) so that the lifted
+query reduces during `simp` / `rw` matching; see the `OracleSpec.SubSpec` docstring. -/
+@[reducible] def subSpecOfChallengeReindex : [p.Challenge]ₒ ⊂ₒ [q.Challenge]ₒ where
+  monadLift qry := ⟨challengeReindexQuery f qry.input,
+    qry.cont ∘ challengeReindexResponse f hf qry.input⟩
+  onQuery := challengeReindexQuery f
+  onResponse := challengeReindexResponse f hf
+
+/-- The induced inclusion is lawful: `onResponse` is bijective on every fibre, which is exactly
+what VCV-io needs to preserve the uniform distribution on challenges under the lift
+(`evalDist_liftComp`, `probEvent_liftComp`, `support_liftComp`). -/
+theorem lawfulSubSpecOfChallengeReindex :
+    letI := subSpecOfChallengeReindex f hf
+    [p.Challenge]ₒ ˡ⊂ₒ [q.Challenge]ₒ := by
+  letI := subSpecOfChallengeReindex f hf
+  exact ⟨challengeReindexResponse_bijective f hf⟩
+
+end ChallengeReindex
+
 /-- The oracle interface for state-restoration and (basic) Fiat-Shamir.
 
 This is the version where we hash the input statement and the entire transcript up to

ArkLib/OracleReduction/ProtocolSpec/SeqCompose.lean

@@ -432,64 +432,70 @@ instance : ∀ i, OracleInterface ((pSpec₁ ++ₚ pSpec₂).Challenge i) := cha
 
 /-- The challenge type of an appended protocol at a left-injected challenge index agrees with the
 challenge type of the left component. This is the transport fact needed to move challenge data
-across `++ₚ`. -/
+across `++ₚ`; it is `append_Type_castAdd` at the underlying round index, since `ChallengeIdx.inl`
+is `Fin.castAdd` on rounds. -/
 theorem challenge_append_inl (i : ChallengeIdx pSpec₁) :
-    (pSpec₁ ++ₚ pSpec₂).Challenge (ChallengeIdx.inl i) = pSpec₁.Challenge i := by
-  simp [ProtocolSpec.Challenge, ChallengeIdx.inl, ProtocolSpec.append,
-    Fin.vappend_eq_append, Fin.append_left]
+    (pSpec₁ ++ₚ pSpec₂).Challenge (ChallengeIdx.inl i) = pSpec₁.Challenge i :=
+  append_Type_castAdd (pSpec₁ := pSpec₁) (pSpec₂ := pSpec₂) i.1
 
 /-- The challenge type of an appended protocol at a right-injected challenge index agrees with the
-challenge type of the right component. -/
+challenge type of the right component. Dually to `challenge_append_inl`, this is
+`append_Type_natAdd` at the underlying round index. -/
 theorem challenge_append_inr (i : ChallengeIdx pSpec₂) :
-    (pSpec₁ ++ₚ pSpec₂).Challenge (ChallengeIdx.inr i) = pSpec₂.Challenge i := by
-  simp [ProtocolSpec.Challenge, ChallengeIdx.inr, ProtocolSpec.append,
-    Fin.vappend_eq_append, Fin.append_right]
-
-/-- Forward map on challenge queries: inject a left-component challenge index. -/
-@[reducible] def challengeInlOnQuery (t : [pSpec₁.Challenge]ₒ.Domain) :
-    [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ.Domain :=
-  ⟨ChallengeIdx.inl t.1, t.2⟩
-
-/-- Backward map on challenge responses for the left injection, transporting along
-`challenge_append_inl`. -/
-@[reducible] def challengeInlOnResponse (t : [pSpec₁.Challenge]ₒ.Domain)
-    (r : [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ.Range (challengeInlOnQuery (pSpec₂ := pSpec₂) t)) :
-    [pSpec₁.Challenge]ₒ.Range t :=
-  show pSpec₁.Challenge t.1 from
-    (challenge_append_inl (pSpec₂ := pSpec₂) t.1) ▸
-      (show (pSpec₁ ++ₚ pSpec₂).Challenge (ChallengeIdx.inl t.1) from r)
-
-/-- The challenge oracles of the left component embed into those of the appended protocol. -/
+    (pSpec₁ ++ₚ pSpec₂).Challenge (ChallengeIdx.inr i) = pSpec₂.Challenge i :=
+  append_Type_natAdd (pSpec₁ := pSpec₁) (pSpec₂ := pSpec₂) i.1
+
+/-- The challenge oracles of the left component embed into those of the appended protocol,
+by reindexing along `ChallengeIdx.inl`. -/
 instance subSpec_challenge_append_left :
-    [pSpec₁.Challenge]ₒ ⊂ₒ [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ where
-  monadLift q := ⟨challengeInlOnQuery (pSpec₂ := pSpec₂) q.input,
-    q.cont ∘ challengeInlOnResponse (pSpec₂ := pSpec₂) q.input⟩
-  onQuery := challengeInlOnQuery (pSpec₂ := pSpec₂)
-  onResponse := challengeInlOnResponse (pSpec₂ := pSpec₂)
-
-/-- Forward map on challenge queries: inject a right-component challenge index. -/
-@[reducible] def challengeInrOnQuery (t : [pSpec₂.Challenge]ₒ.Domain) :
-    [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ.Domain :=
-  ⟨ChallengeIdx.inr t.1, t.2⟩
-
-/-- Backward map on challenge responses for the right injection, transporting along
-`challenge_append_inr`. -/
-@[reducible] def challengeInrOnResponse (t : [pSpec₂.Challenge]ₒ.Domain)
-    (r : [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ.Range (challengeInrOnQuery (pSpec₁ := pSpec₁) t)) :
-    [pSpec₂.Challenge]ₒ.Range t :=
-  show pSpec₂.Challenge t.1 from
-    (challenge_append_inr (pSpec₁ := pSpec₁) t.1) ▸
-      (show (pSpec₁ ++ₚ pSpec₂).Challenge (ChallengeIdx.inr t.1) from r)
-
-/-- The challenge oracles of the right component embed into those of the appended protocol. -/
+    [pSpec₁.Challenge]ₒ ⊂ₒ [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ :=
+  subSpecOfChallengeReindex ChallengeIdx.inl (challenge_append_inl (pSpec₂ := pSpec₂))
+
+/-- The left inclusion is lawful, so lifting along it preserves the distribution and support of
+challenge queries. -/
+instance lawfulSubSpec_challenge_append_left :
+    [pSpec₁.Challenge]ₒ ˡ⊂ₒ [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ :=
+  lawfulSubSpecOfChallengeReindex ChallengeIdx.inl (challenge_append_inl (pSpec₂ := pSpec₂))
+
+/-- The challenge oracles of the right component embed into those of the appended protocol,
+by reindexing along `ChallengeIdx.inr`.
+
+Note that for the degenerate `pSpec ++ₚ pSpec` both this and `subSpec_challenge_append_left` apply,
+and typeclass resolution picks this one (declared later), routing challenges into the second copy.
+That mirrors VCV-io's `subSpec_add_left` / `subSpec_add_right` for `spec + spec`; pass the intended
+instance explicitly if the two components can coincide. -/
 instance subSpec_challenge_append_right :
-    [pSpec₂.Challenge]ₒ ⊂ₒ [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ where
-  monadLift q := ⟨challengeInrOnQuery (pSpec₁ := pSpec₁) q.input,
-    q.cont ∘ challengeInrOnResponse (pSpec₁ := pSpec₁) q.input⟩
-  onQuery := challengeInrOnQuery (pSpec₁ := pSpec₁)
-  onResponse := challengeInrOnResponse (pSpec₁ := pSpec₁)
-
-variable [∀ i, SampleableType (pSpec₁.Challenge i)] [∀ i, SampleableType (pSpec₂.Challenge i)]
+    [pSpec₂.Challenge]ₒ ⊂ₒ [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ :=
+  subSpecOfChallengeReindex ChallengeIdx.inr (challenge_append_inr (pSpec₁ := pSpec₁))
+
+/-- The right inclusion is lawful, so lifting along it preserves the distribution and support of
+challenge queries. -/
+instance lawfulSubSpec_challenge_append_right :
+    [pSpec₂.Challenge]ₒ ˡ⊂ₒ [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ :=
+  lawfulSubSpecOfChallengeReindex ChallengeIdx.inr (challenge_append_inr (pSpec₁ := pSpec₁))
+
+/-- The two inclusions occupy disjoint parts of the appended challenge interface: a left-injected
+round index is `< m` and a right-injected one is `≥ m`. This is what rules out the two components'
+challenge queries aliasing each other after composition. -/
+instance disjointSubSpec_challenge_append_left_right :
+    OracleSpec.DisjointSubSpec
+      [pSpec₁.Challenge]ₒ [pSpec₂.Challenge]ₒ [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ where
+  disjoint_onQuery t₁ t₂ h := by
+    have hv := congrArg
+      (fun (d : [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ.Domain) => (d.1.1 : ℕ))
+      (show challengeReindexQuery ChallengeIdx.inl t₁
+          = challengeReindexQuery ChallengeIdx.inr t₂ from h)
+    simp only [ChallengeIdx.inl, ChallengeIdx.inr, Fin.val_castAdd, Fin.val_natAdd] at hv
+    have := t₁.1.1.isLt
+    omega
+
+/-- `disjointSubSpec_challenge_append_left_right` with the two components swapped, matching
+VCV-io's pairing of `disjointSubSpec_add_left_right` / `disjointSubSpec_add_right_left`. -/
+instance disjointSubSpec_challenge_append_right_left :
+    OracleSpec.DisjointSubSpec
+      [pSpec₂.Challenge]ₒ [pSpec₁.Challenge]ₒ [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ where
+  disjoint_onQuery t₂ t₁ h :=
+    (disjointSubSpec_challenge_append_left_right.disjoint_onQuery t₁ t₂ h.symm)
 
 end Append
 

ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/SeqCompose.lean

@@ -165,7 +165,7 @@ theorem append_nodeOk_inl (S₁ : ChallengeTreeShape p₁) (S₂ : ChallengeTree
     (challenges : Fin ((S₁.append S₂).arity (ChallengeIdx.inl i₁)) →
         (p₁ ++ₚ p₂).Challenge (ChallengeIdx.inl i₁)) :
     (S₁.append S₂).nodeOk (ChallengeIdx.inl i₁) challenges
-      = S₁.nodeOk i₁ (fun j => cast (by simp [ProtocolSpec.append, ChallengeIdx.inl])
+      = S₁.nodeOk i₁ (fun j => cast (ProtocolSpec.challenge_append_inl i₁)
           (challenges (Fin.cast (by
             change S₁.arity i₁ = ChallengeTree.appendArity S₁.arity S₂.arity (ChallengeIdx.inl i₁)
             simp only [ChallengeTree.appendArity, Function.comp_apply,
@@ -186,7 +186,7 @@ theorem append_nodeOk_inr (S₁ : ChallengeTreeShape p₁) (S₂ : ChallengeTree
     (challenges : Fin ((S₁.append S₂).arity (ChallengeIdx.inr i₂)) →
         (p₁ ++ₚ p₂).Challenge (ChallengeIdx.inr i₂)) :
     (S₁.append S₂).nodeOk (ChallengeIdx.inr i₂) challenges
-      = S₂.nodeOk i₂ (fun j => cast (by simp [ProtocolSpec.append, ChallengeIdx.inr])
+      = S₂.nodeOk i₂ (fun j => cast (ProtocolSpec.challenge_append_inr i₂)
           (challenges (Fin.cast (by
             change S₂.arity i₂ = ChallengeTree.appendArity S₁.arity S₂.arity (ChallengeIdx.inr i₂)
             simp only [ChallengeTree.appendArity, Function.comp_apply,