A longtime IF fan's experiment: writing the Z-Machine V3 Standard as a formal, executable spec

Technical Development Specifications
, ,
1

Hello — I’ve been playing interactive fiction since the 1980s; Zork and the Infocom
catalogue are a good part of why I ended up doing this for a living. This is a hobby
project that turned into something I thought this community in particular might enjoy
(and pick apart).

For a while I’ve been building a small pure-functional language called PFCL. I wanted a
proof of concept beyond the usual toy examples — something with real stateful logic but a
simple I/O surface — and the Z-Machine V3 was the obvious choice: a interpreter that
only needs line-based stdin/stdout.

Writing a whole interpreter directly in the functional language was heavy going, so I built
a tiny “intent” language on top: you describe what each function computes — typed inputs,
an output, a few clause forms — and it lowers deterministically to the functional code. Then
I transcribed the Z-Machine Standards Document v1.1 into that language, block by block —
about 228 functions covering the memory model, object tree, ZSCII text, the dictionary, and
save/restore. One function looks like this:

zmachine.op.add
GIVEN state: ZMachineState, operands: List<ZWord>
OUTPUT ZMachineState

WHERE a = list.get(0, operands)
WHERE b = list.get(1, operands)
RETURN zmachine.op.store_result(state, zword.add(a, b))

The nice surprise: the spec turned out to be target-neutral, so the same source generates
not just the functional interpreter but a single-file C one and a single-file Java one too.
All three pass czech (349/349), and the C and Java builds produce transcripts byte-for-byte
identical to dfrotz on Zork I.

Correction, edited in An earlier version of this post claimed Zork I relies on reading locals beyond a routine’s declared count. That’s wrong — thanks to zarf, Mike_G and fredrik in the replies for the catch. What actually happened is that I reached for Frotz while tracking down a bug in my earlier PFCL implementation, and mistook my own bug for a quirk of the game. For the record, the correct behaviour — which the spec implements — is that locals initialise to their header defaults per §6.4.4 and surplus arguments are discarded, exactly as Standard 1.1 specifies; an out-of-range read returns 0 in my interpreter (Frotz hands back frame residue on that path) and nothing in Zork ever reaches it. So the spec was right; only my description here was wrong.

It’s V3 only, and a proof-of-concept terminal interpreter — no Glk, no frills — but it runs
Zork I end to end and passes the V3 conformance suite, all generated from one spec.

What I’d actually like to put up for discussion is the artifact itself: a formal Z-Machine
spec written in Markdown — ordinary prose, citations, and [STD §x] references sitting right
next to machine-checkable function blocks. The Standard is prose, beautifully so, but prose
gets interpreted, which is half of why we have the compatibility quirks we all know. A
formal-but-readable companion buys two things:

  • One source, many targets. This spec produced the PFCL, C, and Java interpreters; in
    principle another platform is just one more lowering, not a from-scratch reimplementation
    that has to re-derive every ZIP quirk.
  • It could be a conformance oracle for other interpreters — including hand-written ones.
    This is the part I’d most like opinions on. You already check interpreters with czech/praxix
    and by diffing against dfrotz; a formal, executable spec might add a finer instrument.
    Because every opcode is pinned down formally, you can derive per-opcode conformance
    vectors from it — a given input state must yield a given output state, checkable opcode by
    opcode — rather than only a whole-game pass/fail, or a transcript diff that tells you
    something broke but not which opcode. The interpreters here are really just the first
    clients of that reference (and how I sanity-checked the spec: czech 349/349 on each,
    byte-identical to dfrotz on Zork I). The open question for this group is whether a
    per-opcode formal oracle is genuinely useful to someone bringing up a new interpreter, or
    whether the existing suites already cover it.

I’m not suggesting this replace the Standard — the prose is the thing, and czech/praxix
already do real work. I’d genuinely like this group’s read on whether a formal, executable
companion is useful as a conformance reference for interpreter authors, or whether it’s been
tried and I’ve reinvented a wheel. And if I’ve mischaracterised the out-of-range-locals
business above, I’d like to be set straight by people who know it far better than I do.

Thanks for reading — and for keeping this whole world alive.

4 Likes
2

Hmm, that’s surprising - ZLR allocates a managed array with just enough room for the declared locals, and it can play Zork. Reading a local past the routine’s declared count is also difficult to do in ZIL, unless it’s using the VALUE (load) opcode, which is generally only used to read global variables. Which release of Zork I did you test with?

1 Like
3

And what’s the routine that shows this?

1 Like
4

This is pretty amazing, really. To be able to produce C code means that anything with a C compiler can then bundle .z3 files and interpret and play them. Is that what is being said here? So that would be that it can be extended and stay 100% faithful. Pretty amazing. I’m not sure I 100% understand the real implications but you had me at C + .z3 = compile and play anywhere.

5

I wonder about the locals thing too as reading past the declared locals generates an diagnostic in my interpreter and I’ve not seen that happen in Zork.

Keep in mind limiting yourself to line-based stdout will get you the vast majority of z3 games it won’t get you everything. Seastalker’s upper window (defined in the spec) requires more complex output. The Lurking Horror with sound also requires features beyond the standard to play as intended. How do you handle transcript output?

6

I interpreted OP as saying that they wrote a general purpose Z-code interpreter in their high-level “intent” language, which can be mechanically translated to C (among other programming languages). So at the end of the day what you get is a Z-code interpreter in C (rather than translating a specific .z3 file into C code, which is what I think you’re saying?)

