~/bend-docscommunity

proofs/kernel_weights_certificate.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/kernel_weights_certificate.bend as Kernel_weights_certificate

12 imports
import Base
import ../kernel_weights.bend as Weights
import ../kernel_tile.bend as Tile
import ../traversal_array.bend as Traversal
import ../storage_allocation.bend as Allocation
import ../tensor.bend as Tensors
import ./kernel_weights_witness.bend as WeightsWitness
import ./traversal_witness.bend as TraversalWitness
import ./storage_witness.bend as Witness
import ./storage_certificate.bend as Certificate
import ./storage_allocation_refinement.bend as AllocationLaws
import ./storage_tree_model.bend as Tree

Definitions

def family source · line 14 · raw

@-input:Array<F32> -> Data

def block source · line 17 · raw

@+depth:Nat -> @+block:U32 -> @+layout:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_weights.Layout -> @-input:Array<F32> -> @-owners:Pair(Array<F32>, Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8>) -> @input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<F32, input> -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.ResultEvidence<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input, depth, owners> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.ResultEvidence<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_weights.copy_block(block, layout, owners)>

def traverse source · line 31 · raw

@+depth:Nat -> @count:Nat -> @+index:U32 -> @+layout:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_weights.Layout -> @-input:Array<F32> -> @-owners:Pair(Array<F32>, Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8>) -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<F32, input> -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.ResultEvidence<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input, depth, owners> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.ResultEvidence<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.indexed_fold(Pair(Array<F32>, Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8>), 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_weights.Layout, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_weights.copy_block, count, index, layout, owners)>

def finish source · line 41 · raw

@-depth:Nat -> @-input:Array<F32> -> @-owners:Pair(Array<F32>, Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8>) -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.ResultEvidence<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input, depth, owners> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_weights.reordered(owners))

def allocated source · line 47 · raw

@+depth:Nat -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_allocation.array(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.filled(0.0)))

def run source · line 52 · raw

@+rows:U32 -> @+inner:U32 -> @-input:Array<F32> -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<F32, input> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor.depth_for(U32.mul(U32.div(U32.add(rows, 7), 8), inner)), 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_weights.run(rows, inner, input))

def equation source · line 61 · raw

@+rows:U32 -> @+inner:U32 -> @-input:Array<F32> -> @certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<F32, input> -> {0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_weights.run(rows, inner, input) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.normalized(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor.depth_for(U32.mul(U32.div(U32.add(rows, 7), 8), inner)), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_weights.run(rows, inner, input)))) : Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8>}

def certificate source · line 70 · raw

@+rows:U32 -> @+inner:U32 -> @-input:Array<F32> -> @certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<F32, input> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_weights.run(rows, inner, input)>