Verification of a Merkle Patricia Tree Library Using F. - Sota Sato 002; Ryotaro Banno; Jun Furuse; Kohei Suenaga; Atsushi Igarashi (CoRR, 2021)