Those are implementation details. As I understand the OP, the concern is that it is difficult / infeasible to interrogate the real protocol of the statement being proven, so to speak.
In a language like Circom, the program being output has a witness generator, and a constraint