Spec: question about variables escaping scope

[jakzale]

I have a question regarding protocol/sapling.pdf, but I suppose it applies to to other specs as well.

Given that the spec is deliberately general and Notation (Section 2) omits the rules for

• variables and scopes, and as a consequence
• let keyword,
• set keyword,
• return keyword, and
• for keyword when used outside of sequence comprehension,

I assumed lexical scoping for variables.

However, there is a case of variable escaping local scope in Variable-base Affine-ctEdwards scalar multiplication, where Acc_250 is used outside of body of the for loop:

As this is the only case of variable escaping local scope in the spec, does the spec rely on variables escaping local scopes in any way? Does the spec rely on any variable scoping semantics?

Following the style of code snippets from BLAKE2 hashes (A.3.7), can the above scope be reformulated to obey lexical scoping by using the return and set keywords?

let Base = B
let Acc^u = k_0 ? Base^u : 0
let Acc^v = k_0 ? Base^v : 1
for i from 1 up to 250:
    set Base = [2] Base
    let Addend^u = k_i ? Base^u : 0
    let Addend^v = k_i ? Base^v : 1
    set Acc := Acc + Addend
return Acc

[daira]

It's pseudocode, not a well-defined language. That said, the intent is that let bindings last until the end of the algorithm, which is harmless because they introduce immutable uniquely named variables — shadowing is prohibited, and I think there are no cases where we introduce a variable with a let binding and then mutate it. (In a few places we use "Initialize" to introduce mutable variables.)

This is not actually the only case of let bindings escaping their lexical scope; there are several in if/else statements. For example, ock and op are defined in each branch of an if/else, in the encryption algorithm of section 4.17.1. (In the 'if' branch 'let' is spelled 'choose'; it could have been written as "let ock <-R- Sym.K" and "let op <-R- BY^{[ell_J+256)/8]}".)

I were designing a real programming language then I'd probably require strict lexical scoping.

Also note that the pseudo-language has evolved over time and algorithms are written in two different styles. (The older style uses English sentences starting with a capital letter, such as in sections 4.18 and 4.19, as opposed to the more programming-language-like style that uses lowercase keywords.)

[jakzale]

I think there are no cases where we introduce a variable with a let binding and then mutate it.

I thought that the set keyword was used for mutating variables in the definition of BLAKE2s-256:

This is not actually the only case of let bindings escaping their lexical scope; there are several in if/else statements.

Ah, thank you for pointing that out.

[daira]

I think there are no cases where we introduce a variable with a let binding and then mutate it.

I thought that the set keyword was used for mutating variables in the definition of BLAKE2s-256:

Yes, that's a bug. Thankyou for pointing it out! I will change it to explicitly mark that the let binding is mutable.