Naive Fixed-Position Implementation
Verifies a single-commit version of insert inspired after the F* development, in which the position argument is not kept fixed, but recomputed when recursing on the right subtree, in order to avoid reasoning about overflows.
TASKS:
-
add internal API implementation for insert_pos
and get. -
prove interchange with the model. -
prove spec of insert_pos -
add external appi implementation for add_pos
. -
prove spec of add_pos and get_pos. -
polish and format comments
Edited by Germán Delbianco