Skip to content

refactor(pi): extract slash/explicit command parsing (Unit 2) - #6

Merged
srdjan merged 27 commits into
mainfrom
unit-2-extract-commands
Apr 19, 2026
Merged

refactor(pi): extract slash/explicit command parsing (Unit 2)#6
srdjan merged 27 commits into
mainfrom
unit-2-extract-commands

Conversation

@srdjan

@srdjan srdjan commented Apr 19, 2026

Copy link
Copy Markdown
Owner

Summary

  • Extract slash and explicit command parsing from packages/pi/src/repl.zig into a new packages/pi/src/commands.zig module.
  • Single command_table now drives both forms (/meta, /features, /modules, /rule, /search, /verify, /check, /build, /test and zigts meta|features|modules|search|describe-rule|verify-paths|verify-modules|check ...). zig build <step> / zig build test* stays as a short special case next to lookup.
  • isQuit / isHelp move with the parsing; repl.zig keeps dispatchLine, shouldDispatchTool, DispatchOutcome, Registry, run unchanged so tui/app.zig and app.zig callers and tests need no edits.
  • Adds focused tests in commands.zig covering slash lookup, explicit lookup, unknown command, zig build test-zigts routing, trailing args, and quit/help aliases.

This is Unit 2 of the parallel refactor plan at
/Users/srdjans/.claude/plans/study-the-plan-provided-clever-wadler.md.

Test plan

  • zig build test-expert-app passes
  • zig build succeeds
  • printf "help\nquit\n" | ./zig-out/bin/zigts expert shows /verify and Registered tools:
  • printf "/meta\nquit\n" | ./zig-out/bin/zigts expert returns "compiler_version" JSON
  • printf "zigts meta\nquit\n" | ./zig-out/bin/zigts expert returns "policy_version" JSON

Generated with Claude Code.

srdjan and others added 27 commits April 19, 2026 09:57
Closes out the W3 vocabulary: every JS dispatch (onOpen, onMessage,
onClose) transitions the connection through live -> parked, and a
new scanIdle(threshold_ms, now_ms) sweep transitions long-parked
connections to dormant while returning the crossed-over ids. live
connections are never swept (a handler blocked mid-dispatch is a
handler bug, not a hibernation case); already-dormant connections
aren't re-reported.

What this closes:
- the ConnectionState enum is now actually used (previously set to
  .parked on every frame, never distinguished from .live)
- the scanIdle hook gives an evented-loop successor a clean point to
  deregister dormant fds' read side without hunting the pool itself

What this doesn't close:
- per-connection thread cost. ws_frame_loop is still thread-per-
  connection, so "dormant" today is an observational label rather
  than a resource-savings win. The real thread release needs a
  shared evented-I/O replacement for ws_frame_loop.run plus a timer
  that drives scanIdle periodically. That's a separate, larger
  refactor — flagged as a future optimization once measured pressure
  justifies it.

What was already true before this commit:
- runtime is released between messages (handler pool lease only held
  during dispatch), so "dormant holds no runtime" is already the
  case for every parked connection
- setAutoResponse (W3-a) short-circuits matching frames without
  waking JS
- ping/pong are answered by the codec, never dispatched to JS

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds two module-level WebSocket consistency rules surfaced through
the existing rule-registry + expert tooling pipeline:

  ZTS320 websocket_import_without_events (warning): handler imports
    zigttp:websocket but doesn't export onMessage. The module surface
    is useless without at least one event handler.

  ZTS321 websocket_events_without_import (error): handler exports
    onOpen/onMessage/onClose/onError but doesn't import
    zigttp:websocket. The exports would be dispatched but
    send/close/etc. would be unreachable.

The checker (packages/zigts/src/ws_consistency.zig) is a pure
function over a small Inputs struct, trivially testable without
standing up the full contract-builder pipeline. Seven unit tests
cover every combination of imports_websocket_module x
exports_on_(open|message|close|error).

