Skip to content

feat(fuzz): Generate arbitrary constraints#8820

Merged
aakoshh merged 12 commits intomasterfrom
af/7932-fuzz-constraint
Jun 9, 2025
Merged

feat(fuzz): Generate arbitrary constraints#8820
aakoshh merged 12 commits intomasterfrom
af/7932-fuzz-constraint

Conversation

@aakoshh
Copy link
Contributor

@aakoshh aakoshh commented Jun 6, 2025

Description

Problem*

Resolves #7932

Summary*

Generate arbitrary constraints in the AST fuzzer. Using a low frequency so not every execution results in constraint failure.

Changed the AST printer to show assert instead of the deprecated constrain keyword, and display the message as well. Also added the message to the SSA interpreter to make it easier to find which constraint caused the failure.

Additional Context

I noticed during testing that the SSA changes the types it runs the constraints on, and thus their display value as well:

both programs failed:
constrain v37 == v38, "TBF" failed:
    Field 313339671284855045676773137498590239475 != Field 0
!=
constrain v49 == v42, "TBF" failed:
    u128 313339671284855045676773137498590239475 != u128 0

and

both programs failed:
constrain v86 == v94, "ISC" failed:
    i64 -1615928006 != i64 -5568658583620095790
!=
constrain v89 == v91, "ISC" failed:
    u64 18446744072093623610 != u64 12878085490089455826

I modified the Comparable implementation of the fuzzer to only look at the message, which I added to the interpreter, and ignore the LHS and RHS values, but I do wonder if we trust that a constraint cannot accidentally fail or pass after casting. As long as casting doesn't change the value, I guess it should be okay.

Documentation*

Check one:

  • No documentation needed.
  • Documentation included in this PR.
  • [For Experimental Features] Documentation to be submitted in a separate PR.

PR Checklist*

  • I have tested the changes locally.
  • I have formatted the changes with Prettier and/or cargo fmt on default settings.

Copy link
Contributor

@github-actions github-actions bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Test Suite Duration'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.20.

Benchmark suite Current: 3eb9616 Previous: f0d3d05 Ratio
test_report_zkpassport_noir_rsa_ 2 s 1 s 2

This comment was automatically generated by workflow using github-action-benchmark.

CC: @TomAFrench

@aakoshh aakoshh marked this pull request as ready for review June 6, 2025 12:06
@aakoshh aakoshh requested review from a team and rkarabut June 6, 2025 12:15
@asterite
Copy link
Collaborator

asterite commented Jun 6, 2025

I noticed during testing that the SSA changes the types it runs the constraints on

Do you know where this specifically happens? I wonder why it would do that.

@aakoshh aakoshh changed the title chore(fuzz): Generate arbitrary constraints feat(fuzz): Generate arbitrary constraints Jun 6, 2025
@aakoshh
Copy link
Contributor Author

aakoshh commented Jun 6, 2025

Do you know where this specifically happens? I wonder why it would do that.

@asterite yes, I still have the programs.

This is the first example
both programs failed: constrain v37 == v38 failed:
    Field 313339671284855045676773137498590239475 != Field 0 vs constrain v49 == v42 failed:
    u128 313339671284855045676773137498590239475 != u128 0
ConstrainEqFailed { lhs: "Field 313339671284855045676773137498590239475", lhs_id: Id(37), rhs: "Field 0", rhs_id: Id(38) }
ConstrainEqFailed { lhs: "u128 313339671284855045676773137498590239475", lhs_id: Id(49), rhs: "u128 0", rhs_id: Id(42) }
---
AST:
global G_A: (u128, [u128; 4], u128) = (68208882519879340829571110414913265451, [141888941893519431495522585334882459772, 78664061307629166694964766019303350777, 229134125080636816429820510416098134851, 246078571536640381569468433466924145168], 281409297734408019540110123275768005705);
global G_B: (u128, [u128; 4], u128) = (178029683271752409168712264797707897684, [35866632039212972075956128730669589847, 278054022342325001852341960081092635767, 40681105989194200543378816448734657328, 250932207057346960404143633361483230010], 125258613224863982175369866539999860115);
global G_C: (u128, [u128; 4], u128) = (213179355600187091451936113944275672394, [182513327886107005623960248002248608728, 185957822557510044736822223600828066861, 144677471795148236097787822081537003656, 158093617099024924450744857034507273574], 35670510297322539680268656225144565474);
fn main(a: call_data(0) u128) -> pub [u128; 4] {
    let mut ctx_limit: u32 = 25;
    assert(((-(G_A.2 as Field)) != if (308881631317704773594667179532684006218 <= 61954629961209201901039865518057240291) {
        (unsafe { func_1_proxy(ctx_limit) }.0 as Field)
    } else {
        (G_B.0 as Field)
    }), "ONL");
    assert(((unsafe { func_1_proxy(ctx_limit) }.1 as Field) == (a as Field)), "TBF");
    for idx_b in 49221 .. 49221 {
        assert(((idx_b as u64) == 3986093456026514159), "OIW");
        let mut c = unsafe { func_2_proxy(a, ctx_limit) }.1.2;
    };
    assert((if unsafe { func_2_proxy(301767583745950347814793913572654123192, ctx_limit) }.1.2 {
        a
    } else {
        G_C.2
    } <= if false {
        if false {
            unsafe { func_1_proxy(ctx_limit) }.0
        } else {
            G_A.1[(3863486974 % 4)]
        }
    } else {
        unsafe { func_1_proxy(ctx_limit) }.1
    }), "CYM");
    {
        let mut d: u32 = 815285805;
        G_A.1
    }
}
unconstrained fn func_1(ctx_limit: &mut u32) -> (u128, u128) {
    if ((*ctx_limit) == 0) {
        (211973039370314431325298847511786466703, 313339671284855045676773137498590239475)
    } else {
        *ctx_limit = ((*ctx_limit) - 1);
        func_1(ctx_limit)
    }
}
unconstrained fn func_2(a: u128, _ctx_limit: &mut u32) -> ([u128; 4], (u128, u128, bool)) {
    ([154393597273046183284570645816597213555, 316114973126160255290652647137746813821, 309369013611773294078320911237563905555, 246773502993923634916978827225769168813], (45323974457163427869295425299351676299, 124837267636409002259242427137493810431, false))
}
unconstrained fn func_1_proxy(mut ctx_limit: u32) -> (u128, u128) {
    func_1((&mut ctx_limit))
}
unconstrained fn func_2_proxy(a: u128, mut ctx_limit: u32) -> ([u128; 4], (u128, u128, bool)) {
    func_2(a, (&mut ctx_limit))
}

