L3/09 — The invariant

Background

The simulation cell of 08 is stated "from any state satisfying I" — and that qualifier is not a convenience, it is load-bearing. From a truly arbitrary state the cell is false: a state where the Execute stage's payload says "branch" while its control bits say "store" will step to something no ISA transition explains. Such states can never actually arise — but "can never arise" is a claim about all reachable states, and the reachable set of a machine with thousands of flip-flops is beyond any computation. The escape is one of the oldest ideas in program verification, due in essence to Floyd and Hoare: don't compute the reachable set — describe a superset of it that maintains itself. An inductive invariant is a predicate I such that (a) all initial states satisfy it, and (b) any single step from a state satisfying it lands in a state satisfying it. Induction then gives reachable ⊆ I for free, and the simulation cell only ever needs to be proved from I-states.

The catch — and the reason this chapter is flagged as the irreducible heart of the project — is that I must be invented, and the invention is forced to encode genuine understanding of the design. The property you want is almost never inductive by itself: "the retired state matches the ISA" says nothing about a half-finished shift or a mid-refill cache line, so a step from such a state cannot be shown to preserve it. To close the induction you must strengthen the invariant — add clauses describing every piece of in-flight machinery precisely enough that each clause's preservation follows from the others. Every stage register the generator emitted, every interlock corner, every implicit assumption in the RTL must be named in a clause. That is why proof effort tracks what this book calls invariant entropy — the number of independent design decisions I must describe — rather than gate count or spec size.

Invention is not entirely unaided, though, and calibrating the aid is this chapter's practical plan. Model checkers are tools that try to prove properties of finite-state systems automatically; the classical kind explores states exhaustively (dead on arrival here), but the modern kind — IC3 is the standard algorithm name — works by guessing and repairing invariant clauses: it accumulates small clauses, checks inductiveness with a SAT solver, and refines on failures. On the shallow, structural parts of an invariant (pipeline control sanity, handshake discipline) such engines routinely succeed unaided; on clauses expressing what a stage payload means, they mostly fail — that content is semantic, and no amount of clause search recovers it. The economics are favourable either way, because an inductive invariant is a certificate: whatever untrusted engine produced it, checking it means checking three entailments, each a SAT query with a machine-checkable proof. Let the engines mine the tedium, pay trust only at the checker, and measure where the boundary actually falls — that measurement, not any estimate, determines this layer's true cost.

Statement

Invent I — the irreducible content of the whole project, the one artifact no tool, decision procedure, or amount of compute produces. Everything else in the stack is either mechanical, certified, or measured; this is the part that is thought.

Invariant entropy, the governing quantity

Proof work is proportional to neither spec size nor gate count but to invariant entropy — the number of independent design decisions I must name. The operational test: a decision is free if the proof is generic over it or its consequence is recoverable by running the machine; expensive if I must describe it. Free here: datapath width, adder topology, decoder encoding. Expensive, and present: the pipeline's occupancy discipline, the interlock rule, the flush protocol, the two cache lines. Expensive and absent — forwarding networks, speculative state, miss queues, TLBs (05's table) — is what keeps the total moderate: the machine's entropy concentrates in one in-order pipe with the simplest possible hazard rule.

The clause sketch

What I must actually say, per the anatomy:

  1. Pipeline control sanity: the stage valid/stall/flush arbitration bits are mutually coherent (no stage simultaneously firing and flushed; stalls propagate upstream contiguously).
  2. Per-stage payload coherence: each stage's control bundle equals the decode of the instruction it travels with — the generated decoder's output, replayed. Wide, shallow, per stage.
  3. In-flight semantics, per station: the iterative mul/div unit's accumulator holds the partial result with its counter consistent; a mid-flight memory transaction's address/data registers hold what the retiring instruction requires; an open LR reservation is consistent with the reserving instruction; the fetch front end's pc chain is consistent with the committed pc plus in-flight redirects.
  4. Bypass/interlock correctness: every value routed sideways through the bypass network equals the value its producer will write back; where bypassing cannot serve (load-use, mul/div in flight, CSR effects), no reader advances past the unresolved writer.
  5. Flush correctness: instructions younger than a taken redirect never reach WriteBack; the redirect target is the one the retiring step computed.
  6. I-cache agreement: every valid line equals backing memory at its tag — modulo the fence.i window, whose obligation is exactly that software cannot observe the staleness.
  7. TileLink transaction coherence: channel legality, source-ID bookkeeping, refill-burst accounting on the fetch side (06).
  8. CSR coherence: mstatus.MIE/mie/mip consistent with the spec state; the PMP configuration consistent with the checks the access paths apply (07).
  9. α-well-definedness: at retirement boundaries, the architectural readout is total.

Clauses 1, 4, and 7 are exactly the local control invariants IC3-class engines find unaided; 2 is wide but mechanical; 3, 5, 6 carry the semantic content the human supplies; the glue — that the clauses jointly imply the retirement step matches the ISA — is human work.

The automation calibration

An inductive invariant is a certificate: init ⊆ I, I ∧ T ⊆ I', I ⊆ P — three queries, each LRAT-checkable. So untrusted engines may invent clauses and we pay only for checking. The plan: build the invariant-checking path first, throw IC3 at clauses 1/4/7 phrased as safety properties, and measure the hit rate before hand-authoring anything. Expect the engines to clear the structural majority and die on clauses 3/5/6 — but measure, because the split determines the layer's real cost.

The state space forbids the alternative outright: reachability and model checking over the full machine are dead on arrival; refinement plus induction is the only game (L2/02 said the same from below).

Structure of the work

The pipe seams the authoring naturally: clause families attach to stages and to plugins (05's tour is the index), so the invariant parallelises across stations in a way a monolithic state machine would not. The per-instruction quantification lives in 10; this file owns the machine-wide skeleton those obligations plug into.

Obligations

  1. Phrase the clause sketch as machine-checkable predicates over ⟦RTL⟧'s state.
  2. The IC3 calibration run; record the found/failed split.
  3. The glue lemma: I + retirement transition ⟹ the ISA step (with 08).

Interface (up). This invariant is the S-refine seam (iface_L3, rtlBeh = archBeh): the arrow from RTL to ISA. L3/08's cosim oracle — 1631 instructions matched against spike — is its executed precursor, and the gap between that oracle and the theorem is exactly the invariant α developed here.

Effort

The heart of the layer's estimate — yet the volume is small: the genuinely irreducible content is plausibly a few hundred lines of clauses plus the glue lemma. The years are the surrounding machinery (symbolic simulation, bitvector automation, the stuttering framework), not the thinking.