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};
9use acir::{
10    AcirField,
11    circuit::{
12        Circuit, Opcode, OpcodeLocation,
13        opcodes::{BlackBoxFuncCall, BlockId, MemOp},
14    },
15    native_types::{Witness, WitnessMap},
16};
17use acvm_blackbox_solver::{
18    BlackBoxFunctionSolver, bit_and, bit_xor, blake2s, blake3, keccakf1600,
19};
20use std::collections::HashMap;
21
22fn unsatisfied_constraint<F>(opcode_index: usize, message: String) -> OpcodeResolutionError<F> {
23    OpcodeResolutionError::UnsatisfiedConstrain {
24        opcode_location: ErrorLocation::Resolved(OpcodeLocation::Acir(opcode_index)),
25        payload: Some(ResolvedAssertionPayload::String(message)),
26    }
27}
28
29fn witness_value<F: AcirField>(
30    w: &Witness,
31    witness_map: &WitnessMap<F>,
32) -> Result<F, OpcodeResolutionError<F>> {
33    Ok(*witness_map.get(w).ok_or(OpcodeNotSolvable::MissingAssignment(w.witness_index()))?)
34}
35
36fn check_fits_in_bits<F: AcirField>(
37    value: F,
38    num_bits: u32,
39    opcode_index: usize,
40    opcode_name: &str,
41) -> Result<(), OpcodeResolutionError<F>> {
42    if value.num_bits() > num_bits {
43        return Err(unsatisfied_constraint(
44            opcode_index,
45            format!(
46                "{opcode_name} opcode violation: value {value} does not fit in {num_bits} bits"
47            ),
48        ));
49    }
50    Ok(())
51}
52
53pub fn validate_witness<F: AcirField>(
54    backend: &impl BlackBoxFunctionSolver<F>,
55    witness_map: WitnessMap<F>,
56    circuit: &Circuit<F>,
57) -> Result<(), OpcodeResolutionError<F>> {
58    let mut block_solvers: HashMap<BlockId, MemoryOpSolver<F>> = HashMap::new();
59
60    for (opcode_index, opcode) in circuit.opcodes.iter().enumerate() {
61        match opcode {
62            Opcode::AssertZero(expression) => {
63                let result = &ExpressionSolver::evaluate(expression, &witness_map);
64                if !result.is_zero() {
65                    return Err(unsatisfied_constraint(
66                        opcode_index,
67                        format!("Invalid witness assignment: {expression}"),
68                    ));
69                }
70            }
71            Opcode::BlackBoxFuncCall(black_box_func_call) => {
72                match black_box_func_call {
73                    BlackBoxFuncCall::AES128Encrypt { inputs, iv, key, outputs } => {
74                        let ciphertext = blackbox::aes128::execute_aes128_encryption_opcode(
75                            &witness_map,
76                            inputs,
77                            iv,
78                            key,
79                        )?;
80                        assert_eq!(outputs.len(), ciphertext.len());
81                        for (output_witness, value) in outputs.iter().zip(ciphertext.into_iter()) {
82                            let witness_value = witness_value(output_witness, &witness_map)?;
83                            let output_value = F::from(u128::from(value));
84                            if witness_value != output_value {
85                                return Err(unsatisfied_constraint(
86                                    opcode_index,
87                                    format!(
88                                        "AES128 opcode violation: expected {output_value} but found {witness_value} for output witness {output_witness}",
89                                    ),
90                                ));
91                            }
92                        }
93                    }
94                    BlackBoxFuncCall::AND { lhs, rhs, num_bits, output } => {
95                        let lhs_value = input_to_value(&witness_map, *lhs)?;
96                        let rhs_value = input_to_value(&witness_map, *rhs)?;
97                        check_fits_in_bits(lhs_value, *num_bits, opcode_index, "AND")?;
98                        check_fits_in_bits(rhs_value, *num_bits, opcode_index, "AND")?;
99                        let and_result = bit_and(lhs_value, rhs_value, *num_bits);
100                        let output_value = witness_map
101                            .get(output)
102                            .ok_or(OpcodeNotSolvable::MissingAssignment(output.0))?;
103                        if and_result != *output_value {
104                            return Err(unsatisfied_constraint(
105                                opcode_index,
106                                format!(
107                                    "AND opcode violation: {lhs_value} AND {rhs_value} != {output_value} for {num_bits} bits"
108                                ),
109                            ));
110                        }
111                    }
112                    BlackBoxFuncCall::XOR { lhs, rhs, num_bits, output } => {
113                        let lhs_value = input_to_value(&witness_map, *lhs)?;
114                        let rhs_value = input_to_value(&witness_map, *rhs)?;
115                        check_fits_in_bits(lhs_value, *num_bits, opcode_index, "XOR")?;
116                        check_fits_in_bits(rhs_value, *num_bits, opcode_index, "XOR")?;
117                        let xor_result = bit_xor(lhs_value, rhs_value, *num_bits);
118                        let output_value = witness_map
119                            .get(output)
120                            .ok_or(OpcodeNotSolvable::MissingAssignment(output.0))?;
121                        if xor_result != *output_value {
122                            return Err(unsatisfied_constraint(
123                                opcode_index,
124                                format!(
125                                    "XOR opcode violation: {lhs_value} XOR {rhs_value} != {output_value} for {num_bits} bits"
126                                ),
127                            ));
128                        }
129                    }
130                    BlackBoxFuncCall::RANGE { input, num_bits } => {
131                        let value = input_to_value(&witness_map, *input)?;
132                        check_fits_in_bits(value, *num_bits, opcode_index, "RANGE")?;
133                    }
134                    BlackBoxFuncCall::Blake2s { inputs, outputs } => {
135                        let message_input = get_hash_input(&witness_map, inputs, None, 8)?;
136                        let digest: [u8; 32] = blake2s(&message_input)?;
137                        for i in 0..32 {
138                            let output_witness = &outputs[i];
139                            let witness_value = witness_map
140                                .get(output_witness)
141                                .ok_or(OpcodeNotSolvable::MissingAssignment(output_witness.0))?;
142                            if *witness_value != F::from_be_bytes_reduce(&[digest[i]]) {
143                                return Err(unsatisfied_constraint(
144                                    opcode_index,
145                                    format!(
146                                        "BLAKE2s opcode violation: expected {:?} but found {:?} for output witness {:?}",
147                                        F::from_be_bytes_reduce(&[digest[i]]),
148                                        witness_value,
149                                        output_witness
150                                    ),
151                                ));
152                            }
153                        }
154                    }
155                    BlackBoxFuncCall::Blake3 { inputs, outputs } => {
156                        let message_input = get_hash_input(&witness_map, inputs, None, 8)?;
157                        let digest: [u8; 32] = blake3(&message_input)?;
158                        for i in 0..32 {
159                            let output_witness = &outputs[i];
160                            let witness_value = witness_value(output_witness, &witness_map)?;
161                            if witness_value != F::from_be_bytes_reduce(&[digest[i]]) {
162                                return Err(unsatisfied_constraint(
163                                    opcode_index,
164                                    format!(
165                                        "BLAKE3 opcode violation: expected {:?} but found {:?} for output witness {:?}",
166                                        F::from_be_bytes_reduce(&[digest[i]]),
167                                        witness_value,
168                                        output_witness
169                                    ),
170                                ));
171                            }
172                        }
173                    }
174                    BlackBoxFuncCall::EcdsaSecp256k1 {
175                        public_key_x,
176                        public_key_y,
177                        signature,
178                        hashed_message,
179                        predicate,
180                        output,
181                    } => {
182                        let predicate_value = input_to_value(&witness_map, *predicate)?.is_one();
183                        if predicate_value {
184                            let is_valid = blackbox::signature::ecdsa::execute_ecdsa(
185                                &witness_map,
186                                public_key_x,
187                                public_key_y,
188                                signature,
189                                hashed_message,
190                                predicate,
191                                true,
192                            )?;
193                            let output_value = witness_value(output, &witness_map)?;
194                            if output_value != F::from(is_valid) {
195                                return Err(unsatisfied_constraint(
196                                    opcode_index,
197                                    format!(
198                                        "EcdsaSecp256k1 opcode violation: expected {:?} but found {:?} for output witness {:?}",
199                                        F::from(is_valid),
200                                        output_value,
201                                        output
202                                    ),
203                                ));
204                            }
205                        }
206                    }
207                    BlackBoxFuncCall::EcdsaSecp256r1 {
208                        public_key_x,
209                        public_key_y,
210                        signature,
211                        hashed_message,
212                        predicate,
213                        output,
214                    } => {
215                        let predicate_value = input_to_value(&witness_map, *predicate)?.is_one();
216                        if predicate_value {
217                            let is_valid = blackbox::signature::ecdsa::execute_ecdsa(
218                                &witness_map,
219                                public_key_x,
220                                public_key_y,
221                                signature,
222                                hashed_message,
223                                predicate,
224                                false,
225                            )?;
226                            let output_value = witness_value(output, &witness_map)?;
227                            if output_value != F::from(is_valid) {
228                                return Err(unsatisfied_constraint(
229                                    opcode_index,
230                                    format!(
231                                        "EcdsaSecp256r1 opcode violation: expected {:?} but found {:?} for output witness {:?}",
232                                        F::from(is_valid),
233                                        output_value,
234                                        output
235                                    ),
236                                ));
237                            }
238                        }
239                    }
240                    BlackBoxFuncCall::MultiScalarMul { points, scalars, predicate, outputs } => {
241                        let predicate_value = input_to_value(&witness_map, *predicate)?.is_one();
242                        if predicate_value {
243                            let (res_x, res_y, res_infinite) = execute_multi_scalar_mul(
244                                backend,
245                                &witness_map,
246                                points,
247                                scalars,
248                                *predicate,
249                            )?;
250                            let output_x_value = witness_value(&outputs.0, &witness_map)?;
251                            let output_y_value = witness_value(&outputs.1, &witness_map)?;
252                            let output_infinite_value = witness_value(&outputs.2, &witness_map)?;
253                            if res_x != output_x_value
254                                || res_y != output_y_value
255                                || res_infinite != output_infinite_value
256                            {
257                                //TODO: should we check x,y values if infinite is true?
258                                return Err(unsatisfied_constraint(
259                                    opcode_index,
260                                    format!(
261                                        "MultiScalarMul opcode violation: expected ({res_x}, {res_y}, {res_infinite}) but found ({output_x_value}, {output_y_value}, {output_infinite_value})"
262                                    ),
263                                ));
264                            }
265                        }
266                    }
267                    BlackBoxFuncCall::EmbeddedCurveAdd { input1, input2, predicate, outputs } => {
268                        let predicate_value = input_to_value(&witness_map, *predicate)?.is_one();
269                        if predicate_value {
270                            let (res_x, res_y, res_infinite) = execute_embedded_curve_add(
271                                backend,
272                                &witness_map,
273                                **input1,
274                                **input2,
275                                *predicate,
276                            )?;
277                            let output_x_value = witness_value(&outputs.0, &witness_map)?;
278                            let output_y_value = witness_value(&outputs.1, &witness_map)?;
279                            let output_infinite_value = witness_value(&outputs.2, &witness_map)?;
280                            if res_x != output_x_value
281                                || res_y != output_y_value
282                                || res_infinite != output_infinite_value
283                            {
284                                //TODO: should we check x,y values if infinite is true?
285                                return Err(unsatisfied_constraint(
286                                    opcode_index,
287                                    format!(
288                                        "EmbeddedCurveAdd opcode violation: expected ({res_x}, {res_y}, {res_infinite}) but found ({output_x_value}, {output_y_value}, {output_infinite_value})"
289                                    ),
290                                ));
291                            }
292                        }
293                    }
294                    BlackBoxFuncCall::Keccakf1600 { inputs, outputs } => {
295                        let mut state = [0; 25];
296                        for (it, input) in state.iter_mut().zip(inputs.as_ref()) {
297                            let witness_assignment = input_to_value(&witness_map, *input)?;
298                            let lane = witness_assignment.try_to_u64();
299                            *it = lane.unwrap();
300                        }
301                        let output_state = keccakf1600(state)?;
302                        for (output_witness, value) in outputs.iter().zip(output_state.into_iter())
303                        {
304                            let witness_value = witness_value(output_witness, &witness_map)?;
305                            if witness_value != F::from(u128::from(value)) {
306                                return Err(unsatisfied_constraint(
307                                    opcode_index,
308                                    format!(
309                                        "Keccakf1600 opcode violation: expected {value} but found {witness_value} for output witness {output_witness}",
310                                    ),
311                                ));
312                            }
313                        }
314                    }
315                    // Recursive aggregation is checked outside of ACVM
316                    BlackBoxFuncCall::RecursiveAggregation { .. } => (),
317                    BlackBoxFuncCall::Poseidon2Permutation { inputs, outputs } => {
318                        let state = blackbox::hash::execute_poseidon2_permutation_opcode(
319                            backend,
320                            &witness_map,
321                            inputs,
322                        )?;
323                        assert_eq!(
324                            outputs.len(),
325                            state.len(),
326                            "Poseidon2Permutation opcode violation: expected {} but found {} results",
327                            state.len(),
328                            outputs.len()
329                        );
330                        for (output_witness, value) in outputs.iter().zip(state.into_iter()) {
331                            let witness_value = witness_map
332                                .get(output_witness)
333                                .ok_or(OpcodeNotSolvable::MissingAssignment(output_witness.0))?;
334                            if *witness_value != value {
335                                return Err(unsatisfied_constraint(
336                                    opcode_index,
337                                    format!(
338                                        "Poseidon2 opcode violation: expected {value} but found {witness_value} for output witness {output_witness}",
339                                    ),
340                                ));
341                            }
342                        }
343                    }
344                    BlackBoxFuncCall::Sha256Compression { inputs, hash_values, outputs } => {
345                        let state = blackbox::hash::execute_sha_256_permutation_opcode(
346                            &witness_map,
347                            inputs,
348                            hash_values,
349                        )?;
350
351                        for (output_witness, value) in outputs.iter().zip(state.into_iter()) {
352                            let witness_value = witness_map
353                                .get(output_witness)
354                                .ok_or(OpcodeNotSolvable::MissingAssignment(output_witness.0))?;
355                            if *witness_value != F::from(u128::from(value)) {
356                                return Err(unsatisfied_constraint(
357                                    opcode_index,
358                                    format!(
359                                        "SHA256 Compression opcode violation: expected {:?} but found {:?} for output witness {:?}",
360                                        F::from(u128::from(value)),
361                                        witness_value,
362                                        output_witness
363                                    ),
364                                ));
365                            }
366                        }
367                    }
368                }
369            }
370            Opcode::MemoryOp { block_id, op } => {
371                let solver = block_solvers
372                    .get_mut(block_id)
373                    .expect("Memory block should have been initialized");
374                solver.check_memory_op(op, &witness_map, opcode_index)?;
375            }
376            Opcode::MemoryInit { block_id, init, .. } => {
377                MemoryOpSolver::new(init, &witness_map).map(|solver| {
378                    let existing_block_id = block_solvers.insert(*block_id, solver);
379                    assert!(existing_block_id.is_none(), "Memory block already initialized");
380                })?;
381            }
382            // BrilligCall is unconstrained
383            Opcode::BrilligCall { .. } => (),
384            Opcode::Call { id: _, inputs, outputs, predicate } => {
385                // Skip validation when predicate is false
386                let pred_value = get_value(predicate, &witness_map)?;
387                if pred_value.is_zero() {
388                    continue;
389                }
390
391                // Verify input witnesses exist
392                for input in inputs {
393                    if witness_map.get(input).is_none() {
394                        return Err(OpcodeNotSolvable::MissingAssignment(input.0).into());
395                    }
396                }
397
398                // Verify output witnesses exist (value should have been validated by the called function)
399                for output in outputs {
400                    if witness_map.get(output).is_none() {
401                        return Err(OpcodeNotSolvable::MissingAssignment(output.0).into());
402                    }
403                }
404            }
405        }
406    }
407
408    Ok(())
409}
410
411impl<F: AcirField> MemoryOpSolver<F> {
412    pub(crate) fn check_memory_op(
413        &mut self,
414        op: &MemOp<F>,
415        witness_map: &WitnessMap<F>,
416        opcode_index: usize,
417    ) -> Result<(), OpcodeResolutionError<F>> {
418        let operation = get_value(&op.operation, witness_map)?;
419
420        // Find the memory index associated with this memory operation.
421        let index = get_value(&op.index, witness_map)?;
422        let memory_index = self.index_from_field(index)?;
423
424        // Calculate the value associated with this memory operation.
425        let value = get_value(&op.value, witness_map)?;
426
427        // `operation == 0` for read operation, `operation == 1` for write operation.
428        let is_read_operation = operation.is_zero();
429
430        if is_read_operation {
431            // `value = arr[memory_index]`
432            let value_in_array = self.read_memory_index(memory_index)?;
433            if value != value_in_array {
434                return Err(unsatisfied_constraint(
435                    opcode_index,
436                    format!(
437                        "Memory read opcode violation at index {memory_index}: expected {value_in_array} but found {value}",
438                    ),
439                ));
440            }
441            Ok(())
442        } else {
443            // `arr[memory_index] = value`
444            self.write_memory_index(memory_index, value)
445        }
446    }
447}
448
449#[cfg(test)]
450mod tests {
451    use std::collections::BTreeMap;
452
453    use acir::{
454        AcirField, FieldElement,
455        circuit::{
456            Circuit, Opcode, PublicInputs,
457            opcodes::{BlackBoxFuncCall, FunctionInput},
458        },
459        native_types::{Expression, Witness, WitnessMap},
460    };
461    use bn254_blackbox_solver::Bn254BlackBoxSolver;
462
463    use super::validate_witness;
464
465    /// Helper to create a simple circuit with the given opcodes
466    fn make_circuit(opcodes: Vec<Opcode<FieldElement>>) -> Circuit<FieldElement> {
467        Circuit {
468            current_witness_index: 10,
469            opcodes,
470            private_parameters: Default::default(),
471            public_parameters: PublicInputs::default(),
472            return_values: PublicInputs::default(),
473            assert_messages: Default::default(),
474            function_name: "test".to_string(),
475        }
476    }
477
478    #[test]
479    fn test_assert_zero_valid() {
480        // w1 + w2 - w3 = 0, where w1=2, w2=3, w3=5
481        let expr = Expression {
482            mul_terms: vec![],
483            linear_combinations: vec![
484                (FieldElement::one(), Witness(1)),
485                (FieldElement::one(), Witness(2)),
486                (-FieldElement::one(), Witness(3)),
487            ],
488            q_c: FieldElement::zero(),
489        };
490
491        let circuit = make_circuit(vec![Opcode::AssertZero(expr)]);
492
493        let witness_map = WitnessMap::from(BTreeMap::from_iter([
494            (Witness(1), FieldElement::from(2u128)),
495            (Witness(2), FieldElement::from(3u128)),
496            (Witness(3), FieldElement::from(5u128)),
497        ]));
498
499        let backend = Bn254BlackBoxSolver;
500        assert!(validate_witness(&backend, witness_map, &circuit).is_ok());
501    }
502
503    #[test]
504    fn test_assert_zero_invalid() {
505        // w1 + w2 - w3 = 0, but w1=2, w2=3, w3=6 (should be 5)
506        let expr = Expression {
507            mul_terms: vec![],
508            linear_combinations: vec![
509                (FieldElement::one(), Witness(1)),
510                (FieldElement::one(), Witness(2)),
511                (-FieldElement::one(), Witness(3)),
512            ],
513            q_c: FieldElement::zero(),
514        };
515
516        let circuit = make_circuit(vec![Opcode::AssertZero(expr)]);
517
518        let witness_map = WitnessMap::from(BTreeMap::from_iter([
519            (Witness(1), FieldElement::from(2u128)),
520            (Witness(2), FieldElement::from(3u128)),
521            (Witness(3), FieldElement::from(6u128)), // Wrong value!
522        ]));
523
524        let backend = Bn254BlackBoxSolver;
525        assert!(validate_witness(&backend, witness_map, &circuit).is_err());
526    }
527
528    #[test]
529    fn test_assert_zero_with_multiplication() {
530        // w1 * w2 - w3 = 0, where w1=3, w2=4, w3=12
531        let expr = Expression {
532            mul_terms: vec![(FieldElement::one(), Witness(1), Witness(2))],
533            linear_combinations: vec![(-FieldElement::one(), Witness(3))],
534            q_c: FieldElement::zero(),
535        };
536
537        let circuit = make_circuit(vec![Opcode::AssertZero(expr)]);
538
539        let witness_map = WitnessMap::from(BTreeMap::from_iter([
540            (Witness(1), FieldElement::from(3u128)),
541            (Witness(2), FieldElement::from(4u128)),
542            (Witness(3), FieldElement::from(12u128)),
543        ]));
544
545        let backend = Bn254BlackBoxSolver;
546        assert!(validate_witness(&backend, witness_map, &circuit).is_ok());
547    }
548
549    #[test]
550    fn test_range_valid() {
551        // w1 should fit in 8 bits
552        let circuit = make_circuit(vec![Opcode::BlackBoxFuncCall(BlackBoxFuncCall::RANGE {
553            input: FunctionInput::Witness(Witness(1)),
554            num_bits: 8,
555        })]);
556
557        let witness_map = WitnessMap::from(BTreeMap::from_iter([
558            (Witness(1), FieldElement::from(255u128)), // Max 8-bit value
559        ]));
560
561        let backend = Bn254BlackBoxSolver;
562        assert!(validate_witness(&backend, witness_map, &circuit).is_ok());
563    }
564
565    #[test]
566    fn test_range_invalid() {
567        // w1 should fit in 8 bits, but 256 doesn't
568        let circuit = make_circuit(vec![Opcode::BlackBoxFuncCall(BlackBoxFuncCall::RANGE {
569            input: FunctionInput::Witness(Witness(1)),
570            num_bits: 8,
571        })]);
572
573        let witness_map = WitnessMap::from(BTreeMap::from_iter([
574            (Witness(1), FieldElement::from(256u128)), // Too large for 8 bits
575        ]));
576
577        let backend = Bn254BlackBoxSolver;
578        assert!(validate_witness(&backend, witness_map, &circuit).is_err());
579    }
580
581    #[test]
582    fn test_and_valid() {
583        // w1 AND w2 = w3, where w1=0b1010, w2=0b1100, w3=0b1000
584        let circuit = make_circuit(vec![Opcode::BlackBoxFuncCall(BlackBoxFuncCall::AND {
585            lhs: FunctionInput::Witness(Witness(1)),
586            rhs: FunctionInput::Witness(Witness(2)),
587            num_bits: 8,
588            output: Witness(3),
589        })]);
590
591        let witness_map = WitnessMap::from(BTreeMap::from_iter([
592            (Witness(1), FieldElement::from(0b1010u128)),
593            (Witness(2), FieldElement::from(0b1100u128)),
594            (Witness(3), FieldElement::from(0b1000u128)),
595        ]));
596
597        let backend = Bn254BlackBoxSolver;
598        assert!(validate_witness(&backend, witness_map, &circuit).is_ok());
599    }
600
601    #[test]
602    fn test_and_invalid() {
603        // w1 AND w2 = w3, but w3 has wrong value
604        let circuit = make_circuit(vec![Opcode::BlackBoxFuncCall(BlackBoxFuncCall::AND {
605            lhs: FunctionInput::Witness(Witness(1)),
606            rhs: FunctionInput::Witness(Witness(2)),
607            num_bits: 8,
608            output: Witness(3),
609        })]);
610
611        let witness_map = WitnessMap::from(BTreeMap::from_iter([
612            (Witness(1), FieldElement::from(0b1010u128)),
613            (Witness(2), FieldElement::from(0b1100u128)),
614            (Witness(3), FieldElement::from(0b1111u128)), // Wrong!
615        ]));
616
617        let backend = Bn254BlackBoxSolver;
618        assert!(validate_witness(&backend, witness_map, &circuit).is_err());
619    }
620
621    #[test]
622    fn test_xor_valid() {
623        // w1 XOR w2 = w3, where w1=0b1010, w2=0b1100, w3=0b0110
624        let circuit = make_circuit(vec![Opcode::BlackBoxFuncCall(BlackBoxFuncCall::XOR {
625            lhs: FunctionInput::Witness(Witness(1)),
626            rhs: FunctionInput::Witness(Witness(2)),
627            num_bits: 8,
628            output: Witness(3),
629        })]);
630
631        let witness_map = WitnessMap::from(BTreeMap::from_iter([
632            (Witness(1), FieldElement::from(0b1010u128)),
633            (Witness(2), FieldElement::from(0b1100u128)),
634            (Witness(3), FieldElement::from(0b0110u128)),
635        ]));
636
637        let backend = Bn254BlackBoxSolver;
638        assert!(validate_witness(&backend, witness_map, &circuit).is_ok());
639    }
640
641    #[test]
642    fn test_xor_invalid() {
643        // w1 XOR w2 = w3, but w3 has wrong value
644        let circuit = make_circuit(vec![Opcode::BlackBoxFuncCall(BlackBoxFuncCall::XOR {
645            lhs: FunctionInput::Witness(Witness(1)),
646            rhs: FunctionInput::Witness(Witness(2)),
647            num_bits: 8,
648            output: Witness(3),
649        })]);
650
651        let witness_map = WitnessMap::from(BTreeMap::from_iter([
652            (Witness(1), FieldElement::from(0b1010u128)),
653            (Witness(2), FieldElement::from(0b1100u128)),
654            (Witness(3), FieldElement::from(0b1111u128)), // Wrong!
655        ]));
656
657        let backend = Bn254BlackBoxSolver;
658        assert!(validate_witness(&backend, witness_map, &circuit).is_err());
659    }
660
661    #[test]
662    fn test_missing_witness_in_expression() {
663        let expr = Expression {
664            mul_terms: vec![],
665            linear_combinations: vec![(FieldElement::one(), Witness(1))],
666            q_c: FieldElement::zero(),
667        };
668
669        let circuit = make_circuit(vec![Opcode::AssertZero(expr)]);
670
671        // Empty witness map - missing w1
672        let witness_map = WitnessMap::default();
673
674        let backend = Bn254BlackBoxSolver;
675        // The expression evaluates with missing witness, but won't be zero
676        // so this should fail
677        assert!(validate_witness(&backend, witness_map, &circuit).is_err());
678    }
679
680    #[test]
681    fn test_call_opcode_valid() {
682        use acir::circuit::opcodes::AcirFunctionId;
683
684        let circuit = make_circuit(vec![Opcode::Call {
685            id: AcirFunctionId(1),
686            inputs: vec![Witness(1), Witness(2)],
687            outputs: vec![Witness(3)],
688            predicate: Expression::one(),
689        }]);
690
691        let witness_map = WitnessMap::from(BTreeMap::from_iter([
692            (Witness(1), FieldElement::from(1u128)),
693            (Witness(2), FieldElement::from(2u128)),
694            (Witness(3), FieldElement::from(3u128)),
695        ]));
696
697        let backend = Bn254BlackBoxSolver;
698        assert!(validate_witness(&backend, witness_map, &circuit).is_ok());
699    }
700
701    #[test]
702    fn test_call_opcode_missing_input() {
703        use acir::circuit::opcodes::AcirFunctionId;
704
705        let circuit = make_circuit(vec![Opcode::Call {
706            id: AcirFunctionId(1),
707            inputs: vec![Witness(1), Witness(2)],
708            outputs: vec![Witness(3)],
709            predicate: Expression::one(),
710        }]);
711
712        // Missing Witness(2)
713        let witness_map = WitnessMap::from(BTreeMap::from_iter([
714            (Witness(1), FieldElement::from(1u128)),
715            (Witness(3), FieldElement::from(3u128)),
716        ]));
717
718        let backend = Bn254BlackBoxSolver;
719        assert!(validate_witness(&backend, witness_map, &circuit).is_err());
720    }
721
722    #[test]
723    fn test_call_opcode_missing_output() {
724        use acir::circuit::opcodes::AcirFunctionId;
725
726        let circuit = make_circuit(vec![Opcode::Call {
727            id: AcirFunctionId(1),
728            inputs: vec![Witness(1), Witness(2)],
729            outputs: vec![Witness(3)],
730            predicate: Expression::one(),
731        }]);
732
733        // Missing Witness(3) output
734        let witness_map = WitnessMap::from(BTreeMap::from_iter([
735            (Witness(1), FieldElement::from(1u128)),
736            (Witness(2), FieldElement::from(2u128)),
737        ]));
738
739        let backend = Bn254BlackBoxSolver;
740        assert!(validate_witness(&backend, witness_map, &circuit).is_err());
741    }
742
743    #[test]
744    fn test_call_opcode_skipped_with_zero_predicate() {
745        use acir::circuit::opcodes::AcirFunctionId;
746
747        // Predicate is zero, so call should be skipped even with missing witnesses
748        let circuit = make_circuit(vec![Opcode::Call {
749            id: AcirFunctionId(1),
750            inputs: vec![Witness(1), Witness(2)],
751            outputs: vec![Witness(3)],
752            predicate: Expression {
753                mul_terms: vec![],
754                linear_combinations: vec![(FieldElement::one(), Witness(4))],
755                q_c: FieldElement::zero(),
756            },
757        }]);
758
759        // Witness(4) = 0, so predicate is false, call is skipped
760        // Missing input/output witnesses should not cause an error
761        let witness_map =
762            WitnessMap::from(BTreeMap::from_iter([(Witness(4), FieldElement::zero())]));
763
764        let backend = Bn254BlackBoxSolver;
765        assert!(validate_witness(&backend, witness_map, &circuit).is_ok());
766    }
767
768    #[test]
769    fn test_memory_init_and_read() {
770        use acir::circuit::opcodes::{BlockId, MemOp};
771
772        let block_id = BlockId(0);
773
774        let circuit = make_circuit(vec![
775            // Initialize memory block with witnesses 1 and 2
776            Opcode::MemoryInit {
777                block_id,
778                init: vec![Witness(1), Witness(2)],
779                block_type: acir::circuit::opcodes::BlockType::Memory,
780            },
781            // Read from index 0 into witness 3
782            Opcode::MemoryOp {
783                block_id,
784                op: MemOp::read_at_mem_index(FieldElement::zero().into(), Witness(3)),
785            },
786        ]);
787
788        let witness_map = WitnessMap::from(BTreeMap::from_iter([
789            (Witness(1), FieldElement::from(42u128)),
790            (Witness(2), FieldElement::from(43u128)),
791            (Witness(3), FieldElement::from(42u128)), // Should match value at index 0
792        ]));
793
794        let backend = Bn254BlackBoxSolver;
795        assert!(validate_witness(&backend, witness_map, &circuit).is_ok());
796    }
797
798    #[test]
799    fn test_memory_read_wrong_value() {
800        use acir::circuit::opcodes::{BlockId, MemOp};
801
802        let block_id = BlockId(0);
803
804        let circuit = make_circuit(vec![
805            Opcode::MemoryInit {
806                block_id,
807                init: vec![Witness(1), Witness(2)],
808                block_type: acir::circuit::opcodes::BlockType::Memory,
809            },
810            Opcode::MemoryOp {
811                block_id,
812                op: MemOp::read_at_mem_index(FieldElement::zero().into(), Witness(3)),
813            },
814        ]);
815
816        let witness_map = WitnessMap::from(BTreeMap::from_iter([
817            (Witness(1), FieldElement::from(42u128)),
818            (Witness(2), FieldElement::from(43u128)),
819            (Witness(3), FieldElement::from(99u128)), // Wrong! Should be 42
820        ]));
821
822        let backend = Bn254BlackBoxSolver;
823        assert!(validate_witness(&backend, witness_map, &circuit).is_err());
824    }
825
826    #[test]
827    fn test_memory_write_then_read() {
828        use acir::circuit::opcodes::{BlockId, MemOp};
829
830        let block_id = BlockId(0);
831
832        let circuit = make_circuit(vec![
833            // Initialize memory block
834            Opcode::MemoryInit {
835                block_id,
836                init: vec![Witness(1), Witness(2)],
837                block_type: acir::circuit::opcodes::BlockType::Memory,
838            },
839            // Write value from witness 3 to index 0
840            Opcode::MemoryOp {
841                block_id,
842                op: MemOp::write_to_mem_index(FieldElement::zero().into(), Witness(3).into()),
843            },
844            // Read from index 0 into witness 4
845            Opcode::MemoryOp {
846                block_id,
847                op: MemOp::read_at_mem_index(FieldElement::zero().into(), Witness(4)),
848            },
849        ]);
850
851        let witness_map = WitnessMap::from(BTreeMap::from_iter([
852            (Witness(1), FieldElement::from(42u128)), // Initial value at index 0
853            (Witness(2), FieldElement::from(43u128)), // Initial value at index 1
854            (Witness(3), FieldElement::from(100u128)), // Value to write
855            (Witness(4), FieldElement::from(100u128)), // Read should get written value
856        ]));
857
858        let backend = Bn254BlackBoxSolver;
859        assert!(validate_witness(&backend, witness_map, &circuit).is_ok());
860    }
861
862    #[test]
863    fn test_brillig_call_with_empty_witness_map() {
864        use acir::circuit::brillig::{BrilligFunctionId, BrilligInputs, BrilligOutputs};
865
866        // Create a BrilligCall opcode with input and output witnesses
867        // Brillig calls are unconstrained and should be skipped during validation,
868        // so this should pass even with an empty witness map
869        let circuit = make_circuit(vec![Opcode::BrilligCall {
870            id: BrilligFunctionId(0),
871            inputs: vec![
872                BrilligInputs::Single(Witness(1).into()),
873                BrilligInputs::Single(Witness(2).into()),
874            ],
875            outputs: vec![BrilligOutputs::Simple(Witness(3))],
876            predicate: Expression::one(),
877        }]);
878
879        // Empty witness map
880        let witness_map = WitnessMap::default();
881
882        let backend = Bn254BlackBoxSolver;
883        assert!(validate_witness(&backend, witness_map, &circuit).is_ok());
884    }
885}
acvm/compiler/validator.rs

acvm/compiler/
validator.rs
