MIRR Compiler — Interactive Paper
Description: MIRR: A safety-critical HDL compiler with formal width inference. Living Research Artifact — interactive paper with in-browser compiler.

# MIRR: A Safety-Critical HDL Compiler
with Formal Width Inference

Brandon · March 2026 · Version — · Commit `dev` · Apache-2.0 · CITATION.cff · Source

## Abstract

Safety-critical cyber-physical systems demand hardware that is correct by construction. We present MIRR, an open-source Rust compiler (30,719 lines, 101 files, zero `unsafe` blocks) for a domain-specific language targeting safety-critical hardware–software co-design. MIRR compiles temporal guards, guarded reflexes, and LTL safety properties through a 9-stage deterministic pipeline into 9 emission backends including SystemVerilog RTL, FIRRTL, and a novel 30-instruction R-SPU ISA with 32-bit binary encoding, tagged-word registers, and cycle-accurate simulation. Width inference is backed by 1,906 lines of Rocq proofs (55 theorems across 12 files). A signedness type system with 16 inference rules rejects mixed signed/unsigned expressions. A homoiconic S-expression IR enables code-as-data transformation with a verified round-trip invariant. The compiler enforces NASA Power-of-10 compliance: bounded iteration, zero recursion, and explicit resource limits throughout. A test suite of 2,601 tests achieves a 1.41:1 test-to-source ratio.

This paper is a Living Research Artifact. Every claim above is verifiable live in the browser below—the compiler runs as WebAssembly, the proofs are in the repo, and the paper is Apache-2.0 licensed so it can never be paywalled.

## Claims

1. MIRR compiles temporal specifications to correct SystemVerilog, FIRRTL, R-SPU assembly, S-expression IR, JSON netlist, and DOT graph. [Evidence ↓]
2. Width inference is sound: no assignment silently truncates a value. Backed by 55 Rocq theorems (52 fully mechanized).
3. All compiler algorithms are bounded: no unbounded recursion or iteration exists. Every loop has an explicit MAX_* constant. [Evidence ↓]
4. The compiler is safe: `#![forbid(unsafe_code)]` on every source file.

## Demo — Compiler Playground (verifies claim 1, claim 3)

Type MIRR source below or select an example. The compiler runs entirely in your browser via WebAssembly — no server, no account. Source is bounded to 64 KiB.

MIRR Source
Output

    Compiler loading...

### Waveform Viewer

Cycles:

### Circuit Graph

## Demo — Compile-Time Benchmarks (verifies claim 3)

Compile the TMR sensor fusion example to all six targets and measure wall-clock time in your browser. Bounded algorithms produce predictable compile times.

Target | Time (ms) | Output lines
--- | --- | ---
Click Run Benchmarks to start.

## 1. Introduction

Safety-critical cyber-physical systems—neonatal respirators, flight controllers, industrial interlocks, autonomous vehicle watchdogs—demand hardware that is correct by construction. Traditional flows compile C++ or hand-written Verilog through opaque synthesis tools, leaving a semantic gap between the engineer’s intent and the generated gates. High-level synthesis (HLS) tools narrow this gap but lack native concepts of temporal behavior and formal safety properties. The resulting verification burden falls on post-synthesis simulation, which cannot exhaustively cover the state space of even modest safety monitors.

Hardware construction languages such as Chisel, Clash, and Bluespec raise the abstraction level above RTL, yet none combines temporal guard specification, LTL property compilation, formal width verification, and instruction-level emission in a single deterministic pipeline. Furthermore, existing tools do not enforce the bounded-resource discipline required by NASA Power-of-10 or DO-254 certification workflows.

### Contributions

1. A three-construct surface language (Signal, Guard, Reflex) that maps directly to synthesizable hardware primitives.
2. A 9-stage deterministic pipeline producing 9 emission backends: SystemVerilog RTL, FIRRTL, JSON netlist, Graphviz DOT, R-SPU assembly, R-SPU binary, S-expression IR, SystemVerilog testbench, and FPGA scaffold.
3. SCC-based width inference with 1,906 lines of Rocq proofs (55 theorems, 52 mechanized, across 12 proof files).
4. A signedness type system (16 rules, E601–E609) rejecting mixed signed/unsigned expressions.
5. An extended type system with 8 features: refinement types, linear types, effect typing, clock domains, phantom types, type-level naturals, dependent types, session types.
6. The R-SPU ISA v2: 30 instructions across 7 tiers with 32-bit binary encoding and cycle-accurate simulation.
7. A homoiconic S-expression IR with verified round-trip invariant and bounded eval/apply core.
8. A MAPE-K feedback loop simulator for autonomic observability with LTL property monitoring.
9. 2,601 tests at a 1.41:1 test-to-source ratio, with 92 `#![forbid(unsafe_code)]` directives and 0 Clippy warnings.

Figure 1 shows the complete system architecture, and Figure 2 presents the core grammar fragment.

Figure 1: MIRR system architecture. The 9-stage pipeline compiles source to 9 emission backends. Width inference (Stage 7) is backed by 1,906 lines of Rocq proofs. The R-SPU path includes cycle-accurate simulation with tagged-word runtime type checking and MAPE-K autonomic monitoring.

## 2. The MIRR Language

MIRR’s design rests on three principles:

P1: The Generative Power of Three. The surface language has exactly three behavioral constructs—Signal, Guard, Reflex—each mapping to a distinct hardware primitive. Signals are typed wires. Guards are temporal conditions implemented as shift registers or saturating counters that fire after a sustained boolean condition holds for a specified number of clock cycles. Reflexes are guarded assignments: when a guard fires, the reflex drives an output signal to a deterministic value.

P2: NASA Power-of-10 Compliance. Every algorithm has an explicit iteration bound. Recursion is forbidden. All 92 source files carry `#![forbid(unsafe_code)]`. Every loop is bounded by an explicit `MAX_*` constant.

P3: Properties Are Verification-Only. Safety properties compile to SVA (SystemVerilog Assertions) directives. They produce no hardware—they constrain the verification environment only. Adding or removing properties never changes the synthesized circuit.

### Formal Grammar (core fragment)

    program   ::= {patterndef} module
    module    ::= "module" ID "{" {item} "}"
    item      ::= signal | guard | reflex | property | call

    signal    ::= "signal" ID ":" dir type ";"
    dir       ::= "in" | "out" | "internal"
    type      ::= "bool" | "u"N | "i"N

    guard     ::= "guard" ID "{" "when" expr "for" N "cycles" ";"  "}"
    reflex    ::= "reflex" ID "{" "on" glist "{" {assign} "}" "}"
    property  ::= "property" ID "{" [dir_p] body "}"
    body      ::= "always(" φ ")" | "never(" φ ")"
                | "eventually_within(" expr "," N ")"
                | "always_followed_by(" expr "," expr "," N ")"

Figure 2: MIRR formal grammar (core fragment). Operator precedence: * > +,- > <<,>> > relational > ==,!= > ^ > && > ||. Pattern definitions (def/reflect) are omitted for brevity.

### Pattern System

Table I: Pattern parameter and argument kinds. Type compatibility is enforced at expansion time.
Param Kind | Accepts | Syntax
--- | --- | ---
`signal` | Signal references | `in u16`
`constant` | Integer/bool literals | `u16`, `bool`
`pattern` | Pattern references | `pattern`

### Property Forms → SVA Compilation

Table II: LTL property form compilation to SVA.
MIRR Form | SVA Output
--- | ---
`always (P)` | `P`
`never (P)` | `!(P)`
`always (P -> Q)` | `P |-> Q`
`never (P -> Q)` | `!(P |-> Q)`
`eventually_within(P, N)` | `##[1:N] P`
`always_followed_by(P, Q, N)` | `P |-> ##N Q`

### Type System

The signedness type system enforces the cross-category invariant: signed and unsigned types never mix in the same expression. This eliminates implicit-conversion bugs common in C and Verilog. The core checker (480 lines) uses 16 inference rules across error codes E601–E609. The extended type system adds 8 certification-oriented features (E610–E625):

Feature | Errors | Purpose
--- | --- | ---
Refinement types | E610–E612 | Value-range bounds
Linear types | E613–E615 | Consume-exactly-once resources
Effect types | E616–E617 | Pure vs. stateful separation
Clock domains | E618–E619 | CDC crossing detection
Phantom types | E620–E621 | Provenance tagging
Type-level naturals | E622–E623 | Dimension checking
Dependent types | E624 | Value-dependent constraints
Session types | E625 | Protocol conformance

## 3. Compilation Pipeline

The pipeline processes MIRR source through 9 deterministic stages, each with explicit bounds on iteration depth and node count.

Stage | Name | Bound | Output
--- | --- | --- | ---
1 | Parse | O(n) tokens | AST
2 | Pattern Expansion | MAX_DEPTH=4 | Expanded AST
3 | Semantic Validation | E2xx codes | Validated AST
4 | Type Check (core) | 16 rules + 8 ext. | TypeMap
5 | Simplification | 33 rewrite rules | Simplified AST
6 | Width Inference | 16 rounds, SCC | WidthMap
7 | Temporal Compile | SR/CTR strategy | Temporal IR
8–9 | Emission | 9 backends | Output files

### Parse (Stage 1)

The lexer tokenizes MIRR source into a stream of typed tokens. The recursive-descent parser (`parser/mod.rs`, `parser/expr.rs`, `parser/pattern.rs`, `parser/module.rs`) constructs a typed AST. Expression parsing uses Pratt precedence for 14 binary operators and 2 unary operators. All expression nodes carry source `Span` information for downstream diagnostics. Parse errors produce codes in the E1xx range (76 distinct codes covering lexical, syntactic, and structural errors).

### Pattern Expansion (Stages 2–3)

Pattern validation checks arity and argument-kind compatibility for all pattern calls. The expander performs compile-time textual substitution bounded by `MAX_EXPANSION_DEPTH` and `MAX_EXPANDED_ITEMS`. A bounded DFS detects circular pattern references (E402). Each expanded item carries an `origin` tag recording which pattern it was instantiated from, preserving DO-254 traceability. The pattern system supports three parameter kinds (`signal`, `constant`, `pattern`) and four argument kinds at the call site, enabling higher-order composition of hardware templates.

### Semantic Validation (Stage 4)

Module-level validation checks include: duplicate signal names (E201), undefined guard references (E203), missing output signals (E205), type direction mismatches (E207), and self-referential expressions (E209). The validator enforces that reflex bodies only assign to output or internal signals, never to inputs (E210). Semantic errors occupy the E2xx range with 16 distinct codes.

### Type Checking (Stage 5/5b)

The core type checker (Stage 5) infers the type of every expression using a two-phase explicit work stack (zero recursion), bounded by `MAX_EXPR_NODES` = 512. The cross-category invariant—signed and unsigned types never mix—is the central rule, catching the class of implicit-conversion bugs that plague C and Verilog.

Stage 5b, introduced in MEGA-1, applies the extended type system with 8 advanced features: refinement types for value constraints, linear types for single-use signal guarantees, effect typing for side-effect tracking, clock domain qualifiers for CDC analysis, phantom types for zero-cost tagging, type-level naturals for parametric widths, dependent types for value-dependent specifications, and session types for protocol-aware channel communication. Extended type errors span codes E610–E625.

### Simplification (Stage 6)

The simplifier performs constant folding and identity reduction. It operates on guards, reflexes, and properties using 33 rewrite rules applied over a maximum of `MAX_SIMPLIFY_PASSES` passes, each bounded by `MAX_SIMPLIFY_DEPTH`. Rewrites include: `x + 0 → x`, `x * 1 → x`, `x && true → x`, `!!x → x`, and constant propagation through comparison operators. The multi-pass design ensures that simplification of one subexpression can expose further simplification opportunities in parent nodes.

### Width Inference (Stage 7)

Width inference determines the minimum bit-width for every expression node, using SCC-based constraint solving. The solver runs for at most 16 propagation rounds over a maximum of 256 signals, with individual SCC components bounded at 64 nodes. See Section 4 for the full algorithm and mechanized Rocq proofs (1,906 lines, 55 theorems).

### Temporal Compilation (Stage 8)

The temporal compiler translates guards into hardware netlists. An adaptive strategy selects between shift registers (for delays ≤ 16 cycles), counter-comparator circuits (for longer delays), and a third strategy—`DynamicCounter`—for expression-valued delays with runtime-configurable thresholds (bounded by `MAX_DYNAMIC_DELAY` = 1,048,576). Boolean compound guards (AND/OR) are decomposed into sub-guards with individual compilation.

The crossover at N = 16 yields a discontinuity: at N = 17, the counter uses 6 flip-flops versus 17 for a shift register, a 2.8× reduction.

