feat(AppendRun): prove Prover.append_run for challenge-free protocols at general arity

[Abraxas1010]

Summary

Proves the library's open composition keystone Prover.append_run (stated with a sorry in Composition/Sequential/Append.lean, under the authors' comment "when do these theorems hold?") for challenge-free (message-only) protocols — the class the commitment/BCS transform actually produces — at fully general arity, in a new module Composition/Sequential/AppendRun.lean:

• append_run_of_challenge_free (right protocol of arity n'+1): running P₁.append P₂ is running P₁, handing its output to P₂.input, running P₂, and appending the transcripts.
• append_run_of_challenge_free_zero (empty right protocol — challenge-freeness on the right is vacuous over Fin 0).
• append_run_of_challenge_free_liftM — the statement spelled exactly as the library's Prover.append_run do-block (destructuring lets, ambient liftM); a definitional restatement of the first theorem.

Structure of the proof

1. Field layer — per-round send/receive/boundary/output equations for Prover.append at abstract indices, HEq-stated to stay transport-free (the boundary equation exhibits composed round m as P₂'s opening round fused with the P₁.output ∘ P₂.input handoff).
2. Left-region invariant — for k ≤ m, the composed runToRound is P₁'s, lifted into the composed challenge sum and transported (Fin.induction).
3. Right-region invariant — past the boundary, the composed partial run is P₁'s full run, the handoff, and P₂'s partial run, glued along trGlue — which is the library's own happend transported along a new spec-level right-prefix identity take_append_add : (pSpec₁ ++ₚ pSpec₂).take (m+j) = pSpec₁ ++ₚ pSpec₂.take j (interpolating the existing take_append_left). Nat-induction with all indices pinned at the definitionally-reducing jv+1 spelling.
4. Assembly at Fin.last, via a liftComp-of-run distribution lemma and the output field equation.

Reusable side-products: take_append_add, the glue transport trGlue with its concat/zero/full laws, the right-region state décalage PrvState_right, and lift-route coherence lemmas for both component challenge sums.

Verification

• lake build ArkLib green with the module registered in ArkLib.lean.
• Every top-level theorem checked with #print axioms: [propext, Classical.choice, Quot.sound] — no sorry, no extra axioms.
• Non-vacuity: the assembly statements are not closed by rfl (probe included in development; the two run-invariant inductions carry the content).

Scope and honesty

• This is the challenge-free instance of Prover.append_run. The general case needs an alignment of the composed challenge oracle with the components' across arbitrary challenge rounds (the general form of the lift-route pinning this proof handles for message rounds); that is a separate development and the original sorry is intentionally left in place for it.
• Stacked on feat(SendWitness): prove reduction completeness; add Prover.runToRound_succ #631 (uses Prover.runToRound_succ), feat(Append): construct the challenge-oracle SubSpec embeddings #633 (uses the challenge-oracle SubSpec embeddings), and fix(ProtocolSpec): prove the partial-transcript splitters and index equivalences for sequential composition (6 sorries removed) #641 (uses append_Type_castAdd/natAdd from the SeqCompose repair). This PR's diff includes those commits until they merge.

[github-actions]

🤖 PR Summary

sorry delta: -9 (9 removed) — net proof progress

Failed to generate AI summary. Please check the per-file summaries and statistics below.

---

Statistics

Metric	Count
📝 Files Changed	6
✅ Lines Added	1168
❌ Lines Removed	21

---

Lean Declarations

✏️ Added: 42 declaration(s)

ArkLib/OracleReduction/Composition/Sequential/Append.lean (2)

• theorem _root_.ProtocolSpec.Challenge_inl (i : pSpec₁.ChallengeIdx) :
• theorem _root_.ProtocolSpec.Challenge_inr (i : pSpec₂.ChallengeIdx) :

ArkLib/OracleReduction/Composition/Sequential/AppendRun.lean (37)

• def trGlue (j : Fin (n + 1)) (T₁ : pSpec₁.FullTranscript) (T₂ : pSpec₂.Transcript j) :
• def trLeft (k : Fin (m + 1)) (T : pSpec₁.Transcript k) :
• theorem PrvState_left (k : Fin (m + 1)) :
• theorem PrvState_right {jv : ℕ} (hjv : jv < n) :
• theorem append_input_general (ctx : Stmt₁ × Wit₁) :
• theorem append_output_general (hn : n ≠ 0)
• theorem append_output_zero {pSpec₂' : ProtocolSpec 0}
• theorem append_receiveChallenge_left_general
• theorem append_receiveChallenge_right_general
• theorem append_runToRound_left_of_challenge_free
• theorem append_runToRound_right_of_challenge_free
• theorem append_run_of_challenge_free_liftM
• theorem append_run_of_challenge_free_zero
• theorem append_run_of_challenge_free
• theorem append_sendMessage_boundary_general (hn : 0 < n)
• theorem append_sendMessage_left_general
• theorem append_sendMessage_right' {jv : ℕ} (hj : jv + 1 < n)
• theorem append_sendMessage_right_general
• theorem cast_bind {ι₂ : Type} {S₂ : OracleSpec ι₂}
• theorem cast_fullTranscript_apply {N : ℕ} {s t : ProtocolSpec N} (h : s = t)
• theorem cast_prod_fst {α α' β β' : Type} (h₁ : α = α') (h₂ : β = β') (p : α × β) :
• theorem cast_prod_snd {α α' β β' : Type} (h₁ : α = α') (h₂ : β = β') (p : α × β) :
• theorem dir_left {i : ℕ} (hi : i < m) :
• theorem dir_right {j : ℕ} (hj : j < n) :
• theorem liftComp_liftM_challenge₁ {α : Type} (x : OracleComp oSpec α) :
• theorem liftComp_liftM_challenge₂ {α : Type} (x : OracleComp oSpec α) :
• theorem liftComp_prover_run {ιT : Type} {tSpec : OracleSpec ιT}
• theorem liftM_cast_comm {ι₁ ι₂ : Type} {S₁ : OracleSpec ι₁} {S₂ : OracleSpec ι₂}
• theorem liftM_liftM_challenge {α : Type} (x : OracleComp oSpec α) :
• theorem liftM_liftM_challenge₂ {α : Type} (x : OracleComp oSpec α) :
• theorem take_append_add {j : ℕ} (hj : j ≤ n) :
• theorem take_append_of_le {k : ℕ} (hk : k ≤ m) :
• theorem trGlue_concat (r : Fin n) (T₁ : pSpec₁.FullTranscript)
• theorem trGlue_full (T₁ : pSpec₁.FullTranscript) (T₂ : pSpec₂.Transcript (Fin.last n)) :
• theorem trGlue_zero (T₁ : pSpec₁.FullTranscript) (T₂ : pSpec₂.Transcript 0) :
• theorem trLeft_concat (i : Fin m) (T : pSpec₁.Transcript i.castSucc)
• theorem vappend_take {γ : Sort*} (f : Fin m → γ) (g : Fin n → γ) {j : ℕ} (hj : j ≤ n) :

ArkLib/OracleReduction/Execution.lean (1)

• theorem Prover.runToRound_succ (i : Fin n)

ArkLib/OracleReduction/ProtocolSpec/SeqCompose.lean (2)

• theorem append_Type_castAdd (i : Fin m) :
• theorem append_Type_natAdd (i : Fin n) :

---

sorry Tracking

✅ Removed: 9 `sorry`(s)

ArkLib/OracleReduction/Composition/Sequential/Append.lean (2)

• def StateFunction.append (L323)
• def StateFunction.append (L324)

ArkLib/OracleReduction/ProtocolSpec/SeqCompose.lean (6)

• def fst (T : (pSpec₁ ++ₚ pSpec₂).Transcript k) : pSpec₁.Transcript ⟨min k m, by omega⟩ (L122)
• def fst (T : (pSpec₁ ++ₚ pSpec₂).Transcript k) : pSpec₁.Transcript ⟨min k m, by omega⟩ (L125)
• def seqComposeChallengeEquiv {m : ℕ} {n : Fin m → ℕ} (pSpec : ∀ i, ProtocolSpec (n i)) : (L500)
• def seqComposeMessageEquiv {m : ℕ} {n : Fin m → ℕ} {pSpec : ∀ i, ProtocolSpec (n i)} : (L524)
• def snd (T : (pSpec₁ ++ₚ pSpec₂).Transcript k) : pSpec₂.Transcript ⟨k - m, by omega⟩ (L133)
• theorem rtake_append_right (T : FullTranscript pSpec₁) (T' : FullTranscript pSpec₂) : (L189)

ArkLib/ProofSystem/Component/SendWitness.lean (1)

• theorem reduction_completeness : (L77)

---

📋 **Additional Analysis**

The diff contains several violations of the ArkLib contribution guidelines, primarily in the new AppendRun.lean file and in Execution.lean. The main issues are style (line length, empty lines inside proofs) and documentation (missing docstrings for many theorems/definitions). The large contribution also suggests a blueprint would be appropriate, though this is not a strict violation.

---

📄 **Per-File Summaries**

• ArkLib/OracleReduction/Composition/Sequential/Append.lean: Summary unavailable — error: 1 validation error for _ProseSummary
  Invalid JSON: expected value at line 1 column 1 [type=json_invalid, input_value="The file replaces two pr...to transport responses.", input_type=str]
  For further information visit https://errors.pydantic.dev/2.13/v/json_invalid
• ArkLib/OracleReduction/Composition/Sequential/AppendRun.lean: This new file (AppendRun.lean) proves Prover.append_run — stated with a sorry in Append.lean — for challenge‑free (message‑only) protocols, the class produced by the commitment/BCS transform, at fully general arity. The central theorems are append_run_of_challenge_free (right protocol non‑empty), append_run_of_challenge_free_zero (empty right protocol), and append_run_of_challenge_free_liftM (the exact do‑block shape of the library's Prover.append_run). The proof is built from a per‑round field layer (append_sendMessage_left_general, …), two run‑invariants (append_runToRound_left_of_challenge_free, append_runToRound_right_of_challenge_free) that glue the left region (P₁'s run) and right region (handoff + P₂'s run) using transcript transports trLeft and trGlue, and an assembly step at Fin.last. All theorems carry the standard axiom footprint [propext, Classical.choice, Quot.sound] and are verified non‑vacuous; the file contains no sorry or admit.
• ArkLib/OracleReduction/Execution.lean: Added theorem Prover.runToRound_succ that provides a one-step unfolding of runToRound: it expresses execution up to round i.succ as executing up to round i.castSucc followed by processing round i. This lemma is intended as the workhorse for collapsing concrete protocol executions round by round, for example in component completeness proofs.
• ArkLib/OracleReduction/ProtocolSpec/SeqCompose.lean: The diff adds the two transport theorems append_Type_castAdd and append_Type_natAdd, which describe the type of a concatenated protocol spec at Fin.castAdd and Fin.natAdd indices respectively. These new lemmas are then used to replace the sorry-filled conditional logic in the Transcript.fst and Transcript.snd functions, providing complete definitions via cast. The previously sorry-terminated proof of rtake_append_right is now finished using eq_of_heq and cast equalities. Additionally, the left_inv proofs of seqComposeChallengeEquiv and seqComposeMessageEquiv are completed by applying Fin.splitSum_embedSum instead of the prior sorry stubs.
• ArkLib/ProofSystem/Component/SendWitness.lean: The theorem reduction_completeness, which states that (reduction oSpec Statement Witness).perfectCompleteness init impl relIn (toRelOut relIn) holds, previously had a sorry for its proof. It is now fully proved, using simulateQ_pure, OptionT, and StateT operations to show that the reduction's execution yields probability 1 of success. No other changes are made to the file.
• 1 file(s) filtered as noise (lockfiles, generated, or trivial): ArkLib.lean

---

Last updated: 2026-07-12 04:39 UTC.

[Abraxas1010]

Pushed one addition: AppendRunNecessity.lean (1790361), answering the converse question — is the challenge-freeness/message-opening restriction actually needed, or does the raw factorization hold for all provers?

It is needed. raw_factorization_fails is a kernel-checked counterexample: for the smallest pair whose boundary round is a challenge (empty left protocol, one V_to_P round on the right) and a prover whose handoff output makes an oracle query, the composed run is not equal to the sequential composition of the two runs. The reason is effect order: the composed machine samples the boundary challenge before the handoff output runs, while the sequential form runs the output first. Since OracleComp is a free monad, the two computations differ at their head query's Sum index, and a Boolean head-query observer (headIsLeft) turns that into False by kernel evaluation alone — two rfl probes pin the two effect orders. Axioms: [propext, Classical.choice, Quot.sound]; full library builds green.

So the hypothesis in this PR sits exactly at the boundary of raw-level truth: left challenges are fine unconditionally, and only the right protocol's opening round matters; past that, agreement can only be distributional (independent effects commute in law, not in syntax), which would be a separate lemma over a commutative effect interpretation rather than a strengthening of this one. Happy to split the necessity module out of this PR if you'd rather keep it minimal.