docs: fix spec self-review issues (cross-refs, example arithmetic)

This commit is contained in:
2026-09-13 14:55:44 -04:00
parent 51355764d1
commit 49b775187d
@@ -33,7 +33,7 @@ The design thesis: because HIR hands VIR a fully annotated "dictionary" of facts
- **Windows / MSVC.** Linux/POSIX-first; gcc and clang only. - **Windows / MSVC.** Linux/POSIX-first; gcc and clang only.
- **LLVM bitcode.** The LLVM backend emits textual `.ll` only; the caller runs `llvm-as`. - **LLVM bitcode.** The LLVM backend emits textual `.ll` only; the caller runs `llvm-as`.
- **LLVM debug metadata.** No `!llvm.dbg` in v1; debug mapping exists on the C path via `#line`. - **LLVM debug metadata.** No `!llvm.dbg` in v1; debug mapping exists on the C path via `#line`.
- **A user-facing VIR.** VIR is internal and intentionally hostile to hand-authoring. - **A hand-authored VIR.** VIR is internal and intentionally hostile to hand-authoring. A textual form exists solely for tools and round-trip tests (§9.8); it is not a supported authoring surface.
- **Consuming LLVM IR or Vox's existing IR.** libVCT owns its IR definition. - **Consuming LLVM IR or Vox's existing IR.** libVCT owns its IR definition.
### 1.3 Glossary ### 1.3 Glossary
@@ -135,7 +135,7 @@ Every attribute carries an `attr_source` bit recording whether it was suggested
| `is_addressed` | Address taken by pointer/reference. | | `is_addressed` | Address taken by pointer/reference. |
| `escapes` | Value escapes its defining scope. | | `escapes` | Value escapes its defining scope. |
| `is_runtime_mutable` | May change at runtime. | | `is_runtime_mutable` | May change at runtime. |
| `may_change_at_runtime` | Alias of intent: value is not frozen. | | `may_change_at_runtime` | The observable value may differ between reads/executions (external state). Distinct from `is_runtime_mutable`, which means the storage is written at runtime. |
| `complex` | Frontend-provided; gates the `NoOptimize` request. | | `complex` | Frontend-provided; gates the `NoOptimize` request. |
### 3.2 Requests ### 3.2 Requests
@@ -312,7 +312,7 @@ HIR carries a real high-level `defer` statement. The optimizer inlines the defer
- **Input:** annotated HIR with **complete, epoch-valid** traits. - **Input:** annotated HIR with **complete, epoch-valid** traits.
- **Output:** VIR — basic blocks, phi-nodes, def-use, SSA. - **Output:** VIR — basic blocks, phi-nodes, def-use, SSA.
- Lowering **validates trait completeness**. A missing or contradictory trait raises an **internal-compiler-error** diagnostic (see §11). - Lowering **validates trait completeness**. A missing or contradictory trait raises an **internal-compiler-error** diagnostic (see §10.5).
- Deterministic; parallelizable per function. - Deterministic; parallelizable per function.
### 5.2 Form ### 5.2 Form
@@ -365,7 +365,7 @@ Well-formed SSA:
- phi arity equals predecessor count, - phi arity equals predecessor count,
- a single def per value. - a single def per value.
Verified in debug builds (§12). Verified in debug builds (§11).
--- ---
@@ -771,8 +771,8 @@ The HIR cascade proceeds as follows:
1. HIR comptime-evaluates `x = 4` → `is_comptime`, `is_constant`, `const_value = 4`. 1. HIR comptime-evaluates `x = 4` → `is_comptime`, `is_constant`, `const_value = 4`.
2. `y = x + 4` unfolds to `y = 8` → `is_comptime`. 2. `y = x + 4` unfolds to `y = 8` → `is_comptime`.
3. `foo(x, y)` is proven small → HIR issues an `Inline` **request**; `z` becomes `8 + ...` constant → comptime. 3. `foo(x, y)` is proven small → HIR issues an `Inline` **request**; after inlining, `z = 4 + 8 = 12` → comptime.
4. `a = sqrt(z)` → `a = sqrt(8)` comptime → `a = 3.4641016151377544`. 4. `a = sqrt(z)` → `a = sqrt(12)` comptime → `a = 3.4641016151377544`.
5. The whole program collapses to `println(3.4641016151377544)`. 5. The whole program collapses to `println(3.4641016151377544)`.
VIR then optimizes the `println` call. The emitted C is effectively a single call with the folded constant. This demonstrates trait propagation HIR → VIR and the request lifecycle (`Inline` accepted). VIR then optimizes the `println` call. The emitted C is effectively a single call with the folded constant. This demonstrates trait propagation HIR → VIR and the request lifecycle (`Inline` accepted).