proofs/traversal_lanes_certificate.bend

stelliferous@0.0.2.0 · 88 lines · 7 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.2.0/kernel_tile.bend as Tile
5import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness
6import stelliferous@0.0.2.0/traversal_lanes.bend as Lanes
7import stelliferous@0.0.2.0/traversal_array.bend as Traversal
8import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
9import stelliferous@0.0.2.0/proofs/storage_certificate.bend as Certificate
10import stelliferous@0.0.2.0/proofs/storage_shape.bend as Shape
11import stelliferous@0.0.2.0/proofs/traversal_lanes_witness.bend as LanesWitness
12import stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend as LanesLaws
13import stelliferous@0.0.2.0/proofs/boolean_logic.bend as Boolean
14import stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend as Arithmetic
15import stelliferous@0.0.2.0/proofs/storage_refinement.bend as StorageLaws
16import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness
17
18def map_when(~Context: Data,~operation: Context -> F32 -> F32,+covered: Bool,+count: Nat,+position: U32,+context: Context,-values: Array<F32>,
19  certificate: Certificate.Certificate<F32,values>) -> Certificate.Certificate<F32,Lanes.map_when(~Context,~operation,covered,count,position,context,values)>:
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<F32>}
25    {==}}
26
27# The cover test of a balanced tree gives the bounds of the refinement.
28def refines(~Context: Data,~operation: Context -> F32 -> F32,+covered: Bool,+count: Nat,+position: U32,+context: Context,+values: Tree.Tree<F32>,+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<F32>}:
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<F32>}
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
42def observed(~Context: Data,~operation: Context -> F32 -> F32,+count: Nat,+position: U32,+context: Context,-values: Array<F32>,+depth: Nat,
43  balanced: Shape.Balanced(F32,depth,Tree.reflect(F32,values)),observation: StorageLaws.Observation<F32,values>) ->
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<F32>}:
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<F32>}
50  refines(~Context,~operation,Lanes.covered(depth,position,count),count,position,context,tree,depth,
51    %Equal.sym(Tree.Tree<F32>,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.
54def certified(~Context: Data,~operation: Context -> F32 -> F32,+count: Nat,+position: U32,+context: Context,values: Array<F32>,+depth: Nat,
55  equation: {values == Tree.pack(F32,Certificate.normalized(F32,depth,Tree.reflect(F32,values))) : Array<F32>}) ->
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<F32>}:
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.
63def gathered_owner(~Context: Data,~map: Context -> F32 -> F32,-values: Array<F32>,position: U32,context: Context,
64  evidence: LanesWitness.Gathered<values,Lanes.gather(~Context,~map,values,position,context)>) ->
65  {TraversalWitness.first(~Array<F32>,~Tile.Tile8,Lanes.gather(~Context,~map,values,position,context)) == values : Array<F32>}:
66  LanesWitness.Gathered{cell,equation} = evidence
67  %Equal.sym(Array<F32> & Tile.Tile8,Lanes.gather(~Context,~map,values,position,context),(values,cell),equation) :
68    {TraversalWitness.first(~Array<F32>,~Tile.Tile8,_) == values : Array<F32>}
69  {==}
70
71def gather(~Context: Data,~map: Context -> F32 -> F32,-values: Array<F32>,+position: U32,+context: Context,
72  certificate: Certificate.Certificate<F32,values>) ->
73  Certificate.Certificate<F32,TraversalWitness.first(~Array<F32>,~Tile.Tile8,Lanes.gather(~Context,~map,values,position,context))>:
74  Certificate.Certificate{+depth,+equation} = certificate
75  %Equal.sym(Array<F32>,TraversalWitness.first(~Array<F32>,~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<F32,_>
79  Certificate.Certificate{depth,equation}
80
81def scatter(-values: Array<F32>,+position: U32,-tile: Tile.Tile8,certificate: Certificate.Certificate<F32,values>) ->
82  Certificate.Certificate<F32,Lanes.scatter(values,position,tile)>:
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<F32>}
88    {==}}