# Hiding local proofs with `assert(...) by { ... }`

## Motivation

Sometimes, in a long function, you need to establish a fact `F` that requires
a modest-size proof `P`. Typically, you do this by `...; P; assert(F); ...`.
But doing this comes with a risk: the facts `P` introduces can be used not
only for proving `F` but also for proving the entire rest of the
function. This gives the SMT solver much more to think about when proving things beyond
`assert(F)`, which is especially problematic when these additional facts are
universally quantified. This can make the solver take longer, and even time out, on
the rest of the function.

## Enter `assert(...) by { ... }`

Saying `assert(F) by {P}` restricts the context that `P` affects, so that
it's used to establish `F` and nothing else. After the closing brace at the
end of `{ P }`, all facts that it established except for `F` are removed from
the proof context.

## Underlying mechanism

The way this works internally is as follows. The solver is given the facts following
from `P` as a premise when proving `F` but isn't given them for the rest of
the proof. For instance, suppose `lemma_A` establishes fact `A` and `lemma_B`
establishes fact `B`. Then
```
lemma_A();
assert(F) by { lemma_B(); };
assert(G);
```
is encoded to the solver as something like `(A && B ==> F) && (A ==> G)`. If `B` is an expansive fact
to think about, like `forall|i: int| b(i)`, the solver won't be able to think about it
when trying to establish `G`.

## Difference from auxiliary lemmas

Another way to isolate the proof of `F` from the local context is to put the
proof `P` in a separate lemma and invoke that lemma. To do this, the proof
writer has to think about what parts of the context (like fact `A` in the
example above) are necessary to establish `F`, and put those as `requires`
clauses in the lemma. The developer may then also need to pass other variables
to the lemma that are mentioned in those required facts. This can be done, but
can be a lot of work. Using `assert(F) by { P }` obviates all this work. It
also makes the proof more compact by removing the need to have a separate
lemma with its own signature.