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>
The chisel. lib/maude/matching.sx: multi-valued matcher mau/mm returning
ALL substitutions, dispatching on op theory (free/comm/assoc/AC). Identity
lets variables grab empty blocks. AC-canonical form (mau/canon) powers
ac-equal? and deterministic printout. AC rewriting extends f-AC equations
with rest vars so a rule fires on any sub-multiset/subword; mau/first-change
only commits rewrites that change the canonical form (idempotency/identity
terminate). Verified on multiset rewriting, set theory, group equations.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Doc-only: records that the http-listen 'handler-mutex deadlock' is not a
mutex bug but an Erlang-scheduler-context issue (handler runs on a native
Thread.create outside any er-sched step, so gen_server:call->receive can
never complete). Pattern A inapplicable; correct fix is Pattern B in
er-bif-http-listen (lib/erlang, m2 scope). Full diagnosis + patch sketch in
plans/fed-sx-host-primitives.md.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Facade read-by-id was top-level only while content/edit's update/delete are
tree-wide — could not read back a nested block content/edit just modified.
Added generic ct-find-id (doc.sx) + doc-find-deep/doc-has-deep?; content/find
+ has? now descend into sections. content/find-top/has-top? keep top-level
lookup. Audit: remaining doc-find/ct-index-of callers are positional
insert/move (top-level by design). +6 api tests.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
lib/maude/reduce.sx — one-sided syntactic matching (non-linear patterns
via bound-var equality), immutable substitutions, innermost fixpoint
normalisation. Tested on Peano arithmetic, list ops, a propositional
logic simplifier, and non-linear matching.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Investigated the http-listen "handler-mutex deadlock" per
plans/agent-briefings/fed-prims-mutex-fix.md. Reproduced deterministically
(single kernel-route request returns empty reply while a non-kernel route
returns 200; also reproduced with a 3-line minimal echo gen_server).
Root cause is in the Erlang substrate, not the OCaml mutex: native
http-listen runs each handler on a fresh Thread.create outside any Erlang
scheduler step, so gen_server:call -> receive (which raises er-suspend-marker
expecting an enclosing er-sched-step-alive! guard + er-sched-run-all! pump)
can never complete.
Pattern A is inapplicable: the failure reproduces on a single request with
zero contention, so it is not a mutex-contention deadlock; the mutex is in
fact required and must stay. Sx_runtime.sx_call is fully synchronous and no
OCaml symbol reaches the SX-level scheduler, so there is no OCaml-only fix.
The correct fix is Pattern B done entirely in er-bif-http-listen
(lib/erlang/runtime.sx) — spawn the handler as an er-process and
er-sched-run-all! to completion — which is m2 / loops/erlang scope.
Doc-only: full diagnosis + concrete patch sketch added to the Blockers and
Progress log of plans/fed-sx-host-primitives.md. No bin/sx_server.ml change.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Term representation (lib/maude/term.sx) plus a module parser
(lib/maude/parser.sx) consuming lib/guest/lex + pratt:
- whitespace+bracket tokenizer (--- / *** comments)
- mixfix classification (split op names on _): infix/prefix/postfix/const
- precedence-climbing term parser over a pratt table built from op decls
- fmod/mod ... endfm/endm with sort/subsort/op/var/eq/ceq/rl/crl
- transitive subsort hierarchy + operator overloading queries
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
ical.sx serializes events to VEVENT/VCALENDAR text for import by standard
clients: UTC basic-format stamps, DURATION (PT#H#M), full RRULE
(FREQ/INTERVAL/COUNT/UNTIL/BYDAY incl. monthly ordinals 2TU/-1FR/BYMONTHDAY)
plus EXDATE/RDATE. Line-oriented (ev/event->ical-lines / ev/events->ical-lines)
with ev/ical-render joining CRLF for the wire format. 332/332 green.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
oauth.sx routes the PKCE check through pkce_ok: an S256 challenge carried as
{s256, Hash} compares crypto:hash(sha256, Verifier) =:= Hash; a bare
challenge stays plain (§4.1), so both methods coexist with no change to
existing flows (the bare path is the old =:= behaviour). Raw sha256 digests
are compared (base64url is wire encoding, omitted). New tests/pkce.sx (6,
incl. S256 through PAR). Verified pkce 6/6; substrate fix is in the
preceding commit. 239 total.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
er-eval-binary-segment evaluated a string-valued segment (the parser
represents <<"abc">> as one integer segment whose value is the whole string
"abc") by calling er-emit-int! on the string, emitting a single bogus 0
byte. So every <<"...">> literal became {:tag "binary" :bytes (0)} — which
made binary =:= read as "always equal" and crypto:hash input-independent.
Fix: the integer branch now expands a string value to one byte per
character (Erlang semantics: <<"abc">> ≡ <<97,98,99>>). Verified:
byte_size(<<"abc">>)=3, <<"a">> =:= <<"b">> is false, crypto:hash distinct
per input.
(User-authorized cross-scope fix from the identity loop; loops/erlang
should adopt this as the owner of lib/erlang.)
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
ev/book-checked! prevents an attendee double-booking themselves across
different events by consulting their persist-derived availability for the
occurrence window (:time-conflict on overlap; same-occurrence re-book stays
idempotent).
