ISA Reference

This document is the specification of predicator's instruction set: the flat list of opcodes a compiled expression becomes and a stack VM runs. It is the artifact a sibling implementation (Ruby, JavaScript) implements against, and the one the conformance corpus is generated from.

It is not a syntax reference. For the expression grammar, operators, and builtin functions, see Language Reference. This document covers the instruction layer beneath that syntax - what an expression compiles to and how it runs, not how it is written.

Per ADR-0003, the Elixir implementation (this repository) is the reference implementation of the ISA. It moves when this library needs it to; sibling parity is a downstream obligation, not an upstream constraint.

1. Versioning

The versioning scheme is settled by ADR-0003; this section records it rather than re-arguing it.

• ISA versions are integers - v1, v2, v3 - with no correspondence to this library's semver. All three ISA v2 opcodes shipped in 3.7.0; 3.8.0 then refined v2 semantics without adding an opcode (it made every arithmetic and legacy logical opcode report an unbound root rather than a type mismatch). ISA v3 both retired and/or and introduced store/pop, the two opcodes the statement layer needed, shipping in 4.0.0.
• An opcode's semantics never change under its own name. A change to what an opcode does is a new name at a new version. This is what makes "scan the opcode names in a list" a sound answer to "what version does this list require".
• Adding an operand form or widening an accepted type is a new version but not a new name. This rule speaks to operand forms carried in the instruction list - what a conformant implementation must accept and execute. Widening §3's value domain at the host/context boundary moves no version, because no opcode-name scan can express it and no existing instruction list changes meaning (px-o9v's null widening is this case). A later source spelling for a value that domain already admits likewise moves no version, because a spelling is surface syntax (§6) and attaches to no opcode name - the undefined literal and the null literal are both this case.
• An additive version - new opcodes only, every existing instruction list still valid - ships in a minor release.
• Retirement mints the next ISA integer, in addition to taking a major library release and an upgrade path. The integer moves because a build that no longer runs an opcode must be distinguishable from one that does - without it, the version stamp reports a list runnable that the build will refuse.
• A version's opcode set is a half-open interval. Each opcode is introduced at one version and, if ever retired, removed at another; version v's set is every opcode with introduced <= v < removed_in. A version's set is fixed once minted - retiring at v3 does not change what v2 was - so a sibling declaring v2 claims v2's whole set, retired opcodes included.
• The check a consumer performs is membership in Predicator.Instructions.opcode_set/1 for this build's version, not a bare comparison against required_isa/1's result: required_isa/1 still names the version an instruction list needs, and retired_in/1 names the version that removed an opcode, and together they are what lets a refusal name a version rather than say "unknown opcode".
• A sibling behind the current version is an expected, documented state. Each sibling publishes the version it supports in its own repository; this document maintains no support matrix.

Current version: ISA v6.

At runtime, Predicator.isa_version/0 returns this build's version as an integer, and Predicator.Instructions.required_isa/1 returns the minimum version a given instruction list needs.

2. Execution model

The rules that govern every opcode, stated once here rather than repeated in each row.

