1	import Base
2	import ./storage_buffer.bend as Storage
3	import ./proofs/storage_certificate.bend as Certificate
4	import ./proofs/storage_clone_certificate.bend as CertificateClone
5	
6	def buffers(~Element: Data,+length: Nat,pair: Array<Element> & Array<Element>,certificates: CertificateClone.Copies<Element,pair>) -> Storage.Buffer<Element> & Storage.Buffer<Element>:
7	  (left,right) = pair
8	  CertificateClone.Copies{left_certificate,right_certificate} = certificates
9	  (Storage.Buffer{left,length,left_certificate},Storage.Buffer{right,length,right_certificate})
10	
11	def clone(~Element: Data,input: Storage.Buffer<Element>) -> Storage.Buffer<Element> & Storage.Buffer<Element>:
12	  Storage.Buffer{input,length,certificate} = input
13	  Certificate.Certificate{+depth,+equation} = certificate
14	  buffers(~Element,length,Array.clone(Element,input),CertificateClone.clone(~Element,input,
15	    Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation}))