Function lemma_u64_and_zero 

pub proof fn lemma_u64_and_zero(x: u64)

ensures

0u64 & x == 0u64,

AND-ing the zero word with any word is zero.