Skip to content

Commit a5b96a8

Browse files
asteriteasterite
committed
Merge branch 'master' into ab/uhashmap-fixes
2 parents 9d64831 + fb8c60e commit a5b96a8

16 files changed

Lines changed: 393 additions & 72 deletions

File tree

‎acvm-repo/acvm/src/compiler/validator.rs‎

Lines changed: 93 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -367,10 +367,14 @@ pub fn validate_witness<F: AcirField>(
367367
solver.check_memory_op(op, &witness_map, opcode_index)?;
368368
}
369369
Opcode::MemoryInit { block_id, init, .. } => {
370-
MemoryOpSolver::new(init, &witness_map).map(|solver| {
371-
let existing_block_id = block_solvers.insert(*block_id, solver);
372-
assert!(existing_block_id.is_none(), "Memory block already initialized");
373-
})?;
370+
let solver = MemoryOpSolver::new(init, &witness_map)?;
371+
let existing_block_id = block_solvers.insert(*block_id, solver);
372+
if existing_block_id.is_some() {
373+
return Err(unsatisfied_constraint(
374+
opcode_index,
375+
format!("Attempted reinitialization of memory block {:?}", block_id.0,),
376+
));
377+
}
374378
}
375379
// BrilligCall is unconstrained
376380
Opcode::BrilligCall { .. } => (),
@@ -443,14 +447,32 @@ mod tests {
443447
use acir::{
444448
AcirField, FieldElement,
445449
circuit::{
446-
Circuit, Opcode, PublicInputs,
447-
opcodes::{BlackBoxFuncCall, FunctionInput},
450+
Circuit, Opcode, OpcodeLocation, PublicInputs,
451+
brillig::{BrilligFunctionId, BrilligInputs, BrilligOutputs},
452+
opcodes::{AcirFunctionId, BlackBoxFuncCall, BlockId, FunctionInput, MemOp},
448453
},
449454
native_types::{Expression, Witness, WitnessMap},
450455
};
451456
use bn254_blackbox_solver::Bn254BlackBoxSolver;
452457

453458
use super::validate_witness;
459+
use crate::pwg::{
460+
ErrorLocation, OpcodeNotSolvable, OpcodeResolutionError, ResolvedAssertionPayload,
461+
};
462+
463+
fn assert_unsatisfied_constraint(
464+
result: Result<(), OpcodeResolutionError<FieldElement>>,
465+
opcode_index: usize,
466+
message: &str,
467+
) {
468+
assert_eq!(
469+
result.unwrap_err(),
470+
OpcodeResolutionError::UnsatisfiedConstrain {
471+
opcode_location: ErrorLocation::Resolved(OpcodeLocation::Acir(opcode_index)),
472+
payload: Some(ResolvedAssertionPayload::String(message.to_string())),
473+
},
474+
);
475+
}
454476

455477
/// Helper to create a simple circuit with the given opcodes
456478
fn make_circuit(opcodes: Vec<Opcode<FieldElement>>) -> Circuit<FieldElement> {
@@ -511,7 +533,11 @@ mod tests {
511533
]));
512534

513535
let backend = Bn254BlackBoxSolver;
514-
assert!(validate_witness(&backend, witness_map, &circuit).is_err());
536+
assert_unsatisfied_constraint(
537+
validate_witness(&backend, witness_map, &circuit),
538+
0,
539+
"Invalid witness assignment: w1 + w2 - w3",
540+
);
515541
}
516542

517543
#[test]
@@ -564,7 +590,11 @@ mod tests {
564590
]));
565591

566592
let backend = Bn254BlackBoxSolver;
567-
assert!(validate_witness(&backend, witness_map, &circuit).is_err());
593+
assert_unsatisfied_constraint(
594+
validate_witness(&backend, witness_map, &circuit),
595+
0,
596+
"RANGE opcode violation: value 256 does not fit in 8 bits",
597+
);
568598
}
569599

570600
#[test]
@@ -604,7 +634,11 @@ mod tests {
604634
]));
605635

