This post provides a first introduction to proving correctness of Jasmin programs in EasyCrpypt