That's the whole reason it's two passes - the first one you can prove (cat the chunks, cmp against the original), the second one the compiler proves. It's an assurance that the process is working.