def last_of_run

stelliferous@0.0.2.0 · proofs/tensor_access_certificate.bend:32

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/traversal_witness.bend as TraversalWitness

32# A strided operation keeps its owners through each part of a run: the stride
33# steps, the state handed to the cursor, and the cursor step that ends the run.
34# The lemmas are generic in the two element steps and in the evidence that
35# each of them keeps.
36def last_of_run(~Element: Data,+depth: Nat,extent: Nat,stride: U32,rewind: U32,rest: Cursor.Depth1(),-input: Array<Element>,
37  -state: Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Stride>,
38  evidence: TraversalWitness.StateEvidence<Array<Element>,Element,Cursor.Stride,input,depth,state>) ->
39  TraversalWitness.StateEvidence<Array<Element>,Element,Cursor.Cursor,input,depth,Access.last_of_run(~Element,extent,stride,rewind,rest,state)>:
40  match evidence:
41    case TraversalWitness.StateEvidence{output,position,Cursor.Stride{address,step},equation,output_evidence}:
42      %Equal.sym(Traversal.State<&1,&1,Array<Element>,Array<Element>,Cursor.Stride>,state,Traversal.State{input,output,position,Cursor.Stride{address,step}},equation) :
43        TraversalWitness.StateEvidence<Array<Element>,Element,Cursor.Cursor,input,depth,Access.last_of_run(~Element,extent,stride,rewind,rest,_)>
44      TraversalWitness.StateEvidence{output,position,Cursor.Cursor{Cursor.Level{Cursor.Axis{extent,1n,stride,rewind},rest},address},{==},output_evidence}