Next steps for Magmide: using Iris

[blainehansen]

Hello!
If you've been watching this repo for a while, you've probably begun to notice that progress is... slow.

The explanation for this is simple: I don't have time! Aside from the "usual" reasons (having a demanding full-time job, being a father), I've temporarily been working on the Persistent Democracy project instead of Magmide. There's one big reason why:

My hope for Persistent Democracy is that it could solve more urgent societal problems. And since it's easier to complete relatively quickly, I was more confident I could build it to the point of having momentum more quickly. It isn't to that point yet (I just barely finished the first real version of the book describing it), but the hope is it could build structures such as persistently democratic open source project cooperatives that could support things like Magmide. After I was unable to find somewhere willing/able to support Magmide so I (or someone) could work on it full-time, I decided it might make more sense to get the ball rolling on those kinds of truly public good supporting structures first.

But I've also realized we don't have to wait before making any progress. So this post is laying out my thoughts about the next stage of work, just like this previous discussion laid out the basic parser infrastructure.

The most important next milestone is to figure out how to use Iris in Magmide. This doesn't promise to be easy, partly because Iris is hard (the papers describing it are much more approachable than most academic papers.... but still), but mostly because Magmide can't/shouldn't use Iris the same way most projects have, which means we have fewer examples to learn from.

I'll just repost a question I asked on the Iris chat to convey why this is:

---

Blaine Hansen:
Hello!

I'm working on the Magmide project, which intends to be a proof language that deeply supports formalizing and compiling imperative bare metal code in a manner that's approachable to practicing engineers.

I want to use Iris, but based on Magmide's goals it seems important to formalize the operational semantics in a more "true" code-as-data style with machine states and an instruction pointer that determines how the step relation works, rather than using a lambda calculus with continuations.

For example, simplified:

Inductive Instruction :=
	(* ... *).

Notation word := (* whatever type represents values, likely just `nat` at first *).

Record MachineState := machine_state {
	instruction_pointer: word;
	registers: (vec word size);
	program_memory: list Instruction
	(* a simplification, eventually want just normal memory *)
}.

Inductive Step: MachineState -> MachineState -> Prop :=
	(* ... *).

Then it's possible to define a proposition that describes program traces using lists, so list operations could be lifted to the trace type:

Inductive Trace: list MachineState -> Prop :=
	| Trace_start: forall start,
		Trace [start]

	| Trace_step: forall past cur next,
		Trace (past ++ [cur])
		-> Step cur next
		-> Trace (past ++ [cur] ++ [next])
.

It's not clear to me whether a semantics like this is even compatible with Iris. The Iris codebase requires some value type and proofs that value is a stuck normal form, and that isn't really a meaningful concept in a semantics like this. If the assembly language has some exit instruction that is defined to not be able to take a step, then I suppose you could get some concept of stuckness from states that point to an exit instruction, but I'm not sure that would even be the same.

I haven't yet gotten to the point where I'm trying to integrate Iris, but I wanted to ask this question ahead of time. Can anyone see any problems I might encounter trying to use Iris in this paradigm? Are there parts of the docs or codebase that I seem to be missing that would fill in this gap?

Thank you! Iris is amazing 🙂
Blaine

Léon Gondelman:
Hello!

You can take a look at the capability machines formalisation in Iris.
(Here is the link to the public repo, and here is the description of machine words, machine state and instructions

I know little about this project, but you can talk to the authors of this project, if it seems to be of help.

Armaël Guéneau:
https://github.com/logsem/cerise should be nicer to look at and a bit more up to date

(I am one of the (later) contributors to the capability machines formalization, cc also @ageorg29)

AFAIK there's basically two ways of dealing with the fact that a machine operational semantics typically has no notion of expression/value

option 1 is to do as is done in cerise, and have a dummy notion of expression (and corresponding values) that amounts to having expressions "do 1 step" or "repeat many steps" (cf expr and val in cap_lang.v). This allows instantiating the EctxiLanguage building blocks provided by Iris and gives you some wp rules for free.

but there's an option 2, which is to define operational semantics the way you like, and define a wp yourself. This is a bit more work, but I suspect that it might be nicer in the long run

---

It seems obvious option 2 is the right choice. We need to define our own wp (weakest precondition predicate). Read Separation Logic Foundations to understand what this is.

Honestly, I don't know how difficult this is going to be. My plan once I got time was to read the Iris papers again and deeply read the relevant parts of the source to understand how to do this. I'm scared defining a custom weakest precondition is going to require wrangling with the nasty category theory inside Iris, but I'm not sure yet!

So broadly we have to do these things:

• Define the machine semantics in the way we want. I can do this, and I'm planning to do so in the coming weeks. I'm going to do this first in an easy way, without making the semantics exactly precisely accurate. As long as it includes instructions in the machine state and defines the step relation based on an instruction pointer, it will allow us to tackle that most important and complex topic of a custom weakest precondition.
• Instantiate Iris. (hand-waving goes here)
• Figure out how to write proofs about possibly infinite Traces. The Trace type needs to be Inductive so we can do normal proofs over finite traces, but is there a way to lift a normal Inductive to CoInductive? Is there an easier way to get what we need? Again, I'm not sure how to proceed here, and I was waiting to attack the problem until it was relevant.
• Slowly increase the complexity/accuracy/generality/usefulness of the operational semantics and machine state, migrating the weakest precondition as necessary.
• At this point we could do things like mimic Iron to create the trackable effects system, fit the semantics to approximate LLVM, and actually start building real interesting programs! We'd be off to the races!

You can see that the biggest obstacle in the way of this plan is the (perceived) difficulty of Iris. What we want to do is certainly possible, but I don't yet have the time to make aggressive progress.

Honestly, one of the most useful things anyone could do to help Magmide is to produce a more approachable explanation of Iris and its innards, "Iris for humans" if you want to think about it that way.

Again, I'm sorry to everyone! I wish I had more time/resources to work on Magmide. I assure you I won't abandon this project, no matter how long it takes. The world needs something like Magmide, and even if we have to wait for things like persistently democratic open source project cooperatives, it will happen.

Thank you!

[jeremyschlatter]

Thanks, Blaine! I'm making my way through the Software Foundations textbooks you linked.

I'm planning to read Volume 6: Separation Logic Foundations, but first I'm starting with the prerequisites: Volume 1: Logical Foundations and the first three chapters of Volume 2: Programming Language Foundations.

The textbooks are excellent. I highly recommend them to anyone else interested in following along with Magmide. The exercises in the text are self-grading, which is quite helpful for learning.