Declaring an axiom to fabricate false proofs, turning Lean 4 proof-carrying array accessors into arbitrary memory reads, and forging a closure object to call readFile
