# Proof assumptions

A proof assumption is anything that limits the applicability of a statement that has been otherwise proved by CBMC. An example of a proof assumptions is the assumption that packets coming off a network are of size at most 1024 bytes. This proof assumption would arise if the proof harness for a function modeled an incoming packet as any character buffer of size at most 1024 characters. Suppose that we run CBMC with this proof harness, and CBMC is unable to find any memory safety errors. We might be tempted to say that CBMC has proved the function is memory safe. But the truth is that CBMC has proved the function is memory safe only when the function is invoked on a packet of size at most 1024 characters. We believe that such a proof has value, and that hard-to-find software issues will be discovered in the course of writing such a proof, but the result is not absolute proof of memory safety.

Just to clear, every proof in mathematics depends on proof assumptions.
In number theory, a theorem may hold for all integers `n`

, assuming `n`

is nonzero. The theorem is powerful because it is applicable to nearly
every integer. In cryptography, a theorem may hold only if `n`

is the product
of two prime numbers `p`

and `q`

of roughly the same size. The theorem
may still have powerful applications, but it applies only to a much smaller
set of integers.

Proof assumptions must be clearly and accurately communicated to any proof reader and to any consumer of the proof. Doing this right may be the hardest part of proof. It is particularly important in the context of software proof, however, because the credibility of the proof tool and the methodology for using the tool depends on getting this right. Trust is hard to earn and easy to lose.

The two most common sources of proof assumptions are memory allocation and function abstraction.

## Memory allocation

There are two common proof assumptions about memory.

### Size

One class of assumption is size. Some are obvious. If the proof harness includes

```
size_t size;
__CPROVER_assume(size < 100);
char *buffer = (char *) malloc(size);
```

then the buffer is assumed to be of size smaller than 100. Some are implicit. If the proof harness includes

```
size_t size;
char *buffer = (char *) malloc(size);
```

then the buffer is implicitly bounded to the size of the maximum object that CBMC can model (which is probably smaller than the largest size representable in a 64-bit integer, see our discussion of the memory model for more information).

### Invariants

One class of assumption is well-formedness or implicit data structure invariants. Suppose the proof harness includes

```
typedef struct {
size_t size;
char *buffer;
} buffer_t;
buffer_t *buffer = (buffer_t *) malloc(sizeof(*buffer));
buffer->buffer = (char *) malloc(buffer->size);
```

then the proof harness is implicitly assuming that the pointer `buffer->buffer`

is either NULL or a valid pointer to a buffer of size `buffer-size`

. This
is implicitly assuming an data structure invariant about `buffer`

.
Is this really something you want to assume about a buffer you receive as
input from an untrusted adversary. Is this really something want to assume
even when `buffer->size == 0`

?

## Function abstraction

There are two common kinds of function abstraction with CBMC.

### Missing functions

One is implicit function abstraction done automatically by CBMC.

When CBMC encounters
the invocation of a function `missing`

and cannot find a function definition
for `missing`

, CBMC issues a warning "no function body for `missing`

" and
models the function `missing`

as a function that

- has no side-effects (makes no change to the state), and
- returns an arbitrary, unconstrained value of the appropriate return type.

This assumption of no side-effects is a serious assumption. Almost no
functions in C are purely functional. On the other hand, it is
an easy way to model something like a random number generator returning
a `unint64_t`

used in some cryptographic code under test.
Including the actual function definition of the random number generator
will probably be too much for CBMC, but by leaving the function
undefined (omitting the code defining the random number generator
from the build), CBMC will consider the impact on the property being
testing of every unsigned, 64-bit integer value that can possibly
be returned by the number generator.

### Stubs

One is explicit function abstraction written by the proof author for the proof.

Consider a cryptographic key generator

```
int key_generator(void *context, public_key_t *public, private_key_t *private)
```

As with the random number generator, including the code for a cryptographic key generator may be too much for CBMC. Reconstructing cryptographic keys is, after all, designed to be intractable!

A reasonable stub for the key generator is:

```
int key_generator(void *context, public_key_t *public, private_key_t *private)
{
__CPROVER_havoc_object(public);
__CPROVER_havoc_object(private);
int rc;
return rc;
}
```

The `__CPROVER_havoc_object`

function fills the objects pointed to by `public`

and `private`

with arbitrary, unconstrained data.

This stub has the pleasing effect of considering possible every value
(well-formed or not) that could be written to `public`

and `private`

by the generator,
and considering possible every integer value that could be used as a
return code.

This stub is, however, making the implicit assumption that the pointers are valid. A better stub would check that the function is being called correctly:

```
int key_generator(void *context, public_key_t *public, private_key_t *private)
{
__CPROVER_assert(context, "context is nonnull");
__CPROVER_assert(public, "public is nonnull");
__CPROVER_assert(private, "private is nonnull");
__CPROVER_havoc_object(public);
__CPROVER_havoc_object(private);
int rc;
return rc;
}
```