ARC-0004: Flagged Operations for Conditional Code

[bendyarm]

---

arc: 4
title: Flagged Operations for Conditional Code
authors: bendyarm, d0cd, acoglio, mikebenfield
discussion: ARC-0004: Flagged Operations for Conditional Code
topic: Protocol
status: Draft
created: 2025-03-09

Abstract

Some Aleo instructions can halt when passed certain arguments.
This halting behavior makes those instructions unusable
by a program that wants to try something else if a halt is detected.

We propose to add nonhalting variants of each such instruction.
The nonhalting variants additionally return an error flag.
This change would be strictly additive; none of the existing instructions
or Aleo Instructions programs would change.

Why does Aleo need this?

The need for these instructions is to enable proper compilation of if-then-else in a circuit. In a circuit, both the then statements and the else statements are executed (both must be executed), and then the if condition is used to select which results will be used for further computation. If a non-taken branch halts, it still halts the entire circuit, which is not the desired behavior.

Especially for code compiled from Leo, this could lead to unexpected program behavior, including possible inaccessibility of funds. The reason Leo code is especially vulnerable is that it has an if-then-else statement that currently has a different semantics than what a Leo programmer would expect (the non-taken branch being executed). However, the problem also exists in Aleo Instructions of not being able to write the equivalent of an if-then-else statement where there are halting instructions in the then statements or else statements.

However, even for Aleo Instructions programs not compiled from Leo, these operations will allow developers to roll their own if-then-else code, and will enable checking if an instruction would have halted without actually triggering a halt.

Why does adding nonhalting variants solve this problem?

By using nonhalting instruction variants in then and else branches, a non-taken branch will not cause a halt, even though it is still executed. When the if condition selects which results to use, at that time the code will trigger a halt if the taken branch would have halted if it had used a halting instruction (i.e., if the error flag was set by the nonhalting instruction).

Simple example in Leo code.

transition main(public x: field, y: field) -> field {
    if y == 0field {
        return x;
    } else {
        return x / y;
    }
}

If called with y equal to 0field, this program will halt because the division is always executed, whereas the expected result would be x. There is currently no way to compile this Leo program to Aleo Instructions that work as expected unless there is a nonhalting div operation. (We are calling this proposed nonhalting Aleo Instructions opcode div.flagged.)

After this ARC is implemented, the Leo compiler can be improved so that this program runs as expected.

Specification

Each flagged operation is identical to its corresponding current operation
when called with arguments that would be nonhalting, except it returns
a second return value of type boolean that is false (meaning that the
current operation would not have halted). When called with arguments
that would have been halting, it generally returns 0 (of the appropriate
output type) and true ("would have halted") for the second return value.

The flagged operations are different from wrapped (e.g. abs.w) or
lossy (e.g. cast.lossy) operations. It is important that the flagged
operation have the same semantics as the current halting instruction
except for the halting behavior and extra return value, for ease of
use by compilers.

Note that most opcodes compile into different operations based on the types
of the operands, and those operations sometimes have different halting
behavior. For example, add cannot halt when given field, group or scalar
arguments, but it can halt when given integer arguments. So add.flagged
will not be implemented for field, group or scalar arguments. We add notes
for these cases in the table below.

Current Halting Opcode	New Flagged Opcode	notes
abs	abs.flagged
add	add.flagged	add.flagged implemented only for integer types.
assert.eq	is.eq	We probably don't need a separate assert.(n)eq.flagged;
assert.neq	is.neq	instead, just use the existing is.(n)eq.
cast	cast.flagged	As of now, docs don't say what causes cast to halt. TBD.
div	div.flagged	div can halt on underflow and divide by zero.
div.w	div.w.flagged	div.w can halt on divide by zero.
inv	inv.flagged
mod	mod.flagged
mul	mul.flagged	mul.flagged implemented only for integer types.
neg	neg.flagged	neg.flagged implemented only for signed integer types.
pow	pow.flagged	pow.flagged implemented only for integer types.
rem	rem.flagged	rem can halt on underflow and divide by zero.
rem.w	rem.w.flagged	rem.w can halt on divide by zero.
shl	shl.flagged	As of now, Aleo docs don't say what causes shl or shr to halt.
shr	shr.flagged	But the Leo docs state that shl and shr halt if the shift distance
		exceeds the bit size of the first argument, and also shl halts if the
		shifted result does not fit within the type of the first argument.
