instruction-encoding.md

VM Bytecode Specification

Instructions are 4 bytes wide: [Opcode: 8] [A: 8] [B: 8] [C: 8].

• Registers are split into per-type banks (int_regs, str_regs, por_regs, bool_regs); an operand indexes the bank implied by the opcode. There is no monetary bank: a monetary is a (str_regs asset, int_regs amount) pair, so the instructions that deal in monetaries take or return the two halves separately.
• 0xFF in a register slot means nil (absent optional operand).
• Bx = a u16 formed by slots B,C (little-endian); used for pool indices and jump targets. sBx is its signed form.
• Most instructions are one word. A few extend into continuation words (shown as ↳ cont.); an instruction's length is fixed by its opcode.
• There is no HALT: programs terminate by design (jumps are forward-only).
• Opcodes are grouped by category with gaps, so new instructions slot into a category without renumbering. Unused values are reserved (users can't emit them, so we stay free to define them later).

Opcode values match the constants in internal/vm/instruction.go; operand layouts match decodeInstr in internal/vm/verify.go.

---

1. State & Assertions

Opcode	Hex	Name	A	B	C	Description
0	0x00	SET_CURRENT_ASSET	asset	-	-	Sets the current asset (used by PULL_ACCOUNT / SEND_TO_ACCOUNT) from str_regs[A]
1	0x01	ASSERT_SAME_ASSET	x	y	-	Traps unless str_regs[A] and str_regs[B] are the same asset
2	0x02	ASSERT_VALID_ACCOUNT	acc	-	-	Traps if the account name in str_regs[A] is malformed
3	0x03	ASSERT_NON_NEGATIVE_BALANCE	amt	acc	-	Traps if int_regs[A] is negative; B = account (for the error)
4	0x04	ASSERT_LEFTOVER	por	exact	-	Traps if por_regs[A] is negative; when B == 1 (no remaining) also traps if non-zero
5	0x05	CHECK_ENOUGH_FUNDS	pulled	target	-	Traps (missing funds) unless int_regs[A] == int_regs[B]: the pulled amount must match the target exactly
6	0x06	ASSERT_VALID_COLOR	color	-	-	Traps if the color in str_regs[A] is malformed (only uppercase letters; the empty string is valid)
7	0x07	ASSERT_NON_NEGATIVE_AMOUNT	amt	-	-	Traps if int_regs[A] (a sent/saved amount) is negative
8	0x08	ASSERT_VALID_SCOPE	scope	-	-	Traps if the scope in str_regs[A] is malformed
9	0x09	ASSERT_NON_NEGATIVE_PORTION	por	-	-	Traps if por_regs[A] (an allotment clause portion) is negative
10	0x0A	ASSERT_UNSCOPED	scope	acc	-	Traps (cannot cast a scoped account to string) if str_regs[A] is not empty; B = account (for the error). Emitted before a scoped account is interpolated into an account name
0x0B..0x0F reserved

2. Constants & Variables

Opcode	Hex	Name	A	B	C	Description
16	0x10	LOAD_INT	dest	Bx (const idx)		int_regs[A] = int_pool[Bx]
17	0x11	LOAD_STR	dest	Bx (const idx)		str_regs[A] = str_pool[Bx]
18	0x12	LOAD_VAR_INT	dest	Bx (var idx)		int_regs[A] = vars.int_pool[Bx]
19	0x13	LOAD_VAR_STR	dest	Bx (var idx)		str_regs[A] = vars.str_pool[Bx]
20	0x14	LOAD_INT_IMMEDIATE	dest	sBx (i16 value)		int_regs[A] = (big.Int)sBx — small literals inline, no pool entry. Reserved; not implemented
21	0x15	CONST_TRUE	dest	-	-	bool_regs[A] = true — the value is in the opcode, so there is nothing to decode and no pool entry
22	0x16	CONST_FALSE	dest	-	-	bool_regs[A] = false
0x17..0x1F reserved

3. Metadata

Opcode	Hex	Name	A	B	C	Description
32	0x20	SET_TX_META	key	val	-	Sets transaction metadata str_regs[A] = str_regs[B]
33	0x21	SET_ACCOUNT_META	acc	key	val	Sets account metadata: account A, key B, value C. 2 words:
​	​	↳ cont.	scope	-	-	Scope reg (0xFF = unscoped)
34	0x22	META_STR	dest	acc	key	str_regs[A] = meta(account B, key C). 2 words:
​	​	↳ cont.	scope	-	-	Scope reg (0xFF = unscoped)
35	0x23	META_INT	dest	acc	key	as META_STR, typed int, same continuation word
36	0x24	META_PORTION	dest	acc	key	as META_STR, typed portion, same continuation word
37	0x25	META_MONETARY	dest asset	acc	key	Parses the value as a monetary. One store read yields both halves, so this is the only two-destination read: str_regs[A] = asset
​	​	↳ cont.	dest amt	scope	-	int_regs[A] = amount; scope reg in B (0xFF = unscoped)
0x26..0x2F reserved

4. Arithmetic & Constructors (binary)

Opcode	Hex	Name	A	B	C	Description
48	0x30	ADD_INT	dest	left	right	int_regs[A] = int_regs[B] + int_regs[C]
49	0x31	SUB_INT	dest	left	right	int_regs[A] = int_regs[B] - int_regs[C]
0x32 reserved (was MIN_INT: a min is a comparison and a copy, so it is LT_INT plus a branch)
51	0x33	SUB_PORTION	dest	left	right	por_regs[A] = por_regs[B] - por_regs[C]. Its counterpart ADD_PORTION is at 0x38, not adjacent, because 0x32 is burned and 0x34..0x37 were taken
52	0x34	MK_PORTION	dest	num	den	por_regs[A] = int_regs[B] / int_regs[C]
0x35 reserved (was MK_MONETARY: a monetary is a register pair, nothing to construct)
54	0x36	ADD_STRING	dest	left	right	str_regs[A] = str_regs[B] + str_regs[C]
0x37 reserved (was STR_EQ: moved to the comparison group, §7, now 0x62)
56	0x38	ADD_PORTION	dest	left	right	por_regs[A] = por_regs[B] + por_regs[C]. A rational sum, so unequal denominators combine correctly and the result is normalised; it may exceed 1
57	0x39	MUL_PORTION	dest	left	right	por_regs[A] = por_regs[B] * por_regs[C]. With PORTION_TO_INT, this is how an allotment share is computed
0x3A..0x3F reserved

5. Unary & Conversions

Opcode	Hex	Name	A	B	C	Description
0x40..0x41 reserved (were GET_AMOUNT / GET_ASSET: projecting a monetary is naming one of its two registers, so it costs no instruction)
66	0x42	INT_COPY	dest	src	-	int_regs[A] = int_regs[B] (fresh copy). One copy per bank, none crossing banks; the family is split across 0x42..0x43 and 0x4A..0x4B because 0x44..0x49 were already spoken for. No monetary copy: a monetary is a (str, int) pair, so copy the halves
67	0x43	PORTION_COPY	dest	src	-	por_regs[A] = por_regs[B] (fresh copy)
68	0x44	NEG_INT	dest	src	-	int_regs[A] = -int_regs[B]
69	0x45	INT_TO_STRING	dest	src	-	str_regs[A] = str(int_regs[B])
70	0x46	PORTION_TO_STRING	dest	src	-	str_regs[A] = str(por_regs[B])
71	0x47	MONETARY_TO_STRING	dest	asset	amt	str_regs[A] = str_regs[B] + " " + str(int_regs[C]) — takes both halves, so it is ternary despite living in this section
0x48 reserved (was IS_ZERO: moved to the comparison group, §7, now 0x63)
0x49 reserved (was NOT: moved to the bool-ops group, §8, now 0x70)
74	0x4A	STR_COPY	dest	src	-	str_regs[A] = str_regs[B]
75	0x4B	BOOL_COPY	dest	src	-	bool_regs[A] = bool_regs[B]
76	0x4C	INT_TO_PORTION	dest	src	-	por_regs[A] = int_regs[B], exact
77	0x4D	PORTION_TO_INT	dest	src	-	int_regs[A] = floor(por_regs[B])
0x4E..0x4F reserved

6. Funds & Postings

Opcode	Hex	Name	A	B	C	Description
80	0x50	PULL_ACCOUNT	dest	acc	cap	Pulls the current asset from account str_regs[B] into the source queue, capped by int_regs[C] (0xFF = uncapped); pulled amount → int_regs[A]. 2 words:
​	​	↳ cont.	overdraft	color	scope	Overdraft bound int_regs[A] (0xFF = unbounded), color str_regs[B] and scope str_regs[C] (0xFF = none). Cap and overdraft both 0xFF traps (unbounded source)
81	0x51	SEND_TO_ACCOUNT	acc	cap	scope	Drains the source queue in the current asset to account str_regs[A], up to int_regs[B] (0xFF = everything queued), scope str_regs[C] (0xFF = unscoped). A = 0xFF is kept: the funds go back to their sources and no posting is emitted. Traps while a mark is open
82	0x52	SAVE	acc	asset	amount	Reduces the balance of account str_regs[A] for asset str_regs[B] by int_regs[C] (C = 0xFF ⇒ save all), floored at 0. Traps while a mark is open. 2 words:
​	​	↳ cont.	scope	-	-	Scope reg (0xFF = unscoped)
0x53 reserved (was MK_ALLOTMENT: an allotment share is built from MUL_PORTION, PORTION_TO_INT and the leftover fixup, so there is no variadic instruction)
84	0x54	BALANCE	dest amt	acc	asset	int_regs[A] = balance(account B, asset C) from the run-state. Only the amount: the resulting monetary's asset is operand C, which the caller already holds. 2 words:
​	​	↳ cont.	scope	-	-	Scope reg (0xFF = unscoped)
85	0x55	MARK_PUSH	-	-	-	Opens a region at the current source-queue depth and posting count, for oneof backtracking. The run-state keeps the stack of open regions; no register is involved
86	0x56	MARK_END	rewind	-	-	Closes the innermost region. A = 1 rewinds it: repays everything pulled and reverses everything posted since the matching MARK_PUSH. A = 0 commits it. Any other value is rejected by the verifier; traps if no region is open. Textual IR: mark_rewind() / mark_commit()
0x57..0x5F reserved (e.g. PULL_ACCOUNT specializations). This block used to run to 0x8F; §7 and §8 took 0x60..0x7F out of it, leaving nine slots for the four specializations sketched in instruction.go

7. Comparisons

Every bool producer lives here. A = dest (a bool_regs index) for all of them; the operand banks are what the opcode implies. IS_ZERO is unary and the rest are binary — they are one group because they are one category, not one arity.

Only < and == exist, per type. The other four surface operators are normalised by the front end:

surface	lowering
a < b	Lt(a, b)
a > b	Lt(b, a) — operands swapped
a <= b	Not(Lt(b, a))
a >= b	Not(Lt(a, b))
a == b	Eq(a, b)
a != b	Not(Eq(a, b))

12 surface operators, 5 opcodes. Every extra predicate is another case in the SMT encoder and in any formal model of the VM, so the cost would be paid three times over. LLVM does the same, canonicalising sgt to slt with swapped operands in InstCombine so downstream passes only ever see one form.

Opcode	Hex	Name	A	B	C	Description
96	0x60	LT_INT	dest	left	right	bool_regs[A] = int_regs[B] < int_regs[C]. Strict
97	0x61	EQ_INT	dest	left	right	bool_regs[A] = int_regs[B] == int_regs[C]
98	0x62	STR_EQ	dest	left	right	bool_regs[A] = str_regs[B] == str_regs[C]. The only string comparison that yields a value rather than trapping (cf. ASSERT_SAME_ASSET). Was 0x37
99	0x63	IS_ZERO	dest	src	-	bool_regs[A] = int_regs[B].Sign() == 0 — the projection from a quantity to a condition, since the jumps take a bool. Tests the sign, so a negative amount is not zero. Kept alongside EQ_INT because it needs no materialised zero and it is on every quantity branch. Was 0x48
100	0x64	LT_PORTION	dest	left	right	bool_regs[A] = por_regs[B] < por_regs[C]. Strict, and by value — see EQ_PORTION
101	0x65	EQ_PORTION	dest	left	right	bool_regs[A] = por_regs[B] == por_regs[C]. Value equality: 1/2 == 2/4 is true. big.Rat normalises on construction, so the rationals are compared — comparing numerator/denominator pairs separately would give the wrong answer
0x66..0x6F reserved for < and == on types that don't exist yet. Str gets equality only, never ordering. Bool equality, and structural comparison of tuples/arrays, are front-end expansions rather than opcodes. No named-but-unimplemented constants live here on purpose: a live opcode with no emitter invites a second lowering path that no test exercises

8. Bool ops

Opcode	Hex	Name	A	B	C	Description
112	0x70	NOT	dest	src	-	bool_regs[A] = !bool_regs[B] — the only operation whose operand and result are both bools, and what the four derived operators above are built from. Was 0x49
0x71..0x7F reserved for and/or, if they ever pay for themselves — both are expressible as branches, so neither is needed for completeness
0x80..0x8F reserved

9. Control Flow

Opcode	Hex	Name	A	B	C	Description
144	0x90	JMP_IF_FALSE	cond	Bx (forward delta)		If bool_regs[A] is false, skip Bx instructions: pc += Bx, where pc already points at the next instruction. Being an unsigned delta, the jump is forward-only (guarantees termination). A quantity is not a condition — project it with IS_ZERO first
145	0x91	JMP	—	Bx (forward delta)		Unconditional: pc += Bx. Forward-only, as above
146	0x92	JMP_IF_TRUE	cond	Bx (forward delta)		The dual of JMP_IF_FALSE, so either edge of a condition is one instruction and no negation opcode is needed
0x93..0xFF reserved