606636
let backend = Bn254BlackBoxSolver;
607-
assert!(validate_witness(&backend, witness_map, &circuit).is_err());
637+
assert_unsatisfied_constraint(
638+
validate_witness(&backend, witness_map, &circuit),
639+
0,
640+
"AND opcode violation: 10 AND 12 != 15 for 8 bits",
641+
);
608642
}
609643

610644
#[test]
@@ -644,7 +678,11 @@ mod tests {
644678
]));
645679

646680
let backend = Bn254BlackBoxSolver;
647-
assert!(validate_witness(&backend, witness_map, &circuit).is_err());
681+
assert_unsatisfied_constraint(
682+
validate_witness(&backend, witness_map, &circuit),
683+
0,
684+
"XOR opcode violation: 10 XOR 12 != 15 for 8 bits",
685+
);
648686
}
649687

650688
#[test]
@@ -661,15 +699,15 @@ mod tests {
661699
let witness_map = WitnessMap::default();
662700

663701
let backend = Bn254BlackBoxSolver;
664-
// The expression evaluates with missing witness, but won't be zero
665-
// so this should fail
666-
assert!(validate_witness(&backend, witness_map, &circuit).is_err());
702+
assert_unsatisfied_constraint(
703+
validate_witness(&backend, witness_map, &circuit),
704+
0,
705+
"Invalid witness assignment: w1",
706+
);
667707
}
668708

