The basics of Faust, Formally!

We have already seen quite a bit about Faust, can we build a formal model in Coq? The answer of course, is yes.

Representing Faust Programs inside Coq

The standard technique to start with program representation is to capture Faust's syntax as a datatype.

Coq's datatypes are so-called inductively-defined datatypes, meaning that an element of a type is usually built out of several cases; we use a simplified version of Faust for educational purposes:

Making sense Faust programs!

We have built a representation of Faust programs, but now we'll like to capture formally their effect on sound too.

Thus, we will build an interpretation function, which basically will take a Faust program and return a Coq's function from signals to singal:

$$ ⟦ f : i ↝ o ⟧ : S^i \to S^o $$

Now the question is what should our signal type $S$, be? We have assumed the basic data type of sampled to be some algebraic field, given that Faust operates at a 1-sample rate, it is convenient to encode signals as list of length $n$, where $n$ is the output produced at the $n^{th}$ step:

Then, the interpreation function only has to run every particular singal processor for $n$ steps:

A sample logic for Faust programs

We can check that the semantics meet the expected properties. And indeed, we can even use more general theorems to check properites about Faust. A common technique in formal verification is to use a program logic, which is then used to reason about programs. Our sample-level logic for Faust looks as follows:

Soundess and interpretation of a judgment

We need to prove our logic sound, then we can profit from it!

Checking stability of our simple smooth filter.

We can use this technique to prove out little filter stable, that is:

$$ \forall x~c, x \in [-1,1] \to c \in [0,1] \to ⟦ \mathit{smooth(c)} ⟧(x) \in [-1,1] $$

which unfolding the signal representation amounts to:

$$ \forall x~c~n, x(n) \in [-1,1] \to c \in [0,1] \to ⟦ \mathit{smooth(c)} ⟧(x)(n) \in [-1,1] $$

The proof is straightforward using the logic, using some interval aritmetic in Coq.