0%

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 logical ValueSemanticsId / ExecutableDropPlan surface with exhaustive Rust matches. The prototype may temporarily accept RcStrategy only 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 DecisionTreePool to 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-owned VmLayoutPlan, 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 separate CompiledLayoutPlan. 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 decodes CompiledEnumLayout or 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

LayerDisposition
L1N/A: no grammar changes.
L2N/A: no typechecking changes.
L3N/A: no canonicalization changes.
L4Covered by the exhaustive legal post-AIMS mapping criterion.
L5Covered by the verified-chunk execution criterion.
L6N/A: native backends do not consume VM bytecode; shared-realization regressions are owned by the contract section.
L7N/A: native backends do not consume VM bytecode; shared-realization regressions are owned by the contract section.
L8N/A: AOT does not consume VM bytecode.
L9Covered by the section cross-executor criterion.
L10Covered by the section leak-freedom criterion.
L11Covered by the ISA feature-fixture criterion.
L12Covered 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 RcStrategy names 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.