ContractBuilder.build() calls the check after its existing scans
and logs findings to stderr during every contract build, so
zig build -Dhandler=x.ts and `zigttp compile` both surface them.
zigts describe-rule / zigts search / zigts meta all see the new
entries.

Golden fixtures (meta, verify_paths_clean, verify_paths_missing)
and policy-hash.txt refreshed to match the two added rules
(policy hash 9ede01bd... -> 422ab281...; rule count 25 -> 27).

Deferred for a follow-up slice:
- Durable-fetch misuse (ZTSF00x): needs call-site AST walking of
  fetch(...) invocations to inspect the durable option object.
  The rule-registry entries and runtime-side validation (which
  already rejects malformed durable options at call time) are in
  place; compile-time diagnostics are the remaining piece.
- Separate ZTSW/ZTSF prefix categories: current rules live in the
  ZTS3xx verifier range to reuse existing infrastructure. A split
  requires extending RuleCategory and the policy hasher.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…e D)

Documents zigttp:websocket and zigttp:fetch as first-class virtual
modules with full API references, runtime flags, and not-yet
sections that enumerate the deliberately deferred pieces
(thread-cost hibernation, durable-fetch compile diagnostics, etc).

New examples:
- examples/websocket/chat.ts: named-peer broadcast handler using
  serializeAttachment for display names and getWebSockets(room) for
  fan-out. Smoke-tested end-to-end.
- examples/fetch/webhook.ts: idempotency-keyed POST dispatcher with
  retry + exponential backoff, annotated with the SIGKILL-restart
  replay protocol.

Both examples compile clean against the current ruleset (no ZTS3xx
diagnostics, policy hash unchanged).

Extends the AWS deploy manifest's Metadata.zigttp block with two
optional sub-keys:
- `websocket`: { onOpen, onMessage, onClose, onError } emitted when
  the contract has any WS event export. Deploy consumers that need
  a different binding (Cloudflare Durable Objects, Azure WebPubSub)
  branch on this instead of re-parsing the contract.
- `fetchHosts`: the egress host list scoped to handlers that import
  zigttp:fetch, so targets can configure a narrower allow-list
  than the full egress set.

Both blocks are omitted entirely when the underlying facts are
empty, keeping existing-handler manifests byte-identical. Three
new renderAws tests cover present/absent for each block.

A full Cloudflare DO target remains a separate plan — the metadata
hook gives downstream tooling what it needs to emit one without
forcing the zigttp core to carry CF-specific rendering.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Fresh-eyes cleanup on the recently added WebSocket runtime:
removed unused FrameEvent union and max_room_peers constant, inlined a
one-line unixMillisNow wrapper, renamed Pool.unlockLock to unlock, and
replaced hand-rolled asciiEqlCaseInsensitive and toUpper/toLower with
their std.ascii counterparts used elsewhere in the codebase.

Pure behavior-preserving; zig build test reports 997 + 146 passing,
same as baseline.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Restructure the 22 virtual modules into six domain subfolders under
packages/zigts/src/modules/, packages/zigts/module-specs/, and
docs/virtual-modules/: security, data, net, http, workflow, platform.
Infrastructure files (resolver, compiler, file_resolver, module_graph,
util, types, root) stay at the modules/ top level.

Also adds dedicated doc pages for the 18 previously-undocumented
modules plus a virtual-modules README that serves as the landing page
and effect-classification reference.

builtin_modules.zig is the single source of truth: all 22 imports and
governance entries updated with the new paths; a build-time assertion
already guards specifier/entry drift. No handler-facing API change -
specifiers are unchanged, only internal paths moved. README's virtual
module table now links each row to its page; the duplicated effect
classification paragraph is replaced by a link to the docs/README.

