def tiled_preserves

stelliferous@0.0.2.0 · proofs/tensor_indexed_certificate.bend:102

import Base
import stelliferous@0.0.2.0/tensor_indexed.bend as Indexed
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
import stelliferous@0.0.2.0/proofs/storage_certificate.bend as Certificate
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness

102def tiled_preserves(~Element: Data,~Context: Data,~index: Context -> U32 -> U32,~base: Context -> U32 -> U32,~blocks: Context -> U32,~size: Context -> U32,~operation: U32 -> Element -> Element,
103  +depth: Nat,tiling: Tiling<Context>,-input: Array<Element>,-output: Array<Element>,input_certificate: Certificate.Certificate<Element,input>,
104  equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>}) ->
105  TraversalWitness.ResultEvidence<Array<Element>,Element,input,depth,tiled_operation(~Element,~Context,~index,~base,~blocks,~size,~operation,tiling,input,output)>:
106  Tiling{+total,+context} = tiling
107  whole_preserves(~Element,~Context,~index,~base,~operation,depth,U32.is_le(total,Indexed.block_limit()) && Nat.is_eq(Nat.mul(U32.to_nat(blocks(context)),U32.to_nat(size(context))),U32.to_nat(total)),
108    blocks(context),size(context),total,context,input,output,input_certificate,equation)