Constraint-based correctness proofs for logic program transformations