return uint64 z
in uint64 x
in uint64 y
call uint64_leq_mask