def store

stelliferous@0.0.2.0 · proofs/traversal_visit_witness.bend:11

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

11def store(~Reader: Type,~Element: Data,~Context: Data,+depth: Nat,-reader: Reader,+position: U32,-output: Array<Element>,
12  -result: Reader & Traversal.Visited<Context,Element>,output_evidence: Witness.Witness(Element,depth,output),sample: Sample<Reader,Element,Context,reader,result>) ->
13  TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,Traversal.visit_store(~Reader,~Element,~Context,position,output,result)>:
14  match sample:
15    case Sample{context,value,equation}:
16      %Equal.sym(Reader & Traversal.Visited<Context,Element>,result,(reader,Traversal.Visited{context,value}),equation) :
17        TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,Traversal.visit_store(~Reader,~Element,~Context,position,output,_)>
18      TraversalWitness.StateEvidence{Array.set(Element,output,position,value),(position + 1 : U32),context,{==},Witness.write(Element,depth,output,position,value,output_evidence)}