def child_limit

stelliferous@0.0.2.0 · proofs/storage_address_bounds.bend:106

import Base
import stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend as Bounds

106# Existing allocation proofs use the smaller, 30-bit allocation limit.
107def child_limit(+depth: Nat,limit: {Nat.is_le(1n+depth,30n) == True{} : Bool}) -> {Nat.is_le(depth,30n) == True{} : Bool}:
108  Bounds.strict_le(depth,30n,Bounds.predecessor_strict(depth,30n,limit))