zig build test reports 1503/1507 passing (4 skipped), identical to the
pre-reorg baseline. Doc link audit: 23 pages, zero broken relative
links. git mv preserves blame history for every moved file.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Align the code layout with docs/virtual-modules/: its top-level has
only the six group folders plus a README index, while the code top
level was cluttered with six infra files (resolver, compiler, util,
types, file_resolver, module_graph) sitting next to the group
folders. Moving those into packages/zigts/src/modules/internal/ leaves
only root.zig and the six group subfolders at the code top level,
matching the docs shape.

No behavior change: ~38 import paths updated (31 infra refs inside
22 virtual-module files, 6 in modules/root.zig, 10 external callers
in module_binding/trace/http/file_io/module_audit), plus the six
moved files themselves bump their ../X.zig refs to ../../X.zig. Git
mv preserves blame on every moved file.

zig build test --summary all: 1503/1507 passing, 4 skipped, identical
to the pre-move baseline.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds websocket capability, expanded ContractCategory variants
(scope_name, cookie_name, cors_origin, rate_limit_key, service_call,
fetch_host), sets_scope_used flag, Law/LawKind/AbsorbingPattern, and
ModuleBinding.self_managed_io to zigttp-sdk so the SDK now covers
every field zigts module_binding.zig carries.

Accepts both zigttp: and zigttp-ext: specifier prefixes in
validateBindings; adapter still enforces zigttp-ext: for extensions.

Phase 0-1 (step 1) of the peer-package move in
docs/virtual-modules-peer-package.md. Plan and SDK inventory doc
checked in alongside.
Adds extractString/extractInt/extractFloat, createString/createObject,
objectSet/objectGet, throwError, resultOk/resultErr/resultErrValue/
resultErrs to zigttp-sdk. Each wraps an extern fn whose zigts-side
impl lives next to the existing capability exports in
module_binding.zig. JSValue crosses the ABI as u64 since both
packages verify the packed-struct layout is bit-identical.

Module state (getModuleState/setModuleState) is deferred to a later
commit because the deinit callback's std.mem.Allocator parameter is
not C-ABI stable. Stateless modules (11 of 22) can port without it.

Phase 1 step 2 of the peer-package move.
Creates the empty zigttp-modules package that will host the 22
built-in virtual modules after Phase 3-7 ports. Depends only on
zigttp-sdk; builds as a standalone module with its own test step.

Ports internal/util.zig to use SDK handle ops: extractString,
createString, createObject, objectSet/Get, result builders,
throwError/TypeError/CapabilityPolicyError. Modules written against
this util can compile against zigttp-sdk alone, no zigts internals.

Registered as dependency in root build.zig.zon but not yet imported
into any binary; zigts continues to source modules from
packages/zigts/src/modules/ until Phase 8 wire-up.

Phase 2 of the peer-package move.
Moves the canonical implementation of zigttp:crypto into
packages/modules/src/security/crypto.zig, depending only on
zigttp-sdk. The zigts-side modules/security/crypto.zig becomes a
two-line adapter that wraps the SDK binding via
adapter.adaptModuleBinding. Phase 8 will delete the stub and wire
builtin_modules.zig directly against zigttp-modules.

SDK additions needed by this port:
- getAllocator(handle) — borrow the runtime allocator
- sha256(handle, data, out) + hmacSha256(handle, data, key, out) —
  capability-gated crypto wrappers so modules can avoid direct
  std.crypto calls forbidden by module-audit ZVM001

Also relaxes adapter.adaptModuleBinding to accept zigttp: builtin
specifiers (previously only zigttp-ext:). The zigts dependency
graph gains zigttp-modules; root build.zig wires it into the
zigts-tests module too.

governance update: builtin_governance_entries crypto module_path
points to packages/modules/src/security/crypto.zig so verify-modules
reads the canonical source.

Phase 3 wave 1 of the peer-package move (crypto only; auth,
validate, decode still to port).
Applied /simplify findings from three parallel reviews:

- Delete 12 no-value pub const re-exports in
  packages/modules/src/internal/util.zig; crypto.zig calls sdk.*
  directly. Dropped the dead no-op test.
