libvct-spec/spec/014-worked-example.md

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:

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).

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
R2	Before substituting a constant for a node, HIR MUST prove the node is not addressed and not runtime-mutable.	002 — Traits, 004 — HIR Optimizer
R3	A is_comptime node with const_value = v has every use replaced by the literal v.	004 — HIR Optimizer
R4	A node with no remaining uses and no side effects MUST be deleted.	004 — HIR Optimizer
R5	Every node whose operands became constant MUST be re-enqueued on the worklist.	004 — HIR Optimizer
R6	HIR MUST NOT inline. It proves smallness and issues an Inline request to VIR.	004 — HIR Optimizer, 007 — VIR Optimizer
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
R8	Each VIR entity MUST carry the Trait of its source HIR node; relationship endpoints are rewritten through the LoweringMap.	005 — Lowering
R9	A scalar that is not addressed, not escaping, and not runtime-mutable MUST lower to a pure SSA value.	005 — Lowering
R10	A comptime value MUST be emitted as a literal, not recomputed.	008 — C Backend

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). 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, 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); 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).

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:

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).

12. Cross-references

• 000 — Overview for the two-stage thesis and the determinism guarantee.
• 002 — Traits for attributes, requests, RequestResult, and DenyReason.
• 004 — HIR Optimizer for the cascade, triggers, and budgets.
• 005 — Lowering for the LoweringMap, SSA construction, and the memory model behind R9.
• 006 — VIR for the SSA and CFG shapes used in section 9.
• 007 — VIR Optimizer for request handling and global DCE.
• 008 — C Backend for emission and literal formatting.