Structure::is_sat does not validate witness lengths, and test_sat does not exercise the eq weights

neutron::relation::Structure::is_sat performs no length validation on the
witness it is handed, and NeutronSNARK::verify calls it on a FoldedWitness
that arrives through Deserialize. A running witness with a short E is an
out-of-bounds index rather than a rejected proof.

I know the module header says the code "currently lacks certain checks, so do
not use this until the experimental feature is removed" — this is one specific
instance, and it comes with a second observation about test_sat that seemed
more useful than the bug itself.

The panic

Popping one element from the running witness's E in an otherwise valid
one-step IVC proof, then calling verify:

thread '<unnamed>' panicked at src/neutron/relation.rs:87:37:
index out of bounds: the len is 63 but the index is 63

W.E.split_at(self.left) leaves the right half one short, and the tensor loop
then indexes E2[i] over 0..self.right.

This is the Neutron sibling of the R1CS case in #399, which I have opened a PR
for on the Nova path.

The fix looks trivial, and then it isn't

The obvious check is

if W.W.len() != self.S.num_vars || W.E.len() != self.left + self.right {
  return Err(NovaError::InvalidWitnessLength);
}

left + right is what FoldedWitness::default produces and what
nifs::NIFS::fold's own sanity checks assert:

src/neutron/nifs.rs:42   assert_eq!(e1.len(), left + right);
src/neutron/nifs.rs:46   assert_eq!(e2.len(), left + right);

But adding it fails the existing relation::tests::test_sat, which builds

let E = EqPolynomial::new(coords).evals();   // length 2^ell = left * right

i.e. the full eq-polynomial evaluations rather than the tensor form. With
num_cons = 16 that is 16 entries where the folding code asserts 8.

test_sat passes today for a reason worth noting: the satisfiability sum is
Σ eₖ · (aₖbₖ − cₖ), and for a satisfying witness every aₖbₖ − cₖ is zero, so
the weights never affect the result. Any E of length ≥ left + right passes,
with any values. The test therefore does not exercise the eq weights at all —
which also means it would not catch a genuine error in the tensor
decomposition.

What I'd need from you

Which length is canonical for FoldedWitness::E — the tensor form
(left + right, per nifs.rs and default), or the full evaluations
(left * right, per test_sat)?

If it is the tensor form, then the fix above is right and test_sat should
build E as two halves. I did not write that patch because the correct
construction depends on which half of coords maps to the i index and which
to j in full_E[i * left + j] = E2[i] * E1[j], and test_sat's assertion is
insensitive to getting that backwards — so I would have been writing a test I
could not verify. That ordering is a question for whoever wrote the scheme.

Happy to send the patch once the invariant is settled.

Start with src/neutron/relation.rs, src/neutron/nifs.rs, FoldedWitness::default, and relation::tests::test_sat. Determine from the folding scheme whether E uses tensor length left + right and which coordinate maps to each half. Done means malformed witnesses are rejected without panicking and test_sat constructs weights that genuinely exercise the tensor decomposition.