From b89afbfa5b780583a02345c3624cd69d36d54af0 Mon Sep 17 00:00:00 2001
From: ascandone <alescandone@gmail.com>
Date: Tue, 14 Jul 2026 17:11:41 +0200
Subject: [PATCH 1/9] feat: bytecode verifier + dynamic register banks
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Verify a program once before execution: valid opcodes, multi-word ext
words present, const-pool indices in range, jump targets forward and on
instruction boundaries. The verifier also derives the exact per-bank
register counts, so the VM allocates register banks sized to the program
(was a fixed [256] per bank) — Vm struct drops from ~41KB to 232 bytes.
Because every access is now proven in-bounds, the execution loop needs no
bounds checks.

Claude-Session: https://claude.ai/code/session_01RGLaD2WtQXbpCMyFEZky3Z
---
 internal/vm/execution_err.go |  12 ++
 internal/vm/verify.go        | 286 +++++++++++++++++++++++++++++++++++
 internal/vm/verify_test.go   |  62 ++++++++
 internal/vm/vm.go            |  45 +++---
 internal/vm/vm_test.go       |   4 +
 5 files changed, 391 insertions(+), 18 deletions(-)
 create mode 100644 internal/vm/verify.go
 create mode 100644 internal/vm/verify_test.go

diff --git a/internal/vm/execution_err.go b/internal/vm/execution_err.go
index 35c20327..85afe71e 100644
--- a/internal/vm/execution_err.go
+++ b/internal/vm/execution_err.go
@@ -68,6 +68,12 @@ type (
 	StoreError struct {
 		Wrapped error
 	}
+
+	// MalformedProgramError is returned when the pre-execution verifier rejects a
+	// program (out-of-range operand, truncated instruction, bad jump, ...).
+	MalformedProgramError struct {
+		Reason string
+	}
 )
 
 func (e MissingFundsError) Error() string {
@@ -86,6 +92,10 @@ func (e InternalError) Error() string {
 	return fmt.Sprintf("internal error: unknown opcode %d", e.Opcode)
 }
 
+func (e MalformedProgramError) Error() string {
+	return "malformed program: " + e.Reason
+}
+
 func (e DivideByZeroError) Error() string {
 	return fmt.Sprintf("cannot divide by zero (in %s/0)", e.Numerator.String())
 }
@@ -124,6 +134,7 @@ func (NegativeBalanceError) execErr()  {}
 func (DivideByZeroError) execErr()     {}
 func (InternalError) execErr()         {}
 func (StoreError) execErr()            {}
+func (MalformedProgramError) execErr() {}
 
 var (
 	_ ExecutionError = (*MissingFundsError)(nil)
@@ -137,4 +148,5 @@ var (
 	_ ExecutionError = (*DivideByZeroError)(nil)
 	_ ExecutionError = (*InternalError)(nil)
 	_ ExecutionError = (*StoreError)(nil)
+	_ ExecutionError = (*MalformedProgramError)(nil)
 )
diff --git a/internal/vm/verify.go b/internal/vm/verify.go
new file mode 100644
index 00000000..788b2d4a
--- /dev/null
+++ b/internal/vm/verify.go
@@ -0,0 +1,286 @@
+package vm
+
+import "fmt"
+
+type regBank int
+
+const (
+	bankInt regBank = iota
+	bankStr
+	bankPortion
+	bankMonetary
+)
+
+type regRef struct {
+	bank  regBank
+	index int
+}
+
+// decoded describes the register/pool/jump operands an instruction touches, so
+// the verifier can size register banks and check every access without the VM
+// having to guard anything at run time.
+type decoded struct {
+	reads      []regRef
+	writes     []regRef
+	constInt   int // index into program IntsPool, or -1
+	constStr   int
+	varInt     int // index into vars IntsPool, or -1
+	varStr     int
+	jumpTarget int // instruction index, or -1
+}
+
+type regCounts struct {
+	ints, strings, portions, monetaries int
+}
+
+type programInfo struct {
+	regs       regCounts
+	varIntsLen int
+	varStrsLen int
+}
+
+func instrWords(op byte) int {
+	switch Opcode(op) {
+	case Op_PullAccount, Op_MkAllotment:
+		return 2
+	default:
+		return 1
+	}
+}
+
+// verify statically checks a program cannot make the VM read out of bounds and
+// returns the exact register-bank sizes it needs. A verified program can be run
+// with no bounds checks in the execution loop.
+func verify(p Program) (programInfo, error) {
+	instrs := p.Instructions
+	n := len(instrs)
+
+	boundary := make([]bool, n+1)
+	boundary[n] = true // jumping past the last instruction halts, which is fine
+
+	type step struct {
+		at int
+		d  decoded
+	}
+	var steps []step
+
+	for i := 0; i < n; {
+		op := instrs[i].Opcode
+		w := instrWords(op)
+		if i+w > n {
+			return programInfo{}, fmt.Errorf("truncated instruction at %d: opcode %d needs %d words", i, op, w)
+		}
+		var ext Instruction
+		if w == 2 {
+			ext = instrs[i+1]
+		}
+		d, err := decodeInstr(instrs[i], ext)
+		if err != nil {
+			return programInfo{}, fmt.Errorf("at instruction %d: %w", i, err)
+		}
+		boundary[i] = true
+		steps = append(steps, step{i, d})
+		i += w
+	}
+
+	info := programInfo{}
+	grow := func(r regRef) {
+		s := r.index + 1
+		switch r.bank {
+		case bankInt:
+			if s > info.regs.ints {
+				info.regs.ints = s
+			}
+		case bankStr:
+			if s > info.regs.strings {
+				info.regs.strings = s
+			}
+		case bankPortion:
+			if s > info.regs.portions {
+				info.regs.portions = s
+			}
+		case bankMonetary:
+			if s > info.regs.monetaries {
+				info.regs.monetaries = s
+			}
+		}
+	}
+
+	for _, st := range steps {
+		d := st.d
+		for _, r := range d.reads {
+			grow(r)
+		}
+		for _, r := range d.writes {
+			grow(r)
+		}
+		if d.constInt >= 0 {
+			if d.constInt >= len(p.IntsPool) {
+				return programInfo{}, fmt.Errorf("at instruction %d: int constant %d out of range (pool size %d)", st.at, d.constInt, len(p.IntsPool))
+			}
+		}
+		if d.constStr >= 0 {
+			if d.constStr >= len(p.StringsPool) {
+				return programInfo{}, fmt.Errorf("at instruction %d: string constant %d out of range (pool size %d)", st.at, d.constStr, len(p.StringsPool))
+			}
+		}
+		if d.varInt >= 0 && d.varInt+1 > info.varIntsLen {
+			info.varIntsLen = d.varInt + 1
+		}
+		if d.varStr >= 0 && d.varStr+1 > info.varStrsLen {
+			info.varStrsLen = d.varStr + 1
+		}
+		if d.jumpTarget >= 0 {
+			t := d.jumpTarget
+			if t <= st.at {
+				return programInfo{}, fmt.Errorf("at instruction %d: backward jump to %d", st.at, t)
+			}
+			if t > n || !boundary[t] {
+				return programInfo{}, fmt.Errorf("at instruction %d: jump to %d is not an instruction boundary", st.at, t)
+			}
+		}
+	}
+
+	return info, nil
+}
+
+func decodeInstr(instr, ext Instruction) (decoded, error) {
+	d := decoded{constInt: -1, constStr: -1, varInt: -1, varStr: -1, jumpTarget: -1}
+	read := func(bank regBank, idx byte) { d.reads = append(d.reads, regRef{bank, int(idx)}) }
+	write := func(bank regBank, idx byte) { d.writes = append(d.writes, regRef{bank, int(idx)}) }
+	readOpt := func(bank regBank, idx byte) {
+		if idx != nilReg {
+			d.reads = append(d.reads, regRef{bank, int(idx)})
+		}
+	}
+
+	switch Opcode(instr.Opcode) {
+	case Op_PullAccount:
+		read(bankStr, instr.B)
+		readOpt(bankInt, instr.C)
+		readOpt(bankInt, ext.A)
+		readOpt(bankStr, ext.B)
+		write(bankInt, instr.A)
+	case Op_SendToAccount:
+		readOpt(bankStr, instr.A)
+		readOpt(bankInt, instr.B)
+		readOpt(bankStr, instr.C)
+	case Op_MkAllotment:
+		for j := int(instr.A); j < int(instr.A)+int(instr.C); j++ {
+			d.writes = append(d.writes, regRef{bankInt, j})
+		}
+		for j := int(instr.B); j < int(instr.B)+int(instr.C); j++ {
+			d.reads = append(d.reads, regRef{bankPortion, j})
+		}
+		read(bankInt, ext.A)
+	case Op_CheckEnoughFunds:
+		read(bankInt, instr.A)
+		read(bankInt, instr.B)
+	case Op_Save:
+		read(bankStr, instr.A)
+		read(bankStr, instr.B)
+		readOpt(bankInt, instr.C)
+	case Op_AssertLeftover:
+		read(bankPortion, instr.A)
+	case Op_SetCurrentAsset:
+		read(bankStr, instr.A)
+	case Op_AssertSameAsset:
+		read(bankStr, instr.A)
+		read(bankStr, instr.B)
+	case Op_AssertValidAccount:
+		read(bankStr, instr.A)
+	case Op_AssertNonNegativeBalance:
+		read(bankMonetary, instr.A)
+		read(bankStr, instr.B)
+	case Op_SetTxMeta:
+		read(bankStr, instr.A)
+		read(bankStr, instr.B)
+	case Op_SetAccountMeta:
+		read(bankStr, instr.A)
+		read(bankStr, instr.B)
+		read(bankStr, instr.C)
+	case Op_MetaStr:
+		read(bankStr, instr.B)
+		read(bankStr, instr.C)
+		write(bankStr, instr.A)
+	case Op_MetaInt:
+		read(bankStr, instr.B)
+		read(bankStr, instr.C)
+		write(bankInt, instr.A)
+	case Op_MetaPortion:
+		read(bankStr, instr.B)
+		read(bankStr, instr.C)
+		write(bankPortion, instr.A)
+	case Op_MetaMonetary:
+		read(bankStr, instr.B)
+		read(bankStr, instr.C)
+		write(bankMonetary, instr.A)
+	case Op_LoadVarInt:
+		d.varInt = int(instr.GetBC())
+		write(bankInt, instr.A)
+	case Op_LoadVarStr:
+		d.varStr = int(instr.GetBC())
+		write(bankStr, instr.A)
+	case Op_LoadInt:
+		d.constInt = int(instr.GetBC())
+		write(bankInt, instr.A)
+	case Op_LoadStr:
+		d.constStr = int(instr.GetBC())
+		write(bankStr, instr.A)
+	case Op_JmpIfZero:
+		read(bankInt, instr.A)
+		d.jumpTarget = int(instr.GetBC())
+	case Op_MinInt, Op_AddInt, Op_SubInt:
+		read(bankInt, instr.B)
+		read(bankInt, instr.C)
+		write(bankInt, instr.A)
+	case Op_AddString:
+		read(bankStr, instr.B)
+		read(bankStr, instr.C)
+		write(bankStr, instr.A)
+	case Op_SubPortion:
+		read(bankPortion, instr.B)
+		read(bankPortion, instr.C)
+		write(bankPortion, instr.A)
+	case Op_MkPortion:
+		read(bankInt, instr.B)
+		read(bankInt, instr.C)
+		write(bankPortion, instr.A)
+	case Op_MkMonetary:
+		read(bankStr, instr.B)
+		read(bankInt, instr.C)
+		write(bankMonetary, instr.A)
+	case Op_Balance:
+		read(bankStr, instr.B)
+		read(bankStr, instr.C)
+		write(bankMonetary, instr.A)
+	case Op_IntCopy:
+		read(bankInt, instr.B)
+		write(bankInt, instr.A)
+	case Op_PortionCopy:
+		read(bankPortion, instr.B)
+		write(bankPortion, instr.A)
+	case Op_GetAsset:
+		read(bankMonetary, instr.B)
+		write(bankStr, instr.A)
+	case Op_GetAmount:
+		read(bankMonetary, instr.B)
+		write(bankInt, instr.A)
+	case Op_NegInt:
+		read(bankInt, instr.B)
+		write(bankInt, instr.A)
+	case Op_IntToString:
+		read(bankInt, instr.B)
+		write(bankStr, instr.A)
+	case Op_PortionToString:
+		read(bankPortion, instr.B)
+		write(bankStr, instr.A)
+	case Op_MonetaryToString:
+		read(bankMonetary, instr.B)
+		write(bankStr, instr.A)
+	default:
+		return decoded{}, fmt.Errorf("unknown opcode %d", instr.Opcode)
+	}
+
+	return d, nil
+}
diff --git a/internal/vm/verify_test.go b/internal/vm/verify_test.go
new file mode 100644
index 00000000..c21ce502
--- /dev/null
+++ b/internal/vm/verify_test.go
@@ -0,0 +1,62 @@
+package vm
+
+import (
+	"math/big"
+	"testing"
+)
+
+func mustReject(t *testing.T, p Program) {
+	t.Helper()
+	_, err := Exec(NewVm(p), nil, mockStore{})
+	if _, ok := err.(MalformedProgramError); !ok {
+		t.Fatalf("expected MalformedProgramError, got %v", err)
+	}
+}
+
+func TestVerify_UnknownOpcode(t *testing.T) {
+	mustReject(t, Program{Instructions: []Instruction{abc(0xFE, 0, 0, 0)}})
+}
+
+func TestVerify_TruncatedMultiWord(t *testing.T) {
+	// a lone Op_PullAccount with no trailing ext word
+	mustReject(t, Program{Instructions: []Instruction{abc(Op_PullAccount, 0, 0, nilReg)}})
+}
+
+func TestVerify_ConstIndexOutOfRange(t *testing.T) {
+	// LoadInt referring to pool index 3 in an empty pool
+	mustReject(t, Program{Instructions: []Instruction{bc(Op_LoadInt, 0, 3)}})
+}
+
+func TestVerify_BackwardJump(t *testing.T) {
+	mustReject(t, Program{Instructions: []Instruction{
+		bc(Op_LoadInt, 0, 0),
+		bc(Op_JmpIfZero, 0, 0), // targets instruction 0 (backward)
+	}, IntsPool: []big.Int{*big.NewInt(0)}})
+}
+
+func TestVerify_JumpOutOfRange(t *testing.T) {
+	mustReject(t, Program{Instructions: []Instruction{
+		bc(Op_LoadInt, 0, 0),
+		bc(Op_JmpIfZero, 0, 99),
+	}, IntsPool: []big.Int{*big.NewInt(0)}})
+}
+
+func TestVerify_MissingVars(t *testing.T) {
+	// reads var int 0 but no vars are passed
+	_, err := Exec(NewVm(Program{Instructions: []Instruction{bc(Op_LoadVarInt, 0, 0)}}), nil, mockStore{})
+	if _, ok := err.(MalformedProgramError); !ok {
+		t.Fatalf("expected MalformedProgramError, got %v", err)
+	}
+}
+
+func TestVerify_SizesBanksToNeed(t *testing.T) {
+	// a program using int reg 5 must get an int bank of at least 6
+	p := Program{Instructions: []Instruction{bc(Op_LoadInt, 5, 0)}, IntsPool: []big.Int{*big.NewInt(1)}}
+	vm := NewVm(p)
+	if _, err := Exec(vm, nil, mockStore{}); err != nil {
+		t.Fatalf("unexpected error: %v", err)
+	}
+	if len(vm.intsRegs) != 6 {
+		t.Fatalf("int bank size = %d, want 6", len(vm.intsRegs))
+	}
+}
diff --git a/internal/vm/vm.go b/internal/vm/vm.go
index efafa4c2..809459d7 100644
--- a/internal/vm/vm.go
+++ b/internal/vm/vm.go
@@ -17,12 +17,14 @@ const worldAccount = "world"
 
 type Vm struct {
 	program  Program
+	verified bool
+	info     programInfo
 	runstate *runtime.RunState
 
-	stringsRegs    [256]string // asset,string,account
-	intsRegs       [256]big.Int
-	portionsRegs   [256]big.Rat
-	monetariesRegs [256]monetary
+	stringsRegs    []string // asset,string,account
+	intsRegs       []big.Int
+	portionsRegs   []big.Rat
+	monetariesRegs []monetary
 }
 
 func NewVm(
@@ -81,6 +83,25 @@ func Exec[S Store](
 	runtimeStore := runtimeStoreAdapter{store: store}
 	// RunState fetches balances lazily through this store; a fetch error surfaces
 	// from the RunState call that triggered it, wrapped in StoreError below.
+	if !vm.verified {
+		info, err := verify(vm.program)
+		if err != nil {
+			return runtime.ExecutionResult{}, MalformedProgramError{Reason: err.Error()}
+		}
+		vm.info = info
+		vm.intsRegs = make([]big.Int, info.regs.ints)
+		vm.stringsRegs = make([]string, info.regs.strings)
+		vm.portionsRegs = make([]big.Rat, info.regs.portions)
+		vm.monetariesRegs = make([]monetary, info.regs.monetaries)
+		vm.verified = true
+	}
+
+	if vm.info.varIntsLen > 0 || vm.info.varStrsLen > 0 {
+		if vars == nil || len(vars.IntsPool) < vm.info.varIntsLen || len(vars.StringsPool) < vm.info.varStrsLen {
+			return runtime.ExecutionResult{}, MalformedProgramError{Reason: "program reads more variables than were provided"}
+		}
+	}
+
 	if vm.runstate == nil {
 		vm.runstate = runtime.New(runtimeStore)
 	} else {
@@ -114,9 +135,6 @@ func Exec[S Store](
 		switch Opcode(instr.Opcode) {
 		// --- Domain-specific ops
 		case Op_PullAccount:
-			// TODO crashes if this is the last instruction (the ext word is
-			// missing): instrs[pc] reads past the end. e.g. a program ending in a
-			// lone Op_PullAccount word.
 			instrExt := instrs[pc]
 			pc++
 
@@ -179,15 +197,11 @@ func Exec[S Store](
 			}
 
 		case Op_MkAllotment:
-			// TODO crashes if this is the last instruction (missing ext word),
-			// same as Op_PullAccount.
 			instrExt := instrs[pc]
 			pc++
 
-			// TODO crashes when instr.A+instr.C > 256: the slice runs past the
-			// register bank. Both are bytes, so A+C can be up to 510.
-			destArrStartReg := intsRegs[instr.A : instr.A+instr.C]
-			inpArrStartReg := portionsRegs[instr.B : instr.B+instr.C]
+			destArrStartReg := intsRegs[instr.A : int(instr.A)+int(instr.C)]
+			inpArrStartReg := portionsRegs[instr.B : int(instr.B)+int(instr.C)]
 
 			amt := &intsRegs[instrExt.A]
 
@@ -320,9 +334,6 @@ func Exec[S Store](
 			dest.amount.Set(amount)
 
 			// --- Vars
-			// TODO both crash if vars is nil (Exec called with no vars for a
-			// program that reads them), or if GetBC() >= len(vars pool) (caller
-			// passed fewer vars than the program declares).
 		case Op_LoadVarInt:
 			intsRegs[instr.A].Set(&vars.IntsPool[instr.GetBC()])
 
@@ -337,8 +348,6 @@ func Exec[S Store](
 			}
 
 		// --- consts
-		// TODO both crash if GetBC() >= len(pool), e.g. an Op_LoadInt referring to
-		// pool index 5 in a program whose ints pool has 3 entries.
 		case Op_LoadInt:
 			const_ := &intsPool[instr.GetBC()]
 			intsRegs[instr.A].Set(const_)
diff --git a/internal/vm/vm_test.go b/internal/vm/vm_test.go
index bf593269..bf57a505 100644
--- a/internal/vm/vm_test.go
+++ b/internal/vm/vm_test.go
@@ -181,6 +181,10 @@ func TestUnknownOpcode(t *testing.T) {
 	_, err := Exec(context.Background(), NewVm(prog), nil, mockStore{})
 	if _, ok := err.(InternalError); !ok {
 		t.Fatalf("expected InternalError, got %v", err)
+		_, err := Exec(NewVm(prog), nil, mockStore{})
+		if _, ok := err.(MalformedProgramError); !ok {
+			t.Fatalf("expected MalformedProgramError, got %v", err)
+		}
 	}
 }
 

From 3b38c43a7d93ce12e17bcf204209e3881c45dba1 Mon Sep 17 00:00:00 2001
From: ascandone <alescandone@gmail.com>
Date: Tue, 14 Jul 2026 17:14:26 +0200
Subject: [PATCH 2/9] feat: verify definite assignment of registers
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Extend the verifier with a definite-assignment dataflow: a register (or
the current asset, modelled as a pseudo-register) may only be read if it
was written on every path reaching that instruction. This makes reuse of
a warm Vm safe — a read can never observe a stale value from a previous
run — and rejects reads of never-written registers.

Claude-Session: https://claude.ai/code/session_01RGLaD2WtQXbpCMyFEZky3Z
---
 internal/vm/verify.go      | 66 ++++++++++++++++++++++++++++++++++++++
 internal/vm/verify_test.go | 19 +++++++++++
 2 files changed, 85 insertions(+)

diff --git a/internal/vm/verify.go b/internal/vm/verify.go
index 788b2d4a..80e0d5d6 100644
--- a/internal/vm/verify.go
+++ b/internal/vm/verify.go
@@ -9,8 +9,13 @@ const (
 	bankStr
 	bankPortion
 	bankMonetary
+	// bankCurrentAsset is a pseudo-bank with a single slot, tracking whether the
+	// current asset has been set. It is never allocated as a register.
+	bankCurrentAsset
 )
 
+var currentAssetRef = regRef{bankCurrentAsset, 0}
+
 type regRef struct {
 	bank  regBank
 	index int
@@ -141,9 +146,67 @@ func verify(p Program) (programInfo, error) {
 		}
 	}
 
+	// definite assignment: a register (or the current asset) may only be read if
+	// it was written on every path reaching that instruction. Jumps are forward
+	// (checked above), so every predecessor is earlier and one ordered pass over
+	// the intersection of predecessors' written-sets suffices.
+	at2idx := make(map[int]int, len(steps))
+	for k, st := range steps {
+		at2idx[st.at] = k
+	}
+	preds := make([][]int, len(steps))
+	for k, st := range steps {
+		if j, ok := at2idx[st.at+instrWords(instrs[st.at].Opcode)]; ok {
+			preds[j] = append(preds[j], k)
+		}
+		if st.d.jumpTarget >= 0 {
+			if j, ok := at2idx[st.d.jumpTarget]; ok {
+				preds[j] = append(preds[j], k)
+			}
+		}
+	}
+	assignedOut := make([]map[regRef]bool, len(steps))
+	for k, st := range steps {
+		in := intersectAssigned(assignedOut, preds[k])
+		for _, r := range st.d.reads {
+			if !in[r] {
+				return programInfo{}, fmt.Errorf("at instruction %d: %s read before being assigned on all paths", st.at, describeRef(r))
+			}
+		}
+		for _, r := range st.d.writes {
+			in[r] = true
+		}
+		assignedOut[k] = in
+	}
+
 	return info, nil
 }
 
+func intersectAssigned(out []map[regRef]bool, preds []int) map[regRef]bool {
+	res := map[regRef]bool{}
+	if len(preds) == 0 {
+		return res
+	}
+	for r := range out[preds[0]] {
+		res[r] = true
+	}
+	for _, p := range preds[1:] {
+		for r := range res {
+			if !out[p][r] {
+				delete(res, r)
+			}
+		}
+	}
+	return res
+}
+
+func describeRef(r regRef) string {
+	if r.bank == bankCurrentAsset {
+		return "current asset"
+	}
+	return fmt.Sprintf("register (bank %d, index %d)", r.bank, r.index)
+}
+
 func decodeInstr(instr, ext Instruction) (decoded, error) {
 	d := decoded{constInt: -1, constStr: -1, varInt: -1, varStr: -1, jumpTarget: -1}
 	read := func(bank regBank, idx byte) { d.reads = append(d.reads, regRef{bank, int(idx)}) }
@@ -160,11 +223,13 @@ func decodeInstr(instr, ext Instruction) (decoded, error) {
 		readOpt(bankInt, instr.C)
 		readOpt(bankInt, ext.A)
 		readOpt(bankStr, ext.B)
+		d.reads = append(d.reads, currentAssetRef)
 		write(bankInt, instr.A)
 	case Op_SendToAccount:
 		readOpt(bankStr, instr.A)
 		readOpt(bankInt, instr.B)
 		readOpt(bankStr, instr.C)
+		d.reads = append(d.reads, currentAssetRef)
 	case Op_MkAllotment:
 		for j := int(instr.A); j < int(instr.A)+int(instr.C); j++ {
 			d.writes = append(d.writes, regRef{bankInt, j})
@@ -184,6 +249,7 @@ func decodeInstr(instr, ext Instruction) (decoded, error) {
 		read(bankPortion, instr.A)
 	case Op_SetCurrentAsset:
 		read(bankStr, instr.A)
+		d.writes = append(d.writes, currentAssetRef)
 	case Op_AssertSameAsset:
 		read(bankStr, instr.A)
 		read(bankStr, instr.B)
diff --git a/internal/vm/verify_test.go b/internal/vm/verify_test.go
index c21ce502..36036bfb 100644
--- a/internal/vm/verify_test.go
+++ b/internal/vm/verify_test.go
@@ -49,6 +49,25 @@ func TestVerify_MissingVars(t *testing.T) {
 	}
 }
 
+func TestVerify_ReadNotAssignedOnAllPaths(t *testing.T) {
+	// r1 is written only on the fall-through path; the jump skips to instr 3
+	// which reads it, so it is not assigned on every path.
+	mustReject(t, Program{Instructions: []Instruction{
+		bc(Op_LoadInt, 0, 0),         // 0: r0 = 0
+		bc(Op_JmpIfZero, 0, 3),       // 1: if r0==0 skip to 3
+		bc(Op_LoadInt, 1, 0),         // 2: r1 = 0 (skipped when jumping)
+		abc(Op_NegInt, 2, 1, nilReg), // 3: r2 = -r1  (r1 maybe unassigned)
+	}, IntsPool: []big.Int{*big.NewInt(0)}})
+}
+
+func TestVerify_CurrentAssetNotSet(t *testing.T) {
+	// a send before any set_current_asset
+	mustReject(t, Program{Instructions: []Instruction{
+		bc(Op_LoadStr, 0, 0), // r0 = "dest"
+		abc(Op_SendToAccount, 0, nilReg, nilReg),
+	}, StringsPool: []string{"dest"}})
+}
+
 func TestVerify_SizesBanksToNeed(t *testing.T) {
 	// a program using int reg 5 must get an int bank of at least 6
 	p := Program{Instructions: []Instruction{bc(Op_LoadInt, 5, 0)}, IntsPool: []big.Int{*big.NewInt(1)}}

From e32e101cae90fbf761bd05bed885ed4c58c57693 Mon Sep 17 00:00:00 2001
From: ascandone <alescandone@gmail.com>
Date: Tue, 14 Jul 2026 17:17:33 +0200
Subject: [PATCH 3/9] test: fuzz Exec to prove it never panics

Feeds arbitrary bytes as an instruction stream; the verifier must reject
malformed programs and execution must always return a result or error,
never crash. ~5M executions found no panic.

Claude-Session: https://claude.ai/code/session_01RGLaD2WtQXbpCMyFEZky3Z
---
 internal/vm/fuzz_test.go | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100644 internal/vm/fuzz_test.go

diff --git a/internal/vm/fuzz_test.go b/internal/vm/fuzz_test.go
new file mode 100644
index 00000000..77119ebf
--- /dev/null
+++ b/internal/vm/fuzz_test.go
@@ -0,0 +1,36 @@
+package vm
+
+import (
+	"math/big"
+	"testing"
+)
+
+// FuzzExec feeds arbitrary bytes as an instruction stream and asserts the VM
+// never panics: the verifier must reject a malformed program, or execution must
+// return a result/error. It never crashes the host.
+func FuzzExec(f *testing.F) {
+	f.Add([]byte{})
+	f.Add([]byte{byte(Op_LoadInt), 0, 0, 0})
+	f.Add([]byte{byte(Op_PullAccount), 0, 0, 0xFF})
+
+	pool := Program{
+		IntsPool:    []big.Int{*big.NewInt(0), *big.NewInt(7)},
+		StringsPool: []string{"world", "dest"},
+	}
+
+	f.Fuzz(func(t *testing.T, data []byte) {
+		instrs := make([]Instruction, len(data)/4)
+		for i := range instrs {
+			off := i * 4
+			instrs[i] = Instruction{data[off], data[off+1], data[off+2], data[off+3]}
+		}
+		prog := Program{Instructions: instrs, IntsPool: pool.IntsPool, StringsPool: pool.StringsPool}
+
+		defer func() {
+			if r := recover(); r != nil {
+				t.Fatalf("Exec panicked: %v", r)
+			}
+		}()
+		_, _ = Exec(NewVm(prog), nil, mockStore{})
+	})
+}

From af50fc143aef199f06a2a52180cd1b62050554a4 Mon Sep 17 00:00:00 2001
From: ascandone <alescandone@gmail.com>
Date: Tue, 14 Jul 2026 17:27:02 +0200
Subject: [PATCH 4/9] test: certify compiler output and fuzz mutated bytecode

- Export vm.Verify so bytecode can be sanity-checked directly.
- TestCompiledCorpusPassesVerify: every compiled spec passes verify
  (property: the compiler only emits code the VM accepts).
- FuzzMutatedBytecode: mutate valid bytecode; if the mutant still passes
  verify, executing it must not crash (property: verified => no crash,
  exercised with near-valid inputs).

Claude-Session: https://claude.ai/code/session_01RGLaD2WtQXbpCMyFEZky3Z
---
 internal/compiler/fuzz_mutate_test.go   | 77 +++++++++++++++++++++++++
 internal/compiler/verify_corpus_test.go | 36 ++++++++++++
 internal/vm/verify.go                   |  7 +++
 3 files changed, 120 insertions(+)
 create mode 100644 internal/compiler/fuzz_mutate_test.go
 create mode 100644 internal/compiler/verify_corpus_test.go

diff --git a/internal/compiler/fuzz_mutate_test.go b/internal/compiler/fuzz_mutate_test.go
new file mode 100644
index 00000000..7b07e271
--- /dev/null
+++ b/internal/compiler/fuzz_mutate_test.go
@@ -0,0 +1,77 @@
+package compiler_test
+
+import (
+	"math/big"
+	"testing"
+
+	"github.com/formancehq/numscript/internal/compiler"
+	"github.com/formancehq/numscript/internal/parser"
+	"github.com/formancehq/numscript/internal/runtime"
+	"github.com/formancehq/numscript/internal/vm"
+)
+
+// a script exercising most opcodes: inorder+max source (jump, min_int),
+// allotment destination (mk_portion, sub_portion, mk_allotment), and no vars.
+const mutateBaseSrc = `send [USD/2 10] (
+	source = {
+		max [USD/2 5] from @a
+		@b
+	}
+	destination = {
+		1/2 to @c
+		remaining to @d
+	}
+)`
+
+// Properties 1 & 3: take valid compiled bytecode, mutate it, and if the mutant
+// still passes the verifier, executing it must never crash.
+func FuzzMutatedBytecode(f *testing.F) {
+	parsed := parser.Parse(mutateBaseSrc)
+	if len(parsed.Errors) != 0 {
+		f.Fatalf("parse: %v", parsed.Errors)
+	}
+	_, base, cErr := compiler.Compile(parsed.Value)
+	if cErr != nil {
+		f.Fatalf("compile: %v", cErr)
+	}
+
+	store := e2eStore{balances: map[runtime.PairKey]*big.Int{
+		{Account: "a", Asset: "USD/2", Color: ""}: big.NewInt(3),
+		{Account: "b", Asset: "USD/2", Color: ""}: big.NewInt(100),
+	}}
+
+	f.Add([]byte{0, 0})
+	f.Add([]byte{4, 255})
+	f.Add([]byte{1, 9, 8, 2, 12, 0})
+
+	f.Fuzz(func(t *testing.T, data []byte) {
+		instrs := make([]vm.Instruction, len(base.Instructions))
+		copy(instrs, base.Instructions)
+		if len(instrs) == 0 {
+			return
+		}
+
+		flat := make([]byte, len(instrs)*4)
+		for k, ins := range instrs {
+			flat[k*4], flat[k*4+1], flat[k*4+2], flat[k*4+3] = ins.Opcode, ins.A, ins.B, ins.C
+		}
+		for i := 0; i+1 < len(data); i += 2 {
+			flat[int(data[i])%len(flat)] = data[i+1]
+		}
+		for k := range instrs {
+			instrs[k] = vm.Instruction{Opcode: flat[k*4], A: flat[k*4+1], B: flat[k*4+2], C: flat[k*4+3]}
+		}
+
+		prog := vm.Program{Instructions: instrs, StringsPool: base.StringsPool, IntsPool: base.IntsPool}
+		if vm.Verify(prog) != nil {
+			return // mutation broke the sanity checks: nothing more to prove
+		}
+
+		defer func() {
+			if r := recover(); r != nil {
+				t.Fatalf("verified program panicked on Exec: %v", r)
+			}
+		}()
+		_, _ = vm.Exec(vm.NewVm(prog), nil, store)
+	})
+}
diff --git a/internal/compiler/verify_corpus_test.go b/internal/compiler/verify_corpus_test.go
new file mode 100644
index 00000000..e0bced25
--- /dev/null
+++ b/internal/compiler/verify_corpus_test.go
@@ -0,0 +1,36 @@
+package compiler_test
+
+import (
+	"path/filepath"
+	"slices"
+	"testing"
+
+	"github.com/formancehq/numscript/internal/compiler"
+	"github.com/formancehq/numscript/internal/parser"
+	"github.com/formancehq/numscript/internal/specs_format"
+	"github.com/formancehq/numscript/internal/vm"
+
+	"github.com/stretchr/testify/require"
+)
+
+// Property 2: every program our compiler emits passes the VM's sanity checks.
+func TestCompiledCorpusPassesVerify(t *testing.T) {
+	rawSpecs, err := specs_format.ReadSpecsFiles([]string{scriptsFolder})
+	require.NoError(t, err)
+
+	for _, rawSpec := range rawSpecs {
+		rel, err := filepath.Rel(scriptsFolder, rawSpec.NumscriptPath)
+		require.NoError(t, err)
+
+		t.Run(rel, func(t *testing.T) {
+			if slices.Contains(scriptsBlacklist, rel) {
+				t.Skip("blacklisted: not supported yet")
+			}
+			parsed := parser.Parse(string(rawSpec.NumscriptContent))
+			require.Empty(t, parsed.Errors)
+			_, program, cErr := compiler.Compile(parsed.Value)
+			require.Nil(t, cErr)
+			require.NoError(t, vm.Verify(program))
+		})
+	}
+}
diff --git a/internal/vm/verify.go b/internal/vm/verify.go
index 80e0d5d6..d4bfaa12 100644
--- a/internal/vm/verify.go
+++ b/internal/vm/verify.go
@@ -44,6 +44,13 @@ type programInfo struct {
 	varStrsLen int
 }
 
+// Verify statically checks that a program is safe to execute: a nil result
+// guarantees the execution loop cannot read out of bounds or crash on it.
+func Verify(p Program) error {
+	_, err := verify(p)
+	return err
+}
+
 func instrWords(op byte) int {
 	switch Opcode(op) {
 	case Op_PullAccount, Op_MkAllotment:

From a43eca3518eced81eea089c686cd139bf1a4a637 Mon Sep 17 00:00:00 2001
From: ascandone <alescandone@gmail.com>
Date: Tue, 14 Jul 2026 17:36:08 +0200
Subject: [PATCH 5/9] feat: compiler self-verifies its output

Compile now runs vm.Verify on the assembled program and fails if it
does not pass, so every script compiled anywhere (all unit tests and
production) is certified to pass the VM sanity checks.
---
 internal/compiler/compiler.go | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/internal/compiler/compiler.go b/internal/compiler/compiler.go
index 3449720d..b2f11c19 100644
--- a/internal/compiler/compiler.go
+++ b/internal/compiler/compiler.go
@@ -28,6 +28,11 @@ func Compile(program parser.Program) (VarsEncoder, vm.Program, error) {
 		return VarsEncoder{}, vm.Program{}, err
 	}
 
+	// the compiler must never emit code the VM would reject
+	if err := vm.Verify(prog); err != nil {
+		return VarsEncoder{}, vm.Program{}, err
+	}
+
 	return compiled.varsEncoder, prog, nil
 }
 

From c9c4eeeec2c9574a4711458d9ee77bcca0072a6c Mon Sep 17 00:00:00 2001
From: ascandone <alescandone@gmail.com>
Date: Fri, 17 Jul 2026 12:25:35 +0200
Subject: [PATCH 6/9] fix: fix after rebase

---
 internal/compiler/fuzz_mutate_test.go |  2 +-
 internal/vm/fuzz_test.go              |  2 +-
 internal/vm/verify_test.go            |  6 +++---
 internal/vm/vm_test.go                | 11 ++++-------
 4 files changed, 9 insertions(+), 12 deletions(-)

diff --git a/internal/compiler/fuzz_mutate_test.go b/internal/compiler/fuzz_mutate_test.go
index 7b07e271..a64cdf8e 100644
--- a/internal/compiler/fuzz_mutate_test.go
+++ b/internal/compiler/fuzz_mutate_test.go
@@ -72,6 +72,6 @@ func FuzzMutatedBytecode(f *testing.F) {
 				t.Fatalf("verified program panicked on Exec: %v", r)
 			}
 		}()
-		_, _ = vm.Exec(vm.NewVm(prog), nil, store)
+		_, _ = vm.Exec(t.Context(), vm.NewVm(prog), nil, store)
 	})
 }
diff --git a/internal/vm/fuzz_test.go b/internal/vm/fuzz_test.go
index 77119ebf..c0fef99d 100644
--- a/internal/vm/fuzz_test.go
+++ b/internal/vm/fuzz_test.go
@@ -31,6 +31,6 @@ func FuzzExec(f *testing.F) {
 				t.Fatalf("Exec panicked: %v", r)
 			}
 		}()
-		_, _ = Exec(NewVm(prog), nil, mockStore{})
+		_, _ = Exec(t.Context(), NewVm(prog), nil, mockStore{})
 	})
 }
diff --git a/internal/vm/verify_test.go b/internal/vm/verify_test.go
index 36036bfb..1b7fca5b 100644
--- a/internal/vm/verify_test.go
+++ b/internal/vm/verify_test.go
@@ -7,7 +7,7 @@ import (
 
 func mustReject(t *testing.T, p Program) {
 	t.Helper()
-	_, err := Exec(NewVm(p), nil, mockStore{})
+	_, err := Exec(t.Context(), NewVm(p), nil, mockStore{})
 	if _, ok := err.(MalformedProgramError); !ok {
 		t.Fatalf("expected MalformedProgramError, got %v", err)
 	}
@@ -43,7 +43,7 @@ func TestVerify_JumpOutOfRange(t *testing.T) {
 
 func TestVerify_MissingVars(t *testing.T) {
 	// reads var int 0 but no vars are passed
-	_, err := Exec(NewVm(Program{Instructions: []Instruction{bc(Op_LoadVarInt, 0, 0)}}), nil, mockStore{})
+	_, err := Exec(t.Context(), NewVm(Program{Instructions: []Instruction{bc(Op_LoadVarInt, 0, 0)}}), nil, mockStore{})
 	if _, ok := err.(MalformedProgramError); !ok {
 		t.Fatalf("expected MalformedProgramError, got %v", err)
 	}
@@ -72,7 +72,7 @@ func TestVerify_SizesBanksToNeed(t *testing.T) {
 	// a program using int reg 5 must get an int bank of at least 6
 	p := Program{Instructions: []Instruction{bc(Op_LoadInt, 5, 0)}, IntsPool: []big.Int{*big.NewInt(1)}}
 	vm := NewVm(p)
-	if _, err := Exec(vm, nil, mockStore{}); err != nil {
+	if _, err := Exec(t.Context(), vm, nil, mockStore{}); err != nil {
 		t.Fatalf("unexpected error: %v", err)
 	}
 	if len(vm.intsRegs) != 6 {
diff --git a/internal/vm/vm_test.go b/internal/vm/vm_test.go
index bf57a505..a3c222cb 100644
--- a/internal/vm/vm_test.go
+++ b/internal/vm/vm_test.go
@@ -178,14 +178,11 @@ func TestAssertNonNegativeBalance(t *testing.T) {
 
 func TestUnknownOpcode(t *testing.T) {
 	prog := Program{Instructions: []Instruction{abc(0xFE, 0, 0, 0)}}
-	_, err := Exec(context.Background(), NewVm(prog), nil, mockStore{})
-	if _, ok := err.(InternalError); !ok {
-		t.Fatalf("expected InternalError, got %v", err)
-		_, err := Exec(NewVm(prog), nil, mockStore{})
-		if _, ok := err.(MalformedProgramError); !ok {
-			t.Fatalf("expected MalformedProgramError, got %v", err)
-		}
+	_, err := Exec(t.Context(), NewVm(prog), nil, mockStore{})
+	if _, ok := err.(MalformedProgramError); !ok {
+		t.Fatalf("expected MalformedProgramError, got %v", err)
 	}
+
 }
 
 func TestMkPortionDivideByZero(t *testing.T) {

From 85fbf2c3adb84c16dff5fb3d50533699c04347fc Mon Sep 17 00:00:00 2001
From: ascandone <alescandone@gmail.com>
Date: Fri, 17 Jul 2026 13:07:07 +0200
Subject: [PATCH 7/9] doc: added checks doc

---
 BYTECODE_CHECKS.md | 119 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 119 insertions(+)
 create mode 100644 BYTECODE_CHECKS.md

diff --git a/BYTECODE_CHECKS.md b/BYTECODE_CHECKS.md
new file mode 100644
index 00000000..9eb066e7
--- /dev/null
+++ b/BYTECODE_CHECKS.md
@@ -0,0 +1,119 @@
+# Bytecode checks
+
+Two independent static passes validate the compiled program before it runs. Once
+both pass, `vm.Exec` can index registers, pools and jump targets directly, with
+no defensive guards in the execution loop.
+
+## Pipeline
+
+```
+parser.Program
+  └─ compileProgramToVirtual   → []vInstr        (virtual instructions)
+       └─ typecheckInstructions → (1) TYPE CHECK  internal/compiler/bytecode_typecheck.go
+            └─ assembleProgram   → vm.Program     (byte-encoded instructions)
+                 └─ vm.Verify    → (2) VERIFIER    internal/vm/verify.go
+```
+
+- Both passes run inside `Compile` (`internal/compiler/compiler.go`), so the
+  compiler *never* emits bytecode the VM would reject.
+- The verifier runs **again** at runtime, lazily, on the first `vm.Exec`
+  (gated by the `verified` flag in `internal/vm/vm.go`). This protects the VM
+  from any bytecode not produced by our compiler (hand-written, decoded from an
+  untrusted source, fuzzed, etc.).
+
+The two passes are complementary: the typechecker works on the high-level
+virtual instructions and enforces *types*; the verifier works on the final
+encoded bytes and enforces *memory safety*.
+
+---
+
+## (1) Bytecode typechecker — `internal/compiler/bytecode_typecheck.go`
+
+Runs on the virtual instruction stream. Every virtual register has exactly one
+type for its whole life, drawn from the four VM banks: `int`, `string`,
+`portion`, `monetary`.
+
+Checks, per instruction, in program order:
+
+- **Read-before-write** — a register read before it was ever written is rejected.
+- **Type consistency on read** — a register must be read with the same type it
+  was written with (`use`).
+- **Type consistency on write** — a register cannot be rewritten with a
+  different type than it already holds (`def`).
+- **Operand types** — each instruction's operands must match the fixed type
+  signature of its opcode (e.g. `AddInt` takes two `int`s and writes an `int`;
+  `MakeMonetary` takes a `string` + `int` and writes a `monetary`).
+
+Example rejections:
+
+```
+register r3 read as int before being written
+register r5 read as string but holds int
+register r2 written as portion but already holds int
+```
+
+This is a check on *our compiler*: a failure here means the code lowering AST →
+virtual instructions produced something inconsistent. It is not reachable from
+user input.
+
+---
+
+## (2) Bytecode verifier — `internal/vm/verify.go`
+
+Runs on the final byte-encoded `vm.Program`. A `nil` result guarantees the
+execution loop cannot read out of bounds or panic. It also computes the exact
+register-bank sizes the program needs.
+
+Checks:
+
+- **Instruction framing** — multi-word instructions (`PullAccount`,
+  `MkAllotment` take 2 words) must not be truncated at the end of the stream.
+- **Known opcodes** — every opcode must decode; unknown opcodes are rejected
+  (`decodeInstr`).
+- **Register bounds** — banks are sized to `maxIndex + 1` per bank from the
+  operands actually used, so every register access is in range by construction.
+- **Constant-pool bounds** — every int/string constant index is `< len(pool)`.
+- **Variable-pool bounds** — records the highest var index used; `Exec` later
+  checks the caller-supplied `Vars` provides at least that many.
+- **Jump validity** — every jump target must be:
+  - **forward** (`target > current`), and
+  - an **instruction boundary** (not the middle of a 2-word instruction, and not
+    past the end — jumping to `len(instrs)` halts, which is allowed).
+- **Definite assignment** — a register (and the `currentAsset` pseudo-slot) may
+  only be read if it was written on *every* path reaching that instruction.
+  Because all jumps are forward, predecessors are always earlier, so a single
+  ordered pass intersecting predecessors' written-sets is sufficient.
+
+Example rejections:
+
+```
+truncated instruction at 7: opcode 17 needs 2 words
+at instruction 3: int constant 5 out of range (pool size 4)
+at instruction 9: backward jump to 2
+at instruction 4: jump to 6 is not an instruction boundary
+at instruction 8: register (bank 0, index 2) read before being assigned on all paths
+```
+
+> Note: the forward-jump restriction is what keeps definite assignment a single
+> linear pass. Numscript has no backward control flow, so this costs nothing.
+
+---
+
+## What is NOT checked here
+
+These passes guarantee **structural and memory safety only**. They do *not*
+validate numscript runtime semantics — those are genuine runtime errors that
+depend on values only known during execution, and the VM checks them inline:
+
+| Runtime check | Opcode | Error |
+|---|---|---|
+| Insufficient funds | `CheckEnoughFunds` | `MissingFundsError` |
+| Allotment portions don't sum to 1 | `AssertLeftover` | `InvalidAllotmentSum` |
+| Mismatched assets | `AssertSameAsset` | `AssetMismatchError` |
+| Malformed account name | `AssertValidAccount` | `InvalidAccountName` |
+| Negative balance | `AssertNonNegativeBalance` | `NegativeBalanceError` |
+| Division by zero in a portion | `MkPortion` | `DivideByZeroError` |
+| Unbounded pull with no cap/overdraft | `PullAccount` | `InvalidUncappedSource` |
+| Non-numeric / malformed metadata | `Meta*` | `BadMetaValueError` |
+
+A verified program is safe to *execute*; it can still fail with any of the above.

From bf1aec12040648843c24fa2e767b4e418079212c Mon Sep 17 00:00:00 2001
From: ascandone <alescandone@gmail.com>
Date: Fri, 17 Jul 2026 13:17:41 +0200
Subject: [PATCH 8/9] perf: capture hoisted register banks by value, not by
 pointer

The rebase base (feat/exp/vm) hoists the register banks as pointers
(intsRegs := &vm.intsRegs) and dereferences them on every access in the
hot loop. The banks are sized once before the loop, so capturing the
slice headers by value (intsRegs := vm.intsRegs) is enough and lets the
loop index them directly, dropping a pointer indirection per access.
No behavior change.

Claude-Session: https://claude.ai/code/session_011sdzhYh6QFgP9uoev9JMXd
---
 internal/vm/vm.go | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/internal/vm/vm.go b/internal/vm/vm.go
index 809459d7..8d8e526c 100644
--- a/internal/vm/vm.go
+++ b/internal/vm/vm.go
@@ -115,10 +115,10 @@ func Exec[S Store](
 	// Hoist register banks and constant pools into locals so the hot loop indexes
 	// them directly instead of reloading the header off *vm / vm.program on every
 	// access.
-	intsRegs := &vm.intsRegs
-	stringsRegs := &vm.stringsRegs
-	portionsRegs := &vm.portionsRegs
-	monetariesRegs := &vm.monetariesRegs
+	intsRegs := vm.intsRegs
+	stringsRegs := vm.stringsRegs
+	portionsRegs := vm.portionsRegs
+	monetariesRegs := vm.monetariesRegs
 	intsPool := vm.program.IntsPool
 	stringsPool := vm.program.StringsPool
 

From a7ffeea642552c1a41ebf156e7e064f912ef217f Mon Sep 17 00:00:00 2001
From: ascandone <alescandone@gmail.com>
Date: Fri, 17 Jul 2026 15:09:19 +0200
Subject: [PATCH 9/9] refactor: declare register/var bank sizes in Program;
 Verify optional

The program now carries its own bank sizes: the assembler writes the max
register per bank (1 byte each, <=255 since 0xFF is nilReg) and the compiler the
var-pool sizes (uint16 each, since a portion is 2 int slots and a monetary 1+1).
These round-trip through Encode/DecodeProgram.

NewVm allocates the four register banks directly from those declared counts, so
Exec no longer verifies or sizes anything on its first call. Verify becomes an
optional, caller-invoked method (program.Verify()) that only reports validity:
it checks every register/var index against the declared counts (over-declaration
is valid, under-declaration is not) plus the existing framing/opcode/const/jump/
definite-assignment checks. Our compiler still self-verifies its own output.

The safety contract flips accordingly: Exec no longer promises to reject
arbitrary bytecode (unverified garbage may panic); instead 'Verify() == nil'
implies 'Exec never panics'. The fuzz tests now assert exactly that. This also
surfaced a real gap: Op_MkAllotment with count 0 slices intsRegs[A:A] /
portionsRegs[B:B], which Go bounds-checks against capacity even when empty, so
Verify now checks the slice endpoints (A+C, B+C) explicitly.

Behavior-preserving for compiler output; the Exec hot loop is unchanged
(benchmarks flat). Enables unchecked (unsafe) register indexing as a follow-up.

Claude-Session: https://claude.ai/code/session_011sdzhYh6QFgP9uoev9JMXd
---
 internal/compiler/assemble.go                 |   6 +
 internal/compiler/compiler.go                 |   5 +-
 internal/compiler/fuzz_mutate_test.go         |   7 +-
 .../fuzz/FuzzMutatedBytecode/ea6dc0f3e8269894 |   2 +
 internal/compiler/verify_corpus_test.go       |   3 +-
 internal/vm/fuzz_test.go                      |  18 ++-
 internal/vm/meta_test.go                      |   4 +-
 internal/vm/program.go                        |  38 +++++-
 internal/vm/program_encode_test.go            |  17 ++-
 internal/vm/vars_test.go                      |   2 +-
 internal/vm/verify.go                         | 125 ++++++++++--------
 internal/vm/verify_test.go                    |  35 +++--
 internal/vm/vm.go                             |  33 +++--
 internal/vm/vm_test.go                        |  82 ++++++++++--
 14 files changed, 260 insertions(+), 117 deletions(-)
 create mode 100644 internal/compiler/testdata/fuzz/FuzzMutatedBytecode/ea6dc0f3e8269894

diff --git a/internal/compiler/assemble.go b/internal/compiler/assemble.go
index a9c22ec0..07de73db 100644
--- a/internal/compiler/assemble.go
+++ b/internal/compiler/assemble.go
@@ -148,6 +148,12 @@ func assembleProgram(instrs []vInstr) (vm.Program, error) {
 		Instructions: a.instructions,
 		StringsPool:  a.stringsPool.items,
 		IntsPool:     a.intsPool.items,
+		// each pool's next is the number of registers used in that bank (<= 255,
+		// since regPool.index/reserveContiguous cap allocation at maxReg)
+		IntRegs:      byte(a.ints.next),
+		StrRegs:      byte(a.strings.next),
+		PortionRegs:  byte(a.portions.next),
+		MonetaryRegs: byte(a.monetaries.next),
 	}, nil
 }
 
diff --git a/internal/compiler/compiler.go b/internal/compiler/compiler.go
index b2f11c19..d0c71325 100644
--- a/internal/compiler/compiler.go
+++ b/internal/compiler/compiler.go
@@ -27,9 +27,12 @@ func Compile(program parser.Program) (VarsEncoder, vm.Program, error) {
 	if err != nil {
 		return VarsEncoder{}, vm.Program{}, err
 	}
+	// declared var-pool sizes: how many int/str slots Encode will produce
+	prog.IntVars = uint16(compiled.varsEncoder.nInt)
+	prog.StrVars = uint16(compiled.varsEncoder.nStr)
 
 	// the compiler must never emit code the VM would reject
-	if err := vm.Verify(prog); err != nil {
+	if err := prog.Verify(); err != nil {
 		return VarsEncoder{}, vm.Program{}, err
 	}
 
diff --git a/internal/compiler/fuzz_mutate_test.go b/internal/compiler/fuzz_mutate_test.go
index a64cdf8e..1009e9f1 100644
--- a/internal/compiler/fuzz_mutate_test.go
+++ b/internal/compiler/fuzz_mutate_test.go
@@ -62,8 +62,11 @@ func FuzzMutatedBytecode(f *testing.F) {
 			instrs[k] = vm.Instruction{Opcode: flat[k*4], A: flat[k*4+1], B: flat[k*4+2], C: flat[k*4+3]}
 		}
 
-		prog := vm.Program{Instructions: instrs, StringsPool: base.StringsPool, IntsPool: base.IntsPool}
-		if vm.Verify(prog) != nil {
+		// keep base's declared counts; a mutation that points an instruction at a
+		// register outside those bounds must be caught by Verify (coherence).
+		prog := base
+		prog.Instructions = instrs
+		if prog.Verify() != nil {
 			return // mutation broke the sanity checks: nothing more to prove
 		}
 
diff --git a/internal/compiler/testdata/fuzz/FuzzMutatedBytecode/ea6dc0f3e8269894 b/internal/compiler/testdata/fuzz/FuzzMutatedBytecode/ea6dc0f3e8269894
new file mode 100644
index 00000000..47ca2519
--- /dev/null
+++ b/internal/compiler/testdata/fuzz/FuzzMutatedBytecode/ea6dc0f3e8269894
@@ -0,0 +1,2 @@
+go test fuzz v1
+[]byte("\xa60\xa4\x12")
diff --git a/internal/compiler/verify_corpus_test.go b/internal/compiler/verify_corpus_test.go
index e0bced25..2b28a0b7 100644
--- a/internal/compiler/verify_corpus_test.go
+++ b/internal/compiler/verify_corpus_test.go
@@ -8,7 +8,6 @@ import (
 	"github.com/formancehq/numscript/internal/compiler"
 	"github.com/formancehq/numscript/internal/parser"
 	"github.com/formancehq/numscript/internal/specs_format"
-	"github.com/formancehq/numscript/internal/vm"
 
 	"github.com/stretchr/testify/require"
 )
@@ -30,7 +29,7 @@ func TestCompiledCorpusPassesVerify(t *testing.T) {
 			require.Empty(t, parsed.Errors)
 			_, program, cErr := compiler.Compile(parsed.Value)
 			require.Nil(t, cErr)
-			require.NoError(t, vm.Verify(program))
+			require.NoError(t, program.Verify())
 		})
 	}
 }
diff --git a/internal/vm/fuzz_test.go b/internal/vm/fuzz_test.go
index c0fef99d..32e8bba9 100644
--- a/internal/vm/fuzz_test.go
+++ b/internal/vm/fuzz_test.go
@@ -5,9 +5,10 @@ import (
 	"testing"
 )
 
-// FuzzExec feeds arbitrary bytes as an instruction stream and asserts the VM
-// never panics: the verifier must reject a malformed program, or execution must
-// return a result/error. It never crashes the host.
+// FuzzExec feeds arbitrary bytes as an instruction stream and asserts that a
+// program which passes Verify never panics under Exec. Verify itself must also
+// never panic on arbitrary input. (Exec no longer verifies, so running an
+// unverified malformed program may legitimately panic — hence the Verify gate.)
 func FuzzExec(f *testing.F) {
 	f.Add([]byte{})
 	f.Add([]byte{byte(Op_LoadInt), 0, 0, 0})
@@ -24,13 +25,18 @@ func FuzzExec(f *testing.F) {
 			off := i * 4
 			instrs[i] = Instruction{data[off], data[off+1], data[off+2], data[off+3]}
 		}
-		prog := Program{Instructions: instrs, IntsPool: pool.IntsPool, StringsPool: pool.StringsPool}
-
 		defer func() {
 			if r := recover(); r != nil {
-				t.Fatalf("Exec panicked: %v", r)
+				t.Fatalf("panicked: %v", r)
 			}
 		}()
+
+		// size as the assembler would, then let Verify be the gate: only a
+		// verified program is required not to panic under Exec.
+		prog := sizeProgram(Program{Instructions: instrs, IntsPool: pool.IntsPool, StringsPool: pool.StringsPool})
+		if prog.Verify() != nil {
+			return
+		}
 		_, _ = Exec(t.Context(), NewVm(prog), nil, mockStore{})
 	})
 }
diff --git a/internal/vm/meta_test.go b/internal/vm/meta_test.go
index 8c317ecc..5c9ba3af 100644
--- a/internal/vm/meta_test.go
+++ b/internal/vm/meta_test.go
@@ -20,7 +20,7 @@ func TestSetAccountMeta(t *testing.T) {
 		StringsPool: []string{"acc", "k", "v"},
 	}
 
-	res, execErr := Exec(context.Background(), NewVm(prog), nil, mockStore{})
+	res, execErr := Exec(context.Background(), NewVm(sizeProgram(prog)), nil, mockStore{})
 	require.Nil(t, execErr)
 	require.Equal(t, runtime.AccountsMetadata{"acc": {"k": "v"}}, res.AccountsMetadata)
 }
@@ -48,7 +48,7 @@ func TestMetaStr(t *testing.T) {
 		"config": {"beneficiary": "alice"},
 	}}
 
-	res, execErr := Exec(context.Background(), NewVm(prog), nil, store)
+	res, execErr := Exec(context.Background(), NewVm(sizeProgram(prog)), nil, store)
 	require.Nil(t, execErr)
 	require.Equal(t, []runtime.Posting{
 		{Source: "world", Destination: "alice", Asset: "USD/2", Amount: big.NewInt(100)},
diff --git a/internal/vm/program.go b/internal/vm/program.go
index c2252b43..1ef47b6e 100644
--- a/internal/vm/program.go
+++ b/internal/vm/program.go
@@ -11,6 +11,20 @@ type Program struct {
 
 	StringsPool []string
 	IntsPool    []big.Int
+
+	// Declared register-bank sizes (max index + 1). Each fits in a byte because
+	// 0xFF is reserved as nilReg, so a real register index is <= 254. NewVm
+	// allocates exactly these; Verify checks no instruction exceeds them.
+	IntRegs      uint8
+	StrRegs      uint8
+	PortionRegs  uint8
+	MonetaryRegs uint8
+
+	// Declared var-pool sizes. A portion var expands to 2 int slots and a
+	// monetary to 1 int + 1 str slot, so these are not bounded by 255 and use
+	// uint16. Exec checks the caller-provided Vars has at least this many.
+	IntVars uint16
+	StrVars uint16
 }
 
 var le = binary.LittleEndian
@@ -24,7 +38,9 @@ func (p Program) Encode() []byte {
 
 	data, strTable, intTable := encodePools(p.StringsPool, p.IntsPool)
 
-	const headerLen = 4 + 4*8 // magic + 4 section pointers
+	// magic + declared counts (4 reg bytes + 2 var uint16s) + 4 section pointers
+	const countsLen = 4 + 2*2
+	const headerLen = 4 + countsLen + 4*8
 	instrStart := uint32(headerLen)
 	dataStart := instrStart + uint32(len(instrs))
 	strTableStart := dataStart + uint32(len(data))
@@ -32,6 +48,9 @@ func (p Program) Encode() []byte {
 
 	buf := make([]byte, 0, int(intTableStart)+len(intTable))
 	buf = append(buf, "NUMB"...)
+	buf = append(buf, p.IntRegs, p.StrRegs, p.PortionRegs, p.MonetaryRegs)
+	buf = le.AppendUint16(buf, p.IntVars)
+	buf = le.AppendUint16(buf, p.StrVars)
 	buf = appendSection(buf, instrStart, uint32(len(instrs)))
 	buf = appendSection(buf, dataStart, uint32(len(data)))
 	buf = appendSection(buf, strTableStart, uint32(len(strTable)))
@@ -191,6 +210,17 @@ func DecodeProgram(buf []byte) (Program, error) {
 
 	idx := 4
 
+	// declared counts: 4 reg bytes + 2 var uint16s
+	if idx+8 > len(buf) {
+		return Program{}, fmt.Errorf("header truncated: missing declared bank counts")
+	}
+	intRegs, strRegs, portionRegs, monetaryRegs := buf[idx], buf[idx+1], buf[idx+2], buf[idx+3]
+	idx += 4
+	intVars := le.Uint16(buf[idx:])
+	idx += 2
+	strVars := le.Uint16(buf[idx:])
+	idx += 2
+
 	instructions, err := readArr("instructions", buf, &idx, parseInstructions) // <- TODO copy into instructions
 	if err != nil {
 		return Program{}, err
@@ -219,5 +249,11 @@ func DecodeProgram(buf []byte) (Program, error) {
 		Instructions: instructions,
 		StringsPool:  stringsPool,
 		IntsPool:     intsPool,
+		IntRegs:      intRegs,
+		StrRegs:      strRegs,
+		PortionRegs:  portionRegs,
+		MonetaryRegs: monetaryRegs,
+		IntVars:      intVars,
+		StrVars:      strVars,
 	}, nil
 }
diff --git a/internal/vm/program_encode_test.go b/internal/vm/program_encode_test.go
index f5332e64..091d981a 100644
--- a/internal/vm/program_encode_test.go
+++ b/internal/vm/program_encode_test.go
@@ -13,13 +13,26 @@ func TestProgramEncodeDecodeRoundTrip(t *testing.T) {
 			bc(Op_LoadInt, 3, 1),
 			abc(Op_AddInt, 4, 3, 3),
 		},
-		StringsPool: []string{"world", "dest", "USD/2"},
-		IntsPool:    []big.Int{*big.NewInt(0), *big.NewInt(-42)},
+		StringsPool:  []string{"world", "dest", "USD/2"},
+		IntsPool:     []big.Int{*big.NewInt(0), *big.NewInt(-42)},
+		IntRegs:      5,
+		StrRegs:      3,
+		PortionRegs:  0,
+		MonetaryRegs: 2,
+		IntVars:      7,
+		StrVars:      300, // exercises the uint16 range (> 255)
 	}
 	got, err := DecodeProgram(prog.Encode())
 	if err != nil {
 		t.Fatalf("decode: %v", err)
 	}
+	if got.IntRegs != prog.IntRegs || got.StrRegs != prog.StrRegs ||
+		got.PortionRegs != prog.PortionRegs || got.MonetaryRegs != prog.MonetaryRegs ||
+		got.IntVars != prog.IntVars || got.StrVars != prog.StrVars {
+		t.Fatalf("declared counts mismatch:\n got %+v\nwant %+v",
+			[]any{got.IntRegs, got.StrRegs, got.PortionRegs, got.MonetaryRegs, got.IntVars, got.StrVars},
+			[]any{prog.IntRegs, prog.StrRegs, prog.PortionRegs, prog.MonetaryRegs, prog.IntVars, prog.StrVars})
+	}
 	if !reflect.DeepEqual(got.Instructions, prog.Instructions) {
 		t.Fatalf("instructions mismatch:\n got %+v\nwant %+v", got.Instructions, prog.Instructions)
 	}
diff --git a/internal/vm/vars_test.go b/internal/vm/vars_test.go
index b22da811..5d952dd4 100644
--- a/internal/vm/vars_test.go
+++ b/internal/vm/vars_test.go
@@ -41,7 +41,7 @@ func TestLoadVarOpcodes(t *testing.T) {
 		StringsPool: []string{"USD/2"},
 	}
 
-	res, execErr := Exec(context.Background(), NewVm(prog), &vars, mockStore{})
+	res, execErr := Exec(context.Background(), NewVm(sizeProgram(prog)), &vars, mockStore{})
 	require.Nil(t, execErr)
 
 	want := []runtime.Posting{
diff --git a/internal/vm/verify.go b/internal/vm/verify.go
index d4bfaa12..bf0a129e 100644
--- a/internal/vm/verify.go
+++ b/internal/vm/verify.go
@@ -34,21 +34,25 @@ type decoded struct {
 	jumpTarget int // instruction index, or -1
 }
 
-type regCounts struct {
-	ints, strings, portions, monetaries int
-}
-
-type programInfo struct {
-	regs       regCounts
-	varIntsLen int
-	varStrsLen int
-}
-
-// Verify statically checks that a program is safe to execute: a nil result
-// guarantees the execution loop cannot read out of bounds or crash on it.
-func Verify(p Program) error {
-	_, err := verify(p)
-	return err
+// regBankSize is the declared size of the register bank r belongs to. The
+// verifier checks every register index against it; the execution loop allocates
+// exactly this many. bankCurrentAsset is a single-slot pseudo-bank that is never
+// allocated (definite-assignment tracking only).
+func (p Program) regBankSize(b regBank) int {
+	switch b {
+	case bankInt:
+		return int(p.IntRegs)
+	case bankStr:
+		return int(p.StrRegs)
+	case bankPortion:
+		return int(p.PortionRegs)
+	case bankMonetary:
+		return int(p.MonetaryRegs)
+	case bankCurrentAsset:
+		return 1
+	default:
+		return 0
+	}
 }
 
 func instrWords(op byte) int {
@@ -60,10 +64,18 @@ func instrWords(op byte) int {
 	}
 }
 
-// verify statically checks a program cannot make the VM read out of bounds and
-// returns the exact register-bank sizes it needs. A verified program can be run
-// with no bounds checks in the execution loop.
-func verify(p Program) (programInfo, error) {
+// Verify statically checks that a program is safe to execute: a nil result
+// guarantees the execution loop cannot read out of bounds or crash on it.
+//
+// It only reports validity — it never derives sizes. Every register/var index is
+// checked against the counts the program declares (see Program.IntRegs etc.);
+// an index within a declared bound is valid, so an over-large declared count is
+// accepted (wasteful, but the producer's concern, not the verifier's).
+//
+// Verify is optional and the caller's responsibility: Exec does not run it.
+// Trusted producers (our own compiler) may skip it; run it on any bytecode whose
+// coherence with its declared counts is not already guaranteed.
+func (p Program) Verify() error {
 	instrs := p.Instructions
 	n := len(instrs)
 
@@ -80,7 +92,7 @@ func verify(p Program) (programInfo, error) {
 		op := instrs[i].Opcode
 		w := instrWords(op)
 		if i+w > n {
-			return programInfo{}, fmt.Errorf("truncated instruction at %d: opcode %d needs %d words", i, op, w)
+			return fmt.Errorf("truncated instruction at %d: opcode %d needs %d words", i, op, w)
 		}
 		var ext Instruction
 		if w == 2 {
@@ -88,67 +100,64 @@ func verify(p Program) (programInfo, error) {
 		}
 		d, err := decodeInstr(instrs[i], ext)
 		if err != nil {
-			return programInfo{}, fmt.Errorf("at instruction %d: %w", i, err)
+			return fmt.Errorf("at instruction %d: %w", i, err)
 		}
 		boundary[i] = true
 		steps = append(steps, step{i, d})
 		i += w
 	}
 
-	info := programInfo{}
-	grow := func(r regRef) {
-		s := r.index + 1
-		switch r.bank {
-		case bankInt:
-			if s > info.regs.ints {
-				info.regs.ints = s
-			}
-		case bankStr:
-			if s > info.regs.strings {
-				info.regs.strings = s
-			}
-		case bankPortion:
-			if s > info.regs.portions {
-				info.regs.portions = s
-			}
-		case bankMonetary:
-			if s > info.regs.monetaries {
-				info.regs.monetaries = s
-			}
+	check := func(at int, r regRef) error {
+		if r.index >= p.regBankSize(r.bank) {
+			return fmt.Errorf("at instruction %d: %s exceeds declared bank size %d", at, describeRef(r), p.regBankSize(r.bank))
 		}
+		return nil
 	}
 
 	for _, st := range steps {
 		d := st.d
 		for _, r := range d.reads {
-			grow(r)
+			if err := check(st.at, r); err != nil {
+				return err
+			}
 		}
 		for _, r := range d.writes {
-			grow(r)
-		}
-		if d.constInt >= 0 {
-			if d.constInt >= len(p.IntsPool) {
-				return programInfo{}, fmt.Errorf("at instruction %d: int constant %d out of range (pool size %d)", st.at, d.constInt, len(p.IntsPool))
+			if err := check(st.at, r); err != nil {
+				return err
 			}
 		}
-		if d.constStr >= 0 {
-			if d.constStr >= len(p.StringsPool) {
-				return programInfo{}, fmt.Errorf("at instruction %d: string constant %d out of range (pool size %d)", st.at, d.constStr, len(p.StringsPool))
+		// Op_MkAllotment slices intsRegs[A:A+C] and portionsRegs[B:B+C]. The
+		// per-element refs above cover C>0, but a slice expression bounds-checks
+		// its endpoints regardless of length, so an empty slice (C==0) with a
+		// start past the bank still panics. Check the endpoints explicitly.
+		if Opcode(instrs[st.at].Opcode) == Op_MkAllotment {
+			ins := instrs[st.at]
+			if int(ins.A)+int(ins.C) > p.regBankSize(bankInt) {
+				return fmt.Errorf("at instruction %d: allotment dest array [%d:%d] exceeds int bank size %d", st.at, ins.A, int(ins.A)+int(ins.C), p.regBankSize(bankInt))
+			}
+			if int(ins.B)+int(ins.C) > p.regBankSize(bankPortion) {
+				return fmt.Errorf("at instruction %d: allotment portion array [%d:%d] exceeds portion bank size %d", st.at, ins.B, int(ins.B)+int(ins.C), p.regBankSize(bankPortion))
 			}
 		}
-		if d.varInt >= 0 && d.varInt+1 > info.varIntsLen {
-			info.varIntsLen = d.varInt + 1
+		if d.constInt >= 0 && d.constInt >= len(p.IntsPool) {
+			return fmt.Errorf("at instruction %d: int constant %d out of range (pool size %d)", st.at, d.constInt, len(p.IntsPool))
+		}
+		if d.constStr >= 0 && d.constStr >= len(p.StringsPool) {
+			return fmt.Errorf("at instruction %d: string constant %d out of range (pool size %d)", st.at, d.constStr, len(p.StringsPool))
+		}
+		if d.varInt >= 0 && d.varInt >= int(p.IntVars) {
+			return fmt.Errorf("at instruction %d: int var %d exceeds declared var count %d", st.at, d.varInt, p.IntVars)
 		}
-		if d.varStr >= 0 && d.varStr+1 > info.varStrsLen {
-			info.varStrsLen = d.varStr + 1
+		if d.varStr >= 0 && d.varStr >= int(p.StrVars) {
+			return fmt.Errorf("at instruction %d: string var %d exceeds declared var count %d", st.at, d.varStr, p.StrVars)
 		}
 		if d.jumpTarget >= 0 {
 			t := d.jumpTarget
 			if t <= st.at {
-				return programInfo{}, fmt.Errorf("at instruction %d: backward jump to %d", st.at, t)
+				return fmt.Errorf("at instruction %d: backward jump to %d", st.at, t)
 			}
 			if t > n || !boundary[t] {
-				return programInfo{}, fmt.Errorf("at instruction %d: jump to %d is not an instruction boundary", st.at, t)
+				return fmt.Errorf("at instruction %d: jump to %d is not an instruction boundary", st.at, t)
 			}
 		}
 	}
@@ -177,7 +186,7 @@ func verify(p Program) (programInfo, error) {
 		in := intersectAssigned(assignedOut, preds[k])
 		for _, r := range st.d.reads {
 			if !in[r] {
-				return programInfo{}, fmt.Errorf("at instruction %d: %s read before being assigned on all paths", st.at, describeRef(r))
+				return fmt.Errorf("at instruction %d: %s read before being assigned on all paths", st.at, describeRef(r))
 			}
 		}
 		for _, r := range st.d.writes {
@@ -186,7 +195,7 @@ func verify(p Program) (programInfo, error) {
 		assignedOut[k] = in
 	}
 
-	return info, nil
+	return nil
 }
 
 func intersectAssigned(out []map[regRef]bool, preds []int) map[regRef]bool {
diff --git a/internal/vm/verify_test.go b/internal/vm/verify_test.go
index 1b7fca5b..8c6eeb5d 100644
--- a/internal/vm/verify_test.go
+++ b/internal/vm/verify_test.go
@@ -5,11 +5,13 @@ import (
 	"testing"
 )
 
+// mustReject asserts Verify rejects p. Programs are sized first (as the
+// assembler would) so a rejection reflects the specific incoherence under test
+// rather than an incidentally-too-small declared bank.
 func mustReject(t *testing.T, p Program) {
 	t.Helper()
-	_, err := Exec(t.Context(), NewVm(p), nil, mockStore{})
-	if _, ok := err.(MalformedProgramError); !ok {
-		t.Fatalf("expected MalformedProgramError, got %v", err)
+	if err := sizeProgram(p).Verify(); err == nil {
+		t.Fatalf("expected program to be rejected by Verify, got nil")
 	}
 }
 
@@ -42,8 +44,10 @@ func TestVerify_JumpOutOfRange(t *testing.T) {
 }
 
 func TestVerify_MissingVars(t *testing.T) {
-	// reads var int 0 but no vars are passed
-	_, err := Exec(t.Context(), NewVm(Program{Instructions: []Instruction{bc(Op_LoadVarInt, 0, 0)}}), nil, mockStore{})
+	// reads var int 0 but no vars are passed. This is an Exec-time guard (vars are
+	// caller input, not part of the bytecode), not a Verify check.
+	p := sizeProgram(Program{Instructions: []Instruction{bc(Op_LoadVarInt, 0, 0)}})
+	_, err := Exec(t.Context(), NewVm(p), nil, mockStore{})
 	if _, ok := err.(MalformedProgramError); !ok {
 		t.Fatalf("expected MalformedProgramError, got %v", err)
 	}
@@ -68,14 +72,19 @@ func TestVerify_CurrentAssetNotSet(t *testing.T) {
 	}, StringsPool: []string{"dest"}})
 }
 
-func TestVerify_SizesBanksToNeed(t *testing.T) {
-	// a program using int reg 5 must get an int bank of at least 6
-	p := Program{Instructions: []Instruction{bc(Op_LoadInt, 5, 0)}, IntsPool: []big.Int{*big.NewInt(1)}}
-	vm := NewVm(p)
-	if _, err := Exec(t.Context(), vm, nil, mockStore{}); err != nil {
-		t.Fatalf("unexpected error: %v", err)
+func TestNewVmSizesBanksFromDeclaredCounts(t *testing.T) {
+	// NewVm allocates each bank to the program's declared count (no scanning).
+	vm := NewVm(Program{IntRegs: 6, StrRegs: 2, PortionRegs: 1, MonetaryRegs: 3})
+	if got := len(vm.intsRegs); got != 6 {
+		t.Fatalf("int bank size = %d, want 6", got)
+	}
+	if got := len(vm.stringsRegs); got != 2 {
+		t.Fatalf("string bank size = %d, want 2", got)
+	}
+	if got := len(vm.portionsRegs); got != 1 {
+		t.Fatalf("portion bank size = %d, want 1", got)
 	}
-	if len(vm.intsRegs) != 6 {
-		t.Fatalf("int bank size = %d, want 6", len(vm.intsRegs))
+	if got := len(vm.monetariesRegs); got != 3 {
+		t.Fatalf("monetary bank size = %d, want 3", got)
 	}
 }
diff --git a/internal/vm/vm.go b/internal/vm/vm.go
index 8d8e526c..b7a2fa48 100644
--- a/internal/vm/vm.go
+++ b/internal/vm/vm.go
@@ -17,8 +17,6 @@ const worldAccount = "world"
 
 type Vm struct {
 	program  Program
-	verified bool
-	info     programInfo
 	runstate *runtime.RunState
 
 	stringsRegs    []string // asset,string,account
@@ -27,11 +25,18 @@ type Vm struct {
 	monetariesRegs []monetary
 }
 
+// NewVm allocates the register banks from the program's declared sizes. It does
+// not verify the program: run program.Verify() first if the bytecode is not
+// already trusted to be coherent with its declared counts.
 func NewVm(
 	program Program,
 ) *Vm {
 	return &Vm{
-		program: program,
+		program:        program,
+		intsRegs:       make([]big.Int, program.IntRegs),
+		stringsRegs:    make([]string, program.StrRegs),
+		portionsRegs:   make([]big.Rat, program.PortionRegs),
+		monetariesRegs: make([]monetary, program.MonetaryRegs),
 	}
 }
 
@@ -83,21 +88,13 @@ func Exec[S Store](
 	runtimeStore := runtimeStoreAdapter{store: store}
 	// RunState fetches balances lazily through this store; a fetch error surfaces
 	// from the RunState call that triggered it, wrapped in StoreError below.
-	if !vm.verified {
-		info, err := verify(vm.program)
-		if err != nil {
-			return runtime.ExecutionResult{}, MalformedProgramError{Reason: err.Error()}
-		}
-		vm.info = info
-		vm.intsRegs = make([]big.Int, info.regs.ints)
-		vm.stringsRegs = make([]string, info.regs.strings)
-		vm.portionsRegs = make([]big.Rat, info.regs.portions)
-		vm.monetariesRegs = make([]monetary, info.regs.monetaries)
-		vm.verified = true
-	}
-
-	if vm.info.varIntsLen > 0 || vm.info.varStrsLen > 0 {
-		if vars == nil || len(vars.IntsPool) < vm.info.varIntsLen || len(vars.StringsPool) < vm.info.varStrsLen {
+	//
+	// Exec does not verify the program (that is program.Verify(), the caller's
+	// responsibility). The register banks are already sized to the declared
+	// counts by NewVm. Vars are separate caller-supplied input, so we still guard
+	// that enough were provided for what the program declares it reads.
+	if vm.program.IntVars > 0 || vm.program.StrVars > 0 {
+		if vars == nil || len(vars.IntsPool) < int(vm.program.IntVars) || len(vars.StringsPool) < int(vm.program.StrVars) {
 			return runtime.ExecutionResult{}, MalformedProgramError{Reason: "program reads more variables than were provided"}
 		}
 	}
diff --git a/internal/vm/vm_test.go b/internal/vm/vm_test.go
index a3c222cb..e8bf50ef 100644
--- a/internal/vm/vm_test.go
+++ b/internal/vm/vm_test.go
@@ -57,6 +57,64 @@ func bc(op Opcode, a byte, v uint16) Instruction {
 	return Instruction{Opcode: byte(op), A: a, B: byte(v), C: byte(v >> 8)}
 }
 
+// sizeProgram fills a hand-built Program's declared register/var counts by
+// scanning its instructions, mirroring what the assembler does for real
+// programs. Test-only: production Programs are decoded/compiled with counts
+// already declared. On a malformed instruction it stops early and leaves the
+// counts scanned so far, which is enough for Verify to then reject the program.
+func sizeProgram(p Program) Program {
+	instrs := p.Instructions
+	n := len(instrs)
+	bump := func(cur byte, idx int) byte {
+		if idx+1 > int(cur) {
+			return byte(idx + 1)
+		}
+		return cur
+	}
+	bump16 := func(cur uint16, idx int) uint16 {
+		if idx+1 > int(cur) {
+			return uint16(idx + 1)
+		}
+		return cur
+	}
+	for i := 0; i < n; {
+		w := instrWords(instrs[i].Opcode)
+		if i+w > n {
+			break
+		}
+		var ext Instruction
+		if w == 2 {
+			ext = instrs[i+1]
+		}
+		d, err := decodeInstr(instrs[i], ext)
+		if err != nil {
+			break
+		}
+		for _, refs := range [][]regRef{d.reads, d.writes} {
+			for _, r := range refs {
+				switch r.bank {
+				case bankInt:
+					p.IntRegs = bump(p.IntRegs, r.index)
+				case bankStr:
+					p.StrRegs = bump(p.StrRegs, r.index)
+				case bankPortion:
+					p.PortionRegs = bump(p.PortionRegs, r.index)
+				case bankMonetary:
+					p.MonetaryRegs = bump(p.MonetaryRegs, r.index)
+				}
+			}
+		}
+		if d.varInt >= 0 {
+			p.IntVars = bump16(p.IntVars, d.varInt)
+		}
+		if d.varStr >= 0 {
+			p.StrVars = bump16(p.StrVars, d.varStr)
+		}
+		i += w
+	}
+	return p
+}
+
 func inorderProgram() Program {
 	// Index of #inorder_end in the ENCODED stream. Note PullAccount occupies
 	// two words each, so this is not the count of source lines.
@@ -87,11 +145,11 @@ func inorderProgram() Program {
 		/* 21 */ abc(Op_SendToAccount, sDest, nilReg, nilReg), // send_to_account(r11)  (no cap, no color)
 	}
 
-	return Program{
+	return sizeProgram(Program{
 		Instructions: instrs,
 		StringsPool:  []string{"USD/2", "s1", "s2", "dest"},
 		IntsPool:     []big.Int{*big.NewInt(10), *big.NewInt(0)},
-	}
+	})
 }
 
 // --- mock store -----------------------------------------------------------
@@ -142,17 +200,17 @@ func TestInorderSend(t *testing.T) {
 }
 
 func assertValidAccountProgram(name string) Program {
-	return Program{
+	return sizeProgram(Program{
 		Instructions: []Instruction{
 			bc(Op_LoadStr, 0, 0),
 			abc(Op_AssertValidAccount, 0, nilReg, nilReg),
 		},
 		StringsPool: []string{name},
-	}
+	})
 }
 
 func balanceNonNegativeProgram() Program {
-	return Program{
+	return sizeProgram(Program{
 		Instructions: []Instruction{
 			bc(Op_LoadStr, 0, 0),
 			bc(Op_LoadStr, 1, 1),
@@ -160,7 +218,7 @@ func balanceNonNegativeProgram() Program {
 			abc(Op_AssertNonNegativeBalance, 0, 0, nilReg),
 		},
 		StringsPool: []string{"acc", "USD/2"},
-	}
+	})
 }
 
 func TestAssertNonNegativeBalance(t *testing.T) {
@@ -177,23 +235,25 @@ func TestAssertNonNegativeBalance(t *testing.T) {
 }
 
 func TestUnknownOpcode(t *testing.T) {
+	// Exec no longer verifies; an unknown opcode reaches the loop's default arm
+	// and returns InternalError (rather than panicking). Rejection at the static
+	// level is covered by TestVerify_UnknownOpcode.
 	prog := Program{Instructions: []Instruction{abc(0xFE, 0, 0, 0)}}
 	_, err := Exec(t.Context(), NewVm(prog), nil, mockStore{})
-	if _, ok := err.(MalformedProgramError); !ok {
-		t.Fatalf("expected MalformedProgramError, got %v", err)
+	if _, ok := err.(InternalError); !ok {
+		t.Fatalf("expected InternalError, got %v", err)
 	}
-
 }
 
 func TestMkPortionDivideByZero(t *testing.T) {
-	prog := Program{
+	prog := sizeProgram(Program{
 		Instructions: []Instruction{
 			bc(Op_LoadInt, 0, 0),
 			bc(Op_LoadInt, 1, 1),
 			abc(Op_MkPortion, 0, 0, 1),
 		},
 		IntsPool: []big.Int{*big.NewInt(1), *big.NewInt(0)},
-	}
+	})
 	_, err := Exec(context.Background(), NewVm(prog), nil, mockStore{})
 	if _, ok := err.(DivideByZeroError); !ok {
 		t.Fatalf("expected DivideByZeroError, got %v", err)