law storage_seek_bounds

bendtorch-core@0.1.0.0 · src/tensor/allocation_LAWS.bend:24

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

24law storage_seek_bounds:
25  for +fuel: Nat
26  for +length: Nat
27  for +depth: Nat
28  for +capacity: Nat
29  for done: Bool
30  for +decided: {done == Nat.is_le(length, capacity) : Bool}
31  for +sized: {capacity == Model.capacity(depth) : Nat}
32  for +left: {Nat.add(fuel, depth) == 20n : Nat}
33  for +limit: {Nat.is_le(length, Model.capacity(20n)) == True{} : Bool}
34  for +positive: {Nat.is_lt(0n, length) == True{} : Bool}
35  {Storage.bounds(Pair.fst(Nat, Nat, Storage.depth_seek(fuel, length, depth, capacity, done)), length) == True{} : Bool}