Consider replacing axioms with conjectures

We currently describe Rust's memory model via `axiom`s. We might want to instead create a Lean object which represents the Rust memory model and implicitly inject this as a conjecture in all of our proofs instead of literally introducing it as an `axiom`.