def updated_strided

stelliferous@0.0.2.0 · proofs/tensor_access_certificate.bend:173

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

173def updated_strided(~Element: Data,~operation: Element -> Element -> Element,+depth: Nat,count: Nat,cursor: Cursor.Cursor,destination: U32,
174  -input: Array<Element>,-output: Array<Element>,input_evidence: Witness.ArrayWitness<Element,input>,
175  equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>}) ->
176  TraversalWitness.ResultEvidence<Array<Element>,Element,input,depth,Access.update_strided(~Element,~operation,count,cursor,destination,input,output)>:
177  strided(~Element,~Traversal.visit_update_step(~Array<Element>,~Element,~Cursor.Stride,~Cursor.read_stride(~Element),~operation),
178    ~Traversal.visit_update_step(~Array<Element>,~Element,~Cursor.Cursor,~Cursor.read(~Element),~operation),
179    ~VisitWitness.update_step(~Array<Element>,~Element,~Cursor.Stride,~TraversalWitness.array_evidence(~Element),~Cursor.read_stride(~Element),~operation,~CursorWitness.read_stride(~Element)),
180    ~VisitWitness.update_step(~Array<Element>,~Element,~Cursor.Cursor,~TraversalWitness.array_evidence(~Element),~Cursor.read(~Element),~operation,~CursorWitness.read(~Element)),
181    depth,count,cursor,destination,input,output,input_evidence,equation)