def natural_bound

stelliferous@0.0.2.0 · proofs/storage_address_bounds.bend:28

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

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