Skip to content

Add TRI-27 machine, bytecode, encoding, VSA VM and C ABI specs (S05 of trinity#988) - #3581

Merged
gHashTag merged 1 commit into
gHashTag:masterfrom
dmitrii-f-t27:spec/trinity-s05-vm-abi
Sep 12, 2026
Merged

gHashTag merged 1 commit into
gHashTag:masterfrom
dmitrii-f-t27:spec/trinity-s05-vm-abi

Conversation

@dmitrii-f-t27

@dmitrii-f-t27 dmitrii-f-t27 commented Sep 12, 2026 •

Copy link
Copy Markdown
Collaborator

Closes #3567 -- work package S05 of gHashTag/trinity#988: VM, TRI-27 bytecode and host ABI behaviour. S01-S04 (#3577-#3580) were merged into master on 2026-09-12 and this branch sits on top of them, so the diff is S05 alone; it touches specs/isa/, specs/vm/, specs/api/, three S01 cards, conformance/trinity/, tools/, docs/now/, README and OWNERS.

What

The consumer has two virtual machines and one C boundary. The issue asks for the actual selected runtime: for TRI-27 that is src/tri27/emu/decoder.zig + executor.zig + loader.zig at 976df517 -- the only path the owner's tests drive (test_comprehensive, test_golden, smoke_tests); for the VSA VM it is src/vm.zig; for the ABI it is src/c_api.zig. Five specs state them rule by rule, every decision a function the C backend executes:

  • specs/isa/ternary_encoding.t27 (module Tri27Encoding, KIND = "isa-encoding") -- rewritten in place. Until today a 38-line algorithm block that did not parse (in specs_generate_baseline.txt) and was the CANONICAL_SPEC of the whole TRI-27 toolchain. Now: the forty-seven opcodes of decoder.zig with values, the three field layouts (opcode 7:0, dst 12:8, src1 at 13, src2 at 18, immediate 31:17), the fifteen-bit immediate and its sign extension and clamp, the four-bit src1 of the immediate form, unknown opcode is NOP, BUNDLE3's third register in bits 27:23, and two rules the owner never wrote down: DOT, BIND, BUNDLE2 cannot carry src2 (it decodes as t0) and SACR cannot carry its mode (every decoded SACR adds). Six findings: the five other layouts in the tree (encoder_simple.zig / asm_parser.zig behind tri tri27 assemble, tbin_format.md, t27_format.md, tri27/README.md, the emit_zig template). 11 tests.
  • specs/isa/tri27_machine.t27 (Tri27Machine, KIND = "isa-machine") -- executor.zig with cpu_state.zig, tri_cpu.zig, tri_memory.zig: 27 i64 registers (not trits, not 27 trits), 19683 eight-byte words read four bytes at a time at pc * 4, the two entry profiles (pc 3, sp 0 by CPUState.init + memcpy: every owner test and tri tri27 run; pc 0, sp 19682 by loader.load), flags Z/N/V/H with V never written, the numeric rule of every executed opcode (no reduction for ADD..DEC, SHL, SHR, logic, EXP, SIN; modulo 3^9 = 19683 for DOT, BIND, SACR; BUNDLE2 truncates; BUNDLE3 majority), CALL/RET, the silent halts, the 100000-instruction budget, the seven declared errors (two never returned), twelve status codes of the spec's own numbering (the owner's error set has no ordinals; halted is 0, everything else nonzero), the tri exit codes, the host boundary (SYSCALL is a no-op; file and string I/O are opcodes that open guest-memory paths through std.fs.cwd(), unsandboxed, absolute paths only). Fifteen findings. 10 tests, 5 invariants.
  • specs/isa/tri27_bytecode.t27 (Tri27Bytecode, KIND = "isa-bytecode") -- the .tbin container of loader.zig: six-byte header (magic 0x54524932, version 1, count), CODE/CONSTANTS/DATA/BSS, every rejection in the loader's order (Truncated, InvalidMagic, InvalidVersion, InvalidSection, DataTooLarge, SectionMissing; CorruptHeader never), where the code lands (eight-byte words from word 3), what the loader leaves (pc 0, sp 19682). Eight findings. 6 tests, 4 invariants.
  • specs/vm/trinity_vm.t27 (TrinityVsaVm, KIND = "vm-contract") -- src/vm.zig: twenty-six opcodes numbered by declaration order (no explicit values), v0..v3 over S04's operations, s0/s1, f0..f3, two f16 accumulators, a register index above 3 aliases v0, step/run rules, condition codes at a tenth, v_random discards its seed, v_bundle3 uses dst as third source, no budget, no serialized form, forty sacred opcodes with six implemented and reachable only through execSacredOpcode. CI evidence as it is: zig test src/vm.zig fails to compile on every push to main (run 34678824259). specs/server/vm.t27 is cited (same names, no numbers, does not parse). 5 tests.
  • specs/api/c_abi.t27 (TrinityCAbi, KIND = "host-abi") -- src/c_api.zig: the twenty-two exports with C prototypes, ownership (every handle the caller frees; two caller buffers; one static string), NULL rules, no error channel, an opaque handle over a struct that is not ABI-stable, the header and its wrong install path. Eight findings, the first: the source does not parse at the pin (trinity_vsa_set_trit opens if (value > 0) { twice, :255-256), so the libraries and the fifteen tests do not build. 4 tests.

tools/trinity_tri27.py -- vectors assembles twenty-two programs in the decoder's layout into tri_asm.zig's container (or a loader-native one) and runs them through a Python model of the three files, writing conformance/trinity/tri27_programs.json with words, container, final registers, flags, memory changes, status and a bounded trace (32 steps); plus eighteen loader vectors (every rejection rule, every accepted shape). run generates the three specs to C, links them into a driver that owns the arrays and the loops and calls the specs for every decision, and replays. check holds the record to the specs and the model (constants, vectors, replay hashes). --self-check plants a wrong expected register (fails exactly its vector), a rejection declared as acceptance, a BIND without its zero identity (fails only the vector that binds a zero to a negative value) and a wrong sign bit (fails only the negative-immediate vectors).

tools/trinity_c_abi.py check --trinity-root -- holds the ABI table to the header and to the export fn lines (names, arity, prototypes), compiles conformance/trinity/abi/abi_fixture.c against the header (cc -fsyntax-only), and with --zig records zig ast-check on the source; --self-check plants a missing prototype, an arity change, a changed return type and a fixture with the wrong arity.

Also: the S01 cards abi.c-api, tri27.toolchain, lib.trinity name their canonical specs (dialect t27); specs/OWNERS.md extends isa/ and adds vm/ and api/ rows (owner labels are proposals); tools/specs_generate_baseline.txt loses the encoding stub; the stub's three stale seals go, five new seals come; tools/published_figures.py: test blocks 12673 -> 12709, pub const OP_* 11 -> 60; docs/now entry; README section and rows.

Measured (2026-09-12)

  • Five specs on C: 11 + 10 + 6 + 5 + 4 tests pass; gen, gen-rust, gen-verilog exit 0; seals verify.
  • Replay: 40 of 40 vectors pass (22 programs, 18 loader) with t27c 0.2.0 and Apple clang 21; traces match step for step.
  • Eight programs end with a nonzero status, deterministically: invalid register (status 1, refused before it counts as executed), invalid opcode ADD3 (6), division by zero (3), the stack guard after loader.load (4), a fetch past memory (8), RET on an empty stack (10), the budget (9), host I/O (11, not replayed).
  • ABI: 22 of 22 functions agree across spec, header and source; the fixture compiles against the header; zig ast-check (0.15.2) rejects src/c_api.zig at the pin, as the spec says.
  • What the replay found in the owner (recorded as findings, with vectors): CALL pushes its own address and RET returns to it, so every subroutine call loops until the budget (call-never-returns: 100000 instructions, t5 = 33333); loader.load writes eight-byte words while run fetches four-byte units (loader-entry: six NOPs, then the code with a NOP between instructions), and reads a tri_asm.zig container two bytes early (load-good vs load-native); the CONSTANTS section's id byte is read as its count (load-constants-documented-layout is rejected); no encodable LD/ST/STI can leave memory.

Verification

python3 tools/trinity_tri27.py --self-check                                   ok (16 checks)
python3 tools/trinity_tri27.py vectors / run / check                          40/40, 0 findings
python3 tools/trinity_c_abi.py --self-check                                   ok (6 checks)
python3 tools/trinity_c_abi.py check --trinity-root <clone> --zig <0.15.2>    0 findings
python3 tools/trinity_manifest.py check                                       OK (50 cards)
t27c seal --verify (five specs, three cards)                                  all hashes MATCH
check_seal_currency/coverage, specs_generate, duplicate_declarations, duplicate_agreement, assertionless,
json_parses, devhome, documented_commands, conflict_markers, catalog count/integrity, damage_negatives --require,
ring_spec_drift, elab_ratchet, vector_data, gate_preconditions, published_figures, status tables, untrusted interp,
now-sync + now-entry shape (as PR), t27c validate-conformance (108/108)         exit 0
t27c ci --repo-root .                                                          114 issues, all pre-existing (115 on master; the encoding stub was one)

The red test-ratchet, if it appears, is pre-existing on master since 2026-09-08 (the same 23 Rust tests; see #3580).

What this does not claim

  • That any of this ran on the owner's Zig: the emulator has no build target, emu/main.zig, emit_zig_test.zig and tri27_cli_simple.zig do not parse, and no Zig on this host builds the tree. The reading is checked against the owner's own test expectations where they exist (owner_test on the vectors) and against an independent model.
  • That the string and file opcodes, cpu.f, the vector registers or SACR modes 2..4 are replayed; that the VSA VM's programs are replayed (its operations are S04's 149 vectors); or that the C ABI is verified across a linked boundary -- the library does not parse at the pin.
  • That registers.t27, ternary_control_flow.t27 or ternary_memory.t27 are wrong: they describe a machine the consumer does not run, and are cited, not copied. Reconciling them with the emulator, or fixing the emulator, is a decision for the owners.
  • No hardware is involved; every result is emulation of a specification and is labeled so.

Do not merge without the owner's approval.

🤖 Generated with Claude Code

specs/isa/ternary_encoding.t27 (module Tri27Encoding, KIND "isa-encoding") is
rewritten from a 38-line block that did not parse into the instruction word of
gHashTag/trinity src/tri27/emu/decoder.zig at 976df517: forty-seven opcodes with
values, three field layouts, the fifteen-bit immediate and its sign extension,
the four-bit src1 of the immediate form, unknown opcode is NOP, and the rules the
owner never wrote down (DOT, BIND, BUNDLE2 cannot carry src2; SACR cannot carry
its mode). specs/isa/tri27_machine.t27 (Tri27Machine, "isa-machine") states
executor.zig with cpu_state.zig: registers, memory, fetch, both entry profiles,
flags, the numeric rule of every executed opcode, stack, budget, errors, twelve
status codes of the spec's own, the tri exit codes, the host boundary, and
fifteen findings (CALL/RET is an endless loop; loader.load writes eight-byte
words while run fetches four-byte units; 3^27 written where 3^9 is computed).
specs/isa/tri27_bytecode.t27 (Tri27Bytecode, "isa-bytecode") states the .tbin
container of loader.zig with every rejection in order and eight findings (the
writer's twelve-byte header is read two bytes early; the CONSTANTS id byte is
read as its count). specs/vm/trinity_vm.t27 (TrinityVsaVm, "vm-contract") states
the VSA VM of src/vm.zig: twenty-six opcodes by declaration order, registers,
step and run, condition codes, no budget, no serialized form, the sacred opcode
space, and its CI evidence (zig test src/vm.zig fails to compile on main).
specs/api/c_abi.t27 (TrinityCAbi, "host-abi") states the twenty-two C exports
of src/c_api.zig with prototypes, ownership and NULL rules, and that the source
does not parse at the pin.

tools/trinity_tri27.py: vectors assembles twenty-two golden programs in the
decoder's layout and runs them through a Python model of the three files,
writing conformance/trinity/tri27_programs.json with final state, status and a
bounded trace, plus eighteen loader vectors; run generates the three specs to C,
links them into a driver that owns the arrays and loops and calls the specs for
every decision, and replays: 40 of 40 pass; eight programs end nonzero (invalid
register, invalid opcode, division by zero, stack guard, fetch past memory, RET
underflow, budget, host I/O not replayed). check holds the record to the specs
and the model; --self-check plants a wrong register, an accepted rejection, a
BIND without its identity and a wrong sign bit.

tools/trinity_c_abi.py check --trinity-root holds the ABI table to the header
and to the export lines (22 of 22 agree), compiles the fixture
conformance/trinity/abi/abi_fixture.c against the header and records that zig
ast-check rejects src/c_api.zig at the pin; conformance/trinity/c_abi.json.

Cards abi.c-api, tri27.toolchain and lib.trinity name their canonical specs;
specs/OWNERS.md extends isa/ and adds vm/ and api/; the encoding stub leaves
tools/specs_generate_baseline.txt; its three stale seals are removed; five new
seals; pins: test blocks 12673 -> 12709, pub const OP_* 11 -> 60; docs/now
entry; README section and rows.

Not claimed: any run on the owner's Zig; the string and file opcodes, SACR modes
2..4 and the VSA VM's programs are not replayed; the ABI is not linked.

Closes gHashTag#3567

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
@gHashTag
gHashTag merged commit e4b7632 into gHashTag:master Sep 12, 2026
30 of 31 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

[spec][Trinity S05] Specify VM, TRI27 bytecode and host ABI behavior

2 participants