Skip to main content

Crate bamts_native

Crate bamts_native 

Source
Expand description

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.

Re-exports§

pub use native_bridge::*;

Modules§

native_bridge
The native runtime bridge: the typed helper-call algebra, the exact 32 bamts_* C-ABI helper exports, the panic- and nesting-safe thread-local NativeOps dispatch seam, and the feature-gated JIT and AOT linkage surfaces.

Structs§

Completion
The out-parameter written by a native entry. size = 8, align = 8.
ShadowFrame
The register frame header shared by the interpreter and native code.
SlotId
A validated heap-reference payload: segment:u16 << 32 | slot:u32, both nonzero. Illegal (zero) identities are unrepresentable.
Value
A NaN-boxed JavaScript value. ABI-identical to a u64, so *mut Value arrays and Completion fields carry it with no wrapping.

Enums§

CompletionTag
The completion class returned by a native entry, as the raw u32 result.
Decoded
The decoded meaning of a Value, mirroring the Value inductive.

Constants§

TAG_BOOLEAN
Tag code for a boolean.
TAG_HEAP_REF
Tag code for a heap reference (SlotId).
TAG_HOLE
Tag code for the array/TDZ hole.
TAG_INT32
Tag code for a boxed 32-bit integer.
TAG_NULL
Tag code for null.
TAG_UNDEFINED
Tag code for undefined.
TAG_UNINITIALIZED
Tag code for an uninitialized register slot.