diff --git a/posts/2022-03-14-digitle-in-maude.md b/posts/2022-03-14-digitle-in-maude.md
new file mode 100644
index 0000000..3661133
--- /dev/null
+++ b/posts/2022-03-14-digitle-in-maude.md
@@ -0,0 +1,350 @@
+---
+title: digitle in maude
+date: 2022-03-14
+tags: [maude, computer]
+...
+
+so you know [digitle] right. it's the countdown numbers round.
+
+[digitle]: https://c.eev.ee/digitle
+
+1. you have six numbers to start with, each picked from 1–10 or 25, 50, 75, 100;
+   and a target.
+2. you can add, subtract, multiply, or divide any of the numbers you currently
+   have.
+3. you can only use each number once, and the intermediates have to also all be
+   positive integers. (it is ok to have some numbers left over at the end.)
+
+you probably have not heard of [maude] though. but it's cool. it lets you define
+rewrite systems with a few equational extras like associativity and
+commutativity. in other words it's essentially a domain specific language for
+solving puzzles like this. it also lets you prove stuff like termination of your
+system, but we are not going to do any of that today.
+
+[maude]: https://maude.cs.illinois.edu/w/index.php/The_Maude_System
+
+**i just think maude is neat and this is a nice little example to show it off.**
+that's all this is really.
+
+---
+
+```maude
+mod DIGITLE is
+  protecting NAT .
+  vars M N : Nat .
+```
+
+the file starts with a module declaration. everything has to live inside some
+module, but this program isn't big enough to be worth splitting up so it's all
+going into one. since digitle involves numbers, i'm also importing the `NAT`
+module, and saying that any time `M` or `N` show up in equations or rewrite
+rules they stand for single numbers.
+
+<aside>
+  **why is importing called `protecting`?** in maude, sorts (approximately,
+  types) aren't necessarily closed. you can add a new constructor, or equations
+  between constructor forms, at any time. unlike in languages like haskell or
+  rust, constructors don't have to be _free_, which means you can have equations
+  like `s (s (s (s z))) = z` and pow you've got $\mathbb{Z}/4\mathbb{Z}$.
+
+  but when you're importing a module, most of the time you don't want to do any
+  of that. so there are three ways of importing a module to express how much you
+  intend to mess with it. `protecting` says you are not adding new constructors
+  or conflating existing ones. `extending` lets you add new constructors, but
+  not new equations. `including` lets you do whatever. since i'm just using
+  _normal_ numbers, `protecting` is what i want.
+
+  an important caveat is that it is not possible for maude itself to check you
+  are telling the truth here, but it can ask `yices` or `cvc4` for help. please
+  don't press me for more detail i have never used this
+</aside>
+
+the first thing i need is a ~~type~~ sort for the pool of numbers we currently
+have. it's a _multiset_: the number of copies of each number matters, but the
+order they're in doesn't. the most convenient way to express that is like this.
+
+```maude
+sort Pool .
+subsort Nat < Pool .
+op nil : -> Pool .
+op __  : Pool Pool -> Pool [assoc comm  id: nil] .
+var Ps : Pool .
+```
+
+first i just declare `Pool` as a sort, without saying anything about what it
+looks like. next i say that any `Nat` is also a `Pool` (containing one copy of
+just that number), by making `Nat` a subsort of `Pool`.
+
+in the third and fourth lines, i say that `nil` is a pool (with no numbers), and
+two `Pool`s written next to each other are also a `Pool`. so far, we've defined
+a binary tree. by making `__` associative, we're saying that the exact
+bracketing of the appends doesn't matter, which flattens it to a list. by saying
+it's commutative, we're saying the order _also_ doesn't matter.
+
+the last attribute, `id: nil`, says that `Ps nil = nil Ps = Ps`. it also allows
+a pattern like `M N Ps` to match against `1 2`, setting `Ps = nil`.
+
+it feels a bit weird at times to be specifying constructors of a tree and then
+telling the language to flatten them after the fact, coming from languages where
+you try to design your datatypes to only have one representation per value. but
+the benefit of writing it like this instead of something like
+`op cons : Nat Pool -> Pool` is that maude knows what `assoc`, `comm`, and `id`
+mean, so later when i have some equations and rewrite rules that match on the
+beginning of a list, it knows that it can actually pick those numbers from
+_anywhere_, without needing extra rules to shuffle the list around manually.
+
+<aside>
+  **the name `__` is pretty weird!** generally operator names are written with an
+  underscore where the arguments go, so the name of the addition operator is
+  `_+_`. in this case, there _is_ no operator, it's just two things next to each
+  other (in a context where a `Pool` value is expected, anyway), so it's just
+  two underscores.
+</aside>
+
+from here, we *could* just define the rewrite rules and be done. something like
+this would work:
+
+```maude
+rl  [add] : M N  =>  M + N .
+rl  [sub] : M N  =>  sd(M, N) .
+rl  [mul] : M N  =>  M * N .
+crl [div] : M N  =>  M quo N if M rem N = 0 .
+```
+
+<aside>
+  **`sd`** is "symmetric difference"---e.g. `sd(1, 4) = sd(4, 1) = 3`.
+</aside>
+
+the first three rules just pick two numbers from our pool (any two, because of
+`comm`; they don't have to be next to each other), and replace them with the
+result of applying them to one of our operations. the last one is slightly more
+complicated, because we can only divide evenly. `_quo_` ignores the remainder
+altogether, so we need a _conditional rule_ which only fires if the remainder
+actually is zero.
+
+save what we have so far, plus a terminating `endm` for the `mod`, in a file
+`digitle.maude`, and feed it into the repl:
+
+```
+$ maude digitle
+                     \||||||||||||||||||/
+                   --- Welcome to Maude ---                   
+                     /||||||||||||||||||\
+            Maude 3.2.1 built: Mar 13 2022 18:56:15
+             Copyright 1997-2022 SRI International
+                   Mon Mar 14 02:28:22 2022
+```
+
+let's use [random puzzle ALO7b9UK](https://c.eev.ee/digitle/#seed=ALO7b9UK)
+as an example. we have to get to **793** starting from
+**75, 4, 7, 9, 8, 2**. so starting from that list, we want to search for a
+sequence of rewrites that leads to a pool containing 793. one solution is all
+we need.
+
+```
+Maude> search [1] (75 4 7 9 8 2) =>* (793 Ps) .
+search [1] in DIGITLE : 75 4 7 9 2 8 =>* Ps 793 .
+
+Solution 1 (state 9577)
+states: 9578  rewrites: 273357 in 128ms cpu (128ms real) (2135601 rewrites/second)
+Ps --> 7
+```
+
+ok, so there _is_ at least one solution, which leaves 7 unused (because it is
+in the assignment for `Ps`). we can use the state label `9577` to replay the
+sequence that reaches it, and see which steps it took.
+
+```
+Maude> show path 9577 .
+state 0, Pool: 2 4 7 8 9 75
+===[ rl N M Ps => Ps N + M [label add] . ]===>
+state 4, Pool: 4 7 8 11 75
+===[ rl N M Ps => Ps N * M [label mul] . ]===>
+state 146, Pool: 7 11 32 75
+===[ rl N M Ps => Ps N * M [label mul] . ]===>
+state 1733, Pool: 7 32 825
+===[ rl N M Ps => Ps sd(N, M) [label sub] . ]===>
+state 9577, Pool: 7 793
+```
+
+squinting at the available numbers each time, along with the rule labels, we can
+just about make out what it did to get to a solution:
+
+:::twocol
+- 2 + 9 = **11**
+- 4 × 8 = **32**
+- 11 × 75 = **825**
+- 825 − 32 = **793** :star::star:
+:::
+
+ok that's cool. but reading the output is a bit annoying. let's instead keep
+track of what we did so that it's just printed legibly at the end of `search`.
+thanks to maude's flexible expression syntax, we can make this look like pretty
+much whatever we want.
+
+```maude
+sort Op .
+ops + - × ÷ : -> Op .
+
+sort Steps .
+
+--- empty list
+op nil : -> Steps .
+
+--- a single step, like "3 + 4 → 7"
+op ___→_ : Nat Op Nat Nat -> Steps [prec 10] .
+
+--- sequence of steps
+op _,_ : Steps Steps -> Steps [assoc id: nil prec 20] .
+
+var Ss : Steps .
+```
+
+<aside>
+  **`prec N`** is parsing/printing precedence (higher is looser, same as coq,
+  opposite of haskell/agda/idris).
+</aside>
+
+so solution traces are written like
+`2 + 9 → 11,4 × 8 → 32,11 × 75 → 825,825 - 32 → 793`
+and that is also how maude will print them.
+
+the given state at any point is now going to be the available pool of numbers,
+_plus_ the steps taken so far. this is just a pair, along with an abbreviation
+`\{Ps}` to make the `search` command look a little nicer.
+
+```maude
+sort State .
+op _&_ : Pool Steps -> State .
+
+op {_} : Pool -> State .
+eq {Ps} = Ps & nil .
+
+var S : State .
+```
+
+one last thing before the expanded rewrite rules is a predicate to say what we
+are looking for. this isn't strictly necessary, you could just continue to
+pattern match in the `search` command like last time; i just think this looks a
+bit nicer. but a state "has" a number `N` if `N` occurs anywhere in the pool.
+maude supports repeating pattern variables so this is nice and short.
+
+```maude
+op _has_ : State Nat -> Bool .
+eq (N Ps & Ss) has N = true .
+eq S           has N = false [otherwise] .
+```
+
+<aside>
+  it could even skip the `false` line with a slightly different signature but
+  then i would have to explain more about the sort & kind system... this is good
+  enough.
+</aside>
+
+
+the new rewrite rules (delete the other ones) have the same behaviour for the
+number pool, and also append the current step to the trace. since we don't need
+`show path` any more i removed the labels.
+
+```maude
+rl  M N Ps & Ss  =>  Ps (M + N)   & Ss, (M + N → (M + N)) .
+rl  M N Ps & Ss  =>  Ps sd(M, N)  & Ss, (M - N → sd(M,N)) .
+rl  M N Ps & Ss  =>  Ps (M * N)   & Ss, (M × N → (M * N)) .
+crl M N Ps & Ss  =>  Ps (M quo N) & Ss, (M ÷ N → (M quo N)) if M rem N = 0 .
+```
+
+now load the updated file into maude and run the search command. i'm using
+`s.t.` (short for `such that`) to identify solutions by a boolean expression,
+the `_has_` function above.
+
+```
+$ maude -no-banner digitle
+Maude> search [1] {75 4 7 9 8 2} =>* S s.t. S has 793 .
+search [1] in DIGITLE : {75 4 7 9 2 8} =>* S such that S has 793 = true .
+
+Solution 1 (state 335734)
+states: 335735  rewrites: 1114984 in 832ms cpu (830ms real) (1340125 rewrites/second)
+S --> (7 793) & (9 + 2 → 11),(8 × 4 → 32),(75 × 11 → 825),(825 - 32 → 793)
+```
+
+and now we have our solution nicely printed!
+
+there is one small thing that is still bothering me. if we are trying `M + N`,
+then trying `N + M` later is just wasting time. so what if we make all the rules
+conditional so that the first argument is never smaller than the second.
+
+```maude
+crl M N Ps & Ss  =>  Ps (M + N)   & Ss, (M + N → (M + N)) if M >= N .
+crl M N Ps & Ss  =>  Ps sd(M, N)  & Ss, (M - N → sd(M,N)) if M >  N .
+crl M N Ps & Ss  =>  Ps (M * N)   & Ss, (M × N → (M * N)) if M >= N .
+crl M N Ps & Ss  =>  Ps (M quo N) & Ss, (M ÷ N → (M quo N))
+  if M >= N /\ M rem N = 0 .
+```
+
+and look, it's five times faster now it's not repeating itself.
+
+```
+Maude> search [1] {75 4 7 9 8 2} =>* S s.t. S has 793 .
+search [1] in DIGITLE : {75 4 7 9 2 8} =>* S such that S has 793 = true .
+
+Solution 1 (state 46714)
+states: 46715  rewrites: 270529 in 160ms cpu (158ms real) (1690806 rewrites/second)
+S --> (7 793) & (9 + 2 → 11),(8 × 4 → 32),(75 × 11 → 825),(825 - 32 → 793)
+```
+
+---
+
+here's the full file. the `format` directives i didn't discuss: the one in `_,_`
+puts a space after the comma, and the rest do some colours & indenting to make
+the solution a little bit prettier. it also contains a predicate `_has!_` for
+Hard Mode, that requires _all_ the numbers get used up; and `_almost has_`,
+which finds any almost-solution within 10 of the target, and uses language
+features that maybe i will discuss if i ever write a second post about maude.
+
+```maude
+mod DIGITLE is
+  protecting NAT .
+  var M N : Nat .
+
+  sort Pool .
+  subsort Nat < Pool .
+  op nil : -> Pool .
+  op __  : Pool Pool -> Pool [assoc comm  id: nil] .
+  var Ps : Pool .
+
+  sort Op .
+  op + : -> Op [format (r o)] .
+  op - : -> Op [format (g o)] .
+  op × : -> Op [format (y o)] .
+  op ÷ : -> Op [format (b o)] .
+
+  sort Steps .
+  op nil : -> Steps .
+  op ___→_ : Nat Op Nat Nat -> Steps [prec 20  format (d d d d ! o)] .
+  op _,_ : Steps Steps -> Steps [assoc  id: nil  prec 10  format (d d s d)] .
+  var Ss : Steps .
+
+  sort State .
+  op _&_ : Pool Steps -> State [format (d d n++i --)] .
+  op {_} : Pool -> State .
+  eq {Ps} = Ps & nil .
+  var S : State .
+
+  op _has_ : State Nat -> Bool .
+  eq (N Ps & Ss) has N = true .
+  eq S           has N = false [otherwise] .
+
+  op _has!_ : State Nat -> Bool .
+  eq (N & Ss) has! N = true .
+  eq S        has! N = false [otherwise] .
+
+  op _almost has_ : State Nat -> [Bool] .
+  ceq (M Ps & Ss) almost has N = true if sd(M,N) <= 10 .
+
+  crl M N Ps & Ss  =>  Ps (M + N)   & Ss, (M + N → (M + N)) if M >= N .
+  crl M N Ps & Ss  =>  Ps sd(M, N)  & Ss, (M - N → sd(M,N)) if M >  N .
+  crl M N Ps & Ss  =>  Ps (M * N)   & Ss, (M × N → (M * N)) if M >= N .
+  crl M N Ps & Ss  =>  Ps (M quo N) & Ss, (M ÷ N → (M quo N))
+    if M >= N /\ M rem N = 0 .
+endm
+```
diff --git a/posts/test.md b/posts/test.md
deleted file mode 100644
index 85c584d..0000000
--- a/posts/test.md
+++ /dev/null
@@ -1,16 +0,0 @@
----
-title: test
-tags: [a, b]
-date: 2021-07-25
-conlang: laantas
-...
-
-# hello
-
-im gecs
-
-:::example
-`{#kášńḿł | size=100 ; stroke=4}`
-:::
-
-$$\mathbb{wow},\, \mathcal{MATH}$$
diff --git a/style/page.css b/style/page.css
index 48ee047..8be0f5f 100644
--- a/style/page.css
+++ b/style/page.css
@@ -88,6 +88,10 @@ hr {
   height: 0;
 }
 
+pre + hr {
+  margin-top: 1.5em;
+}
+
 .meta {
   display: flex;
   column-gap: 1em;
@@ -168,8 +172,11 @@ code {
 }
 
 pre {
-  width: min-content;
-  margin: auto;
+  width:      min-content;
+  margin:     0.5em auto;
+  padding:    0.5em 0.8em;
+  border:     1px solid var(--root-col);
+  background: hsla(0deg, 0%, 100%, 40%);
 }
 
 
@@ -378,6 +385,14 @@ blockquote {
 }
 
 
+aside {
+  font-size: 90%;
+  margin: 0.5em 3em;
+  border-left: 2px solid var(--root-col);
+  padding-left: 1em;
+}
+
+
 /* syntax highlighting for maude
  * [todo] does this also look ok for other langs */
 .maude .pp { color: hsl(343deg, 100%, 40%); font-weight: 500; }