Verification and traceability

Platform spec article

Verification and traceability

Back to Extern dispatch and policy ◎ Open feature in platform map

Spec standingStandard

Owner

Piotr Mikstacki pmikstacki@cybernomad.it

Submitter

Piotr Mikstacki pmikstacki@cybernomad.it

Current document

ADRs (2)

1. 0005-link-time-extern-standard Link-time extern is the Standard path Accepted

   User foreign libraries resolve at link time; dlopen remains legacy.

   Context

   Early engine prototypes resolved Extern(Library:…) via dlopen/dlsym. That complicates reproducible AOT artifacts and blurs security review of loaded code.

   Decision

   Track	Status
   Link-time	Standard for v0.3 — addresses fixed before execution via C ABI profile
   Dynamic extern_dlopen	Proposed / legacy — engine feature only; not required for reference CLI
   Validation	High-level Beskid types in extern signatures must be rejected before codegen
   Syscalls	User externs must not embed OS syscall sequences — see Panic, IO, and syscalls

   Consequences

   New platform work documents link-time flows first. Dynamic resolution stays gated behind extern_dlopen in beskid_engine.

   Verification anchors

   compiler/crates/beskid_analysis extern validation; beskid_engine link paths.

   Open full ADR page

2. 0006-interop-dispatch-builtins Runtime interop_dispatch builtins for tagged values Accepted

   Compiler thunks call stable dispatch entrypoints for language/runtime interop layouts.

   Context

   Tagged interop values need runtime-known layout offsets. Per-site custom trampolines would fork ABI stability.

   Decision

   Builtin family	Role
   interop_dispatch_unit	Unit-tagged dispatch
   interop_dispatch_ptr	Pointer payloads
   interop_dispatch_usize	Scalar bridge
   Layout stability	Offsets are versioned with ABI versioning
   Implementation	beskid_runtime::interop exports registered in BUILTIN_SPECS

   Lowering must route approved tagged calls through these builtins rather than ad-hoc host calls.

   Consequences

   Interop layout changes require ABI bump or additive symbol policy per D-EXEC-ABI-0002.

   Verification anchors

   compiler/crates/beskid_runtime/src/interop/; interop lowering tests.

   Open full ADR page

Articles

• Contracts and edge cases MUST rules for extern validation, dynamic linking policy, and interop dispatch layout. article Standard Reviewed Fri May 22
• Design model Extern resolution layers, runtime dispatch builtins, and host policy boundaries. article Standard Reviewed Fri May 22
• Examples Declaring Extern contracts, dynamic getpid smoke, and interop dispatch usage patterns. article Standard Reviewed Fri May 22
• FAQ and troubleshooting Extern linking failures, dlopen policy, and interop dispatch debugging. article Standard Reviewed Fri May 22
• Flow and algorithm Extern validation, link registration, optional dlopen resolution, and interop dispatch calls. article Standard Reviewed Fri May 22
• Verification and traceability Engine extern tests, analysis diagnostics, and interop layout traceability. article Standard Reviewed Fri May 22

History

0 revisions (git unavailable at build; counts may be empty)

Open full history on GitHub

No commits recorded for this path.

Completeness

OKfeature · 2 SpecSection(s) · 1 H2 heading(s)

Section id	Required	Found
what-this-feature-specifies	yes	yes
implementation-anchors	yes	yes

Full tree: run pnpm verify:platform-spec-layout (writes src/generated/platform-spec-layout-report.json).

Related spec docs

• Feature
  Extern dispatch and policy

  Parent feature hub

Implementation anchors

Path	Role
compiler/crates/beskid_analysis/src/beskid.pest	Extern syntax
compiler/crates/beskid_analysis/src/analysis/diagnostic_kinds.rs	Extern-related diagnostics
compiler/crates/beskid_abi/src/builtins.rs	interop_dispatch_* in BUILTIN_SPECS
compiler/crates/beskid_codegen	declare_validated_extern_imports, signature validation
compiler/crates/beskid_engine	extern_dlopen tests, new_with_symbols
compiler/crates/beskid_runtime/src/interop.rs	Dispatch implementations
compiler/crates/beskid_runtime/src/interop_layout.rs	Tag/payload offsets

Test matrix

Test (engine)	Asserts
extern_resolution_only_compiles_with_feature	Resolution succeeds when feature on
extern_real_call_getpid	Live call returns plausible PID
extern_resolution_fails_without_feature	EXT-001 style failure
extern_missing_symbol_errors	dlsym diagnostic quality
extern_missing_library_errors	dlopen diagnostic quality

Requirement traceability

ID	Evidence
EXT-001	extern_resolution_fails_without_feature
EXT-002	ExternDeclarationError::InvalidSignature unit paths in codegen
EXT-003–004	Engine cache tests + code review of dlopen flags
EXT-005	interop_layout.rs + runtime dispatch tests

Related topics

• Contracts and edge cases
• Builtins and symbols