Stupid question: if the lean4 code is a copy of the C code, how does "it" know which code is a bug and which code is working as intended?