Verifying Cake-Cutting, Faster

TL;DR

This paper enhances the Slice language and verification methods for envy-free cake-cutting protocols, enabling efficient verification of more complex protocols, including the first nontrivial four-agent example.

Contribution

It introduces a linear type system and reduces verification to linear real arithmetic, improving scalability and enabling verification of complex protocols.

Findings

Successfully verified complex cake-cutting protocols

Reduced verification to linear real arithmetic formulas

Verified the first nontrivial four-agent protocol

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.