sqrt	sqrt.flagged
sub	sub.flagged	sub.flagged implemented only for integer types.

Test Cases

The following note applies to all tests of Aleo Instructions. For all tests, both literal constant arguments
and variable arguments should be tested. For example, if there are two arguments, we need to test all four
combinations. This is because the Aleo Instructions compiler generates more optimized code for literal
constant arguments, and the circuits can differ substantially.

One or more arguments that causes halting for a current halting opcode should be used as an input
for the equivalent new flagged opcode to make sure it doesn't halt.

An assortment of arguments that do not cause halting for a current halting opcode should be
used as input to both halting and flagged operations to make sure they return the same value
(other than the halting flag, of course).

Audit and Formal Verification

We intend to have an audit of the implementation of the new opcodes, as well as to formally
verify the implementation.

Reference Implementations

This ARC will not be fully implemented unless approved. However, there is a proof-of-concept (PoC)
implementation with the following components:

• In a snarkVM branch, Aleo Instructions div.flagged and inv.flagged have been implemented, both for
  only field operands.

• In a Leo branch, there is a PoC change to the Leo compiler that compiles uses of / and inv() (that
  are applied to field operands and that are in conditionals) to the new Aleo Instructions div.flagged and
  inv.flagged, along with the appropriate logic to make sure halts happen only when appropriate.

This To try out this PoC implementation, first make sure you have already installed the
preliminaries for snarkVM
and for Leo.

// cd to the parent of where you want this copy of snarkVM to go.
git clone --branch poc-flagged https://github.com/bendyarm/snarkvm
cd snarkvm
cargo install --path .

// cd to the parent of where you want this copy of Leo to go.
git clone --branch div-flagged https://github.com/ProvableHQ/leo
cd leo
cargo install --path .

At this point you can use the snarkVM CLI and the Leo CLI to make programs and run them.

This PoC fixes this Leo issue.
Similarly, implementing the full ARC will fix similar issues for all the haltable operations
when they are in conditional code.

Dependencies

The main change is to the snarkVM repository.

Any tool that needs to know what all the opcodes are needs to be changed. For example, the Aleo
Explorer and the Provable SDK.

After the ARC is implemented, the Leo compiler can use the new opcodes to improve the quality of compiled code.
However, if the Leo compiler is not changed, the resulting code will continue to work the same way it did before the ARC was implemented.

Backwards Compatibility

For snarkVM, this change is strictly additive, and does not require any changes to existing Aleo Instructions programs. Also, use of the new opcodes is optional; the change does not require any changes to how you are writing new Aleo Instructions programs.

If there are any Leo programs that were actually depending on the behavior of halting operations in non-taken branches causing halts, then those Leo programs would behave differently after being recompiled. We believe this case is very unlikely; it is more likely that the recompilation would fix latent bugs that just had not yet been encountered.

Security & Compliance

This change does not affect security or regulatory issues.

References

Example Leo bug:
ProvableHQ/leo#27482

[mikebenfield]

The table here indicates that some hash and commit functions will get flagged versions, and indeed Aleo opcode docs say these hash functions will fail if the input is too large (for the Pedersen functions) or too small ( for the BHP functions). In practice, the BHP functions don't seem to fail even with u8 input. This Leo code:

program test.aleo {
    transition main(x: u8) -> field {
        let x1: field = BHP256::hash_to_field(x);
        let x2: field = BHP512::hash_to_field(x);
        let x3: field = BHP768::hash_to_field(x);
        let x4: field = BHP1024::hash_to_field(x);
        let x5: field = Pedersen64::hash_to_field(x);
        let x6: field = Pedersen128::hash_to_field(x);
        let x7: field = BHP256::commit_to_field(x, 1scalar);
        let x8: field = BHP512::commit_to_field(x, 1scalar);
        let x9: field = BHP768::commit_to_field(x, 1scalar);
        let x10: field = BHP1024::commit_to_field(x, 1scalar);
        let x11: field = Pedersen64::commit_to_field(x, 1scalar);
        let x12: field = Pedersen128::commit_to_field(x, 1scalar);
        return x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 + x9 + x10 + x11 + x12;
    }
}

