GitLab

This is a followup on !19 (merged) . After a long brainstorming session with @paskevyc , here is the system we have devised to improve the diverges effect, so that it covers a lot more cases.

Regarding the implementation, divergence is currently encoded by a boolean named Ity.eff_oneway. We propose to replace this boolean by a tristate value that says ghostifiable (1) or non-ghostifiable terminating (2) or possibly non-terminating (3). State 2 is the new one; the semantics of the other two is left unchanged. The ordering is from left to right, i.e., combining a state-i expression with a state-j expression gives an expression with state max i j. Moreover, a val declaration with a given state can only be refined with a let definition with a state lower or equal. A val diverges declaration has state 3, and so has a non-terminating let expression. A ghost expression can only have state 1. A let definition with state 3 must be explicitly specified as diverges. So, the two critical points are that a let definition with state 2 does not need to be specified as such, and that it can be declared neither ghost nor function.

Regarding the surface language, we just need a new effect keyword to specify that a val declaration has state 2. For now, we do not give any way for the user to split state 2 into several subcategories for the sake of documentation; this can come later.

Applications of this new state are:

• peano.Int63.to_in63 @bobot ;
• alloca and c_assert @rrieuhel ;
• read, write, random, etc.

Note that, in the later applications, e.g. random, we no longer need a dummy writes specification (if we are not interested in a bit-precise modeling). Note also that state 2 has been described as terminating, but it should be understood as terminating if the environment is cooperating. For example, a WhyML program with state 2 can end up being killed by SIGPIPE during a write call.

I am assigning this report to @rrieuhel . But @bobot, if you need it soon, do not hesitate to take over.