TensorAccessCertificate.run_axis: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend as TensorAccessCertificate
Lines 61-78 of stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend&start_line=61&end_line=78

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

def 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>,
  ~inside_keeps: Keeps(~Element,~Cursor.Stride,~inside),
  ~last_keeps: Keeps(~Element,~Cursor.Cursor,~last),
  +depth: Nat,remaining: Nat,extent: Nat,+stride: U32,rewind: U32,rest: Cursor.Depth1(),+address: U32,
  -input: Array<Element>,-output: Array<Element>,position: U32,+input_evidence: Witness.ArrayWitness<Element,input>,
  output_evidence: Witness.Witness(Element,depth,output)) ->
  TraversalWitness.StateEvidence<Array<Element>,Element,Cursor.Cursor,input,depth,Access.run_axis(~Element,~inside,~last,remaining,extent,stride,rewind,rest,address,input,output,position)>:
  match remaining:
    case 0n:
      last_keeps(depth,input,Traversal.State{input,output,position,Cursor.Cursor{Cursor.Level{Cursor.Axis{extent,0n,stride,rewind},rest},address}},input_evidence,
        TraversalWitness.StateEvidence{output,position,Cursor.Cursor{Cursor.Level{Cursor.Axis{extent,0n,stride,rewind},rest},address},{==},output_evidence})
    case 1n+count:
      last_keeps(depth,input,
        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}})),
        input_evidence,
        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}}),
          loop(~Element,~Cursor.Stride,~inside,~inside_keeps,depth,count,input,Traversal.State{input,output,position,Cursor.Stride{address,stride}},input_evidence,
            TraversalWitness.StateEvidence{output,position,Cursor.Stride{address,stride},{==},output_evidence})))

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=ArrayWitness
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=Witness
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend&name=Keeps
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend&name=last_of_run
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend&name=loop
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_witness.bend&name=StateEvidence
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_access.bend&name=last_of_run
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_access.bend&name=run_axis
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_cursor.bend&name=Axis
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_cursor.bend&name=Cursor
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_cursor.bend&name=Depth1
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_cursor.bend&name=Level
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_cursor.bend&name=Stride
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_array.bend&name=State
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_loop.bend&name=run