def contents

stelliferous@0.0.2.0 · proofs/storage_allocation_refinement.bend:58

import Base
import stelliferous@0.0.2.0/storage_buffer.bend as Storage
import stelliferous@0.0.2.0/storage_allocation.bend as Allocation
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
import stelliferous@0.0.2.0/proofs/storage_refinement.bend as StorageLaws
import stelliferous@0.0.2.0/proofs/storage_buffer_model.bend as Buffer

58def contents(~Element: Data,+depth: Nat,+value: Element,+length: Nat) ->
59  {Buffer.contents(~Element,Allocation.allocate(~Element,depth,value,length)) == Buffer.Content{Tree.fresh(Element,depth,value),length} : Buffer.Content<Element>}:
60  %Equal.sym(Storage.Buffer<Element>,Allocation.allocate(~Element,depth,value,length),Storage.allocate(~Element,depth,value,length),dispatch_same(Element,Allocation.allocated(~Element),depth,value,length)) :
61    {Buffer.contents(~Element,_) == Buffer.Content{Tree.fresh(Element,depth,value),length} : Buffer.Content<Element>}
62  %Equal.sym(Array<Element>,Array.new(Element,depth,value),Tree.pack(Element,Tree.fresh(Element,depth,value)),StorageLaws.fresh(Element,depth,value)) :
63    {Buffer.Content{Tree.reflect(Element,_),length} == Buffer.Content{Tree.fresh(Element,depth,value),length} : Buffer.Content<Element>}
64  Equal.cong(Tree.Tree<Element>,Buffer.Content<Element>,tree => Buffer.Content{tree,length},Tree.reflect(Element,Tree.pack(Element,Tree.fresh(Element,depth,value))),Tree.fresh(Element,depth,value),StorageLaws.reflect_packed(Element,Tree.fresh(Element,depth,value)))