Typed Register ISA over Post-AIMS ARC
Goal
Define a compact, verifiable bytecode encoding for the legal post-realization ARC surface without baking current enum counts or future native ABI assumptions into the format.
Implementation Sketch
- Map the current legal post-AIMS
ArcInstr,ArcTerminator, and logicalValueSemanticsId/ExecutableDropPlansurface with exhaustive Rust matches. The prototype may temporarily acceptRcStrategyonly as a named migration carrier;HeapPointer,FatPointer, inline-field location, helper symbol, and atomic opcode are not final AIMS vocabulary. Do not repeat numeric variant counts in prose or tests; adding a variant must produce a compile error or an explicit unsupported-residue failure. - Treat match control flow and self-tail-call loops as ordinary ARC CFG edges because ARC has already lowered them. The VM never consumes
DecisionTreePoolto recover meaning. - Start from the provisional skeleton encoding, then define opcode/version fields, byte order, operand-width extensions, register/constant limits, function references, source locations, and deterministic encode/decode behavior. Fixed 32-bit words are a measured option, not an invariant.
- Prototype operand-form-specific operations selected from shared logical type, callable,
ValueSemanticsId, drop, and AIMS descriptors plus a VM-ownedVmLayoutPlan, then compare them with unspecialized bytecode. Only the logical descriptors are shared; register banks, packed fields, immediates, opcode forms, and storage widths are VM projections. LLVM uses its separateCompiledLayoutPlan. Neither consumer may re-derive semantics or ownership policy. Promote the design only if the verifier can recheck every declared fact and macro evidence shows that avoiding repeated dynamic discovery pays for the larger ISA. - Compile enum operations from validated
VmEnumLayout: construct, inspect a logical tag, switch, project a semantic(variant, field), trace, and drop. Rewrite each operand to verified VM storage before execution; the interpreter never decodesCompiledEnumLayoutor guesses a payload slot. - Add a chunk verifier for bounds, register types, CFG targets, call signatures, constants, RC opcode operands, and version compatibility. Malformed/untrusted chunks return structured errors and never panic or invoke undefined behavior.
- Keep opcode semantics aligned with ARC operations, while allowing VM-only fused/specialized opcodes only when their ARC expansion, type proof, ownership/RC trace, source provenance, and exceptional edges are mechanically verified. The optimizer emits an auditable transformation record and every optimized fixture also runs through the unfused bytecode path.
- Experiment with a deterministic portable encoded chunk plus an optional validated execution-layout cache. Measure packed 32-bit words, wider fixed records, and predecoded typed instructions in the real VM before choosing; no host-specific execution layout becomes the serialized semantic contract by prototype inertia.
Layer Coverage
| Layer | Disposition |
|---|---|
| L1 | N/A: no grammar changes. |
| L2 | N/A: no typechecking changes. |
| L3 | N/A: no canonicalization changes. |
| L4 | Covered by the exhaustive legal post-AIMS mapping criterion. |
| L5 | Covered by the verified-chunk execution criterion. |
| L6 | N/A: native backends do not consume VM bytecode; shared-realization regressions are owned by the contract section. |
| L7 | N/A: native backends do not consume VM bytecode; shared-realization regressions are owned by the contract section. |
| L8 | N/A: AOT does not consume VM bytecode. |
| L9 | Covered by the section cross-executor criterion. |
| L10 | Covered by the section leak-freedom criterion. |
| L11 | Covered by the ISA feature-fixture criterion. |
| L12 | Covered by the production VM decoding/execution criterion. |
Work Items
- Define exhaustive typed opcode semantics for every legal
post-AIMS ARC instruction, terminator, and logical value/drop plan without
hard-coded variant counts; reject unsupported residues explicitly and retire
physical
RcStrategynames from the shared artifact. - Specify versioned deterministic chunks and implement encode/decode plus structural/type/CFG verification, operand extensions, malformed-input tests, and source-map behavior.