Exact $p$-adic computation in Magma

We describe a new arithmetic system for the Magma computer algebra system for working with $p$-adic numbers exactly, in the sense that numbers are represented lazily to infinite $p$-adic precision. This is the first highly featured such implementation. This has the benefits of increasing user-friendliness and speeding up some computations, as well as forcibly producing provable results. We give theoretical and practical justification for its design and describe some use cases. The intention is that this article will be of benefit to anyone wanting to implement similar functionality in other languages.