Skip to content

fix(ProtocolSpec): prove the partial-transcript splitters and index equivalences for sequential composition (6 sorries removed) #641

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
alexanderlhicks merged 1 commit into from
Jul 13, 2026
Merged

fix(ProtocolSpec): prove the partial-transcript splitters and index equivalences for sequential composition (6 sorries removed) #641

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
50 changes: 33 additions & 17 deletions ArkLib/OracleReduction/ProtocolSpec/SeqCompose.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -109,6 +109,18 @@ theorem rtake_append_right :
simp only [rtake, Fin.vappend_eq_append]
ext i : 2 <;> simp [Fin.rtake, Fin.append_right]

/-- Left type transport for `++ₚ` at a `castAdd` index: the appended spec's type
at an index in the first half is the left spec's type. -/
theorem append_Type_castAdd (i : Fin m) :
(pSpec₁ ++ₚ pSpec₂).«Type» (Fin.castAdd n i) = pSpec₁.«Type» i := by
simp only [Fin.vappend_eq_append, Fin.append_left]

/-- Right type transport for `++ₚ` at a `natAdd` index: the appended spec's type
at an index in the second half is the right spec's type. -/
theorem append_Type_natAdd (i : Fin n) :
(pSpec₁ ++ₚ pSpec₂).«Type» (Fin.natAdd m i) = pSpec₂.«Type» i := by
simp only [Fin.vappend_eq_append, Fin.append_right]

namespace Transcript

variable {k : Fin (m + n + 1)}
Expand All @@ -117,21 +129,20 @@ variable {k : Fin (m + n + 1)}

This is defined to be the full transcript for the first half if `k ≥ m`. -/
def fst (T : (pSpec₁ ++ₚ pSpec₂).Transcript k) : pSpec₁.Transcript ⟨min k m, by omega⟩ :=
if hk : k ≤ m then
fun i => by
dsimp [take]; have := T ⟨i, lt_of_lt_of_le i.isLt (inf_le_left)⟩; simp at this; sorry
-- dcast (by sorry) (T ⟨i, lt_of_lt_of_le i.isLt (inf_le_left)⟩)
else
fun i => sorry
-- dcast (by sorry) (T ⟨i, by omega⟩)
fun i => by
have him : (i : ℕ) < min (k : ℕ) m := i.isLt
exact _root_.cast
(append_Type_castAdd (pSpec₁ := pSpec₁) (pSpec₂ := pSpec₂) ⟨i.val, by omega⟩)
(T ⟨i.val, by omega⟩)

/-- The second half of a partial transcript for a concatenated protocol. -/
def snd (T : (pSpec₁ ++ₚ pSpec₂).Transcript k) : pSpec₂.Transcript ⟨k - m, by omega⟩ :=
if hk : k ≤ m then
fun i => Fin.elim0 (by simpa [hk] using i)
else
fun i => sorry
-- dcast (by sorry) (T ⟨m + i, by simp_all; dsimp at i; have := i.isLt; omega⟩)
fun i => by
have him : (i : ℕ) < (k : ℕ) - m := i.isLt
have hk := k.isLt
exact _root_.cast
(append_Type_natAdd (pSpec₁ := pSpec₁) (pSpec₂ := pSpec₂) ⟨i.val, by omega⟩)
(T ⟨m + i.val, by omega⟩)

end Transcript

Expand Down Expand Up @@ -186,7 +197,8 @@ theorem rtake_append_right (T : FullTranscript pSpec₁) (T' : FullTranscript pS
simp [rtake, Fin.rtake, append, Fin.cast, FullTranscript.cast, Transcript.cast]
have : ⟨m + n - n + i.val, by omega⟩ = Fin.natAdd m i := by ext; simp
rw! (castMode := .all) [this, Fin.happend_right]
sorry
apply eq_of_heq
exact ((eqRec_heq _ _).trans (cast_heq _ _)).trans (cast_heq _ _).symm

/-- The first half of a transcript for a concatenated protocol -/
def fst (T : FullTranscript (pSpec₁ ++ₚ pSpec₂)) : FullTranscript pSpec₁ :=
Expand Down Expand Up @@ -496,8 +508,10 @@ def seqComposeChallengeEquiv {m : ℕ} {n : Fin m → ℕ} (pSpec : ∀ i, Proto
toFun := fun ⟨i, j⟩ => sigmaChallengeIdxToSeqCompose i j
invFun := seqComposeChallengeIdxToSigma
left_inv := by
intro ⟨_, _⟩; simp [seqComposeChallengeIdxToSigma, sigmaChallengeIdxToSeqCompose]
sorry
intro ⟨i, j⟩
simp only [seqComposeChallengeIdxToSigma, sigmaChallengeIdxToSeqCompose]
rw! (castMode := .all) [Fin.splitSum_embedSum i j.1]
rfl
right_inv := by intro; simp [seqComposeChallengeIdxToSigma, sigmaChallengeIdxToSeqCompose]

def sigmaMessageIdxToSeqCompose {m : ℕ} {n : Fin m → ℕ} {pSpec : ∀ i, ProtocolSpec (n i)}
Expand All @@ -520,8 +534,10 @@ def seqComposeMessageEquiv {m : ℕ} {n : Fin m → ℕ} {pSpec : ∀ i, Protoco
toFun := fun ⟨i, msgIdx⟩ => sigmaMessageIdxToSeqCompose i msgIdx
invFun := seqComposeMessageIdxToSigma
left_inv := by
intro ⟨i, ⟨j, h⟩⟩ ; simp [seqComposeMessageIdxToSigma, sigmaMessageIdxToSeqCompose]
sorry
intro ⟨i, j⟩
simp only [seqComposeMessageIdxToSigma, sigmaMessageIdxToSeqCompose]
rw! (castMode := .all) [Fin.splitSum_embedSum i j.1]
rfl
right_inv := by intro; simp [seqComposeMessageIdxToSigma, sigmaMessageIdxToSeqCompose]

instance {m : ℕ} {n : Fin m → ℕ} {pSpec : ∀ i, ProtocolSpec (n i)}
Expand Down
Loading