Skip to content

# Syntax: Change rewrite arrow to <- #192

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 3 commits into
base: main
Choose a base branch
from
Open

# Syntax: Change rewrite arrow to <- #192

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
4b42993
Add LARROW symbol and update syntax for storage operations
mrscottyrose Apr 18, 2025
9ca7ca7
Refactor postconditions: update constructor parameters and storage op…
mrscottyrose Apr 28, 2025
c919e32
Update storage operations to use LARROW syntax across multiple test f…
mrscottyrose May 3, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions src/Act/Lex.x
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -90,6 +90,7 @@ tokens :-
-- symbols
":=" { mk ASSIGN }
"=>" { mk ARROW }
"<-" { mk LARROW }
"|->" { mk POINTSTO }
"==" { mk EQEQ }
"=/=" { mk NEQ }
Expand Down Expand Up @@ -186,6 +187,8 @@ data LEX =
-- symbols
| ASSIGN
| ARROW
| LARROW
| POINTSTO
| EQEQ
| NEQ
| GE
Expand Down
3 changes: 2 additions & 1 deletion src/Act/Parse.y
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,6 +77,7 @@ import Act.Error
-- symbols
':=' { L ASSIGN _ }
'=>' { L ARROW _ }
'<-' { L LARROW _ }
'|->' { L POINTSTO _ }
'==' { L EQEQ _ }
'=/=' { L NEQ _ }
Expand Down Expand Up @@ -209,7 +210,7 @@ Storage : 'storage' nonempty(Store) { $2 }
Precondition : 'iff' nonempty(Expr) { Iff (posn $1) $2 }
| 'iff in range' AbiType nonempty(Expr) { IffIn (posn $1) $2 $3 }

Store : Entry '=>' Expr { Rewrite $1 $3 }
Store : Entry '<-' Expr { Rewrite $1 $3 }

Entry : id { EVar (posn $1) (name $1) }
| Entry '[' Expr ']' list(Index) { EMapping (posn $2) $1 ($3:$5) }
Expand Down
2 changes: 1 addition & 1 deletion src/Act/Print.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -165,7 +165,7 @@ prettyLocation :: StorageLocation t -> String
prettyLocation (Loc _ item) = prettyItem item

prettyUpdate :: StorageUpdate t -> String
prettyUpdate (Update _ item e) = prettyItem item <> " => " <> prettyExp e
prettyUpdate (Update _ item e) = prettyItem item <> " <- " <> prettyExp e

prettyEnv :: EthEnv -> String
prettyEnv e = case e of
Expand Down
18 changes: 9 additions & 9 deletions tests/coq/ERC20/erc20.act
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,8 @@ case CALLER =/= to:

storage

balanceOf[CALLER] => balanceOf[CALLER] - value
balanceOf[to] => balanceOf[to] + value
balanceOf[CALLER] <- balanceOf[CALLER] - value
balanceOf[to] <- balanceOf[to] + value

returns 1

Expand All @@ -45,27 +45,27 @@ case src =/= dst and CALLER == src:

storage

balanceOf[src] => balanceOf[src] - amount
balanceOf[dst] => balanceOf[dst] + amount
balanceOf[src] <- balanceOf[src] - amount
balanceOf[dst] <- balanceOf[dst] + amount

returns 1

case src =/= dst and CALLER =/= src and allowance[src][CALLER] == 2^256 - 1:

storage

balanceOf[src] => balanceOf[src] - amount
balanceOf[dst] => balanceOf[dst] + amount
balanceOf[src] <- balanceOf[src] - amount
balanceOf[dst] <- balanceOf[dst] + amount

returns 1

case src =/= dst and CALLER =/= src and allowance[src][CALLER] < 2^256 - 1:

storage

allowance[src][CALLER] => allowance[src][CALLER] - amount
balanceOf[src] => balanceOf[src] - amount
balanceOf[dst] => balanceOf[dst] + amount
allowance[src][CALLER] <- allowance[src][CALLER] - amount
balanceOf[src] <- balanceOf[src] - amount
balanceOf[dst] <- balanceOf[dst] + amount

returns 1

Expand Down
10 changes: 5 additions & 5 deletions tests/coq/multi/multi.act
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,14 +11,14 @@ interface setx(uint z)

storage

a.x => z
a.x <- z

behaviour setf of B
interface setf(address i)

storage

a.f[i] => 1
a.f[i] <- 1

// Contract A
constructor of A
Expand All @@ -41,12 +41,12 @@ interface setf(address i)

storage

