Implementing `Invariant` is just under twice as slow as creating a function called `invariant` and manually adding `requires`/`ensures`

[sarsko]

NOTE: (Okay, I just remembered #[why3::attr = "inline:trivial"] exists, which, when added to the fn invariant in Invariant causes the two implementations to take roughly the same amount of time).

Implementing Invariant seems to generate "one more layer of indirection" which for me (4 solvers, Auto Level 3) causes invariant from Invariant to take just under twice as long (27s vs 14s) as implementing fn invariant as a regular predicate and then manually adding requires/ensures.

---

As a related note:

NOTE: (This note seems to be partially annulled by the existence of #[why3::attr = "inline:trivial"])

Most invariants I have encountered are a conjunction of invariants. This means that proving them often requires a gazillion splits. Sometimes (ie during development of CreuSAT), I would have to either manually do these split steps, or manually unroll parts of the invariants in the code and either proof_assert! or requires/ensures-ing those directly. I therefore think there is a case to be made for doing this automatically, as in: the code below doesn't add: [requires(self.invariant())] [ensures((^self).invariant())] but rather: [requires(self.wait > 0usize)] [requires(self.period > 0usize)] [ensures((^self).period > 0usize)] [ensures((^self).wait > 0usize)] (If each conjunct was itself an invariant, then these could themselves be unrolled further).

This doesn't have to be on by default, but could either be set by optionally annotating each invariant with an unroll level (I guess this is like #[why3::attr = "inline:trivial"], but in the "opposite direction"), or by passing a compilation flag.

---

To test the speed, I do the following:

1. Load it up into Why3 IDE
2. Split on the Update node
3. Select the postcondition node (for me that is number 5, the last one)
4. Call Auto Level 3, starting timing at the same time.
5. When the node is verified, time is stopped.

#[allow(clippy::upper_case_acronyms)]
struct EMA {
    value: f64,
    alpha: f64,
    beta: f64,
    wait: usize,
    period: usize,
}

impl EMA {
    #[predicate]
    fn invariant(self) -> bool {
        pearlite! {
            self.wait > 0usize
            && self.period > 0usize
        }
    }
}

impl EMA {
    #[requires(self.invariant())]
    #[ensures((^self).invariant())]
    fn update(&mut self, next: f64) {
        self.value += self.beta * (next - self.value);

        if self.beta > self.alpha {
            self.wait -= 1;
            if self.wait == 0 {
                if self.period < usize::MAX / 2 {
                    self.period *= 2;
                }
                self.wait = self.period;
                self.beta *= 0.5;
                if self.beta < self.alpha {
                    self.beta = self.alpha;
                }
            }
        }
    }
}

Checks out in 14.22

#[allow(clippy::upper_case_acronyms)]
struct EMA {
    value: f64,
    alpha: f64,
    beta: f64,
    wait: usize,
    period: usize,
}

impl Invariant for EMA {
    #[predicate]
    fn invariant(self) -> bool {
        pearlite! {
            self.wait > 0usize
            && self.period > 0usize
        }
    }
}

impl EMA {
    fn update(&mut self, next: f64) {
        self.value += self.beta * (next - self.value);

        if self.beta > self.alpha {
            self.wait -= 1;
            if self.wait == 0 {
                if self.period < usize::MAX / 2 {
                    self.period *= 2;
                }
                self.wait = self.period;
                self.beta *= 0.5;
                if self.beta < self.alpha {
                    self.beta = self.alpha;
                }
            }
        }
    }
}

Checks out in 27.27

[xldenis]

I think realistically Creusot needs to at least heuristically add inline_trivial to certain definitions. Perhaps there's a more systematic approach we can take as well.

I believe we have a Why3 GT soon-ish which should allow us to discuss this (for the why3 side)

[jhjourdan]

Actually, inline_trivial may or may not be what we want, because it only changes what is emitted to proves, not what is shown to the user. I.e., inline_trivial does not change the behavior of the split transformations.

But your are right that invariant add one layer of indirection which might be harmful for the performance. Not sure what we can do: should we inline in Creusot user invariants in structural invariants?