def block_step

stelliferous@0.0.2.0 · proofs/tensor_indexed_certificate.bend:57

import Base
import stelliferous@0.0.2.0/tensor_indexed.bend as Indexed
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

57def block_step(~Element: Data,~Context: Data,~base: Context -> U32 -> U32,~operation: U32 -> Element -> Element,+depth: Nat,-input: Array<Element>,-state: Traversal.State<&1,&1,Array<Element>,Array<Element>,Indexed.Blocks<Context>>,
58  +input_evidence: Witness.ArrayWitness<Element,input>,evidence: TraversalWitness.StateEvidence<Array<Element>,Element,Indexed.Blocks<Context>,input,depth,state>) ->
59  TraversalWitness.StateEvidence<Array<Element>,Element,Indexed.Blocks<Context>,input,depth,Indexed.block_step(~Element,~Context,~base,~operation,state)>:
60  match evidence:
61    case TraversalWitness.StateEvidence{output,+position,Indexed.Blocks{+block,+size,+context},equation,output_evidence}:
62      %Equal.sym(Traversal.State<&1,&1,Array<Element>,Array<Element>,Indexed.Blocks<Context>>,state,Traversal.State{input,output,position,Indexed.Blocks{block,size,context}},equation) :
63        TraversalWitness.StateEvidence<Array<Element>,Element,Indexed.Blocks<Context>,input,depth,Indexed.block_step(~Element,~Context,~base,~operation,_)>
64      next_block(~Element,~Context,depth,block,size,context,input,
65        Traversal.run(~Array<Element>,~Element,~Indexed.Block,~Indexed.read(~Element,~Indexed.Block,~Indexed.block_index,~operation),~Indexed.destination(~Indexed.Block),U32.to_nat(size),
66          Traversal.State{input,output,position,Indexed.Block{base(context,block),position}}),
67        TraversalWitness.run(~Array<Element>,~Element,~Indexed.Block,~TraversalWitness.array_evidence(~Element),~Indexed.read(~Element,~Indexed.Block,~Indexed.block_index,~operation),
68          ~Indexed.destination(~Indexed.Block),~read(~Element,~Indexed.Block,~Indexed.block_index,~operation),depth,U32.to_nat(size),input,
69          Traversal.State{input,output,position,Indexed.Block{base(context,block),position}},input_evidence,
70          TraversalWitness.StateEvidence{output,position,Indexed.Block{base(context,block),position},{==},output_evidence}))