~/bend-docscommunity

proofs/traversal_lanes_refinement.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend as Traversal_lanes_refinement

Lanes.map is Traversal.map_in_place: on a balanced array that holds its count positions, the rounds through tiles and the ordered scalar map leave the same array.

19 imports
import Base
import ../traversal_lanes.bend as Lanes
import ../traversal_cells.bend as Cells
import ../traversal_array.bend as Traversal
import ../traversal_loop.bend as Loop
import ../kernel_tile.bend as Tile
import ./traversal_cells_refinement.bend as CellLaws
import ./traversal_batch_refinement.bend as Batch
import ./traversal_array_refinement.bend as ArrayLaws
import ./traversal_map_readback.bend as MapReadback
import ./storage_tree_model.bend as Tree
import ./storage_refinement.bend as StorageLaws
import ./storage_shape.bend as Shape
import ./nat_to_u32_bounds.bend as Bounds
import ./nat_order.bend as Order
import ./nat_division.bend as Division
import ./word_encoding.bend as WordEncoding
import ./word_arithmetic.bend as WordArithmetic
import ./word_power_of_two.bend as Power

Definitions

def written source · line 73 · raw

@+values:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<F32> -> @+position:U32 -> @a:F32 -> @b:F32 -> @c:F32 -> @d:F32 -> @e:F32 -> @f:F32 -> @g:F32 -> @h:F32 -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<F32>

Eight ordered writes from position.

def scattered source · line 83 · raw

@+values:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<F32> -> @+position:U32 -> @+a:F32 -> @+b:F32 -> @+c:F32 -> @+d:F32 -> @+e:F32 -> @+f:F32 -> @+g:F32 -> @+h:F32 -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.scatter(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(F32, values), position, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile{a, b, c, d, e, f, g, h}) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(F32, written(values, position, a, b, c, d, e, f, g, h)) : Array<F32>}

def stepped source · line 171 · raw

@steps:Nat -> @start:Nat -> U32

The position of the model map after k steps from start.

def advanced source · line 176 · raw

@+steps:Nat -> @+start:Nat -> {stepped(steps, start) == U32.from_nat(Nat.add(steps, start)) : U32}

def after_round source · line 183 · raw

@+start:Nat -> {U32.add(U32.from_nat(start), 8) == U32.from_nat(8n+start) : U32}

def round_room source · line 187 · raw

@+start:Nat -> @+rest:Nat -> @+capacity:Nat -> @room:{Nat.is_le(Nat.add(start, 8n+rest), capacity) == True{} : Bool} -> {Nat.is_le(Nat.add(start, 8n), capacity) == True{} : Bool}

def rest_room source · line 191 · raw

@+start:Nat -> @+rest:Nat -> @+capacity:Nat -> @room:{Nat.is_le(Nat.add(start, 8n+rest), capacity) == True{} : Bool} -> {Nat.is_le(Nat.add(8n+start, rest), capacity) == True{} : Bool}

Templates

template cell source · line 25 · raw

@-Context:Data -> @-map:(@_:Context -> @_:F32 -> F32) -> @+values:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<F32> -> @+position:U32 -> @+context:Context -> 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8

The tile a round gathers at position.

template gathered source · line 36 · raw

@-Context:Data -> @-map:(@_:Context -> @_:F32 -> F32) -> @+values:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<F32> -> @+position:U32 -> @+context:Context -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.gather(Context, map, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(F32, values), position, context) == (0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(F32, values), cell(Context, map, values, position, context)) : Pair(Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8)}

template cell_scattered source · line 116 · raw

@-Context:Data -> @-map:(@_:Context -> @_:F32 -> F32) -> @+values:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<F32> -> @+position:U32 -> @+context:Context -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.scatter(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(F32, values), position, cell(Context, map, values, position, context)) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(F32, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_batch_refinement.batch(F32, Context, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_array_refinement.unindexed(F32, Context, map), 8n, position, context, values, values)) : Array<F32>}

template round source · line 130 · raw

@-Context:Data -> @-map:(@_:Context -> @_:F32 -> F32) -> @+values:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<F32> -> @+scratch:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @+start:Nat -> @+slot:U32 -> @+context:Context -> @+depth:Nat -> @+capacity:U32 -> @+capacity_equal:{0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(F32, values) == capacity : U32} -> @+balanced:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_shape.Balanced(F32, depth, values) -> @+limit:{Nat.is_le(depth, 30n) == True{} : Bool} -> @+capacity_ok:{U32.is_le(capacity, 2147483648) == True{} : Bool} -> @+room:{Nat.is_le(Nat.add(start, 8n), U32.to_nat(capacity)) == True{} : Bool} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.step(Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, Context, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.gather(Context, map), 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.scatter, 8, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.State{0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(F32, values), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, scratch), U32.from_nat(start), slot, context}) == 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.State{0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(F32, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_map_readback.run(F32, Context, map, 8n, U32.from_nat(start), context, values)), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.write(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, scratch, slot, cell(Context, map, values, U32.from_nat(start), context))), U32.add(U32.from_nat(start), 8), U32.and(U32.add(slot, 1), 63), context} : 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.State<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, Context>}