669709
#[test]
670710
fn test_call_opcode_valid() {
671-
use acir::circuit::opcodes::AcirFunctionId;
672-
673711
let circuit = make_circuit(vec![Opcode::Call {
674712
id: AcirFunctionId(1),
675713
inputs: vec![Witness(1), Witness(2)],
@@ -689,8 +727,6 @@ mod tests {
689727

690728
#[test]
691729
fn test_call_opcode_missing_input() {
692-
use acir::circuit::opcodes::AcirFunctionId;
693-
694730
let circuit = make_circuit(vec![Opcode::Call {
695731
id: AcirFunctionId(1),
696732
inputs: vec![Witness(1), Witness(2)],
@@ -705,13 +741,14 @@ mod tests {
705741
]));
706742

707743
let backend = Bn254BlackBoxSolver;
708-
assert!(validate_witness(&backend, witness_map, &circuit).is_err());
744+
assert_eq!(
745+
validate_witness(&backend, witness_map, &circuit).unwrap_err(),
746+
OpcodeResolutionError::OpcodeNotSolvable(OpcodeNotSolvable::MissingAssignment(2)),
747+
);
709748
}
710749

711750
#[test]
712751
fn test_call_opcode_missing_output() {
713-
use acir::circuit::opcodes::AcirFunctionId;
714-
715752
let circuit = make_circuit(vec![Opcode::Call {
716753
id: AcirFunctionId(1),
717754
inputs: vec![Witness(1), Witness(2)],
@@ -726,13 +763,14 @@ mod tests {
726763
]));
727764

728765
let backend = Bn254BlackBoxSolver;
729-
assert!(validate_witness(&backend, witness_map, &circuit).is_err());
766+
assert_eq!(
767+
validate_witness(&backend, witness_map, &circuit).unwrap_err(),
768+
OpcodeResolutionError::OpcodeNotSolvable(OpcodeNotSolvable::MissingAssignment(3)),
769+
);
730770
}
731771

732772
#[test]
733773
fn test_call_opcode_skipped_with_zero_predicate() {
734-
use acir::circuit::opcodes::AcirFunctionId;
735-
736774
// Predicate is zero, so call should be skipped even with missing witnesses
737775
let circuit = make_circuit(vec![Opcode::Call {
738776
id: AcirFunctionId(1),
@@ -756,8 +794,6 @@ mod tests {
756794

757795
#[test]
758796
fn test_memory_init_and_read() {
759-
use acir::circuit::opcodes::{BlockId, MemOp};
760-
761797
let block_id = BlockId(0);
762798

763799
let circuit = make_circuit(vec![
@@ -784,8 +820,6 @@ mod tests {
784820

785821
#[test]
786822
fn test_memory_read_wrong_value() {
787-
use acir::circuit::opcodes::{BlockId, MemOp};
788-
789823
let block_id = BlockId(0);
790824

791825
let circuit = make_circuit(vec![
@@ -805,13 +839,15 @@ mod tests {
805839
]));
806840

807841
let backend = Bn254BlackBoxSolver;
808-
assert!(validate_witness(&backend, witness_map, &circuit).is_err());
842+
assert_unsatisfied_constraint(
843+
validate_witness(&backend, witness_map, &circuit),
844+
1,
845+
"Memory read opcode violation at index 0: expected 42 but found 99",
846+
);
809847
}
810848

811849
#[test]
812850
fn test_memory_write_then_read() {
813-
use acir::circuit::opcodes::{BlockId, MemOp};
814-
815851
let block_id = BlockId(0);
816852

817853
let circuit = make_circuit(vec![
@@ -841,8 +877,6 @@ mod tests {
841877

842878
#[test]
843879
fn test_brillig_call_with_empty_witness_map() {
844-
use acir::circuit::brillig::{BrilligFunctionId, BrilligInputs, BrilligOutputs};
845-
846880
// Create a BrilligCall opcode with input and output witnesses
847881
// Brillig calls are unconstrained and should be skipped during validation,
848882
// so this should pass even with an empty witness map
@@ -862,4 +896,31 @@ mod tests {
862896
let backend = Bn254BlackBoxSolver;
863897
assert!(validate_witness(&backend, witness_map, &circuit).is_ok());
864898
}
899+
900+
#[test]
901+
fn error_on_memory_init_duplicate_block_id() {
902+
let block_id = BlockId(0);
903+
904+
let circuit = make_circuit(vec![
905+
Opcode::MemoryInit {
906+
block_id,
907+
init: vec![],
908+
block_type: acir::circuit::opcodes::BlockType::Memory,
909+
},
910+
Opcode::MemoryInit {
911+
block_id,
912+
init: vec![],
913+
block_type: acir::circuit::opcodes::BlockType::Memory,
914+
},
915+
]);
916+
917+
let witness_map = WitnessMap::default();
918+
let backend = Bn254BlackBoxSolver;
919+
920+
assert_unsatisfied_constraint(
921+
validate_witness(&backend, witness_map, &circuit),
922+
1,
923+
format!("Attempted reinitialization of memory block {}", block_id.0).as_str(),
924+
);
925+
}
865926
}

‎compiler/noirc_evaluator/src/ssa/interpreter/mod.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1379,7 +1379,7 @@ impl<'ssa, W: Write> Interpreter<'ssa, W> {
13791379
elements.iter().zip(element_types.iter().cycle()).enumerate()
13801380
{
13811381
let actual_type = element.get_type();
1382-
if &actual_type != expected_type {
1382+
if !actual_type.canonical_eq(expected_type) {
13831383
return Err(internal(InternalError::MakeArrayElementTypeMismatch {
13841384
result,
13851385
index,

‎compiler/noirc_evaluator/src/ssa/interpreter/tests/instructions.rs‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1161,6 +1161,31 @@ fn make_array() {
11611161
assert_eq!(values[3], Value::vector(hello, Arc::new(vec![Type::char()])));
11621162
}
11631163

1164+
#[test]
1165+
fn make_array_allows_reference_mutability_mismatch() {
1166+
// Reference mutability is a frontend concern with no meaning at the SSA
1167+
// level: the validator accepts a `&mut T` value in a `&T` MakeArray slot,
1168+
// and the interpreter must agree so that running the post-validation SSA
1169+
// doesn't fail with `MakeArrayElementTypeMismatch`. The unconstrained
1170+
// SSA-gen pattern this guards is a tuple `[&mut T, &T]` constructed from
1171+
// a mutable allocate alongside an immutable one — exactly what the
1172+
// `pass_vs_prev` fuzzer surfaces when it interprets intermediate SSA
1173+
// between passes.
1174+
executes_with_no_errors(
1175+
"
1176+
brillig(inline) fn main f0 {
1177+
b0():
1178+
v0 = allocate -> &mut Field
1179+
store Field 1 at v0
1180+
v1 = allocate -> &Field
1181+
store Field 2 at v1
1182+
v2 = make_array [v0, v1] : [&Field; 2]
1183+
return
1184+
}
1185+
",
1186+
);
1187+
}
1188+
11641189
#[test]
11651190
fn nop() {
11661191
executes_with_no_errors(

‎compiler/noirc_evaluator/src/ssa/validation/mod.rs‎

Lines changed: 66 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -315,7 +315,7 @@ impl<'f> Validator<'f> {
315315
};
316316

317317
let value_type = dfg.type_of_value(*value);
318-
if **address_value_type != *value_type {
318+
if !address_value_type.canonical_eq(&value_type) {
319319
panic!(
320320
"Store address type {address_value_type} does not match value type {value_type}"
321321
);
@@ -1203,17 +1203,21 @@ impl<'f> Validator<'f> {
12031203
};
12041204
let result = dfg.instruction_results(instruction)[0];
12051205
let result_type = dfg.type_of_value(result);
1206-
if *result_type != *expected_type {
1207-
panic!("load should return {expected_type}, not {result_type}");
1206+
if !result_type.canonical_eq(expected_type) {
1207+
panic!(
1208+
"load should return {expected_type}, not {result_type}; address = {address}, result = {result}"
1209+
);
12081210
}
12091211
}
12101212
Instruction::Store { address, value } => {
12111213
let Some(expected_type) = self.allocate_element_types.get(address) else {
12121214
return;
12131215
};
12141216
let value_type = dfg.type_of_value(*value);
1215-
if *value_type != *expected_type {
1216-
panic!("store value should have type {expected_type}, not {value_type}");
1217+
if !value_type.canonical_eq(expected_type) {
1218+
panic!(
1219+
"store value should have type {expected_type}, not {value_type}; address = {address}, value = {value}"
1220+
);
12171221
}
12181222
}
12191223
_ => (),
@@ -2103,6 +2107,63 @@ mod tests {
21032107
let _ = Ssa::from_str(src).unwrap();
21042108
}
21052109

2110+
#[test]
2111+
fn store_allows_reference_mutability_mismatch() {
2112+
// Reference mutability is a frontend concern with no meaning at the SSA
2113+
// level, so a `&mut Field` value is accepted at a `&mut &Field` slot
2114+
// (and vice versa). The minimal SSA-gen pattern this guards is an
2115+
// assignment like `b.1 = &b.0` inside an unconstrained mutable tuple:
2116+
// the slot is allocated as `&mut &T` while the right-hand side carries
2117+
// `&mut T` because `b.0` itself lives in a mutable binding.
2118+
let src = "
2119+
acir(inline) fn main f0 {
2120+
b0():
2121+
v0 = allocate -> &mut Field
2122+
v1 = allocate -> &mut &Field
2123+
store v0 at v1
2124+
return
2125+
}
2126+
";
2127+
let _ = Ssa::from_str(src).unwrap();
2128+
2129+
let src = "
2130+
acir(inline) fn main f0 {
2131+
b0():
2132+
v0 = allocate -> &Field
2133+
v1 = allocate -> &mut &mut Field
2134+
store v0 at v1
2135+
return
2136+
}
2137+
";
2138+
let _ = Ssa::from_str(src).unwrap();
2139+
}
2140+
2141+
#[test]
2142+
fn load_allows_reference_mutability_mismatch() {
2143+
// The Load path mirrors the Store path: when an Allocate's recorded
2144+
// element type only differs from the Load result type by reference
2145+
// mutability we must accept it.
2146+
let src = "
2147+
acir(inline) fn main f0 {
2148+
b0():
2149+
v0 = allocate -> &mut &mut Field
2150+
v1 = load v0 -> &Field
2151+
return
2152+
}
2153+
";
2154+
let _ = Ssa::from_str(src).unwrap();
2155+
2156+
let src = "
2157+
acir(inline) fn main f0 {
2158+
b0():
2159+
v0 = allocate -> &mut &Field
2160+
v1 = load v0 -> &mut Field
2161+
return
2162+
}
2163+
";
2164+
let _ = Ssa::from_str(src).unwrap();
2165+
}
2166+
21062167
#[test]
21072168
#[should_panic(expected = "store value should have type u8, not Field")]
21082169
fn store_has_incorrect_type() {

0 commit comments

Comments
 (0)