Encoded-circuit proof internals

Aggregation module for the codec, appendable-fragment laws, semantics, and raw-to-typed reconstruction internals of the canonical fan-in-two circuit encoding.