bamts-native 0.1.0

Native linkage, FFI, and execution bridge for BamTS
Documentation

Native ABI foundations for BamTiScript.

This module owns the C-layout value representation shared verbatim between the register interpreter and generated native code. Value constants and ShadowFrame layout are grounded in the machine-checked formal models:

  • formal/lean/Bamti/Value.lean — the NaN-boxed Word64 field algebra (header:13 || tag:3 || payload:48), the seven nonzero tags, and the encode/decode round-trip theorem.
  • formal/lean/Bamti/Abi.lean — the 32-byte, 8-aligned ShadowFrame header layout theorem.

Completion and CompletionTag belong to the native-entry contract in the canonical execution plan (N5); the Lean files do not assign them a wire layout. Bamti.NodeLoop.Completion is a separate event-loop proof record.

The value/frame primitives in this file are total, allocation-free, and require no unsafe. The native runtime bridge — the exported bamts_* helper ABI, the panic- and nesting-safe [native_bridge::NativeOps] dispatch seam, and the feature-gated JIT/AOT linkage surfaces — lives in [native_bridge], which centralizes every unsafe operation the generated code requires.