The opcode map
You will learn
Which of the 256 opcode bytes mean something, and what the rest do.
Of 256 byte values, 47 are TRI-27 opcodes, from NOP and LD through ADD, JMP and HALT to SYSCALL. The other 209 are not errors to the emulator: decode_opcode() reads an unknown byte as NOP, so decoding never fails. The lesson spec, t27a_mnemonics.t27, gives the t27a assembler a strict decoder that refuses those bytes instead.
Try it
Find the opcode bytes of ADD and HALT; then press an unlit byte and say why a strict decoder is safer for an assembler.
Every byte from 0 to 255 as a cell; green ones are TRI-27 opcodes. Press a byte: an undefined one decodes as NOP, decoding never fails.
specs/isa/t27a_mnemonics.t27
// SPDX-License-Identifier: Apache-2.0
; specs/isa/t27a_mnemonics.t27 -- the t27a mnemonic table and a strict decoder for the 47 TRI-27
; opcodes (gHashTag/t27#6516, epic #6488; theorems T735-T736 in
; specs/compiler/theory/isa_round_trip.t27).
; One table, two directions. The assembler reads it as table index -> opcode byte (opcode_at), the
; disassembler as opcode byte -> table index (index_of). Both walk the same order as OPCODE_VALUES
; and OPCODE_NAMES in specs/isa/ternary_encoding.t27, so index i names OPCODE_NAMES[i] and encodes
; as OPCODE_VALUES[i]. The functions are written as if-chains over the OP_ constants of that spec,
; not as array indexing, so the C and Verilog backends lower them without a table in memory.
; Why a strict decoder. decode_opcode in specs/isa/ternary_encoding.t27 follows the pinned Trinity
; decoder: an undefined byte decodes as NOP and decoding never fails (UNKNOWN_OPCODE_RULE). That is
; right for the emulator and wrong for a disassembler: 209 of the 256 bytes are not opcodes, and a
; listing built on decode_opcode prints them as NOP (T735, last paragraph). strict_decode returns
; the byte for a defined opcode and INVALID_OPCODE (256, outside the byte range) for every other
; byte, so garbage cannot be mistaken for a NOP. decode_opcode is not changed; it is called below
; only as the negative control.
; ASCII only (L3).
; phi^2 + 1/phi^2 = 3 | TRINITY
module T27aMnemonics;
use isa::ternary_encoding;
pub const INVALID_OPCODE : u32 = 256;
pub const NO_INDEX : u32 = 47;
pub const BYTE_VALUES : u32 = 256;
pub const UNDEFINED_BYTES : u32 = 209;
; Table index 0..46 -> opcode byte, in the order of OPCODE_VALUES. Any other index -> 256.
pub fn opcode_at(i: u32) -> u32 {
if (i == 0) { return OP_NOP; }
if (i == 1) { return OP_LD; }
if (i == 2) { return OP_ST; }
if (i == 3) { return OP_LDI; }
if (i == 4) { return OP_STI; }
if (i == 5) { return OP_MOV; }
if (i == 6) { return OP_ADD; }
if (i == 7) { return OP_SUB; }
if (i == 8) { return OP_MUL; }
if (i == 9) { return OP_DIV; }
if (i == 10) { return OP_INC; }
if (i == 11) { return OP_DEC; }
if (i == 12) { return OP_EXP; }
if (i == 13) { return OP_SIN; }
if (i == 14) { return OP_AND; }
if (i == 15) { return OP_OR; }
if (i == 16) { return OP_XOR; }
if (i == 17) { return OP_NOT; }
if (i == 18) { return OP_SHL; }
if (i == 19) { return OP_SHR; }
if (i == 20) { return OP_STR_LOAD; }
if (i == 21) { return OP_STR_CONCAT; }
if (i == 22) { return OP_STR_PRINT; }
if (i == 23) { return OP_FILE_READ; }
if (i == 24) { return OP_FILE_WRITE; }
if (i == 25) { return OP_FILE_EXISTS; }
if (i == 26) { return OP_JMP; }
if (i == 27) { return OP_JZ; }
if (i == 28) { return OP_JNZ; }
if (i == 29) { return OP_CALL; }
if (i == 30) { return OP_JGT; }
if (i == 31) { return OP_JLT; }
if (i == 32) { return OP_RET; }
if (i == 33) { return OP_HALT; }
if (i == 34) { return OP_DOT; }
if (i == 35) { return OP_BIND; }
if (i == 36) { return OP_BUNDLE2; }
if (i == 37) { return OP_BUNDLE3; }
if (i == 38) { return OP_PHI_CONST; }
if (i == 39) { return OP_PI_CONST; }
if (i == 40) { return OP_E_CONST; }
if (i == 41) { return OP_SACR; }
if (i == 42) { return OP_LD_IMM; }
if (i == 43) { return OP_ADD3; }
if (i == 44) { return OP_SUB3; }
if (i == 45) { return OP_CMP3; }
if (i == 46) { return OP_SYSCALL; }
return INVALID_OPCODE;
}
; Opcode byte -> table index 0..46, the inverse of opcode_at. An undefined byte -> 47.
pub fn index_of(op: u32) -> u32 {
if (op == OP_NOP) { return 0; }
if (op == OP_LD) { return 1; }
if (op == OP_ST) { return 2; }
if (op == OP_LDI) { return 3; }
if (op == OP_STI) { return 4; }
if (op == OP_MOV) { return 5; }
if (op == OP_ADD) { return 6; }
if (op == OP_SUB) { return 7; }
if (op == OP_MUL) { return 8; }
if (op == OP_DIV) { return 9; }
if (op == OP_INC) { return 10; }
if (op == OP_DEC) { return 11; }
if (op == OP_EXP) { return 12; }
if (op == OP_SIN) { return 13; }
if (op == OP_AND) { return 14; }
if (op == OP_OR) { return 15; }
if (op == OP_XOR) { return 16; }
if (op == OP_NOT) { return 17; }
if (op == OP_SHL) { return 18; }
if (op == OP_SHR) { return 19; }
if (op == OP_STR_LOAD) { return 20; }
if (op == OP_STR_CONCAT) { return 21; }
if (op == OP_STR_PRINT) { return 22; }
if (op == OP_FILE_READ) { return 23; }
if (op == OP_FILE_WRITE) { return 24; }
if (op == OP_FILE_EXISTS) { return 25; }
if (op == OP_JMP) { return 26; }
if (op == OP_JZ) { return 27; }
if (op == OP_JNZ) { return 28; }
if (op == OP_CALL) { return 29; }
if (op == OP_JGT) { return 30; }
if (op == OP_JLT) { return 31; }
if (op == OP_RET) { return 32; }
if (op == OP_HALT) { return 33; }
if (op == OP_DOT) { return 34; }
if (op == OP_BIND) { return 35; }
if (op == OP_BUNDLE2) { return 36; }
if (op == OP_BUNDLE3) { return 37; }
if (op == OP_PHI_CONST) { return 38; }
if (op == OP_PI_CONST) { return 39; }
if (op == OP_E_CONST) { return 40; }
if (op == OP_SACR) { return 41; }
if (op == OP_LD_IMM) { return 42; }
if (op == OP_ADD3) { return 43; }
if (op == OP_SUB3) { return 44; }
if (op == OP_CMP3) { return 45; }
if (op == OP_SYSCALL) { return 46; }
return NO_INDEX;
}
; The byte itself for one of the 47 opcodes; INVALID_OPCODE (256) for the 209 other bytes.
pub fn strict_decode(byte: u32) -> u32 {
if (index_of(byte) < OPCODE_COUNT) { return byte; }
return INVALID_OPCODE;
}
pub fn is_valid(decoded: u32) -> bool {
return decoded != INVALID_OPCODE;
}
invariant the_bytes_split_into_opcodes_and_rejects {
assert OPCODE_COUNT + UNDEFINED_BYTES == BYTE_VALUES;
assert NO_INDEX == OPCODE_COUNT;
assert INVALID_OPCODE == BYTE_VALUES;
}
; T736 for the table: index_of is a left inverse of opcode_at on every index 0..46.
test index_of_inverts_opcode_at_for_all_47 {
var i : u32 = 0;
var ok : u32 = 0;
while (i < OPCODE_COUNT) {
if (index_of(opcode_at(i)) == i) { ok = ok + 1; }
i = i + 1;
}
assert ok == 47;
assert opcode_at(47) == INVALID_OPCODE;
assert opcode_at(1000) == INVALID_OPCODE;
}
; The if-chain walks the same order as OPCODE_VALUES, strictly increasing, so no byte is listed twice.
test opcode_at_follows_opcode_values {
var i : u32 = 0;
var same : u32 = 0;
var rising : u32 = 0;
while (i < OPCODE_COUNT) {
if (opcode_at(i) == OPCODE_VALUES[i]) { same = same + 1; }
if (i > 0) {
if (opcode_at(i) > opcode_at(i - 1)) { rising = rising + 1; }
}
i = i + 1;
}
assert same == 47;
assert rising == 46;
assert opcode_at(0) == OP_NOP;
assert opcode_at(46) == OP_SYSCALL;
}
; The other direction: opcode_at inverts index_of on every defined byte, and every undefined byte
; has no index.
test opcode_at_inverts_index_of_on_defined_bytes {
var b : u32 = 0;
var back : u32 = 0;
var no_index : u32 = 0;
while (b < BYTE_VALUES) {
var k : u32 = index_of(b);
if (k < OPCODE_COUNT) {
if (opcode_at(k) == b) { back = back + 1; }
} else {
if (k == NO_INDEX) { no_index = no_index + 1; }
}
b = b + 1;
}
assert back == 47;
assert no_index == 209;
}
; Exactly 47 bytes decode, exactly 209 are rejected, and the accepted set is is_defined_opcode.
test strict_decode_accepts_47_and_rejects_209 {
var b : u32 = 0;
var accepted : u32 = 0;
var rejected : u32 = 0;
var agree : u32 = 0;
while (b < BYTE_VALUES) {
var d : u32 = strict_decode(b);
if (d != INVALID_OPCODE) {
accepted = accepted + 1;
if (d == b) { agree = agree + 1; }
} else {
rejected = rejected + 1;
}
if (is_valid(d) != is_defined_opcode(b)) { agree = 0; }
b = b + 1;
}
assert accepted == 47;
assert rejected == 209;
assert agree == 47;
}
; Negative control: the emulator's decoder reads byte 1 as NOP; the strict decoder rejects it, and
; still accepts the real NOP byte 0.
test undefined_byte_is_rejected_not_nop {
assert decode_opcode(1) == OP_NOP;
assert strict_decode(1) == INVALID_OPCODE;
assert is_valid(strict_decode(1)) == false;
assert strict_decode(OP_NOP) == OP_NOP;
assert is_valid(strict_decode(OP_NOP));
assert strict_decode(70) == INVALID_OPCODE;
assert strict_decode(137) == INVALID_OPCODE;
assert strict_decode(255) == INVALID_OPCODE;
assert strict_decode(OP_HALT) == OP_HALT;
assert index_of(1) == NO_INDEX;
}
All lessons
Module 1 · Three values
Why three, how balanced ternary writes every number without a sign, and what flipping and cutting trits do.
Module 2 · Logic with unknown
Kleene's three-valued gates, two gates binary has no twin for, and addition as a pair of tables.
Module 3 · Adding trits
The half adder, the full adder and a carry that ripples left, one place at a time.
Module 4 · Multiplying without a multiplier
Copy, drop or flip: a product by one trit, long multiplication, and a MAC that only adds.
Module 5 · Trits in binary memory
Two bits per trit, five trits per byte, and the bits a 27-trit word needs.
Module 6 · The TRI-27 instruction word
The 32-bit word the Trinity emulator decodes: its fields, its 47 opcodes and its 15-bit immediate.
Module 7 · A ternary machine
An ALU built from this course's adders, a three-way jump, and a program you can step.
Module 8 · Three answers
Compare at the highest differing trit, find a number in thirds, sort with three-way compares.
Module 9 · Ternary neurons
Weights of -1, 0, +1: one neuron, a detector and a small layer, with no multiplier anywhere.