Skip to content

Commit dd4008f

Browse files
committed
Add bounded same-tree chain3 TypeScript execution
1 parent b4f40d0 commit dd4008f

12 files changed

Lines changed: 1560 additions & 1244 deletions

File tree

CHANGELOG.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44

55
### Changed
66

7-
- **The bounded TypeScript lane now proves the same-tree wrapper family in M52** — eligible `kind:function` roots may still use the helper-aware monotone-up lane from M46, and may now also classify to `function.wrapper.pipeline.v1` when they declare the exact same-tree local dep tuple `function.arithmetic_leaf.monotone_down_nonnegative.v1` then `function.arithmetic_leaf.monotone_up.v1`. The lane remains Bun-only, atom-only, and additive to Rust proof; it still does not widen to chain3 execution, molecule execution, generic multi-dep execution, seam kinds, cross-library TypeScript resolution, `spec validate --target-language`, or `spec export --target-language`.
7+
- **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`.
88

99
## 0.14.0 - 2026-05-07
1010

ORCH_PLAN.md

Lines changed: 528 additions & 673 deletions
Large diffs are not rendered by default.

PLAN.md

Lines changed: 359 additions & 547 deletions
Large diffs are not rendered by default.

README.md

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -47,14 +47,16 @@ spec validate examples/ecommerce/units
4747
spec generate examples/ecommerce/units
4848
```
4949

50-
## Bounded TypeScript lane (M52)
50+
## Bounded TypeScript lane (M54)
5151

5252
`spec` now exposes one bounded TypeScript execution lane. It is intentionally narrow:
5353

5454
- Bun is the only TypeScript prerequisite. The lane shells out to `bun`; no alternate Node, npm, or tsx contract is supported.
55-
- Eligible roots are exactly `kind: function` specs that classify to either `function.arithmetic_leaf.monotone_up.v1` or `function.wrapper.pipeline.v1`.
55+
- 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`.
5656
- 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.
5757
- 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`.
58+
- 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`.
59+
- 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.
5860
- Rust remains the default target. TypeScript proof is additive only; it writes `target_proofs.typescript` without replacing the Rust proof surface.
5961
- TypeScript execution is atom-only. Only `local_tests` run in this lane; `.test.spec` molecule tests remain unsupported for `--target-language typescript` and fail before Bun runs.
6062
- The accepted `local_tests.expect` grammar is deliberately small: `<current_unit>(Decimal::new(int, scale), ...) == Decimal::new(int, scale)`. The left-hand side must be a direct call to the current unit, and both the arguments and expected value must use integer-literal `Decimal::new(...)` forms.
@@ -68,19 +70,19 @@ spec test <path> --target-language typescript
6870
spec status <unit-or-root> --target-language typescript
6971
```
7072

71-
`spec status <unit-or-root> --target-language typescript` reports target-specific proof only. In M52, 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 or wrapper lane, or truthfully remains outside that lane.
73+
`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.
7274

73-
The generated helper filenames remain frozen in M52:
75+
The generated helper filenames remain frozen in M54:
7476

7577
- `__spec_ts/runtime.ts`
7678
- `__spec_ts/build_entry.ts`
7779
- `__spec_ts/local_tests.ts`
7880

79-
Commands and surfaces that do not widen for M52:
81+
Commands and surfaces that do not widen for M54:
8082

8183
- `spec validate` does not accept `--target-language`
8284
- `spec export` does not accept `--target-language`
83-
- This lane does not widen to chain3 execution, molecule execution, generic multi-dep execution, seam kinds, cross-library TypeScript resolution, `spec validate --target-language`, or `spec export --target-language`.
85+
- 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`.
8486

8587
## Spec format
8688

TODOS.md

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -190,6 +190,8 @@
190190

191191
- [x] **Wrapper TypeScript execution in `spec`** — Completed by M52 (2026-05-12). The bounded Bun-backed TypeScript lane now admits the same-tree `function.wrapper.pipeline.v1` family with the frozen direct local dep tuple `monotone_down_nonnegative -> monotone_up`, while keeping proof additive and target-specific.
192192

193+
- [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.
194+
193195
- [ ] **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.
194196

195-
- [ ] **Generic multi-dependency TypeScript execution** — Deferred again after M52. The current lane is intentionally family-shaped: helper-aware monotone-up roots plus same-tree wrapper roots only, not arbitrary dependency topologies.
197+
- [ ] **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.

semantic-families/function.wrapper.pipeline.chain3.v1/fixtures/aligned/units/pricing/checkout_chain3_aligned.unit.spec

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,12 @@ body:
2424
let surcharged_total = pricing_tax_leaf_aligned(base_total, surcharge_rate);
2525
pricing_discount_leaf_aligned(surcharged_total, loyalty_rate)
2626
}
27+
typescript: |
28+
{
29+
const base_total = pricing_total_wrapper_aligned(subtotal, discount_rate, tax_rate);
30+
const surcharged_total = pricing_tax_leaf_aligned(base_total, surcharge_rate);
31+
return pricing_discount_leaf_aligned(surcharged_total, loyalty_rate);
32+
}
2733
local_tests:
2834
- id: checkout_chain3_aligned_basic
2935
expect: checkout_chain3_aligned(Decimal::new(10000, 2), Decimal::new(10, 2), Decimal::new(10, 2), Decimal::new(10, 2), Decimal::new(10, 2)) == Decimal::new(9801, 2)

semantic-families/function.wrapper.pipeline.chain3.v1/fixtures/aligned/units/pricing/pricing_discount_leaf_aligned.unit.spec

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,11 @@ body:
1818
{
1919
(subtotal - subtotal * rate).max(Decimal::ZERO)
2020
}
21+
typescript: |
22+
{
23+
const discounted = subtotal.add(subtotal.mul(Decimal.new(-1n, 0n).mul(rate)));
24+
return discounted;
25+
}
2126
local_tests:
2227
- id: pricing_discount_leaf_aligned_basic
2328
expect: pricing_discount_leaf_aligned(Decimal::new(10000, 2), Decimal::new(10, 2)) == Decimal::new(9000, 2)

semantic-families/function.wrapper.pipeline.chain3.v1/fixtures/aligned/units/pricing/pricing_tax_leaf_aligned.unit.spec

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,10 @@ body:
1717
{
1818
subtotal + subtotal * rate
1919
}
20+
typescript: |
21+
{
22+
return subtotal.add(subtotal.mul(rate));
23+
}
2024
local_tests:
2125
- id: pricing_tax_leaf_aligned_basic
2226
expect: pricing_tax_leaf_aligned(Decimal::new(10000, 2), Decimal::new(10, 2)) == Decimal::new(11000, 2)

semantic-families/function.wrapper.pipeline.chain3.v1/fixtures/aligned/units/pricing/pricing_total_wrapper_aligned.unit.spec

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,11 @@ body:
2020
let discounted = pricing_discount_leaf_aligned(subtotal, discount_rate);
2121
pricing_tax_leaf_aligned(discounted, tax_rate)
2222
}
23+
typescript: |
24+
{
25+
const discounted = pricing_discount_leaf_aligned(subtotal, discount_rate);
26+
return pricing_tax_leaf_aligned(discounted, tax_rate);
27+
}
2328
local_tests:
2429
- id: pricing_total_wrapper_aligned_basic
2530
expect: pricing_total_wrapper_aligned(Decimal::new(10000, 2), Decimal::new(10, 2), Decimal::new(10, 2)) == Decimal::new(9900, 2)

spec-cli/tests/cli.rs

Lines changed: 155 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1328,6 +1328,25 @@ fn inject_typescript_body_if_missing(unit_path: &Path, typescript_body: &str) {
13281328
fs::write(unit_path, rewritten).unwrap();
13291329
}
13301330

