KEVM & eDSL Usage
examples
definition
code: definition
syntax TypedArg ::=
#bytes ( Int , Int ) | #array ( TypedArg , Int , TypedArgs ) examples
requires:
requires:
requires:
definition
code: definition
syntax Bool ::= "#range" "(" Int "<" Int "<" Int ")"
| "#range" "(" Int "<" Int "<=" Int ")"
| "#range" "(" Int "<=" Int "<" Int ")"
| "#range" "(" Int "<=" Int "<=" Int ")"
examples
code: 0 parameter
(.TypedArgs refers to an empty list )
code: 1 parameter
definition
code: definition
examples
code: example int
...
requires:
andBool 0 <=Int TOTAL andBool TOTAL <Int (2 ^Int 256)
code: example mapping
...
requires:
andBool 0 <=Int OWNER andBool OWNER <Int (2 ^Int 160)
andBool 0 <=Int BAL andBool BAL <Int (2 ^Int 256)
definition
code: definition
code: template
<output> {OUTPUT} </output>
となっているとき
1つの値を返す
code: example
複数の値を返す
code: example
output: _ => intList2ByteStack(CHILD_ROOT CHILD_TIME_STAMP)
difinition
code: definition
syntax WordStack ::= intList2ByteStack( IntList ) function // ------------------------------------------------------------
rule intList2ByteStack(.IntList) => .WordStack
requires 0 <=Int V andBool V <Int pow256
endmodule
(outputはWordStackになる)
examples
code: example
definition
code: definition
syntax EventArg ::= TypedArg
code: example
compiler: "Solidity"
_balances: 0
code: "0x60606040526004361061008e576000357c0100000000000..."
gasCap: 100000
compiler -> {COMPILER}
_balances -> {_BALANCES}
code: example
<network>
...
<activeAccounts> SetItem(ACCT1_ID) SetItem(ACCT2_ID) _:Set </activeAccounts>
<accounts>
<account>
<acctID> ACCT1_ID </acctID>
<balance> ACCT1_BAL </balance>
<storage> _ </storage>
<origStorage> _ </origStorage>
<nonce> ACCT1_NONCE </nonce>
</account>
<account>
<acctID> ACCT2_ID </acctID>
<balance> ACCT2_BAL </balance>
<storage> _ </storage>
<origStorage> _ </origStorage>
<nonce> ACCT2_NONCE </nonce>
</account>
...
</network>
※ activeAccounts などはテンプレート可したほうが便利
code: definition?
<network>
<activeAccounts> .Set </activeAccounts>
<accounts>
<account multiplicity="*" type="Map">
<acctID> 0 </acctID>
<balance> 0 </balance>
<code> .WordStack:AccountCode </code>
<storage> .Map </storage>
<origStorage> .Map </origStorage>
<nonce> 0 </nonce>
</account>
</accounts>
</network>
構造体のストレージ変数 nrryuya.icon
フィールドが上から順に本来のスロット位置から+0, +1, +2とされていく
code: k
syntax Int ::= "#Vat.ilks" "Int ".rate" function // ----------------------------------------------------
yudetamago.icon > +INT 1 じゃなくて 1 +Word にしないといけないのってどういう場合でしたっけ?
nrryuya.icon > 追記: Solidityのコンパイラの仕様的に、下記のように書かないとダメっぽい(klabは上のでうまくっているのが不思議)
code: k
定数やピュアな関数を使いまわしたい場合 nrryuya.icon
マクロをかく
code: k
syntax Int ::= "#expectedBlockNumber" "(" Int "," Int ")" function // ---------------------------------------------------------------------
オーバーフローとSafeMathに関する雑感 nrryuya.icon
SafeMath的にオーバー(アンダー)フローを扱っている場合、successのspecificationは、当然ながら「SafeMathを使っているプログラムのどの箇所でも、大き(小さ)すぎる場合はrevertする」という仕様も含む
よって、プログラム中の全てのSafeMath系の演算に関して、#range系のrequireが必要
これをサボると、SafeMath使い忘れた演算の時に気づけない
また、SafeMath系ではない演算に関しても、暗黙的に「流石にここまで大きくはならないだろう」と言う前提があり、オーバー・アンダーフローすると本来のspecが満たされないことが多いので、これも制約が必要
bool型とWordStack
bool型の返り値の関数を検証するためにこのようなDSLを加えた
rule bool2ByteStack(X, 32) => 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : 0 : X : .WordStack
最後の : .WordStackを抜かすと、以下のエラーがでる
code: sh
Error Compiler: Had 1 parsing errors. Error Critical: Could not infer a sort for variable 'X' to match every location.
Source(/Users/ryuya.nakamura/work/LayerXcom/verified-vyper-contracts/.build/evm-semantics/.build/java/edsl.k)
Location(320,10,320,181)
疑問・メモ
※あとで整理する(yudetamago.icon)
返り値がない関数のspec、なんでこうしているんだろう。。。明示的に空だと主張した方がいいのでは
code: K
<output> _ => _ </output>
こういう()はあってもなくてもいいっぽい
code: K
andBool #rangeUInt(256, (CURRENTCHILDBLOCK -Int 1000 +Int CURRENTDEPOSITBLOCK)) storageのMapのlook up先はシンボルじゃないといけないっぽい
これを
code: k
こうしたら、K and AccountCell are not compatibleがでた
nrryuya.icon > これあとでカテゴリ別に整理したいですね