Smart Contracts to go live next week!
All hands are on deck in the core tech and Scilla teams, as we gear up for the activation of smart contracts on 10 June. We are very excited for this day, which delivers on the promise we made two years ago. As we go into the following week, you will hear more from us on why this is significant. Stay tuned!
For further information, connect with us on one of our social channels:
Meanwhile, we take you through the key core tech and scilla updates.
Readers of our earlier blog posts may recall that Zilliqa Research bootstrapped and hosts a fraction of the mainnet by deploying AWS-powered instances through Kubernetes. This week we are taking a break from the usual format of detailing the latest updates to the core C++ Zilliqa code base to highlight some of the more recent developments to our mainnet infrastructure.
Lookup API availability improvement. With the community’s help, we identified an issue where a faulty lookup node was not de-registered from our load-balancer in a timely manner, causing some service degradation on the API endpoint. An enhanced monitoring mechanism has since been put into action to alleviate such issues.
Metadata persistence enhancement. We discovered one potential issue in our service discovery system which may cause metadata loss that requires human intervention. Although this has not led to any substantial problem thus far, we were able to quickly fix the issue by upgrading the persistent storage.
Infrastructure isolation reinforcement. The isolation of several critical systems in our infrastructure has been reinforced at multiple layers, from the underlying cloud services to application deployment. This creates fault domains to protect high-priority workload if certain vulnerabilities are discovered in our infrastructure.
Formal verification: Overflows and underflows in integer arithmetic within smart contracts has always been a real concern. The community has witnessed several incidents in the recent past, the most notable one being the batchOverflow attack, where attackers were able to create overflows at runtime leading to unexpectedly large transfer of funds to the attacker’s wallet.
The standard integer library in Scilla implements overflows and underflows checks and throws error at runtime when required. And hence, developers do not have to rely on any external safe math like library. We recently decided to go a step further and formalize safe integer arithmetic and prove correctness of the Scilla integer functions in Coq.
To this end, we need to have library support for bit arithmetics in Coq, including definitions of bitwise operations and proofs of their properties. The usual representations are tailored to ease proving rather than provide computational efficiency. The
coq-bits library provides us with the tools to switch between representations for efficient symbolic manipulation and efficient calculation. In addition, the library’s designers have carefully approached extraction, which means we can utilize it to get OCaml code from the ongoing formalization.
Procedures: We have finished implementing procedures in Scilla in time for the release of smart contracts on the Zilliqa mainnet.
The primary use of procedures is the sharing of code that accesses the contract’s state. This will be particularly helpful if different parts of the state (e.g., different maps) need to be kept synchronised, as a common procedure will be able to update the maps consistently. Another use case is the standardisation of error messaging.
Procedures come with a few limitations:
- Recursive or mutually recursive procedures are not allowed, as they can potentially cause non-termination. In the future we plan to extend Scilla with a
foreachconstruct to allow the application of a procedure to each element of a list
- A procedure cannot accept a map as a parameter, nor a parameter whose type contains a type variable. Maps are disallowed for efficiency reasons, because the entire map would need to be copied if passed to a procedure
- Procedures do not return values. Procedures are intended to be run because for their side-effects, so if a value needs to be computed, one should use a library function instead (if the contract state needs to be updated before the value can be computed, use a procedure to update the state, then call a library function to compute the value)