proofs/traversal_array_refinement.bend
stelliferous@0.0.3.0 · 1,069 lines · 0 definitions
1# The same ownership-parameterized state is used by implementation and model.
2# One read contract and one generic Array.set refinement cover every traversal.
3import Base
4import stelliferous@0.0.3.0/traversal_array.bend as Traversal
5import stelliferous@0.0.3.0/traversal_loop.bend as Loop
6import stelliferous@0.0.3.0/proofs/storage_tree_model.bend as Tree
7import stelliferous@0.0.3.0/proofs/storage_refinement.bend as StorageLaws
8import stelliferous@0.0.3.0/proofs/loop_projection.bend as Projection
9import stelliferous@0.0.3.0/proofs/natural_addition.bend as Addition
10import stelliferous@0.0.3.0/proofs/nat_to_u32_bounds.bend as Bounds
11import stelliferous@0.0.3.0/proofs/nat_order.bend as Order
12import stelliferous@0.0.3.0/proofs/sequence_membership.bend as Members
13import stelliferous@0.0.3.0/proofs/storage_shape.bend as Shape
14import stelliferous@0.0.3.0/proofs/ordered_ranges.bend as Ranges
15import stelliferous@0.0.3.0/proofs/list_storage_readback.bend as ListRead
16import stelliferous@0.0.3.0/proofs/bounded_u32_arithmetic.bend as Arithmetic
17
18def collect_values_context(~ownership: Quant,~Runtime: Kind(ownership),~Model: Data,~Context: Data,~pack: Context -> Model -> Runtime,values: List<&2,Model>,+context: Context) -> List<ownership,Runtime>:
19 match values:
20 case Nil{}: []
21 case head <> tail: pack(context,head) <> collect_values_context(~ownership,~Runtime,~Model,~Context,~pack,tail,context)
22
23def collect_values(~ownership: Quant,~Runtime: Kind(ownership),~Model: Data,~pack: Model -> Runtime,values: List<&2,Model>) -> List<ownership,Runtime>:
24 collect_values_context(~ownership,~Runtime,~Model,~Unit,~{context => pack : Unit -> Model -> Runtime},values,Unit{})
25
26def collect_result(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,
27 ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,result: Source & List<&2,Model>) -> Reader & List<ownership,Runtime>:
28 (+source,+values) = result
29 (pack_reader(source),collect_values(~ownership,~Runtime,~Model,~pack_value,values))
30
31def collected_result(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,~Context: Data,
32 ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,result: Source & Traversal.Collected<&2,Context,Model>) -> Reader & Traversal.Collected<ownership,Context,Runtime>:
33 (source,Traversal.Collected{context,value}) = result
34 (pack_reader(source),Traversal.Collected{context,pack_value(value)})
35
36def collect_prepend_matches(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,
37 ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,+value: Model,result: Source & List<&2,Model>) ->
38 {Traversal.collect_prepend(~ownership,~Reader,~Runtime,pack_value(value),collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,result)) ==
39 collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,Traversal.collect_prepend(~&2,~Source,~Model,value,result)) : Reader & List<ownership,Runtime>}:
40 (+source,+values) = result
41 {==}
42
43def collect_next_matches(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,~Context: Data,
44 ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,head: Source & Traversal.Collected<&2,Context,Model>,
45 -runtime_tail: Reader -> Context -> Reader & List<ownership,Runtime>,model_tail: Source -> Context -> Source & List<&2,Model>,
46 tail_matches: @+source: Source -> @+context: Context ->
47 {runtime_tail(pack_reader(source),context) == collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,model_tail(source,context)) : Reader & List<ownership,Runtime>}) ->
48 {Traversal.collect_next(~ownership,~Reader,~Runtime,~Context,collected_result(~ownership,~Reader,~Source,~Runtime,~Model,~Context,~pack_reader,~pack_value,head),runtime_tail) ==
49 collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,Traversal.collect_next(~&2,~Source,~Model,~Context,head,model_tail)) : Reader & List<ownership,Runtime>}:
50 (+source,Traversal.Collected{+context,+value}) = head
51 %Equal.sym(Reader & List<ownership,Runtime>,runtime_tail(pack_reader(source),context),collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,model_tail(source,context)),tail_matches(source,context)) :
52 {Traversal.collect_prepend(~ownership,~Reader,~Runtime,pack_value(value),_) == collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,Traversal.collect_prepend(~&2,~Source,~Model,value,model_tail(source,context))) : Reader & List<ownership,Runtime>}
53 collect_prepend_matches(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,value,model_tail(source,context))
54
55def collect_refines_model(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,~Context: Data,
56 ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,
57 ~read: Reader -> Context -> Reader & Traversal.Collected<ownership,Context,Runtime>,~model_read: Source -> Context -> Source & Traversal.Collected<&2,Context,Model>,
58 ~read_matches: @+source: Source -> @+context: Context ->
59 {read(pack_reader(source),context) == collected_result(~ownership,~Reader,~Source,~Runtime,~Model,~Context,~pack_reader,~pack_value,model_read(source,context)) : Reader & Traversal.Collected<ownership,Context,Runtime>},
60 count: Nat,+source: Source,+context: Context) ->
61 {Traversal.collect(~ownership,~Reader,~Runtime,~Context,~read,count,pack_reader(source),context) ==
62 collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,Traversal.collect(~&2,~Source,~Model,~Context,~model_read,count,source,context)) : Reader & List<ownership,Runtime>}:
63 match count:
64 case 0n: {==}
65 case 1n+ +rest:
66 %Equal.sym(Reader & Traversal.Collected<ownership,Context,Runtime>,read(pack_reader(source),context),collected_result(~ownership,~Reader,~Source,~Runtime,~Model,~Context,~pack_reader,~pack_value,model_read(source,context)),read_matches(source,context)) :
67 {Traversal.collect_next(~ownership,~Reader,~Runtime,~Context,_,reader => context => Traversal.collect(~ownership,~Reader,~Runtime,~Context,~read,rest,reader,context)) == collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,Traversal.collect(~&2,~Source,~Model,~Context,~model_read,1n+rest,source,context)) : Reader & List<ownership,Runtime>}
68 collect_next_matches(~ownership,~Reader,~Source,~Runtime,~Model,~Context,~pack_reader,~pack_value,model_read(source,context),
69 reader => context => Traversal.collect(~ownership,~Reader,~Runtime,~Context,~read,rest,reader,context),source => context => Traversal.collect(~&2,~Source,~Model,~Context,~model_read,rest,source,context),
70 source => context => collect_refines_model(~ownership,~Reader,~Source,~Runtime,~Model,~Context,~pack_reader,~pack_value,~read,~model_read,~read_matches,rest,source,context))
71
72def collect_identity(~Element: Data,~Context: Data,context: Context,value: Element) -> Element:
73 value
74
75def collect_values_context_identity(~Element: Data,~Context: Data,values: List<&2,Element>,+context: Context) ->
76 {collect_values_context(~&2,~Element,~Element,~Context,~collect_identity(~Element,~Context),values,context) == values : List<&2,Element>}:
77 match values:
78 case Nil{}: {==}
79 case +head <> +rest:
80 Equal.cong(List<&2,Element>,List<&2,Element>,values => head <> values,
81 collect_values_context(~&2,~Element,~Element,~Context,~collect_identity(~Element,~Context),rest,context),rest,collect_values_context_identity(~Element,~Context,rest,context))
82
83def collect_values_identity(~Element: Data,values: List<&2,Element>) ->
84 {collect_values(~&2,~Element,~Element,~(value => value),values) == values : List<&2,Element>}:
85 collect_values_context_identity(~Element,~Unit,values,Unit{})
86
87def collect_result_identity(~Reader: Type,~Source: Data,~Element: Data,~pack_reader: Source -> Reader,result: Source & List<&2,Element>) ->
88 {collect_result(~&2,~Reader,~Source,~Element,~Element,~pack_reader,~(value => value),result) ==
89 (pack_reader(Pair.fst(Source,List<&2,Element>,result)),Pair.snd(Source,List<&2,Element>,result)) : Reader & List<&2,Element>}:
90 (source,+values) = result
91 Equal.cong(List<&2,Element>,Reader & List<&2,Element>,values => (pack_reader(source),values),collect_values(~&2,~Element,~Element,~(value => value),values),values,collect_values_identity(~Element,values))
92
93def collect_prepend_source(~Source: Data,~Element: Data,+value: Element,result: Source & List<&2,Element>) ->
94 {Pair.fst(Source,List<&2,Element>,Traversal.collect_prepend(~&2,~Source,~Element,value,result)) == Pair.fst(Source,List<&2,Element>,result) : Source}:
95 (source,values) = result
96 {==}
97
98def collect_next_source(~Source: Data,~Element: Data,~Context: Data,head: Source & Traversal.Collected<&2,Context,Element>,
99 tail: Source -> Context -> Source & List<&2,Element>,
100 kept: @+source: Source -> @+context: Context -> {Pair.fst(Source,List<&2,Element>,tail(source,context)) == source : Source}) ->
101 {Pair.fst(Source,List<&2,Element>,Traversal.collect_next(~&2,~Source,~Element,~Context,head,tail)) == Pair.fst(Source,Traversal.Collected<&2,Context,Element>,head) : Source}:
102 (+source,+collected) = head
103 Traversal.Collected{+context,+value} = collected
104 Equal.trans(Source,Pair.fst(Source,List<&2,Element>,Traversal.collect_prepend(~&2,~Source,~Element,value,tail(source,context))),Pair.fst(Source,List<&2,Element>,tail(source,context)),source,collect_prepend_source(~Source,~Element,value,tail(source,context)),kept(source,context))
105
106def collect_preserves_source(~Source: Data,~Element: Data,~Context: Data,
107 ~read: Source -> Context -> Source & Traversal.Collected<&2,Context,Element>,
108 ~kept: @+source: Source -> @+context: Context -> {Pair.fst(Source,Traversal.Collected<&2,Context,Element>,read(source,context)) == source : Source},
109 count: Nat,+source: Source,+context: Context) ->
110 {Pair.fst(Source,List<&2,Element>,Traversal.collect(~&2,~Source,~Element,~Context,~read,count,source,context)) == source : Source}:
111 match count:
112 case 0n: {==}
113 case 1n+ +rest:
114 Equal.trans(Source,Pair.fst(Source,List<&2,Element>,Traversal.collect(~&2,~Source,~Element,~Context,~read,1n+rest,source,context)),Pair.fst(Source,Traversal.Collected<&2,Context,Element>,read(source,context)),source,
115 collect_next_source(~Source,~Element,~Context,read(source,context),source => context => Traversal.collect(~&2,~Source,~Element,~Context,~read,rest,source,context),
116 source => context => collect_preserves_source(~Source,~Element,~Context,~read,~kept,rest,source,context)),kept(source,context))
117
118def collect_list_next_source(~Source: Data,~Element: Data,head: Source & Element,tail: Source -> Source & List<&2,Element>,
119 kept: @+source: Source -> {Pair.fst(Source,List<&2,Element>,tail(source)) == source : Source}) ->
120 {Pair.fst(Source,List<&2,Element>,Traversal.collect_list_next(~&2,~Source,~Element,head,tail)) == Pair.fst(Source,Element,head) : Source}:
121 (+source,+value) = head
122 Equal.trans(Source,Pair.fst(Source,List<&2,Element>,Traversal.collect_prepend(~&2,~Source,~Element,value,tail(source))),Pair.fst(Source,List<&2,Element>,tail(source)),source,
123 collect_prepend_source(~Source,~Element,value,tail(source)),kept(source))
124
125# A keyed collection whose reads keep the source keeps it.
126def collect_list_preserves_source(~Source: Data,~Element: Data,~Key: Data,~Context: Data,
127 ~read: Source -> Context -> Key -> Source & Element,
128 ~kept: @+source: Source -> @+context: Context -> @+key: Key -> {Pair.fst(Source,Element,read(source,context,key)) == source : Source},
129 keys: List<&2,Key>,+source: Source,+context: Context) ->
130 {Pair.fst(Source,List<&2,Element>,Traversal.collect_list(~&2,~Source,~Element,~Key,~Context,~read,keys,source,context)) == source : Source}:
131 match keys:
132 case Nil{}: {==}
133 case Con{+key,+rest}:
134 Equal.trans(Source,Pair.fst(Source,List<&2,Element>,Traversal.collect_list(~&2,~Source,~Element,~Key,~Context,~read,Con{key,rest},source,context)),
135 Pair.fst(Source,Element,read(source,context,key)),source,
136 collect_list_next_source(~Source,~Element,read(source,context,key),source => Traversal.collect_list(~&2,~Source,~Element,~Key,~Context,~read,rest,source,context),
137 source => collect_list_preserves_source(~Source,~Element,~Key,~Context,~read,~kept,rest,source,context)),kept(source,context,key))
138
139def collect_list_read(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,
140 ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,result: Source & Model) -> Reader & Runtime:
141 (source,value) = result
142 (pack_reader(source),pack_value(value))
143
144def collect_list_next_matches(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,
145 ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,head: Source & Model,
146 -runtime_tail: Reader -> Reader & List<ownership,Runtime>,model_tail: Source -> Source & List<&2,Model>,
147 tail_matches: @+source: Source ->
148 {runtime_tail(pack_reader(source)) == collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,model_tail(source)) : Reader & List<ownership,Runtime>}) ->
149 {Traversal.collect_list_next(~ownership,~Reader,~Runtime,collect_list_read(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,head),runtime_tail) ==
150 collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,Traversal.collect_list_next(~&2,~Source,~Model,head,model_tail)) : Reader & List<ownership,Runtime>}:
151 (+source,+value) = head
152 %Equal.sym(Reader & List<ownership,Runtime>,runtime_tail(pack_reader(source)),collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,model_tail(source)),tail_matches(source)) :
153 {Traversal.collect_prepend(~ownership,~Reader,~Runtime,pack_value(value),_) == collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,Traversal.collect_prepend(~&2,~Source,~Model,value,model_tail(source))) : Reader & List<ownership,Runtime>}
154 collect_prepend_matches(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,value,model_tail(source))
155
156def collect_list_refines_model(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,~Key: Data,~Context: Data,
157 ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,
158 ~read: Reader -> Context -> Key -> Reader & Runtime,~model_read: Source -> Context -> Key -> Source & Model,
159 ~read_matches: @+source: Source -> @+context: Context -> @+key: Key ->
160 {read(pack_reader(source),context,key) == collect_list_read(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,model_read(source,context,key)) : Reader & Runtime},
161 keys: List<&2,Key>,+source: Source,+context: Context) ->
162 {Traversal.collect_list(~ownership,~Reader,~Runtime,~Key,~Context,~read,keys,pack_reader(source),context) ==
163 collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,Traversal.collect_list(~&2,~Source,~Model,~Key,~Context,~model_read,keys,source,context)) : Reader & List<ownership,Runtime>}:
164 match keys:
165 case Nil{}: {==}
166 case +key <> +rest:
167 %Equal.sym(Reader & Runtime,read(pack_reader(source),context,key),collect_list_read(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,model_read(source,context,key)),read_matches(source,context,key)) :
168 {Traversal.collect_list_next(~ownership,~Reader,~Runtime,_,reader => Traversal.collect_list(~ownership,~Reader,~Runtime,~Key,~Context,~read,rest,reader,context)) == collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,Traversal.collect_list(~&2,~Source,~Model,~Key,~Context,~model_read,keys,source,context)) : Reader & List<ownership,Runtime>}
169 collect_list_next_matches(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,model_read(source,context,key),
170 reader => Traversal.collect_list(~ownership,~Reader,~Runtime,~Key,~Context,~read,rest,reader,context),source => Traversal.collect_list(~&2,~Source,~Model,~Key,~Context,~model_read,rest,source,context),
171 source => collect_list_refines_model(~ownership,~Reader,~Source,~Runtime,~Model,~Key,~Context,~pack_reader,~pack_value,~read,~model_read,~read_matches,rest,source,context))
172
173# The loops gather newest first and reverse once; a gathered prefix stands
174# in front of the recursive collection of the rest.
175def onto(~Source: Data,~Model: Data,gathered: List<&2,Model>,result: Source & List<&2,Model>) -> Source & List<&2,Model>:
176 (+source,+values) = result
177 (source,Traversal.reversed_onto(~&2,~Model,gathered,values))
178
179def onto_empty(~Source: Data,~Model: Data,result: Source & List<&2,Model>) -> {onto(~Source,~Model,[],result) == result : Source & List<&2,Model>}:
180 (+source,+values) = result
181 {==}
182
183def onto_prepend(~Source: Data,~Model: Data,+value: Model,+gathered: List<&2,Model>,result: Source & List<&2,Model>) ->
184 {onto(~Source,~Model,value <> gathered,result) == onto(~Source,~Model,gathered,Traversal.collect_prepend(~&2,~Source,~Model,value,result)) : Source & List<&2,Model>}:
185 (+source,+values) = result
186 {==}
187
188def collect_values_reversed(~ownership: Quant,~Runtime: Kind(ownership),~Model: Data,~pack_value: Model -> Runtime,values: List<&2,Model>,+tail: List<&2,Model>) ->
189 {collect_values(~ownership,~Runtime,~Model,~pack_value,Traversal.reversed_onto(~&2,~Model,values,tail)) ==
190 Traversal.reversed_onto(~ownership,~Runtime,collect_values(~ownership,~Runtime,~Model,~pack_value,values),collect_values(~ownership,~Runtime,~Model,~pack_value,tail)) : List<ownership,Runtime>}:
191 match values:
192 case Nil{}: {==}
193 case +head <> +rest: collect_values_reversed(~ownership,~Runtime,~Model,~pack_value,rest,head <> tail)
194
195def gathering_finished(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,
196 ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,+source: Source,+gathered: List<&2,Model>) ->
197 {(pack_reader(source),Traversal.reversed_onto(~ownership,~Runtime,collect_values(~ownership,~Runtime,~Model,~pack_value,gathered),[])) ==
198 collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,gathered,(source,[]))) : Reader & List<ownership,Runtime>}:
199 Equal.cong(List<ownership,Runtime>,Reader & List<ownership,Runtime>,values => (pack_reader(source),values),
200 Traversal.reversed_onto(~ownership,~Runtime,collect_values(~ownership,~Runtime,~Model,~pack_value,gathered),[]),
201 collect_values(~ownership,~Runtime,~Model,~pack_value,Traversal.reversed_onto(~&2,~Model,gathered,[])),
202 Equal.sym(List<ownership,Runtime>,collect_values(~ownership,~Runtime,~Model,~pack_value,Traversal.reversed_onto(~&2,~Model,gathered,[])),
203 Traversal.reversed_onto(~ownership,~Runtime,collect_values(~ownership,~Runtime,~Model,~pack_value,gathered),[]),
204 collect_values_reversed(~ownership,~Runtime,~Model,~pack_value,gathered,[])))
205
206def gathered_matches(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,~Context: Data,
207 ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,head: Source & Traversal.Collected<&2,Context,Model>,+gathered: List<&2,Model>,
208 -runtime_rest: Traversal.Gathering<&1,ownership,Reader,Runtime,Context> -> Reader & List<ownership,Runtime>,model_rest: Source -> Context -> Source & List<&2,Model>,
209 rest_matches: @+source: Source -> @+context: Context -> @+gathered: List<&2,Model> ->
210 {runtime_rest(Traversal.Gathering{pack_reader(source),context,collect_values(~ownership,~Runtime,~Model,~pack_value,gathered)}) ==
211 collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,gathered,model_rest(source,context))) : Reader & List<ownership,Runtime>}) ->
212 {runtime_rest(Traversal.gathered(~ownership,~Reader,~Runtime,~Context,collected_result(~ownership,~Reader,~Source,~Runtime,~Model,~Context,~pack_reader,~pack_value,head),
213 collect_values(~ownership,~Runtime,~Model,~pack_value,gathered))) ==
214 collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,gathered,Traversal.collect_next(~&2,~Source,~Model,~Context,head,model_rest))) : Reader & List<ownership,Runtime>}:
215 (+source,Traversal.Collected{+context,+value}) = head
216 Equal.trans(Reader & List<ownership,Runtime>,
217 runtime_rest(Traversal.Gathering{pack_reader(source),context,collect_values(~ownership,~Runtime,~Model,~pack_value,value <> gathered)}),
218 collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,value <> gathered,model_rest(source,context))),
219 collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,gathered,Traversal.collect_prepend(~&2,~Source,~Model,value,model_rest(source,context)))),
220 rest_matches(source,context,value <> gathered),
221 Equal.cong(Source & List<&2,Model>,Reader & List<ownership,Runtime>,result => collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,result),
222 onto(~Source,~Model,value <> gathered,model_rest(source,context)),onto(~Source,~Model,gathered,Traversal.collect_prepend(~&2,~Source,~Model,value,model_rest(source,context))),
223 onto_prepend(~Source,~Model,value,gathered,model_rest(source,context))))
224
225def collect_loop_gathers(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,~Context: Data,
226 ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,
227 ~read: Reader -> Context -> Reader & Traversal.Collected<ownership,Context,Runtime>,~model_read: Source -> Context -> Source & Traversal.Collected<&2,Context,Model>,
228 ~read_matches: @+source: Source -> @+context: Context ->
229 {read(pack_reader(source),context) == collected_result(~ownership,~Reader,~Source,~Runtime,~Model,~Context,~pack_reader,~pack_value,model_read(source,context)) : Reader & Traversal.Collected<ownership,Context,Runtime>},
230 count: Nat,+source: Source,+context: Context,+gathered: List<&2,Model>) ->
231 {Traversal.gathering_result(~ownership,~Reader,~Runtime,~Context,
232 Loop.run(~Traversal.Gathering<&1,ownership,Reader,Runtime,Context>,~Traversal.gather_step(~ownership,~Reader,~Runtime,~Context,~read),count,
233 Traversal.Gathering{pack_reader(source),context,collect_values(~ownership,~Runtime,~Model,~pack_value,gathered)})) ==
234 collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,gathered,Traversal.collect(~&2,~Source,~Model,~Context,~model_read,count,source,context))) : Reader & List<ownership,Runtime>}:
235 match count:
236 case 0n: gathering_finished(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,source,gathered)
237 case 1n+ +rest:
238 %Equal.sym(Reader & Traversal.Collected<ownership,Context,Runtime>,read(pack_reader(source),context),collected_result(~ownership,~Reader,~Source,~Runtime,~Model,~Context,~pack_reader,~pack_value,model_read(source,context)),read_matches(source,context)) :
239 {Traversal.gathering_result(~ownership,~Reader,~Runtime,~Context,
240 Loop.run(~Traversal.Gathering<&1,ownership,Reader,Runtime,Context>,~Traversal.gather_step(~ownership,~Reader,~Runtime,~Context,~read),rest,
241 Traversal.gathered(~ownership,~Reader,~Runtime,~Context,_,collect_values(~ownership,~Runtime,~Model,~pack_value,gathered)))) ==
242 collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,gathered,Traversal.collect(~&2,~Source,~Model,~Context,~model_read,1n+rest,source,context))) : Reader & List<ownership,Runtime>}
243 gathered_matches(~ownership,~Reader,~Source,~Runtime,~Model,~Context,~pack_reader,~pack_value,model_read(source,context),gathered,
244 state => Traversal.gathering_result(~ownership,~Reader,~Runtime,~Context,
245 Loop.run(~Traversal.Gathering<&1,ownership,Reader,Runtime,Context>,~Traversal.gather_step(~ownership,~Reader,~Runtime,~Context,~read),rest,state)),
246 source => context => Traversal.collect(~&2,~Source,~Model,~Context,~model_read,rest,source,context),
247 source => context => gathered => collect_loop_gathers(~ownership,~Reader,~Source,~Runtime,~Model,~Context,~pack_reader,~pack_value,~read,~model_read,~read_matches,rest,source,context,gathered))
248
249# The collection loop refines the recursive model collection.
250def collect_loop_refines_model(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,~Context: Data,
251 ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,
252 ~read: Reader -> Context -> Reader & Traversal.Collected<ownership,Context,Runtime>,~model_read: Source -> Context -> Source & Traversal.Collected<&2,Context,Model>,
253 ~read_matches: @+source: Source -> @+context: Context ->
254 {read(pack_reader(source),context) == collected_result(~ownership,~Reader,~Source,~Runtime,~Model,~Context,~pack_reader,~pack_value,model_read(source,context)) : Reader & Traversal.Collected<ownership,Context,Runtime>},
255 +count: Nat,+source: Source,+context: Context) ->
256 {Traversal.collect_loop(~ownership,~Reader,~Runtime,~Context,~read,count,pack_reader(source),context) ==
257 collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,Traversal.collect(~&2,~Source,~Model,~Context,~model_read,count,source,context)) : Reader & List<ownership,Runtime>}:
258 %onto_empty(~Source,~Model,Traversal.collect(~&2,~Source,~Model,~Context,~model_read,count,source,context)) :
259 {Traversal.collect_loop(~ownership,~Reader,~Runtime,~Context,~read,count,pack_reader(source),context) ==
260 collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,_) : Reader & List<ownership,Runtime>}
261 collect_loop_gathers(~ownership,~Reader,~Source,~Runtime,~Model,~Context,~pack_reader,~pack_value,~read,~model_read,~read_matches,count,source,context,[])
262
263def gathered_key_matches(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,~Key: Data,~Context: Data,
264 ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,head: Source & Model,+rest: List<&2,Key>,+context: Context,+gathered: List<&2,Model>,
265 -runtime_rest: Traversal.Gathering<&1,ownership,Reader,Runtime,Traversal.Keyed<Key,Context>> -> Reader & List<ownership,Runtime>,model_rest: Source -> Source & List<&2,Model>,
266 rest_matches: @+source: Source -> @+gathered: List<&2,Model> ->
267 {runtime_rest(Traversal.Gathering{pack_reader(source),Traversal.Keyed{rest,context},collect_values(~ownership,~Runtime,~Model,~pack_value,gathered)}) ==
268 collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,gathered,model_rest(source))) : Reader & List<ownership,Runtime>}) ->
269 {runtime_rest(Traversal.gathered_key(~ownership,~Reader,~Runtime,~Key,~Context,collect_list_read(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,head),rest,context,
270 collect_values(~ownership,~Runtime,~Model,~pack_value,gathered))) ==
271 collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,gathered,Traversal.collect_list_next(~&2,~Source,~Model,head,model_rest))) : Reader & List<ownership,Runtime>}:
272 (+source,+value) = head
273 Equal.trans(Reader & List<ownership,Runtime>,
274 runtime_rest(Traversal.Gathering{pack_reader(source),Traversal.Keyed{rest,context},collect_values(~ownership,~Runtime,~Model,~pack_value,value <> gathered)}),
275 collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,value <> gathered,model_rest(source))),
276 collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,gathered,Traversal.collect_prepend(~&2,~Source,~Model,value,model_rest(source)))),
277 rest_matches(source,value <> gathered),
278 Equal.cong(Source & List<&2,Model>,Reader & List<ownership,Runtime>,result => collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,result),
279 onto(~Source,~Model,value <> gathered,model_rest(source)),onto(~Source,~Model,gathered,Traversal.collect_prepend(~&2,~Source,~Model,value,model_rest(source))),
280 onto_prepend(~Source,~Model,value,gathered,model_rest(source))))
281
282def collect_list_loop_gathers(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,~Key: Data,~Context: Data,
283 ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,
284 ~read: Reader -> Context -> Key -> Reader & Runtime,~model_read: Source -> Context -> Key -> Source & Model,
285 ~read_matches: @+source: Source -> @+context: Context -> @+key: Key ->
286 {read(pack_reader(source),context,key) == collect_list_read(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,model_read(source,context,key)) : Reader & Runtime},
287 keys: List<&2,Key>,+source: Source,+context: Context,+gathered: List<&2,Model>) ->
288 {Traversal.gathering_result(~ownership,~Reader,~Runtime,~Traversal.Keyed<Key,Context>,
289 Loop.run(~Traversal.Gathering<&1,ownership,Reader,Runtime,Traversal.Keyed<Key,Context>>,~Traversal.gather_key_step(~ownership,~Reader,~Runtime,~Key,~Context,~read),List.length(&2,Key,keys),
290 Traversal.Gathering{pack_reader(source),Traversal.Keyed{keys,context},collect_values(~ownership,~Runtime,~Model,~pack_value,gathered)})) ==
291 collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,gathered,Traversal.collect_list(~&2,~Source,~Model,~Key,~Context,~model_read,keys,source,context))) : Reader & List<ownership,Runtime>}:
292 match keys:
293 case Nil{}: gathering_finished(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,source,gathered)
294 case +key <> +rest:
295 %Equal.sym(Reader & Runtime,read(pack_reader(source),context,key),collect_list_read(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,model_read(source,context,key)),read_matches(source,context,key)) :
296 {Traversal.gathering_result(~ownership,~Reader,~Runtime,~Traversal.Keyed<Key,Context>,
297 Loop.run(~Traversal.Gathering<&1,ownership,Reader,Runtime,Traversal.Keyed<Key,Context>>,~Traversal.gather_key_step(~ownership,~Reader,~Runtime,~Key,~Context,~read),List.length(&2,Key,rest),
298 Traversal.gathered_key(~ownership,~Reader,~Runtime,~Key,~Context,_,rest,context,collect_values(~ownership,~Runtime,~Model,~pack_value,gathered)))) ==
299 collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,onto(~Source,~Model,gathered,Traversal.collect_list(~&2,~Source,~Model,~Key,~Context,~model_read,key <> rest,source,context))) : Reader & List<ownership,Runtime>}
300 gathered_key_matches(~ownership,~Reader,~Source,~Runtime,~Model,~Key,~Context,~pack_reader,~pack_value,model_read(source,context,key),rest,context,gathered,
301 state => Traversal.gathering_result(~ownership,~Reader,~Runtime,~Traversal.Keyed<Key,Context>,
302 Loop.run(~Traversal.Gathering<&1,ownership,Reader,Runtime,Traversal.Keyed<Key,Context>>,~Traversal.gather_key_step(~ownership,~Reader,~Runtime,~Key,~Context,~read),List.length(&2,Key,rest),state)),
303 source => Traversal.collect_list(~&2,~Source,~Model,~Key,~Context,~model_read,rest,source,context),
304 source => gathered => collect_list_loop_gathers(~ownership,~Reader,~Source,~Runtime,~Model,~Key,~Context,~pack_reader,~pack_value,~read,~model_read,~read_matches,rest,source,context,gathered))
305
306# The keyed collection loop refines the recursive model collection.
307def collect_list_loop_refines_model(~ownership: Quant,~Reader: Type,~Source: Data,~Runtime: Kind(ownership),~Model: Data,~Key: Data,~Context: Data,
308 ~pack_reader: Source -> Reader,~pack_value: Model -> Runtime,
309 ~read: Reader -> Context -> Key -> Reader & Runtime,~model_read: Source -> Context -> Key -> Source & Model,
310 ~read_matches: @+source: Source -> @+context: Context -> @+key: Key ->
311 {read(pack_reader(source),context,key) == collect_list_read(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,model_read(source,context,key)) : Reader & Runtime},
312 +keys: List<&2,Key>,+source: Source,+context: Context) ->
313 {Traversal.collect_list_loop(~ownership,~Reader,~Runtime,~Key,~Context,~read,keys,pack_reader(source),context) ==
314 collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,Traversal.collect_list(~&2,~Source,~Model,~Key,~Context,~model_read,keys,source,context)) : Reader & List<ownership,Runtime>}:
315 %onto_empty(~Source,~Model,Traversal.collect_list(~&2,~Source,~Model,~Key,~Context,~model_read,keys,source,context)) :
316 {Traversal.collect_list_loop(~ownership,~Reader,~Runtime,~Key,~Context,~read,keys,pack_reader(source),context) ==
317 collect_result(~ownership,~Reader,~Source,~Runtime,~Model,~pack_reader,~pack_value,_) : Reader & List<ownership,Runtime>}
318 collect_list_loop_gathers(~ownership,~Reader,~Source,~Runtime,~Model,~Key,~Context,~pack_reader,~pack_value,~read,~model_read,~read_matches,keys,source,context,[])
319
320def represent(~Reader: Type,~Model: Data,~Element: Data,~Context: Data,~pack_reader: Model -> Reader,
321 state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) -> Traversal.State<&1,&1,Reader,Array<Element>,Context>:
322 Traversal.State{reader,output,position,context} = state
323 Traversal.State{pack_reader(reader),Tree.pack(Element,output),position,context}
324
325def model_step(~Model: Data,~Element: Data,~Context: Data,
326 ~sample: Model -> Context -> U32 -> Element,~destination: Context -> U32 -> U32,
327 state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) -> Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>:
328 Traversal.State{+reader,output,+position,+context} = state
329 Traversal.State{reader,Tree.write(Element,output,destination(context,position),sample(reader,context,position)),(position + 1 : U32),context}
330
331def model_reader(~Model: Data,~Element: Data,~Context: Data,state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) -> Model:
332 Traversal.State{reader,output,position,context} = state
333 reader
334
335def model_reader_step(~Model: Data,~Element: Data,~Context: Data,~sample: Model -> Context -> U32 -> Element,~destination: Context -> U32 -> U32,
336 +state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) ->
337 {model_reader(~Model,~Element,~Context,model_step(~Model,~Element,~Context,~sample,~destination,state)) == model_reader(~Model,~Element,~Context,state) : Model}:
338 Traversal.State{reader,output,position,context} = state
339 {==}
340
341def model_reader_kept(~Model: Data,~Element: Data,~Context: Data,~sample: Model -> Context -> U32 -> Element,~destination: Context -> U32 -> U32,
342 +count: Nat,+state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) ->
343 {model_reader(~Model,~Element,~Context,Loop.run(~Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>,~model_step(~Model,~Element,~Context,~sample,~destination),count,state)) == model_reader(~Model,~Element,~Context,state) : Model}:
344 Projection.preserves_observation(~Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>,~Model,~model_step(~Model,~Element,~Context,~sample,~destination),~model_reader(~Model,~Element,~Context),~model_reader_step(~Model,~Element,~Context,~sample,~destination),count,state)
345
346def step_refines_model(~Reader: Type,~Model: Data,~Element: Data,~Context: Data,
347 ~pack_reader: Model -> Reader,~read: Reader -> Context -> U32 -> Reader & Element,
348 ~sample: Model -> Context -> U32 -> Element,~destination: Context -> U32 -> U32,
349 ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
350 {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
351 +state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) ->
352 {Traversal.step(~Reader,~Element,~Context,~read,~destination,represent(~Reader,~Model,~Element,~Context,~pack_reader,state)) ==
353 represent(~Reader,~Model,~Element,~Context,~pack_reader,model_step(~Model,~Element,~Context,~sample,~destination,state)) :
354 Traversal.State<&1,&1,Reader,Array<Element>,Context>}:
355 Traversal.State{+reader,+output,+position,+context} = state
356 %Equal.sym(Reader & Element,read(pack_reader(reader),context,position),(pack_reader(reader),sample(reader,context,position)),read_matches(reader,context,position)) :
357 {Traversal.store(~Reader,~Element,~Context,~destination,position,context,Tree.pack(Element,output),_) ==
358 represent(~Reader,~Model,~Element,~Context,~pack_reader,model_step(~Model,~Element,~Context,~sample,~destination,
359 Traversal.State{reader,output,position,context})) : Traversal.State<&1,&1,Reader,Array<Element>,Context>}
360 %Equal.sym(Array<Element>,Array.set(Element,Tree.pack(Element,output),destination(context,position),sample(reader,context,position)),
361 Tree.pack(Element,Tree.write(Element,output,destination(context,position),sample(reader,context,position))),
362 StorageLaws.write(Element,output,destination(context,position),sample(reader,context,position))) :
363 {Traversal.State{pack_reader(reader),_,(position + 1 : U32),context} ==
364 represent(~Reader,~Model,~Element,~Context,~pack_reader,model_step(~Model,~Element,~Context,~sample,~destination,
365 Traversal.State{reader,output,position,context})) : Traversal.State<&1,&1,Reader,Array<Element>,Context>}
366 {==}
367
368def traversal_refines_model(~Reader: Type,~Model: Data,~Element: Data,~Context: Data,
369 ~pack_reader: Model -> Reader,~read: Reader -> Context -> U32 -> Reader & Element,
370 ~sample: Model -> Context -> U32 -> Element,~destination: Context -> U32 -> U32,
371 ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
372 {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
373 +count: Nat,+state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) ->
374 {Traversal.run(~Reader,~Element,~Context,~read,~destination,count,represent(~Reader,~Model,~Element,~Context,~pack_reader,state)) ==
375 represent(~Reader,~Model,~Element,~Context,~pack_reader,
376 Loop.run(~Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>,~model_step(~Model,~Element,~Context,~sample,~destination),count,state)) :
377 Traversal.State<&1,&1,Reader,Array<Element>,Context>}:
378 Projection.iteration_refines_model(~Traversal.State<&1,&1,Reader,Array<Element>,Context>,~Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>,
379 ~Traversal.step(~Reader,~Element,~Context,~read,~destination),~model_step(~Model,~Element,~Context,~sample,~destination),
380 ~represent(~Reader,~Model,~Element,~Context,~pack_reader),~step_refines_model(~Reader,~Model,~Element,~Context,~pack_reader,~read,~sample,~destination,~read_matches),count,state)
381# Concrete copy/zip readers discharge the generic traversal's only read premise.
382
383def pack_tree(~Element: Data,tree: Tree.Tree<Element>) -> Array<Element>:
384 Tree.pack(Element,tree)
385
386def sample_offset(~Element: Data,tree: Tree.Tree<Element>,context: Traversal.Offsets,position: U32) -> Element:
387 Traversal.Offsets{source,destination} = context
388 Tree.read(Element,tree,(source + position : U32))
389
390def offset_read_refines_storage(~Element: Data,+tree: Tree.Tree<Element>,+context: Traversal.Offsets,+position: U32) ->
391 {Traversal.source_offset(~Element,pack_tree(~Element,tree),context,position) ==
392 (pack_tree(~Element,tree),sample_offset(~Element,tree,context,position)) : Array<Element> & Element}:
393 Traversal.Offsets{source,destination} = context
394 StorageLaws.read(Element,tree,(source + position : U32))
395
396def sample_strided(~Element: Data,tree: Tree.Tree<Element>,context: Traversal.Strided,position: U32) -> Element:
397 Traversal.Strided{base,stride} = context
398 Tree.read(Element,tree,(base + position * stride : U32))
399
400def strided_read_refines_storage(~Element: Data,+tree: Tree.Tree<Element>,+context: Traversal.Strided,+position: U32) ->
401 {Traversal.strided(~Element,pack_tree(~Element,tree),context,position) ==
402 (pack_tree(~Element,tree),sample_strided(~Element,tree,context,position)) : Array<Element> & Element}:
403 Traversal.Strided{base,stride} = context
404 StorageLaws.read(Element,tree,(base + position * stride : U32))
405
406def copy_traversal_refines_storage(~Element: Data,+count: Nat,
407 +state: Traversal.State<&2,&2,Tree.Tree<Element>,Tree.Tree<Element>,Traversal.Offsets>) ->
408 {Traversal.run(~Array<Element>,~Element,~Traversal.Offsets,~Traversal.source_offset(~Element),~Traversal.destination_offset,count,
409 represent(~Array<Element>,~Tree.Tree<Element>,~Element,~Traversal.Offsets,~pack_tree(~Element),state)) ==
410 represent(~Array<Element>,~Tree.Tree<Element>,~Element,~Traversal.Offsets,~pack_tree(~Element),
411 Loop.run(~Traversal.State<&2,&2,Tree.Tree<Element>,Tree.Tree<Element>,Traversal.Offsets>,
412 ~model_step(~Tree.Tree<Element>,~Element,~Traversal.Offsets,~sample_offset(~Element),~Traversal.destination_offset),count,state)) :
413 Traversal.State<&1,&1,Array<Element>,Array<Element>,Traversal.Offsets>}:
414 traversal_refines_model(~Array<Element>,~Tree.Tree<Element>,~Element,~Traversal.Offsets,~pack_tree(~Element),
415 ~Traversal.source_offset(~Element),~sample_offset(~Element),~Traversal.destination_offset,~offset_read_refines_storage(~Element),count,state)
416
417# The accumulator is an observation, independent of its numeric interpretation.
418# In particular this theorem never rewrites or reassociates a floating sum.
419def represent_fold(~Reader: Type,~Model: Data,~Accumulator: Data,~Context: Data,~pack_reader: Model -> Reader,
420 state: Traversal.State<&2,&2,Model,Accumulator,Context>) -> Traversal.State<&1,&2,Reader,Accumulator,Context>:
421 Traversal.State{reader,accumulator,position,context} = state
422 Traversal.State{pack_reader(reader),accumulator,position,context}
423
424def model_fold_step(~Model: Data,~Element: Data,~Accumulator: Data,~Context: Data,
425 ~sample: Model -> Context -> U32 -> Element,~combine: Accumulator -> Element -> Accumulator,
426 state: Traversal.State<&2,&2,Model,Accumulator,Context>) -> Traversal.State<&2,&2,Model,Accumulator,Context>:
427 Traversal.State{+reader,accumulator,+position,+context} = state
428 Traversal.State{reader,combine(accumulator,sample(reader,context,position)),(position + 1 : U32),context}
429
430def fold_step_refines_model(~Reader: Type,~Model: Data,~Element: Data,~Accumulator: Data,~Context: Data,
431 ~pack_reader: Model -> Reader,~read: Reader -> Context -> U32 -> Reader & Element,
432 ~sample: Model -> Context -> U32 -> Element,~combine: Accumulator -> Element -> Accumulator,
433 ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
434 {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
435 +state: Traversal.State<&2,&2,Model,Accumulator,Context>) ->
436 {Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine,
437 represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,state)) ==
438 represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,
439 model_fold_step(~Model,~Element,~Accumulator,~Context,~sample,~combine,state)) : Traversal.State<&1,&2,Reader,Accumulator,Context>}:
440 Traversal.State{+reader,+accumulator,+position,+context} = state
441 %Equal.sym(Reader & Element,read(pack_reader(reader),context,position),(pack_reader(reader),sample(reader,context,position)),
442 read_matches(reader,context,position)) :
443 {Traversal.fold_value(~Reader,~Element,~Accumulator,~Context,~combine,accumulator,position,context,_) ==
444 represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,
445 model_fold_step(~Model,~Element,~Accumulator,~Context,~sample,~combine,Traversal.State{reader,accumulator,position,context})) :
446 Traversal.State<&1,&2,Reader,Accumulator,Context>}
447 {==}
448
449def fold_refines_ordered_model(~Reader: Type,~Model: Data,~Element: Data,~Accumulator: Data,~Context: Data,
450 ~pack_reader: Model -> Reader,~read: Reader -> Context -> U32 -> Reader & Element,
451 ~sample: Model -> Context -> U32 -> Element,~combine: Accumulator -> Element -> Accumulator,
452 ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
453 {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
454 +count: Nat,+state: Traversal.State<&2,&2,Model,Accumulator,Context>) ->
455 {Loop.run(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine),
456 count,represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,state)) ==
457 represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,
458 Loop.run(~Traversal.State<&2,&2,Model,Accumulator,Context>,~model_fold_step(~Model,~Element,~Accumulator,~Context,~sample,~combine),count,state)) :
459 Traversal.State<&1,&2,Reader,Accumulator,Context>}:
460 Projection.iteration_refines_model(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.State<&2,&2,Model,Accumulator,Context>,
461 ~Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine),~model_fold_step(~Model,~Element,~Accumulator,~Context,~sample,~combine),
462 ~represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader),
463 ~fold_step_refines_model(~Reader,~Model,~Element,~Accumulator,~Context,~pack_reader,~read,~sample,~combine,~read_matches),count,state)
464
465# The eight reads of a round are the samples at position, position + 1, ...
466def read_last_matches(~Reader: Type,~Model: Data,~Element: Data,~Context: Data,~pack_reader: Model -> Reader,
467 ~read: Reader -> Context -> U32 -> Reader & Element,~sample: Model -> Context -> U32 -> Element,
468 ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
469 {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
470 +reader: Model,+context: Context,+position: U32,+a: Element,+b: Element,+c: Element,+d: Element,+e: Element,+f: Element,+g: Element) ->
471 {Traversal.read_last(~Reader,~Element,a,b,c,d,e,f,g,read(pack_reader(reader),context,position)) ==
472 (pack_reader(reader),Traversal.Eight{a,b,c,d,e,f,g,sample(reader,context,position)}) : Reader & Traversal.Eight<Element>}:
473 %Equal.sym(Reader & Element,read(pack_reader(reader),context,position),(pack_reader(reader),sample(reader,context,position)),read_matches(reader,context,position)) :
474 {Traversal.read_last(~Reader,~Element,a,b,c,d,e,f,g,_) == (pack_reader(reader),Traversal.Eight{a,b,c,d,e,f,g,sample(reader,context,position)}) : Reader & Traversal.Eight<Element>}
475 {==}
476
477def read_seventh_matches(~Reader: Type,~Model: Data,~Element: Data,~Context: Data,~pack_reader: Model -> Reader,
478 ~read: Reader -> Context -> U32 -> Reader & Element,~sample: Model -> Context -> U32 -> Element,
479 ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
480 {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
481 +reader: Model,+context: Context,+position: U32,+a: Element,+b: Element,+c: Element,+d: Element,+e: Element,+f: Element) ->
482 {Traversal.read_seventh(~Reader,~Element,~Context,~read,position,context,a,b,c,d,e,f,read(pack_reader(reader),context,position)) ==
483 (pack_reader(reader),Traversal.Eight{a,b,c,d,e,f,sample(reader,context,position),sample(reader,context,(position + 1 : U32))}) : Reader & Traversal.Eight<Element>}:
484 %Equal.sym(Reader & Element,read(pack_reader(reader),context,position),(pack_reader(reader),sample(reader,context,position)),read_matches(reader,context,position)) :
485 {Traversal.read_seventh(~Reader,~Element,~Context,~read,position,context,a,b,c,d,e,f,_) ==
486 (pack_reader(reader),Traversal.Eight{a,b,c,d,e,f,sample(reader,context,position),sample(reader,context,(position + 1 : U32))}) : Reader & Traversal.Eight<Element>}
487 read_last_matches(~Reader,~Model,~Element,~Context,~pack_reader,~read,~sample,~read_matches,reader,context,(position + 1 : U32),a,b,c,d,e,f,sample(reader,context,position))
488
489def read_sixth_matches(~Reader: Type,~Model: Data,~Element: Data,~Context: Data,~pack_reader: Model -> Reader,
490 ~read: Reader -> Context -> U32 -> Reader & Element,~sample: Model -> Context -> U32 -> Element,
491 ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
492 {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
493 +reader: Model,+context: Context,+position: U32,+a: Element,+b: Element,+c: Element,+d: Element,+e: Element) ->
494 {Traversal.read_sixth(~Reader,~Element,~Context,~read,position,context,a,b,c,d,e,read(pack_reader(reader),context,position)) ==
495 (pack_reader(reader),Traversal.Eight{a,b,c,d,e,sample(reader,context,position),sample(reader,context,(position + 1 : U32)),
496 sample(reader,context,((position + 1 : U32) + 1 : U32))}) : Reader & Traversal.Eight<Element>}:
497 %Equal.sym(Reader & Element,read(pack_reader(reader),context,position),(pack_reader(reader),sample(reader,context,position)),read_matches(reader,context,position)) :
498 {Traversal.read_sixth(~Reader,~Element,~Context,~read,position,context,a,b,c,d,e,_) ==
499 (pack_reader(reader),Traversal.Eight{a,b,c,d,e,sample(reader,context,position),sample(reader,context,(position + 1 : U32)),
500 sample(reader,context,((position + 1 : U32) + 1 : U32))}) : Reader & Traversal.Eight<Element>}
501 read_seventh_matches(~Reader,~Model,~Element,~Context,~pack_reader,~read,~sample,~read_matches,reader,context,(position + 1 : U32),a,b,c,d,e,sample(reader,context,position))
502
503def read_fifth_matches(~Reader: Type,~Model: Data,~Element: Data,~Context: Data,~pack_reader: Model -> Reader,
504 ~read: Reader -> Context -> U32 -> Reader & Element,~sample: Model -> Context -> U32 -> Element,
505 ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
506 {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
507 +reader: Model,+context: Context,+position: U32,+a: Element,+b: Element,+c: Element,+d: Element) ->
508 {Traversal.read_fifth(~Reader,~Element,~Context,~read,position,context,a,b,c,d,read(pack_reader(reader),context,position)) ==
509 (pack_reader(reader),Traversal.Eight{a,b,c,d,sample(reader,context,position),sample(reader,context,(position + 1 : U32)),
510 sample(reader,context,((position + 1 : U32) + 1 : U32)),sample(reader,context,(((position + 1 : U32) + 1 : U32) + 1 : U32))}) : Reader & Traversal.Eight<Element>}:
511 %Equal.sym(Reader & Element,read(pack_reader(reader),context,position),(pack_reader(reader),sample(reader,context,position)),read_matches(reader,context,position)) :
512 {Traversal.read_fifth(~Reader,~Element,~Context,~read,position,context,a,b,c,d,_) ==
513 (pack_reader(reader),Traversal.Eight{a,b,c,d,sample(reader,context,position),sample(reader,context,(position + 1 : U32)),
514 sample(reader,context,((position + 1 : U32) + 1 : U32)),sample(reader,context,(((position + 1 : U32) + 1 : U32) + 1 : U32))}) : Reader & Traversal.Eight<Element>}
515 read_sixth_matches(~Reader,~Model,~Element,~Context,~pack_reader,~read,~sample,~read_matches,reader,context,(position + 1 : U32),a,b,c,d,sample(reader,context,position))
516
517def read_fourth_matches(~Reader: Type,~Model: Data,~Element: Data,~Context: Data,~pack_reader: Model -> Reader,
518 ~read: Reader -> Context -> U32 -> Reader & Element,~sample: Model -> Context -> U32 -> Element,
519 ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
520 {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
521 +reader: Model,+context: Context,+position: U32,+a: Element,+b: Element,+c: Element) ->
522 {Traversal.read_fourth(~Reader,~Element,~Context,~read,position,context,a,b,c,read(pack_reader(reader),context,position)) ==
523 (pack_reader(reader),Traversal.Eight{a,b,c,sample(reader,context,position),sample(reader,context,(position + 1 : U32)),
524 sample(reader,context,((position + 1 : U32) + 1 : U32)),sample(reader,context,(((position + 1 : U32) + 1 : U32) + 1 : U32)),
525 sample(reader,context,((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32))}) : Reader & Traversal.Eight<Element>}:
526 %Equal.sym(Reader & Element,read(pack_reader(reader),context,position),(pack_reader(reader),sample(reader,context,position)),read_matches(reader,context,position)) :
527 {Traversal.read_fourth(~Reader,~Element,~Context,~read,position,context,a,b,c,_) ==
528 (pack_reader(reader),Traversal.Eight{a,b,c,sample(reader,context,position),sample(reader,context,(position + 1 : U32)),
529 sample(reader,context,((position + 1 : U32) + 1 : U32)),sample(reader,context,(((position + 1 : U32) + 1 : U32) + 1 : U32)),
530 sample(reader,context,((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32))}) : Reader & Traversal.Eight<Element>}
531 read_fifth_matches(~Reader,~Model,~Element,~Context,~pack_reader,~read,~sample,~read_matches,reader,context,(position + 1 : U32),a,b,c,sample(reader,context,position))
532
533def read_third_matches(~Reader: Type,~Model: Data,~Element: Data,~Context: Data,~pack_reader: Model -> Reader,
534 ~read: Reader -> Context -> U32 -> Reader & Element,~sample: Model -> Context -> U32 -> Element,
535 ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
536 {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
537 +reader: Model,+context: Context,+position: U32,+a: Element,+b: Element) ->
538 {Traversal.read_third(~Reader,~Element,~Context,~read,position,context,a,b,read(pack_reader(reader),context,position)) ==
539 (pack_reader(reader),Traversal.Eight{a,b,sample(reader,context,position),sample(reader,context,(position + 1 : U32)),
540 sample(reader,context,((position + 1 : U32) + 1 : U32)),sample(reader,context,(((position + 1 : U32) + 1 : U32) + 1 : U32)),
541 sample(reader,context,((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32)),
542 sample(reader,context,(((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32))}) : Reader & Traversal.Eight<Element>}:
543 %Equal.sym(Reader & Element,read(pack_reader(reader),context,position),(pack_reader(reader),sample(reader,context,position)),read_matches(reader,context,position)) :
544 {Traversal.read_third(~Reader,~Element,~Context,~read,position,context,a,b,_) ==
545 (pack_reader(reader),Traversal.Eight{a,b,sample(reader,context,position),sample(reader,context,(position + 1 : U32)),
546 sample(reader,context,((position + 1 : U32) + 1 : U32)),sample(reader,context,(((position + 1 : U32) + 1 : U32) + 1 : U32)),
547 sample(reader,context,((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32)),
548 sample(reader,context,(((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32))}) : Reader & Traversal.Eight<Element>}
549 read_fourth_matches(~Reader,~Model,~Element,~Context,~pack_reader,~read,~sample,~read_matches,reader,context,(position + 1 : U32),a,b,sample(reader,context,position))
550
551def read_second_matches(~Reader: Type,~Model: Data,~Element: Data,~Context: Data,~pack_reader: Model -> Reader,
552 ~read: Reader -> Context -> U32 -> Reader & Element,~sample: Model -> Context -> U32 -> Element,
553 ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
554 {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
555 +reader: Model,+context: Context,+position: U32,+a: Element) ->
556 {Traversal.read_second(~Reader,~Element,~Context,~read,position,context,a,read(pack_reader(reader),context,position)) ==
557 (pack_reader(reader),Traversal.Eight{a,sample(reader,context,position),sample(reader,context,(position + 1 : U32)),
558 sample(reader,context,((position + 1 : U32) + 1 : U32)),sample(reader,context,(((position + 1 : U32) + 1 : U32) + 1 : U32)),
559 sample(reader,context,((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32)),
560 sample(reader,context,(((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32)),
561 sample(reader,context,((((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32))}) : Reader & Traversal.Eight<Element>}:
562 %Equal.sym(Reader & Element,read(pack_reader(reader),context,position),(pack_reader(reader),sample(reader,context,position)),read_matches(reader,context,position)) :
563 {Traversal.read_second(~Reader,~Element,~Context,~read,position,context,a,_) ==
564 (pack_reader(reader),Traversal.Eight{a,sample(reader,context,position),sample(reader,context,(position + 1 : U32)),
565 sample(reader,context,((position + 1 : U32) + 1 : U32)),sample(reader,context,(((position + 1 : U32) + 1 : U32) + 1 : U32)),
566 sample(reader,context,((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32)),
567 sample(reader,context,(((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32)),
568 sample(reader,context,((((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32))}) : Reader & Traversal.Eight<Element>}
569 read_third_matches(~Reader,~Model,~Element,~Context,~pack_reader,~read,~sample,~read_matches,reader,context,(position + 1 : U32),a,sample(reader,context,position))
570
571# The model of eight fold steps.
572def model_round(~Model: Data,~Element: Data,~Accumulator: Data,~Context: Data,
573 ~sample: Model -> Context -> U32 -> Element,~combine: Accumulator -> Element -> Accumulator,
574 state: Traversal.State<&2,&2,Model,Accumulator,Context>) -> Traversal.State<&2,&2,Model,Accumulator,Context>:
575 Loop.run(~Traversal.State<&2,&2,Model,Accumulator,Context>,~model_fold_step(~Model,~Element,~Accumulator,~Context,~sample,~combine),8n,state)
576
577def round_refines_model(~Reader: Type,~Model: Data,~Element: Data,~Accumulator: Data,~Context: Data,
578 ~pack_reader: Model -> Reader,~read: Reader -> Context -> U32 -> Reader & Element,
579 ~sample: Model -> Context -> U32 -> Element,~combine: Accumulator -> Element -> Accumulator,
580 ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
581 {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
582 +state: Traversal.State<&2,&2,Model,Accumulator,Context>) ->
583 {Traversal.fold_round(~Reader,~Element,~Accumulator,~Context,~read,~combine,
584 represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,state)) ==
585 represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,
586 model_round(~Model,~Element,~Accumulator,~Context,~sample,~combine,state)) : Traversal.State<&1,&2,Reader,Accumulator,Context>}:
587 Traversal.State{+reader,+accumulator,+position,+context} = state
588 %Equal.sym(Reader & Element,read(pack_reader(reader),context,position),(pack_reader(reader),sample(reader,context,position)),read_matches(reader,context,position)) :
589 {Traversal.round_value(~Reader,~Element,~Accumulator,~Context,~combine,accumulator,position,context,
590 Traversal.read_eight(~Reader,~Element,~Context,~read,position,context,_)) ==
591 represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,
592 model_round(~Model,~Element,~Accumulator,~Context,~sample,~combine,Traversal.State{reader,accumulator,position,context})) : Traversal.State<&1,&2,Reader,Accumulator,Context>}
593 %Equal.sym(Reader & Traversal.Eight<Element>,
594 Traversal.read_second(~Reader,~Element,~Context,~read,(position + 1 : U32),context,sample(reader,context,position),read(pack_reader(reader),context,(position + 1 : U32))),
595 (pack_reader(reader),Traversal.Eight{sample(reader,context,position),sample(reader,context,(position + 1 : U32)),
596 sample(reader,context,((position + 1 : U32) + 1 : U32)),sample(reader,context,(((position + 1 : U32) + 1 : U32) + 1 : U32)),
597 sample(reader,context,((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32)),
598 sample(reader,context,(((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32)),
599 sample(reader,context,((((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32)),
600 sample(reader,context,(((((((position + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32) + 1 : U32))}),
601 read_second_matches(~Reader,~Model,~Element,~Context,~pack_reader,~read,~sample,~read_matches,reader,context,(position + 1 : U32),sample(reader,context,position))) :
602 {Traversal.round_value(~Reader,~Element,~Accumulator,~Context,~combine,accumulator,position,context,_) ==
603 represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,
604 model_round(~Model,~Element,~Accumulator,~Context,~sample,~combine,Traversal.State{reader,accumulator,position,context})) : Traversal.State<&1,&2,Reader,Accumulator,Context>}
605 {==}
606
607def round_steps(~Model: Data,~Element: Data,~Accumulator: Data,~Context: Data,
608 ~sample: Model -> Context -> U32 -> Element,~combine: Accumulator -> Element -> Accumulator,-state: Traversal.State<&2,&2,Model,Accumulator,Context>) ->
609 {model_round(~Model,~Element,~Accumulator,~Context,~sample,~combine,state) ==
610 Loop.run(~Traversal.State<&2,&2,Model,Accumulator,Context>,~model_fold_step(~Model,~Element,~Accumulator,~Context,~sample,~combine),8n,state) : Traversal.State<&2,&2,Model,Accumulator,Context>}:
611 {==}
612
613# fold_rounds runs the ordered model fold: count % 8 steps, then rounds of eight.
614def rounds_refine_ordered_model(~Reader: Type,~Model: Data,~Element: Data,~Accumulator: Data,~Context: Data,
615 ~pack_reader: Model -> Reader,~read: Reader -> Context -> U32 -> Reader & Element,
616 ~sample: Model -> Context -> U32 -> Element,~combine: Accumulator -> Element -> Accumulator,
617 ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
618 {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Element},
619 +count: Nat,+state: Traversal.State<&2,&2,Model,Accumulator,Context>) ->
620 {Loop.run(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.fold_round(~Reader,~Element,~Accumulator,~Context,~read,~combine),Nat.div(count,8n),
621 Loop.run(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine),Nat.mod(count,8n),
622 represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,state))) ==
623 represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,
624 Loop.run(~Traversal.State<&2,&2,Model,Accumulator,Context>,~model_fold_step(~Model,~Element,~Accumulator,~Context,~sample,~combine),count,state)) :
625 Traversal.State<&1,&2,Reader,Accumulator,Context>}:
626 +head = Loop.run(~Traversal.State<&2,&2,Model,Accumulator,Context>,~model_fold_step(~Model,~Element,~Accumulator,~Context,~sample,~combine),Nat.mod(count,8n),state)
627 %Projection.head_then_eights(~Traversal.State<&2,&2,Model,Accumulator,Context>,~model_fold_step(~Model,~Element,~Accumulator,~Context,~sample,~combine),
628 ~model_round(~Model,~Element,~Accumulator,~Context,~sample,~combine),~round_steps(~Model,~Element,~Accumulator,~Context,~sample,~combine),count,state) :
629 {Loop.run(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.fold_round(~Reader,~Element,~Accumulator,~Context,~read,~combine),Nat.div(count,8n),
630 Loop.run(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine),Nat.mod(count,8n),
631 represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,state))) ==
632 represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,_) : Traversal.State<&1,&2,Reader,Accumulator,Context>}
633 %Equal.sym(Traversal.State<&1,&2,Reader,Accumulator,Context>,
634 Loop.run(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine),Nat.mod(count,8n),
635 represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,state)),
636 represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,head),
637 fold_refines_ordered_model(~Reader,~Model,~Element,~Accumulator,~Context,~pack_reader,~read,~sample,~combine,~read_matches,Nat.mod(count,8n),state)) :
638 {Loop.run(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.fold_round(~Reader,~Element,~Accumulator,~Context,~read,~combine),Nat.div(count,8n),_) ==
639 represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader,
640 Loop.run(~Traversal.State<&2,&2,Model,Accumulator,Context>,~model_round(~Model,~Element,~Accumulator,~Context,~sample,~combine),Nat.div(count,8n),head)) :
641 Traversal.State<&1,&2,Reader,Accumulator,Context>}
642 Projection.iteration_refines_model(~Traversal.State<&1,&2,Reader,Accumulator,Context>,~Traversal.State<&2,&2,Model,Accumulator,Context>,
643 ~Traversal.fold_round(~Reader,~Element,~Accumulator,~Context,~read,~combine),~model_round(~Model,~Element,~Accumulator,~Context,~sample,~combine),
644 ~represent_fold(~Reader,~Model,~Accumulator,~Context,~pack_reader),
645 ~round_refines_model(~Reader,~Model,~Element,~Accumulator,~Context,~pack_reader,~read,~sample,~combine,~read_matches),Nat.div(count,8n),head)
646
647# In-place transforms retain one owner and use the same generic loop lifting.
648def represent_map(~Element: Data,~Context: Data,
649 state: Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>) -> Traversal.State<&2,&1,Unit,Array<Element>,Context>:
650 Traversal.State{Unit{},output,position,context} = state
651 Traversal.State{Unit{},Tree.pack(Element,output),position,context}
652
653def unindexed(~Element: Data,~Context: Data,~map: Context -> Element -> Element,context: Context,position: U32,value: Element) -> Element:
654 map(context,value)
655
656def model_map_step(~Element: Data,~Context: Data,~map: Context -> U32 -> Element -> Element,
657 state: Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>) -> Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>:
658 Traversal.State{Unit{},+output,+position,+context} = state
659 Traversal.State{Unit{},Tree.write(Element,output,position,map(context,position,Tree.read(Element,output,position))),
660 (position + 1 : U32),context}
661
662def map_step_refines_model(~Element: Data,~Context: Data,~map: Context -> Element -> Element,
663 +state: Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>) ->
664 {Traversal.map_step(~Element,~Context,~map,represent_map(~Element,~Context,state)) ==
665 represent_map(~Element,~Context,model_map_step(~Element,~Context,~unindexed(~Element,~Context,~map),state)) : Traversal.State<&2,&1,Unit,Array<Element>,Context>}:
666 Traversal.State{Unit{},+output,+position,+context} = state
667 %Equal.sym(Array<Element> & Element,Array.get(Element,Tree.pack(Element,output),position),
668 (Tree.pack(Element,output),Tree.read(Element,output,position)),StorageLaws.read(Element,output,position)) :
669 {Traversal.mapped_value(~Element,~Context,~map,position,context,_) ==
670 represent_map(~Element,~Context,model_map_step(~Element,~Context,~unindexed(~Element,~Context,~map),state)) : Traversal.State<&2,&1,Unit,Array<Element>,Context>}
671 %Equal.sym(Array<Element>,Array.set(Element,Tree.pack(Element,output),position,map(context,Tree.read(Element,output,position))),
672 Tree.pack(Element,Tree.write(Element,output,position,map(context,Tree.read(Element,output,position)))),
673 StorageLaws.write(Element,output,position,map(context,Tree.read(Element,output,position)))) :
674 {Traversal.State{Unit{},_,(position + 1 : U32),context} ==
675 represent_map(~Element,~Context,model_map_step(~Element,~Context,~unindexed(~Element,~Context,~map),state)) : Traversal.State<&2,&1,Unit,Array<Element>,Context>}
676 {==}
677
678def map_loop_refines_model(~Element: Data,~Context: Data,~map: Context -> Element -> Element,
679 +count: Nat,+state: Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>) ->
680 {Loop.run(~Traversal.State<&2,&1,Unit,Array<Element>,Context>,~Traversal.map_step(~Element,~Context,~map),
681 count,represent_map(~Element,~Context,state)) ==
682 represent_map(~Element,~Context,Loop.run(~Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>,
683 ~model_map_step(~Element,~Context,~unindexed(~Element,~Context,~map)),count,state)) : Traversal.State<&2,&1,Unit,Array<Element>,Context>}:
684 Projection.iteration_refines_model(~Traversal.State<&2,&1,Unit,Array<Element>,Context>,~Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>,
685 ~Traversal.map_step(~Element,~Context,~map),~model_map_step(~Element,~Context,~unindexed(~Element,~Context,~map)),~represent_map(~Element,~Context),
686 ~map_step_refines_model(~Element,~Context,~map),count,state)
687
688# One representation proof covers the entire indexed output traversal. The
689# strategy supplies a single-step result, not another outer-loop induction.
690
691# In-place binary updates use the current destination value in left position.
692# This theorem models sequential writes, including modular/overlapping raw
693# addresses. Valid view guards and non-overlap are separate obligations.
694def model_update_step(~Model: Data,~Element: Data,~Sample: Data,~Context: Data,
695 ~sample: Model -> Context -> U32 -> Sample,~combine: Element -> Sample -> Element,~destination: Context -> U32 -> U32,
696 state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) -> Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>:
697 Traversal.State{+reader,+output,+position,+context} = state
698 Traversal.State{reader,Tree.write(Element,output,destination(context,position),
699 combine(Tree.read(Element,output,destination(context,position)),sample(reader,context,position))),(position + 1 : U32),context}
700
701def update_step_refines_model(~Reader: Type,~Model: Data,~Element: Data,~Sample: Data,~Context: Data,
702 ~pack_reader: Model -> Reader,~read: Reader -> Context -> U32 -> Reader & Sample,
703 ~sample: Model -> Context -> U32 -> Sample,~combine: Element -> Sample -> Element,~destination: Context -> U32 -> U32,
704 ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
705 {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Sample},
706 +state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) ->
707 {Traversal.update_step(~Reader,~Element,~Sample,~Context,~read,~combine,~destination,
708 represent(~Reader,~Model,~Element,~Context,~pack_reader,state)) ==
709 represent(~Reader,~Model,~Element,~Context,~pack_reader,model_update_step(~Model,~Element,~Sample,~Context,~sample,~combine,~destination,state)) :
710 Traversal.State<&1,&1,Reader,Array<Element>,Context>}:
711 Traversal.State{+reader,+output,+position,+context} = state
712 %Equal.sym(Array<Element> & Element,Array.get(Element,Tree.pack(Element,output),destination(context,position)),
713 (Tree.pack(Element,output),Tree.read(Element,output,destination(context,position))),StorageLaws.read(Element,output,destination(context,position))) :
714 {Traversal.update_current(~Reader,~Element,~Sample,~Context,~read,~combine,~destination,pack_reader(reader),position,context,_) ==
715 represent(~Reader,~Model,~Element,~Context,~pack_reader,model_update_step(~Model,~Element,~Sample,~Context,~sample,~combine,~destination,
716 Traversal.State{reader,output,position,context})) : Traversal.State<&1,&1,Reader,Array<Element>,Context>}
717 %Equal.sym(Reader & Sample,read(pack_reader(reader),context,position),(pack_reader(reader),sample(reader,context,position)),read_matches(reader,context,position)) :
718 {Traversal.update_sample(~Reader,~Element,~Sample,~Context,~combine,~destination,position,context,Tree.pack(Element,output),
719 Tree.read(Element,output,destination(context,position)),_) ==
720 represent(~Reader,~Model,~Element,~Context,~pack_reader,model_update_step(~Model,~Element,~Sample,~Context,~sample,~combine,~destination,
721 Traversal.State{reader,output,position,context})) : Traversal.State<&1,&1,Reader,Array<Element>,Context>}
722 %Equal.sym(Array<Element>,Array.set(Element,Tree.pack(Element,output),destination(context,position),
723 combine(Tree.read(Element,output,destination(context,position)),sample(reader,context,position))),
724 Tree.pack(Element,Tree.write(Element,output,destination(context,position),
725 combine(Tree.read(Element,output,destination(context,position)),sample(reader,context,position)))),
726 StorageLaws.write(Element,output,destination(context,position),combine(Tree.read(Element,output,destination(context,position)),sample(reader,context,position)))) :
727 {Traversal.State{pack_reader(reader),_,(position + 1 : U32),context} ==
728 represent(~Reader,~Model,~Element,~Context,~pack_reader,model_update_step(~Model,~Element,~Sample,~Context,~sample,~combine,~destination,
729 Traversal.State{reader,output,position,context})) : Traversal.State<&1,&1,Reader,Array<Element>,Context>}
730 {==}
731
732def update_refines_model(~Reader: Type,~Model: Data,~Element: Data,~Sample: Data,~Context: Data,
733 ~pack_reader: Model -> Reader,~read: Reader -> Context -> U32 -> Reader & Sample,
734 ~sample: Model -> Context -> U32 -> Sample,~combine: Element -> Sample -> Element,~destination: Context -> U32 -> U32,
735 ~read_matches: @+reader: Model -> @+context: Context -> @+position: U32 ->
736 {read(pack_reader(reader),context,position) == (pack_reader(reader),sample(reader,context,position)) : Reader & Sample},
737 +count: Nat,+state: Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>) ->
738 {Traversal.update(~Reader,~Element,~Sample,~Context,~read,~combine,~destination,count,
739 represent(~Reader,~Model,~Element,~Context,~pack_reader,state)) ==
740 represent(~Reader,~Model,~Element,~Context,~pack_reader,
741 Loop.run(~Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>,
742 ~model_update_step(~Model,~Element,~Sample,~Context,~sample,~combine,~destination),count,state)) :
743 Traversal.State<&1,&1,Reader,Array<Element>,Context>}:
744 Projection.iteration_refines_model(~Traversal.State<&1,&1,Reader,Array<Element>,Context>,~Traversal.State<&2,&2,Model,Tree.Tree<Element>,Context>,
745 ~Traversal.update_step(~Reader,~Element,~Sample,~Context,~read,~combine,~destination),
746 ~model_update_step(~Model,~Element,~Sample,~Context,~sample,~combine,~destination),
747 ~represent(~Reader,~Model,~Element,~Context,~pack_reader),
748 ~update_step_refines_model(~Reader,~Model,~Element,~Sample,~Context,~pack_reader,~read,~sample,~combine,~destination,~read_matches),count,state)
749
750# A state with a moving counter is the same indexed fold as its stores.
751def indexed_loop(~Runtime: Type,~Model: Data,~Context: Data,
752 ~step: Runtime -> Runtime,~update: U32 -> Context -> Model -> Model,
753 ~represent: Context -> U32 -> Model -> Runtime,
754 ~step_matches: @+context: Context -> @+index: U32 -> @+state: Model ->
755 {step(represent(context,index,state)) == represent(context,(index + 1 : U32),update(index,context,state)) : Runtime},
756 count: Nat,+index: U32,+context: Context,+state: Model) ->
757 {Loop.run(~Runtime,~step,count,represent(context,index,state)) ==
758 represent(context,(index + U32.from_nat(count) : U32),Traversal.indexed_fold(~Model,~Context,~update,count,index,context,state)) : Runtime}:
759 match count:
760 case 0n:
761 %Equal.sym(U32,(index + 0 : U32),index,Arithmetic.add_zero(index)) :
762 {represent(context,index,state) == represent(context,_,state) : Runtime}
763 {==}
764 case 1n+ +rest:
765 %Equal.sym(Runtime,step(represent(context,index,state)),represent(context,(index + 1 : U32),update(index,context,state)),step_matches(context,index,state)) :
766 {Loop.run(~Runtime,~step,rest,_) == represent(context,(index + U32.from_nat(1n+rest) : U32),
767 Traversal.indexed_fold(~Model,~Context,~update,rest,(index + 1 : U32),context,update(index,context,state))) : Runtime}
768 %Equal.sym(U32,(index + U32.from_nat(1n+rest) : U32),((index + 1 : U32) + U32.from_nat(rest) : U32),Projection.indexed_successor(index,rest)) :
769 {Loop.run(~Runtime,~step,rest,represent(context,(index + 1 : U32),update(index,context,state))) ==
770 represent(context,_,Traversal.indexed_fold(~Model,~Context,~update,rest,(index + 1 : U32),context,update(index,context,state))) : Runtime}
771 indexed_loop(~Runtime,~Model,~Context,~step,~update,~represent,~step_matches,rest,(index + 1 : U32),context,update(index,context,state))
772
773def indexed_fold_refines_model(~Runtime: Type,~Model: Data,~Context: Data,
774 ~update: U32 -> Context -> Runtime -> Runtime,~model_update: U32 -> Context -> Model -> Model,
775 ~represent: Model -> Runtime,
776 ~step_matches: @+index: U32 -> @+context: Context -> @+state: Model ->
777 {update(index,context,represent(state)) == represent(model_update(index,context,state)) : Runtime},
778 +count: Nat,+index: U32,+context: Context,+state: Model) ->
779 {Traversal.indexed_fold(~Runtime,~Context,~update,count,index,context,represent(state)) ==
780 represent(Traversal.indexed_fold(~Model,~Context,~model_update,count,index,context,state)) : Runtime}:
781 match count:
782 case 0n: {==}
783 case 1n+ +rest:
784 %Equal.sym(Runtime,update(index,context,represent(state)),represent(model_update(index,context,state)),step_matches(index,context,state)) :
785 {Traversal.indexed_fold(~Runtime,~Context,~update,rest,(index + 1 : U32),context,_) ==
786 represent(Traversal.indexed_fold(~Model,~Context,~model_update,rest,(index + 1 : U32),context,model_update(index,context,state))) : Runtime}
787 indexed_fold_refines_model(~Runtime,~Model,~Context,~update,~model_update,~represent,~step_matches,
788 rest,(index + 1 : U32),context,model_update(index,context,state))
789
790# An indexed traversal transports a fixed observation through its own update.
791def indexed_fold_observes(~State: Data,~Observation: Data,~Context: Data,
792 ~update: U32 -> Context -> State -> State,~observe: State -> Observation,
793 ~observed_update: U32 -> Context -> Observation -> Observation,
794 ~step_observed: @+index: U32 -> @+context: Context -> @+state: State ->
795 {observe(update(index,context,state)) == observed_update(index,context,observe(state)) : Observation},
796 count: Nat,+first: U32,+context: Context,+state: State) ->
797 {observe(Traversal.indexed_fold(~State,~Context,~update,count,first,context,state)) ==
798 Traversal.indexed_fold(~Observation,~Context,~observed_update,count,first,context,observe(state)) : Observation}:
799 match count:
800 case 0n: {==}
801 case 1n+rest:
802 %step_observed(first,context,state) :
803 {observe(Traversal.indexed_fold(~State,~Context,~update,rest,(first + 1 : U32),context,update(first,context,state))) ==
804 Traversal.indexed_fold(~Observation,~Context,~observed_update,rest,(first + 1 : U32),context,_) : Observation}
805 indexed_fold_observes(~State,~Observation,~Context,~update,~observe,~observed_update,~step_observed,
806 rest,(first + 1 : U32),context,update(first,context,state))
807
808def indexed_fold_fixed(~State: Data,~Context: Data,~update: U32 -> Context -> State -> State,
809 ~fixed: @+index: U32 -> @+context: Context -> @+state: State -> {update(index,context,state) == state : State},
810 count: Nat,+first: U32,+context: Context,+state: State) ->
811 {Traversal.indexed_fold(~State,~Context,~update,count,first,context,state) == state : State}:
812 match count:
813 case 0n: {==}
814 case 1n+rest:
815 %Equal.sym(State,update(first,context,state),state,fixed(first,context,state)) :
816 {Traversal.indexed_fold(~State,~Context,~update,rest,(first + 1 : U32),context,_) == state : State}
817 indexed_fold_fixed(~State,~Context,~update,~fixed,rest,(first + 1 : U32),context,state)
818
819# One bounded induction carries capacity, preserved sources and completed
820# output values together. A strategy proves its local update obligation;
821# it does not reimplement the whole output traversal proof.
822def indexed_fold_change_context(~State: Data,~Outer: Data,~Inner: Data,
823 ~project: Outer -> Inner,~outer_step: U32 -> Outer -> State -> State,~inner_step: U32 -> Inner -> State -> State,
824 ~same_step: @+index: U32 -> @+context: Outer -> @+state: State ->
825 {outer_step(index,context,state) == inner_step(index,project(context),state) : State},
826 +count: Nat,+first: U32,+context: Outer,+state: State) ->
827 {Traversal.indexed_fold(~State,~Outer,~outer_step,count,first,context,state) ==
828 Traversal.indexed_fold(~State,~Inner,~inner_step,count,first,project(context),state) : State}:
829 match count:
830 case 0n: {==}
831 case 1n+ +rest:
832 %Equal.sym(State,outer_step(first,context,state),inner_step(first,project(context),state),same_step(first,context,state)) :
833 {Traversal.indexed_fold(~State,~Outer,~outer_step,rest,(first + 1 : U32),context,_) ==
834 Traversal.indexed_fold(~State,~Inner,~inner_step,rest,(first + 1 : U32),project(context),inner_step(first,project(context),state)) : State}
835 indexed_fold_change_context(~State,~Outer,~Inner,~project,~outer_step,~inner_step,~same_step,
836 rest,(first + 1 : U32),context,inner_step(first,project(context),state))
837
838def indexed_fold_preserves_invariant(~State: Data,~Context: Data,
839 ~limit: Context -> Nat,~Invariant: Context -> Nat -> State -> Data,
840 ~update: U32 -> Context -> State -> State,
841 ~preserve: @+context: Context -> @+index: Nat -> @+state: State ->
842 {Nat.is_lt(index,limit(context)) == True{} : Bool} -> Invariant(context,index,state) ->
843 Invariant(context,1n+index,update(U32.from_nat(index),context,state)),
844 +count: Nat,+first: Nat,+context: Context,+state: State,
845 +room: {Nat.is_le(Nat.add(first,count),limit(context)) == True{} : Bool},
846 evidence: Invariant(context,first,state)) ->
847 Invariant(context,Nat.add(first,count),Traversal.indexed_fold(~State,~Context,~update,count,U32.from_nat(first),context,state)):
848 match count:
849 case 0n:
850 %Equal.sym(Nat,Nat.add(first,0n),first,Addition.zero_right(first)) : Invariant(context,_,state)
851 evidence
852 case 1n+ +rest:
853 %Equal.sym(U32,(U32.from_nat(first) + 1 : U32),U32.from_nat(1n+first),Bounds.add_one(U32.from_nat(first))) :
854 Invariant(context,Nat.add(first,1n+rest),Traversal.indexed_fold(~State,~Context,~update,rest,_,context,update(U32.from_nat(first),context,state)))
855 %Equal.sym(Nat,Nat.add(first,1n+rest),1n+Nat.add(first,rest),Addition.successor_right(first,rest)) :
856 Invariant(context,_,Traversal.indexed_fold(~State,~Context,~update,rest,U32.from_nat(1n+first),context,update(U32.from_nat(first),context,state)))
857 indexed_fold_preserves_invariant(~State,~Context,~limit,~Invariant,~update,~preserve,rest,1n+first,context,update(U32.from_nat(first),context,state),
858 Order.advance_room(first,rest,limit(context),room),preserve(context,first,state,Order.room_index(first,rest,limit(context),room),evidence))
859
860# Splitting a traversal preserves every state update in the same order. The
861# boundary uses modular U32 conversion; no scalar/FP32-specific induction.
862def indexed_fold_split(~Value: Type,~Context: Data,~update: U32 -> Context -> Value -> Value,
863 +first: Nat,+second: Nat,+start: Nat,+context: Context,-initial: Value) ->
864 {Traversal.indexed_fold(~Value,~Context,~update,Nat.add(first,second),U32.from_nat(start),context,initial) ==
865 Traversal.indexed_fold(~Value,~Context,~update,second,U32.from_nat(Nat.add(start,first)),context,
866 Traversal.indexed_fold(~Value,~Context,~update,first,U32.from_nat(start),context,initial)) : Value}:
867 match first:
868 case 0n:
869 %Equal.sym(Nat,Nat.add(start,0n),start,Addition.zero_right(start)) :
870 {Traversal.indexed_fold(~Value,~Context,~update,second,U32.from_nat(start),context,initial) ==
871 Traversal.indexed_fold(~Value,~Context,~update,second,U32.from_nat(_),context,initial) : Value}
872 {==}
873 case 1n+ +rest:
874 %Equal.sym(U32,(U32.from_nat(start) + 1 : U32),U32.from_nat(1n+start),Bounds.add_one(U32.from_nat(start))) :
875 {Traversal.indexed_fold(~Value,~Context,~update,Nat.add(rest,second),_,context,update(U32.from_nat(start),context,initial)) ==
876 Traversal.indexed_fold(~Value,~Context,~update,second,U32.from_nat(Nat.add(start,1n+rest)),context,
877 Traversal.indexed_fold(~Value,~Context,~update,rest,_,context,update(U32.from_nat(start),context,initial))) : Value}
878 %Equal.sym(Nat,Nat.add(start,1n+rest),1n+Nat.add(start,rest),Addition.successor_right(start,rest)) :
879 {Traversal.indexed_fold(~Value,~Context,~update,Nat.add(rest,second),U32.from_nat(1n+start),context,update(U32.from_nat(start),context,initial)) ==
880 Traversal.indexed_fold(~Value,~Context,~update,second,U32.from_nat(_),context,
881 Traversal.indexed_fold(~Value,~Context,~update,rest,U32.from_nat(1n+start),context,update(U32.from_nat(start),context,initial))) : Value}
882 indexed_fold_split(~Value,~Context,~update,rest,second,1n+start,context,update(U32.from_nat(start),context,initial))
883
884# Reading the values projection does not need the reader's representation.
885def collect_prepend_values(~Reader: Type,~Element: Data,+value: Element,result: Reader & List<&2,Element>) ->
886 {Pair.snd(Reader,List<&2,Element>,Traversal.collect_prepend(~&2,~Reader,~Element,value,result)) == value <> Pair.snd(Reader,List<&2,Element>,result) : List<&2,Element>}:
887 (reader,values) = result
888 {==}
889
890# One leaf supplies source, value and observation facts. The shared collection
891# lifts all three together, including leaf premises for each input key.
892def collected_leaf_frame(~Source: Data,~Element: Data,~Key: Data,~Context: Data,~Model: Data,
893 ~Frame: Context -> Source -> Data,~ValueFrame: Context -> Element -> Data,
894 ~observe: Context -> Element -> Model,~sample: Context -> Key -> Model,context: Context,key: Key,result: Source & Element) -> Data:
895 (+source,+value) = result
896 Shape.Both<Frame(context,source),Shape.Both<ValueFrame(context,value),{observe(context,value) == sample(context,key) : Model}>>
897
898def collected_list_frame(~Source: Data,~Element: Data,~Key: Data,~Context: Data,~Model: Data,
899 ~Frame: Context -> Source -> Data,~ValueFrame: Context -> Element -> Data,
900 ~observe: Context -> Element -> Model,~sample: Context -> Key -> Model,+context: Context,+keys: List<&2,Key>,result: Source & List<&2,Element>) -> Data:
901 (+source,+values) = result
902 Shape.Both<Frame(context,source),Shape.Both<Members.All(Element,{value => ValueFrame(context,value) : Element -> Data},values),
903 {collect_values_context(~&2,~Model,~Element,~Context,~observe,values,context) ==
904 collect_values_context(~&2,~Model,~Key,~Context,~sample,keys,context) : List<&2,Model>}>>
905
906def collect_list_certified_join(~Source: Data,~Element: Data,~Key: Data,~Context: Data,~Model: Data,
907 ~Frame: Context -> Source -> Data,~ValueFrame: Context -> Element -> Data,
908 ~observe: Context -> Element -> Model,~sample: Context -> Key -> Model,+context: Context,+key: Key,+rest: List<&2,Key>,+value: Element,
909 tail: Source & List<&2,Element>,value_frame: ValueFrame(context,value),+value_equal: {observe(context,value) == sample(context,key) : Model},
910 tail_frame: collected_list_frame(~Source,~Element,~Key,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,rest,tail)) ->
911 collected_list_frame(~Source,~Element,~Key,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,key <> rest,Traversal.collect_prepend(~&2,~Source,~Element,value,tail)):
912 (source,+values) = tail
913 Shape.Both{source_frame,Shape.Both{values_frame,+values_equal}} = tail_frame
914 Shape.Both{source_frame,Shape.Both{Shape.Both{value_frame,values_frame},
915 %value_equal : {observe(context,value) <> collect_values_context(~&2,~Model,~Element,~Context,~observe,values,context) == _ <> collect_values_context(~&2,~Model,~Key,~Context,~sample,rest,context) : List<&2,Model>}
916 Equal.cong(List<&2,Model>,List<&2,Model>,values => observe(context,value) <> values,
917 collect_values_context(~&2,~Model,~Element,~Context,~observe,values,context),
918 collect_values_context(~&2,~Model,~Key,~Context,~sample,rest,context),values_equal)}}
919
920def collect_list_certified_next(~Source: Data,~Element: Data,~Key: Data,~Context: Data,~Model: Data,
921 ~Frame: Context -> Source -> Data,~ValueFrame: Context -> Element -> Data,
922 ~observe: Context -> Element -> Model,~sample: Context -> Key -> Model,+context: Context,+key: Key,+rest: List<&2,Key>,
923 head: Source & Element,tail: Source -> Source & List<&2,Element>,
924 head_frame: collected_leaf_frame(~Source,~Element,~Key,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,key,head),
925 tail_frame: @+source: Source -> Frame(context,source) -> collected_list_frame(~Source,~Element,~Key,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,rest,tail(source))) ->
926 collected_list_frame(~Source,~Element,~Key,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,key <> rest,
927 Traversal.collect_list_next(~&2,~Source,~Element,head,tail)):
928 (+source,+value) = head
929 Shape.Both{source_frame,Shape.Both{value_frame,+value_equal}} = head_frame
930 collect_list_certified_join(~Source,~Element,~Key,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,key,rest,value,tail(source),value_frame,value_equal,tail_frame(source,source_frame))
931
932def collect_list_certified(~Source: Data,~Element: Data,~Key: Data,~Context: Data,~Model: Data,~ReadContext: Data,~project: Context -> ReadContext,
933 ~Frame: Context -> Source -> Data,~ValueFrame: Context -> Element -> Data,~KeyFrame: Context -> Key -> Data,
934 ~observe: Context -> Element -> Model,~sample: Context -> Key -> Model,
935 ~read: Source -> ReadContext -> Key -> Source & Element,
936 ~leaf: @+source: Source -> @+context: Context -> @+key: Key -> Frame(context,source) -> KeyFrame(context,key) ->
937 collected_leaf_frame(~Source,~Element,~Key,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,key,read(source,project(context),key)),
938 +keys: List<&2,Key>,+source: Source,+context: Context,source_frame: Frame(context,source),
939 keys_frame: Members.All(Key,{key => KeyFrame(context,key) : Key -> Data},keys)) ->
940 collected_list_frame(~Source,~Element,~Key,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,keys,
941 Traversal.collect_list(~&2,~Source,~Element,~Key,~ReadContext,~read,keys,source,project(context))):
942 match keys:
943 case Nil{}: Shape.Both{source_frame,Shape.Both{Unit{},{==}}}
944 case +key <> +rest:
945 Shape.Both{head_frame,+tail_frame} = keys_frame
946 collect_list_certified_next(~Source,~Element,~Key,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,key,rest,read(source,project(context),key),
947 source => Traversal.collect_list(~&2,~Source,~Element,~Key,~ReadContext,~read,rest,source,project(context)),leaf(source,context,key,source_frame,head_frame),
948 source => source_frame => collect_list_certified(~Source,~Element,~Key,~Context,~Model,~ReadContext,~project,~Frame,~ValueFrame,~KeyFrame,~observe,~sample,~read,~leaf,rest,source,context,source_frame,tail_frame))
949
950def collect_values_context_length(~ownership: Quant,~Runtime: Kind(ownership),~Model: Data,~Context: Data,~pack: Context -> Model -> Runtime,
951 values: List<&2,Model>,+context: Context) ->
952 {List.length(ownership,Runtime,collect_values_context(~ownership,~Runtime,~Model,~Context,~pack,values,context)) == List.length(&2,Model,values) : Nat}:
953 match values:
954 case Nil{}: {==}
955 case head <> +rest:
956 Equal.cong(Nat,Nat,value => 1n+value,List.length(ownership,Runtime,collect_values_context(~ownership,~Runtime,~Model,~Context,~pack,rest,context)),
957 List.length(&2,Model,rest),collect_values_context_length(~ownership,~Runtime,~Model,~Context,~pack,rest,context))
958
959# A projected context exposes the logical index while the reader carries its
960# own counters. The leaf proves the transition used by the common collector.
961def collected_indexed_leaf_frame(~Source: Data,~Element: Data,~Context: Data,~Model: Data,~ReadContext: Data,~project: Context -> Nat -> ReadContext,
962 ~Frame: Context -> Source -> Data,~ValueFrame: Context -> Element -> Data,
963 ~observe: Context -> Element -> Model,~sample: Context -> Nat -> Model,+context: Context,+index: Nat,
964 result: Source & Traversal.Collected<&2,ReadContext,Element>) -> Data:
965 (+source,Traversal.Collected{next,+value}) = result
966 Shape.Both<{next == project(context,1n+index) : ReadContext},
967 collected_leaf_frame(~Source,~Element,~Nat,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,index,(source,value))>
968
969def collect_certified_next(~Source: Data,~Element: Data,~Context: Data,~Model: Data,~ReadContext: Data,~project: Context -> Nat -> ReadContext,
970 ~Frame: Context -> Source -> Data,~ValueFrame: Context -> Element -> Data,
971 ~observe: Context -> Element -> Model,~sample: Context -> Nat -> Model,+context: Context,+count: Nat,+index: Nat,
972 head: Source & Traversal.Collected<&2,ReadContext,Element>,tail: Source -> ReadContext -> Source & List<&2,Element>,
973 head_frame: collected_indexed_leaf_frame(~Source,~Element,~Context,~Model,~ReadContext,~project,~Frame,~ValueFrame,~observe,~sample,context,index,head),
974 tail_frame: @+source: Source -> Frame(context,source) ->
975 collected_list_frame(~Source,~Element,~Nat,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,Ranges.range(count,1n+index),tail(source,project(context,1n+index)))) ->
976 collected_list_frame(~Source,~Element,~Nat,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,Ranges.range(1n+count,index),
977 Traversal.collect_next(~&2,~Source,~Element,~ReadContext,head,tail)):
978 (+source,Traversal.Collected{+next,+value}) = head
979 Shape.Both{+next_equal,Shape.Both{source_frame,Shape.Both{value_frame,+value_equal}}} = head_frame
980 %Equal.sym(ReadContext,next,project(context,1n+index),next_equal) :
981 collected_list_frame(~Source,~Element,~Nat,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,Ranges.range(1n+count,index),
982 Traversal.collect_prepend(~&2,~Source,~Element,value,tail(source,_)))
983 collect_list_certified_join(~Source,~Element,~Nat,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,index,Ranges.range(count,1n+index),value,
984 tail(source,project(context,1n+index)),value_frame,value_equal,tail_frame(source,source_frame))
985
986def collect_certified(~Source: Data,~Element: Data,~Context: Data,~Model: Data,~ReadContext: Data,~project: Context -> Nat -> ReadContext,
987 ~Frame: Context -> Source -> Data,~ValueFrame: Context -> Element -> Data,~KeyFrame: Context -> Nat -> Data,
988 ~observe: Context -> Element -> Model,~sample: Context -> Nat -> Model,
989 ~read: Source -> ReadContext -> Source & Traversal.Collected<&2,ReadContext,Element>,
990 ~leaf: @+source: Source -> @+context: Context -> @+index: Nat -> Frame(context,source) -> KeyFrame(context,index) ->
991 collected_indexed_leaf_frame(~Source,~Element,~Context,~Model,~ReadContext,~project,~Frame,~ValueFrame,~observe,~sample,context,index,read(source,project(context,index))),
992 +count: Nat,+index: Nat,+source: Source,+context: Context,source_frame: Frame(context,source),
993 keys_frame: Members.All(Nat,{key => KeyFrame(context,key) : Nat -> Data},Ranges.range(count,index))) ->
994 collected_list_frame(~Source,~Element,~Nat,~Context,~Model,~Frame,~ValueFrame,~observe,~sample,context,Ranges.range(count,index),
995 Traversal.collect(~&2,~Source,~Element,~ReadContext,~read,count,source,project(context,index))):
996 match count:
997 case 0n: Shape.Both{source_frame,Shape.Both{Unit{},{==}}}
998 case 1n+ +rest:
999 Shape.Both{head_frame,+tail_frame} = keys_frame
1000 collect_certified_next(~Source,~Element,~Context,~Model,~ReadContext,~project,~Frame,~ValueFrame,~observe,~sample,context,rest,index,read(source,project(context,index)),
1001 source => context => Traversal.collect(~&2,~Source,~Element,~ReadContext,~read,rest,source,context),leaf(source,context,index,source_frame,head_frame),
1002 source => source_frame => collect_certified(~Source,~Element,~Context,~Model,~ReadContext,~project,~Frame,~ValueFrame,~KeyFrame,~observe,~sample,~read,~leaf,rest,1n+index,source,context,source_frame,tail_frame))
1003
1004def collect_values_context_range(~Element: Data,~Context: Data,~sample: Context -> Nat -> Element,
1005 count: Nat,+first: Nat,+context: Context) ->
1006 {collect_values_context(~&2,~Element,~Nat,~Context,~sample,Ranges.range(count,first),context) ==
1007 ListRead.enumerate(~Element,~Context,~sample,count,first,context) : List<&2,Element>}:
1008 match count:
1009 case 0n: {==}
1010 case 1n+ +rest:
1011 Equal.cong(List<&2,Element>,List<&2,Element>,values => sample(context,first) <> values,
1012 collect_values_context(~&2,~Element,~Nat,~Context,~sample,Ranges.range(rest,1n+first),context),
1013 ListRead.enumerate(~Element,~Context,~sample,rest,1n+first,context),collect_values_context_range(~Element,~Context,~sample,rest,1n+first,context))
1014
1015def collect_next_length(~Source: Data,~Element: Data,~Context: Data,+count: Nat,
1016 head: Source & Traversal.Collected<&2,Context,Element>,tail: Source -> Context -> Source & List<&2,Element>,
1017 tail_length: @+source: Source -> @+context: Context -> {List.length(&2,Element,Pair.snd(Source,List<&2,Element>,tail(source,context))) == count : Nat}) ->
1018 {List.length(&2,Element,Pair.snd(Source,List<&2,Element>,Traversal.collect_next(~&2,~Source,~Element,~Context,head,tail))) == 1n+count : Nat}:
1019 (+source,Traversal.Collected{+context,+value}) = head
1020 %Equal.sym(List<&2,Element>,Pair.snd(Source,List<&2,Element>,Traversal.collect_prepend(~&2,~Source,~Element,value,tail(source,context))),
1021 value <> Pair.snd(Source,List<&2,Element>,tail(source,context)),collect_prepend_values(~Source,~Element,value,tail(source,context))) :
1022 {List.length(&2,Element,_) == 1n+count : Nat}
1023 Equal.cong(Nat,Nat,length => 1n+length,List.length(&2,Element,Pair.snd(Source,List<&2,Element>,tail(source,context))),count,tail_length(source,context))
1024
1025def collect_length(~Source: Data,~Element: Data,~Context: Data,
1026 ~read: Source -> Context -> Source & Traversal.Collected<&2,Context,Element>,count: Nat,+source: Source,+context: Context) ->
1027 {List.length(&2,Element,Pair.snd(Source,List<&2,Element>,Traversal.collect(~&2,~Source,~Element,~Context,~read,count,source,context))) == count : Nat}:
1028 match count:
1029 case 0n: {==}
1030 case 1n+ +rest:
1031 collect_next_length(~Source,~Element,~Context,rest,read(source,context),
1032 source => context => Traversal.collect(~&2,~Source,~Element,~Context,~read,rest,source,context),
1033 source => context => collect_length(~Source,~Element,~Context,~read,rest,source,context))
1034
1035# Pointwise equality on the visited keys preserves any collected value list.
1036def collect_values_context_agrees(~Element: Data,~Key: Data,~LeftContext: Data,~RightContext: Data,
1037 ~left: LeftContext -> Key -> Element,~right: RightContext -> Key -> Element,
1038 +keys: List<&2,Key>,+left_context: LeftContext,+right_context: RightContext,
1039 agreements: Members.All(Key,{key => {left(left_context,key) == right(right_context,key) : Element} : Key -> Data},keys)) ->
1040 {collect_values_context(~&2,~Element,~Key,~LeftContext,~left,keys,left_context) ==
1041 collect_values_context(~&2,~Element,~Key,~RightContext,~right,keys,right_context) : List<&2,Element>}:
1042 match keys:
1043 case Nil{}: {==}
1044 case +key <> +rest:
1045 Shape.Both{head,tail} = agreements
1046 %Equal.sym(Element,left(left_context,key),right(right_context,key),head) :
1047 {_ <> collect_values_context(~&2,~Element,~Key,~LeftContext,~left,rest,left_context) ==
1048 right(right_context,key) <> collect_values_context(~&2,~Element,~Key,~RightContext,~right,rest,right_context) : List<&2,Element>}
1049 Equal.cong(List<&2,Element>,List<&2,Element>,values => right(right_context,key) <> values,
1050 collect_values_context(~&2,~Element,~Key,~LeftContext,~left,rest,left_context),
1051 collect_values_context(~&2,~Element,~Key,~RightContext,~right,rest,right_context),
1052 collect_values_context_agrees(~Element,~Key,~LeftContext,~RightContext,~left,~right,rest,left_context,right_context,tail))
1053
1054# A fixed context condition is carried unchanged while its fold is projected.
1055def indexed_fold_change_context_under(~State: Data,~Outer: Data,~Inner: Data,
1056 ~project: Outer -> Inner,~Condition: Outer -> Data,
1057 ~outer_step: U32 -> Outer -> State -> State,~inner_step: U32 -> Inner -> State -> State,
1058 ~same_step: @+index: U32 -> @+context: Outer -> @+state: State -> Condition(context) ->
1059 {outer_step(index,context,state) == inner_step(index,project(context),state) : State},
1060 count: Nat,+first: U32,+context: Outer,+state: State,+condition: Condition(context)) ->
1061 {Traversal.indexed_fold(~State,~Outer,~outer_step,count,first,context,state) ==
1062 Traversal.indexed_fold(~State,~Inner,~inner_step,count,first,project(context),state) : State}:
1063 match count:
1064 case 0n: {==}
1065 case 1n+rest:
1066 %Equal.sym(State,outer_step(first,context,state),inner_step(first,project(context),state),same_step(first,context,state,condition)) :
1067 {Traversal.indexed_fold(~State,~Outer,~outer_step,rest,(first + 1 : U32),context,_) ==
1068 Traversal.indexed_fold(~State,~Inner,~inner_step,rest,(first + 1 : U32),project(context),inner_step(first,project(context),state)) : State}
1069 indexed_fold_change_context_under(~State,~Outer,~Inner,~project,~Condition,~outer_step,~inner_step,~same_step,rest,(first + 1 : U32),context,inner_step(first,project(context),state),condition)