def clone

stelliferous@0.0.2.0 · proofs/storage_witness.bend:208

import Base

208# The native clone duplicates payload ownership, while its source observation
209# and balance depth are unchanged. This theorem is consumed only by rewrites.
210def clone(-Element: Data,+depth: Nat,-storage: Array<Element>,witness: Witness(Element,depth,storage)) ->
211  {Array.clone(Element,storage) == (storage,storage) : Array<Element> & Array<Element>}:
212  match depth witness:
213    case 0n Leaf{value,owner}:
214      %Equal.sym(Array<Element>,storage,ALeaf{value},owner) : {Array.clone(Element,_) == (_,_) : Array<Element> & Array<Element>}
215      {==}
216    case 1n+ +rest Node{left,right,owner,left_balanced,right_balanced}:
217      %Equal.sym(Array<Element>,storage,ANode{left,right},owner) : {Array.clone(Element,_) == (_,_) : Array<Element> & Array<Element>}
218      %Equal.sym(Array<Element> & Array<Element>,Array.clone(Element,left),(left,left),clone(Element,rest,left,left_balanced)) :
219        {Array.clone.node(Element,_,Array.clone(Element,right)) == (ANode{left,right},ANode{left,right}) : Array<Element> & Array<Element>}
220      %Equal.sym(Array<Element> & Array<Element>,Array.clone(Element,right),(right,right),clone(Element,rest,right,right_balanced)) :
221        {Array.clone.node(Element,(left,left),_) == (ANode{left,right},ANode{left,right}) : Array<Element> & Array<Element>}
222      {==}