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

Open

Abraxas1010 wants to merge 4 commits into

Verified-zkEVM:mainfrom

Abraxas1010:feat/append-run-challenge-free

Commits on Jul 10, 2026

feat(Append): construct the challenge-oracle SubSpec embeddings (2 sorries removed)
Abraxas1010
committed
feat(SendWitness): prove reduction completeness; add Prover.runToRound_succ
Abraxas1010
committed

Commits on Jul 12, 2026

fix(ProtocolSpec): prove the partial-transcript splitters and index equivalences for seqCompose (6 sorries removed)
Richard Goodman
committed
feat(AppendRun): prove Prover.append_run for challenge-free protocols at general arity
Richard Goodman
committed