Restructure indshrink helper functions
Restructure indshrink helper functions

The helper functions were proven to leave every indirect block tree in a
consistent state, where the top block was valid iff any of its children were
valid. This resulted in useless re-reads of the same block and redundant checks
on bounds. This patch adds an indshrink_clear helper and restructures the
indshrink_aligned and indshrink_ragged_to_aligned helpers to work on invalid
trees, leaving it to the caller to ensure that the tree is valid upon
completion. This had the pleasant side effect of reducing the preconditions to
these functions as well.

As of now, all the indshrink helpers are proven, though indshrink itself is
not. The messy proofs will be cleaned up in a future commit.

mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl