~/jendhub

def allocated

stelliferous@0.0.2.0 · proofs/kernel_weights_certificate.bend:47

import stelliferous@0.0.2.0/proofs/kernel_weights_certificate.bend as KernelWeightsCertificate
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

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

Uses (10)

Used by (1)