~/bend-docscommunity

proofs/tensor_cursor_witness.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/tensor_cursor_witness.bend as Tensor_cursor_witness

6 imports
import Base
import ../tensor_cursor.bend as Cursor
import ../traversal_array.bend as Traversal
import ./storage_witness.bend as Witness
import ./traversal_witness.bend as TraversalWitness
import ./traversal_visit_witness.bend as VisitWitness

Templates

template read_value source · line 8 · raw

@-Element:Data -> @axes:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Levels -> @address:U32 -> @-storage:Array<Element> -> @-result:Pair(Array<Element>, Element) -> @observed:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Read<Element, storage, result> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_visit_witness.Sample<Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor, storage, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.read_value(Element, axes, address, result)>

template read source · line 17 · raw

@-Element:Data -> @-storage:Array<Element> -> @cursor:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<Element, storage> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_visit_witness.Sample<Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Cursor, storage, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.read(Element, storage, cursor)>

template stride_value source · line 22 · raw

@-Element:Data -> @address:U32 -> @+stride:U32 -> @-storage:Array<Element> -> @-result:Pair(Array<Element>, Element) -> @observed:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Read<Element, storage, result> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_visit_witness.Sample<Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Stride, storage, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.stride_value(Element, address, stride, result)>

template read_stride source · line 31 · raw

@-Element:Data -> @-storage:Array<Element> -> @cursor:0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Stride -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<Element, storage> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_visit_witness.Sample<Array<Element>, Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.Stride, storage, 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.read_stride(Element, storage, cursor)>