- Cross JSValue directly across the extern ABI instead of u64. Both
  packages verify layout equivalence, so the .raw bookkeeping is
  ceremony; simpler signatures, same machine code.
- Drop unused handle parameter from zigttpSdkSha256/HmacSha256. The
  capability check lives inside sha256ForActiveModule, which reads
  the active-module threadlocal, not the handle.
- Drop the now-redundant requireCapability hop in sdk.sha256 and
  sdk.hmacSha256 wrappers. The zigts-side *ForActiveModule already
  enforces the check; double enforcement was one extern call per
  crypto op.
- getAllocator returns *const std.mem.Allocator directly instead of
  *anyopaque + @ptrCast/@constcast dance.
- Collapse six near-identical ordinal-check if-blocks in
  module_binding_adapter.zig into a single assertOrdinal helper.
- Strip commit-referencing rot ("Phase 8 will delete…") and
  narrating block comments. The design doc is the source of truth.

Tests stay at 1503/1507.
Moves zigttp:auth into packages/modules/src/security/auth.zig.
Zigts-side stub delegates via adapter.adaptModuleBinding.

SDK gained one new helper: parseJson(handle, json) which wraps
builtins/json.zig's parseJsonValue. Everything else auth needs
(hmacSha256, getAllocator, extractString/Float, createString,
objectGet for exp/nbf claim lookup, nowMs, resultOk/Err) is
already in the SDK from prior commits.

Coverage gap: 9 unit tests from the original auth.zig (base64url
roundtrip, pure byte-compare tests) don't migrate yet — the modules
package cannot link zigts exports standalone, so its test root
fails to resolve zigttpSdk* symbols. Proper fix requires the SDK
test-harness planned for Phase 1 follow-up. Tests exercised std
behavior and are covered indirectly by integration.

Phase 3 wave 1 (auth). validate + decode still to go.
Completes Phase 3 of the peer-package move. Both modules now live
in packages/modules/src/security/; zigts-side files reduced to
two-line adapter stubs.

SDK additions needed:
- isString/isObject/isArray/arrayLength/arrayGet/arraySet/
  createArray/stringify as extern-backed helpers
- isNull/isUndefined/isTrue/isNullish/isNumber as inline JSValue
  methods (bit-pattern checks, no extern)
- getModuleState/setModuleState with SdkStateEnvelope wrapper on
  the zigts side. SDK callback uses `callconv(.c)` with just the
  state pointer; zigts stores the SDK deinit in an envelope and
  registers a static internal deinit_fn that invokes it. Works
  around std.mem.Allocator not being C-ABI stable.
- parseJson(handle, json) wrapping builtins/json.zig parseJsonValue

SchemaRegistry is now allocated from sdk.getAllocator(handle) and
stored via sdk.setModuleState; its deinit is a `callconv(.c)`
function that frees the registry through its stored allocator.

decode.decodeJson/decodeObject become module-to-module API in the
package, called directly from decode.zig via `@import("validate.zig")`.

Coverage: 21 unit tests from validate + decode don't migrate since
the modules package cannot link zigts exports standalone (test
discovery boundary across the Zig module graph). Same follow-up as
the auth port — the SDK test-harness needs to come before Phase 8.

Tests: 1473/1477 (was 1494 before this commit, 1503 at session
baseline; net -30 tests, all from module-package test discovery).
Phase 4 of the peer-package move. All five modules now live in
packages/modules/src/platform/; zigts-side files reduced to two-line
adapter stubs.

SDK additions needed:
- readEnv(handle, name) — capability-gated env var read (wraps
  zigts readEnvChecked)
- allowsEnv(handle, name) — policy-check gate, used by env before
  reading
- objectKeys(handle, obj) — enumerate own keys as a JS array; log
  module iterates context-object properties for NDJSON output
- isFalse on JSValue (inline, bit-pattern)