compiles to this .aleo file:

program test.aleo;

function main:
    input r0 as u8.private;
    hash.bhp256 r0 into r1 as field;
    hash.bhp512 r0 into r2 as field;
    hash.bhp768 r0 into r3 as field;
    hash.bhp1024 r0 into r4 as field;
    hash.ped64 r0 into r5 as field;
    hash.ped128 r0 into r6 as field;
    commit.bhp256 r0 1scalar into r7 as field;
    commit.bhp512 r0 1scalar into r8 as field;
    commit.bhp768 r0 1scalar into r9 as field;
    commit.bhp1024 r0 1scalar into r10 as field;
    commit.ped64 r0 1scalar into r11 as field;
    commit.ped128 r0 1scalar into r12 as field;
    add r1 r2 into r13;
    add r13 r3 into r14;
    add r14 r4 into r15;
    add r15 r5 into r16;
    add r16 r6 into r17;
    add r17 r7 into r18;
    add r18 r8 into r19;
    add r19 r9 into r20;
    add r20 r10 into r21;
    add r21 r11 into r22;
    add r22 r12 into r23;
    output r23 as field.private;

and runs fine, producing an output.

% leo run main 1u8
     Leo ✅ Compiled 'test.aleo' into Aleo instructions

✅ Request              (Constant: 3440, Public: 9, Private: 11065, Constraints: 11068, NonZeros: (24563, 33391, 15140))
✅ Function 'main()'    (Constant: 8554, Public: 9, Private: 11441, Constraints: 11444, NonZeros: (25131, 33951, 15812))
✅ Response             (Constant: 9302, Public: 10, Private: 13236, Constraints: 13242, NonZeros: (31611, 44418, 17782))
✅ Complete             (Constant: 9302, Public: 10, Private: 13236, Constraints: 13242, NonZeros: (31611, 44418, 17782))
✅ Request              (Constant: 3440, Public: 9, Private: 11065, Constraints: 11068, NonZeros: (24563, 33391, 15140))
✅ Function 'main()'    (Constant: 8554, Public: 9, Private: 11441, Constraints: 11444, NonZeros: (25131, 33951, 15812))
✅ Response             (Constant: 9302, Public: 10, Private: 13236, Constraints: 13242, NonZeros: (31611, 44418, 17782))
✅ Complete             (Constant: 9302, Public: 10, Private: 13236, Constraints: 13242, NonZeros: (31611, 44418, 17782))
⛓  Constraints

•  'test.aleo/main' - 376 constraints (called 1 time)

➡️  Output

• 7317243804445408870221393009163869128263930477525187016603911032950961795919field

     Leo ✅ Finished 'test.aleo/main' (in "/Users/michaelbenfield/Code/test/build")

I don't know if this is a bug in the docs or in SnarkVM.

[bendyarm]

Thank you @mikebenfield for the observation!

It is out-of-date documentation. The commit.bhp* and hash.bhp* instructions now type-length-encode their argument so there is no minimum bit size. I have removed these instructions from the list.

Also, the commit.ped* and hash.ped* will not generate a circuit when passed an input struct > 64 bits. Since the struct size is known at synthesis time, synthesis gets an error when the type-length-encoded struct size is > 64 bits. (The documentation calls this error a "halt", but we generally reserve that word for when a circuit's constraints can't be satisfied.) Since we only need flagged versions of instructions that can halt in the sense of the circuit's constraints not being satisfied, I have removed these instructions from the list as well.

[alexanderkim11]

LGTM! On the backward compatibility issue, I think it's fine that the (unlikely) use case of Leo programs that were actually depending on the behavior of halting operations in non-taken branches is no longer supported. It's a poor programming behavior, and I haven't seen any programs that take advantage of this.

[d0cd]

Big fan of this proposal! It's important to give developers the semantics they expect.
We should be sure that the implementations are correct before they are rolled out.
I'd recommend an audit on the new opcodes (and possibly existing ones, if not yet audited) and formally verifying the new implementations.

[bendyarm]

@d0cd Thanks for the suggestions! I added a short section on auditing and formal verification.