~/bend-docscommunity

proofs/tensor_access_certificate.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend as Tensor_access_certificate

Discharge the reader premises for the actual tensor traversal kernels. Public operations use only the flat certificates returned at their boundary.

13 imports
import Base
import ../tensor_access.bend as Access
import ../tensor_view.bend as Views
import ../traversal_array.bend as Traversal
import ../traversal_loop.bend as Loop
import ../tensor_cursor.bend as Cursor
import ./tensor_cursor_witness.bend as CursorWitness
import ./traversal_visit_witness.bend as VisitWitness
import ./storage_certificate.bend as Certificate
import ./storage_tree_model.bend as Tree
import ./storage_witness.bend as Witness
import ./traversal_witness.bend as TraversalWitness
import ./traversal_certificate.bend as TraversalCertificate

Types

type CopyCall source · line 21 · raw

Data

type ScatterCall source · line 183 · raw

Data

type ReduceCall source · line 245 · raw

Data

type IndexedCall source · line 274 · raw

Data

type SweepCall source · line 356 · raw

@-Element:Data -> Data

Templates

template read_index source · line 17 · raw

@-Element:Data -> @-input:Array<Element> -> @context:Unit -> @index:U32 -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<Element, input> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<Element>, Element, input, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.read_index(Element, input, context, index)>

template copy_operation source · line 24 · raw

@-Element:Data -> @call:CopyCall -> @input:Array<Element> -> @output:Array<Element> -> Pair(Array<Element>, Array<Element>)

template combine_operation source · line 28 · raw

@-Element:Data -> @-operation:(@_:Element -> @_:Element -> Element) -> @call:CopyCall -> @input:Array<Element> -> @output:Array<Element> -> Pair(Array<Element>, Array<Element>)

template last_of_run source · line 36 · raw

@-Element:Data -> @+depth:Nat -> @extent:Nat -> @stride:U32 -> @rewind:U32 -> @rest:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Depth1 -> @-input:Array<Element> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Stride> -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Stride, input, depth, state> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor, input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.last_of_run(Element, extent, stride, rewind, rest, state)>

A strided operation keeps its owners through each part of a run: the stride steps, the state handed to the cursor, and the cursor step that ends the run. The lemmas are generic in the two element steps and in the evidence that each of them keeps.

template Keeps source · line 47 · raw

@-Element:Data -> @-Context:Data -> @-step:(@_:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, Context> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, Context>) -> Type

A step keeps the evidence of its state.

template loop source · line 51 · raw

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

template run_axis source · line 61 · raw

@-Element:Data -> @-inside:(@_:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Stride> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Stride>) -> @-last:(@_:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor>) -> @-inside_keeps:Keeps(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Stride, inside) -> @-last_keeps:Keeps(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor, last) -> @+depth:Nat -> @remaining:Nat -> @extent:Nat -> @+stride:U32 -> @rewind:U32 -> @rest:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Depth1 -> @+address:U32 -> @-input:Array<Element> -> @-output:Array<Element> -> @position:U32 -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<Element, input> -> @output_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(Element, depth, output) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor, input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.run_axis(Element, inside, last, remaining, extent, stride, rewind, rest, address, input, output, position)>

template run_step source · line 80 · raw

@-Element:Data -> @-inside:(@_:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Stride> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Stride>) -> @-last:(@_:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor>) -> @-inside_keeps:Keeps(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Stride, inside) -> @-last_keeps:Keeps(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor, last) -> @+depth:Nat -> @-input:Array<Element> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor> -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<Element, input> -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor, input, depth, state> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor, input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.run_step(Element, inside, last, state)>

template run_loop source · line 93 · raw

@-Element:Data -> @-inside:(@_:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Stride> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Stride>) -> @-last:(@_:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor>) -> @-inside_keeps:Keeps(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Stride, inside) -> @-last_keeps:Keeps(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor, last) -> @+depth:Nat -> @count:Nat -> @-input:Array<Element> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor> -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<Element, input> -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor, input, depth, state> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor, input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run(0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.run_step(Element, inside, last), count, state)>

template last_loop source · line 105 · raw

@-Element:Data -> @-last:(@_:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor>) -> @-last_keeps:Keeps(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor, last) -> @+depth:Nat -> @count:Nat -> @-input:Array<Element> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor> -> @+input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<Element, input> -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor, input, depth, state> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor, input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run(0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor>, last, count, state)>

