def round

stelliferous@0.0.2.0 · proofs/traversal_cells_refinement.bend:44

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

44def round(~Element: Data,~Cell: Data,~Context: Data,~gather: Array<Element> -> U32 -> Context -> Array<Element> & Cell,
45  ~scatter: Array<Element> -> U32 -> Cell -> Array<Element>,~width: U32,
46  +values: Tree.Tree<Element>,+scratch: Tree.Tree<Cell>,+position: U32,+slot: U32,+context: Context,+cell: Cell,+result: Tree.Tree<Element>,
47  gathered: {gather(Tree.pack(Element,values),position,context) == (Tree.pack(Element,values),cell) : Array<Element> & Cell},
48  scattered: {scatter(Tree.pack(Element,values),position,cell) == Tree.pack(Element,result) : Array<Element>}) ->
49  {Cells.step(~Array<Element>,~Cell,~Context,~gather,~scatter,~width,Cells.State{Tree.pack(Element,values),Tree.pack(Cell,scratch),position,slot,context}) ==
50    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} :
51    Cells.State<Array<Element>,Cell,Context>}:
52  round_with(~Array<Element>,~Cell,~Context,~gather,~scatter,~width,Tree.pack(Element,values),scratch,position,slot,context,cell,Tree.pack(Element,result),gathered,scattered)