Experiment: dark compile <fn> (merge compiler repo into main repo)#5690
Draft
StachuDotNet wants to merge 172 commits into
Draft
Experiment: dark compile <fn> (merge compiler repo into main repo)#5690StachuDotNet wants to merge 172 commits into
dark compile <fn> (merge compiler repo into main repo)#5690StachuDotNet wants to merge 172 commits into
Conversation
Make the package store event-sourced: the op logs (package_ops, branch_ops, resolutions) are the canonical, append-only source of truth, and the package / location / deprecation tables are projections folded from them. A store "grows" by applying unapplied ops and evaluating values; a schema change is safe (drop projections, re-fold the log). This is the durable, stable base that sync rides on — the append side and the fold side are cleanly split. - Op logs + projections as plain SQLite tables. `Seed.growIfNeeded` applies unapplied ops, regenerates refs, and evaluates values — and self-heals a store that has ops applied but values still NULL (evaluates any NULL rt_dval on startup) instead of leaving it stuck. Value reads are null-safe for a not-yet-evaluated value (returns None, never a NULL crash). The self-heal is silent maintenance — it never prints to stdout. - Convergence: timestamp-LWW by one canonical `origin_ts` (Lww); a synced `resolutions` overlay so a human override travels and peers converge on it; `conflicts` records every auto-resolved divergence (never silent). - Meaning-stable, content-addressed hashing (alpha-normalized) so the same definition hashes identically on every instance — the basis for convergence. - Release / version model and a legacy-DB adopt that runs schema.sql before stamping. Op playback applies branch structure before content. (LibDB, LibExecution, LibSerialization, LocalExec, schema + migrations) Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The F# builtins that expose the store + sync primitives to the Dark side. Kept thin and content-addressed; each carries a real capability so untrusted `dark run` code can't reach the raw file/SQL or op-log surface. - Op-log builtins: append/read the package, branch, and resolution logs; the blob channel (content-addressed bytes, fetch-on-miss) with `syncBlobInsert` re-hashing peer bytes so a poisoned/mismatched blob is rejected. - The arbitrary-path `sqlite*` builtins are gated by a `fileReadWrite` capability (the interpreter no longer skips their capability check). - Package-manager getters by hash (values / fns / types) and the conflict list/keep/acknowledge builtins that back `dark conflicts`. (backend/src/Builtins) Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Package sync over HTTP, written in Dark. Local-first: sync is opt-in, and
all your branches sync wholesale — a branch is the same id+name on every
instance you connect (no per-branch private/follow controls).
- Engine (sync.dark): connect/pull/serve, per-peer resume cursors, the
bounded ops-over-HTTP wire, and receive that folds branch structure before
content. `connect` probes GET /sync/health so a dead/typo'd peer URL is
caught up front. A DB error during pull stops without advancing the cursor
(no silent divergence). Adaptive daemon poll interval, clamped + validated.
- Server (sync/server.dark): the /sync/{health,events,blobs,blob} endpoints
a peer pulls from.
- CLI: `dark sync` (+ `daemon` for background pull/serve on boot),
`dark conflicts` (review + keep-mine/keep-theirs — `show` renders each
version's actual contents, not just hashes), `dark ops` (inspect the log),
`devices`, and login/serve wording fixes. `conflicts` + `ops` are in the
compact command list so they're discoverable.
- Stdlib: the generic eventLog append/fold + sqlite helpers the engine uses.
(packages/darklang)
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Cross-instance convergence is the property that matters, tested at three levels plus supporting unit coverage. - `MultiInstance.Tests.fs` — in-process, true multi-store (a swappable test connection repoints LibDB at each instance). Branch sync + identity consistency, package convergence, cross-store conflict + LWW + recorded divergence, keep-mine/keep-theirs, resolution-survives-rebuild, rebase and deprecation convergence, pagination. Carries an in-process CLI driver so a test can assert on what the CLI actually renders (incl. a `dark conflicts` display regression). - `SyncScenarios.Tests.fs` — fast one-store order-independence (= convergence). - `OpsProjections.Tests.fs` — receiveOps idempotency/convergence, the origin_ts MIN-reconcile, detection, the full conflict → resolution flow. - `SyncE2E.Tests.fs` — flag-gated (DARK_E2E=1) heavy tier: real `dark` processes syncing over real HTTP — the server, pull loop, cursors, and process isolation the in-process tests can't reach. Basic sync, conflict race + keep-mine/keep-theirs, branch sync, offline-peer honesty. - Testfiles (blob channel, adaptive poll, eventlog, sqlite) + unit coverage for alpha-normalized hashing and the Release model. (backend/tests, backend/testfiles) Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
`Stdlib.List.collect` isn't a function (never defined, not a builtin), but `cli/utils/syntaxHighlighting.dark` calls it at two sites — so every `dark view` (which highlights its output) errored with "List.collect not found". Replace each `|> List.collect f` with `|> List.map f |> List.flatten` (the same semantics). Unrelated to sync — it's a pre-existing regression on main surfaced by rebasing onto it; folded here so this branch builds green. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Feriel (account …0004) is the collaborator persona. schema.sql seeded an extra 'Ocean' account (…0005) that duplicated her — removed it, and moved the four SyncE2E `login Ocean` calls to `login Feriel` so they still resolve. Example peer URLs `ocean.tailnet` → `feriel.tailnet`. Prep for real two-machine testing (Stachu + Feriel). Full suite + DARK_E2E green (9,956/0). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
export-seed dropped projections but kept `trace_fn_calls`/`traces` — dev run telemetry that ballooned the seed (268 MB of a 305 MB store) and thus every shipped CLI. Strip them: seed 305 MB → 35 MB, gzip → exe far smaller. Traces are never part of a seed's canon. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The config path in portable mode was the relative string "rundir/cli-config.json" — resolved against the process CWD. A released exe runs from wherever the user is (e.g. $HOME), which has no rundir/, so `login` printed "Logged in" but persisted nothing, and the next `commit` said "Not logged in". Anchor the config to the store's own directory (dirname of localDbPath) — absolute, always-present, CWD-independent, and identical to today's path for the dev CLI and installed mode. SyncE2E's now-needless rundir/ setup dropped; suite green (5/5 E2E). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
A keep-mine/keep-theirs override mints a synced Resolution that converges the value everywhere — but the peer that independently recorded the same divergence kept showing "1 unreviewed conflict" (value said 100, its conflict record still pointed at the stale LWW winner). recordAndApply now marks any auto-resolved conflict at the location overridden, so applying a resolution (local OR synced-in) settles the review log on every instance. Found on real two-machine testing (pop-os + framey). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
`dark conflicts` listed only hashes — you couldn't tell what actually
diverged without running `show` on each. Now each conflict previews both
values inline:
Stachu.Demo.clash (value)
yours 111 · theirs 222 → theirs active (auto:last-writer-wins)
For a value it drops the redundant "val <name> =" and shows just the body;
fns/types show the trimmed signature. See the divergence at a glance.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
A full-screen view (apps, outliner, CLI views) launched with stdin redirected — from a script, a pipe, or a daemon — crashed with a raw InvalidOperation_ConsoleReadKeyOnFile stack dump: Console.ReadKey and Console.KeyAvailable both throw when input isn't a console. Detect redirected input in readKeyOrPaste and report Escape, which every view already treats as "exit", so it closes cleanly instead of blowing up. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The inline conflict preview showed the item's SIGNATURE (identical on both sides) instead of its BODY (where the two versions actually differ), so a fn/type conflict looked the same on both sides. And the non-active candidate rendered its own name as "<hash:SHORT>" — a name isn't part of an item's content-addressed hash, so the pretty-printer can't resolve it from the (superseded) binding. renderInline now shows the definition body (the part after the first " = "), collapsed to one line and truncated — so you see "Hello," vs "Hey there," at a glance. renderContent restores the real leaf name (known from the conflict's location) over the placeholder, so `show` reads cleanly for fns and types too. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ergence) A synced-in 'keep theirs'/'keep mine' resolution was silently reverted on the next grow, so two peers that agreed via a resolution DIVERGED. Effective binding = fold(package_ops)[LWW] -> then apply resolutions. The full rebuild path (rebuildProjections) already re-applied the overlay after re-folding, but growIfNeeded — the incremental fold that runs when a pull brings new ops — folded them by LWW and never re-applied resolutions. So a 'keep theirs' that a peer synced in was clobbered by the very op it was meant to override the moment the next command triggered a grow: the binding reverted to the LWW loser while the deciding peer stayed on the chosen version. Repro: A and B both author name N differently; B keep-theirs -> B converges; A pulls B's resolution -> A momentarily converges, then a grow reverts A to the LWW winner. A=X, B=Y, stuck. Fix: growIfNeeded re-applies Resolutions.reapplyAll after the fold when it applied new ops, symmetric with rebuildProjections. Also mark the conflict 'overridden' in reapplyAll (mirrors recordAndApply) so the resolved divergence doesn't pop back up as unreviewed in `dark conflicts` after a grow. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
… the fix) 3232aa6 re-applied the overlay after growIfNeeded's fold, but the pull folds through a different path — receiveOps calls applyUnappliedOps directly and returns, so after a pull all ops are already applied and the next growIfNeeded sees appliedCount=0 and never re-applies. Net: a synced-in keep-theirs still lost to auto-LWW on the receiving peer. Add the reapply at receiveOps' own fold site (gated on foldedCount>0), so the overlay is restored immediately after the pull folds ops — including the case where the overlay's own apply was an idempotent no-op because the peer happened to already be on the chosen value, and the later fold then moved it to the LWW winner. Semantics: a manual resolution DOMINATES the auto pick, locally and on any peer it syncs to (verified target: reapplyAll is not stale-gated out here — res.at is later than the op it overrides). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
`apps status` filtered to Registry.installed, so a daemon started with `apps start <slug>` but not "installed" (auto-start-on-login) printed "no daemon apps installed" even while it was actively running — misleading right after you start one (e.g. the sync daemon). Now it lists every daemon that's installed OR currently running, and the empty message points at `apps start sync`. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The authoring account is recorded on every commit (commits.account_id) and syncs across instances, and getCommitsForBranchChain already resolves it to a name (committerName) — but `dark log` never displayed it. On a shared / multi-user tailnet you couldn't tell WHO made a change from the history, only what + when. Print committerName on each log line (dimmed). Pure display fix; the data was already there + synced. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…bounded disk-fill) The soak caught a hard blocker: two sync daemons cross-pulling every ~30s grew each data.db to 93 GB / 186 GB in ~40 min (only 10,664 ops). Cause: trace storage is ON by default and has NO retention/GC (its own TODO admits this), and a `serve` request records its ENTIRE response as trace args — the sync endpoints return whole op/blob batches, so single trace_fn_calls rows reached ~900 MB. Every daemon pull traces the serve side, forever, until the disk fills (framey hit 0 bytes; `dark` then crashes with raw 'disk is full'). Traces are dev telemetry — already STRIPPED from the exported seed — so the shipped binary must not accumulate them. Flip TraceDetail default to Off (opt back in with DARK_CONFIG_TRACE_DETAIL=on), and set that var in config/dev + config/circleci so development and CI are unchanged (tests also pin via setForTesting). Interactive `dark eval` already uses noTracing, so this only stops the serve/daemon trace accumulation. Follow-up (existing TODO, not this commit): per-row size cap + a retention sweeper, so traces can be safely re-enabled by default. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…blob promotion) The earlier commit defaulted trace storage off but only gated the DB row write (TraceStorage.store). The sync soak then caught a SECOND unbounded growth: package_blobs ballooned (~4/3x per pull) even with traces 'off'. Root (same as the trace disk-fill): storeTrace runs prepareDvalForStorage BEFORE the store's off-check, and that PROMOTES every captured ephemeral blob into package_blobs (so a trace survives its VM). The serve traces each request (createCliTracer, HttpServer), and the sync endpoints' responses are whole op/blob batches — so their blobs got promoted on every pull, forever, with no GC. Confirmed by an instrumented Blob.insert: the inserts came from Tracing.prepareDvalForStorage -> promoteEphemeralLeaf -> Blob.insert on the serve. Fix: make trace-detail OFF a true no-op. storeTrace bails immediately when off (before prepare/promote/store) — the single choke point for both the sqlite and CLI tracers — and create returns the non-tracer when off (skip capture too). Verified on two real machines: daemons ran several minutes, data.db held at 43 MB (was GB-scale), package_blobs had 0 rows >1 MB, 0 blob inserts observed, and sync still converged (a beacon propagated A->B). Both disk-fill bugs closed. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…isk-fill) Both red-green verified (fail without the fix, pass with it): - MultiInstance 'resolution survives the INCREMENTAL fold on the pull path': guards the divergence fix. The existing test only covered a full rebuildProjections; this folds a fresh op through receiveOps (the pull path) after a resolution and asserts the human override survives. Models the idempotent-skip case that receiveOps' fold used to clobber. With the reapply disabled it reverts to the LWW winner and errors. - SyncE2E 'daemon disk-safety: serving pulls accumulates NO traces + NO oversized blobs': guards the trace disk-fills. Serves one instance, pulls it repeatedly, asserts the SERVER's trace_fn_calls stays 0 and package_blobs doesn't grow past the seed. With the storeTrace off-gate disabled the server promotes a fresh blob per request (4 after a few pulls) and errors — the test class that would have caught the overnight 90-186 GB disk-fills. Full in-process suite re-run after all overnight changes: 9,951 passed / 0 failed. SyncE2E tier (DARK_E2E=1): 6 passed / 0 failed. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Bare `dark sync` folded every failed pull into an `unreachable` counter and
printed "Couldn't reach N of M instance", discarding the actual error. But a
pull can fail for reasons that have nothing to do with reachability — most
notably "{peer}: a database error applying ops — stopped without advancing the
cursor". Bucketing those as "unreachable" is an outright lie: the peer answered
fine (curl to /sync/events returns 200), the *apply* failed.
This surfaced during branch stress-testing: two branches created independently
on two instances with the SAME name (different uuids) violate the branch-name
UNIQUE constraint. The losing CreateBranch is INSERT-OR-IGNORE'd away, its
package_ops then reference a branch id that doesn't exist locally, and the FK
check aborts the pull. The operator saw only "Couldn't reach" and chased a
phantom network problem for hours.
Collect each pull's real Error message (already peer-prefixed and
self-describing) and print them verbatim, so a genuine unreachable peer and a
DB-apply error read as the different problems they are.
The underlying same-name-branch convergence gap (independent creation breaks the
"same id+name everywhere" invariant and jams the cursor) is a separate structural
follow-up, tracked with the merge-timing divergence residual.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Tighten comments that had narrated the development of this branch rather than documenting the code: the trace-storage disk-fill incident specifics (GB/minute figures, "before this default flipped"), "overnight fix"/"the nastiest shape"/ "before the fix" in the regression tests, "phase-1/phase-2 measurements", "premature for this PR", and a couple of over-long TODO rationales. No behavior change — comments and one test-assertion message only. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Two robustness fixes to human conflict resolution: - conflictKeep now refuses a chosenHash that isn't one of the conflict's two candidates (localHash/incomingHash). A Resolution must bind content that was actually in contention at that location; without the guard a caller could mint a SYNCED Resolution to arbitrary content and converge every peer onto it. - keep-mine/keep-theirs now branch on conflictKeep's Bool like `ok` already does, instead of discarding it and unconditionally printing "Kept … will sync". If the conflict was concurrently acknowledged/removed (keep returns false) the user is no longer told a resolution was minted when it was a no-op. Verified: backend builds clean; packages load; MultiInstance (17) + SyncScenarios (6) resolution/conflict tests pass; `conflicts keep-mine <missing>` reports no open conflict. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The first-run setup prompt stored port/interval on a bare Int.parse success, bypassing the 1..65535 / positive-interval range checks that `dark sync daemon config` enforces — so `0`/`70000` got written and only failed later at daemon start. Route both through daemonConfigValue (the same validator), so an out-of-range value is rejected at the prompt instead of silently persisted. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
reapplyAll runs on every op-applying grow and every pull that folds, calling markOverriddenByLocation once per stored resolution — an UPDATE filtered on (branch_id, location, status). sync_conflicts was indexed only on detected_at, so each call full-scanned the table, making reapply O(resolutions x conflicts) on the sync/startup hot path. Add the covering index. CREATE INDEX IF NOT EXISTS via schema.sql, so it also lands on existing stores on reload. Migration + release path verified: Releases tests (16) pass. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…n negative - The idempotence test compared computeFnHash(normalizeFn(normalizeFn f)) to computeFnHash(normalizeFn f), but computeFnHash normalizes internally — both sides got re-normalized, so a first-pass non-idempotence couldn't be observed. Compare the normalizeExpr structures directly (ids preserved, only binders renamed) over a body with real let/lambda/shadowing binders. - Add a negative test that match-binder POSITION matters: `| (x,y) -> x` must hash differently from `| (x,y) -> y`. The prior match test had a single binder, so a bug collapsing all match binders to one symbol would have passed. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The shipped CLI seeds a fresh store from the embedded db but never migrated an
EXISTING store from a previous release: it runs neither the schema-bootstrap nor
the Release migrator (those live in LocalExec, not the CLI), so a store whose
schema/op-format/hashing predates the running binary was used as-is — and crashed
on the first write (e.g. "table package_ops has no column named origin_ts") with
a raw SQLite stack trace, while the designed Release-3 clean-break never fired.
On startup, when data.db already exists, reconcile its Release stamp with this
binary's currentRelease. The release is read via a throwaway NON-POOLED
connection so LibDB's shared connection isn't bound to the old file before a
possible reseed, and the read distinguishes three cases:
- Stamped = current -> proceed
- Stamped > current -> refuse with a clear message + exit 1 (older code
must not open a newer store)
- Stamped < current, or PreTracking (no release_state_v0) -> crossing into the
current (clean-break) Release means the old package
data can't be reused in place; back up data.db
(+wal/shm) to a timestamped .bak and re-extract the
embedded current-Release seed, then tell the user
where the backup is and to re-pull / re-author.
- Unreadable (couldn't open/query at all) -> do NOT touch it; a transient lock
must never trigger a data-destroying reseed.
Verified end-to-end on a rebuilt release artifact: fresh install; same-release
no-op; pre-tracking old-shape store (the crash case) reseeds + first author now
succeeds; release-2 store reseeds; release-4 store refuses with exit 1 and leaves
the store untouched.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…n clean-break
The startup reconcile previously re-seeded (discard + backup) on ANY older/
pre-tracking store. But the Release framework already migrates a store forward
in place, source-free, for a DURABLE release (schema copy-swap + op-format
re-serialize + refold) — only a clean-break Release (e.g. a content-hashing
change, like Release 3) truly invalidates the on-disk data.
Add `Releases.planCliUpgrade` (pure, unit-tested): reuses `planRelease`, then
splits a Migrate on whether any pending step is `clearForRebuild`:
- Proceed / RefuseNewer — as before
- MigrateInPlace — all pending steps durable → run applyPending,
PRESERVING the store
- Reseed — a clean-break step, or a pre-tracking store of
unknown format → back up + re-seed from the embedded
current-Release store
The CLI reconcile now dispatches on it. Behaviour for the current Release 3
(clean-break) is unchanged — it still routes to Reseed — so this only adds the
data-preserving path for future additive/format releases. Five new planCliUpgrade
unit tests; existing Release tests still green (21 total).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The receive-side append builtins (packageOps/branchOps/resolutions) `List.choose` away any event/commit they can't parse. Those rows are dropped, not counted as applied — yet the pull cursor still advances past them, so a peer that ships a malformed op silently diverges the two stores with nothing recorded. The old comment even mislabelled the skips as "correctly count as applied"; they don't. Emit a visible warning at each skip site (`sync: skipped an unparseable <kind> from a peer (dropped, not applied) …`) so a divergence is diagnosable instead of silent. This is the stopgap; the real fix — quarantine the op + retry per-op and don't advance the cursor past it — is the structural per-op-isolation change tracked in CLEANUP(sync-security) / the fix proposals, and also closes the same-name-branch and cross-log-batch jams. Additive (fires only on a parse failure); MultiInstance + append path green. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…data The CLI's data-preserving upgrade path (planCliUpgrade MigrateInPlace -> applyPending -> applyRelease's durable branch) was unit-tested at the routing level but never exercised end-to-end on real data — the only shipped Release (3) is a clean-break, so the durable branch had never fired. Add a MultiInstance test over an isolated seeded store: apply a synthetic durable Release (an additive schema column, no clean-break) and assert the column lands in place, every op is preserved (not cleared), and the projected package content still resolves. Closes the "durable path unfired" gap and guards applyRelease's durable branch against regressions. MultiInstance now 18 (was 17). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
A clean-break reseed replaces data.db, which holds the sync peer list (sync_peers_v0) — so after an upgrade `dark sync` reported "you're not syncing with anyone yet" and the user had to re-add every peer. Peers are sync CONFIG, not disposable package content, so carry the peer URLs from the backed-up store into the fresh one (best-effort: if the table's absent or the copy fails, the reseed still succeeds). Cursors are deliberately NOT carried — a clean break means the fresh store must re-pull from scratch, so a stale cursor would skip ops. The reseed message now reports how many peers were kept. Found on a two-machine test: authored on B, reseeded A, re-pulled → data came back but A's peer to B was gone. This keeps it. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This kills the value-inlining blowup and finally lets valueRefsInExpr walk pipes.
The bridge INLINED a package value`s body at every EValue, and a value`s stored
body already had its own dependencies inlined into it -- so A gets spliced into C
with B already inside it, and down a chain the copies MULTIPLY. The bodies are
tiny (all 417 package values total 133KB; mean 319 bytes, max 6.5KB) -- it was
never big values, it was 2^depth copies of small ones. Adding EPipe to the walker
resolved enough extra references to make that visible: 55GB on a 50-fn batch.
Fix: a package value is a CONSTANT, and the runtime already evaluates and caches
it (package_values.rt_dval; all 417 populated). So ask the RT package manager for
the Dval, take the TYPE from it -- which is exactly what previously made this
impossible, since PT.PackageValue carries no declared type and FunctionDef
requires a ReturnType -- and emit each value ONCE as
`def __val.<hash>(__unit: Unit) : T = <literal>`. Every EValue becomes a call.
BridgeCtx.Values is now a Set: only membership matters, the body never travels.
An empty container (`let empty = []`) genuinely has no element type, so rather
than guess one it emits a GENERIC value fn (`def __val.<h><a>() : List<a> = []`)
and each call site infers -- which is what an empty literal should do anyway.
That alone took "value did not bridge" from 105 to 4.
With values shared, EPipe finally lands: the ~307-fn "package value not resolved"
bucket is GONE -- a value used inside a pipe is now seeded and fetched.
Measured (chunked sweeps kept corrupting -- see below -- so this is sampled):
- the 50-fn batch that hit 55GB: now 4.2GB, WITH pipes enabled
- one fn in isolation: ~0.00GB (the 4.2GB is 50 compiles of un-returned .NET
heap, not per-fn cost; GC.Collect() changes nothing -- collecting is not
decommitting)
- 250/250 random currently-compiling fns still compile: 0 regressions
- of 40 previously value-blocked fns, 4 now compile (~10% -> roughly +22 of 225);
the rest advance to REAL blockers -- 24 of 40 are altJsonFormat, an effectful
builtin that needs marshalling
- differential on the new ones: match, 0 diffs -- the Dval-reconstructed
literals give the same answers
- self-tests green; fib still matches the interpreter
The coverage delta is modest; the point is the architecture (values are 133KB
once, not 2^depth) and that the #1 bucket dissolved into nameable causes.
…preter
We could compile ~2000 fns but had only PROVEN 95 of them equal the interpreter.
The differential compared STDOUT, and the compiler prints records/nested containers
as empty (the print pass only handles lists of Int64/Bool/String/Float via
toDisplayString_*), so 434 fns ran fine and could never be checked. "51% compiles"
was a claim backed for 95 functions.
Make both sides emit the SAME canonical encoding and compare bytes:
- interpreter: Dval -> dvalToWire (already existed, and is the spec)
- compiled: Bridge.marshalTyped, its mirror — a type-directed serializer that
builds an expression emitting that exact format (escaped elements
joined by newline, Case / Case+payload, "unit"). Covers scalars, all
int widths, List, Tuple, Option, Result; isSerializableType says what
can be proven.
Real args, not synthesized zeros: Builtin.compilerEquivCheck takes the args as a
tuple (2+), a bare value (1), or () for none — a Dark list cannot hold mixed types.
The args are real Dvals, so dvalToAst hands the compiled side EXACTLY what the
interpreter gets.
Generic fns needed one more piece: List.head declares List<a> -> Option<a>, so its
return type still mentioned the tvar and was unserializable. unifyType binds the
type params structurally from the ACTUAL argument types, which both instantiates a
concrete entry point and makes the return type concrete (mainCall's existing
default — guess Int64 — is wrong once real args are involved).
Proven so far (each is a fn stdout could not check):
fib 20 -> match
String.slice("hello", 1, 3) -> match (3 args, String return)
List.head [10;20;30] -> match (generic, Option<Int64> return)
List.append [1;2] [3] -> match (generic, List<Int64> return)
And it reports honestly rather than passing: List.reverse -> cf|Undefined variable:
reverseHelper; a non-serializable return -> unprovable|<type>, never a silent "ran".
Next: a hand-authored args file (hash -> args) so this can run over the tree.
…PC seam wireToDval had no TInt case, so it fell through to `| _ -> DString s`. Dark's TInt is arbitrary-precision and is NOT TInt64 -- and buildEffectfulMap happily routes a TInt param (as WAInt) -- so every effectful builtin taking a TInt received its numbers as strings and returned garbage. intRandom(5,5) returned a fixed 3744625903238887673 no matter the bounds; the interpreter returns 5. Add TInt (and the remaining int widths, which had the same hole: TInt8/16/32/128 and TUInt8/16/32/64/128). This is the same shape as the DList-as-handle bug: the fn compiles, the fn RUNS, and it returns a wrong answer. A compile check can never see it. The equivalence harness found it within minutes of existing, on the first 30 fns swept -- which is the argument for the harness. Also fix a harness bug it exposed: unifyType used List.zip on declared-vs-actual arg types, which throws when arity differs (a Dark nullary fn declares one Unit param but is called with no args). Truncate to the common length instead. intRandom(5,5) -> match ; intRandom(1,1) -> match ; fib 20 -> match
Three limits kept the equivalence harness from proving most of what compiles. Over a
400-fn sample it went 105 -> 148 proven, with these:
1. ARGS for custom types (191 of 222 unprovable fns took a record or enum).
sampleArgDeep reads the type definition and builds a real Dval: every field for a
record, the first samplable case for an enum (so a recursive type terminates via
its base case, like zeroValue). noargs fell 222 -> 54.
2. RETURNS that are records/custom enums (104 + 68 of the rest). Both sides needed it
and had to agree byte-for-byte:
- dvalToWire had NO DRecord case at all -- records hit "?unmarshalable:DRecord",
so any record-returning fn was unprovable. Fields are emitted in NAME order
(DvalMap iterates sorted).
- marshalTyped grew TRecord (sort fields by name to match) and TSum for user enums
(match every variant; `Case` or `Case\n<escaped fields>`). A multi-field variant
is packed by the bridge into a TUPLE payload, so it is destructured and each
field escaped separately -- dvalToWire escapes fields individually, and encoding
them as a nested tuple would silently mismatch on every such enum.
3. NONDETERMINISM. The interpreter now runs twice; a fn that disagrees with ITSELF
(uuidGenerate, intRandom) reports `nondet` instead of a false DIFF. That is what
the one remaining DIFF in the 400-sample was -- a generated UUID.
Also fixed, all found by running the thing:
- sample ints 42 -> 5. 42 hung the entire sweep on the first exponential fn it met:
fib(42) interpreted is ~2000x fib(27), which alone takes 21s. A sample arg has to be
cheap as well as realistic.
- TrimEnd('\n') on compiled stdout ate newlines belonging to the VALUE and reported
two false DIFFs on strings that legitimately end in one. Strip exactly the one
Print appends.
- NonEmptyList.fromList [] threw for nullary fns (28 harness-exns); a nullary call is
spelled with a Unit arg.
Chunked sweeping is abandoned for this: equivOne caps the BINARY at 10s but the
interpreter call has no timeout, so one slow fn made a 20-fn chunk time out and emit
NOTHING -- silently costing 20 results. Run one fn per invocation and bound it from
the shell.
… say WHY not
Two fixes to the equivalence harness, both found by reading its own output.
1. GENERIC type defs were read without substituting the use site's type args. A def
stores `Only of 'a`, but the value in hand is `Scope<String>` -- so walking it hit a
bare TVar and the type looked unserializable. substTVarsB/defSubstB instantiate the
def's params from the args at both the checking and marshalling sites (records and
sums, including multi-field variants).
2. "unprovable|return type not serializable: TRecord(T.a6fa...)" told you nothing --
the exact vague-bucket trap that hid the last two big blockers. serializableReason
returns a REASON and names the culprit by path, so the same fn now reports:
T.<caps>.httpClient: T.<http>.methods: T.<scope>.Only: TVar "a"
which is what identified (1) in one line.
fib and List.head still prove out as match.
The seam only ever carried scalars in the ARG direction, so any builtin taking a record/enum was unroutable — altJsonFormat (arg: a Json enum), cliExecute, fileRead and ~300 others simply couldn't compile. This builds the arg half: - wireToDvalTyped: the daemon-side recursive decoder (wire -> Dval) for containers, records and enums — the mirror of Bridge.marshalTyped and the inverse of dvalToWire. Async, since it fetches type definitions. - unescWire: escWire's inverse. It never existed, because the daemon only ever ESCAPED (encoding a return); nothing had needed to decode. - WireArg += WATyped, marshalled with marshalTyped; BridgeCtx carries the emitted type defs so a record/enum arg can be encoded. - rtToMarshalable names custom types by hash. It is built from the runtime and has no type env, so it can't tell record from sum — marshalTyped/serializableReason now dispatch on the DEFINITION instead of the TRecord/TSum tag, so either works. - dispatchBuiltin decodes args with wireToDvalTyped (the scalar-only path is what made every TInt arg a string). Three bugs this surfaced, all of the "silently wrong" kind: 1. CRASH: marshalTyped INLINES the serializer, so a recursive type (Json = ... | Array of List<Json>) generated AST forever and core-dumped the CLI. A recursive type genuinely can't be encoded by a finite inlined expression — it needs a recursive serializer FN. Guard added; it now refuses cleanly. 2. Unencodable args fell back to the RAW VALUE, emitting code that sent a Json where the seam expects a String. Hard-fail instead. 3. Making rtToMarshalable name custom types also widened the RETURN path, where unmarshalTyped has no custom-type case and falls through to `| _ -> src` — it would have handed back the raw wire string AS the value. Gated returns on isMarshalableType: the arg and return directions have DIFFERENT capabilities and one must not imply the other. No coverage gain yet, and altJsonFormat still doesn't compile — but it now routes and says exactly what's missing: "unsupported-builtin: altJsonFormat: arg recursive type T.<json> (needs a recursive serializer fn)" which is true, and names the next piece of work instead of emitting wrong code. 60/60 sampled fns still compile (the apparent 59/60 was a 25s test timeout on a fn that compiles in 34s to a 2.7MB binary). fib, intRandom, slice, marshal/daemon self-tests all still match.
marshalTyped INLINES the serializer, so a recursive type could never be encoded: Stdlib.AltJson.Json is `... | Array of List<Json>`, and expanding it generated AST forever (it core-dumped the CLI before the guard). That blocked altJsonFormat, and with it ~98 fns. Emit ONE marshaller function per non-generic type instead — `__marshal.<T>(v: T) : String` — so recursion becomes a CALL and terminates. Its body is the only place a type expands inline (inFnBody=true); every nested custom type inside it becomes a call to that type's own marshaller. serializableReason agrees: once a non-generic type is seen, stop descending — the fn calls itself. Generic types are deliberately skipped: their marshaller needs a marshalling fn per type param (higher-order), which isn't built. They stay inline, which is correct as long as they aren't recursive — and the guard still catches it if they are. Result: altJsonFormat ROUTES. Of 25 previously altJson-blocked fns, 3 compile and the rest moved on to a genuinely different blocker: 15 unsupported-builtin: stringToBlob_v0 2 unsupported-builtin: blobToBytes_v0 i.e. Bytes through the seam is now the JSON bottleneck, not recursion. fib still matches; bridge and marshal self-tests green.
The equivalence harness, pointed at a non-ASCII input, found three routed builtins
that are NOT equivalent to their "native" counterparts. Each returned a wrong answer
in compiled code; ASCII hid all three completely:
Stdlib.String.length "héllo日本" -> compiled 12, interpreted 7
The compiler's String.length counts UTF-8 BYTES (it reads the length prefix;
__string_hash loops it with getByteAt). Dark counts CHARACTERS.
Stdlib.String.toUppercase "héllo" -> compiled "HéLLO", interpreted "HÉLLO"
Stdlib.String.toLowercase "HÉLLO" -> compiled "hÉllo", interpreted "héllo"
The compiler's case conversion is ASCII-only.
Un-route all three. This costs NOTHING: Dark's own implementations compile fine and
are unicode-correct, so all four cases now match. The "optimization" of substituting
the compiler's native versions WAS the bug — exactly the trap the REALLY-equivalent
rule exists to catch, and my own routing table walked into it.
Also fixes a blast-radius bug I introduced with the recursive serializers: marshalFnDefs
emitted a `__marshal.T` fn for EVERY type into EVERY program, so a single marshaller
that failed to typecheck broke fns that never marshal anything (11 of 60 sampled).
Now only marshallers actually reachable from the bridged fns are emitted, closed
transitively (marshalCallsInExpr). That recovers all 10 real losses — 59/60, and the
1 is a fn that compiles in 34s against the test's 25s timeout.
Note the ordering trap for anyone auditing: the 11 losses looked like they came from
un-routing (same commit window). They didn't. Correctness cost zero coverage.
… (+8)
Adds a native `Stdlib.String.toBytes` and routes the `stringToBlob` builtin to it,
then teaches every marshalling site about TBytes so Blob-typed values can actually
cross the seam and be *proven*, not just compiled.
Why it's sound: a compiler String is already stored as UTF-8 bytes behind a length
prefix — which is exactly what `String.length` (the prefix) and `getByteAt` (raw byte
at index) read, as `__string_hash` demonstrates by FNV-1a'ing over that same range. So
toBytes is a byte copy, and matches Encoding.UTF8.GetBytes. Verified on the cases that
discriminate: é=C3A9, 日=E697A5, 😀=F09F9880, plus ASCII and empty — all `match`. Had
the compiler been emitting char codes, é would be [233] vs [195,169] and diffed.
Four sites had to agree, and each was a separate silent failure mode:
- dvalToWire — DBlob(Ephemeral) -> byte values, one per line (same shape as DList).
Persistent resolves through state.blobs (IO) and dvalToWire is pure,
so it stays on the ?unmarshalable marker: unprovable, never guessed.
- marshalTypedSeen — reuse the TList encoder over Bytes.toList rather than writing a
second encoding to keep in sync.
- serializableReason — the provability gate. Without it the fns compiled and reported
`unprovable|TBytes`: coverage with no proof, which is not a win.
- isMarshalableType + unmarshalTyped — widening the return gate made unmarshalTyped's
"unreachable" `| _ -> src` fallthrough REACHABLE, which would hand
compiled code the raw wire String typed as Bytes. Added the decoder
in the same change; the two must move together.
blobToBytes is deliberately NOT routed: it returns List<UInt8> where the native
Bytes.toList returns List<Int64>. Same bytes, different element type — the difference
would be invisible until it wasn't.
Verified: aligned per-hash sweep over all 3900, rows=3900, **0 regressions**, +8
(2088 -> 2096). Both halves measured under the same two-phase regime (chunk 200/600s
then a 25/2400s repair); 75 hashes remain unmeasured on BOTH sides (the known
compile-for-minutes outliers, task #20) and count as False, so this understates rather
than overstates. Of the 8 gains, 7 are proven byte-identical to the interpreter; the
8th (Discord.buildBody) is a bare-`None` inferred as Option<Int64> against an
Option<String> field — the known bare-polymorphic-literal gap (task #16), unmasked
rather than filed under a vague bucket. Worth noting it counts True in the coverage
sweep but cannot be built into a runnable program, so "compiles" overcounts a little.
buildPieces seeds marshaller reachability from the bridged fn BODIES, but equivOne builds its return-marshalling expression afterwards — so any `__marshal.X` that expression calls had no def, and the program died with "no variable named __marshal.T.<hash>". That failure reported as `cf|compile:`, i.e. it looked like the FUNCTION didn't compile, when the function compiles fine (the coverage sweep counts these True) and it was the harness's own wrapper that didn't. So the harness was silently under-reporting what it could prove, in a bucket that pointed at the wrong culprit. Fix: close the marshaller set over the return-marshalling expr too, dropping anything buildPieces already emitted (a duplicate def is itself a compile error). Verified on the 8 fns this branch just unblocked: 5 went `cf|compile: no variable named __marshal.T.4d68…` -> `match`. 7 of 8 now proven byte-identical; the 8th is a real bare-`None` inference gap (task #16), not this.
The equivalence sweep reported Stdlib.Int.toFloat as a DIFF — `c=5.0` vs `i=5` — while
both engines held the identical value. The wire was comparing RENDERINGS: dvalToWire
used F#'s `string f` ("5") against the compiler's Stdlib.Float.toString ("5.0").
The wire is a comparison medium, not Dark semantics. Its only job is
`same value <-> same bytes`, and no rendering does that here:
- F#'s `string f` isn't Dark's float repr at all.
- Dark's own floatToString is G12-LOSSY, so 123456789012345.0 and 123456789012346.0
render identically — a rendering wire cannot see a miscompile it cannot print. It
also appends ".0" to exponent form, emitting the malformed "1e+13.0".
- The compiler's Float.toString builds from intPart/fracPart and disagrees with both.
So floats now travel as their IEEE-754 bit pattern (marshalTyped, WAFloat, dvalToWire,
wireToDval). Exact, total, and NaN/Inf/-0.0 fall out for free. This also fixes the ARG
direction, where a Float handed to a real builtin through the seam previously arrived
rounded to 12 significant digits — and, past Float.toInt's range, as garbage.
Sent as two 32-bit halves ("hi:lo") to route around TWO real codegen bugs in
LibCompiler, both now documented in PROGRESSION-LOG.md and filed as task #22:
1. Unsigned comparisons are SIGNED — MIR.Lt lowers to LIR.LT (setl) with no
operand-type awareness, so UInt64.toString returns a bare "?" for any n >= 2^63,
which is every negative float's bit pattern. Proof: 5.0 (0x4014…) renders; -5.0
(0xC014…) gives "?".
2. `AND r/m64, imm32` sign-extends, so `b &&& 0xFFFFFFFFUL` is a no-op and the compiled
side returned all 64 bits as the low half. Hence `lo = b - ((b >> 32) << 32)`.
Both halves are < 2^32, so they stringify correctly under signed comparison. Neither
bug is fixed here — each is a deep change and neither was blocking; worth doing properly.
Verified: Int.toFloat over 9 values (negatives, 1e13, 15-significant-digit, ±) all
`match`, was DIFF. All 40 Float package fns: 23 match, 0 DIFF (the 16 cf are
pre-existing unsupported-builtin/type blockers). Aligned per-hash sweep over all 3900:
rows=3900, 0 regressions, 0 gains — coverage is untouched, which is what a wire-format
change should do.
The RPC request was `name \n arg1 \n arg2 …` with the args UNESCAPED, and the daemon
recovered them with `request.Split('\n')` followed by `List.truncate (param count)`. So
an arg whose encoding contained a newline arrived as several "args" and everything past
its first line was dropped:
AltJson.format(Json.Null) -> "Null" -> match (nullary = one line)
AltJson.format(Json.Bool true) -> "Bool\ntrue" -> daemon saw "Bool" -> ERR:exn:Invalid Json
AltJson.format(Json.Array […]) -> multi-line -> ERR:exn:Invalid Json
So EVERY non-scalar arg through the seam was mutilated, and it only failed loudly by
luck: wireToDvalTyped rejects a malformed enum. A List arg is the dangerous shape —
"a\nb\nc" truncates to "a" and decodes as a perfectly valid ONE-ELEMENT LIST. Silently
wrong; the Directory.list bug over again, in the arg direction. A String arg containing
a newline had the same flaw.
Fix: escape each arg (Stdlib.hostRpcEscape) before joining, unescape it in the daemon.
Both halves already existed and were applied to container ELEMENTS — just never to the
top-level frame. Unescape is a no-op for text without a backslash or newline, which is
why the hand-built self-test requests still round-trip untouched.
Third instance of one pattern, now written up in PROGRESSION-LOG.md: a wire format needs
the same escaping discipline at EVERY nesting level, and the encoder/decoder must agree
about the cases neither considered. Sampling matters as much as the check — a nullary or
one-element value passes straight through this bug and looks like proof.
Verified: AltJson.format over Null/Bool/String/Number/Array now 5/5 `match`, was 1/5.
All five self-tests pass (bridge 42, marshal /home/dark, daemon 5, handle 1, listhnd 3).
Aligned per-hash sweep over all 3900: rows=3900, 0 regressions, 0 gains — right for a
runtime-protocol change, which should move values and not compile counts.
rtToMarshalable had no TBlob case, so any Blob-taking builtin was unroutable — which is what blocked stringFromBlobWithReplacement, the single largest category in the current histogram at 121 fns. Adds the TBlob arg case plus the daemon-side decode (wire byte values -> Blob.newEphemeral), the inverse of dvalToWire's DBlob. Routing to the REAL builtin is the sound choice here, not a native reimplementation: stringFromBlobWithReplacement is Encoding.UTF8.GetString, which replaces invalid sequences with U+FFFD per maximal subpart. A hand-written decoder would pass on valid input, and the sampler never generates invalid UTF-8 — so it would "prove" correct while being silently wrong on precisely the input the "WithReplacement" in its name is about. This depends on the arg-escaping fix landing first: a Blob's wire is byte values one per line, i.e. exactly the multi-line arg the old protocol truncated. blobToBytes is still NOT routed, deliberately: it returns List<UInt8> where the native Bytes.toList returns List<Int64>. rtToMarshalable has no TUInt8 case, so it stays out. **+9, not +121** — the histogram counts each fn's FIRST blocker only, so those counts are an upper bound, never a prediction. All four sampled ex-stringFromBlobWithReplacement fns now report `unsupported-builtin: altJsonParse_v0` instead: genuinely unblocked, then stopped by the next thing. Written up in PROGRESSION-LOG.md, along with the fact that the old report's "≈300+ from custom-type marshalling" never materialised (altJsonFormat has since vanished from the histogram entirely). Verified: aligned per-hash sweep over all 3900, rows=3900, 0 regressions, +9 (2096 -> 2105). Of the 9: 8 proven byte-identical (base64Encode, base64UrlEncode, digest, Blob.fromString, HttpClient.basicAuth, the three shell-config writers), 0 DIFF, and Blob.concat is `noargs|TList TBlob` — the sampler can't build a List<Blob>, so it's honestly unproven rather than passing.
…ing raw wire unmarshalTyped ended in `| _ -> src`, which hands compiled code the raw wire String typed as whatever the return type claimed. That was sound only while every isMarshalableType case had a matching decoder here — an invariant a comment cannot enforce, and one I broke myself this session: widening the gate for TBytes made that "unreachable" line reachable, and I only caught it by re-reading the comment that said it couldn't happen. So encode the invariant instead of asserting it. unmarshalTypedR returns Result<AST.Expr, string>; an undecodable type is a named blocker (`unsupported-builtin: <name>: unmarshalable-return: <type>`), reported like any other, never a guess. The gate and the decoder can no longer drift silently. This also unblocks the next step architecturally. buildEffectfulMap has to pre-gate returns on isMarshalableType because it is built from the RUNTIME and has no type env — it cannot tell whether a custom type is decodable. Now that the bridge (which does have the defs) fails precisely, that gate can be relaxed for custom-type returns without the failure mode being a silently-wrong value. That's what altJsonParse needs — it returns Result<Json, ParseError>, and it's the blocker sitting behind the Blob work. No behaviour change: isMarshalableType still pre-gates, so the new error path is a safety net, not a live path. Verified exactly that — aligned per-hash sweep over all 3900, rows=3900, 0 regressions AND 0 gains, 2105 both sides. All five self-tests pass, the two that now thread the Result included (marshal /home/dark, listhnd 3). The failwith shim I first reached for is banned in this repo; the two self-test callers handle the Result properly instead, which is better anyway.
The biggest gain of the branch, and it's the payoff for making the decoder total first. Emits one `__unmarshal.<T>(s: String) : T` per non-generic custom type — the exact twin of `__marshal.<T>` — so a recursive type decodes by calling itself instead of generating AST forever (the lesson from the inlined Json serializer that core-dumped the CLI). Records split on "\n" and decode positionally in NAME order; enums split off the first line as the case name and dispatch; tuples mirror the marshal side. Reachable unmarshallers only, transitively closed, for the same reason as the marshal side: one emitted per type broke 11 of 60 sampled fns. buildEffectfulMap no longer pre-gates returns on isMarshalableType. That gate existed only because the decoder used to end in `| _ -> src` — and the map is built from the RUNTIME, with no type env, so it cannot itself tell whether a custom type decodes. With a total decoder the bridge reports a precise blocker instead, so optimism here is safe: the worst case is a named `unsupported-builtin`, not a wrong value. Two bugs found while building it, both from swallowed errors: - No TTuple case, so anything containing a tuple failed — including Json's `Object of List<(String * Json)>`. - unmarshalFnDefsFor drops a failing decoder (`| Error _ -> None`) while the CALL to it was emitted anyway, so the program died with a dangling "no variable named __unmarshal.T.<hash>" — an error naming the symbol and hiding the cause. It cost two debug cycles. Now the call site verifies the def will generate and propagates the real reason, so dangling references are structurally impossible. altJsonParse now reports the truth: `altJsonParse: T.130be4b5(Json): unmarshalable-return: TFloat64` — Json holds a Float, and Float.toBits has no inverse intrinsic (task #23, the next blocker). Verified: aligned per-hash sweep over all 3900, rows=3900, **+129** (2105 -> ~2234) and **0 regressions**. The 12 apparent True->False are all STILL-FAILED, i.e. UNMEASURED: one 25-chunk blew even the 2400s budget, and each of the 12 compiles fine when run individually (String.toBlob among them, which is separately proven to match). Cost noted honestly: unmeasurable outliers rose 75 -> 100, because the decoder makes programs bigger and slower to compile. Differential on a 20-fn sample of the gains: 13 match, 0 miscompiles, 2 DIFF that are harness artifacts, not compiler bugs — Posix.symlink (c=Ok vs i=EEXIST) and Posix.unlink (c=Ok vs i=ENOENT). The compiled run mutates the filesystem and the interpreter then sees what it left behind; each error is exactly what a correct SECOND run returns. The nondet double-run can't catch it because it happens after the compiled run, so both interpreter runs agree. Filed as task #24.
…und-trips (+3)
AltJson.parse compiles and matches the interpreter on all 9 probes, including 3.14 and
[1.5,{"b":[true,null]}] — a recursive JSON value decoded through the seam, byte-identical.
The compile count only moves +3; the capability is the point.
Three things were in the way, each found by unmasking the error rather than guessing:
1. **Float had no inverse.** Stdlib.Float.toBits existed with nothing going the other
way, so a Float could not be RECONSTRUCTED in compiled code — which blocked decoding
any type containing one (Json's `Number of Float`). Turned out to need NO codegen at
all: `__raw_get<Float>` already lowers to RawGet + GpToFp (a movq into an xmm), so
fromBits is store-the-bits / load-at-Float-type, five lines of stdlib. Takes Int64
deliberately — it's a bit PATTERN, the sign label is meaningless, and Int64 keeps
clear of the unsigned-comparison codegen bug (task #22). Task #23 assumed a new
intrinsic; it didn't need one.
2. **An if-chain can't decode an enum.** The ANF pass refused with "If expression
requires lazy branch lowering", and it was right: an If in ATOM position lowers to
IfValue only when BOTH branches are eagerly safe, and these branches call
__unmarshal — eagerly decoding every variant would be wrong, and would never
terminate on a recursive type. Uses Match now (lazy arms), which is why the marshal
side uses Match too.
3. **Decoded sub-expressions sat in atom positions.** A constructor payload, a record
field and a tuple slot are all atom positions, and a decoder body can be an If (the
TList case is `if wire == "" then [] else map …`). That If was fine while it was a
whole fn's return and only became illegal once nested — so `Array of List<Json>` hit
it. Each decoded part is now bound with a Let first, leaving vars in the atom slots.
The enum's own case/rest split dropped its Ifs another way: default indexOf to LENGTH
rather than -1 and the branches vanish, since slice clamps.
Verified: aligned per-hash sweep over all 3900, rows=3900, 0 regressions, +3
(2222 -> 2225). Differential: AltJson.parse 9/9 match (null/true/42/"hi"/[1,2]/{"a":1}/
not json/3.14/nested), covering the Ok and Error branches, the Float path, and recursion.
Cost, stated plainly: compile time keeps climbing as the decoder grows — dead 200-fn
chunks went 600 -> 800 -> 1000 across this work, and unmeasurable outliers sit at 100
(was 75 before the decoder). The repair pass still resolves them, but the trend is real
and task #20 should look at AST size, not GC.
The custom-type decoders got Match + Let-bound payloads last commit; the Option and Result decoders didn't, and they have the same two problems: - An If in ATOM position needs BOTH branches eagerly safe, and the payload body can be an If itself (the TList decoder is `if wire == "" then [] else map …`) — illegal as a constructor arg. This is what "ANF conversion error: If expression requires lazy branch lowering" was, and it had grown into the 6th-biggest blocker at 39 fns (11 of them pre-existing, 28 exposed by the decoder work getting those fns further down the pipe). - An If also decodes the Some payload on the None path, where there is no payload. Match arms are lazy and each payload is now bound to a var first, so atom positions hold plain vars. Same shape as the marshal side. Verified: aligned per-hash diff over the 2900 lines measured on BOTH sides, 0 regressions, +28. Lazy-branch errors 30 -> 3 in the comparable set. Option<String> through the daemon still decodes (marshal self-test -> /home/dark), listhnd 3, and AltJson.parse still matches on 3.14 / nested / error paths. Method note: this diff took ~30s, not the ~35min the last several did. Comparing only the lines MEASURED on both sides is a valid aligned diff — the padded lines are unknown on both sides and are the same ~1000 pathological fns every run. The two-phase repair only ever made the HEADLINE COUNT exact; it never gated regressions, and paying it per commit was pure waste.
…iled (+31) "There is no variable named: Stdlib.__int64_to_bytes" was the 7th-biggest blocker (35 fns) and read like a missing compiler primitive. It wasn't: the intrinsic is registered (LibCompiler/Stdlib.fs:139) and matched (passes/2_AST_to_ANF.fs:291) under its BARE name, while zeroLit called it QUALIFIED — so it resolved to nothing and every Bytes-taking fn failed the compile-check. A harness bug wearing a compiler bug's clothes; the third time on this branch that a generated NAME, not a missing capability, was the wall. zeroLit now calls Stdlib.Bytes.create(0), a real empty blob. The old form also cast 0 into a NULL Bytes pointer, which its "compile-check only, never run" comment was quietly covering for; Bytes.create(0) is safe even if it does run. Then the same fns were `noargs`, and then `skip|arg-literal: value-dval: DBlob` — the sampler couldn't build a Blob and dvalToAst couldn't lower one. Both added: - sampleArg TBlob -> "hé" (68 c3 a9). NON-ASCII on purpose: a pure-ASCII sample cannot distinguish a byte-correct implementation from a char-based one, which is exactly how the String.length / toUppercase routing bugs hid on this branch. - dvalToAst DBlob -> Stdlib.Bytes.fromList([bytes]), the shape marshalTypedSeen uses. Ephemeral only; a Persistent blob is a content hash needing IO, so it stays an Error rather than a guess. Verified: all 31 fns carrying this blocker now compile (31/31 True). Fast regression gate over a 400-fn sample of known-good: 0 regressions, 40s. Differential on 11 of them: 7 match, **0 DIFF**, 4 crash — unmasked rather than bucketed: 2 SIGSEGV and 2 exit-1 (one is a server handler that plausibly wants an environment it hasn't got). The segfaults are not miscompiles (no wrong answer, the binary dies) but are real and now filed as task #26 — running Blob-taking fns is newly possible, so this is the first time anything could see them.
… Blob field) Found a REAL codegen bug and worked around it in the two places that emit a RecordLiteral. Minimal repro (task #26), an Http.Request { url: String; headers: List<String*String>; body: Blob } handed to a fn that just calls responseWithText: hdrs=[] body="" -> match hdrs=[] body="hé" -> match <- blob alone fine, ANY size hdrs=[("a","b")] body="" -> match <- list alone fine hdrs=[("a","b")] body="x" (1 byte) -> match hdrs=[("a","b")] body="xy" (2 bytes) -> crash|139 hdrs=[("a","b")] body="é" (2 bytes) -> crash|139 SIGSEGV iff a record holds a NON-EMPTY List and a >=2-BYTE Blob, both built inline in the literal. It's size, not content: "xy" crashes, "x" doesn't. Neither ingredient faults alone at any size — two heap objects in one record literal, one clobbering the other. Binding each to a Let first fixes it, which is what proved the diagnosis. Ruled out first, since my own Blob work exposed it (each matches): the Bytes.fromList arg literal (Blob.toHex), the Response marshaller (Http.success takes a Blob AND returns a Response), Bytes.fromList itself (String.toBytes "héllo日本", 12 bytes), and the fn body (matches with explicit args in every non-crashing combo). Bytes.fromList's layout is also correct: __raw_alloc(16+len), length at 0, bytes at 8.., refcount at 8+len. The workaround is GATED on exactly that shape, and the gate is the whole story. Hoisting costs TYPE PROPAGATION — a record-field position pushes the field's declared type into the expression, a Let does not, so a hoisted field infers alone and its fresh tvar stops unifying. Measured, twice: hoisting every field regressed Stachu.Parser.many ("expected T.830ffbde<List<a>>, got T.830ffbde<List<t>>"); hoisting every CALL field still regressed Cli.Packages.Deprecate.parseArgs ("expected (String, List<t>), got (String, List<String>)"). That's the fifth instance of this branch's tvar-vs-unification trap. So: hoist only when the record actually has both a List and a Bytes field, and only the call-shaped fields. Every other record compiles exactly as before. This is a WORKAROUND. The codegen bug is still live for anyone else emitting a RecordLiteral, and the strongest lead is recorded in PROGRESSION-LOG + task #26: __writeListHelper writes one byte then RECURSES — len=1 does a single write with no recursion, len>=2 recurses, matching the crash threshold exactly. Look there and at 2.5_RefCountInsertion.fs next. Verified: full known-good gate (1840), 0 regressions — 1640 measured, one 200-fn chunk unmeasured and EXCLUDED rather than padded to False (padding fabricates regressions). Both previously-segfaulting fns now `match`. Also worth noting the 400-fn SAMPLE gate said 0 regressions while the full set found parseArgs: samples are for iterating, the full set is for committing.
Unmasked the `unsupported-value` bucket (105, the 2nd-biggest blocker). It wasn't one
thing — five, and two were just missing cases:
33 unresolved value name
25 value-type: KTBlob
14 value-type: KTUuid
10 value-dval: DApplicable
1 value-dval: DUuid
valueTypeToAst had no KTBlob/KTUuid case, so a package VALUE of a type that params and
returns already handle fine couldn't bridge. Added both to the conventions bridgeType
already set (TBlob -> TBytes, TUuid -> canonical TString), plus dvalToAst's DUuid to match
dvalToWire's `DUuid g -> string g`. Three places now agree per type instead of two.
That exposed the real one: `value-dval: DBlob` for all 25. A package value lives in the DB,
so its blobs are PERSISTENT — a content hash into package_blobs — while dvalToAst can only
lower Ephemeral, because it's pure and resolving a hash is IO. Fix: materializeBlobs walks
a Dval in valueFnDef's existing Ply context (via LibDB.RuntimeTypes.Blob.get) and swaps
Persistent for Ephemeral before lowering, so dvalToAst stays pure.
The same gap was silently corrupting the HARNESS. The differential reported 2 DIFFs:
c=\n\n403 | i=?unmarshalable:DBlob\n\n403
The compiled side was RIGHT; dvalToWire simply couldn't encode a Persistent blob in the
interpreter's result and emitted its marker, which the harness then read as a mismatch.
equivOne now materializes before wiring — both DIFFs are `match`. Applied to BOTH
interpreter runs, or the nondet check would compare unlike things.
**+7, not +40** — the histogram counts each fn's FIRST blocker. 19 of the remaining 33 now
report httpClientRequest_v0, the current #1. The fix landed; those fns just have another
wall behind it.
Verified: full known-good gate (1840/1840 measured), 0 regressions, then a 400 sample after
the equivOne change, 0 regressions. Differential on the value fns: 2 match (were DIFF), 0
miscompiles. Self-tests pass (marshal /home/dark, listhnd 3), recursive JSON still matches,
and the record-literal segv workaround still holds.
…utable (+21)
httpClientRequest was the biggest category in the histogram (164 fns) and the reason was
one missing case:
httpClientRequest(method: String, uri: String, headers: List<(String,String)>, body: Blob)
: Result<ResponseOK, ResponseError>
Every layer already handled tuples — marshalTypedSeen encodes them, wireToDvalTyped
decodes them daemon-side, unmarshalTypedSeen decodes them in compiled code. Only
rtToMarshalable, which decides whether a builtin is routable AT ALL, had no TTuple case,
so `headers` made the whole builtin unroutable. The Blob body and the custom-type Result
return, the parts that looked hard, were already handled by earlier work this session.
After the fix `httpClientRequest` does not appear as a blocker ANYWHERE in those 128 fns
(0 mentions, was every one of them). **+21, not +128** — the histogram counts each fn's
FIRST blocker, and the other 107 hit real type errors behind it (e.g. "Type mismatch in
variable e: expected String, got T.8dc77b20…" — a ParseError landing where a String is
expected). Those are separate problems, now visible.
Verified: full known-good gate, 1840/1840 measured, 0 regressions.
**Differential deliberately NOT run on the gains, and this is a real limitation, not an
oversight.** These fns call httpClientRequest, and routing means the daemon invokes the
REAL builtin — so the harness would fire actual HTTP requests at whatever URL the sampler
invents. That's outward-facing and unauthorized, and a network response isn't
deterministic, so "equivalent" isn't even well-defined for them. Compile coverage is all
that's claimed here.
The TUPLE path itself IS proven, via a safe route: AltJson.parse decodes
`Object of List<(String * Json)>` — a list of tuples across the wire — and matches on
{"a":1}, {"a":1,"b":[true,null]}, and [1.5,{"b":[true,null]}]. dictToList would have been
the obvious test but it stays deliberately unrouted (Dict iteration order differs between
the engines).
The bridge hard-failed `if cond then e` (no else) with "unsupported-if: if without else" — 35 fns. It's exactly `if cond then e else ()`. Verified against the interpreter, not assumed: `let f (b: Bool) : Unit = if b then printLine "x"` returns unit for BOTH b=true (branch runs) and b=false (branch skipped). The then-branch is Unit-typed or the fn wouldn't typecheck, so an implicit unit else is type-correct as well as semantically right. +4, not +35 — the histogram counts each fn's FIRST blocker, and `if without else` no longer appears anywhere in those 35 (0 mentions, was all of them); the other 31 moved on to pmSearch / dateTimeToString / unresolved-value. Verified: full known-good gate (1942/1942 measured), 0 regressions. Differential on the set: 2 match, 0 miscompiles, rest noargs (custom-type params the sampler can't build) — the empirical semantics check above is the stronger guarantee for this one.
…timeouts) equivOne fenced the compiled binary (`CompilerLibrary.execute 0 timeoutMs`) but ran the interpreter as a bare `.Result` — UNBOUNDED — and did so TWICE (the nondet double-run). So one exponential fn stalled a whole differential chunk indefinitely; this was the "79 interpreter timeouts blocking proof" that the priority list has carried for many iterations. Fix: run each interpreter call as `task.Wait(timeoutMs)`. A completed wait decodes as before; a miss reports `itimeout` — deliberately distinct from `ierr` (a real interpreter error) and from a DIFF, so it reads as "couldn't prove in the budget", never a false mismatch. Both runs now go through one `runInterp ()` helper (removes the duplicated block), and a timeout on EITHER run short-circuits to `itimeout`. Verified: full differential over 40 known-good fns completes in 9.9s (was: a single slow fn could hang the run forever) — 20 match, 0 DIFF. Fast path intact: JSON and fib(10) still `match`, no false `itimeout` on fns that finish in budget. Touches only equivOne (the harness), so compile coverage is unaffected by construction; SAMPLE=400 gate confirms 0 regressions. HONEST CAVEAT: .NET has no interpreter cancellation, so `Wait` frees the HARNESS thread but the timed-out Task keeps running in the background until the process exits — it burns a core until then. That's still strictly better than the old bare `.Result`, which blocked the harness thread forever, and in a sweep the process is short-lived and killed at the end (plus the sweep's own per-fn `timeout` + 6GB watchdog bound it). A real fix needs a cancellation token threaded through Execution.executeFunction; filed as follow-up. I did NOT catch a live fn hitting `itimeout` in these samples (none was slow enough at a 10s bound), so that verdict path is proven by construction (Task.Wait(ms):bool) rather than by a captured case.
…ry (task #24) equivOne ran the compiled binary first, then the interpreter twice for the nondet check. For a STATE-MUTATING fn that order defeats the check: Posix.symlink run by the binary creates the link, then both interpreter passes see the post-state (EEXIST) and AGREE, so nondet misses it and the harness reports a false DIFF (c=Ok vs i=Error 17 "File exists"). Same for Posix.unlink (ENOENT). Fix: run the two interpreter passes first, decide nondet, and only then run the binary. symlink now gives Ok then EEXIST across the two interpreter runs -> they DISAGREE -> `nondet` -> honestly skipped, and the binary never runs to muddy the filesystem. A pure fn's two runs still agree, so the provable set is unaffected. Verified: Posix.symlink and Posix.unlink now report `nondet` (were false DIFF); pure fns (JSON) still `match`. Harness-only change, so compile coverage is unaffected by construction — SAMPLE=400 gate confirms 0 regressions. The one DIFF in the 40-fn differential (SemanticTokensOptionsRange.toJson, c=Object vs i=Bool) is PRE-EXISTING — it reproduces with this change stashed at HEAD, so the reorder introduced it neither. That one is a separate real finding, investigated next.
…lookups by type FIRST confirmed miscompile of the branch (task #28), a silent wrong-answer: SemanticTokensOptionsRange.toJson given `Bool true` returned `Json.Object []` compiled vs `Json.Bool true` interpreted — it took the EmptyObject match arm. `Bool` is the variant name, and it collides with the native Bool type and Json.Bool. Root cause: TWO sites resolved a variant to its TAG with a bare `Map.tryFind variantName variantLookup`, which returns whichever type won the name collision — and that type's tag index: - CONSTRUCTION (2_AST_to_ANF ~8163): `AST.Constructor (_, variantName, _)` DISCARDED the AST's own type name and looked up bare, so `SemanticTokensOptionsRange.Bool` was built with Json.Bool's tag. - MATCH tag-compare (~5822, buildPatternComparison): emitted `tag == N` with N from the bare lookup, so the arm's tag constant was wrong too. Both now use `TypeChecking.tryFindVariant` scoped by the constructor's / scrutinee's type name (falls back to bare when unscoped). This is the same family as the earlier scoped-key fix (02ba43a) which covered other readers but missed these two. This is exactly why the mandate is "compile coverage is NOT correctness": the miscompile was always there; only a good-enough proof harness (bounded interpreter #15, reordered nondet #24) could surface it. Verified: full known-good gate, 1946/1946 measured, 0 compile regressions (this is a hot path — every enum construction and match). 20-fn differential: 0 DIFF (no wrong answers introduced). HONEST FOLLOW-UP: the repro fn now returns `crash|1` instead of the wrong answer — the silent miscompile is eliminated (a loud crash beats a wrong result), but once the tag is correct the fn hits a SEPARATE failure (suspect the task #26 tuple bug in its Json.Object arm, or Json.Bool result marshalling). Kept task #28 open for that; it's no longer a silent-corruption bug.
The branch's one hard codegen bug. `HeapStore(addr, offset, StringSymbol)`
builds the heap string inline using RCX as its length/byte/refcount temp, but
RCX is X3 — an allocatable caller-saved register. The else-branch never saved
it, and the addrReg=scratch sub-case silently popped the address into RCX,
destroying whatever live value was there.
Tuples store fields in ascending offset order, so `("a", Some 1)` stored the
string at offset 0 first (clobbering RCX), then stored the Some-pointer at
offset 8 from the now-garbage RCX -> a garbage heap pointer that SIGSEGVs when
later dereferenced. That is exactly the tuple-second-element crash: it needed a
string first (real inline build touches RCX), a heap-pointer second (only a
corrupted pointer faults; a corrupted int doesn't), and enough register
pressure (2+ list elements) to land that pointer in RCX.
The truth table it now satisfies, all seam-free:
(String, Option) 2nd -> 3 (was exit 139)
(String, nested-tup) 2nd -> 3 (was exit 139)
(String, String) 2nd -> xy (offset-8 is also a literal, never regressed)
(Option, Option) 2nd -> 17 (no string store to clobber RCX)
(Int64, Option) 2nd -> 3 (int at offset 0 is an Imm store, safe)
Fix: preserve RCX across all three address cases (in-RCX, in-scratch, other).
Mirrors the discipline the RawSet/RawGet paths already follow.
Not a register-allocation bug — the prior "documented-Open upstream" attribution
was wrong. Post-regalloc LIR of the crash and working variants is byte-identical
but for the field offset; the corruption is in HeapStore lowering, upstream of
allocation. No allocator or finger-tree change needed.
Verify: #26 repro crash -> correct on 5 tuple shapes; fastcheck 390/390, 0
compile regressions; differential proof sweep over a 487-fn known-good sample —
the only DIFF + crash are pre-existing (identical on the stashed pre-fix binary),
so 0 new miscompiles.
Claude-Session: https://claude.ai/code/session_015dcGWPp734R2y8UP3Qtva1
Integer comparisons and division ignored operand signedness: MIR->LIR emitted signed condition codes (setl/setg via LIR.LT/GT/LE/GE) and signed IDIV (Sdiv) for every integer type, so UInt* operands >= 2^63 compared as negative and unsigned division ran IDIV. Symptom in the wild: UInt64.toString emitted a bare "?" for large values (the digit-extraction loop compares against 10 and read the value as negative). The signedness (operandType: AST.Type) was already in scope at the lowering sites. Fix: - LIR: add unsigned conditions ULT/UGT/ULE/UGE and a Udiv instruction. - 4_MIR_to_LIR: select unsigned condition / Udiv / unsigned-modulo (Udiv+Msub, no toward-negative-infinity sign fixup) when isUnsignedIntType operandType. - x64/6_CodeGen: ULT/UGT/ULE/UGE -> setb/seta/setbe/setae (Cset) and b/a/be/ae (CondBranch); Udiv mirrors Sdiv but zero-extends via `xor rdx,rdx` instead of CQO, uses DIV not IDIV, and drops the INT64_MIN/-1 overflow guard. - 5_RegisterAllocation: Udiv threaded through getUsedVRegs / getDefinedVReg / spill-reload (the first two have a catch-all that would silently miscompile a missed div, so this is load-bearing, not cosmetic). - Peephole (LICM purity) + IRPrinter: Udiv parity with Sdiv. - arm64/6_CodeGen: Udiv wired to ARM64 UDIV; unsigned conditions map to signed as a stopgap (ARM64.Condition has no LO/HI/LS/HS) — ARM64 is not the compiled/tested backend, marked TODO(#22). x64 is correct. Verified: UInt64 >/</>=/<= and //% on typed variables now match the interpreter across the 2^63 boundary; signed Int compare/div/mod unchanged (spot-checked both directions + euclidean mod); the previously-DIFFing UInt64 fn 5afb269d now matches; differential over 194 known-good fns still 194/194, 0 DIFF. Known residual (separate, narrow): a UInt64 *literal* compared against another literal is constant-folded at compile time (2.3_ANF_Optimize) using signed F# ops, and the compiler-dialect literal path tags large UL literals as Int64. This only bites literal-vs-literal folding (typed variables are correct); left as a follow-up since it's an upstream literal-typing issue, not the LIR lowering. Claude-Session: https://claude.ai/code/session_015dcGWPp734R2y8UP3Qtva1
A 2-arg float call whose arguments need a cyclic shuffle in the ABI registers computed the wrong result. The x64 FArgMoves lowering emitted the parallel moves naively in sequence, so a swap FArgMoves(D0<-D1, D1<-D0) became `movsd D0,D1; movsd D1,D0` — the second move reads the already-overwritten D0, so BOTH registers end up holding the old D1. `multiply(x, sqrt 4.0)` computed x*x; the shipping fn `turnsToRadians = Float.multiply(Math.tau, angleInTurns)` computed tau*tau (39.478) instead of tau*2.5 (15.708) — the differential DIFF 512efce2. ARM64 already resolved this correctly via ParallelMoves.resolve + a reserved temp (D16); x64 never did. Fix: lower x64 FArgMoves through the same ParallelMoves.resolve and break cycles through a reserved float scratch. XMM15 (D15) is removed from the allocatable/callee-saved set to serve as that scratch (analogous to the integer R11 and ARM64's D16). Cost: 15 allocatable XMMs instead of 16. Seam-free truth table, all now correct (were wrong): multiply (sqrt 9) (sqrt 4) -> 6 (was 9 = arg0^2) multiply x (sqrt 4) @x=2.5 -> 5 (was 6.25 = x^2) multiply (sqrt 4) x -> 5 (was already ok — no cycle) multiply x y (two params) -> 7.5 (ok) Verify: truth table correct; 512efce2 now matches the interpreter; differential over 194 known-good fns still 194/194, 0 DIFF. Claude-Session: https://claude.ai/code/session_015dcGWPp734R2y8UP3Qtva1
…he seam
rtToMarshalable — the gate deciding whether a builtin is routable — had no case
for the sized integer types, so any builtin taking an Int8/16/32 or UInt* arg was
silently unroutable (e.g. intFromUInt64, uint64ToFloat). Both wire directions for
these already existed: the compiled side encodes via Stdlib.<T>.toString
(marshalTyped) and the daemon decodes with .NET's full-range parse (wireToDval),
so UInt64 round-trips as a decimal string — not the Int64 wire that would overflow
>= 2^63. Only the gate was missing.
Safe by construction: rtToMarshalable also gates returns, but unmarshalTyped ends
in `| other -> Error "unmarshalable-return: {other}"`, so a UInt/narrow-Int RETURN
yields a clean blocker, never a silent raw-string value. So the only fns that
newly compile are those whose sized-int types are all in ARG position with an
already-decodable return — and those args round-trip correctly.
Verify: +5 compile on a 385-fn blocked sample (~15 tree-wide); the provable one
(763b1d43, a UInt-arg fn) matches the interpreter; differential over 194
known-good fns still 194/194, 0 DIFF. Sized-int RETURNS still need unmarshalTyped
cases + a UInt64-safe parser (task #31).
Claude-Session: https://claude.ai/code/session_015dcGWPp734R2y8UP3Qtva1
sampleArgDeep (the differential harness's arg synthesizer) ignored a generic
custom type's type ARGS: it read `Option<'a>`'s definition and sampled `'a` as
the fallback Int64, so a param typed `Option<String>` got `Some(42)` and the
whole call failed to type-check. That's ~a fifth of the known-good set stuck in
`cf` (compiled fine, unprovable) purely because the harness couldn't build a
valid input.
Fix: substituteType binds each custom type's declared params to its actual type
args before descending, so `Option<String>` samples `Some("hello")`. Depth- and
node-budget-bounded (maxSampleDepth/sampleNodeBudget) so wide nested records don't
build an arg that makes the proof crawl.
On a 389-fn sample this collapses `cf` ~77 -> ~22 and pushes proven matches up
accordingly. It also surfaces 2 real miscompiles that were never exercisable
before (task #32: first numeric field of a JSON-serialized record compiles to
garbage float bits) — which is the point: more of the tree becomes provable, and
the bugs it finds were always there.
Not free: fns whose interpreter execution is genuinely slow now hit the per-fn
timeout as harness-drop instead of failing fast at arg-synth. The sweep's per-fn
retry isolates them so they don't hang the run, but a real fix wants interpreter
cancellation (task #27).
Claude-Session: https://claude.ai/code/session_015dcGWPp734R2y8UP3Qtva1
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
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.
(very WIP, dunno if this will go anywhere)
Vendored
darklang/compiler(the x64 AOT compiler) intodarklang/darkas a build-gated project andwired up a
dark compile <fn>path: resolve a package fn, bridge it into the compiler's AST, compile tonative ELF, run it, diff the bytes against the interpreter. All behind
-p:DarkWithCompiler=true/#if DARK_WITH_COMPILER— flag off and the.sln/default build are byte-identical, so this can't breakanyone. The question: fold the compiler in-tree, point it at real package fns, and see how far it gets +
what has to sit between the two codebases.
Where it landed: ~59% of package fns compile to native ELF (floor), and of those ~61% prove
byte-identical to the interpreter, 0 known miscompiles (also a floor — the harness can't synth args for
a big chunk of them, see below).
dark compile <fn>works but it's still builtin-shaped, not a nicecommand yet.
What it looks like
Still builtin-shaped (
dark eval 'Builtin.compiler…'), but this is the whole loop — bridge, compile tonative ELF, run it, diff against the interpreter:
Two runtimes + the glue
dark(ProgramTypes, real F# builtins, package mgr, live ExecutionState) and the compiler (its ownAST -> ANF -> MIR -> LIR -> x64, its own
.darkstdlib, finger-tree lists, regalloc — knows nothing aboutour builtins or package store). Three bits of glue:
Builtins.Compiler/Bridge.fs, ~2300 loc) — total, hard-failing lowering of a fn +its whole type/call closure, in-process, no text hop. Anything unbridgeable ->
unsupported-<cat>,which is the only reason the blocker histogram is trustworthy.
hostRpc("Stdlib.String.length\n args")and an in-process F# daemon runs the real builtin against a real ExecutionState and marshalsback. One boundary, per-builtin table, swap to native later with no ABI change. Costs an IPC hop per
builtin call (real tax on builtin-heavy code; native migration kills it).
wire bytes. Compile != correct; every number here is diffed, not assumed.
Compiles fine
Basically the whole surface: arith + all int widths, strings, records/enums (construct/access/match),
generics (monomorphized), lists, tuples, record-update, string interp, pipes, lambdas/HOFs, recursion,
package-value constants, aliases. Real code — JSON serializers, LSP types, render helpers — mostly goes
straight through.
Doesn't
Long-tail plateau, no single wall: generic/alias custom types, bare-
[]inference (the naive fix hangsthe compiler), effectful builtins (route through the seam fine but can't be cleanly proven — IO/nondet),
and a pile of upstream-unresolved names the stored PT itself can't resolve. And the harness is its own
ceiling: ~a third of compiling fns are "unprovable" — not wrong, just can't synth valid args for
custom-type/fn params. Fixing arg-synth (bind generic tyargs, sample nested records with bounds) converts
most of those to proven — and immediately outed 2 more real miscompiles nobody had ever exercised. That
fix is written but not committed: it also shows the interpreter can't be interrupted, so a slow fn hangs
the whole sweep (wants a cancellation token first).
What had to change in each repo
darklang/compiler(~369 loc, 9 files — needs upstreaming). The fun part: most of the "hard" bugs inits own notes were mischaracterized. The real ones were small register bugs, found by diffing the
post-regalloc LIR of a wrong minimal case vs a right one:
passes/x64/6_CodeGen.fs: (a)HeapStoreof a string literal clobberedRCX— an allocatable reg —smashing the adjacent tuple slot -> the tuple/list SIGSEGV the notes blamed on "unfixable register
allocation" this whole time; (b) unsigned compare/div/mod lowered signed (UInt64 >= 2^63 read
negative); (c)
FArgMovesskipped parallel-move resolution, so a cyclic float shuffle likef(x, g())quietly computed
f(x, x). PlusFile.deletewas a no-op stub -> realunlink.passes/2_AST_to_ANF.fs: variant-tag lookup scoped by type (latent wrong-tag miscompile); lambda-liftinference leniency.
passes/1.5_TypeChecking.fs: tvar unification instead of structural eq in Apply/FuncRef — it wasrejecting correct code anywhere one side still held a tvar (bit us ~6x).
Float.fromBits,String.toBytes,Rpc.darkseam prims; reserved XMM15 as a float scratch forthe FArgMoves fix.
darklang/dark— basically all additive and flagged. Bridge + seam (Builtins.Compiler, ~2300 loc)is new; the compiler is vendored as a gated project; one guarded combine entry is the only shared-wiring
touch. Flag off -> default build unchanged.
Takeaways + next
Biggest lesson: most of the wins came from disproving the compiler's own notes or fixing my harness, not
from compiler limits. The structural-eq trap bit 6x; two of three "walls" in the notes were stale
comments; the headline "unfixable register bug" was a one-line RCX save.
To make it actually real:
Execution.executeFunction) is the keystone — unblocks thearg-synth proof-coverage jump and makes full-tree sweeps robust. It's the one thing that reaches into
the non-gated interpreter, so it wants care.
.so) is the live call if we pivot; wire formatis checked only via package-fn diffs — which is exactly how those three register miscompiles survived in
darklang/compilerin the first place.Not shippable, but the shape's clear and the correctness bar is real. Ping me for the LIR-diff trick —
it's the thing that made the codegen bugs tractable.