Skip to content

feat: kiln-builtins crate — no_std staticlib for synth-compiled embedded targets#175

Merged
avrabe merged 3 commits intomainfrom
feat/kiln-builtins-stub
Mar 21, 2026
Merged

feat: kiln-builtins crate — no_std staticlib for synth-compiled embedded targets#175
avrabe merged 3 commits intomainfrom
feat/kiln-builtins-stub

Conversation

@avrabe
Copy link
Copy Markdown
Collaborator

@avrabe avrabe commented Mar 21, 2026

Summary

Phase 1 stub of kiln-builtins per RFC #46 toolchain architecture. This is the C ABI bridge between synth-compiled ARM ELF binaries and kiln's runtime services.

Functions

  • __meld_dispatch_import(import_index: u32) -> u32 — stub, returns 0
  • __meld_get_memory_base() -> *mut u8 — returns linker-provided memory base
  • cabi_realloc(old_ptr, old_size, align, new_size) -> u32 — bump allocator
  • __kiln_builtins_init(heap_start: u32) — initialize bump allocator

Build

cargo build -p kiln-builtins --target thumbv7em-none-eabi --release
# Produces: target/thumbv7em-none-eabi/release/libkiln_builtins.a

Properties

  • Pure no_std, zero dependencies
  • Builds as staticlib for ARM Cortex-M4
  • Enables synth --link --builtins integration
  • Phase 2: real WASI dispatch via import table from meld

Phase 1 stub implementation of kiln-builtins — the C ABI bridge between
synth-compiled ARM code and kiln's runtime services. Per RFC #46, this
is the no_std execution path for embedded targets via gale/Zephyr.

Three functions:
- __meld_dispatch_import: routes import calls (stub returns 0)
- __meld_get_memory_base: returns linear memory base from linker symbol
- cabi_realloc: bump allocator for canonical ABI memory allocation

Also: __kiln_builtins_init for heap initialization.

Builds for thumbv7em-none-eabi (Cortex-M4) as libkiln_builtins.a.
Zero dependencies, pure no_std.

Trace: skip
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@github-actions
Copy link
Copy Markdown

github-actions Bot commented Mar 21, 2026

🔍 Build Diagnostics Report

Summary

Metric Base Branch This PR Change
Errors 0 0 0
Warnings 5 8 3

🎯 Impact Analysis

Issues in Files You Modified

  • 0 new errors introduced by your changes
  • 3 new warnings introduced by your changes
  • 0 total errors in modified files
  • 3 total warnings in modified files
  • 1 files you modified

Cascading Issues (Your Changes Breaking Other Files)

  • 0 new errors in unchanged files
  • 0 new warnings in unchanged files
  • 0 unchanged files now affected

Note: "Cascading issues" are errors in files you didn't modify, caused by your changes (e.g., breaking API changes, dependency issues).

⚠️ Warnings in Modified Files

kiln-builtins/src/lib.rs:400:7 - unexpected cfg condition name: kani (unexpected_cfgs)
kiln-builtins/src/lib.rs:182:5 - unnecessary unsafe block (unused_unsafe)
kiln-builtins/src/lib.rs:249:4 - function platform is never used (dead_code)

✅ No Cascading Issues

Good! Your changes don't break any existing code in other files.


📊 Full diagnostic data available in workflow artifacts

🔧 To reproduce locally:

# Install cargo-kiln
cargo install --path cargo-kiln

# Analyze your changes
cargo-kiln build --output json --filter-severity error
cargo-kiln check --output json --filter-severity warning

avrabe and others added 2 commits March 21, 2026 20:38
Tests:
- cabi_realloc uninitialized returns 0
- cabi_realloc zero size returns 0
- cabi_realloc basic allocation and sequential bumping
- cabi_realloc alignment (8-byte, 4-byte from misaligned start)
- cabi_realloc overflow returns 0 (checked_add)
- dispatch_import stub always returns 0

Kani proofs:
- cabi_realloc_never_overflows: no u32 overflow in allocation
- cabi_realloc_alignment_correct: result always respects alignment
- dispatch_import_always_returns_zero: stub contract

Also: use checked_add for overflow safety in cabi_realloc.

Trace: skip
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…igration

Add Platform struct — C-compatible function pointers for hardware/OS
operations (write, clock, random, exit). This supports two coexisting
paths:

1. C shim (today): callbacks call Zephyr C APIs directly via FFI
2. Verified Rust (gradual): swap individual callbacks to route through
   gale's formally verified kernel primitives, then to Zephyr C for HW

The design mirrors Zephyr's device driver API pattern: a static struct
of function pointers, registered at init, no generics, no vtable.

Firmware init:
  __kiln_init(&PLATFORM, heap_start)

Migration pattern: replace one callback at a time as gale modules
become available, without changing kiln-builtins or synth.

Tests: 9 unit tests + 3 Kani proofs. All pass.

Trace: skip
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@avrabe avrabe merged commit ce319fd into main Mar 21, 2026
15 checks passed
@avrabe avrabe deleted the feat/kiln-builtins-stub branch March 21, 2026 20:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant