Bankrupt TypeScript + the bug zoo#1936
Merged
Merged
Conversation
TS had no source-oracle resolve path (lift-refusal + an LLM propose path, the least-developed kit), so per the whole-tree bankruptcy it goes. The bug zoo (the main `pnpm exec tsx` consumer) is bankrupt too. Deleted: implementations/typescript, the 2 ts shims (typescript-better-sqlite3 / -pg), the 3 ts realize manifests, menagerie/bug-zoo (workspace member + Makefile target), and the wholly-ts rust integration tests (cmd_recognize_typescript_parity / cmd_emit_typescript_vitest / cmd_mint_typescript_source_runtime_failure / cmd_verify_typescript_production_bridge, and the now-empty library_tag_dispatch_test). build-ts / test-ts + the ci.yml node/pnpm setup removed; build-ts dropped from test-rust + build-all. kit_declaration_rpc's typescript test already skip-guards on BCARGO_TYPESCRIPT_ENV (skips in CI). numpy stays (the proof); java is the next bankruptcy. cli tests compile; make ci parses. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
|
Important Review skippedToo many files! This PR contains 295 files, which is 145 over the limit of 150. To get a review, narrow the scope: ⚙️ Run configurationConfiguration used: Organization UI Review profile: CHILL Plan: Pro Run ID: ⛔ Files ignored due to path filters (5)
📒 Files selected for processing (295)
You can disable this status message by setting the Use the checkbox below for a quick retry:
✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 3bf58a27f7
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Comment on lines
-25
to
-30
| export function main(argv: string[] = process.argv.slice(2)): void { | ||
| if (!argv.includes("--rpc")) { | ||
| process.stderr.write("usage: provekit-lift-typescript-source --rpc\n"); | ||
| process.exit(1); | ||
| } | ||
| runRpcMode(); |
There was a problem hiding this comment.
After deleting this RPC entry point, the checked-in root manifest .provekit/lift/typescript-bind/manifest.toml still runs npx tsx implementations/typescript/src/lift/typescript-source/bin.ts --rpc for --lang=typescript / typescript-bind. I searched for a replacement for that path and there is none, so any TypeScript bind/lift invocation now fails before the plugin can initialize instead of cleanly retiring the surface.
Useful? React with 👍 / 👎.
Comment on lines
-25
to
-29
| import { readFileSync, readdirSync, statSync, mkdirSync, writeFileSync } from "node:fs"; | ||
| import { join, resolve, extname } from "node:path"; | ||
| import { KeyObject } from "node:crypto"; | ||
| import ts from "typescript"; | ||
|
|
There was a problem hiding this comment.
The Supply Chain Rails runner is still a Rust workspace member and its npm lifter still shells out to pnpm exec tsx menagerie/supply-chain-rails/authenticated-betrayal/kit-rpc/supply-chain-ts-contracts.ts, which imports ../../../../implementations/typescript/src/lift/index.js. Since this deletion removes that module and I found no replacement export, the documented provekit-supply-chain-rails --all path fails at TypeScript module resolution whenever it reaches run_typescript_contract_lifter.
Useful? React with 👍 / 👎.
Comment on lines
-1
to
-7
| /** | ||
| * Entry point for the provekit-lsp-ts daemon binary. | ||
| * Invokes the main loop. | ||
| */ | ||
| import { main } from "./daemon.js"; | ||
|
|
||
| main(); |
There was a problem hiding this comment.
The root package.json still publishes the provekit-lsp-ts bin, and bin/provekit-lsp-ts.cjs still resolves this deleted implementations/typescript/src/lsp/daemon-entry.ts file before spawning tsx. In environments where users install or copy that bin (also referenced by provekit-linkerd), invoking provekit-lsp-ts now exits with a missing-module error rather than starting or being explicitly unavailable.
Useful? React with 👍 / 👎.
TSavo
added a commit
that referenced
this pull request
Jun 6, 2026
Two CI failures on this branch were inherited from #1936 (TypeScript + bug-zoo bankruptcy), red on main too -- references to things #1936 deleted but did not clean up: - `bug_zoo_machinery_is_self_contained` (cli_surface.rs) asserted `menagerie/bug-zoo/Cargo.toml` EXISTS -- but #1936 deleted the bug zoo. The test is obsolete; `provekit_cli_does_not_expose_zoo_subcommand` still holds and stays. - `.github/workflows/provekit.yml` was a TS/node "prove" job whose only steps typecheck (`tsc --noEmit`) and test (`pnpm test`) the deleted `implementations/typescript` tree -- TS18003 "no inputs found" every run. A job that only checks deleted code is not a gate. The real signal is `acid test (make ci)` (rust + python). - `tsconfig.json` pinned `include: implementations/typescript/src` (gone). Deleted all three. The acid test now has no dangling rust test; the dead TS gate is removed rather than left rotting red. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
Jun 6, 2026
`package_inspection_rejects_missing_npm_tarball` invokes the supply-chain-npm lifter (run-supply-chain-npm-lifter.sh -> tsx), which the TypeScript bankruptcy (#1936) deleted. The run now fails "tsx not found" before reaching the missing-tarball path the assertion checks, so the test grades a dead TS lifter. Its sibling tsx-driven tests are already ignored (#1476); ignore this one to match, with a note to re-enable when the npm supply-chain demo is redone off the removed TS lifter. The rust `package inspect` tests (no tsx) keep running. (The doctor::doctor_kit_declaration_non_rust_vocabulary_rejects_unknown_concept CI failure is a kit-LSP-spawn flake -- it passed in the sibling acid-test job on the SAME commit and passes locally -- not addressed here.) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
Jun 6, 2026
) * Add the pandas.testing lift seat (sibling of numpy.testing) The next package up the ladder from numpy is pandas, and per the federation design it is just another lifter package: provekit-lift-py-pandas-testing, the exact sibling of provekit-lift-py-numpy-testing, reusing the pytest seat's term/formula machinery so equivalent claims federate. The pandas EXACT/APPROXIMATE discipline is SHARPER than numpy's because pandas makes approximate the DEFAULT: assert_frame_equal / assert_series_equal compare floats with a tolerance unless check_exact is pinned. (Confirmed against pandas 3.0.3: check_exact's default is the <no_default> sentinel, resolved at runtime by dtype.) So lifting an un-pinned frame assertion as `=` would FALSE-PASS, claiming exact equality pandas never checked. Version-independently, the seat lifts a frame/series/index/extension-array assertion as `=` ONLY when check_exact=True is explicitly pinned AND no relation-altering keyword (check_like, rtol/atol, check_dtype, ...) is present; everything else is a LOUD REFUSE. The whole pandas._testing (tm) 22-name vocabulary is recognised so nothing real is silently skipped -- the trichotomy: express the exact, loudly refuse the rest. assert_equal is deliberately excluded (cross-library generic name owned by the numpy/generic seat). Honest scope: a frame/series equality is opaque-EUF on both sides, so z3 cannot manufacture a contradiction between two opaque DataFrame constructors -- same as numpy array equality. The CONSISTENCY teeth for pandas come from SCALAR assertions, which the pytest bare-assert seat already lifts (and this seat lifts when they ride a claimed pandas.testing test). This seat's load-bearing job is sound loud-refusal of approximate frame comparison plus callsite keying of the pandas op under test for the witness axis. 17 unit tests: positive lifts (check_exact pinned), the approximate-by-default refusal, relation-altering-kwarg refusals, mutation/control-flow/side-effect refusals, SSA independence, broad-tm claim+refuse, and assert_equal non-claim. Wired into the Makefile test-python loop. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Add pandas-showcase: the two-axis correctness claim on pandas Stands up pandas next to numpy, proving correctness with zero code changes. Differs from numpy-showcase only by swapping in the pandas.testing seat and pointing the witness venv at pandas -- the next package is just another lifter package, as designed. Three lift seats over the project: the plain pytest CONSISTENCY seat (scalar assertions, where z3's teeth are), the pandas.testing seat (frame assertions; approximate-by-default refused unless check_exact pinned), and pytest-witness (runs the tests under real pandas). The project deliberately contains a buggy (self-contradictory) test, so the showcase proves the CORRECT pandas code AND catches the contradiction -- refused BOTH ways: consistency: Series.sum() == 6 consistent (discharged); == 6 AND == 7 UNSAT (refused). witness : the good tests reproduce (discharged); the contradictory run is 'failed' (refused). run.sh is self-checking: it asserts provekit produces exactly that verdict and exits non-zero otherwise. Verified green (4 discharged, 2 refused). Scope: demonstrates lift + prove (consistency + witness by recompute). The stricter signed-receipt verify path re-resolves each witness body, which for the pytest-witness kit needs a packaged witness body or full re-run metadata forwarded by the verifier -- a follow-up increment, noted in the README. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Add python-guard-shapes: the 2x4 runtime-guard matrix (numpy + pandas) Guard shapes #2-#5 (index-bounds, empty-container, divide-by-zero, key-access) proved on BOTH numpy and pandas -- 8 cells, each a real library idiom with a discrimination mutant. Zero code changes. These are RUNTIME faults (IndexError / ValueError / KeyError / silent inf), not logical contradictions, so the consistency (z3) axis is blind to them: `a[5] == 0` is a consistent proposition. Only running the code catches the bug, so this example registers ONLY the pytest-witness seat -- the axis that proves correctness by execution. It re-runs each case under real numpy/pandas: the guarded `_ok` case is witnessed (discharged); the `_bad` case breaches the guard so the run raises (or, for divide-by-zero, the finiteness assertion fails) and the witness is refused. Divide-by-zero is the sharp cell: numpy/pandas return silent `inf` rather than raising; provekit catches it because `_ok` asserts isfinite and `_bad` fails it. The witness is per-file (runs `pytest <file>`), so `_ok`/`_bad` are separate files -- 8 cells x 2 = 16. run.sh checks the verdict PER FILE (every `_ok` discharged, every `_bad` refused), so a swapped or missing verdict fails the gate. Verified green: 8 discharged, 8 refused. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Fix verify witness re-resolution for all-tests projects (empty code_files) The signed-receipt verify path refused good witnesses with "no package file and not re-runnable" on projects that are all tests (numpy/pandas showcases). Root cause: the resolve_witness RECOMPUTE guard tested `memento.get("code_files")` for truthiness, but an all-tests project pins an EMPTY code_files (the code under test is the installed library, not a local file), and `[]` is falsy in Python. So a trivially re-runnable witness was declared not re-runnable. Fix is one line: gate on `code_files is not None` (present), not truthiness. The empty list is part of the pinned witness body and reconstructs correctly, so the tamper check at line 150 still holds -- this stays sound. After the fix, verify re-resolves the good witnesses by recompute (rust re-runs the test, recomputes the CID, matches) and refuses the contradictory ones as failed runs -- the same verdict prove gives. Confirmed on pandas-showcase and python-guard-shapes. Adds a regression test driving the resolve_witness RPC with an empty-code_files witness (would fail pre-fix), and drops the now-stale verify caveat from the pandas-showcase README. Kit tests: 20 passed. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Witness Oracle: per-test granularity + the multi-witness .witness bundle At full-package scale the per-FILE witness fell over: the Oracle ran `pytest <file>` and keyed ONE witness off the file's exit code, so a single failing test out of ~1,600 refused the whole file (numpy: all 179 files refused, ~every passing test discarded). That is not a numpy finding, it is a granularity defect. Running witnessing is the Oracle's job, so the fix lives in the Oracle's run primitive, shared by mint (lift) and verify (recompute). PER-TEST (witness.py + _witness_collect.py): run_file_witnesses runs the file ONCE -- in the package's own execution context (conftest, fixtures, relative imports) -- and a tiny pytest plugin (_witness_collect, json/os only, loaded standalone so it never drags in the kit dep chain) records every test's outcome. One file run -> one witness PER TEST, keyed by the pytest node id. run_and_witness routes a node id back through its file, so LIFT and RECOMPUTE agree on outcome under shared file state. Proven on real numpy test_scalarmath.py: 1,582 per-test witnesses, 1,581 discharged, 1 isolated refusal (was: whole file refused). .witness BUNDLE (witness.py): A per-test run of a real package yields thousands of witnesses; one file per CID or thousands of inline .proof mementos do not scale. write/read_witness_bundle pack MANY bodies into ONE content-addressed .witness file -- JSONL, one canonical body per line, blake3(line) == that witness's cid. The content IS the key: no index, nothing to trust; the Oracle resolves by scan + blake3, exactly its content-address check. read_witness_body now resolves from bundles too. mint writes the bundle to .provekit/witnesses/; the .proof carries only the signed pointers. Also fixes a real full-scale robustness bug: bind_rpc._send crashed with UnicodeEncodeError when a pandas source emoji (🐍) split a surrogate pair across the 9,802-binding response; now encodes with errors="replace" so one pathological character never aborts the run. Lesson recorded: a real package's suite must be witnessed against the INSTALLED package, not a loose copy -- a compiled package (numpy) cannot be duplicated and imported alongside itself (ndarray-type identity clash). Kit: 23 tests (3 new: per-test, recompute-agreement, content-addressed bundle). Examples green: guard-shapes 8/8, pandas-showcase both axes. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Witness addressing: the proof carries ONE cid -- a WitnessPackageMemento The full-package numpy proof was 900 MB / 99,189 members because the proof carried 48,935 witnesses BY VALUE (a ContractDecl + memento per test). That is an addressing bug, not a size problem: a proof should carry witnesses BY REFERENCE -- one content-addressed package, not N inline bodies. The oracle mints, the verifier asks the oracle, the proof carries one cid: - MINT (the oracle): `build_suite_bundle` runs the whole suite per-test and assembles ONE content-addressed `.witness` package (cid = blake3(bundle)). `handle_lift` emits ONE `WitnessPackageMemento` (a pointer + signature over the package cid, carrying the test/code files the oracle needs to reproduce it) and ONE contract whose evidence pins the package cid. NOT N mementos. - VERIFY (the verifier asks the oracle): UNCHANGED. `try_witness_discharge` already spawns the kit's discharge command; `witness_verify` already calls `resolve_witness`. So discharge re-runs the suite, rebuilds the package, and confirms it reproduces the pinned cid (`discharge_bundle`); the signed dimension resolves the package by cid (package file or recompute) and content-addresses it. No rust change. - THE PROOF CARRIES ONE WITNESS CID: the package. Per-test granularity lives IN the package (each line a witness body, self-addressing), committed by the one cid. Result on guard-shapes: proof 900MB-shape -> 4,394 bytes, 99k members -> 2 (one package contract + one WitnessPackageMemento), the 16 per-test facts in the content-addressed package. Discharge re-runs the suite and names the exact 8 failing tests. verify resolves the package via the package file, blake3 matches. A package DISCHARGES iff it reproduces AND every test passed; a failing test refuses it (naming the failures) -- which is what a failing test in a package means. Examples read per-test discrimination straight from the package. Kit: 25 tests (2 new: package one-cid roundtrip + refuses-on-failure/drift). guard-shapes + pandas-showcase green. No compressor, no RNG -- content-addressing is the dedup, determinism is the point. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Delete the inline-source path: the SourceMemento is the only thing a proof carries A flag (PROVEKIT_LEAN_SOURCE=1) gated the right thing -- so the DEFAULT proof inlined the function body, a doubled copy of code the package already holds, and you had to remember a flag to get the lean SourceMemento. A flag gating correctness means the default is wrong. Deleted, not inverted. - bind_lifter: `_body_source_locator` is the FULL reconstruction (locus + cids + body + ast_template) -- what the Source Oracle returns. The MINT path strips it to the SourceMemento (`source_memento_of`: file, source_cid, span, template_cid, param_names) before anything enters the `.proof`. The body NEVER touches the proof. No flag, no fat alternative. - source_oracle: the flag-pop dance is gone; the reconstructor is unconditionally complete, so resolve just calls it. Deleting the bad path flushed out every consumer that was secretly leaning on the inline body (the whole point of deleting it): - `_binding_template_from_sugar_entry` REQUIRED inline ast_template and silently DROPPED lean bindings. Recognize matches by template_cid (always present, even lean), so the gate was wrong; build the template for lean entries and carry `body_source` + `source_function_name` so the oracle can resolve. - `materialize_impl` indexed only bindings that already had `body_text`, so a lean binding produced "no sugar binding in scope" and 0 materialized. Now it resolves the body through the Source Oracle -- the same resolution recognize uses. Result: numpy-showcase mints lean with NO flag -- 0 inline body, SourceMementos only. recognize + materialize + the snake-eats-tail fixpoint all resolve from disk via the oracle, CID-verified, refusing on drift. The proof signs what you run; it does not carry a copy of it. Tests migrated off the deleted inline form to assert the SourceMemento + oracle reconstruction. python-source 235, pytest-witness 25, py-tests 349 -- all green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ci: remove the TS/bug-zoo bankruptcy leftovers that rot the gate Two CI failures on this branch were inherited from #1936 (TypeScript + bug-zoo bankruptcy), red on main too -- references to things #1936 deleted but did not clean up: - `bug_zoo_machinery_is_self_contained` (cli_surface.rs) asserted `menagerie/bug-zoo/Cargo.toml` EXISTS -- but #1936 deleted the bug zoo. The test is obsolete; `provekit_cli_does_not_expose_zoo_subcommand` still holds and stays. - `.github/workflows/provekit.yml` was a TS/node "prove" job whose only steps typecheck (`tsc --noEmit`) and test (`pnpm test`) the deleted `implementations/typescript` tree -- TS18003 "no inputs found" every run. A job that only checks deleted code is not a gate. The real signal is `acid test (make ci)` (rust + python). - `tsconfig.json` pinned `include: implementations/typescript/src` (gone). Deleted all three. The acid test now has no dangling rust test; the dead TS gate is removed rather than left rotting red. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ci: ignore the supply-chain test that drives the deleted TS lifter `package_inspection_rejects_missing_npm_tarball` invokes the supply-chain-npm lifter (run-supply-chain-npm-lifter.sh -> tsx), which the TypeScript bankruptcy (#1936) deleted. The run now fails "tsx not found" before reaching the missing-tarball path the assertion checks, so the test grades a dead TS lifter. Its sibling tsx-driven tests are already ignored (#1476); ignore this one to match, with a note to re-enable when the npm supply-chain demo is redone off the removed TS lifter. The rust `package inspect` tests (no tsx) keep running. (The doctor::doctor_kit_declaration_non_rust_vocabulary_rejects_unknown_concept CI failure is a kit-LSP-spawn flake -- it passed in the sibling acid-test job on the SAME commit and passes locally -- not addressed here.) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
TypeScript was the least-developed kit: no source-oracle resolve path (just a lift-refusal + an LLM
proposepath), so per the whole-tree bankruptcy it goes. The bug zoo — the mainpnpm exec tsxconsumer — is bankrupt too.Deleted
implementations/typescriptprovekit-shim-typescript-better-sqlite3/-pg).provekit/realize/menagerie/bug-zoo(workspace member + Makefile target + help echo)cmd_recognize_typescript_parity,cmd_emit_typescript_vitest,cmd_mint_typescript_source_runtime_failure,cmd_verify_typescript_production_bridge, and the now-emptylibrary_tag_dispatch_test)Build/CI
build-ts/test-tstargets; droppedbuild-tsfromtest-rust+build-allSelf-skipping leftovers (harmless):
kit_declaration_rpc's ts case skip-guards onBCARGO_TYPESCRIPT_ENV;multi_kit::test5_typescript_kit_dispatchskip-guards onprovekit-lsp-tsbeing on PATH (never built now). Both skip in CI.numpy stays (the proof). Java is the next bankruptcy (keeping the tested Product-A core).
cli tests compile;
make ciparses.