def write_sequence

stelliferous@0.0.2.0 · proofs/storage_refinement.bend:223

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

223# Sequence transfers preserve native modular addressing for every element type.
224# Logical bounds belong to callers, independently of this representation law.
225def write_sequence(~Element: Data,+values: List<&2,Element>,+offset: U32,+tree: Tree.Tree<Element>) ->
226  {Storage.write_list(Element,values,offset,Tree.pack(Element,tree)) ==
227    Tree.pack(Element,Tree.write_sequence(~Element,values,offset,tree)) : Array<Element>}:
228  match values:
229    case Nil{}: {==}
230    case +head <> +tail:
231      %Equal.sym(Array<Element>,Array.set(Element,Tree.pack(Element,tree),offset,head),
232        Tree.pack(Element,Tree.write(Element,tree,offset,head)),write(Element,tree,offset,head)) :
233        {Storage.write_list(Element,tail,(offset + 1 : U32),_) ==
234          Tree.pack(Element,Tree.write_sequence(~Element,tail,(offset + 1 : U32),Tree.write(Element,tree,offset,head))) : Array<Element>}
235      write_sequence(~Element,tail,(offset + 1 : U32),Tree.write(Element,tree,offset,head))