def parse.multi.sized.index_length

mylsm-lsm-store@0.6.0.1 · src/ByteSstFile.bend:1883

import Base
import mylsm-lsm-store@0.6.0.1/src/ByteMemTable.bend as ByteMemTable
import bend-kit-bytes@0.3.2.0/bytes.bend as Bytes

1883def parse.multi.sized.index_length(
1884  source: Bytes.Bytes,
1885  file: Bytes.Bytes,
1886  +blocks: Nat,
1887  +entries: Nat,
1888  +level: Nat,
1889  +size: Nat,
1890  result: Bytes.Bytes & Maybe<&2, U32>
1891) -> Result<&1, &1, Error, ByteMemTable.Table>:
1892  match result:
1893    case (_, Some{length}):
1894      +index_length = U32.to_nat(length)
1895      +minimum_index_length = Nat.add(8n, Nat.mul(blocks, 16n))
1896      +index_size = Nat.add(44n, index_length)
1897      parse.multi.sized.valid(source, file, blocks, entries, level, size,
1898        index_length,
1899        Nat.is_le(minimum_index_length, index_length) &&
1900          Nat.is_le(index_size, size) &&
1901          Nat.is_le(20n, Nat.sub(size, index_size)))
1902    case (_, None{}): Fail{Malformed{}}