Skip to content

Commit b31f51b

Browse files
yzhang90ehildenb
authored andcommitted
rename G => GAAS in one of the lemmas. (#433)
1 parent 615db59 commit b31f51b

File tree

3 files changed

+9
-9
lines changed

3 files changed

+9
-9
lines changed

tests/specs/ds-token-erc20/abstract-semantics-segmented-gas.k

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,10 +15,10 @@ module ABSTRACT-SEMANTICS-SEGMENTED-GAS
1515
// ########################
1616

1717
// accumulate the gas cost and never run out of gas
18-
rule <k> G ~> #deductGas => . ... </k>
19-
<gas> #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM +Int G, MEM) </gas>
18+
rule <k> GAAS:Int ~> #deductGas => . ... </k>
19+
<gas> #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM +Int GAAS, MEM) </gas>
2020
<callGas> _ => #gas(INITGAS, NONMEM, MEM) </callGas>
21-
requires #notKLabel(G, "#symCmem")
21+
requires #notKLabel(GAAS, "#symCmem")
2222
[trusted, matching(#gas)]
2323

2424
rule <k> #symCmem(MEM') ~> #deductGas => . ... </k>

tests/specs/hkg-erc20/abstract-semantics-segmented-gas.k

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,10 +15,10 @@ module ABSTRACT-SEMANTICS-SEGMENTED-GAS
1515
// ########################
1616

1717
// accumulate the gas cost and never run out of gas
18-
rule <k> G ~> #deductGas => . ... </k>
19-
<gas> #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM +Int G, MEM) </gas>
18+
rule <k> GAAS:Int ~> #deductGas => . ... </k>
19+
<gas> #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM +Int GAAS, MEM) </gas>
2020
<callGas> _ => #gas(INITGAS, NONMEM, MEM) </callGas>
21-
requires #notKLabel(G, "#symCmem")
21+
requires #notKLabel(GAAS, "#symCmem")
2222
[trusted, matching(#gas)]
2323

2424
rule <k> #symCmem(MEM') ~> #deductGas => . ... </k>

tests/specs/hobby-erc20/abstract-semantics-segmented-gas.k

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,10 +15,10 @@ module ABSTRACT-SEMANTICS-SEGMENTED-GAS
1515
// ########################
1616

1717
// accumulate the gas cost and never run out of gas
18-
rule <k> G ~> #deductGas => . ... </k>
19-
<gas> #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM +Int G, MEM) </gas>
18+
rule <k> GAAS:Int ~> #deductGas => . ... </k>
19+
<gas> #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM +Int GAAS, MEM) </gas>
2020
<callGas> _ => #gas(INITGAS, NONMEM, MEM) </callGas>
21-
requires #notKLabel(G, "#symCmem")
21+
requires #notKLabel(GAAS, "#symCmem")
2222
[trusted, matching(#gas)]
2323

2424
rule <k> #symCmem(MEM') ~> #deductGas => . ... </k>

0 commit comments

Comments
 (0)