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/LAWS.bend as StorageLaws
6	import ../storage/PROOF.bend as StorageProof
7	import ../storage/arith.bend as Arith
8	import ./core.bend as Core
9	import ./lifecycle.bend as Lifecycle
10	import ./allocation_spec.bend as Allocation
11	import ./allocation_PROOF.bend as AllocationProof
12	import ./word_conversion.bend as Conversion
13	import ./observation.bend as Observation
14	import ./read_write_records.bend as Laws
15	import ./read_contract.bend as Reads
16	
17	def write_value_projection(-shape: Shape.Shape, -original: Storage.Storage,
18	  -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +value: F32, +other: U32,
19	  pair: Storage.Storage & Result<&2, &2, Storage.Error, Unit>, -same: {pair == Storage.set(original, index, value) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>}) ->
20	  {Observation.written_value_pair(shape, other, Core.write_result(shape, original, valid, index, value, pair, same)) ==
21	    Lifecycle.read_value(Storage.get(StorageLaws.owner(Result<&2, &2, Storage.Error, Unit>, pair), other)) : Maybe<&2, F32>}:
22	  (storage, result) = pair
23	  Core.read_result_value(shape, storage,
24	    Equal.trans(Nat, Lifecycle.logical_length(storage), Lifecycle.logical_length(original), Shape.logical_numel(Shape.dimensions(shape)),
25	      %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>, (storage, result), Storage.set(original, index, value), same) :
26	        {Lifecycle.retained_write(_) == Lifecycle.logical_length(original) : Nat}
27	      Lifecycle.set_length(original, index, value), valid),
28	    other, Storage.get(storage, other), {==})
29	
30	def written_pick(+shape: Shape.Shape, +index: U32, +value: F32, +other: U32, +fill: F32) -> F32:
31	  Bool.pick(F32, Bool.and(Nat.is_lt(U32.to_nat(index), U32.to_nat(Shape.count(shape))), Nat.is_eq(U32.to_nat(index), U32.to_nat(other))), value, fill)
32	
33	def write_value_done(+shape: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +value: F32, +other: U32, inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
34	  {Observation.written_value(shape, index, value, other, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{written_pick(shape, index, value, other, fill)} : Maybe<&2, F32>}:
35	  Equal.trans(Maybe<&2, F32>,
36	    Observation.written_value_pair(shape, other, Core.write_result(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, value, Storage.set(StorageLaws.created(Shape.count(shape), fill), index, value), {==})),
37	    Lifecycle.read_value(Storage.get(StorageLaws.written(StorageLaws.created(Shape.count(shape), fill), index, value), other)), Some{written_pick(shape, index, value, other, fill)},
38	    write_value_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, value, other, Storage.set(StorageLaws.created(Shape.count(shape), fill), index, value), {==}),
39	    Reads.stored_value(StorageLaws.written(StorageLaws.created(Shape.count(shape), fill), index, value), other, written_pick(shape, index, value, other, fill),
40	      StorageLaws.replay_get(Shape.count(shape), fill, [StorageLaws.Write{index, value}], other, Conversion.shape_count_within(shape), Reads.word_inside(shape, other, inside))))
41	
42	def write_code_projection(-shape: Shape.Shape, -original: Storage.Storage,
43	  -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +value: F32,
44	  pair: Storage.Storage & Result<&2, &2, Storage.Error, Unit>, -same: {pair == Storage.set(original, index, value) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>}) ->
45	  {Observation.write_code_pair(shape, Core.write_result(shape, original, valid, index, value, pair, same)) ==
46	    Observation.write_status(Core.storage_write_error(StorageLaws.outcome(Result<&2, &2, Storage.Error, Unit>, pair))) : U32}:
47	  (storage, result) = pair
48	  {==}
49	
50	def write_code_done(+shape: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +value: F32, -expected: Result<&2, &2, Storage.Error, Unit>,
51	  status: {StorageLaws.status(StorageLaws.created(Shape.count(shape), fill), index, value) == expected : Result<&2, &2, Storage.Error, Unit>}) ->
52	  {Observation.write_code(shape, index, value, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{Observation.write_status(Core.storage_write_error(expected))} : Maybe<&2, U32>}:
53	  Equal.cong(U32, Maybe<&2, U32>, code => Some{code},
54	    Observation.write_code_pair(shape, Core.write_result(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, value, Storage.set(StorageLaws.created(Shape.count(shape), fill), index, value), {==})),
55	    Observation.write_status(Core.storage_write_error(expected)),
56	    Equal.trans(U32, Observation.write_code_pair(shape, Core.write_result(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, value, Storage.set(StorageLaws.created(Shape.count(shape), fill), index, value), {==})),
57	      Observation.write_status(Core.storage_write_error(StorageLaws.status(StorageLaws.created(Shape.count(shape), fill), index, value))), Observation.write_status(Core.storage_write_error(expected)),
58	      write_code_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, value, Storage.set(StorageLaws.created(Shape.count(shape), fill), index, value), {==}),
59	      Equal.cong(Result<&2, &2, Storage.Error, Unit>, U32, result => Observation.write_status(Core.storage_write_error(result)), StorageLaws.status(StorageLaws.created(Shape.count(shape), fill), index, value), expected, status)))
60	
61	def written_dimensions_pair(+shape: Shape.Shape, pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>) ->
62	  {Observation.written_dimensions_pair(shape, pair) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>}:
63	  (tensor, result) = pair
64	  {==}
65	
66	def written_count_pair(+shape: Shape.Shape, pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>) ->
67	  {Observation.written_count_pair(shape, pair) == Some{Shape.count(shape)} : Maybe<&2, U32>}:
68	  (tensor, result) = pair
69	  {==}
70	
71	def write_length_projection(-shape: Shape.Shape, -original: Storage.Storage,
72	  -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +value: F32,
73	  pair: Storage.Storage & Result<&2, &2, Storage.Error, Unit>, -same: {pair == Storage.set(original, index, value) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>}) ->
74	  {Observation.written_length_pair(shape, Core.write_result(shape, original, valid, index, value, pair, same)) == Lifecycle.retained_write(pair) : Nat}:
75	  (storage, result) = pair
76	  {==}
77	
78	def write_length_done(+shape: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +value: F32) ->
79	  {Observation.written_length(shape, index, value, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}:
80	  Equal.cong(Nat, Maybe<&2, Nat>, number => Some{number},
81	    Observation.written_length_pair(shape, Core.write_result(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, value, Storage.set(StorageLaws.created(Shape.count(shape), fill), index, value), {==})), Shape.logical_numel(Shape.dimensions(shape)),
82	    Equal.trans(Nat, Observation.written_length_pair(shape, Core.write_result(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, value, Storage.set(StorageLaws.created(Shape.count(shape), fill), index, value), {==})),
83	      Lifecycle.retained_write(Storage.set(StorageLaws.created(Shape.count(shape), fill), index, value)), Shape.logical_numel(Shape.dimensions(shape)),
84	      write_length_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, value, Storage.set(StorageLaws.created(Shape.count(shape), fill), index, value), {==}),
85	      Equal.trans(Nat, Lifecycle.retained_write(Storage.set(StorageLaws.created(Shape.count(shape), fill), index, value)), Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)), Shape.logical_numel(Shape.dimensions(shape)),
86	        Lifecycle.set_length(StorageLaws.created(Shape.count(shape), fill), index, value), Reads.created_exact(shape, fill))))
87	
88	def pick_hit(+shape: Shape.Shape, +index: U32, +value: F32, +fill: F32, inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
89	  {written_pick(shape, index, value, index, fill) == value : F32}:
90	  %Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), U32.to_nat(Shape.count(shape))), True{}, Reads.word_inside(shape, index, inside)) :
91	    {Bool.pick(F32, Bool.and(_, Nat.is_eq(U32.to_nat(index), U32.to_nat(index))), value, fill) == value : F32}
92	  %Equal.sym(Bool, Nat.is_eq(U32.to_nat(index), U32.to_nat(index)), True{}, Arith.eq_refl(U32.to_nat(index))) :
93	    {Bool.pick(F32, _, value, fill) == value : F32}
94	  {==}
95	
96	def pick_frame(+shape: Shape.Shape, +index: U32, +value: F32, +other: U32, +fill: F32, inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
97	  different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool}) ->
98	  {written_pick(shape, index, value, other, fill) == fill : F32}:
99	  %Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), U32.to_nat(Shape.count(shape))), True{}, Reads.word_inside(shape, index, inside)) :
100	    {Bool.pick(F32, Bool.and(_, Nat.is_eq(U32.to_nat(index), U32.to_nat(other))), value, fill) == fill : F32}
101	  %Equal.sym(Bool, Nat.is_eq(U32.to_nat(index), U32.to_nat(other)), False{}, different) :
102	    {Bool.pick(F32, _, value, fill) == fill : F32}
103	  {==}
104	
105	def pick_outside(+shape: Shape.Shape, +index: U32, +value: F32, +other: U32, +fill: F32, outside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == False{} : Bool}) ->
106	  {written_pick(shape, index, value, other, fill) == fill : F32}:
107	  %Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), U32.to_nat(Shape.count(shape))), False{}, Reads.word_outside(shape, index, outside)) :
108	    {Bool.pick(F32, Bool.and(_, Nat.is_eq(U32.to_nat(index), U32.to_nat(other))), value, fill) == fill : F32}
109	  {==}
110	
111	def written_value(+shape: Shape.Shape, +fill: F32, +index: U32, +value: F32, +other: U32, -expected: F32,
112	  inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}, picked: {written_pick(shape, index, value, other, fill) == expected : F32}) ->
113	  {Observation.written_value(shape, index, value, other, Core.new(shape, fill)) == Some{expected} : Maybe<&2, F32>}:
114	  Reads.new_lift(shape, fill, result => {Observation.written_value(shape, index, value, other, result) == Some{expected} : Maybe<&2, F32>},
115	    valid => Equal.trans(Maybe<&2, F32>, Observation.written_value(shape, index, value, other, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}),
116	      Some{written_pick(shape, index, value, other, fill)}, Some{expected},
117	      write_value_done(shape, fill, valid, index, value, other, inside),
118	      Equal.cong(F32, Maybe<&2, F32>, number => Some{number}, written_pick(shape, index, value, other, fill), expected, picked)))
119	
120	def write_contract(+shape: Shape.Shape, +fill: F32, +index: U32, +value: F32, -expected: Result<&2, &2, Storage.Error, Unit>,
121	  status: {StorageLaws.status(StorageLaws.created(Shape.count(shape), fill), index, value) == expected : Result<&2, &2, Storage.Error, Unit>}) ->
122	  Laws.WriteContract<shape, fill, index, value, Observation.write_status(Core.storage_write_error(expected))>:
123	  Laws.WriteContract{
124	    Reads.new_lift(shape, fill, result => {Observation.write_code(shape, index, value, result) == Some{Observation.write_status(Core.storage_write_error(expected))} : Maybe<&2, U32>},
125	      valid => write_code_done(shape, fill, valid, index, value, expected, status)),
126	    Reads.new_lift(shape, fill, result => {Observation.written_dimensions(shape, index, value, result) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>},
127	      valid => written_dimensions_pair(shape, Core.write_flat(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}, index, value))),
128	    Reads.new_lift(shape, fill, result => {Observation.written_length(shape, index, value, result) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>},
129	      valid => write_length_done(shape, fill, valid, index, value)),
130	    Reads.new_lift(shape, fill, result => {Observation.written_count(shape, index, value, result) == Some{Shape.count(shape)} : Maybe<&2, U32>},
131	      valid => written_count_pair(shape, Core.write_flat(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}, index, value)))}
132	
133	def located_index(-shape: Shape.Shape, +index: Shape.FlatIndex<shape>, +expected: U32,
134	  located: {Observation.coordinate_index(shape, Done{index}) == Some{expected} : Maybe<&2, U32>}) ->
135	  {Shape.index_value(shape, index) == expected : U32}:
136	  Equal.cong(Maybe<&2, U32>, U32, word => Maybe.default(&2, U32, word, 0), Some{Shape.index_value(shape, index)}, Some{expected}, located)
137	
138	def coordinate_read_flat(+shape: Shape.Shape, -tensor: Core.Tensor<shape>, result: Result<&2, &2, Shape.Error, Shape.FlatIndex<shape>>,
139	  +index: U32, located: {Observation.coordinate_index(shape, result) == Some{index} : Maybe<&2, U32>}) ->
140	  {Core.read_coordinate_result(shape, tensor, result) == Core.read_flat(shape, tensor, index) : Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>}:
141	  match result:
142	    case Fail{error}:
143	      Empty.absurd({(tensor, Fail{Core.ShapeError{error}}) == Core.read_flat(shape, tensor, index) : Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>},
144	        Arith.clash(Equal.cong(Maybe<&2, U32>, Bool, word => Maybe.is_some(&2, U32, word), None{}, Some{index}, located)))
145	    case Done{+flat}:
146	      Equal.cong(U32, Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, word => Core.read_flat(shape, tensor, word),
147	        Shape.index_value(shape, flat), index, located_index(shape, flat, index, located))
148	
149	def coordinate_write_flat(+shape: Shape.Shape, -tensor: Core.Tensor<shape>, -value: F32,
150	  result: Result<&2, &2, Shape.Error, Shape.FlatIndex<shape>>,
151	  +index: U32, located: {Observation.coordinate_index(shape, result) == Some{index} : Maybe<&2, U32>}) ->
152	  {Core.write_coordinate_result(shape, tensor, value, result) == Core.write_flat(shape, tensor, index, value) : Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>}:
153	  match result:
154	    case Fail{error}:
155	      Empty.absurd({(tensor, Fail{Core.ShapeError{error}}) == Core.write_flat(shape, tensor, index, value) : Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>},
156	        Arith.clash(Equal.cong(Maybe<&2, U32>, Bool, word => Maybe.is_some(&2, U32, word), None{}, Some{index}, located)))
157	    case Done{+flat}:
158	      Equal.cong(U32, Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>, word => Core.write_flat(shape, tensor, word, value),
159	        Shape.index_value(shape, flat), index, located_index(shape, flat, index, located))
160	
161	def coordinate_value_pair(+shape: Shape.Shape, +coordinates: List<&2, U32>, +index: U32,
162	  located: {Observation.coordinate_index(shape, Shape.flatten_checked(shape, coordinates)) == Some{index} : Maybe<&2, U32>},
163	  pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>) ->
164	  {Observation.coordinate_value_pair(shape, coordinates, pair) == Observation.written_value_pair(shape, index, pair) : Maybe<&2, F32>}:
165	  (tensor, result) = pair
166	  Equal.cong(Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, Maybe<&2, F32>, read => Core.read_value(shape, read),
167	    Core.read_coordinate(shape, tensor, coordinates), Core.read_flat(shape, tensor, index),
168	    coordinate_read_flat(shape, tensor, Shape.flatten_checked(shape, coordinates), index, located))
169	
170	def coordinate_value_result(+shape: Shape.Shape, +coordinates: List<&2, U32>, +index: U32, +value: F32,
171	  located: {Observation.coordinate_index(shape, Shape.flatten_checked(shape, coordinates)) == Some{index} : Maybe<&2, U32>},
172	  result: Result<&2, &1, Core.Error, Core.Tensor<shape>>) ->
173	  {Observation.coordinate_value(shape, index, value, coordinates, result) == Observation.written_value(shape, index, value, index, result) : Maybe<&2, F32>}:
174	  match result:
175	    case Fail{error}:
176	      {==}
177	    case Done{tensor}:
178	      coordinate_value_pair(shape, coordinates, index, located, Core.write_flat(shape, tensor, index, value))
179	
180	def coordinate_written_result(+shape: Shape.Shape, +coordinates: List<&2, U32>, +index: U32, +value: F32, +other: U32,
181	  located: {Observation.coordinate_index(shape, Shape.flatten_checked(shape, coordinates)) == Some{index} : Maybe<&2, U32>},
182	  result: Result<&2, &1, Core.Error, Core.Tensor<shape>>) ->
183	  {Observation.coordinate_written(shape, coordinates, value, other, result) == Observation.written_value(shape, index, value, other, result) : Maybe<&2, F32>}:
184	  match result:
185	    case Fail{error}:
186	      {==}
187	    case Done{tensor}:
188	      Equal.cong(Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>, Maybe<&2, F32>, pair => Observation.written_value_pair(shape, other, pair),
189	        Core.write_coordinate(shape, tensor, coordinates, value), Core.write_flat(shape, tensor, index, value),
190	        coordinate_write_flat(shape, tensor, value, Shape.flatten_checked(shape, coordinates), index, located))
191	
192	def write_inside(+shape: Shape.Shape, +fill: F32, +index: U32, +value: F32,
193	  inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) -> Laws.WriteInside<shape, fill, index, value>:
194	  +inside = inside
195	  Laws.WriteInside{
196	    write_contract(shape, fill, index, value, Done{Unit{}},
197	      StorageLaws.replay_set(Shape.count(shape), fill, [], index, value, Conversion.shape_count_within(shape), Reads.word_inside(shape, index, inside))),
198	    written_value(shape, fill, index, value, index, value, inside, pick_hit(shape, index, value, fill, inside)),
199	    other => inside_other => different =>
200	      written_value(shape, fill, index, value, other, fill, inside_other, pick_frame(shape, index, value, other, fill, inside, different))}
201	
202	def write_outside(+shape: Shape.Shape, +fill: F32, +index: U32, +value: F32,
203	  outside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == False{} : Bool}) -> Laws.WriteOutside<shape, fill, index, value>:
204	  +outside = outside
205	  Laws.WriteOutside{
206	    write_contract(shape, fill, index, value, Fail{Storage.OutOfBounds{}},
207	      StorageLaws.set_outside(StorageLaws.created(Shape.count(shape), fill), index, value, Reads.size_outside(shape, fill, index, outside))),
208	    other => inside =>
209	      written_value(shape, fill, index, value, other, fill, inside, pick_outside(shape, index, value, other, fill, outside))}
210	
211	def coordinate_inside(+shape: Shape.Shape, +fill: F32, +coordinates: List<&2, U32>, +index: U32, +value: F32,
212	  located: {Observation.coordinate_index(shape, Shape.flatten_checked(shape, coordinates)) == Some{index} : Maybe<&2, U32>},
213	  inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
214	  Laws.CoordinateInside<shape, fill, coordinates, index, value>:
215	  +located = located
216	  +inside = inside
217	  Laws.CoordinateInside{
218	    Equal.trans(Maybe<&2, F32>, Observation.coordinate_value(shape, index, value, coordinates, Core.new(shape, fill)),
219	      Observation.written_value(shape, index, value, index, Core.new(shape, fill)), Some{value},
220	      coordinate_value_result(shape, coordinates, index, value, located, Core.new(shape, fill)),
221	      written_value(shape, fill, index, value, index, value, inside, pick_hit(shape, index, value, fill, inside))),
222	    Equal.trans(Maybe<&2, F32>, Observation.coordinate_written(shape, coordinates, value, index, Core.new(shape, fill)),
223	      Observation.written_value(shape, index, value, index, Core.new(shape, fill)), Some{value},
224	      coordinate_written_result(shape, coordinates, index, value, index, located, Core.new(shape, fill)),
225	      written_value(shape, fill, index, value, index, value, inside, pick_hit(shape, index, value, fill, inside))),
226	    other => inside_other => different =>
227	      Equal.trans(Maybe<&2, F32>, Observation.coordinate_written(shape, coordinates, value, other, Core.new(shape, fill)),
228	        Observation.written_value(shape, index, value, other, Core.new(shape, fill)), Some{fill},
229	        coordinate_written_result(shape, coordinates, index, value, other, located, Core.new(shape, fill)),
230	        written_value(shape, fill, index, value, other, fill, inside_other, pick_frame(shape, index, value, other, fill, inside, different)))}