1	import Base
2	import ../storage/main.bend as Storage
3	import ../storage/model.bend as Model
4	import ./allocation_spec.bend as Allocation
5	import ./core.bend as Core
6	import ../shape/core.bend as Shape
7	
8	law 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	
14	law storage_new_zero:
15	  for +fill: F32
16	  {Storage.new(0, fill) == Done{Storage.Empty{}} : Result<&2, &1, Storage.Error, Storage.Storage>}
17	
18	law 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	
24	law 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	
37	law 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	
42	law core_new_done:
43	  for +shape: Shape.Shape
44	  for +fill: F32
45	  Allocation.TensorDone<shape, Core.new(shape, fill)>