refactor assert_satisfied_full

[zemse]

• uses MockProver utils inside assert_satisfied_full which enables additional missing checks for things like assert zero expressions.
• removes duplicate code to check of multiplicity
• enables MockProver to check for multiplicity of all instances (previously only instance 0 was considered)

[matthiasgoergens]

The other possibility is GoldilocksExt2?

[zemse]

LkMultiplicity's key previously was just u64. From the e2e witness we also get case where we want key as GoldilocksExt2. To enable reuse of the same code in MockProver, the trait LkMultiplicityKey helps.

[matthiasgoergens]

Please see #793 for most of the suggestions that are also in the comments.

[matthiasgoergens]

Suggested change

	format!("Element: {a} < {b}")
	format!("Element: {a} && {b}")

[matthiasgoergens]

That seems pretty hacky?

[zemse]

count is recorded to print errors in the following fashion:

# when you have Uint::new in construct while Value::new_unchecked in assign
LkMultiplicityError:
2 Lookups of U16 missing in assignments
Element: 0

# when you have Uint::new_unchecked in construct while Value::new in assign
LkMultiplicityError:
2 Lookups of U16 missing in constraint system
Element: 0

But I agree this could be more self explaining. Instead of count being a signed int, it could be an enum, something like-

enum LkMultiplicityErrorCount {
    MissingInAssignments(u64),
    MissingInConstraintSystem(u64),
}

[matthiasgoergens]

Yes. Perhaps something for the next PR?

[matthiasgoergens]

Looks like we use count in a pretty hacky way?

[matthiasgoergens]

If panic_on_error is set, we should probably put the full error message into the panic message? (In that case, we don't need to println the error message, just put it in the panic only.)

[zemse]

Sometimes the errors can be a lot and it can go beyond the terminal lines limit (if it's set low) and the following default rust panic stderr line would not be easily visible or lost.

thread 'main' panicked at /Users/.../mock_prover.rs:919:9:

That's why the panic message was purposefully kept short summary so that when program terminates, it can be obvious it was a panic and at which line, and dev can look at logs before to learn more details about what caused "(Unexpected) Constraints not satisfied".

But if it doesn't seem helpful, for better code we can put everything in panic.

[matthiasgoergens]

This seems all too complicated, but let me think a bit more about it. (We can merge first.)

[zemse]

@matthiasgoergens Thanks for review and suggestion PR!

[hero78119]

LGTM now 👍
In summary

• in assert_satisfied_raw, each opcode we extract raw value from rlc expression and checked with expected lookup multiplicity
• in assert_satisfied_full, the lookup value was in rlc format and so as table, and do rlc to rlc comparison.

some lefted TODO after this PR

• have better naming on assert_satisfied_raw and assert_satisfied_full. E.g. assert_satisfied_full -> assert_satisfied_zkvm
• retain this debug message

  ceno/ceno_zkvm/src/scheme/mock_prover.rs

  Lines 900 to 930 in 1d7818e

  	// log mismatch error
  	let witness = wit_mles
  	.get(&circuit_name)
  	.map(|mles| {
  	mles.iter()
  	.map(|mle| E::from(mle.get_base_field_vec()[row as usize]))
  	.collect_vec()
  	})
  	.unwrap();
  	let values = input_value_exprs
  	.iter()
  	.map(|expr| {
  	eval_by_expr_with_instance(
  	&[],
  	&witness,
  	&[],
  	&instance,
  	challenges.as_slice(),
  	expr,
  	)
  	.as_bases()[0]
  	})
  	.collect_vec();
  	tracing::error!(
  	"{}: value {:x?} mismatch lk_multiplicity: real {:x} > remaining {:x} in {:?} table",
  	lk_input_annotation,
  	values,
  	input_multiplicity,
  	table_multiplicity,
  	rom_type,
  	);

  => this break down raw value is very useful, e.g. once program table lookup failed we can quickly targeting on the opcode.