  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.
