KernelWeightsCertificate.allocated: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/kernel_weights_certificate.bend as KernelWeightsCertificate
Lines 47-50 of stelliferous@0.0.2.0/proofs/kernel_weights_certificate.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/kernel_weights_certificate.bend&start_line=47&end_line=50

import Base
import stelliferous@0.0.2.0/kernel_tile.bend as Tile
import stelliferous@0.0.2.0/storage_allocation.bend as Allocation
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness
import stelliferous@0.0.2.0/proofs/storage_allocation_refinement.bend as AllocationLaws

def allocated(+depth: Nat) -> Witness.Witness(Tile.Tile8,depth,Allocation.array(~Tile.Tile8,depth,Tile.filled(0.0))):
  %Equal.sym(Array<Tile.Tile8>,Allocation.array(~Tile.Tile8,depth,Tile.filled(0.0)),Array.new(Tile.Tile8,depth,Tile.filled(0.0)),
    AllocationLaws.array_same(Tile.Tile8,depth,Tile.filled(0.0))) : Witness.Witness(Tile.Tile8,depth,_)
  Witness.fresh(Tile.Tile8,depth,Tile.filled(0.0))

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.new
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=Tile8
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=filled
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_allocation_refinement.bend&name=array_same
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=Witness
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=fresh
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/storage_allocation.bend&name=array