template stepped source · line 112 · raw

@-Element:Data -> @-last:(@_:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor>) -> @-last_keeps:Keeps(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor, last) -> @+depth:Nat -> @count:Nat -> @cursor:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor -> @destination:U32 -> @-input:Array<Element> -> @-output:Array<Element> -> @input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<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/traversal_array.finish(Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run(0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor>, last, count, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State{input, output, destination, cursor}))>

template guarded source · line 124 · raw

@-Element:Data -> @-inside:(@_:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Stride> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Stride>) -> @-last:(@_:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor>) -> @-inside_keeps:Keeps(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Stride, inside) -> @-last_keeps:Keeps(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor, last) -> @+depth:Nat -> @full_run:Bool -> @whole_runs:Bool -> @runs:Nat -> @count:Nat -> @cursor:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor -> @destination:U32 -> @-input:Array<Element> -> @-output:Array<Element> -> @input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<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_access.run_guarded(Element, inside, last, full_run, whole_runs, runs, count, cursor, destination, input, output)>

template remaining_run source · line 139 · raw

@-Element:Data -> @-inside:(@_:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Stride> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Stride>) -> @-last:(@_:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor>) -> @-inside_keeps:Keeps(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Stride, inside) -> @-last_keeps:Keeps(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor, last) -> @+depth:Nat -> @remaining:Nat -> @+extent:Nat -> @stride:U32 -> @rewind:U32 -> @rest:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Depth1 -> @address:U32 -> @+count:Nat -> @destination:U32 -> @-input:Array<Element> -> @-output:Array<Element> -> @input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<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_access.run_remaining(Element, inside, last, remaining, extent, stride, rewind, rest, address, count, destination, input, output)>

template strided source · line 153 · raw

@-Element:Data -> @-inside:(@_:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Stride> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Stride>) -> @-last:(@_:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor>) -> @-inside_keeps:Keeps(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Stride, inside) -> @-last_keeps:Keeps(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor, last) -> @+depth:Nat -> @count:Nat -> @cursor:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor -> @destination:U32 -> @-input:Array<Element> -> @-output:Array<Element> -> @input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<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_access.run_strided(Element, inside, last, count, cursor, destination, input, output)>

template copied_strided source · line 163 · raw

@-Element:Data -> @+depth:Nat -> @count:Nat -> @cursor:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor -> @destination:U32 -> @-input:Array<Element> -> @-output:Array<Element> -> @input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<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_access.copy_strided(Element, count, cursor, destination, input, output)>

template updated_strided source · line 173 · raw

@-Element:Data -> @-operation:(@_:Element -> @_:Element -> Element) -> @+depth:Nat -> @count:Nat -> @cursor:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor -> @destination:U32 -> @-input:Array<Element> -> @-output:Array<Element> -> @input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<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_access.update_strided(Element, operation, count, cursor, destination, input, output)>

template scatter_operation source · line 186 · raw

@-Element:Data -> @call:ScatterCall -> @input:Array<Element> -> @output:Array<Element> -> Pair(Array<Element>, Array<Element>)

template scattered source · line 190 · raw

@-Element:Data -> @+depth:Nat -> @call:ScatterCall -> @-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, scatter_operation(Element, call, input, output)>

template copied source · line 199 · raw

@-Element:Data -> @+depth:Nat -> @call:CopyCall -> @-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, copy_operation(Element, call, input, output)>

template combined source · line 211 · raw

@-Element:Data -> @-operation:(@_:Element -> @_:Element -> Element) -> @+depth:Nat -> @call:CopyCall -> @-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, combine_operation(Element, operation, call, input, output)>

template copy source · line 224 · raw

@-Element:Data -> @fast:Bool -> @count:Nat -> @source:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> @destination:U32 -> @-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_access.copy_run(Element, fast, count, source, destination, input, output)>

template scatter source · line 231 · raw

@-Element:Data -> @count:Nat -> @target:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> @source:U32 -> @-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_access.scatter_run(Element, count, target, source, input, output)>

template combine source · line 238 · raw

@-Element:Data -> @-operation:(@_:Element -> @_:Element -> Element) -> @fast:Bool -> @count:Nat -> @source:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> @destination:U32 -> @-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_access.combine_run(Element, operation, fast, count, source, destination, input, output)>

template reduce_operation source · line 248 · raw

