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

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
import stelliferous@0.0.2.0/proofs/storage_refinement.bend as StorageLaws

# One shared scratch round; gather and scatter supply their numerical laws.
def stored_observed(~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: Tree.Tree<Cell>,result: Owner & Cell) ->
  {observe(~Owner,~Model,~Cell,~Context,~project,Cells.stored(~Owner,~Cell,~Context,~scatter,~width,position,slot,context,Tree.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>}:
  (owner,+cell) = result
  %Equal.sym(Array<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),scratch_readback(~Cell,scratch,slot,cell)) :
    {observe(~Owner,~Model,~Cell,~Context,~project,Cells.scattered(~Owner,~Cell,~Context,~scatter,~width,position,slot,context,owner,_)) ==
      model_stored(~Model,~Cell,~Context,~model_scatter,~width,position,slot,context,scratch,(project(owner),cell)) : Observed<Model,Cell,Context>}
  %Equal.sym(Tree.Tree<Cell>,Tree.reflect(Cell,Tree.pack(Cell,Tree.write(Cell,scratch,slot,cell))),Tree.write(Cell,scratch,slot,cell),StorageLaws.reflect_packed(Cell,Tree.write(Cell,scratch,slot,cell))) :
    {Observed{project(scatter(owner,position,cell)),_,(position + width : U32),U32.and((slot + 1 : U32),63),context} ==
      model_stored(~Model,~Cell,~Context,~model_scatter,~width,position,slot,context,scratch,(project(owner),cell)) : Observed<Model,Cell,Context>}
  Equal.cong(Model,Observed<Model,Cell,Context>,values => Observed{values,Tree.write(Cell,scratch,slot,cell),(position + width : U32),U32.and((slot + 1 : U32),63),context},
    project(scatter(owner,position,cell)),model_scatter(project(owner),position,cell),scatter_matches(owner,position,cell))

Uses (22):
  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.cong
  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=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.and
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_refinement.bend&name=reflect_packed
  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=reflect
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=write
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_cells_refinement.bend&name=Observed
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_cells_refinement.bend&name=model_stored
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_cells_refinement.bend&name=observe
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_cells_refinement.bend&name=observe_gather
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_cells_refinement.bend&name=scratch_readback
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_cells.bend&name=scattered
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_cells.bend&name=stored