Function native_aux_name 

pub fn native_aux_name(name: &str) -> String

Suffix for the native-emit auxiliary fn that carries the explicit precondition parameter. Mirrors fuel_helper_name’s ASCII-only shape so Lean accepts it verbatim.