Xavier Denis

Fix #127

12

Adds a `#[creusot::decl::opaque]` annotation which prevents using the body of a definition in dependencies.

Add support for `old`

10

The specifications used in #83 critically depend on having a functioning version of `old` in pearlite. On the one hand this requires adding support for the syntax of `old` but...

Currently the specification of `Vec::pop` is less than optimal: the encoding of `match` in the logic means that the code in the attached test is not automatically provable without a...

The core loop of Creusot is powered by a 'query' system: a HashMap which stores the results of translating functions. Structuring things as queries is quite natural when interacting with...

I don't like _having_ to name my invariants, we should generate a name for you if you didn't provide one. We must provide a name at some level as its...

Support macro invocations in pearlite terms.

1

We should allow calls to macros in pearlite terms. Currently this is an error in `pearlite_syn`.

Provide `derive` macros for `Resolve`

1

These traits are going to end up being quite pervasive in `Creusot` developments but most instances will be incredibly boring, we should provide `derive` macros to handle those cases: sums,...

At the moment, we have a rather [basic](https://github.com/xldenis/creusot/blob/master/creusot/src/ctx.rs#L223-L237) error reporting mechanism, as a result most of Creusot just panics upon an error. Obviously this sucks: we don't produce helpful error...

Creusot is starting to get large, it would be beneficial to have _proper_ documentation of how to use creusot. This should cover a few key aspects 1. Pearlite: Syntax, Type...