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_cells.bend as Cells 8 import ../traversal_array.bend as Traversal 9 import ./storage_tree_model.bend as Tree 10 import ./storage_certificate.bend as Certificate 11 import ./storage_shape.bend as Shape 12 import ./traversal_lanes_witness.bend as LanesWitness 13 import ./traversal_lanes_refinement.bend as LanesLaws 14 import ./boolean_logic.bend as Boolean 15 import ./bounded_u32_arithmetic.bend as Arithmetic 16 import ./storage_refinement.bend as StorageLaws 17 import ./storage_witness.bend as Witness 18 19 def map_when(~Context: Data,~operation: Context -> F32 -> F32,+covered: Bool,+count: Nat,+position: U32,+context: Context,-values: Array, 20 certificate: Certificate.Certificate) -> Certificate.Certificate: 21 Certificate.Certificate{+depth,equation} = certificate 22 Certificate.Certificate{depth, 23 %Certificate.restored(F32,depth,Lanes.map_when(~Context,~operation,covered,count,position,context,values), 24 LanesWitness.map_when(~Context,~operation,covered,depth,count,position,context,values,Certificate.witness_at(F32,depth,values,equation))) : 25 {_ == Tree.pack(F32,Certificate.normalized(F32,depth,Tree.reflect(F32,Lanes.map_when(~Context,~operation,covered,count,position,context,values)))) : Array} 26 {==}} 27 28 # The cover test of a balanced tree gives the bounds of the refinement. 29 def refines(~Context: Data,~operation: Context -> F32 -> F32,+covered: Bool,+count: Nat,+position: U32,+context: Context,+values: Tree.Tree,+depth: Nat, 30 +balanced: Shape.Balanced(F32,depth,values),+guard: {Lanes.covered(depth,position,count) == covered : Bool}) -> 31 {Lanes.map_when(~Context,~operation,covered,count,position,context,Tree.pack(F32,values)) == 32 Traversal.map_in_place(~F32,~Context,~operation,count,position,context,Tree.pack(F32,values)) : Array}: 33 match covered: 34 case False{}: {==} 35 case True{}: 36 +room = Nat.is_le(Nat.add(U32.to_nat(position),count),U32.to_nat(U32.shln(1,depth))) 37 %Arithmetic.native_roundtrip(position) : 38 {Lanes.map(~Context,~operation,count,_,context,Tree.pack(F32,values)) == 39 Traversal.map_in_place(~F32,~Context,~operation,count,_,context,Tree.pack(F32,values)) : Array} 40 LanesLaws.map(~Context,~operation,count,U32.to_nat(position),context,values,depth,balanced,Boolean.left(Nat.is_le(depth,30n),room,guard), 41 Boolean.right(Nat.is_le(depth,30n),room,guard)) 42 43 def observed(~Context: Data,~operation: Context -> F32 -> F32,+count: Nat,+position: U32,+context: Context,-values: Array,+depth: Nat, 44 balanced: Shape.Balanced(F32,depth,Tree.reflect(F32,values)),observation: StorageLaws.Observation) -> 45 {Lanes.map_when(~Context,~operation,Lanes.covered(depth,position,count),count,position,context,values) == 46 Traversal.map_in_place(~F32,~Context,~operation,count,position,context,values) : Array}: 47 StorageLaws.Observation{+tree,packed,reflected} = observation 48 %packed : 49 {Lanes.map_when(~Context,~operation,Lanes.covered(depth,position,count),count,position,context,_) == 50 Traversal.map_in_place(~F32,~Context,~operation,count,position,context,_) : Array} 51 refines(~Context,~operation,Lanes.covered(depth,position,count),count,position,context,tree,depth, 52 %Equal.sym(Tree.Tree,tree,Tree.reflect(F32,values),reflected) : Shape.Balanced(F32,depth,_) balanced,{==}) 53 54 # On any certified array the map through tiles is the ordered map. 55 def certified(~Context: Data,~operation: Context -> F32 -> F32,+count: Nat,+position: U32,+context: Context,values: Array,+depth: Nat, 56 equation: {values == Tree.pack(F32,Certificate.normalized(F32,depth,Tree.reflect(F32,values))) : Array}) -> 57 {Lanes.map_when(~Context,~operation,Lanes.covered(depth,position,count),count,position,context,values) == 58 Traversal.map_in_place(~F32,~Context,~operation,count,position,context,values) : Array}: 59 observed(~Context,~operation,count,position,context,values,depth,Witness.balanced(F32,depth,values,Certificate.witness_at(F32,depth,values,equation)), 60 StorageLaws.observe(F32,values)) 61 62 # Reuse the existing gather/scatter witnesses when a cell owns certified 63 # buffers rather than passing flat certificates outside the whole traversal. 64 def gathered_owner(~Context: Data,~map: Context -> F32 -> F32,-values: Array,position: U32,context: Context, 65 evidence: LanesWitness.Gathered) -> 66 {TraversalWitness.first(~Array,~Tile.Tile8,Lanes.gather(~Context,~map,values,position,context)) == values : Array}: 67 LanesWitness.Gathered{cell,equation} = evidence 68 %Equal.sym(Array & Tile.Tile8,Lanes.gather(~Context,~map,values,position,context),(values,cell),equation) : 69 {TraversalWitness.first(~Array,~Tile.Tile8,_) == values : Array} 70 {==} 71 72 def gather(~Context: Data,~map: Context -> F32 -> F32,-values: Array,+position: U32,+context: Context, 73 certificate: Certificate.Certificate) -> 74 Certificate.Certificate,~Tile.Tile8,Lanes.gather(~Context,~map,values,position,context))>: 75 Certificate.Certificate{+depth,+equation} = certificate 76 %Equal.sym(Array,TraversalWitness.first(~Array,~Tile.Tile8,Lanes.gather(~Context,~map,values,position,context)),values, 77 gathered_owner(~Context,~map,values,position,context, 78 LanesWitness.gather(~Context,~map,depth,values,position,context,Certificate.witness_at(F32,depth,values,equation)))) : 79 Certificate.Certificate 80 Certificate.Certificate{depth,equation} 81 82 def scatter(-values: Array,+position: U32,-tile: Tile.Tile8,certificate: Certificate.Certificate) -> 83 Certificate.Certificate: 84 Certificate.Certificate{+depth,equation} = certificate 85 Certificate.Certificate{depth, 86 %Certificate.restored(F32,depth,Lanes.scatter(values,position,tile), 87 LanesWitness.scatter(depth,values,position,tile,Certificate.witness_at(F32,depth,values,equation))) : 88 {_ == Tree.pack(F32,Certificate.normalized(F32,depth,Tree.reflect(F32,Lanes.scatter(values,position,tile)))) : Array} 89 {==}} 90 91 # Transforming a gathered cell keeps the owner and its shape witness. 92 def transformed_gathered(~Context: Data,~transform: Context -> Tile.Tile8 -> Tile.Tile8,-values: Array,+position: U32,+context: Context, 93 evidence: LanesWitness.Gathered) -> 94 LanesWitness.Gathered: 95 LanesWitness.Gathered{cell,equation} = evidence 96 LanesWitness.Gathered{transform(context,cell), 97 Equal.cong(Array & Tile.Tile8,Array & Tile.Tile8,Lanes.transformed(~Context,~transform,context), 98 Lanes.gather(~Context,~Lanes.identity(~Context),values,position,context),(values,cell),equation)} 99 100 def transformed_gather(~Context: Data,~transform: Context -> Tile.Tile8 -> Tile.Tile8,+depth: Nat,-values: Array,+position: U32,+context: Context,+witness: Witness.Witness(F32,depth,values)) -> 101 LanesWitness.Gathered: 102 transformed_gathered(~Context,~transform,values,position,context,LanesWitness.gather(~Context,~Lanes.identity(~Context),depth,values,position,context,witness)) 103 104 def transformed_mapped(~Context: Data,~operation: Context -> F32 -> F32,~transform: Context -> Tile.Tile8 -> Tile.Tile8,+depth: Nat,count: Nat,+position: U32,+context: Context,-values: Array,witness: Witness.Witness(F32,depth,values)) -> 105 Witness.Witness(F32,depth,Lanes.map_with(~Context,~operation,~Lanes.gather_transformed(~Context,~transform),count,position,context,values)): 106 LanesWitness.rounds_with(~Context,~operation,~Lanes.gather_transformed(~Context,~transform),~transformed_gather(~Context,~transform),depth,count,Cells.State{values,Lanes.scratch(),position,0,context}, 107 LanesWitness.Evidence{values,Lanes.scratch(),position,0,context,{==},witness,Witness.fresh(Tile.Tile8,6n,Tile.filled(0.0))}) 108 109 def transformed_shape(~Context: Data,~operation: Context -> F32 -> F32,~transform: Context -> Tile.Tile8 -> Tile.Tile8,covered: Bool,+depth: Nat,count: Nat,+position: U32,+context: Context,-values: Array,witness: Witness.Witness(F32,depth,values)) -> 110 Witness.Witness(F32,depth,Lanes.map_with_when(~Context,~operation,~Lanes.gather_transformed(~Context,~transform),covered,count,position,context,values)): 111 match covered: 112 case True{}: transformed_mapped(~Context,~operation,~transform,depth,count,position,context,values,witness) 113 case False{}: TraversalWitness.map_in_place(~F32,~Context,~operation,depth,count,position,context,values,witness) 114 115 def transformed_map_when(~Context: Data,~operation: Context -> F32 -> F32,~transform: Context -> Tile.Tile8 -> Tile.Tile8,+covered: Bool,+count: Nat,+position: U32,+context: Context,-values: Array,certificate: Certificate.Certificate) -> 116 Certificate.Certificate: 117 Certificate.Certificate{+depth,equation} = certificate 118 Certificate.Certificate{depth, 119 %Certificate.restored(F32,depth,Lanes.map_with_when(~Context,~operation,~Lanes.gather_transformed(~Context,~transform),covered,count,position,context,values), 120 transformed_shape(~Context,~operation,~transform,covered,depth,count,position,context,values,Certificate.witness_at(F32,depth,values,equation))) : 121 {_ == Tree.pack(F32,Certificate.normalized(F32,depth,Tree.reflect(F32,Lanes.map_with_when(~Context,~operation,~Lanes.gather_transformed(~Context,~transform),covered,count,position,context,values)))) : Array} 122 {==}} 123 124 def certified_with_observed(~Context: Data,~operation: Context -> F32 -> F32,~collect: Array -> U32 -> Context -> Array & Tile.Tile8,~lawful: LanesLaws.GatherLaw(~Context,~operation,~collect),+count: Nat,+position: U32,+context: Context,-values: Array,+depth: Nat, 125 +equation: {values == Tree.pack(F32,Certificate.normalized(F32,depth,Tree.reflect(F32,values))) : Array},observation: StorageLaws.Observation) -> 126 {Lanes.map_with_when(~Context,~operation,~collect,Lanes.covered(depth,position,count),count,position,context,values) == Traversal.map_in_place(~F32,~Context,~operation,count,position,context,values) : Array}: 127 StorageLaws.Observation{+tree,+packed,reflected} = observation 128 %packed : {Lanes.map_with_when(~Context,~operation,~collect,Lanes.covered(depth,position,count),count,position,context,_) == Traversal.map_in_place(~F32,~Context,~operation,count,position,context,_) : Array} 129 Equal.trans(Array,Lanes.map_with_when(~Context,~operation,~collect,Lanes.covered(depth,position,count),count,position,context,Tree.pack(F32,tree)), 130 Lanes.map_when(~Context,~operation,Lanes.covered(depth,position,count),count,position,context,Tree.pack(F32,tree)), 131 Traversal.map_in_place(~F32,~Context,~operation,count,position,context,Tree.pack(F32,tree)), 132 LanesLaws.map_with_when(~Context,~operation,~collect,~lawful,Lanes.covered(depth,position,count),count,position,context,Tree.pack(F32,tree)), 133 certified(~Context,~operation,count,position,context,Tree.pack(F32,tree),depth, 134 %Equal.sym(Array,Tree.pack(F32,tree),values,packed) : {_ == Tree.pack(F32,Certificate.normalized(F32,depth,Tree.reflect(F32,_))) : Array} 135 equation)) 136 137 def certified_with(~Context: Data,~operation: Context -> F32 -> F32,~collect: Array -> U32 -> Context -> Array & Tile.Tile8,~lawful: LanesLaws.GatherLaw(~Context,~operation,~collect),+count: Nat,+position: U32,+context: Context,values: Array,+depth: Nat, 138 +equation: {values == Tree.pack(F32,Certificate.normalized(F32,depth,Tree.reflect(F32,values))) : Array}) -> 139 {Lanes.map_with_when(~Context,~operation,~collect,Lanes.covered(depth,position,count),count,position,context,values) == Traversal.map_in_place(~F32,~Context,~operation,count,position,context,values) : Array}: 140 certified_with_observed(~Context,~operation,~collect,~lawful,count,position,context,values,depth,equation,StorageLaws.observe(F32,values))