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.

[Abraxas1010]

Rebased onto current main (7466a592); #641 having merged, its commit drops out of the stack cleanly, so this branch is now three commits.

Why now: the whole stack was pinned to leanprover/lean4:v4.30.0 while main moved to v4.31.0. Every PR read as mergeable-and-green, but those runs are from 10–12 July against 4.30-era main. I have rebased all five (#631, #633, #635, #636, this one) and build-verified each locally at 4.31: full lake build ArkLib green, no new sorry. Only #636 needed a repair — a CoeT (QueryImpl …) synthesis timeout from an unpinned pSpec, detailed there — and it was elaboration, not mathematics.

An offer about the shape of this stack

Five open PRs from one outside contributor is a large review ask, and I suspect that is the real reason this has been sitting rather than anything in the proofs. The contents are one connected result — sequential-composition completeness — split the way I happened to develop it:

• feat(SendWitness): prove reduction completeness; add Prover.runToRound_succ #631 SendWitness reduction completeness + Prover.runToRound_succ
• feat(Append): construct the challenge-oracle SubSpec embeddings #633 the challenge-oracle SubSpec embeddings
• feat(Append): completeness composition under init-uniformity + run_pure_verifier #635 completeness composition under init-uniformity + run_pure_verifier
• feat(AppendOneMsg): unconditional append perfect completeness at 1-message ++ 1-message #636 unconditional append perfect completeness at 1-message ++ 1-message
• feat(AppendRun): prove Prover.append_run for challenge-free protocols at general arity #643 Prover.append_run for challenge-free protocols at general arity, plus AppendRunNecessity.raw_factorization_fails showing the hypothesis is not removable

I am happy to collapse these into a single feat(Append): sequential composition completeness PR if that is cheaper to review — one branch, one CI run, one conversation — and close the other four as superseded. Or to keep them split, or to split them differently. Say which and I will restructure; I would rather spend the effort on the packaging you actually want to read than leave five stale branches in your queue.

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

[github-actions]

🤖 PR Summary

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

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

---

Statistics

Metric	Count
📝 Files Changed	5
✅ Lines Added	1135
❌ Lines Removed	4

---

Lean Declarations

✏️ Added: 40 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)

---

sorry Tracking

✅ Removed: 3 `sorry`(s)

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

• def StateFunction.append (L334)
• def StateFunction.append (L335)

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

• theorem reduction_completeness : (L100)

---

📋 **Additional Analysis**

Several violations of the ArkLib contribution guidelines were found. File naming, theorem naming, element naming within theorems, line length, and style all contain deviations from the specified standards. Please see the detailed findings below. Note: A full line-length check was not performed; the few flagged examples indicate the presence of lines exceeding the 100-character limit. The diff is largely relevant to the instructions, so 'No findings' was not returned.

---

📄 **Per-File Summaries**

