fix: global state object in yul formal specification

This commit is contained in:
Quentin Garchery 2022-07-28 11:12:14 +02:00
parent 72f1907298
commit b3fd11a66f
No known key found for this signature in database
GPG Key ID: 7A0027EE6A3DB63B

View File

@ -663,10 +663,10 @@ We will use a destructuring notation for the AST nodes.
E(G, L, <var_1, ..., var_n := rhs>: Assignment) = E(G, L, <var_1, ..., var_n := rhs>: Assignment) =
let G1, L1, v1, ..., vn = E(G, L, rhs) let G1, L1, v1, ..., vn = E(G, L, rhs)
let L2 be a copy of L1 where L2[$var_i] = vi for i = 1, ..., n let L2 be a copy of L1 where L2[$var_i] = vi for i = 1, ..., n
G, L2, regular G1, L2, regular
E(G, L, <for { i1, ..., in } condition post body>: ForLoop) = E(G, L, <for { i1, ..., in } condition post body>: ForLoop) =
if n >= 1: if n >= 1:
let G1, L, mode = E(G, L, i1, ..., in) let G1, L1, mode = E(G, L, i1, ..., in)
// mode has to be regular or leave due to the syntactic restrictions // mode has to be regular or leave due to the syntactic restrictions
if mode is leave then if mode is leave then
G1, L1 restricted to variables of L, leave G1, L1 restricted to variables of L, leave
@ -686,7 +686,7 @@ We will use a destructuring notation for the AST nodes.
else: else:
G3, L3, mode = E(G2, L2, post) G3, L3, mode = E(G2, L2, post)
if mode is leave: if mode is leave:
G2, L3, leave G3, L3, leave
otherwise otherwise
E(G3, L3, for {} condition post body) E(G3, L3, for {} condition post body)
E(G, L, break: BreakContinue) = E(G, L, break: BreakContinue) =