proofs/kernel_packing_certificate.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/kernel_packing_certificate.bend as Kernel_packing_certificate

8 imports

import Base
import ../kernel_spatial_packing.bend as Packing
import ../kernel_tile.bend as Tile
import ./kernel_packing_witness.bend as PackingWitness
import ./storage_tree_model.bend as Tree
import ./storage_certificate.bend as Certificate
import ./traversal_witness.bend as TraversalWitness
import ./traversal_certificate.bend as TraversalCertificate

Definitions

def preserves source · line 10 · raw

@+depth:Nat -> @call:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.Call -> @-input:Array<F32> -> @-output:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @input_certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<F32, input> -> @equation:{output == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.normalized(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, output))) : Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8>} -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.ResultEvidence<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.run(call, input, output)>

def certificates source · line 16 · raw

@call:0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.Call -> @-input:Array<F32> -> @-output:Array<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8> -> @input_certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<F32, input> -> @output_certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, output> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_certificate.Certificates<Array<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.family(F32), 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.run(call, input, output)>