feat: replace boolean ANDs with multiplication

[TomAFrench]

Description

Problem*

Resolves

Summary*

The Noir program below

fn main(x: u1) -> pub u1 {
    x & 1
}

previously would output the ACIR

current witness index : 3
public parameters indices : []
return value indices : [3]
BLACKBOX::RANGE [(_1, num_bits: 1)] [ ]
EXPR [ (-1, _2) 1 ]
BLACKBOX::AND [(_1, num_bits: 1), (_2, num_bits: 1)] [ _3]

This is suboptimal for a couple of reasons:

• we know that x & 1 == x so these gates should be optimised away
• even if we're performing x & y where neither are comptime then it's cheaper to multiply them together than do an AND.

I've then added a special case for AND between boolean variables which performs a multiplication. This results in the same program being optimized away such that we get the ACIR:

Compiled ACIR for main:
current witness index : 1
public parameters indices : []
return value indices : [1]
BLACKBOX::RANGE [(_1, num_bits: 1)] [ ]

Documentation

• This PR requires documentation updates when merged.

  • I will submit a noir-lang/docs PR.
  • I will request for and support Dev Rel's help in documenting this PR.

Additional Context

PR Checklist*

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

[TomAFrench]

For instance

fn main(x: u1, y: u1) -> pub u1 {
    x & y + 1
}

requires 2784 gates without this optimisation but afterwards requires just 11.

[jfecher]

The change looks good, but have you considered adding it during ssa-gen instead of acir gen so that further optimizations can potentially be triggered afterward?

[jfecher]

requires 2784 gates without this optimisation but afterwards requires just 11.

I wonder if we can have an optimization when we convert something to bits to only convert N bits for a uN type.

[TomAFrench]

have you considered adding it during ssa-gen instead of acir gen so that further optimizations can potentially be triggered afterward?

No I didn't but this seems like a good excuse to get more familiar with the internals of that. Seems to me like we want to insert a snippet like

let instruction = match instruction {
    Instruction::Binary(op) if self.type_of_value(op.lhs).is_boolean() => {
        instruction.booleanize()
    }
    instruction => instruction,
};

before L162 in

noir/crates/noirc_evaluator/src/ssa_refactor/ir/dfg.rs

Lines 155 to 169 in 720b1be

	match instruction.simplify(self, block) {
	SimplifyResult::SimplifiedTo(simplification) => SimplifiedTo(simplification),
	SimplifyResult::SimplifiedToMultiple(simplification) => {
	SimplifiedToMultiple(simplification)
	}
	SimplifyResult::Remove => InstructionRemoved,
	SimplifyResult::None => {
	let id = self.make_instruction(instruction, ctrl_typevars);
	self.blocks[block].insert_instruction(id);
	if let Some(location) = location {
	self.locations.insert(id, location);
	}
	InsertInstructionResult::Results(self.instruction_results(id))
	}
	}

Does this look sensible to you?

[jfecher]

I think it should probably go within the simplify call. There should be a case that handles binary operators already, and you can find the case for And and add to that.

[TomAFrench]

Ah, I looked at that but wasn't sure if I could return a non-constant value out. So I then just need to return something like SimplifyResult::SimplifiedTo(dfg.make_value(booleanised_instruction)) from there?

[kevaundray]

For instance

fn main(x: u1, y: u1) -> pub u1 {
    x & y + 1
}

requires 2784 gates without this optimisation but afterwards requires just 11.

Why does this require 2784 gates?

[TomAFrench]

Why does this require 2784 gates?

Barretenberg is using a plookup version of AND/XOR afaik so I guess that has some constant lower bound on the number of gates it uses.

[TomAFrench]

Compilation error comes from this line.

https://github.com/noir-lang/noir/blob/master/noir_stdlib/src/ec/swcurve.nr#L38-L39

Seems like we don't update some values correctly when we swap out the instruction. I need to dig into this more though.

[TomAFrench]

Minimal program for reproducing the panic:

use dep::std::ec::tecurve::affine::Curve as AffineCurve;
use dep::std::ec::tecurve::affine::Point as Gaffine;
use dep::std::ec::tecurve::curvegroup::Curve;
use dep::std::ec::tecurve::curvegroup::Point as G;

use dep::std::ec::swcurve::affine::Point as SWGaffine;
use dep::std::ec::swcurve::curvegroup::Point as SWG;

use dep::std::ec::montcurve::affine::Point as MGaffine;
use dep::std::ec::montcurve::curvegroup::Point as MG;

