[Bug] multiple returns allowed

[0rphon]

🐛 Bug Report

Code snippet to reproduce

function main () -> u8 {
    return 1u8;
    let x: u8 = 1u8;
    return x;
}

Stack trace & error message

     Build Starting...
     Build Compiling main program... ("/home/0rphon/Work/Aleo/leo-playground/src/main.leo")
     Build Complete
      Done Finished in 0 milliseconds

Your Environment

• testnet3 commit d43605538d1fcb225b21c07bb76c1a8708613213

[acoglio]

This relates to #1847.

[Centril]

My take on this is that per approach 2 in https://github.com/AleoHQ/leo/issues/1847#issuecomment-1142077457, this should not fail, i.e. this isn't a bug.

[0rphon]

what about the following case? none of this is dead code yet it would have been considered illegal before but now passes

function main(a: u8) -> u8 {
    if a == 0u8 {
        return 1u8;
    }
    let b: u8 = a - 1u8;
    if b == a {
        return a;
    }
    return 0u8;
}

[acoglio]

Why was this considered illegal before? (I mean, the latter example.)

[0rphon]

im not really certain about the design decisions on why, but early returns werent allowed. so the above code would need to be written like so to be considered valid

function main(a: u8) -> u8 {
    if a == 0u8 {
        return 1u8;
    } else {
        let b: u8 = a - 1u8;
        if b == a {
            return a;
        } else {
            return 0u8;
        }
    }
}

[0rphon]

i tried running the illegal example on master just to confirm and got the following

     Build Starting...
     Build Compiling main program... ("E:\\Work\\Aleo\\leo-playground\\src/main.leo")
      Done Finished in 41 milliseconds 

Error [EASG0373034]: function 'main' failed to validate return path: 'cannot have asymmetrical return in if statement'
    --> E:\Work\Aleo\leo-playground\src/main.leo:2:5
     |
   2 |     if a == 0u8 {
   3 |          ...
   4 |     }
     |     ^

[0rphon]

found the exact pr that made the code illegal https://github.com/AleoHQ/leo/pull/469

[acoglio]

Thanks for digging that up.

I think that the motivation was ease of compilation to R1CS, but it should be relatively easy to allow that code, which is natural to write, by making the ifs "balanced" with respect to the returns. We need to flatten all the ifs anyways. In particular, it is fairly easy to transform

if ... {
    return ...;
}
...
return ...;

into

if ... {
    return ...;
} else {
    ...
    return ...;
}
The current static semantics of Leo (in the Leo Reference and in the ACL2 formalization) allows code like this, so if we wanted to prohibit it we would have to make the static semantics more restrictive.

[gluax]

I won't make any decisions until we reach an agreement in #1847. Though I do realize according to the current spec we are supposed to follow the first approach there. However, might as well wait before making any changes on a final decision.

[collinc97]

Dead code is not allowed in Leo programs. The above program will give the following error on Leo v1.6.2.

Error [ETYC0372025]: Cannot reach the following statement.
    --> src/main.leo:5:9
     |
   5 |         return x;
     |         ^^^^^^^^^
     |
     = Remove the unreachable code.