~/bend-docscommunity

proofs/traversal_cells_refinement.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/traversal_cells_refinement.bend as Traversal_cells_refinement

One round of Cells.map on packed trees, for every element and cell type: the cell passes through the scratch array unchanged, so the round is what gather and scatter do to the values.

5 imports
import Base
import ../traversal_cells.bend as Cells
import ./storage_tree_model.bend as Tree
import ./storage_refinement.bend as StorageLaws
import ./storage_readback.bend as StorageReadback

Types

type Observed source · line 54 · raw

@-Model:Type -> @-Cell:Data -> @-Context:Data -> Type

Templates

template scratch_readback source · line 12 · raw

@-Cell:Data -> @+scratch:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Cell> -> @+slot:U32 -> @+cell:Cell -> {Array.get(Cell, Array.set(Cell, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Cell, scratch), slot, cell), slot) == (0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Cell, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.write(Cell, scratch, slot, cell)), cell) : Pair(Array<Cell>, Cell)}

Reading the just-written scratch slot returns its cell at every slot. Owner projections can use this fact without identifying their certificates.

template round_with source · line 24 · raw

@-Owner:Type -> @-Cell:Data -> @-Context:Data -> @-gather:(@_:Owner -> @_:U32 -> @_:Context -> Pair(Owner, Cell)) -> @-scatter:(@_:Owner -> @_:U32 -> @_:Cell -> Owner) -> @-width:U32 -> @-values:Owner -> @+scratch:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Cell> -> @+position:U32 -> @+slot:U32 -> @+context:Context -> @+cell:Cell -> @-result:Owner -> @gathered:{gather(values, position, context) == (values, cell) : Pair(Owner, Cell)} -> @scattered:{scatter(values, position, cell) == result : Owner} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.step(Owner, Cell, Context, gather, scatter, width, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.State{values, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Cell, scratch), position, slot, context}) == 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.State{result, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Cell, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.write(Cell, scratch, slot, cell)), U32.add(position, width), U32.and(U32.add(slot, 1), 63), context} : 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.State<Owner, Cell, Context>}

template round source · line 44 · raw

@-Element:Data -> @-Cell:Data -> @-Context:Data -> @-gather:(@_:Array<Element> -> @_:U32 -> @_:Context -> Pair(Array<Element>, Cell)) -> @-scatter:(@_:Array<Element> -> @_:U32 -> @_:Cell -> Array<Element>) -> @-width:U32 -> @+values:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @+scratch:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Cell> -> @+position:U32 -> @+slot:U32 -> @+context:Context -> @+cell:Cell -> @+result:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Element> -> @gathered:{gather(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, values), position, context) == (0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, values), cell) : Pair(Array<Element>, Cell)} -> @scattered:{scatter(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, values), position, cell) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, result) : Array<Element>} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.step(Array<Element>, Cell, Context, gather, scatter, width, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.State{0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, values), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Cell, scratch), position, slot, context}) == 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.State{0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, result), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Cell, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.write(Cell, scratch, slot, cell)), U32.add(position, width), U32.and(U32.add(slot, 1), 63), context} : 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.State<Array<Element>, Cell, Context>}

template observe source · line 57 · raw

@-Owner:Type -> @-Model:Type -> @-Cell:Data -> @-Context:Data -> @-project:(@_:Owner -> Model) -> @state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.State<Owner, Cell, Context> -> Observed<Model, Cell, Context>

template observe_gather source · line 61 · raw

@-Owner:Type -> @-Model:Type -> @-Cell:Data -> @-project:(@_:Owner -> Model) -> @result:Pair(Owner, Cell) -> Pair(Model, Cell)

template model_stored source · line 65 · raw

@-Model:Type -> @-Cell:Data -> @-Context:Data -> @-scatter:(@_:Model -> @_:U32 -> @_:Cell -> Model) -> @-width:U32 -> @+position:U32 -> @+slot:U32 -> @context:Context -> @scratch:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Cell> -> @result:Pair(Model, Cell) -> Observed<Model, Cell, Context>

template stored_observed source · line 71 · raw

@-Owner:Type -> @-Model:Type -> @-Cell:Data -> @-Context:Data -> @-project:(@_:Owner -> Model) -> @-scatter:(@_:Owner -> @_:U32 -> @_:Cell -> Owner) -> @-model_scatter:(@_:Model -> @_:U32 -> @_:Cell -> Model) -> @-width:U32 -> @-scatter_matches:(@owner:Owner -> @+position:U32 -> @+cell:Cell -> {project(scatter(owner, position, cell)) == model_scatter(project(owner), position, cell) : Model}) -> @+position:U32 -> @+slot:U32 -> @+context:Context -> @+scratch:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<Cell> -> @result:Pair(Owner, Cell) -> {observe(Owner, Model, Cell, Context, project, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.stored(Owner, Cell, Context, scatter, width, position, slot, context, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Cell, scratch), result)) == model_stored(Model, Cell, Context, model_scatter, width, position, slot, context, scratch, observe_gather(Owner, Model, Cell, project, result)) : Observed<Model, Cell, Context>}

One shared scratch round; gather and scatter supply their numerical laws.