TraversalCellsRefinement.round: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/traversal_cells_refinement.bend as TraversalCellsRefinement
Lines 44-52 of stelliferous@0.0.2.0/proofs/traversal_cells_refinement.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/traversal_cells_refinement.bend&start_line=44&end_line=52

import Base
import stelliferous@0.0.2.0/traversal_cells.bend as Cells
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree

def round(~Element: Data,~Cell: Data,~Context: Data,~gather: Array<Element> -> U32 -> Context -> Array<Element> & Cell,
  ~scatter: Array<Element> -> U32 -> Cell -> Array<Element>,~width: U32,
  +values: Tree.Tree<Element>,+scratch: Tree.Tree<Cell>,+position: U32,+slot: U32,+context: Context,+cell: Cell,+result: Tree.Tree<Element>,
  gathered: {gather(Tree.pack(Element,values),position,context) == (Tree.pack(Element,values),cell) : Array<Element> & Cell},
  scattered: {scatter(Tree.pack(Element,values),position,cell) == Tree.pack(Element,result) : Array<Element>}) ->
  {Cells.step(~Array<Element>,~Cell,~Context,~gather,~scatter,~width,Cells.State{Tree.pack(Element,values),Tree.pack(Cell,scratch),position,slot,context}) ==
    Cells.State{Tree.pack(Element,result),Tree.pack(Cell,Tree.write(Cell,scratch,slot,cell)),(position + width : U32),U32.and((slot + 1 : U32),63),context} :
    Cells.State<Array<Element>,Cell,Context>}:
  round_with(~Array<Element>,~Cell,~Context,~gather,~scatter,~width,Tree.pack(Element,values),scratch,position,slot,context,cell,Tree.pack(Element,result),gathered,scattered)

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.and
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=Tree
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=pack
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=write
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_cells_refinement.bend&name=round_with
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_cells.bend&name=State
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_cells.bend&name=step