storage_clone.bend source

storage_clone.bend on the hub · documented module

import Baseimport ./storage_buffer.bend as Storageimport ./proofs/storage_certificate.bend as Certificateimport ./proofs/storage_clone_certificate.bend as CertificateClonedef buffers(~Element: Data,+length: Nat,pair: Array<Element> & Array<Element>,certificates: CertificateClone.Copies<Element,pair>) -> Storage.Buffer<Element> & Storage.Buffer<Element>:  (left,right) = pair  CertificateClone.Copies{left_certificate,right_certificate} = certificates  (Storage.Buffer{left,length,left_certificate},Storage.Buffer{right,length,right_certificate})def clone(~Element: Data,input: Storage.Buffer<Element>) -> Storage.Buffer<Element> & Storage.Buffer<Element>:  Storage.Buffer{input,length,certificate} = input  Certificate.Certificate{+depth,+equation} = certificate  buffers(~Element,length,Array.clone(Element,input),CertificateClone.clone(~Element,input,    Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation}))