Gap 2 — Certification seat: flight-profile requirements here first, keystones in the implementation, a qualified native toolchain in the chain

[O6lvl4]

Part of #9. Implementation-side work is tracked in almide/almide#586 (flight-grade program); this epic holds the judge's side and the honest picture of the seat.

Measured (2026-08-20)

• R1a (IR → Rust → Ferrocene-class rustc) and R1b (IR → wasm → C via a small-TCB translator → CompCert-class) RATIFIED 2026-08-19 in the greenfield ARCHITECTURE §7. Destinations, not implementations: no qualified compiler is in the chain.
• Flight ladder (docs/roadmap/active/flight-profile.md §7.3): G-F0 in progress, G-F1 designed/unenforced, G-F2/G-F3 designed/unimplemented, G-F4 Slice 0 green, G-F5/G-F6 designed.
• Receipt rows C-WCET and C-FAITHFUL: PENDING.
• Seams a DER will challenge (flight-qualification.md §2): witness → emitted bytes is trusted (V is a structural presence check, not semantic refinement); extraction is trusted (ocamlopt); a single checker; MC/DC zero (line coverage 65.89% only, no branch); wasmtime is an unqualified COTS component (TOR-9, Qualified/minimal execution environment for wasm Critical-profile output (wasmtime has no qualification path) almide#865).

Work

• [als first] the bounded profile (@bounded, formerly @flight — renamed at adjudication, Adjudicate ADR-0017 — flight profile as a normative subset (three ⚖ decisions) #29) as requirements — ALS sections + contracts + fixtures for the flight profile (counted loops, no allocation in loops, bounded static allocation, bounded recursion). Two-PR order: it lands here, then the checker enforces it as a wall (G-F1).
• [impl] G-F2 — loops lifted into Rocq, counted-loop bound + allocation ceiling as proven properties → C-WCET not PENDING.
• [impl] G-F3, one seat through to the end — R1a: production MIR→Rust renderer + rust_pattern faithfulness + compile with a Ferrocene-built rustc; or R1b: wasm→C small-TCB translator + CompCert. The technical demonstration is solo (Ferrocene's source is public; CompCert is usable non-commercially); the qualified attribute of the toolchain is Qualified native toolchain material — Ferrocene subscription or CompCert commercial licence #18.
• [impl] G-F4 — the reference app (control-law kernel / state machine / watchdog) through make verify end to end.
• [impl] Seams — V from structural to semantic refinement (or per-build translation validation); verified extraction; a second, independent checker; branch and MC/DC coverage of the checker and the renderer (the tool's own structural coverage is a DO-330 objective, separate from the customer's application MC/DC).
• [impl] Cert profile without wasmtime (R1b is AOT-only) — TOR-9 resolved by construction for the cert seat.
• [als] Conformance statement gains the cert-build leg once it exists: ref ↔ wasm ↔ cert-build identity over spec/.

Exit

C-WCET and C-FAITHFUL hold on the flight subset; the reference app is built by the chosen seat with output identity to the reference leg and wasm; the flight-profile ALS sections are cited by contracts with fixtures.

External dependency

The word qualified (#18). Acceptance of the whole argument is #17. A recommendation, not a rule: choose between R1a and R1b after the gap assessment in #15, so the renderer effort (designed at ~5× render_wasm) is spent on the seat an assessor prefers.