def read_sequence

stelliferous@0.0.2.0 · proofs/storage_refinement.bend:237

import Base
import stelliferous@0.0.2.0/storage_buffer.bend as Storage
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree

237def read_sequence(~Element: Data,+count: Nat,+offset: U32,+tree: Tree.Tree<Element>) ->
238  {Storage.read_list(Element,count,offset,Tree.pack(Element,tree)) ==
239    Tree.read_sequence(~Element,count,offset,tree) : List<&2,Element>}:
240  match count:
241    case 0n: {==}
242    case 1n+ +rest:
243      %Equal.sym(Array<Element> & Element,Array.get(Element,Tree.pack(Element,tree),offset),
244        (Tree.pack(Element,tree),Tree.read(Element,tree,offset)),read(Element,tree,offset)) :
245        {Storage.bind_pair(Array<Element>,Element,List<&2,Element>,_,storage => value =>
246          value <> Storage.read_list(Element,rest,(offset + 1 : U32),storage)) ==
247          Tree.read(Element,tree,offset) <> Tree.read_sequence(~Element,rest,(offset + 1 : U32),tree) : List<&2,Element>}
248      %read_sequence(~Element,rest,(offset + 1 : U32),tree) :
249        {Tree.read(Element,tree,offset) <> Storage.read_list(Element,rest,(offset + 1 : U32),Tree.pack(Element,tree)) ==
250          Tree.read(Element,tree,offset) <> _ : List<&2,Element>}
251      {==}