Testing smart contracts with QuickCheck
Please log in to watch this conference skillscast.
I will talk about some recent work on a random testing framework for smart contracts on the Cardano blockchain--which supports the world's largest "proof of stake" cryptocurrency. In contrast to the Ethereum blockchain, Cardano contracts are written in Haskell, but of course, they still need to be tested. I'll talk about the testing framework we've built, and its most novel aspect: not only must we test that nothing bad ever happens, but also that something good is always possible.
Q&A
Question: Something I’ve always wanted for this sort of testing is, while going through this process of finding the correct test, all the failing tests should automatically ask you: Is this something you expected to fail? If so, I’ll add a unit test to make sure it continues to break
Answer: Yes, saving failed tests can be useful. I generally don't bother if they were quick to find, but shrunk tests that were costly to find can be worth saving. They do tend to bit rot though. Ah, yes, and I do quite often write properties that say "this should fail". That is a useful test of the generation, it says "my testing is good enough to find this error".
Question: is this extension to quickcheck released on hackage?
Answer: This code is in the IOHK plutus repo. It's customized for Plutus so would need some modification to go on Hackage.
Question: Do you have any suggestions for helping others build up the skills in determining what properties are useful? They can often seem like a difficult topic for some to wrap their heads around, particularly if they are coming from a heavy unit test background with e.g. Ruby.
Answer: Yes. I published a paper last year called "How to specify it!" which is on exactly this topic... how to come up with properties in the first place. In the paper I talk about pure functions, which are the easier case, but on the other hand that's how come I can discuss 4-5 different approaches in one paper. (Trends in Functional Programming 2019 (which came out in 2020). Also, in the Chalmers research repo. https://research.chalmers.se/en/publication/517894
The ideas apply to code with state also. Then one useful way to evaluate a property is to make it fail. Plant a number of reasonable bugs and make sure they get caught.
Jon Carstens - G'Day, Nerves!
I show several links in my talk. Here they are in order so you don't have to manually search
* https://hexdocs.pm/nerves/getting-started.html * https://github.com/jjcarstens/replex * https://github.com/F5OEO/rpitx * Erlang! The movie - https://www.youtube.com/watch?v=BXmOlCy0oBM * https://erlang.org/doc/man/heart.html * https://github.com/nerves-project/nervesheart * https://embedded-elixir.com/post/2018-12-10-heart/ * Nerves of Steel - https://www.youtube.com/watch?v=tuY2IxAfe-I * https://github.com/nerves-project/nervesexamples * https://elixir-circuits.github.io * https://github.com/elixir-circuits/circuitsquickstart * https://github.com/fhunleth/nerveslivebook * https://github.com/drizzle-org/drizzle * https://github.com/nerves-keyboard * https://farm.bot * https://smartrent.com * #nerves channel in Elixir slack - https://elixir-lang.slack.com/archives/C0AB4A879 * Nerves Forum - https://elixirforum.com/c/nerves-forum/74 * https://nerves.group * https://github.com/nerves-project
Question: Would Nerves suit hard realtime systems?
Answer: Well, this might be a loaded question of personal preference. I think you could definitely start with it and get very far, but it depends on how strictly you need “hard” real time as Nerves is prob closer to being soft real time.
Question: I think Erlang itself is meant for soft realtime systems
Answer: Yes. The GRiSP project is another embedded erlang setup targeted for “bare-metal erlang” and hard real-time event handling which might be worth a look as well:
The difference being GRiSP is custom designed hardware and erlang VM vs Nerves which relies on Linux kernel + buildroot. But at the end of the day, Erlang is more for the soft real time
O! And, what we do for this requirement is typically do hard real time on a microcontroller that interfaces with Nerves, and then Nerves does the control and command in Elixir
Question: I'm a realtime systems noob. What's "hard" realtime? Very small slice guarantee? Very low probability of missing a slice?
Answer: It's all about guarantees down to the processor deadlines. It basically means you cannot miss any computational deadline when chomping the bits which gets problematic on processor load, because timings may fail where “soft real time” can handle those missed deadlines with reschedules and eventually hit the mark. But we’re talking like imperceptible deadlines that only become noticeably missed accrued over time.
Question: Has there been any work with Nerves and network booting?
Answer: I think you might need to elaborate your question for me? Just to boot an image remotely on the network? Or maybe..whats your direct goal here?
Question: Right to boot an image from the network instead of using an sd card. I was thinking for the ability to have more than 1 fallback and less upstream internet usage if a firmware can be downloaded once and then shared on a local network.
Answer: There is not work I know of for network booting. for rpi, there has been work to utilize initramfs and some other intermediate files, but thats an interesting idea to be able to netboot. Though the main use-case I can think of would be to obtain the first firmware, such as provisioning new hardware.
I’m going to have to look at this more. There is also the option to use Erlang to connect local devices in distribution and pass the new firmware there instead
We have a lot of devices on cellular and reducing network traffic is a huge deal. The route we’ve been going is for delta-updates and only sending the change bits of the firmware to the device. Thats currently supported be default in the official systems and https://nerves-hub.org supports delivering those firmware updates.
Question: I'm going to have to get into this. I'm also a qualified security technician (alarms/ CCTV/ access control/ home automation). Are there implementations on commercial grade hardware?
Answer: What you’d prob want to look at are what “systems” have been ported so far. We develop a lot of in house hardware for this using Octavo and iMX6uLL chipsets which I see used a lot more https://hex.pm/packages?search=nervessystem&sort=recentdownloads
And there are other places using it commercially, like https://farm.bot . I believe there is also a startup to use it with grid system monitoring
Basically, you would see what processor the target hardware is using, see if
there is a nervessystem* port for it, or port yourself
O! And we also use it with access control systems with the iMX6uLL chip, but has been a pretty custom setup
YOU MAY ALSO LIKE:
Thank you to our sponsors and partners
Platinum
Silver
Bronze
Testing smart contracts with QuickCheck
John Hughes
Creator
QuickCheck