---
ABI Inputs:
a = "0x0000000000000000000000000000000000000000000000000000000000000000"

---
SSA Inputs:
0: u128 0
---
Options:
CompareOptions { inliner_aggressiveness: -9223372036854775808 }
---
SSA 1 after step 2 (Defunctionalization):
g0 = u128 68208882519879340829571110414913265451
g1 = u128 141888941893519431495522585334882459772
g2 = u128 78664061307629166694964766019303350777
g3 = u128 229134125080636816429820510416098134851
g4 = u128 246078571536640381569468433466924145168
g5 = make_array [u128 141888941893519431495522585334882459772, u128 78664061307629166694964766019303350777, u128 229134125080636816429820510416098134851, u128 246078571536640381569468433466924145168] : [u128; 4]
g6 = u128 281409297734408019540110123275768005705
g7 = u128 178029683271752409168712264797707897684
g8 = u128 35866632039212972075956128730669589847
g9 = u128 278054022342325001852341960081092635767
g10 = u128 40681105989194200543378816448734657328
g11 = u128 250932207057346960404143633361483230010
g12 = make_array [u128 35866632039212972075956128730669589847, u128 278054022342325001852341960081092635767, u128 40681105989194200543378816448734657328, u128 250932207057346960404143633361483230010] : [u128; 4]
g13 = u128 125258613224863982175369866539999860115
g14 = u128 213179355600187091451936113944275672394
g15 = u128 182513327886107005623960248002248608728
g16 = u128 185957822557510044736822223600828066861
g17 = u128 144677471795148236097787822081537003656
g18 = u128 158093617099024924450744857034507273574
g19 = make_array [u128 182513327886107005623960248002248608728, u128 185957822557510044736822223600828066861, u128 144677471795148236097787822081537003656, u128 158093617099024924450744857034507273574] : [u128; 4]
g20 = u128 35670510297322539680268656225144565474

acir(inline) fn main f0 {
  b0(v21: u128):
    v22 = make_array [v21] : [Field; 1]
    v24 = allocate -> &mut u32
    store u32 25 at v24
    v34 = load v24 -> u32
    v35, v36 = call f1(v34) -> (u128, u128)
    v37 = cast v36 as Field
    v38 = cast v21 as Field
    v39 = eq v37, v38
    constrain v37 == v38, "TBF"
    v43 = load v24 -> u32
    v44, v45, v46, v47 = call f2(u128 301767583745950347814793913572654123192, v43) -> ([u128; 4], u128, u128, u1)
    jmpif v47 then: b1, else: b2
  b1():
    jmp b3(v21)
  b2():
    jmp b3(u128 35670510297322539680268656225144565474)
  b3(v48: u128):
    v49 = load v24 -> u32
    v50, v51 = call f1(v49) -> (u128, u128)
    v52 = lt v51, v48
    v53 = not v52
    constrain v52 == u1 0, "CYM"
    v55 = allocate -> &mut u32
    store u32 815285805 at v55
    return g5
}
brillig(inline_always) fn func_1_proxy f1 {
  b0(v21: u32):
    v22 = allocate -> &mut u32
    store v21 at v22
    v24, v25 = call f4(v22) -> (u128, u128)
    return v24, v25
}
brillig(inline_always) fn func_2_proxy f2 {
  b0(v21: u128, v22: u32):
    v23 = allocate -> &mut u32
    store v22 at v23
    v25, v26, v27, v28 = call f3(v21, v23) -> ([u128; 4], u128, u128, u1)
    return v25, v26, v27, v28
}
brillig(inline_always) fn func_2 f3 {
  b0(v21: u128, v22: &mut u32):
    v27 = make_array [u128 154393597273046183284570645816597213555, u128 316114973126160255290652647137746813821, u128 309369013611773294078320911237563905555, u128 246773502993923634916978827225769168813] : [u128; 4]
    return v27, u128 45323974457163427869295425299351676299, u128 124837267636409002259242427137493810431, u1 0
}
brillig(inline_always) fn func_1 f4 {
  b0(v21: &mut u32):
    v22 = load v21 -> u32
    v24 = eq v22, u32 0
    jmpif v24 then: b1, else: b2
  b1():
    jmp b3(u128 211973039370314431325298847511786466703, u128 313339671284855045676773137498590239475)
  b2():
    v27 = load v21 -> u32
    v29 = sub v27, u32 1
    store v29 at v21
    v31, v32 = call f4(v21) -> (u128, u128)
    jmp b3(v31, v32)
  b3(v33: u128, v34: u128):
    return v33, v34
}

