Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Verifying Cake-Cutting, Faster

Noah Bertram, Tean Lai, Justin Hsu

TL;DR

The paper advances verification of envy-free cake-cutting protocols by (i) proving that any Slice execution under arbitrary valuations can be replicated by piecewise uniform valuations, enabling a reduction of envy-freeness constraints to linear real arithmetic and establishing decidability; (ii) introducing a linear (affine) type system that enforces disjoint allocations, eliminating the need for SMT to verify this essential correctness property; (iii) implementing both approaches atop Slice and validating them on increasingly complex protocols, including the first nontrivial four-agent case, with substantial runtime improvements and counterexample discovery capabilities. The methods yield scalable, automatic verification of envy-freeness alongside disjointness, broadening the practical applicability of formal methods to complex fair-division protocols. The work situates itself within social choice theory and formal verification, contributing a concrete, scalable pathway from high-level protocol descriptions to decidable, efficient constraint solving. Overall, it demonstrates that disjointness can be enforced via type systems, and envy-freeness can be decided via linear real arithmetic, enabling robust verification of complex protocols.

Abstract

Envy-free cake-cutting protocols procedurally divide an infinitely divisible good among a set of agents so that no agent prefers another's allocation to their own. These protocols are highly complex and difficult to prove correct. Recently, Bertram, Levinson, and Hsu introduced a language called Slice for describing and verifying cake-cutting protocols. Slice programs can be translated to formulas encoding envy-freeness, which are solved by SMT. While Slice works well on smaller protocols, it has difficulty scaling to more complex cake-cutting protocols. We improve Slice in two ways. First, we show any protocol execution in Slice can be replicated using piecewise uniform valuations. We then reduce Slice's constraint formulas to formulas within the theory of linear real arithmetic, showing that verifying envy-freeness is efficiently decidable. Second, we design and implement a linear type system which enforces that no two agents receive the same part of the good. We implement our methods and verify a range of challenging examples, including the first nontrivial four-agent protocol.

Verifying Cake-Cutting, Faster

TL;DR

The paper advances verification of envy-free cake-cutting protocols by (i) proving that any Slice execution under arbitrary valuations can be replicated by piecewise uniform valuations, enabling a reduction of envy-freeness constraints to linear real arithmetic and establishing decidability; (ii) introducing a linear (affine) type system that enforces disjoint allocations, eliminating the need for SMT to verify this essential correctness property; (iii) implementing both approaches atop Slice and validating them on increasingly complex protocols, including the first nontrivial four-agent case, with substantial runtime improvements and counterexample discovery capabilities. The methods yield scalable, automatic verification of envy-freeness alongside disjointness, broadening the practical applicability of formal methods to complex fair-division protocols. The work situates itself within social choice theory and formal verification, contributing a concrete, scalable pathway from high-level protocol descriptions to decidable, efficient constraint solving. Overall, it demonstrates that disjointness can be enforced via type systems, and envy-freeness can be decided via linear real arithmetic, enabling robust verification of complex protocols.

Abstract

Envy-free cake-cutting protocols procedurally divide an infinitely divisible good among a set of agents so that no agent prefers another's allocation to their own. These protocols are highly complex and difficult to prove correct. Recently, Bertram, Levinson, and Hsu introduced a language called Slice for describing and verifying cake-cutting protocols. Slice programs can be translated to formulas encoding envy-freeness, which are solved by SMT. While Slice works well on smaller protocols, it has difficulty scaling to more complex cake-cutting protocols. We improve Slice in two ways. First, we show any protocol execution in Slice can be replicated using piecewise uniform valuations. We then reduce Slice's constraint formulas to formulas within the theory of linear real arithmetic, showing that verifying envy-freeness is efficiently decidable. Second, we design and implement a linear type system which enforces that no two agents receive the same part of the good. We implement our methods and verify a range of challenging examples, including the first nontrivial four-agent protocol.
Paper Structure (10 sections, 2 theorems, 4 equations, 4 figures)

This paper contains 10 sections, 2 theorems, 4 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Verifying envy-freeness.
  3. Our work: verifying disjointness and envy-freeness, faster.
  4. Outline.
  5. Cake-Cutting Preliminaries
  6. Language and Type System
  7. Syntax of Base Slice
  8. A Linear Type System for Slice
  9. Semantics
  10. Disjointness

Key Result

proposition thmcounterproposition

If $\cdot \vdash e : \tau$ and $e \Downarrow v$, then $\cdot \vdash v : \tau$.

Figures (4)

  • Figure 1: The grammar for Slice expressions (top) and values (bottom).
  • Figure 2: Cut-choose in Slice.
  • Figure 3: Select typing rules for Slice expressions.
  • Figure 4: Select evaluation rules for Slice expressions.

Theorems & Definitions (2)

  • proposition thmcounterproposition: Type soundness
  • proposition thmcounterproposition