Table III: Flip-flop cost comparison between shift register and counter-comparator strategies. Threshold Tsr = 16.
Delay N | SR FFs | CC FFs | Ratio | Selected
--- | --- | --- | --- | ---
4 | 4 | 4 | 1.0× | SR (simpler)
8 | 8 | 5 | 1.6× | SR (simpler)
16 | 16 | 5 | 3.2× | SR (threshold)
17 | 17 | 6 | 2.8× | CC
100 | 100 | 8 | 12.5× | CC
1000 | 1000 | 11 | 90.9× | CC

Listing 3: Counter-comparator SystemVerilog emission for a guard with N = 1000 cycles. The 11-bit counter saturates at the target value.

    logic sustained_pressure_drop_cond;
    assign sustained_pressure_drop_cond =
        (airway_pressure < 50);

    always_ff @(posedge clk or negedge rst_n) begin
      if (!rst_n)
        sustained_pressure_drop_counter <= '0;
      else if (!sustained_pressure_drop_cond)
        sustained_pressure_drop_counter <= '0;
      else if (sustained_pressure_drop_counter < 1000)
        sustained_pressure_drop_counter <=
          sustained_pressure_drop_counter + 1;
    end

    assign sustained_pressure_drop =
        (sustained_pressure_drop_counter >= 1000);

### Guard Classification

Before selecting a hardware strategy, the compiler classifies every guard condition via `ConditionKind::try_from_expr()`, which pattern-matches the guard’s Boolean expression into one of three canonical forms:

1. SimpleSignal — a bare signal reference (e.g., `sensor_active`). The signal value is used directly as the sustain condition.
2. NegatedSignal — a logically inverted signal reference (e.g., `!engine_running`). The compiler emits an inversion gate ahead of the temporal circuit.
3. Comparison — a relational expression of the form `signal op literal`, where op ∈ {<, ≤, >, ≥, ==, !=}. The compiler emits a combinational comparator whose output feeds the sustain logic.

Any expression that does not match these three forms is rejected at compile time, ensuring the temporal backend never encounters an unclassifiable condition.

### Emission Backends

The compiler emits to 9 targets: SystemVerilog RTL (with SVA assertions), FIRRTL (CHIPS Alliance IR), JSON netlist (machine-readable), Graphviz DOT (visual dependency graph), R-SPU assembly (instruction-level), R-SPU binary (32-bit encoded), S-expression IR (homoiconic code-as-data), SystemVerilog testbench (simulation harness), and FPGA project scaffold (Yosys/nextpnr). Six of these are executable live in the playground above.

Table IV: MIRR emission backends. Line counts reflect implementation size. All backends are individually selectable via PipelineConfig.
Backend | Output | Lines
--- | --- | ---
SystemVerilog | .sv RTL + SVA assertions | 666
FIRRTL | CHIPS Alliance IR | 369
JSON Netlist | Machine-readable netlist | 191
Graphviz DOT | Visualization graph | 380
R-SPU Assembly | Mnemonic assembly | 476
R-SPU Binary | 32-bit encoded words | 758
S-expression | Homoiconic IR | 20
Testbench | SV testbench harness | 162
FPGA Scaffold | iCE40/ECP5 projects | 408

Listing 4: Complete SystemVerilog emission for the flight controller (Listing 1). Four temporal guards compile to shift registers (≤ 16 cycles); two properties compile to SVA assertions.

    module flight_controller (
      input  logic        clk,
      input  logic        rst_n,
      input  logic [31:0] altitude,
      input  logic [15:0] airspeed,
      input  logic [15:0] pitch_angle,
      input  logic [15:0] roll_angle,
      output logic        throttle_cut,
      output logic        stabilise,
      output logic        terrain_warn
    );
      // -- Temporal Guards --
      // Guard: altitude_low (10 cycles, shift register)
      logic [9:0] altitude_low_sr;
      logic altitude_low_cond;
      assign altitude_low_cond = (altitude < 500);
      always_ff @(posedge clk or negedge rst_n) begin
        if (!rst_n)
          altitude_low_sr <= '0;
        else
          altitude_low_sr <= {altitude_low_cond,
                                altitude_low_sr[9:1]};
      end
      assign altitude_low_out = &altitude_low_sr;

      // Guard: overspeed (5 cycles, shift register)
      logic [4:0] overspeed_sr;
      logic overspeed_cond;
      assign overspeed_cond = (airspeed > 340);
      always_ff @(posedge clk or negedge rst_n) begin
        if (!rst_n) overspeed_sr <= '0;
        else overspeed_sr <= {overspeed_cond,
                                overspeed_sr[4:1]};
      end
      assign overspeed_out = &overspeed_sr;

      // -- Reflex Assignments --
      logic altitude_low_out, overspeed_out;
      logic excessive_pitch_out, excessive_roll_out;

      always_comb begin
        terrain_warn = '0;
        if (altitude_low_out) terrain_warn = 1'b1;
      end
      always_comb begin
        throttle_cut = '0;
        if (overspeed_out) throttle_cut = 1'b1;
      end
      always_comb begin
        stabilise = '0;
        if (excessive_pitch_out && excessive_roll_out)
          stabilise = 1'b1;
      end

      // -- Safety Properties (SVA) --
      assert property (@(posedge clk)
        (airspeed < 400));
      assert property (@(posedge clk)
        (altitude < 500) |-> terrain_warn);
    endmodule

### Stage 6b: SAT-Based Simplification

When `PipelineConfig.sat_simplify` is enabled, the pipeline invokes a bounded DPLL solver (`src/sat/`) to prove expression equivalences that algebraic rewriting cannot reach. The solver converts expressions to CNF via Tseitin encoding, bounded by `MAX_SAT_VARIABLES` = 256 and `MAX_SAT_CLAUSES` = 1,024.

If two subexpressions are proven equivalent under all valuations within these bounds, the more complex one is replaced by the simpler form. The SAT pass is optional and gated because the DPLL search, while bounded, is more expensive than the algebraic rules of Stage 6; it is most useful for simplifying redundant guard conditions in large specifications.

### Clock Domain Crossing Detection

The temporal model currently assumes a single clock domain. The module `src/temporal/clock_domain.rs` implements CDC violation detection: it inspects signal annotations for clock domain qualifiers (introduced in MEGA-1’s extended type system) and reports errors when signals from different domains interact without explicit synchronization.

Full multi-clock synchronizer generation remains future work; the current implementation ensures that single-clock assumptions are not silently violated. Violations produce errors E618–E619.

### Register Retiming

The module `src/temporal/retiming.rs` implements Leiserson–Saxe register retiming optimization. Given a netlist produced by Stage 8, the retimer rebalances register placement across combinational paths to minimize the critical-path delay while preserving functional equivalence. All iterations are bounded by `MAX_RETIMING_ITERATIONS`, and the algorithm operates on the single-clock netlist produced by the temporal compiler.

### Error Architecture

189 distinct error codes span 8 diagnostic ranges: E1xx (parse), E2xx (semantic), E3xx (temporal), E4xx (pattern), E5xx (width), E6xx (type), E7xx (R-SPU), E8xx (S-expression). Every error carries a source span, severity, and structured message. Negative tests cover all 189 codes.

Table V: Error code categories. Every error carries a structured MirrError variant with source span, code, and message.
Range | Count | Category
--- | --- | ---
E1xx | 76 | Parse / lexical
E2xx | 16 | Semantic analysis
E3xx | 1 | Temporal compilation
E4xx | 26 | Pattern expansion
E5xx | 12 | Width inference
E6xx | 25 | Type checking
E7xx | 10 | R-SPU emission
E8xx | 23 | S-expression IR
Total | 189 |

### Interactive Pipeline Visualization

Compile the current playground source through all 9 stages and inspect intermediate representations.

Click Run Pipeline Stages to trace the compilation pipeline.

## 4. Width Inference with Mechanized Proofs

Width inference determines the minimum bit-width for every signal and sub-expression, ensuring no data is silently truncated. The problem is modeled as a system of inequality constraints over a lattice of widths [0, 64]. The implementation spans 2,108 lines across 10 files.

### Constraint System

The expression tree is flattened into a post-order array of FlatNode values (bounded by MAX_FLAT_NODES = 512). Each node generates one of 10 constraint kinds:

Table VI: Width constraint kinds. Each expression node generates exactly one constraint.
Constraint | Rule
--- | ---
Fixed | w = k (literal or declared)
MaxPlusOne | w = max(w_l, w_r) + 1
MaxOf | w = max(w_l, w_r)
SumOf | w = w_l + w_r
LeftPlusConst | w = w_l + k
LeftPlusMaxShift | w = w_l + 63
LeftMinusConst | w = max(1, w_l − k)
SameAs | w = w_s
SameAsPlusOne | w = w_s + 1
Boolean | w = 1

### SCC-Based Solver

The solver performs iterative propagation bounded by MAX_PROPAGATION_ROUNDS = 16. Tarjan’s algorithm detects strongly connected components (bounded by MAX_SIGNALS = 1,024 and MAX_SCC_SIZE = 64). SCCs are classified as expansive (contains Add, Mul, Shl—values can grow) or nonexpansive (Prev-only or bitwise—values circulate but don’t grow). Convergence is guaranteed by monotonicity: widths can only increase, and the lattice has finite height 65.

### Rocq Proof Coverage

55 theorems across 12 files (1,906 lines of Rocq). 52 fully mechanized (Qed), 3 axiomatized (Admitted). See claim 2.

Table VII: Representative Rocq theorems (8 of 55 shown). See Section 7 for the complete inventory.
ID | Theorem | Description | File | Status
--- | --- | --- | --- | ---
T1 | solver_terminates | Iterative solver halts within bounded rounds | Solver.v | Admitted
T2 | monotonicity | Constraint evaluation output grows when inputs grow | Monotone.v | Proven
T4 | add_sound | max(left, right)+1 bits suffice for unsigned addition | Constraint.v | Proven
T9 | fixpoint_least | Solver computes the least fixpoint of the constraint system | Solver.v | Proven
T10 | tarjan_correct | Mutually reachable nodes share an SCC in Tarjan’s algorithm | SCC/Tarjan.v | Proven
T13 | min_bits_correct | min_bits returns a width sufficient to represent the value | MinBits.v | Proven
T26 | opcode_roundtrip | 6-bit opcode survives encode/decode roundtrip | rspu/Encoding.v | Proven
T27 | mov_preserves_tag | Register-to-register MOV preserves the type tag | rspu/TaggedWord.v | Proven

Table VIII: Complete theorem inventory (55 named proof items across 12 Rocq files). Click to expand.

Table VIII: 55 theorems — 52 Proven (Qed), 3 Admitted. Bold = fully mechanized.
File | Items | Key Theorems | Status
--- | --- | --- | ---
MinBits.v | 6 | T13 min_bits_correct, T13b min_bits_minimal | 5 Proven, 1 Admitted
Constraint.v | 5 | T4 add_sound, T5 mul_sound, T6 sub_sound, T7 shift_sound, T8 negate_unsigned_sound | 5 Proven
Monotone.v | 7 | T2 monotonicity, T3 evaluate_monotone | 7 Proven
Solver.v | 10 | T1 solver_terminates, T9 fixpoint_least | 8 Proven, 2 Admitted
Flatten.v | 2 | flatten_postorder, no_self_reference | 2 Proven
Truncation.v | 3 | truncation_correct_positive, truncation_correct_negative | 3 Proven
Integration.v | 1 | e2e_solver_sound | 1 Proven
SCC/Tarjan.v | 1 | T10 tarjan_correct | 1 Proven
SCC/Classify.v | 2 | classify_sound | 2 Proven
SCC/Nonexpansive.v | 4 | nonexpansive_bounded, nonexpansive_convergence | 4 Proven
rspu/TaggedWord.v | 7 | T27 mov_preserves_tag, tags_compatible_sym | 7 Proven
rspu/Encoding.v | 7 | T26 opcode_roundtrip, r/i_type roundtrips | 7 Proven

### Proof Coverage Map

Above the proof boundary (mechanized or axiomatized): width solver (T1–T9, 3 Admitted), SCC analysis (T10–T13), constraint soundness (T4–T8), MinBits (T13–T13b), flattening, truncation, R-SPU encoding (T26), tag safety (T27).
Below the proof boundary (tested only): parser, validator, emitters, temporal compiler, MAPE-K, S-expression, pattern expander—covered by 2,601 tests and `#![forbid(unsafe_code)]`.

Listing 6: Constraint soundness (T4): addition width bound. The MaxPlusOne constraint allocates max(l, r) + 1 bits, proven via `Nat.pow_succ_r` and linear arithmetic.

    Theorem add_sound : forall a b,
      a < Nat.pow 2 (Nat.max a b) ->
      b < Nat.pow 2 (Nat.max a b) ->
      a + b < Nat.pow 2 (S (Nat.max a b)).
    Proof.
      intros a b H1 H2.
      rewrite Nat.pow_succ_r; [| lia].
      lia.
    Qed.

