src/autograd/tensor_chain_PROOF.bend

bendtorch-core@0.1.0.0 · 631 lines · 47 definitions

1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
4import bendtorch-core@0.1.0.0/src/autograd/gradient.bend as Gradient
5import bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend as Backward
6import bendtorch-core@0.1.0.0/src/autograd/tensor_chain_LAWS.bend as Laws
7
8# What the pull side holds for a push-side list of pending slots: each pending
9# slot x, the one with k older slots, is what take gathers for id k from the
10# log into the starting slot w, and the rest of the log serves the older slots.
11# Every witness is erased; only the equations are evidence.
12type Cell<-x: Gradient.Slot, -rest: List<&1, Gradient.Slot>, -slots: List<&1, Gradient.Slot>, -below: Nat, -log: Laws.Log()> is Data:
13  Cell{-w: Gradient.Slot, -older: List<&1, Gradient.Slot>, -left: Laws.Log(),
14    at: {slots == w <> older : List<&1, Gradient.Slot>},
15    took: {Laws.take(log, below, w) == (Done{x}, left) : Laws.Taken()},
16    tail: Pulls(rest, older, below, left)}
17
18def Pulls(pending: List<&1, Gradient.Slot>, -slots: List<&1, Gradient.Slot>, +count: Nat, -log: Laws.Log()) -> Data:
19  match pending count:
20    case Nil{} count:
21      {slots == Nil{} : List<&1, Gradient.Slot>}
22    case Con{x, rest} 0n:
23      {slots == x <> rest : List<&1, Gradient.Slot>}
24    case Con{x, rest} 1n+below:
25      Cell<x, rest, slots, below, log>
26
27# With no entry left, the pull side gathers exactly the pending slots.
28def gathered(pending: List<&1, Gradient.Slot>, +count: Nat, -slots: List<&1, Gradient.Slot>, -log: Laws.Log(),
29  pulls: Pulls(pending, slots, count, log)) -> {Laws.gather(slots, count, log) == Done{pending} : Laws.Slots()}:
30  match pending count:
31    case Nil{} count:
32      %Equal.sym(List<&1, Gradient.Slot>, slots, Nil{}, pulls) : {Laws.gather(_, count, log) == Done{Nil{}} : Laws.Slots()}
33      {==}
34    case Con{x, rest} 0n:
35      %Equal.sym(List<&1, Gradient.Slot>, slots, x <> rest, pulls) : {Laws.gather(_, 0n, log) == Done{x <> rest} : Laws.Slots()}
36      {==}
37    case Con{x, rest} 1n+below:
38      Cell{w, older, left, at, took, tail} = pulls
39      %Equal.sym(List<&1, Gradient.Slot>, slots, w <> older, at) : {Laws.gather(_, 1n+below, log) == Done{x <> rest} : Laws.Slots()}
40      %Equal.sym(Laws.Taken(), Laws.take(log, below, w), (Done{x}, left), took) :
41        {Laws.gather_step(_, more => Laws.gather(older, below, more)) == Done{x <> rest} : Laws.Slots()}
42      Equal.cong(Laws.Slots(), Laws.Slots(), result => Backward.prepend(Gradient.Slot, x, result),
43        Laws.gather(older, below, left), Done{rest}, gathered(rest, below, older, left, tail))
44
45# The starting slots, handed back, with the pull side of an empty log.
46type Started<-pending: List<&1, Gradient.Slot>, -count: Nat> is Type:
47  Started{copy: List<&1, Gradient.Slot>, same: {copy == pending : List<&1, Gradient.Slot>},
48    pulls: Pulls(copy, pending, count, Nil{})}
49
50def restarted(x: Gradient.Slot, -rest: List<&1, Gradient.Slot>, +below: Nat, out: Started<rest, below>) ->
51  Started<x <> rest, 1n+below>:
52  Started{copy, same, pulls} = out
53  Started{x <> copy, Equal.cong(List<&1, Gradient.Slot>, List<&1, Gradient.Slot>, more => x <> more, copy, rest, same),
54    Cell{x, rest, Nil{}, {==}, {==}, pulls}}
55
56def started(pending: List<&1, Gradient.Slot>, +count: Nat) -> Started<pending, count>:
57  match pending count:
58    case Nil{} count:
59      Started{Nil{}, {==}, {==}}
60    case Con{x, rest} 0n:
61      Started{x <> rest, {==}, {==}}
62    case Con{x, rest} 1n+below:
63      restarted(x, rest, below, started(rest, below))
64
65def Pushed(state: Laws.Slots(), -slots: List<&1, Gradient.Slot>, +count: Nat, -log: Laws.Log()) -> Data:
66  match state:
67    case Fail{error}:
68      Unit
69    case Done{pending}:
70      Pulls(pending, slots, count, log)
71
72# One contribution bumped into the push side, the new state handed back.
73type Bumped<-pending: List<&1, Gradient.Slot>, -count: Nat, -target: Nat, -shape: Shape.Shape, -gradient: Core.Dynamic, -same: Bool,
74  -slots: List<&1, Gradient.Slot>, -log: Laws.Log()> is Type:
75  Bumped{state: Laws.Slots(), bumped: {state == Backward.bump(pending, count, target, shape, gradient, same) : Laws.Slots()},
76    pushed: Pushed(state, slots, count, Backward.Contribution{target, shape, gradient} <> log)}
77
78type Hit<-outcome: Gradient.Outcome, -rest: List<&1, Gradient.Slot>, -below: Nat, -target: Nat, -shape: Shape.Shape, -gradient: Core.Dynamic,
79  -slots: List<&1, Gradient.Slot>, -log: Laws.Log()> is Type:
80  Hit{state: Laws.Slots(), placed: {state == Backward.placed(rest, outcome) : Laws.Slots()},
81    pushed: Pushed(state, slots, 1n+below, Backward.Contribution{target, shape, gradient} <> log)}
82
83def hit(outcome: Gradient.Outcome, rest: List<&1, Gradient.Slot>, +below: Nat, +target: Nat, +shape: Shape.Shape, -gradient: Core.Dynamic,
84  -slots: List<&1, Gradient.Slot>, -log: Laws.Log(), -w: Gradient.Slot, -older: List<&1, Gradient.Slot>, -left: Laws.Log(),
85  at: {slots == w <> older : List<&1, Gradient.Slot>}, tail: Pulls(rest, older, below, left),
86  took: {Laws.take(Backward.Contribution{target, shape, gradient} <> log, below, w) == (Laws.settled(outcome), left) : Laws.Taken()}) ->
87  Hit<outcome, rest, below, target, shape, gradient, slots, log>:
88  match outcome:
89    case Gradient.Accumulated{slot}:
90      Hit{Done{slot <> rest}, {==}, Cell{w, older, left, at, took, tail}}
91    case Gradient.Refused{slot, contribution, error}:
92      Hit{Fail{Backward.GradientError{error}}, {==}, Unit{}}
93
94def hit_bumped(-x: Gradient.Slot, -rest: List<&1, Gradient.Slot>, +below: Nat, +target: Nat, +shape: Shape.Shape, -gradient: Core.Dynamic,
95  -slots: List<&1, Gradient.Slot>, -log: Laws.Log(), out: Hit<Gradient.accumulate(shape, x, gradient), rest, below, target, shape, gradient, slots, log>) ->
96  Bumped<x <> rest, 1n+below, target, shape, gradient, True{}, slots, log>:
97  Hit{state, placed, pushed} = out
98  Bumped{state, placed, pushed}
99
100def took_hit(+below: Nat, +target: Nat, +shape: Shape.Shape, -gradient: Core.Dynamic, -log: Laws.Log(), -w: Gradient.Slot,
101  -x: Gradient.Slot, -left: Laws.Log(), took: {Laws.take(log, below, w) == (Done{x}, left) : Laws.Taken()},
102  decided: {Nat.is_eq(below, target) == True{} : Bool}) ->
103  {Laws.take(Backward.Contribution{target, shape, gradient} <> log, below, w) == (Laws.settled(Gradient.accumulate(shape, x, gradient)), left) : Laws.Taken()}:
104  %Equal.sym(Bool, Nat.is_eq(below, target), True{}, decided) :
105    {Laws.sorted(target, shape, gradient, _, Laws.take(log, below, w)) == (Laws.settled(Gradient.accumulate(shape, x, gradient)), left) : Laws.Taken()}
106  %Equal.sym(Laws.Taken(), Laws.take(log, below, w), (Done{x}, left), took) :
107    {Laws.sorted(target, shape, gradient, True{}, _) == (Laws.settled(Gradient.accumulate(shape, x, gradient)), left) : Laws.Taken()}
108  {==}
109
110def took_miss(+below: Nat, +target: Nat, +shape: Shape.Shape, -gradient: Core.Dynamic, -log: Laws.Log(), -w: Gradient.Slot,
111  -x: Gradient.Slot, -left: Laws.Log(), took: {Laws.take(log, below, w) == (Done{x}, left) : Laws.Taken()},
112  decided: {Nat.is_eq(below, target) == False{} : Bool}) ->
113  {Laws.take(Backward.Contribution{target, shape, gradient} <> log, below, w) == (Done{x}, Backward.Contribution{target, shape, gradient} <> left) : Laws.Taken()}:
114  %Equal.sym(Bool, Nat.is_eq(below, target), False{}, decided) :
115    {Laws.sorted(target, shape, gradient, _, Laws.take(log, below, w)) == (Done{x}, Backward.Contribution{target, shape, gradient} <> left) : Laws.Taken()}
116  %Equal.sym(Laws.Taken(), Laws.take(log, below, w), (Done{x}, left), took) :
117    {Laws.sorted(target, shape, gradient, False{}, _) == (Done{x}, Backward.Contribution{target, shape, gradient} <> left) : Laws.Taken()}
118  {==}
119
120def missed(x: Gradient.Slot, -rest: List<&1, Gradient.Slot>, +below: Nat, +target: Nat, +shape: Shape.Shape, -gradient: Core.Dynamic,
121  -slots: List<&1, Gradient.Slot>, -log: Laws.Log(), -w: Gradient.Slot, -older: List<&1, Gradient.Slot>, -left: Laws.Log(),
122  at: {slots == w <> older : List<&1, Gradient.Slot>},
123  took: {Laws.take(Backward.Contribution{target, shape, gradient} <> log, below, w) == (Done{x}, Backward.Contribution{target, shape, gradient} <> left) : Laws.Taken()},
124  out: Bumped<rest, below, target, shape, gradient, Backward.at_head(below, target), older, left>) ->
125  Bumped<x <> rest, 1n+below, target, shape, gradient, False{}, slots, log>:
126  Bumped{state, bumped, pushed} = out
127  match state:
128    case Fail{error}:
129      Bumped{Fail{error}, Equal.cong(Laws.Slots(), Laws.Slots(), result => Backward.prepend(Gradient.Slot, x, result), Fail{error},
130        Backward.bump(rest, below, target, shape, gradient, Backward.at_head(below, target)), bumped), Unit{}}
131    case Done{pending}:
132      Bumped{Done{x <> pending}, Equal.cong(Laws.Slots(), Laws.Slots(), result => Backward.prepend(Gradient.Slot, x, result), Done{pending},
133        Backward.bump(rest, below, target, shape, gradient, Backward.at_head(below, target)), bumped),
134        Cell{w, older, Backward.Contribution{target, shape, gradient} <> left, at, took, pushed}}
135
136# Bumping a contribution into the push side keeps the pull side in step, with
137# the contribution at the head of the log.
138def bump_pulls(pending: List<&1, Gradient.Slot>, +count: Nat, +target: Nat, +shape: Shape.Shape, gradient: Core.Dynamic, same: Bool,
139  -slots: List<&1, Gradient.Slot>, -log: Laws.Log(), pulls: Pulls(pending, slots, count, log),
140  decided: {Backward.at_head(count, target) == same : Bool}) -> Bumped<pending, count, target, shape, gradient, same, slots, log>:
141  match pending count same:
142    case Nil{} count same:
143      Bumped{Done{Nil{}}, {==}, pulls}
144    case Con{x, rest} 0n same:
145      Bumped{Done{x <> rest}, {==}, pulls}
146    case Con{x, rest} 1n+below True{}:
147      Cell{w, older, left, at, took, tail} = pulls
148      hit_bumped(x, rest, below, target, shape, gradient, slots, log,
149        hit(Gradient.accumulate(shape, x, gradient), rest, below, target, shape, gradient, slots, log, w, older, left, at, tail,
150          took_hit(below, target, shape, gradient, log, w, x, left, took, decided)))
151    case Con{x, rest} 1n+below False{}:
152      Cell{w, older, left, at, took, tail} = pulls
153      missed(x, rest, below, target, shape, gradient, slots, log, w, older, left, at,
154        took_miss(below, target, shape, gradient, log, w, x, left, took, decided),
155        bump_pulls(rest, below, target, shape, gradient, Backward.at_head(below, target), older, left, tail, {==}))
156
157# A whole list of contributions delivered into any push-side state.
158type Delivered<-items: Laws.Log(), -state: Laws.Slots(), -count: Nat, -slots: List<&1, Gradient.Slot>, -log: Laws.Log()> is Type:
159  Delivered{after: Laws.Slots(), delivered: {after == Backward.deliver(items, count, state) : Laws.Slots()},
160    pushed: Pushed(after, slots, count, List.reverse.go(&1, Backward.Contribution, items, log))}
161
162def relay(-rest: Laws.Log(), +count: Nat, +target: Nat, +shape: Shape.Shape, -gradient: Core.Dynamic, -pending: List<&1, Gradient.Slot>,
163  -slots: List<&1, Gradient.Slot>, -log: Laws.Log(), -state: Laws.Slots(),
164  bumped: {state == Backward.bump(pending, count, target, shape, gradient, Backward.at_head(count, target)) : Laws.Slots()},
165  out: Delivered<rest, state, count, slots, Backward.Contribution{target, shape, gradient} <> log>) ->
166  Delivered<Backward.Contribution{target, shape, gradient} <> rest, Done{pending}, count, slots, log>:
167  Delivered{after, delivered, pushed} = out
168  Delivered{after, Equal.trans(Laws.Slots(), after, Backward.deliver(rest, count, state),
169    Backward.deliver(rest, count, Backward.bump(pending, count, target, shape, gradient, Backward.at_head(count, target))), delivered,
170    Equal.cong(Laws.Slots(), Laws.Slots(), result => Backward.deliver(rest, count, result), state,
171      Backward.bump(pending, count, target, shape, gradient, Backward.at_head(count, target)), bumped)), pushed}
172
173def rebump(-rest: Laws.Log(), +count: Nat, +target: Nat, +shape: Shape.Shape, -gradient: Core.Dynamic, -pending: List<&1, Gradient.Slot>,
174  -slots: List<&1, Gradient.Slot>, -log: Laws.Log(),
175  out: Bumped<pending, count, target, shape, gradient, Backward.at_head(count, target), slots, log>,
176  ih: @state: Laws.Slots() -> @-slots2: List<&1, Gradient.Slot> -> @-log2: Laws.Log() -> @pushed2: Pushed(state, slots2, count, log2) ->
177    Delivered<rest, state, count, slots2, log2>) ->
178  Delivered<Backward.Contribution{target, shape, gradient} <> rest, Done{pending}, count, slots, log>:
179  Bumped{state, bumped, pushed} = out
180  relay(rest, count, target, shape, gradient, pending, slots, log, state, bumped,
181    ih(state, slots, Backward.Contribution{target, shape, gradient} <> log, pushed))
182
183def delivered(items: Laws.Log(), state: Laws.Slots(), +count: Nat, -slots: List<&1, Gradient.Slot>, -log: Laws.Log(),
184  pushed: Pushed(state, slots, count, log)) -> Delivered<items, state, count, slots, log>:
185  match items state:
186    case Nil{} state:
187      Delivered{state, {==}, pushed}
188    case Con{Backward.Contribution{+target, +shape, gradient}, rest} Fail{error}:
189      Delivered{Fail{error}, {==}, Unit{}}
190    case Con{Backward.Contribution{+target, +shape, gradient}, rest} Done{pending}:
191      rebump(rest, count, target, shape, gradient, pending, slots, log,
192        bump_pulls(pending, count, target, shape, gradient, Backward.at_head(count, target), slots, log, pushed, {==}),
193        after => slots2 => log2 => pushed2 => delivered(rest, after, count, slots2, log2, pushed2))
194
195# What a sweep from a push-side state does, with the pull side's answer when
196# it succeeds: done and gradients are the sweep's own outputs.
197type Stop<-entries: List<&1, Backward.Entry>, -error: Backward.Error, -count: Nat> is Data:
198  Stop{-done: List<&1, Backward.Entry>, swept: {Backward.sweep(entries, Fail{error}, count) == (done, Fail{error}) : Backward.Swept()}}
199
200type Run<-entries: List<&1, Backward.Entry>, -pending: List<&1, Gradient.Slot>, -count: Nat, -slots: List<&1, Gradient.Slot>, -log: Laws.Log()> is Data:
201  Kept{-done: List<&1, Backward.Entry>, -gradients: List<&1, Gradient.Slot>,
202    swept: {Backward.sweep(entries, Done{pending}, count) == (done, Done{gradients}) : Backward.Swept()},
203    pulled: {Laws.chained(entries, slots, count, log) == Done{gradients} : Laws.Slots()}}
204  Stopped{-done: List<&1, Backward.Entry>, -error: Backward.Error,
205    swept: {Backward.sweep(entries, Done{pending}, count) == (done, Fail{error}) : Backward.Swept()}}
206
207def Out(-entries: List<&1, Backward.Entry>, state: Laws.Slots(), +count: Nat, -slots: List<&1, Gradient.Slot>, -log: Laws.Log()) -> Data:
208  match state:
209    case Fail{error}:
210      Stop<entries, error, count>
211    case Done{pending}:
212      Run<entries, pending, count, slots, log>
213
214# The same for the entry whose VJP pass is known.
215type Fired<-node: Backward.Node, -shape: Shape.Shape, -value: Core.Dynamic, -slot: Gradient.Slot, -rest: List<&1, Backward.Entry>,
216  -more: List<&1, Gradient.Slot>, -below: Nat, -older: List<&1, Gradient.Slot>, -left: Laws.Log(), -pass: Backward.Pass> is Data:
217  FiredKept{-done: List<&1, Backward.Entry>, -gradients: List<&1, Gradient.Slot>,
218    swept: {Backward.passed(node, shape, value, slot, below, more, state => Backward.sweep(rest, state, below), pass) ==
219      (done, Done{gradients}) : Backward.Swept()},
220    pulled: {Laws.fired(pass, left, next => Laws.chained(rest, older, below, next)) == Done{gradients} : Laws.Slots()}}
221  FiredStopped{-done: List<&1, Backward.Entry>, -error: Backward.Error,
222    swept: {Backward.passed(node, shape, value, slot, below, more, state => Backward.sweep(rest, state, below), pass) ==
223      (done, Fail{error}) : Backward.Swept()}}
224
225def fired_stop(+node: Backward.Node, +shape: Shape.Shape, -value: Core.Dynamic, -saved: Backward.Saved, -slot: Gradient.Slot,
226  -g: Core.Dynamic, -rest: List<&1, Backward.Entry>, -more: List<&1, Gradient.Slot>, +below: Nat, -older: List<&1, Gradient.Slot>,
227  -left: Laws.Log(), -items: Laws.Log(), -error: Backward.Error,
228  delivered: {Fail{error} == Backward.deliver(items, below, Done{more}) : Laws.Slots()}, out: Stop<rest, error, below>) ->
229  Fired<node, shape, value, slot, rest, more, below, older, left, Backward.Pass{saved, g, Done{items}}>:
230  Stop{done, swept} = out
231  FiredStopped{Backward.Entry{node, shape, value, saved, slot} <> done, error,
232    Equal.trans(Backward.Swept(),
233      Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g},
234        Backward.sweep(rest, Backward.deliver(items, below, Done{more}), below)),
235      Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g}, Backward.sweep(rest, Fail{error}, below)),
236      Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g}, (done, Fail{error})),
237      Equal.cong(Laws.Slots(), Backward.Swept(),
238        state => Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g}, Backward.sweep(rest, state, below)),
239        Backward.deliver(items, below, Done{more}), Fail{error}, Equal.sym(Laws.Slots(), Fail{error}, Backward.deliver(items, below, Done{more}), delivered)),
240      Equal.cong(Backward.Swept(), Backward.Swept(),
241        pair => Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g}, pair),
242        Backward.sweep(rest, Fail{error}, below), (done, Fail{error}), swept))}
243
244def fired_go(+node: Backward.Node, +shape: Shape.Shape, -value: Core.Dynamic, -saved: Backward.Saved, -slot: Gradient.Slot,
245  -g: Core.Dynamic, -rest: List<&1, Backward.Entry>, -more: List<&1, Gradient.Slot>, +below: Nat, -older: List<&1, Gradient.Slot>,
246  -left: Laws.Log(), -items: Laws.Log(), -pending: List<&1, Gradient.Slot>,
247  delivered: {Done{pending} == Backward.deliver(items, below, Done{more}) : Laws.Slots()},
248  out: Run<rest, pending, below, older, List.reverse.go(&1, Backward.Contribution, items, left)>) ->
249  Fired<node, shape, value, slot, rest, more, below, older, left, Backward.Pass{saved, g, Done{items}}>:
250  match out:
251    case Kept{done, gradients, swept, pulled}:
252      FiredKept{Backward.Entry{node, shape, value, saved, slot} <> done, Gradient.Held{g} <> gradients,
253        Equal.trans(Backward.Swept(),
254          Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g},
255            Backward.sweep(rest, Backward.deliver(items, below, Done{more}), below)),
256          Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g}, Backward.sweep(rest, Done{pending}, below)),
257          Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g}, (done, Done{gradients})),
258          Equal.cong(Laws.Slots(), Backward.Swept(),
259            state => Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g}, Backward.sweep(rest, state, below)),
260            Backward.deliver(items, below, Done{more}), Done{pending},
261            Equal.sym(Laws.Slots(), Done{pending}, Backward.deliver(items, below, Done{more}), delivered)),
262          Equal.cong(Backward.Swept(), Backward.Swept(),
263            pair => Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g}, pair),
264            Backward.sweep(rest, Done{pending}, below), (done, Done{gradients}), swept)),
265        Equal.cong(Laws.Slots(), Laws.Slots(), result => Backward.prepend(Gradient.Slot, Gradient.Held{g}, result),
266          Laws.chained(rest, older, below, List.reverse.go(&1, Backward.Contribution, items, left)), Done{gradients}, pulled)}
267    case Stopped{done, error, swept}:
268      FiredStopped{Backward.Entry{node, shape, value, saved, slot} <> done, error,
269        Equal.trans(Backward.Swept(),
270          Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g},
271            Backward.sweep(rest, Backward.deliver(items, below, Done{more}), below)),
272          Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g}, Backward.sweep(rest, Done{pending}, below)),
273          Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g}, (done, Fail{error})),
274          Equal.cong(Laws.Slots(), Backward.Swept(),
275            state => Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g}, Backward.sweep(rest, state, below)),
276            Backward.deliver(items, below, Done{more}), Done{pending},
277            Equal.sym(Laws.Slots(), Done{pending}, Backward.deliver(items, below, Done{more}), delivered)),
278          Equal.cong(Backward.Swept(), Backward.Swept(),
279            pair => Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g}, pair),
280            Backward.sweep(rest, Done{pending}, below), (done, Fail{error}), swept))}
281
282def fail_fired(+node: Backward.Node, +shape: Shape.Shape, -value: Core.Dynamic, -saved: Backward.Saved, -slot: Gradient.Slot,
283  -g: Core.Dynamic, -rest: List<&1, Backward.Entry>, -more: List<&1, Gradient.Slot>, +below: Nat, -older: List<&1, Gradient.Slot>,
284  -left: Laws.Log(), -error: Backward.Error, out: Stop<rest, error, below>) ->
285  Fired<node, shape, value, slot, rest, more, below, older, left, Backward.Pass{saved, g, Fail{error}}>:
286  Stop{done, swept} = out
287  FiredStopped{Backward.Entry{node, shape, value, saved, slot} <> done, error,
288    Equal.cong(Backward.Swept(), Backward.Swept(),
289      pair => Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Held{g}, pair),
290      Backward.sweep(rest, Fail{error}, below), (done, Fail{error}), swept)}
291
292def done_fired(+node: Backward.Node, +shape: Shape.Shape, -value: Core.Dynamic, -saved: Backward.Saved, -slot: Gradient.Slot,
293  -g: Core.Dynamic, -rest: List<&1, Backward.Entry>, -more: List<&1, Gradient.Slot>, +below: Nat, -older: List<&1, Gradient.Slot>,
294  -left: Laws.Log(), -items: Laws.Log(), sent: Delivered<items, Done{more}, below, older, left>,
295  ih: @state: Laws.Slots() -> @-slots2: List<&1, Gradient.Slot> -> @+count2: Nat -> @-log2: Laws.Log() ->
296    @pushed2: Pushed(state, slots2, count2, log2) -> Out(rest, state, count2, slots2, log2)) ->
297  Fired<node, shape, value, slot, rest, more, below, older, left, Backward.Pass{saved, g, Done{items}}>:
298  Delivered{after, delivered, pushed} = sent
299  match after:
300    case Fail{error}:
301      fired_stop(node, shape, value, saved, slot, g, rest, more, below, older, left, items, error, delivered,
302        ih(Fail{error}, older, below, List.reverse.go(&1, Backward.Contribution, items, left), pushed))
303    case Done{pending}:
304      fired_go(node, shape, value, saved, slot, g, rest, more, below, older, left, items, pending, delivered,
305        ih(Done{pending}, older, below, List.reverse.go(&1, Backward.Contribution, items, left), pushed))
306
307def held_step(+node: Backward.Node, +shape: Shape.Shape, -value: Core.Dynamic, -slot: Gradient.Slot, -rest: List<&1, Backward.Entry>,
308  more: List<&1, Gradient.Slot>, +below: Nat, -older: List<&1, Gradient.Slot>, -left: Laws.Log(), tail: Pulls(more, older, below, left),
309  pass: Backward.Pass,
310  ih: @state: Laws.Slots() -> @-slots2: List<&1, Gradient.Slot> -> @+count2: Nat -> @-log2: Laws.Log() ->
311    @pushed2: Pushed(state, slots2, count2, log2) -> Out(rest, state, count2, slots2, log2)) ->
312  Fired<node, shape, value, slot, rest, more, below, older, left, pass>:
313  Backward.Pass{saved, g, contributions} = pass
314  match contributions:
315    case Fail{error}:
316      fail_fired(node, shape, value, saved, slot, g, rest, more, below, older, left, error, ih(Fail{error}, older, below, left, Unit{}))
317    case Done{items}:
318      done_fired(node, shape, value, saved, slot, g, rest, more, below, older, left, items,
319        delivered(items, Done{more}, below, older, left, tail), ih)
320
321def unset_step(+node: Backward.Node, +shape: Shape.Shape, -value: Core.Dynamic, -saved: Backward.Saved, -slot: Gradient.Slot,
322  -rest: List<&1, Backward.Entry>, -more: List<&1, Gradient.Slot>, +below: Nat, -slots: List<&1, Gradient.Slot>, -log: Laws.Log(),
323  -w: Gradient.Slot, -older: List<&1, Gradient.Slot>, -left: Laws.Log(),
324  at: {slots == w <> older : List<&1, Gradient.Slot>}, took: {Laws.take(log, below, w) == (Done{Gradient.Unset{}}, left) : Laws.Taken()},
325  out: Run<rest, more, below, older, left>) ->
326  Run<Backward.Entry{node, shape, value, saved, slot} <> rest, Gradient.Unset{} <> more, 1n+below, slots, log>:
327  match out:
328    case Kept{done, gradients, swept, pulled}:
329      Kept{Backward.Entry{node, shape, value, saved, slot} <> done, Gradient.Unset{} <> gradients,
330        Equal.cong(Backward.Swept(), Backward.Swept(),
331          pair => Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Unset{}, pair),
332          Backward.sweep(rest, Done{more}, below), (done, Done{gradients}), swept),
333        Equal.trans(Laws.Slots(), Laws.chained(Backward.Entry{node, shape, value, saved, slot} <> rest, slots, 1n+below, log),
334          Laws.chained(Backward.Entry{node, shape, value, saved, slot} <> rest, w <> older, 1n+below, log),
335          Done{Gradient.Unset{} <> gradients},
336          Equal.cong(List<&1, Gradient.Slot>, Laws.Slots(),
337            list => Laws.chained(Backward.Entry{node, shape, value, saved, slot} <> rest, list, 1n+below, log), slots, w <> older, at),
338          Equal.trans(Laws.Slots(), Laws.reached(node, saved, Laws.take(log, below, w), next => Laws.chained(rest, older, below, next)),
339            Laws.reached(node, saved, (Done{Gradient.Unset{}}, left), next => Laws.chained(rest, older, below, next)),
340            Done{Gradient.Unset{} <> gradients},
341            Equal.cong(Laws.Taken(), Laws.Slots(), taken => Laws.reached(node, saved, taken, next => Laws.chained(rest, older, below, next)),
342              Laws.take(log, below, w), (Done{Gradient.Unset{}}, left), took),
343            Equal.cong(Laws.Slots(), Laws.Slots(), result => Backward.prepend(Gradient.Slot, Gradient.Unset{}, result),
344              Laws.chained(rest, older, below, left), Done{gradients}, pulled)))}
345    case Stopped{done, error, swept}:
346      Stopped{Backward.Entry{node, shape, value, saved, slot} <> done, error,
347        Equal.cong(Backward.Swept(), Backward.Swept(),
348          pair => Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Unset{}, pair),
349          Backward.sweep(rest, Done{more}, below), (done, Fail{error}), swept)}
350
351def fired_run(+node: Backward.Node, +shape: Shape.Shape, -value: Core.Dynamic, -saved: Backward.Saved, -slot: Gradient.Slot,
352  -rest: List<&1, Backward.Entry>, -g: Core.Dynamic, -more: List<&1, Gradient.Slot>, +below: Nat, -slots: List<&1, Gradient.Slot>,
353  -log: Laws.Log(), -w: Gradient.Slot, -older: List<&1, Gradient.Slot>, -left: Laws.Log(),
354  at: {slots == w <> older : List<&1, Gradient.Slot>}, took: {Laws.take(log, below, w) == (Done{Gradient.Held{g}}, left) : Laws.Taken()},
355  out: Fired<node, shape, value, slot, rest, more, below, older, left, Backward.vjp(node, saved, g)>) ->
356  Run<Backward.Entry{node, shape, value, saved, slot} <> rest, Gradient.Held{g} <> more, 1n+below, slots, log>:
357  match out:
358    case FiredKept{done, gradients, swept, pulled}:
359      Kept{done, gradients, swept,
360        Equal.trans(Laws.Slots(), Laws.chained(Backward.Entry{node, shape, value, saved, slot} <> rest, slots, 1n+below, log),
361          Laws.chained(Backward.Entry{node, shape, value, saved, slot} <> rest, w <> older, 1n+below, log),
362          Done{gradients},
363          Equal.cong(List<&1, Gradient.Slot>, Laws.Slots(),
364            list => Laws.chained(Backward.Entry{node, shape, value, saved, slot} <> rest, list, 1n+below, log), slots, w <> older, at),
365          Equal.trans(Laws.Slots(), Laws.reached(node, saved, Laws.take(log, below, w), next => Laws.chained(rest, older, below, next)),
366            Laws.reached(node, saved, (Done{Gradient.Held{g}}, left), next => Laws.chained(rest, older, below, next)),
367            Done{gradients},
368            Equal.cong(Laws.Taken(), Laws.Slots(), taken => Laws.reached(node, saved, taken, next => Laws.chained(rest, older, below, next)),
369              Laws.take(log, below, w), (Done{Gradient.Held{g}}, left), took),
370            pulled))}
371    case FiredStopped{done, error, swept}:
372      Stopped{done, error, swept}
373
374def slot_step(+node: Backward.Node, +shape: Shape.Shape, -value: Core.Dynamic, saved: Backward.Saved, -slot: Gradient.Slot,
375  -rest: List<&1, Backward.Entry>, x: Gradient.Slot, more: List<&1, Gradient.Slot>, +below: Nat, -slots: List<&1, Gradient.Slot>,
376  -log: Laws.Log(), pushed: Cell<x, more, slots, below, log>,
377  ih: @state: Laws.Slots() -> @-slots2: List<&1, Gradient.Slot> -> @+count2: Nat -> @-log2: Laws.Log() ->
378    @pushed2: Pushed(state, slots2, count2, log2) -> Out(rest, state, count2, slots2, log2)) ->
379  Run<Backward.Entry{node, shape, value, saved, slot} <> rest, x <> more, 1n+below, slots, log>:
380  match x:
381    case Gradient.Unset{}:
382      Cell{w, older, left, at, took, tail} = pushed
383      unset_step(node, shape, value, saved, slot, rest, more, below, slots, log, w, older, left, at, took,
384        ih(Done{more}, older, below, left, tail))
385    case Gradient.Held{g}:
386      Cell{w, older, left, at, took, tail} = pushed
387      fired_run(node, shape, value, saved, slot, rest, g, more, below, slots, log, w, older, left, at, took,
388        held_step(node, shape, value, slot, rest, more, below, older, left, tail, Backward.vjp(node, saved, g), ih))
389
390def stepped(+node: Backward.Node, +shape: Shape.Shape, -value: Core.Dynamic, saved: Backward.Saved, -slot: Gradient.Slot,
391  -rest: List<&1, Backward.Entry>, pending: List<&1, Gradient.Slot>, +count: Nat, -slots: List<&1, Gradient.Slot>, -log: Laws.Log(),
392  pushed: Pulls(pending, slots, count, log),
393  ih: @state: Laws.Slots() -> @-slots2: List<&1, Gradient.Slot> -> @+count2: Nat -> @-log2: Laws.Log() ->
394    @pushed2: Pushed(state, slots2, count2, log2) -> Out(rest, state, count2, slots2, log2)) ->
395  Run<Backward.Entry{node, shape, value, saved, slot} <> rest, pending, count, slots, log>:
396  match pending count:
397    case Nil{} count:
398      Kept{Backward.Entry{node, shape, value, saved, slot} <> rest, Nil{}, {==},
399        Equal.cong(List<&1, Gradient.Slot>, Laws.Slots(),
400          list => Laws.chained(Backward.Entry{node, shape, value, saved, slot} <> rest, list, count, log), slots, Nil{}, pushed)}
401    case Con{x, more} 0n:
402      Kept{Backward.Entry{node, shape, value, saved, slot} <> rest, Nil{}, {==},
403        Equal.cong(List<&1, Gradient.Slot>, Laws.Slots(),
404          list => Laws.chained(Backward.Entry{node, shape, value, saved, slot} <> rest, list, 0n, log), slots, x <> more, pushed)}
405    case Con{x, more} 1n+below:
406      slot_step(node, shape, value, saved, slot, rest, x, more, below, slots, log, pushed, ih)
407
408# The sweep from any push-side state, in step with the pull side.
409def swept_pulls(entries: List<&1, Backward.Entry>, state: Laws.Slots(), -slots: List<&1, Gradient.Slot>, +count: Nat, -log: Laws.Log(),
410  pushed: Pushed(state, slots, count, log)) -> Out(entries, state, count, slots, log):
411  match entries state:
412    case Nil{} Fail{error}:
413      Stop{Nil{}, {==}}
414    case Nil{} Done{pending}:
415      Kept{Nil{}, pending, {==}, gathered(pending, count, slots, log, pushed)}
416    case Con{Backward.Entry{+node, +shape, value, saved, slot}, rest} Fail{error}:
417      Stop{Backward.Entry{node, shape, value, saved, slot} <> rest, {==}}
418    case Con{Backward.Entry{+node, +shape, value, saved, slot}, rest} Done{pending}:
419      stepped(node, shape, value, saved, slot, rest, pending, count, slots, log, pushed,
420        after => slots2 => count2 => log2 => pushed2 => swept_pulls(rest, after, slots2, count2, log2, pushed2))
421
422def is_done(result: Laws.Slots()) -> Type:
423  match result:
424    case Fail{error}:
425      Empty
426    case Done{slots}:
427      Unit
428
429def done_fail(-error: Backward.Error, -gs: List<&1, Gradient.Slot>, clash: {Fail{error} == Done{gs} : Laws.Slots()}) -> Empty:
430  %Equal.sym(Laws.Slots(), Fail{error}, Done{gs}, clash) : is_done(_)
431  Unit{}
432
433def conclude(-entries: List<&1, Backward.Entry>, -copy: List<&1, Gradient.Slot>, -gradients: List<&1, Gradient.Slot>, +count: Nat,
434  -gs: List<&1, Gradient.Slot>, same: {copy == gradients : List<&1, Gradient.Slot>},
435  succeeded: {Laws.result(Backward.sweep(entries, Done{gradients}, count)) == Done{gs} : Laws.Slots()},
436  out: Run<entries, copy, count, gradients, Nil{}>) -> {Laws.chained(entries, gradients, count, Nil{}) == Done{gs} : Laws.Slots()}:
437  match out:
438    case Kept{done, found, swept, pulled}:
439      Equal.trans(Laws.Slots(), Laws.chained(entries, gradients, count, Nil{}), Done{found}, Done{gs}, pulled,
440        Equal.trans(Laws.Slots(), Done{found}, Laws.result(Backward.sweep(entries, Done{copy}, count)), Done{gs},
441          Equal.sym(Laws.Slots(), Laws.result(Backward.sweep(entries, Done{copy}, count)), Done{found},
442            Equal.cong(Backward.Swept(), Laws.Slots(), pair => Laws.result(pair), Backward.sweep(entries, Done{copy}, count), (done, Done{found}), swept)),
443          Equal.trans(Laws.Slots(), Laws.result(Backward.sweep(entries, Done{copy}, count)), Laws.result(Backward.sweep(entries, Done{gradients}, count)),
444            Done{gs},
445            Equal.cong(List<&1, Gradient.Slot>, Laws.Slots(), list => Laws.result(Backward.sweep(entries, Done{list}, count)), copy, gradients, same),
446            succeeded)))
447    case Stopped{done, error, swept}:
448      Empty.absurd({Laws.chained(entries, gradients, count, Nil{}) == Done{gs} : Laws.Slots()},
449        done_fail(error, gs,
450          Equal.trans(Laws.Slots(), Fail{error}, Laws.result(Backward.sweep(entries, Done{copy}, count)), Done{gs},
451            Equal.sym(Laws.Slots(), Laws.result(Backward.sweep(entries, Done{copy}, count)), Fail{error},
452              Equal.cong(Backward.Swept(), Laws.Slots(), pair => Laws.result(pair), Backward.sweep(entries, Done{copy}, count), (done, Fail{error}), swept)),
453            Equal.trans(Laws.Slots(), Laws.result(Backward.sweep(entries, Done{copy}, count)), Laws.result(Backward.sweep(entries, Done{gradients}, count)),
454              Done{gs},
455              Equal.cong(List<&1, Gradient.Slot>, Laws.Slots(), list => Laws.result(Backward.sweep(entries, Done{list}, count)), copy, gradients, same),
456              succeeded))))
457
458def started_pulls(entries: List<&1, Backward.Entry>, -gradients: List<&1, Gradient.Slot>, +count: Nat, -gs: List<&1, Gradient.Slot>,
459  succeeded: {Laws.result(Backward.sweep(entries, Done{gradients}, count)) == Done{gs} : Laws.Slots()}, init: Started<gradients, count>) ->
460  {Laws.chained(entries, gradients, count, Nil{}) == Done{gs} : Laws.Slots()}:
461  Started{copy, same, pulls} = init
462  conclude(entries, copy, gradients, count, gs, same, succeeded, swept_pulls(entries, Done{copy}, gradients, count, Nil{}, pulls))
463
464def Laws.tensor_sweep_chain_rule(entries, gradients, count, gs, succeeded):
465  started_pulls(entries, gradients, count, gs, succeeded, started(gradients, count))
466
467# Id arithmetic for the entries newer than the output, as in
468# tensor_backward_PROOF.bend, kept here so this file checks on its own.
469def eq_refl(+number: Nat) -> {True{} == Nat.is_eq(number, number) : Bool}:
470  match number:
471    case 0n:
472      {==}
473    case 1n+rest:
474      eq_refl(rest)
475
476def add_zero(+number: Nat) -> {number == Nat.add(number, 0n) : Nat}:
477  match number:
478    case 0n:
479      {==}
480    case 1n+rest:
481      Equal.cong(Nat, Nat, value => 1n+value, rest, Nat.add(rest, 0n), add_zero(rest))
482
483def add_succ(+left: Nat, -right: Nat) -> {1n+Nat.add(left, right) == Nat.add(left, 1n+right) : Nat}:
484  match left:
485    case 0n:
486      {==}
487    case 1n+rest:
488      Equal.cong(Nat, Nat, value => 1n+value, 1n+Nat.add(rest, right), Nat.add(rest, 1n+right), add_succ(rest, right))
489
490# A node with older nodes below it and extra + 1 newer ones above it never has
491# the id of the target.
492def older_ne(+older: Nat, -extra: Nat) -> {False{} == Nat.is_eq(Nat.add(older, 1n+extra), older) : Bool}:
493  match older:
494    case 0n:
495      {==}
496    case 1n+rest:
497      older_ne(rest, extra)
498
499# What a backward's pass does, with the chained answer when it succeeds.
500type Passed<-entries: List<&1, Backward.Entry>, -count: Nat, -output: Nat, -selected: Bool, -slots: List<&1, Gradient.Slot>> is Data:
501  PassKept{-done: List<&1, Backward.Entry>, -gradients: List<&1, Gradient.Slot>,
502    passed: {Backward.pass(entries, count, output, selected) == (done, Done{gradients}) : Backward.Swept()},
503    chained: {Laws.chained(entries, slots, count, Nil{}) == Done{gradients} : Laws.Slots()}}
504  PassStopped{-done: List<&1, Backward.Entry>, -error: Backward.Error,
505    passed: {Backward.pass(entries, count, output, selected) == (done, Fail{error}) : Backward.Swept()}}
506
507def seeded_out(+node: Backward.Node, +shape: Shape.Shape, -value: Core.Dynamic, -saved: Backward.Saved, -slot: Gradient.Slot,
508  -rest: List<&1, Backward.Entry>, +older: Nat, -ones: Core.Tensor<shape>, -copy: List<&1, Gradient.Slot>,
509  made: {Core.new(shape, 1.0) == Done{ones} : Result<&2, &1, Core.Error, Core.Tensor<shape>>},
510  same: {copy == Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older) : List<&1, Gradient.Slot>},
511  out: Run<Backward.Entry{node, shape, value, saved, slot} <> rest, copy, 1n+older,
512    Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older), Nil{}>) ->
513  Passed<Backward.Entry{node, shape, value, saved, slot} <> rest, 1n+older, older, True{},
514    Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older)>:
515  match out:
516    case Kept{done, gradients, swept, chained}:
517      PassKept{done, gradients,
518        Equal.trans(Backward.Swept(), Backward.seeded(node, shape, value, saved, slot, rest, older, Core.new(shape, 1.0)),
519          Backward.seeded(node, shape, value, saved, slot, rest, older, Done{ones}), (done, Done{gradients}),
520          Equal.cong(Result<&2, &1, Core.Error, Core.Tensor<shape>>, Backward.Swept(),
521            made_ones => Backward.seeded(node, shape, value, saved, slot, rest, older, made_ones), Core.new(shape, 1.0), Done{ones}, made),
522          Equal.trans(Backward.Swept(), Backward.seeded(node, shape, value, saved, slot, rest, older, Done{ones}),
523            Backward.sweep(Backward.Entry{node, shape, value, saved, slot} <> rest, Done{copy}, 1n+older), (done, Done{gradients}),
524            Equal.cong(List<&1, Gradient.Slot>, Backward.Swept(),
525              list => Backward.sweep(Backward.Entry{node, shape, value, saved, slot} <> rest, Done{list}, 1n+older),
526              Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older), copy,
527              Equal.sym(List<&1, Gradient.Slot>, copy, Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older), same)),
528            swept)),
529        chained}
530    case Stopped{done, error, swept}:
531      PassStopped{done, error,
532        Equal.trans(Backward.Swept(), Backward.seeded(node, shape, value, saved, slot, rest, older, Core.new(shape, 1.0)),
533          Backward.seeded(node, shape, value, saved, slot, rest, older, Done{ones}), (done, Fail{error}),
534          Equal.cong(Result<&2, &1, Core.Error, Core.Tensor<shape>>, Backward.Swept(),
535            made_ones => Backward.seeded(node, shape, value, saved, slot, rest, older, made_ones), Core.new(shape, 1.0), Done{ones}, made),
536          Equal.trans(Backward.Swept(), Backward.seeded(node, shape, value, saved, slot, rest, older, Done{ones}),
537            Backward.sweep(Backward.Entry{node, shape, value, saved, slot} <> rest, Done{copy}, 1n+older), (done, Fail{error}),
538            Equal.cong(List<&1, Gradient.Slot>, Backward.Swept(),
539              list => Backward.sweep(Backward.Entry{node, shape, value, saved, slot} <> rest, Done{list}, 1n+older),
540              Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older), copy,
541              Equal.sym(List<&1, Gradient.Slot>, copy, Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older), same)),
542            swept))}
543
544def seeded_run(+node: Backward.Node, +shape: Shape.Shape, value: Core.Dynamic, saved: Backward.Saved, slot: Gradient.Slot,
545  rest: List<&1, Backward.Entry>, +older: Nat, -ones: Core.Tensor<shape>,
546  made: {Core.new(shape, 1.0) == Done{ones} : Result<&2, &1, Core.Error, Core.Tensor<shape>>},
547  init: Started<Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older), 1n+older>) ->
548  Passed<Backward.Entry{node, shape, value, saved, slot} <> rest, 1n+older, older, True{},
549    Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older)>:
550  Started{copy, same, pulls} = init
551  seeded_out(node, shape, value, saved, slot, rest, older, ones, copy, made, same,
552    swept_pulls(Backward.Entry{node, shape, value, saved, slot} <> rest, Done{copy},
553      Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older), 1n+older, Nil{}, pulls))
554
555def newer_step(+node: Backward.Node, +shape: Shape.Shape, -value: Core.Dynamic, -saved: Backward.Saved, -slot: Gradient.Slot,
556  -rest: List<&1, Backward.Entry>, -below: Nat, +older: Nat, -slots: List<&1, Gradient.Slot>,
557  out: Passed<rest, below, older, Backward.at_head(below, older), slots>) ->
558  Passed<Backward.Entry{node, shape, value, saved, slot} <> rest, 1n+below, older, False{}, Gradient.Unset{} <> slots>:
559  match out:
560    case PassKept{done, gradients, passed, chained}:
561      PassKept{Backward.Entry{node, shape, value, saved, slot} <> done, Gradient.Unset{} <> gradients,
562        Equal.cong(Backward.Swept(), Backward.Swept(),
563          pair => Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Unset{}, pair),
564          Backward.pass(rest, below, older, Backward.at_head(below, older)), (done, Done{gradients}), passed),
565        Equal.cong(Laws.Slots(), Laws.Slots(), result => Backward.prepend(Gradient.Slot, Gradient.Unset{}, result),
566          Laws.chained(rest, slots, below, Nil{}), Done{gradients}, chained)}
567    case PassStopped{done, error, passed}:
568      PassStopped{Backward.Entry{node, shape, value, saved, slot} <> done, error,
569        Equal.cong(Backward.Swept(), Backward.Swept(),
570          pair => Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Unset{}, pair),
571          Backward.pass(rest, below, older, Backward.at_head(below, older)), (done, Fail{error}), passed)}
572
573def newer_chain(newer: List<&1, Backward.Entry>, +node: Backward.Node, +shape: Shape.Shape, value: Core.Dynamic, saved: Backward.Saved,
574  slot: Gradient.Slot, rest: List<&1, Backward.Entry>, +older: Nat, ones: Core.Tensor<shape>,
575  made: {Core.new(shape, 1.0) == Done{ones} : Result<&2, &1, Core.Error, Core.Tensor<shape>>}) ->
576  Passed<List.append(&1, Backward.Entry, newer, Backward.Entry{node, shape, value, saved, slot} <> rest),
577    1n+Nat.add(older, List.length(&1, Backward.Entry, newer)), older,
578    Backward.at_head(1n+Nat.add(older, List.length(&1, Backward.Entry, newer)), older),
579    Laws.seeds(List.length(&1, Backward.Entry, newer), shape, ones, older)>:
580  match newer:
581    case Nil{}:
582      %add_zero(older) :
583        Passed<Backward.Entry{node, shape, value, saved, slot} <> rest, 1n+_, older, Backward.at_head(1n+_, older),
584          Laws.seeds(0n, shape, ones, older)>
585      %eq_refl(older) :
586        Passed<Backward.Entry{node, shape, value, saved, slot} <> rest, 1n+older, older, _, Laws.seeds(0n, shape, ones, older)>
587      seeded_run(node, shape, value, saved, slot, rest, older, ones, made,
588        started(Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older), 1n+older))
589    case Con{Backward.Entry{+top, +top_shape, top_value, top_saved, top_slot}, tail}:
590      %older_ne(older, List.length(&1, Backward.Entry, tail)) :
591        Passed<Backward.Entry{top, top_shape, top_value, top_saved, top_slot} <>
592            List.append(&1, Backward.Entry, tail, Backward.Entry{node, shape, value, saved, slot} <> rest),
593          1n+Nat.add(older, 1n+List.length(&1, Backward.Entry, tail)), older, _,
594          Laws.seeds(1n+List.length(&1, Backward.Entry, tail), shape, ones, older)>
595      %add_succ(older, List.length(&1, Backward.Entry, tail)) :
596        Passed<Backward.Entry{top, top_shape, top_value, top_saved, top_slot} <>
597            List.append(&1, Backward.Entry, tail, Backward.Entry{node, shape, value, saved, slot} <> rest),
598          1n+_, older, False{}, Laws.seeds(1n+List.length(&1, Backward.Entry, tail), shape, ones, older)>
599      newer_step(top, top_shape, top_value, top_saved, top_slot,
600        List.append(&1, Backward.Entry, tail, Backward.Entry{node, shape, value, saved, slot} <> rest),
601        1n+Nat.add(older, List.length(&1, Backward.Entry, tail)), older,
602        Laws.seeds(List.length(&1, Backward.Entry, tail), shape, ones, older),
603        newer_chain(tail, node, shape, value, saved, slot, rest, older, ones, made))
604
605def passed_chain(-entries: List<&1, Backward.Entry>, -count: Nat, -output: Nat, -selected: Bool, -slots: List<&1, Gradient.Slot>,
606  -gradients: List<&1, Gradient.Slot>,
607  succeeded: {Laws.result(Backward.pass(entries, count, output, selected)) == Done{gradients} : Laws.Slots()},
608  out: Passed<entries, count, output, selected, slots>) -> {Laws.chained(entries, slots, count, Nil{}) == Done{gradients} : Laws.Slots()}:
609  match out:
610    case PassKept{done, found, passed, chained}:
611      Equal.trans(Laws.Slots(), Laws.chained(entries, slots, count, Nil{}), Done{found}, Done{gradients}, chained,
612        Equal.trans(Laws.Slots(), Done{found}, Laws.result(Backward.pass(entries, count, output, selected)), Done{gradients},
613          Equal.sym(Laws.Slots(), Laws.result(Backward.pass(entries, count, output, selected)), Done{found},
614            Equal.cong(Backward.Swept(), Laws.Slots(), pair => Laws.result(pair), Backward.pass(entries, count, output, selected),
615              (done, Done{found}), passed)),
616          succeeded))
617    case PassStopped{done, error, passed}:
618      Empty.absurd({Laws.chained(entries, slots, count, Nil{}) == Done{gradients} : Laws.Slots()},
619        done_fail(error, gradients,
620          Equal.trans(Laws.Slots(), Fail{error}, Laws.result(Backward.pass(entries, count, output, selected)), Done{gradients},
621            Equal.sym(Laws.Slots(), Laws.result(Backward.pass(entries, count, output, selected)), Fail{error},
622              Equal.cong(Backward.Swept(), Laws.Slots(), pair => Laws.result(pair), Backward.pass(entries, count, output, selected),
623                (done, Fail{error}), passed)),
624            succeeded)))
625
626def Laws.tensor_backward_chain_rule(newer, node, shape, value, saved, slot, rest, older, ones, made, gradients, succeeded):
627  passed_chain(List.append(&1, Backward.Entry, newer, Backward.Entry{node, shape, value, saved, slot} <> rest),
628    1n+Nat.add(older, List.length(&1, Backward.Entry, newer)), older,
629    Backward.at_head(1n+Nat.add(older, List.length(&1, Backward.Entry, newer)), older),
630    Laws.seeds(List.length(&1, Backward.Entry, newer), shape, ones, older), gradients, succeeded,
631    newer_chain(newer, node, shape, value, saved, slot, rest, older, ones, made))