1 # The live certificate of Lanes.map_when, and its refinement: with the cover 2 # test of the certificate's depth it is Traversal.map_in_place. 3 import Base 4 import ../kernel_tile.bend as Tile 5 import ./traversal_witness.bend as TraversalWitness 6 import ../traversal_lanes.bend as Lanes 7 import ../traversal_array.bend as Traversal 8 import ./storage_tree_model.bend as Tree 9 import ./storage_certificate.bend as Certificate 10 import ./storage_shape.bend as Shape 11 import ./traversal_lanes_witness.bend as LanesWitness 12 import ./traversal_lanes_refinement.bend as LanesLaws 13 import ./boolean_logic.bend as Boolean 14 import ./bounded_u32_arithmetic.bend as Arithmetic 15 import ./storage_refinement.bend as StorageLaws 16 import ./storage_witness.bend as Witness 17 18 def map_when(~Context: Data,~operation: Context -> F32 -> F32,+covered: Bool,+count: Nat,+position: U32,+context: Context,-values: Array, 19 certificate: Certificate.Certificate) -> Certificate.Certificate: 20 Certificate.Certificate{+depth,equation} = certificate 21 Certificate.Certificate{depth, 22 %Certificate.restored(F32,depth,Lanes.map_when(~Context,~operation,covered,count,position,context,values), 23 LanesWitness.map_when(~Context,~operation,covered,depth,count,position,context,values,Certificate.witness_at(F32,depth,values,equation))) : 24 {_ == Tree.pack(F32,Certificate.normalized(F32,depth,Tree.reflect(F32,Lanes.map_when(~Context,~operation,covered,count,position,context,values)))) : Array} 25 {==}} 26 27 # The cover test of a balanced tree gives the bounds of the refinement. 28 def refines(~Context: Data,~operation: Context -> F32 -> F32,+covered: Bool,+count: Nat,+position: U32,+context: Context,+values: Tree.Tree,+depth: Nat, 29 +balanced: Shape.Balanced(F32,depth,values),+guard: {Lanes.covered(depth,position,count) == covered : Bool}) -> 30 {Lanes.map_when(~Context,~operation,covered,count,position,context,Tree.pack(F32,values)) == 31 Traversal.map_in_place(~F32,~Context,~operation,count,position,context,Tree.pack(F32,values)) : Array}: 32 match covered: 33 case False{}: {==} 34 case True{}: 35 +room = Nat.is_le(Nat.add(U32.to_nat(position),count),U32.to_nat(U32.shln(1,depth))) 36 %Arithmetic.native_roundtrip(position) : 37 {Lanes.map(~Context,~operation,count,_,context,Tree.pack(F32,values)) == 38 Traversal.map_in_place(~F32,~Context,~operation,count,_,context,Tree.pack(F32,values)) : Array} 39 LanesLaws.map(~Context,~operation,count,U32.to_nat(position),context,values,depth,balanced,Boolean.left(Nat.is_le(depth,30n),room,guard), 40 Boolean.right(Nat.is_le(depth,30n),room,guard)) 41 42 def observed(~Context: Data,~operation: Context -> F32 -> F32,+count: Nat,+position: U32,+context: Context,-values: Array,+depth: Nat, 43 balanced: Shape.Balanced(F32,depth,Tree.reflect(F32,values)),observation: StorageLaws.Observation) -> 44 {Lanes.map_when(~Context,~operation,Lanes.covered(depth,position,count),count,position,context,values) == 45 Traversal.map_in_place(~F32,~Context,~operation,count,position,context,values) : Array}: 46 StorageLaws.Observation{+tree,packed,reflected} = observation 47 %packed : 48 {Lanes.map_when(~Context,~operation,Lanes.covered(depth,position,count),count,position,context,_) == 49 Traversal.map_in_place(~F32,~Context,~operation,count,position,context,_) : Array} 50 refines(~Context,~operation,Lanes.covered(depth,position,count),count,position,context,tree,depth, 51 %Equal.sym(Tree.Tree,tree,Tree.reflect(F32,values),reflected) : Shape.Balanced(F32,depth,_) balanced,{==}) 52 53 # On any certified array the map through tiles is the ordered map. 54 def certified(~Context: Data,~operation: Context -> F32 -> F32,+count: Nat,+position: U32,+context: Context,values: Array,+depth: Nat, 55 equation: {values == Tree.pack(F32,Certificate.normalized(F32,depth,Tree.reflect(F32,values))) : Array}) -> 56 {Lanes.map_when(~Context,~operation,Lanes.covered(depth,position,count),count,position,context,values) == 57 Traversal.map_in_place(~F32,~Context,~operation,count,position,context,values) : Array}: 58 observed(~Context,~operation,count,position,context,values,depth,Witness.balanced(F32,depth,values,Certificate.witness_at(F32,depth,values,equation)), 59 StorageLaws.observe(F32,values)) 60 61 # Reuse the existing gather/scatter witnesses when a cell owns certified 62 # buffers rather than passing flat certificates outside the whole traversal. 63 def gathered_owner(~Context: Data,~map: Context -> F32 -> F32,-values: Array,position: U32,context: Context, 64 evidence: LanesWitness.Gathered) -> 65 {TraversalWitness.first(~Array,~Tile.Tile8,Lanes.gather(~Context,~map,values,position,context)) == values : Array}: 66 LanesWitness.Gathered{cell,equation} = evidence 67 %Equal.sym(Array & Tile.Tile8,Lanes.gather(~Context,~map,values,position,context),(values,cell),equation) : 68 {TraversalWitness.first(~Array,~Tile.Tile8,_) == values : Array} 69 {==} 70 71 def gather(~Context: Data,~map: Context -> F32 -> F32,-values: Array,+position: U32,+context: Context, 72 certificate: Certificate.Certificate) -> 73 Certificate.Certificate,~Tile.Tile8,Lanes.gather(~Context,~map,values,position,context))>: 74 Certificate.Certificate{+depth,+equation} = certificate 75 %Equal.sym(Array,TraversalWitness.first(~Array,~Tile.Tile8,Lanes.gather(~Context,~map,values,position,context)),values, 76 gathered_owner(~Context,~map,values,position,context, 77 LanesWitness.gather(~Context,~map,depth,values,position,context,Certificate.witness_at(F32,depth,values,equation)))) : 78 Certificate.Certificate 79 Certificate.Certificate{depth,equation} 80 81 def scatter(-values: Array,+position: U32,-tile: Tile.Tile8,certificate: Certificate.Certificate) -> 82 Certificate.Certificate: 83 Certificate.Certificate{+depth,equation} = certificate 84 Certificate.Certificate{depth, 85 %Certificate.restored(F32,depth,Lanes.scatter(values,position,tile), 86 LanesWitness.scatter(depth,values,position,tile,Certificate.witness_at(F32,depth,values,equation))) : 87 {_ == Tree.pack(F32,Certificate.normalized(F32,depth,Tree.reflect(F32,Lanes.scatter(values,position,tile)))) : Array} 88 {==}}