---
SSA 2 after step 3 (Inlining simple functions):
g0 = u128 68208882519879340829571110414913265451
g1 = u128 141888941893519431495522585334882459772
g2 = u128 78664061307629166694964766019303350777
g3 = u128 229134125080636816429820510416098134851
g4 = u128 246078571536640381569468433466924145168
g5 = make_array [u128 141888941893519431495522585334882459772, u128 78664061307629166694964766019303350777, u128 229134125080636816429820510416098134851, u128 246078571536640381569468433466924145168] : [u128; 4]
g6 = u128 281409297734408019540110123275768005705
g7 = u128 178029683271752409168712264797707897684
g8 = u128 35866632039212972075956128730669589847
g9 = u128 278054022342325001852341960081092635767
g10 = u128 40681105989194200543378816448734657328
g11 = u128 250932207057346960404143633361483230010
g12 = make_array [u128 35866632039212972075956128730669589847, u128 278054022342325001852341960081092635767, u128 40681105989194200543378816448734657328, u128 250932207057346960404143633361483230010] : [u128; 4]
g13 = u128 125258613224863982175369866539999860115
g14 = u128 213179355600187091451936113944275672394
g15 = u128 182513327886107005623960248002248608728
g16 = u128 185957822557510044736822223600828066861
g17 = u128 144677471795148236097787822081537003656
g18 = u128 158093617099024924450744857034507273574
g19 = make_array [u128 182513327886107005623960248002248608728, u128 185957822557510044736822223600828066861, u128 144677471795148236097787822081537003656, u128 158093617099024924450744857034507273574] : [u128; 4]
g20 = u128 35670510297322539680268656225144565474

acir(inline) fn main f0 {
  b0(v42: u128):
    v43 = make_array [v42] : [Field; 1]
    v44 = allocate -> &mut u32
    store u32 25 at v44
    v46 = load v44 -> u32
    v48, v49 = call f1(v46) -> (u128, u128)
    v50 = cast v49 as Field
    v51 = cast v42 as Field
    v52 = eq v50, v51
    constrain v49 == v42, "TBF"
    v53 = load v44 -> u32
    v56, v57, v58, v59 = call f2(u128 301767583745950347814793913572654123192, v53) -> ([u128; 4], u128, u128, u1)
    jmpif v59 then: b1, else: b2
  b1():
    jmp b3(v42)
  b2():
    jmp b3(u128 35670510297322539680268656225144565474)
  b3(v60: u128):
    v61 = load v44 -> u32
    v62, v63 = call f1(v61) -> (u128, u128)
    v64 = lt v63, v60
    v65 = not v64
    constrain v64 == u1 0, "CYM"
    v67 = allocate -> &mut u32
    store u32 815285805 at v67
    v69 = make_array [u128 141888941893519431495522585334882459772, u128 78664061307629166694964766019303350777, u128 229134125080636816429820510416098134851, u128 246078571536640381569468433466924145168] : [u128; 4]
    return v69
}
brillig(inline_always) fn func_1_proxy f1 {
  b0(v42: u32):
    v43 = allocate -> &mut u32
    store v42 at v43
    v45, v46 = call f4(v43) -> (u128, u128)
    return v45, v46
}
brillig(inline_always) fn func_2_proxy f2 {
  b0(v42: u128, v43: u32):
    v44 = allocate -> &mut u32
    store v43 at v44
    v50 = make_array [u128 154393597273046183284570645816597213555, u128 316114973126160255290652647137746813821, u128 309369013611773294078320911237563905555, u128 246773502993923634916978827225769168813] : [u128; 4]
    return v50, u128 45323974457163427869295425299351676299, u128 124837267636409002259242427137493810431, u1 0
}
brillig(inline_always) fn func_2 f3 {
  b0(v42: u128, v43: &mut u32):
    v48 = make_array [u128 154393597273046183284570645816597213555, u128 316114973126160255290652647137746813821, u128 309369013611773294078320911237563905555, u128 246773502993923634916978827225769168813] : [u128; 4]
    return v48, u128 45323974457163427869295425299351676299, u128 124837267636409002259242427137493810431, u1 0
}
brillig(inline_always) fn func_1 f4 {
  b0(v42: &mut u32):
    v43 = load v42 -> u32
    v45 = eq v43, u32 0
    jmpif v45 then: b1, else: b2
  b1():
    jmp b3(u128 211973039370314431325298847511786466703, u128 313339671284855045676773137498590239475)
  b2():
    v50 = load v42 -> u32
    v52 = sub v50, u32 1
    store v52 at v42
    v54, v55 = call f4(v42) -> (u128, u128)
    jmp b3(v54, v55)
  b3(v46: u128, v47: u128):
    return v46, v47
}
This is the second example
Comparison failed:
both programs failed:
constrain v86 == v94, "ISC" failed:
    i64 -1615928006 != i64 -5568658583620095790
