add initial version of equal and mismatch algorithm, together with verifast annotations