Function check_encoder_sound 

pub fn check_encoder_sound(source: &str) -> SoundnessReport

Cross-validate the LOGOS encoder against the tree-walking interpreter on one program.

Runs the program through interpret_program (the independent ground truth) and the symbolic encoder, then proves with Z3 that they agree on the full observable behavior — the ordered Show outputs and whether an error was raised. This is the meta-oracle that makes the encoder trustworthy: a buggy encoder is caught here, not masked by a downstream equivalence that “proves” two wrong things equal.