• A program is a flat list of instructions. An instruction is a JSON array whose first element is the opcode name and whose remaining elements are operands (Predicator.Types.instruction/0). Nothing else is in the wire format - source positions and spans travel in an Elixir-side side table that is never serialized (Predicator.Types.position_table/0, Predicator.Types.span_table/0).
• Execution is sequential from index 0. The program halts when the instruction pointer reaches or passes the end of the list, so a forward jump past the last instruction is a normal halt, not an error.
• In expression mode, the result is the top of the stack at halt. An empty stack at halt is an EvaluationError with reason "empty_stack"; it is the one error that belongs to no instruction and therefore carries no source position. A deeper stack is not an error: the top is the result and anything beneath it is discarded. This rule, empty_stack included, is expression mode's alone - see "Two execution modes" below.
• Opcodes validate, they do not coerce. There is no general truthiness rule; a boolean-expecting opcode handed a non-boolean is a TypeMismatchError.
• What "falsy" means at a jump: false, null, or :undefined, and nothing else. "True" means exactly true. This is ECMAScript-aligned, deliberately not symmetric-Kleene (ADR-0001).
• Jumps are relative; the operand is always a positive integer. jump, jump_if_falsy_or_pop, and jump_if_true_or_pop target index + offset; jump_backward (ISA v6) targets index - offset. There is no absolute jump in the ISA.
• Execution of a list containing jump_backward must be bounded. An implementation charges a per-execution budget on each back edge taken and, on exhaustion, stops with an EvaluationError whose reason is "loop_budget_exceeded". The budget's default value and the option that configures it are implementation-local, as on_unbound is - only the bound's existence and the exhaustion reason are normative. The derived guarantee: between consecutive back edges the instruction pointer strictly increases, so total work is at most (budget + 1) * length(program) instructions.
• :undefined is a first-class value, not an absence. Some opcodes propagate it (compare under a non-strict operator, in, contains), some reject it (not, the arithmetic five, unary_minus, unary_bang, legacy and/or), and the jumps treat it as falsy. Each opcode's subsection below says which. null is also a first-class value, and the two are not the same thing: :undefined is an absence (no value was ever supplied), while null is a value that is present and empty. The opcodes treat them alike at a jump (both falsy) but differently under === and membership (null === undefined is false, and null is only ever equal to itself) - see §3 and §5.
• A malformed operand is an unknown instruction, not a bad operand. Every opcode's clause is guarded on its operand's shape, so an out-of-range or wrong-typed operand falls through to the catch-all clause and returns an EvaluationError with reason "unknown_instruction". Examples: ["make_list", -1], ["jump_if_falsy_or_pop", 0], ["compare", "FOO"], ["load", 5].
• Error types are normative; error messages are not. A sibling wording a message in its own idiom conforms. Three error types exist: EvaluationError, TypeMismatchError, UndefinedVariableError (lib/predicator/errors/).
• Insufficient operands is EvaluationError, not TypeMismatchError, at every opcode that checks stack depth before checking types.
• The Elixir-side on_unbound policy (:undefined versus :error on a load of an absent root) is an evaluation option, not part of the ISA: it changes what a load of an absent root does but adds no opcode and no wire-format change. See docs/architecture.md for that option; it is not respecified here.
• A host may name context roots a store refuses to write (the :protected_roots evaluation option). This is likewise an evaluation option, not part of the ISA: it adds no opcode and no wire-format change, and a run with no such option behaves exactly as specified above. When configured, a store whose path's root segment is protected returns EvaluationError with reason "protected_root" instead of writing. See §5's store subsection and docs/architecture.md for the option; it is not respecified here.

Two execution modes

A program is a flat instruction list with no header, so nothing in the wire format says whether it is an expression or a statement program. The mode is carried by the entry point, not by the artifact. In this implementation Predicator.evaluate/2,3 is expression mode and Predicator.execute/2 - the 4.0 statement layer, §6 - is statement mode; a sibling exposes the same two calls under whatever names it likes. The instruction set is identical in both: no opcode is restricted to one mode, and no opcode means anything different in the other. Only what "result" means differs.

• Expression mode - the result is the top of the stack at halt, and an empty stack at halt is empty_stack, as above.
• Statement mode - the result is the context at halt, not a stack value. The stack is scratch space between statement boundaries: a well-formed statement program ends each statement with a store or a pop and therefore halts with an empty stack by design. That is a normal halt. empty_stack is an expression-mode rule and is never raised in statement mode. A non-empty stack at halt is likewise not an error in statement mode; the residue is discarded, exactly as expression mode discards everything beneath the top.

A statement program that halts on an error has no result. Whether the partially applied context from the statements that completed before the error is kept or discarded is a property of the host API, not of the VM; the VM specifies only that execution stops at the failing instruction.

A host may additionally surface the value of the program's last expression statement alongside the context. That is a host-API convenience, not an ISA guarantee - the statement boundary's pop discards it as far as the VM is concerned. Predicator.execute_value/2 is this implementation's answer: it obtains the value by having the machine retain what pop discarded rather than by compiling the program differently, so the compiled artifact is identical either way.

Statement mode was specified here, ahead of the opcodes that reach it, so the statement layer arrived as two opcodes plus an entry point rather than as a change to this specification. Predicator.execute/2 is that entry point.

3. Value types

The value domain the opcodes operate over: integer, float, string, boolean, list, map (object), Date, DateTime, duration, null, and :undefined.

null and :undefined are both first-class values and neither is the other: :undefined is an absence - no value was ever supplied - while null is a value that is present and empty. Both read symmetrically at the surface: each has a literal keyword (undefined, null), and each compiles to the corresponding lit operand (§5, §6). null additionally enters the value domain through a host-supplied context, a load of a bound null, an access/bracket_access result, or a function return.

A duration's shape is normative, because ["duration", units] produces one and add/subtract consume it: a map with the seven keys years, months, weeks, days, hours, minutes, seconds, all present and defaulting to 0, plus an optional milliseconds key present only when a ms-family unit was used.

How these values cross a language boundary in the conformance corpus's tagged-value JSON encoding is px-35i.4's concern, not restated here.

Crossing a plain-JSON boundary

Seven of those eleven types are JSON's own - integer, float, string, boolean, list, map, null - and survive a JSON round trip unchanged. The other four do not, and because a lit operand may be any of them, an instruction list written out as plain JSON and read back is not necessarily the list that was written:

Each right-hand value is itself a member of the domain above, so the loss is silent in both directions: the encode succeeds, the decode yields a well-formed instruction, and the program runs. It runs a different program. ["lit", :undefined] stored and reloaded is ["lit", "undefined"], which turns the boundness test x === undefined into a string comparison that is always false. Nothing raises, and no version check catches it - the list requires the same ISA version either way, because no opcode changed.

This is not new with any particular version. Date, DateTime, and duration have been in the domain since v1; :undefined joined the list of spellings in 5.0.0 without joining the domain, which it was already in (§6).

The ISA defines no envelope for this, and does not intend to. Section 2's wire format is a plain JSON array and stays one; an envelope is something a consumer wraps around that array, and the right choice depends on the store - a consumer persisting to a JSON column has the problem, one persisting the source text or a language-native binary term does not have it at all. Two approaches work:

• The conformance corpus's tagged-value encoding, specified in conformance/README.md, carries exactly these four as {"$type": ...} objects and is the encoding to reach for. It is recommended, not normative outside the corpus: it is corpus apparatus, not a published API, and a consumer adopting it copies it rather than calls it. Its one caveat travels with it - a genuine predicator map containing a literal "$type" key is ambiguous with the tag namespace, and the corpus codec rejects such a map rather than emit a tag that would decode wrong.
• Persist the source and recompile on load. Recompiling the same source is deterministic, so this loses nothing, and it is already the recommended way to get a position table back after a round trip (Predicator.Compiled, ADR-0009). It costs a compile per load, which is the trade against storing a compiled artifact at all.

4. The opcode table

One row per opcode the ISA has ever contained, including opcodes the compiler no longer emits and opcodes a later version retired. A retired opcode keeps its row so the version scan stays total. Columns: Opcode, Operands, Pops, Pushes, ISA, Tier, Emitted by compiler, Removed in.

Error semantics are not a table column: several opcodes have three or four distinct error paths, more than a cell can carry cleanly. See the per-opcode subsections below the table.

Every opcode is ISA v1 except jump_if_falsy_or_pop, jump_if_true_or_pop, and make_list, which are v2 (ADR-0001), store and pop, which are v3, cast, which is v4 (ADR-0011), jump and pop_jump_if_falsy, which are v5 (ADR-0013), and jump_backward, which is v6 (ADR-0013).

Tiers

Tiers group opcodes for the conformance corpus (px-35i.4); a lower tier is a smaller, more foundational surface. Tier is a function of opcode only - a row's tier does not depend on the value types the expression happens to use (see the note after the table).

Tiers are defined by opcode, not by value. A date comparison ([["lit", Date], ["lit", Date], ["compare", "GT"]]) is tier 1 by opcode, even though it needs Date support and chronological comparison. Value-level requirements (dates, datetimes, durations) are carried by px-35i.4's feature tags, not by tiers.

Opcodes

jump_if_falsy_or_pop and jump_if_true_or_pop pop 0 or 1 values and push 0: on the taken branch they leave the value on the stack (net 0 change), and on the fall-through branch they pop it and execution continues into the next instruction, which pushes its own value. Neither jump itself ever pushes.

Retired opcodes

An opcode's Removed in cell holds - for a live opcode or vN for one retired at ISA vN. That marker is the ISA version that removed the opcode, not a library version (§1). A retired opcode keeps its row in this table, its entry in Predicator.Instructions's opcode map, and its membership in the tier-names table above; it loses exactly one thing, its execute_instruction/2 clause in the evaluator. required_isa/1 and tier/1 keep answering for it with a version rather than falling back to unknown_opcode. The conformance corpus keeps a retired opcode's cases too, with frozen expectations rather than ones the evaluator recomputes - see §8 and conformance/README.md. Retiring an opcode still requires an upgrade path (ADR-0003).

5. Per-opcode semantics and errors

Each opcode names the private functions in lib/predicator/evaluator.ex that implement it: the execute_instruction/2 clause matching its name, plus the helper it delegates to. Function names rather than line numbers, so a reference survives an edit above it.

• lit - pushes the operand unchanged. No error path. The operand may be any value in §3's value domain, :undefined and null included, and a source spelling exists for both as of the changes that added them (the undefined and null literal keywords, §6). Worth naming the one asymmetry: ["lit", nil] survives a plain-JSON round trip, while ["lit", :undefined] does not (§3's lossy table).

• load (load_from_context/2) - string-key lookup in the context; an absent key pushes :undefined. Atom keys are not read: the context is normalized to string keys before evaluation. This is the only opcode that reads a root variable; access and bracket_access operate on a value already on the stack.

• access (execute_access/2, access_value/3) - pops the target, pushes target[property]. A missing key, a property against a list (the compiler only ever emits a binary property, which a list never accepts as an index), or a target that is neither a map nor a list, all push :undefined - never an error. A null target falls into that last case: null.foo is :undefined, not a type error - indexing into a null is not a rule this opcode enforces. An empty stack is EvaluationError insufficient operands.

