Skip to content

P3 async intrinsic compilation: generate ARM code for stream/future/task host calls #80

@avrabe

Description

@avrabe

Context

When Meld lowers P3 async components to core modules, the output contains imports for RFC #46 host intrinsics (stream_read, stream_write, waitable_set_wait, task_return, etc). Synth must compile call sites for these intrinsics to native ARM code that invokes kiln-builtins, which dispatches to Gale's verified RTOS primitives.

What Synth Needs

1. Host Intrinsic Call Convention

RFC #46 intrinsics are imported as core WASM functions. Synth already handles host function imports by generating calls to kiln-builtins' C ABI surface. The P3 intrinsics follow the same pattern:

;; Core module (after Meld lowering)
(import "pulseengine:async" "stream_read" (func $stream_read (param i32 i32 i32 i32) (result i32)))

;; Synth generates ARM:
BL kiln_builtins_stream_read   ; Call into kiln-builtins

2. Callback Trampoline Code Generation

For P3 callback lifting mode, Meld generates a __callback export that the host calls. Synth compiles this export as a normal function entry point, but must ensure:

  • The callback can be called from Gale's scheduler context (correct stack setup)
  • Linear memory base register is restored on entry (callback may fire on a different Gale task)
  • Fuel metering continues across callback invocations

3. Stream Buffer Memory Layout

Stream read/write intrinsics reference linear memory for data transfer. Synth must generate correct memory access patterns:

  • Bounds check before stream_read writes to linear memory
  • Alignment requirements for typed stream elements
  • Integration with Synth's existing memory bounds checking proofs

4. Async State Preservation

If a component uses stackful async (not callback mode), Synth must generate code that:

  • Saves register state before waitable_set_wait (which yields to Gale scheduler)
  • Restores register state on resume
  • Maintains correct stack frame across yield points

Verification

  • Extend Z3 translation validation to cover host intrinsic call sites
  • Verify register save/restore around yield points
  • Verify memory bounds for stream buffer arguments

Connects to

  • kiln#230: P3 async runtime (provides the intrinsics Synth calls)
  • meld#94: P3 lowering (generates the intrinsic imports Synth compiles)
  • gale#13: Typed stream extensions (provides the backend)
  • synth#77: Platform abstraction (intrinsic calling convention per platform)

Priority

Medium-High — follows after Meld P3 lowering and Kiln P3 runtime.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions