src/autograd/gradient_PROOF.bend
bendtorch-core@0.1.0.0 · 898 lines · 63 definitions
1import Base
2
3import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
4
5import bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend as PlanProof
6
7import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
8
9import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
10
11import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
12
13import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
14
15import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
16
17import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as Totality
18
19import bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend as ElementwiseProof
20
21import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CoreProof
22
23import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformProof
24
25import bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend as TransformTotality
26
27import bendtorch-core@0.1.0.0/src/tensor/allocation_spec.bend as Allocation
28
29import bendtorch-core@0.1.0.0/src/tensor/allocation_PROOF.bend as AllocationProof
30
31import bendtorch-core@0.1.0.0/src/tensor/construction_contract_PROOF.bend as ConstructionProof
32
33import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
34
35import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Observation
36
37import bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend as ReduceProof
38
39import bendtorch-core@0.1.0.0/src/autograd/gradient.bend as Gradient
40
41import bendtorch-core@0.1.0.0/src/autograd/gradient_LAWS.bend as Laws
42
43type Holds<-P: Type> is Data:
44 Holds{-proof: P}
45
46def lt_self(+number: Nat) -> {Nat.is_lt(number, number) == False{} : Bool}:
47 match number:
48 case 0n:
49 {==}
50 case 1n+rest:
51 lt_self(rest)
52
53def lt_succ_self(+number: Nat) -> {Nat.is_lt(number, 1n+number) == True{} : Bool}:
54 match number:
55 case 0n:
56 {==}
57 case 1n+rest:
58 lt_succ_self(rest)
59
60def below_zero(+number: Nat) -> {Nat.is_lt(number, 0n) == False{} : Bool}:
61 match number:
62 case 0n:
63 {==}
64 case 1n+rest:
65 {==}
66
67def below_one_more(+rest: Nat) -> {Nat.is_lt(1n+rest, 0n) == Nat.is_lt(1n+rest, 1n) : Bool}:
68 match rest:
69 case 0n:
70 {==}
71 case 1n+deeper:
72 {==}
73
74def lt_step(+position: Nat, +cursor: Nat, different: {False{} == Nat.is_eq(cursor, position) : Bool}) ->
75 {Nat.is_lt(position, cursor) == Nat.is_lt(position, 1n+cursor) : Bool}:
76 match position cursor:
77 case 0n 0n:
78 Empty.absurd({Nat.is_lt(0n, 0n) == Nat.is_lt(0n, 1n) : Bool}, Arith.clash(different))
79 case 0n 1n+bound:
80 {==}
81 case 1n+rest 0n:
82 below_one_more(rest)
83 case 1n+rest 1n+bound:
84 lt_step(rest, bound, different)
85
86def words_dimensions(+left: Shape.Shape, +right: Shape.Shape,
87 -decided: {True{} == Layout.words_same(Shape.dimensions(left), Shape.dimensions(right)) : Bool}) ->
88 Holds<{Shape.dimensions(left) == Shape.dimensions(right) : List<&2, U32>}>:
89 Holds{TransformProof.words_equal(Shape.dimensions(left), Shape.dimensions(right), decided)}
90
91def same_checked(-original: Core.Dynamic, -retained: Core.Dynamic, -same: Totality.SameSource(original, retained), +index: U32) ->
92 Holds<{Core.checked_observe_dynamic(retained, index) == Core.checked_observe_dynamic(original, index) : Maybe<&2, F32>}>:
93 Holds{Equal.cong(Totality.Inspection, Maybe<&2, F32>, ReduceProof.inspection_value,
94 Totality.inspect(Totality.Checked{index}, retained), Totality.inspect(Totality.Checked{index}, original), same(Totality.Checked{index}))}
95
96def same_dimensions(-original: Core.Dynamic, -retained: Core.Dynamic, -same: Totality.SameSource(original, retained)) ->
97 Holds<{Totality.dimensions(retained) == Totality.dimensions(original) : List<&2, U32>}>:
98 Holds{Equal.cong(Totality.Inspection, List<&2, U32>, ElementwiseProof.inspection_dimensions,
99 Totality.inspect(Totality.Dimensions{}, retained), Totality.inspect(Totality.Dimensions{}, original), same(Totality.Dimensions{}))}
100
101def same_trans(-a: Core.Dynamic, -b: Core.Dynamic, -c: Core.Dynamic,
102 -ab: Totality.SameSource(a, b), -bc: Totality.SameSource(b, c)) -> Holds<Totality.SameSource(a, c)>:
103 Holds{property => Equal.trans(Totality.Inspection, Totality.inspect(property, c), Totality.inspect(property, b), Totality.inspect(property, a),
104 bc(property), ab(property))}
105
106def word_exact(+left: U32, +right: U32, equal: {True{} == Nat.is_eq(U32.to_nat(left), U32.to_nat(right)) : Bool}) -> Holds<{left == right : U32}>:
107 Holds{
108 %Conversion.word_natural_exact(left) : {_ == right : U32}
109 %Conversion.word_natural_exact(right) : {U32.from_nat(U32.to_nat(left)) == _ : U32}
110 Equal.cong(Nat, U32, U32.from_nat, U32.to_nat(left), U32.to_nat(right),
111 Lifecycle.natural_equal(U32.to_nat(left), U32.to_nat(right), equal))}
112
113def unset_zeros(+shape: Shape.Shape, result: Result<&2, &1, Core.Error, Core.Tensor<shape>>,
114 -same: {result == Core.new(shape, 0.0) : Result<&2, &1, Core.Error, Core.Tensor<shape>>},
115 -done: Allocation.TensorDone<shape, result>) ->
116 Laws.ZerosModel<shape, Core.construct_values(shape, result)>:
117 match result:
118 case Fail{error}:
119 Laws.ZerosModel{
120 {\{Allocation.TensorDone: tensor => equal => Arith.clash(Equal.cong(Result<&2, &1, Core.Error, Core.Tensor<shape>>, Bool,
121 found => Result.is_done(&2, &1, Core.Error, Core.Tensor<shape>, found), Fail{error}, Done{tensor},
122 Equal.sym(Result<&2, &1, Core.Error, Core.Tensor<shape>>, Done{tensor}, Fail{error}, equal)))} :
123 Allocation.TensorDone<shape, Fail{error}> -> Empty}(done)}
124 case Done{tensor}:
125 Laws.ZerosModel{({==}, index => inside => Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, tensor, index),
126 Core.read_value(shape, Core.read_flat(shape, tensor, index)), Some{0.0},
127 Equal.sym(Maybe<&2, F32>, Core.read_value(shape, Core.read_flat(shape, tensor, index)), Core.checked_observe(shape, tensor, index),
128 {\{Core.SourceRead: meaning => meaning} : Core.SourceRead<shape, tensor, index> ->
129 {Core.read_value(shape, Core.read_flat(shape, tensor, index)) == Core.checked_observe(shape, tensor, index) : Maybe<&2, F32>}}(
130 Core.source_read_model(shape, tensor, index))),
131 %Equal.sym(Result<&2, &1, Core.Error, Core.Tensor<shape>>, Done{tensor}, Core.new(shape, 0.0), same) :
132 {Observation.point(shape, index, _) == Some{0.0} : Maybe<&2, F32>}
133 ConstructionProof.point_value(shape, 0.0, index, inside)))}
134
135def Laws.gradient_unset_zeros(shape):
136 unset_zeros(shape, Core.new(shape, 0.0), {==}, AllocationProof.core_new_done(shape, 0.0))
137
138def Laws.gradient_held(shape, held):
139 {==}
140
141def state_contribution(-shape: Shape.Shape, state: Gradient.State<shape>) -> Core.Dynamic:
142 Gradient.State{contribution, total} = state
143 contribution
144
145def state_total(-shape: Shape.Shape, state: Gradient.State<shape>) -> Core.Tensor<shape>:
146 Gradient.State{contribution, total} = state
147 total
148
149def step_owner(-shape: Shape.Shape, result: Gradient.Step<shape>) -> Core.Dynamic:
150 match result:
151 case Gradient.Stop{contribution, total, error}:
152 contribution
153 case Gradient.Continue{state}:
154 state_contribution(shape, state)
155
156def step_continued(-shape: Shape.Shape, result: Gradient.Step<shape>) -> Bool:
157 match result:
158 case Gradient.Stop{contribution, total, error}:
159 False{}
160 case Gradient.Continue{state}:
161 True{}
162
163def write_owner(-shape: Shape.Shape, -contribution: Core.Dynamic, pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>) ->
164 Holds<{step_owner(shape, Gradient.step_write(shape, contribution, pair)) == contribution : Core.Dynamic}>:
165 (total, result) = pair
166 match result:
167 case Fail{error}:
168 Holds{{==}}
169 case Done{unit}:
170 Holds{{==}}
171
172def total_owner(-shape: Shape.Shape, +index: U32, -contribution: Core.Dynamic, +value: F32,
173 pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>) ->
174 Holds<{step_owner(shape, Gradient.step_total(shape, index, contribution, value, pair)) == contribution : Core.Dynamic}>:
175 (total, result) = pair
176 match result:
177 case Fail{error}:
178 Holds{{==}}
179 case Done{+accumulated}:
180 write_owner(shape, contribution, Core.write_flat(shape, total, index, F32.add(accumulated, value)))
181
182def contribution_retains(-shape: Shape.Shape, +index: U32, total: Core.Tensor<shape>, -original: Core.Dynamic,
183 pair: Core.Dynamic & Result<&2, &2, Core.Error, F32>,
184 -same: Totality.SameSource(original, ElementwiseProof.dynamic_read_owner(pair))) ->
185 Holds<Totality.SameSource(original, step_owner(shape, Gradient.step_contribution(shape, index, total, pair)))>:
186 (contribution, result) = pair
187 match result:
188 case Fail{error}:
189 Holds{same}
190 case Done{value}:
191 Holds{property => Equal.trans(Totality.Inspection,
192 Totality.inspect(property, step_owner(shape, Gradient.step_total(shape, index, contribution, value, Core.read_flat(shape, total, index)))),
193 Totality.inspect(property, contribution), Totality.inspect(property, original),
194 Equal.cong(Core.Dynamic, Totality.Inspection, owner => Totality.inspect(property, owner),
195 step_owner(shape, Gradient.step_total(shape, index, contribution, value, Core.read_flat(shape, total, index))), contribution,
196 {\{Holds: proof => proof} : Holds<{step_owner(shape, Gradient.step_total(shape, index, contribution, value, Core.read_flat(shape, total, index))) == contribution : Core.Dynamic}> ->
197 {step_owner(shape, Gradient.step_total(shape, index, contribution, value, Core.read_flat(shape, total, index))) == contribution : Core.Dynamic}}(
198 total_owner(shape, index, contribution, value, Core.read_flat(shape, total, index)))),
199 same(property))}
200
201def step_retains(-shape: Shape.Shape, +index: U32, state: Gradient.State<shape>) ->
202 Holds<Totality.SameSource(state_contribution(shape, state), step_owner(shape, Gradient.step(shape, index, state)))>:
203 Gradient.State{contribution, total} = state
204 Holds{{\{ElementwiseProof.SourceModel: same =>
205 {\{Holds: proof => proof} :
206 Holds<Totality.SameSource(contribution, step_owner(shape, Gradient.step_contribution(shape, index, total, Core.read_dynamic(contribution, index))))> ->
207 Totality.SameSource(contribution, step_owner(shape, Gradient.step_contribution(shape, index, total, Core.read_dynamic(contribution, index))))}(
208 contribution_retains(shape, index, total, contribution, Core.read_dynamic(contribution, index), same))} :
209 ElementwiseProof.SourceModel<contribution, ElementwiseProof.dynamic_read_owner(Core.read_dynamic(contribution, index))> ->
210 Totality.SameSource(contribution, step_owner(shape, Gradient.step_contribution(shape, index, total, Core.read_dynamic(contribution, index))))}(
211 ElementwiseProof.dynamic_read_retains(contribution, index))}
212
213def partial(+below: Bool, total: Maybe<&2, F32>, contribution: Maybe<&2, F32>) -> Maybe<&2, F32>:
214 match below:
215 case True{}:
216 Laws.add_word(total, contribution)
217 case False{}:
218 total
219
220def Inv(+shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +cursor: Nat, total: Core.Tensor<shape>) -> Type:
221 @+index: U32 -> @inside: Laws.Inside(shape, index) ->
222 {Core.checked_observe(shape, total, index) ==
223 partial(Nat.is_lt(U32.to_nat(index), cursor), Core.checked_observe(shape, original, index), Core.checked_observe_dynamic(contribution, index)) : Maybe<&2, F32>}
224
225def StepInv(+shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +cursor: Nat, result: Gradient.Step<shape>) -> Type:
226 match result:
227 case Gradient.Stop{owner, total, error}:
228 Unit
229 case Gradient.Continue{state}:
230 Inv(shape, original, contribution, 1n+cursor, state_total(shape, state))
231
232def Dims(+shape: Shape.Shape, after: Gradient.Slot) -> Type:
233 {Laws.held_dimensions(after) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>}
234
235def Values(+shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +limit: Nat, after: Gradient.Slot) -> Type:
236 @+index: U32 -> @inside: Laws.Inside(shape, index) ->
237 {Laws.held_observe(after, index) ==
238 partial(Nat.is_lt(U32.to_nat(index), limit), Core.checked_observe(shape, original, index), Core.checked_observe_dynamic(contribution, index)) : Maybe<&2, F32>}
239
240def LoopInv(+shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +limit: Nat, outcome: Gradient.Outcome) -> Type:
241 match outcome:
242 case Gradient.Refused{after, returned, error}:
243 Unit
244 case Gradient.Accumulated{after}:
245 Dims(shape, after) & Values(shape, original, contribution, limit, after)
246
247def written_true(+shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +cursor: Nat,
248 -before: Core.Tensor<shape>, -written: Core.Tensor<shape>, +index: U32, +accumulated: F32, +value: F32,
249 +other: U32, -equal: {True{} == Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) : Bool},
250 -inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
251 -exact: {U32.to_nat(index) == cursor : Nat},
252 -inv: Inv(shape, original, contribution, cursor, before),
253 -read: {Core.checked_observe(shape, before, index) == Some{accumulated} : Maybe<&2, F32>},
254 -stored: {Core.checked_observe(shape, written, index) == Some{F32.add(accumulated, value)} : Maybe<&2, F32>},
255 -word: {Core.checked_observe_dynamic(contribution, index) == Some{value} : Maybe<&2, F32>}) ->
256 Holds<{Core.checked_observe(shape, written, other) ==
257 partial(Nat.is_lt(U32.to_nat(other), 1n+cursor), Core.checked_observe(shape, original, other), Core.checked_observe_dynamic(contribution, other)) : Maybe<&2, F32>}>:
258 Holds{
259 %{\{Holds: proof => proof} : Holds<{index == other : U32}> -> {index == other : U32}}(word_exact(index, other, equal)) :
260 {Core.checked_observe(shape, written, _) ==
261 partial(Nat.is_lt(U32.to_nat(_), 1n+cursor), Core.checked_observe(shape, original, _), Core.checked_observe_dynamic(contribution, _)) : Maybe<&2, F32>}
262 Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, written, index), Some{F32.add(accumulated, value)},
263 partial(Nat.is_lt(U32.to_nat(index), 1n+cursor), Core.checked_observe(shape, original, index), Core.checked_observe_dynamic(contribution, index)),
264 stored,
265 %Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), 1n+cursor), True{},
266 %Equal.sym(Nat, U32.to_nat(index), cursor, exact) : {Nat.is_lt(_, 1n+cursor) == True{} : Bool}
267 lt_succ_self(cursor)) :
268 {Some{F32.add(accumulated, value)} == partial(_, Core.checked_observe(shape, original, index), Core.checked_observe_dynamic(contribution, index)) : Maybe<&2, F32>}
269 %Equal.sym(Maybe<&2, F32>, Core.checked_observe(shape, original, index), Some{accumulated},
270 Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, original, index),
271 partial(Nat.is_lt(U32.to_nat(index), cursor), Core.checked_observe(shape, original, index), Core.checked_observe_dynamic(contribution, index)),
272 Some{accumulated},
273 %Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), cursor), False{},
274 %Equal.sym(Nat, U32.to_nat(index), cursor, exact) : {Nat.is_lt(_, cursor) == False{} : Bool}
275 lt_self(cursor)) :
276 {Core.checked_observe(shape, original, index) ==
277 partial(_, Core.checked_observe(shape, original, index), Core.checked_observe_dynamic(contribution, index)) : Maybe<&2, F32>}
278 {==},
279 Equal.trans(Maybe<&2, F32>,
280 partial(Nat.is_lt(U32.to_nat(index), cursor), Core.checked_observe(shape, original, index), Core.checked_observe_dynamic(contribution, index)),
281 Core.checked_observe(shape, before, index), Some{accumulated},
282 Equal.sym(Maybe<&2, F32>, Core.checked_observe(shape, before, index),
283 partial(Nat.is_lt(U32.to_nat(index), cursor), Core.checked_observe(shape, original, index), Core.checked_observe_dynamic(contribution, index)),
284 inv(index)(
285 %Equal.sym(U32, index, other, {\{Holds: proof => proof} : Holds<{index == other : U32}> -> {index == other : U32}}(word_exact(index, other, equal))) :
286 {Nat.is_lt(U32.to_nat(_), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}
287 inside)),
288 read))) :
289 {Some{F32.add(accumulated, value)} == Laws.add_word(_, Core.checked_observe_dynamic(contribution, index)) : Maybe<&2, F32>}
290 %Equal.sym(Maybe<&2, F32>, Core.checked_observe_dynamic(contribution, index), Some{value}, word) :
291 {Some{F32.add(accumulated, value)} == Laws.add_word(Some{accumulated}, _) : Maybe<&2, F32>}
292 {==})}
293
294def written_false(+shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +cursor: Nat,
295 -before: Core.Tensor<shape>, -read_owner: Core.Tensor<shape>, -written: Core.Tensor<shape>, +index: U32,
296 +other: U32, -equal: {False{} == Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) : Bool},
297 -inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
298 -exact: {U32.to_nat(index) == cursor : Nat},
299 -inv: Inv(shape, original, contribution, cursor, before),
300 -kept: {Core.checked_observe(shape, read_owner, other) == Core.checked_observe(shape, before, other) : Maybe<&2, F32>},
301 -frame: {Core.checked_observe(shape, written, other) == Core.checked_observe(shape, read_owner, other) : Maybe<&2, F32>}) ->
302 Holds<{Core.checked_observe(shape, written, other) ==
303 partial(Nat.is_lt(U32.to_nat(other), 1n+cursor), Core.checked_observe(shape, original, other), Core.checked_observe_dynamic(contribution, other)) : Maybe<&2, F32>}>:
304 Holds{Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, written, other), Core.checked_observe(shape, read_owner, other),
305 partial(Nat.is_lt(U32.to_nat(other), 1n+cursor), Core.checked_observe(shape, original, other), Core.checked_observe_dynamic(contribution, other)),
306 frame,
307 Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, read_owner, other), Core.checked_observe(shape, before, other),
308 partial(Nat.is_lt(U32.to_nat(other), 1n+cursor), Core.checked_observe(shape, original, other), Core.checked_observe_dynamic(contribution, other)),
309 kept,
310 Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, before, other),
311 partial(Nat.is_lt(U32.to_nat(other), cursor), Core.checked_observe(shape, original, other), Core.checked_observe_dynamic(contribution, other)),
312 partial(Nat.is_lt(U32.to_nat(other), 1n+cursor), Core.checked_observe(shape, original, other), Core.checked_observe_dynamic(contribution, other)),
313 inv(other)(inside),
314 %lt_step(U32.to_nat(other), cursor,
315 %exact : {False{} == Nat.is_eq(_, U32.to_nat(other)) : Bool}
316 equal) :
317 {partial(Nat.is_lt(U32.to_nat(other), cursor), Core.checked_observe(shape, original, other), Core.checked_observe_dynamic(contribution, other)) ==
318 partial(_, Core.checked_observe(shape, original, other), Core.checked_observe_dynamic(contribution, other)) : Maybe<&2, F32>}
319 {==})))}
320
321def position_inv(+shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +cursor: Nat,
322 -before: Core.Tensor<shape>, read_owner: Core.Tensor<shape>, -written: Core.Tensor<shape>,
323 +index: U32, +accumulated: F32, +value: F32, -unit: Unit,
324 +other: U32, decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), U32.to_nat(other))>,
325 -inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
326 -exact: {U32.to_nat(index) == cursor : Nat},
327 -meaning: Core.CheckedUpdateMeaning(shape, read_owner, index, F32.add(accumulated, value), (written, Done{unit})),
328 -inv: Inv(shape, original, contribution, cursor, before),
329 -read: {Core.checked_observe(shape, before, index) == Some{accumulated} : Maybe<&2, F32>},
330 -kept: @+position: U32 -> {Core.checked_observe(shape, read_owner, position) == Core.checked_observe(shape, before, position) : Maybe<&2, F32>},
331 -word: {Core.checked_observe_dynamic(contribution, index) == Some{value} : Maybe<&2, F32>}) ->
332 Holds<{Core.checked_observe(shape, written, other) ==
333 partial(Nat.is_lt(U32.to_nat(other), 1n+cursor), Core.checked_observe(shape, original, other), Core.checked_observe_dynamic(contribution, other)) : Maybe<&2, F32>}>:
334 match decision:
335 case Shape.BTrue{equal}:
336 written_true(shape, original, contribution, cursor, before, written, index, accumulated, value, other, equal, inside, exact, inv, read,
337 ReduceProof.update_written(shape, read_owner, written, index, F32.add(accumulated, value), unit, meaning), word)
338 case Shape.BFalse{equal}:
339 written_false(shape, original, contribution, cursor, before, read_owner, written, index, other, equal, inside, exact, inv,
340 kept(other),
341 ReduceProof.frame_equal(shape, written, read_owner, other,
342 ReduceProof.update_frame(shape, read_owner, written, index, F32.add(accumulated, value), unit, meaning)(other)(
343 {\{TransformProof.CheckedObservationModel: checked => checked} :
344 TransformProof.CheckedObservationModel<shape, read_owner, other> -> Core.ObservationChecked(Core.Packed{shape, read_owner}, other)}(
345 TransformProof.checked_observation_model(shape, read_owner, other, inside)))(
346 Equal.sym(Bool, False{}, Nat.is_eq(U32.to_nat(index), U32.to_nat(other)), equal))))
347
348def write_inv(+shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +cursor: Nat,
349 -before: Core.Tensor<shape>, -read_owner: Core.Tensor<shape>, +index: U32, +accumulated: F32, +value: F32,
350 owner: Core.Dynamic, pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>,
351 -exact: {U32.to_nat(index) == cursor : Nat},
352 -meaning: Core.CheckedUpdateMeaning(shape, read_owner, index, F32.add(accumulated, value), pair),
353 -inv: Inv(shape, original, contribution, cursor, before),
354 -read: {Core.checked_observe(shape, before, index) == Some{accumulated} : Maybe<&2, F32>},
355 -kept: @+position: U32 -> {Core.checked_observe(shape, read_owner, position) == Core.checked_observe(shape, before, position) : Maybe<&2, F32>},
356 -word: {Core.checked_observe_dynamic(contribution, index) == Some{value} : Maybe<&2, F32>}) ->
357 Holds<StepInv(shape, original, contribution, cursor, Gradient.step_write(shape, owner, pair))>:
358 (written, result) = pair
359 match result:
360 case Fail{error}:
361 Holds{Unit{}}
362 case Done{unit}:
363 Holds{other => inside => {\{Holds: proof => proof} :
364 Holds<{Core.checked_observe(shape, written, other) ==
365 partial(Nat.is_lt(U32.to_nat(other), 1n+cursor), Core.checked_observe(shape, original, other), Core.checked_observe_dynamic(contribution, other)) : Maybe<&2, F32>}> ->
366 {Core.checked_observe(shape, written, other) ==
367 partial(Nat.is_lt(U32.to_nat(other), 1n+cursor), Core.checked_observe(shape, original, other), Core.checked_observe_dynamic(contribution, other)) : Maybe<&2, F32>}}(
368 position_inv(shape, original, contribution, cursor, before, read_owner, written, index, accumulated, value, unit,
369 other, Shape.bool_case(Nat.is_eq(U32.to_nat(index), U32.to_nat(other))), inside, exact, meaning, inv, read, kept, word))}
370
371def total_inv(+shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +cursor: Nat,
372 -before: Core.Tensor<shape>, +index: U32, +value: F32, owner: Core.Dynamic,
373 pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>,
374 -exact: {U32.to_nat(index) == cursor : Nat},
375 -source: {Core.read_value(shape, pair) == Core.checked_observe(shape, before, index) : Maybe<&2, F32>},
376 -keeps: @+position: U32 -> {Core.retained_read_observe(shape, pair, position) == Core.checked_observe(shape, before, position) : Maybe<&2, F32>},
377 -inv: Inv(shape, original, contribution, cursor, before),
378 -word: {Core.checked_observe_dynamic(contribution, index) == Some{value} : Maybe<&2, F32>}) ->
379 Holds<StepInv(shape, original, contribution, cursor, Gradient.step_total(shape, index, owner, value, pair))>:
380 (read_owner, result) = pair
381 match result:
382 case Fail{error}:
383 Holds{Unit{}}
384 case Done{+accumulated}:
385 write_inv(shape, original, contribution, cursor, before, read_owner, index, accumulated, value, owner,
386 Core.write_flat(shape, read_owner, index, F32.add(accumulated, value)), exact,
387 {\{Core.CheckedUpdateModel: meaning => meaning} :
388 Core.CheckedUpdateModel<shape, read_owner, index, F32.add(accumulated, value)> ->
389 Core.CheckedUpdateMeaning(shape, read_owner, index, F32.add(accumulated, value),
390 Core.write_flat(shape, read_owner, index, F32.add(accumulated, value)))}(
391 CoreProof.checked_update_model(shape, read_owner, index, F32.add(accumulated, value))),
392 inv, Equal.sym(Maybe<&2, F32>, Some{accumulated}, Core.checked_observe(shape, before, index), source), keeps, word)
393
394def contribution_inv(+shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +cursor: Nat, +index: U32,
395 total: Core.Tensor<shape>, -current: Core.Dynamic, pair: Core.Dynamic & Result<&2, &2, Core.Error, F32>,
396 -exact: {U32.to_nat(index) == cursor : Nat},
397 -source: {Core.dynamic_read_value(pair) == Core.checked_observe_dynamic(current, index) : Maybe<&2, F32>},
398 -same: Totality.SameSource(contribution, current),
399 -inv: Inv(shape, original, contribution, cursor, total)) ->
400 Holds<StepInv(shape, original, contribution, cursor, Gradient.step_contribution(shape, index, total, pair))>:
401 (owner, result) = pair
402 match result:
403 case Fail{error}:
404 Holds{Unit{}}
405 case Done{+value}:
406 total_inv(shape, original, contribution, cursor, total, index, value, owner, Core.read_flat(shape, total, index), exact,
407 {\{Core.SourceRead: meaning => meaning} : Core.SourceRead<shape, total, index> ->
408 {Core.read_value(shape, Core.read_flat(shape, total, index)) == Core.checked_observe(shape, total, index) : Maybe<&2, F32>}}(
409 Core.source_read_model(shape, total, index)),
410 {\{Core.SourceReadKeeps: kept => kept} : Core.SourceReadKeeps<shape, total, index> ->
411 @+position: U32 -> {Core.retained_read_observe(shape, Core.read_flat(shape, total, index), position) == Core.checked_observe(shape, total, position) : Maybe<&2, F32>}}(
412 Core.source_read_keeps(shape, total, index)),
413 inv,
414 Equal.trans(Maybe<&2, F32>, Core.checked_observe_dynamic(contribution, index), Core.checked_observe_dynamic(current, index), Some{value},
415 Equal.sym(Maybe<&2, F32>, Core.checked_observe_dynamic(current, index), Core.checked_observe_dynamic(contribution, index),
416 {\{Holds: proof => proof} : Holds<{Core.checked_observe_dynamic(current, index) == Core.checked_observe_dynamic(contribution, index) : Maybe<&2, F32>}> ->
417 {Core.checked_observe_dynamic(current, index) == Core.checked_observe_dynamic(contribution, index) : Maybe<&2, F32>}}(
418 same_checked(contribution, current, same, index))),
419 Equal.sym(Maybe<&2, F32>, Some{value}, Core.checked_observe_dynamic(current, index), source)))
420
421def step_inv(+shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +cursor: Nat, +index: U32,
422 -exact: {U32.to_nat(index) == cursor : Nat}, state: Gradient.State<shape>,
423 -inv: Inv(shape, original, contribution, cursor, state_total(shape, state)),
424 -same: Totality.SameSource(contribution, state_contribution(shape, state))) ->
425 Holds<StepInv(shape, original, contribution, cursor, Gradient.step(shape, index, state))>:
426 Gradient.State{current, total} = state
427 contribution_inv(shape, original, contribution, cursor, index, total, current, Core.read_dynamic(current, index), exact,
428 {\{Core.DynamicSourceRead: meaning => meaning} : Core.DynamicSourceRead<current, index> ->
429 {Core.dynamic_read_value(Core.read_dynamic(current, index)) == Core.checked_observe_dynamic(current, index) : Maybe<&2, F32>}}(
430 Core.dynamic_source_read_model(current, index)),
431 same, inv)
432
433def continue_inv(+remaining: Nat, +shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +cursor: Nat,
434 result: Gradient.Step<shape>, -step: StepInv(shape, original, contribution, cursor, result),
435 -same: Totality.SameSource(contribution, step_owner(shape, result)),
436 -rec: @state: Gradient.State<shape> -> @-inv: Inv(shape, original, contribution, 1n+cursor, state_total(shape, state)) ->
437 @-same: Totality.SameSource(contribution, state_contribution(shape, state)) ->
438 Holds<LoopInv(shape, original, contribution, Nat.add(remaining, 1n+cursor), Gradient.loop(remaining, shape, 1n+cursor, state))>) ->
439 Holds<LoopInv(shape, original, contribution, Nat.add(remaining, 1n+cursor),
440 Gradient.continue_step(shape, state => Gradient.loop(remaining, shape, 1n+cursor, state), result))>:
441 match result:
442 case Gradient.Stop{owner, total, error}:
443 Holds{Unit{}}
444 case Gradient.Continue{state}:
445 Holds{{\{Holds: proof => proof} :
446 Holds<LoopInv(shape, original, contribution, Nat.add(remaining, 1n+cursor), Gradient.loop(remaining, shape, 1n+cursor, state))> ->
447 LoopInv(shape, original, contribution, Nat.add(remaining, 1n+cursor), Gradient.loop(remaining, shape, 1n+cursor, state))}(rec(state, step, same))}
448
449def conversion_inv(+shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +limit: Nat, state: Gradient.State<shape>) ->
450 Holds<LoopInv(shape, original, contribution, limit, Gradient.conversion_error(shape, state))>:
451 Gradient.State{owner, total} = state
452 Holds{Unit{}}
453
454def decided_inv(+remaining: Nat, +shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +cursor: Nat, +index: U32,
455 state: Gradient.State<shape>, decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), cursor)>,
456 -inv: Inv(shape, original, contribution, cursor, state_total(shape, state)),
457 -same: Totality.SameSource(contribution, state_contribution(shape, state)),
458 -rec: @state: Gradient.State<shape> -> @-inv: Inv(shape, original, contribution, 1n+cursor, state_total(shape, state)) ->
459 @-same: Totality.SameSource(contribution, state_contribution(shape, state)) ->
460 Holds<LoopInv(shape, original, contribution, Nat.add(remaining, 1n+cursor), Gradient.loop(remaining, shape, 1n+cursor, state))>) ->
461 Holds<LoopInv(shape, original, contribution, Nat.add(remaining, 1n+cursor), Gradient.decided(shape, cursor, index, state,
462 state => Gradient.loop(remaining, shape, 1n+cursor, state), decision))>:
463 match decision:
464 case Shape.BFalse{equal}:
465 conversion_inv(shape, original, contribution, Nat.add(remaining, 1n+cursor), state)
466 case Shape.BTrue{equal}:
467 continue_inv(remaining, shape, original, contribution, cursor, Gradient.step(shape, index, state),
468 {\{Holds: proof => proof} : Holds<StepInv(shape, original, contribution, cursor, Gradient.step(shape, index, state))> ->
469 StepInv(shape, original, contribution, cursor, Gradient.step(shape, index, state))}(
470 step_inv(shape, original, contribution, cursor, index, Lifecycle.natural_equal(U32.to_nat(index), cursor, equal), state, inv, same)),
471 {\{Holds: proof => proof} : Holds<Totality.SameSource(contribution, step_owner(shape, Gradient.step(shape, index, state)))> ->
472 Totality.SameSource(contribution, step_owner(shape, Gradient.step(shape, index, state)))}(
473 same_trans(contribution, state_contribution(shape, state), step_owner(shape, Gradient.step(shape, index, state)), same,
474 {\{Holds: proof => proof} : Holds<Totality.SameSource(state_contribution(shape, state), step_owner(shape, Gradient.step(shape, index, state)))> ->
475 Totality.SameSource(state_contribution(shape, state), step_owner(shape, Gradient.step(shape, index, state)))}(
476 step_retains(shape, index, state)))),
477 rec)
478
479def loop_inv(fuel: Nat, +shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +cursor: Nat, state: Gradient.State<shape>,
480 -inv: Inv(shape, original, contribution, cursor, state_total(shape, state)),
481 -same: Totality.SameSource(contribution, state_contribution(shape, state))) ->
482 Holds<LoopInv(shape, original, contribution, Nat.add(fuel, cursor), Gradient.loop(fuel, shape, cursor, state))>:
483 match fuel:
484 case 0n:
485 Gradient.State{owner, total} = state
486 Holds{({==}, inv)}
487 case 1n+remaining:
488 Holds{
489 %Arith.add_succ(remaining, cursor) : LoopInv(shape, original, contribution, _, Gradient.loop(1n+remaining, shape, cursor, state))
490 {\{Holds: proof => proof} :
491 Holds<LoopInv(shape, original, contribution, Nat.add(remaining, 1n+cursor), Gradient.loop(1n+remaining, shape, cursor, state))> ->
492 LoopInv(shape, original, contribution, Nat.add(remaining, 1n+cursor), Gradient.loop(1n+remaining, shape, cursor, state))}(
493 decided_inv(remaining, shape, original, contribution, cursor, U32.from_nat(cursor), state,
494 Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)), inv, same,
495 state => inv => same => loop_inv(remaining, shape, original, contribution, 1n+cursor, state, inv, same)))}
496
497def initial_inv(+shape: Shape.Shape, total: Core.Tensor<shape>, -contribution: Core.Dynamic) ->
498 Holds<Inv(shape, total, contribution, 0n, total)>:
499 Holds{index => inside =>
500 %Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), 0n), False{}, below_zero(U32.to_nat(index))) :
501 {Core.checked_observe(shape, total, index) ==
502 partial(_, Core.checked_observe(shape, total, index), Core.checked_observe_dynamic(contribution, index)) : Maybe<&2, F32>}
503 {==}}
504
505def finish_mapping(+total_shape: Shape.Shape, +shape: Shape.Shape, -total: Core.Tensor<total_shape>, -contribution: Core.Dynamic,
506 outcome: Gradient.Outcome,
507 -dimensions: {Shape.dimensions(total_shape) == Shape.dimensions(shape) : List<&2, U32>},
508 -loop: LoopInv(total_shape, total, contribution, Nat.add(Shape.elements(total_shape), 0n), outcome)) ->
509 Holds<Laws.Mapping(Gradient.Held{Core.Packed{total_shape, total}}, contribution, shape, outcome)>:
510 match outcome:
511 case Gradient.Refused{after, returned, error}:
512 Holds{Unit{}}
513 case Gradient.Accumulated{after}:
514 Holds{(
515 Equal.trans(Maybe<&2, List<&2, U32>>, Laws.held_dimensions(after), Some{Shape.dimensions(total_shape)}, Some{Shape.dimensions(shape)},
516 Pair.fst(Dims(total_shape, after), Values(total_shape, total, contribution, Nat.add(Shape.elements(total_shape), 0n), after), loop),
517 %dimensions : {Some{Shape.dimensions(total_shape)} == Some{_} : Maybe<&2, List<&2, U32>>}
518 {==}),
519 index => inside => Equal.trans(Maybe<&2, F32>, Laws.held_observe(after, index),
520 partial(Nat.is_lt(U32.to_nat(index), Nat.add(Shape.elements(total_shape), 0n)),
521 Core.checked_observe(total_shape, total, index), Core.checked_observe_dynamic(contribution, index)),
522 Laws.add_word(Core.checked_observe(total_shape, total, index), Core.checked_observe_dynamic(contribution, index)),
523 Pair.snd(Dims(total_shape, after), Values(total_shape, total, contribution, Nat.add(Shape.elements(total_shape), 0n), after), loop)(index)(
524 %Equal.sym(List<&2, U32>, Shape.dimensions(total_shape), Shape.dimensions(shape), dimensions) :
525 {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(_)) == True{} : Bool}
526 inside),
527 %Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), Nat.add(Shape.elements(total_shape), 0n)), True{},
528 %Equal.sym(Nat, Nat.add(Shape.elements(total_shape), 0n), Shape.elements(total_shape), TransformProof.add_zero_right(Shape.elements(total_shape))) :
529 {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
530 %Equal.sym(Nat, Shape.elements(total_shape), Shape.numel(Shape.extents(total_shape)), Shape.elements_exact(total_shape)) :
531 {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
532 %Equal.sym(List<&2, U32>, Shape.dimensions(total_shape), Shape.dimensions(shape), dimensions) :
533 {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(_)) == True{} : Bool}
534 inside) :
535 {partial(_, Core.checked_observe(total_shape, total, index), Core.checked_observe_dynamic(contribution, index)) ==
536 Laws.add_word(Core.checked_observe(total_shape, total, index), Core.checked_observe_dynamic(contribution, index)) : Maybe<&2, F32>}
537 {==}))}
538
539def held_checked_mapping(+shape: Shape.Shape, contribution: Core.Dynamic, +total_shape: Shape.Shape, total: Core.Tensor<total_shape>, same: Bool,
540 -decided: {same == Layout.words_same(Shape.dimensions(total_shape), Shape.dimensions(shape)) : Bool}) ->
541 Holds<Laws.Mapping(Gradient.Held{Core.Packed{total_shape, total}}, contribution, shape, Gradient.held_checked(contribution, total_shape, total, same))>:
542 match same:
543 case False{}:
544 Holds{Unit{}}
545 case True{}:
546 finish_mapping(total_shape, shape, total, contribution,
547 Gradient.loop(Shape.elements(total_shape), total_shape, 0n, Gradient.State{contribution, total}),
548 {\{Holds: proof => proof} : Holds<{Shape.dimensions(total_shape) == Shape.dimensions(shape) : List<&2, U32>}> ->
549 {Shape.dimensions(total_shape) == Shape.dimensions(shape) : List<&2, U32>}}(words_dimensions(total_shape, shape, decided)),
550 {\{Holds: proof => proof} :
551 Holds<LoopInv(total_shape, total, contribution, Nat.add(Shape.elements(total_shape), 0n),
552 Gradient.loop(Shape.elements(total_shape), total_shape, 0n, Gradient.State{contribution, total}))> ->
553 LoopInv(total_shape, total, contribution, Nat.add(Shape.elements(total_shape), 0n),
554 Gradient.loop(Shape.elements(total_shape), total_shape, 0n, Gradient.State{contribution, total}))}(
555 loop_inv(Shape.elements(total_shape), total_shape, total, contribution, 0n, Gradient.State{contribution, total},
556 {\{Holds: proof => proof} : Holds<Inv(total_shape, total, contribution, 0n, total)> -> Inv(total_shape, total, contribution, 0n, total)}(
557 initial_inv(total_shape, total, contribution)),
558 property => {==})))
559
560def held_mapping(+shape: Shape.Shape, contribution: Core.Dynamic, gradient: Core.Dynamic) ->
561 Holds<Laws.Mapping(Gradient.Held{gradient}, contribution, shape, Gradient.held(shape, contribution, gradient))>:
562 Core.Packed{+total_shape, total} = gradient
563 held_checked_mapping(shape, contribution, total_shape, total,
564 Layout.words_same(Shape.dimensions(total_shape), Shape.dimensions(shape)), {==})
565
566def agreed_mapping(+shape: Shape.Shape, slot: Gradient.Slot, contribution: Core.Dynamic,
567 -agrees: {Totality.dimensions(contribution) == Shape.dimensions(shape) : List<&2, U32>}) ->
568 Holds<Laws.Mapping(slot, contribution, shape, Gradient.agreed(shape, slot, contribution))>:
569 match slot:
570 case Gradient.Unset{}:
571 Holds{(
572 %agrees : {Some{Totality.dimensions(contribution)} == Some{_} : Maybe<&2, List<&2, U32>>}
573 {==},
574 index => inside => {==})}
575 case Gradient.Held{gradient}:
576 held_mapping(shape, contribution, gradient)
577
578def checked_mapping(+shape: Shape.Shape, slot: Gradient.Slot, +contribution_shape: Shape.Shape, tensor: Core.Tensor<contribution_shape>, same: Bool,
579 -decided: {same == Layout.words_same(Shape.dimensions(contribution_shape), Shape.dimensions(shape)) : Bool}) ->
580 Holds<Laws.Mapping(slot, Core.Packed{contribution_shape, tensor}, shape, Gradient.checked(shape, slot, contribution_shape, tensor, same))>:
581 match same:
582 case False{}:
583 Holds{Unit{}}
584 case True{}:
585 agreed_mapping(shape, slot, Core.Packed{contribution_shape, tensor},
586 {\{Holds: proof => proof} : Holds<{Shape.dimensions(contribution_shape) == Shape.dimensions(shape) : List<&2, U32>}> ->
587 {Shape.dimensions(contribution_shape) == Shape.dimensions(shape) : List<&2, U32>}}(words_dimensions(contribution_shape, shape, decided)))
588
589def Laws.accumulate_mapping(shape, slot, contribution):
590 Core.Packed{+contribution_shape, tensor} = contribution
591 Laws.MappingModel{
592 {\{Holds: proof => proof} :
593 Holds<Laws.Mapping(slot, Core.Packed{contribution_shape, tensor}, shape,
594 Gradient.checked(shape, slot, contribution_shape, tensor, Layout.words_same(Shape.dimensions(contribution_shape), Shape.dimensions(shape))))> ->
595 Laws.Mapping(slot, Core.Packed{contribution_shape, tensor}, shape, Gradient.accumulate(shape, slot, Core.Packed{contribution_shape, tensor}))}(
596 checked_mapping(shape, slot, contribution_shape, tensor, Layout.words_same(Shape.dimensions(contribution_shape), Shape.dimensions(shape)), {==}))}
597
598def write_success(-shape: Shape.Shape, owner: Core.Dynamic, pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>,
599 -successful: {TransformTotality.write_succeeded(shape, pair) == True{} : Bool}) ->
600 Holds<{step_continued(shape, Gradient.step_write(shape, owner, pair)) == True{} : Bool}>:
601 (total, result) = pair
602 match result:
603 case Fail{error}:
604 Holds{Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))}
605 case Done{unit}:
606 Holds{{==}}
607
608def total_success(+shape: Shape.Shape, +index: U32, owner: Core.Dynamic, value: F32,
609 pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>,
610 -successful: {TransformTotality.read_succeeded(shape, pair) == True{} : Bool},
611 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
612 Holds<{step_continued(shape, Gradient.step_total(shape, index, owner, value, pair)) == True{} : Bool}>:
613 (total, result) = pair
614 match result:
615 case Fail{error}:
616 Holds{Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))}
617 case Done{+accumulated}:
618 write_success(shape, owner, Core.write_flat(shape, total, index, F32.add(accumulated, value)),
619 {\{TransformTotality.WriteSuccess: successful => successful} :
620 TransformTotality.WriteSuccess<shape, total, index, F32.add(accumulated, value)> ->
621 {TransformTotality.write_succeeded(shape, Core.write_flat(shape, total, index, F32.add(accumulated, value))) == True{} : Bool}}(
622 TransformProof.tensor_write_success(shape, total, index, F32.add(accumulated, value), inside)))
623
624def contribution_success(+shape: Shape.Shape, +index: U32, total: Core.Tensor<shape>,
625 pair: Core.Dynamic & Result<&2, &2, Core.Error, F32>,
626 -successful: {ElementwiseProof.dynamic_read_succeeded(pair) == True{} : Bool},
627 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
628 Holds<{step_continued(shape, Gradient.step_contribution(shape, index, total, pair)) == True{} : Bool}>:
629 (owner, result) = pair
630 match result:
631 case Fail{error}:
632 Holds{Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))}
633 case Done{value}:
634 total_success(shape, index, owner, value, Core.read_flat(shape, total, index),
635 {\{TransformTotality.ReadSuccess: successful => successful} : TransformTotality.ReadSuccess<shape, total, index> ->
636 {TransformTotality.read_succeeded(shape, Core.read_flat(shape, total, index)) == True{} : Bool}}(
637 TransformProof.read_success_status(shape, total, index, TransformProof.read_success(shape, total, index, inside))),
638 inside)
639
640def step_success(+shape: Shape.Shape, +index: U32, state: Gradient.State<shape>,
641 -fits: {Totality.dimensions(state_contribution(shape, state)) == Shape.dimensions(shape) : List<&2, U32>},
642 -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
643 Holds<{step_continued(shape, Gradient.step(shape, index, state)) == True{} : Bool}>:
644 Gradient.State{owner, total} = state
645 contribution_success(shape, index, total, Core.read_dynamic(owner, index),
646 {\{ElementwiseProof.DynamicReadSuccess: successful => successful} : ElementwiseProof.DynamicReadSuccess<owner, index> ->
647 {ElementwiseProof.dynamic_read_succeeded(Core.read_dynamic(owner, index)) == True{} : Bool}}(
648 ElementwiseProof.dynamic_read_success(owner, index,
649 %Equal.sym(List<&2, U32>, Totality.dimensions(owner), Shape.dimensions(shape), fits) :
650 {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(_)) == True{} : Bool}
651 inside)),
652 inside)
653
654def continue_success(+remaining: Nat, +shape: Shape.Shape, +cursor: Nat, result: Gradient.Step<shape>,
655 -continued: {step_continued(shape, result) == True{} : Bool},
656 -fits: {Totality.dimensions(step_owner(shape, result)) == Shape.dimensions(shape) : List<&2, U32>},
657 -rec: @state: Gradient.State<shape> -> @-fits: {Totality.dimensions(state_contribution(shape, state)) == Shape.dimensions(shape) : List<&2, U32>} ->
658 Holds<{Laws.accumulated(Gradient.loop(remaining, shape, 1n+cursor, state)) == True{} : Bool}>) ->
659 Holds<{Laws.accumulated(Gradient.continue_step(shape, state => Gradient.loop(remaining, shape, 1n+cursor, state), result)) == True{} : Bool}>:
660 match result:
661 case Gradient.Stop{owner, total, error}:
662 Holds{Empty.absurd({False{} == True{} : Bool}, Arith.clash(continued))}
663 case Gradient.Continue{state}:
664 Holds{{\{Holds: proof => proof} : Holds<{Laws.accumulated(Gradient.loop(remaining, shape, 1n+cursor, state)) == True{} : Bool}> ->
665 {Laws.accumulated(Gradient.loop(remaining, shape, 1n+cursor, state)) == True{} : Bool}}(rec(state, fits))}
666
667def decided_success(+remaining: Nat, +shape: Shape.Shape, +cursor: Nat, +index: U32,
668 state: Gradient.State<shape>, decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), cursor)>,
669 -exact: {U32.to_nat(index) == cursor : Nat},
670 -fits: {Totality.dimensions(state_contribution(shape, state)) == Shape.dimensions(shape) : List<&2, U32>},
671 -inside: {Nat.is_lt(cursor, Shape.elements(shape)) == True{} : Bool},
672 -rec: @state: Gradient.State<shape> -> @-fits: {Totality.dimensions(state_contribution(shape, state)) == Shape.dimensions(shape) : List<&2, U32>} ->
673 Holds<{Laws.accumulated(Gradient.loop(remaining, shape, 1n+cursor, state)) == True{} : Bool}>) ->
674 Holds<{Laws.accumulated(Gradient.decided(shape, cursor, index, state,
675 state => Gradient.loop(remaining, shape, 1n+cursor, state), decision)) == True{} : Bool}>:
676 match decision:
677 case Shape.BFalse{equal}:
678 Holds{Empty.absurd({Laws.accumulated(Gradient.conversion_error(shape, state)) == True{} : Bool},
679 Nats.contradiction(Nat.is_eq(U32.to_nat(index), cursor), PlanProof.eq_true(U32.to_nat(index), cursor, exact), equal))}
680 case Shape.BTrue{equal}:
681 continue_success(remaining, shape, cursor, Gradient.step(shape, index, state),
682 {\{Holds: proof => proof} : Holds<{step_continued(shape, Gradient.step(shape, index, state)) == True{} : Bool}> ->
683 {step_continued(shape, Gradient.step(shape, index, state)) == True{} : Bool}}(
684 step_success(shape, index, state, fits,
685 %Shape.elements_exact(shape) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
686 %Equal.sym(Nat, U32.to_nat(index), cursor, exact) : {Nat.is_lt(_, Shape.elements(shape)) == True{} : Bool}
687 inside)),
688 Equal.trans(List<&2, U32>, Totality.dimensions(step_owner(shape, Gradient.step(shape, index, state))),
689 Totality.dimensions(state_contribution(shape, state)), Shape.dimensions(shape),
690 {\{Holds: proof => proof} : Holds<{Totality.dimensions(step_owner(shape, Gradient.step(shape, index, state))) == Totality.dimensions(state_contribution(shape, state)) : List<&2, U32>}> ->
691 {Totality.dimensions(step_owner(shape, Gradient.step(shape, index, state))) == Totality.dimensions(state_contribution(shape, state)) : List<&2, U32>}}(
692 same_dimensions(state_contribution(shape, state), step_owner(shape, Gradient.step(shape, index, state)),
693 {\{Holds: proof => proof} : Holds<Totality.SameSource(state_contribution(shape, state), step_owner(shape, Gradient.step(shape, index, state)))> ->
694 Totality.SameSource(state_contribution(shape, state), step_owner(shape, Gradient.step(shape, index, state)))}(
695 step_retains(shape, index, state)))),
696 fits),
697 rec)
698
699def loop_success(fuel: Nat, +shape: Shape.Shape, +cursor: Nat, state: Gradient.State<shape>,
700 -fits: {Totality.dimensions(state_contribution(shape, state)) == Shape.dimensions(shape) : List<&2, U32>},
701 -within: {Nat.is_le(Nat.add(fuel, cursor), Shape.elements(shape)) == True{} : Bool}) ->
702 Holds<{Laws.accumulated(Gradient.loop(fuel, shape, cursor, state)) == True{} : Bool}>:
703 match fuel:
704 case 0n:
705 Gradient.State{owner, total} = state
706 Holds{{==}}
707 case 1n+remaining:
708 decided_success(remaining, shape, cursor, U32.from_nat(cursor), state,
709 Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)),
710 TransformProof.cursor_word_exact(shape, cursor,
711 Conversion.lt_le(cursor, Shape.elements(shape),
712 Arith.lt_le_trans(cursor, 1n+Nat.add(remaining, cursor), Shape.elements(shape),
713 Arith.lt_succ(cursor, Nat.add(remaining, cursor), TransformProof.add_cursor_le(remaining, cursor)), within))),
714 fits,
715 Arith.lt_le_trans(cursor, 1n+Nat.add(remaining, cursor), Shape.elements(shape),
716 Arith.lt_succ(cursor, Nat.add(remaining, cursor), TransformProof.add_cursor_le(remaining, cursor)), within),
717 state => fits => loop_success(remaining, shape, 1n+cursor, state, fits,
718 %Equal.sym(Nat, Nat.add(remaining, 1n+cursor), 1n+Nat.add(remaining, cursor), Arith.add_succ(remaining, cursor)) :
719 {Nat.is_le(_, Shape.elements(shape)) == True{} : Bool}
720 within))
721
722def full_loop(+shape: Shape.Shape) -> {Nat.is_le(Nat.add(Shape.elements(shape), 0n), Shape.elements(shape)) == True{} : Bool}:
723 %Equal.sym(Nat, Nat.add(Shape.elements(shape), 0n), Shape.elements(shape), TransformProof.add_zero_right(Shape.elements(shape))) :
724 {Nat.is_le(_, Shape.elements(shape)) == True{} : Bool}
725 Conversion.le_reflexive(Shape.elements(shape))
726
727def held_checked_success(+shape: Shape.Shape, contribution: Core.Dynamic, +total_shape: Shape.Shape, total: Core.Tensor<total_shape>, same: Bool,
728 -decided: {same == Layout.words_same(Shape.dimensions(total_shape), Shape.dimensions(shape)) : Bool},
729 -fits: {Shape.dimensions(total_shape) == Shape.dimensions(shape) : List<&2, U32>},
730 -agrees: {Totality.dimensions(contribution) == Shape.dimensions(shape) : List<&2, U32>}) ->
731 Laws.Success<Gradient.held_checked(contribution, total_shape, total, same)>:
732 match same:
733 case False{}:
734 Laws.Success{Empty.absurd({False{} == True{} : Bool},
735 Arith.clash(Equal.trans(Bool, False{}, Layout.words_same(Shape.dimensions(total_shape), Shape.dimensions(shape)), True{}, decided,
736 %fits : {Layout.words_same(Shape.dimensions(total_shape), _) == True{} : Bool}
737 TransformProof.words_same_refl(Shape.dimensions(total_shape)))))}
738 case True{}:
739 Laws.Success{{\{Holds: proof => proof} :
740 Holds<{Laws.accumulated(Gradient.loop(Shape.elements(total_shape), total_shape, 0n, Gradient.State{contribution, total})) == True{} : Bool}> ->
741 {Laws.accumulated(Gradient.loop(Shape.elements(total_shape), total_shape, 0n, Gradient.State{contribution, total})) == True{} : Bool}}(
742 loop_success(Shape.elements(total_shape), total_shape, 0n, Gradient.State{contribution, total},
743 Equal.trans(List<&2, U32>, Totality.dimensions(contribution), Shape.dimensions(shape), Shape.dimensions(total_shape), agrees,
744 Equal.sym(List<&2, U32>, Shape.dimensions(total_shape), Shape.dimensions(shape), fits)),
745 full_loop(total_shape)))}
746
747def held_success(+shape: Shape.Shape, contribution: Core.Dynamic, gradient: Core.Dynamic,
748 -fits: {Totality.dimensions(gradient) == Shape.dimensions(shape) : List<&2, U32>},
749 -agrees: {Totality.dimensions(contribution) == Shape.dimensions(shape) : List<&2, U32>}) ->
750 Laws.Success<Gradient.held(shape, contribution, gradient)>:
751 Core.Packed{+total_shape, total} = gradient
752 held_checked_success(shape, contribution, total_shape, total,
753 Layout.words_same(Shape.dimensions(total_shape), Shape.dimensions(shape)), {==}, fits, agrees)
754
755def agreed_success(+shape: Shape.Shape, slot: Gradient.Slot, contribution: Core.Dynamic,
756 -fits: Laws.Fits(shape, slot),
757 -agrees: {Totality.dimensions(contribution) == Shape.dimensions(shape) : List<&2, U32>}) ->
758 Laws.Success<Gradient.agreed(shape, slot, contribution)>:
759 match slot:
760 case Gradient.Unset{}:
761 Laws.Success{{==}}
762 case Gradient.Held{gradient}:
763 held_success(shape, contribution, gradient, fits, agrees)
764
765def checked_success(+shape: Shape.Shape, slot: Gradient.Slot, +contribution_shape: Shape.Shape, tensor: Core.Tensor<contribution_shape>, same: Bool,
766 -decided: {same == Layout.words_same(Shape.dimensions(contribution_shape), Shape.dimensions(shape)) : Bool},
767 -fits: Laws.Fits(shape, slot),
768 -agrees: {Shape.dimensions(contribution_shape) == Shape.dimensions(shape) : List<&2, U32>}) ->
769 Laws.Success<Gradient.checked(shape, slot, contribution_shape, tensor, same)>:
770 match same:
771 case False{}:
772 Laws.Success{Empty.absurd({False{} == True{} : Bool},
773 Arith.clash(Equal.trans(Bool, False{}, Layout.words_same(Shape.dimensions(contribution_shape), Shape.dimensions(shape)), True{}, decided,
774 %agrees : {Layout.words_same(Shape.dimensions(contribution_shape), _) == True{} : Bool}
775 TransformProof.words_same_refl(Shape.dimensions(contribution_shape)))))}
776 case True{}:
777 agreed_success(shape, slot, Core.Packed{contribution_shape, tensor}, fits, agrees)
778
779def Laws.accumulate_valid_success(shape, slot, contribution, fits, agrees):
780 Core.Packed{+contribution_shape, tensor} = contribution
781 checked_success(shape, slot, contribution_shape, tensor,
782 Layout.words_same(Shape.dimensions(contribution_shape), Shape.dimensions(shape)), {==}, fits, agrees)
783
784def accumulated_keeps(-slot: Gradient.Slot, -contribution: Core.Dynamic, outcome: Gradient.Outcome,
785 -successful: {Laws.accumulated(outcome) == True{} : Bool}) -> Holds<Laws.RefusalKeeps(slot, contribution, outcome)>:
786 match outcome:
787 case Gradient.Accumulated{after}:
788 Holds{Unit{}}
789 case Gradient.Refused{after, returned, error}:
790 Holds{Empty.absurd(Laws.RefusalKeeps(slot, contribution, Gradient.Refused{after, returned, error}), Arith.clash(successful))}
791
792def slot_kept(slot: Gradient.Slot) -> Holds<Laws.SlotKept(slot, slot)>:
793 match slot:
794 case Gradient.Unset{}:
795 Holds{{==}}
796 case Gradient.Held{gradient}:
797 Holds{({==}, index => {==})}
798
799def held_checked_refusal(+shape: Shape.Shape, contribution: Core.Dynamic, +total_shape: Shape.Shape, total: Core.Tensor<total_shape>, same: Bool,
800 -decided: {same == Layout.words_same(Shape.dimensions(total_shape), Shape.dimensions(shape)) : Bool},
801 -agrees: {Totality.dimensions(contribution) == Shape.dimensions(shape) : List<&2, U32>}) ->
802 Holds<Laws.RefusalKeeps(Gradient.Held{Core.Packed{total_shape, total}}, contribution, Gradient.held_checked(contribution, total_shape, total, same))>:
803 match same:
804 case False{}:
805 Holds{({==}, (property => {==}, ({==}, index => {==})))}
806 case True{}:
807 accumulated_keeps(Gradient.Held{Core.Packed{total_shape, total}}, contribution,
808 Gradient.loop(Shape.elements(total_shape), total_shape, 0n, Gradient.State{contribution, total}),
809 {\{Laws.Success: successful => successful} :
810 Laws.Success<Gradient.loop(Shape.elements(total_shape), total_shape, 0n, Gradient.State{contribution, total})> ->
811 {Laws.accumulated(Gradient.loop(Shape.elements(total_shape), total_shape, 0n, Gradient.State{contribution, total})) == True{} : Bool}}(
812 held_checked_success(shape, contribution, total_shape, total, True{}, decided,
813 {\{Holds: proof => proof} : Holds<{Shape.dimensions(total_shape) == Shape.dimensions(shape) : List<&2, U32>}> ->
814 {Shape.dimensions(total_shape) == Shape.dimensions(shape) : List<&2, U32>}}(words_dimensions(total_shape, shape, decided)),
815 agrees)))
816
817def held_refusal(+shape: Shape.Shape, contribution: Core.Dynamic, gradient: Core.Dynamic,
818 -agrees: {Totality.dimensions(contribution) == Shape.dimensions(shape) : List<&2, U32>}) ->
819 Holds<Laws.RefusalKeeps(Gradient.Held{gradient}, contribution, Gradient.held(shape, contribution, gradient))>:
820 Core.Packed{+total_shape, total} = gradient
821 held_checked_refusal(shape, contribution, total_shape, total,
822 Layout.words_same(Shape.dimensions(total_shape), Shape.dimensions(shape)), {==}, agrees)
823
824def agreed_refusal(+shape: Shape.Shape, slot: Gradient.Slot, contribution: Core.Dynamic,
825 -agrees: {Totality.dimensions(contribution) == Shape.dimensions(shape) : List<&2, U32>}) ->
826 Holds<Laws.RefusalKeeps(slot, contribution, Gradient.agreed(shape, slot, contribution))>:
827 match slot:
828 case Gradient.Unset{}:
829 Holds{Unit{}}
830 case Gradient.Held{gradient}:
831 held_refusal(shape, contribution, gradient, agrees)
832
833def checked_refusal(+shape: Shape.Shape, slot: Gradient.Slot, +contribution_shape: Shape.Shape, tensor: Core.Tensor<contribution_shape>, same: Bool,
834 -decided: {same == Layout.words_same(Shape.dimensions(contribution_shape), Shape.dimensions(shape)) : Bool}) ->
835 Holds<Laws.RefusalKeeps(slot, Core.Packed{contribution_shape, tensor}, Gradient.checked(shape, slot, contribution_shape, tensor, same))>:
836 match same:
837 case False{}:
838 Holds{({==}, (property => {==}, {\{Holds: proof => proof} : Holds<Laws.SlotKept(slot, slot)> -> Laws.SlotKept(slot, slot)}(slot_kept(slot))))}
839 case True{}:
840 agreed_refusal(shape, slot, Core.Packed{contribution_shape, tensor},
841 {\{Holds: proof => proof} : Holds<{Shape.dimensions(contribution_shape) == Shape.dimensions(shape) : List<&2, U32>}> ->
842 {Shape.dimensions(contribution_shape) == Shape.dimensions(shape) : List<&2, U32>}}(words_dimensions(contribution_shape, shape, decided)))
843
844def Laws.accumulate_refusal_keeps(shape, slot, contribution):
845 Core.Packed{+contribution_shape, tensor} = contribution
846 Laws.RefusalModel{
847 {\{Holds: proof => proof} :
848 Holds<Laws.RefusalKeeps(slot, Core.Packed{contribution_shape, tensor},
849 Gradient.checked(shape, slot, contribution_shape, tensor, Layout.words_same(Shape.dimensions(contribution_shape), Shape.dimensions(shape))))> ->
850 Laws.RefusalKeeps(slot, Core.Packed{contribution_shape, tensor}, Gradient.accumulate(shape, slot, Core.Packed{contribution_shape, tensor}))}(
851 checked_refusal(shape, slot, contribution_shape, tensor, Layout.words_same(Shape.dimensions(contribution_shape), Shape.dimensions(shape)), {==}))}
852
853def Laws.grad_unset_none():
854 {==}
855
856def Laws.grad_held_some(held):
857 {==}
858
859def Laws.reset_unset(slot):
860 {==}
861
862def reset_checked(+shape: Shape.Shape, +contribution_shape: Shape.Shape, tensor: Core.Tensor<contribution_shape>, same: Bool,
863 decided: {same == Layout.words_same(Shape.dimensions(contribution_shape), Shape.dimensions(shape)) : Bool},
864 agrees: {Shape.dimensions(contribution_shape) == Shape.dimensions(shape) : List<&2, U32>}) ->
865 {Gradient.checked(shape, Gradient.Unset{}, contribution_shape, tensor, same) ==
866 Gradient.Accumulated{Gradient.Held{Core.Packed{contribution_shape, tensor}}} : Gradient.Outcome}:
867 match same:
868 case False{}:
869 Empty.absurd({Gradient.checked(shape, Gradient.Unset{}, contribution_shape, tensor, False{}) ==
870 Gradient.Accumulated{Gradient.Held{Core.Packed{contribution_shape, tensor}}} : Gradient.Outcome},
871 Arith.clash(Equal.trans(Bool, False{}, Layout.words_same(Shape.dimensions(contribution_shape), Shape.dimensions(shape)), True{}, decided,
872 %agrees : {Layout.words_same(Shape.dimensions(contribution_shape), _) == True{} : Bool}
873 TransformProof.words_same_refl(Shape.dimensions(contribution_shape)))))
874 case True{}:
875 {==}
876
877def Laws.reset_then_accumulate_moves_in(shape, slot, contribution, agrees):
878 Core.Packed{+contribution_shape, tensor} = contribution
879 reset_checked(shape, contribution_shape, tensor, Layout.words_same(Shape.dimensions(contribution_shape), Shape.dimensions(shape)), {==}, agrees)
880
881def checked_wrong_shape(+shape: Shape.Shape, slot: Gradient.Slot, +contribution_shape: Shape.Shape,
882 tensor: Core.Tensor<contribution_shape>, flag: Bool,
883 decided: {flag == Layout.words_same(Shape.dimensions(contribution_shape), Shape.dimensions(shape)) : Bool},
884 differ: {Shape.dimensions(contribution_shape) != Shape.dimensions(shape) : List<&2, U32>}) ->
885 {Gradient.checked(shape, slot, contribution_shape, tensor, flag) ==
886 Gradient.Refused{slot, Core.Packed{contribution_shape, tensor}, Gradient.ShapeMismatch{}} : Gradient.Outcome}:
887 match flag:
888 case False{}:
889 {==}
890 case True{}:
891 Empty.absurd({Gradient.checked(shape, slot, contribution_shape, tensor, True{}) ==
892 Gradient.Refused{slot, Core.Packed{contribution_shape, tensor}, Gradient.ShapeMismatch{}} : Gradient.Outcome},
893 differ(TransformProof.words_equal(Shape.dimensions(contribution_shape), Shape.dimensions(shape), decided)))
894
895def Laws.accumulate_wrong_shape_refused(shape, slot, contribution, differ):
896 Core.Packed{+contribution_shape, tensor} = contribution
897 checked_wrong_shape(shape, slot, contribution_shape, tensor,
898 Layout.words_same(Shape.dimensions(contribution_shape), Shape.dimensions(shape)), {==}, differ)