!=
constrain v89 == v91, "ISC" failed:
    u64 18446744072093623610 != u64 12878085490089455826

ConstrainEqFailed { lhs: "i64 -1615928006", lhs_id: Id(86), rhs: "i64 -5568658583620095790", rhs_id: Id(94), msg: ", \"ISC\"" }
ConstrainEqFailed { lhs: "u64 18446744072093623610", lhs_id: Id(89), rhs: "u64 12878085490089455826", rhs_id: Id(91), msg: ", \"ISC\"" }
---
AST:
global G_A: [bool; 1] = [true];
global G_B: [bool; 1] = [true];
global G_C: [bool; 1] = [true];
fn main(a: [bool; 1], b: [bool; 1], c: pub ([bool; 2], [bool; 1])) -> pub ([bool; 2], [bool; 1]) {
    let mut ctx_limit: u32 = 25;
    let m = (unsafe { func_1_proxy(3171016502, ((!G_A[0]) > G_C[0]), ctx_limit) }[0] as Field);
    for idx_d in -1615928006 .. -1615927997 {
        let mut e: [str<3>; 4] = ["ILJ", if false {
            "EBK"
        } else {
            if (!((idx_d as i64) == -8564492324688510635)) {
                "JKJ"
            } else {
                "AQU"
            }
        }, "XBG", "NHH"];
        for idx_f in 309439623515069517414984241121608787966 .. 309439623515069517414984241121608787968 {
            for idx_g in 261947748728904975729542616533650847710 .. 261947748728904975729542616533650847712 {
                e[3] = e[2];
                let h: str<2> = "IG";
                let mut i: str<2> = "YH";
                let mut l: str<1> = {
                    i = i;
                    e[(1031974153 % 4)] = {
                        let mut j: str<2> = "DL";
                        let k: [str<2>; 4] = {
                            assert(((idx_d as i64) == (-5568658583620095790)), "ISC");
                            [j, "PU", j, "HS"]
                        };
                        "ZQG"
                    };
                    "L"
                };
            };
            assert(((G_C[0] as Field) != (a[0] as Field)), "HTH");
        };
    };
    (c.0, b)
}
unconstrained fn func_1(mut a: u32, b: bool, _ctx_limit: &mut u32) -> [bool; 2] {
    [G_B[(a % 1)], ((a as u64) < 6539024747699217127)]
}
unconstrained fn func_1_proxy(mut a: u32, b: bool, mut ctx_limit: u32) -> [bool; 2] {
    func_1(a, b, (&mut ctx_limit))
}

---
ABI Inputs:
a = [false]
b = [true]
c = [[true, true], [false]]

---
SSA Inputs:
0: rc1 [u1 false]
1: rc1 [u1 true]
2: rc1 [u1 true, u1 true]
3: rc1 [u1 false]
---
Options:
CompareOptions { inliner_aggressiveness: 9223372036854775807 }
---
SSA 1 after step 2 (Defunctionalization):
g0 = u1 1
g1 = make_array [u1 1] : [u1; 1]
g2 = make_array [u1 1] : [u1; 1]
g3 = make_array [u1 1] : [u1; 1]

