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>
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>
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>
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>
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).
ev/book-checked! prevents an attendee double-booking themselves across
different events: consults their persist-derived availability (ev/free-p?) for
the occurrence window, returns :time-conflict on overlap else the normal
ev/book-occ! result. Re-booking the same occurrence stays idempotent
(:already); other actors unaffected. ev/would-time-conflict? predicate.
311/311 green.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The er-bif-http-listen BIF body in lib/erlang/runtime.sx referenced
er-http-resp-to-sx / er-http-req-of-sx — helpers deleted by 78eae9ef
("fed-sx-m1: 8b-bridge cleanup") because the BIF body never picked
them up. Listener bound but every request handler crashed on first
call to the undefined helpers; curl got 000 / empty body.
Rewrote the sx-handler bridge to thread through the live marshallers
that the cleanup commit's message claimed were already in use:
Inbound: SX Dict {:method :path :query :headers :body}
-> er-request-dict-to-proplist
-> Erlang request proplist matching http_server:route/2 shape
(binaries for path/method/body, dict-like proplist for headers)
Outbound: Erlang [{status, N}, {headers, [{Bin, Bin}, ...]}, {body, Bin}]
-> er-proplist-to-dict
-> SX Dict matching what native http-listen serialises
(er-to-sx-deep auto-converts binary values to strings and
flattens the 2-tuple headers cons to a nested SX dict)
This is technically substrate work in lib/erlang/runtime.sx but
stays within the m2 briefing's allowed exception scope — the http
BIF wrappers (Step 8a / 8e / now 12-prep) are the explicit substrate
carve-outs. Unblocks Step 12's REAL two-instance smoke test rather
than an in-process loopback variant.
Test: next/tests/http_server_tcp.sh 5/5
- GET / -> 200
- GET /.well-known/sx-capabilities -> 200 (body contains "kernel:")
- GET /no-such-path -> 404
- POST /activity (no bearer) -> 401
- POST /activity (bad bearer) -> 401
No-regression gates green: Erlang conformance 761/761,
httpc_request 10/10, dispatch_http 10/10, http_listen_bif 5/5,
discovery_fetch 11/11, http_multi_actor 44/44, http_marshal 10/10.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
tests/integration.sx — one narrative across every module: catalog -> stock
check -> quote (promo+stack+tax) -> attribution -> order flow -> payment
envelope -> settle -> recon -> refund flow -> ledger mismatch, asserting the
seams tie together with consistent numbers. Proves the three-substrate
composition (minikanren pricing + flow lifecycle + persist ledger) end to end.
Total 297/297 across 18 suites.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
content/diff + diff-versions enumerated ids top-level only (doc-ids/
doc-find), so diffs of documents with sections missed every nested add/
remove/change. Now via doc-tree-ids + doc-deep-find; sections excluded from
:changed (no own content), still reported in :added/:removed. Flat-doc
diffs unchanged. +9 store tests.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>