|
| 1 | +# VCR Tool-Qualification Roots — multi-standard top-of-V |
| 2 | +# |
| 3 | +# System: synth — WebAssembly→ARM/RISC-V AOT compiler, treated as a SOFTWARE |
| 4 | +# TOOL whose output (machine code) is incorporated into safety-related |
| 5 | +# software. Cover targets i.MX RT1062 / STM32H743. |
| 6 | +# |
| 7 | +# WHY THIS FILE EXISTS (bootstrap-verification seed) |
| 8 | +# The verified-codegen program (VCR-*, verified-codegen-roadmap.yaml) plans |
| 9 | +# the structural cure for the recurring codegen bug class. What was MISSING |
| 10 | +# was the top-of-V tool-qualification root: a stated tool classification and |
| 11 | +# the evidence strategy that discharges it. This file seeds that root so the |
| 12 | +# whole VCR program traces UP to a defensible certification claim, and the |
| 13 | +# STPA code-generation hazards (H-CODE-*) trace to the program that |
| 14 | +# eliminates them by construction rather than by accreting point-fixes. |
| 15 | +# |
| 16 | +# STANDARDS NOTE (honest tool-capability constraint) |
| 17 | +# The four target standards are NOT separately loadable schemas in this rivet |
| 18 | +# install (loaded: common / stpa / aspice / stpa-aspice.bridge / ai- |
| 19 | +# provenance). They are therefore expressed here as CONTENT — a mapping of the |
| 20 | +# VCR evidence to each standard's tool-qualification objectives — not as four |
| 21 | +# schema declarations. Captured as tool friction for rivet (see |
| 22 | +# report-tool-friction): a project targeting DO-178C/ISO 26262/IEC 61508/ |
| 23 | +# EN 50128 cannot today declare those presets in rivet.yaml. |
| 24 | +# |
| 25 | +# Format: rivet generic-yaml |
| 26 | + |
| 27 | +artifacts: |
| 28 | + |
| 29 | + # =========================================================================== |
| 30 | + # Tool classification — the integrity-level decision (bootstrap step 1) |
| 31 | + # =========================================================================== |
| 32 | + - id: VCR-TQ-001 |
| 33 | + type: system-req |
| 34 | + title: > |
| 35 | + synth codegen requires tool qualification across DO-178C / ISO 26262 / |
| 36 | + IEC 61508 / EN 50128 (highest tool-impact class) |
| 37 | + description: > |
| 38 | + synth is a development TOOL whose output (ARM Thumb-2 / RISC-V RV32IMAC |
| 39 | + machine code) is incorporated into safety-related software with NO |
| 40 | + independent downstream verification of the generated binary beyond |
| 41 | + synth's own evidence. Under every target standard this places synth in |
| 42 | + the highest tool-impact class, REQUIRING qualification or an equivalent |
| 43 | + tool-confidence argument: |
| 44 | +
|
| 45 | + - DO-178C §12.2 + DO-330: the tool can INSERT an error into the |
| 46 | + airborne software and its output is not independently verified -> |
| 47 | + tool qualification at a TQL set by the Criteria; for a code generator |
| 48 | + whose output is not separately verified this is Criteria 1 |
| 49 | + (most rigorous). |
| 50 | +
|
| 51 | + - ISO 26262-8 §11: a tool error can violate a safety requirement |
| 52 | + (Tool Impact TI2) and the confidence that such a malfunction is |
| 53 | + prevented or detected is low without measures (Tool error Detection |
| 54 | + TD3) -> Tool Confidence Level TCL3 -> qualification required. |
| 55 | +
|
| 56 | + - IEC 61508-3 §7.4.4: an off-line support tool whose output contributes |
| 57 | + directly to the executable safety function is class T3 -> evidence of |
| 58 | + tool correctness required. |
| 59 | +
|
| 60 | + - EN 50128 §6.5.4 + Table A.6: a tool that can introduce undetected |
| 61 | + faults into the executable is class T3 -> a validated tool / proven- |
| 62 | + in-use / diverse-evidence argument is required. |
| 63 | +
|
| 64 | + The conclusion is uniform across all four: synth-as-shipped cannot be |
| 65 | + taken on trust; its correctness must be argued with evidence. The VCR |
| 66 | + program (VCR-001) is that evidence strategy. |
| 67 | + status: proposed |
| 68 | + tags: [tool-qualification, do-178c, iso-26262, iec-61508, en-50128, vcr, bootstrap, release-v0.12] |
| 69 | + links: |
| 70 | + # A system-level tool-qualification requirement traces to the stakeholder |
| 71 | + # need for a qualifiable compiler (BR-001 "Safety-critical qualification"); |
| 72 | + # the VCR program (VCR-001) is the sibling system-req that realizes it. |
| 73 | + - type: derives-from |
| 74 | + target: BR-001 |
| 75 | + - type: mitigates |
| 76 | + target: H-CODE-1 |
| 77 | + - type: mitigates |
| 78 | + target: H-CODE-3 |
| 79 | + fields: |
| 80 | + req-type: safety |
| 81 | + priority: must |
| 82 | + verification-criteria: > |
| 83 | + For each target standard, a tool-qualification / tool-confidence |
| 84 | + argument exists that cites concrete synth evidence (formal proofs, |
| 85 | + differential oracle, frozen-fixture result-identity) and is accepted at |
| 86 | + the stated class (TQL/TCL3/T3). Kill-criterion: if any standard's |
| 87 | + assessor rejects the argument as process-only with no product evidence, |
| 88 | + VCR-TQ-002's evidence pillars are insufficient and must be strengthened. |
| 89 | +
|
| 90 | + # =========================================================================== |
| 91 | + # Evidence strategy — how the VCR tracks discharge the qualification |
| 92 | + # =========================================================================== |
| 93 | + - id: VCR-TQ-002 |
| 94 | + type: sw-req |
| 95 | + title: VCR evidence pillars discharge tool qualification by construction |
| 96 | + description: > |
| 97 | + The qualification argument rests on three product-evidence pillars, each |
| 98 | + a VCR track, mapped to the standards' acceptable means: |
| 99 | +
|
| 100 | + 1. FORMAL LOWERING PROOF (VCR-SEL-001 + VCR-ISA-001 + VCR-WASM-001): |
| 101 | + verified-source -> verified-lowering -> verified-target, discharged |
| 102 | + in Rocq against authoritative semantics (WasmCert-Coq source, Sail |
| 103 | + ISA target). This is the DO-330 "verified tool" / EN 50128 "proven |
| 104 | + by formal methods" / IEC 61508 Route 2s (formal) tier — the strongest |
| 105 | + qualification evidence, and the means that lets a code generator be |
| 106 | + trusted without independently verifying every output. |
| 107 | +
|
| 108 | + 2. COVERAGE-GUIDED DIFFERENTIAL ORACLE (VCR-ORACLE-001): the empirical |
| 109 | + witness that the hand-written ARM/RISC-V model matches silicon — |
| 110 | + i.e. it validates the PROOF's assumptions. This is the ISO 26262 TD |
| 111 | + (tool-error-detection) measure that lowers TCL, and the EN 50128 / |
| 112 | + IEC 61508 "validation by testing" tier for the parts not yet proven. |
| 113 | +
|
| 114 | + 3. FROZEN-FIXTURE RESULT-IDENTITY GATE (control_step 0x00210A55, |
| 115 | + flight_algo 0x07FDF307, divseam 338/338): behavioral-regression |
| 116 | + evidence that every change preserves established behavior — the |
| 117 | + configuration-controlled baseline a tool-operational-requirements |
| 118 | + argument needs. |
| 119 | +
|
| 120 | + Together the pillars are the defense-in-depth the standards reward: |
| 121 | + proof where it reaches, validated testing where it does not, and a frozen |
| 122 | + baseline that makes every increment auditable. |
| 123 | + status: proposed |
| 124 | + tags: [tool-qualification, evidence, formal, oracle, vcr, bootstrap, release-v0.12] |
| 125 | + links: |
| 126 | + - type: derives-from |
| 127 | + target: VCR-TQ-001 |
| 128 | + - type: refines |
| 129 | + target: VCR-001 |
| 130 | + fields: |
| 131 | + req-type: safety |
| 132 | + priority: must |
| 133 | + verification-criteria: > |
| 134 | + Each pillar has a concrete realized artifact cited in the qualification |
| 135 | + argument: (1) >=1 op-class lowering Rocq-discharged end-to-end against |
| 136 | + the Sail/WasmCert anchors; (2) the oracle reports rule-coverage and |
| 137 | + flags any silicon-observed op absent from the model; (3) the frozen |
| 138 | + fixtures remain bit-identical across the program. Kill-criterion: a |
| 139 | + pillar with no realized artifact is a process promise, not evidence. |
0 commit comments