Skip to main content

Overview

The Songlark toolchain performs three main functions:

  • the Lark source language lets you write programs;
  • the model checker lets you prove that your program is safe; and
  • the code generation lets you execute them on real hardware.

All of these parts are written in Scala. The source language is implemented as an embedded domain-specific-language (EDSL) which is basically equivalent to writing a Scala program that generates a program. It's not as bad as it sounds.

For the old guard​

If you've used any of the open-source tooling around Lustre before, you're probably aware of the limitations of the alternative tools. The existing tools are good at what they do, but sometimes that's not aligned with what we need. Songlark is all of the bits of Lustre you know and love, in a new and expressive form.

Most of the improvements can be characterised into three main categories: expressivity, predictability, and soundness.

Expressive: more interesting programs​

Most of the extra expressivity comes from being an embedded language inside a general-purpose language. This means that we can have a fairly small core language and still write interesting programs.

  • Polymorphism, or generics, let you reuse functions across multiple types. You can write a generic sample-and-hold function that works for any type or a PID controller that works for any numeric type.
  • You can compute look-up tables in pure Scala code and use them from your embedded code.
  • Automata support has some optimisations to reduce proof state, so you can write bigger programs.

Predictable: what's true today is true tomorrow​

  • Deterministic proof replay uses a different invariant generation technique that is less susceptible to small, semantically-irrelevant program changes. The idea is that the proof process is more predictable so small changes or re-runs in CI won't break proofs.
  • Additionally, generated invariants can be saved to a separate file, so that each proof attempt doesn't need to search for the same invariants (and maybe not find it).

Sound: what you prove is what you run​

  • Bounded integers: signed and unsigned integers of different sizes. All intermediate operations are checked for overflow.
  • Safe, well-defined division matches the SMT semantics.
  • The compiler and model checker are designed together and work on the same program representation. They're also extensively tested against each other. It's more likely that they agree.
  • Grind mode checks that the proofs and compilation are right for your program specifically: it uses the SMT solver to generate test cases and checks that the C code agrees. Later we'll extend this to prove that at least part of the compilation is correct.