Garbage collectors relieve the programmer from manual memory
management, but lead to compiler-generated machine code that can
behave differently (e.g.\ out-of-memory errors) from the source
code. To ensure that the generated code behaves exactly like the
source code, programmers need a way to answer questions of the form:
what is a sufficient amount of memory for
my program to never reach an out-of-memory error?

This paper develops a cost semantics that can answer such
questions for CakeML programs. The work described in this paper is
the first to be able to answer such questions with proofs in the
context of a language that depends on garbage collection. We
demonstrate that positive answers can be used to transfer liveness
results proved for the source code to liveness guarantees about the
generated machine code. Without guarantees about space usage, only
safety results can be transferred from source to machine code.

Our cost semantics is phrased in terms of an abstract intermediate
language of the CakeML compiler, but results proved at that level
map directly to the space cost of the compiler-generated machine
code. All of the work described in this paper has been developed in
the HOL4 theorem prover.