ainvs: clean up and arch split BCorres RISCV64 will need slight variations in the arch dependent proofs