From 0f4e43a8b24b52b8ebfb48fbeaa4f198042f38e7 Mon Sep 17 00:00:00 2001 From: Eric McCarthy Date: Sun, 9 Mar 2025 17:56:14 -0700 Subject: [PATCH 1/7] new version of ARC-0004 Flagged Operations for Conditional Code --- arc-0004/README.md | 174 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 174 insertions(+) create mode 100644 arc-0004/README.md diff --git a/arc-0004/README.md b/arc-0004/README.md new file mode 100644 index 0000000..96edf15 --- /dev/null +++ b/arc-0004/README.md @@ -0,0 +1,174 @@ +--- +arc: 4 Add an unused ARC number. **DO NOT ADD LEADING ZEROS.** +title: Flagged Operations for Conditional Code +authors: @bendyarm, @d0cd, @acoglio, @mikebenfield +discussion: [https://github.com/ProvableHQ/ARCs/discussions/89](89) +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. + +```leo +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. + +| Current Halting Opcode | New Flagged Opcode | notes | +|:-------------------:|:-----------------------:|:--------------------------:| +| abs | abs.flagged | +| add | add.flagged | +| 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. +| commit.bhp256 | commit.bhp256.flagged | +| commit.bhp512 | commit.bhp512.flagged | +| commit.bhp768 | commit.bhp768.flagged | +| commit.bhp768 | commit.bhp1024.flagged | +| commit.ped64 | commit.ped64.flagged | +| commit.ped128 | commit.ped128.flagged | +| 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. +| hash.bhp256 | hash.bhp256.flagged | +| hash.bhp512 | hash.bhp512.flagged | +| hash.bhp768 | hash.bhp768.flagged | +| hash.bhp1024 | hash.bhp1024.flagged | +| hash.ped64 | hash.ped64.flagged | +| hash.ped128 | hash.ped128.flagged | +| inv | inv.flagged | +| mod | mod.flagged | +| mul | mul.flagged | +| neg | neg.flagged | +| pow | pow.flagged | +| 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 | + +### 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, f 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). + + +## 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](https://developer.aleo.org/guides/introduction/getting_started) +and [for Leo](https://docs.leo-lang.org/getting_started/installation). + +``` +// 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](https://developer.aleo.org/guides/aleo/commands) and the [Leo CLI](https://docs.leo-lang.org/cli/overview) to make programs and run them. + +This PoC fixes [this Leo issue](https://github.com/ProvableHQ/leo/issues/27482). +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 + +This section should provide any materials that would help reviewers have better context on the nature of the ARC proposal. + +Example Leo bug: +https://github.com/AleoHQ/leo/issues/27482 From 9f2aad397e5211a36d66477cb0fd35a83d93b17b Mon Sep 17 00:00:00 2001 From: Eric McCarthy Date: Sun, 9 Mar 2025 18:01:07 -0700 Subject: [PATCH 2/7] cleanup on arc: field --- arc-0004/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/arc-0004/README.md b/arc-0004/README.md index 96edf15..debc638 100644 --- a/arc-0004/README.md +++ b/arc-0004/README.md @@ -1,5 +1,5 @@ --- -arc: 4 Add an unused ARC number. **DO NOT ADD LEADING ZEROS.** +arc: 4 title: Flagged Operations for Conditional Code authors: @bendyarm, @d0cd, @acoglio, @mikebenfield discussion: [https://github.com/ProvableHQ/ARCs/discussions/89](89) From 104feefc7290019e00d6e50d42bd0e8b9d662c2f Mon Sep 17 00:00:00 2001 From: Eric McCarthy Date: Sun, 9 Mar 2025 18:15:23 -0700 Subject: [PATCH 3/7] remove lefttover comment in references section --- arc-0004/README.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/arc-0004/README.md b/arc-0004/README.md index debc638..2c73556 100644 --- a/arc-0004/README.md +++ b/arc-0004/README.md @@ -168,7 +168,5 @@ This change does not affect security or regulatory issues. ## References -This section should provide any materials that would help reviewers have better context on the nature of the ARC proposal. - Example Leo bug: https://github.com/AleoHQ/leo/issues/27482 From 2dfa282b3506e742b6e13ddebb147fc0651b05fd Mon Sep 17 00:00:00 2001 From: Eric McCarthy Date: Mon, 10 Mar 2025 12:15:26 -0700 Subject: [PATCH 4/7] [arc-0004] Add note about which types of operands the flagged operations are needed for. --- arc-0004/README.md | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) diff --git a/arc-0004/README.md b/arc-0004/README.md index 2c73556..ec5856a 100644 --- a/arc-0004/README.md +++ b/arc-0004/README.md @@ -61,13 +61,20 @@ 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 | 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. +| cast | cast.flagged | As of now, docs don't say what causes cast to halt. TBD. | commit.bhp256 | commit.bhp256.flagged | | commit.bhp512 | commit.bhp512.flagged | | commit.bhp768 | commit.bhp768.flagged | @@ -84,9 +91,9 @@ use by compilers. | hash.ped128 | hash.ped128.flagged | | inv | inv.flagged | | mod | mod.flagged | -| mul | mul.flagged | -| neg | neg.flagged | -| pow | pow.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. @@ -94,7 +101,7 @@ use by compilers. || | 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 | sub.flagged | sub.flagged implemented only for integer types. ### Test Cases From 574a51f065ca7563adb0a54ebd14cd27fa0c5124 Mon Sep 17 00:00:00 2001 From: Eric McCarthy Date: Mon, 10 Mar 2025 12:22:11 -0700 Subject: [PATCH 5/7] [arc-0004] Remove atsigns preceding github usernames because it confuses YAML --- arc-0004/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/arc-0004/README.md b/arc-0004/README.md index ec5856a..defe582 100644 --- a/arc-0004/README.md +++ b/arc-0004/README.md @@ -1,7 +1,7 @@ --- arc: 4 title: Flagged Operations for Conditional Code -authors: @bendyarm, @d0cd, @acoglio, @mikebenfield +authors: bendyarm, d0cd, acoglio, mikebenfield discussion: [https://github.com/ProvableHQ/ARCs/discussions/89](89) topic: Protocol status: Draft From c7a715942a40c65dd4be7f4f051b175b62b3d770 Mon Sep 17 00:00:00 2001 From: Eric McCarthy Date: Tue, 25 Mar 2025 20:40:20 -0700 Subject: [PATCH 6/7] [arc-0004] remove commit.bhp* hash.bhp* commit.ped* and hash.ped* from the list of current halting opcodes --- arc-0004/README.md | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/arc-0004/README.md b/arc-0004/README.md index defe582..8017701 100644 --- a/arc-0004/README.md +++ b/arc-0004/README.md @@ -75,20 +75,8 @@ for these cases in the table below. | 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. -| commit.bhp256 | commit.bhp256.flagged | -| commit.bhp512 | commit.bhp512.flagged | -| commit.bhp768 | commit.bhp768.flagged | -| commit.bhp768 | commit.bhp1024.flagged | -| commit.ped64 | commit.ped64.flagged | -| commit.ped128 | commit.ped128.flagged | | 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. -| hash.bhp256 | hash.bhp256.flagged | -| hash.bhp512 | hash.bhp512.flagged | -| hash.bhp768 | hash.bhp768.flagged | -| hash.bhp1024 | hash.bhp1024.flagged | -| hash.ped64 | hash.ped64.flagged | -| hash.ped128 | hash.ped128.flagged | | inv | inv.flagged | | mod | mod.flagged | | mul | mul.flagged | mul.flagged implemented only for integer types. From e05ad0de3ef2370853eda0e9cac16dfb073e4174 Mon Sep 17 00:00:00 2001 From: Eric McCarthy Date: Wed, 23 Apr 2025 08:13:28 -0700 Subject: [PATCH 7/7] [arc-0004] add small section on auditing and formal verification --- arc-0004/README.md | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/arc-0004/README.md b/arc-0004/README.md index 8017701..8e3e00b 100644 --- a/arc-0004/README.md +++ b/arc-0004/README.md @@ -94,17 +94,21 @@ for these cases in the table below. ### 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, f there are two arguments, we need to test all four +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. +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