Macro verus_exec_expr_keep_ghost 

verus_exec_expr_keep_ghost!() { /* proc-macro */ }