Skip to content

Commit 11c1a15

Browse files
robdockinsrobdockins
committed
Add an actual README that explains what copilot-verifier is,
and how the proof techinque works at a medium level of detail.
1 parent a845c2f commit 11c1a15

1 file changed

Lines changed: 228 additions & 1 deletion

File tree

‎README.md‎

Lines changed: 228 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1,228 @@
1-
TODO
1+
# Copilot Verifier
2+
3+
This "Copilot Verifier" is an add-on to the
4+
[Copilot Stream DSL](https://copilot-language.github.io)
5+
for verifying the correctness of C code generated
6+
by the `copilot-c99` package.
7+
8+
The main idea of the verifier is to use the
9+
[Crucible symbolic simulator](https://github.com/galoisinc/crucible)
10+
to interpret the semantics of the generated C program and
11+
and to produce verification conditions sufficient to guarantee
12+
that the meaning of the generated program corresponds in a precise
13+
way to the meaning of the original stream specification. The generated
14+
verification conditions are then dispatched to SMT solvers to
15+
be automatically solved. We will have more to say about exactly
16+
what is meant by this correspondence below.
17+
18+
## Using the Copilot Verifier
19+
20+
The main interface to the verifier is the `Copilot.Verifier.verify`
21+
function, which takes some options to drive the code generation
22+
process and a Copilot `Spec` object. It will invoke the Copilot
23+
code generator to obtain C sources, compile the C sources into
24+
LLVM bitcode using the `clang` compiler front-end, then
25+
parse and interpret the bitcode using `crucible`. After generating
26+
verification conditions, it will dispatch them to an SMT solver,
27+
and the result of those queries will be presented to the user.
28+
29+
There are a number of examples (based on similar examples
30+
from the main Copilot repository) demonstrating how to
31+
incorporate the verifier into a Copilot program.
32+
See the `copilot-verifier/examples` subdirectory of this repository.
33+
34+
## Details of the Verification
35+
36+
### Synopsis of Copilot semantics
37+
38+
The Copilot DSL represents a certain nicely-behaved
39+
class of discrete-time stream programs. Each `Stream`
40+
in Copilot denotes an infinite stream of values; one may
41+
just as well think that `Stream a` represents a pure mathematical
42+
function `ℕ → a` from natural numbers to values of type `a`.
43+
See the
44+
[Copilot manual]
45+
(https://ntrs.nasa.gov/api/citations/20200003164/downloads/20200003164.pdf)
46+
for more details of the Copilot language itself and its semantics.
47+
48+
One of the central design considerations for Copilot is that is should
49+
be possible to implement stream programs using a fixed, finite amount
50+
of storage. As a result, Copilot will only accept stream programs
51+
that access a bounded amount of their input streams (including any
52+
recursive stream references). This allows an
53+
implementation strategy where the generated C code can use fixed-size
54+
ring buffers to store a limited number of previous stream values.
55+
56+
The execution model for the generated programs is that the program
57+
starts in a state corresponding to stream values at time `t = 0`;
58+
"external" stream input values are placed in distinguished global
59+
variables by the calling environment, which then executes a `step()`
60+
function to move to the next time step. The `step()` function captures
61+
the values of these external inputs and does whatever computation is
62+
necessary to update its internal state from time `t=n` to time
63+
`t=n+1`. In addition, it will call any defined "trigger" functions
64+
if the stream state at that time step satisfies the defined guard condition.
65+
In short, the generated C program steps one moment at a time through
66+
the stream program, consuming a sequence of input values provided by
67+
a cooperating environment and calling handler functions whenever
68+
states of interest occur.
69+
70+
### The Desired Correspondence
71+
72+
What does it mean, then, for a generated C program in this style
73+
to correctly implement a given stream program? The intuition
74+
is basically that after `n` calls to the `step` function,
75+
the state of the ring-buffers of the C program should correctly
76+
compute the value of the corresponding stream expression
77+
evaluated at index `n`, assuming the C program has been fed
78+
inputs corresponding to the first `n` values of the external stream
79+
inputs. Moreover, the trigger functions should be called from
80+
the `step` function exactly at time values when the stream expressions
81+
evaluate to true.
82+
83+
The notion of correspondence for the values flowing in streams is
84+
relatively straightforward: these values consist of fixed-width
85+
machine integers, floating-point values, structs and fixed-length
86+
arrays. For each, the appropriate notion of equality is fairly clear.
87+
88+
Both the original Stream program and the generated C program
89+
can be viewed straightforwardly as a transition system, and under
90+
this view, the correspondence we want to establish is a bisimulation
91+
between the states of the high-level stream program and the low-level
92+
C program. The proof method for bisimulation requires us to provide
93+
a "correspondence" relation between the program states, and then prove
94+
three things about this relation:
95+
96+
1. that the initial states of thee programs are in the relation;
97+
2. if we assume two arbitrary program states begin in the relation
98+
and each takes a single transition (consuming corresponding inputs),
99+
the resulting states are back in the relation;
100+
3. that any observable
101+
actions taken by one program are exactly mirrored by the other.
102+
103+
On the high-level side of the bisimulation, the program
104+
state is essentially just the value of the current time step `n`,
105+
whereas on the C side it consists of the regions of global memory that
106+
contain the ring-buffers and their current indices. The transition
107+
relation for the high-level program just increments the time value by
108+
one, and the transition for the C program is defined by the action
109+
of the generated `step()` function.
110+
111+
Suppose `s` is one of the stream definitions in the original Copilot
112+
program which is required to retain `k` previous values;
113+
let `buf` be the global variable name of the ring-buffer in the C
114+
program, and `idx` be the global variable name maintaining the
115+
current index into the ring buffer. Then the correspondence
116+
relation is basically that `0 <= idx < k` and
117+
`s[n+i] =buf[(idx+i) mod k]` as `i` ranges from `0 .. k-1`.
118+
By abuse of notation, here we mean that `s[j]` is
119+
the value of the stream expression `s` evaluated at index `j`,
120+
whereas `buf[j]` means the value obtained by reading the `j`th value
121+
of the buffer `buf` from memory. The overall correspondence relation
122+
is a conjunction of statements like this, one for each stream
123+
expression that is realized via a buffer.
124+
125+
### Implementing the Bismulation proof steps
126+
127+
The kind of program correspondence property we desire is a largely
128+
mechanical affair. As the code under consideration is automatically
129+
generated, it has a very regular structure and is specifically
130+
intended to implement the semantics we wich to verify it against. As
131+
such, we expect these proofs to be highly automatable.
132+
133+
The proof principle of bisimulation itself is not amenable
134+
to reduction to SMT, as if falls outside the first-order theories
135+
those solvers understand. Likewise, the semantics of Copilot
136+
and C might possibly be reducible directly to SMT, but it would be
137+
impractical to do so. However, we can reduce the individual
138+
proof obligations mentioned above into a series of lower-level
139+
logical statements that are amenable to SMT proof by
140+
defining the logical semantics of stream programs, and using
141+
symbolic simulation techniques to interpret the semantics of the
142+
C program. Performing this reduction is the key contribution
143+
of `copilot-verifier`.
144+
145+
#### Initial state correspondence
146+
147+
The proof first obligation we must discharge is to show that
148+
the initial states of the two programs correspond. For each
149+
stream `s` there is a corresponding `k`, which is the length of
150+
the ring-buffer implementing it. We must simply verify that
151+
the C program initializes its buffer with the first `k` values
152+
of the stream `s`, and that the `idx` value starts at 0.
153+
Because of the restrictions Copilot places on programs, these
154+
first `k` values must be specified concretely and will not be
155+
able to depend on any external inputs. As such, this step
156+
is quite easily performed, as it requires only direct evaluation
157+
of concrete inputs.
158+
159+
#### Transition correspondence
160+
161+
The bulk of the proof effort consists of demonstrating that
162+
the bisimulation relation is preserved by transitions.
163+
In order to do this step, we must begin with totally symbolic
164+
initial states: we know nothing except that we are at some
165+
arbitrary time value `n`, and that the C program buffers
166+
correspond to their stream values as required by the relation.
167+
Thus, we create fresh symbolic variables for the streams
168+
from `n` to `n + k-1`, and for the values of all the involved
169+
external streams at time `n`. Then, we run forward the Copilot
170+
program by evaluating the stream recurrence expression to
171+
compute the value of each stream at time `n+k`.
172+
173+
Next we set up an initial state of the C program by choosing,
174+
for each ring buffer, an arbitrary value for its current index
175+
within it's allowed range, and then writing the variables
176+
corresponding to each stream value into the buffers at
177+
their appropriate offsets. The symbolic simulator is then
178+
invoked to compute the state update effects of the `step()`
179+
function. Afterward, we read the poststate values from the
180+
ring-buffers and verify that the correspond to the stream
181+
values from `n+1` up to `n+k`.
182+
183+
As part of symbolic simulation, Crucible may also generate
184+
side-conditions that relate to memory safety of the program, or to
185+
error conditions that must be avoided. All of the bisimulation
186+
equivalence conditions and the safety side-conditions will be
187+
submitted to an SMT solver.
188+
189+
#### Observable effects
190+
191+
For our purposes, the only observable effects of a Copilot program
192+
relate to any "trigger" functions defined in the spec. Our task it to
193+
show that the generated C code calls the external trigger functions if
194+
and only if the corresponding guard condition is true, and that the
195+
arguments passed to those functions are as expected.
196+
This proof obligation is proved in the same phase along with
197+
the transition relation proof above because the `step()` function
198+
is responsible for both invoking triggers and for performing state
199+
updates.
200+
201+
The technique we use to perform this aspect of the proof is to
202+
install "override" functions to the external symbols corresponding
203+
to the C trigger functions before we begin symbolic simulation.
204+
In a real system, the external environment would be responsible
205+
for implementing these functions and taking whatever appropriate
206+
action is necessary when the triggers fire. However, we are verifying
207+
the generated code in isolation from its environment, so we have no
208+
implementation in hand. Instead, the override will
209+
essentially implement a stub function that simply captures its
210+
arguments and the path condition under which it was called.
211+
After simulation completes, the captured arguments and path condition
212+
are required to be equivalent to the corresponding trigger guard
213+
and arguments from the Copilot spec. These conditions are
214+
discharged to the SMT solver at the same time as the transition
215+
relation obligations.
216+
217+
Because of the way we model the trigger functions, we make a number of
218+
implicit assumptions about how the actual implementations of those
219+
functions must behave. The most important of those assumptions is that
220+
the trigger functions must not modify any memory under the control of
221+
the Copilot program, including its ring buffers and stack. We also
222+
assume that the trigger functions are well defined, i.e. they are
223+
memory safe and do not perform any undefined behavior. Finally, we
224+
assume that they implement "normal" control flow and will eventually
225+
return to their caller. This last requirement may well be violated if
226+
the trigger function actually performs some aborting action, or
227+
otherwise halts normal execution; however, this seems relatively
228+
harmless from the point of view of correctness of the generated code.

0 commit comments

Comments
 (0)