proofs/list_storage_readback.bend
stelliferous@0.0.3.0 · 228 lines · 0 definitions
1# Finite list writes preserve earlier addresses and read back every list item.
2# Allocation bounds come from the real public count, never example shapes.
3import Base
4import stelliferous@0.0.3.0/proofs/storage_tree_model.bend as Tree
5import stelliferous@0.0.3.0/proofs/storage_shape.bend as Shape
6import stelliferous@0.0.3.0/proofs/storage_readback.bend as Readback
7import stelliferous@0.0.3.0/proofs/u32_full_range.bend as FullRange
8import stelliferous@0.0.3.0/proofs/u32_comparison.bend as Comparison
9import stelliferous@0.0.3.0/proofs/natural_addition.bend as Addition
10import stelliferous@0.0.3.0/proofs/nat_order.bend as Order
11import stelliferous@0.0.3.0/proofs/nat_to_u32_bounds.bend as Bounds
12import stelliferous@0.0.3.0/proofs/word_encoding.bend as Words
13import stelliferous@0.0.3.0/proofs/nat_interval.bend as Interval
14import stelliferous@0.0.3.0/proofs/nat_division.bend as Division
15import stelliferous@0.0.3.0/proofs/loop_projection.bend as Projection
16import stelliferous@0.0.3.0/proofs/bounded_u32_arithmetic.bend as NativeArithmetic
17
18def end_position(~Element: Data,values: List<&2,Element>,offset: U32) -> U32:
19 match values:
20 case Nil{}: offset
21 case head <> rest: end_position(~Element,rest,(offset + 1 : U32))
22
23def end_position_length(~Element: Data,values: List<&2,Element>,+offset: U32) ->
24 {end_position(~Element,values,offset) == (offset + U32.from_nat(List.length(&2,Element,values)) : U32) : U32}:
25 match values:
26 case Nil{}: Equal.sym(U32,(offset + 0 : U32),offset,NativeArithmetic.add_zero(offset))
27 case head <> +rest:
28 Equal.trans(U32,end_position(~Element,rest,(offset + 1 : U32)),((offset + 1 : U32) + U32.from_nat(List.length(&2,Element,rest)) : U32),
29 (offset + U32.from_nat(1n+List.length(&2,Element,rest)) : U32),end_position_length(~Element,rest,(offset + 1 : U32)),
30 Equal.sym(U32,(offset + U32.from_nat(1n+List.length(&2,Element,rest)) : U32),((offset + 1 : U32) + U32.from_nat(List.length(&2,Element,rest)) : U32),
31 Projection.indexed_successor(offset,List.length(&2,Element,rest))))
32
33def append_length(~Element: Data,left: List<&2,Element>,+right: List<&2,Element>) ->
34 {List.length(&2,Element,List.append(&2,Element,left,right)) == Nat.add(List.length(&2,Element,left),List.length(&2,Element,right)) : Nat}:
35 match left:
36 case Nil{}: {==}
37 case head <> +rest:
38 %append_length(~Element,rest,right) : {1n+List.length(&2,Element,List.append(&2,Element,rest,right)) == 1n+_ : Nat}
39 {==}
40
41def concatenated(~Element: Data,+first: List<&2,Element>,+second: List<&2,Element>,+offset: U32,+tree: Tree.Tree<Element>) ->
42 {Tree.write_sequence(~Element,List.append(&2,Element,first,second),offset,tree) ==
43 Tree.write_sequence(~Element,second,end_position(~Element,first,offset),Tree.write_sequence(~Element,first,offset,tree)) : Tree.Tree<Element>}:
44 match first:
45 case Nil{}: {==}
46 case +head <> +rest: concatenated(~Element,rest,second,(offset + 1 : U32),Tree.write(Element,tree,offset,head))
47
48def at(~Element: Data,+fallback: Element,index: Nat,values: List<&2,Element>) -> Element:
49 match index values:
50 case 0n Nil{}: fallback
51 case 0n head <> tail: head
52 case 1n+rest Nil{}: fallback
53 case 1n+rest head <> tail: at(~Element,fallback,rest,tail)
54
55# Generic ordered enumeration; the parameter bridge keeps its F32 wrappers.
56def enumerate(~Element: Data,~Context: Data,~value: Context -> Nat -> Element,remaining: Nat,+first: Nat,+context: Context) -> List<&2,Element>:
57 match remaining:
58 case 0n: []
59 case 1n+rest: value(context,first) <> enumerate(~Element,~Context,~value,rest,1n+first,context)
60
61def enumerate_length(~Element: Data,~Context: Data,~value: Context -> Nat -> Element,remaining: Nat,+first: Nat,+context: Context) -> {List.length(&2,Element,enumerate(~Element,~Context,~value,remaining,first,context)) == remaining : Nat}:
62 match remaining:
63 case 0n: {==}
64 case 1n+ +rest:
65 %enumerate_length(~Element,~Context,~value,rest,1n+first,context) : {1n+List.length(&2,Element,enumerate(~Element,~Context,~value,rest,1n+first,context)) == 1n+_ : Nat}
66 {==}
67
68def enumerate_at(~Element: Data,~Context: Data,~value: Context -> Nat -> Element,+fallback: Element,remaining: Nat,index: Nat,+first: Nat,+context: Context,within: {Nat.is_lt(index,remaining) == True{} : Bool}) ->
69 {at(~Element,fallback,index,enumerate(~Element,~Context,~value,remaining,first,context)) == value(context,Nat.add(first,index)) : Element}:
70 match remaining index:
71 case 0n 0n: Empty.absurd({fallback == value(context,Nat.add(first,0n)) : Element},Words.false_true(within))
72 case 0n 1n+index: Empty.absurd({fallback == value(context,Nat.add(first,1n+index)) : Element},Words.false_true(within))
73 case 1n+rest 0n:
74 %Equal.sym(Nat,Nat.add(first,0n),first,Addition.zero_right(first)) : {value(context,first) == value(context,_) : Element}
75 {==}
76 case 1n+ +rest 1n+ +previous:
77 %Equal.sym(Nat,Nat.add(first,1n+previous),1n+Nat.add(first,previous),Addition.successor_right(first,previous)) : {at(~Element,fallback,previous,enumerate(~Element,~Context,~value,rest,1n+first,context)) == value(context,_) : Element}
78 enumerate_at(~Element,~Context,~value,fallback,rest,previous,1n+first,context,within)
79
80def inside(+index: Nat,+capacity: U32,+bound: {Nat.is_lt(index,U32.to_nat(capacity)) == True{} : Bool}) -> {U32.is_lt(U32.from_nat(index),capacity) == True{} : Bool}:
81 %Equal.sym(Bool,U32.is_lt(U32.from_nat(index),capacity),Nat.is_lt(U32.to_nat(U32.from_nat(index)),U32.to_nat(capacity)),Comparison.lt(U32.from_nat(index),capacity)) : {_ == True{} : Bool}
82 %Equal.sym(Nat,U32.to_nat(U32.from_nat(index)),index,FullRange.roundtrip(index,capacity,Bounds.strict_le(index,U32.to_nat(capacity),bound))) : {Nat.is_lt(_,U32.to_nat(capacity)) == True{} : Bool}
83 bound
84
85def distinct(+first: Nat,+second: Nat,+capacity: U32,+first_bound: {Nat.is_lt(first,U32.to_nat(capacity)) == True{} : Bool},+second_bound: {Nat.is_lt(second,U32.to_nat(capacity)) == True{} : Bool},ordered: {Nat.is_lt(second,first) == True{} : Bool}) -> {U32.is_eq(U32.from_nat(first),U32.from_nat(second)) == False{} : Bool}:
86 %Equal.sym(Bool,U32.is_eq(U32.from_nat(first),U32.from_nat(second)),Nat.is_eq(U32.to_nat(U32.from_nat(first)),U32.to_nat(U32.from_nat(second))),Comparison.eq(U32.from_nat(first),U32.from_nat(second))) : {_ == False{} : Bool}
87 %Equal.sym(Nat,U32.to_nat(U32.from_nat(first)),first,FullRange.roundtrip(first,capacity,Bounds.strict_le(first,U32.to_nat(capacity),first_bound))) : {Nat.is_eq(_,U32.to_nat(U32.from_nat(second))) == False{} : Bool}
88 %Equal.sym(Nat,U32.to_nat(U32.from_nat(second)),second,FullRange.roundtrip(second,capacity,Bounds.strict_le(second,U32.to_nat(capacity),second_bound))) : {Nat.is_eq(first,_) == False{} : Bool}
89 %Equal.sym(Bool,Nat.is_eq(first,second),Nat.is_eq(second,first),Order.equal_symmetric(first,second)) : {_ == False{} : Bool}
90 Order.less_not_equal(second,first,ordered)
91
92def preserved(~Element: Data,values: List<&2,Element>,+offset: Nat,+query: Nat,+depth: Nat,+tree: Tree.Tree<Element>,+balanced: Shape.Balanced(Element,depth,tree),+limit: {Nat.is_le(depth,30n) == True{} : Bool},
93 +room: {Nat.is_le(Nat.add(offset,List.length(&2,Element,values)),U32.to_nat(Tree.capacity(Element,tree))) == True{} : Bool},
94 +query_inside: {Nat.is_lt(query,U32.to_nat(Tree.capacity(Element,tree))) == True{} : Bool},+before: {Nat.is_lt(query,offset) == True{} : Bool}) ->
95 {Tree.read(Element,Tree.write_sequence(~Element,values,U32.from_nat(offset),tree),U32.from_nat(query)) == Tree.read(Element,tree,U32.from_nat(query)) : Element}:
96 match values:
97 case []: {==}
98 case +head <> +rest:
99 +index_inside = Order.room_index(offset,List.length(&2,Element,rest),U32.to_nat(Tree.capacity(Element,tree)),room)
100 +written = Tree.write(Element,tree,U32.from_nat(offset),head)
101 +capacity = Readback.write_capacity(~Element,tree,U32.from_nat(offset),head)
102 %Equal.sym(U32,(U32.from_nat(offset) + 1 : U32),U32.from_nat(1n+offset),Bounds.increment_encoded(offset)) :
103 {Tree.read(Element,Tree.write_sequence(~Element,rest,_,written),U32.from_nat(query)) == Tree.read(Element,tree,U32.from_nat(query)) : Element}
104 Equal.trans(Element,Tree.read(Element,Tree.write_sequence(~Element,rest,U32.from_nat(1n+offset),written),U32.from_nat(query)),Tree.read(Element,written,U32.from_nat(query)),Tree.read(Element,tree,U32.from_nat(query)),
105 preserved(~Element,rest,1n+offset,query,depth,written,Shape.write(Element,depth,tree,U32.from_nat(offset),head,balanced),limit,
106 %Equal.sym(U32,Tree.capacity(Element,written),Tree.capacity(Element,tree),capacity) : {Nat.is_le(Nat.add(1n+offset,List.length(&2,Element,rest)),U32.to_nat(_)) == True{} : Bool}
107 Order.advance_room(offset,List.length(&2,Element,rest),U32.to_nat(Tree.capacity(Element,tree)),room),
108 %Equal.sym(U32,Tree.capacity(Element,written),Tree.capacity(Element,tree),capacity) : {Nat.is_lt(query,U32.to_nat(_)) == True{} : Bool} query_inside,
109 Order.lt_succ(query,offset,Bounds.strict_le(query,offset,before))),
110 Readback.read_preserved(~Element,depth,tree,U32.from_nat(offset),U32.from_nat(query),head,balanced,limit,inside(offset,Tree.capacity(Element,tree),index_inside),inside(query,Tree.capacity(Element,tree),query_inside),distinct(offset,query,Tree.capacity(Element,tree),index_inside,query_inside,before)))
111
112def outside(~Element: Data,values: List<&2,Element>,+offset: Nat,+query: Nat,+depth: Nat,+tree: Tree.Tree<Element>,+balanced: Shape.Balanced(Element,depth,tree),+limit: {Nat.is_le(depth,30n) == True{} : Bool},
113 +room: {Nat.is_le(Nat.add(offset,List.length(&2,Element,values)),U32.to_nat(Tree.capacity(Element,tree))) == True{} : Bool},
114 +query_inside: {Nat.is_lt(query,U32.to_nat(Tree.capacity(Element,tree))) == True{} : Bool},
115 +separate: Interval.Outside<offset,List.length(&2,Element,values),query>) ->
116 {Tree.read(Element,Tree.write_sequence(~Element,values,U32.from_nat(offset),tree),U32.from_nat(query)) == Tree.read(Element,tree,U32.from_nat(query)) : Element}:
117 match values:
118 case Nil{}: {==}
119 case +head <> +rest:
120 +capacity = Tree.capacity(Element,tree)
121 +index_inside = Order.room_index(offset,List.length(&2,Element,rest),U32.to_nat(capacity),room)
122 +written = Tree.write(Element,tree,U32.from_nat(offset),head)
123 +same_capacity = Readback.write_capacity(~Element,tree,U32.from_nat(offset),head)
124 +different = {
125 %Equal.sym(Bool,U32.is_eq(U32.from_nat(offset),U32.from_nat(query)),Nat.is_eq(U32.to_nat(U32.from_nat(offset)),U32.to_nat(U32.from_nat(query))),Comparison.eq(U32.from_nat(offset),U32.from_nat(query))) : {_ == False{} : Bool}
126 %Equal.sym(Nat,U32.to_nat(U32.from_nat(offset)),offset,FullRange.roundtrip(offset,capacity,Bounds.strict_le(offset,U32.to_nat(capacity),index_inside))) : {Nat.is_eq(_,U32.to_nat(U32.from_nat(query))) == False{} : Bool}
127 %Equal.sym(Nat,U32.to_nat(U32.from_nat(query)),query,FullRange.roundtrip(query,capacity,Bounds.strict_le(query,U32.to_nat(capacity),query_inside))) : {Nat.is_eq(offset,_) == False{} : Bool}
128 %Order.equal_symmetric(query,offset) : {_ == False{} : Bool}
129 Interval.outside_head(offset,List.length(&2,Element,rest),query,separate) : {U32.is_eq(U32.from_nat(offset),U32.from_nat(query)) == False{} : Bool}}
130 %Equal.sym(U32,(U32.from_nat(offset) + 1 : U32),U32.from_nat(1n+offset),Bounds.increment_encoded(offset)) :
131 {Tree.read(Element,Tree.write_sequence(~Element,rest,_,written),U32.from_nat(query)) == Tree.read(Element,tree,U32.from_nat(query)) : Element}
132 Equal.trans(Element,Tree.read(Element,Tree.write_sequence(~Element,rest,U32.from_nat(1n+offset),written),U32.from_nat(query)),Tree.read(Element,written,U32.from_nat(query)),Tree.read(Element,tree,U32.from_nat(query)),
133 outside(~Element,rest,1n+offset,query,depth,written,Shape.write(Element,depth,tree,U32.from_nat(offset),head,balanced),limit,
134 %Equal.sym(U32,Tree.capacity(Element,written),capacity,same_capacity) : {Nat.is_le(Nat.add(1n+offset,List.length(&2,Element,rest)),U32.to_nat(_)) == True{} : Bool}
135 Order.advance_room(offset,List.length(&2,Element,rest),U32.to_nat(capacity),room),
136 %Equal.sym(U32,Tree.capacity(Element,written),capacity,same_capacity) : {Nat.is_lt(query,U32.to_nat(_)) == True{} : Bool} query_inside,
137 Interval.outside_tail(offset,List.length(&2,Element,rest),query,separate)),
138 Readback.read_preserved(~Element,depth,tree,U32.from_nat(offset),U32.from_nat(query),head,balanced,limit,inside(offset,capacity,index_inside),inside(query,capacity,query_inside),different))
139
140def listed(~Element: Data,+values: List<&2,Element>,index: Nat,+offset: Nat,+depth: Nat,+tree: Tree.Tree<Element>,+fallback: Element,+balanced: Shape.Balanced(Element,depth,tree),+limit: {Nat.is_le(depth,30n) == True{} : Bool},
141 +room: {Nat.is_le(Nat.add(offset,List.length(&2,Element,values)),U32.to_nat(Tree.capacity(Element,tree))) == True{} : Bool},
142 within: {Nat.is_lt(index,List.length(&2,Element,values)) == True{} : Bool}) ->
143 {Tree.read(Element,Tree.write_sequence(~Element,values,U32.from_nat(offset),tree),U32.from_nat(Nat.add(offset,index))) == at(~Element,fallback,index,values) : Element}:
144 match values index:
145 case [] 0n: Empty.absurd({Tree.read(Element,tree,U32.from_nat(Nat.add(offset,0n))) == fallback : Element},Words.false_true(within))
146 case [] 1n+rest: Empty.absurd({Tree.read(Element,tree,U32.from_nat(Nat.add(offset,1n+rest))) == fallback : Element},Words.false_true(within))
147 case +head <> +rest 0n:
148 +written = Tree.write(Element,tree,U32.from_nat(offset),head)
149 +capacity = Readback.write_capacity(~Element,tree,U32.from_nat(offset),head)
150 %Equal.sym(Nat,Nat.add(offset,0n),offset,Addition.zero_right(offset)) : {Tree.read(Element,Tree.write_sequence(~Element,rest,(U32.from_nat(offset) + 1 : U32),written),U32.from_nat(_)) == head : Element}
151 %Equal.sym(U32,(U32.from_nat(offset) + 1 : U32),U32.from_nat(1n+offset),Bounds.increment_encoded(offset)) : {Tree.read(Element,Tree.write_sequence(~Element,rest,_,written),U32.from_nat(offset)) == head : Element}
152 Equal.trans(Element,Tree.read(Element,Tree.write_sequence(~Element,rest,U32.from_nat(1n+offset),written),U32.from_nat(offset)),Tree.read(Element,written,U32.from_nat(offset)),head,
153 preserved(~Element,rest,1n+offset,offset,depth,written,Shape.write(Element,depth,tree,U32.from_nat(offset),head,balanced),limit,
154 %Equal.sym(U32,Tree.capacity(Element,written),Tree.capacity(Element,tree),capacity) : {Nat.is_le(Nat.add(1n+offset,List.length(&2,Element,rest)),U32.to_nat(_)) == True{} : Bool}
155 Order.advance_room(offset,List.length(&2,Element,rest),U32.to_nat(Tree.capacity(Element,tree)),room),
156 %Equal.sym(U32,Tree.capacity(Element,written),Tree.capacity(Element,tree),capacity) : {Nat.is_lt(offset,U32.to_nat(_)) == True{} : Bool}
157 Order.room_index(offset,List.length(&2,Element,rest),U32.to_nat(Tree.capacity(Element,tree)),room),Order.lt_succ(offset,offset,Order.reflexive(offset))),
158 Readback.read_written(~Element,tree,U32.from_nat(offset),head))
159 case +head <> +rest 1n+ +previous:
160 +written = Tree.write(Element,tree,U32.from_nat(offset),head)
161 +capacity = Readback.write_capacity(~Element,tree,U32.from_nat(offset),head)
162 %Equal.sym(U32,(U32.from_nat(offset) + 1 : U32),U32.from_nat(1n+offset),Bounds.increment_encoded(offset)) : {Tree.read(Element,Tree.write_sequence(~Element,rest,_,written),U32.from_nat(Nat.add(offset,1n+previous))) == at(~Element,fallback,previous,rest) : Element}
163 %Equal.sym(Nat,Nat.add(offset,1n+previous),1n+Nat.add(offset,previous),Addition.successor_right(offset,previous)) : {Tree.read(Element,Tree.write_sequence(~Element,rest,U32.from_nat(1n+offset),written),U32.from_nat(_)) == at(~Element,fallback,previous,rest) : Element}
164 listed(~Element,rest,previous,1n+offset,depth,written,fallback,Shape.write(Element,depth,tree,U32.from_nat(offset),head,balanced),limit,
165 %Equal.sym(U32,Tree.capacity(Element,written),Tree.capacity(Element,tree),capacity) : {Nat.is_le(Nat.add(1n+offset,List.length(&2,Element,rest)),U32.to_nat(_)) == True{} : Bool}
166 Order.advance_room(offset,List.length(&2,Element,rest),U32.to_nat(Tree.capacity(Element,tree)),room),within)
167
168# Readback from concatenated lists preserves each rectangular row's order.
169def appended_before(~Element: Data,+fallback: Element,+left: List<&2,Element>,+right: List<&2,Element>,index: Nat,
170 inside: {Nat.is_lt(index,List.length(&2,Element,left)) == True{} : Bool}) ->
171 {at(~Element,fallback,index,List.append(&2,Element,left,right)) == at(~Element,fallback,index,left) : Element}:
172 match left index:
173 case Nil{} index:
174 Empty.absurd({at(~Element,fallback,index,right) == at(~Element,fallback,index,[]) : Element},
175 Words.false_true(Equal.trans(Bool,False{},Nat.is_lt(index,0n),True{},Equal.sym(Bool,Nat.is_lt(index,0n),False{},Division.lt_zero(index)),inside)))
176 case head <> rest 0n: {==}
177 case head <> +rest 1n+ +previous: appended_before(~Element,fallback,rest,right,previous,inside)
178
179def appended_after(~Element: Data,+fallback: Element,left: List<&2,Element>,+right: List<&2,Element>,+index: Nat) ->
180 {at(~Element,fallback,Nat.add(List.length(&2,Element,left),index),List.append(&2,Element,left,right)) == at(~Element,fallback,index,right) : Element}:
181 match left:
182 case Nil{}: {==}
183 case head <> rest: appended_after(~Element,fallback,rest,right,index)
184
185def concat_enumerate_at(~Element: Data,~Context: Data,~row: Context -> Nat -> List<&2,Element>,~width: Context -> Nat,
186 ~row_length: @+context: Context -> @+index: Nat -> {List.length(&2,Element,row(context,index)) == width(context) : Nat},
187 +fallback: Element,+rows: Nat,+first: Nat,+row_index: Nat,+column_index: Nat,+context: Context,
188 row_inside: {Nat.is_lt(row_index,rows) == True{} : Bool},+column_inside: {Nat.is_lt(column_index,width(context)) == True{} : Bool}) ->
189 {at(~Element,fallback,Nat.add(Nat.mul(row_index,width(context)),column_index),List.concat(&2,Element,enumerate(~List<&2,Element>,~Context,~row,rows,first,context))) ==
190 at(~Element,fallback,column_index,row(context,Nat.add(first,row_index))) : Element}:
191 match rows row_index:
192 case 0n row_index:
193 Empty.absurd({at(~Element,fallback,Nat.add(Nat.mul(row_index,width(context)),column_index),[]) == at(~Element,fallback,column_index,row(context,Nat.add(first,row_index))) : Element},
194 Words.false_true(Equal.trans(Bool,False{},Nat.is_lt(row_index,0n),True{},Equal.sym(Bool,Nat.is_lt(row_index,0n),False{},Division.lt_zero(row_index)),row_inside)))
195 case 1n+ +rest 0n:
196 %Equal.sym(Nat,Nat.add(first,0n),first,Addition.zero_right(first)) :
197 {at(~Element,fallback,column_index,List.append(&2,Element,row(context,first),List.concat(&2,Element,enumerate(~List<&2,Element>,~Context,~row,rest,1n+first,context)))) == at(~Element,fallback,column_index,row(context,_)) : Element}
198 appended_before(~Element,fallback,row(context,first),List.concat(&2,Element,enumerate(~List<&2,Element>,~Context,~row,rest,1n+first,context)),column_index,
199 %Equal.sym(Nat,List.length(&2,Element,row(context,first)),width(context),row_length(context,first)) : {Nat.is_lt(column_index,_) == True{} : Bool} column_inside)
200 case 1n+ +rest 1n+ +previous:
201 +tail_index = Nat.add(Nat.mul(previous,width(context)),column_index)
202 +tail = List.concat(&2,Element,enumerate(~List<&2,Element>,~Context,~row,rest,1n+first,context))
203 %Equal.sym(Nat,Nat.add(first,1n+previous),1n+Nat.add(first,previous),Addition.successor_right(first,previous)) :
204 {at(~Element,fallback,Nat.add(Nat.mul(1n+previous,width(context)),column_index),List.append(&2,Element,row(context,first),tail)) == at(~Element,fallback,column_index,row(context,_)) : Element}
205 %Equal.sym(Nat,Nat.add(Nat.add(width(context),Nat.mul(previous,width(context))),column_index),Nat.add(width(context),tail_index),Addition.associative(width(context),Nat.mul(previous,width(context)),column_index)) :
206 {at(~Element,fallback,_,List.append(&2,Element,row(context,first),tail)) == at(~Element,fallback,column_index,row(context,1n+Nat.add(first,previous))) : Element}
207 %row_length(context,first) :
208 {at(~Element,fallback,Nat.add(_,tail_index),List.append(&2,Element,row(context,first),tail)) == at(~Element,fallback,column_index,row(context,1n+Nat.add(first,previous))) : Element}
209 Equal.trans(Element,at(~Element,fallback,Nat.add(List.length(&2,Element,row(context,first)),tail_index),List.append(&2,Element,row(context,first),tail)),at(~Element,fallback,tail_index,tail),
210 at(~Element,fallback,column_index,row(context,1n+Nat.add(first,previous))),appended_after(~Element,fallback,row(context,first),tail,tail_index),
211 concat_enumerate_at(~Element,~Context,~row,~width,~row_length,fallback,rest,1n+first,previous,column_index,context,row_inside,column_inside))
212
213def concat_enumerate_length(~Element: Data,~Context: Data,~row: Context -> Nat -> List<&2,Element>,~width: Context -> Nat,
214 ~row_length: @+context: Context -> @+index: Nat -> {List.length(&2,Element,row(context,index)) == width(context) : Nat},
215 rows: Nat,+first: Nat,+context: Context) ->
216 {List.length(&2,Element,List.concat(&2,Element,enumerate(~List<&2,Element>,~Context,~row,rows,first,context))) == Nat.mul(rows,width(context)) : Nat}:
217 match rows:
218 case 0n: {==}
219 case 1n+ +rest:
220 +head = row(context,first)
221 +tail = List.concat(&2,Element,enumerate(~List<&2,Element>,~Context,~row,rest,1n+first,context))
222 %Equal.sym(Nat,List.length(&2,Element,List.append(&2,Element,head,tail)),Nat.add(List.length(&2,Element,head),List.length(&2,Element,tail)),append_length(~Element,head,tail)) :
223 {_ == Nat.add(width(context),Nat.mul(rest,width(context))) : Nat}
224 %Equal.sym(Nat,List.length(&2,Element,head),width(context),row_length(context,first)) :
225 {Nat.add(_,List.length(&2,Element,tail)) == Nat.add(width(context),Nat.mul(rest,width(context))) : Nat}
226 %Equal.sym(Nat,List.length(&2,Element,tail),Nat.mul(rest,width(context)),concat_enumerate_length(~Element,~Context,~row,~width,~row_length,rest,1n+first,context)) :
227 {Nat.add(width(context),_) == Nat.add(width(context),Nat.mul(rest,width(context))) : Nat}
228 {==}