proofs/traversal_lanes_certificate.bend
stelliferous@0.0.3.0 · 140 lines · 0 definitions
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.
3import Base
4import stelliferous@0.0.3.0/kernel_tile.bend as Tile
5import stelliferous@0.0.3.0/proofs/traversal_witness.bend as TraversalWitness
6import stelliferous@0.0.3.0/traversal_lanes.bend as Lanes
7import stelliferous@0.0.3.0/traversal_cells.bend as Cells
8import stelliferous@0.0.3.0/traversal_array.bend as Traversal
9import stelliferous@0.0.3.0/proofs/storage_tree_model.bend as Tree
10import stelliferous@0.0.3.0/proofs/storage_certificate.bend as Certificate
11import stelliferous@0.0.3.0/proofs/storage_shape.bend as Shape
12import stelliferous@0.0.3.0/proofs/traversal_lanes_witness.bend as LanesWitness
13import stelliferous@0.0.3.0/proofs/traversal_lanes_refinement.bend as LanesLaws
14import stelliferous@0.0.3.0/proofs/boolean_logic.bend as Boolean
15import stelliferous@0.0.3.0/proofs/bounded_u32_arithmetic.bend as Arithmetic
16import stelliferous@0.0.3.0/proofs/storage_refinement.bend as StorageLaws
17import stelliferous@0.0.3.0/proofs/storage_witness.bend as Witness
18
19def map_when(~Context: Data,~operation: Context -> F32 -> F32,+covered: Bool,+count: Nat,+position: U32,+context: Context,-values: Array<F32>,
20 certificate: Certificate.Certificate<F32,values>) -> Certificate.Certificate<F32,Lanes.map_when(~Context,~operation,covered,count,position,context,values)>:
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<F32>}
26 {==}}
27
28# The cover test of a balanced tree gives the bounds of the refinement.
29def refines(~Context: Data,~operation: Context -> F32 -> F32,+covered: Bool,+count: Nat,+position: U32,+context: Context,+values: Tree.Tree<F32>,+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<F32>}:
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<F32>}
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
43def observed(~Context: Data,~operation: Context -> F32 -> F32,+count: Nat,+position: U32,+context: Context,-values: Array<F32>,+depth: Nat,
44 balanced: Shape.Balanced(F32,depth,Tree.reflect(F32,values)),observation: StorageLaws.Observation<F32,values>) ->
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<F32>}:
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<F32>}
51 refines(~Context,~operation,Lanes.covered(depth,position,count),count,position,context,tree,depth,
52 %Equal.sym(Tree.Tree<F32>,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.
55def certified(~Context: Data,~operation: Context -> F32 -> F32,+count: Nat,+position: U32,+context: Context,values: Array<F32>,+depth: Nat,
56 equation: {values == Tree.pack(F32,Certificate.normalized(F32,depth,Tree.reflect(F32,values))) : Array<F32>}) ->
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<F32>}:
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.
64def gathered_owner(~Context: Data,~map: Context -> F32 -> F32,-values: Array<F32>,position: U32,context: Context,
65 evidence: LanesWitness.Gathered<values,Lanes.gather(~Context,~map,values,position,context)>) ->
66 {TraversalWitness.first(~Array<F32>,~Tile.Tile8,Lanes.gather(~Context,~map,values,position,context)) == values : Array<F32>}:
67 LanesWitness.Gathered{cell,equation} = evidence
68 %Equal.sym(Array<F32> & Tile.Tile8,Lanes.gather(~Context,~map,values,position,context),(values,cell),equation) :
69 {TraversalWitness.first(~Array<F32>,~Tile.Tile8,_) == values : Array<F32>}
70 {==}
71
72def gather(~Context: Data,~map: Context -> F32 -> F32,-values: Array<F32>,+position: U32,+context: Context,
73 certificate: Certificate.Certificate<F32,values>) ->
74 Certificate.Certificate<F32,TraversalWitness.first(~Array<F32>,~Tile.Tile8,Lanes.gather(~Context,~map,values,position,context))>:
75 Certificate.Certificate{+depth,+equation} = certificate
76 %Equal.sym(Array<F32>,TraversalWitness.first(~Array<F32>,~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<F32,_>
80 Certificate.Certificate{depth,equation}
81
82def scatter(-values: Array<F32>,+position: U32,-tile: Tile.Tile8,certificate: Certificate.Certificate<F32,values>) ->
83 Certificate.Certificate<F32,Lanes.scatter(values,position,tile)>:
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<F32>}
89 {==}}
90
91# Transforming a gathered cell keeps the owner and its shape witness.
92def transformed_gathered(~Context: Data,~transform: Context -> Tile.Tile8 -> Tile.Tile8,-values: Array<F32>,+position: U32,+context: Context,
93 evidence: LanesWitness.Gathered<values,Lanes.gather(~Context,~Lanes.identity(~Context),values,position,context)>) ->
94 LanesWitness.Gathered<values,Lanes.gather_transformed(~Context,~transform,values,position,context)>:
95 LanesWitness.Gathered{cell,equation} = evidence
96 LanesWitness.Gathered{transform(context,cell),
97 Equal.cong(Array<F32> & Tile.Tile8,Array<F32> & Tile.Tile8,Lanes.transformed(~Context,~transform,context),
98 Lanes.gather(~Context,~Lanes.identity(~Context),values,position,context),(values,cell),equation)}
99
100def transformed_gather(~Context: Data,~transform: Context -> Tile.Tile8 -> Tile.Tile8,+depth: Nat,-values: Array<F32>,+position: U32,+context: Context,+witness: Witness.Witness(F32,depth,values)) ->
101 LanesWitness.Gathered<values,Lanes.gather_transformed(~Context,~transform,values,position,context)>:
102 transformed_gathered(~Context,~transform,values,position,context,LanesWitness.gather(~Context,~Lanes.identity(~Context),depth,values,position,context,witness))
103
104def transformed_mapped(~Context: Data,~operation: Context -> F32 -> F32,~transform: Context -> Tile.Tile8 -> Tile.Tile8,+depth: Nat,count: Nat,+position: U32,+context: Context,-values: Array<F32>,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
109def 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<F32>,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
115def 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<F32>,certificate: Certificate.Certificate<F32,values>) ->
116 Certificate.Certificate<F32,Lanes.map_with_when(~Context,~operation,~Lanes.gather_transformed(~Context,~transform),covered,count,position,context,values)>:
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<F32>}
122 {==}}
123
124def certified_with_observed(~Context: Data,~operation: Context -> F32 -> F32,~collect: Array<F32> -> U32 -> Context -> Array<F32> & Tile.Tile8,~lawful: LanesLaws.GatherLaw(~Context,~operation,~collect),+count: Nat,+position: U32,+context: Context,-values: Array<F32>,+depth: Nat,
125 +equation: {values == Tree.pack(F32,Certificate.normalized(F32,depth,Tree.reflect(F32,values))) : Array<F32>},observation: StorageLaws.Observation<F32,values>) ->
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<F32>}:
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<F32>}
129 Equal.trans(Array<F32>,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<F32>,Tree.pack(F32,tree),values,packed) : {_ == Tree.pack(F32,Certificate.normalized(F32,depth,Tree.reflect(F32,_))) : Array<F32>}
135 equation))
136
137def certified_with(~Context: Data,~operation: Context -> F32 -> F32,~collect: Array<F32> -> U32 -> Context -> Array<F32> & Tile.Tile8,~lawful: LanesLaws.GatherLaw(~Context,~operation,~collect),+count: Nat,+position: U32,+context: Context,values: Array<F32>,+depth: Nat,
138 +equation: {values == Tree.pack(F32,Certificate.normalized(F32,depth,Tree.reflect(F32,values))) : Array<F32>}) ->
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<F32>}:
140 certified_with_observed(~Context,~operation,~collect,~lawful,count,position,context,values,depth,equation,StorageLaws.observe(F32,values))