1331+
fn remove_typescript_body(unit_path: &Path) {
1332+
let contents = fs::read_to_string(unit_path).unwrap();
1333+
let (before, after) = contents
1334+
.split_once("\n typescript: |\n")
1335+
.expect("expected a typescript body block to remove");
1336+
let (_, tail) = after
1337+
.split_once("\nlocal_tests:\n")
1338+
.expect("expected local_tests after the typescript body block");
1339+
let rewritten = format!("{before}\nlocal_tests:\n{tail}");
1340+
fs::write(unit_path, rewritten).unwrap();
1341+
}
1342+
1343+
fn replace_in_file(path: &Path, from: &str, to: &str) {
1344+
let contents = fs::read_to_string(path).unwrap();
1345+
let rewritten = contents.replace(from, to);
1346+
assert_ne!(rewritten, contents, "expected fixture rewrite for `{}`", path.display());
1347+
fs::write(path, rewritten).unwrap();
1348+
}
1349+
13311350
fn setup_m12_data_seam_project() -> (tempfile::TempDir, PathBuf) {
13321351
let temp_dir = temp_repo_dir();
13331352
let project_dir = temp_dir.path().join("m12-data-seam");
@@ -15445,7 +15464,7 @@ fn typescript_near_miss_rejects_before_bun_runs() {
1544515464
let stderr = String::from_utf8_lossy(&output.stderr);
1544615465
assert!(
1544715466
stderr.contains(
15448-
"TypeScript target requires compatibility key function.arithmetic_leaf.monotone_up.v1 or function.wrapper.pipeline.v1 in M52; found function.arithmetic_leaf.monotone_down_nonnegative.v1"
15467+
"TypeScript target requires compatibility key function.arithmetic_leaf.monotone_up.v1, function.wrapper.pipeline.v1, or function.wrapper.pipeline.chain3.v1 in M52; found function.arithmetic_leaf.monotone_down_nonnegative.v1"
1544915468
),
1545015469
"{stderr}"
1545115470
);
@@ -15595,12 +15614,142 @@ fn typescript_molecule_test_is_rejected_before_bun_runs() {
1559515614

1559615615
#[cfg(unix)]
1559715616
#[test]
15598-
fn typescript_chain3_wrapper_rejects_before_bun_runs() {
15617+
fn typescript_chain3_wrapper_executes_with_bun() {
15618+
if !bun_available() {
15619+
return;
15620+
}
15621+
1559915622
let (_temp_dir, fixture_dir) = copy_m21_chain3_fixture("aligned");
15623+
let output = run_in(
15624+
&fixture_dir,
15625+
&[
15626+
"test",
15627+
"units/pricing/checkout_chain3_aligned.unit.spec",
15628+
"--target-language",
15629+
"typescript",
15630+
],
15631+
);
15632+
assert_output_success(
15633+
"aligned chain3 fixture should pass in the bounded same-tree TypeScript lane",
15634+
&output,
15635+
);
15636+
15637+
let passport = read_passport_json(
15638+
&fixture_dir.join("units/pricing/checkout_chain3_aligned.spec.passport.json"),
15639+
);
15640+
assert_eq!(
15641+
passport["target_proofs"]["typescript"]["evidence"]["build_status"],
15642+
"pass"
15643+
);
15644+
assert_eq!(
15645+
passport["target_proofs"]["typescript"]["evidence"]["test_results"][0]["status"],
15646+
"pass"
15647+
);
15648+
}
15649+
15650+
#[cfg(unix)]
15651+
#[test]
15652+
fn typescript_chain3_wrong_family_rejects_before_bun_runs() {
15653+
let (_temp_dir, fixture_dir) = copy_m21_chain3_fixture("unsupported_near_miss");
15654+
inject_typescript_body_if_missing(
15655+
&fixture_dir.join("units/pricing/checkout_chain3_unsupported_near_miss.unit.spec"),
15656+
" {\n const base_total = pricing_total_wrapper_unsupported_near_miss(subtotal, discount_rate, tax_rate);\n const surcharged_total = pricing_tax_leaf_unsupported_near_miss(base_total, surcharge_rate);\n return pricing_discount_leaf_unsupported_near_miss(surcharged_total, loyalty_rate);\n }",
15657+
);
15658+
inject_typescript_body_if_missing(
15659+
&fixture_dir.join("units/pricing/pricing_total_wrapper_unsupported_near_miss.unit.spec"),
15660+
" {\n const discounted = pricing_discount_leaf_unsupported_near_miss(subtotal, discount_rate);\n return pricing_tax_leaf_unsupported_near_miss(discounted, tax_rate);\n }",
15661+
);
15662+
inject_typescript_body_if_missing(
15663+
&fixture_dir.join("units/pricing/pricing_tax_leaf_unsupported_near_miss.unit.spec"),
15664+
" {\n return subtotal.add(subtotal.mul(rate));\n }",
15665+
);
1560015666
inject_typescript_body_if_missing(
15667+
&fixture_dir.join("units/pricing/pricing_discount_leaf_unsupported_near_miss.unit.spec"),
15668+
" {\n const discounted = subtotal.add(subtotal.mul(Decimal.new(-1n, 0n).mul(rate)));\n return discounted;\n }",
15669+
);
15670+
15671+
let marker_path = fixture_dir.join("bun-invoked.txt");
15672+
let fake_bun = format!(
15673+
"#!/bin/sh\nif [ \"$1\" = \"--version\" ]; then\n echo '1.2.15'\n exit 0\nfi\necho invoked > \"{}\"\nexit 99\n",
15674+
marker_path.display()
15675+
);
15676+
let path_override = path_with_fake_bun(&fixture_dir, &fake_bun);
15677+
15678+
let output = run_in_with_env(
15679+
&fixture_dir,
15680+
&[
15681+
"test",
15682+
"units/pricing/checkout_chain3_unsupported_near_miss.unit.spec",
15683+
"--target-language",
15684+
"typescript",
15685+
],
15686+
&[("PATH", path_override.as_os_str())],
15687+
);
15688+
assert!(
15689+
!output.status.success(),
15690+
"unsupported chain3-like TypeScript target should be rejected before Bun"
15691+
);
15692+
let stderr = String::from_utf8_lossy(&output.stderr);
15693+
assert!(
15694+
stderr.contains("unsupported.function.v1"),
15695+
"{stderr}"
15696+
);
15697+
assert!(
15698+
!marker_path.exists(),
15699+
"chain3 wrong-family rejection should happen before Bun build/test execution"
15700+
);
15701+
}
15702+
15703+
#[cfg(unix)]
15704+
#[test]
15705+
fn typescript_chain3_missing_typescript_body_rejects_before_bun_runs() {
15706+
let (_temp_dir, fixture_dir) = copy_m21_chain3_fixture("aligned");
15707+
remove_typescript_body(
15708+
&fixture_dir.join("units/pricing/pricing_total_wrapper_aligned.unit.spec"),
15709+
);
15710+
15711+
let marker_path = fixture_dir.join("bun-invoked.txt");
15712+
let fake_bun = format!(
15713+
"#!/bin/sh\nif [ \"$1\" = \"--version\" ]; then\n echo '1.2.15'\n exit 0\nfi\necho invoked > \"{}\"\nexit 99\n",
15714+
marker_path.display()
15715+
);
15716+
let path_override = path_with_fake_bun(&fixture_dir, &fake_bun);
15717+
15718+
let output = run_in_with_env(
15719+
&fixture_dir,
15720+
&[
15721+
"test",
15722+
"units/pricing/checkout_chain3_aligned.unit.spec",
15723+
"--target-language",
15724+
"typescript",
15725+
],
15726+
&[("PATH", path_override.as_os_str())],
15727+
);
15728+
assert!(
15729+
!output.status.success(),
15730+
"chain3 targets with missing direct-dep TypeScript bodies should be rejected"
15731+
);
15732+
let stderr = String::from_utf8_lossy(&output.stderr);
15733+
assert!(
15734+
stderr.contains("TypeScript chain3 target requires direct deps to author body.typescript in M54"),
15735+
"{stderr}"
15736+
);
15737+
assert!(
15738+
!marker_path.exists(),
15739+
"missing body.typescript rejection should happen before Bun build/test execution"
15740+
);
15741+
}
15742+
15743+
#[cfg(unix)]
15744+
#[test]
15745+
fn typescript_chain3_wrong_dep_order_rejects_before_bun_runs() {
15746+
let (_temp_dir, fixture_dir) = copy_m21_chain3_fixture("aligned");
15747+
replace_in_file(
1560115748
&fixture_dir.join("units/pricing/checkout_chain3_aligned.unit.spec"),
15602-
" {\n const base_total = pricing_total_wrapper_aligned(subtotal, discount_rate, tax_rate);\n const surcharged_total = pricing_tax_leaf_aligned(base_total, surcharge_rate);\n return pricing_discount_leaf_aligned(surcharged_total, loyalty_rate);\n }",
15749+
"deps:\n - pricing/pricing_total_wrapper_aligned\n - pricing/pricing_tax_leaf_aligned\n - pricing/pricing_discount_leaf_aligned\n",
15750+
"deps:\n - pricing/pricing_tax_leaf_aligned\n - pricing/pricing_total_wrapper_aligned\n - pricing/pricing_discount_leaf_aligned\n",
1560315751
);
15752+
1560415753
let marker_path = fixture_dir.join("bun-invoked.txt");
1560515754
let fake_bun = format!(
1560615755
"#!/bin/sh\nif [ \"$1\" = \"--version\" ]; then\n echo '1.2.15'\n exit 0\nfi\necho invoked > \"{}\"\nexit 99\n",
@@ -15620,16 +15769,16 @@ fn typescript_chain3_wrapper_rejects_before_bun_runs() {
1562015769
);
1562115770
assert!(
1562215771
!output.status.success(),
15623-
"chain3 wrapper TypeScript target should be rejected in M52"
15772+
"chain3 targets with wrong dep order should be rejected"
1562415773
);
1562515774
let stderr = String::from_utf8_lossy(&output.stderr);
1562615775
assert!(
15627-
stderr.contains("function.wrapper.pipeline.chain3.v1"),
15776+
stderr.contains("TypeScript chain3 target requires direct deps to classify as function.wrapper.pipeline.v1 then function.arithmetic_leaf.monotone_up.v1 then function.arithmetic_leaf.monotone_down_nonnegative.v1 in M54"),
1562815777
"{stderr}"
1562915778
);
1563015779
assert!(
1563115780
!marker_path.exists(),
15632-
"chain3 wrapper rejection should happen before Bun build/test execution"
15781+
"wrong dep order rejection should happen before Bun build/test execution"
1563315782
);
1563415783
}
1563515784

0 commit comments

Comments
 (0)