• compare (execute_compare/2, compare_values/3) - operand is one of GT, LT, EQ, GTE, LTE, NE, STRICT_EQ, STRICT_NE; any other string is an unknown instruction. Pops right then left (stack top is the right operand).

  • :undefined on either side under a non-strict operator (anything except STRICT_EQ/STRICT_NE) pushes :undefined.
  • STRICT_EQ/STRICT_NE are resolved before any type dispatch and work over every value including :undefined. A Date is never strictly equal to a DateTime, since strict equality is Elixir === and the two are different structs.
  • Date/Date and DateTime/DateTime compare chronologically, never by struct-key order; a mixed Date/DateTime pair coerces the Date to 00:00:00 UTC before comparing.
  • Every other pair must be type-matched, where "matched" means both numbers, both booleans, both strings, both lists, or both plain maps (types_match/2). Integer and float are the same type for this purpose, so 1 < 2.0 compares and 1 == 1.0 is true - while STRICT_EQ on that same pair is false, because strict equality does not bridge integer and float. This is the one place the two equality families disagree on numbers, and it is worth a conformance case.
  • A type-mismatched pair under a non-strict operator pushes :undefined - it is not an error. 1 > "a" is :undefined, and so is true == 1.
  • null's four-row matrix: null === undefined is false; null == undefined is :undefined; null === null is true; null == null is :undefined. No new clause implements this - null is not admitted by types_match/2, so every non-strict comparison involving it falls to the type-mismatch catch-all above, and STRICT_EQ/STRICT_NE already work over every value. The rule in one sentence: == and the ordering operators are typed comparisons and null has no type peer, so every non-strict comparison involving null yields :undefined; === is the operator that answers a boolean about null, exactly as it is for :undefined.
  • Ordering on a matched pair, by type:
    • numbers - numeric order.
    • strings - lexicographic by Unicode codepoint, comparing the UTF-8 bytes. Not a locale collation: no case folding, no accent folding.
    • booleans - false < true.
    • lists - element-wise, comparing the first position where the two differ; a proper prefix sorts before the longer list.
    • maps - the Elixir reference implementation orders these by Erlang term order (size first, then sorted keys, then values). A sibling should treat ordering comparisons between two maps as unspecified rather than reproduce that rule; the conformance corpus does not exercise them. EQ/NE/STRICT_EQ/STRICT_NE on two maps are well-defined and portable - only GT/LT/GTE/LTE are not.
  • Fewer than two values on the stack is EvaluationError.

• and, or - retired at ISA v3; never emitted by the compiler. Both operands must be booleans; anything else, including :undefined, is TypeMismatchError with operation logical_and / logical_or and expected type boolean. They do not short-circuit: both operands are already on the stack by the time either opcode runs. This is the semantics a v1 or v2 implementation still has to provide - a sibling declaring either version claims and/or under the interval rule (§1). This build has no execute_instruction/2 clause for them: evaluating a list containing either is refused with reason "retired_opcode", naming ISA v3 and pointing at Predicator.Instructions.upgrade/1, which is the migration ADR-0003 requires (px-tbv.9).

• not (execute_logical_not/1) - boolean required; :undefined, null, or any other type is TypeMismatchError (operation logical_not, expected boolean).

• in (execute_membership/2) - left in right. Either operand :undefined pushes :undefined. The right operand must be a list, else TypeMismatchError (operation in, expected list). Membership uses type-matched equality with chronological date comparison (values_equal?/2), and :undefined is never equal to anything. null is the one place null behaves as a value rather than an absence: values_equal?(nil, nil) is true, so null in [null] is true (and null in [1] is false, matched against nothing) - null does not propagate the way :undefined does. Note the resulting surface tension, deliberate and documented rather than reconciled: null == null is :undefined (above) while null in [null] is true. == and in already disagree about :undefined in the opposite direction (undefined in [undefined] propagates :undefined rather than answering false), so the two operators were never one predicate.

• contains (execute_membership/2) - left contains right. Mirror of in; the left operand must be the list, and the type mismatch is reported against the left operand's type. null on the right behaves as it does under in: identity via values_equal?/2, not propagation.

• add (execute_arithmetic/2) - number+number is numeric addition; string+string, string+number, and number+string concatenate (numbers are stringified); list+list concatenates; Date/DateTime + duration and duration + Date/DateTime do date arithmetic. Anything else, including any :undefined or null operand, is TypeMismatchError (operation add, expected number_or_string).

• subtract (execute_arithmetic/2) - number-number is numeric subtraction; Date-Date yields a duration in days; DateTime-DateTime a duration in seconds; a mixed Date/DateTime pair coerces the Date to UTC midnight first; Date/DateTime - duration does date arithmetic. Else TypeMismatchError (operation subtract, expected number_or_date), null included. Note the asymmetry with add: subtraction does not concatenate strings or lists.

