fixes to move compat lemma, started working on move-return-address compat lemma