1	# One round of Cells.map on packed trees, for every element and cell type:
2	# the cell passes through the scratch array unchanged, so the round is what
3	# gather and scatter do to the values.
4	import Base
5	import ../traversal_cells.bend as Cells
6	import ./storage_tree_model.bend as Tree
7	import ./storage_refinement.bend as StorageLaws
8	import ./storage_readback.bend as StorageReadback
9	
10	# Reading the just-written scratch slot returns its cell at every slot.
11	# Owner projections can use this fact without identifying their certificates.
12	def 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	  {==}
23	
24	def round_with(~Owner: Type,~Cell: Data,~Context: Data,~gather: Owner -> U32 -> Context -> Owner & Cell,
25	  ~scatter: Owner -> U32 -> Cell -> Owner,~width: U32,
26	  -values: Owner,+scratch: Tree.Tree<Cell>,+position: U32,+slot: U32,+context: Context,+cell: Cell,-result: Owner,
27	  gathered: {gather(values,position,context) == (values,cell) : Owner & Cell},
28	  scattered: {scatter(values,position,cell) == result : Owner}) ->
29	  {Cells.step(~Owner,~Cell,~Context,~gather,~scatter,~width,Cells.State{values,Tree.pack(Cell,scratch),position,slot,context}) ==
30	    Cells.State{result,Tree.pack(Cell,Tree.write(Cell,scratch,slot,cell)),(position + width : U32),U32.and((slot + 1 : U32),63),context} :
31	    Cells.State<Owner,Cell,Context>}:
32	  +written = Tree.write(Cell,scratch,slot,cell)
33	  %Equal.sym(Owner & Cell,gather(values,position,context),(values,cell),gathered) :
34	    {Cells.stored(~Owner,~Cell,~Context,~scatter,~width,position,slot,context,Tree.pack(Cell,scratch),_) ==
35	      Cells.State{result,Tree.pack(Cell,written),(position + width : U32),U32.and((slot + 1 : U32),63),context} : Cells.State<Owner,Cell,Context>}
36	  %Equal.sym(Array<Cell> & Cell,Array.get(Cell,Array.set(Cell,Tree.pack(Cell,scratch),slot,cell),slot),(Tree.pack(Cell,written),cell),scratch_readback(~Cell,scratch,slot,cell)) :
37	    {Cells.scattered(~Owner,~Cell,~Context,~scatter,~width,position,slot,context,values,_) ==
38	      Cells.State{result,Tree.pack(Cell,written),(position + width : U32),U32.and((slot + 1 : U32),63),context} : Cells.State<Owner,Cell,Context>}
39	  %Equal.sym(Owner,scatter(values,position,cell),result,scattered) :
40	    {Cells.State{_,Tree.pack(Cell,written),(position + width : U32),U32.and((slot + 1 : U32),63),context} ==
41	      Cells.State{result,Tree.pack(Cell,written),(position + width : U32),U32.and((slot + 1 : U32),63),context} : Cells.State<Owner,Cell,Context>}
42	  {==}
43	
44	def round(~Element: Data,~Cell: Data,~Context: Data,~gather: Array<Element> -> U32 -> Context -> Array<Element> & Cell,
45	  ~scatter: Array<Element> -> U32 -> Cell -> Array<Element>,~width: U32,
46	  +values: Tree.Tree<Element>,+scratch: Tree.Tree<Cell>,+position: U32,+slot: U32,+context: Context,+cell: Cell,+result: Tree.Tree<Element>,
47	  gathered: {gather(Tree.pack(Element,values),position,context) == (Tree.pack(Element,values),cell) : Array<Element> & Cell},
48	  scattered: {scatter(Tree.pack(Element,values),position,cell) == Tree.pack(Element,result) : Array<Element>}) ->
49	  {Cells.step(~Array<Element>,~Cell,~Context,~gather,~scatter,~width,Cells.State{Tree.pack(Element,values),Tree.pack(Cell,scratch),position,slot,context}) ==
50	    Cells.State{Tree.pack(Element,result),Tree.pack(Cell,Tree.write(Cell,scratch,slot,cell)),(position + width : U32),U32.and((slot + 1 : U32),63),context} :
51	    Cells.State<Array<Element>,Cell,Context>}:
52	  round_with(~Array<Element>,~Cell,~Context,~gather,~scatter,~width,Tree.pack(Element,values),scratch,position,slot,context,cell,Tree.pack(Element,result),gathered,scattered)
53	
54	type Observed<-Model: Type,-Cell: Data,-Context: Data> is Type:
55	  Observed{values: Model,scratch: Tree.Tree<Cell>,position: U32,slot: U32,context: Context}
56	
57	def observe(~Owner: Type,~Model: Type,~Cell: Data,~Context: Data,~project: Owner -> Model,state: Cells.State<Owner,Cell,Context>) -> Observed<Model,Cell,Context>:
58	  Cells.State{values,scratch,position,slot,context} = state
59	  Observed{project(values),Tree.reflect(Cell,scratch),position,slot,context}
60	
61	def observe_gather(~Owner: Type,~Model: Type,~Cell: Data,~project: Owner -> Model,result: Owner & Cell) -> Model & Cell:
62	  (owner,cell) = result
63	  (project(owner),cell)
64	
65	def model_stored(~Model: Type,~Cell: Data,~Context: Data,~scatter: Model -> U32 -> Cell -> Model,~width: U32,
66	  +position: U32,+slot: U32,context: Context,scratch: Tree.Tree<Cell>,result: Model & Cell) -> Observed<Model,Cell,Context>:
67	  (owner,+cell) = result
68	  Observed{scatter(owner,position,cell),Tree.write(Cell,scratch,slot,cell),(position + width : U32),U32.and((slot + 1 : U32),63),context}
69	
70	# One shared scratch round; gather and scatter supply their numerical laws.
71	def 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))