• multiply (execute_arithmetic/2) - numbers only, else TypeMismatchError (expected number) - :undefined and null included.

• divide (execute_arithmetic/2) - the zero check runs before the type check, so a right operand of integer 0 or float 0.0 is EvaluationError "division_by_zero" regardless of the left operand's type. Two integers use truncating integer division; any float operand uses float division. Otherwise TypeMismatchError (expected number), null included.

• modulo (execute_arithmetic/2) - integers only, which is the one place modulo diverges from the other four arithmetic opcodes: a float operand is TypeMismatchError (expected number). A right operand of integer 0 is checked before the type check, as in divide, and is EvaluationError "modulo_by_zero". There is no float-zero clause - unlike divide, a right operand of 0.0 is a TypeMismatchError, not "modulo_by_zero". null is TypeMismatchError, same as any non-integer.

• unary_minus (execute_unary/2) - number required, else TypeMismatchError (expected number) - :undefined and null included.

• unary_bang (execute_unary/2) - boolean required, else TypeMismatchError (expected boolean). Semantically identical to not; the two differ only in which surface operator produced them and in the operation name carried on the error.

• bracket_access (execute_bracket_access/1, access_value/3) - pops the key (stack top), then the target.

  • Against a map: a string, an integer, a boolean, or :undefined indexes it. (The reference implementation writes this as one Elixir clause on is_atom/1, which is also true of true, false, and :undefined; a sibling with no atom type implements the clause as string, integer, boolean, and its own undefined value.) A key of any other type - float, list, map, date, duration - is TypeMismatchError (operation bracket_access, expected string). A missing key pushes :undefined, and an :undefined key is an ordinary miss on any map that does not carry one, not a type error - unlike the list case below.
  • Boolean keys are data, not a type error. A map may legitimately be keyed by true/false (config[true]); the reference implementation's context normalization preserves boolean keys for exactly this reason. m[true] against a map with no true key is an ordinary miss and pushes :undefined, the same as any other missing key - it is not a type rejection that leaked through.
  • Against a list: only a non-negative integer indexes; out-of-range and negative indices push :undefined. Any non-integer key - string, boolean, :undefined, float - is TypeMismatchError (operation bracket_access, expected integer).
  • Against a target that is neither map nor list: :undefined, whatever the key. A null target takes this branch - null["x"] is :undefined, the same treatment as access above.
  • Fewer than two values on the stack is EvaluationError.
  • This bullet, not the ISA version, changed to state the above precisely: the list-with-a-non-integer-key case was previously unspecified here and the reference implementation crashed on it rather than returning an error value, and the boolean-map-key line corrects an earlier erratum in this document rather than describing a behavior change - see §1's versioning rules for why neither warrants a version bump.

• call (execute_function_call/3, call_function/4) - pops arg_count values; the deepest (pushed first) is the first argument. Fewer than arg_count values on the stack is EvaluationError "insufficient_arguments". An unknown function name, an arity mismatch, a function returning {:error, message}, or a function that raises are all EvaluationError with operation function_call. The builtin function set is not part of the ISA table - see Language Reference. A sibling implements call plus whatever functions it chooses to provide; the conformance corpus's functions tier is where that set is pinned.

• object_new (execute_object_new/1) - pushes an empty map. No error path.

• object_set (execute_object_set/2) - pops the value (stack top) and the object beneath it, pushes the object with key set to that value. Fewer than two values on the stack is EvaluationError insufficient operands. A non-map beneath the value is EvaluationError "invalid_stack_value", checked after the stack-depth check. The compiler only ever emits object_set immediately after object_new, so the non-map case is reachable only from a hand-built instruction list - but it is specified, not undefined: a sibling implements it to claim tier 4.

• make_list (execute_make_list/2) - pops count values and pushes them as a list in source order: the stack holds them reversed, deepest first, and this opcode reverses them back. Fewer than count values on the stack is EvaluationError. count of 0 pushes []. The compiler only emits this opcode for a list with at least one non-literal element; an all-literal list compiles to a single ["lit", [...]] instead, which is why v1 siblings can still run most list expressions.

• jump_if_falsy_or_pop (execute_jump_if_falsy_or_pop/2, jump_to/2) - if the stack top is false, null, or :undefined, jump to index + offset, leaving the value on the stack as the result of the expression; if it is exactly true, pop it and fall through to the next instruction; any other value is TypeMismatchError (expected boolean). An empty stack is EvaluationError. Worked example, a AND b: [["load","a"],["jump_if_falsy_or_pop",2],["load","b"]] - if a is falsy, the jump lands past ["load","b"] and a's value is the result; if a is true, it is popped and b's value becomes the result.

