Improve the "diverges" effect
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:
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.