safety: initial STPA analysis

[avrabe]

Summary

• Adds STPA (System-Theoretic Process Analysis) for Synth as a WebAssembly-to-ARM AOT compiler
• 6 losses, 10 hazards (3 sub-hazards)
• Follows the same schema as Meld's STPA (pulseengine/meld/safety/schema/stpa.schema.json)

Key coverage areas:

• Instruction selection correctness
• Peephole optimization safety
• Bounds check generation
• ARM encoding validity (ISA variant matching)
• Control flow translation (block/loop/if → labels/branches)
• Register allocation correctness
• ELF generation (vector table, relocations, sections)
• Meld dispatch ABI compatibility (__meld_dispatch_import)
• Verification gap (52 Admitted Rocq proofs, Z3 spec vs implementation)
• Cross-toolchain canonical ABI consistency with Meld and Kiln (H-10)

Context

Motivated by BA RFC #46 analysis. Synth provides an alternative execution path (AOT) to the RFC's runtime-based approach. The STPA identifies hazards specific to the compilation path that the RFC doesn't cover.

Cross-toolchain consistency analysis in pulseengine/meld at safety/stpa/cross-toolchain-consistency.yaml.

Next steps

• Add control structure and controlled processes (Step 2)
• Add UCAs (Step 3)
• Add loss scenarios (Step 4)
• Add safety requirements
• Connect to existing Rocq proof coverage

🤖 Generated with Claude Code