Doesn't that put the Rust compiler (and its assert lowering) in the trusted base? How do you know the asserts you wrote are the traps you're reasoning about?