Upstream DM for Monotonic State

[andricicezar]

Dear all,

Recently, I built a Dijkstra Monad for Monotonic State using a Free Monad as the base, instead of the usual state-passing monad. The surprising benefit is that it seems one could use this DM without being unsound (compared to state-passing, as described in section 2.2 in Recalling a witness).

You can check my development here.

The current STATE_h effect has to be abstract because the state-passing monad does not have enough structure to enforce the monotonicity of the state, which is necessary for witness/recall to be sound. This means that, if it is not abstract, one could mount the attack presented in section 2.2: a computation that witnesses something, to which we bind a continuation where we reify and run recall with a state that violates the preorder. (PoC here)

My impression is that against the DM I use, the same attack cannot be mounted because the monad is more syntactic. One cannot reify recall and pass it a state and a witness. One can build non-monotonic syntax by using the free monad (see here), but it cannot be typed as the DM (see here).

I would like to know your opinion about this! If I'm correct, and this representation removes the need to have State as an abstract effect, then I would like to try to upstream it because it would have the following nice benefits: de-axiomatize the STATE_h effect (plus, FStar.ST and FStar.HyperStack.ST) and also having a representation to reify to/reflect into.

I discussed about this in the past few weeks with: @catalin-hritcu, @danelahman and @kyoDralliam.