acvm/compiler/
validator.rs

1use crate::pwg::{
2    ErrorLocation, OpcodeNotSolvable, OpcodeResolutionError, ResolvedAssertionPayload,
3    arithmetic::ExpressionSolver,
4    blackbox::embedded_curve_ops::{execute_embedded_curve_add, execute_multi_scalar_mul},
5    blackbox::{self, hash::get_hash_input},
6    get_value, input_to_value,
7    memory_op::MemoryOpSolver,
8    witness_to_value,
9};
10use acir::{
11    AcirField,
12    circuit::{
13        Circuit, Opcode, OpcodeLocation,
14        opcodes::{BlackBoxFuncCall, BlockId, MemOp, MemOpKind},
15    },
16    native_types::{Witness, WitnessMap},
17};
18use acvm_blackbox_solver::{
19    BlackBoxFunctionSolver, bit_and, bit_xor, blake2s, blake3, keccakf1600,
20};
21use itertools::Itertools;
22use std::collections::HashMap;
23
24fn unsatisfied_constraint<F>(opcode_index: usize, message: String) -> OpcodeResolutionError<F> {
25    OpcodeResolutionError::UnsatisfiedConstrain {
26        opcode_location: ErrorLocation::Resolved(OpcodeLocation::Acir(opcode_index)),
27        payload: Some(ResolvedAssertionPayload::String(message)),
28    }
29}
30
31fn witness_value<F: AcirField>(
32    w: &Witness,
33    witness_map: &WitnessMap<F>,
34) -> Result<F, OpcodeResolutionError<F>> {
35    Ok(*witness_map.get(w).ok_or(OpcodeNotSolvable::MissingAssignment(w.witness_index()))?)
36}
37
38fn check_fits_in_bits<F: AcirField>(
39    value: F,
40    num_bits: u32,
41    opcode_index: usize,
42    opcode_name: &str,
43) -> Result<(), OpcodeResolutionError<F>> {
44    if value.num_bits() > num_bits {
45        return Err(unsatisfied_constraint(
46            opcode_index,
47            format!(
48                "{opcode_name} opcode violation: value {value} does not fit in {num_bits} bits"
49            ),
50        ));
51    }
52    Ok(())
53}
54
55/// Checks that an already-complete `witness_map` satisfies every *constraint* imposed by
56/// `circuit`, returning the first violation found.
57///
58/// This is a debugging/checking aid that re-evaluates each opcode's constraint against the
59/// provided witness, mirroring what a proving backend enforces: a witness that passes here is
60/// one the backend should accept, and a witness that fails here is one it should reject.
61///
62/// The unit of correctness is constraint satisfaction. Only opcodes that *impose constraints*
63/// are checked here; opcodes that impose none are intentionally skipped, because there is
64/// nothing about them for a witness to satisfy or violate. The most important example is
65/// [`Opcode::BrilligCall`], which runs unconstrained bytecode and is ignored entirely.
66pub fn validate_witness<F: AcirField>(
67    backend: &impl BlackBoxFunctionSolver<F>,
68    witness_map: &WitnessMap<F>,
69    circuit: &Circuit<F>,
70) -> Result<(), OpcodeResolutionError<F>> {
71    let mut block_solvers: HashMap<BlockId, MemoryOpSolver<F>> = HashMap::new();
72
73    for (opcode_index, opcode) in circuit.opcodes.iter().enumerate() {
74        match opcode {
75            Opcode::AssertZero(expression) => {
76                let result = &ExpressionSolver::evaluate(expression, witness_map);
77                if !result.is_zero() {
78                    return Err(unsatisfied_constraint(
79                        opcode_index,
80                        format!("Invalid witness assignment: {expression}"),
81                    ));
82                }
83            }
84            Opcode::BlackBoxFuncCall(black_box_func_call) => {
85                match black_box_func_call {
86                    BlackBoxFuncCall::AES128Encrypt { inputs, iv, key, outputs } => {
87                        let ciphertext = blackbox::aes128::execute_aes128_encryption_opcode(
88                            witness_map,
89                            inputs,
90                            iv,
91                            key,
92                        )?;
93                        for (output_witness, value) in outputs.iter().zip_eq(ciphertext) {
94                            let witness_value = witness_value(output_witness, witness_map)?;
95                            let output_value = F::from(u128::from(value));
96                            if witness_value != output_value {
97                                return Err(unsatisfied_constraint(
98                                    opcode_index,
99                                    format!(
100                                        "AES128 opcode violation: expected {output_value} but found {witness_value} for output witness {output_witness}",
101                                    ),
102                                ));
103                            }
104                        }
105                    }
106                    BlackBoxFuncCall::AND { lhs, rhs, num_bits, output } => {
107                        let lhs_value = input_to_value(witness_map, *lhs)?;
108                        let rhs_value = input_to_value(witness_map, *rhs)?;
109                        check_fits_in_bits(lhs_value, *num_bits, opcode_index, "AND")?;
110                        check_fits_in_bits(rhs_value, *num_bits, opcode_index, "AND")?;
111                        let and_result = bit_and(lhs_value, rhs_value, *num_bits);
112                        let output_value = witness_map
113                            .get(output)
114                            .ok_or(OpcodeNotSolvable::MissingAssignment(output.witness_index()))?;
115                        if and_result != *output_value {
116                            return Err(unsatisfied_constraint(
117                                opcode_index,
118                                format!(
119                                    "AND opcode violation: {lhs_value} AND {rhs_value} != {output_value} for {num_bits} bits"
120                                ),
121                            ));
122                        }
123                    }
124                    BlackBoxFuncCall::XOR { lhs, rhs, num_bits, output } => {
125                        let lhs_value = input_to_value(witness_map, *lhs)?;
126                        let rhs_value = input_to_value(witness_map, *rhs)?;
127                        check_fits_in_bits(lhs_value, *num_bits, opcode_index, "XOR")?;
128                        check_fits_in_bits(rhs_value, *num_bits, opcode_index, "XOR")?;
129                        let xor_result = bit_xor(lhs_value, rhs_value, *num_bits);
130                        let output_value = witness_map
131                            .get(output)
132                            .ok_or(OpcodeNotSolvable::MissingAssignment(output.witness_index()))?;
133                        if xor_result != *output_value {
134                            return Err(unsatisfied_constraint(
135                                opcode_index,
136                                format!(
137                                    "XOR opcode violation: {lhs_value} XOR {rhs_value} != {output_value} for {num_bits} bits"
138                                ),
139                            ));
140                        }
141                    }
142                    BlackBoxFuncCall::RANGE { input, num_bits } => {
143                        let value = input_to_value(witness_map, *input)?;
144                        check_fits_in_bits(value, *num_bits, opcode_index, "RANGE")?;
145                    }
146                    BlackBoxFuncCall::Blake2s { inputs, outputs } => {
147                        let message_input = get_hash_input(witness_map, inputs, None, 8)?;
148                        let digest: [u8; 32] = blake2s(&message_input)?;
149                        for i in 0..32 {
150                            let output_witness = &outputs[i];
151                            let witness_value = witness_map.get(output_witness).ok_or(
152                                OpcodeNotSolvable::MissingAssignment(
153                                    output_witness.witness_index(),
154                                ),
155                            )?;
156                            if *witness_value != F::from_be_bytes_reduce(&[digest[i]]) {
157                                return Err(unsatisfied_constraint(
158                                    opcode_index,
159                                    format!(
160                                        "BLAKE2s opcode violation: expected {:?} but found {:?} for output witness {:?}",
161                                        F::from_be_bytes_reduce(&[digest[i]]),
162                                        witness_value,
163                                        output_witness
164                                    ),
165                                ));
166                            }
167                        }
168                    }
169                    BlackBoxFuncCall::Blake3 { inputs, outputs } => {
170                        let message_input = get_hash_input(witness_map, inputs, None, 8)?;
171                        let digest: [u8; 32] = blake3(&message_input)?;
172                        for i in 0..32 {
173                            let output_witness = &outputs[i];
174                            let witness_value = witness_value(output_witness, witness_map)?;
175                            if witness_value != F::from_be_bytes_reduce(&[digest[i]]) {
176                                return Err(unsatisfied_constraint(
177                                    opcode_index,
178                                    format!(
179                                        "BLAKE3 opcode violation: expected {:?} but found {:?} for output witness {:?}",
180                                        F::from_be_bytes_reduce(&[digest[i]]),
181                                        witness_value,
182                                        output_witness
183                                    ),
184                                ));
185                            }
186                        }
187                    }
188                    BlackBoxFuncCall::EcdsaSecp256k1 {
189                        public_key_x,
190                        public_key_y,
191                        signature,
192                        hashed_message,
193                        predicate,
194                        output,
195                    } => {
196                        let predicate_value = input_to_value(witness_map, *predicate)?.is_one();
197                        if predicate_value {
198                            let is_valid = blackbox::signature::ecdsa::execute_ecdsa(
199                                witness_map,
200                                public_key_x,
201                                public_key_y,
202                                signature,
203                                hashed_message,
204                                predicate,
205                                true,
206                            )?;
207                            let output_value = witness_value(output, witness_map)?;
208                            if output_value != F::from(is_valid) {
209                                return Err(unsatisfied_constraint(
210                                    opcode_index,
211                                    format!(
212                                        "EcdsaSecp256k1 opcode violation: expected {:?} but found {:?} for output witness {:?}",
213                                        F::from(is_valid),
214                                        output_value,
215                                        output
216                                    ),
217                                ));
218                            }
219                        }
220                    }
221                    BlackBoxFuncCall::EcdsaSecp256r1 {
222                        public_key_x,
223                        public_key_y,
224                        signature,
225                        hashed_message,
226                        predicate,
227                        output,
228                    } => {
229                        let predicate_value = input_to_value(witness_map, *predicate)?.is_one();
230                        if predicate_value {
231                            let is_valid = blackbox::signature::ecdsa::execute_ecdsa(
232                                witness_map,
233                                public_key_x,
234                                public_key_y,
235                                signature,
236                                hashed_message,
237                                predicate,
238                                false,
239                            )?;
240                            let output_value = witness_value(output, witness_map)?;
241                            if output_value != F::from(is_valid) {
242                                return Err(unsatisfied_constraint(
243                                    opcode_index,
244                                    format!(
245                                        "EcdsaSecp256r1 opcode violation: expected {:?} but found {:?} for output witness {:?}",
246                                        F::from(is_valid),
247                                        output_value,
248                                        output
249                                    ),
250                                ));
251                            }
252                        }
253                    }
254                    BlackBoxFuncCall::MultiScalarMul { points, scalars, predicate, outputs } => {
255                        let predicate_value = input_to_value(witness_map, *predicate)?.is_one();
256                        if predicate_value {
257                            let (res_x, res_y) = execute_multi_scalar_mul(
258                                backend,
259                                witness_map,
260                                points,
261                                scalars,
262                                *predicate,
263                            )?;
264                            let output_x_value = witness_value(&outputs.0, witness_map)?;
265                            let output_y_value = witness_value(&outputs.1, witness_map)?;
266                            if res_x != output_x_value || res_y != output_y_value {
267                                return Err(unsatisfied_constraint(
268                                    opcode_index,
269                                    format!(
270                                        "MultiScalarMul opcode violation: expected ({res_x}, {res_y}) but found ({output_x_value}, {output_y_value})"
271                                    ),
272                                ));
273                            }
274                        }
275                    }
276                    BlackBoxFuncCall::EmbeddedCurveAdd { input1, input2, predicate, outputs } => {
277                        let predicate_value = input_to_value(witness_map, *predicate)?.is_one();
278                        if predicate_value {
279                            let (res_x, res_y) = execute_embedded_curve_add(
280                                backend,
281                                witness_map,
282                                **input1,
283                                **input2,
284                                *predicate,
285                            )?;
286                            let output_x_value = witness_value(&outputs.0, witness_map)?;
287                            let output_y_value = witness_value(&outputs.1, witness_map)?;
288                            if res_x != output_x_value || res_y != output_y_value {
289                                return Err(unsatisfied_constraint(
290                                    opcode_index,
291                                    format!(
292                                        "EmbeddedCurveAdd opcode violation: expected ({res_x}, {res_y}) but found ({output_x_value}, {output_y_value})"
293                                    ),
294                                ));
295                            }
296                        }
297                    }
298                    BlackBoxFuncCall::Keccakf1600 { inputs, outputs } => {
299                        let mut state = [0; 25];
300                        for (it, input) in state.iter_mut().zip_eq(inputs.as_ref()) {
301                            let witness_assignment = input_to_value(witness_map, *input)?;
302                            check_fits_in_bits(
303                                witness_assignment,
304                                64,
305                                opcode_index,
306                                "Keccakf1600",
307                            )?;
308                            *it = witness_assignment
309                                .try_to_u64()
310                                .expect("value was just checked to fit in 64 bits");
311                        }
312                        let output_state = keccakf1600(state)?;
313                        for (output_witness, value) in outputs.iter().zip_eq(output_state) {
314                            let witness_value = witness_value(output_witness, witness_map)?;
315                            if witness_value != F::from(u128::from(value)) {
316                                return Err(unsatisfied_constraint(
317                                    opcode_index,
318                                    format!(
319                                        "Keccakf1600 opcode violation: expected {value} but found {witness_value} for output witness {output_witness}",
320                                    ),
321                                ));
322                            }
323                        }
324                    }
325                    // Recursive aggregation is verified by the backend rather than the ACVM, so
326                    // there is no constraint to evaluate here. Its operands must still be present
327                    // in the witness map though, matching the PWG solver which requires every
328                    // `get_inputs_vec()` operand to be assigned before treating the opcode as
329                    // backend-owned.
330                    BlackBoxFuncCall::RecursiveAggregation { .. } => {
331                        for input in black_box_func_call.get_inputs_vec() {
332                            input_to_value(witness_map, input)?;
333                        }
334                    }
335                    BlackBoxFuncCall::Poseidon2Permutation { inputs, outputs } => {
336                        let state = blackbox::hash::execute_poseidon2_permutation_opcode(
337                            backend,
338                            witness_map,
339                            inputs,
340                        )?;
341                        for (output_witness, value) in outputs.iter().zip_eq(state) {
342                            let witness_value = witness_map.get(output_witness).ok_or(
343                                OpcodeNotSolvable::MissingAssignment(
344                                    output_witness.witness_index(),
345                                ),
346                            )?;
347                            if *witness_value != value {
348                                return Err(unsatisfied_constraint(
349                                    opcode_index,
350                                    format!(
351                                        "Poseidon2 opcode violation: expected {value} but found {witness_value} for output witness {output_witness}",
352                                    ),
353                                ));
354                            }
355                        }
356                    }
357                    BlackBoxFuncCall::Sha256Compression { inputs, hash_values, outputs } => {
358                        let state = blackbox::hash::execute_sha_256_permutation_opcode(
359                            witness_map,
360                            inputs,
361                            hash_values,
362                        )?;
363
364                        for (output_witness, value) in outputs.iter().zip_eq(state) {
365                            let witness_value = witness_map.get(output_witness).ok_or(
366                                OpcodeNotSolvable::MissingAssignment(
367                                    output_witness.witness_index(),
368                                ),
369                            )?;
370                            if *witness_value != F::from(u128::from(value)) {
371                                return Err(unsatisfied_constraint(
372                                    opcode_index,
373                                    format!(
374                                        "SHA256 Compression opcode violation: expected {:?} but found {:?} for output witness {:?}",
375                                        F::from(u128::from(value)),
376                                        witness_value,
377                                        output_witness
378                                    ),
379                                ));
380                            }
381                        }
382                    }
383                }
384            }
385            Opcode::MemoryOp { block_id, op } => {
386                let solver = block_solvers
387                    .get_mut(block_id)
388                    .expect("Memory block should have been initialized");
389                solver.check_memory_op(op, witness_map, opcode_index)?;
390            }
391            Opcode::MemoryInit { block_id, init, .. } => {
392                let solver = MemoryOpSolver::new(init, witness_map)?;
393                let existing_block_id = block_solvers.insert(*block_id, solver);
394                if existing_block_id.is_some() {
395                    return Err(unsatisfied_constraint(
396                        opcode_index,
397                        format!(
398                            "Attempted reinitialization of memory block {:?}",
399                            block_id.as_u32(),
400                        ),
401                    ));
402                }
403            }
404            // A `BrilligCall` runs unconstrained bytecode: it generates no constraints on either
405            // its inputs or its outputs, so there is nothing for a witness to satisfy and the
406            // opcode is ignored entirely.
407            Opcode::BrilligCall { .. } => (),
408            Opcode::Call { id: _, inputs, outputs, predicate } => {
409                // Skip validation when predicate is false
410                let pred_value = get_value(predicate, witness_map)?;
411                if pred_value.is_zero() {
412                    continue;
413                }
414
415                // Verify input witnesses exist
416                for input in inputs {
417                    if witness_map.get(input).is_none() {
418                        return Err(
419                            OpcodeNotSolvable::MissingAssignment(input.witness_index()).into()
420                        );
421                    }
422                }
423
424                // Verify output witnesses exist (value should have been validated by the called function)
425                for output in outputs {
426                    if witness_map.get(output).is_none() {
427                        return Err(
428                            OpcodeNotSolvable::MissingAssignment(output.witness_index()).into()
429                        );
430                    }
431                }
432            }
433        }
434    }
435
436    Ok(())
437}
438
439impl<F: AcirField> MemoryOpSolver<F> {
440    pub(crate) fn check_memory_op(
441        &mut self,
442        op: &MemOp,
443        witness_map: &WitnessMap<F>,
444        opcode_index: usize,
445    ) -> Result<(), OpcodeResolutionError<F>> {
446        // Find the memory index associated with this memory operation.
447        let index = *witness_to_value(witness_map, op.index)?;
448        let memory_index = self.index_from_field(index)?;
449
450        let value = *witness_to_value(witness_map, op.value)?;
451
452        match op.operation {
453            MemOpKind::Read => {
454                // `value = arr[memory_index]`
455                let value_in_array = self.read_memory_index(memory_index)?;
456                if value != value_in_array {
457                    return Err(unsatisfied_constraint(
458                        opcode_index,
459                        format!(
460                            "Memory read opcode violation at index {memory_index}: expected {value_in_array} but found {value}",
461                        ),
462                    ));
463                }
464                Ok(())
465            }
466            MemOpKind::Write => {
467                // `arr[memory_index] = value`
468                self.write_memory_index(memory_index, value)
469            }
470        }
471    }
472}
473
474#[cfg(test)]
475mod tests {
476    use std::collections::BTreeMap;
477
478    use acir::{
479        AcirField, BlackBoxFunc, FieldElement,
480        circuit::{
481            Circuit, Opcode, OpcodeLocation, PublicInputs,
482            brillig::{BrilligFunctionId, BrilligInputs, BrilligOutputs},
483            opcodes::{AcirFunctionId, BlackBoxFuncCall, BlockId, FunctionInput, MemOp},
484        },
485        native_types::{Expression, Witness, WitnessMap},
486    };
487    use bn254_blackbox_solver::Bn254BlackBoxSolver;
488
489    use super::validate_witness;
490    use crate::pwg::{
491        ErrorLocation, OpcodeNotSolvable, OpcodeResolutionError, ResolvedAssertionPayload,
492    };
493
494    fn assert_unsatisfied_constraint(
495        result: Result<(), OpcodeResolutionError<FieldElement>>,
496        opcode_index: usize,
497        message: &str,
498    ) {
499        assert_eq!(
500            result.unwrap_err(),
501            OpcodeResolutionError::UnsatisfiedConstrain {
502                opcode_location: ErrorLocation::Resolved(OpcodeLocation::Acir(opcode_index)),
503                payload: Some(ResolvedAssertionPayload::String(message.to_string())),
504            },
505        );
506    }
507
508    /// Helper to create a simple circuit with the given opcodes
509    fn make_circuit(opcodes: Vec<Opcode<FieldElement>>) -> Circuit<FieldElement> {
510        Circuit {
511            opcodes,
512            private_parameters: Default::default(),
513            public_parameters: PublicInputs::default(),
514            return_values: PublicInputs::default(),
515            assert_messages: Default::default(),
516            function_name: "test".to_string(),
517        }
518    }
519
520    /// Builds a Keccakf1600 circuit over input witnesses `0..25` and output witnesses `25..50`.
521    fn keccakf1600_circuit() -> Circuit<FieldElement> {
522        let inputs: Box<[FunctionInput<FieldElement>; 25]> =
523            Box::new(std::array::from_fn(|i| FunctionInput::Witness(Witness(i as u32))));
524        let outputs: Box<[Witness; 25]> =
525            Box::new(std::array::from_fn(|i| Witness((25 + i) as u32)));
526        make_circuit(vec![Opcode::BlackBoxFuncCall(BlackBoxFuncCall::Keccakf1600 {
527            inputs,
528            outputs,
529        })])
530    }
531
532    #[test]
533    fn test_keccakf1600_out_of_range_lane_does_not_panic() {
534        // A lane holding 2^64 does not fit in 64 bits: `validate_witness` must report a
535        // graceful, opcode-located constraint violation rather than panicking on the
536        // internal `try_to_u64` conversion.
537        let circuit = keccakf1600_circuit();
538        let mut witness_map = WitnessMap::new();
539        witness_map.insert(Witness(0), FieldElement::from(1u128 << 64));
540        for i in 1..50u32 {
541            witness_map.insert(Witness(i), FieldElement::zero());
542        }
543
544        let backend = Bn254BlackBoxSolver;
545        assert_unsatisfied_constraint(
546            validate_witness(&backend, &witness_map, &circuit),
547            0,
548            "Keccakf1600 opcode violation: value 18446744073709551616 does not fit in 64 bits",
549        );
550    }
551
552    #[test]
553    fn test_multi_scalar_mul_mixed_scalar_limbs_rejected() {
554        // The `MultiScalarMul` opcode requires each scalar's `(lo, hi)` limbs to be
555        // uniformly witnesses or uniformly constants, just like each point's coordinates.
556        // A witness cannot satisfy a circuit whose declared input shape is invalid, so
557        // `validate_witness` must reject the circuit rather than compute an output for it.
558        let generator_y = FieldElement::try_from_str(
559            "17631683881184975370165255887551781615748388533673675138860",
560        )
561        .unwrap();
562
563        let circuit =
564            make_circuit(vec![Opcode::BlackBoxFuncCall(BlackBoxFuncCall::MultiScalarMul {
565                points: vec![
566                    FunctionInput::Witness(Witness(0)),
567                    FunctionInput::Witness(Witness(1)),
568                ],
569                scalars: vec![
570                    FunctionInput::Constant(FieldElement::one()),
571                    FunctionInput::Witness(Witness(2)),
572                ],
573                predicate: FunctionInput::Constant(FieldElement::one()),
574                outputs: (Witness(3), Witness(4)),
575            })]);
576
577        let witness_map = WitnessMap::from(BTreeMap::from_iter([
578            (Witness(0), FieldElement::one()),
579            (Witness(1), generator_y),
580            (Witness(2), FieldElement::zero()),
581            (Witness(3), FieldElement::one()),
582            (Witness(4), generator_y),
583        ]));
584
585        let result = validate_witness(&Bn254BlackBoxSolver, &witness_map, &circuit);
586        let Err(OpcodeResolutionError::BlackBoxFunctionFailed(func, message)) = result else {
587            panic!("expected a mixed constant/witness scalar pair to be rejected, got {result:?}");
588        };
589        assert_eq!(func, BlackBoxFunc::MultiScalarMul);
590        assert!(
591            message.contains("both witnesses or both constants"),
592            "unexpected failure message: {message}"
593        );
594    }
595
596    #[test]
597    fn test_assert_zero_valid() {
598        // w1 + w2 - w3 = 0, where w1=2, w2=3, w3=5
599        let expr = Expression {
600            mul_terms: vec![],
601            linear_combinations: vec![
602                (FieldElement::one(), Witness(1)),
603                (FieldElement::one(), Witness(2)),
604                (-FieldElement::one(), Witness(3)),
605            ],
606            q_c: FieldElement::zero(),
607        };
608
609        let circuit = make_circuit(vec![Opcode::AssertZero(expr)]);
610
611        let witness_map = WitnessMap::from(BTreeMap::from_iter([
612            (Witness(1), FieldElement::from(2u128)),
613            (Witness(2), FieldElement::from(3u128)),
614            (Witness(3), FieldElement::from(5u128)),
615        ]));
616
617        let backend = Bn254BlackBoxSolver;
618        assert!(validate_witness(&backend, &witness_map, &circuit).is_ok());
619    }
620
621    #[test]
622    fn test_assert_zero_invalid() {
623        // w1 + w2 - w3 = 0, but w1=2, w2=3, w3=6 (should be 5)
624        let expr = Expression {
625            mul_terms: vec![],
626            linear_combinations: vec![
627                (FieldElement::one(), Witness(1)),
628                (FieldElement::one(), Witness(2)),
629                (-FieldElement::one(), Witness(3)),
630            ],
631            q_c: FieldElement::zero(),
632        };
633
634        let circuit = make_circuit(vec![Opcode::AssertZero(expr)]);
635
636        let witness_map = WitnessMap::from(BTreeMap::from_iter([
637            (Witness(1), FieldElement::from(2u128)),
638            (Witness(2), FieldElement::from(3u128)),
639            (Witness(3), FieldElement::from(6u128)), // Wrong value!
640        ]));
641
642        let backend = Bn254BlackBoxSolver;
643        assert_unsatisfied_constraint(
644            validate_witness(&backend, &witness_map, &circuit),
645            0,
646            "Invalid witness assignment: w1 + w2 - w3",
647        );
648    }
649
650    #[test]
651    fn test_assert_zero_with_multiplication() {
652        // w1 * w2 - w3 = 0, where w1=3, w2=4, w3=12
653        let expr = Expression {
654            mul_terms: vec![(FieldElement::one(), Witness(1), Witness(2))],
655            linear_combinations: vec![(-FieldElement::one(), Witness(3))],
656            q_c: FieldElement::zero(),
657        };
658
659        let circuit = make_circuit(vec![Opcode::AssertZero(expr)]);
660
661        let witness_map = WitnessMap::from(BTreeMap::from_iter([
662            (Witness(1), FieldElement::from(3u128)),
663            (Witness(2), FieldElement::from(4u128)),
664            (Witness(3), FieldElement::from(12u128)),
665        ]));
666
667        let backend = Bn254BlackBoxSolver;
668        assert!(validate_witness(&backend, &witness_map, &circuit).is_ok());
669    }
670
671    #[test]
672    fn test_range_valid() {
673        // w1 should fit in 8 bits
674        let circuit = make_circuit(vec![Opcode::BlackBoxFuncCall(BlackBoxFuncCall::RANGE {
675            input: FunctionInput::Witness(Witness(1)),
676            num_bits: 8,
677        })]);
678
679        let witness_map = WitnessMap::from(BTreeMap::from_iter([
680            (Witness(1), FieldElement::from(255u128)), // Max 8-bit value
681        ]));
682
683        let backend = Bn254BlackBoxSolver;
684        assert!(validate_witness(&backend, &witness_map, &circuit).is_ok());
685    }
686
687    #[test]
688    fn test_range_invalid() {
689        // w1 should fit in 8 bits, but 256 doesn't
690        let circuit = make_circuit(vec![Opcode::BlackBoxFuncCall(BlackBoxFuncCall::RANGE {
691            input: FunctionInput::Witness(Witness(1)),
692            num_bits: 8,
693        })]);
694
695        let witness_map = WitnessMap::from(BTreeMap::from_iter([
696            (Witness(1), FieldElement::from(256u128)), // Too large for 8 bits
697        ]));
698
699        let backend = Bn254BlackBoxSolver;
700        assert_unsatisfied_constraint(
701            validate_witness(&backend, &witness_map, &circuit),
702            0,
703            "RANGE opcode violation: value 256 does not fit in 8 bits",
704        );
705    }
706
707    #[test]
708    fn test_and_valid() {
709        // w1 AND w2 = w3, where w1=0b1010, w2=0b1100, w3=0b1000
710        let circuit = make_circuit(vec![Opcode::BlackBoxFuncCall(BlackBoxFuncCall::AND {
711            lhs: FunctionInput::Witness(Witness(1)),
712            rhs: FunctionInput::Witness(Witness(2)),
713            num_bits: 8,
714            output: Witness(3),
715        })]);
716
717        let witness_map = WitnessMap::from(BTreeMap::from_iter([
718            (Witness(1), FieldElement::from(0b1010u128)),
719            (Witness(2), FieldElement::from(0b1100u128)),
720            (Witness(3), FieldElement::from(0b1000u128)),
721        ]));
722
723        let backend = Bn254BlackBoxSolver;
724        assert!(validate_witness(&backend, &witness_map, &circuit).is_ok());
725    }
726
727    #[test]
728    fn test_and_invalid() {
729        // w1 AND w2 = w3, but w3 has wrong value
730        let circuit = make_circuit(vec![Opcode::BlackBoxFuncCall(BlackBoxFuncCall::AND {
731            lhs: FunctionInput::Witness(Witness(1)),
732            rhs: FunctionInput::Witness(Witness(2)),
733            num_bits: 8,
734            output: Witness(3),
735        })]);
736
737        let witness_map = WitnessMap::from(BTreeMap::from_iter([
738            (Witness(1), FieldElement::from(0b1010u128)),
739            (Witness(2), FieldElement::from(0b1100u128)),
740            (Witness(3), FieldElement::from(0b1111u128)), // Wrong!
741        ]));
742
743        let backend = Bn254BlackBoxSolver;
744        assert_unsatisfied_constraint(
745            validate_witness(&backend, &witness_map, &circuit),
746            0,
747            "AND opcode violation: 10 AND 12 != 15 for 8 bits",
748        );
749    }
750
751    #[test]
752    fn test_xor_valid() {
753        // w1 XOR w2 = w3, where w1=0b1010, w2=0b1100, w3=0b0110
754        let circuit = make_circuit(vec![Opcode::BlackBoxFuncCall(BlackBoxFuncCall::XOR {
755            lhs: FunctionInput::Witness(Witness(1)),
756            rhs: FunctionInput::Witness(Witness(2)),
757            num_bits: 8,
758            output: Witness(3),
759        })]);
760
761        let witness_map = WitnessMap::from(BTreeMap::from_iter([
762            (Witness(1), FieldElement::from(0b1010u128)),
763            (Witness(2), FieldElement::from(0b1100u128)),
764            (Witness(3), FieldElement::from(0b0110u128)),
765        ]));
766
767        let backend = Bn254BlackBoxSolver;
768        assert!(validate_witness(&backend, &witness_map, &circuit).is_ok());
769    }
770
771    #[test]
772    fn test_xor_invalid() {
773        // w1 XOR w2 = w3, but w3 has wrong value
774        let circuit = make_circuit(vec![Opcode::BlackBoxFuncCall(BlackBoxFuncCall::XOR {
775            lhs: FunctionInput::Witness(Witness(1)),
776            rhs: FunctionInput::Witness(Witness(2)),
777            num_bits: 8,
778            output: Witness(3),
779        })]);
780
781        let witness_map = WitnessMap::from(BTreeMap::from_iter([
782            (Witness(1), FieldElement::from(0b1010u128)),
783            (Witness(2), FieldElement::from(0b1100u128)),
784            (Witness(3), FieldElement::from(0b1111u128)), // Wrong!
785        ]));
786
787        let backend = Bn254BlackBoxSolver;
788        assert_unsatisfied_constraint(
789            validate_witness(&backend, &witness_map, &circuit),
790            0,
791            "XOR opcode violation: 10 XOR 12 != 15 for 8 bits",
792        );
793    }
794
795    #[test]
796    fn test_missing_witness_in_expression() {
797        let expr = Expression {
798            mul_terms: vec![],
799            linear_combinations: vec![(FieldElement::one(), Witness(1))],
800            q_c: FieldElement::zero(),
801        };
802
803        let circuit = make_circuit(vec![Opcode::AssertZero(expr)]);
804
805        // Empty witness map - missing w1
806        let witness_map = WitnessMap::default();
807
808        let backend = Bn254BlackBoxSolver;
809        assert_unsatisfied_constraint(
810            validate_witness(&backend, &witness_map, &circuit),
811            0,
812            "Invalid witness assignment: w1",
813        );
814    }
815
816    #[test]
817    fn test_call_opcode_valid() {
818        let circuit = make_circuit(vec![Opcode::Call {
819            id: AcirFunctionId::new(1),
820            inputs: vec![Witness(1), Witness(2)],
821            outputs: vec![Witness(3)],
822            predicate: Expression::one(),
823        }]);
824
825        let witness_map = WitnessMap::from(BTreeMap::from_iter([
826            (Witness(1), FieldElement::from(1u128)),
827            (Witness(2), FieldElement::from(2u128)),
828            (Witness(3), FieldElement::from(3u128)),
829        ]));
830
831        let backend = Bn254BlackBoxSolver;
832        assert!(validate_witness(&backend, &witness_map, &circuit).is_ok());
833    }
834
835    #[test]
836    fn test_call_opcode_missing_input() {
837        let circuit = make_circuit(vec![Opcode::Call {
838            id: AcirFunctionId::new(1),
839            inputs: vec![Witness(1), Witness(2)],
840            outputs: vec![Witness(3)],
841            predicate: Expression::one(),
842        }]);
843
844        // Missing Witness(2)
845        let witness_map = WitnessMap::from(BTreeMap::from_iter([
846            (Witness(1), FieldElement::from(1u128)),
847            (Witness(3), FieldElement::from(3u128)),
848        ]));
849
850        let backend = Bn254BlackBoxSolver;
851        assert_eq!(
852            validate_witness(&backend, &witness_map, &circuit).unwrap_err(),
853            OpcodeResolutionError::OpcodeNotSolvable(OpcodeNotSolvable::MissingAssignment(2)),
854        );
855    }
856
857    #[test]
858    fn test_call_opcode_missing_output() {
859        let circuit = make_circuit(vec![Opcode::Call {
860            id: AcirFunctionId::new(1),
861            inputs: vec![Witness(1), Witness(2)],
862            outputs: vec![Witness(3)],
863            predicate: Expression::one(),
864        }]);
865
866        // Missing Witness(3) output
867        let witness_map = WitnessMap::from(BTreeMap::from_iter([
868            (Witness(1), FieldElement::from(1u128)),
869            (Witness(2), FieldElement::from(2u128)),
870        ]));
871
872        let backend = Bn254BlackBoxSolver;
873        assert_eq!(
874            validate_witness(&backend, &witness_map, &circuit).unwrap_err(),
875            OpcodeResolutionError::OpcodeNotSolvable(OpcodeNotSolvable::MissingAssignment(3)),
876        );
877    }
878
879    #[test]
880    fn test_call_opcode_skipped_with_zero_predicate() {
881        // Predicate is zero, so call should be skipped even with missing witnesses
882        let circuit = make_circuit(vec![Opcode::Call {
883            id: AcirFunctionId::new(1),
884            inputs: vec![Witness(1), Witness(2)],
885            outputs: vec![Witness(3)],
886            predicate: Expression {
887                mul_terms: vec![],
888                linear_combinations: vec![(FieldElement::one(), Witness(4))],
889                q_c: FieldElement::zero(),
890            },
891        }]);
892
893        // Witness(4) = 0, so predicate is false, call is skipped
894        // Missing input/output witnesses should not cause an error
895        let witness_map =
896            WitnessMap::from(BTreeMap::from_iter([(Witness(4), FieldElement::zero())]));
897
898        let backend = Bn254BlackBoxSolver;
899        assert!(validate_witness(&backend, &witness_map, &circuit).is_ok());
900    }
901
902    #[test]
903    fn test_memory_init_and_read() {
904        let block_id = BlockId::new(0);
905
906        let circuit = make_circuit(vec![
907            // Initialize memory block with witnesses 1 and 2
908            Opcode::MemoryInit {
909                block_id,
910                init: vec![Witness(1), Witness(2)],
911                block_type: acir::circuit::opcodes::BlockType::Memory,
912            },
913            // Read from index 0 (Witness(0)=0) into witness 3
914            Opcode::MemoryOp { block_id, op: MemOp::read_at_mem_index(Witness(0), Witness(3)) },
915        ]);
916
917        let witness_map = WitnessMap::from(BTreeMap::from_iter([
918            (Witness(0), FieldElement::zero()),
919            (Witness(1), FieldElement::from(42u128)),
920            (Witness(2), FieldElement::from(43u128)),
921            (Witness(3), FieldElement::from(42u128)), // Should match value at index 0
922        ]));
923
924        let backend = Bn254BlackBoxSolver;
925        assert!(validate_witness(&backend, &witness_map, &circuit).is_ok());
926    }
927
928    #[test]
929    fn test_memory_read_wrong_value() {
930        let block_id = BlockId::new(0);
931
932        let circuit = make_circuit(vec![
933            Opcode::MemoryInit {
934                block_id,
935                init: vec![Witness(1), Witness(2)],
936                block_type: acir::circuit::opcodes::BlockType::Memory,
937            },
938            Opcode::MemoryOp { block_id, op: MemOp::read_at_mem_index(Witness(0), Witness(3)) },
939        ]);
940
941        let witness_map = WitnessMap::from(BTreeMap::from_iter([
942            (Witness(0), FieldElement::zero()),
943            (Witness(1), FieldElement::from(42u128)),
944            (Witness(2), FieldElement::from(43u128)),
945            (Witness(3), FieldElement::from(99u128)), // Wrong! Should be 42
946        ]));
947
948        let backend = Bn254BlackBoxSolver;
949        assert_unsatisfied_constraint(
950            validate_witness(&backend, &witness_map, &circuit),
951            1,
952            "Memory read opcode violation at index 0: expected 42 but found 99",
953        );
954    }
955
956    #[test]
957    fn test_memory_write_then_read() {
958        let block_id = BlockId::new(0);
959
960        let circuit = make_circuit(vec![
961            // Initialize memory block
962            Opcode::MemoryInit {
963                block_id,
964                init: vec![Witness(1), Witness(2)],
965                block_type: acir::circuit::opcodes::BlockType::Memory,
966            },
967            // Write value from witness 3 to index 0 (Witness(0)=0)
968            Opcode::MemoryOp { block_id, op: MemOp::write_to_mem_index(Witness(0), Witness(3)) },
969            // Read from index 0 into witness 4
970            Opcode::MemoryOp { block_id, op: MemOp::read_at_mem_index(Witness(0), Witness(4)) },
971        ]);
972
973        let witness_map = WitnessMap::from(BTreeMap::from_iter([
974            (Witness(0), FieldElement::zero()),
975            (Witness(1), FieldElement::from(42u128)), // Initial value at index 0
976            (Witness(2), FieldElement::from(43u128)), // Initial value at index 1
977            (Witness(3), FieldElement::from(100u128)), // Value to write
978            (Witness(4), FieldElement::from(100u128)), // Read should get written value
979        ]));
980
981        let backend = Bn254BlackBoxSolver;
982        assert!(validate_witness(&backend, &witness_map, &circuit).is_ok());
983    }
984
985    #[test]
986    fn test_brillig_call_with_empty_witness_map() {
987        // Create a BrilligCall opcode with input and output witnesses
988        // Brillig calls are unconstrained and should be skipped during validation,
989        // so this should pass even with an empty witness map
990        let circuit = make_circuit(vec![Opcode::BrilligCall {
991            id: BrilligFunctionId::new(0),
992            inputs: vec![
993                BrilligInputs::Single(Witness(1).into()),
994                BrilligInputs::Single(Witness(2).into()),
995            ],
996            outputs: vec![BrilligOutputs::Simple(Witness(3))],
997            predicate: Expression::one(),
998        }]);
999
1000        // Empty witness map
1001        let witness_map = WitnessMap::default();
1002
1003        let backend = Bn254BlackBoxSolver;
1004        assert!(validate_witness(&backend, &witness_map, &circuit).is_ok());
1005    }
1006
1007    #[test]
1008    fn test_brillig_call_outputs_are_not_validated() {
1009        // A `BrilligCall` imposes no constraints, so the validator must not check its outputs.
1010        // Here the output witness holds an arbitrary value that no Brillig program needs to have
1011        // produced, and nothing constrained consumes it. Validation must still succeed because the
1012        // witness satisfies every constraint in the circuit (there are none). This is exactly the
1013        // behaviour audit finding noir-claude#502 mistook for a bug.
1014        let circuit = make_circuit(vec![Opcode::BrilligCall {
1015            id: BrilligFunctionId::new(0),
1016            inputs: vec![BrilligInputs::Single(Witness(1).into())],
1017            outputs: vec![BrilligOutputs::Simple(Witness(2))],
1018            predicate: Expression::one(),
1019        }]);
1020
1021        let witness_map = WitnessMap::from(BTreeMap::from_iter([
1022            (Witness(1), FieldElement::from(7u128)),
1023            (Witness(2), FieldElement::from(123_456u128)), // arbitrary; intentionally not checked
1024        ]));
1025
1026        let backend = Bn254BlackBoxSolver;
1027        assert!(validate_witness(&backend, &witness_map, &circuit).is_ok());
1028    }
1029
1030    #[test]
1031    fn test_brillig_output_validated_by_consuming_constraint() {
1032        // Brillig outputs are only ever "checked" via the later *constrained* opcodes that read
1033        // them. A wrong value is reported against that constrained opcode (index 1 here), never
1034        // against the unconstrained `BrilligCall` (index 0).
1035        let circuit = make_circuit(vec![
1036            Opcode::BrilligCall {
1037                id: BrilligFunctionId::new(0),
1038                inputs: vec![],
1039                outputs: vec![BrilligOutputs::Simple(Witness(1))],
1040                predicate: Expression::one(),
1041            },
1042            // Constrain the Brillig output: w1 - 5 == 0.
1043            Opcode::AssertZero(Expression {
1044                mul_terms: vec![],
1045                linear_combinations: vec![(FieldElement::one(), Witness(1))],
1046                q_c: -FieldElement::from(5u128),
1047            }),
1048        ]);
1049
1050        let witness_map =
1051            WitnessMap::from(BTreeMap::from_iter([(Witness(1), FieldElement::from(6u128))]));
1052
1053        let backend = Bn254BlackBoxSolver;
1054        assert_unsatisfied_constraint(
1055            validate_witness(&backend, &witness_map, &circuit),
1056            1,
1057            "Invalid witness assignment: w1 - 5",
1058        );
1059    }
1060
1061    #[test]
1062    fn error_on_memory_init_duplicate_block_id() {
1063        let block_id = BlockId::new(0);
1064
1065        let circuit = make_circuit(vec![
1066            Opcode::MemoryInit {
1067                block_id,
1068                init: vec![],
1069                block_type: acir::circuit::opcodes::BlockType::Memory,
1070            },
1071            Opcode::MemoryInit {
1072                block_id,
1073                init: vec![],
1074                block_type: acir::circuit::opcodes::BlockType::Memory,
1075            },
1076        ]);
1077
1078        let witness_map = WitnessMap::default();
1079        let backend = Bn254BlackBoxSolver;
1080
1081        assert_unsatisfied_constraint(
1082            validate_witness(&backend, &witness_map, &circuit),
1083            1,
1084            format!("Attempted reinitialization of memory block {}", block_id.as_u32()).as_str(),
1085        );
1086    }
1087
1088    fn recursive_aggregation_opcode() -> Opcode<FieldElement> {
1089        Opcode::BlackBoxFuncCall(BlackBoxFuncCall::RecursiveAggregation {
1090            verification_key: vec![FunctionInput::Witness(Witness(1))],
1091            proof: vec![FunctionInput::Witness(Witness(2))],
1092            public_inputs: vec![FunctionInput::Witness(Witness(3))],
1093            key_hash: FunctionInput::Witness(Witness(4)),
1094            proof_type: 0,
1095            predicate: FunctionInput::Witness(Witness(5)),
1096        })
1097    }
1098
1099    #[test]
1100    fn test_recursive_aggregation_missing_inputs() {
1101        // Recursive aggregation is verified by the backend, but its operands must still be
1102        // assigned. An empty witness map leaves every operand unassigned, so validation must
1103        // report the first missing operand rather than silently succeeding.
1104        let circuit = make_circuit(vec![recursive_aggregation_opcode()]);
1105
1106        let witness_map = WitnessMap::default();
1107
1108        let backend = Bn254BlackBoxSolver;
1109        assert_eq!(
1110            validate_witness(&backend, &witness_map, &circuit).unwrap_err(),
1111            OpcodeResolutionError::OpcodeNotSolvable(OpcodeNotSolvable::MissingAssignment(1)),
1112        );
1113    }
1114
1115    #[test]
1116    fn test_recursive_aggregation_with_assigned_inputs() {
1117        // With every operand assigned the opcode is treated as backend-owned and validation
1118        // succeeds without evaluating a constraint.
1119        let circuit = make_circuit(vec![recursive_aggregation_opcode()]);
1120
1121        let witness_map = WitnessMap::from(BTreeMap::from_iter([
1122            (Witness(1), FieldElement::zero()),
1123            (Witness(2), FieldElement::zero()),
1124            (Witness(3), FieldElement::zero()),
1125            (Witness(4), FieldElement::zero()),
1126            (Witness(5), FieldElement::one()),
1127        ]));
1128
1129        let backend = Bn254BlackBoxSolver;
1130        assert!(validate_witness(&backend, &witness_map, &circuit).is_ok());
1131    }
1132}
acvm/compiler/validator.rs

acvm/compiler/
validator.rs