@-Element:Data -> @-Accumulator:Data -> @-operation:(@_:Accumulator -> @_:Element -> Accumulator) -> @call:ReduceCall -> @storage:Array<Element> -> @initial:Accumulator -> Pair(Array<Element>, Accumulator)

template reduced source · line 253 · raw

@-Element:Data -> @-Accumulator:Data -> @-operation:(@_:Accumulator -> @_:Element -> Accumulator) -> @call:ReduceCall -> @-storage:Array<Element> -> @-initial:Accumulator -> @certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<Element, storage> -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.first(Array<Element>, Accumulator, reduce_operation(Element, Accumulator, operation, call, storage, initial)) == storage : Array<Element>}

template reduce source · line 267 · raw

@-Element:Data -> @-Accumulator:Data -> @-operation:(@_:Accumulator -> @_:Element -> Accumulator) -> @fast:Bool -> @count:Nat -> @view:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> @-storage:Array<Element> -> @-initial:Accumulator -> @certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<Element, storage> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.first(Array<Element>, Accumulator, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.reduce_run(Element, Accumulator, operation, fast, count, view, storage, initial))>

template indexed_operation source · line 277 · raw

@-Element:Data -> @-operation:(@_:U32 -> @_:Element -> Element) -> @call:IndexedCall -> @input:Array<Element> -> @output:Array<Element> -> Pair(Array<Element>, Array<Element>)

template indexed_sample source · line 282 · raw

@-Element:Data -> @-operation:(@_:U32 -> @_:Element -> Element) -> @-storage:Array<Element> -> @+position:U32 -> @-result:Pair(Array<Element>, Element) -> @sample:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<Element>, Element, storage, result> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<Element>, Element, storage, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.indexed_value(Element, operation, position, result)>

template indexed_read source · line 291 · raw

@-Element:Data -> @-operation:(@_:U32 -> @_:Element -> Element) -> @-storage:Array<Element> -> @context:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Offsets -> @index:U32 -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<Element, storage> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<Element>, Element, storage, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.read_indexed(Element, operation, storage, context, index)>

template indexed source · line 298 · raw

@-Element:Data -> @-operation:(@_:U32 -> @_:Element -> Element) -> @+depth:Nat -> @call:IndexedCall -> @-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, indexed_operation(Element, operation, call, input, output)>

template apply_indexed source · line 309 · raw

@-Element:Data -> @-operation:(@_:U32 -> @_:Element -> Element) -> @count:Nat -> @view:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.View -> @-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_access.apply_indexed_run(Element, operation, count, view, input, output)>

template window_read_sample source · line 316 · raw

@-Element:Data -> @+pad:Element -> @valid:Bool -> @-input:Array<Element> -> @+index:U32 -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<Element, input> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<Element>, Element, input, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.window_read(Element, pad, valid, input, index)>

template read_line_sample source · line 325 · raw

@-Element:Data -> @-input:Array<Element> -> @line:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.Line<Element> -> @position:U32 -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<Element, input> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<Element>, Element, input, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.read_line(Element, input, line, position)>

The one-axis window reduction: every sample is an element of the input or the pad, so the sweep returns its input and writes only its output.

template line_sample source · line 332 · raw

@-Element:Data -> @-input:Array<Element> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &2, Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.Line<Element>> -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.FoldEvidence<Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.Line<Element>, input, state> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<Element>, Element, input, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.finish_fold(Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.Line<Element>, state)>

template swept_sample source · line 342 · raw

@-Element:Data -> @-operation:(@_:Element -> @_:Element -> Element) -> @-input:Array<Element> -> @context:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.SweepContext<Element> -> @position:U32 -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<Element, input> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Array<Element>, Element, input, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.read_swept(Element, operation, input, context, position)>

template sweep_operation source · line 359 · raw

@-Element:Data -> @-operation:(@_:Element -> @_:Element -> Element) -> @call:SweepCall<Element> -> @input:Array<Element> -> @output:Array<Element> -> Pair(Array<Element>, Array<Element>)

template swept source · line 364 · raw

@-Element:Data -> @-operation:(@_:Element -> @_:Element -> Element) -> @+depth:Nat -> @call:SweepCall<Element> -> @-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, sweep_operation(Element, operation, call, input, output)>

template sweep source · line 376 · raw

@-Element:Data -> @-operation:(@_:Element -> @_:Element -> Element) -> @count:Nat -> @context:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.SweepContext<Element> -> @-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_access.sweep_run(Element, operation, count, context, input, output)>