• jump_if_true_or_pop (execute_jump_if_true_or_pop/2, jump_to/2) - mirror of jump_if_falsy_or_pop: jump on exactly true, leaving the value on the stack; pop and fall through on false, null, or :undefined; anything else is TypeMismatchError. Worked example, a OR b: [["load","a"],["jump_if_true_or_pop",2],["load","b"]]. State the ECMAScript alignment explicitly: undefined AND x short-circuits to :undefined without evaluating x, while undefined OR x falls through and takes x's value.

• duration (execute_duration/2) - pushes a duration map built from the operand's unit pairs. Accepted unit strings, all of them: y/year/years, mo/month/months, w/week/weeks, d/day/days, h/hour/hours, m/min/minute/minutes, s/sec/second/seconds, ms/millisecond/milliseconds. Later pairs overwrite earlier ones naming the same unit. An unrecognized unit string is EvaluationError "invalid_duration_unit"; a pair that is not [integer, string] is EvaluationError "invalid_duration_format".

• relative_date (execute_relative_date/2) - pops a duration map, pushes a DateTime. "ago" and "last" subtract the duration from the current time; "future" and "next" add it. Any other direction string is EvaluationError "invalid_direction"; a non-map on top of the stack is EvaluationError "invalid_stack_value"; an empty stack is EvaluationError insufficient operands. The result depends on the current time - it reads the system clock at evaluation time - so a conformance case exercising it cannot pin an exact expected value.

• store (execute_store/2) - pops the value from the stack top, then n location segments beneath it, and reverses those n into root-first path order: the compiler pushes segments root-to-leaf followed by the value, so the stack holds the segments deepest-first, exactly as make_list does. Writes path -> value into the evaluator's context via the same write algorithm Predicator.ContextLocation.put/3 implements: a missing, null, or :undefined interior slot is auto-vivified as a list when the next segment is an integer and a map otherwise - writing through a null intermediate vivifies it exactly as it would an :undefined one, deliberately: "you cannot index into a null" is not a rule this ISA enforces anywhere else (access/bracket_access above agree - a null target is an ordinary miss, not a type error). An integer past a list's end pads with :undefined, and the leaf is always overwritten. Pushes nothing. Fewer than n + 1 values on the stack is EvaluationError insufficient operands. A segment that is neither a string nor an integer is TypeMismatchError (operation store, expected string, the message naming string and integer as the accepted segment types), the mirror of bracket_access's key rule. A write that cannot be performed is EvaluationError with reason not_assignable (empty path, only reachable from a hand-built ["store", 0]), not_a_container (an interior segment holds a scalar), or invalid_index (a negative list index). This is the only opcode that writes the context. A host that supplied a protected-root list (the :protected_roots evaluation option) gets EvaluationError "protected_root" when the path's root segment is in it, checked after segment-type validation and before the write, so a refused write leaves no partial write behind. This is host policy, not an ISA rule - see §2.

• pop (execute_pop/1) - discards the stack top and pushes nothing. The statement-boundary opcode: the compiler emits it after every expression statement so the next statement starts from a clean stack. An empty stack is EvaluationError insufficient operands. It is unrelated to jump_if_falsy_or_pop/jump_if_true_or_pop, which pop conditionally as part of a jump. Non-normative: this implementation additionally retains the discarded value in the evaluator's own state, which is how Predicator.execute_value/2 reports the last expression statement's value; the stack effect, the error, and everything else a conforming implementation must reproduce are unchanged, and a sibling need not retain anything.

