def scratch_readback

stelliferous@0.0.2.0 · proofs/traversal_cells_refinement.bend:10

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

10# Reading the just-written scratch slot returns its cell at every slot.
11# Owner projections can use this fact without identifying their certificates.
12def scratch_readback(~Cell: Data,+scratch: Tree.Tree<Cell>,+slot: U32,+cell: Cell) ->
13  {Array.get(Cell,Array.set(Cell,Tree.pack(Cell,scratch),slot,cell),slot) ==
14    (Tree.pack(Cell,Tree.write(Cell,scratch,slot,cell)),cell) : Array<Cell> & Cell}:
15  +written = Tree.write(Cell,scratch,slot,cell)
16  %Equal.sym(Array<Cell>,Array.set(Cell,Tree.pack(Cell,scratch),slot,cell),Tree.pack(Cell,written),StorageLaws.write(Cell,scratch,slot,cell)) :
17    {Array.get(Cell,_,slot) == (Tree.pack(Cell,written),cell) : Array<Cell> & Cell}
18  %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)) :
19    {_ == (Tree.pack(Cell,written),cell) : Array<Cell> & Cell}
20  %Equal.sym(Cell,Tree.read(Cell,written,slot),cell,StorageReadback.read_written(~Cell,scratch,slot,cell)) :
21    {(Tree.pack(Cell,written),_) == (Tree.pack(Cell,written),cell) : Array<Cell> & Cell}
22  {==}