src/tensor/allocation_LAWS.bend

bendtorch-core@0.1.0.0 · 45 lines · 6 definitions

1import Base
2import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
3import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
4import bendtorch-core@0.1.0.0/src/tensor/allocation_spec.bend as Allocation
5import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
6import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
7
8law storage_new_complete:
9  for +word: U32
10  for +fill: F32
11  for +within: {U32.is_le(word, 1048576) == True{} : Bool}
12  {Allocation.storage_length(Storage.new(word, fill)) == Some{U32.to_nat(word)} : Maybe<&2, Nat>}
13
14law storage_new_zero:
15  for +fill: F32
16  {Storage.new(0, fill) == Done{Storage.Empty{}} : Result<&2, &1, Storage.Error, Storage.Storage>}
17
18law storage_new_depth_bounds:
19  for +word: U32
20  for +within: {U32.is_le(word, 1048576) == True{} : Bool}
21  for positive: {U32.is_lt(0, word) == True{} : Bool}
22  {Storage.bounds(Pair.fst(Nat, Nat, Storage.depth_seek(20n, U32.to_nat(word), 0n, 1n, Nat.is_le(U32.to_nat(word), 1n))), U32.to_nat(word)) == True{} : Bool}
23
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}
36
37law core_new_complete:
38  for +shape: Shape.Shape
39  for +fill: F32
40  {Allocation.tensor_length(shape, Core.new(shape, fill)) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}
41
42law core_new_done:
43  for +shape: Shape.Shape
44  for +fill: F32
45  Allocation.TensorDone<shape, Core.new(shape, fill)>