Comment by dselsam

Yes, this is easy to express in a prover. A naive implementation can always serve as a specification for a sophisticated one.