Library import mechanism in Scilla
Scilla supports deploying both libraries and contract, and each library or contract can import already deployed libraries. This article describes how Scilla loads libraries and what inputs it expects to facilitate this. The mechanism described here applies to both scilla-runner and scilla-checker.
When Scilla encounters an import Foo construct (in either a library or a contract), it needs to find and load the library Foo. There are two mechanisms that it uses for this, one to facilitate ease of local development and the other one for the blockchain to fetch and provide libraries to Scilla.
When an init.json is provided (to either the runner or the checker) and the init.json contains an entry as shown below:
{
"vname" : "_extlibs",
"type" : "List(Pair String ByStr20)",
"value" : [
{
"constructor" : "Pair",
"argtypes" : ["String", "ByStr20"],
"arguments" : ["Foo", "0x986556789012345678901234567890123456abcd"]
},
...
]
}In this scenario, the library loader looks for 0x986556789012345678901234567890123456abcd.scillib in it's -libdir path and loads that as library Foo. In the case of Foo itself importing more libraries, it also looks for 0x986556789012345678901234567890123456abcd.json (in the same place), treating it as the init JSON for Foo and continues the loading process with the same mechanism.
To facilitate local development and to "simply" enable loading of standard libraries, when Scilla is not provided with an init JSON argument (Note: the argument is mandatory for the runner, but not checker) OR the init JSON provided does not contain a relevant _extlibs entry, then the library loading mechanism looks for Foo.scillib and loads it. Continuing the process for transitively loading imports, if Foo.json exists and it contains _extlibs entries for libraries imported inside Foo, the information is used for continuing the process.