1	import Base
2	import ./kernel_spatial_packing.bend as Packing
3	import ./kernel_tile.bend as Tile
4	import ./storage_buffer.bend as Storage
5	import ./proofs/kernel_packing_certificate.bend as PackingCertificate
6	import ./proofs/storage_certificate.bend as Certificate
7	import ./proofs/traversal_certificate.bend as TraversalCertificate
8	
9	def buffers(input_length: Nat,output_length: Nat,result: Array<F32> & Array<Tile.Tile8>,
10	  certificates: TraversalCertificate.Certificates<Array<F32>,Tile.Tile8,Certificate.family(~F32),result>) ->
11	  Storage.Buffer<F32> & Storage.Buffer<Tile.Tile8>:
12	  (input,output) = result
13	  TraversalCertificate.Certificates{source_certificate,output_certificate} = certificates
14	  (Storage.Buffer{input,input_length,source_certificate},Storage.Buffer{output,output_length,output_certificate})
15	
16	def run(+call: Packing.Call,input: Storage.Buffer<F32>,output: Storage.Buffer<Tile.Tile8>) -> Storage.Buffer<F32> & Storage.Buffer<Tile.Tile8>:
17	  Storage.Buffer{input,input_length,input_certificate} = input
18	  Storage.Buffer{output,output_length,output_certificate} = output
19	  buffers(input_length,output_length,Packing.run(call,input,output),PackingCertificate.certificates(call,input,output,input_certificate,output_certificate))