Limited functions

[fpoli]

How hard would it be to add limited non-heap-dependent functions to Silicon, e.g. with a command-line flag to specify the maximum instantiation depth to be used in the program? In Prusti we ended up axiomatizing limited functions on our own instead of using Viper functions, but that has various downsides (it adds some complexity to Prusti, other frontends cannot benefit from it...).

To give a concrete example, --instantiationDepth=2 should be enough to verify the following program. The default value can be --instantiationDepth=1 to make the change backward compatible.

function identity(x: Int): Int
    requires x >= 0
    ensures result >= 0
{
    x == 0 ? 0 : 1 + identity(x - 1)
}

method test() {
    assert identity(3) >= 2 // Currently, this does not verify in Silicon
    assert identity(3) >= 1 // Ok
}

The limited functions axiomatization would also make it possible to have Dafny-like opaque functions in Viper, imagining that the instantiation depth can be configured per function and/or per call.

[mschwerhoff]

I'm open to the idea, but would like to understand a few things better. E.g.

• why the focus on heap-independent functions?
• is one depth for all sufficient, or wouldn't it be better to add one per function (via an annotation? AST meta data?), while we're at it?
• why is backend support necessary, i.e. why not address the issue why a Silver plugin?

One could also consider carrying the idea over to axioms (finite unrolling up to instantiationDepth).

Regarding how hard it would be: I won't have time, but I assume it wouldn't take Marco too long to implement a first solution. With more substance, it could also be a PW project, I'd believe.

[fpoli]

• why the focus on heap-independent functions?

Because we have a use case for it in Prusti. Limited heap-dependent functions sound interesting too, but we don't have a use case for it at the moment.

• is one depth for all sufficient, or wouldn't it be better to add one per function (via an annotation? AST meta data?), while we're at it?

One depth is the minimum that makes the feature usable. More flexibility would be better, sure, but if I were the one that implements it I would probably not do the extra work.

• why is backend support necessary, i.e. why not address the issue why a Silver plugin?

If it's possible yes, sure. I got the feeling that backend support is easier because it's about tweaking some axioms. Also, I wonder whether a plugin solution can be as efficient as the change to the axioms.

One could also consider carrying the idea over to axioms (finite unrolling up to instantiationDepth).

That's what I thought, yes. I'm not sure how to do it efficiently otherwise. In Prusti we generate those axioms, but they seem more appropriate as a Viper feature than as a Prusti feature.

Regarding how hard it would be: I won't have time, but I assume it wouldn't take Marco too long to implement a first solution. With more substance, it could also be a PW project, I'd believe.

If it's reasonably easy I can even consider doing it myself. For example, if working on the Rust generation of the axioms is more work than implementing the feature in Silicon directly.

[mschwerhoff]

I'm not yet convinced that hacking something into Silicon is the right way to go, if there is basically no argument for why it has a chance of performing better than a Silver plugin. If it's not the performance: I doubt that changing Silicon will be easier than writing a plugin.

In both cases, it seems that distinguishing between heap-dependent and heap-independent pure functions will likely just increase complexity. Targeting all pure functions seems more reasonable.

In any case: if you feel like it, just go ahead an implement the feature in a Silicon branch. If it turns out to be beneficial for Prusti (and if it's not messing up Silicon too much), I wouldn't mind merging it in.

[fpoli]

Thanks! I never wrote a plugin; it's useful to know that it's not necessarily slower nor more complex than directly modifying Silicon.