Updated the "governance entries stay aligned" test in
builtin_modules.zig to assert the new env module_path. 30 pure
tests in the ported files don't run yet (same modules-package test
discovery gap as Phase 3).

Tests: 1455/1459 green (33/35 build steps, all OK).
Phase 5 of the peer-package move. All three http modules now live
in packages/modules/src/http/; zigts-side files reduced to two-line
adapter stubs.

No new SDK surface was required - existing handle ops (objectGet,
objectKeys, arrayLength, arrayGet, extractString/Float, createObject,
objectSet, createString, isObject/isTrue/isFalse) covered every
zigts-internal call the three modules made.

The router's object-key iteration uses sdk.objectKeys → JS array,
trading two extern-fn hops per iteration for ABI-stability. Cost
is a single-digit-ns per route-table entry; negligible for the
typical ≤ dozen routes in a handler.

Tests: 1441/1445. 14 pure unit tests in the ported files don't run
under test-zigts yet (known modules-package test discovery gap).
The pi loop tests called std.testing.tmpDir(.{}) (which creates
.zig-cache/tmp/<sub_path>/) but then passed only tmp.sub_path (the 16-char
random component) as workspace_root. std.fs.path.resolve joined that
against CWD, so every test write landed in <repo>/<sub_path>/ instead of
the tmp dir. tmp.cleanup() only deleted the .zig-cache/tmp side, leaving
one stray repo-root folder per test run.

Compose the full relative path via a tmpWorkspacePath helper so writes
land inside the real tmp dir. Also update the .gitignore glob comment to
reference the fix; the glob stays as defense-in-depth.
Phase 6 (data group), first two modules. Both are stateful with per-
runtime stores owned through setModuleState/sdkDeinit. ratelimit uses
the clock capability; cache additionally uses policy_check to gate the
namespace through the capability policy.

Added to the SDK:
- numberFromF64 helper that folds safe integers into the int32 tagged
  form, matching the runtime's allocFloat hot path.
- allowsCacheNamespace wired through a new zigttpSdkAllowsCacheNamespace
  extern; the zigts-side implementation delegates to
  allowsCacheNamespaceChecked.

sql stays in packages/zigts/src/modules/data/ for now; it needs a
larger SDK surface for prepare/step/bind/columns and will land in a
follow-up commit.
Completes Phase 6 (data group). The SQL module now lives in
packages/modules/src/data/sql.zig and talks to SQLite through a new
SDK surface. Thirteen extern fns cover what sql.zig needs:
open/close/errmsg/changes/lastInsertRowId for the db, and
prepare/finalize/step/readonly/stmt_errmsg/param_count/param_name/
bind_null/bind_int64/bind_double/bind_text/column_count/column_name/
column_type/column_int64/column_double/column_text for statements.

Opaque SqliteDb and SqliteStmt handles are the raw *c.sqlite3 and
*c.sqlite3_stmt pointers cast to opaque; no extra heap allocation.
arrayPush and allowsSqlQuery rounded out the SDK additions.

installStore keeps living on the zigts side of the split: it runs
during runtime bootstrap, outside any module invocation, so it can't
use the SDK's handle-gated setModuleState. The shim allocates the
module's SqlStore via ctx.allocator and writes it directly into the
slot the module reads from.

Tests green at 1441/1445. The two sql integration tests from the
previous file relied on full-context setup that only makes sense
inside zigts itself; flagging those for the Phase 8 SDK test harness
alongside the other cross-boundary unit tests.
Phase 7 partial. Four of seven net/workflow modules now live in
packages/modules/. Each zigts-side file becomes a thin stub that
adapts the modules-package binding via adapter.adaptModuleBinding
and keeps an installState shim for runtime bootstrap to wire up
callbacks.

- compose is comptime-only, no runtime coupling.
- fetch, service, websocket dispatch through runtime-installed
  callbacks. The state struct lives in the modules package with
  SDK-typed function pointers; the zigts-side InstalledState wraps
  the runtime's Context-typed callbacks with ModuleHandle-typed
  thunks that cast through handleToContext.

