Document Assumption 1

[catalin-hritcu]

Our README should not only explain how we tested Assumption 1 from our CCS'24 paper, but also where that axiom is stated for use in the proofs.

We should also make sure the axiom includes the MAX_TRACE_LENGTH prefix size bound like in the paper, and we should probably have another axiom that MAX_TRACE_LENGTH < 2 ^ 64 (since otherwise we would need to include 2 ^ 64 in our main theorem too, coming from back-translation).