Skip to content

Commit

Permalink
fix: zero out input to to_radix calls if inactive (#4116)
Browse files Browse the repository at this point in the history
# Description

## Problem\*

Resolves <!-- Link to GitHub Issue -->

## Summary\*

In situations where a `to_le_bytes` call is in an inactive if-statement,
the requirement for the produced byte array to represent the input field
is not disabled. This can result in situations such as below where we
want to decompose a value into a number of bytes which is dependent on
the inputs to the circuit.


https://github.com/porco-rosso-j/safe-recovery-noir/blob/b80a1fd49d370bd095827318b378c8fdef2e2d9b/circuits/social/src/root.nr#L11-L22

All branches of this snippet are limited by the fact that the first will
fail on `index` with values greater than 1.



```
fn main(x: Field, cond: bool) {
    if cond {
        let bad_byte_array = x.to_le_bytes(1);
        assert_eq(bad_byte_array.len(), 1);
    }
}
```

This compiles down to 

```
acir fn main f0 {
  b0(v0: Field, v1: u1):
    enable_side_effects v1
    v31, v32 = call to_le_radix(v0, u32 2⁸, u32 1)
    v34 = cast v1 as Field
    v35 = mul v31, v34
    constrain v35 == v34
    enable_side_effects u1 1
    return 
}
```

The `to_le_radix` will revert for all `v0 >= 8` no matter the value of
`v1`.

I've modified the `flatten_cfg` pass such that we multiply in the side
effects variable to zero out the input should the instruction be
deactivated.


## Additional Context



## Documentation\*

Check one:
- [x] No documentation needed.
- [ ] Documentation included in this PR.
- [ ] **[Exceptional Case]** Documentation to be submitted in a separate
PR.

# PR Checklist\*

- [x] I have tested the changes locally.
- [x] I have formatted the changes with [Prettier](https://prettier.io/)
and/or `cargo fmt` on default settings.
  • Loading branch information
TomAFrench authored Jan 25, 2024
1 parent 0590432 commit 3f5bad3
Show file tree
Hide file tree
Showing 5 changed files with 36 additions and 7 deletions.
5 changes: 3 additions & 2 deletions compiler/noirc_evaluator/src/ssa/ir/instruction.rs
Original file line number Diff line number Diff line change
Expand Up @@ -87,6 +87,9 @@ impl Intrinsic {
match self {
Intrinsic::AssertConstant | Intrinsic::ApplyRangeConstraint => true,

// These apply a constraint that the input must fit into a specified number of limbs.
Intrinsic::ToBits(_) | Intrinsic::ToRadix(_) => true,

Intrinsic::Sort
| Intrinsic::ArrayLen
| Intrinsic::SlicePushBack
Expand All @@ -96,8 +99,6 @@ impl Intrinsic {
| Intrinsic::SliceInsert
| Intrinsic::SliceRemove
| Intrinsic::StrAsBytes
| Intrinsic::ToBits(_)
| Intrinsic::ToRadix(_)
| Intrinsic::FromField
| Intrinsic::AsField => false,

Expand Down
26 changes: 24 additions & 2 deletions compiler/noirc_evaluator/src/ssa/opt/flatten_cfg.rs
Original file line number Diff line number Diff line change
Expand Up @@ -144,9 +144,9 @@ use crate::ssa::{
dfg::{CallStack, InsertInstructionResult},
function::Function,
function_inserter::FunctionInserter,
instruction::{BinaryOp, Instruction, InstructionId, TerminatorInstruction},
instruction::{BinaryOp, Instruction, InstructionId, Intrinsic, TerminatorInstruction},
types::Type,
value::ValueId,
value::{Value, ValueId},
},
ssa_gen::Ssa,
};
Expand Down Expand Up @@ -683,6 +683,28 @@ impl<'f> Context<'f> {
);
Instruction::RangeCheck { value, max_bit_size, assert_message }
}
Instruction::Call { func, mut arguments } => match self.inserter.function.dfg[func]
{
Value::Intrinsic(Intrinsic::ToBits(_) | Intrinsic::ToRadix(_)) => {
let field = arguments[0];
let argument_type = self.inserter.function.dfg.type_of_value(field);

let casted_condition = self.insert_instruction(
Instruction::Cast(condition, argument_type),
call_stack.clone(),
);
let field = self.insert_instruction(
Instruction::binary(BinaryOp::Mul, field, casted_condition),
call_stack.clone(),
);

arguments[0] = field;

Instruction::Call { func, arguments }
}

_ => Instruction::Call { func, arguments },
},
other => other,
}
} else {
Expand Down
2 changes: 0 additions & 2 deletions test_programs/compile_success_empty/intrinsic_die/src/main.nr
Original file line number Diff line number Diff line change
@@ -1,8 +1,6 @@
use dep::std;
// This test checks that we perform dead-instruction-elimination on intrinsic functions.
fn main(x: Field) {
let bytes = x.to_be_bytes(32);

let hash = std::hash::pedersen_commitment([x]);
let _p1 = std::scalar_mul::fixed_base_embedded_curve(x, 0);
}
1 change: 1 addition & 0 deletions test_programs/execution_success/to_le_bytes/Prover.toml
Original file line number Diff line number Diff line change
@@ -1 +1,2 @@
x = "2040124"
cond = false
9 changes: 8 additions & 1 deletion test_programs/execution_success/to_le_bytes/src/main.nr
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
fn main(x: Field) -> pub [u8; 31] {
fn main(x: Field, cond: bool) -> pub [u8; 31] {
// The result of this byte array will be little-endian
let byte_array = x.to_le_bytes(31);
assert(byte_array.len() == 31);
Expand All @@ -7,5 +7,12 @@ fn main(x: Field) -> pub [u8; 31] {
for i in 0..31 {
bytes[i] = byte_array[i];
}

if cond {
// We've set x = "2040124" so we shouldn't be able to represent this as a single byte.
let bad_byte_array = x.to_le_bytes(1);
assert_eq(bad_byte_array.len(), 1);
}

bytes
}

0 comments on commit 3f5bad3

Please sign in to comment.