def run_axis

stelliferous@0.0.2.0 · proofs/tensor_access_certificate.bend:61

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/traversal_loop.bend as Loop
import stelliferous@0.0.2.0/tensor_cursor.bend as Cursor
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness

61def run_axis(~Element: Data,~inside: Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Stride> -> Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Stride>,~last: Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor> -> Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Cursor>,
62  ~inside_keeps: Keeps(~Element,~Cursor.Stride,~inside),
63  ~last_keeps: Keeps(~Element,~Cursor.Cursor,~last),
64  +depth: Nat,remaining: Nat,extent: Nat,+stride: U32,rewind: U32,rest: Cursor.Depth1(),+address: U32,
65  -input: Array<Element>,-output: Array<Element>,position: U32,+input_evidence: Witness.ArrayWitness<Element,input>,
66  output_evidence: Witness.Witness(Element,depth,output)) ->
67  TraversalWitness.StateEvidence<Array<Element>,Element,Cursor.Cursor,input,depth,Access.run_axis(~Element,~inside,~last,remaining,extent,stride,rewind,rest,address,input,output,position)>:
68  match remaining:
69    case 0n:
70      last_keeps(depth,input,Traversal.State{input,output,position,Cursor.Cursor{Cursor.Level{Cursor.Axis{extent,0n,stride,rewind},rest},address}},input_evidence,
71        TraversalWitness.StateEvidence{output,position,Cursor.Cursor{Cursor.Level{Cursor.Axis{extent,0n,stride,rewind},rest},address},{==},output_evidence})
72    case 1n+count:
73      last_keeps(depth,input,
74        Access.last_of_run(~Element,extent,stride,rewind,rest,Loop.run(~Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Stride>,~inside,count,Traversal.State{input,output,position,Cursor.Stride{address,stride}})),
75        input_evidence,
76        last_of_run(~Element,depth,extent,stride,rewind,rest,input,Loop.run(~Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Stride>,~inside,count,Traversal.State{input,output,position,Cursor.Stride{address,stride}}),
77          loop(~Element,~Cursor.Stride,~inside,~inside_keeps,depth,count,input,Traversal.State{input,output,position,Cursor.Stride{address,stride}},input_evidence,
78            TraversalWitness.StateEvidence{output,position,Cursor.Stride{address,stride},{==},output_evidence})))