Macro try_open_atomic_update_internal 

macro_rules! try_open_atomic_update_internal {
    ($au:expr, $x:pat => $body:block, @EXEC, $wrap_fn:ident) => { ... };
    ($au:expr, $x:pat => $body:block, @PROOF, $wrap_fn:ident) => { ... };
    ($au:expr, $x:pat => $body:block) => { ... };
}