Why Extension-Based Proofs Fail
summary
Claim: no extension-based proof can establish the impossibility of k‑set agreement for more than k processes. Proof works in the non-uniform iterated immediate snapshot (NIS) model, builds an adaptive adversarial decision map Δ, and answers any prover query by incrementally defining outputs so queried regions remain local and far apart via repeated chromatic subdivision. The construction forces every finite phase to terminate without producing an inconsistency or infinite chain, so every prover loses against this protocol.
AI-written summary · about
chapters (10)
- 0:00Intro
- 0:19Consensus Problem
- 2:08k-set Agreement Problem
- 3:50Outline
- 7:37Non-uniform Iterated Immediate Snapshot (NIIS) Model HS99 . An adversarial scheduler decides the order in which processes take
- 11:51Some Basic Combinatorial Topology
- 18:25Non-Uniform Chromatic Subdivision of a Simplicial Complex
- 29:04There is no Extension-Based Proof for the Unsolvability of k-set agreement
- 30:34A Strategy for the Adversarial Protocol During phase 1, when the prover performs a query scheduling a set of processes from
- 31:33A Strategy for the Adversarial Protocol At the beginning of phase 2
related talks
45mCorrectness proofs of distributed systems with Isabelle
01h 03mTrustworthy Automated Reasoning
19mDIZK: A Distributed Zero Knowledge Proof System
22mDIZK: A Distributed Zero Knowledge Proof System
24mVerifying Almost-Sure Termination for Randomized Distributed Algorithms
25mProperty-agnostic base case extension for scalable verification of distributed systems
16mInductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline...
13mCharacterizing Implementability of Global Protocols with Infinite States and Data