SDK additions: isCallable, readFile + freeFileBuffer.

Deferred to a later pass: durable, io, scope. durable has an
un-diagnosed function-pointer mismatch between install-time and
read-time addresses when going through the wrapper; io pulls
fetchSync state via a threadlocal that's read by zigts HTTP code;
scope manipulates GC roots directly. Each requires SDK surface or
runtime-flow changes that don't fit in this phase.

Tests green.
Phase 8. builtin_modules.zig now imports ported bindings directly
from the zigttp-modules peer package and adapts them in-place via
adapter.adaptModuleBinding. The 15 pure-adapter stub files under
packages/zigts/src/modules/{security,platform,http,data,workflow}/
are gone; the directory only holds the modules that still need
zigts-internal access:

- sql, fetch, service, websocket — installState/installStore shims
  called from runtime bootstrap, outside any module invocation.
- io, scope, durable — genuinely coupled to zigts internals
  (fetchSync threadlocal, GC roots, open function-pointer issue).

Ported bindings live under a local `ported` namespace so their
names don't shadow the `<name>_binding` locals in the governance
assertion tests at the bottom of the file.

modules/root.zig trimmed to only re-export the seven still-in-tree
modules plus the module resolver/compiler internals.

Tests green.
Specs move: git mv packages/zigts/module-specs/ packages/modules/module-specs/.
The 22 JSON spec files live alongside their implementations now.

Tooling:
- builtin_modules.zig: spec_path strings in all governance entries
  point at the new packages/modules/module-specs/ root.
- module_audit.zig: looksLikeBuiltinAdjacentPath accepts source under
  packages/modules/src/ as well as the legacy packages/zigts/src/modules/
  (still holds io, scope, durable, and the install-shim files).
- check-capability-helpers.sh: glob covers both module-source roots so
  the audit runs over the peer-package modules too.

Docs:
- README virtual-modules section notes the peer-package layout and
  which modules still live in zigts for runtime coupling.
- docs/architecture.md: tree now shows packages/zigttp-sdk/ and
  packages/modules/; enforcement-points list points at the new paths;
  module-binding key-files list adds the SDK entry.
- Extract contextFromHandle, sdkValue, internalValue, internalArgs
  helpers in module_binding_adapter.zig; fetch/service/websocket
  shims use them instead of hand-rolled @ptrCast/@bitcast chains.
- Trim WHAT-narration comments in builtin_modules.zig and the
  modules/root.zig preamble. Keep only the WHY lines.
- Add a one-line rationale for the 20000 branch-quota bump in
  validateBindings (was 5000 default; O(n*m) name/specifier dup
  checks blow it out once the full roster hits).
- Drop redundant freeFileBuffer from the SDK: readFile already
  allocates via the runtime allocator exposed by getAllocator,
  so callers free through that. Also drops the paired zigts-side
  bridge fn.
FetchState.sdkDeinit was never referenced — the zigts-side shim
overrides deinit with its own stateDeinitAdapter. The allocator
field only existed to feed that dead method, and its remaining
use in stateDeinitAdapter is redundant with the allocator that
setModuleState passes in as the second arg.
…ator field