• cast (execute_cast/2, Predicator.Cast.cast/2) - pops the stack top, converts it to the named type, pushes the result. The operand must be one of the seven scalar type names below; any other value is unknown_instruction, the standing malformed-operand rule (ADR-0011) - cast has no other error path. An empty stack is EvaluationError insufficient operands. This subsection is the normative conversion matrix: a sibling claiming ISA v4 implements exactly it.

  Two rules generate every cell:

  1. :undefined propagates: cast(:undefined, _type) is :undefined for every target.
  2. cast is total over values: a conversion that cannot produce a value of the target type pushes :undefined, never an error. The type name itself already failed at parse time if it was invalid; what remains at evaluation time is the data's half, and data problems go soft here, as at a compare mismatch or an access miss.

  null::T is :undefined for every target T, via rule 2, not rule 1: null is not :undefined and does not propagate the way it does - a null simply cannot produce a value of any target type, the same total failure a list or a map hits below. null::string is :undefined, not "null". A cast is an explicit request for a typed value, and losing the null/undefined distinction across one is the correct, accepted cost.

  The seven scalar type names are integer, float, string, boolean, date, datetime, duration (§3). = is identity, a word names a conversion, - is :undefined:

  source \ target	integer	float	string	boolean	date	datetime	duration
  integer	=	widen	format	-	-	-	-
  float	truncate	=	format	-	-	-	-
  string	parse	parse	=	parse	parse	parse	parse
  boolean	-	-	format	=	-	-	-
  date	-	-	format	-	=	midnight UTC	-
  datetime	-	-	format	-	calendar date	=	-
  duration	-	-	format	-	-	-	=
  list	-	-	-	-	-	-	-
  map	-	-	-	-	-	-	-
  null	-	-	-	-	-	-	-
  :undefined	-	-	-	-	-	-	-

  Numeric conversions.

  • integer::float widens to the nearest representable double, which is exact up to 2^53 and rounds beyond it: (2^53+1)::float is 2^53. Siblings agree, because a 53-bit mantissa is what their host float types have too, but the conversion is not lossless and a round trip through float is not identity for a large integer.
  • float::integer truncates toward zero. PostgreSQL rounds here; this diverges deliberately, because truncation is what Elixir trunc, JavaScript Math.trunc, and Ruby to_i all do natively, and matching the siblings' host languages is worth more than matching PG's tie-breaking.

  String parses. Each parse accepts the whole string or yields :undefined; no trimming, no partial consumption, no locale forms.

  • ::integer - an optionally-negated decimal integer (-?[0-9]+).
  • ::float - an optionally-negated decimal number with an optional fraction (-?[0-9]+(\.[0-9]+)?); "3"::float is 3.0. No exponent form, matching the language's own float literal grammar.
  • ::boolean - exactly "true" or "false", case-sensitive.
  • ::date - ISO 8601 calendar date (2026-08-09).
  • ::datetime - ISO 8601 datetime with a UTC offset, normalized to UTC. A date-only string is :undefined here; the supported spelling is s::date::datetime.
  • ::duration - the language's own duration-literal grammar, a sequence of [0-9]+(\.[0-9]+)?<unit> pairs ("1d2h30m", "1.5s"). A number may carry a decimal fraction; there is no bare fraction (".5s") and no trailing dot ("1.s"). A fractional component must convert to an exact whole number of milliseconds or the whole string is :undefined - a sub-millisecond remainder ("0.5ms") is rejected, never rounded or truncated. A valid fraction expands to the integer part on its own unit plus a remainder decomposed largest-first through d, h, m, s, ms only, never back into w, mo, or y. Fractions are permitted on every unit; mo and y fractions commit this document's 30-day and 365-day approximations at parse time, so "0.5mo"::duration has days: 15 and no months component. Repeated units accumulate, expansions included. This bullet, not the ISA version, changed to state the widened grammar precisely - see §1's versioning rules for why: no operand form carried in the instruction list moves, and a string moving from the unparseable set to the parseable set is the monotone widening cast's :undefined failure mode was built to absorb.

  String formats (::string).

  • integer - decimal.
  • float - the shortest round-trip decimal. Shortest-round-trip printing is a known cross-language hazard, so the conformance corpus pins values chosen to format identically across languages.
  • boolean - "true" / "false".
  • date - ISO 8601 calendar date (2026-08-09).
  • datetime - ISO 8601 in UTC with Z, and the fractional-seconds field is normative: omitted entirely when the sub-second component is zero (2026-08-09T12:00:00Z), and exactly six digits when it is not (2026-08-09T12:00:00.500000Z). Never any other digit count, and never a zero fraction spelled out. Sub-second precision is microseconds - the ::datetime parse truncates digits past the sixth - so the field is stated in terms of the instant, not in terms of any host type's precision or scale field. dt::string::datetime preserves the instant, but s::datetime::string is a canonicalization rather than a string identity: "…:00.5Z" returns as "…:00.500000Z", and a seventh digit is gone.
  • duration - the duration-literal grammar, largest unit first, zero components omitted, "0s" when all components are zero, so d::string::duration round-trips.
  • Lists and maps are -: serialization is JSON.stringify's job, not a cast's.

  The date/datetime bridge.

  • date::datetime is midnight UTC - the same coercion compare and subtract already apply to a mixed pair.
  • datetime::date is the datetime's calendar date.

  No boolean/number bridge. 1::boolean and true::integer are :undefined. The ISA has no truthiness rule (§2) and compare refuses to bridge booleans and numbers; casts do not open a side door.

• jump (jump_to/2) - unconditional jump to index + offset. Pops nothing, pushes nothing. No error path beyond the standing malformed-operand rule (a non-integer or non-positive offset falls through to unknown_instruction). Statement-level control flow's only unconditional jump - if/else uses it to skip the else branch once the if branch has run. Worked example, if c { A } else { B }: c; ["pop_jump_if_falsy", lenA + 2]; A; ["jump", lenB + 1]; B - after A runs, jump skips past B to the instruction following it.

