Verification of functions using mutability (STRef)

Stream: Program verification

[Francisco Giordano]

Sorry for the broad question but I am wondering if in general functions using mutability such as STRefs in Lean are amenable to verification, so if it is possible to prove theorems about those functions in Lean. Interested in any thoughts about this.

[Jannis Limperg]

As it stands, no. Lean would need to provide a semantics for IO actions, which are currently completely opaque (i.e. you can't prove anything about them). In principle, sure, such a semantics could be provided.

[Shreyas Srinivas]

To what degree is this an open question?

[Jannis Limperg]

Don't know. I imagine someone must have experimented with stuff like this though.

[Mario Carneiro]

Here's a relevant quote from me on the matter:

By the way (on the subject of "This conflicts with my belief that monadic code should also be able to be proven correct"), I have a strong suspicion that ST is inconsistent, or at least ST augmented with reasonable axioms for how references behave, although I have not been able to prove it. (The short version is that ST ω Unit is an impossibly big type, since it seems to hold the state of an arbitrary number of references in arbitrarily large types, including ST ω Unit itself.)

[Mario Carneiro]

Continued in a PM with @Joe Hendrix (I think there is nothing in here which can't be reprinted):

Mario Carneiro: The ST monad lets you create new references with ST.mkRef, and these references can store values of any type

Mario Carneiro: and the current state of all references is conceptually "stored in" the monad state

Mario Carneiro: This is in stark contrast to StateT, which has space for exactly one "reference", and the type of this reference is part of the monad itself

Joe Hendrix: Oh, I interpreted that as meaning types in bigger universes. It does seem tricky to formalize.

Mario Carneiro: Well the fact that it's any type in the same universe is already bad

Mario Carneiro: If ST lived one universe up it would be fine

Mario Carneiro: but you can create ST.Refs containing the whole monad state, this is a short trip to cantor's paradox

Mario Carneiro: ST was originally designed for haskell, which uses System F as it's underlying theory, and there the whole thing with quantifying over types as a means of abstraction works marvelously. But in lean we can't do this because it's basically Type : Type, and in the context of a universe hierarchy it is deeply suspicious that ST doesn't involve a universe bump

[Joe Hendrix]

Thanks Mario. Monadic verification is something I plan to work on in 2024. Lean should support Hoare triples on monadic computations. There's some existing work in Std due to @Mario Carneiro.

Due to the above foundational issues, I think we may not be able to reason about IO, but rather some subset that includes no references or constrained references.

[Shreyas Srinivas]

Are there literature references you would recommend to someone who wishes to work on this problem. For reference I am currently taking a graduate semantics course which covers basic stuff upto system F and then switches to separation logic (iris) in the second half.

[Joe Hendrix]

I haven't looked closely myself. Relational Hoare triples is a topic that comes up in this context, and this was one of the first results when searching for papers on the topic.

[Francisco Giordano]

Mario Carneiro said:

a strong suspicion that ST is inconsistent, or at least ST augmented with reasonable axioms for how references behave

I'd be interested in seeing a draft of what these axioms could be