fn main() {
    // This test only makes sense if Field is the right prime field.
    if 21888242871839275222246405745257275088548364400416034343698204186575808495617 == 0
    {
        // Define Baby Jubjub (ERC-2494) parameters in affine representation
        let bjj_affine = AffineCurve::new(168700, 168696, Gaffine::new(995203441582195749578291179787384436505546430278305826713579947235728471134,5472060717959818805561601436314318772137091100104008585924551046643952123905));

        // Test addition
        let p1_affine = Gaffine::new(17777552123799933955779906779655732241715742912184938656739573121738514868268, 2626589144620713026669568689430873010625803728049924121243784502389097019475);
        let p2_affine = Gaffine::new(16540640123574156134436876038791482806971768689494387082833631921987005038935, 20819045374670962167435360035096875258406992893633759881276124905556507972311);      
        let p3_affine = bjj_affine.add(p1_affine, p2_affine);


        
        // Test CurveGroup equivalents
        let bjj = bjj_affine.into_group(); // Baby Jubjub

        let p1 = p1_affine.into_group();
        let p2 = p2_affine.into_group();
        let p3 = p3_affine.into_group();

        
        // Test SWCurve equivalents of the above
        // First the affine representation
        let bjj_swcurve_affine = bjj_affine.into_swcurve();

        let p1_swcurve_affine = bjj_affine.map_into_swcurve(p1_affine);
        let p2_swcurve_affine = bjj_affine.map_into_swcurve(p2_affine);
        let p3_swcurve_affine = bjj_affine.map_into_swcurve(p3_affine);
        
        // Addition
        assert(
            p3_swcurve_affine.eq(
                bjj_swcurve_affine.add(
                p1_swcurve_affine,
                p2_swcurve_affine
                )
            )
        );

        // Check that these points are on the curve
        assert(
            bjj_swcurve_affine.contains(bjj_swcurve_affine.gen) &
            bjj_swcurve_affine.contains(p1_swcurve_affine) &
            bjj_swcurve_affine.contains(p2_swcurve_affine) &
            bjj_swcurve_affine.contains(p3_swcurve_affine)
        );
        
        // Then the CurveGroup representation
        let bjj_swcurve = bjj.into_swcurve();

        let p1_swcurve = bjj.map_into_swcurve(p1);
        let p2_swcurve = bjj.map_into_swcurve(p2);
        let p3_swcurve = bjj.map_into_swcurve(p3);
        
        // Addition
        assert(p3_swcurve.eq(bjj_swcurve.add(p1_swcurve,p2_swcurve)));        
    }            
}

[TomAFrench]

I'm getting a panic on this line due to one of the inputs to the multiplication instruction being a Value::Param which should be cached.

noir/crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs

Lines 490 to 492 in 88a4f74

	Value::Instruction { .. } | Value::Param { .. } => {
	unreachable!("ICE: Should have been in cache {value_id} {value:?}")
	}

I'm not clear on how changing instruction.operation has resulted in this as lhs and rhs are unaffected. @jfecher Do you have any idea how this error might be occurring?

[vezenovm]

Barretenberg is using a plookup version of AND/XOR afaik so I guess that has some constant lower bound on the number of gates it uses.

The plookup versions of different ops are going to have a constant lower bound around 3k gates. Do we know if it is always cheaper to do a multiply rather than an AND? Like if this optimization is used in a larger circuit that is significantly over the 3k lower bound?

[TomAFrench]

If I use the program in new and old SSA I get

fn main(array: [u1; 1000]) -> pub u1 {
    let mut result = 1;
    for element in array {
        result &= element;
    }
    result
}

// Old
...
EXPR [ (1, _996, _996) (-1, _996) 0 ]
EXPR [ (1, _997, _997) (-1, _997) 0 ]
EXPR [ (1, _998, _998) (-1, _998) 0 ]
EXPR [ (1, _999, _999) (-1, _999) 0 ] // Range checks
EXPR [ (1, _1000, _1000) (-1, _1000) 0 ]
EXPR [ (1, _1, _2) (-1, _1001) 0 ]   // AND multiplications
EXPR [ (1, _3, _1001) (-1, _1002) 0 ]
EXPR [ (1, _4, _1002) (-1, _1003) 0 ]
EXPR [ (1, _5, _1003) (-1, _1004) 0 ]
...

Total ACIR opcodes generated for language PLONKCSat { width: 3 }: 1999
Backend circuit size: 2000

