From 4b42993316546d6aaeea7a8bd481e7d69939c7e0 Mon Sep 17 00:00:00 2001 From: Scott Rose Date: Fri, 18 Apr 2025 05:55:22 -0500 Subject: [PATCH 1/4] Add LARROW symbol and update syntax for storage operations --- src/Act/Lex.x | 3 +++ src/Act/Parse.y | 3 ++- src/Act/Print.hs | 2 +- 3 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/Act/Lex.x b/src/Act/Lex.x index b33f827d..d4f0c5f7 100644 --- a/src/Act/Lex.x +++ b/src/Act/Lex.x @@ -90,6 +90,7 @@ tokens :- -- symbols ":=" { mk ASSIGN } "=>" { mk ARROW } + "<-" { mk LARROW } "|->" { mk POINTSTO } "==" { mk EQEQ } "=/=" { mk NEQ } @@ -186,6 +187,8 @@ data LEX = -- symbols | ASSIGN | ARROW + | LARROW + | POINTSTO | EQEQ | NEQ | GE diff --git a/src/Act/Parse.y b/src/Act/Parse.y index d3a3f372..bfd3dd29 100644 --- a/src/Act/Parse.y +++ b/src/Act/Parse.y @@ -77,6 +77,7 @@ import Act.Error -- symbols ':=' { L ASSIGN _ } '=>' { L ARROW _ } + '<-' { L LARROW _ } '|->' { L POINTSTO _ } '==' { L EQEQ _ } '=/=' { L NEQ _ } @@ -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) } diff --git a/src/Act/Print.hs b/src/Act/Print.hs index 076a2ea7..7912edc6 100644 --- a/src/Act/Print.hs +++ b/src/Act/Print.hs @@ -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 From 9ca7ca7e34799e3fb81f2f39b5ff72e998c083fd Mon Sep 17 00:00:00 2001 From: Scott Rose Date: Mon, 28 Apr 2025 08:52:07 -0500 Subject: [PATCH 2/4] Refactor postconditions: update constructor parameters and storage operations for consistency --- tests/postconditions/pass/assignment_poststate.act | 14 ++++++++++++++ tests/postconditions/pass/assignment_prestate.act | 13 +++++-------- tests/postconditions/pass/increase.act | 4 ++-- 3 files changed, 21 insertions(+), 10 deletions(-) create mode 100644 tests/postconditions/pass/assignment_poststate.act diff --git a/tests/postconditions/pass/assignment_poststate.act b/tests/postconditions/pass/assignment_poststate.act new file mode 100644 index 00000000..eb5029d0 --- /dev/null +++ b/tests/postconditions/pass/assignment_poststate.act @@ -0,0 +1,14 @@ +constructor of C +interface constructor(uint x0) + +creates + + uint x := x0 + +behaviour f of C +interface f() + +storage + x <- post(x) + +returns post(x) \ No newline at end of file diff --git a/tests/postconditions/pass/assignment_prestate.act b/tests/postconditions/pass/assignment_prestate.act index b7325cc6..15837d0a 100644 --- a/tests/postconditions/pass/assignment_prestate.act +++ b/tests/postconditions/pass/assignment_prestate.act @@ -1,17 +1,14 @@ constructor of C -interface constructor(uint24 _x) +interface constructor(uint x0) creates - uint24 x := _x + uint x := x0 behaviour f of C -interface f(uint24 y) +interface f() storage + x <- pre(x) - x => x + y - -ensures - - post(x) == pre(x) + y +returns pre(x) diff --git a/tests/postconditions/pass/increase.act b/tests/postconditions/pass/increase.act index c8bf3e37..d210110d 100644 --- a/tests/postconditions/pass/increase.act +++ b/tests/postconditions/pass/increase.act @@ -10,13 +10,13 @@ interface increase(uint24 new_x) case new_x > x: storage - x => new_x + x <- new_x returns post(x) - pre(x) case new_x <= x: storage - x => x + new_x + x <- x + new_x returns post(x) - pre(x) From c919e329df388c078b0b0b795c4ca0147a184399 Mon Sep 17 00:00:00 2001 From: Scott Rose Date: Sat, 3 May 2025 13:13:28 -0500 Subject: [PATCH 3/4] Update storage operations to use LARROW syntax across multiple test files for consistency --- tests/coq/ERC20/erc20.act | 18 +++++------ tests/coq/multi/multi.act | 10 +++---- tests/coq/token/token.act | 4 +-- tests/coq/transitions/state_machine.act | 6 ++-- tests/frontend/fail/case-fail1.act | 4 +-- tests/frontend/fail/case-fail2.act | 4 +-- tests/frontend/pass/case/case.act | 6 ++-- tests/frontend/pass/dss/vat.act | 12 ++++---- tests/frontend/pass/multi/multi.act | 6 ++-- tests/frontend/pass/storageread0.act | 2 +- tests/frontend/pass/storageread1.act | 2 +- tests/frontend/pass/storageread2.act | 2 +- tests/frontend/pass/token/transfer.act | 30 +++++++++++++------ tests/hevm/fail/redundant/redundant.act | 2 +- tests/hevm/pass/amm/amm.act | 20 ++++++------- tests/hevm/pass/cast-3/cast-3.act | 8 ++--- tests/hevm/pass/cast-4/cast-4.act | 4 +-- tests/hevm/pass/cast/cast.act | 6 ++-- tests/hevm/pass/layout4/layout4.act | 4 +-- tests/hevm/pass/maps/maps.act | 2 +- tests/hevm/pass/multi/multi.act | 8 ++--- tests/hevm/pass/multi2/multi2.act | 2 +- tests/hevm/pass/multi3/multi3.act | 10 +++---- tests/hevm/pass/multi4/multi4.act | 4 +-- tests/hevm/pass/shape/shape.act | 4 +-- tests/hevm/pass/simple/simple.act | 2 +- .../hevm/pass/state_machine/state_machine.act | 6 ++-- .../pass/transfer-simple/transfer-simple.act | 4 +-- tests/hevm/pass/transfer/transfer.act | 18 +++++------ .../fail/duplicated_argument_name.act | 2 +- tests/invariants/fail/ethEnv.act | 22 +++++++------- tests/invariants/fail/non-inductive.act | 6 ++-- tests/invariants/pass/amm.act | 8 ++--- tests/invariants/pass/case.act | 4 +-- tests/invariants/pass/homogeneous.act | 8 ++--- tests/invariants/pass/ite.act | 8 ++--- tests/invariants/pass/log.act | 4 +-- tests/invariants/pass/mutex.act | 2 +- tests/invariants/pass/state_machine.act | 6 ++-- tests/postconditions/fail/bad_assignment.act | 2 +- .../fail/bad_assignment_prestate.act | 2 +- tests/postconditions/pass/amm.act | 20 ++++++------- tests/postconditions/pass/assignment.act | 2 +- .../pass/assignment_poststate.act | 5 +++- .../pass/assignment_prestate.act | 3 ++ .../postconditions/pass/assignment_return.act | 2 +- 46 files changed, 166 insertions(+), 150 deletions(-) diff --git a/tests/coq/ERC20/erc20.act b/tests/coq/ERC20/erc20.act index 17d7096c..9c0caa2e 100644 --- a/tests/coq/ERC20/erc20.act +++ b/tests/coq/ERC20/erc20.act @@ -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 @@ -45,8 +45,8 @@ 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 @@ -54,8 +54,8 @@ 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 @@ -63,9 +63,9 @@ 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 diff --git a/tests/coq/multi/multi.act b/tests/coq/multi/multi.act index 5346715d..8c377ce4 100644 --- a/tests/coq/multi/multi.act +++ b/tests/coq/multi/multi.act @@ -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 @@ -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 diff --git a/tests/coq/token/token.act b/tests/coq/token/token.act index 69590f34..14b7a17f 100644 --- a/tests/coq/token/token.act +++ b/tests/coq/token/token.act @@ -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 diff --git a/tests/coq/transitions/state_machine.act b/tests/coq/transitions/state_machine.act index 308ebac5..ec214a60 100644 --- a/tests/coq/transitions/state_machine.act +++ b/tests/coq/transitions/state_machine.act @@ -13,7 +13,7 @@ interface f() iff x == 0 storage - x => 1 + x <- 1 behaviour g of StateMachine interface g() @@ -21,7 +21,7 @@ interface g() iff x == 1 storage - x => 2 + x <- 2 behaviour h of StateMachine interface h() @@ -29,4 +29,4 @@ interface h() iff x == 2 storage - x => 0 + x <- 0 diff --git a/tests/frontend/fail/case-fail1.act b/tests/frontend/fail/case-fail1.act index 0ec954ae..d6752b7f 100644 --- a/tests/frontend/fail/case-fail1.act +++ b/tests/frontend/fail/case-fail1.act @@ -13,9 +13,9 @@ iff case z == 0: storage - x => z + x <- z case z >= 2: storage - x => z + 1 \ No newline at end of file + x <- z + 1 \ No newline at end of file diff --git a/tests/frontend/fail/case-fail2.act b/tests/frontend/fail/case-fail2.act index 49156b8e..47df82f0 100644 --- a/tests/frontend/fail/case-fail2.act +++ b/tests/frontend/fail/case-fail2.act @@ -13,9 +13,9 @@ iff case z == 0: storage - x => z + x <- z case z >= 1: storage - x => z + 1 \ No newline at end of file + x <- z + 1 \ No newline at end of file diff --git a/tests/frontend/pass/case/case.act b/tests/frontend/pass/case/case.act index 589b652c..be9a9e75 100644 --- a/tests/frontend/pass/case/case.act +++ b/tests/frontend/pass/case/case.act @@ -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 \ No newline at end of file + x <- z + 2 \ No newline at end of file diff --git a/tests/frontend/pass/dss/vat.act b/tests/frontend/pass/dss/vat.act index 9aa2e344..ad7619dd 100644 --- a/tests/frontend/pass/dss/vat.act +++ b/tests/frontend/pass/dss/vat.act @@ -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 diff --git a/tests/frontend/pass/multi/multi.act b/tests/frontend/pass/multi/multi.act index 9dfbfc4a..7410a2ad 100644 --- a/tests/frontend/pass/multi/multi.act +++ b/tests/frontend/pass/multi/multi.act @@ -18,7 +18,7 @@ iff CALLVALUE == 0 storage - a.x => z + a.x <- z behaviour multi of B interface multi(uint z) @@ -27,5 +27,5 @@ iff CALLVALUE == 0 storage - y => 1 - a.x => z + y <- 1 + a.x <- z diff --git a/tests/frontend/pass/storageread0.act b/tests/frontend/pass/storageread0.act index 9e6abc56..71bd493b 100644 --- a/tests/frontend/pass/storageread0.act +++ b/tests/frontend/pass/storageread0.act @@ -11,5 +11,5 @@ interface f() storage - x => y + x <- y y diff --git a/tests/frontend/pass/storageread1.act b/tests/frontend/pass/storageread1.act index d62877d4..f593073f 100644 --- a/tests/frontend/pass/storageread1.act +++ b/tests/frontend/pass/storageread1.act @@ -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 diff --git a/tests/frontend/pass/storageread2.act b/tests/frontend/pass/storageread2.act index dce446dc..380ee7e6 100644 --- a/tests/frontend/pass/storageread2.act +++ b/tests/frontend/pass/storageread2.act @@ -20,5 +20,5 @@ interface f() storage C - x => y + x <- y y diff --git a/tests/frontend/pass/token/transfer.act b/tests/frontend/pass/token/transfer.act index d41e2726..f504dd5f 100644 --- a/tests/frontend/pass/token/transfer.act +++ b/tests/frontend/pass/token/transfer.act @@ -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 @@ -53,8 +53,8 @@ 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 @@ -62,8 +62,8 @@ 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 @@ -71,13 +71,25 @@ 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 diff --git a/tests/hevm/fail/redundant/redundant.act b/tests/hevm/fail/redundant/redundant.act index 57158094..12f42ece 100644 --- a/tests/hevm/fail/redundant/redundant.act +++ b/tests/hevm/fail/redundant/redundant.act @@ -19,4 +19,4 @@ iff storage - x => 2 \ No newline at end of file + x <- 2 \ No newline at end of file diff --git a/tests/hevm/pass/amm/amm.act b/tests/hevm/pass/amm/amm.act index e7a880eb..54609b24 100644 --- a/tests/hevm/pass/amm/amm.act +++ b/tests/hevm/pass/amm/amm.act @@ -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 @@ -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 @@ -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 diff --git a/tests/hevm/pass/cast-3/cast-3.act b/tests/hevm/pass/cast-3/cast-3.act index ff1e072d..8119458d 100644 --- a/tests/hevm/pass/cast-3/cast-3.act +++ b/tests/hevm/pass/cast-3/cast-3.act @@ -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 @@ -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 diff --git a/tests/hevm/pass/cast-4/cast-4.act b/tests/hevm/pass/cast-4/cast-4.act index c1c2b66a..4d17db92 100644 --- a/tests/hevm/pass/cast-4/cast-4.act +++ b/tests/hevm/pass/cast-4/cast-4.act @@ -41,5 +41,5 @@ iff storage - a1 => create A(42) - a2 => create A(43) \ No newline at end of file + a1 <- create A(42) + a2 <- create A(43) \ No newline at end of file diff --git a/tests/hevm/pass/cast/cast.act b/tests/hevm/pass/cast/cast.act index 20c20620..30753127 100644 --- a/tests/hevm/pass/cast/cast.act +++ b/tests/hevm/pass/cast/cast.act @@ -26,7 +26,7 @@ iff CALLVALUE == 0 storage - x => x1 + x <- x1 constructor of B @@ -53,5 +53,5 @@ iff CALLVALUE == 0 storage - a1.x => 42 - a2.x => 11 \ No newline at end of file + a1.x <- 42 + a2.x <- 11 \ No newline at end of file diff --git a/tests/hevm/pass/layout4/layout4.act b/tests/hevm/pass/layout4/layout4.act index e6ba27ca..2b32aa32 100644 --- a/tests/hevm/pass/layout4/layout4.act +++ b/tests/hevm/pass/layout4/layout4.act @@ -50,7 +50,7 @@ iff storage - f[key] => value + f[key] <- value returns 1 @@ -64,6 +64,6 @@ iff storage - g[key] => value + g[key] <- value returns 1 \ No newline at end of file diff --git a/tests/hevm/pass/maps/maps.act b/tests/hevm/pass/maps/maps.act index b060325a..e86bb578 100644 --- a/tests/hevm/pass/maps/maps.act +++ b/tests/hevm/pass/maps/maps.act @@ -37,6 +37,6 @@ iff storage - f[key] => value + f[key] <- value returns 1 \ No newline at end of file diff --git a/tests/hevm/pass/multi/multi.act b/tests/hevm/pass/multi/multi.act index 6a94273c..c6899e65 100644 --- a/tests/hevm/pass/multi/multi.act +++ b/tests/hevm/pass/multi/multi.act @@ -14,7 +14,7 @@ iff CALLVALUE == 0 storage - x => z + x <- z constructor of B @@ -34,7 +34,7 @@ iff CALLVALUE == 0 storage - a.x => z + a.x <- z returns 0 @@ -45,5 +45,5 @@ interface multi(uint z) iff CALLVALUE == 0 storage - y => z - a.x => 42 \ No newline at end of file + y <- z + a.x <- 42 \ No newline at end of file diff --git a/tests/hevm/pass/multi2/multi2.act b/tests/hevm/pass/multi2/multi2.act index f58065ab..949cfba7 100644 --- a/tests/hevm/pass/multi2/multi2.act +++ b/tests/hevm/pass/multi2/multi2.act @@ -25,7 +25,7 @@ iff CALLVALUE == 0 storage - x => z + x <- z constructor of B interface constructor(uint u) diff --git a/tests/hevm/pass/multi3/multi3.act b/tests/hevm/pass/multi3/multi3.act index 28b54f7c..3603e25d 100644 --- a/tests/hevm/pass/multi3/multi3.act +++ b/tests/hevm/pass/multi3/multi3.act @@ -29,7 +29,7 @@ iff storage - x => x + y + x <- x + y // contract B @@ -52,7 +52,7 @@ iff storage - z => z + 1 + z <- z + 1 behaviour a_add_x of B interface a_add_x(uint y) @@ -63,7 +63,7 @@ iff storage - a.x => a.x + y + a.x <- a.x + y // contract C @@ -91,7 +91,7 @@ iff storage - b.z => b.z + 1 - b.a.x => b.a.x + z + b.z <- b.z + 1 + b.a.x <- b.a.x + z returns z \ No newline at end of file diff --git a/tests/hevm/pass/multi4/multi4.act b/tests/hevm/pass/multi4/multi4.act index dcc495dd..78176ee6 100644 --- a/tests/hevm/pass/multi4/multi4.act +++ b/tests/hevm/pass/multi4/multi4.act @@ -29,7 +29,7 @@ iff storage - x => x + y + x <- x + y // contract B @@ -50,4 +50,4 @@ iff CALLVALUE == 0 storage - a => create A(42) + a <- create A(42) diff --git a/tests/hevm/pass/shape/shape.act b/tests/hevm/pass/shape/shape.act index 18dbd6a7..adb4ffa7 100644 --- a/tests/hevm/pass/shape/shape.act +++ b/tests/hevm/pass/shape/shape.act @@ -25,7 +25,7 @@ iff CALLVALUE == 0 storage - x => z + x <- z // contract B constructor of B @@ -77,4 +77,4 @@ iff CALLVALUE == 0 storage - b.a.x => 17 \ No newline at end of file + b.a.x <- 17 \ No newline at end of file diff --git a/tests/hevm/pass/simple/simple.act b/tests/hevm/pass/simple/simple.act index b8cc159f..133e66b2 100644 --- a/tests/hevm/pass/simple/simple.act +++ b/tests/hevm/pass/simple/simple.act @@ -18,6 +18,6 @@ iff storage - x[0] => 1 + x[0] <- 1 returns 1 \ No newline at end of file diff --git a/tests/hevm/pass/state_machine/state_machine.act b/tests/hevm/pass/state_machine/state_machine.act index 5b49ac22..9fee31e6 100644 --- a/tests/hevm/pass/state_machine/state_machine.act +++ b/tests/hevm/pass/state_machine/state_machine.act @@ -20,7 +20,7 @@ iff CALLVALUE == 0 storage - x => 1 + x <- 1 behaviour g of StateMachine interface g() @@ -31,7 +31,7 @@ iff x == 1 storage - x => 2 + x <- 2 behaviour h of StateMachine interface h() @@ -41,4 +41,4 @@ iff x == 2 storage - x => 0 + x <- 0 diff --git a/tests/hevm/pass/transfer-simple/transfer-simple.act b/tests/hevm/pass/transfer-simple/transfer-simple.act index 88733f3d..7094aa56 100644 --- a/tests/hevm/pass/transfer-simple/transfer-simple.act +++ b/tests/hevm/pass/transfer-simple/transfer-simple.act @@ -27,8 +27,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 diff --git a/tests/hevm/pass/transfer/transfer.act b/tests/hevm/pass/transfer/transfer.act index 41093330..8ffdd0d8 100644 --- a/tests/hevm/pass/transfer/transfer.act +++ b/tests/hevm/pass/transfer/transfer.act @@ -27,8 +27,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 @@ -58,8 +58,8 @@ case src =/= dst and CALLER == src: balanceOf[CALLER] allowance[src][CALLER] - balanceOf[src] => balanceOf[src] - amount - balanceOf[dst] => balanceOf[dst] + amount + balanceOf[src] <- balanceOf[src] - amount + balanceOf[dst] <- balanceOf[dst] + amount returns 1 @@ -69,8 +69,8 @@ case src =/= dst and CALLER =/= src and allowance[src][CALLER] == 2^256 - 1: balanceOf[CALLER] allowance[src][CALLER] - balanceOf[src] => balanceOf[src] - amount - balanceOf[dst] => balanceOf[dst] + amount + balanceOf[src] <- balanceOf[src] - amount + balanceOf[dst] <- balanceOf[dst] + amount returns 1 @@ -79,9 +79,9 @@ case src =/= dst and CALLER =/= src and allowance[src][CALLER] < 2^256 - 1: storage balanceOf[CALLER] - 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 diff --git a/tests/invariants/fail/duplicated_argument_name.act b/tests/invariants/fail/duplicated_argument_name.act index 7fcd902e..cf556b32 100644 --- a/tests/invariants/fail/duplicated_argument_name.act +++ b/tests/invariants/fail/duplicated_argument_name.act @@ -14,4 +14,4 @@ interface f(uint _x) storage - x => _x + x <- _x diff --git a/tests/invariants/fail/ethEnv.act b/tests/invariants/fail/ethEnv.act index 1326c75e..6be3f024 100644 --- a/tests/invariants/fail/ethEnv.act +++ b/tests/invariants/fail/ethEnv.act @@ -35,14 +35,14 @@ interface break() storage - this => 1 - value => 1 - depth => 1 - number => 1 - difficulty => 1 - chainid => 1 - gaslimit => 1 - coinbase => 1 - timestamp => 1 - nonce => 1 - hash => 1 + this <- 1 + value <- 1 + depth <- 1 + number <- 1 + difficulty <- 1 + chainid <- 1 + gaslimit <- 1 + coinbase <- 1 + timestamp <- 1 + nonce <- 1 + hash <- 1 diff --git a/tests/invariants/fail/non-inductive.act b/tests/invariants/fail/non-inductive.act index b71d5aa7..3d741059 100644 --- a/tests/invariants/fail/non-inductive.act +++ b/tests/invariants/fail/non-inductive.act @@ -24,7 +24,7 @@ case x == 0: storage - x => 1 + x <- 1 behaviour g of C interface g() @@ -33,7 +33,7 @@ case x == 1: storage - x => 2 + x <- 2 behaviour j of C interface j() @@ -42,4 +42,4 @@ case x == 7: storage - x => 100 + x <- 100 diff --git a/tests/invariants/pass/amm.act b/tests/invariants/pass/amm.act index 65438074..063fdf38 100644 --- a/tests/invariants/pass/amm.act +++ b/tests/invariants/pass/amm.act @@ -19,8 +19,8 @@ iff in range uint256 storage - reserve0 => reserve0 + amt - reserve1 => (reserve0 * reserve1) / (reserve0 + amt) + 1 + reserve0 <- reserve0 + amt + reserve1 <- (reserve0 * reserve1) / (reserve0 + amt) + 1 behaviour swap1 of Amm interface swap1(uint256 amt) @@ -31,5 +31,5 @@ iff in range uint256 storage - reserve0 => (reserve0 * reserve1) / (reserve1 + amt) + 1 - reserve1 => reserve1 + amt + reserve0 <- (reserve0 * reserve1) / (reserve1 + amt) + 1 + reserve1 <- reserve1 + amt diff --git a/tests/invariants/pass/case.act b/tests/invariants/pass/case.act index 3aa99e07..889b6695 100644 --- a/tests/invariants/pass/case.act +++ b/tests/invariants/pass/case.act @@ -16,9 +16,9 @@ iff case z == 0: storage - x => z + x <- z case 0 < z: storage - x => 0 \ No newline at end of file + x <- 0 \ No newline at end of file diff --git a/tests/invariants/pass/homogeneous.act b/tests/invariants/pass/homogeneous.act index 19ccf68a..271f929f 100644 --- a/tests/invariants/pass/homogeneous.act +++ b/tests/invariants/pass/homogeneous.act @@ -18,8 +18,8 @@ iff z * scalar > z storage - x => x * scalar - z => z * scalar + x <- x * scalar + z <- z * scalar behaviour g of Homogeneous @@ -30,5 +30,5 @@ iff z * scalar > z storage - y => y * scalar - z => z * scalar + y <- y * scalar + z <- z * scalar diff --git a/tests/invariants/pass/ite.act b/tests/invariants/pass/ite.act index 8d206651..d048def4 100644 --- a/tests/invariants/pass/ite.act +++ b/tests/invariants/pass/ite.act @@ -16,18 +16,16 @@ case z < 10: storage - x => if z == 5 then 4 else 1 + x <- if z == 5 then 4 else 1 case 10 <= z and z < 100: storage - x => if z == 50 then 3 else 2 - - + x <- if z == 50 then 3 else 2 case z >= 100: storage - x => if z == 50 then 3 else 2 + x <- if z == 50 then 3 else 2 diff --git a/tests/invariants/pass/log.act b/tests/invariants/pass/log.act index 7cda0ba7..bb80d22a 100644 --- a/tests/invariants/pass/log.act +++ b/tests/invariants/pass/log.act @@ -18,5 +18,5 @@ iff n > 1 storage - n => n / 2 - count => count + 1 + n <- n / 2 + count <- count + 1 diff --git a/tests/invariants/pass/mutex.act b/tests/invariants/pass/mutex.act index d66bb215..87666cd8 100644 --- a/tests/invariants/pass/mutex.act +++ b/tests/invariants/pass/mutex.act @@ -17,4 +17,4 @@ iff not lock storage - x => _x + x <- _x diff --git a/tests/invariants/pass/state_machine.act b/tests/invariants/pass/state_machine.act index 8531ae7a..c4267be9 100644 --- a/tests/invariants/pass/state_machine.act +++ b/tests/invariants/pass/state_machine.act @@ -14,18 +14,18 @@ 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 diff --git a/tests/postconditions/fail/bad_assignment.act b/tests/postconditions/fail/bad_assignment.act index fbbadb80..f477cfd1 100644 --- a/tests/postconditions/fail/bad_assignment.act +++ b/tests/postconditions/fail/bad_assignment.act @@ -10,7 +10,7 @@ interface f() storage - x => 2 + x <- 2 ensures diff --git a/tests/postconditions/fail/bad_assignment_prestate.act b/tests/postconditions/fail/bad_assignment_prestate.act index 22684c29..1eea6847 100644 --- a/tests/postconditions/fail/bad_assignment_prestate.act +++ b/tests/postconditions/fail/bad_assignment_prestate.act @@ -10,7 +10,7 @@ interface f(uint24 y) storage - x => x + y + x <- x + y ensures diff --git a/tests/postconditions/pass/amm.act b/tests/postconditions/pass/amm.act index 1af234c7..34c8e568 100644 --- a/tests/postconditions/pass/amm.act +++ b/tests/postconditions/pass/amm.act @@ -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 @@ -70,11 +70,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 @@ -106,11 +106,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 diff --git a/tests/postconditions/pass/assignment.act b/tests/postconditions/pass/assignment.act index d0c9c098..141f827f 100644 --- a/tests/postconditions/pass/assignment.act +++ b/tests/postconditions/pass/assignment.act @@ -10,7 +10,7 @@ interface f() storage - x => 2 + x <- 2 ensures diff --git a/tests/postconditions/pass/assignment_poststate.act b/tests/postconditions/pass/assignment_poststate.act index eb5029d0..1323f583 100644 --- a/tests/postconditions/pass/assignment_poststate.act +++ b/tests/postconditions/pass/assignment_poststate.act @@ -11,4 +11,7 @@ interface f() storage x <- post(x) -returns post(x) \ No newline at end of file +ensures + x == post(x) + +returns post(x) \ No newline at end of file diff --git a/tests/postconditions/pass/assignment_prestate.act b/tests/postconditions/pass/assignment_prestate.act index 15837d0a..47f54e75 100644 --- a/tests/postconditions/pass/assignment_prestate.act +++ b/tests/postconditions/pass/assignment_prestate.act @@ -11,4 +11,7 @@ interface f() storage x <- pre(x) +ensures + x == pre(x) + returns pre(x) diff --git a/tests/postconditions/pass/assignment_return.act b/tests/postconditions/pass/assignment_return.act index ef79501c..a37148c2 100644 --- a/tests/postconditions/pass/assignment_return.act +++ b/tests/postconditions/pass/assignment_return.act @@ -10,7 +10,7 @@ interface f() storage - x => 2 + x <- 2 returns From 037d6def3716750f017876a1e583792b8dc67c91 Mon Sep 17 00:00:00 2001 From: Scott Rose Date: Tue, 27 May 2025 13:27:13 -0500 Subject: [PATCH 4/4] Refactor storage operations to consistently use LARROW syntax in various test files --- src/Act/Lex.x | 1 - tests/coq/exponent/exponent.act | 4 ++-- tests/frontend/fail/cycle.act | 6 +++--- tests/frontend/fail/cycle2.act | 2 +- tests/frontend/fail/missingdef0.act | 2 +- tests/frontend/fail/missingdef2.act | 2 +- tests/frontend/fail/typecheck/silly_types.act | 6 +++--- tests/hevm/fail/multi/multi.act | 2 +- tests/hevm/fail/shape-2/shape-2.act | 2 +- tests/hevm/fail/shape/shape.act | 4 ++-- tests/hevm/fail/simple/simple.act | 2 +- tests/hevm/pass/layout1/layout1.act | 4 ++-- tests/hevm/pass/layout2/layout2.act | 12 ++++++------ tests/hevm/pass/layout3/layout3.act | 2 +- 14 files changed, 25 insertions(+), 26 deletions(-) diff --git a/src/Act/Lex.x b/src/Act/Lex.x index d4f0c5f7..08fefabb 100644 --- a/src/Act/Lex.x +++ b/src/Act/Lex.x @@ -140,7 +140,6 @@ data LEX = | INRANGE | IFF | POINTERS - | POINTSTO | AND | NOT | OR diff --git a/tests/coq/exponent/exponent.act b/tests/coq/exponent/exponent.act index bbf976ba..952c33fe 100644 --- a/tests/coq/exponent/exponent.act +++ b/tests/coq/exponent/exponent.act @@ -26,5 +26,5 @@ iff in range uint storage - r => r * b - e => e - 1 \ No newline at end of file + r <- r * b + e <- e - 1 \ No newline at end of file diff --git a/tests/frontend/fail/cycle.act b/tests/frontend/fail/cycle.act index ffb74ae3..eb7b0a87 100644 --- a/tests/frontend/fail/cycle.act +++ b/tests/frontend/fail/cycle.act @@ -19,7 +19,7 @@ iff CALLVALUE == 0 storage - a.x => z + a.x <- z behaviour multi of B interface set_remote2(uint z) @@ -28,5 +28,5 @@ iff CALLVALUE == 0 storage - y => 1 - a.x => z + y <- 1 + a.x <- z diff --git a/tests/frontend/fail/cycle2.act b/tests/frontend/fail/cycle2.act index 72b970d4..e01aa883 100644 --- a/tests/frontend/fail/cycle2.act +++ b/tests/frontend/fail/cycle2.act @@ -28,7 +28,7 @@ iff CALLVALUE == 0 storage - d.x => z + d.x <- z constructor of C interface constructor(uint u) diff --git a/tests/frontend/fail/missingdef0.act b/tests/frontend/fail/missingdef0.act index 70cf3d6c..6bd3064c 100644 --- a/tests/frontend/fail/missingdef0.act +++ b/tests/frontend/fail/missingdef0.act @@ -12,4 +12,4 @@ interface f() storage - x => y + x <- y diff --git a/tests/frontend/fail/missingdef2.act b/tests/frontend/fail/missingdef2.act index de6343e1..ed785f08 100644 --- a/tests/frontend/fail/missingdef2.act +++ b/tests/frontend/fail/missingdef2.act @@ -20,4 +20,4 @@ interface f() storage C - x => y + x <- y diff --git a/tests/frontend/fail/typecheck/silly_types.act b/tests/frontend/fail/typecheck/silly_types.act index da278961..23e3a7e9 100644 --- a/tests/frontend/fail/typecheck/silly_types.act +++ b/tests/frontend/fail/typecheck/silly_types.act @@ -18,7 +18,7 @@ iff in range uint256 storage // TODO: remove this hack once bug #81 is fixed... - x => x - y => (x + p) == (q > y) - p => (x + p) and (q > y) + x <- x + y <- (x + p) == (q > y) + p <- (x + p) and (q > y) q diff --git a/tests/hevm/fail/multi/multi.act b/tests/hevm/fail/multi/multi.act index c442e8cd..66ad205a 100644 --- a/tests/hevm/fail/multi/multi.act +++ b/tests/hevm/fail/multi/multi.act @@ -15,7 +15,7 @@ iff CALLVALUE == 0 storage - x => z + x <- z constructor of B diff --git a/tests/hevm/fail/shape-2/shape-2.act b/tests/hevm/fail/shape-2/shape-2.act index d4cd687d..0878bd69 100644 --- a/tests/hevm/fail/shape-2/shape-2.act +++ b/tests/hevm/fail/shape-2/shape-2.act @@ -36,4 +36,4 @@ iff CALLVALUE == 0 storage - a1 => a2 \ No newline at end of file + a1 <- a2 \ No newline at end of file diff --git a/tests/hevm/fail/shape/shape.act b/tests/hevm/fail/shape/shape.act index ee024fd3..2a4c02e8 100644 --- a/tests/hevm/fail/shape/shape.act +++ b/tests/hevm/fail/shape/shape.act @@ -25,7 +25,7 @@ iff CALLVALUE == 0 storage - x => z + x <- z // contract B constructor of B @@ -77,4 +77,4 @@ iff CALLVALUE == 0 storage - a => create A(42) \ No newline at end of file + a <- create A(42) \ No newline at end of file diff --git a/tests/hevm/fail/simple/simple.act b/tests/hevm/fail/simple/simple.act index 21d4d18e..a0cbc073 100644 --- a/tests/hevm/fail/simple/simple.act +++ b/tests/hevm/fail/simple/simple.act @@ -18,7 +18,7 @@ iff storage - x[0] => 1 + x[0] <- 1 returns diff --git a/tests/hevm/pass/layout1/layout1.act b/tests/hevm/pass/layout1/layout1.act index aed166a1..41a54ce4 100644 --- a/tests/hevm/pass/layout1/layout1.act +++ b/tests/hevm/pass/layout1/layout1.act @@ -19,7 +19,7 @@ iff storage - x => y - y => x + x <- y + y <- x returns 1 \ No newline at end of file diff --git a/tests/hevm/pass/layout2/layout2.act b/tests/hevm/pass/layout2/layout2.act index 59a8fcfc..e4849ee3 100644 --- a/tests/hevm/pass/layout2/layout2.act +++ b/tests/hevm/pass/layout2/layout2.act @@ -23,10 +23,10 @@ iff storage - x => y - y => x - z => 11 - flag => not flag + x <- y + y <- x + z <- 11 + flag <- not flag returns 1 @@ -39,7 +39,7 @@ iff storage - flag => b + flag <- b behaviour get_flag of A @@ -64,7 +64,7 @@ iff case flag: storage - y => v + y <- v returns 1 diff --git a/tests/hevm/pass/layout3/layout3.act b/tests/hevm/pass/layout3/layout3.act index af26f4a3..79a8cc91 100644 --- a/tests/hevm/pass/layout3/layout3.act +++ b/tests/hevm/pass/layout3/layout3.act @@ -37,6 +37,6 @@ iff storage - f[key] => value + f[key] <- value returns 1 \ No newline at end of file