def model_stored

stelliferous@0.0.2.0 · proofs/traversal_cells_refinement.bend:65

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

65def model_stored(~Model: Type,~Cell: Data,~Context: Data,~scatter: Model -> U32 -> Cell -> Model,~width: U32,
66  +position: U32,+slot: U32,context: Context,scratch: Tree.Tree<Cell>,result: Model & Cell) -> Observed<Model,Cell,Context>:
67  (owner,+cell) = result
68  Observed{scatter(owner,position,cell),Tree.write(Cell,scratch,slot,cell),(position + width : U32),U32.and((slot + 1 : U32),63),context}