proofs/traversal_lanes_witness.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/traversal_lanes_witness.bend as Traversal_lanes_witness

Shape evidence for Lanes.map: every round reads the values array, writes a scratch tile, reads it back and stores eight values, so the array keeps its depth. Numerical loops call none of these functions.

7 imports

import Base
import ../traversal_lanes.bend as Lanes
import ../traversal_cells.bend as Cells
import ../traversal_array.bend as Traversal
import ../kernel_tile.bend as Tile
import ./storage_witness.bend as Witness
import ./traversal_witness.bend as TraversalWitness

Types

type Gathered source · line 12 · raw

@-values:Array<F32> -> @-result:Pair(Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8) -> Data

Gathered

@-values:Array<F32> -> @-result:Pair(Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8) -> @-cell:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8 -> @equation:{result == (values, cell) : Pair(Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8)} -> Gathered<values, result>

type Evidence source · line 82 · raw

@-Context:Data -> @-depth:Nat -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.State<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, Context> -> Data

Evidence

@-Context:Data -> @-depth:Nat -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.State<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, Context> -> @-values:Array<F32> -> @-scratch:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @position:U32 -> @slot:U32 -> @context:Context -> @equation:{state == 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.State{values, scratch, position, slot, context} : 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.State<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, Context>} -> @values_witness:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, values) -> @scratch_witness:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, 6n, scratch) -> Evidence<Context, depth, state>

Definitions

def scatter source · line 57 · raw

@+depth:Nat -> @-values:Array<F32> -> @+position:U32 -> @-tile:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8 -> @witness:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, values) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.scatter(values, position, tile))

Templates

template gathered source · line 15 · raw

@-Context:Data -> @-map:(@_:Context -> @_:F32 -> F32) -> @-values:Array<F32> -> @+position:U32 -> @+context:Context -> @r0:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Read<F32, values, Array.get(F32, values, position)> -> @r1:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Read<F32, values, Array.get(F32, values, U32.add(position, 1))> -> @r2:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Read<F32, values, Array.get(F32, values, U32.add(U32.add(position, 1), 1))> -> @r3:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Read<F32, values, Array.get(F32, values, U32.add(U32.add(U32.add(position, 1), 1), 1))> -> @r4:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Read<F32, values, Array.get(F32, values, U32.add(U32.add(U32.add(U32.add(position, 1), 1), 1), 1))> -> @r5:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Read<F32, values, Array.get(F32, values, U32.add(U32.add(U32.add(U32.add(U32.add(position, 1), 1), 1), 1), 1))> -> @r6:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Read<F32, values, Array.get(F32, values, U32.add(U32.add(U32.add(U32.add(U32.add(U32.add(position, 1), 1), 1), 1), 1), 1))> -> @r7:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Read<F32, values, Array.get(F32, values, U32.add(U32.add(U32.add(U32.add(U32.add(U32.add(U32.add(position, 1), 1), 1), 1), 1), 1), 1))> -> Gathered<values, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.gather(Context, map, values, position, context)>

template gather source · line 44 · raw

@-Context:Data -> @-map:(@_:Context -> @_:F32 -> F32) -> @+depth:Nat -> @-values:Array<F32> -> @+position:U32 -> @+context:Context -> @+witness:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, values) -> Gathered<values, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.gather(Context, map, values, position, context)>

template scattered source · line 87 · raw

@-Context:Data -> @+depth:Nat -> @-values:Array<F32> -> @-scratch:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @+position:U32 -> @+slot:U32 -> @+context:Context -> @values_witness:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, values) -> @scratch_witness:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, 6n, scratch) -> @read:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Read<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, scratch, Array.get(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, scratch, slot)> -> Evidence<Context, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.scattered(Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, Context, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.scatter, 8, position, slot, context, values, Array.get(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, scratch, slot))>

template stored source · line 98 · raw

@-Context:Data -> @-map:(@_:Context -> @_:F32 -> F32) -> @+depth:Nat -> @-values:Array<F32> -> @-scratch:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @+position:U32 -> @+slot:U32 -> @+context:Context -> @values_witness:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, values) -> @scratch_witness:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, 6n, scratch) -> @gathered:Gathered<values, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.gather(Context, map, values, position, context)> -> Evidence<Context, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.stored(Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, Context, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.scatter, 8, position, slot, context, scratch, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.gather(Context, map, values, position, context))>

template step source · line 110 · raw

@-Context:Data -> @-map:(@_:Context -> @_:F32 -> F32) -> @+depth:Nat -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.State<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, Context> -> @evidence:Evidence<Context, depth, state> -> Evidence<Context, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.step(Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, Context, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.gather(Context, map), 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.scatter, 8, state)>

template finish source · line 119 · raw

@-Context:Data -> @-map:(@_:Context -> @_:F32 -> F32) -> @+depth:Nat -> @count:Nat -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.State<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, Context> -> @evidence:Evidence<Context, depth, state> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.finish(Context, map, count, state))

template rounds source · line 127 · raw

@-Context:Data -> @-map:(@_:Context -> @_:F32 -> F32) -> @+depth:Nat -> @count:Nat -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.State<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, Context> -> @evidence:Evidence<Context, depth, state> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.rounds(Context, map, count, state))

template map source · line 142 · raw

@-Context:Data -> @-map:(@_:Context -> @_:F32 -> F32) -> @+depth:Nat -> @count:Nat -> @+position:U32 -> @+context:Context -> @-values:Array<F32> -> @witness:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, values) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.map(Context, map, count, position, context, values))

template map_when source · line 147 · raw

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