Qualified MC/DC coverage tooling — GNATcoverage + GNATPro for Rust (the pedigree path rustc abandoned)

[O6lvl4]

Part of #11 / #12; the sibling of #18 on the same shelf (adjudicated direction, 2026-08-27). Context: rustc removed its MC/DC instrumentation upstream (rust-lang/rust#144999), so almide's rung-2 evidence is the per-decision vector ledger (almide#566) with condition coverage as backstop. AdaCore's GNATcoverage supports Rust at statement / decision / MC/DC level — but only against the commercial GNATPro for Rust toolchain ("compatibility with other rust toolchains is not guaranteed"; the Rust support is declared unstable). That is the qualified-pedigree endgame: gnatcov is the DO-178C-qualifiable coverage tool family, and GNATPro for Rust doubles as a second candidate for the qualified native seat (#18: Ferrocene / CompCert / — now — GNATPro for Rust).

Why external

A commercial toolchain subscription and, for certification credit, gnatcov's qualification material. Engineering here only prepares the evaluation.

What the project prepares in advance (solo)

• Free cross-check measurement: a workflow_dispatch CI job pins a PRE-REMOVAL dated nightly (the -Zcoverage-options=mcdc era) and measures real MC/DC for the safety set once — not evidence to pin (dead flag, upstream calls the implementation incomplete), but a calibration of the vector ledger: any decision the old instrumentation marks uncovered that the ledger calls vectors is a ledger bug. (almide side, in flight.)
• Evaluation acceptance test, written before any sales call: gnatcov + GNATPro on the ten safety files must (1) report MC/DC per decision; (2) agree with the 16 landed independence-pair vectors (each resolved site fully covered when only its vector tests run); (3) run on the pinned CI OS; (4) not change the compiled artifact's behaviour (byte-compare the test binaries' outputs).

Questions for AdaCore (the dossier)

