Correctness of the TRIM Compiler