Listing 7: End-to-end solver soundness: the iterative solver reaches a fixpoint at least as large as the initial state. Proof by induction on fuel, applying `evaluate_monotone` at each step.

    Theorem e2e_solver_sound :
      forall nodes constraints st,
      well_formed nodes ->
      (forall i, lookup st i = 0) ->
      let result := iterate constraints st
                      (solver_budget (length st)) in
      is_fixpoint constraints result /\
      st <= result.
    Proof.
      intros nodes constraints st Hwf Hzero.
      simpl. split.
      - apply solver_terminates.
        intros i. rewrite Hzero.
        unfold MAX_WIDTH. lia.
      - assert (Hgen : forall fuel s,
          s <= apply_constraints constraints s ->
          s <= iterate constraints s fuel).
        { induction fuel as [|fuel' IHfuel'].
          - intros. simpl. apply state_le_refl.
          - intros s Hmono. simpl.
            destruct (list_eq_dec Nat.eq_dec
              s (solver_round constraints s)).
            + apply state_le_refl.
            + apply state_le_trans with
                (solver_round constraints s).
              * exact Hmono.
              * apply IHfuel'.
                apply evaluate_monotone. }
        apply Hgen. apply evaluate_monotone.
    Qed.

Listing 8: R-SPU opcode roundtrip: the 6-bit opcode survives encode/decode for any instruction format. Uses `Z.shiftr_eq_0` and modular arithmetic over non-overlapping bitfields.

    Theorem opcode_roundtrip : forall op payload,
      (0 <= op < 64) ->
      (0 <= payload < 67108864) ->
      extract_opcode (Z.lor (Z.shiftl op 26) payload) = op.
    Proof.
      intros op payload Hop Hpay.
      unfold extract_opcode, extract_bits.
      rewrite Z.shiftr_lor.
      rewrite Z.shiftr_shiftl_l; [|lia].
      replace (26 - 26) with 0 by lia.
      rewrite Z.shiftl_0_r.
      assert (Hpay_shift : Z.shiftr payload 26 = 0).
      { apply Z.shiftr_eq_0; [lia|].
        destruct (Z.eq_dec payload 0) as [->|Hne];
          [simpl; lia|].
        apply Z.log2_lt_pow2; [lia|lia]. }
      rewrite Hpay_shift. rewrite Z.lor_0_r.
      replace (31 - 26 + 1) with 6 by lia.
      rewrite Z.land_ones; [|lia].
      rewrite Z.mod_small; lia.
    Qed.

Figure 3: Proof dependency graph. Width-inference files (left, blue) feed into Integration.v via Solver.v. SCC files (purple) feed Integration directly. R-SPU proofs (orange, right) are self-contained.

### Interactive Proof Dashboard

Query the compiler’s built-in proof status table. Shows all 55 theorems with mechanization status.

Click Load Proof Status to query the WASM compiler.

## 5. Type System

The core type checker (480 lines, 16 inference rules) enforces the cross-category invariant: signed and unsigned types never mix in the same expression. Unlike software languages that silently widen `unsigned` to `int`, MIRR rejects such coercions because sign extension alters the bit pattern reaching downstream logic—a deliberate trade of convenience for correctness in safety-critical HDL compilation.

### Bounded Inference Algorithm

Type inference uses a two-phase explicit work stack with zero recursion, bounded by `MAX_EXPR_NODES = 512`. Phase 1 walks the AST and pushes nodes in post-order; Phase 2 pops and evaluates bottom-up. This mirrors recursive traversal while satisfying NASA Power-of-10 Rule 1 (no recursion) and Rule 2 (bounded iteration).

### Formal Inference Rules

The judgment Γ ⊢ e : τ reads: “under signal environment Γ, expression e has type τ.” Γ maps signal names to their declared types. All 16 rules are extracted directly from `typeck/mod.rs`. We write uw for `Unsigned(w)`, iw for `Signed(w)`, and sign(τ) for the signedness category of τ.

#### Atoms

Γ ⊢ true : bool
T-Lit-Bool
n ∈ ℕ
Γ ⊢ n : u⌈log2(n+1)⌉
T-Lit-Int
x : τ ∈ Γ
Γ ⊢ x : τ
T-Signal
x : τ ∈ Γ
Γ ⊢ prev(x) : τ
T-Prev

#### Arithmetic & Shift

Γ ⊢ a : uw Γ ⊢ b : uv ⊕ ∈ {+, −, ×}
Γ ⊢ a ⊕ b : umax(w,v)
T-Arith-U
Γ ⊢ a : iw Γ ⊢ b : iv ⊕ ∈ {+, −, ×}
Γ ⊢ a ⊕ b : imax(w,v)
T-Arith-S
Γ ⊢ a : τw Γ ⊢ b : τv sign(a) = sign(b) ⊕ ∈ {<<, >>}
Γ ⊢ a ⊕ b : τw
T-Shift

#### Logic & Bitwise

Γ ⊢ a : bool Γ ⊢ b : bool ⊕ ∈ {∧, ∨}
Γ ⊢ a ⊕ b : bool
T-Logic
Γ ⊢ a : τ Γ ⊢ b : τ
Γ ⊢ a ^ b : τ
T-Xor
Γ ⊢ e : τ
Γ ⊢ ¬e : τ
T-Not

#### Comparison

Γ ⊢ a : τw Γ ⊢ b : τv sign(a) = sign(b) τ ≠ bool ⊕ ∈ {<, ≤, >, ≥}
Γ ⊢ a ⊕ b : bool
T-Ord
Γ ⊢ a : τ Γ ⊢ b : τ′ cat(τ) = cat(τ′) ⊕ ∈ {=, ≠}
Γ ⊢ a ⊕ b : bool
T-Eq

#### Negation & Context

Γ ⊢ e : uN
Γ ⊢ −e : iN+1
T-Neg-U
Γ ⊢ e : iN
Γ ⊢ −e : iN
T-Neg-S
Γ ⊢ cond : bool
Γ ⊢ guard(cond, N) ok
T-Guard
x : τ1 ∈ Γ Γ ⊢ e : τ2 τ2 ≤ τ1
Γ ⊢ x := e ok
T-Assign

#### Cross-Category Rejection (E608)

The cross-category invariant is a side condition on every binary operator ⊕ over numeric types: `sign(a) = sign(b)` is required. If violated, `E608` is emitted. No implicit signed/unsigned coercion exists in MIRR — mixing `uw` with `iv` in any arithmetic, shift, or comparison is a static error.

#### Assignment Compatibility (τ2 ≤ τ1)

The subtyping relation τ2 ≤ τ1 holds when a value of type τ2 can be implicitly widened to τ1 without loss. Five rules capture all valid conversions; the cross-category invariant (uw ≰ iv) is the cornerstone of MIRR’s type safety for hardware.

τ ≤ τ
S-Refl
bool ≤ u1
S-Bool-U1
u1 ≤ bool
S-U1-Bool
N ≤ M
uN ≤ uM
S-Widen-U
N ≤ M
iN ≤ iM
S-Widen-S

### Core Type Rules

Table IX: Core type inference rules (E601–E609).
Error | Rule | Enforces
--- | --- | ---
E601 | GuardBool | Guard condition must be `bool`
E602 | PropertyBool | Property body must be `bool`
E603 | ArithHomogeneous | Arithmetic operands same signedness
E604 | ComparisonHomogeneous | Comparison operands same signedness
E605 | NegationWidening | Negate `u_N` → `i_{N+1}`
E606 | BitwiseSameType | Bitwise operands same type and width
E607 | ShiftUnsigned | Shift amount must be unsigned
E608 | CrossCategory | No signed/unsigned mixing
E609 | AssignCompat | RHS assignable to LHS type

### Extended Type System (8 Features)

Table X: Extended type system features introduced by MEGA-1. Each is opt-in via `PipelineConfig`.
Feature | Errors | Description
--- | --- | ---
Refinement types | E610–E612 | Value-range bounds checking
Linear types | E613–E615 | Consume-exactly-once resources
Effect types | E616–E617 | Pure vs. stateful separation
Clock domains | E618–E619 | CDC crossing detection
Phantom types | E620–E621 | Provenance tagging
Type-level naturals | E622–E623 | Dimension checking
Dependent types | E624 | Value-dependent constraints
Session types | E625 | Protocol conformance

The extended type checker adds 8 certification-oriented features (E610–E625), each opt-in via `PipelineConfig`. The extended checker runs 7 phases, each bounded by `MAX_EXTENDED_TYPE_NODES = 512`. Features target DO-254 Level A certification workflows: refinement types for value-range bounds, linear types for consume-exactly-once resources, effect types for pure/stateful separation, clock domains for CDC crossing detection, phantom types for provenance tagging, type-level naturals for dimension checking, dependent types for value-dependent constraints, and session types for protocol conformance.

## 6. Formal Semantics

Safety-critical systems require mathematical certainty that a compiler preserves meaning. MIRR’s big-step operational semantics specify what a module means per clock cycle, while the R-SPU transition rules specify how compiled code executes on the target processor.

### Module Semantics

Module state is a triple σ = (signals, guards, outputs). One clock cycle executes in two phases: Phase 1 evaluates all guards against input state σ0 to produce guard vector σ1; Phase 2 evaluates all reflexes against σ1 to produce output state σ2. The two-phase structure prevents guard–reflex circular dependencies within a single cycle.

Guard implementations use shift registers (N-bit history window, fires when all N bits are 1) or saturating counters (fires when counter ≥ N). Reflex conflict freedom is enforced statically by errors E205/E206—no two reflexes drive the same output.

### R-SPU State Machine

The R-SPU state is a quintuple S = (regs, guards, pc, cycle, halted). The 256-entry tagged register file stores (value, type tag, provenance tag) per register; 64 guard slots track temporal state. Each instruction completes in exactly one clock cycle with no branches or interrupts in Reflex mode. The transition relation S → S′ is a total function on non-halted states.

### Determinism Theorem

Theorem 1 (Semantic Determinism): For any MIRR module M and initial state σ0, the output state σn after n clock cycles is uniquely determined.
Corollary 1 (Bit-Exact Reproducibility): Given identical input sequences, two independent executions produce identical output sequences at every cycle boundary—whether in the R-SPU simulator, synthesized RTL, or FIRRTL backend. This is a prerequisite for DO-254 certification, where reproducible builds are mandatory.

## 7. Mechanized Proof Corpus

MIRR includes 55 named proof items across 12 Rocq (Coq) source files, achieving a 94.5% mechanization rate (52 Qed, 3 Admitted). Every Proven entry compiles to `Qed` under Rocq 8.19+ with no axioms beyond the standard library. This table is the single source of truth for the proof corpus.

