refactor(lifted-stark): replace bus-identity reduction with general eval_external + flat external_public_inputs

[adr1anh]

Summary

Generalizes the cross-AIR bus-identity check (ReducedAuxValues { prod, sum }) into per-AIR external assertions, and simplifies the variable-length public-input plumbing into a flat &[F] slice that the AIR decodes itself.

Motivation

The previous design baked two assumptions into the trait surface:

1. External assertions had a fixed shape — every AIR's contribution had to be a (product, sum) pair representing a multiset/logup bus identity. This is fine for those bus shapes but doesn't generalize to other assertions over aux values + challenges + public inputs.
2. Variable-length public inputs were a list of fixed-width matrices — the framework declared widths up front via num_var_len_public_inputs() and validated them on every instance. This was extra plumbing for callers without buying flexibility: AIRs that wanted heterogeneous inputs (length-prefixed sublists, scalar headers, etc.) couldn't express them.

Both pieces are folded into a single, narrower contract: the AIR returns a vector of scalar assertions and decodes its inputs from a flat slice.

API changes

LiftedAir

Before	After
fn reduced_aux_values(...) -> Result<ReducedAuxValues<EF>, ReductionError>	fn eval_external(...) -> Result<Vec<EF>, ReductionError>
fn num_var_len_public_inputs() -> usize	(removed; AIR owns its own schema)

eval_external returns a list of extension-field values that must each equal zero. The verifier checks them individually (no Horner/alpha fold) so a non-zero entry is reported with its caller-original instance index and assertion position:

VerifierError::ExternalAssertionFailed { caller_instance, assertion }

Instance / witness types

Before	After
var_len_public_inputs: &[&[F]]	external_public_inputs: &[F]

AirInstance, AirWitness, prove_single, and verify_single now take a flat slice. The AIR is responsible for any decode/length checks and reports failures via ReductionError.

Removed

• ReducedAuxValues<EF> type and the auxiliary/values.rs module
• InstanceValidationError::VarLenPublicInputsMismatch
• InstanceValidationError::VarLenPublicInputWidthMismatch
• Matrix-width validation block in instance::validate_inputs and debug::check_constraints_multi
• VerifierError::InvalidReducedAux

Fiat-Shamir

Caller absorption simplifies to a single line:

ch.observe_slice(public_values);
ch.observe_slice(external_public_inputs);  // was a per-matrix loop

Both prover and verifier MUST absorb the same slice.

AIR migration

For an AIR that previously did:

fn reduced_aux_values(&self, aux, ch, pv, var_len) -> Result<ReducedAuxValues<EF>, _> {
    let pi_0 = QuadFelt::from(var_len[0][0]);
    let pi_1 = QuadFelt::from(var_len[1][0]);
    Ok(ReducedAuxValues {
        prod: aux[0] * (ch[0] + pi_0),
        sum: (aux[1] - ch[1]) - pi_1,
    })
}

The equivalent now is:

fn eval_external(&self, aux, ch, pv, external) -> Result<Vec<EF>, _> {
    let mut it = external.iter().copied();
    let pi_0 = QuadFelt::from(it.next().ok_or("missing pi_0")?);
    let pi_1 = QuadFelt::from(it.next().ok_or("missing pi_1")?);
    Ok(vec![
        aux[0] * (ch[0] + pi_0) - QuadFelt::ONE,         // multiset: prod == 1
        (aux[1] - ch[1]) - pi_1,                          // logup: sum == 0
    ])
}

Note the multiset assertion is rewritten to prod - 1 == 0 (each entry is its own zero-equation; there's no separate "identity" form anymore).

Test plan

• cargo test -p miden-lifted-stark --lib — 73/73 pass, including:
  • bus_identity_check (positive case)
  • bus_wrong_external_pi_fails (mismatched value → ExternalAssertionFailed)
  • bus_short_external_inputs_fails (truncated input → Reduction(_) from the AIR's decoder)
• cargo clippy -p miden-lifted-air -p miden-lifted-stark -p miden-bench --all-targets clean
• cargo check clean across all three affected crates

Notes for reviewers

• Soundness: per-assertion zero-check is equivalent to a Horner fold over concrete EF values. The fold was bookkeeping, not adding any cryptographic guarantee.
• The framework no longer cross-checks shape against the AIR for external_public_inputs. If the caller and AIR disagree on encoding, the AIR's decoder fails (returning ReductionError), which yields VerifierError::Reduction(_) rather than a panic.

[adr1anh]

We should relax the bounds to allow symbolic representation of these constraints.

[adr1anh]

This could be replaced by has_external_inputs, in which case the eval_external function is a constant circuit.