artdag/opt-improvement compares the original output cone (dce to id) vs the
maude-reduced DAG under an injected cost-fn, returning before/after total-work and
critical-path. opt-cheaper? asserts optimisation never increases cost: the 5-node
chain drops to 2 (work 5->2, path 5->2) and stays cheaper under radius-weighted cost
(5->3); over dedup and untouched DAGs are never pessimised. Consumes cost.sx. Phase 7
base + (later) cost box done. maude-optimize 38/38, total 196/196.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
artdag/opt-reduce: encode a DAG cone -> opt-term, mau/creduce against the
optimisation module, decode the normal form back to build-entries and rebuild.
Result-preserving: a 5-node blur;blur;id;bright0 chain collapses to 2 nodes and an
over(I,I) dedup 3->2, both executing identically to the original; non-optimisable
DAGs round-trip their radius faithfully (unary 1+1+1 -> 3). Completes Phase 7's
bridge-back + equivalence boxes. maude-optimize 33/33, total 191/191.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
lib/artdag/optimize-rules.sx — the effect-pipeline optimisation passes (identity
elim, no-op/zero-radius elim, adjacent fusion, idempotent over dedup) as a maude
module. Radius algebra is _+_ [assoc comm id: 0] (NOT Peano successor rules, which
are non-confluent here); mau/confluent? certifies 0 non-joinable critical pairs, so
the optimised pipeline's normal form / content id is rewrite-order stable. Consumes
lib/maude/confluence.sx. maude-optimize 25/25, total 183/183.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
next/tests/smoke_federate.sh boots two sx_server instances on
distinct ephemeral ports, each running http_server:start with its
own kernel + actor + the peer's AS pre-populated. The test signs
a real Follow envelope with alice's key in a third subprocess
(outbox:construct(follow, alice, 1, bob) + outbox:sign +
term_codec:encode), POSTs the bytes to B's /actors/bob/inbox over
real HTTP, and asserts:
- Both instances bind and serve their welcome route.
- Each instance's kernel-aware outbox returns the expected tip.
- B accepts the Follow (status 202 — pipeline validated the
signature against the pre-populated alice peer-AS,
nx_kernel appended to the inbox, auto-accept fired).
- bob's outbox tip advances 0 -> 1 (the Accept publish
landed in the outbox via outbox:publish + the kernel
gen_server).
This exercises every layer that m2 built:
- Step 8e httpc:request/4 BIF wrapper
- Step 8f dispatch_http closure (delivery_worker for the peer)
- Step 10c discovery_fetch (peer-actor doc shape)
- Blockers #1 marshaller bridge (er-request-dict-to-proplist
+ er-proplist-to-dict)
- Blockers #4 :pending-args substrate fix (kernel routes
suspend/resume in the SX scheduler)
All under real cross-instance HTTP load with both kernels
running as full gen_servers.
Step 12's plan body sketches the full Follow/Accept/Note/restart
flow (13+ steps); the m2 acceptance criterion is the cross-
instance signed-envelope round-trip with auto-accept fan-out,
which this 6/6 pass proves end-to-end. Step 8b-timer (retry
schedule) still gates on Blockers #3 send_after — the smoke
drains synchronously, sufficient for the wiring proof but
production retry needs the timer primitive.
m2 is now feature-complete except for the substrate timer
gate. The plan's Step 12 entry is ticked and a Progress log
entry added.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The CID-stability check now calls mau/confluent? / mau/non-joinable-pairs from
lib/maude/confluence.sx (merged in) instead of re-implementing critical-pair
analysis inside lib/artdag. Picks up confluence.sx via the architecture merge.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Adds lib/maude/confluence.sx — the CID-stability oracle the artdag optimiser
needs. 274 tests.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Substrate fix: two-line change to lib/erlang/runtime.sx that lets
http-listen handler routes call gen_server:call without deadlocking.
1. er-sched-step-alive!: pass :pending-args (when set) to the
initial-fun call instead of always passing an empty list.
Default behavior (no field) stays (list) — drop-in safe.
2. er-bif-http-listen sx-handler: instead of er-apply-fun handler
inline (which blows up on receive's er-suspend-marker because
the connection thread has no scheduler step on its stack),
create a real er-process with :initial-fun = handler and
:pending-args = (list req-pl), then er-sched-run-all! to drain.
Any receive (e.g. gen_server:call) suspends + resumes inside
the SX scheduler frame the process owns. Read :exit-result
for the response proplist; marshal back to SX dict.
Investigation arc (see plans/fed-sx-milestone-2.md Blockers #4 +
Progress log):
- loops/fed-prims bf8d0bf2 diagnosed it as Erlang-substrate, not
OCaml mutex (Pattern A wrong, Pattern B right but sketchy).
- First Pattern B attempt failed: tried er-spawn-fun on a raw SX
lambda, hit (er-fun? fv) gate. Connection-thread bisect
pinpointed the exact line.
- Real fix: use the existing er-fun (user's handler) directly,
but feed it via :pending-args so step-alive's hardcoded
(list) doesn't drop the request arg.
Acceptance:
- new next/tests/smoke_kernel_route.sh: 6/6 over real HTTP
(welcome /, /actors/alice, /actors/alice/outbox with
gen_server-backed tip, /actors/alice/inbox, unknown-actor,
via http_server:start(P, [{kernel, nx_kernel}])).
- next/tests/http_server_tcp.sh: 5/5 (bumped wait_bound from
30s to 180s — cold boot is slow under sibling-loop CPU load
and the per-handler scheduler ramp adds a small margin).
- Erlang conformance: 761/761.
Step 12's two-instance smoke test is now unblocked — its full
Follow / Accept / Note flow can layer on top of this kernel-route
surface. m2 plan updated.
Pre-existing httpc_request.sh flakiness ("Undefined symbol:
http-request" on the live-call epochs) reproduces WITHOUT this
change — see git stash A/B in the investigation. Unrelated.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
A tz event now exports DTSTART;TZID=<name>:<local> (EXDATE/RDATE likewise;
UNTIL stays UTC per RFC), and the VCALENDAR emits a VTIMEZONE per distinct zone
with DAYLIGHT/STANDARD sub-components generated from the zone's transition rules
(offsets + FREQ=YEARLY;BYMONTH;BYDAY) — London/Paris blocks match real-world
definitions. Clients recur at fixed wall-clock time, DST-correct (prior caveat
gone). Importer tolerates ;TZID= params. 376/376 green.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
lib/host/sxtp.sx implements the host<->subsystem wire format per
applications/sxtp/spec.sx:
- message algebra (request/response/condition/event + status helpers
ok/created/not-found/forbidden/invalid/fail) as string-keyed dicts;
verb/status/type stored as symbols (ride the wire bare)
- codec: sxtp/serialize (dict -> text/sx list form, deterministic top-level
field order, nested messages emitted in their own list form, no :msg leak)
and sxtp/parse (text/sx -> dict via a deep keyword-token->string normaliser)
- Dream bridge: sxtp/from-dream (HTTP req -> SXTP req, method->verb,
query->params) and sxtp/to-dream (SXTP resp -> HTTP resp, status->code,
body serialised to text/sx)
- 39-test suite covering algebra, serialise/parse round-trip, mappings, bridge
Runtime notes: serialize renders string-keyed dicts as {:k v} and symbols
bare; parsed keyword tokens are a distinct type (not = to string literals) so
parse normalises; unquote-splicing is unreliable so the emitter is str-based.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
lib/maude is now on this branch (fast-forwarded to architecture). The fit is
proven (lib/maude/tests/effects.sx). Phase 7 spells out the adapter
(maude-bridge.sx), the optimisation laws as a maude module, equivalence with
optimize.sx, and a syntactic confluence/CID-stability check. maude is a
read-only consumed substrate; gotchas recorded.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Composable handler->handler layers over Dream's primitives, with auth and
permission POLICY injected so the layer is policy-free and testable:
- middleware.sx: host/wrap-errors (JSON 500 via dream-catch-with),
host/require-auth (bearer->principal via dream-bearer-token, JSON 401,
injected token resolver), host/require-permission (lib/acl acl/permit? gate,
JSON 403, injected resource extractor), host/pipeline (first = outermost)
- feed.sx: POST /feed via host/feed-write-routes — auth ∘ ACL(post,feed) ∘
wrap-errors over host/feed-create (parse JSON body -> feed/post -> 201;
non-object -> 400). Created activity reads back via GET /feed.
- middleware suite (9) + feed write tests (6 new); conformance preloads now
include the Datalog engine + ACL subsystem + Dream auth/error.
ACL works with string atoms (no symbol coercion). Mute/prefs layer and sxtp.sx
deferred to the next tick.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Walked Pattern B's failure step-by-step from the connection thread
under a live http-listen instance, instrumenting each piece as its
own minimal sx-handler with a hardcoded reply dict:
hardcoded {:status 200 :headers {} :body "..."} -> HTTP 200 ✓
read er-sched-process-count -> "procs=2" ✓
er-pid-new! -> 204 ✓
er-proc-new! (er-env-new) -> 205 ✓
er-spawn-fun (fn () 42) -> HTTP 000
The break is er-spawn-fun's (not (er-fun? fv)) gate raising
"Erlang: spawn/1: not a fun" because the raw SX lambda isn't an
Erlang-fun-shaped {:tag "fun"} dict. The `error` raise propagates
through Sx_runtime.sx_call and is swallowed by the native http-listen
(try ... with _ -> ()) at sx_server.ml:852; connection writes
nothing and closes -> curl reports HTTP 000.
This invalidates the previous "scheduler-re-entry race" hypothesis:
the global er-sched-* state IS shared with the connection thread
and reads correctly (process count of 2 = boot main + http:listen).
The breakage is the strict er-fun? shape check, not concurrency.
Path forward (still substrate scope, one helper):
- Add an er-mk-host-fun helper in lib/erlang/runtime.sx (or a
small AST-constructor in transpile.sx) that produces a real
er-fun dict from a host SX closure.
- sx-handler can then build a 0-arity wrapper-with-captured-req-pl
and feed it to er-spawn-fun.
- er-sched-run-all! drains, exit-result is read, response goes
back to the wire.
Reverted runtime.sx to the Blockers #1 marshaller-bridge fix (the
in-flight Pattern B attempts are not committed). Blockers #4 entry
in plans/fed-sx-milestone-2.md updated with the verified diagnosis
and the one-helper path. Progress log entry added.
m2 stays at 11/12 steps; the substrate helper is loops/erlang scope.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
lib/maude/tests/effects.sx — proves artdag's effect-pipeline optimisations
(fusion, no-op/dead-op elim, identity elim, CSE/idempotent dedup) are
equational rewriting: the optimised pipeline is the normal form, confluence
gives a stable content id. The 'second consumer' spike for a maude-driven
optimiser in lib/artdag. Surfaced faithfulness note: id: affects matching/canon
not auto-reduction.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
First migrated endpoint onto the SX host. lib/host is a thin wiring layer:
a host handler is a Dream handler (request->response) that calls a subsystem
public API and serialises via a shared JSON envelope.
- handler.sx: host/ok, host/ok-status, host/error, host/json-status (Dream's
dream-json is 200-only), host/query-int
- router.sx: host/make-app assembles per-domain route groups + /health probe
into one dream-router (reuses dr/flatten-routes)
- feed.sx: GET /feed reads feed/all + stream combinators, recent-first, with
?actor= filter and ?limit= cap
- 3 test suites incl. a golden test (body == subsystem recent stream + envelope)
- conformance.sh mirrors lib/dream's runner
Builds on dream-on-sx (merged, gate green 480/480) rather than a throwaway
native request model; collapses most of plan Phase 4 into Phase 1.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Bug: tz events store wall-clock LOCAL times but export stamped them with a Z
(UTC) suffix, so a London 18:00 event falsely read as 18:00 UTC. ev-ical-conv
now converts a tz event's DTSTART/UNTIL/EXDATE/RDATE local->UTC before
formatting (London summer 18:00 -> 170000Z; Paris -> 160000Z); non-tz events
unchanged. Caveat: UTC RRULE drifts from wall-clock-stable tz recurrence across
a DST boundary (VTIMEZONE deferred). 366/366 green.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
ical.sx parses VEVENT/VCALENDAR text back into events (ev/ical-lines->event,
ev/parse-vcalendar): DTSTART/DURATION/RRULE (ordinal BYDAY, BYMONTHDAY, UNTIL/
COUNT/INTERVAL) + EXDATE/RDATE. Round-trip is occurrence-exact — export->import
expands to the identical occurrence set. Completes bidirectional interop.
360/360 green.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
run.sx now handles 'search START =>* GOAL .' (reports the witness path) and
mau/run-pretty prints Maude-style 'result SORT: TERM' using least-sort
inference. searchpath.sx exposes mau/search-path-terms (term-level entry).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
lib/maude/sorts.sx — mau/term-sort computes the least sort of a term (smallest
result sort among op declarations whose arg sorts the actuals satisfy modulo
subsorting); overloaded f(1)=NzNat vs f(s 0)=Nat. mau/has-sort? for
membership-style checks. Answers the plan's order-sorted substrate question.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Infix ops parse left (default / gather (E e)) or right (gather (e E)) per the
gather attribute, so _:_ [gather (e E)] reads a : b : c as right-nested. Full
insertion sort now runs over bare cons lists with no parentheses.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Parser reads trailing eq attributes (eq L = R [owise] .) via mau/split-attrs.
mau/crewrite-top is two-pass: ordinary equations first, owise last — an owise
catch-all fires only when no ordinary equation applies, regardless of
declaration order. Verified a catch-all declared first still defers.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
lib/maude/searchpath.sx — mau/search-path returns the shortest sequence of
states from start to goal (the solution moves), mau/search-length its step
count. BFS over all one-step successors, threading the path.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
lib/maude/run.sx — mau/run-program / mau/run parse a module plus trailing
reduce/red/rewrite/rew commands (with optional 'in MOD :' qualifier) and
execute them, rendering results in mixfix surface syntax. An idiomatic
.maude file now runs end-to-end.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
lib/maude/pretty.sx — mau/term->maude renders internal prefix terms back
in Maude mixfix syntax driven by op forms; mau/red->maude / mau/rew->maude
reduce-then-render. Output now reads as idiomatic Maude.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
lib/maude/meta.sx — up-term/down-term encode terms as data (mt-var/mt-app),
reflective meta-reduce/meta-rewrite/meta-apply, the meta-circular law
down(metaReduce(up t)) =AC= reduce t, and meta-prove-equal? as a generic
equational theorem helper. Verified round-trips, reflection agreement,
single-rule meta-apply, and proving commutativity/associativity instances.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
lib/maude/strategy.sx — first-class set-valued strategies: idle/fail/all/
rule/seq/alt/star/plus/bang/name combinators, named-strategy env. Same
rule set computes different things under different strategies; verified
with single-rule vs all vs seq-order vs alt vs star vs bang.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
lib/maude/rewrite.sx: rl/crl transitions interleaved with eq normalisation.
mau/rewrite = default strategy (top-down, leftmost-outermost, first rule);
mau/rew bounded; mau/search = BFS reachability over all successors.
lib/maude/fire.sx: short-circuiting matcher (mau/fire-eq) — finds the first
productive match instead of enumerating the whole solution set. Fixes the
exponential blowup of AC rewriting on many identical elements (8 coins:
60s+ to <1s). Eager match-multiset kept only for match-all / search.
Verified on AC coin-change, traffic light, branching search, crl clock.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
loops/fed-prims commit bf8d0bf2 (merged as 94f6ab9f) diagnosed
Blockers #4 as Erlang-substrate scope and sketched a Pattern B fix
purely in er-bif-http-listen: wrap the handler call in er-spawn-fun
+ er-sched-run-all! and read the spawned process's :exit-result.
Tried it on lib/erlang/runtime.sx — does not work. Listener binds,
connection thread enters sx-handler, but the spawned handler's
response never reaches the wire; even the non-kernel welcome
route returns HTTP 000 (empty reply). Reverted to the Blockers #1
marshaller-bridge sx-handler, which correctly serves the
welcome / capabilities / 404 / 401 surface even though kernel-
aware routes still hang.
Working hypothesis (documented in Blockers #4): the http_server:
start spawn itself is parked inside the native Unix.accept loop on
the boot thread; the global er-sched-* state still has that
process in its queue. When the connection thread (under the
per-instance native mutex) calls er-sched-run-all!, it re-enters
the SAME global scheduler — the boot thread's er-sched-step! of
the http:listen process is blocked forever inside the native
primitive, so the connection-thread pump races against that
parked frame or otherwise fails to drive the handler process to
completion before sx-handler returns.
The fed-prims diagnosis was correct that the bug is substrate
scope and that Pattern A (the mutex) is wrong — but the Pattern
B sketch assumed a fresh / private scheduler context that doesn't
exist in the current substrate. Blockers #4 entry updated with
three substrate fixes that would actually work (non-blocking
http-listen + per-thread sched, full erlang-eval-ast-style
per-handler sched-init, or skipping the per-process scheduler
entirely for HTTP handlers via a synchronous reply channel).
m2 stays at 11/12 steps done; Step 12 remains gated. Loop pacing
dialled back down — substrate work owes to loops/erlang or a
follow-on fed-prims tick with a more careful design pass.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
ev/book-series! / ev/cancel-series! apply a booking/cancel to every occurrence
of one event in a window (RSVP the whole weekly class), returning per-
occurrence (occ-key status) results; capacity still enforced per occurrence
(some :booked, some :full), idempotent re-book (:already). ev/series-count,
ev/series-booked. 341/341 green.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Surgical add of the two radar-authored planning docs onto architecture (both new
files, no conflict). Migration strategy: duplicate->cutover->diverge, strangler edge
+ layer-split shadow-diff, host-trio critical path. abstractions.md is the evidence
base the strategy cites (A1 done, W1/W4/W8 substrate-adoption findings).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
lib/maude/conditional.sx — condition-aware reducer. ceq fires only when
its guard holds: equational guards (l=r reduce to same normal form) and
boolean guards (term reduces to true), evaluated by recursing through the
same reducer. Verified on gcd, insertion sort, max, even.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
