Right, that's what I thought. So at a high level helper methods are equivalent in some sense to 'unsafe' code in rust and require manual validation for security

Right, that's what I thought. So at a high level helper methods are equivalent in some sense to 'unsafe' code in rust and require manual validation for security (i.e. the verifier ignores them other than to check they are in some helper method whitelist for the program type)?