1	import Base
2	import ../shape/core.bend as Shape
3	import ../storage/main.bend as Storage
4	import ../storage/LAWS.bend as StorageLaws
5	import ../storage/PROOF.bend as StorageProof
6	import ./core.bend as Core
7	import ./lifecycle.bend as Lifecycle
8	import ./word_conversion.bend as Conversion
9	import ./observation.bend as Observation
10	import ./read_contract.bend as Reads
11	import ./write_contract.bend as Writes
12	import ./clone_metadata_records.bend as Laws
13	
14	def first_value_projection(-shape: Shape.Shape, -original: Storage.Storage, -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +other: U32,
15	  pair: Storage.Storage & Storage.Storage, -same: {pair == Storage.clone(original) : Storage.Storage & Storage.Storage}) ->
16	  {Observation.clone_first_value_pair(shape, other, Core.clone_result(shape, original, valid, pair, same)) ==
17	    Lifecycle.read_value(Storage.get(StorageLaws.owner(Storage.Storage, pair), other)) : Maybe<&2, F32>}:
18	  (first, second) = pair
19	  Core.read_result_value(shape, first,
20	    Equal.trans(Nat, Lifecycle.logical_length(first), Lifecycle.logical_length(original), Shape.logical_numel(Shape.dimensions(shape)),
21	      %Equal.sym(Storage.Storage & Storage.Storage, (first, second), Storage.clone(original), same) :
22	        {Lifecycle.first_length(_) == Lifecycle.logical_length(original) : Nat}
23	      Lifecycle.clone_first_length(original), valid),
24	    other, Storage.get(first, other), {==})
25	
26	def untouched_value(-shape: Shape.Shape, +other: U32, written: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>,
27	  storage: Storage.Storage, -valid: {Lifecycle.logical_length(storage) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
28	  {Observation.untouched(shape, other, written, Core.TTensor{storage, valid}) == Lifecycle.read_value(Storage.get(storage, other)) : Maybe<&2, F32>}:
29	  (tensor, result) = written
30	  Core.read_result_value(shape, storage, valid, other, Storage.get(storage, other), {==})
31	
32	def second_value_projection(-shape: Shape.Shape, -original: Storage.Storage, -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +other: U32,
33	  pair: Storage.Storage & Storage.Storage, -same: {pair == Storage.clone(original) : Storage.Storage & Storage.Storage}) ->
34	  {Observation.clone_second_value_pair(shape, other, Core.clone_result(shape, original, valid, pair, same)) ==
35	    Lifecycle.read_value(Storage.get(StorageLaws.outcome(Storage.Storage, pair), other)) : Maybe<&2, F32>}:
36	  (first, second) = pair
37	  Core.read_result_value(shape, second,
38	    Equal.trans(Nat, Lifecycle.logical_length(second), Lifecycle.logical_length(original), Shape.logical_numel(Shape.dimensions(shape)),
39	      %Equal.sym(Storage.Storage & Storage.Storage, (first, second), Storage.clone(original), same) :
40	        {Lifecycle.second_length(_) == Lifecycle.logical_length(original) : Nat}
41	      Lifecycle.clone_second_length(original), valid),
42	    other, Storage.get(second, other), {==})
43	
44	def first_written_projection(-shape: Shape.Shape, -original: Storage.Storage, -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +value: F32, +other: U32,
45	  pair: Storage.Storage & Storage.Storage, -same: {pair == Storage.clone(original) : Storage.Storage & Storage.Storage}) ->
46	  {Observation.clone_written_first_pair(shape, index, value, other, Core.clone_result(shape, original, valid, pair, same)) ==
47	    Lifecycle.read_value(Storage.get(StorageLaws.written(StorageLaws.owner(Storage.Storage, pair), index, value), other)) : Maybe<&2, F32>}:
48	  (first, second) = pair
49	  Writes.write_value_projection(shape, first,
50	    Equal.trans(Nat, Lifecycle.logical_length(first), Lifecycle.logical_length(original), Shape.logical_numel(Shape.dimensions(shape)),
51	      %Equal.sym(Storage.Storage & Storage.Storage, (first, second), Storage.clone(original), same) :
52	        {Lifecycle.first_length(_) == Lifecycle.logical_length(original) : Nat}
53	      Lifecycle.clone_first_length(original), valid),
54	    index, value, other, Storage.set(first, index, value), {==})
55	
56	def second_written_projection(-shape: Shape.Shape, -original: Storage.Storage, -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +value: F32, +other: U32,
57	  pair: Storage.Storage & Storage.Storage, -same: {pair == Storage.clone(original) : Storage.Storage & Storage.Storage}) ->
58	  {Observation.clone_written_second_pair(shape, index, value, other, Core.clone_result(shape, original, valid, pair, same)) ==
59	    Lifecycle.read_value(Storage.get(StorageLaws.outcome(Storage.Storage, pair), other)) : Maybe<&2, F32>}:
60	  (first, second) = pair
61	  untouched_value(shape, other, Core.write_flat(shape, Core.TTensor{first, Equal.trans(Nat, Lifecycle.logical_length(first), Lifecycle.logical_length(original), Shape.logical_numel(Shape.dimensions(shape)),
62	      %Equal.sym(Storage.Storage & Storage.Storage, (first, second), Storage.clone(original), same) :
63	        {Lifecycle.first_length(_) == Lifecycle.logical_length(original) : Nat}
64	      Lifecycle.clone_first_length(original), valid)}, index, value), second,
65	    Equal.trans(Nat, Lifecycle.logical_length(second), Lifecycle.logical_length(original), Shape.logical_numel(Shape.dimensions(shape)),
66	      %Equal.sym(Storage.Storage & Storage.Storage, (first, second), Storage.clone(original), same) :
67	        {Lifecycle.second_length(_) == Lifecycle.logical_length(original) : Nat}
68	      Lifecycle.clone_second_length(original), valid))
69	
70	def first_length_projection(-shape: Shape.Shape, -original: Storage.Storage, -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, pair: Storage.Storage & Storage.Storage, -same: {pair == Storage.clone(original) : Storage.Storage & Storage.Storage}) ->
71	  {Observation.clone_first_length_pair(shape, Core.clone_result(shape, original, valid, pair, same)) == Lifecycle.first_length(pair) : Nat}:
72	  (first, second) = pair
73	  {==}
74	
75	def second_length_projection(-shape: Shape.Shape, -original: Storage.Storage, -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, pair: Storage.Storage & Storage.Storage, -same: {pair == Storage.clone(original) : Storage.Storage & Storage.Storage}) ->
76	  {Observation.clone_second_length_pair(shape, Core.clone_result(shape, original, valid, pair, same)) == Lifecycle.second_length(pair) : Nat}:
77	  (first, second) = pair
78	  {==}
79	
80	def first_dimensions_pair(+shape: Shape.Shape, pair: Core.Tensor<shape> & Core.Tensor<shape>) ->
81	  {Observation.clone_first_dimensions_pair(shape, pair) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>}:
82	  (first, second) = pair
83	  {==}
84	
85	def second_dimensions_pair(+shape: Shape.Shape, pair: Core.Tensor<shape> & Core.Tensor<shape>) ->
86	  {Observation.clone_second_dimensions_pair(shape, pair) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>}:
87	  (first, second) = pair
88	  {==}
89	
90	def first_count_pair(+shape: Shape.Shape, pair: Core.Tensor<shape> & Core.Tensor<shape>) ->
91	  {Observation.clone_first_count_pair(shape, pair) == Some{Shape.count(shape)} : Maybe<&2, U32>}:
92	  (first, second) = pair
93	  {==}
94	
95	def second_count_pair(+shape: Shape.Shape, pair: Core.Tensor<shape> & Core.Tensor<shape>) ->
96	  {Observation.clone_second_count_pair(shape, pair) == Some{Shape.count(shape)} : Maybe<&2, U32>}:
97	  (first, second) = pair
98	  {==}
99	
100	def first_value_done(+shape: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +other: U32, inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
101	  {Observation.clone_first_value(shape, other, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{fill} : Maybe<&2, F32>}:
102	  Equal.trans(Maybe<&2, F32>, Observation.clone_first_value_pair(shape, other, Core.clone(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid})),
103	    Lifecycle.read_value(Storage.get(StorageLaws.first(StorageLaws.created(Shape.count(shape), fill)), other)), Some{fill},
104	    first_value_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, other, Storage.clone(StorageLaws.created(Shape.count(shape), fill)), {==}),
105	    Reads.stored_value(StorageLaws.first(StorageLaws.created(Shape.count(shape), fill)), other, fill,
106	      StorageLaws.replay_get(Shape.count(shape), fill, [StorageLaws.First{}], other, Conversion.shape_count_within(shape), Reads.word_inside(shape, other, inside))))
107	
108	def second_value_done(+shape: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +other: U32, inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
109	  {Observation.clone_second_value(shape, other, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{fill} : Maybe<&2, F32>}:
110	  Equal.trans(Maybe<&2, F32>, Observation.clone_second_value_pair(shape, other, Core.clone(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid})),
111	    Lifecycle.read_value(Storage.get(StorageLaws.second(StorageLaws.created(Shape.count(shape), fill)), other)), Some{fill},
112	    second_value_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, other, Storage.clone(StorageLaws.created(Shape.count(shape), fill)), {==}),
113	    Reads.stored_value(StorageLaws.second(StorageLaws.created(Shape.count(shape), fill)), other, fill,
114	      StorageLaws.replay_get(Shape.count(shape), fill, [StorageLaws.Second{}], other, Conversion.shape_count_within(shape), Reads.word_inside(shape, other, inside))))
115	
116	def first_written_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}) ->
117	  {Observation.clone_written_first(shape, index, value, other, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{Writes.written_pick(shape, index, value, other, fill)} : Maybe<&2, F32>}:
118	  Equal.trans(Maybe<&2, F32>, Observation.clone_written_first_pair(shape, index, value, other, Core.clone(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid})),
119	    Lifecycle.read_value(Storage.get(StorageLaws.written(StorageLaws.first(StorageLaws.created(Shape.count(shape), fill)), index, value), other)),
120	    Some{Writes.written_pick(shape, index, value, other, fill)},
121	    first_written_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, value, other, Storage.clone(StorageLaws.created(Shape.count(shape), fill)), {==}),
122	    Reads.stored_value(StorageLaws.written(StorageLaws.first(StorageLaws.created(Shape.count(shape), fill)), index, value), other, Writes.written_pick(shape, index, value, other, fill),
123	      StorageLaws.replay_get(Shape.count(shape), fill, [StorageLaws.First{}, StorageLaws.Write{index, value}], other, Conversion.shape_count_within(shape),
124	        Reads.word_inside(shape, other, inside))))
125	
126	def second_written_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}) ->
127	  {Observation.clone_written_second(shape, index, value, other, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{fill} : Maybe<&2, F32>}:
128	  Equal.trans(Maybe<&2, F32>, Observation.clone_written_second_pair(shape, index, value, other, Core.clone(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid})),
129	    Lifecycle.read_value(Storage.get(StorageLaws.second(StorageLaws.created(Shape.count(shape), fill)), other)), Some{fill},
130	    second_written_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, value, other, Storage.clone(StorageLaws.created(Shape.count(shape), fill)), {==}),
131	    Reads.stored_value(StorageLaws.second(StorageLaws.created(Shape.count(shape), fill)), other, fill,
132	      StorageLaws.replay_get(Shape.count(shape), fill, [StorageLaws.Second{}], other, Conversion.shape_count_within(shape), Reads.word_inside(shape, other, inside))))
133	
134	def first_length_done(+shape: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
135	  {Observation.clone_first_length(shape, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}:
136	  Equal.cong(Nat, Maybe<&2, Nat>, number => Some{number}, Observation.clone_first_length_pair(shape, Core.clone(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid})), Shape.logical_numel(Shape.dimensions(shape)),
137	    Equal.trans(Nat, Observation.clone_first_length_pair(shape, Core.clone(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid})), Lifecycle.first_length(Storage.clone(StorageLaws.created(Shape.count(shape), fill))), Shape.logical_numel(Shape.dimensions(shape)),
138	      first_length_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, Storage.clone(StorageLaws.created(Shape.count(shape), fill)), {==}),
139	      Equal.trans(Nat, Lifecycle.first_length(Storage.clone(StorageLaws.created(Shape.count(shape), fill))), Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)), Shape.logical_numel(Shape.dimensions(shape)),
140	        Lifecycle.clone_first_length(StorageLaws.created(Shape.count(shape), fill)), Reads.created_exact(shape, fill))))
141	
142	def second_length_done(+shape: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
143	  {Observation.clone_second_length(shape, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}:
144	  Equal.cong(Nat, Maybe<&2, Nat>, number => Some{number}, Observation.clone_second_length_pair(shape, Core.clone(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid})), Shape.logical_numel(Shape.dimensions(shape)),
145	    Equal.trans(Nat, Observation.clone_second_length_pair(shape, Core.clone(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid})), Lifecycle.second_length(Storage.clone(StorageLaws.created(Shape.count(shape), fill))), Shape.logical_numel(Shape.dimensions(shape)),
146	      second_length_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, Storage.clone(StorageLaws.created(Shape.count(shape), fill)), {==}),
147	      Equal.trans(Nat, Lifecycle.second_length(Storage.clone(StorageLaws.created(Shape.count(shape), fill))), Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)), Shape.logical_numel(Shape.dimensions(shape)),
148	        Lifecycle.clone_second_length(StorageLaws.created(Shape.count(shape), fill)), Reads.created_exact(shape, fill))))
149	
150	def clone_written(+shape: Shape.Shape, +fill: F32, +index: U32, +value: F32, +other: U32, -expected: F32,
151	  inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}, picked: {Writes.written_pick(shape, index, value, other, fill) == expected : F32}) ->
152	  {Observation.clone_written_first(shape, index, value, other, Core.new(shape, fill)) == Some{expected} : Maybe<&2, F32>}:
153	  Reads.new_lift(shape, fill, result => {Observation.clone_written_first(shape, index, value, other, result) == Some{expected} : Maybe<&2, F32>},
154	    valid => Equal.trans(Maybe<&2, F32>, Observation.clone_written_first(shape, index, value, other, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}),
155	      Some{Writes.written_pick(shape, index, value, other, fill)}, Some{expected},
156	      first_written_done(shape, fill, valid, index, value, other, inside),
157	      Equal.cong(F32, Maybe<&2, F32>, number => Some{number}, Writes.written_pick(shape, index, value, other, fill), expected, picked)))
158	
159	def clone_contract(+shape: Shape.Shape, +fill: F32) -> Laws.CloneContract<shape, fill>:
160	  Laws.CloneContract{
161	    Reads.new_lift(shape, fill, result => {Observation.clone_first_dimensions(shape, result) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>},
162	      valid => first_dimensions_pair(shape, Core.clone(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}))),
163	    Reads.new_lift(shape, fill, result => {Observation.clone_second_dimensions(shape, result) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>},
164	      valid => second_dimensions_pair(shape, Core.clone(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}))),
165	    Reads.new_lift(shape, fill, result => {Observation.clone_first_length(shape, result) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>},
166	      valid => first_length_done(shape, fill, valid)),
167	    Reads.new_lift(shape, fill, result => {Observation.clone_second_length(shape, result) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>},
168	      valid => second_length_done(shape, fill, valid)),
169	    Reads.new_lift(shape, fill, result => {Observation.clone_first_count(shape, result) == Some{Shape.count(shape)} : Maybe<&2, U32>},
170	      valid => first_count_pair(shape, Core.clone(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}))),
171	    Reads.new_lift(shape, fill, result => {Observation.clone_second_count(shape, result) == Some{Shape.count(shape)} : Maybe<&2, U32>},
172	      valid => second_count_pair(shape, Core.clone(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}))),
173	    other => inside => Reads.new_lift(shape, fill, result => {Observation.clone_first_value(shape, other, result) == Some{fill} : Maybe<&2, F32>},
174	      valid => first_value_done(shape, fill, valid, other, inside)),
175	    other => inside => Reads.new_lift(shape, fill, result => {Observation.clone_second_value(shape, other, result) == Some{fill} : Maybe<&2, F32>},
176	      valid => second_value_done(shape, fill, valid, other, inside))}
177	
178	def clone_write(+shape: Shape.Shape, +fill: F32, +index: U32, +value: F32,
179	  inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) -> Laws.CloneWrite<shape, fill, index, value>:
180	  +inside = inside
181	  Laws.CloneWrite{
182	    clone_written(shape, fill, index, value, index, value, inside, Writes.pick_hit(shape, index, value, fill, inside)),
183	    other => inside_other => different =>
184	      clone_written(shape, fill, index, value, other, fill, inside_other, Writes.pick_frame(shape, index, value, other, fill, inside, different)),
185	    other => inside_other => Reads.new_lift(shape, fill, result => {Observation.clone_written_second(shape, index, value, other, result) == Some{fill} : Maybe<&2, F32>},
186	      valid => second_written_done(shape, fill, valid, index, value, other, inside_other))}