acir(inline) fn main f0 {
  b0(v4: [u1; 1], v5: [u1; 1], v6: [u1; 2], v7: [u1; 1]):
    v9 = allocate -> &mut u32
    store u32 25 at v9
    v15 = load v9 -> u32
    v16 = call f1(u32 3171016502, u1 0, v15) -> [u1; 2]
    v18 = array_get v16, index u32 0 -> u1
    v19 = cast v18 as Field
    jmp b1(i32 2679039290)
  b1(v22: i32):
    v23 = lt v22, i32 2679039299
    jmpif v23 then: b2, else: b3
  b2():
    v27 = make_array b"ILJ"
    v28 = cast v22 as u32
    v30 = lt v28, u32 2147483648
    v32 = not v30
    v33 = cast v32 as u64
    v34 = unchecked_mul u64 18446744069414584320, v33
    v35 = cast v22 as u64
    v36 = unchecked_add v34, v35
    v37 = cast v36 as i64
    v39 = eq v37, i64 9882251749021040981
    v40 = not v39
    jmpif v40 then: b4, else: b5
  b3():
    return v6, v5
  b4():
    v42 = make_array b"JKJ"
    jmp b6(v42)
  b5():
    v46 = make_array b"AQU"
    jmp b6(v46)
  b6(v47: [u8; 3]):
    v51 = make_array b"XBG"
    v54 = make_array b"NHH"
    v55 = make_array [v27, v47, v51, v54] : [[u8; 3]; 4]
    v56 = allocate -> &mut [[u8; 3]; 4]
    store v55 at v56
    jmp b7(u128 309439623515069517414984241121608787966)
  b7(v59: u128):
    v60 = lt v59, u128 309439623515069517414984241121608787968
    jmpif v60 then: b8, else: b9
  b8():
    jmp b10(u128 261947748728904975729542616533650847710)
  b9():
    v119 = unchecked_add v22, i32 1
    jmp b1(v119)
  b10(v63: u128):
    v64 = lt v63, u128 261947748728904975729542616533650847712
    jmpif v64 then: b11, else: b12
  b11():
    v65 = load v56 -> [[u8; 3]; 4]
    v67 = array_get v65, index u32 2 -> [u8; 3]
    v68 = load v56 -> [[u8; 3]; 4]
    v70 = array_set v68, index u32 3, value v67
    store v70 at v56
    v71 = make_array b"IG"
    v73 = make_array b"YH"
    v74 = allocate -> &mut [u8; 2]
    store v73 at v74
    v75 = load v74 -> [u8; 2]
    store v75 at v74
    v77 = make_array b"DL"
    v78 = allocate -> &mut [u8; 2]
    store v77 at v78
    v79 = cast v22 as u32
    v80 = lt v79, u32 2147483648
    v81 = not v80
    v82 = cast v81 as u64
    v83 = unchecked_mul u64 18446744069414584320, v82
    v84 = cast v22 as u64
    v85 = unchecked_add v83, v84
    v86 = cast v85 as i64
    v94 = cast u64 12878085490089455826 as i64
    v95 = eq v86, v94
    constrain v86 == v94, "ISC"
    v96 = load v78 -> [u8; 2]
    v98 = make_array b"PU"
    v99 = load v78 -> [u8; 2]
    v101 = make_array b"HS"
    v102 = make_array [v96, v98, v99, v101] : [[u8; 2]; 4]
    v104 = make_array b"ZQG"
    v105 = load v56 -> [[u8; 3]; 4]
    v107 = array_set v105, index u32 1, value v104
    store v107 at v56
    v108 = make_array b"L"
    v109 = allocate -> &mut [u8; 1]
    store v108 at v109
    v111 = unchecked_add v63, u128 1
    jmp b10(v111)
  b12():
    v113 = array_get v4, index u32 0 -> u1
    v114 = cast v113 as Field
    v115 = eq Field 1, v114
    v116 = not v115
    constrain v115 == u1 0, "HTH"
    v117 = unchecked_add v59, u128 1
    jmp b7(v117)
}
brillig(inline_always) fn func_1_proxy f1 {
  b0(v4: u32, v6: u1, v7: u32):
    v5 = allocate -> &mut u32
    store v4 at v5
    v8 = allocate -> &mut u32
    store v7 at v8
    v10 = load v5 -> u32
    v11 = call f2(v10, v6, v8) -> [u1; 2]
    return v11
}
brillig(inline_always) fn func_1 f2 {
  b0(v4: u32, v6: u1, v7: &mut u32):
    v5 = allocate -> &mut u32
    store v4 at v5
    v8 = load v5 -> u32
    v11 = load v5 -> u32
    v12 = cast v11 as u64
    v14 = lt v12, u64 6539024747699217127
    v15 = make_array [u1 1, v14] : [u1; 2]
    return v15
}

---
SSA 2 after step 3 (Inlining simple functions):
g0 = u1 1
g1 = make_array [u1 1] : [u1; 1]
g2 = make_array [u1 1] : [u1; 1]
g3 = make_array [u1 1] : [u1; 1]