• ArkLib.lean: The file ArkLib.lean adds an import for ArkLib.OracleReduction.Composition.Sequential.AppendRun. This new import makes the definitions, theorems, and API from that module available to any project that imports ArkLib, extending the library’s support for sequential composition of oracle reductions with an “append run” variant.
• ArkLib/OracleReduction/Composition/Sequential/Append.lean: Replaces two placeholder sorry instances for [(pSpec₁).Challenge]ₒ ⊂ₒ [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ and [(pSpec₂).Challenge]ₒ ⊂ₒ [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ with complete implementations. Adds two new theorems ProtocolSpec.Challenge_inl and ProtocolSpec.Challenge_inr that prove the challenge type at a left‑ or right‑embedded index equals the original protocol's challenge type. The instances use these theorems to transport responses via cast together with ChallengeIdx.inl/inr for index embedding.
• ArkLib/OracleReduction/Composition/Sequential/AppendRun.lean: This file, AppendRun.lean, proves the Prover.append_run theorem (previously stated as a sorry in Append.lean) for the special case of challenge-free (message-only) protocols — the class produced by the commitment/BCS transform. It adds three main theorems: append_run_of_challenge_free (for a non-empty right protocol, n = n' + 1), append_run_of_challenge_free_zero (for an empty right protocol, n = 0), and append_run_of_challenge_free_liftM (which restates the first with the exact liftM-based signature of the library's original Prover.append_run). The proof is structured as a three-layer construction: (1) a per-round field layer of HEq-stated equations (append_sendMessage_left_general, append_receiveChallenge_left_general, append_sendMessage_boundary_general, append_sendMessage_right_general, append_receiveChallenge_right_general, append_output_general) for the Prover.append operations at abstract left/boundary/right indices; (2) two run invariants — append_runToRound_left_of_challenge_free (left region: the appended run is P₁'s run, lifted and transported) and append_runToRound_right_of_challenge_free (right region: the appended run is P₁'s full run, then the P₁.output ∘ P₂.input handoff, then P₂'s run, glued via a new trGlue transport defined using take_append_add); and (3) the assembly at Fin.last. Supporting infrastructure includes new theorems dir_left, dir_right, PrvState_left, PrvState_right, take_append_of_le, take_append_add, trLeft, trLeft_concat, trGlue, trGlue_concat, trGlue_zero, trGlue_full, and several commuting lemmas for liftM/liftComp/cast (liftM_cast_comm, cast_bind, cast_prod_fst, cast_prod_snd, liftM_liftM_challenge, liftM_liftM_challenge₂, liftComp_liftM_challenge₁, liftComp_liftM_challenge₂). The file adds a total of 0 sorry or admit declarations; it includes a detailed comment block at the end documenting the proof status, tooling lessons, and honest fences (notably that the general non-challenge-free case remains gated on a separate challenge-lift alignment development).
• ArkLib/OracleReduction/Execution.lean: Adds the theorem Prover.runToRound_succ, which provides a one-step unfolding lemma for runToRound. It states that running the prover to round i.succ equals running to round i.castSucc and then processing round i via prover.processRound. This complements the existing Prover.runToRound_zero_of_prover_first theorem and is intended as a workhorse for collapsing concrete protocol executions round by round, e.g. in component completeness proofs.
• ArkLib/ProofSystem/Component/SendWitness.lean: The proof of reduction_completeness was completed by replacing a sorry with a detailed argument. The proof now uses simp to unfold the completeness definitions and then establishes the two conditions for one_le_probEvent_iff. The first condition shows that the probability of failure is zero by rewriting with simulateQ_pure and using probOutput_eq_zero_of_not_mem_support, exploiting the fact that none is not in the support of a pure some computation. The second condition shows that every possible output x in the support is of the expected form, using the same rewriting to reduce to a case analysis on the pure value, concluding that the witness must satisfy the input relation hIn.

---

Last updated: 2026-07-28 14:54 UTC.

[Abraxas1010]

Note on the red checks: both failures are pre-existing on main, not from this PR.

CI — the Lean build is green. lake build ArkLib completes (✔ Built ArkLib) with no errors; the job then fails in ./scripts/validate.sh on:

Errors:
  - Paper page without matching BibTeX key: docs/kb/papers/NOZ26.md

docs/kb/papers/NOZ26.md is on main and was added upstream in June; this branch adds no docs/kb files. The same error reproduces byte-for-byte on unrelated open PRs — e.g. #574 (guruswami-sudan), whose CI ran after this one.

Build and Deploy Website to GitHub Pages — fails on the blueprint declaration check:

Fold.folding_preserves_listdecoding_base is missing.
Fold.folding_preserves_listdecoding_bound is missing.
Fold.folding_preserves_listdecoding_base_ne_subset is missing.
WhirIOP.whir_rbr_soundness is missing.

This workflow has failed on every run for at least the past two weeks, across every contributor's branch (#574, #610, #503, ElijahVlasov/*, tr/*, …). None of those declarations are touched here.

Logs: CI run · Pages run

Happy to open a separate fix for the NOZ26 BibTeX entry if that would help unblock CI repo-wide.