b.a.f[i] => 2
b.a.f[i] <- 2

behaviour setxw of C
interface setxw(address i)

storage

b.a.x => 1
b.x => 1
b.a.x <- 1
b.x <- 1
4 changes: 2 additions & 2 deletions tests/coq/token/token.act
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,8 @@ case CALLER =/= to:

storage

balances[CALLER] => balances[CALLER] - amt
balances[to] => balances[to] + amt
balances[CALLER] <- balances[CALLER] - amt
balances[to] <- balances[to] + amt

returns 1

Expand Down
6 changes: 3 additions & 3 deletions tests/coq/transitions/state_machine.act
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,20 +13,20 @@ interface f()
iff x == 0

storage
x => 1
x <- 1

behaviour g of StateMachine
interface g()

iff x == 1

storage
x => 2
x <- 2

behaviour h of StateMachine
interface h()

iff x == 2

storage
x => 0
x <- 0
4 changes: 2 additions & 2 deletions tests/frontend/fail/case-fail1.act
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,9 +13,9 @@ iff
case z == 0:

storage
x => z
x <- z

case z >= 2:

storage
x => z + 1
x <- z + 1
4 changes: 2 additions & 2 deletions tests/frontend/fail/case-fail2.act
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,9 +13,9 @@ iff
case z == 0:

storage
x => z
x <- z

case z >= 1:

storage
x => z + 1
x <- z + 1
6 changes: 3 additions & 3 deletions tests/frontend/pass/case/case.act
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,14 +13,14 @@ iff
case z == 0:

storage
x => z
x <- z

case z == 1:

storage
x => z + 1
x <- z + 1

case z > 1:

storage
x => z + 2
x <- z + 2
12 changes: 6 additions & 6 deletions tests/frontend/pass/dss/vat.act
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,9 +45,9 @@ iff

storage

urns[i][u].ink => urns[i][u].ink + dink
urns[i][u].art => urns[i][u].art + dart
ilks[i].Art => ilks[i].Art + dart
gem[i][v] => gem[i][v] - dink
dai[w] => dai[w] + ilks[i].rate * dart
debt => debt + ilks[i].rate * dart
urns[i][u].ink <- urns[i][u].ink + dink
urns[i][u].art <- urns[i][u].art + dart
ilks[i].Art <- ilks[i].Art + dart
gem[i][v] <- gem[i][v] - dink
dai[w] <- dai[w] + ilks[i].rate * dart
debt <- debt + ilks[i].rate * dart
6 changes: 3 additions & 3 deletions tests/frontend/pass/multi/multi.act
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ iff
CALLVALUE == 0

storage
a.x => z
a.x <- z

behaviour multi of B
interface multi(uint z)
Expand All @@ -27,5 +27,5 @@ iff
CALLVALUE == 0

storage
y => 1
a.x => z
y <- 1
a.x <- z
2 changes: 1 addition & 1 deletion tests/frontend/pass/storageread0.act
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,5 +11,5 @@ interface f()

storage

x => y
x <- y
y
2 changes: 1 addition & 1 deletion tests/frontend/pass/storageread1.act
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ iff in range uint256
storage

// TODO: remove this hack once bug #81 is fixed...
x => x
x <- x
y

returns x + y
2 changes: 1 addition & 1 deletion tests/frontend/pass/storageread2.act
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,5 +20,5 @@ interface f()

storage C

x => y
x <- y
y
30 changes: 21 additions & 9 deletions tests/frontend/pass/token/transfer.act
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,8 +29,8 @@ case CALLER =/= to:

storage

balanceOf[CALLER] => balanceOf[CALLER] - value
balanceOf[to] => balanceOf[to] + value
balanceOf[CALLER] <- balanceOf[CALLER] - value
balanceOf[to] <- balanceOf[to] + value

returns 1

Expand All @@ -53,31 +53,43 @@ case src =/= dst and CALLER == src:

storage

balanceOf[src] => balanceOf[src] - amount
balanceOf[dst] => balanceOf[dst] + amount
balanceOf[src] <- balanceOf[src] - amount
balanceOf[dst] <- balanceOf[dst] + amount

returns 1

case src =/= dst and CALLER =/= src and allowance[src][CALLER] == 2^256 - 1:

storage

balanceOf[src] => balanceOf[src] - amount
balanceOf[dst] => balanceOf[dst] + amount
balanceOf[src] <- balanceOf[src] - amount
balanceOf[dst] <- balanceOf[dst] + amount

returns 1

