Method circuit

crates/aiur/src/vk_codec.rs:163–173

(&mut self, c: &Circuit<AiurCircuit>)

/// and `lookup_prefix_len` (= 1 + max node id reachable from the lookups)
/// are all recomputed on decode, and the Lean reader derives the observed
/// shape limbs the same way.
fn encode_circuit(buf: &mut Vec<u8>, circuit: &Circuit<Val>) {
  let compiled = &circuit.graph;
  push_u16(buf, circuit.main_width);
  push_u16(buf, circuit.preprocessed_width);
  // u32: the Bytes2 table height is exactly 65536.
  push_u32(buf, circuit.preprocessed_height);
  // Combined max degree (user graph + analytic logUp), as observed. Not
  // derivable cheaply in-circuit (it would need a full degree pass).
  push_u16(buf, circuit.max_constraint_degree);
  // The lookup group size is a free per-circuit choice (it changes the
  // constraint structure, not just counts), so it must be serialized.
  buf
    .push(u8::try_from(circuit.lookup_group_size).expect("group size fits u8"));