~/bend-docscommunity

proofs/traversal_lanes_certificate.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/traversal_lanes_certificate.bend as Traversal_lanes_certificate

The live certificate of Lanes.map_when, and its refinement: with the cover test of the certificate's depth it is Traversal.map_in_place.

14 imports
import Base
import ../kernel_tile.bend as Tile
import ./traversal_witness.bend as TraversalWitness
import ../traversal_lanes.bend as Lanes
import ../traversal_array.bend as Traversal
import ./storage_tree_model.bend as Tree
import ./storage_certificate.bend as Certificate
import ./storage_shape.bend as Shape
import ./traversal_lanes_witness.bend as LanesWitness
import ./traversal_lanes_refinement.bend as LanesLaws
import ./boolean_logic.bend as Boolean
import ./bounded_u32_arithmetic.bend as Arithmetic
import ./storage_refinement.bend as StorageLaws
import ./storage_witness.bend as Witness

Definitions

def scatter source · line 81 · raw

@-values:Array<F32> -> @+position:U32 -> @-tile:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8 -> @certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<F32, values> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<F32, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.scatter(values, position, tile)>

Templates

template map_when source · line 18 · raw

@-Context:Data -> @-operation:(@_:Context -> @_:F32 -> F32) -> @+covered:Bool -> @+count:Nat -> @+position:U32 -> @+context:Context -> @-values:Array<F32> -> @certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<F32, values> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<F32, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.map_when(Context, operation, covered, count, position, context, values)>

template refines source · line 28 · raw

@-Context:Data -> @-operation:(@_:Context -> @_:F32 -> F32) -> @+covered:Bool -> @+count:Nat -> @+position:U32 -> @+context:Context -> @+values:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<F32> -> @+depth:Nat -> @+balanced:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_shape.Balanced(F32, depth, values) -> @+guard:{0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.covered(depth, position, count) == covered : Bool} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.map_when(Context, operation, covered, count, position, context, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(F32, values)) == 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.map_in_place(F32, Context, operation, count, position, context, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(F32, values)) : Array<F32>}

The cover test of a balanced tree gives the bounds of the refinement.

template observed source · line 42 · raw

@-Context:Data -> @-operation:(@_:Context -> @_:F32 -> F32) -> @+count:Nat -> @+position:U32 -> @+context:Context -> @-values:Array<F32> -> @+depth:Nat -> @balanced:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_shape.Balanced(F32, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(F32, values)) -> @observation:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_refinement.Observation<F32, values> -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.map_when(Context, operation, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.covered(depth, position, count), count, position, context, values) == 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.map_in_place(F32, Context, operation, count, position, context, values) : Array<F32>}

template certified source · line 54 · raw

@-Context:Data -> @-operation:(@_:Context -> @_:F32 -> F32) -> @+count:Nat -> @+position:U32 -> @+context:Context -> @values:Array<F32> -> @+depth:Nat -> @equation:{values == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(F32, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.normalized(F32, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(F32, values))) : Array<F32>} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.map_when(Context, operation, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.covered(depth, position, count), count, position, context, values) == 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.map_in_place(F32, Context, operation, count, position, context, values) : Array<F32>}

On any certified array the map through tiles is the ordered map.

template gathered_owner source · line 63 · raw

@-Context:Data -> @-map:(@_:Context -> @_:F32 -> F32) -> @-values:Array<F32> -> @position:U32 -> @context:Context -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_lanes_witness.Gathered<values, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.gather(Context, map, values, position, context)> -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.first(Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.gather(Context, map, values, position, context)) == values : Array<F32>}

Reuse the existing gather/scatter witnesses when a cell owns certified buffers rather than passing flat certificates outside the whole traversal.

template gather source · line 71 · raw

@-Context:Data -> @-map:(@_:Context -> @_:F32 -> F32) -> @-values:Array<F32> -> @+position:U32 -> @+context:Context -> @certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<F32, values> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<F32, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.first(Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.gather(Context, map, values, position, context))>