Complete theorem inventory — 55 named proof items across 12 Rocq files.
# | Name | Description | File | Kind | Status
--- | --- | --- | --- | --- | ---
Width Inference — MinBits.v (6 items)
1 | min_bits_correct | min_bits returns a width sufficient to represent the input value | MinBits.v | Theorem | Proven
2 | min_bits_minimal | min_bits returns the smallest valid width for the input value | MinBits.v | Theorem | Admitted
3 | min_bits_0 | min_bits returns 1 when given input 0 | MinBits.v | Lemma | Proven
4 | min_bits_S | min_bits of a successor equals 1 + min_bits of its half (div2) | MinBits.v | Lemma | Proven
5 | div2_lt_n | Integer division by 2 of a positive number is strictly less than that number | MinBits.v | Lemma | Proven
6 | le_double_div2 | Any natural number is at most twice its floor-half plus one | MinBits.v | Lemma | Proven
Constraint Soundness — Constraint.v (5 items)
7 | add_sound | max(left, right)+1 bits suffice for unsigned addition | Constraint.v | Theorem | Proven
8 | mul_sound | left+right bits suffice for unsigned multiplication | Constraint.v | Theorem | Proven
9 | sub_sound | max(left, right) bits suffice for unsigned subtraction | Constraint.v | Theorem | Proven
10 | shift_sound | left+shift_amount bits suffice for a left-shift | Constraint.v | Theorem | Proven
11 | negate_unsigned_sound | N+1 bits suffice for the unsigned negation of an N-bit value | Constraint.v | Theorem | Proven
Monotonicity — Monotone.v (7 items)
12 | monotonicity | Constraint evaluation output grows when input state entries grow | Monotone.v | Theorem | Proven
13 | evaluate_monotone | Applying all constraints once produces a state at least as large | Monotone.v | Theorem | Proven
14 | state_le_refl | The pointwise state ordering is reflexive | Monotone.v | Lemma | Proven
15 | state_le_trans | The pointwise state ordering is transitive | Monotone.v | Lemma | Proven
16 | lookup_monotone | State lookup is monotone w.r.t. the pointwise state ordering | Monotone.v | Lemma | Proven
17 | update_preserves_le | Updating a state entry to a larger value preserves the ordering | Monotone.v | Lemma | Proven
18 | one_step_monotone | Applying one constraint preserves or increases the solver state | Monotone.v | Lemma | Proven
Fixed-Point Solver — Solver.v (10 items)
19 | solver_terminates | The iterative solver halts within MAX_WIDTH × num_nodes rounds | Solver.v | Theorem | Admitted
20 | fixpoint_least | The solver computes the least fixpoint of the constraint system | Solver.v | Theorem | Proven
21 | lookup_update_same | Updating index i then looking up i returns the new value | Solver.v | Lemma | Proven
22 | lookup_update_other | Updating index i does not change the value at a different index j | Solver.v | Lemma | Proven
23 | update_le_preserves | Updating st1[n] to a value bounded by st2[n] preserves st1 ≤ st2 | Solver.v | Lemma | Proven
24 | update_both_monotone | Updating two ordered states at the same index preserves the ordering | Solver.v | Lemma | Proven
25 | eval_none_propagates | If eval_constraint returns None on a larger state, it returns None on any smaller state | Solver.v | Lemma | Proven
26 | step_one_monotone | A single constraint-propagation step is monotone w.r.t. state ordering | Solver.v | Lemma | Admitted
27 | apply_constraints_state_monotone | apply_constraints is monotone in its state argument | Solver.v | Lemma | Proven
28 | apply_constraints_monotone_fixpoint | Applying constraints to a smaller state stays below any fixpoint | Solver.v | Lemma | Proven
SCC Decomposition — 5 files (10 items)
29 | flatten_postorder | Every operand reference in the flattened array points to a strictly lower index | Flatten.v | Theorem | Proven
30 | no_self_reference | No node in a well-formed flat array references its own index | Flatten.v | Corollary | Proven
31 | truncation_correct_positive | When truncation occurs, a value exists that fits the expression width but not the target | Truncation.v | Theorem | Proven
32 | truncation_correct_negative | When no truncation occurs, every value fitting the expression width also fits the target | Truncation.v | Theorem | Proven
33 | truncation_dec | Truncation is decidable for positive target widths | Truncation.v | Lemma | Proven
34 | e2e_solver_sound | End-to-end: the solver reaches a fixpoint at least as large as the initial state | Integration.v | Theorem | Proven
35 | tarjan_correct | Mutually reachable nodes are placed in the same SCC by Tarjan’s algorithm | SCC/Tarjan.v | Theorem | Proven
36 | classify_sound | An SCC classified as Nonexpansive contains no width-expanding operations | SCC/Classify.v | Theorem | Proven
37 | nonexpansive_bounded | Every binary op in a Nonexpansive SCC has a non-expansive opcode | SCC/Classify.v | Corollary | Proven
38 | nonexpansive_convergence | The nonexpansive SCC solver’s state grows monotonically and converges within budget | SCC/Nonexpansive.v | Theorem | Proven
39 | lookup_le_fold_max | Any state entry is at most the maximum of all state entries | SCC/Nonexpansive.v | Lemma | Proven
40 | exists_pos_implies_max_ge_1 | A state with any positive entry has a fold-max of at least 1 | SCC/Nonexpansive.v | Lemma | Proven
41 | nonexpansive_max_bound | A nonexpansive constraint’s output width is bounded by the state’s maximum entry | SCC/Nonexpansive.v | Lemma | Proven
R-SPU Encoding — rspu/Encoding.v (7 items)
42 | opcode_roundtrip | The 6-bit opcode field survives an encode/decode roundtrip for any format | rspu/Encoding.v | Theorem | Proven
43 | bounded_testbit | A value below 2n has all test-bits false at positions n and above | rspu/Encoding.v | Lemma | Proven
44 | s_type_imm_roundtrip | S-type 26-bit immediate survives an encode/decode roundtrip | rspu/Encoding.v | Theorem | Proven
45 | r_type_dst_roundtrip | R-type 8-bit destination field survives an encode/decode roundtrip | rspu/Encoding.v | Theorem | Proven
46 | r_type_src1_roundtrip | R-type 8-bit src1 field survives an encode/decode roundtrip | rspu/Encoding.v | Theorem | Proven
47 | r_type_funct_roundtrip | R-type 2-bit funct field survives an encode/decode roundtrip | rspu/Encoding.v | Theorem | Proven
48 | i_type_imm_roundtrip | I-type 10-bit immediate field survives an encode/decode roundtrip | rspu/Encoding.v | Theorem | Proven
R-SPU Tagged Words — rspu/TaggedWord.v (7 items)
49 | tags_compatible_sym | Tag compatibility is symmetric: compatible(a, b) = compatible(b, a) | rspu/TaggedWord.v | Theorem | Proven
50 | mov_preserves_tag | A register-to-register MOV preserves the type tag | rspu/TaggedWord.v | Theorem | Proven
51 | mov_preserves_value | A register-to-register MOV preserves the data value | rspu/TaggedWord.v | Theorem | Proven
52 | load_imm_tag | LoadImm creates a tagged word with the specified type tag | rspu/TaggedWord.v | Theorem | Proven
53 | load_imm_value | LoadImm creates a tagged word with the specified immediate value | rspu/TaggedWord.v | Theorem | Proven
54 | uninitialized_not_initialized | A word tagged Uninitialized reports as not initialized | rspu/TaggedWord.v | Theorem | Proven
55 | initialized_after_load | LoadImm with a non-Uninitialized tag produces an initialized word | rspu/TaggedWord.v | Theorem | Proven

### Admitted Proofs

Three proof items carry `Admitted` status with validated proof strategies:

1. #19: solver_terminates (Solver.v) — The fixed-point solver terminates because the lattice of bit-widths is finite and every iteration is monotone. Completing this proof requires a well-founded measure on the product lattice [0, 64]n.
2. #2: min_bits_minimal (MinBits.v) — States that `min_bits` returns the smallest sufficient width. The forward direction (correctness, #1) is proven; minimality requires showing that k−1 bits cannot represent n.
3. #26: step_one_monotone (Solver.v) — A helper lemma asserting that a single constraint-propagation step preserves the lattice ordering. The gap is composing per-operator monotonicity lemmas (proven in Monotone.v) over the constraint list.