(Which, yes, does technically mean that you can play a Z-code game in more or less any environment which has a C compiler! But portable C Z-code interpreters are not new.)

7

I think this is incorrect. Ozmoo will throw an exception if this happens. We’ve had 0 reports of it happening, and we know Ozmoo’s been used a lot for many years now.

One point where the modern standard and Infocom’s own standard deviate is around what happens when calling a procedure with more arguments than it has local variables. According to the modern standard, this is perfectly fine, and the extra values are just quietly discarded, but some Infocom interpreters throw an exception, while others silently cause havoc, typically altering locals in the calling routine instead.

Very interesting project though!

1 Like
8

Thanks, all — correction first, because it’s the important bit.

I got the out-of-range locals claim wrong, and I’m grateful zarf, Mike_G and fredrik all
caught it. The short version: I’d reached for Frotz while tracking down a bug in my earlier
PFCL implementation, and ended up turning my own bug into a wrong story about the game.
There’s no routine in Zork I that reads past its declared locals, and nothing relies on
residue (tested on r119 / serial 880429).

Actually, I’m glad the mistake is mine and that Standard 1.1 is the part that’s right: Locals initialise to their header defaults per §6.4.4 and surplus arguments are discarded, exactly as Standard 1.1 says; an out-of-range read returns 0 in my interpreter (Frotz happens to hand back frame residue on that path), and nothing in Zork ever reaches it — which is why my interpreter, Frotz, ZLR and Ozmoo all play r119 the same despite handling that never-taken path differently.

To be clear, none of this touches the spec or the interpreter. The Markdown V3 spec is still
correct and still the single source the C, Java and in-browser builds are generated from —
czech passes 349/349 and the output matches Frotz on real games.

fredrik — thank you for the precise version. The genuine divergence is the
more-arguments-than-locals case, and my interpreter follows the modern Standard there: the
extras are discarded rather than thrown on or written into the caller’s locals.

Candy64 / JTN — JTN read it exactly right. It’s one general-purpose Z-code interpreter
written in the higher-level “intent” language, lowered mechanically to several targets from
that single source: PFCL, C, Java — and, through the PFCL JavaScript backend
(pfcl-compile --target ts), a single self-contained HTML page that runs the interpreter
client-side, so you can open it offline and drop in a story file to play. So what you get is
a Z-code interpreter — in C, or in the browser — not a specific .z3 compiled to C. As JTN
says, portable Z-code interpreters aren’t new; the part I find worthwhile is that every one
of those targets falls out of one source you can read as a spec.

Mike_G — you’re right that line-based stdout won’t get you everything. This was a proof of
concept, and I took it to the point where the game progressed correctly and the concept was
proven, rather than to full display coverage. So, honestly: I don’t implement the upper
window, sound, or the output streams — no Seastalker sonarscope, no Lurking Horror sound,
and to your direct question, no @output_streamoutput_streamoutput_streamoutput_stream transcript. Those are exactly the gaps if
this were ever taken past PoC.

On where this goes: the Z-machine spec was a side proof of concept. My actual focus right
now is PFCL and the Intent language as general-purpose languages and a runtime. The Markdown
spec can keep going in an exploratory direction — how the rest of an interpreter, and even
other authoring systems, might be formalised in the intent-lang format.

Thanks again for the scrutiny — genuinely glad I posted this rather than quietly shipping
the wrong claim.

(Housekeeping: the forum’s new-account limit stripped my repo links when I edited the top
post, so for now they’re here as plain text — codeberg.org/vickov/intent-lang for the
Z-machine / intent-language work and codeberg.org/vickov/pfcl for PFCL. I’ll restore them
as proper links once the account is allowed to.)

3 Likes
9

According to 4.2.2 in the standard: " It is illegal to refer to local variables which do not exist for the current routine (there may even be none)"

11

You’re right — §4.2.2 makes a reference to a non-existent local illegal, so the Standard
doesn’t define what such a read returns; it forbids the read. I shouldn’t have called
returning 0 “Standard-correct.” The accurate split: initialising locals to their header
defaults is the §6.4.4 behaviour the Standard prescribes; the out-of-range case is just
illegal, so it never arises in conforming code — my interpreter returns 0 there only as a
defensive fallback so it can’t fault, not because any value is sanctioned. Which is really
the cleaner way to put the whole correction: since §4.2.2 makes the access illegal, a
conforming game can’t lean on it, and that’s exactly why my original “Zork relies on it”
claim couldn’t have been true. Thanks for the precision.

13

Many years ago this FPGA implementation of the Z-Machine was shared. I’ve always thought that was the purest an implementation could be.

14

I think this is pretty amazing. It sounds like there is some historical baggage that can’t be solved and what defines “canon” anyway? What people do want is backwards compatibility and new features. I read about it all the time around here. A functional specification like this that “lowers deterministically to functional code” is the beginning of backwards compatibility and future extensibility. A formal specification like this means that extensions can be added that do not break legacy. Maybe I’m way off but this is still an incredible engineering feat.

1 Like
15

You’ve got it right, and it’s the functional background of both layers that makes it possible.
Intent describes values rather than steps, and PFCL — the substrate it lowers to — identifies
every function by the hash of its body. So extending it (say V5 on top of V3) never touches
what’s already there: new behaviour is new functions sitting beside the old ones, which keep
their exact hashes and behaviour. Backward compatibility comes out structural rather than
something I maintain by hand, and a new feature is purely additive — so you’re not off at all.
That’s exactly the property, and it’s the functional core that buys it.

2 Likes