StorageAddressBounds.natural_bound: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_address_bounds.bend as StorageAddressBounds
Lines 28-31 of stelliferous@0.0.2.0/proofs/storage_address_bounds.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/storage_address_bounds.bend&start_line=28&end_line=31

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

def natural_bound(+depth: Nat,+index: U32,+limit: {Nat.is_le(depth,31n) == True{} : Bool},bound: {U32.is_lt(index,capacity(depth)) == True{} : Bool}) ->
  {Nat.is_lt(U32.to_nat(index),Shape.extent(depth)) == True{} : Bool}:
  %capacity_value(depth,limit) : {Nat.is_lt(U32.to_nat(index),_) == True{} : Bool}
  Bounds.as_nat_lt(index,capacity(depth),bound)

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend&name=as_nat_lt
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_address_bounds.bend&name=capacity
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_address_bounds.bend&name=capacity_value
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_shape.bend&name=extent