AllocationLAWS.storage_seek_bounds: law of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/allocation_LAWS.bend as AllocationLAWS
Lines 24-35 of bendtorch-core@0.1.0.0/src/tensor/allocation_LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/allocation_LAWS.bend&start_line=24&end_line=35

import Base
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model

law storage_seek_bounds:
  for +fuel: Nat
  for +length: Nat
  for +depth: Nat
  for +capacity: Nat
  for done: Bool
  for +decided: {done == Nat.is_le(length, capacity) : Bool}
  for +sized: {capacity == Model.capacity(depth) : Nat}
  for +left: {Nat.add(fuel, depth) == 20n : Nat}
  for +limit: {Nat.is_le(length, Model.capacity(20n)) == True{} : Bool}
  for +positive: {Nat.is_lt(0n, length) == True{} : Bool}
  {Storage.bounds(Pair.fst(Nat, Nat, Storage.depth_seek(fuel, length, depth, capacity, done)), length) == True{} : Bool}

Uses (10):
  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.add
  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=Pair.fst
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=seek_bounds
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=bounds
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=depth_seek
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=capacity