Formal Specification for Dis VM?

[Andrew Gunawan]

I've been looking around at the space, and noticed that porting efforts for Inferno (The Challenges of porting Inferno to RISC-V, Stephansen; Porting Inferno OS to ARMv7-M and Cortex-M7, Berven) onto newer platforms would be helped by a tighter definition of the semantics of the Dis VM.

Are there any internal documents that describe the behaviour of the Dis VM in a more precise or detailed manner? If not, what about any specification efforts to tighten down the description of the Dis VM?

I'm asking this because I'm really interested in Inferno, and I think it would be a fun project to try to document the semantics of the Dis VM. Kind of as a learning project, because I want to learn to read other people's code, and also dip my toes into formal methods.

My professor is willing to help me figure this out, so I won't be flying blind, but he's also not too familiar with Inferno. He is, however, a formal methods junkie.

Something I've noticed is that the document "The Dis VM Specification" on the inferno-os website (https://inferno-os.org/inferno/papers/dis.html) is an informal specification that explains per-instruction semantics in prose, leaving the reader to interpret any ambiguities by consulting the C source code, or the VM execution itself.

For example, in the description for the case instruction:

pc = 0..i: dst[i].pc where
    dst[i].lo >= src && dst[i].hi < src

Meanwhile, the prose says, "searches the table for the first matching value where the src operand is greater than or equal to the low word and less than the high word"

Which contradicts the code snippet. The prose says `src >= dst[i].lo && src < dst[i].hi` from what I understand. So we need to consult the source (which at that point does cast into doubt how authoritative the spec is).

Looking at libinterp/xec.c:OP(icase)

OP(icase)
{
WORD v, *t, *l, d, n, n2;

v = W(s);
t = (WORD*)((WORD)R.d + IBY2WD);
n = t[-1];
d = t[n*3];

while(n > 0) {
n2 = n >> 1;
l = t + n2*3;
if(v < l[0]) {
n = n2;
continue;
}
if(v >= l[1]) {
t = l+3;
n -= n2 + 1;
continue;
}
d = l[2];
break;
}
if(R.M->compiled) {
R.PC = (Inst*)d;
return;
}
R.PC = R.M->prog + d;
}

I'm assuming icase means integer case. Also this snippet is beyond my current level of C fluency. Which is part of the reason that I'm hoping to embark on this project.

While it's extremely tempting to outsource the work to LLMs, so it's actually done quicker, I do not want to shortchange my own learning. Anyway, I do think that people immersed in this ecosystem may provide better insights than an LLM.

Anyway, this is my first post in this user group :)

Best wishes,

Andrew

[da...@boddie.org.uk]

[Resending this via the Google Groups interface...]

On Wednesday, 15 July 2026 at 05:26:40 UTC+2 andrewgu...@gmail.com wrote:

> I've been looking around at the space, and noticed that porting efforts for

> Inferno (The Challenges of porting Inferno to RISC-V, Stephansen; Porting

> Inferno OS to ARMv7-M and Cortex-M7, Berven) onto newer platforms would be

> helped by a tighter definition of the semantics of the Dis VM.

>

> Are there any internal documents that describe the behaviour of the Dis VM

> in a more precise or detailed manner? If not, what about any specification

> efforts to tighten down the description of the Dis VM?

I thought there were efforts before to write an improved specification,

though maybe I'm mistaken. There were efforts to write independent

implementations. There's this one, at least:

https://bitbucket.org/linuxuser27/disvm

> I'm asking this because I'm really interested in Inferno, and I think it

> would be a fun project to try to document the semantics of the Dis VM.

> Kind of as a learning project, because I want to learn to read other

> people's code, and also dip my toes into formal methods.

>

> My professor is willing to help me figure this out, so I won't be flying

> blind, but he's also not too familiar with Inferno. He is, however, a

> formal methods junkie.

This sounds like a good situation to be in. You want to learn about

something, tie it to a field of study, and you have a supportive professor.

> Something I've noticed is that the document "The Dis VM Specification" on

> the inferno-os website (https://inferno-os.org/inferno/papers/dis.html) is

> an informal specification that explains per-instruction semantics in prose,

> leaving the reader to interpret any ambiguities by consulting the C source

> code, or the VM execution itself.

>

> For example, in the description for the case instruction:

>

> pc = 0..i: dst[i].pc where

> dst[i].lo >= src && dst[i].hi < src

>

> Meanwhile, the prose says, "searches the table for the first matching value

> where the src operand is greater than or equal to the low word and less

> than the high word"

Yes, it looks like the logic is inverted in the prose.

"icase" corresponds to the case instruction. I imagine that "icase" was used

because "case" is reserved for the case keyword in C.

> While it's extremely tempting to outsource the work to LLMs, so it's

> actually done quicker, I do not want to shortchange my own learning.

> Anyway, I do think that people immersed in this ecosystem may provide

> better insights than an LLM.

Another useful approach you can try to help understand what the VM does is to

generate code with the Limbo compiler then disassemble it with the disdump

tool, or run Limbo to generate source text for the assembler.

disdump <.dis file>

limbo -S <.b file>

This should help with understanding.

> Anyway, this is my first post in this user group :)

Welcome!

David

[Andrew Gunawan]

Thanks, David! I'll go through it slowly. University inundates me.

Just wanted to introduce myself first hehe.

I'll post any updates as they come

[Charles Forsyth]

You're right that the Function condition is wrong, even though that spec really had been proofread by several people,

and that's in the partly formal part! The English text is I think correct.

It would be interesting to have a formal specification, since as you noted the source code is too detailed and overly constraining.

Compared to some others the abstract machine isn't huge, and has a fairly regular structure.

--
You received this message because you are subscribed to the Google Groups "inferno-os" group.
To unsubscribe from this group and stop receiving emails from it, send an email to inferno-os+...@googlegroups.com.
To view this discussion, visit https://groups.google.com/d/msgid/inferno-os/d24dd43a-5fea-4317-9cbf-3fc0a33aee31n%40googlegroups.com.