Store ordinary task returns in HIR

freak-conformance-audit.md

@@ -96,14 +96,14 @@ Verdict legend: 🛠 code fix, 📖 amend bible, ✅ already aligned.
 |---|---|---|---|
 | `pilot x = value` declares variable, mutable by default | ✅ | ✅ | [freakc/parser.py:900-950](freakc/parser.py); confirmed by `tests/suite/test_variables.fk` |
 | `fixed pilot x = value` immutable | ✅ | ✅ | parsed and enforced |
-| Type annotation optional / inferred | ✅ | ✅ | The shipping checker infers unannotated literals. In V4, task-local `pilot` and `fixed pilot` annotations—including tuple and fixed-array annotations used by tuple/list destructuring—are normalized with exact spans into HIR snapshot v4 facts, exposed/canonicalized by TY, and consumed by MIR build without re-reading their type tokens. MIR build still uses body tokens for patterns, initializer boundaries, places, and CFG; six unrelated type-text callers remain guarded, backend representation is unchanged, and symbol-valued annotated locals retain the existing phantom-local-IR limitation. |
+| Type annotation optional / inferred | ✅ | ✅ | The shipping checker infers unannotated literals. In V4, task-local `pilot` and `fixed pilot` annotations—including tuple and fixed-array annotations used by tuple/list destructuring—are normalized with exact spans into HIR snapshot v5 facts, exposed/canonicalized by TY, and consumed by MIR build without re-reading their type tokens. MIR build still uses body tokens for patterns, initializer boundaries, places, and CFG; six unrelated type-text callers remain guarded, backend representation is unchanged, and symbol-valued annotated locals retain the existing phantom-local-IR limitation. |
 | `pilot mut x = ...` (Phase-1 BC) for explicit mutability under `--strict-borrow` | ✅ | 📖 | [src/compiler/v3/checker.fk](src/compiler/v3/checker.fk) — bible should mention this dual mode (default leak-everything vs `--strict-borrow`) |
 
 #### §1.2 Functions ([freak-full-bible.md:42-71](freak-full-bible.md))
 
 | Contract | Status | Verdict | Notes |
 |---|---|---|---|
-| `task name(...) -> type { ... }` | ✅ | ✅ | core feature |
+| `task name(...) -> type { ... }` | ✅ | ✅ | Core feature. V4 stores ordinary top-level tasks as closed `explicit` / `implicit-block` / `arrow` HIR return-form facts; an explicit `-> T` carries normalized surface text and its exact span through HIR snapshot v5, and TY consumes that declared type/span without token reconstruction. Arrow inference, implicit block returns, impl/doctrine/extern signatures, MIR body lowering, and backend behavior retain their existing semantics and remain separately bounded. |
 | `give back` return keyword | ✅ | ✅ | |
 | `say` print keyword always available | ✅ | ✅ | |
 | String path interpolation `"{path}"` | ✅ | ✅ | Self-hosted V3 lowers resolved `IDENT(.IDENT)*` paths in every word-expression context on C and LLVM; non-path brace bodies remain literal. Executable evidence: [tests/v3_interpolation.py](tests/v3_interpolation.py) and [tests/v3_legacy_golden.py](tests/v3_legacy_golden.py). |

freakc/auditor.py

@@ -2867,6 +2867,103 @@ def add(label: str, ok: bool, detail: str = "") -> None:
     if unw_missing:
         failures.append("V4 unwinder-import diagnostic regressed: " + "; ".join(unw_missing))
 
+    # Check 9b: V4 ordinary-task return facts belong to HIR. This is an
+    # ownership boundary, not a new return semantic.
+    v4_hir_task_return = repo / "src" / "compiler" / "v4" / "crates" / "freak_hir" / "src" / "lib.fk"
+    v4_ty_task_return = repo / "src" / "compiler" / "v4" / "crates" / "freak_ty" / "src" / "lib.fk"
+    v4_task_return_smoke = repo / "src" / "compiler" / "v4" / "tests" / "task_return_semantic_boundary_smoke.fk"
+    v4_task_return_harness = repo / "src" / "compiler" / "v4" / "check_v4.py"
+    v4_task_return_readme = repo / "src" / "compiler" / "v4" / "README.md"
+    task_return_boundary_missing: List[str] = []
+    if v4_hir_task_return.exists():
+        hir_src = v4_hir_task_return.read_text(encoding="utf-8")
+        for needle in (
+            'pilot v4_hir_snapshot_format = "freak-hir-snapshot-v5"',
+            'pilot v4_hir_task_return_explicit = "explicit"',
+            'pilot v4_hir_task_return_implicit_block = "implicit-block"',
+            'pilot v4_hir_task_return_arrow = "arrow"',
+            "pilot v4_hir_task_return_items = 0",
+            "pilot v4_hir_task_return_forms = 0",
+            "pilot v4_hir_task_return_types = 0",
+            "pilot v4_hir_task_return_spans = 0",
+            "task v4_hir_task_return_form(",
+            "task v4_hir_task_return_type(",
+            "task v4_hir_task_return_span(",
+            'pilot out = "hir-task-return"',
+            '"task-returns"',
+            "task v4_hir_snapshot_task_return_is_valid(",
+            "task v4_hir_snapshot_task_return_owner_is_valid(",
+            "task v4_hir_snapshot_task_return_slots_are_valid(",
+        ):
+            if needle not in hir_src:
+                task_return_boundary_missing.append(f"freak_hir: {needle}")
+    else:
+        task_return_boundary_missing.append("freak_hir/src/lib.fk missing")
+    if v4_ty_task_return.exists():
+        ty_src = v4_ty_task_return.read_text(encoding="utf-8")
+        for needle in (
+            "task v4_ty_signature_is_ordinary_hir_task(",
+            "task v4_ty_ordinary_task_explicit_return_from_hir(",
+            "task v4_ty_ordinary_task_explicit_return_span_from_hir(",
+            "task v4_ty_ordinary_task_arrow_return_fallback(",
+            "task v4_ty_nonordinary_signature_return_fallback(",
+            "task v4_ty_nonordinary_signature_return_span_fallback(",
+            "task v4_ty_nonordinary_hir_item_return_fallback(",
+        ):
+            if needle not in ty_src:
+                task_return_boundary_missing.append(f"freak_ty: {needle}")
+    else:
+        task_return_boundary_missing.append("freak_ty/src/lib.fk missing")
+    if not v4_task_return_smoke.exists():
+        task_return_boundary_missing.append("smoke fixture: task_return_semantic_boundary_smoke.fk")
+    if v4_task_return_harness.exists():
+        harness_src = v4_task_return_harness.read_text(encoding="utf-8")
+        for needle in (
+            '"name": "task return semantic boundary"',
+            '"fixture": "task_return_semantic_boundary_smoke.fk"',
+            "def check_task_return_hir_boundary() -> None:",
+            "def task_return_explicit_call_closure_violations(ty_source: str) -> list[str]:",
+            "task return boundary guard self-test: helper-indirected fallback rejected",
+            "check_task_return_hir_boundary()",
+        ):
+            if needle not in harness_src:
+                task_return_boundary_missing.append(f"check_v4.py: {needle}")
+    else:
+        task_return_boundary_missing.append("check_v4.py harness missing")
+    for doc_path, needles in (
+        (
+            v4_task_return_readme,
+            (
+                "The third bounded boundary covers declared returns on ordinary top-level tasks.",
+                "HIR snapshot v5 validates that vocabulary",
+            ),
+        ),
+        (
+            audit_doc,
+            (
+                "V4 stores ordinary top-level tasks as closed",
+                "TY consumes that declared type/span without token reconstruction",
+            ),
+        ),
+    ):
+        if not doc_path.exists():
+            task_return_boundary_missing.append(f"documentation missing: {doc_path.name}")
+            continue
+        doc_src = doc_path.read_text(encoding="utf-8")
+        for needle in needles:
+            if needle not in doc_src:
+                task_return_boundary_missing.append(f"{doc_path.name}: {needle}")
+    add(
+        "V4 task return HIR boundary",
+        not task_return_boundary_missing,
+        "HIR v5 + TY adapters + smoke + docs wired" if not task_return_boundary_missing else f"{len(task_return_boundary_missing)} gap(s)",
+    )
+    if task_return_boundary_missing:
+        failures.append(
+            "V4 ordinary-task return HIR boundary regressed: "
+            + "; ".join(task_return_boundary_missing)
+        )
+
     # ── Check 10: V4 contract-region source sets ──
     # Borrowed return signatures may select every parameter whose lifetime
     # outlives the return region. Require the set-valued TY/MIR/Meiya contract,

src/compiler/v4/README.md

@@ -79,12 +79,20 @@ construction. Six unrelated `v4_ty_type_text` consumers remain allowlisted for
 method type arguments, raw-pointer instance methods, associated methods,
 shape/route constructor heads, and route-case expressions; the harness requires
 that exact set and prevents local declaration lowering from returning to it.
-Task parameter and return types, shape/route fields, const annotations,
-doctrine/extern types, the remaining MIR body families, and all other type
-families remain explicit follow-up slices. These boundaries change fact
-ownership, not language semantics or backend representation. Symbol-valued
-annotated locals still retain the pre-existing phantom-local-IR limitation
-described in the FFI section below.
+The third bounded boundary covers declared returns on ordinary top-level tasks.
+`freak_hir` stores one closed `explicit` / `implicit-block` / `arrow` record per
+task, including normalized surface type and exact contained span only for an
+explicit `-> T`; HIR snapshot v5 validates that vocabulary, task-only ownership,
+canonical spans, contiguous slots, and declared counts before restore. TY reads
+explicit return types and spans only through those HIR facts. Arrow inference,
+implicit block returns, and non-ordinary impl/doctrine/extern signatures remain
+separately named fallbacks and keep their existing semantics. Task parameter
+types, shape/route fields, const annotations, non-ordinary signatures, the
+remaining MIR body families, and all other type families remain explicit
+follow-up slices. These boundaries change fact ownership, not language
+semantics or backend representation. Symbol-valued annotated locals still
+retain the pre-existing phantom-local-IR limitation described in the FFI
+section below.
 Closures now form a complete first-pass frontend/query slice. The resilient
 parser records arrow and block forms as `ClosureExpr` trees and leaves
 `IncompleteNode` recovery facts for missing pipes, body markers, expressions,
@@ -510,7 +518,7 @@ unit-section|<section-name>|<escaped-checkpoint-identity>|<escaped-section-paylo
 end|freak-00-unit-snapshot-v3
 ```
 
-The source records describe the current `freak_session` source database. The checkpoint identity folds the source identity and content digests for all 15 sections in canonical order, including identity expansion between parse and HIR, so a section cannot be transplanted from a different checkpoint even when source text is unchanged. This is an integrity checksum, not an authentication primitive. Section records are owned by `freak_snapshot`; each section is allowed to change internally only when its format helper and validator change together. Standalone expansion- and HIR-component restore dirty their cached query families and transitive dependents before arena-slot reuse; full prevalidated 00-Unit restore instead keeps both component restores raw before installing the checkpoint's saved query section. HIR v4 validation requires canonical alias-target and local-annotation spans, exact child ownership/slot identity, and exact declared counts. Adding the expansion section changes the complete checkpoint format from v2 to v3; v2 payloads are rejected rather than reinterpreted.
+The source records describe the current `freak_session` source database. The checkpoint identity folds the source identity and content digests for all 15 sections in canonical order, including identity expansion between parse and HIR, so a section cannot be transplanted from a different checkpoint even when source text is unchanged. This is an integrity checksum, not an authentication primitive. Section records are owned by `freak_snapshot`; each section is allowed to change internally only when its format helper and validator change together. Standalone expansion- and HIR-component restore dirty their cached query families and transitive dependents before arena-slot reuse; full prevalidated 00-Unit restore instead keeps both component restores raw before installing the checkpoint's saved query section. HIR v5 validation requires canonical alias-target, local-annotation, and ordinary-task declared-return spans, exact child ownership/slot identity, a closed return-form vocabulary, and exact declared counts. Adding the expansion section changes the complete checkpoint format from v2 to v3; v2 payloads are rejected rather than reinterpreted.
 
 ### `workspace/unitSnapshotManifest`