case src =/= dst and CALLER =/= src and allowance[src][CALLER] < 2^256 - 1:

storage

allowance[src][CALLER] => allowance[src][CALLER] - amount
balanceOf[src] => balanceOf[src] - amount
balanceOf[dst] => balanceOf[dst] + amount
allowance[src][CALLER] <- allowance[src][CALLER] - amount
balanceOf[src] <- balanceOf[src] - amount
balanceOf[dst] <- balanceOf[dst] + amount

returns 1

case src == dst:

storage

balanceOf[src] <- balanceOf[src] - amount
balanceOf[dst] <- balanceOf[dst] + amount

returns 1

case CALLER =/= src:

storage

allowance[src][CALLER] <- allowance[src][CALLER] - amount
balanceOf[src] <- balanceOf[src] - amount
balanceOf[dst] <- balanceOf[dst] + amount
2 changes: 1 addition & 1 deletion tests/hevm/fail/redundant/redundant.act
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,4 +19,4 @@ iff

storage

x => 2
x <- 2
20 changes: 10 additions & 10 deletions tests/hevm/pass/amm/amm.act
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,8 +30,8 @@ case from =/= to:

storage

balanceOf[from] => balanceOf[from] - value
balanceOf[to] => balanceOf[to] + value
balanceOf[from] <- balanceOf[from] - value
balanceOf[to] <- balanceOf[to] + value

returns 1

Expand Down Expand Up @@ -74,11 +74,11 @@ case CALLER =/= THIS:

storage

token0.balanceOf[CALLER] => token0.balanceOf[CALLER] - amt
token0.balanceOf[THIS] => token0.balanceOf[THIS] + amt
token0.balanceOf[CALLER] <- token0.balanceOf[CALLER] - amt
token0.balanceOf[THIS] <- token0.balanceOf[THIS] + amt

token1.balanceOf[THIS] => token1.balanceOf[THIS] - ((token1.balanceOf[THIS] * amt) / (token0.balanceOf[THIS] + amt))
token1.balanceOf[CALLER] => token1.balanceOf[CALLER] + ((token1.balanceOf[THIS] * amt) / (token0.balanceOf[THIS] + amt))
token1.balanceOf[THIS] <- token1.balanceOf[THIS] - ((token1.balanceOf[THIS] * amt) / (token0.balanceOf[THIS] + amt))
token1.balanceOf[CALLER] <- token1.balanceOf[CALLER] + ((token1.balanceOf[THIS] * amt) / (token0.balanceOf[THIS] + amt))

returns 1

Expand Down Expand Up @@ -109,11 +109,11 @@ case CALLER =/= THIS:

storage

token1.balanceOf[CALLER] => token1.balanceOf[CALLER] - amt
token1.balanceOf[THIS] => token1.balanceOf[THIS] + amt
token1.balanceOf[CALLER] <- token1.balanceOf[CALLER] - amt
token1.balanceOf[THIS] <- token1.balanceOf[THIS] + amt

token0.balanceOf[THIS] => token0.balanceOf[THIS] - ((token0.balanceOf[THIS] * amt) / (token1.balanceOf[THIS] + amt))
token0.balanceOf[CALLER] => token0.balanceOf[CALLER] + ((token0.balanceOf[THIS] * amt) / (token1.balanceOf[THIS] + amt))
token0.balanceOf[THIS] <- token0.balanceOf[THIS] - ((token0.balanceOf[THIS] * amt) / (token1.balanceOf[THIS] + amt))
token0.balanceOf[CALLER] <- token0.balanceOf[CALLER] + ((token0.balanceOf[THIS] * amt) / (token1.balanceOf[THIS] + amt))

returns 1

Expand Down
8 changes: 4 additions & 4 deletions tests/hevm/pass/cast-3/cast-3.act
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,8 +30,8 @@ case CALLER =/= to:

storage

balanceOf[CALLER] => balanceOf[CALLER] - value
balanceOf[to] => balanceOf[to] + value
balanceOf[CALLER] <- balanceOf[CALLER] - value
balanceOf[to] <- balanceOf[to] + value

returns 1

Expand Down Expand Up @@ -67,8 +67,8 @@ case CALLER =/= THIS:

storage

token.balanceOf[CALLER] => token.balanceOf[CALLER] + 1
token.balanceOf[THIS] => token.balanceOf[THIS] - 1
token.balanceOf[CALLER] <- token.balanceOf[CALLER] + 1
token.balanceOf[THIS] <- token.balanceOf[THIS] - 1

returns 1

Expand Down
Loading
Loading