Proved mk_asn and made better hoare rules. However, the specification of these is not finished.
Trying with a new definition of hoare_read.