acir(inline) fn main f0 {
  b0(v8: [u1; 1], v9: [u1; 1], v10: [u1; 2], v11: [u1; 1]):
    v12 = allocate -> &mut u32
    store u32 25 at v12
    v14 = load v12 -> u32
    v18 = call f1(u32 3171016502, u1 0, v14) -> [u1; 2]
    v20 = array_get v18, index u32 0 -> u1
    v21 = cast v20 as Field
    jmp b1(i32 2679039290)
  b1(v22: i32):
    v25 = lt v22, i32 2679039299
    jmpif v25 then: b2, else: b3
  b2():
    v29 = make_array b"ILJ"
    v30 = cast v22 as u32
    v32 = lt v30, u32 2147483648
    v33 = not v32
    v34 = cast v33 as u64
    v36 = unchecked_mul u64 18446744069414584320, v34
    v37 = cast v22 as u64
    v38 = unchecked_add v36, v37
    v39 = cast v38 as i64
    v41 = eq v39, i64 9882251749021040981
    v42 = not v41
    jmpif v42 then: b4, else: b5
  b3():
    return v10, v9
  b4():
    v44 = make_array b"JKJ"
    jmp b6(v44)
  b5():
    v49 = make_array b"AQU"
    jmp b6(v49)
  b6(v45: [u8; 3]):
    v53 = make_array b"XBG"
    v56 = make_array b"NHH"
    v57 = make_array [v29, v45, v53, v56] : [[u8; 3]; 4]
    v58 = allocate -> &mut [[u8; 3]; 4]
    store v57 at v58
    jmp b7(u128 309439623515069517414984241121608787966)
  b7(v59: u128):
    v62 = lt v59, u128 309439623515069517414984241121608787968
    jmpif v62 then: b8, else: b9
  b8():
    jmp b10(u128 261947748728904975729542616533650847710)
  b9():
    v66 = unchecked_add v22, i32 1
    jmp b1(v66)
  b10(v63: u128):
    v68 = lt v63, u128 261947748728904975729542616533650847712
    jmpif v68 then: b11, else: b12
  b11():
    v69 = load v58 -> [[u8; 3]; 4]
    v71 = array_get v69, index u32 2 -> [u8; 3]
    v72 = load v58 -> [[u8; 3]; 4]
    v74 = array_set v72, index u32 3, value v71
    store v74 at v58
    v75 = make_array b"IG"
    v77 = make_array b"YH"
    v78 = allocate -> &mut [u8; 2]
    store v77 at v78
    v79 = load v78 -> [u8; 2]
    store v79 at v78
    v81 = make_array b"DL"
    v82 = allocate -> &mut [u8; 2]
    store v81 at v82
    v83 = cast v22 as u32
    v84 = lt v83, u32 2147483648
    v85 = not v84
    v86 = cast v85 as u64
    v87 = unchecked_mul u64 18446744069414584320, v86
    v88 = cast v22 as u64
    v89 = unchecked_add v87, v88
    v90 = cast v89 as i64
    v92 = cast u64 12878085490089455826 as i64
    v93 = eq v90, v92
    constrain v89 == u64 12878085490089455826, "ISC"
    v94 = load v82 -> [u8; 2]
    v96 = make_array b"PU"
    v97 = load v82 -> [u8; 2]
    v99 = make_array b"HS"
    v100 = make_array [v94, v96, v97, v99] : [[u8; 2]; 4]
    v102 = make_array b"ZQG"
    v103 = load v58 -> [[u8; 3]; 4]
    v105 = array_set v103, index u32 1, value v102
    store v105 at v58
    v106 = make_array b"L"
    v107 = allocate -> &mut [u8; 1]
    store v106 at v107
    v109 = unchecked_add v63, u128 1
    jmp b10(v109)
  b12():
    v110 = array_get v8, index u32 0 -> u1
    v111 = cast v110 as Field
    v113 = eq Field 1, v111
    v114 = not v113
    constrain v113 == u1 0, "HTH"
    v115 = unchecked_add v59, u128 1
    jmp b7(v115)
}
brillig(inline_always) fn func_1_proxy f1 {
  b0(v8: u32, v9: u1, v10: u32):
    v11 = allocate -> &mut u32
    store v8 at v11
    v12 = allocate -> &mut u32
    store v10 at v12
    v13 = load v11 -> u32
    v15 = allocate -> &mut u32
    store v13 at v15
    v16 = load v15 -> u32
    v17 = load v15 -> u32
    v18 = cast v17 as u64
    v20 = lt v18, u64 6539024747699217127
    v21 = make_array [u1 1, v20] : [u1; 2]
    return v21
}
brillig(inline_always) fn func_1 f2 {
  b0(v8: u32, v9: u1, v10: &mut u32):
    v11 = allocate -> &mut u32
    store v8 at v11
    v12 = load v11 -> u32
    v13 = load v11 -> u32
    v14 = cast v13 as u64
    v16 = lt v14, u64 6539024747699217127
    v17 = make_array [u1 1, v16] : [u1; 2]
    return v17
}


thread 'targets::pass_vs_prev::tests::fuzz_with_arbtest' panicked at tooling/ast_fuzzer/fuzz/src/targets/mod.rs:46:18:
called `Result::unwrap()` on an `Err` value: both programs failed:
constrain v86 == v94, "ISC" failed:
    i64 -1615928006 != i64 -5568658583620095790
!=
constrain v89 == v91, "ISC" failed:
    u64 18446744072093623610 != u64 12878085490089455826

ConstrainEqFailed { lhs: "i64 -1615928006", lhs_id: Id(86), rhs: "i64 -5568658583620095790", rhs_id: Id(94), msg: ", \"ISC\"" }
ConstrainEqFailed { lhs: "u64 18446744072093623610", lhs_id: Id(89), rhs: "u64 12878085490089455826", rhs_id: Id(91), msg: ", \"ISC\"" }

In the first one, main takes a u128, and casts it to Field before comparing it to another:

