TraversalCellsRefinement.scratch_readback: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/traversal_cells_refinement.bend as TraversalCellsRefinement
Lines 10-22 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=10&end_line=22

import Base
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
import stelliferous@0.0.2.0/proofs/storage_refinement.bend as StorageLaws
import stelliferous@0.0.2.0/proofs/storage_readback.bend as StorageReadback

# Reading the just-written scratch slot returns its cell at every slot.
# Owner projections can use this fact without identifying their certificates.
def scratch_readback(~Cell: Data,+scratch: Tree.Tree<Cell>,+slot: U32,+cell: Cell) ->
  {Array.get(Cell,Array.set(Cell,Tree.pack(Cell,scratch),slot,cell),slot) ==
    (Tree.pack(Cell,Tree.write(Cell,scratch,slot,cell)),cell) : Array<Cell> & Cell}:
  +written = Tree.write(Cell,scratch,slot,cell)
  %Equal.sym(Array<Cell>,Array.set(Cell,Tree.pack(Cell,scratch),slot,cell),Tree.pack(Cell,written),StorageLaws.write(Cell,scratch,slot,cell)) :
    {Array.get(Cell,_,slot) == (Tree.pack(Cell,written),cell) : Array<Cell> & Cell}
  %Equal.sym(Array<Cell> & Cell,Array.get(Cell,Tree.pack(Cell,written),slot),(Tree.pack(Cell,written),Tree.read(Cell,written,slot)),StorageLaws.read(Cell,written,slot)) :
    {_ == (Tree.pack(Cell,written),cell) : Array<Cell> & Cell}
  %Equal.sym(Cell,Tree.read(Cell,written,slot),cell,StorageReadback.read_written(~Cell,scratch,slot,cell)) :
    {(Tree.pack(Cell,written),_) == (Tree.pack(Cell,written),cell) : Array<Cell> & Cell}
  {==}

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.set
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=stelliferous@0.0.2.0/proofs/storage_readback.bend&name=read_written
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_refinement.bend&name=read
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_refinement.bend&name=write
  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=read
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=write