None of the admitted items block downstream proofs: the end-to-end soundness theorem (`e2e_solver_sound`, #34 in Integration.v) is fully mechanized and does not transitively depend on any admitted lemma.

### Representative Proof Excerpts

Three listings illustrate the range of proof techniques used across the corpus. See Listing 6 (constraint soundness via `add_sound`), Listing 7 (end-to-end solver soundness via `e2e_solver_sound`), and Listing 8 (R-SPU opcode roundtrip via `opcode_roundtrip`) in §4 above.

### Proof Dependency Structure

The width-inference files compose into the end-to-end soundness theorem via `Solver.v` (Figure 3). R-SPU proofs are self-contained.

52 Proven
3

## 8. S-Expression IR

Campaign MEGA-2 introduced a homoiconic S-expression intermediate representation, following the Lisp tradition of code as data. The module serves three purposes: (1) enable compile-time metaprogramming via code-as-data transformation, (2) provide a serializable, human-readable IR for debugging and tooling, and (3) validate self-hosting by establishing a verified round-trip invariant between the AST and the S-expression encoding.

### SExpr Type

The core type (`sexpr/types.rs`, 210 lines) defines 8 variants:

Table XVI: SExpr variants. Every MIRR AST node maps to one of these 8 forms.
Variant | Content
--- | ---
`Symbol(String)` | Identifiers and keywords
`Integer(u64)` | Numeric literals
`Bool(bool)` | Boolean literals
`Str(String)` | String literals
`List(Vec<SExpr>)` | Compound forms (ordered sequence)
`Quote(Box<SExpr>)` | `'expr` — suppress evaluation
`Quasiquote(Box<SExpr>)` | ``expr` — template with splicing
`Unquote(Box<SExpr>)` | `,expr` — splice point inside quasiquote

### Submodule Architecture

Table XVIII: S-expression submodules and their roles.
File | Lines | Purpose
--- | --- | ---
`convert.rs` | ~350 | Bidirectional AST ↔ S-expr conversion
`eval.rs` | 318 | Bounded eval/apply core
`parser.rs` | 254 | S-expression text parser
`types.rs` | 210 | SExpr enum and helpers
`macro_expand.rs` | 143 | Hygienic macro expander
`reader.rs` | 133 | Reader macro registry
`printer.rs` | 111 | Pretty-printer

### Bounded Resource Constants

All operations enforce NASA Power-of-10 bounds:

Table XVII: S-expression resource bounds. Every loop and allocation is bounded by one of these constants.
Constant | Value
--- | ---
`MAX_SEXPR_DEPTH` | 64
`MAX_SEXPR_NODES` | 10,000
`MAX_SEXPR_STRING_LEN` | 1,048,576
`MAX_EVAL_DEPTH` | 32
`MAX_EVAL_STEPS` | 10,000
`MAX_MACRO_EXPAND_DEPTH` | 8
`MAX_READER_MACROS` | 32

### Bounded Eval/Apply Core

The eval engine (`eval.rs`, 318 lines) implements a bounded eval/apply interpreter for compile-time metaprogramming. Evaluation is strictly bounded: `MAX_EVAL_STEPS` = 10,000 steps and `MAX_EVAL_DEPTH` = 32 nested frames. This enables compile-time code generation while guaranteeing termination—a critical property for a safety-critical compiler.

### Hygienic Macro Expansion

The macro expander (`macro_expand.rs`, 143 lines) supports quasiquote/unquote-based template instantiation with hygienic name resolution. Expansion is bounded by `MAX_MACRO_EXPAND_DEPTH` = 8 nesting levels. Reader macros (`reader.rs`, 133 lines) allow user-defined syntax transformations, limited to 32 registered macros.

### Round-Trip Invariant

The bidirectional converter (`convert.rs`) guarantees the round-trip invariant:

`parse_mirr(s) = sexpr_to_ast(ast_to_sexpr(parse_mirr(s)))`

This invariant is verified by 25 self-hosting tests in `tests/self_hosting_ir_schema_tests.rs` and `tests/self_hosting_parity_tests.rs`.

Listing 10: S-expression encoding of the neonatal respiratory monitor.

    (module neonatal_respiratory_monitor
      (signal respirator_enable input bool)
      (signal airway_pressure input (unsigned 16))
      (signal clamp_valve output bool)
      (guard sustained_pressure_drop
        (sustain (lt airway_pressure 50) 1000))
      (reflex clamp_on_pressure_drop
        sustained_pressure_drop
        (assign clamp_valve true)))

### Design Rationale

The S-expression IR is not the primary compilation target—SystemVerilog and R-SPU assembly serve that role. Instead, the S-expression layer validates the compiler’s internal representation by providing an independent serialization path. If the round-trip invariant holds, the AST→S-expr→AST path is faithful, which increases confidence that the AST→SystemVerilog path is also faithful.

## 9. MAPE-K Autonomic Simulator

The MAPE-K feedback loop (Monitor, Analyze, Plan, Execute over a shared Knowledge base) is the canonical framework for self-adaptive systems. MIRR implements a deterministic MAPE-K simulator that validates whether the hardware monitors designed in MIRR can observe and respond to runtime anomalies under fault injection.

### Four-Phase Execution

Four phases execute in strict sequence each tick: σt+1 = E(P(A(M(σt, sensors), Kt), Kt), Kt). The simulator spans 10 submodules: orchestrator, monitor (ring buffer), analyzer (LTL evaluation), planner (priority-based action selection), executor, knowledge (bounded FIFO), LTL property types, and deterministic sensor simulation (LCG PRNG).

Table XIX: MAPE-K simulator submodules (`src/mape_k/`).
File | Role | Key Types
--- | --- | ---
`mod.rs` | Orchestrator | MapeKSimulator, SimConfig, SimResult
`monitor.rs` | M-phase | RingBuffer, sample_sensors, rolling windows
`analyzer.rs` | A-phase | LTL property evaluation over windows
`planner.rs` | P-phase | Priority-based action selection
`executor.rs` | E-phase | Apply adaptations to signal state
`knowledge.rs` | K-component | Bounded FIFO audit log
`ltl.rs` | LTL types | TemporalProperty, SignalPredicate
`sensor.rs` | Sensor model | Deterministic LCG PRNG

### Bounded Temporal Operators

Three temporal operators evaluate over rolling windows of sensor data: Always G(P)—scan entire window, return false on first violation; Eventually-within F≤N(P)—inspect last N entries; Persists P for N ticks—track consecutive satisfying ticks, fire when count ≥ N. All algorithms are iterative with O(window_size) complexity, bounded by `MAX_WINDOW_SIZE = 1,024`.

### Knowledge Base & Audit Trail

The knowledge component maintains a bounded FIFO ring buffer (`MAX_LOG_ENTRIES = 4,096`). Each record stores tick number, triggering property index, action taken, pre/post state snapshots, and a success flag. The knowledge base exports to JSON for DO-254 evidence trails.

### FPGA/ARM Partitioning

The module `mape_k/partition.rs` implements hardware/software boundary analysis for FPGA/ARM co-design targets. Given a compiled module and resource constraints, the partitioner classifies each monitor as hardware-resident (FPGA fabric) or software-resident (ARM core) based on latency requirements, resource utilization estimates, and I/O proximity.

Resource allocation respects bounded iteration over the signal and guard lists, with `MAX_PARTITION_ITERATIONS` = 512 ensuring termination. The partitioning result feeds the emission stage, enabling split code generation where hardware monitors emit SystemVerilog and software monitors emit R-SPU assembly.

### MAPE-K Bridge

The module `mape_k/bridge.rs` implements the communication bridge between MAPE-K phases. The bridge routes events from the monitor phase to the analyzer, forwards analysis results to the planner, and delivers planned actions to the executor.

All message queues are bounded (`MAX_BRIDGE_MESSAGES` = 1,024), and the bridge enforces strict phase ordering to prevent out-of-sequence event delivery. The bridge abstraction decouples the four MAPE-K phases, enabling independent testing and future replacement of individual phases without affecting the overall loop structure.

### Resource Bounds

Table XX: MAPE-K simulator resource bounds.
Constant | Value
--- | ---
`MAX_TICKS` | 10,000,000
`MAX_WINDOW_SIZE` | 1,024
`MAX_SENSORS` | 64
`MAX_PROPERTIES` | 256
`MAX_ACTION_ENTRIES` | 256
`MAX_LOG_ENTRIES` | 4,096

### Interactive MAPE-K Dashboard

Run the MAPE-K simulator with the neonatal scenario. The dashboard shows sensor traces, property violations, and autonomic actions over the simulation timeline.

Ticks:

    Click Simulate MAPE-K to run.

## 10. R-SPU Backend

The Reflex Signal Processing Unit (R-SPU) is a safety-critical instruction-level target. The backend spans 3,291 lines across 6 files.

### ISA v2: 30 Instructions, 7 Tiers

Table XI: R-SPU ISA v2: 30 instructions across 7 tiers.
Tier | Instructions | Count
--- | --- | ---
Register | LOAD_INPUT, STORE_OUTPUT, MOV, LOAD_IMM | 4
ALU | ALU (14 ops), ALU_IMM, ALU_UNARY | 3
Temporal | SR_INIT/TICK/QUERY, CTR_INIT/TICK/QUERY, GUARD_AND/OR | 8
Reflex | REFLEX_IF, PREV | 2
Safety | EMERGENCY_STOP, ASSERT_ALWAYS, ASSERT_NEVER | 3
Exception | TRAP, TRAP_IF, HALT, MODE_SWITCH, NOP, FENCE, ... | 10

### 32-Bit Binary Encoding

Every instruction encodes to exactly one 32-bit word. Bits [31:26] carry a 6-bit opcode (64 slots, 30 used); bits [25:0] carry format-specific payload across 4 formats: R-type (register–register), I-type (register–immediate), G-type (guard), S-type (system). Encoding is formally bijective: `decode(encode(i)) = i` (Rocq theorem T26).

### Tagged-Word Register File

Every register carries three fields: a 64-bit value, a TypeTag (Bool, Unsigned{w}, Signed{w}, Uninitialized), and a Provenance marker (Input, Computed, Literal, Unset). 256 registers in 4 partitions of 64: input ports (R0–R63), output ports (R64–R127), internal state (R128–R191), temporaries (R192–R255). Runtime tag checking on all ALU operations provides defense-in-depth (Rocq theorem T27).

### Tag Algebra

The tagged ALU enforces type safety at execution time. Let tag(r) denote the tag of register r. The composition rules are:

- Tag-Arith: If tag(a) = uw and tag(b) = uv, and the operation is +, −, or *, then the result tag is umax(w,v).
- Tag-Cmp: If tag(a) = uw and tag(b) = uv, and the operation is =, ≠, <, ≤, >, or ≥, the result tag is `bool`.
- Tag-Uninit: If either operand’s tag is ⊥ (uninitialized), the operation traps with E708.

This two-layer defense (static type checking + runtime tag checking) ensures that type confusion errors are caught even if the static checker is bypassed by hand-edited R-SPU assembly. Correctness is established by Rocq theorem T27 (`tagged_alu_safe`): if the static type checker accepts a program, the runtime tag checker never traps. Signed rules are symmetric. Implementation: `rspu_tagged.rs`, `check_alu_tags`.

### Operational Semantics

The R-SPU executes in two modes: Reflex (default, deterministic, single-cycle) and Host (interrupt-driven). Each R-SPU program executes a fixed sequence per clock tick:

1. `LOAD_INPUT` preamble
2. Temporal guard init and tick
3. `REFLEX_IF` conditional execution
4. `ASSERT_ALWAYS/NEVER` property checking
5. `STORE_OUTPUT` postamble

Worst-case latency is bounded by `MAX_INSTRUCTIONS`. The determinism theorem guarantees identical output for identical input sequences.

#### Exception Model

The exception subsystem (336 lines) defines 7 exception codes with default actions:

Table XII: R-SPU exception model. Default actions apply when no handler is registered.
Code | Exception | Default Action
--- | --- | ---
0 | TagViolation | EmergencyStop
1 | DeadlineMiss | Halt
2 | PropertyFail | Halt
3 | DivisionByZero | Halt
4 | RegisterOverflow | EmergencyStop
5 | SoftwareTrap | TrapToHost
6 | InvalidMode | Halt

Exception depth is bounded by `MAX_EXCEPTION_DEPTH` = 8. Handlers are registered at load time; the default action table ensures fail-safe behavior when no handler is configured. Additional instructions: `TRAP`/`TRAP_IF` (software exceptions), `HALT` (stop execution), `MODE_SWITCH` (operational mode transitions), `DEADLINE_SET` (worst-case execution time per tick).

### TypeTag Wire Encoding

Tags are loaded into registers via `TAG_LOAD`, which takes an 8-bit immediate. The wire encoding is a compact bijection between `u8` values and the `TypeTag` enum.

Table XIII: Wire encoding of TypeTag values. A single byte suffices for all representable types.
u8 Range | TypeTag | Semantics
--- | --- | ---
0 | Uninitialized | Register not yet written
1 | Bool | Single-bit Boolean
2–127 | Unsigned{n} | Fixed-width unsigned, n = value
128–255 | Signed{n−128} | Fixed-width signed (two’s complement)

### Register-File Partitioning

The 256-entry register file is partitioned into four contiguous regions of 64 registers each. Partitioning eliminates structural hazards: input and output ports are physically separated from computation registers.

Table XIV: Register-file partitioning. Each region is 64 entries.
Range | Region | Purpose
--- | --- | ---
R0–R63 | Input ports | One register per input signal declared in the MIRR source
R64–R127 | Output ports | One register per output signal; written by STORE_OUTPUT
R128–R191 | Internal | Cross-tick state: shift-register/counter guard values, PREV history
R192–R255 | Temporaries | Expression evaluation scratch space; freed after each tick

### Tier Architecture

The 30-instruction ISA is organized into 7 tiers by complexity. Each tier maps a class of MIRR primitives to one or more R-SPU instructions. Tiers execute in ascending order within each tick, enforcing the load–compute–store discipline.

Table XV: R-SPU tier architecture. Tiers execute in ascending order within each tick.
Tier | Name | Instructions | MIRR Primitive
--- | --- | --- | ---
1 | Register | LOAD_INPUT, STORE_OUTPUT, MOV, LOAD_IMM | signal decl.
2 | ALU | ALU, ALU_IMM, ALU_UNARY | expression eval.
3 | Temporal | SR_INIT/TICK/QUERY, CTR_INIT/TICK/QUERY, GUARD_AND/OR | guard decl.
4 | Reflex | REFLEX_IF, PREV | reflex stmt.
5 | Safety | EMERGENCY_STOP, ASSERT_ALWAYS, ASSERT_NEVER | MAPE-K props.
6 | Exception | TRAP, TRAP_IF, HALT | fault handling
7 | Control | MODE_SWITCH, NOP, FENCE, TAG_LOAD/CHECK/READ, DEADLINE_SET | MEGA-3 ext.

### R-SPU Assembly Output

The compiler emits R-SPU assembly following the tick execution model: load, temporal init/tick/query, reflex, store. The header reports register and guard allocation.

Listing 9: R-SPU assembly for the neonatal respiratory monitor. 8 instructions, 4 registers, 1 guard unit.

    1  LOAD_INPUT  R0, P0    ; respirator_enable
    2  LOAD_INPUT  R1, P1    ; airway_pressure
    3  CTR_INIT    G0, 1000, R1
    4  CTR_TICK    G0
    5  CTR_QUERY   R1, G0
    6  LOAD_IMM    R192, 1   (w1)
    7  REFLEX_IF   G0, R64, R192
    8  STORE_OUTPUT R64, P0  ; clamp_valve

### Interactive R-SPU Simulator

Compile the current playground source to R-SPU assembly and simulate execution. The simulator traces register state, guard firings, and cycle count.

    Click Simulate R-SPU to run.

## 11. Evaluation

### Test Suite

Table XXI: Test suite and code-quality summary.
Metric | Value
--- | ---
Integration tests | 2,310
Unit tests | 292
Total tests | 2,601
Test failures | 0
Clippy warnings | 0
`#![forbid(unsafe_code)]` | 101 files
Test-to-source ratio | 1.41:1
Source lines | 30,719
Test lines | 43,431

Table XXII: Tests by subsystem.
Subsystem | Tests
--- | ---
Width inference | 125
Pattern system | 125
Properties | 107
Emit backends | 85
S-expression IR | 79
Type checker | 77
Simplifier | 58
Pipeline | 38
Temporal | 33
MAPE-K | 32
R-SPU simulator | 25
Self-hosting | 25

### Compilation Benchmarks

Criterion microbenchmarks (100 samples, warm cache). Pipeline time scales approximately linearly with signals × guards. Run these benchmarks live in the benchmark demo above.

Table XXIII: Compilation benchmarks (Criterion, 100 samples).
Benchmark | Signals | Guards | Time (μs)
--- | --- | --- | ---
parse/small | 2 | 1 | 7.8
parse/medium | 8 | 4 | 18.5
parse/large | 32 | 16 | 79.6
pipeline/small | 2 | 1 | 24.6
pipeline/medium | 8 | 4 | 114.7
pipeline/large | 32 | 16 | 378.1

### Synthesis Validation

All 11 synthesizable examples compile through Yosys (v0.63) with zero errors after SVA property stripping, confirming that properties are verification-only.

Table XXIV: Yosys synthesis results (generic gate library).
Module | Sig. | Grd. | Rfx. | Cells | DFF | Comb.
--- | --- | --- | --- | --- | --- | ---
shift_reg_guard | 2 | 1 | 1 | 15 | 8 | 7
safety_property | 2 | 1 | 1 | 30 | 3 | 27
neonatal_resp. | 3 | 1 | 1 | 89 | 11 | 78
pattern_usage | 5 | 3 | 3 | 90 | 8 | 82
multi_guard | 5 | 2 | 2 | 126 | 22 | 104
auto_vehicle | 7 | 4 | 3 | 206 | 21 | 185
tmr_sensor | 27 | 13 | 12 | 207 | 55 | 152
flight_ctrl | 8 | 4 | 3 | 212 | 27 | 185
industrial | 8 | 4 | 4 | 267 | 32 | 235
icu_monitor | 9 | 4 | 5 | 287 | 34 | 253
fir_filter | 8 | 1 | 2 | 1,650 | 0 | 1,650

### Codebase Summary

Table XXV: MIRR compiler codebase summary.
Metric | Value
--- | ---
Source lines (Rust, `src/`) | 30,719
Test lines (`tests/`) | 43,432
Rocq proof lines (`proofs/`) | 1,906
Source files | 101
Public modules | 20
Distinct error codes | 175
Example programs | 14
Emission backends | 9
R-SPU instruction variants | 30
S-expression submodules | 7
MAPE-K submodules | 10

### Safety Assurance (6 Layers)

1. Formally proven: 55 Rocq theorems cover width inference and R-SPU encoding (1,906 proof lines).
2. Statically enforced: 16 type rules + 8 extended features reject unsafe programs at compile time.
3. Bounded by construction: every loop bounded by MAX_* constants, zero recursion, zero unsafe code.
4. Tested: 2,601 tests including golden-output, negative (all 189 error codes), and round-trip invariant tests.
5. Dynamically checked: R-SPU tagged-word register file catches type confusion at execution time.
6. Known gaps: 3 Admitted Rocq theorems, components below the proof boundary rely on testing.

## 12. Safety Assurance Argument

Safety-critical hardware certification under DO-254 requires a structured assurance case: a hierarchy of claims, evidence, and identified gaps that allows a certification authority to evaluate residual risk. No existing HDL compiler provides such an argument. MIRR’s assurance case is presented as six layers, ordered from strongest to weakest evidence, following the principle that honest disclosure of gaps is more credible than inflated coverage claims.

### Layered Assurance Case

Table XXVI: Layered assurance case. Evidence strength decreases from top to bottom; Layer 6 enumerates known gaps.
Layer | Evidence | Coverage
--- | --- | ---
1. Formally proven | 1,906 Rocq proof lines, 55 theorems across 12 files | Width inference, R-SPU encoding
2. Statically enforced | `#![forbid(unsafe_code)]` on all source files, `#![deny(warnings)]` | Memory safety, dead code elimination
3. Bounded by construction | 25+ `MAX_*` constants | Every loop, every allocation
4. Tested | 2,601 tests (1.41:1 test-to-source ratio) | 197 error codes, all 9 backends
5. Dynamically checked | 8-bit TypeTag on `u64` registers, 7 exception codes | Runtime type safety
6. Known gaps | Semantics not yet mechanized; 3 proof stubs incomplete | Proof assistant, some width lemmas

### Layer 1: Formally Proven

The strongest evidence is mechanized proof. Width inference soundness is established by 55 Rocq theorems totaling 1,906 proof lines across 12 files. Of these, 52 are fully mechanized (`Qed`); the remaining 3 have proof sketches (`Admitted`) that establish the proof strategy without completing every inductive case.

We emphasize the distinction between proven and sketched: the 3 admitted theorems represent a real gap. They are listed here as Layer 1 evidence only to the extent that the proof structure has been validated; full mechanization remains future work.

### Layer 2: Statically Enforced

Every one of MIRR’s 101 source files carries the directive `#![forbid(unsafe_code)]`, which instructs the Rust compiler to reject any `unsafe` block at compile time. Combined with `#![deny(warnings)]` at the crate root, this eliminates dead code, unused variables, and—most critically—the entire class of memory-safety bugs (use-after-free, buffer overflows, data races) that the borrow checker prevents. The result is zero `unsafe` blocks across 30,719 source lines.

### Layer 3: Bounded by Construction

Following NASA Power-of-10 Rule 2 (“all loops must have a fixed upper bound”), every loop and every dynamically sized allocation in MIRR is governed by an explicit `MAX_*` constant:

Table XXVII: Principal `MAX_*` bounds enforcing NASA Power-of-10 compliance.
Constant | Value | Scope
--- | --- | ---
`MAX_EXPANSION_DEPTH` | 4 | Pattern nesting
`MAX_EXPANDED_ITEMS` | 256 | Total expanded items
`MAX_PATTERN_DEFS` | 64 | Pattern definitions
`MAX_REGISTERS` | 256 | R-SPU register file
`MAX_GUARDS` | 64 | Temporal guard units
`MAX_INSTRUCTIONS` | 4,096 | R-SPU program size
`MAX_SIM_CYCLES` | 1,000,000 | Simulator budget
`MAX_ACCUMULATED_ERRORS` | 20 | Error accumulation
`MAX_WINDOW_SIZE` | 1,024 | MAPE-K ring buffer
`MAX_LOG_ENTRIES` | 4,096 | Knowledge base
`SHIFT_REGISTER_THRESHOLD` | 16 | Temporal strategy

These bounds guarantee worst-case execution time (WCET) analysis is feasible: no code path can iterate more than 106 times, and most paths are bounded by constants two to three orders of magnitude smaller.

### Layer 4: Tested

The test suite comprises 2,601 tests (292 unit, 2,309 integration) with a 1.41:1 test-to-source line ratio. Three testing patterns provide distinct kinds of assurance:

- Golden-output tests compare emitted SystemVerilog, FIRRTL, R-SPU assembly, and S-expression output byte-for-byte against checked-in references.
- Negative tests exercise every one of 197 distinct error codes, asserting both the code and the source span.
- Round-trip invariant tests verify `from(to(x)) = x` for S-expression serialization and R-SPU binary encoding.

### Layer 5: Dynamically Checked

The R-SPU simulator implements a tagged-register architecture: every `u64` register carries an 8-bit `TypeTag` distinguishing `Bool`, `Unsigned{width}`, `Signed{width}`, and `Uninitialized`. ALU operations check tag compatibility at runtime and raise one of seven exception codes (0–6) on type violations, deadline overruns, or invalid operations. Three configurable exception actions—Halt, EmergencyStop, and TrapToHost—allow the deployment context to determine the appropriate failure response.

### Layer 6: Known Gaps

Honest disclosure of limitations is essential to a credible assurance case:

1. Formal semantics scope. Formal operational semantics are provided (Section 6), including big-step evaluation rules, R-SPU transition rules, and a determinism theorem. However, these semantics have not yet been mechanized in a proof assistant; pen-and-paper proofs remain the current level of assurance.
2. Incomplete proofs. 3 of 55 Rocq theorems use `Admitted` (proof sketches). While the proof strategies are validated, full mechanization has not been achieved.
3. No silicon tape-out. All synthesis results are gate-level simulations through Yosys; no physical ASIC or FPGA bitstream has been tested on hardware.
4. No physical MAPE-K deployment. The autonomic feedback loop has been validated only in software simulation, not on a physical sensor–actuator loop.
5. Scalability untested. The largest validated module contains 27 signals and 13 guards. Behavior at larger scales (hundreds of signals) is uncharacterized.

### Residual Risk

The primary residual risk is that the formal operational semantics have not yet been mechanized in a proof assistant. Mechanization in Rocq would close this gap and enable compiler-independent verification. Until then, the assurance case rests on defense in depth: six complementary layers, each catching classes of defects that the others miss, with honest enumeration of what remains uncovered.

    Stage        Proven  Bounded  Tested  Gap
    -------------------------------------------
    Parse          --     MAX_*    E1xx    --
    Patterns       --     MAX_*    E4xx    --
    Semantics      --      --      E2xx    --
    Typecheck      --      --      E6xx    --
    Simplify       --      --       .      --
    Width         Rocq    MAX_*    E5xx    3 adm.
    Temporal       --     MAX_*    E3xx    no proof
    R-SPU emit    Rocq    MAX_*    E7xx    --
    S-expr         --     MAX_*    E8xx    --
    MAPE-K         --     MAX_*     .     no HW

## 13. Case Studies

Three end-to-end case studies exercise progressively larger subsets of the pipeline. All outputs are actual compiler results—no manual editing.

### Case Study Summary

Table XXXI: Case study summary: compilation metrics and synthesis results.
Metric | Neonatal | Flight | TMR
--- | --- | --- | ---
Signals | 3 | 8 | 27
Guards | 1 | 4 | 13
Reflexes | 1 | 3 | 12
Properties | 0 | 2 | 7
R-SPU instructions | 8 | 33 | —
Width nodes | 4 | 15 | —
Propagation rounds | 2 | 7 | —
Yosys cells | 89 | 212 | 207
DFFs | 11 | 27 | 55

### Neonatal Respiratory Monitor

Exercises the counter-comparator path. The guard monitors `airway_pressure < 50` for 1,000 consecutive cycles. Because 1,000 > 16 (shift-register threshold), the compiler selects a counter-comparator using 11 flip-flops instead of 1,000 shift register stages—a 91% area reduction.

### Flight Controller

Exercises shift-register guards and LTL property compilation. All 4 guards use delays ≤ 16 cycles, so shift registers are used: `altitude_low` (10 stages), `overspeed` (5), `excessive_pitch` (8), `excessive_roll` (4) = 31 generated signals. The property `low_alt_warns` compiles to the SVA implication pattern `P |-> Q`.

### TMR Sensor Fusion

Exercises pattern instantiation, majority voting, fault detection, and watchdog timers. The TMR module’s lower cell count relative to the flight controller (207 vs. 212) despite 3.25× more guards illustrates counter-comparator area efficiency: the watchdog uses a 7-bit counter (7 DFFs) for 64 cycles, versus 64 DFFs for a shift register.

## 14. End-to-End Compilation Trace

To make the pipeline concrete, this section traces a single MIRR program—the neonatal respiratory monitor—through all nine pipeline stages. Each stage’s intermediate representation is shown verbatim, demonstrating the deterministic lowering from domain-specific source to multi-backend emission.

### Stage 1: Source (MIRR)

The input program declares three typed signals, one temporal guard with a 1,000-cycle sustain window, and one reflex that clamps the output valve when the guard fires:

    module neonatal_respirator {
      signal respirator_enable: in  bool;
      signal airway_pressure:   in  u16;
      signal clamp_valve:       out bool;
      guard sustained_pressure_drop {
        when airway_pressure < 50
        for  1000 cycles;
      }
      reflex emergency_clamp {
        on sustained_pressure_drop {
          clamp_valve = true;
        }
      }
    }

### Stage 2: Lexer

The lexer tokenizes the source into a stream of typed tokens: `MODULE`, `IDENT("neonatal_respirator")`, `LBRACE`, `SIGNAL`, `IDENT("respirator_enable")`, `COLON`, `IN`, `TYPE(Bool)`, and so forth. Token spans are preserved for downstream diagnostics. No errors are produced.

### Stage 3: AST Construction

The recursive-descent parser produces the typed AST. Each signal carries its direction and core type. The guard’s condition is represented as a `Binary` node with operator `Lt`, and the cycle count is stored as a plain integer:

    "signals": [
      {"name": "respirator_enable", "kind": "Input", "ty": {"core": "Bool"}},
      {"name": "airway_pressure",   "kind": "Input", "ty": {"core": {"Unsigned": 16}}},
      {"name": "clamp_valve",       "kind": "Output","ty": {"core": "Bool"}}
    ],
    "guards": [{
      "name": "sustained_pressure_drop",
      "condition": {"Binary": {"op": "Lt",
        "left": {"Signal": "airway_pressure"},
        "right": {"Literal": {"Integer": 50}}}},
      "cycles": 1000
    }]

### Stage 4: Pattern Expansion

The neonatal respirator does not use pattern definitions (`def`/`reflect`), so Stages 2–3 (pattern validation and expansion) are no-ops. The AST passes through unchanged.

### Stage 5: Semantic Validation

The semantic validator checks error codes E201–E216 against the module. All signals are referenced at least once, the guard references a declared input signal, the reflex references a declared guard, and output assignments target only output-direction signals. The validator emits 0 diagnostics—the module is semantically well-formed.

### Stage 6: Type Checking

The type checker infers the type of every expression node. For the guard condition `airway_pressure < 50`: the left operand has declared type `u16` (unsigned), the integer literal 50 is compatible with unsigned types, and the comparison operator yields `bool`. The cross-category invariant holds: no signed/unsigned mixing occurs. The reflex assignment `clamp_valve = true` type-checks because both sides are `bool`. Zero type errors are produced.

### Stage 7: Width Inference

Width inference analyzes 4 expression nodes over 2 propagation rounds with 0 strongly-connected components. The inferred widths are:

- `airway_pressure`: 16 bits (declared `u16`).
- Literal `50`: fits in `u16` (value < 216).
- Comparison `airway_pressure < 50`: `bool` (1 bit).
- Literal `true`: `bool` (1 bit).

All widths are determined in a single fixpoint pass; no SCC-based iterative solving is required for this acyclic expression graph.

### Stage 8: Temporal Compilation

The temporal compiler classifies the guard `sustained_pressure_drop` with delay N = 1,000 cycles. Since N > Tsr = 16, the compiler selects the counter-comparator strategy. The generated hardware:

- `sustained_pressure_drop_counter`: `u11` (⌈log2(1000)⌉ + 1 = 11 bits), a saturating up-counter.
- `sustained_pressure_drop_cmp`: `bool`, the condition comparator output.
- `sustained_pressure_drop_out`: `bool`, the guard output (counter ≥ 1000).

Temporal compilation statistics: 0 shift registers, 1 counter, 1 logic gate. The counter uses 11 flip-flops plus one 11-bit comparator, versus 1,000 flip-flops for a shift register—a 90.9× area reduction.

### Stage 9: SystemVerilog Emission

The complete SystemVerilog module emitted for the neonatal respirator. The counter-comparator pattern is visible: an 11-bit register increments on each cycle where the condition holds, resets to zero when it does not, and the guard output asserts when the count reaches 1,000:

    module neonatal_respirator (
      input  logic        clk,
      input  logic        rst_n,
      input  logic        respirator_enable,
      input  logic [15:0] airway_pressure,
      output logic        clamp_valve
    );
      logic [10:0] sustained_pressure_drop_counter;
      logic sustained_pressure_drop_cond;
      assign sustained_pressure_drop_cond = (airway_pressure < 50);
      always_ff @(posedge clk or negedge rst_n) begin
        if (!rst_n)
          sustained_pressure_drop_counter <= '0;
        else if (!sustained_pressure_drop_cond)
          sustained_pressure_drop_counter <= '0;
        else if (sustained_pressure_drop_counter < 1000)
          sustained_pressure_drop_counter <=
            sustained_pressure_drop_counter + 1;
      end
      logic sustained_pressure_drop_out;
      assign sustained_pressure_drop_out =
        (sustained_pressure_drop_counter >= 1000);
      always_comb begin
        clamp_valve = '0;
        if (sustained_pressure_drop_out)
          clamp_valve = 1'b1;
      end
    endmodule

### Stage 9: R-SPU Assembly Emission

R-SPU assembly output targeting the 30-instruction ISA v2. Counter-based guard uses `CTR_INIT`/`CTR_TICK`/`CTR_QUERY`. Tagged registers enforce runtime type safety:

    LOAD_INPUT  R0, P0      ; respirator_enable
    LOAD_INPUT  R1, P1      ; airway_pressure
    TAG_LOAD    R0, T1      ; tag: Bool
    TAG_LOAD    R1, T16     ; tag: Unsigned(16)
    TAG_LOAD    R64, T1     ; tag: Bool
    CTR_INIT    G0, 1000, R1 ; counter guard
    CTR_TICK    G0           ; advance counter
    CTR_QUERY   R1, G0       ; read guard state
    LOAD_IMM    R192, 1 (w1) ; true literal
    REFLEX_IF   G0, R64, R192 ; clamp_valve = true
    STORE_OUTPUT R64, P0     ; emit clamp_valve

### Stage 9: S-Expression IR Emission

Homoiconic S-expression IR. The structure mirrors the AST directly; every node is a first-class data value suitable for macro transformation:

    (program
      (patterns)
      (module "neonatal_respirator"
        (signals
          (signal "respirator_enable" input bool)
          (signal "airway_pressure"   input (unsigned 16))
          (signal "clamp_valve"       output bool))
        (guards
          (guard "sustained_pressure_drop"
            (< (signal "airway_pressure") 50) 1000))
        (reflexes
          (reflex "emergency_clamp"
            (on "sustained_pressure_drop")
            (assign "clamp_valve" true)))))

### Trace Summary

Table XXXII: Pipeline trace summary for the neonatal respirator. Each stage produces a well-typed intermediate result; zero errors are emitted across all nine stages.
Stage | Name | Key Output | Errors
--- | --- | --- | ---
1 | Source | 14-line MIRR program | 0
2 | Lexer | Typed tokens with spans | 0
3 | Parser | Typed AST (3 sigs, 1 guard) | 0
4 | Patterns | No-op (no patterns) | 0
5 | Validation | E201–E216 checked | 0
6 | Typecheck | `u16 < int → bool` | 0
7 | Width | 4 nodes, 2 rounds | 0
8 | Temporal | 1 counter (u11), 0 SRs | 0
9 | Emission | SV + R-SPU + S-expr | 0

The key observation is deterministic multi-target emission: the same 14-line MIRR source produces SystemVerilog RTL for synthesis, R-SPU assembly for the Reflexive Processing Unit, and S-expression IR for metaprogramming—all from a single invocation of `run_pipeline`. No stage introduces nondeterminism; given identical source and `PipelineConfig`, the compiler produces bit-identical output across runs. This is a prerequisite for DO-254 certification, where reproducible builds are mandatory.

## 15. Toolchain Integration

The MIRR `toolchain` module provides wrappers for five external EDA tools: Yosys (synthesis), Verilator (lint), SymbiYosys (formal verification), EQY (equivalence checking), and icetime (timing analysis).

### Yosys Synthesis Flow

All 11 synthesizable examples compile through Yosys (v0.63) targeting either a generic gate library or iCE40 FPGAs. The MIRR compiler generates a companion `bind` file that wraps SVA property blocks into a separate verification module, allowing synthesis tools to strip properties before gate-level mapping.

Cell counts range from 15 (shift register guard) to 1,650 (FIR filter). This demonstrates that the compiler produces synthesis-ready SystemVerilog across a range of module complexities.

### FPGA Scaffold Generation

The `--emit fpga-scaffold` flag generates a complete iCE40 HX8K project directory including: top-level wrapper with clock/reset, pin constraint file (`.pcf`), Yosys synthesis script, nextpnr place-and-route script, and a Makefile. This enables one-command synthesis-to-bitstream for prototyping.

### Verilator Lint Integration

The toolchain module provides a Verilator `--lint-only` wrapper for local validation. The wrapper captures lint diagnostics and maps them back to MIRR source locations using the provenance metadata embedded in emitted comments. CI integration is planned.

### LSP Integration

The `lsp` module provides Language Server Protocol support for VS Code. Diagnostics from all 8 error code ranges (E1xx through E8xx) are mapped to LSP severity levels: E1xx/E2xx errors map to `Error`; E5xx width warnings map to `Warning`; E4xx pattern hints map to `Information`.

### Planned Extensions

Future toolchain integration targets:

- SymbiYosys for bounded model checking of SVA properties.
- nextpnr for place-and-route with timing-driven optimization.
- icetime for static timing analysis of critical paths.
- EQY for formal equivalence checking between MIRR revisions.

## 16. Related Work

### Hardware Construction Languages

Chisel [1] and its intermediate representation FIRRTL [4] provide a Scala-embedded hardware construction language with parameterized generators. Chisel’s strength is hardware abstraction via Scala classes and traits; its weakness is the absence of built-in temporal specification or formal verification of compiler passes.

Clash [2] uses Haskell’s type system to describe synchronous hardware, leveraging parametric polymorphism and type-level naturals for compile-time dimension checking. Bluespec [3] employs guarded atomic actions with transactional semantics, providing a scheduling model that is more expressive than MIRR’s guard/reflex model but without explicit temporal cycle-count specifications.

None of these languages provides native temporal guard specifications, LTL property compilation to SVA, or instruction-level emission to a bounded ISA.

### High-Level Synthesis

HLS tools such as Vivado HLS and Catapult compile C/C++ to RTL but rely on timing constraints and scheduling algorithms rather than explicit temporal semantics. MIRR’s temporal guards are a semantic-level construct, not a synthesis-time optimization.

### Temporal Logic in Hardware

Cement2 introduces temporal hardware transactions with latency guards. MIRR’s temporal guard model is simpler: guards specify a condition and a cycle count, compiled to shift registers or counters. This trades expressiveness for deterministic resource usage.

### Width Inference

FIRWINE provides formally verified width inference for FIRRTL with Rocq proofs. MIRR’s width inference implements a comparable SCC-based approach with its own proof development (1,906 lines, 55 theorems). Unlike FIRWINE, MIRR’s width pass is integrated into a full compilation pipeline including temporal compilation and instruction emission.

### Formal Verification of Compilers

CompCert verified a C compiler in Coq. CakeML verified an ML implementation. MIRR’s proofs target a narrower claim—soundness of width inference and R-SPU encoding—but demonstrate that mechanized proofs are tractable for hardware compiler passes.

### Autonomic Computing

The MAPE-K feedback loop [9, 10] is the canonical framework for self-adaptive systems. MIRR’s MAPE-K simulator (10 submodules) applies this framework to hardware monitor observability, providing LTL-based property monitoring with bounded knowledge-base recording. Unlike purely static verification, the simulator exercises the temporal properties under fault injection, closing the loop between design-time specification and runtime adaptation.

### Feature Comparison

Table XXVIII compares MIRR with related systems across seven key capabilities: temporal guards (TG), LTL/SVA properties (LTL), type system (TS), formal proofs (FP), instruction-level backend (ISA), S-expression IR (SE), and MAPE-K simulator (MK). MIRR is, to our knowledge, the only open-source system that combines all seven in a single deterministic pipeline.

Table XXVIII: Feature comparison with related systems.
System | TG | LTL | TS | FP | ISA | SE | MK
--- | --- | --- | --- | --- | --- | --- | ---
Chisel/FIRRTL | — | — | ✓ | — | — | — | —
Clash | — | — | ✓ | — | — | — | —
Bluespec | ∼ | — | ✓ | — | — | — | —
Vivado HLS | — | — | — | — | — | — | —
Cement2 | ✓ | — | — | — | — | — | —
FIRWINE | — | — | — | ✓ | — | — | —
CompCert | — | — | ✓ | ✓ | — | — | —
MIRR | ✓ | ✓ | ✓ | ✓ | ✓ | ✓ | ✓

### Quantitative Comparison

Table XXIX compares measurable evidence across the systems, limited to peer-reviewed publications or public release documentation.

Table XXIX: Quantitative comparison of HDL systems. “—” indicates the metric is not applicable or not reported.
System | Proofs | Tests | ISA | Backends
--- | --- | --- | --- | ---
Chisel/FIRRTL | 0 | — | — | 1
Clash | 0 | — | — | 1
Bluespec | 0 | — | — | 2
Cement2 | 0 | — | — | 1
FIRWINE | 1,200 | — | — | 0
MIRR | 1,906 | 2,601 | 30 | 6

FIRWINE has more proof lines but targets a single compiler pass (width inference) for an existing language. MIRR’s proofs cover two passes (width inference and R-SPU encoding) within a full compilation pipeline that also produces executable instructions. Among HDL compilers that serve as both synthesis tools and verification platforms, MIRR has the highest formal verification coverage per source line.

## 17. Vision and Claims

The original architectural exploration made five design claims. The table below maps each to its implementation status, updated with MEGA-1/2/3 evidence.

Table XXX: Mapping speculative claims to implementation evidence.
Claim | Evidence
--- | ---
Temporal guards | Shift registers (≤16 cycles) and counter-comparators (>16) generated by Stage 8. Adaptive strategy proven by synthesis.
LTL safety in silicon | 4 property forms compiled to SVA. R-SPU emits `ASSERT_ALWAYS/NEVER`. All 11 synthesizable examples synthesize with zero errors.
Formally verified width | 1,906 lines of Rocq proofs. 52 of 55 theorems fully mechanized.
Deterministic ISA | 30-instruction R-SPU ISA v2 with 32-bit encoding, tagged registers, exception handling (MEGA-3), cycle-accurate simulation.
MAPE-K loop | MAPE-K simulator with 10 submodules. Bounded by MAX_TICKS=10,000,000.

### Four Roles of MIRR

MIRR serves four complementary roles in the safety-critical hardware ecosystem:

1. Design language — a domain-specific surface syntax for specifying temporal safety monitors with three constructs (Signal, Guard, Reflex) and LTL properties.
2. Compiler — a 9-stage deterministic pipeline producing 6 output formats, with SCC-based width inference backed by mechanized proofs.
3. Runtime ISA — the R-SPU provides instruction-level execution of compiled monitors with deterministic tick-level semantics, tagged registers, and exception handling.
4. Homoiconic IR — the S-expression representation enables code-as-data transformation, compile-time metaprogramming, and self-hosting validation.

### Extended Type System as a Path to Dependent Types

The MEGA-1 extended type system introduces 8 advanced type features (Section 5). While each feature is currently independent, the long-term vision is convergence toward a dependent type system for hardware:

- Refinement types prove signal bounds statically, replacing runtime range checks.
- Linear types enforce resource discipline (e.g., each emergency stop channel consumed exactly once).
- Type-level naturals enable compile-time dimension checking (e.g., FIR filter tap count matches coefficient array length).
- Session types verify protocol conformance between communicating hardware modules.

### SAT-Based Simplification

A bounded DPLL solver is implemented in `src/sat/` with Tseitin CNF encoding (`MAX_SAT_VARIABLES` = 256, `MAX_SAT_CLAUSES` = 1,024), gated by `PipelineConfig.sat_simplify`. Future work includes extending the solver to full property checking of guard conditions.

### Future Directions

- Fixed-point types: extend the type system with fixed-point arithmetic (`fixed<I,F>`) for DSP pipelines.
- DPR controller: generate dynamic partial reconfiguration controllers targeting Xilinx/Intel FPGAs.
- Multi-core R-SPU: extend the ISA for multi-core configurations with inter-core messaging.
- Certification: pursue DO-254 Level A and IEC 61508 SIL 3 certification for the compiler.

## 18. Conclusion

We presented MIRR, a safety-critical hardware rule language with a Rust compiler (30,719 lines, 101 files, zero `unsafe` blocks) that compiles temporal guards, guarded reflexes, and LTL safety properties through a 9-stage deterministic pipeline into 9 emission backends. All 11 synthesizable examples compile through Yosys with zero errors, and the full pipeline processes a 32-signal module in 378 microseconds.

### Limitations

- Source input bounded to 64 KiB in the browser demo.
- Signed guard lowering is not yet supported.
- The LSP server is not compiled to WebAssembly.
- The R-SPU simulator is available via WASM (simulate_rspu) but provides batch-mode results rather than cycle-stepping.
- 3 of 55 Rocq theorems use Admitted stubs.
- No FPGA bitstream generation in the browser—Yosys synthesis requires the native toolchain.
- Scalability ceiling: largest tested module has 27 signals and 13 guards; industrial systems may require hundreds of monitors.
- Clock domain crossing detection (`temporal/clock_domain.rs`) identifies violations; multi-clock synchronizer generation remains future work.
- Formal semantics remain pen-and-paper; full Rocq mechanization is future work.

### Future Directions

- Fixed-point types (`fixed<I,F>`) for DSP pipelines.
- SAT-based simplification is implemented in `src/sat/` using a bounded DPLL solver with Tseitin CNF encoding, gated by `PipelineConfig.sat_simplify`. Future work: extend to full property checking.
- DPR controller generation for Xilinx/Intel FPGAs.
- Multi-core R-SPU configurations with inter-core messaging.
- DO-254 Level A certification pathway.

## 19. AI Tool Disclosure

In accordance with DAC and IEEE policy on the use of artificial intelligence tools in research, we disclose the following:

### Tools Used

Claude (Anthropic) was used as a coding assistant during the implementation of the MIRR compiler and as an editorial assistant during manuscript preparation.

### Scope of Use

- Code generation: Claude assisted with Rust implementation of compiler passes, test generation, pattern expansion, width inference, type checking, R-SPU backend, S-expression IR, and MAPE-K simulation. All code was reviewed, tested, and validated by the human author.
- Writing assistance: Claude was used for drafting, editing, and formatting portions of this manuscript. All technical claims, experimental design, and intellectual contributions are the sole responsibility of the human author.
- Campaign execution: Claude was used to execute parallel development campaigns (MEGA-1 through MEGA-3) under human supervision, with all changes gated by automated CI (`fmt + clippy + test`).
- Literature search: Claude was used to identify relevant prior work.

### Intellectual Contribution

The MIRR language design, the R-SPU architecture, the compiler pipeline architecture, the decision to use Rocq for formal proofs, and the experimental methodology are original contributions of the human author. The human author takes full responsibility for all content in this paper.

### Verification and Quality Assurance

All AI-generated code was subject to the following verification pipeline before acceptance:

- `cargo fmt --check` — formatting conformance
- `cargo clippy --all-targets -- -D warnings` — zero warnings policy
- `cargo test --all` — full test suite (2,601 tests)
- Manual review of every Rocq proof against the proof assistant (`Qed.` discharge)
- Campaign proposal system with audit, propose, sign/veto, execute, close-out phases

The proposal archive (`proposals/`) contains the full audit trail: 47 proposals, 42 executed, 5 superseded.

AI tools were not listed as co-authors and did not generate the core intellectual contributions of this work.

## 20. Campaign Log

The MIRR compiler evolves through a proposal system: audit, propose, sign/veto, execute, close out. This section records the history of changes to the living document and the compiler. Each entry corresponds to a campaign or documentation update.

Campaign log: full history of MIRR development proposals.
ID | Date | Summary
--- | --- | ---
001 | 2026-03-08 | SEM-001: Assign unique error codes to all semantic diagnostics (E2xx).
002 | 2026-03-08 | TYPE-001: Semantic type checker implementation.
003 | 2026-03-08 | TYPE-002: Signed integer types.
004 | 2026-03-08 | TYPE-003: Signed-aware width inference.
005 | 2026-03-08 | TYPE-004: Linear signal ownership.
006 | 2026-03-08 | ROCQ-001: Width inference proofs in Rocq.
007 | 2026-03-08 | TYPE-005 + RSPU-001: Multi-campaign proposal (extended types + R-SPU backend).
008 | 2026-03-08 | DOC-001: Documentation synchronization campaign.
009 | 2026-03-09 | SITE-001: Documentation & website cleanup campaign.
010 | 2026-03-09 | SITE-002: Website visual identity campaign.
011 | 2026-03-09 | SPAN-001 + LSP-001: Span infrastructure & Language Server Protocol.
012 | 2026-03-09 | ERR-001 + VSCODE-001: Rustc-quality error messages & VS Code extension upgrade.
013 | 2026-03-09 | FPGA-001: Synthesis-ready SystemVerilog emission.
014 | 2026-03-09 | FPGA-002: DSP inference for multiply operations.
015 | 2026-03-09 | ERR-002: Error accumulation — multi-error reporting.
016 | 2026-03-09 | SAFE-001: Restore `#![forbid(unsafe_code)]` defense-in-depth.
017 | 2026-03-09 | DEBT-001: Zero-debt inaugural — eliminate all technical debt.
018 | 2026-03-09 | DEBT-002: Zero-debt sweep — comments, constants, and abstractions.
019 | 2026-03-09 | DOC-001: DAC paper update + documentation refresh.
020 | 2026-03-09 | DOC-002: Documentation cleanup — remove internal/redundant files.
021 | 2026-03-09 | SYNTH-001: End-to-end Yosys synthesis — MIRR source to gate-level netlist.
022 | 2026-03-09 | PAPER-001: Paper accuracy, formal content, and synthesis evaluation.
023 | 2026-03-10 | PHASE7-FOUNDATION: Documentation overhaul, living document, and OSS-CAD-Suite toolchain.
024 | 2026-03-10 | MEGA-0: Pre-MEGA-1 infrastructure cleanup.
025 | 2026-03-10 | FOUNDATION-001 + MEGA-1: Type system infrastructure & advanced type system (refinement, linear, effect, clock domain, phantom, type-level naturals, dependent, session types; E610–E625).
026 | 2026-03-10 | MEGA-2: LISP-CORE — homoiconic kernel & S-expression IR. Bounded eval/apply kernel, hygienic macro expander, reader macros, round-trip converter, `--emit sexpr` backend.
027 | 2026-03-10 | MEGA-1b: Extended type system wiring.
028 | 2026-03-10 | MEGA-3: R-SPU ISA v2 — tagged architecture, binary encoding, and cycle-accurate simulator. 32-bit encoding, tagged-word register file, exception handling (TRAP, TRAP_IF, HALT, MODE_SWITCH), deadline enforcement.
029 | 2026-03-11 | AUDIT-001: Full-project audit — code, docs, and living document. Fixed 4 unbounded recursions, R-SPU ALU encoding bug, 8 error code collisions in E170–E183 range. Removed 5 dead code items.
030 | 2026-03-11 | LRA-001: Living Research Artifact — interactive MIRR paper (622 lines), WASM crate, CI pipeline (wasm-build + pages-deploy), CITATION.cff.
031 | 2026-03-11 | LRA-002: Paper upgrade — all 14 references, 10 data tables, OG meta tags, `<noscript>`, MIRR examples, benchmark demo.
032a | 2026-03-12 | META-001: Production-grade LRA + GitHub template + OSS infrastructure. (Superseded by 032b.)
032b | 2026-03-12 | STD-001: Living Research Artifact Standard — template directory (13 files), spec with Bronze/Silver/Gold compliance tiers, GitHub Pages workflow.
033 | 2026-03-12 | LRA-PHASE1: The Trojan Horse — privacy lockdown (gitignore + pre-push hook), template regex tester demo, Service Worker stubs, protocol meta tags, OG social card images. Phase 1 of 9-phase arc.
034 | 2026-03-12 | LRA-PHASE2: Production hardening.
035 | 2026-03-12 | LRA Phase 3 + Phase 4: CLI tool & protocol layer.
036 | 2026-03-12 | CI-GREEN: Fix CI pipeline failures. (Superseded.)
037 | 2026-03-12 | HARDEN-001: Production hardening. (Superseded.)
038 | 2026-03-12 | PAPER-001: Interactive paper & website cleanup. (Superseded.)
039 | 2026-03-12 | CI-RUST-001: Compiler-grade CI & verification pipeline. (Superseded.)
040 | 2026-03-12 | PAGES-001: Modern GitHub Pages deployment.
041 | 2026-03-12 | ULTRA-FORMAL-001: Verified compiler convergence.
042 | 2026-03-13 | PAPER-001: Living paper genesis.
043 | 2026-03-13 | TITAN-CONVERGENCE: The full stack renaissance — signed types, Rocq proofs, R-SPU ISA extensions.
044 | 2026-03-13 | OUROBOROS-DESIGN: Syntax highlighting, playground redesign & visual identity.
045 | 2026-03-14 | MEGA-CONVERGENCE: SAT solver, DynamicCounter, CDC detection, FPGA/ARM partitioning.
046 | 2026-03-14 | POLISH-AND-SHIP: Theorem cap, playground live, doc sync. (Superseded by 047.)
047 | 2026-03-14 | POLISH-2: Fix all metrics, add 4 missing chapters, wire dead button, add search, fix contradictions, expand stub subsections.

### AUDIT-001 Highlights

- Fixed 4 unbounded recursions (NASA Power-of-10 compliance restored)
- Fixed R-SPU ALU encoding bug (b-register truncation for registers ≥ 64)
- Resolved 8 error code collisions in E170–E183 range
- Removed 5 dead code items (Zero-Debt D3 compliance)
- Merged `rspu-reference.md` into `rspu_isa_spec.md`
- Reconciled stale metrics: test count, TMR signals/reflexes
- Fixed living doc contradictions: formal semantics claim, Layer 5 tags
- Created user-facing docs for S-expr IR, MAPE-K, FPGA targets

Full log: `proposals/` directory (47 files).

## References

1. J. Bachrach et al., “Chisel: Constructing hardware in a Scala embedded language,” in Proc. DAC, 2012.
2. C. Baaij et al., “CλaSH: Structural descriptions of synchronous hardware using Haskell,” in Proc. Euromicro Conf. on Digital System Design, 2010.
3. R. S. Nikhil, “Bluespec System Verilog: Efficient, correct RTL from high-level specifications,” in Proc. MEMOCODE, 2004.
4. A. Izraelevitz et al., “Reusability is FIRRTL ground: Hardware construction languages, compiler frameworks, and transformations,” in Proc. ICCAD, 2017.
5. C. Wolf, “Yosys Open SYnthesis Suite,” 2013. yosyshq.net/yosys
6. G. J. Holzmann, “The Power of 10: Rules for developing safety-critical code,” IEEE Computer, vol. 39, no. 6, pp. 95–97, 2006.
7. RTCA, “DO-254: Design Assurance Guidance for Airborne Electronic Hardware,” 2000.
8. RTCA, “DO-178C: Software Considerations in Airborne Systems and Equipment Certification,” 2011.
9. A. Pnueli, “The temporal logic of programs,” in 18th Annual Symp. on Foundations of Computer Science, IEEE, 1977.
10. R. Tarjan, “Depth-first search and linear graph algorithms,” SIAM J. Computing, vol. 1, no. 2, pp. 146–160, 1972.
11. J. McCarthy, “Recursive functions of symbolic expressions and their computation by machine, Part I,” Commun. ACM, vol. 3, no. 4, pp. 184–195, 1960.
12. J. O. Kephart and D. M. Chess, “The vision of autonomic computing,” IEEE Computer, vol. 36, no. 1, pp. 41–50, 2003.
13. Y. Wang et al., “FIRWINE: Formally verified width inference for FIRRTL,” in Proc. ASPLOS, 2026.
14. H. Nane et al., “A survey and evaluation of FPGA high-level synthesis tools,” IEEE Trans. CAD, vol. 35, no. 10, pp. 1591–1604, 2016.

## How to Cite This Work

    @software{mirr2026,
      title  = {MIRR: A Safety-Critical HDL Compiler},
      author = {Brandon},
      year   = {2026},
      url    = {https://github.com/brandonfromph/mirr-project},
      license = {Apache-2.0}
    }

Or use CITATION.cff for citation managers. Cite by commit hash for exact reproducibility.