1	import Base
2	import ../shape/core.bend as Shape
3	import ../tensor/core.bend as Core
4	import ./gradient.bend as Gradient
5	import ./tensor_backward.bend as Backward
6	import ./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.
12	type 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	
18	def 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.
28	def 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.
46	type 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	
50	def 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	
56	def 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	
65	def 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.
73	type 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	
78	type 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	
83	def 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	
94	def 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	
100	def 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	
110	def 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	
120	def 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.
138	def 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.
158	type 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	
162	def 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	
173	def 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	
183	def 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.
197	type 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	
200	type 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	
207	def 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.
215	type 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	
225	def 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	
244	def 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	
282	def 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	
292	def 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	
307	def 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	
321	def 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	
351	def 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	
374	def 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	
390	def 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.
409	def 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	
422	def is_done(result: Laws.Slots()) -> Type:
423	  match result:
424	    case Fail{error}:
425	      Empty
426	    case Done{slots}:
427	      Unit
428	
429	def 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	
433	def 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	
458	def 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	
464	def 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.
469	def 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	
476	def 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	
483	def 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.
492	def 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.
500	type 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	
507	def 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	
544	def 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	
555	def 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	
573	def 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	
605	def 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	
626	def 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))