Engine: definition and proven correctness of unanchored MemoBT

[shilangyu]

Termination is not proven due to issues described here:

Linden/future.typ

Line 26 in 4568342

- [ ] The proof of termination is admitted, namely `memobt_match_terminates_unanchored'`. By termination we mean that the fuel will be enough. The unanchored matching itself is not fuel based, its termination is proven on the fact that the input is decreasing on every recursive call. But between those recursive calls we call the anchored search function which is fuel based. We have a proof that the fuel we provide for the anchored search is sufficient, but the issue stems from the cache we share between each call.

But this is already self contained and has no admits. It also adds the LazyPrefix module which we previously discussed.