def spread_step

stelliferous@0.0.2.0 · proofs/traversal_visit_witness.bend:41

import Base
import stelliferous@0.0.2.0/traversal_array.bend as Traversal
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness

41def spread_step(~Element: Data,~Context: Data,~target: Context -> Traversal.Target<Context>,
42  +depth: Nat,-input: Array<Element>,-state: Traversal.State<&1,&1,Array<Element>,Array<Element>,Context>,input_evidence: Witness.ArrayWitness<Element,input>,
43  evidence: TraversalWitness.StateEvidence<Array<Element>,Element,Context,input,depth,state>) ->
44  TraversalWitness.StateEvidence<Array<Element>,Element,Context,input,depth,Traversal.spread_step(~Element,~Context,~target,state)>:
45  match evidence:
46    case TraversalWitness.StateEvidence{output,+position,context,equation,output_evidence}:
47      %Equal.sym(Traversal.State<&1,&1,Array<Element>,Array<Element>,Context>,state,Traversal.State{input,output,position,context},equation) :
48        TraversalWitness.StateEvidence<Array<Element>,Element,Context,input,depth,Traversal.spread_step(~Element,~Context,~target,_)>
49      spread_store(~Element,~Context,depth,input,position,output,target(context),Array.get(Element,input,position),output_evidence,
50        Witness.observed(Element,input,position,input_evidence))