# 014 — Worked Example

- **Status:** Draft
- **Normative language:** `MUST`, `MUST NOT`, `SHOULD`, `SHOULD NOT`, and `MAY` are to be
  interpreted as described in RFC 2119.

## 1. Purpose

This file walks one small program from the HIR builder through the comptime cascade, trait
derivation, request handling, lowering, VIR optimization, and C emission. It is **normative for
trait and request semantics**: a conforming implementation **MUST** reach the trait states,
request outcomes, and observable result described here. Where a stage file gives the general
rule, this file gives the concrete instance that fixes its meaning.

## 2. Scope

The example covers the HIR optimizer, the trait vocabulary, lowering, the VIR optimizer's
handling of one request, and the C backend. It does not restate the full grammar of HIR or VIR,
and it is not a conformance test by itself. It is the reference walkthrough that other files cite.

## 3. The input program

```
fn foo(x: int, y: int) -> int {
    return x + y;
}

fn main() -> int {
    x = 4;
    y = x + 4;
    z = foo(x, y);
    a = sqrt(z);
    println(a);
}
```

A frontend builds this through the HIR builder. The builder calls are illustrative; their shapes
show how nodes and values enter HIR:

```d
auto m   = ModuleBuilder("foo");
auto fn  = m.function("foo", [intTy, intTy], intTy);
auto body = fn.block();
body.ret(body.add(fn.param(0), fn.param(1)));

auto main_ = m.function("main", [], intTy);
auto b     = main_.block();
auto x = b.local("x", b.literal(4));
auto y = b.local("y", b.add(x, b.literal(4)));
auto z = b.local("z", b.call("foo", x, y));
auto a = b.local("a", b.call("sqrt", z));
b.expr(b.call("println", a));
```

The frontend **MAY** suggest traits while building. HIR validates each suggestion and overwrites a
wrong value with the derived one, promoting the mismatch to an error under `-Werror` (see
[002 — Traits](002-traits.md)).

## 4. Rules exercised

| Rule | Statement | Defined in |
|---|---|---|
| **R1** | When every operand of a pure primitive is `is_comptime`, the evaluator computes `const_value` and sets `is_comptime` and `is_constant`. | [004 — HIR Optimizer](004-hir-optimizer.md) |
| **R2** | Before substituting a constant for a node, HIR **MUST** prove the node is not addressed and not runtime-mutable. | [002 — Traits](002-traits.md), [004 — HIR Optimizer](004-hir-optimizer.md) |
| **R3** | A `is_comptime` node with `const_value = v` has every use replaced by the literal `v`. | [004 — HIR Optimizer](004-hir-optimizer.md) |
| **R4** | A node with no remaining uses and no side effects **MUST** be deleted. | [004 — HIR Optimizer](004-hir-optimizer.md) |
| **R5** | Every node whose operands became constant **MUST** be re-enqueued on the worklist. | [004 — HIR Optimizer](004-hir-optimizer.md) |
| **R6** | HIR **MUST NOT** inline. It proves smallness and issues an `Inline` request to VIR. | [004 — HIR Optimizer](004-hir-optimizer.md), [007 — VIR Optimizer](007-vir-optimizer.md) |
| **R7** | Every request **MUST** yield a `RequestResult`; an accepted request needs no reason, and a denial **MUST** carry a `DenyReason` and a one-line note. | [002 — Traits](002-traits.md) |
| **R8** | Each VIR entity **MUST** carry the `Trait` of its source HIR node; relationship endpoints are rewritten through the `LoweringMap`. | [005 — Lowering](005-lowering.md) |
| **R9** | A scalar that is not addressed, not escaping, and not runtime-mutable **MUST** lower to a pure SSA value. | [005 — Lowering](005-lowering.md) |
| **R10** | A comptime value **MUST** be emitted as a literal, not recomputed. | [008 — C Backend](008-c-backend.md) |

## 5. The canonical cascade shape

The cascade is the chain of rewrites triggered by one fold. Its canonical textbook shape uses
`4 * 16`:

