use assert_satisfied_raw in assert_satisfied_full e2e tests

[zemse]

• replace a part of assert_satisfied_full code to use assert_satisfied_raw logic for performing constraints and multiplicity checks.

[hero78119]

This new design although idea is nice and capture lkm on row (per instance) level, however this design will bring quite lot of overhead because we will create #instance of lkm (probably 1 billion of row), comparing with original design we just create ~ #opcode + #table lkm which is roughly riscv opcode 38 + all tables, overall less than 50.

So I suggest we just rollback to single lkm version. In current assignment design, lkm check failed will imply on all row contributed to the failed, because we dont have per row conditional logic. With single lkm, we can still know which table failed, while retain the efficiency of the design

[hero78119]

this change seems unrelated and just optional, is it trigger any clippy warning?

[hero78119]

The logic to retrieve padding instance is somehow incorrect.

The correct way to retrieve number of padding row is via

ceno/ceno_zkvm/src/scheme/mock_prover.rs

Line 789 in cec7b82

let num_rows = witness.num_instances();

and

ceno/ceno_zkvm/src/scheme/mock_prover.rs

Line 829 in cec7b82

.get_ext_field_vec())[..num_rows]

[hero78119]

I suggest in this PR, we can refactor duplicate part from another mock_prover util

ceno/ceno_zkvm/src/scheme/mock_prover.rs

Line 748 in cec7b82

pub fn assert_satisfied_full(

In summary, in assert_satisfied_full

• test on all opcode + table circuit
• output error per opcode/table
• per opcode/table circuit, it only evaluate expression values on errors happened, and just output first row raw value

Since assert_satisfied_full is like a super set of ALL opcode + table circuit, whereas run_maybe_challenge for single opcode circuit. So probably it make sense to extract common part to run_maybe_challenge, then assert_satisfied_full just call run_maybe_challenge per opcode. With that, we remove all the duplicated, while keep a good debugging ability.

[hero78119]

does it work if we just wrap program to Arc right before ProgramTableCircuit::generate_fixed_traces, and keep load_program_table program as reference type?
with that it seems to keep Program instead of Arc in test code.

[hero78119]

it's not very intuive to me for why cs need to be mutable, does it nessesary?

[zemse]

I am trying to call assert_satisfied_raw inside assert_satisfied_full. Currently, assert_satisfied_raw takes CircuitBuilder struct which wants a mut ConstraintSystem.

Self::assert_satisfied_raw(
    &CircuitBuilder {
        cs: op_cs,
        params: cs.params.clone(),
    },
    ...
);

To remove the mutable reference, assert_satisfied_raw API need to be changed to take ConstraintSystem directly and would cause more changes everywhere.

[hero78119]

I c the reason, it's because assert_satisfied_raw api take CircuitBuilder.
But assert_satisfied_full take ConstainSystem which cause confuse to be mutable. I suggest take this small change to fit the expectation

diff --git a/ceno_zkvm/src/scheme/mock_prover.rs b/ceno_zkvm/src/scheme/mock_prover.rs
index 75340435..f5fe7cda 100644
--- a/ceno_zkvm/src/scheme/mock_prover.rs
+++ b/ceno_zkvm/src/scheme/mock_prover.rs
@@ -726,7 +726,7 @@ Hints:
     }

     pub fn assert_satisfied_full(
-        cs: &mut ZKVMConstraintSystem<E>,
+        cs: &ZKVMConstraintSystem<E>,
         mut fixed_trace: ZKVMFixedTraces<E>,
         witnesses: &ZKVMWitnesses<E>,
         pi: &PublicValues<u32>,
@@ -864,7 +864,7 @@ Hints:
         }

         // assert all opcodes and check lk multiplicity
-        for (name, op_cs) in (cs.circuit_css).iter_mut() {
+        for (name, op_cs) in &cs.circuit_css {
             let is_opcode = op_cs.lk_table_expressions.is_empty()
                 && op_cs.r_table_expressions.is_empty()
                 && op_cs.w_table_expressions.is_empty();
@@ -875,7 +875,7 @@ Hints:
             if let Some(witness) = witnesses.get_table_witness(name) {
                 Self::assert_satisfied_raw(
                     &CircuitBuilder {
-                        cs: op_cs,
+                        cs: &mut op_cs.clone(),
                         params: cs.params.clone(),
                     },
                     witness,

[hero78119]

rom_tables checking logic are missing in new refactor.
We need to check all opcode rom_type multiplicity sum are matching with table rom_type multiplicity