Claude/thalyx programmable transaction hrexv1 - #3
Merged
CesarManzoCode merged 6 commits intoAug 30, 2026
Conversation
…hat never disappears The 2026-08-29 Fedora run reported 2 FAILED and two `NOT PROVEN` for one cause with two faces. **Why sudo could not see the toolchain.** `dev/verify.sh` needs root, rustup installs into the invoking user's home, and `sudo` sets `HOME=/root`. There were three separate searches for a Rust binary in this repository — one in `metadata::cargo` (`$CARGO`, else the bare name, which is a `PATH` walk), one in `analyzer::find` (`$HOME/.rustup`, then `PATH`), one in `exec::find_cargo` (`$HOME` and two system paths) — and all three asked about a home the process running them did not have. `HAVE_ANALYZER` in `verify.sh` did the same, so a machine where `rustup component add rust-analyzer` had just succeeded was told to install rust-analyzer. They are now one: `thalyx_rust::toolchain`. It looks in named places, in this order — what `THALYX_CARGO`/`THALYX_RUST_ANALYZER` name, what `RUSTUP_HOME` and `CARGO_HOME` say, `$SUDO_USER`'s home from the passwd database, `$HOME`, then `/usr/local/bin` and `/usr/bin` — and never walks `PATH`, because a verdict produced by whichever compiler came first on a caller's environment is a verdict nobody can reproduce. Every candidate is *run* before it is believed: `~/.cargo/bin/rust-analyzer` exists on every rustup install and is a shim that answers `error: Unknown binary`. A refusal now names every path it looked at. "There is no cargo" is a sentence nobody can act on when the cargo is one directory away under another home. **Why two tests failed.** `exec::tests::a_check_of_bytes_nobody_has_seen_is_run` and `the_rust_check_selects_the_crates_the_change_reaches` both assert `output["cached"] == false` and got `Null`: the `no_cargo` arm — the one the missing toolchain took — never wrote the field, and neither did the two arms above it. So the failure a person read was two assertions about a cache, and what had happened was a `HOME`. `cached` is now written by every arm the check has, with a test that walks them rather than one that happens to take one. The confined `cargo` is also *told* where the toolchain is now: `ForeignRequest` carries an environment, `RUSTUP_HOME` and `CARGO_HOME` reach the child, and the grant list comes from `toolchain::readable` instead of being assembled at the call site. A grant list written twice is two lists, and the second is always missing the entry that only matters on somebody else's machine — which under `sudo` is every entry. This is not a widening: the root filesystem holds only what was granted and the LSM refuses every open the policy does not name, so a path in a variable that nobody granted names something that is not there. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018bpdo399t4oTK6fLo5QDXd
…x order `Provider::ask_about` resolved a name with `candidates.into_iter().find(|s| s.name == name)`. On a workspace holding `crate_a::Config`, `crate_b::Config` and `crate_c::Config` that is: take whichever one rust-analyzer listed first, describe it as *the* `Config`, and answer `source: "rust-analyzer"` — which is true, and is exactly why it would have been believed. What acts on that answer is `renombrar-simbolo`. So the failure was one of three crates rewritten everywhere it is used, chosen by index order, with nothing anywhere saying a choice had been made. A confident wrong answer is the worst shape a wrong answer has. `known` now returns a `Resolution` with three arms — `Nothing`, `One`, `Several` — and there is no way to get a declaration out of it without having handled the third. Each candidate carries its kind, its crate, its container, its signature and a handle that is `path:line:column`: deliberately the shape `renombrar` and `contexto` already take, so resolving an ambiguity needs nothing new to be learned. Nothing is ranked; a "most likely" candidate would be the guess this shape exists to remove, wearing a disclaimer. `contexto` carries `resolution` on every answer — `one`, `ambiguous`, `nothing`, `file`, or `matched` when it came from the index, which matches text and is therefore never entitled to claim an ambiguity. `renombrar-simbolo` refuses with the word `ambiguous`, the candidate list, and `files_changed: 0`, from `place` — which runs before `rename_texts`, which writes nothing, which runs before the loop that opens files. The tree is byte for byte what it was and the test asserts the bytes rather than the count. Two entries at one position are one declaration: rust-analyzer answers a workspace-symbol query out of several indexes and the same item can come back twice, so candidates are sorted and deduped by position. Without that a workspace with exactly one `Config` in it would get a refusal nobody could act on. `KIND_SYMBOL` becomes `rust.symbol.2`. What is stored under it changed shape, and a store written by the old one would deserialise as a miss on every question forever, in silence. Every test has the control rule 4 asks for: `Unmistakable`, declared once in the same tree, resolves and renames. Without it a provider that answered `Several` to everything would pass all of this while having broken the programming face. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018bpdo399t4oTK6fLo5QDXd
…cally
`hacer` took a `Vec<Step>`, which means the model had to know every operation
and every argument before anything ran. That is batching. It cannot express
the thing an agent actually spends its turns on — ask, look at the answer,
decide — so every one of those decisions was a round trip to a frontier model,
dragging the whole conversation with it.
`hacer` now takes `run`: a short JavaScript program, executed here, inside the
same reversible boundary. Variables, loops, `if`, arrays, string work,
structured values, assertions, and calls to the machine whose answers the next
line reads. The model is asked again when the program finishes, when it calls
`thalyx.needModel(…)`, or when it cannot continue.
**QuickJS, compiled in.** The language is not sacred and the properties are;
what decided it: a frontier model already writes JavaScript, so the syntax
costs zero prompt; QuickJS's core has no ambient authority to take away — no
`fs`, no `net`, no `process`, no `require`, no `fetch` — so a program starts
able to do arithmetic and reaches only what is bound, which is the opposite of
embedding a shell where the work is subtracting authority from something that
starts with all of it; it is C99 with no dependencies, so it links into the
static musl image the way SQLite already does; and it can be stopped.
**The program is not the authority.** It runs on its own thread and asks the
machine over a channel; every request is served by `Runner`, whose `request`
is `external::one` — the same function, the same argument check, the same
workspace boundary a single request goes through. Its `validate` is the same
`run_check` the declarative list uses, and its `changed` is
`thalyx_snapshot::difference` against the same snapshot. There is no second
store, no second checker and no second boundary. A refusal comes back as a
value with `ok: false`, which the program branches on — turning it into an
error would make every mistake end the run, which is the opposite of being
able to write `if`.
**The hole a program opened, and closing it.** `Program::read` refuses a
*step* named `exec` or `attempt` before a snapshot is taken, which is right
for a list because a list is a value something can look at. A program is not:
it reaches verbs by name at runtime. A test asked for `attempt abandonar` from
inside a program and got `ok: true` with a `confirm_with` line carrying the
snapshot name and the exact state witness the machine had just computed — two
more lines and the transaction would have abandoned itself, mid-run, with
`carry_out` still holding a boundary that no longer existed. `NOT_FROM_INSIDE`
refuses both verbs at the moment of the call, and the refusal hands back
nothing to retry with.
**Ceilings, because a language can loop.** `MOST_STEPS` bounded the old form
by construction; nothing bounds a program but counting. Wall time and an
instruction budget through the engine's interrupt handler, a memory ceiling, a
stack ceiling, a ceiling on machine calls, on processes started, on bytes of
answers taken in, and on the size of what may be returned — the last refused
rather than truncated, because a halved answer is one a model acts on
believing it is whole. `while (true) {}` terminates; so does a loop that
catches its own interruption, which is the shape a model writes without
meaning to.
**Assertions latch.** `thalyx.assert` records the failure where the program
cannot reach it, throws, and halts the engine. A `try`/`catch` around it
cannot get past it, because the thing that stops the run is not in the
language. `needsModel` works the same way, and is neither a success nor a
failure: the transaction puts the tree back, so a program that met a decision
it would not make leaves nothing behind.
The evidence keeps the source, the finish, every call's whole answer as a
step — the same shape `evidencia <id> paso=N` already fetches — and what the
program printed. What crosses back is `returned`, whatever the program decided
mattered.
The fixtures are the claim. A tree of five modules where three use `old_api`
and *which three is not visible from the names*: one request lists, loops,
reads each, changes three, leaves two, observes what really changed, validates,
branches on the validation, and returns three names. A `Vec<Step>` cannot
express it — to produce the same result it would have to already contain the
answer. Beside it: the same program over a tree that will not parse rolls back
byte for byte with the diagnosis kept; a program that asks for the model
changes nothing; and a composition test where A's answer is a count nothing
outside the tree knows, B is a decision on it, and C runs on one side only —
run twice over two trees, with the program identical and the branch different.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_018bpdo399t4oTK6fLo5QDXd
The list is the prompt. Fourteen schemas arrived with every inference of every session, and each was a branch the model had to consider before any work happened. That is the tool proliferation the research named as a hazard in its own right — not a matter of taste, and not fixed by writing "prefer these three" in a description that competes with eleven others for attention. Since `thalyx_exec` takes a program, an operation no longer needs a schema to be reachable: `thalyx.read`, `thalyx.grep`, `thalyx.substitute`, `thalyx.list` and the rest are one line each inside a program and cost nothing until one is used. That is the research's conclusion exactly — one always-available programmable capability, with the specific operations beneath it. So the default surface is `thalyx_context`, `thalyx_exec`, `thalyx_evidence`: what a name is, do a stretch of work, fetch what the work did not send back. **Nothing is deleted.** `--surface legacy`, or `THALYX_MCP_SURFACE=legacy`, offers the whole catalogue. It stays for compatibility, for debugging, for the benchmarks already run against it, and — the reason it will not be removed — as the control column: "the small surface is better" is a comparison, and a comparison needs its other arm. The adapter's own tests run against it, since what they exercise is framing and refusals rather than which tools are advertised. `thalyx_exec`'s description is now the whole of what a model needs, because it is most of what a model sees: the `thalyx` object's methods listed by name, what a check answers, that a refusal is a value to branch on rather than an error, that `assert` stops the run and cannot be caught, that `needModel` leaves the workspace untouched, and that only what the program returns crosses back. The two new adapter tests skip with `NOT PROVEN` where there is no Btrfs — `hacer` opens a real boundary — and they decide that by *running* the smallest possible program rather than by looking at the filesystem, because a test that infers its own precondition from something adjacent is rule 5's eighth entry. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018bpdo399t4oTK6fLo5QDXd
This module said, in its own header, that the provider is *a reader*: it never applies an edit, a rename comes back as a description, and Thalyx does the writing. Every word of that is true about the LSP protocol and none of it is true about the process tree. **rust-analyzer runs Cargo.** To answer anything about a workspace holding a proc-macro or a build script it compiles and runs them — arbitrary code from a registry, executing at analysis time, with whatever reach the process that started it had. Which was Thalyx's own: the whole filesystem, and the network. "It does not apply edits, therefore it is read-only" was the wrong conclusion from a true premise, and it stood for a week. It now starts through `thalyx_core::start_foreign` — the same establishment `ejecutar` uses, so there is one enforcement gate and one uid assignment rather than two. `run_foreign` was refactored onto the same `establish`, since a second launcher is a second place for the checks to drift and the one that drifts is always the one nobody runs on the machine that can enforce. The provider gets: its own user; its own cgroup with a policy in the kernel; its own root filesystem holding the workspace, the toolchain and the registry and nothing else; its own pid namespace, so killing the one process Thalyx holds kills every `cargo`, `rustc` and build script under it; its own network namespace, which is what "network denied by default" means here; and the seccomp filter. It is granted the workspace read and write — rust-analyzer's first act on a workspace with no `Cargo.lock` is to write one — the toolchain read-only, and a build directory outside the tree, because a `target/` inside the workspace is inside the snapshot and a rollback would destroy the build cache that makes the next question cheap. `profile::semantic_provider` is `module_standard` with two numbers changed: 6 GiB instead of 1, because a provider killed partway through indexing reports as "the analyzer timed out", which is a true sentence about the wrong thing; and 2048 processes instead of 512, because this is a compiler *tree*. It is not a service framework and there is exactly one of them. `thalyx-rust` learns none of that. It gained a `Spawn` trait and a `Started` carrying a boxed teardown closure, so the crate that resolves names does not depend on the crate that confines processes — a `thalyx-rust` that knew about cgroups would be the semantic provider deciding what a process may reach. **It falls back, it says so, and it can be made to refuse.** `start_foreign` refuses where the kernel is not denying — `Programas-Ajenos.md`'s decree, and right — and a Thalyx that could therefore not resolve a symbol at all would be a machine where the programming face does not exist. So on such a machine it runs on the host and every answer carries `analyzer_confined: false` with the reason in `analyzer_how`. `THALYX_REQUIRE_CONFINED_ANALYZER=1` turns the fallback into a refusal: rule 3's shape, one variable per requirement, so a machine that can enforce can demand that it did rather than silently getting a host process on the day the LSM failed to load. Two supporting pieces. `Cgroup::kill` writes `cgroup.kill` rather than walking `cgroup.procs` and signalling: the walk races the tree it is walking, and the tree here forks. `ForeignProcess` holds an `Option<Child>` so the analyzer can own the conversation while the confinement stays behind to be torn down — the first shape left a placeholder process running and made this depend on a `/bin/true` existing, and the image holds the Linux kernel and one program. The teardown waits, bounded, for the cgroup to empty before releasing, because `SIGKILL` is delivered rather than completed and a release that finds the cgroup occupied declines — leaving a kernel policy outliving what it was written for. Whether this machine actually confines it is `dev/verify.sh`'s question. What the tests demand is the honesty, which holds everywhere: every semantic answer says which of the two happened, the two fields agree, and neither is ever absent. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018bpdo399t4oTK6fLo5QDXd
Stage 59 of `dev/verify.sh` is the sprint's own claim on the only machine that
can hold it: a tree of five modules where three use `old_api` and **which three
is not visible from the file names**, run over a real Btrfs subvolume with a
compiler under a kernel that really denies. One request lists a directory
nobody has described, loops, reads five files, changes three, leaves two,
watches the subvolume agree, compiles what the change reaches, branches on the
verdict, and answers with three names.
Four columns, because the first is only believable with the other three: the
same program over a tree with nothing to change changes nothing — without it, a
program that always edited three files would pass; a program whose check cannot
pass leaves the subvolume byte for byte with the diagnosis in the store; and
`while (true) {}` after a mutation stops and rolls back. A fifth line, reported
separately, says whether the semantic provider was confined or was a host
process — merging that into the result would let a green stage hide a compiler
tree running with Thalyx's own reach.
**The program lives in `dev/programs/looking-decides.js` and both places read
it.** A program copied into a shell script and into a Rust test is two
programs, and the second is the one with the typo nobody finds until Fedora. So
`the_program_verify_runs_is_the_one_that_is_tested_here` runs the same file
against the directory-backed fake on every `cargo test`, and what stage 59 adds
is the half a container cannot have: a real snapshot, a kernel that denies, a
compiler that runs.
Running it here immediately found something. The program's strict assertion —
`the tree shows 4 change(s) and the program made 3` — caught `Cargo.lock`:
rust-analyzer resolves the full dependency graph, and resolving writes a lock,
so a workspace without one **gains a file because it was asked a question**. A
read that mutates the tree, inside the transaction, attributed to nobody. Same
family as the `target/` that used to land in the snapshot. Nothing is hidden —
`changed()` reports it and a rollback removes it — and the fixtures now carry a
lockfile, which is what a real workspace has committed. The first version of
that constant was hand-written and Cargo rewrote it, which is rule 6 in the
small.
Stage 53 now also runs `thalyx-program` and the two ambiguity suites, so the
arithmetic it checks includes the control flow and the refusal.
The vault: `Transaccion-Programable` is the new decree; `Ejecucion-Transaccional`
and `Semantica-Compilada` carry revisions saying what changed and why;
`Estrategia-de-Pruebas` gains seven rules, each written from the thing that
went wrong; `Punto-Actual`, `Tareas-Pendientes` and the README say where the
project is. The semantic provider's pendiente is closed by half — the process
is under Thalyx's authority now, and where its binary comes from inside the
image is still Cesar's.
Checked here: `cargo fmt`, `cargo clippy --workspace --all-targets` clean, 1873
tests passing with a real rust-analyzer, and the one program the image carries
builds static-pie for `x86_64-unknown-linux-musl` with QuickJS compiled into
it — rule 12, and the half of this sprint that could have arrived unbootable.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_018bpdo399t4oTK6fLo5QDXd
CesarManzoCode
deleted the
claude/thalyx-programmable-transaction-hrexv1
branch
September 5, 2026 03:01
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
2 participants
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.
No description provided.