Same pattern as fetch: sdkDeinit was never referenced, and the
allocator field only fed it. The zigts-side stateDeinitAdapter
now uses the allocator passed in by setModuleState.
Never referenced. deinitSelf stays (called by the zigts-side
shim's stateDeinitAdapter for the StringHashMap teardown).
Move the REPL's slash-command and explicit-command parsing out of
repl.zig into a dedicated commands.zig module with a single command
table driving both forms. repl.zig now focuses on dispatch, tokenization,
and help rendering.

Unit 2 of the parallel refactor plan:
/Users/srdjans/.claude/plans/study-the-plan-provided-clever-wadler.md

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@srdjan
srdjan merged commit 27dcee3 into main Apr 19, 2026
@srdjan
srdjan deleted the unit-2-extract-commands branch April 19, 2026 23:32
srdjan added a commit that referenced this pull request May 24, 2026
nextGuardId returned a bare counter starting at 1. The value is stored
verbatim in JSObject.inline_slots[FUNC_GUARD_ID] and the GC walks every
inline slot as a JSValue via markValue -> isPtr. A counter value whose
top 16 bits landed in the NaN-box pointer prefix range
(0xFFFC_xxxx_xxxx_xxxx) would be misclassified as a heap pointer and
dereferenced. The counter wraps to that range after ~281 trillion
calls, but a hash-seeded or PRNG-seeded variant could land there
immediately.

Step the counter through the 48-bit payload space and OR in
value.JSValue.INT_PREFIX (0xFFFD_xxxx_xxxx_xxxx) before returning. The
JIT loads the slot as raw u64 (movRegMem / OBJ_FUNC_GUARD_ID_OFF) and
compares against callee.guard_id, also raw u64; both sides carry the
prefix bits so the equality check still passes byte-for-byte without
any tag-aware code. Skip 0 so the sentinel is reserved.

Two tests: 1024-iteration property test confirms (id & PREFIX_MASK) ==
INT_PREFIX and uniqueness across the run; end-to-end ensureGuardId test
asserts !slot.isPtr() and !slot.isExternPtr() on the stored value.

Intent: fix-defect
Scope: zigts/bytecode, zigts/value, zigts/gc, zigts/jit
Decided-Against: a parallel non-JSValue slot for guard IDs (touches createBytecodeFunction, createClosure, and 15 JIT call sites)
Decided-Against: marking the slot as untyped via a parallel bitmap (GC walks all inline slots uniformly today)
Refs: 2026-05-23 overall-repo review, P0 #6

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
srdjan added a commit that referenced this pull request Jun 28, 2026
…adapter

xhigh review #2/#6: the SMT solver adapter collapsed every failure into one
verdict and its module doc described the opposite policy from the code.

- parseVerdict only inspected the first stdout token, so a z3 startup banner or
  a `success` line under :print-success was misread as a solver error. Scan for
  the first sat/unsat/unknown token instead, skipping benign preamble; an
  `(error ...)` anywhere still wins (fatal). Add banner/print-success/error-wins
  tests.
- A pre-exec failure to RUN z3 (spawn/IO error, or z3 gone since available())
  now maps to .unknown (environmental, benign/unproven), not .solver_error.
  .solver_error is reserved for z3 RUNNING and emitting no usable verdict - the
  only case that signals the present solver cannot evaluate the model. This stops
  a transient spawn hiccup from failing the audit with a misleading
  "missing FP/String theory" message while keeping the fail-closed property
  (an incapable z3 still manifests as z3 output -> .solver_error -> ZTS758).
- Rewrite the stale module doc (claimed spawn/IO -> .unknown and "inherits the
  parent environment" while the code uses an empty environ) to describe the
  actual two-class policy.

spec-check --audit: 13/13 SMT proved, 4/4 refuted, PASS. test-zigts-cli 76/76.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
srdjan added a commit that referenced this pull request Jul 12, 2026
pi's PropertiesSnapshot now mirrors the engine's full HandlerProperties boolean
surface: adds cost_bounded and post_only (both were silently missing). The
proof card highlights a `cost_bounded` chip, guaranteeCounts folds the new
dimensions into the /ledger proven-path ratio (16/16 -> 18/18), and the persona
gains a "Cost bounds" section teaching the loop-bound discharge forms (literal
arrays, range(n), SQL LIMIT, schema maxItems).

The engine->pi mapper is now a compile-time field copy instead of a hand-written
literal, removing that drift point, and a comptime drift gate asserts pi mirrors
every engine boolean property - a new proof dimension added to the engine now
fails the build until the expert surfaces it (verified by temporarily dropping a
field: the gate fires with an actionable message).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant