Update spec workflow instructions

Author: Spenquatch

CHANGELOG.md

@@ -4,7 +4,7 @@
 
 ### Changed
 
-- **The bounded TypeScript lane now proves the same-tree chain3 family in M54** — eligible `kind:function` roots may still use the helper-aware monotone-up lane from M46 and the same-tree wrapper lane from M52, and may now also classify to `function.wrapper.pipeline.chain3.v1` when they declare the exact same-tree local dep tuple `function.wrapper.pipeline.v1` then `function.arithmetic_leaf.monotone_up.v1` then `function.arithmetic_leaf.monotone_down_nonnegative.v1`. The lane remains Bun-only, atom-only, and additive to Rust proof; it still does not widen to molecule execution, generic multi-dep execution, seam kinds, nested chain3 closure members, cross-library TypeScript resolution, `spec validate --target-language`, or `spec export --target-language`.
+- **The bounded TypeScript lane now admits cross-library helper imports in M55** — eligible `kind:function` roots may still use the helper-aware monotone-up lane from M46, the same-tree wrapper lane from M52, and the same-tree chain3 lane from M54. In M55, the one legal helper slot under the monotone-up lane may now resolve a sibling-library helper like `shared::money/round`, and bounded wrapper/chain3 closures may reuse that shared helper transitively once it is in the loaded tree. The lane remains Bun-only, atom-only, and additive to Rust proof; it still does not widen to molecule execution, generic multi-dep execution, seam kinds, direct cross-library wrapper roots, direct cross-library chain3 roots, nested chain3 closure members, `spec validate --target-language`, or `spec export --target-language`.
 
 ## 0.14.0 - 2026-05-07
 

ORCH_PLAN.md

@@ -47,13 +47,13 @@ spec validate examples/ecommerce/units
 spec generate examples/ecommerce/units
 ```
 
-## Bounded TypeScript lane (M54)
+## Bounded TypeScript lane (M55)
 
 `spec` now exposes one bounded TypeScript execution lane. It is intentionally narrow:
 
 - Bun is the only TypeScript prerequisite. The lane shells out to `bun`; no alternate Node, npm, or tsx contract is supported.
 - Eligible roots are exactly `kind: function` specs that classify to `function.arithmetic_leaf.monotone_up.v1`, `function.wrapper.pipeline.v1`, or the bounded same-tree `function.wrapper.pipeline.chain3.v1`.
-- Monotone-up roots may declare `deps: []` or exactly one direct local helper dep. That helper must classify to `function.helper.identity_passthrough.v1`, exist in the same loaded unit set and generated tree, and be the only direct dep of the current unit.
+- Monotone-up roots may declare `deps: []` or exactly one direct helper dep. That helper must classify to `function.helper.identity_passthrough.v1`, author non-empty `body.typescript`, and exist in the loaded unit set and generated tree. In M55, that one helper dep may now be cross-library when it is referenced through `[libraries]` as a sibling import like `shared::money/round`.
 - Wrapper roots must declare exactly two direct local deps in the same loaded unit set and generated tree. The ordered dep tuple is frozen to `function.arithmetic_leaf.monotone_down_nonnegative.v1` then `function.arithmetic_leaf.monotone_up.v1`, and both deps must author non-empty `body.typescript`.
 - Chain3 roots must declare exactly three direct local deps in the same loaded unit set and generated tree. The ordered dep tuple is frozen to `function.wrapper.pipeline.v1` then `function.arithmetic_leaf.monotone_up.v1` then `function.arithmetic_leaf.monotone_down_nonnegative.v1`, and every direct dep must author non-empty `body.typescript`.
 - Chain3 closure collection stays bounded. A same-tree wrapper may appear as a closure member under a chain3 root, but nested `function.wrapper.pipeline.chain3.v1` closure members remain unsupported.
@@ -70,19 +70,19 @@ spec test <path> --target-language typescript
 spec status <unit-or-root> --target-language typescript
 ```
 
-`spec status <unit-or-root> --target-language typescript` reports target-specific proof only. In M54, a root-level status over a mixed example like `examples/ecommerce` may stay non-green unless every unit in scope is either freshly proven in the bounded monotone-up, wrapper, or same-tree chain3 lane, or truthfully remains outside that lane.
+`spec status <unit-or-root> --target-language typescript` reports target-specific proof only. In M55, a root-level status over a mixed example like `examples/ecommerce` or `examples/crosslib-app` may stay non-green unless every unit in scope is either freshly proven in the bounded monotone-up, wrapper, or same-tree chain3 lane, or truthfully remains outside that lane.
 
-The generated helper filenames remain frozen in M54:
+The generated helper filenames remain frozen in M55:
 
 - `__spec_ts/runtime.ts`
 - `__spec_ts/build_entry.ts`
 - `__spec_ts/local_tests.ts`
 
-Commands and surfaces that do not widen for M54:
+Commands and surfaces that do not widen for M55:
 
 - `spec validate` does not accept `--target-language`
 - `spec export` does not accept `--target-language`
-- This lane does not widen to molecule execution, generic multi-dep execution, seam kinds, cross-library TypeScript resolution, nested chain3 closure members, `spec validate --target-language`, or `spec export --target-language`.
+- This lane does not widen to molecule execution, generic multi-dep execution, seam kinds, direct cross-library wrapper roots, direct cross-library chain3 roots, nested chain3 closure members, `spec validate --target-language`, or `spec export --target-language`.
 
 ## Spec format
 

PLAN.md

@@ -192,6 +192,8 @@
 
 - [x] **Bounded same-tree chain3 TypeScript execution in `spec`** — Completed by M54 (2026-05-13). The bounded Bun-backed TypeScript lane now admits the same-tree `function.wrapper.pipeline.chain3.v1` family with the frozen direct local dep tuple `wrapper.pipeline -> monotone_up -> monotone_down_nonnegative`, while keeping proof additive, atom-only, and target-specific.
 
-- [ ] **Cross-library TypeScript helper imports** — Deferred by the M46 review. Same-tree helper execution is enough to close the current product-family mismatch; cross-library target resolution is a different portability problem.
+- [x] **Cross-library TypeScript helper imports** — Completed by M55 (2026-05-13). The bounded Bun-backed TypeScript lane now admits cross-library helper imports in the one legal helper slot for `function.arithmetic_leaf.monotone_up.v1`, and bounded wrapper/chain3 closures may reuse that shared helper transitively once it is in the loaded tree.
 
-- [ ] **Generic multi-dependency TypeScript execution** — Deferred again after M54. The current lane is intentionally family-shaped: helper-aware monotone-up roots plus same-tree wrapper roots and same-tree chain3 roots only, not arbitrary dependency topologies.
+- [ ] **Direct cross-library wrapper and chain3 TypeScript roots** — Deferred after M55. Cross-library helper imports are now allowed only in legal helper slots; direct wrapper root deps and direct chain3 root deps remain local-only.
+
+- [ ] **Generic multi-dependency TypeScript execution** — Deferred again after M55. The current lane is intentionally family-shaped: helper-aware monotone-up roots, cross-library helper imports only in that legal helper slot, plus same-tree wrapper roots and same-tree chain3 roots only, not arbitrary dependency topologies.

README.md

@@ -1,6 +1,6 @@
 # crosslib app example
 
-This example demonstrates M9 direct sibling-library reuse.
+This example demonstrates M9 direct sibling-library reuse plus M55 cross-library helper imports in the bounded TypeScript lane.
 
 From the repo root:
 
@@ -9,4 +9,5 @@ cargo run -p spec-cli -- generate examples/shared-spec/units --output examples/s
 cargo run -p spec-cli -- generate examples/crosslib-app/units --output examples/crosslib-app/src/generated
 cargo check --manifest-path examples/crosslib-app/Cargo.toml
 cargo test --manifest-path examples/crosslib-app/Cargo.toml
+cargo run -p spec-cli -- test examples/crosslib-app/units/pricing/apply_tax.unit.spec --target-language typescript
 ```

TODOS.md

@@ -24,7 +24,7 @@
       "expect": "apply_tax(Decimal::new(10000, 2), Decimal::new(725, 4)) == Decimal::new(10725, 2)"
     }
   ],
-  "generated_at": "2026-05-02T15:59:38Z",
+  "generated_at": "2026-05-13T16:26:14Z",
   "source_file": "examples/crosslib-app/units/pricing/apply_tax.unit.spec",
   "evidence": {
     "build_status": "pass",
@@ -47,6 +47,54 @@
     "authored_truth_status": "fresh",
     "backend_execution_status": "unknown"
   },
+  "target_proofs": {
+    "rust": {
+      "evidence": {
+        "build_status": "pass",
+        "test_results": [
+          {
+            "id": "happy_path",
+            "status": "pass"
+          }
+        ],
+        "observed_at": "2026-05-02T15:59:40Z",
+        "provenance": {
+          "git_commit_sha": "8577dfb5a64daaa02be54501f97131fb25459f72"
+        }
+      },
+      "freshness_anchor": {
+        "authored_truth_digest": "sha256:695b199a2fc2a1073658d52bd80efe5658e4cc55debaf5de2d029cdfe8197617"
+      },
+      "freshness": {
+        "authored_truth_digest": "sha256:695b199a2fc2a1073658d52bd80efe5658e4cc55debaf5de2d029cdfe8197617",
+        "authored_truth_status": "fresh",
+        "backend_execution_status": "unknown"
+      }
+    },
+    "typescript": {
+      "evidence": {
+        "build_status": "pass",
+        "test_results": [
+          {
+            "id": "happy_path",
+            "status": "pass"
+          }
+        ],
+        "observed_at": "2026-05-13T16:26:14Z",
+        "provenance": {
+          "git_commit_sha": "b0b88a9ad26f8e9d986aa0354dcf27b22d43a8d2"
+        }
+      },
+      "freshness_anchor": {
+        "authored_truth_digest": "sha256:dc857f9ce5e43cdcd14c4f9ca879fe1fd8a8bc2b59b81f103c04cfb9faaa6e31"
+      },
+      "freshness": {
+        "authored_truth_digest": "sha256:dc857f9ce5e43cdcd14c4f9ca879fe1fd8a8bc2b59b81f103c04cfb9faaa6e31",
+        "authored_truth_status": "fresh",
+        "backend_execution_status": "unknown"
+      }
+    }
+  },
   "semantic_review": {
     "verdict": "aligned",
     "compatibility_key": "function.arithmetic_leaf.monotone_up.v1",
@@ -68,6 +116,10 @@
       {
         "path": "deps",
         "summary": "1 declared dep(s)"
+      },
+      {
+        "path": "body.typescript",
+        "summary": "authored TypeScript body present"
       }
     ],
     "executable_surfaces": [

examples/crosslib-app/README.md

@@ -18,6 +18,11 @@ body:
         let taxed = subtotal + subtotal * rate;
         round(taxed).max(Decimal::ZERO)
     }
+  typescript: |
+    {
+        const taxed = subtotal.add(subtotal.mul(rate));
+        return round(taxed);
+    }
 local_tests:
   - id: happy_path
     expect: apply_tax(Decimal::new(10000, 2), Decimal::new(725, 4)) == Decimal::new(10725, 2)

examples/crosslib-app/units/pricing/apply_tax.spec.passport.json

@@ -13,7 +13,7 @@
   },
   "deps": [],
   "local_tests": [],
-  "generated_at": "2026-05-11T22:23:29Z",
+  "generated_at": "2026-05-13T16:36:50Z",
   "source_file": "examples/ecommerce/units/money/round.unit.spec",
   "evidence": {
     "build_status": "pass",

examples/crosslib-app/units/pricing/apply_tax.unit.spec

@@ -28,7 +28,7 @@
       "expect": "apply_discount(Decimal::new(10000, 2), Decimal::new(10, 2)) == Decimal::new(9000, 2)"
     }
   ],
-  "generated_at": "2026-05-11T22:23:29Z",
+  "generated_at": "2026-05-13T16:36:50Z",
   "source_file": "examples/ecommerce/units/pricing/apply_discount.unit.spec",
   "evidence": {
     "build_status": "pass",