1. GNATPro for Rust: which upstream rustc does it track, and is its MC/DC the pre-#144999 implementation or an independent one?
2. Stability commitment for the Rust MC/DC feature (the docs mark it unstable) and the roadmap to qualification material for Rust coverage (gnatcov's DO-330 kit today covers Ada/C/C++).
3. Platform coverage (linux x86_64 CI + macOS arm64 dev), licensing model per-seat vs per-CI-runner, and evaluation licence availability.
4. Interaction with a Ferrocene-based build (Qualified native toolchain material — Ferrocene subscription or CompCert commercial licence #18): can gnatcov consume coverage from a Ferrocene-compiled artifact, or is GNATPro-for-Rust-only instrumentation assumed?

Exit

Either: an evaluation licence obtained, the acceptance test green, and a decision recorded (ADR) on GNATPro-for-Rust as coverage tool and/or native seat — or a written finding of why not, kept with #18.

[O6lvl4]

Free calibration measurement completed (almide mcdc-probe run 33024780591; three attempts — the current tree cannot build on any MC/DC-era rustc since the wasmtime-47 embed raised MSRV to 1.94, and nightly-2025-06-01 broke on zerocopy; nightly-2025-07-25 at the last pre-embed ref succeeded).

Safety-set MC/DC under the abandoned rustc instrumentation (tests-only workload):

file	MC/DC conditions instrumented	covered
check/calls.rs	21	0% (workload: the CLI path was not run)
infer_calls_closures.rs	19	0%
certificate_b.rs	26	26.9%
certificate_c.rs	4	75%
certificate_p2.rs	5	0%
translation_validation.rs	4	50%
perceus_verified.rs	0	—
pass_effect_inference.rs / certificate.rs / certificate_b_tail.rs	0	—

The calibration's finding: the pre-removal implementation is measurably incomplete — perceus_verified.rs carries four ledgered boolean sites including a three-condition decision, and the instrumentation sees zero MC/DC conditions there (the decision head is macro-expanded: !matches!(…) && …). Upstream's stated removal reason ("not complete") is now a measured fact in this codebase. Consequences:

1. The per-decision vector ledger stays the primary instrument (it sees what the compiler didn't), and the adjudicated Q1/Q2 design is validated.
2. New question 5 for the AdaCore dossier: does GNATPro-for-Rust's MC/DC instrument decisions whose conditions are macro-expanded (matches!, custom macros)? That is the exact hole the abandoned upstream implementation had — a discriminating acceptance-test case.
3. Baseline for the evaluation: 3,082 MC/DC conditions across the measured crates, 17.16% covered under the tests-only workload at the pre-embed ref.

[O6lvl4]

Two additions from today's desk research (2026-08-27), ahead of any contact.

Manual finding: the Rust leg is toolchain-delegated instrumentation, and it fails silent

The current GNAT DAS manual (27.0w, 2026) documents the Rust workflow: unlike Ada/C/C++ where gnatcov instrument rewrites sources, Rust instrumentation is delegated to the rustc-based compiler (-Cinstrument-coverage plus -Ccoverage-options=mcdc) — gnatcov only consumes the resulting coverage data. Two consequences:

• Sharpens dossier Q1: the flag spelled -C (the abandoned upstream implementation was -Z…, nightly-only) implies a stabilized option in their toolchain — i.e. a maintained fork of the pre-#144999 implementation, or an independent one. Q1's answer now has a concrete discriminator to check against.
• The manual states the Rust workflow lacks the instrumentation-level safety check the other languages have: analysing with --level=stmt+mcdc against an artifact not instrumented for MC/DC reports no violations, silently. That mandates a negative control in the acceptance test: a canary file with a known two-condition decision and a deliberately partial test run must produce an MC/DC violation; a silent-green canary fails the evaluation regardless of the other criteria. (Added as acceptance-test check (5).)

Given the delegation, the calibration's zero-conditions finding on perceus_verified.rs (comment above) is the prior for question 5, not just background: unless their toolchain patched beyond the abandoned upstream implementation, the macro-expansion hole should reproduce identically under gnatcov.

Source: https://docs.adacore.com/gnatcoverage-docs/html/gnatcov/cov_rust.html

Widened outreach: the dossier is vendor-agnostic — three directions, one dataset

The calibration data (0 conditions on macro-expanded decision heads; 3,082 conditions / 17.16% baseline) is the same ammunition for all three:

1. Second vendor recipient — Rapita Systems (RapiCover, DO-178C verification specialist, DO-330 qualification material). They publish "Certification-Ready Rust: GNAT Pro & RVS for Avionics Standards", i.e. they already position their verification suite alongside AdaCore's Rust toolchain. Same dossier, same acceptance test; a parallel RFI is normal procurement and improves the negotiating position with both. (LDRA checked and parked: no Rust support — C/C++/Java/Ada only.)
2. Upstream — report the measured macro-expansion blind spot to Tracking implementation for MC/DC rust-lang/rust#124144 (MC/DC tracking) with the calibration numbers; the removal rationale of #144999 ("not complete") is now a measured fact in a real codebase, which is exactly the kind of datum a reinstatement discussion needs. Zero cost, possible root fix, upstream standing.
3. Academic — arXiv:2409.08708 "Towards Modified Condition/Decision Coverage of Rust" (AIAA JAIS) treats MC/DC semantics for Rust pattern matching: the theory side of precisely our matches! hole. Authors are a sales-filter-free contact; the per-decision vector ledger (almide#566) is a working artifact their line of work rarely gets to see.

Sequencing unchanged in spirit, updated in letter: the free calibration is done (comment above); next actions are the outreach mails (owner-side: AdaCore + Rapita with the dossier) and the upstream/academic reports (engineering-side, no sales gate). Purchase remains deferred: the tool's unique remaining value is the maintained MC/DC toolchain + DO-330 kit, which prices in at rung 3 unless question 5 comes back "yes, macro-expanded conditions are instrumented" — that answer alone would justify a rung-2 evaluation license exercise on the pending 45 sites of almide#566.