// New
....
BLACKBOX::RANGE [(_997, num_bits: 1)] [ ]
BLACKBOX::RANGE [(_998, num_bits: 1)] [ ]
BLACKBOX::RANGE [(_999, num_bits: 1)] [ ]
BLACKBOX::RANGE [(_1000, num_bits: 1)] [ ] // Range checks
EXPR [ (-1, _1001) 1 ] // `result` initialisation
BLACKBOX::AND [(_1001, num_bits: 1), (_1, num_bits: 1)] [ _1002]
BLACKBOX::AND [(_1002, num_bits: 1), (_2, num_bits: 1)] [ _1003]
BLACKBOX::AND [(_1003, num_bits: 1), (_3, num_bits: 1)] [ _1004]
BLACKBOX::AND [(_1004, num_bits: 1), (_4, num_bits: 1)] [ _1005]
....

Total ACIR opcodes generated for language PLONKCSat { width: 3 }: 2001
Backend circuit size: 41991

We can see that we actually have this multiplication optimisation in the old SSA code which causes it to outperform. In case this was an artifact of only having boolean ANDs and we would get better scaling with the plookup AND when we have a mix of boolean and non-boolean types I repeated with

fn main(array: [u1; 1000], byte_array: [u8; 1000]) -> pub u8 {
    let mut result = 1;
    for element in array {
        result &= element;
    };

    let mut byte_result: u8 = 5;
    for element in byte_array {
        byte_result &= element;
    };

    (result as u8) * byte_result
}

which gives the results

// Old
Total ACIR opcodes generated for language PLONKCSat { width: 3 }: 4001
Backend circuit size: 44098

// New
Total ACIR opcodes generated for language PLONKCSat { width: 3 }: 4007
Backend circuit size: 81360

[vezenovm]

If I use the program in new and old SSA I get

Awesome. Thank you for the clear comparison

[jfecher]

I'm not clear on how changing instruction.operation has resulted in this as lhs and rhs are unaffected. @jfecher Do you have any idea how this error might be occurring?

No, unfortunately. My thought was the same as yours, as long as the arguments of the instruction remained the same it shouldn't require extra handling. Let me know if you want me to try to look into this as well.

[TomAFrench]

New minimal reproduction.

use dep::std::ec::tecurve::affine::Curve as AffineCurve;
use dep::std::ec::tecurve::affine::Point as Gaffine;
use dep::std::ec::tecurve::curvegroup::Curve;
use dep::std::ec::tecurve::curvegroup::Point as G;

use dep::std::ec::swcurve::affine::Point as SWGaffine;
use dep::std::ec::swcurve::curvegroup::Point as SWG;

use dep::std::ec::montcurve::affine::Point as MGaffine;
use dep::std::ec::montcurve::curvegroup::Point as MG;

fn main() {
    
    // Define Baby Jubjub (ERC-2494) parameters in affine representation
    let bjj_affine = AffineCurve::new(168700, 168696, Gaffine::new(995203441582195749578291179787384436505546430278305826713579947235728471134,5472060717959818805561601436314318772137091100104008585924551046643952123905));

    // Test addition
    let p1_affine = Gaffine::new(17777552123799933955779906779655732241715742912184938656739573121738514868268, 2626589144620713026669568689430873010625803728049924121243784502389097019475);
    let p2_affine = Gaffine::new(16540640123574156134436876038791482806971768689494387082833631921987005038935, 20819045374670962167435360035096875258406992893633759881276124905556507972311);      
    let p3_affine = bjj_affine.add(p1_affine, p2_affine);
    
    // Test SWCurve equivalents of the above
    // First the affine representation
    let bjj_swcurve_affine = bjj_affine.into_swcurve();

    let p1_swcurve_affine = bjj_affine.map_into_swcurve(p1_affine);
    let p2_swcurve_affine = bjj_affine.map_into_swcurve(p2_affine);
    let p3_swcurve_affine = bjj_affine.map_into_swcurve(p3_affine);

    let p3_swcurve_affine_from_add = bjj_swcurve_affine.add(
        p1_swcurve_affine,
        p2_swcurve_affine
    );

    // Check that these points are on the curve
    assert(
        bjj_swcurve_affine.contains(p1_swcurve_affine)
    );            
}

[TomAFrench]

This now panics with

The application panicked (crashed).
Message:  internal error: entered unreachable code: ICE: Should have been in cache v170 Param { block: Id(12), position: 2, typ: Numeric(Unsigned { bit_size: 1 }) }
Location: crates/noirc_evaluator/src/ssa_refactor/acir_gen/mod.rs:722

with the printed SSA being

/* snip */

@jfecher I don't think I can meaningfully debug this to be honest. It seems odd to me that we wouldn't create a numeric constant rather than a param for an function argument if we know it's value at compile time though, should we be rewriting these?

[jfecher]

@TomAFrench found the error: #2117. Not sure why this PR specifically was triggering it though.

[TomAFrench]

@jfecher can you rereview please? Your requested changes should be addressed.

[jfecher]

Glad to finally merge this in 🙂