Verify the list based insert optimization
We verify the sapling client library's implementation API for IMTs, as shipped in Edo-008.
TASKS
-
Add iterated insertion to the model (as a foldl with insert_model) -
Add split_at
implementation and prove its specification. -
Implement the mutually recursvie [insert_list] and [insert_node]. -
Prove interchange with iter_insert in the model. -
Prove the specification for [insert_list] -
Pack the external API and prove the specification. -
Improve comments.
Edited by Germán Delbianco