1	import Base
2	import ../shape/core.bend as Shape
3	import ../shape/nat_proofs.bend as Nats
4	import ../storage/main.bend as Storage
5	import ../storage/model.bend as Model
6	import ../storage/api.bend as Api
7	import ../storage/PROOF.bend as StorageProof
8	import ../storage/arith.bend as Arith
9	import ./core.bend as Core
10	import ./lifecycle.bend as Lifecycle
11	import ./allocation_spec.bend as Allocation
12	import ./allocation_LAWS.bend as Laws
13	import ./word_conversion.bend as Conversion
14	import ./word_conversion_PROOF.bend as ConversionProof
15	
16	def allocate_length(+depth: Nat, +length: Nat, +fill: F32, valid: Bool,
17	  -decision: {valid == Storage.bounds(depth, length) : Bool}, accepted: {valid == True{} : Bool}) ->
18	  {Allocation.storage_length(Storage.allocate(depth, length, fill, valid, decision)) == Some{length} : Maybe<&2, Nat>}:
19	  match valid:
20	    case False{}:
21	      Empty.absurd({None{} == Some{length} : Maybe<&2, Nat>}, Arith.clash(accepted))
22	    case True{}:
23	      {==}
24	
25	def allocate_at_length(+length: Nat, +fill: F32, metadata: Nat & Nat,
26	  valid: {Storage.bounds(Pair.fst(Nat, Nat, metadata), length) == True{} : Bool}) ->
27	  {Allocation.storage_length(Storage.allocate_at(length, fill, metadata)) == Some{length} : Maybe<&2, Nat>}:
28	  (+depth, capacity) = metadata
29	  allocate_length(depth, length, fill, Storage.bounds(depth, length), {==}, valid)
30	
31	def new_checked_length(+length: Nat, +fill: F32, allowed: Bool, accepted: {allowed == True{} : Bool},
32	  limit: {Nat.is_le(length, Model.capacity(20n)) == True{} : Bool}) ->
33	  {Allocation.storage_length(Storage.new_checked(length, fill, allowed)) == Some{length} : Maybe<&2, Nat>}:
34	  match length allowed:
35	    case 0n False{}:
36	      {==}
37	    case 0n True{}:
38	      {==}
39	    case 1n+p False{}:
40	      Empty.absurd({None{} == Some{1n+p} : Maybe<&2, Nat>}, Arith.clash(accepted))
41	    case 1n+p True{}:
42	      allocate_at_length(1n+p, fill, Storage.depth_seek(20n, 1n+p, 0n, 1n, Nat.is_le(1n+p, 1n)), Api.seek(1n+p, limit, {==}))
43	
44	def storage_new(+word: U32, +fill: F32, +within: {U32.is_le(word, 1048576) == True{} : Bool}) ->
45	  {Allocation.storage_length(Storage.new(word, fill)) == Some{U32.to_nat(word)} : Maybe<&2, Nat>}:
46	  new_checked_length(U32.to_nat(word), fill, U32.is_le(word, 1048576), within, Api.cap_from(word, within))
47	
48	def storage_zero(+fill: F32) -> {Storage.new(0, fill) == Done{Storage.Empty{}} : Result<&2, &1, Storage.Error, Storage.Storage>}:
49	  {==}
50	
51	def natural_equal_true(+a: Nat, +b: Nat, equal: {a == b : Nat}) -> {True{} == Nat.is_eq(a, b) : Bool}:
52	  Equal.sym(Bool, Nat.is_eq(a, b), True{},
53	    Equal.trans(Bool, Nat.is_eq(a, b), Nat.is_eq(b, b), True{},
54	      Equal.cong(Nat, Bool, n => Nat.is_eq(n, b), a, b, equal), Arith.eq_refl(b)))
55	
56	def attach_decided_length(+shape: Shape.Shape, +length: Nat, decision: Shape.BoolCase<Nat.is_eq(length, Shape.elements(shape))>,
57	  storage: Storage.Storage, exact: {Lifecycle.logical_length(storage) == length : Nat}, accepted: {True{} == Nat.is_eq(length, Shape.elements(shape)) : Bool}) ->
58	  {Allocation.tensor_length(shape, Core.attach_decided(shape, storage, length, exact, decision)) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}:
59	  match decision:
60	    case Shape.BFalse{equal}:
61	      Empty.absurd({None{} == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}, Nats.contradiction(Nat.is_eq(length, Shape.elements(shape)), accepted, equal))
62	    case Shape.BTrue{equal}:
63	      Equal.cong(Nat, Maybe<&2, Nat>, n => Some{n}, Lifecycle.logical_length(storage), Shape.logical_numel(Shape.dimensions(shape)),
64	        Equal.trans(Nat, Lifecycle.logical_length(storage), length, Shape.logical_numel(Shape.dimensions(shape)), exact,
65	          Equal.trans(Nat, length, Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)), Lifecycle.natural_equal(length, Shape.elements(shape), equal), Shape.elements_exact(shape))))
66	
67	def attach_length(+shape: Shape.Shape, storage: Storage.Storage, exact: {Lifecycle.logical_length(storage) == Shape.elements(shape) : Nat}) ->
68	  {Allocation.tensor_length(shape, Core.attach(shape, storage)) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}:
69	  match storage:
70	    case Storage.Empty{}:
71	      attach_decided_length(shape, 0n, Shape.bool_case(Nat.is_eq(0n, Shape.elements(shape))), Storage.Empty{}, {==}, natural_equal_true(0n, Shape.elements(shape), exact))
72	    case Storage.Owned{+depth, +length, array, balanced, valid}:
73	      attach_decided_length(shape, length, Shape.bool_case(Nat.is_eq(length, Shape.elements(shape))), Storage.Owned{depth, length, array, balanced, valid}, {==}, natural_equal_true(length, Shape.elements(shape), exact))
74	
75	def new_result_length(+shape: Shape.Shape, result: Result<&2, &1, Storage.Error, Storage.Storage>,
76	  exact: {Allocation.storage_length(result) == Some{Shape.elements(shape)} : Maybe<&2, Nat>}) ->
77	  {Allocation.tensor_length(shape, Core.new_result(shape, result)) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}:
78	  match result:
79	    case Fail{error}:
80	      Empty.absurd({None{} == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>},
81	        Arith.clash(Equal.cong(Maybe<&2, Nat>, Bool, value => Maybe.is_some(&2, Nat, value), None{}, Some{Shape.elements(shape)}, exact)))
82	    case Done{storage}:
83	      attach_length(shape, storage,
84	        Equal.cong(Maybe<&2, Nat>, Nat, value => Maybe.default(&2, Nat, value, 0n), Some{Lifecycle.logical_length(storage)}, Some{Shape.elements(shape)}, exact))
85	
86	def tensor_done(+shape: Shape.Shape, result: Result<&2, &1, Core.Error, Core.Tensor<shape>>,
87	  exact: {Allocation.tensor_length(shape, result) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}) -> Allocation.TensorDone<shape, result>:
88	  match result:
89	    case Fail{error}:
90	      Empty.absurd(Allocation.TensorDone<shape, Fail{error}>,
91	        Arith.clash(Equal.cong(Maybe<&2, Nat>, Bool, value => Maybe.is_some(&2, Nat, value), None{}, Some{Shape.logical_numel(Shape.dimensions(shape))}, exact)))
92	    case Done{tensor}:
93	      Allocation.TensorDone{tensor, {==}}
94	
95	def core_new(+shape: Shape.Shape, +fill: F32) ->
96	  {Allocation.tensor_length(shape, Core.new(shape, fill)) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}:
97	  new_result_length(shape, Storage.new(Shape.count(shape), fill),
98	    Equal.trans(Maybe<&2, Nat>, Allocation.storage_length(Storage.new(Shape.count(shape), fill)), Some{U32.to_nat(Shape.count(shape))}, Some{Shape.elements(shape)},
99	      storage_new(Shape.count(shape), fill, Conversion.shape_count_within(shape)),
100	      Equal.cong(Nat, Maybe<&2, Nat>, n => Some{n}, U32.to_nat(Shape.count(shape)), Shape.elements(shape), Conversion.shape_count_exact(shape))))
101	
102	def core_new_done(+shape: Shape.Shape, +fill: F32) -> Allocation.TensorDone<shape, Core.new(shape, fill)>:
103	  tensor_done(shape, Core.new(shape, fill), core_new(shape, fill))
104	
105	def Laws.storage_new_complete(word, fill, within):
106	  storage_new(word, fill, within)
107	
108	def Laws.storage_new_zero(fill):
109	  storage_zero(fill)
110	
111	def Laws.storage_new_depth_bounds(word, within, positive):
112	  Api.seek(U32.to_nat(word), Api.cap_from(word, within),
113	    Equal.trans(Bool, Nat.is_lt(0n, U32.to_nat(word)), U32.is_lt(0, word), True{}, Arith.u32_lt(0, word), positive))
114	
115	def Laws.storage_seek_bounds(fuel, length, depth, capacity, done, decided, sized, left, limit, positive):
116	  Api.seek_bounds(fuel, length, depth, capacity, done, decided, sized, left, limit, positive)
117	
118	def Laws.core_new_complete(shape, fill):
119	  core_new(shape, fill)
120	
121	def Laws.core_new_done(shape, fill):
122	  core_new_done(shape, fill)