fn main(a: call_data(0) u128) -> pub [u128; 4] {
    ...
    assert(((unsafe { func_1_proxy(ctx_limit) }.1 as Field) == (a as Field)), "TBF");

In the 1st pass the comparison is on the Field values:

acir(inline) fn main f0 {
  b0(v21: u128):
...
    v35, v36 = call f1(v34) -> (u128, u128)
    v37 = cast v36 as Field
    v38 = cast v21 as Field
...
    constrain v37 == v38, "TBF"

while in the 2nd pass it's on the u128 input:

acir(inline) fn main f0 {
  b0(v42: u128):
...
    v48, v49 = call f1(v46) -> (u128, u128)
    v50 = cast v49 as Field
...
    constrain v49 == v42, "TBF"

In the second example, we have this in the code:

  assert(((idx_d as i64) == (-5568658583620095790)), "ISC");

In the 1st pass it compares i64:

    v85 = unchecked_add v83, v84
    v86 = cast v85 as i64
    v94 = cast u64 12878085490089455826 as i64
    v95 = eq v86, v94
    constrain v86 == v94, "ISC"

in the 2nd pass it bypasses the cast and does it on the originals:

    v89 = unchecked_add v87, v88
    v90 = cast v89 as i64
    v92 = cast u64 12878085490089455826 as i64
    v93 = eq v90, v92
    constrain v89 == u64 12878085490089455826, "ISC"

@aakoshh aakoshh added this pull request to the merge queue Jun 9, 2025
Merged via the queue into master with commit 2b8651d Jun 9, 2025
119 checks passed
@aakoshh aakoshh deleted the af/7932-fuzz-constraint branch June 9, 2025 08:47
github-merge-queue bot pushed a commit to AztecProtocol/aztec-packages that referenced this pull request Jun 10, 2025
Automated pull of nightly from the
[noir](https://github.com/noir-lang/noir) programming language, a
dependency of Aztec.
BEGIN_COMMIT_OVERRIDE
chore(docs): Update noirjs app page to use to beta.6
(noir-lang/noir#8853)
fix: support recursive call to main function in SSA parser
(noir-lang/noir#8760)
chore(SSA): validate that constrain values have the same type
(noir-lang/noir#8850)
fix: Comptime field division should error when the rhs is zero
(noir-lang/noir#8845)
chore: redo typo PR by osrm
(noir-lang/noir#8840)
fix: (SSA interpreter) to_le_bits returns [u1; _], not [u8; _]
(noir-lang/noir#8837)
chore(ssa): Initial validation module
(noir-lang/noir#8765)
chore: bump external pinned commits
(noir-lang/noir#8834)
feat(fuzz): Generate arbitrary constraints
(noir-lang/noir#8820)
fix: bind self generic type in trait calls via a concrete type in more
cases (noir-lang/noir#8827)
fix(comptime): Overflow on shl
(noir-lang/noir#8829)
fix(interpreter): Return -1 for negative shr signed overflow or 0 for
positive shr signed overflow
(noir-lang/noir#8828)
feat(ssa_fuzzer): branching + constrains
(noir-lang/noir#8599)
chore(docs): Add experimental warning in Debugger docs
(noir-lang/noir#8824)
fix: Thread errors through remove_if_else instead of panicing when the
value merger finds reference values
(noir-lang/noir#8783)
fix(interpreter): Do not overflow on signed checked ops
(noir-lang/noir#8806)
feat: short circuit creation of `Type::InfixExpr` containing errors
(noir-lang/noir#8826)
fix(mem2reg): Keep last stores used in array returned from a function
(noir-lang/noir#8801)
chore(ci): `cargo clippy` CI script to save time
(noir-lang/noir#8787)
chore: only follow bindings on interface to `arithmetic` module
(noir-lang/noir#8822)
fix: bind self generic type in trait calls via a concrete type
(noir-lang/noir#8825)
chore(docs): Reorder tooling docs
(noir-lang/noir#8742)
chore: small fix for outdated docs
(noir-lang/noir#8821)
fix(mem2reg): Keep last stores used in MakeArray
(noir-lang/noir#8743)
fix!: Error when re-assigning a mutable reference
(noir-lang/noir#8790)
fix!: indexing arrays with non-u32 is now an error
(noir-lang/noir#8804)
fix: signed right shift overflows to 0 or -1
(noir-lang/noir#8805)
chore(fuzz): Tool to minimize Noir programs with `cvise`
(noir-lang/noir#8789)
END_COMMIT_OVERRIDE

---------

Co-authored-by: AztecBot <tech@aztecprotocol.com>
Co-authored-by: Tom French <15848336+TomAFrench@users.noreply.github.com>
github-merge-queue bot pushed a commit to AztecProtocol/aztec-packages that referenced this pull request Jun 10, 2025
Automated pull of nightly from the
[noir](https://github.com/noir-lang/noir) programming language, a
dependency of Aztec.
BEGIN_COMMIT_OVERRIDE
chore(docs): Update noirjs app page to use to beta.6
(noir-lang/noir#8853)
fix: support recursive call to main function in SSA parser
(noir-lang/noir#8760)
chore(SSA): validate that constrain values have the same type
(noir-lang/noir#8850)
fix: Comptime field division should error when the rhs is zero
(noir-lang/noir#8845)
chore: redo typo PR by osrm
(noir-lang/noir#8840)
fix: (SSA interpreter) to_le_bits returns [u1; _], not [u8; _]
(noir-lang/noir#8837)
chore(ssa): Initial validation module
(noir-lang/noir#8765)
chore: bump external pinned commits
(noir-lang/noir#8834)
feat(fuzz): Generate arbitrary constraints
(noir-lang/noir#8820)
fix: bind self generic type in trait calls via a concrete type in more
cases (noir-lang/noir#8827)
fix(comptime): Overflow on shl
(noir-lang/noir#8829)
fix(interpreter): Return -1 for negative shr signed overflow or 0 for
positive shr signed overflow
(noir-lang/noir#8828)
feat(ssa_fuzzer): branching + constrains
(noir-lang/noir#8599)
chore(docs): Add experimental warning in Debugger docs
(noir-lang/noir#8824)
fix: Thread errors through remove_if_else instead of panicing when the
value merger finds reference values
(noir-lang/noir#8783)
fix(interpreter): Do not overflow on signed checked ops
(noir-lang/noir#8806)
feat: short circuit creation of `Type::InfixExpr` containing errors
(noir-lang/noir#8826)
fix(mem2reg): Keep last stores used in array returned from a function
(noir-lang/noir#8801)
chore(ci): `cargo clippy` CI script to save time
(noir-lang/noir#8787)
chore: only follow bindings on interface to `arithmetic` module
(noir-lang/noir#8822)
fix: bind self generic type in trait calls via a concrete type
(noir-lang/noir#8825)
chore(docs): Reorder tooling docs
(noir-lang/noir#8742)
chore: small fix for outdated docs
(noir-lang/noir#8821)
fix(mem2reg): Keep last stores used in MakeArray
(noir-lang/noir#8743)
fix!: Error when re-assigning a mutable reference
(noir-lang/noir#8790)
fix!: indexing arrays with non-u32 is now an error
(noir-lang/noir#8804)
fix: signed right shift overflows to 0 or -1
(noir-lang/noir#8805)
chore(fuzz): Tool to minimize Noir programs with `cvise`
(noir-lang/noir#8789)
END_COMMIT_OVERRIDE

---------

Co-authored-by: AztecBot <tech@aztecprotocol.com>
Co-authored-by: Tom French <15848336+TomAFrench@users.noreply.github.com>
danielntmd pushed a commit to danielntmd/aztec-packages that referenced this pull request Jul 16, 2025
Automated pull of nightly from the
[noir](https://github.com/noir-lang/noir) programming language, a
dependency of Aztec.
BEGIN_COMMIT_OVERRIDE
chore(docs): Update noirjs app page to use to beta.6
(noir-lang/noir#8853)
fix: support recursive call to main function in SSA parser
(noir-lang/noir#8760)
chore(SSA): validate that constrain values have the same type
(noir-lang/noir#8850)
fix: Comptime field division should error when the rhs is zero
(noir-lang/noir#8845)
chore: redo typo PR by osrm
(noir-lang/noir#8840)
fix: (SSA interpreter) to_le_bits returns [u1; _], not [u8; _]
(noir-lang/noir#8837)
chore(ssa): Initial validation module
(noir-lang/noir#8765)
chore: bump external pinned commits
(noir-lang/noir#8834)
feat(fuzz): Generate arbitrary constraints
(noir-lang/noir#8820)
fix: bind self generic type in trait calls via a concrete type in more
cases (noir-lang/noir#8827)
fix(comptime): Overflow on shl
(noir-lang/noir#8829)
fix(interpreter): Return -1 for negative shr signed overflow or 0 for
positive shr signed overflow
(noir-lang/noir#8828)
feat(ssa_fuzzer): branching + constrains
(noir-lang/noir#8599)
chore(docs): Add experimental warning in Debugger docs
(noir-lang/noir#8824)
fix: Thread errors through remove_if_else instead of panicing when the
value merger finds reference values
(noir-lang/noir#8783)
fix(interpreter): Do not overflow on signed checked ops
(noir-lang/noir#8806)
feat: short circuit creation of `Type::InfixExpr` containing errors
(noir-lang/noir#8826)
fix(mem2reg): Keep last stores used in array returned from a function
(noir-lang/noir#8801)
chore(ci): `cargo clippy` CI script to save time
(noir-lang/noir#8787)
chore: only follow bindings on interface to `arithmetic` module
(noir-lang/noir#8822)
fix: bind self generic type in trait calls via a concrete type
(noir-lang/noir#8825)
chore(docs): Reorder tooling docs
(noir-lang/noir#8742)
chore: small fix for outdated docs
(noir-lang/noir#8821)
fix(mem2reg): Keep last stores used in MakeArray
(noir-lang/noir#8743)
fix!: Error when re-assigning a mutable reference
(noir-lang/noir#8790)
fix!: indexing arrays with non-u32 is now an error
(noir-lang/noir#8804)
fix: signed right shift overflows to 0 or -1
(noir-lang/noir#8805)
chore(fuzz): Tool to minimize Noir programs with `cvise`
(noir-lang/noir#8789)
END_COMMIT_OVERRIDE

---------

Co-authored-by: AztecBot <tech@aztecprotocol.com>
Co-authored-by: Tom French <15848336+TomAFrench@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Generate arbitrary Constraints

3 participants