proofs/tensor_indexed_certificate.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/tensor_indexed_certificate.bend as Tensor_indexed_certificate

9 imports

import Base
import ../tensor_indexed.bend as Indexed
import ../traversal_array.bend as Traversal
import ../traversal_loop.bend as Loop
import ./storage_tree_model.bend as Tree
import ./storage_certificate.bend as Certificate
import ./storage_witness.bend as Witness
import ./traversal_witness.bend as TraversalWitness
import ./traversal_certificate.bend as TraversalCertificate

Types

type Tiling source · line 82 · raw

@-Context:Data -> Data

Tiling

@-Context:Data -> @total:U32 -> @context:Context -> Tiling<Context>

Templates

template sample source · line 11 · raw

@-Element:Data -> @-Context:Data -> @-index:(@_:Context -> @_:U32 -> U32) -> @-operation:(@_:U32 -> @_:Element -> Element) -> @-input:Array<Element> -> @+context:Context -> @+position:U32 -> @-result:Pair(Array<Element>, Element) -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<Element>, Element, input, result> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<Element>, Element, input, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_indexed.value(Element, Context, index, operation, context, position, result)>

template read source · line 21 · raw

@-Element:Data -> @-Context:Data -> @-index:(@_:Context -> @_:U32 -> U32) -> @-operation:(@_:U32 -> @_:Element -> Element) -> @-input:Array<Element> -> @context:Context -> @position:U32 -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<Element, input> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<Element>, Element, input, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_indexed.read(Element, Context, index, operation, input, context, position)>

template preserves source · line 28 · raw

@-Element:Data -> @-Context:Data -> @-index:(@_:Context -> @_:U32 -> U32) -> @-operation:(@_:U32 -> @_:Element -> Element) -> @+depth:Nat -> @call:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_indexed.Call<Context> -> @-input:Array<Element> -> @-output:Array<Element> -> @input_certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<Element, input> -> @equation:{output == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.normalized(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, output))) : Array<Element>} -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.ResultEvidence<Array<Element>, Element, input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_indexed.run(Element, Context, index, operation, call, input, output)>

template certificates source · line 39 · raw

@-Element:Data -> @-Context:Data -> @-index:(@_:Context -> @_:U32 -> U32) -> @-operation:(@_:U32 -> @_:Element -> Element) -> @+call:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_indexed.Call<Context> -> @-input:Array<Element> -> @-output:Array<Element> -> @input_certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<Element, input> -> @output_certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<Element, output> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_certificate.Certificates<Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.family(Element), 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_indexed.run(Element, Context, index, operation, call, input, output)>

template next_block source · line 48 · raw

@-Element:Data -> @-Context:Data -> @+depth:Nat -> @block:U32 -> @size:U32 -> @context:Context -> @-input:Array<Element> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_indexed.Block> -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_indexed.Block, input, depth, state> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_indexed.Blocks<Context>, input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_indexed.next_block(Element, Context, block, size, context, state)>

template block_step source · line 57 · raw

@-Element:Data -> @-Context:Data -> @-base:(@_:Context -> @_:U32 -> U32) -> @-operation:(@_:U32 -> @_:Element -> Element) -> @+depth:Nat -> @-input:Array<Element> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_indexed.Blocks<Context>> -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<Element, input> -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_indexed.Blocks<Context>, input, depth, state> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_indexed.Blocks<Context>, input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_indexed.block_step(Element, Context, base, operation, state)>

template block_loop source · line 72 · raw

@-Element:Data -> @-Context:Data -> @-base:(@_:Context -> @_:U32 -> U32) -> @-operation:(@_:U32 -> @_:Element -> Element) -> @+depth:Nat -> @count:Nat -> @-input:Array<Element> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_indexed.Blocks<Context>> -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<Element, input> -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_indexed.Blocks<Context>, input, depth, state> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_indexed.Blocks<Context>, input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run(0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_indexed.Blocks<Context>>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_indexed.block_step(Element, Context, base, operation), count, state)>

template tiled_operation source · line 85 · raw

@-Element:Data -> @-Context:Data -> @-index:(@_:Context -> @_:U32 -> U32) -> @-base:(@_:Context -> @_:U32 -> U32) -> @-blocks:(@_:Context -> U32) -> @-size:(@_:Context -> U32) -> @-operation:(@_:U32 -> @_:Element -> Element) -> @tiling:Tiling<Context> -> @input:Array<Element> -> @output:Array<Element> -> Pair(Array<Element>, Array<Element>)

template whole_preserves source · line 90 · raw

@-Element:Data -> @-Context:Data -> @-index:(@_:Context -> @_:U32 -> U32) -> @-base:(@_:Context -> @_:U32 -> U32) -> @-operation:(@_:U32 -> @_:Element -> Element) -> @+depth:Nat -> @whole:Bool -> @blocks:U32 -> @size:U32 -> @total:U32 -> @context:Context -> @-input:Array<Element> -> @-output:Array<Element> -> @input_certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<Element, input> -> @equation:{output == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.normalized(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, output))) : Array<Element>} -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.ResultEvidence<Array<Element>, Element, input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_indexed.run_whole(Element, Context, index, base, operation, whole, blocks, size, total, context, input, output)>

template tiled_preserves source · line 102 · raw

@-Element:Data -> @-Context:Data -> @-index:(@_:Context -> @_:U32 -> U32) -> @-base:(@_:Context -> @_:U32 -> U32) -> @-blocks:(@_:Context -> U32) -> @-size:(@_:Context -> U32) -> @-operation:(@_:U32 -> @_:Element -> Element) -> @+depth:Nat -> @tiling:Tiling<Context> -> @-input:Array<Element> -> @-output:Array<Element> -> @input_certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<Element, input> -> @equation:{output == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.normalized(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, output))) : Array<Element>} -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.ResultEvidence<Array<Element>, Element, input, depth, tiled_operation(Element, Context, index, base, blocks, size, operation, tiling, input, output)>

template tiled_certificates source · line 110 · raw

@-Element:Data -> @-Context:Data -> @-index:(@_:Context -> @_:U32 -> U32) -> @-base:(@_:Context -> @_:U32 -> U32) -> @-blocks:(@_:Context -> U32) -> @-size:(@_:Context -> U32) -> @-operation:(@_:U32 -> @_:Element -> Element) -> @+total:U32 -> @+context:Context -> @-input:Array<Element> -> @-output:Array<Element> -> @input_certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<Element, input> -> @output_certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<Element, output> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_certificate.Certificates<Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.family(Element), 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_indexed.run_tiled(Element, Context, index, base, blocks, size, operation, total, context, input, output)>