```
n = 4 * 16
  -> const 64                          (R1; trigger ConstantUnfolded)
  -> mark is_comptime / is_constant / const_value = 64
  -> prove not addressed / not runtime-mutable   (R2)
  -> replace all uses with literal 64  (R3; trigger UsesReplaced)
  -> node dead -> delete               (R4; trigger NodeDeleted)
  -> downstream nodes now constant -> enqueue   (R5; trigger TraitChanged)
```

Each hop emits a trigger. The worklist scheduler dedupes `(pass, node)` pairs and runs to a
fixpoint, bounded by the per-function and per-module rewrite budgets (see
[004 — HIR Optimizer](004-hir-optimizer.md)). Step 6 of the walkthrough below is exactly this
shape applied to `y = x + 4`, and the same shape recurs for `z`, `a`, and the argument of
`println`.

## 6. Worked cascade for `foo` / `main`

The steps below run per function, in deterministic order. Each step names the rule it exercises.

1. **Build.** `main` binds `x` to the literal `4`. The literal already carries
   `const_value = 4`; HIR sets `is_comptime = true` and `is_constant = true` (R1).
2. **Prove `x`.** HIR proves `x` is not addressed and not runtime-mutable: `is_addressed = false`,
   `is_runtime_mutable = false`, `escapes = false`, `is_mutably_used = false` (R2).
3. **Replace uses of `x`.** Every use of `x` becomes the literal `4`. Trigger `UsesReplaced`
   (R3).
4. **Delete `x`.** `x` has no uses and no side effects; it is deleted. Trigger `NodeDeleted`
   (R4).
5. **Re-enqueue.** `y = x + 4` is now `y = 4 + 4`, so `y` is enqueued. Trigger `TraitChanged`
   (R5).
6. **Fold `y`.** The evaluator computes `4 + 4 = 8`, and sets `y.const_value = 8`,
   `y.is_comptime = true`, `y.is_constant = true`. Trigger `ConstantUnfolded` (R1).
7. **Prove and replace `y`.** R2 holds for `y`; R3 rewrites its uses to `8`; R4 deletes `y`.
8. **Re-enqueue `z`.** `z = foo(x, y)` is now `z = foo(4, 8)`; `z` is enqueued (R5).
9. **Fold `z`.** `foo` is pure, non-recursive, and its body evaluates with primitives only, so
   the evaluator interprets the call with arguments `4` and `8` and computes `12`. `z` becomes
   `is_comptime = true`, `is_constant = true`, `const_value = 12` (R1). This is constant
   evaluation, not inlining: HIR computes a value and does not rewrite `foo` into `main`
   (R6).
10. **Request inlining.** Separately, HIR proves `foo` is small and issues an `Inline` request on
    the call edge. HIR does not perform the inlining (R6).
11. **Prove, replace, delete `z`.** R2 holds; R3 rewrites the use in `a = sqrt(z)` to
    `a = sqrt(12)`; R4 deletes `z`.
12. **Fold `a`.** `sqrt` is a primitive and its argument is `is_comptime`, so the evaluator
    computes a `double` result: `a.const_value = 3.4641016151377544`, `a.is_comptime = true`,
    `a.is_constant = true` (R1). The other float arithmetic in this example is exact; the square
    root is not, and the field holds the IEEE 754 binary64 value of `sqrt(12)`, printed with the
    shortest decimal string that round-trips.
13. **Replace and delete `a`.** R3 rewrites the argument of `println` to
    `3.4641016151377544`; R4 deletes `a`.
14. **Collapse.** What remains of `main` is `println(3.4641016151377544)`. The `foo` function now
    has no call site. HIR does not delete functions; that is a VIR/IPA concern.

The worklist drains when no node changes, which here is after step 14.

## 7. Traits at completion

The derived traits that survive the cascade are:

| Node | `ty` | `const_value` | `is_comptime` | `is_constant` | `is_addressed` | `is_runtime_mutable` | `escapes` |
|---|---|---|---|---|---|---|---|
| `x` (deleted) | `int` | `4` | true | true | false | false | false |
| `y` (deleted) | `int` | `8` | true | true | false | false | false |
| `z` (deleted) | `int` | `12` | true | true | false | false | false |
| `a` (deleted) | `double` | `3.4641016151377544` | true | true | false | false | false |
| `println` arg | `double` | `3.4641016151377544` | true | true | false | false | false |
| `foo` | function | absent | false | false | false | false | false |

`foo.is_used` falls to `false` once its only call is folded. `is_constant` without `is_comptime`
is possible in general; every value in this example is comptime.

## 8. Requests and their results

| Request | Target | Strength | Requested because | Result |
|---|---|---|---|---|
| `Inline` | call edge of `foo` in `main` | Soft | `foo` proven small (R6) | denied: `AlreadyDone` (call folded in HIR; no live call remains) (R7) |

The `Inline` request is soft, so VIR **MAY** decline it; here it declines with `AlreadyDone`
because HIR already folded the only call site, so no live call remains to inline. A denial
**MUST** carry a `DenyReason` and a one-line note, for example
`denied Inline on @foo, reason CostModel, note "callee exceeds size budget"`. No conflicting
`Strong` request is issued in this example, and `NoInline` **MUST NOT** be requested for `foo`.
Recording the request as accepted would violate O-28 of
[007 — VIR Optimizer](007-vir-optimizer.md), which forbids marking a request accepted when no
transform was performed. VIR removes the now-unused `foo` through global dead-code elimination.

## 9. Lowering to VIR

Lowering is a pure translation. It builds a `LoweringMap` from HIR nodes to VIR entities and
copies each node's `Trait` onto its VIR entity (R8). Each local here satisfies R9, so it lowers
to a pure SSA value rather than an `alloca`. An illustrative VIR listing for the optimized
`main`, plus the still-present `foo`, is:

```
define i32 @foo(i32 %x, i32 %y) {
entry:
  %s = add i32 %x, %y
  ret i32 %s
}

define i32 @main() {
entry:
  %r = call i32 @println(double 3.4641016151377544)
  ret i32 %r
}
```

The textual form is shown for clarity only. It is not an authoring surface (see
[000 — Overview](000-overview.md)); the same module can be expressed with the builder or as
opaque binary structures.

VIR optimization resolves the `Inline` request (denied `AlreadyDone`), runs global DCE, and
leaves the call to `println`. It does not re-derive traits; every fact it uses came from HIR (see
[007 — VIR Optimizer](007-vir-optimizer.md)).

## 10. Emitted C

The C backend emits C17. Because the argument is comptime, it is emitted as a literal (R10), and
the irreducible shape collapses to a single call:

```c
extern int println(double);

int main(void) {
    return println(3.4641016151377544);
}
```

The exact spelling of the float literal is implementation-defined as long as it round-trips to
the same binary64 value; the value `3.4641016151377544` is normative.

## 11. Invariants

- A conforming implementation **MUST** derive the trait values in section 7 from the section 3
  input.
- A conforming implementation **MUST** issue an `Inline` request for `foo` and **MUST NOT**
  inline it in HIR.
- A conforming implementation **MUST** reach the observable behavior of `println` called once
  with the binary64 value of `sqrt(12)`, whatever its internal pipeline order.
- Running the example twice with the same `Config` **MUST** produce byte-identical output (see
  [000 — Overview](000-overview.md)).

## 12. Cross-references

- [000 — Overview](000-overview.md) for the two-stage thesis and the determinism guarantee.
- [002 — Traits](002-traits.md) for attributes, requests, `RequestResult`, and `DenyReason`.
- [004 — HIR Optimizer](004-hir-optimizer.md) for the cascade, triggers, and budgets.
- [005 — Lowering](005-lowering.md) for the `LoweringMap`, SSA construction, and the memory
  model behind R9.
- [006 — VIR](006-vir.md) for the SSA and CFG shapes used in section 9.
- [007 — VIR Optimizer](007-vir-optimizer.md) for request handling and global DCE.
- [008 — C Backend](008-c-backend.md) for emission and literal formatting.