def stored_observed

stelliferous@0.0.2.0 · proofs/traversal_cells_refinement.bend:70

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

70# One shared scratch round; gather and scatter supply their numerical laws.
71def stored_observed(~Owner: Type,~Model: Type,~Cell: Data,~Context: Data,~project: Owner -> Model,
72  ~scatter: Owner -> U32 -> Cell -> Owner,~model_scatter: Model -> U32 -> Cell -> Model,~width: U32,
73  ~scatter_matches: @owner: Owner -> @+position: U32 -> @+cell: Cell ->
74    {project(scatter(owner,position,cell)) == model_scatter(project(owner),position,cell) : Model},
75  +position: U32,+slot: U32,+context: Context,+scratch: Tree.Tree<Cell>,result: Owner & Cell) ->
76  {observe(~Owner,~Model,~Cell,~Context,~project,Cells.stored(~Owner,~Cell,~Context,~scatter,~width,position,slot,context,Tree.pack(Cell,scratch),result)) ==
77    model_stored(~Model,~Cell,~Context,~model_scatter,~width,position,slot,context,scratch,observe_gather(~Owner,~Model,~Cell,~project,result)) : Observed<Model,Cell,Context>}:
78  (owner,+cell) = result
79  %Equal.sym(Array<Cell> & Cell,Array.get(Cell,Array.set(Cell,Tree.pack(Cell,scratch),slot,cell),slot),
80    (Tree.pack(Cell,Tree.write(Cell,scratch,slot,cell)),cell),scratch_readback(~Cell,scratch,slot,cell)) :
81    {observe(~Owner,~Model,~Cell,~Context,~project,Cells.scattered(~Owner,~Cell,~Context,~scatter,~width,position,slot,context,owner,_)) ==
82      model_stored(~Model,~Cell,~Context,~model_scatter,~width,position,slot,context,scratch,(project(owner),cell)) : Observed<Model,Cell,Context>}
83  %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))) :
84    {Observed{project(scatter(owner,position,cell)),_,(position + width : U32),U32.and((slot + 1 : U32),63),context} ==
85      model_stored(~Model,~Cell,~Context,~model_scatter,~width,position,slot,context,scratch,(project(owner),cell)) : Observed<Model,Cell,Context>}
86  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},
87    project(scatter(owner,position,cell)),model_scatter(project(owner),position,cell),scatter_matches(owner,position,cell))