1	import Base
2	import ./backward.bend as Backward
3	import ./backward_LAWS.bend as Laws
4	
5	def truth(value: Bool) -> Data:
6	  match value:
7	    case True{}:
8	      Unit
9	    case False{}:
10	      Empty
11	
12	def true_false(equal: {True{} == False{} : Bool}) -> Empty:
13	  %equal : truth(_)
14	  Unit{}
15	
16	def eq_refl(+number: Nat) -> {True{} == Nat.is_eq(number, number) : Bool}:
17	  match number:
18	    case 0n:
19	      {==}
20	    case 1n+rest:
21	      eq_refl(rest)
22	
23	def add_succ(+left: Nat, +right: Nat) -> {Nat.add(left, 1n+right) == 1n+Nat.add(left, right) : Nat}:
24	  match left:
25	    case 0n:
26	      {==}
27	    case 1n+rest:
28	      Equal.cong(Nat, Nat, number => 1n+number, Nat.add(rest, 1n+right), 1n+Nat.add(rest, right), add_succ(rest, right))
29	
30	def succ_add_ne(+left: Nat, +right: Nat) -> {False{} == Nat.is_eq(1n+Nat.add(left, right), right) : Bool}:
31	  match right:
32	    case 0n:
33	      {==}
34	    case 1n+rest:
35	      %Equal.sym(Nat, Nat.add(left, 1n+rest), 1n+Nat.add(left, rest), add_succ(left, rest)) :
36	        {False{} == Nat.is_eq(1n+_, 1n+rest) : Bool}
37	      succ_add_ne(left, rest)
38	
39	def length_append(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>) ->
40	  {List.length(&2, A, List.append(&2, A, xs, ys)) == Nat.add(List.length(&2, A, xs), List.length(&2, A, ys)) : Nat}:
41	  match xs:
42	    case Nil{}:
43	      {==}
44	    case Con{head, tail}:
45	      Equal.cong(Nat, Nat, number => 1n+number, List.length(&2, A, List.append(&2, A, tail, ys)),
46	        Nat.add(List.length(&2, A, tail), List.length(&2, A, ys)), length_append(A, tail, ys))
47	
48	def append_ne(-A: Data, +xs: List<&2, A>, +item: A, +rest: List<&2, A>) ->
49	  {False{} == Nat.is_eq(List.length(&2, A, List.append(&2, A, xs, item <> rest)), List.length(&2, A, rest)) : Bool}:
50	  %Equal.sym(Nat, List.length(&2, A, List.append(&2, A, xs, item <> rest)),
51	    Nat.add(List.length(&2, A, xs), 1n+List.length(&2, A, rest)), length_append(A, xs, item <> rest)) :
52	    {False{} == Nat.is_eq(_, List.length(&2, A, rest)) : Bool}
53	  %Equal.sym(Nat, Nat.add(List.length(&2, A, xs), 1n+List.length(&2, A, rest)),
54	    1n+Nat.add(List.length(&2, A, xs), List.length(&2, A, rest)), add_succ(List.length(&2, A, xs), List.length(&2, A, rest))) :
55	    {False{} == Nat.is_eq(_, List.length(&2, A, rest)) : Bool}
56	  succ_add_ne(List.length(&2, A, xs), List.length(&2, A, rest))
57	
58	def not_lt_succ_ne(+id: Nat, +bound: Nat, outside: {Nat.is_lt(id, 1n+bound) == False{} : Bool}) ->
59	  {False{} == Nat.is_eq(bound, id) : Bool}:
60	  match id bound:
61	    case 0n bound:
62	      Empty.absurd({False{} == Nat.is_eq(bound, 0n) : Bool}, true_false(outside))
63	    case 1n+rest 0n:
64	      {==}
65	    case 1n+rest 1n+smaller:
66	      not_lt_succ_ne(rest, smaller, outside)
67	
68	def not_lt_succ_lt(+id: Nat, +bound: Nat, outside: {Nat.is_lt(id, 1n+bound) == False{} : Bool}) ->
69	  {Nat.is_lt(id, bound) == False{} : Bool}:
70	  match id bound:
71	    case 0n bound:
72	      Empty.absurd({Nat.is_lt(0n, bound) == False{} : Bool}, true_false(outside))
73	    case 1n+rest 0n:
74	      {==}
75	    case 1n+rest 1n+smaller:
76	      not_lt_succ_lt(rest, smaller, outside)
77	
78	def Laws.vjp_leaf(g):
79	  {==}
80	
81	def Laws.vjp_add(a, b, g):
82	  {==}
83	
84	def Laws.vjp_sub(a, b, g):
85	  {==}
86	
87	def Laws.vjp_mul(a, b, left, right, g):
88	  {==}
89	
90	def Laws.vjp_neg(a, g):
91	  {==}
92	
93	def Laws.backward_add(x, y):
94	  {==}
95	
96	def Laws.backward_sub(x, y):
97	  {==}
98	
99	def Laws.backward_mul(x, y):
100	  {==}
101	
102	def Laws.backward_neg(x):
103	  {==}
104	
105	def Laws.seed_selected_output(newer, node, rest):
106	  match newer:
107	    case Nil{}:
108	      %eq_refl(List.length(&2, Backward.Node, rest)) :
109	        {Backward.chosen(node, rest, List.length(&2, Backward.Node, rest),
110	          unit => Backward.pass(rest, List.length(&2, Backward.Node, rest), List.length(&2, Backward.Node, rest)), _) ==
111	          Some{1.0} <> Backward.sweep(rest,
112	            Backward.contribute(node, Some{1.0}, List.length(&2, Backward.Node, rest), Backward.nones(List.length(&2, Backward.Node, rest))),
113	            List.length(&2, Backward.Node, rest)) : List<&2, Maybe<&2, F32>>}
114	      {==}
115	    case Con{head, tail}:
116	      %append_ne(Backward.Node, tail, node, rest) :
117	        {Backward.chosen(head, List.append(&2, Backward.Node, tail, node <> rest),
118	          List.length(&2, Backward.Node, List.append(&2, Backward.Node, tail, node <> rest)),
119	          unit => Backward.pass(List.append(&2, Backward.Node, tail, node <> rest),
120	            List.length(&2, Backward.Node, List.append(&2, Backward.Node, tail, node <> rest)), List.length(&2, Backward.Node, rest)), _) ==
121	          None{} <> List.append(&2, Maybe<&2, F32>, Backward.nones(List.length(&2, Backward.Node, tail)),
122	            Some{1.0} <> Backward.sweep(rest,
123	              Backward.contribute(node, Some{1.0}, List.length(&2, Backward.Node, rest), Backward.nones(List.length(&2, Backward.Node, rest))),
124	              List.length(&2, Backward.Node, rest))) : List<&2, Maybe<&2, F32>>}
125	      Equal.cong(List<&2, Maybe<&2, F32>>, List<&2, Maybe<&2, F32>>, xs => None{} <> xs,
126	        Backward.pass(List.append(&2, Backward.Node, tail, node <> rest),
127	          List.length(&2, Backward.Node, List.append(&2, Backward.Node, tail, node <> rest)), List.length(&2, Backward.Node, rest)),
128	        List.append(&2, Maybe<&2, F32>, Backward.nones(List.length(&2, Backward.Node, tail)),
129	          Some{1.0} <> Backward.sweep(rest,
130	            Backward.contribute(node, Some{1.0}, List.length(&2, Backward.Node, rest), Backward.nones(List.length(&2, Backward.Node, rest))),
131	            List.length(&2, Backward.Node, rest))),
132	        Laws.seed_selected_output(tail, node, rest))
133	
134	def is_some_accumulate(slot: Maybe<&2, F32>, +value: F32) ->
135	  {Maybe.is_some(&2, F32, Backward.accumulate(slot, Some{value})) == True{} : Bool}:
136	  match slot:
137	    case None{}:
138	      {==}
139	    case Some{held}:
140	      {==}
141	
142	def somes_bumped(slot: Maybe<&2, F32>, +rest: List<&2, Maybe<&2, F32>>, +below: Nat, +target: Nat, +value: F32, flag: Bool,
143	  ih: {Laws.somes(Backward.bump(rest, below, target, value)) == Laws.mark(Laws.somes(rest), below, target) : List<&2, Bool>}) ->
144	  {Laws.somes(Backward.bumped(slot, rest, value, unit => Backward.bump(rest, below, target, value), flag)) ==
145	    Laws.marked(Maybe.is_some(&2, F32, slot), Laws.somes(rest), unit => Laws.mark(Laws.somes(rest), below, target), flag) : List<&2, Bool>}:
146	  match flag:
147	    case True{}:
148	      Equal.cong(Bool, List<&2, Bool>, found => found <> Laws.somes(rest),
149	        Maybe.is_some(&2, F32, Backward.accumulate(slot, Some{value})), True{}, is_some_accumulate(slot, value))
150	    case False{}:
151	      Equal.cong(List<&2, Bool>, List<&2, Bool>, xs => Maybe.is_some(&2, F32, slot) <> xs,
152	        Laws.somes(Backward.bump(rest, below, target, value)), Laws.mark(Laws.somes(rest), below, target), ih)
153	
154	def somes_bump(slots: List<&2, Maybe<&2, F32>>, +count: Nat, +target: Nat, +value: F32) ->
155	  {Laws.somes(Backward.bump(slots, count, target, value)) == Laws.mark(Laws.somes(slots), count, target) : List<&2, Bool>}:
156	  match slots count:
157	    case Nil{} count:
158	      {==}
159	    case Con{slot, rest} 0n:
160	      {==}
161	    case Con{slot, +rest} 1n+below:
162	      somes_bumped(slot, rest, below, target, value, Nat.is_eq(below, target), somes_bump(rest, below, target, value))
163	
164	def contribution_targets(contributions: List<&2, Backward.Contribution>) -> List<&2, Nat>:
165	  match contributions:
166	    case Nil{}:
167	      Nil{}
168	    case Con{Backward.Contribution{target, value}, rest}:
169	      target <> contribution_targets(rest)
170	
171	def somes_deliver(contributions: List<&2, Backward.Contribution>, +count: Nat, +slots: List<&2, Maybe<&2, F32>>) ->
172	  {Laws.somes(Backward.deliver(contributions, count, slots)) ==
173	    Laws.mark_all(contribution_targets(contributions), count, Laws.somes(slots)) : List<&2, Bool>}:
174	  match contributions:
175	    case Nil{}:
176	      {==}
177	    case Con{Backward.Contribution{+target, +value}, rest}:
178	      %somes_bump(slots, count, target, value) :
179	        {Laws.somes(Backward.deliver(rest, count, Backward.bump(slots, count, target, value))) ==
180	          Laws.mark_all(contribution_targets(rest), count, _) : List<&2, Bool>}
181	      somes_deliver(rest, count, Backward.bump(slots, count, target, value))
182	
183	def vjp_targets(node: Backward.Node, +g: F32) -> {contribution_targets(Backward.vjp(node, g)) == Laws.targets(node) : List<&2, Nat>}:
184	  match node:
185	    case Backward.Leaf{}:
186	      {==}
187	    case Backward.Add{a, b}:
188	      {==}
189	    case Backward.Sub{a, b}:
190	      {==}
191	    case Backward.Mul{a, b, left, right}:
192	      {==}
193	    case Backward.Neg{a}:
194	      {==}
195	
196	def somes_contribute(+node: Backward.Node, gradient: Maybe<&2, F32>, +count: Nat, +slots: List<&2, Maybe<&2, F32>>) ->
197	  {Laws.somes(Backward.contribute(node, gradient, count, slots)) ==
198	    Laws.spread(node, Maybe.is_some(&2, F32, gradient), count, Laws.somes(slots)) : List<&2, Bool>}:
199	  match gradient:
200	    case None{}:
201	      {==}
202	    case Some{+value}:
203	      %vjp_targets(node, value) :
204	        {Laws.somes(Backward.deliver(Backward.vjp(node, value), count, slots)) == Laws.mark_all(_, count, Laws.somes(slots)) : List<&2, Bool>}
205	      somes_deliver(Backward.vjp(node, value), count, slots)
206	
207	def sweep_reach(nodes: List<&2, Backward.Node>, gradients: List<&2, Maybe<&2, F32>>, +count: Nat) ->
208	  {Laws.somes(Backward.sweep(nodes, gradients, count)) == Laws.reach(nodes, Laws.somes(gradients), count) : List<&2, Bool>}:
209	  match nodes gradients count:
210	    case Nil{} gradients count:
211	      {==}
212	    case Con{node, rest} Nil{} count:
213	      {==}
214	    case Con{node, rest} Con{gradient, pending} 0n:
215	      {==}
216	    case Con{+node, rest} Con{+gradient, +pending} 1n+below:
217	      %somes_contribute(node, gradient, below, pending) :
218	        {Maybe.is_some(&2, F32, gradient) <> Laws.somes(Backward.sweep(rest, Backward.contribute(node, gradient, below, pending), below)) ==
219	          Maybe.is_some(&2, F32, gradient) <> Laws.reach(rest, _, below) : List<&2, Bool>}
220	      Equal.cong(List<&2, Bool>, List<&2, Bool>, xs => Maybe.is_some(&2, F32, gradient) <> xs,
221	        Laws.somes(Backward.sweep(rest, Backward.contribute(node, gradient, below, pending), below)),
222	        Laws.reach(rest, Laws.somes(Backward.contribute(node, gradient, below, pending)), below),
223	        sweep_reach(rest, Backward.contribute(node, gradient, below, pending), below))
224	
225	def somes_nones(+count: Nat) -> {Laws.somes(Backward.nones(count)) == Laws.falses(count) : List<&2, Bool>}:
226	  match count:
227	    case 0n:
228	      {==}
229	    case 1n+rest:
230	      Equal.cong(List<&2, Bool>, List<&2, Bool>, xs => False{} <> xs, Laws.somes(Backward.nones(rest)), Laws.falses(rest), somes_nones(rest))
231	
232	def chosen_reached(+node: Backward.Node, +rest: List<&2, Backward.Node>, +below: Nat, +output: Nat, flag: Bool,
233	  ih: {Laws.somes(Backward.pass(rest, below, output)) == Laws.reached(rest, below, output) : List<&2, Bool>}) ->
234	  {Laws.somes(Backward.chosen(node, rest, below, unit => Backward.pass(rest, below, output), flag)) ==
235	    Laws.reached_chosen(node, rest, below, unit => Laws.reached(rest, below, output), flag) : List<&2, Bool>}:
236	  match flag:
237	    case True{}:
238	      %somes_nones(below) :
239	        {Laws.somes(Backward.sweep(node <> rest, Some{1.0} <> Backward.nones(below), 1n+below)) ==
240	          Laws.reach(node <> rest, True{} <> _, 1n+below) : List<&2, Bool>}
241	      sweep_reach(node <> rest, Some{1.0} <> Backward.nones(below), 1n+below)
242	    case False{}:
243	      Equal.cong(List<&2, Bool>, List<&2, Bool>, xs => False{} <> xs,
244	        Laws.somes(Backward.pass(rest, below, output)), Laws.reached(rest, below, output), ih)
245	
246	def pass_reached(nodes: List<&2, Backward.Node>, +count: Nat, +output: Nat) ->
247	  {Laws.somes(Backward.pass(nodes, count, output)) == Laws.reached(nodes, count, output) : List<&2, Bool>}:
248	  match nodes count:
249	    case Nil{} count:
250	      {==}
251	    case Con{node, rest} 0n:
252	      {==}
253	    case Con{+node, +rest} 1n+below:
254	      chosen_reached(node, rest, below, output, Nat.is_eq(below, output), pass_reached(rest, below, output))
255	
256	def Laws.reached_exactly(graph, output):
257	  pass_reached(graph, List.length(&2, Backward.Node, graph), output)
258	
259	def Laws.unused_leaf_none(x, y, z):
260	  {==}
261	
262	def Laws.accumulate_moves_in(contribution):
263	  {==}
264	
265	def Laws.accumulate_adds_total_first(held, value):
266	  {==}
267	
268	def Laws.accumulate_keeps_without_contribution(held):
269	  {==}
270	
271	def Laws.bump_target(newer, slot, rest, value):
272	  match newer:
273	    case Nil{}:
274	      %eq_refl(List.length(&2, Maybe<&2, F32>, rest)) :
275	        {Backward.bumped(slot, rest, value,
276	          unit => Backward.bump(rest, List.length(&2, Maybe<&2, F32>, rest), List.length(&2, Maybe<&2, F32>, rest), value), _) ==
277	          Backward.accumulate(slot, Some{value}) <> rest : List<&2, Maybe<&2, F32>>}
278	      {==}
279	    case Con{head, tail}:
280	      %append_ne(Maybe<&2, F32>, tail, slot, rest) :
281	        {Backward.bumped(head, List.append(&2, Maybe<&2, F32>, tail, slot <> rest), value,
282	          unit => Backward.bump(List.append(&2, Maybe<&2, F32>, tail, slot <> rest),
283	            List.length(&2, Maybe<&2, F32>, List.append(&2, Maybe<&2, F32>, tail, slot <> rest)), List.length(&2, Maybe<&2, F32>, rest), value), _) ==
284	          head <> List.append(&2, Maybe<&2, F32>, tail, Backward.accumulate(slot, Some{value}) <> rest) : List<&2, Maybe<&2, F32>>}
285	      Equal.cong(List<&2, Maybe<&2, F32>>, List<&2, Maybe<&2, F32>>, xs => head <> xs,
286	        Backward.bump(List.append(&2, Maybe<&2, F32>, tail, slot <> rest),
287	          List.length(&2, Maybe<&2, F32>, List.append(&2, Maybe<&2, F32>, tail, slot <> rest)), List.length(&2, Maybe<&2, F32>, rest), value),
288	        List.append(&2, Maybe<&2, F32>, tail, Backward.accumulate(slot, Some{value}) <> rest),
289	        Laws.bump_target(tail, slot, rest, value))
290	
291	def Laws.fan_out_arrival_order(x, a, b, c):
292	  {==}
293	
294	def Laws.lookup_exact(A, newer, item, rest):
295	  match newer:
296	    case Nil{}:
297	      %eq_refl(List.length(&2, A, rest)) :
298	        {Backward.picked(A, item, unit => Backward.find(A, rest, List.length(&2, A, rest), List.length(&2, A, rest)), _) ==
299	          Some{item} : Maybe<&2, A>}
300	      {==}
301	    case Con{head, tail}:
302	      %append_ne(A, tail, item, rest) :
303	        {Backward.picked(A, head, unit => Backward.find(A, List.append(&2, A, tail, item <> rest),
304	          List.length(&2, A, List.append(&2, A, tail, item <> rest)), List.length(&2, A, rest)), _) == Some{item} : Maybe<&2, A>}
305	      Laws.lookup_exact(A, tail, item, rest)
306	
307	def find_unknown(-A: Data, +xs: List<&2, A>, +id: Nat, +outside: {Nat.is_lt(id, List.length(&2, A, xs)) == False{} : Bool}) ->
308	  {Backward.find(A, xs, List.length(&2, A, xs), id) == None{} : Maybe<&2, A>}:
309	  match xs:
310	    case Nil{}:
311	      {==}
312	    case Con{head, tail}:
313	      %not_lt_succ_ne(id, List.length(&2, A, tail), outside) :
314	        {Backward.picked(A, head, unit => Backward.find(A, tail, List.length(&2, A, tail), id), _) == None{} : Maybe<&2, A>}
315	      find_unknown(A, tail, id, not_lt_succ_lt(id, List.length(&2, A, tail), outside))
316	
317	def Laws.lookup_unknown(A, items, id, outside):
318	  find_unknown(A, items, id, outside)
319	
320	def Laws.bump_unknown(gradients, target, value, outside):
321	  match gradients:
322	    case Nil{}:
323	      {==}
324	    case Con{slot, tail}:
325	      %not_lt_succ_ne(target, List.length(&2, Maybe<&2, F32>, tail), outside) :
326	        {Backward.bumped(slot, tail, value,
327	          unit => Backward.bump(tail, List.length(&2, Maybe<&2, F32>, tail), target, value), _) == slot <> tail : List<&2, Maybe<&2, F32>>}
328	      Equal.cong(List<&2, Maybe<&2, F32>>, List<&2, Maybe<&2, F32>>, xs => slot <> xs,
329	        Backward.bump(tail, List.length(&2, Maybe<&2, F32>, tail), target, value), tail,
330	        Laws.bump_unknown(tail, target, value, not_lt_succ_lt(target, List.length(&2, Maybe<&2, F32>, tail), outside)))
331	
332	def Laws.value_unknown(entries, id, outside):
333	  %Equal.sym(Maybe<&2, Backward.Entry>, Backward.lookup(Backward.Entry, entries, id), None{},
334	    find_unknown(Backward.Entry, entries, id, outside)) :
335	    {Backward.entry_value(_) == Fail{Backward.UnknownNode{}} : Result<&2, &2, Backward.Error, F32>}
336	  {==}
337	
338	def Laws.grad_unknown(entries, id, outside):
339	  %Equal.sym(Maybe<&2, Backward.Entry>, Backward.lookup(Backward.Entry, entries, id), None{},
340	    find_unknown(Backward.Entry, entries, id, outside)) :
341	    {Backward.entry_grad(_) == Fail{Backward.UnknownNode{}} : Result<&2, &2, Backward.Error, Maybe<&2, F32>>}
342	  {==}
343	
344	def Laws.record_unknown_left(entries, kind, a, b, outside):
345	  %Equal.sym(Result<&2, &2, Backward.Error, F32>, Backward.value(Backward.Tape{entries}, a), Fail{Backward.UnknownNode{}},
346	    Laws.value_unknown(entries, a, outside)) :
347	    {Backward.operands(entries, kind, a, b, _, Backward.value(Backward.Tape{entries}, b)) ==
348	      (Backward.Tape{entries}, Fail{Backward.UnknownNode{}}) : Backward.Tape & Result<&2, &2, Backward.Error, Nat>}
349	  {==}
350	
351	def operands_right(+entries: List<&2, Backward.Entry>, kind: Backward.Binary, +a: Nat, +b: Nat, left: Result<&2, &2, Backward.Error, F32>) ->
352	  {Backward.operands(entries, kind, a, b, left, Fail{Backward.UnknownNode{}}) ==
353	    (Backward.Tape{entries}, Fail{Backward.UnknownNode{}}) : Backward.Tape & Result<&2, &2, Backward.Error, Nat>}:
354	  match left:
355	    case Fail{error}:
356	      {==}
357	    case Done{x}:
358	      {==}
359	
360	def Laws.record_unknown_right(entries, kind, a, b, outside):
361	  %Equal.sym(Result<&2, &2, Backward.Error, F32>, Backward.value(Backward.Tape{entries}, b), Fail{Backward.UnknownNode{}},
362	    Laws.value_unknown(entries, b, outside)) :
363	    {Backward.operands(entries, kind, a, b, Backward.value(Backward.Tape{entries}, a), _) ==
364	      (Backward.Tape{entries}, Fail{Backward.UnknownNode{}}) : Backward.Tape & Result<&2, &2, Backward.Error, Nat>}
365	  operands_right(entries, kind, a, b, Backward.value(Backward.Tape{entries}, a))
366	
367	def Laws.neg_unknown(entries, a, outside):
368	  %Equal.sym(Result<&2, &2, Backward.Error, F32>, Backward.value(Backward.Tape{entries}, a), Fail{Backward.UnknownNode{}},
369	    Laws.value_unknown(entries, a, outside)) :
370	    {Backward.negated(entries, a, _) ==
371	      (Backward.Tape{entries}, Fail{Backward.UnknownNode{}}) : Backward.Tape & Result<&2, &2, Backward.Error, Nat>}
372	  {==}
373	
374	def nodes_length(+entries: List<&2, Backward.Entry>) ->
375	  {List.length(&2, Backward.Entry, entries) == List.length(&2, Backward.Node, Backward.nodes(entries)) : Nat}:
376	  match entries:
377	    case Nil{}:
378	      {==}
379	    case Con{Backward.Entry{node, value, slot}, rest}:
380	      Equal.cong(Nat, Nat, number => 1n+number, List.length(&2, Backward.Entry, rest),
381	        List.length(&2, Backward.Node, Backward.nodes(rest)), nodes_length(rest))
382	
383	def Laws.backward_unknown(entries, output, outside):
384	  %nodes_length(entries) :
385	    {Backward.merged(entries, Backward.checked(Backward.nodes(entries), _, output, Nat.is_lt(output, _),
386	      Backward.wired(Backward.nodes(entries), _))) == Fail{Backward.UnknownNode{}} : Result<&2, &2, Backward.Error, Backward.Tape>}
387	  %Equal.sym(Bool, Nat.is_lt(output, List.length(&2, Backward.Entry, entries)), False{}, outside) :
388	    {Backward.merged(entries, Backward.checked(Backward.nodes(entries), List.length(&2, Backward.Entry, entries), output, _,
389	      Backward.wired(Backward.nodes(entries), List.length(&2, Backward.Entry, entries)))) ==
390	      Fail{Backward.UnknownNode{}} : Result<&2, &2, Backward.Error, Backward.Tape>}
391	  {==}
392	
393	def Laws.backward_dangling(entries, output, inside, unsound):
394	  %nodes_length(entries) :
395	    {Backward.merged(entries, Backward.checked(Backward.nodes(entries), _, output, Nat.is_lt(output, _),
396	      Backward.wired(Backward.nodes(entries), _))) == Fail{Backward.DanglingOperand{}} : Result<&2, &2, Backward.Error, Backward.Tape>}
397	  %Equal.sym(Bool, Nat.is_lt(output, List.length(&2, Backward.Entry, entries)), True{}, inside) :
398	    {Backward.merged(entries, Backward.checked(Backward.nodes(entries), List.length(&2, Backward.Entry, entries), output, _,
399	      Backward.wired(Backward.nodes(entries), List.length(&2, Backward.Entry, entries)))) ==
400	      Fail{Backward.DanglingOperand{}} : Result<&2, &2, Backward.Error, Backward.Tape>}
401	  %Equal.sym(Bool, Backward.wired(Backward.nodes(entries), List.length(&2, Backward.Entry, entries)), False{}, unsound) :
402	    {Backward.merged(entries, Backward.checked(Backward.nodes(entries), List.length(&2, Backward.Entry, entries), output, True{}, _)) ==
403	      Fail{Backward.DanglingOperand{}} : Result<&2, &2, Backward.Error, Backward.Tape>}
404	  {==}
405	
406	def Laws.backward_success(entries, output, inside, sound):
407	  %nodes_length(entries) :
408	    {Backward.merged(entries, Backward.checked(Backward.nodes(entries), _, output, Nat.is_lt(output, _),
409	      Backward.wired(Backward.nodes(entries), _))) ==
410	      Done{Backward.Tape{Backward.merge(entries, Backward.pass(Backward.nodes(entries), List.length(&2, Backward.Entry, entries), output))}} :
411	      Result<&2, &2, Backward.Error, Backward.Tape>}
412	  %Equal.sym(Bool, Nat.is_lt(output, List.length(&2, Backward.Entry, entries)), True{}, inside) :
413	    {Backward.merged(entries, Backward.checked(Backward.nodes(entries), List.length(&2, Backward.Entry, entries), output, _,
414	      Backward.wired(Backward.nodes(entries), List.length(&2, Backward.Entry, entries)))) ==
415	      Done{Backward.Tape{Backward.merge(entries, Backward.pass(Backward.nodes(entries), List.length(&2, Backward.Entry, entries), output))}} :
416	      Result<&2, &2, Backward.Error, Backward.Tape>}
417	  %Equal.sym(Bool, Backward.wired(Backward.nodes(entries), List.length(&2, Backward.Entry, entries)), True{}, sound) :
418	    {Backward.merged(entries, Backward.checked(Backward.nodes(entries), List.length(&2, Backward.Entry, entries), output, True{}, _)) ==
419	      Done{Backward.Tape{Backward.merge(entries, Backward.pass(Backward.nodes(entries), List.length(&2, Backward.Entry, entries), output))}} :
420	      Result<&2, &2, Backward.Error, Backward.Tape>}
421	  {==}
422	
423	def and_true(+value: Bool) -> {Bool.and(value, True{}) == value : Bool}:
424	  match value:
425	    case True{}:
426	      {==}
427	    case False{}:
428	      {==}
429	
430	def and_false(+value: Bool) -> {Bool.and(value, False{}) == False{} : Bool}:
431	  match value:
432	    case True{}:
433	      {==}
434	    case False{}:
435	      {==}
436	
437	def operands_bounded(+node: Backward.Node, +bound: Nat) ->
438	  {Backward.operands_below(node, bound) == Laws.bounded(Laws.targets(node), bound) : Bool}:
439	  match node:
440	    case Backward.Leaf{}:
441	      {==}
442	    case Backward.Add{a, b}:
443	      Equal.cong(Bool, Bool, flag => Bool.and(Nat.is_lt(a, bound), flag), Nat.is_lt(b, bound), Bool.and(Nat.is_lt(b, bound), True{}),
444	        Equal.sym(Bool, Bool.and(Nat.is_lt(b, bound), True{}), Nat.is_lt(b, bound), and_true(Nat.is_lt(b, bound))))
445	    case Backward.Sub{a, b}:
446	      Equal.cong(Bool, Bool, flag => Bool.and(Nat.is_lt(a, bound), flag), Nat.is_lt(b, bound), Bool.and(Nat.is_lt(b, bound), True{}),
447	        Equal.sym(Bool, Bool.and(Nat.is_lt(b, bound), True{}), Nat.is_lt(b, bound), and_true(Nat.is_lt(b, bound))))
448	    case Backward.Mul{a, b, left, right}:
449	      Equal.cong(Bool, Bool, flag => Bool.and(Nat.is_lt(a, bound), flag), Nat.is_lt(b, bound), Bool.and(Nat.is_lt(b, bound), True{}),
450	        Equal.sym(Bool, Bool.and(Nat.is_lt(b, bound), True{}), Nat.is_lt(b, bound), and_true(Nat.is_lt(b, bound))))
451	    case Backward.Neg{a}:
452	      Equal.sym(Bool, Bool.and(Nat.is_lt(a, bound), True{}), Nat.is_lt(a, bound), and_true(Nat.is_lt(a, bound)))
453	
454	def Laws.wired_matches_operand_bounds(graph):
455	  match graph:
456	    case Nil{}:
457	      {==}
458	    case Con{node, rest}:
459	      %Equal.sym(Bool, Backward.operands_below(node, List.length(&2, Backward.Node, rest)),
460	        Laws.bounded(Laws.targets(node), List.length(&2, Backward.Node, rest)), operands_bounded(node, List.length(&2, Backward.Node, rest))) :
461	        {Bool.and(_, Backward.wired(rest, List.length(&2, Backward.Node, rest))) ==
462	          Bool.and(Laws.bounded(Laws.targets(node), List.length(&2, Backward.Node, rest)), Laws.well_formed(rest)) : Bool}
463	      Equal.cong(Bool, Bool, flag => Bool.and(Laws.bounded(Laws.targets(node), List.length(&2, Backward.Node, rest)), flag),
464	        Backward.wired(rest, List.length(&2, Backward.Node, rest)), Laws.well_formed(rest), Laws.wired_matches_operand_bounds(rest))
465	
466	def wired_entries(+entries: List<&2, Backward.Entry>) ->
467	  {Backward.wired(Backward.nodes(entries), List.length(&2, Backward.Entry, entries)) == Laws.well_formed(Backward.nodes(entries)) : Bool}:
468	  %Equal.sym(Nat, List.length(&2, Backward.Entry, entries), List.length(&2, Backward.Node, Backward.nodes(entries)), nodes_length(entries)) :
469	    {Backward.wired(Backward.nodes(entries), _) == Laws.well_formed(Backward.nodes(entries)) : Bool}
470	  Laws.wired_matches_operand_bounds(Backward.nodes(entries))
471	
472	def head_ill_formed(+entry: Backward.Entry, +rest: List<&2, Backward.Entry>,
473	  unbound: {Laws.bounded(Laws.targets(Laws.entry_node(entry)), List.length(&2, Backward.Entry, rest)) == False{} : Bool}) ->
474	  {Laws.well_formed(Backward.nodes(entry <> rest)) == False{} : Bool}:
475	  match entry:
476	    case Backward.Entry{node, value, slot}:
477	      %nodes_length(rest) :
478	        {Bool.and(Laws.bounded(Laws.targets(node), _), Laws.well_formed(Backward.nodes(rest))) == False{} : Bool}
479	      %Equal.sym(Bool, Laws.bounded(Laws.targets(node), List.length(&2, Backward.Entry, rest)), False{}, unbound) :
480	        {Bool.and(_, Laws.well_formed(Backward.nodes(rest))) == False{} : Bool}
481	      {==}
482	
483	def unbound_ill_formed(+newer: List<&2, Backward.Entry>, +entry: Backward.Entry, +rest: List<&2, Backward.Entry>,
484	  +unbound: {Laws.bounded(Laws.targets(Laws.entry_node(entry)), List.length(&2, Backward.Entry, rest)) == False{} : Bool}) ->
485	  {Laws.well_formed(Backward.nodes(List.append(&2, Backward.Entry, newer, entry <> rest))) == False{} : Bool}:
486	  match newer:
487	    case Nil{}:
488	      head_ill_formed(entry, rest, unbound)
489	    case Con{Backward.Entry{node, value, slot}, tail}:
490	      %Equal.sym(Bool, Laws.well_formed(Backward.nodes(List.append(&2, Backward.Entry, tail, entry <> rest))), False{},
491	        unbound_ill_formed(tail, entry, rest, unbound)) :
492	        {Bool.and(Laws.bounded(Laws.targets(node), List.length(&2, Backward.Node, Backward.nodes(List.append(&2, Backward.Entry, tail, entry <> rest)))), _) ==
493	          False{} : Bool}
494	      and_false(Laws.bounded(Laws.targets(node), List.length(&2, Backward.Node, Backward.nodes(List.append(&2, Backward.Entry, tail, entry <> rest)))))
495	
496	def Laws.backward_rejects_unbound_operand(newer, entry, rest, output, inside, unbound):
497	  Laws.backward_dangling(List.append(&2, Backward.Entry, newer, entry <> rest), output, inside,
498	    Equal.trans(Bool, Backward.wired(Backward.nodes(List.append(&2, Backward.Entry, newer, entry <> rest)),
499	        List.length(&2, Backward.Entry, List.append(&2, Backward.Entry, newer, entry <> rest))),
500	      Laws.well_formed(Backward.nodes(List.append(&2, Backward.Entry, newer, entry <> rest))), False{},
501	      wired_entries(List.append(&2, Backward.Entry, newer, entry <> rest)),
502	      unbound_ill_formed(newer, entry, rest, unbound)))
503	
504	def Laws.backward_accepts_bound_operands(entries, output, inside, bound):
505	  Laws.backward_success(entries, output, inside,
506	    Equal.trans(Bool, Backward.wired(Backward.nodes(entries), List.length(&2, Backward.Entry, entries)),
507	      Laws.well_formed(Backward.nodes(entries)), True{}, wired_entries(entries), bound))
508	
509	def nodes_merge(+entries: List<&2, Backward.Entry>, +gradients: List<&2, Maybe<&2, F32>>) ->
510	  {Backward.nodes(entries) == Backward.nodes(Backward.merge(entries, gradients)) : List<&2, Backward.Node>}:
511	  match entries gradients:
512	    case Nil{} gradients:
513	      {==}
514	    case Con{Backward.Entry{node, value, slot}, rest} Nil{}:
515	      {==}
516	    case Con{Backward.Entry{node, value, slot}, rest} Con{gradient, more}:
517	      Equal.cong(List<&2, Backward.Node>, List<&2, Backward.Node>, xs => node <> xs,
518	        Backward.nodes(rest), Backward.nodes(Backward.merge(rest, more)), nodes_merge(rest, more))
519	
520	def Laws.backward_twice_accumulates(entries, output, found, computed):
521	  %Equal.sym(Result<&2, &2, Backward.Error, List<&2, Maybe<&2, F32>>>, Backward.gradients(Backward.Tape{entries}, output), Done{found}, computed) :
522	    {Laws.again(Backward.merged(entries, _), output) ==
523	      Done{Backward.Tape{Backward.merge(Backward.merge(entries, found), found)}} : Result<&2, &2, Backward.Error, Backward.Tape>}
524	  %nodes_merge(entries, found) :
525	    {Backward.merged(Backward.merge(entries, found), Backward.planned(_, output)) ==
526	      Done{Backward.Tape{Backward.merge(Backward.merge(entries, found), found)}} : Result<&2, &2, Backward.Error, Backward.Tape>}
527	  %Equal.sym(Result<&2, &2, Backward.Error, List<&2, Maybe<&2, F32>>>, Backward.gradients(Backward.Tape{entries}, output), Done{found}, computed) :
528	    {Backward.merged(Backward.merge(entries, found), _) ==
529	      Done{Backward.Tape{Backward.merge(Backward.merge(entries, found), found)}} : Result<&2, &2, Backward.Error, Backward.Tape>}
530	  {==}
531	
532	def Laws.backward_twice_mul(x, y):
533	  {==}
534	
535	def Laws.zero_grad_empties(entries):
536	  match entries:
537	    case Nil{}:
538	      {==}
539	    case Con{Backward.Entry{node, value, slot}, rest}:
540	      Equal.cong(List<&2, Maybe<&2, F32>>, List<&2, Maybe<&2, F32>>, xs => None{} <> xs,
541	        Laws.slots(Backward.cleared(rest)), Backward.nones(List.length(&2, Backward.Entry, rest)), Laws.zero_grad_empties(rest))
542	
543	def Laws.zero_grad_keeps_nodes(entries):
544	  match entries:
545	    case Nil{}:
546	      {==}
547	    case Con{Backward.Entry{node, value, slot}, rest}:
548	      Equal.cong(List<&2, Backward.Node>, List<&2, Backward.Node>, xs => node <> xs,
549	        Backward.nodes(Backward.cleared(rest)), Backward.nodes(rest), Laws.zero_grad_keeps_nodes(rest))