• pop_jump_if_falsy (execute_pop_jump_if_falsy/2, jump_to/2) - pops the stack top always. If the popped value is false, null, or :undefined, jump to index + offset; if it is exactly true, fall through to the next instruction; any other value is TypeMismatchError (expected boolean). An empty stack is EvaluationError insufficient operands.

  Contrast with jump_if_falsy_or_pop: that opcode pops only on the fall-through branch and leaves the value on the stack on the taken branch, because it exists to make a AND b yield a as the expression's result. pop_jump_if_falsy pops unconditionally - a statement's condition is never a result, so there is nothing to preserve, and leaving it behind would strand a value on the stack for the following statement to trip over. CPython draws the same distinction between JUMP_IF_FALSE_OR_POP and POP_JUMP_IF_FALSE, and this opcode is the latter's counterpart, not the former's.

  Worked example, if c { A } (no else): c; ["pop_jump_if_falsy", lenA + 1]; A - a falsy c jumps past A entirely; A's length plus one lands on the instruction after A. Worked example, if c { A } else { B } (continuing the jump example above): a falsy c jumps over both A and the trailing jump, landing on B's first instruction, lenA + 2 past the pop_jump_if_falsy itself.

• jump_backward (execute_jump_backward/2, jump_backward_to/2) - the one back edge in the ISA (ISA v6, ADR-0013). Unconditional jump to index - offset. Pops nothing, pushes nothing. A non-integer offset, a non-positive offset, or a target before index 0 is unknown_instruction, the standing malformed-operand rule (§2).

  The opcode has its own name rather than being a negative jump offset deliberately: it keeps opcode-name scanning a sound version check, and the absence of jump_backward in a list remains a termination proof - a list without it still halts in at most length(program) steps, since every other jump is forward-only (§2).

  Every execution of a back edge charges a per-execution loop budget (§2). On exhaustion, the instruction returns an EvaluationError with reason "loop_budget_exceeded", carrying the jump_backward instruction's own source position - the same position-attachment every other opcode's error gets, with no special-case plumbing.

  Worked example, while c { A }: c; ["pop_jump_if_falsy", lenA + 2]; A; ["jump_backward", lenC + lenA + 1]

  • the pop_jump_if_falsy skips past A and the trailing jump_backward once c goes falsy (the +2); the jump_backward at the end targets the condition's first instruction, lenC instructions before A began, so its offset counts both lenC and lenA.

6. Not in the ISA

What a reader might expect to find here and will not:

• Source positions and spans - these travel in an Elixir-side side table, never serialized as part of the instruction list. See docs/reference/ast.md for the blame-token and span tables, and docs/reference/language.md's "Error Shapes" for how they surface on an error.
• Surface syntax, including the = grammar break (ADR-0002). Both = and == compile to ["compare", "EQ"], so no instruction-level divergence exists between them: the difference is a parse error in expression position and an assignment in statement position, entirely at the parser layer, and it is outside the conformance corpus's scope. The undefined literal keyword is the same shape: it compiles to the existing ["lit", :undefined], an instruction this ISA's value domain (§3) already admitted, so the new spelling attaches to no opcode name and moves no version. The null literal keyword is the same shape again: null compiles to the existing ["lit", nil], an operand §3's value domain already admitted, so this spelling too attaches to no opcode name and moves no version.
• The builtin function set - see Language Reference.
• A serialization envelope. Four of §3's value types cannot round-trip through plain JSON, and choosing what to do about that is the consumer's call, not the ISA's - see "Crossing a plain-JSON boundary" in §3 for the four types and for the two approaches that work.
• Absolute jumps. Every jump in the ISA is relative. Backward jumps entered at v6 as exactly one opcode, jump_backward - see §5.

7. Version history

This table records the release each opcode was introduced in, and, now that an opcode has been retired, the release each was removed in - both ends of the interval §1 defines. A version whose only change is a retirement still gets a row here. A version's semantics can also be refined in a later release without a new opcode and without a new ISA version - 3.8.0 did exactly that to v2, as noted in §1.

ISA v1 is defined as the full opcode set the Elixir evaluator accepted before ADR-0001. A sibling declaring v1 support is claiming that whole set; where a sibling falls short of it, the sibling publishes that fact in its own repository. No support matrix is maintained here (ADR-0003).

8. Conformance corpus

This document specifies the ISA in prose; conformance/README.md is its executable form - a checked-in, language-neutral JSON corpus a sibling runs its compiler and evaluator against, tier by tier, without an Elixir toolchain (px-35i.4, ADR-0003). Read it before implementing against a tier or adding a case. conformance/RATCHET.md is the companion format a sibling uses to record and defend its conformance claim over time (px-35i.8).

The corpus's scope boundary matches this document's: it does not cover surface syntax (§6 - = and == compile identically, so a source-level test would encode a divergence that does not exist) and it does not cover parse or lexer errors (every authored case's source, when present, compiles successfully). Coverage here means the instruction layer this document specifies, nothing above it.