~/bend-docscommunity

proofs/kernel_gather_certificate.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/kernel_gather_certificate.bend as Kernel_gather_certificate

7 imports
import Base
import ../kernel_gather.bend as Gather
import ../traversal_array.bend as Traversal
import ./storage_witness.bend as Witness
import ./storage_tree_model.bend as Tree
import ./storage_certificate.bend as Certificate
import ./traversal_witness.bend as TraversalWitness

Definitions

def channel source · line 9 · raw

@+depth:Nat -> @+channel:U32 -> @+width:U32 -> @+offset:U32 -> @+positions:U32 -> @+span:U32 -> @-input:Array<F32> -> @-owners:Pair(Array<F32>, Array<F32>) -> @input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<F32, input> -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.ResultEvidence<Array<F32>, F32, input, depth, owners> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.ResultEvidence<Array<F32>, F32, input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gather.gather_channel(channel, width, offset, positions, span, owners)>

def channels source · line 22 · raw

@+depth:Nat -> @count:Nat -> @+index:U32 -> @+width:U32 -> @+offset:U32 -> @+positions:U32 -> @+span:U32 -> @-input:Array<F32> -> @-owners:Pair(Array<F32>, Array<F32>) -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<F32, input> -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.ResultEvidence<Array<F32>, F32, input, depth, owners> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.ResultEvidence<Array<F32>, F32, input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gather.gather_channels(count, index, width, offset, positions, span, owners)>

def finish source · line 31 · raw

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

def block source · line 37 · raw

@+depth:Nat -> @+count:U32 -> @+offset:U32 -> @+positions:U32 -> @+span:U32 -> @-input:Array<F32> -> @-output:Array<F32> -> @input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<F32, input> -> @balanced:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, output) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(F32, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gather.gather_block(count, offset, positions, span, input, output))

def equation source · line 44 · raw

@+depth:Nat -> @count:U32 -> @offset:U32 -> @positions:U32 -> @span:U32 -> @-input:Array<F32> -> @-output:Array<F32> -> @input_certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<F32, input> -> @balanced:{output == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(F32, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.normalized(F32, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(F32, output))) : Array<F32>} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gather.gather_block(count, offset, positions, span, input, output) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(F32, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.normalized(F32, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(F32, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gather.gather_block(count, offset, positions, span, input, output)))) : Array<F32>}

def certificate source · line 53 · raw

@count:U32 -> @offset:U32 -> @positions:U32 -> @span:U32 -> @-input:Array<F32> -> @-output:Array<F32> -> @input_certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<F32, input> -> @output_certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<F32, output> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<F32, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gather.gather_block(count, offset, positions, span, input, output)>