def copied_strided

stelliferous@0.0.2.0 · proofs/tensor_access_certificate.bend:163

import Base
import stelliferous@0.0.2.0/tensor_access.bend as Access
import stelliferous@0.0.2.0/traversal_array.bend as Traversal
import stelliferous@0.0.2.0/tensor_cursor.bend as Cursor
import stelliferous@0.0.2.0/proofs/tensor_cursor_witness.bend as CursorWitness
import stelliferous@0.0.2.0/proofs/traversal_visit_witness.bend as VisitWitness
import stelliferous@0.0.2.0/proofs/storage_certificate.bend as Certificate
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness

163def copied_strided(~Element: Data,+depth: Nat,count: Nat,cursor: Cursor.Cursor,destination: U32,-input: Array<Element>,-output: Array<Element>,
164  input_evidence: Witness.ArrayWitness<Element,input>,
165  equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>}) ->
166  TraversalWitness.ResultEvidence<Array<Element>,Element,input,depth,Access.copy_strided(~Element,count,cursor,destination,input,output)>:
167  strided(~Element,~Traversal.visit_step(~Array<Element>,~Element,~Cursor.Stride,~Cursor.read_stride(~Element)),
168    ~Traversal.visit_step(~Array<Element>,~Element,~Cursor.Cursor,~Cursor.read(~Element)),
169    ~VisitWitness.step(~Array<Element>,~Element,~Cursor.Stride,~TraversalWitness.array_evidence(~Element),~Cursor.read_stride(~Element),~CursorWitness.read_stride(~Element)),
170    ~VisitWitness.step(~Array<Element>,~Element,~Cursor.Cursor,~TraversalWitness.array_evidence(~Element),~Cursor.read(~Element),~CursorWitness.read(~Element)),
171    depth,count,cursor,destination,input,output,input_evidence,equation)