feat(#77,#80): platform space-consistency invariant + P3 async error-context.drop lowering

[avrabe]

Bounded v0.49 hub Lane 7 (BREADTH — platform semantics). Two sub-parts, each red-first and oracle-gated. Refs #77, #80.

Part A — #77: execution-space / memory-space consistency invariant

Gives the RAJA/Kokkos execution-space + memory-space choice a checked property, not a convention. New synth_memory::space model (ExecutionSpace × MemorySpace) with PlatformSpaces::validate() enforcing two consistency invariants:

1. OS-mapping: a bare-metal execution space cannot use an OS-mapped (Linux-only) memory space; a hosted space cannot claim a physical on-silicon space (Flash/TCM/ExternalRAM). (the issue's own worked example.)
2. FPU capability: an FP-requiring memory space cannot be hosted by an FPU-less core (Cortex-M0).

An inconsistent pairing is REJECTED with a machine reason naming the offending space (SpaceError).

Red-first evidence: 7 unit tests cover both directions of each invariant; neutering validate() to always-Ok fails 4 rejection tests.

Bounded scope: geometry (linmem/globals overlap, static-data addressing) is deliberately OUT — owned by synth_core::static_data_addr (VCR-VER-003, no file overlap with L2). This is a standalone model; wiring into live target selection is a named follow-up (disclosed in TP-009).

Part B — #80: P3 async intrinsic compilation (honest degradation)

Meld lowers P3 async components with RFC #46 host intrinsics under the pulseengine:async module. Synth's raw call lowering to a field-name BL already exists (#197 relocatable path); the missing piece is the semantic gate. New synth_core::async_intrinsics classifier, wired at the single CLI import-collection choke point (before instruction selection → both selector paths covered):

• LOWERED: exactly error-context.drop — a pure scalar handle op (one i32 handle in, nothing out). It marshals as an ordinary AAPCS C call and compiles to a BL error-context.drop call site (UNDEF symbol the host linker resolves against kiln-builtins).
• DECLINED by name with a machine reason: error-context.new / .debug-message (they carry a linmem message pointer — the SAME bounds-checked buffer class as stream, NOT scalar), stream, future, waitable-set/task (register save/restore across the scheduler yield). Unknown async intrinsics also decline.

The lowering decision is per op, not per family — lowering error-context.new as if scalar would silently miscompile its pointer argument (the exact bug #80 exists to prevent).

Gate evidence: 7 unit tests + 2 CLI end-to-end tests. The lowered op compiles to a relocatable ELF carrying error-context.drop in the symtab (executes-vs-reference ABI contract, checked via symtab not disasm); each of 5 declined-op fixtures FAILS the compile with the #80 reason.

Contract caveat: the pulseengine:async namespace and dotted resource.method field format are synth's assumed contract pending meld#94 — the gate does not fire until Meld's lowering confirms these strings. Pinned in one place citing RFC #46.

Frozen / gates

• Frozen control_step 13/13 PASS (byte-invisible — the async gate fires only on the pulseengine:async namespace; non-async modules are untouched). flight_algo anchor unaffected by the same argument (import-free module, binary proven unchanged by control_step).
• cargo build -p synth-cli --features riscv clean; touched-crate + synth-cli tests green; clippy -D; fmt.
• claim_check.py 25/25.
• rivet: TP-009 + TP-VER-001 (Formalize platform abstraction: Memory Space + Execution Space model (RAJA/Kokkos pattern) #77), KB-010 + KB-VER-001 (P3 async intrinsic compilation: generate ARM code for stream/future/task host calls #80) — all sys-verification carry a verifies link; rivet validate adds 0 errors vs baseline (52/52).
• No Rocq proofs added → bazel test //coq:verify_proofs not run (nothing to verify there).
• CI oracle steps appended to ci.yml for both parts.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L