Module Composition_types.Wrap

module Proof_state : sig ... end
module Messages_for_next_step_proof : sig ... end

The component of the proof accumulation state that is only computed on by the "stepping" proof system, and that can be handled opaquely by any "wrap" circuits.

module Lookup_parameters : sig ... end
module Statement : sig ... end

This is the full statement for "wrap" proofs which contains