One round maps eight positions.

template output source · line 149 · raw

@-Context:Data -> @+state:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_batch_refinement.ModelState(F32, Context) -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.mapped_output(F32, Context, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_array_refinement.represent_map(F32, Context, state)) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(F32, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_map_readback.output(F32, Context, state)) : Array<F32>}

The scalar map from any position, on a packed tree.

template scalar source · line 154 · raw

@-Context:Data -> @-map:(@_:Context -> @_:F32 -> F32) -> @+count:Nat -> @+position:U32 -> @+context:Context -> @+values:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<F32> -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.map_in_place(F32, Context, map, count, position, context, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(F32, values)) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(F32, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_map_readback.run(F32, Context, map, count, position, context, values)) : Array<F32>}

template few source · line 165 · raw

@-Context:Data -> @-map:(@_:Context -> @_:F32 -> F32) -> @+count:Nat -> @+position:U32 -> @+slot:U32 -> @+context:Context -> @+values:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<F32> -> @+scratch:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.finish(Context, map, count, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.State{0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(F32, values), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, scratch), position, slot, context}) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(F32, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_map_readback.run(F32, Context, map, count, position, context, values)) : Array<F32>}

template finish_small source · line 199 · raw

@-Owner:Type -> @-Context:Data -> @-gather:(@_:Owner -> @_:U32 -> @_:Context -> Pair(Owner, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8)) -> @-scatter:(@_:Owner -> @_:U32 -> @_:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8 -> Owner) -> @-finish:(@_:Nat -> @_:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.State<Owner, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, Context> -> Owner) -> @+count:Nat -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.State<Owner, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, Context> -> @small:{Nat.is_lt(count, 8n) == True{} : Bool} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.rounds_with(Owner, Context, gather, scatter, finish, count, state) == finish(count, state) : Owner}

The shared induction on eight-value rounds. The proposition may carry all owners and bounds, so binary and ternary instances need only local cases.

template by_rounds source · line 216 · raw

@-Property:(@_:Nat -> Type) -> @-few:(@+count:Nat -> @_:{Nat.is_lt(count, 8n) == True{} : Bool} -> Property(count)) -> @-more:(@+rest:Nat -> @_:Property(rest) -> Property(8n+rest)) -> @count:Nat -> Property(count)

template rounds_property source · line 232 · raw

@-Context:Data -> @-map:(@_:Context -> @_:F32 -> F32) -> @count:Nat -> Type

Every count: whole rounds, then the last positions one by one.

template few_rounds source · line 240 · raw

@-Context:Data -> @-map:(@_:Context -> @_:F32 -> F32) -> @+count:Nat -> @small:{Nat.is_lt(count, 8n) == True{} : Bool} -> rounds_property(Context, map, count)

template more_rounds source · line 264 · raw

@-Context:Data -> @-map:(@_:Context -> @_:F32 -> F32) -> @+rest:Nat -> @previous:rounds_property(Context, map, rest) -> rounds_property(Context, map, 8n+rest)

template rounds source · line 285 · raw

@-Context:Data -> @-map:(@_:Context -> @_:F32 -> F32) -> @count:Nat -> @+start:Nat -> @+slot:U32 -> @+context:Context -> @+values:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<F32> -> @+scratch:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @+depth:Nat -> @+capacity:U32 -> @+capacity_equal:{0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.capacity(F32, values) == capacity : U32} -> @+balanced:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_shape.Balanced(F32, depth, values) -> @+limit:{Nat.is_le(depth, 30n) == True{} : Bool} -> @+capacity_ok:{U32.is_le(capacity, 2147483648) == True{} : Bool} -> @+room:{Nat.is_le(Nat.add(start, count), U32.to_nat(capacity)) == True{} : Bool} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.rounds(Context, map, count, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.State{0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(F32, values), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, scratch), U32.from_nat(start), slot, context}) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(F32, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_map_readback.run(F32, Context, map, count, U32.from_nat(start), context, values)) : Array<F32>}

template map source · line 294 · raw

@-Context:Data -> @-map:(@_:Context -> @_:F32 -> F32) -> @+count:Nat -> @+start:Nat -> @+context:Context -> @+values:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.Tree<F32> -> @+depth:Nat -> @+balanced:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_shape.Balanced(F32, depth, values) -> @+limit:{Nat.is_le(depth, 30n) == True{} : Bool} -> @+room:{Nat.is_le(Nat.add(start, count), U32.to_nat(U32.shln(1, depth))) == True{} : Bool} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.map(Context, map, count, U32.from_nat(start), context, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(F32, values)) == 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.map_in_place(F32, Context, map, count, U32.from_nat(start), context, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(F32, values)) : Array<F32>}

The whole map from any position, with a fresh scratch array.