diff --git a/libmath/README.md b/libmath/README.md
index aefba2b..bc1f919 100644
--- a/libmath/README.md
+++ b/libmath/README.md
@@ -15,6 +15,7 @@ We support the following functions and special functions:
 - `++factorial`, $!$ factorial
 - `++abs`, $\text{abs}$
 - `++exp`, $\exp$
+- `++expm1`, $\exp - 1$
 - `++sin`, $\sin$
 - `++cos`, $\cos$
 - `++tan`, $\tan$
@@ -35,9 +36,9 @@ Logical functions:
 - `++gte`, $\geq$ (also `++geq`)
 - `++equ`, $=$
 - `++neq`, $\neq$
-- `is-close`
-- `all-close`
-- `is-int`
+- `++is-close`
+- `++all-close`
+- `++is-int`
 
 Constants (to machine accuracy):
 
@@ -67,3 +68,200 @@ It would be nice to have the following special functions as well:
 We do not envision including the Bessel functions and other more abstruse functions.
 
 We use naïve algorithms which are highly reproducible.  We special-case some arguments to make them tractable without catastrophic cancellation.
+
+---
+
+# `/lib/unum` for Urbit
+
+A library for universal numbers (posits, quires, and valids) per the [2022 Posit Standard](https://posithub.org/docs/posit_standard-2.pdf) (Posit Working Group, John Gustafson chair).
+
+We implement the three standard precisions:
+
+- $\text{posit}\langle 8,2\rangle$
+- $\text{posit}\langle 16,2\rangle$
+- $\text{posit}\langle 32,2\rangle$
+
+> **Standard, not legacy.**  The 2022 Posit Standard fixes the exponent size at **`es = 2` for every width** (§2 defines the exponent field as a 2-bit unsigned integer).  This differs from the original 2017 draft (and from SoftPosit's *fast* `p8`/`p16` types), which scaled `es` with width as `posit<8,0>`, `posit<16,1>`, `posit<32,2>`.  Only `posit32` coincides between the two conventions; `posit8` and `posit16` have different bit layouts.  We target the standard.  The reference oracle for 8- and 16-bit posits is therefore SoftPosit's `pX2` (es=2 at any width) path, *not* the fast `p8`/`p16` types; `p32` is used directly.
+
+##  Format and encoding
+
+A posit of precision $n$ has four bit-fields, most-significant first (§3.3):
+
+| field | width | meaning |
+|---|---|---|
+| sign $S$ | 1 bit | integer $s \in \{0,1\}$; implicit value $1-3s$ (so $+1$ or $-2$) |
+| regime $R$ | $k$ bits | run of bits equal to $R_0$, terminated by $\overline{R_0}$; signed integer $r = -k$ if $R_0=0$, else $r = k-1$ |
+| exponent $E$ | 2 bits | unsigned $e \in \{0,1,2,3\}$ (`es = 2`); may be truncated past the LSB, then treated as 0 |
+| fraction $F$ | up to $\max(0,n-5)$ bits | unsigned $f = F / 2^m$, $0 \le f < 1$; trailing truncated bits are 0 |
+
+The represented value (with `useed` $= 2^{2^{es}} = 16$, so the regime contributes $4r$ to the power of two) is:
+
+$$p = \bigl((1-3s) + f\bigr) \times 2^{(1-2s)\,(4r + e + s)}$$
+
+**Exceptions** (all bits except $S$ are zero): $S=0 \Rightarrow$ posit $0$; $S=1 \Rightarrow$ **NaR** (Not a Real — the single non-real value, with bit pattern equal to the most-negative two's-complement integer, $1000\ldots0$).
+
+Key constants per width (§3, Table 1; $n$ = bit width):
+
+| property | posit8 | posit16 | posit32 | $\text{posit}n$ |
+|---|---|---|---|---|
+| fraction length | 0–3 | 0–11 | 0–27 | $0$–$\max(0,n-5)$ |
+| $\textit{minPos}$ | $2^{-24}$ | $2^{-56}$ | $2^{-120}$ | $2^{-4n+8}$ |
+| $\textit{maxPos}$ | $2^{24}$ | $2^{56}$ | $2^{120}$ | $2^{4n-8}$ |
+| $\textit{pIntMax}$ | $16$ | $1024$ | $8388608$ | $2^{\lceil 4(n-3)/5\rceil}$ |
+| quire bits | 128 | 256 | 512 | $16n$ |
+| decimals to round-trip | 2 | 5 | 10 | — |
+
+$\textit{minPos} = 1/\textit{maxPos}$, and every posit value is an integer multiple of $\textit{minPos}$.  $\textit{pIntMax}$ is the largest integer all of whose predecessors are exactly representable (so posit8 represents every integer only up to 16).
+
+### Rounding
+
+Posits have exactly **one** rounding mode (§4.1): round-to-nearest, **ties-to-even**, and **saturating** — a magnitude above $\textit{maxPos}$ rounds to $\pm\textit{maxPos}$ and a nonzero magnitude below $\textit{minPos}$ rounds to $\pm\textit{minPos}$.  Posits never round up to NaR nor down to zero.  Fused operations (`++fmm`, `++rsqrt`, `++exp-minus-1`, `++hypot`, …) are evaluated exactly and rounded once.
+
+### Comparisons
+
+Posit ordering is **identical to two's-complement signed-integer ordering of the raw bits** (§5.3), so comparisons need no decoding — a single signed compare suffices.  NaR shares the bit pattern of the most-negative integer, so it compares less than every real posit; `NaR == NaR` is true and `++sign` of NaR is NaR.
+
+### Quire
+
+The quire is a fixed-point exact accumulator of $16n$ bits (§3.4): sign (1) · carry guard (31) · integer part ($8n-16$) · fraction part ($8n-16$).  Its value is $2^{16-8n}$ times the two's-complement integer formed by all bits; $S=1$ with all other bits zero is NaR.  The quire makes dot products and sums of up to $\sim 2^{23+4n}$ terms exact before a single final rounding — the core reason posits beat floats for linear algebra.
+
+### Auras
+
+| aura | meaning | width |
+|---|---|---|
+| `@rpb` `@rph` `@rps` `@rpd` | posit | byte (8), half (16), single (32), double (64) |
+| `@rqb` `@rqh` `@rqs` | quire | for posit8 / posit16 / posit32 |
+| `@rvb` `@rvh` `@rvs` | valid (interval) | byte / half / single |
+
+The `@rq*` quire auras nest under `@rq` (quad-precision float) by Hoon's prefix-nesting rule; this overlap is accepted intentionally.  There is currently **no literal syntax or pretty-printer** for posit auras — values are written as bit-casts, e.g. `` `@rpb`0b100.0000 `` for $1.0$.  A decimal printer (emitting the §6.3 minimum significant digits: 2/5/10/21 for posit8/16/32/64) would be an *optional local runtime patch*, decoupled from this library, with no upstream-timing commitment.
+
+### Implemented
+
+`lib/unum.hoon` implements the `es = 2` layout above as a single generic core `++pp` (keyed on `bloq`), specialized into `++rpb` / `++rph` / `++rps` / `++rpd` / `++rpq` (posit8/16/32/64/128).  The g-layer record `+$up` mirrors the standard library float `+$fn`.  Each width exposes:
+
+- **decode / encode** — `++sea` (`@` → `+$up`), `++bit` (`+$up` → `@`, round-to-nearest-even, saturating)
+- **constants** — `++zero` `++nar` `++one` `++maxpos` `++minpos` `++huge` `++tiny`, and `++pi` `++tau` `++e` `++phi` `++sqt2` `++invsqt2` `++log2` `++invlog2` `++log10` (correctly rounded at every width)
+- **comparison / sign** — `++gth` `++lth` `++gte` `++lte` `++equ` `++neq`, `++neg` `++abs` `++sgn`
+- **arithmetic** — `++add` `++sub` `++mul` `++div` (correctly rounded), `++fma` (fused multiply-add), `++sqt` (square root)
+- **rounding** — `++round` with `++rnd` (nearest-even) / `++flr` (floor) / `++cel` (ceil)
+- **integer conversion** — `++sun` (`@u`→), `++san` (`@s`→), `++toi` (→`(unit @s)`)
+- **IEEE-754 conversion** — `++to-rh` `++to-rs` `++to-rd` `++to-rq` and `++from-rh` `++from-rs` `++from-rd` `++from-rq`, value-based across *any* posit/float width pair
+- **quire** (the `16n`-bit exact accumulator) — `++p-to-q` `++q-to-p` `++q-mul-add` `++q-mul-sub` `++q-add-p` `++q-sub-p` `++q-add-q` `++q-sub-q` `++q-negate`, and `++fdp` (fused dot product, single rounding)
+- **elementary** — `++exp` `++sin` `++cos` `++tan` `++pow-n` `++log` `++log-2` `++log-10` `++pow` `++is-close` (naive Taylor series in the `/lib/math` style: reproducible, accurate near 0, not range-reduced)
+
+Arithmetic is verified against SoftPosit (the reference C implementation, via its Python wrapper): exhaustively over all posit8 pairs and sampled at posit16/32, with the offline harness in `tools/posit_check.py`; the on-ship suite is `tests/lib/unum-core` and `tests/lib/unum-fns`.
+
+### Not yet implemented
+
+- the standard-name alias interface (below): `++negate` `++addition` `++compare-less` `++sin-pi` `++compound` `++root-n` `++fmm` `++hypot` `++arctan2` etc., and the inverse / hyperbolic / `*-plus-1` / `*-minus-1` elementary functions
+- `++next` / `++prior` / `++nearest-int` / `++ceil` / `++floor` under their standard names (the behaviors exist as `++rnd`/`++flr`/`++cel`)
+- valids (the interval unum class, `@rv*`)
+- jets (the library is pure Hoon; SoftPosit's C is the spec for a future jet)
+
+##  Posit Standard Compliance (planned alias layer)
+
+The following is the *planned* second interface for `/lib/unum`: standard-named aliases over the implemented operations above, plus the not-yet-written functions.  One interface hews to the `/lib/math` and `/lib/saloon` conventions; this one aliases in the 2022 Posit Standard names, slightly modified to adhere to Hoon name requirements.
+
+### Basic functions of one posit value argument
+
+- `++negate` ← `(sub 0 val)`
+- `++abs` ← no change
+- `++sign` ← `++sgn`
+- `++nearest-int`
+- `++ceil`
+- `++floor`
+- `++next`
+- `++prior`
+
+### Comparison functions of two posit value arguments
+
+- `++compare-equal` ← `++equ`
+- `++compare-not-equal` ← `!(equ val)`
+- `++compare-greater` ← `++gth`
+- `++compare-greater-equal` ← `++gte`
+- `++compare-less` ← `++lth`
+- `++compare-less-equal` ← `++lte`
+
+### Arithmetic functions of two posit value arguments
+
+- `++addition` ← `++add`
+- `++subtraction` ← `++sub`
+- `++multiplication` ← `++mul`
+- `++division` ← `++div`
+
+### Elementary functions of one posit value argument
+
+- `++sqrt` ← no change
+- `++rsqrt` ← TODO
+- `++exp` ← no change
+- `++exp-minus-1` ← `++expm1`
+- `++exp2` ← no change
+- `++exp2-minus-1` ← `++exp2m1`
+- `++exp10` ← no change
+- `++exp10-minus-1` ← `++exp10m1`
+- `++log` ← no change
+- `++log-plus-1` ← `++logp1`
+- `++log2` ← no change
+- `++log2-plus-1` ← `++log2p1`
+- `++log10` ← no change
+- `++log10-plus-1` ← `++log10p1`
+- `++sin` ← no change
+- `++sin-pi` ← `(sin (mul pi val))`
+- `++cos` ← no change
+- `++cos-pi` ← `(cos (mul pi val))`
+- `++tan` ← no change
+- `++tan-pi` ← `(tan (mul pi val))`
+- `++arcsin` ← no change
+- `++arcsin-pi` ← `(arcsin (div val pi))`
+- `++arccos` ← no change
+- `++arccos-pi` ← `(arccos (div val pi))`
+- `++arctan` ← no change
+- `++arctan-pi` ← `(arctan (div val pi))`
+- `++sinh` ← no change
+- `++cosh` ← no change
+- `++tanh` ← no change
+- `++arcsinh` ← no change
+- `++arccosh` ← no change
+- `++arctanh` ← no change
+
+### Elementary functions of two posit value arguments
+
+- `++hypot` ← `(sqt (mul val-1 val-1) (mul val-2 val-2))`
+- `++pow` ← no change
+- `++arctan2` ← ??? complex
+- `++arctan2-pi` ← `(div (arctan2 val) pi)`
+
+### Functions of three posit value arguments
+
+- `++fmm` ← `:(mul val-1 val-2 val-3)`
+
+### Functions of one posit value argument and one integer argument
+
+- `++compound` ← `(pow (add val 1) int)`
+- `++root-n` ← `(pow val (div 1 int))`
+
+### Functions involving quire value arguments
+
+- `++p-to-q`
+- `++q-negate`
+- `++q-abs`
+- `++q-add-p`
+- `++q-sub-p`
+- `++q-add-q`
+- `++q-sub-q`
+- `++q-mul-add`
+- `++q-mul-sub`
+- `++q-to-p`
+
+### Conversions between different precisions
+
+- `++p8-to-16`
+- `++p8-to-32`
+- `++p16-to-8`
+- `++p16-to-32`
+- `++p32-to-8`
+- `++p32-to-16`
+
+### Conversions between posit format and decimal format
+
+### Conversions between posit format and IEEE 754 format
diff --git a/libmath/desk/lib/twoc.hoon b/libmath/desk/lib/twoc.hoon
index b07c3b7..9ddc40e 100644
--- a/libmath/desk/lib/twoc.hoon
+++ b/libmath/desk/lib/twoc.hoon
@@ -56,7 +56,7 @@
   ++  overflow
     |=  [a=@ b=@ c=@]
     ?|  &(=(0 (msb c)) =(1 (msb a)) =(1 (msb b)))
-        &(=(1 (msb c)) =(0 (msb a)) =(0 (msb a)))
+        &(=(1 (msb c)) =(0 (msb a)) =(0 (msb b)))
     ==
   ::
   ++  mul
@@ -99,6 +99,8 @@
     ::  if signs same, use the default gth
     (^gth a b)
   ::
-  ++  lth  |=([a=@ b=@] !(gth a b))
+  ++  lth  |=([a=@ b=@] (gth b a))
+  ++  lte  |=([a=@ b=@] !(gth a b))
+  ++  gte  |=([a=@ b=@] !(gth b a))
   --
 --
\ No newline at end of file
diff --git a/libmath/desk/lib/unum.hoon b/libmath/desk/lib/unum.hoon
new file mode 100644
index 0000000..bca01ee
--- /dev/null
+++ b/libmath/desk/lib/unum.hoon
@@ -0,0 +1,504 @@
+/+  twoc   :: two's-complement helpers (sign, comparison) shared with numerics
+  ::
+::::  Universal numbers (unums), Type III: posits, quires, valids
+::
+::  Per the 2022 Posit Standard (Posit Working Group, John Gustafson chair):
+::  https://posithub.org/docs/posit_standard-2.pdf
+::
+::  We represent unums using Hoon auras at four bitwidths:
+::  - @rpb @rph @rps @rpd @rpq  :: posits  (byte/half/single/double/quad)
+::  - @rqb @rqh @rqs            :: quires
+::  - @rvb @rvh @rvs            :: valids  (not yet implemented)
+::
+::  STANDARD, NOT LEGACY.  The 2022 standard fixes the exponent size at
+::  es = 2 for every width (the exponent field is a 2-bit unsigned integer,
+::  0..3), so useed = 2^2^es = 16.  This differs from the 2017 draft (and
+::  SoftPosit's fast p8/p16 types) which scaled es with width.  Only posit32
+::  coincides between the two.  We target the standard.
+::
+::  A posit of precision n has, most-significant first:
+::  - sign     S  (1 bit)              s in {0,1}; implicit value 1-3s
+::  - regime   R  (k+1 bits)           run of R0 bits, terminated by ~R0;
+::                                     r = -k if R0=0, else r = k-1
+::  - exponent E  (2 bits, truncable)  e in {0,1,2,3}
+::  - fraction F  (rest, truncable)    f = F / 2^m, 0 <= f < 1
+::
+::  value:  p = ((1-3s) + f) * 2^((1-2s)*(4r + e + s))
+::
+::  Exceptions: all bits but S zero -> S=0 is posit 0, S=1 is NaR.
+::
+::  NB: this core defines posit add/sub/mul/div, which shadow the stdlib
+::  gates of the same name.  Internal integer arithmetic therefore uses the
+::  ^-prefixed forms (^add/^sub/^mul/^div) to reach the standard library.
+::
+|%
+::  G-layer (decoded) representation of a posit, mirroring the stdlib float +$fn
+::  (`[%f s=? e=@s a=@u]`):  value = (sign) a * 2^e, with a an integer
+::  significand (the hidden 1 included) and e a signed binary exponent.
+::
+::  s=%.y is non-negative (the +$si convention), so value is
+::  ?:(s +1 -1) * a * 2^e.
+::
++$  up
+  $%  [%p s=? e=@s a=@u]   :: real posit
+      [%z ~]              :: zero
+      [%n ~]              :: Not a Real (NaR)
+  ==
+::  Type III Unum Quire: a fixed-point exact accumulator of 16n bits (§3.4):
+::  sign (1) . carry guard (31) . integer (8n-16) . fraction (8n-16).
+::
++$  uq
+  $%  $:  %q
+          s=?      :: sign
+          c=@      :: carry guard, 31 bits
+          i=@      :: integer part, 8n-16 bits
+          f=@      :: fractional part, 8n-16 bits
+      ==
+      [%n ~]       :: NaR
+  ==
+::  Generic posit core, parameterized by bloq (log2 of the bitwidth).
+::
+::  Specialize with %*: posit8 is bloq=3 (n=8), posit16 bloq=4, posit32 bloq=5.
+::
+++  pp
+  |_  =bloq
+  ++  n  (bex bloq)
+  ++  es  2
+  ++  useed  16
+  ++  msk  (dec (bex n))
+  ++  zero    `@`0
+  ++  nar     (bex (dec n))
+  ++  maxpos  (dec (bex (dec n)))
+  ++  minpos  `@`1
+  ++  huge  maxpos
+  ++  tiny  minpos
+  ++  one  (bit [%p %.y --0 1])
+  ::  Mathematical constants (Q2.52 fixed-point hex of the value, rounded by
+  ::  +bit at each width).  Cross-checked vs SoftPosit (pX2) and a reference.
+  ++  pi       (bit [%p %.y -52 0x32.43f6.a888.5a31])   ::  3.14159265358979
+  ++  tau      (bit [%p %.y -52 0x64.87ed.5110.b461])   ::  6.28318530717959
+  ++  e        (bit [%p %.y -52 0x2b.7e15.1628.aed3])   ::  2.71828182845905
+  ++  phi      (bit [%p %.y -52 0x19.e377.9b97.f4a8])   ::  1.61803398874989
+  ++  sqt2     (bit [%p %.y -52 0x16.a09e.667f.3bcd])   ::  1.41421356237310
+  ++  invsqt2  (bit [%p %.y -52 0xb.504f.333f.9de6])    ::  0.70710678118655
+  ++  log2     (bit [%p %.y -52 0xb.1721.7f7d.1cf8])    ::  0.69314718055995
+  ++  invlog2  (bit [%p %.y -52 0x17.1547.652b.82fe])   ::  1.44269504088896
+  ++  log10    (bit [%p %.y -52 0x24.d763.776a.aa2b])   ::  2.30258509299405
+  ::    +sea:  @ -> $up   (decode an n-bit posit into its g-layer form)
+  ++  sea
+    |=  p=@
+    ^-  up
+    =.  p  (dis msk p)
+    ?:  =(0 p)    [%z ~]
+    ?:  =(nar p)  [%n ~]
+    =/  neg  =(1 (cut 0 [(dec n) 1] p))
+    =/  mag  ?:(neg (^sub (bex n) p) p)
+    =/  pw   (dec n)
+    =/  r0   (cut 0 [(dec pw) 1] mag)
+    =/  k=@  1
+    |-  ^-  up
+    ?:  =(k pw)
+      =/  r  ?:(=(1 r0) (sun:si (dec k)) (dif:si --0 (sun:si k)))
+      [%p !neg (pro:si r --4) 1]
+    =/  nb  (cut 0 [(^sub (dec pw) k) 1] mag)
+    ?:  =(nb r0)
+      $(k +(k))
+    =/  r       ?:(=(1 r0) (sun:si (dec k)) (dif:si --0 (sun:si k)))
+    =/  remwid  (^sub pw +(k))
+    =/  rem     (dis (dec (bex remwid)) mag)
+    =/  elo  ?:  (^gte remwid 2)
+               (rsh [0 (^sub remwid 2)] rem)
+             ?:(=(1 remwid) (^mul 2 rem) 0)
+    =/  fw    ?:((^gte remwid 2) (^sub remwid 2) 0)
+    =/  frac  (dis (dec (bex fw)) rem)
+    =/  x  (sum:si (pro:si r --4) (sun:si elo))
+    =/  a  (^add (bex fw) frac)
+    [%p !neg (dif:si x (sun:si fw)) a]
+  ::    +bit:  $up -> @   (encode, round-to-nearest-even, saturating)
+  ++  bit
+    |=  =up
+    ^-  @
+    ?:  ?=(%z -.up)  zero
+    ?:  ?=(%n -.up)  nar
+    ?>  ?=(%p -.up)
+    ?:  =(0 a.up)  zero
+    =/  neg   !s.up
+    =/  lead  (dec (met 0 a.up))
+    =/  x     (sum:si e.up (sun:si lead))
+    =/  frac  (dis (dec (bex lead)) a.up)
+    =/  rel
+      =/  ax  (abs:si x)
+      ?:  (syn:si x)
+        [(sun:si (^div ax 4)) (mod ax 4)]
+      =/  q  (^div ax 4)
+      =/  m  (mod ax 4)
+      ?:  =(0 m)
+        [(dif:si --0 (sun:si q)) 0]
+      [(dif:si --0 (sun:si +(q))) (^sub 4 m)]
+    =/  r=@s   -.rel
+    =/  elo=@  +.rel
+    ?:  (gte-s r (sun:si (^sub n 2)))    (smag neg maxpos)
+    ?:  (lte-s r (dif:si --0 (sun:si (dec n))))  (smag neg minpos)
+    =/  rmag  (abs:si r)
+    =/  rr
+      ?:  (syn:si r)
+        [(lsh [0 1] (dec (bex +(rmag)))) (^add rmag 2)]
+      [1 (^add rmag 1)]
+    =/  regval=@  -.rr
+    =/  regwid=@  +.rr
+    =/  totw  (^add (^add regwid 2) lead)
+    =/  pay   (con (lsh [0 (^add 2 lead)] regval) (con (lsh [0 lead] elo) frac))
+    =/  pw    (dec n)
+    ?:  (^lte totw pw)
+      (smag neg (lsh [0 (^sub pw totw)] pay))
+    =/  sh      (^sub totw pw)
+    =/  keep    (rsh [0 sh] pay)
+    =/  guard   (cut 0 [(dec sh) 1] pay)
+    =/  sticky  ?:(=(0 (dis (dec (bex (dec sh))) pay)) 0 1)
+    =/  lsbit   (dis 1 keep)
+    =/  roundup  &(=(1 guard) |(=(1 sticky) =(1 lsbit)))
+    =/  mag      ?:(roundup +(keep) keep)
+    =?  mag  (^gth mag maxpos)  maxpos
+    (smag neg mag)
+  ++  smag
+    |=  [neg=? mag=@]
+    ^-  @
+    ?.  neg  mag
+    (dis msk (^sub (bex n) mag))
+  ++  gte-s  |=([a=@s b=@s] ^-(? !=(-1 (cmp:si a b))))
+  ++  lte-s  |=([a=@s b=@s] ^-(? !=(--1 (cmp:si a b))))
+  ::  Comparisons (= two's-complement integer ordering of the raw bits, sec 5.3).
+  ++  gth  |=([a=@ b=@] ^-(? (~(gth twoc:twoc bloq) a b)))
+  ++  lth  |=([a=@ b=@] ^-(? (~(lth twoc:twoc bloq) a b)))
+  ++  gte  |=([a=@ b=@] ^-(? (~(gte twoc:twoc bloq) a b)))
+  ++  lte  |=([a=@ b=@] ^-(? (~(lte twoc:twoc bloq) a b)))
+  ++  equ  |=([a=@ b=@] ^-(? =(a b)))
+  ++  neq  |=([a=@ b=@] ^-(? !=(a b)))
+  ++  neg  |=(a=@ ^-(@ (dis msk (^sub (bex n) a))))
+  ++  abs  |=(a=@ ^-(@ ?:(=(1 (~(msb twoc:twoc bloq) a)) (neg a) a)))
+  ++  sgn
+    |=  a=@
+    ^-  @
+    ?:  =(zero a)  zero
+    ?:  =(nar a)   nar
+    ?:  =(1 (~(msb twoc:twoc bloq) a))  (neg one)
+    one
+  ::  Arithmetic (sec 5.4); exact g-layer combine, single round via +bit.
+  ++  mul
+    |=  [a=@ b=@]
+    ^-  @
+    =/  ua  (sea a)
+    =/  ub  (sea b)
+    ?:  |(?=(%n -.ua) ?=(%n -.ub))  nar
+    ?:  |(?=(%z -.ua) ?=(%z -.ub))  zero
+    ?>  ?=(%p -.ua)
+    ?>  ?=(%p -.ub)
+    (bit [%p =(s.ua s.ub) (sum:si e.ua e.ub) (^mul a.ua a.ub)])
+  ++  add
+    |=  [a=@ b=@]
+    ^-  @
+    =/  ua  (sea a)
+    =/  ub  (sea b)
+    ?:  |(?=(%n -.ua) ?=(%n -.ub))  nar
+    ?:  ?=(%z -.ua)  b
+    ?:  ?=(%z -.ub)  a
+    ?>  ?=(%p -.ua)
+    ?>  ?=(%p -.ub)
+    =/  emin  ?:(=(-1 (cmp:si e.ua e.ub)) e.ua e.ub)
+    =/  s1  (lsh [0 (abs:si (dif:si e.ua emin))] a.ua)
+    =/  s2  (lsh [0 (abs:si (dif:si e.ub emin))] a.ub)
+    ?:  =(s.ua s.ub)
+      (bit [%p s.ua emin (^add s1 s2)])
+    ?:  (^gth s1 s2)
+      (bit [%p s.ua emin (^sub s1 s2)])
+    ?:  (^gth s2 s1)
+      (bit [%p s.ub emin (^sub s2 s1)])
+    zero
+  ++  sub  |=([a=@ b=@] ^-(@ (add a (neg b))))
+  ++  div
+    |=  [a=@ b=@]
+    ^-  @
+    =/  ua  (sea a)
+    =/  ub  (sea b)
+    ?:  |(?=(%n -.ua) ?=(%n -.ub))  nar
+    ?:  ?=(%z -.ub)  nar
+    ?:  ?=(%z -.ua)  zero
+    ?>  ?=(%p -.ua)
+    ?>  ?=(%p -.ub)
+    =/  g    (^add n n)
+    =/  num  (lsh [0 g] a.ua)
+    =/  q    (^div num a.ub)
+    =/  qs   ?:(=(0 (mod num a.ub)) q (con q 1))
+    =/  eo   (dif:si (dif:si e.ua e.ub) (sun:si g))
+    (bit [%p =(s.ua s.ub) eo qs])
+  ::  Elementary and rounding ops.
+  ++  isqt
+    |=  x=@
+    ^-  @
+    ?:  =(0 x)  0
+    =/  r  (bex (^div (^add (met 0 x) 1) 2))
+    |-  ^-  @
+    =/  nr  (^div (^add r (^div x r)) 2)
+    ?:  (^gte nr r)
+      |-  ^-  @
+      ?:  (^gth (^mul r r) x)  $(r (dec r))
+      r
+    $(r nr)
+  ++  sqt
+    |=  p=@
+    ^-  @
+    =/  u  (sea p)
+    ?:  ?=(%n -.u)  nar
+    ?:  ?=(%z -.u)  zero
+    ?>  ?=(%p -.u)
+    ?.  s.u  nar
+    =/  odd  =(1 (dis 1 (abs:si e.u)))
+    =/  aa   ?:(odd (lsh [0 1] a.u) a.u)
+    =/  ee   ?:(odd (dif:si e.u --1) e.u)
+    =/  g    (^add n n)
+    =/  m    (lsh [0 (^mul 2 g)] aa)
+    =/  s    (isqt m)
+    =/  sx   ?:(=(m (^mul s s)) s (con s 1))
+    (bit [%p %.y (dif:si (fra:si ee --2) (sun:si g)) sx])
+  ++  round
+    |=  mode=?(%near %down %up)
+    |=  p=@
+    ^-  @
+    =/  u  (sea p)
+    ?.  ?=(%p -.u)  p
+    ?:  (gte-s e.u --0)  p
+    =/  sh    (abs:si e.u)
+    =/  hi    (rsh [0 sh] a.u)
+    =/  rem   (dis (dec (bex sh)) a.u)
+    =/  half  (bex (dec sh))
+    =?  hi  &(?=(%near mode) |((^gth rem half) &(=(rem half) =(1 (dis 1 hi)))))
+      +(hi)
+    =?  hi  &(?=(%down mode) !s.u !=(0 rem))  +(hi)
+    =?  hi  &(?=(%up mode) s.u !=(0 rem))     +(hi)
+    ?:  =(0 hi)  zero
+    (bit [%p s.u --0 hi])
+  ++  rnd  (round %near)
+  ++  flr  (round %down)
+  ++  cel  (round %up)
+  ++  sun  |=(v=@ ^-(@ ?:(=(0 v) zero (bit [%p %.y --0 v]))))
+  ++  san
+    |=  v=@s
+    ^-  @
+    =+  [sn mg]=(old:si v)
+    ?:  =(0 mg)  zero
+    (bit [%p sn --0 mg])
+  ++  toi
+    |=  p=@
+    ^-  (unit @s)
+    =/  u  (sea p)
+    ?:  ?=(%n -.u)  ~
+    =/  r   (rnd p)
+    =/  ur  (sea r)
+    ?:  ?=(%z -.ur)  `--0
+    ?>  ?=(%p -.ur)
+    =/  sh   (abs:si e.ur)
+    =/  mag  ?:((gte-s e.ur --0) (lsh [0 sh] a.ur) (rsh [0 sh] a.ur))
+    `(new:si s.ur mag)
+  ++  fma
+    |=  [a=@ b=@ c=@]
+    ^-  @
+    =/  ua  (sea a)
+    =/  ub  (sea b)
+    =/  uc  (sea c)
+    ?:  |(?=(%n -.ua) ?=(%n -.ub) ?=(%n -.uc))  nar
+    ?:  |(?=(%z -.ua) ?=(%z -.ub))  c
+    ?>  ?=(%p -.ua)
+    ?>  ?=(%p -.ub)
+    =/  ps  =(s.ua s.ub)
+    =/  pe  (sum:si e.ua e.ub)
+    =/  pa  (^mul a.ua a.ub)
+    ?:  ?=(%z -.uc)  (bit [%p ps pe pa])
+    ?>  ?=(%p -.uc)
+    =/  emin  ?:(=(-1 (cmp:si pe e.uc)) pe e.uc)
+    =/  s1  (lsh [0 (abs:si (dif:si pe emin))] pa)
+    =/  s2  (lsh [0 (abs:si (dif:si e.uc emin))] a.uc)
+    ?:  =(ps s.uc)    (bit [%p ps emin (^add s1 s2)])
+    ?:  (^gth s1 s2)  (bit [%p ps emin (^sub s1 s2)])
+    ?:  (^gth s2 s1)  (bit [%p s.uc emin (^sub s2 s1)])
+    zero
+  ::
+  ::  Transcendental / elementary functions, in the naive, reproducible
+  ::  Taylor-series style of /lib/math: fixed term counts, posit arithmetic
+  ::  throughout (the loop counters use ^-escaped stdlib ops).  NOT correctly
+  ::  rounded and accurate only near 0 (no range reduction), matching libmath;
+  ::  the running sums could later move to the quire for exact accumulation.
+  ::
+  ::    +exp:  @ -> @   (e^x = sum x^k/k!)
+  ++  exp
+    |=  x=@
+    ^-  @
+    =/  sum   one
+    =/  term  one
+    =/  nn=@  1
+    |-
+    ?:  (^gth nn 20)  sum
+    =.  term  (mul term (div x (sun nn)))
+    =.  sum   (add sum term)
+    $(nn +(nn))
+  ::    +sin:  @ -> @   (sum (-1)^k x^(2k+1)/(2k+1)!)
+  ++  sin
+    |=  x=@
+    ^-  @
+    =/  term  x
+    =/  sum   x
+    =/  nn=@  1
+    |-
+    ?:  (^gth nn 20)  sum
+    =/  k  (^mul 2 nn)
+    =.  term  (neg (mul term (div (mul x x) (mul (sun k) (sun +(k))))))
+    =.  sum   (add sum term)
+    $(nn +(nn))
+  ::    +cos:  @ -> @   (sum (-1)^k x^2k/(2k)!)
+  ++  cos
+    |=  x=@
+    ^-  @
+    =/  term  one
+    =/  sum   one
+    =/  nn=@  1
+    |-
+    ?:  (^gth nn 20)  sum
+    =/  k  (^mul 2 nn)
+    =.  term  (neg (mul term (div (mul x x) (mul (sun (dec k)) (sun k)))))
+    =.  sum   (add sum term)
+    $(nn +(nn))
+  ::    +tan:  @ -> @
+  ++  tan  |=(x=@ ^-(@ (div (sin x) (cos x))))
+  ::    +pow-n:  @ -> @u -> @   (integer power by repeated multiplication)
+  ++  pow-n
+    |=  [x=@ p=@u]
+    ^-  @
+    =/  res  one
+    |-
+    ?:  =(0 p)  res
+    $(p (dec p), res (mul res x))
+  ::    +log:  @ -> @   (ln, via 2*atanh((x-1)/(x+1)))
+  ++  log
+    |=  x=@
+    ^-  @
+    =/  y     (div (sub x one) (add x one))
+    =/  y2    (mul y y)
+    =/  sum   y
+    =/  term  y
+    =/  nn=@  1
+    |-
+    ?:  (^gth nn 30)  (mul (sun 2) sum)
+    =.  term  (mul term y2)
+    =/  coef  (div one (sun +((^mul 2 nn))))
+    =.  sum   (add sum (mul coef term))
+    $(nn +(nn))
+  ::    +log-2 / +log-10:  base-2 / base-10 logarithm
+  ++  log-2   |=(x=@ ^-(@ (div (log x) log2)))
+  ++  log-10  |=(x=@ ^-(@ (div (log x) log10)))
+  ::    +pow:  @ -> @ -> @   (x^y = exp(y * log x))
+  ++  pow  |=([x=@ y=@] ^-(@ (exp (mul y (log x)))))
+  ::    +is-close:  @ -> @ -> @ -> ?   (|a - b| <= tol)
+  ++  is-close  |=([a=@ b=@ tol=@] ^-(? (lte (abs (sub a b)) tol)))
+  ::
+  ::  Quire (sec 3.4 / 5.11): a 16n-bit fixed-point exact accumulator, held
+  ::  as a raw two's-complement atom.  Sums of products accumulate exactly and
+  ::  round only once, via +q-to-p -- the basis of the fused dot product +fdp,
+  ::  which is why posits beat floats for linear algebra.  q-NaR is the most
+  ::  negative pattern.  Verified against SoftPosit qX2 over random vectors.
+  ::
+  ++  qbits   (^mul 16 n)
+  ++  qscale  (^sub (^mul 8 n) 16)
+  ++  qmod    (bex qbits)
+  ++  q-nar   (bex (dec qbits))
+  ++  q-zero  `@`0
+  ++  p-to-q
+    |=  p=@
+    ^-  @
+    =/  u  (sea p)
+    ?:  ?=(%n -.u)  q-nar
+    ?:  ?=(%z -.u)  q-zero
+    ?>  ?=(%p -.u)
+    =/  m  (lsh [0 (abs:si (sum:si e.u (sun:si qscale)))] a.u)
+    ?:(s.u m (^sub qmod m))
+  ++  q-to-p
+    |=  q=@
+    ^-  @
+    =.  q  (dis (dec qmod) q)
+    ?:  =(q-nar q)  nar
+    =/  neg  =(1 (cut 0 [(dec qbits) 1] q))
+    =/  acc  ?:(neg (^sub qmod q) q)
+    ?:  =(0 acc)  zero
+    (bit [%p !neg (dif:si --0 (sun:si qscale)) acc])
+  ++  q-mul-add
+    |=  [q=@ a=@ b=@]
+    ^-  @
+    ?:  =(q-nar q)  q-nar
+    =/  ua  (sea a)
+    =/  ub  (sea b)
+    ?:  |(?=(%n -.ua) ?=(%n -.ub))  q-nar
+    ?:  |(?=(%z -.ua) ?=(%z -.ub))  q
+    ?>  ?=(%p -.ua)
+    ?>  ?=(%p -.ub)
+    =/  m   (lsh [0 (abs:si :(sum:si e.ua e.ub (sun:si qscale)))] (^mul a.ua a.ub))
+    =/  qc  ?:(=(s.ua s.ub) m (^sub qmod m))
+    (mod (^add q qc) qmod)
+  ++  q-mul-sub  |=([q=@ a=@ b=@] ^-(@ (q-mul-add q a (neg b))))
+  ++  q-add-p  |=([q=@ p=@] ^-(@ (q-mul-add q p one)))
+  ++  q-sub-p  |=([q=@ p=@] ^-(@ (q-mul-add q (neg p) one)))
+  ++  q-negate  |=(q=@ ^-(@ ?:(=(q-nar q) q-nar (mod (^sub qmod q) qmod))))
+  ++  q-add-q
+    |=  [x=@ y=@]
+    ^-  @
+    ?:  |(=(q-nar x) =(q-nar y))  q-nar
+    (mod (^add x y) qmod)
+  ++  q-sub-q  |=([x=@ y=@] ^-(@ (q-add-q x (q-negate y))))
+  ::    +fdp:  (list @) -> (list @) -> @  (fused dot product, single rounding)
+  ++  fdp
+    |=  [av=(list @) bv=(list @)]
+    ^-  @
+    =|  q=@
+    |-  ^-  @
+    ?~  av  (q-to-p q)
+    ?~  bv  (q-to-p q)
+    $(q (q-mul-add q i.av i.bv), av t.av, bv t.bv)
+  ::
+  ::  IEEE-754 interop (sec 6.5).  Conversion is by VALUE, so a posit of ANY
+  ::  width converts to/from a float of ANY width -- the full matrix.  Posits
+  ::  pack more accuracy per bit (posit16 ~ float32, posit32 ~ float64), so
+  ::  same-width is NOT the meaningful correspondence.  Posit zero <-> float
+  ::  +0; posit NaR <-> float NaN; float +-inf/NaN -> NaR.  +up-to-fn/+fn-to-up
+  ::  bridge the (identical) posit g-layer +$up and the stdlib float +$fn.
+  ::
+  ++  up-to-fn
+    |=  u=up
+    ^-  fn
+    ?:  ?=(%n -.u)  [%n ~]
+    ?:  ?=(%z -.u)  [%f %.y --0 0]
+    [%f s.u e.u a.u]
+  ++  fn-to-up
+    |=  f=fn
+    ^-  up
+    ?.  ?=(%f -.f)  [%n ~]                 :: NaN / +-inf -> NaR
+    ?:  =(0 a.f)  [%z ~]
+    [%p s.f e.f a.f]
+  ::    +to-rh/rs/rd/rq:  this-width posit -> half/single/double/quad float
+  ++  to-rh  |=(p=@ ^-(@rh (bit:rh (up-to-fn (sea p)))))
+  ++  to-rs  |=(p=@ ^-(@rs (bit:rs (up-to-fn (sea p)))))
+  ++  to-rd  |=(p=@ ^-(@rd (bit:rd (up-to-fn (sea p)))))
+  ++  to-rq  |=(p=@ ^-(@rq (bit:rq (up-to-fn (sea p)))))
+  ::    +from-rh/rs/rd/rq:  half/single/double/quad float -> this-width posit
+  ++  from-rh  |=(r=@rh ^-(@ (bit (fn-to-up (sea:rh r)))))
+  ++  from-rs  |=(r=@rs ^-(@ (bit (fn-to-up (sea:rs r)))))
+  ++  from-rd  |=(r=@rd ^-(@ (bit (fn-to-up (sea:rd r)))))
+  ++  from-rq  |=(r=@rq ^-(@ (bit (fn-to-up (sea:rq r)))))
+  --
+::  posit8   ("byte"),   posit<8,2>
+++  rpb  %*(. pp bloq 3)
+::  posit16  ("half"),   posit<16,2>
+++  rph  %*(. pp bloq 4)
+::  posit32  ("single"), posit<32,2>
+++  rps  %*(. pp bloq 5)
+::  posit64  ("double"), posit<64,2>
+++  rpd  %*(. pp bloq 6)
+::  posit128 ("quad"),   posit<128,2>
+++  rpq  %*(. pp bloq 7)
+--
diff --git a/libmath/desk/tests/lib/unum-core.hoon b/libmath/desk/tests/lib/unum-core.hoon
new file mode 100644
index 0000000..6317849
--- /dev/null
+++ b/libmath/desk/tests/lib/unum-core.hoon
@@ -0,0 +1,144 @@
+  ::  /tests/lib/unum-core
+::::
+::    Posits (2022 Posit Standard, es=2) -- decode/encode, constants,
+::    comparison, and core arithmetic.  Split from a single oversized file so
+::    each compiles quickly (cf. the lagoon test-by-category convention).
+::
+::  Heavy exhaustive cross-checks vs SoftPosit run once, offline, in Python
+::  (libmath/tools/posit_check.py).  The on-ship suite is lean: round-trips,
+::  a property sweep, and curated SoftPosit-verified spot values.
+::
+/+  *test,
+    unum
+^|
+|%
+++  test-round-trip-rpb  ^-  tang
+  =|  i=@
+  |-  ^-  tang
+  ?:  =(256 i)  ~
+  =/  rt  (bit:rpb:unum (sea:rpb:unum i))
+  ?:  =(i rt)  $(i +(i))
+  [(cat 3 'rpb round-trip failed at ' (scot %ux i)) $(i +(i))]
+::
+++  test-round-trip-rph  ^-  tang
+  =|  i=@
+  |-  ^-  tang
+  ?:  =(65.536 i)  ~
+  =/  rt  (bit:rph:unum (sea:rph:unum i))
+  ?:  =(i rt)  $(i +(i))
+  [(cat 3 'rph round-trip failed at ' (scot %ux i)) $(i +(i))]
+::
+++  test-values-rpb  ^-  tang
+  ;:  weld
+    %+  expect-eq  !>(`@`0x0)   !>(zero:rpb:unum)
+    %+  expect-eq  !>(`@`0x80)  !>(nar:rpb:unum)
+    %+  expect-eq  !>(`@`0x40)  !>(one:rpb:unum)
+    %+  expect-eq  !>(`@`0x7f)  !>(maxpos:rpb:unum)
+    %+  expect-eq  !>(`@`0x1)   !>(minpos:rpb:unum)
+  ==
+::
+++  test-consts-rpb  ^-  tang
+  ;:  weld
+    %+  expect-eq  !>(`@`0x4d)  !>(pi:rpb:unum)
+    %+  expect-eq  !>(`@`0x55)  !>(tau:rpb:unum)
+    %+  expect-eq  !>(`@`0x4b)  !>(e:rpb:unum)
+    %+  expect-eq  !>(`@`0x45)  !>(phi:rpb:unum)
+    %+  expect-eq  !>(`@`0x43)  !>(sqt2:rpb:unum)
+    %+  expect-eq  !>(`@`0x3b)  !>(invsqt2:rpb:unum)
+    %+  expect-eq  !>(`@`0x3b)  !>(log2:rpb:unum)
+    %+  expect-eq  !>(`@`0x44)  !>(invlog2:rpb:unum)
+    %+  expect-eq  !>(`@`0x49)  !>(log10:rpb:unum)
+  ==
+::
+++  test-consts-rph  ^-  tang
+  ;:  weld
+    %+  expect-eq  !>(`@`0x4c91)  !>(pi:rph:unum)
+    %+  expect-eq  !>(`@`0x5491)  !>(tau:rph:unum)
+    %+  expect-eq  !>(`@`0x4ae0)  !>(e:rph:unum)
+    %+  expect-eq  !>(`@`0x44f2)  !>(phi:rph:unum)
+    %+  expect-eq  !>(`@`0x4350)  !>(sqt2:rph:unum)
+    %+  expect-eq  !>(`@`0x3b50)  !>(invsqt2:rph:unum)
+    %+  expect-eq  !>(`@`0x3b17)  !>(log2:rph:unum)
+    %+  expect-eq  !>(`@`0x438b)  !>(invlog2:rph:unum)
+    %+  expect-eq  !>(`@`0x4936)  !>(log10:rph:unum)
+  ==
+::
+++  test-consts-rps  ^-  tang
+  ;:  weld
+    %+  expect-eq  !>(`@`0x4c90.fdaa)  !>(pi:rps:unum)
+    %+  expect-eq  !>(`@`0x5490.fdaa)  !>(tau:rps:unum)
+    %+  expect-eq  !>(`@`0x4adf.8546)  !>(e:rps:unum)
+    %+  expect-eq  !>(`@`0x44f1.bbce)  !>(phi:rps:unum)
+    %+  expect-eq  !>(`@`0x4350.4f33)  !>(sqt2:rps:unum)
+    %+  expect-eq  !>(`@`0x3b50.4f33)  !>(invsqt2:rps:unum)
+    %+  expect-eq  !>(`@`0x3b17.217f)  !>(log2:rps:unum)
+    %+  expect-eq  !>(`@`0x438a.a3b3)  !>(invlog2:rps:unum)
+    %+  expect-eq  !>(`@`0x4935.d8de)  !>(log10:rps:unum)
+  ==
+::
+++  test-sea-rpb  ^-  tang
+  ;:  weld
+    %+  expect-eq  !>([%z ~])             !>((sea:rpb:unum 0x0))
+    %+  expect-eq  !>([%n ~])             !>((sea:rpb:unum 0x80))
+    %+  expect-eq  !>([%p %.y -3 8])      !>((sea:rpb:unum 0x40))
+    %+  expect-eq  !>([%p %.y -2 8])      !>((sea:rpb:unum 0x48))
+    %+  expect-eq  !>([%p %.y -3 10])     !>((sea:rpb:unum 0x42))
+  ==
+::
+++  test-bit-rpb  ^-  tang
+  ;:  weld
+    %+  expect-eq  !>(`@`0x0)   !>((bit:rpb:unum [%z ~]))
+    %+  expect-eq  !>(`@`0x80)  !>((bit:rpb:unum [%n ~]))
+    %+  expect-eq  !>(`@`0x40)  !>((bit:rpb:unum [%p %.y --0 1]))
+    %+  expect-eq  !>(`@`0x48)  !>((bit:rpb:unum [%p %.y -2 8]))
+    %+  expect-eq  !>(`@`0xc0)  !>((bit:rpb:unum [%p %.n --0 1]))
+  ==
+::
+++  test-compare-rpb  ^-  tang
+  ;:  weld
+    %+  expect-eq  !>(%.y)  !>((lth:rpb:unum 0x38 0x40))
+    %+  expect-eq  !>(%.n)  !>((lth:rpb:unum 0x40 0x38))
+    %+  expect-eq  !>(%.y)  !>((gth:rpb:unum 0x40 0xc0))
+    %+  expect-eq  !>(%.y)  !>((lth:rpb:unum 0x80 0xc0))
+    %+  expect-eq  !>(%.y)  !>((equ:rpb:unum 0x80 0x80))
+    %+  expect-eq  !>(`@`0xc0)  !>((neg:rpb:unum 0x40))
+    %+  expect-eq  !>(`@`0x40)  !>((abs:rpb:unum 0xc0))
+    %+  expect-eq  !>(`@`0xc0)  !>((sgn:rpb:unum 0xa0))
+  ==
+::
+++  test-arith-spot-rpb  ^-  tang
+  ;:  weld
+    %+  expect-eq  !>(`@`0x48)  !>((add:rpb:unum 0x40 0x40))
+    %+  expect-eq  !>(`@`0x40)  !>((add:rpb:unum 0x38 0x38))
+    %+  expect-eq  !>(`@`0x4c)  !>((add:rpb:unum 0x40 0x48))
+    %+  expect-eq  !>(`@`0x48)  !>((sub:rpb:unum 0x4c 0x40))
+    %+  expect-eq  !>(`@`0x54)  !>((mul:rpb:unum 0x48 0x4c))
+    %+  expect-eq  !>(`@`0x38)  !>((div:rpb:unum 0x40 0x48))
+    %+  expect-eq  !>(`@`0x80)  !>((div:rpb:unum 0x40 0x0))
+    %+  expect-eq  !>(`@`0x80)  !>((mul:rpb:unum 0x40 0x80))
+  ==
+::
+++  test-arith-spot-rph  ^-  tang
+  ;:  weld
+    %+  expect-eq  !>(`@`0x4c00)  !>((add:rph:unum 0x4000 0x4800))
+    %+  expect-eq  !>(`@`0x319a)  !>((mul:rph:unum 0x4c00 0x24cd))
+  ==
+::
+++  test-arith-props-rpb  ^-  tang
+  =/  mu  mul:rpb:unum
+  =/  ad  add:rpb:unum
+  =/  ng  neg:rpb:unum
+  =/  on  one:rpb:unum
+  =/  no  (ng on)
+  =|  i=@
+  |-  ^-  tang
+  ?:  =(256 i)  ~
+  =/  a  i
+  =/  b  (mod (add (mul i 181) 67) 256)
+  =/  e1=tang  ?:(=((mu a b) (mu b a)) ~ ~[(cat 3 'mul comm at ' (scot %ux i))])
+  =/  e2=tang  ?:(=((ad a b) (ad b a)) ~ ~[(cat 3 'add comm at ' (scot %ux i))])
+  =/  e3=tang  ?:(=(a (ad a 0x0)) ~ ~[(cat 3 'a+0 at ' (scot %ux i))])
+  =/  e4=tang  ?:(=(a (mu a on)) ~ ~[(cat 3 'a*1 at ' (scot %ux i))])
+  =/  e5=tang  ?:(=((ng a) (mu a no)) ~ ~[(cat 3 'a*-1 at ' (scot %ux i))])
+  :(weld e1 e2 e3 e4 e5 $(i +(i)))
+--
diff --git a/libmath/desk/tests/lib/unum-fns.hoon b/libmath/desk/tests/lib/unum-fns.hoon
new file mode 100644
index 0000000..e980195
--- /dev/null
+++ b/libmath/desk/tests/lib/unum-fns.hoon
@@ -0,0 +1,124 @@
+  ::  /tests/lib/unum-fns
+::::
+::    Posits (2022 Posit Standard, es=2) -- elementary functions, rounding,
+::    integer/IEEE conversions, the quire, and transcendentals.  Split from a
+::    single oversized file so each compiles quickly.
+::
+::  Note: the from-rh/rs/rd/rq gates are typed on the float aura, so their
+::  arguments must be cast (`@rs`0x..) -- a bare 0x.. literal is @ux and will
+::  not nest.  The to-* gates take a bare @, so their literals need no cast.
+::
+/+  *test,
+    unum
+^|
+|%
+++  test-sqt-rpb  ^-  tang
+  ;:  weld
+    %+  expect-eq  !>(`@`0x48)  !>((sqt:rpb:unum 0x50))
+    %+  expect-eq  !>(`@`0x43)  !>((sqt:rpb:unum 0x48))
+    %+  expect-eq  !>(`@`0x80)  !>((sqt:rpb:unum 0xc0))
+    %+  expect-eq  !>(`@`0x0)   !>((sqt:rpb:unum 0x0))
+    %+  expect-eq  !>(`@`0x80)  !>((sqt:rpb:unum 0x80))
+  ==
+::
+++  test-round-rpb  ^-  tang
+  ;:  weld
+    %+  expect-eq  !>(`@`0x40)  !>((rnd:rpb:unum 0x42))
+    %+  expect-eq  !>(`@`0x48)  !>((rnd:rpb:unum 0x4a))
+    %+  expect-eq  !>(`@`0x0)   !>((rnd:rpb:unum 0x38))
+    %+  expect-eq  !>(`@`0x50)  !>((rnd:rpb:unum 0x4e))
+    %+  expect-eq  !>(`@`0x40)  !>((flr:rpb:unum 0x42))
+    %+  expect-eq  !>(`@`0x48)  !>((cel:rpb:unum 0x42))
+    %+  expect-eq  !>(`@`0xb8)  !>((flr:rpb:unum 0xbe))
+    %+  expect-eq  !>(`@`0xc0)  !>((cel:rpb:unum 0xbe))
+  ==
+::
+++  test-convert-rpb  ^-  tang
+  ;:  weld
+    %+  expect-eq  !>(`@`0x4c)  !>((sun:rpb:unum 3))
+    %+  expect-eq  !>(`@`0x0)   !>((sun:rpb:unum 0))
+    %+  expect-eq  !>(`@`0x4c)  !>((san:rpb:unum --3))
+    %+  expect-eq  !>(`@`0xb4)  !>((san:rpb:unum -3))
+    %+  expect-eq  !>(`(unit @s)`[~ --1])  !>((toi:rpb:unum 0x42))
+    %+  expect-eq  !>(`(unit @s)`[~ --4])  !>((toi:rpb:unum 0x4e))
+    %+  expect-eq  !>(`(unit @s)`~)        !>((toi:rpb:unum 0x80))
+    %+  expect-eq  !>(`(unit @s)`[~ --0])  !>((toi:rpb:unum 0x0))
+  ==
+::
+++  test-fma-rpb  ^-  tang
+  ;:  weld
+    %+  expect-eq  !>(`@`0x56)  !>((fma:rpb:unum 0x48 0x4c 0x40))
+    %+  expect-eq  !>(`@`0x80)  !>((fma:rpb:unum 0x48 0x80 0x40))
+  ==
+::
+++  test-quire-rpb  ^-  tang
+  ;:  weld
+    %+  expect-eq  !>(`@`0x42)  !>((q-to-p:rpb:unum (p-to-q:rpb:unum 0x42)))
+    %+  expect-eq  !>(`@`0x38)  !>((q-to-p:rpb:unum (p-to-q:rpb:unum 0x38)))
+    %+  expect-eq  !>(`@`0x4c)
+      !>((q-to-p:rpb:unum (q-add-p:rpb:unum (p-to-q:rpb:unum 0x40) 0x48)))
+    %+  expect-eq  !>(`@`0x54)
+      !>((q-to-p:rpb:unum (q-mul-add:rpb:unum q-zero:rpb:unum 0x48 0x4c)))
+  ==
+::
+++  test-fdp-rpb  ^-  tang
+  ;:  weld
+    %+  expect-eq  !>(`@`0x52)  !>((fdp:rpb:unum ~[0x40 0x48] ~[0x4c 0x40]))
+    %+  expect-eq  !>(`@`0x5d)  !>((fdp:rpb:unum ~[0x48 0x4c] ~[0x48 0x4c]))
+    %+  expect-eq  !>(`@`0x40)
+      !>((fdp:rpb:unum ~[0x7f 0x40 0x81] ~[0x40 0x40 0x40]))
+  ==
+::
+::  posit32 <-> single (value-based; posit -2.0 = 0xb800.0000, NOT the
+::  single -2.0 = 0xc000.0000 -- the two formats differ at the same width).
+++  test-ieee-rps  ^-  tang
+  ;:  weld
+    %+  expect-eq  !>(`@`0x3f80.0000)  !>((to-rs:rps:unum 0x4000.0000))
+    %+  expect-eq  !>(`@`0xc000.0000)  !>((to-rs:rps:unum 0xb800.0000))
+    %+  expect-eq  !>(`@`0x3f00.0000)  !>((to-rs:rps:unum 0x3800.0000))
+    %+  expect-eq  !>(`@`0x4000.0000)  !>((from-rs:rps:unum `@rs`0x3f80.0000))
+    %+  expect-eq  !>(`@`0xb800.0000)  !>((from-rs:rps:unum `@rs`0xc000.0000))
+    %+  expect-eq  !>(`@`0x3800.0000)  !>((from-rs:rps:unum `@rs`0x3f00.0000))
+  ==
+::
+++  test-ieee-rph  ^-  tang
+  ;:  weld
+    %+  expect-eq  !>(`@`0x3c00)  !>((to-rh:rph:unum 0x4000))
+    %+  expect-eq  !>(`@`0xc000)  !>((to-rh:rph:unum 0xb800))
+    %+  expect-eq  !>(`@`0x4000)  !>((from-rh:rph:unum `@rh`0x3c00))
+    %+  expect-eq  !>(`@`0xb800)  !>((from-rh:rph:unum `@rh`0xc000))
+  ==
+::
+::  The matrix: ANY posit width <-> ANY float width (value-based).  posits
+::  pack more accuracy per bit, so cross-width is the useful correspondence.
+::
+++  test-ieee-matrix  ^-  tang
+  ;:  weld
+    %+  expect-eq  !>(`@`0x3f80.0000)  !>((to-rs:rph:unum 0x4000))
+    %+  expect-eq  !>(`@`0x3ff0.0000.0000.0000)  !>((to-rd:rps:unum 0x4000.0000))
+    %+  expect-eq  !>(`@`0x3f80.0000)  !>((to-rs:rpb:unum 0x40))
+    %+  expect-eq  !>(`@`0x4000)  !>((from-rs:rph:unum `@rs`0x3f80.0000))
+    %+  expect-eq  !>(`@`0x4000.0000)  !>((from-rd:rps:unum `@rd`0x3ff0.0000.0000.0000))
+  ==
+::
+::  Transcendentals (naive Taylor series, /lib/math style).  These posit8
+::  values are the series outputs, which match the SoftPosit correctly-rounded
+::  result (verified offline by a Python port of the same series).  pow-n is
+::  exact integer power.
+::
+++  test-transcendental-rpb  ^-  tang
+  =/  u  rpb:unum
+  ;:  weld
+    %+  expect-eq  !>(`@`0x40)  !>((exp:u 0x0))
+    %+  expect-eq  !>(`@`0x4b)  !>((exp:u 0x40))
+    %+  expect-eq  !>(`@`0x0)   !>((sin:u 0x0))
+    %+  expect-eq  !>(`@`0x3d)  !>((sin:u 0x40))
+    %+  expect-eq  !>(`@`0x40)  !>((cos:u 0x0))
+    %+  expect-eq  !>(`@`0x39)  !>((cos:u 0x40))
+    %+  expect-eq  !>(`@`0x44)  !>((tan:u 0x40))
+    %+  expect-eq  !>(`@`0x0)   !>((log:u 0x40))
+    %+  expect-eq  !>(`@`0x3b)  !>((log:u (sun:u 2)))
+    %+  expect-eq  !>(`@`0x58)  !>((pow-n:u (sun:u 2) 3))
+    %+  expect-eq  !>(`@`0x40)  !>((pow:u (sun:u 2) 0x0))
+  ==
+--
diff --git a/libmath/tools/posit_check.py b/libmath/tools/posit_check.py
new file mode 100644
index 0000000..ca98e7a
--- /dev/null
+++ b/libmath/tools/posit_check.py
@@ -0,0 +1,290 @@
+#!/usr/bin/env python3
+"""Offline verification harness for /lib/unum (2022 Posit Standard, es=2).
+
+Runs the *exhaustive* checks that are too expensive for the on-ship Hoon
+suite, against two independent oracles:
+
+  1. SoftPosit (the `softposit` pip package, pX2 = es=2 at any width)
+  2. a from-scratch exact-rational reference encoder/decoder
+
+It (a) cross-checks the math constants baked into lib/unum.hoon at
+posit8/16/32, and (b) exhaustively checks add/sub/mul/div over ALL
+65,536 posit8 pairs.  The Hoon suite mirrors a lean subset (round-trips,
+spot values, a property sweep); this is the heavy proof, run once.
+
+    pip install softposit mpmath
+    python3 libmath/tools/posit_check.py
+"""
+from fractions import Fraction
+try:
+    import softposit as sp
+except ImportError:
+    sp = None
+from mpmath import mp, mpf, pi as PI, e as E, sqrt, log, phi as PHI
+mp.dps = 80
+
+# ---- reference decoder/encoder, mirroring lib/unum.hoon (es=2) ----
+
+def decode(p, n):
+    msk = (1 << n) - 1; p &= msk; nar = 1 << (n - 1)
+    if p == 0: return ('z',)
+    if p == nar: return ('n',)
+    neg = (p >> (n - 1)) & 1
+    mag = (1 << n) - p if neg else p
+    pw = n - 1; r0 = (mag >> (pw - 1)) & 1; k = 1
+    while True:
+        if k == pw:
+            r = (k - 1) if r0 == 1 else -k
+            return ('p', neg, 4 * r, 1)
+        if (mag >> (pw - 1 - k)) & 1 == r0: k += 1; continue
+        break
+    r = (k - 1) if r0 == 1 else -k
+    remwid = pw - (k + 1); rem = mag & ((1 << remwid) - 1)
+    if remwid >= 2: elo = rem >> (remwid - 2); fw = remwid - 2
+    elif remwid == 1: elo = rem << 1; fw = 0
+    else: elo = 0; fw = 0
+    frac = rem & ((1 << fw) - 1)
+    x = 4 * r + elo; a = (1 << fw) + frac
+    return ('p', neg, x - fw, a)
+
+def encode(neg, e, a, n):
+    if a == 0: return 0
+    msk = (1 << n) - 1; maxpos = (1 << (n - 1)) - 1
+    lead = a.bit_length() - 1; x = e + lead; frac = a & ((1 << lead) - 1)
+    r = x >> 2; elo = x - 4 * r
+    if r >= n - 2: return ((1 << n) - maxpos) & msk if neg else maxpos
+    if r <= -(n - 1): return ((1 << n) - 1) & msk if neg else 1
+    if r >= 0: regval = ((1 << (r + 1)) - 1) << 1; regwid = r + 2
+    else: regval = 1; regwid = -r + 1
+    totw = regwid + 2 + lead
+    pay = (regval << (2 + lead)) | (elo << lead) | frac
+    pw = n - 1
+    if totw <= pw:
+        mag = pay << (pw - totw)
+    else:
+        sh = totw - pw; keep = pay >> sh
+        guard = (pay >> (sh - 1)) & 1; low = pay & ((1 << (sh - 1)) - 1)
+        if guard and ((1 if low else 0) or (keep & 1)): keep += 1
+        if keep > maxpos: keep = maxpos
+        mag = keep
+    return ((1 << n) - mag) & msk if neg else mag
+
+def ref_value_encode(v, n):  # v: Fraction
+    if v == 0: return 0
+    neg = v < 0; w = -v if neg else v
+    maxv = Fraction(2) ** (4 * n - 8)
+    if w >= maxv: return ((1 << n) - maxpos_of(n)) & ((1 << n) - 1) if neg else maxpos_of(n)
+    if w <= 1 / maxv: return ((1 << n) - 1) & ((1 << n) - 1) if neg else 1
+    x = 0; vv = w
+    while vv >= 2: vv /= 2; x += 1
+    while vv < 1: vv *= 2; x -= 1
+    K = 80; a = int(vv * Fraction(1 << K))  # significand with hidden 1
+    return encode(neg, x - K, a, n)
+
+def maxpos_of(n): return (1 << (n - 1)) - 1
+
+# ---- g-layer arithmetic, mirroring lib/unum.hoon ----
+
+def mul(a, b, n):
+    ua, ub = decode(a, n), decode(b, n)
+    if ua[0] == 'n' or ub[0] == 'n': return 1 << (n - 1)
+    if ua[0] == 'z' or ub[0] == 'z': return 0
+    _, sa, ea, aa = ua; _, sb, eb, ab = ub
+    return encode(sa ^ sb, ea + eb, aa * ab, n)
+
+def add(a, b, n):
+    ua, ub = decode(a, n), decode(b, n)
+    if ua[0] == 'n' or ub[0] == 'n': return 1 << (n - 1)
+    if ua[0] == 'z': return b
+    if ub[0] == 'z': return a
+    _, sa, ea, aa = ua; _, sb, eb, ab = ub
+    emin = min(ea, eb); s1 = aa << (ea - emin); s2 = ab << (eb - emin)
+    if sa == sb: return encode(sa, emin, s1 + s2, n)
+    if s1 > s2: return encode(sa, emin, s1 - s2, n)
+    if s2 > s1: return encode(sb, emin, s2 - s1, n)
+    return 0
+
+def neg(a, n): return ((1 << n) - a) & ((1 << n) - 1)
+def sub(a, b, n): return add(a, neg(b, n), n)
+
+def div(a, b, n):
+    ua, ub = decode(a, n), decode(b, n)
+    if ua[0] == 'n' or ub[0] == 'n': return 1 << (n - 1)
+    if ub[0] == 'z': return 1 << (n - 1)
+    if ua[0] == 'z': return 0
+    _, sa, ea, aa = ua; _, sb, eb, ab = ub
+    g = 2 * n; num = aa << g; q = num // ab
+    if num % ab: q |= 1
+    return encode(sa ^ sb, ea - eb - g, q, n)
+
+# ---- softposit oracle ----
+
+def sp_pat(p, n): return p.v >> (32 - n)
+def sp_mk(pat, n):
+    o = sp.convertDoubleToPX2(0.0, n); o.v = pat << (32 - n); return o
+def sp_op(op, a, b, n):
+    f = {'add': sp.pX2_add, 'sub': sp.pX2_sub, 'mul': sp.pX2_mul, 'div': sp.pX2_div}[op]
+    return sp_pat(f(sp_mk(a, n), sp_mk(b, n), n), n)
+
+# ---- checks ----
+
+CONSTS = {'pi': PI, 'tau': 2 * PI, 'e': E, 'phi': PHI, 'sqt2': sqrt(2),
+          'invsqt2': 1 / sqrt(2), 'log2': log(2), 'invlog2': 1 / log(2),
+          'log10': log(10)}
+WIDTHS = [('rpb', 8), ('rph', 16), ('rps', 32)]
+
+def check_consts():
+    ok = True
+    for name, val in CONSTS.items():
+        fr = Fraction(int(mp.nint(val * (mpf(2) ** 120))), 1 << 120)
+        for w, n in WIDTHS:
+            ref = ref_value_encode(fr, n)
+            if sp is not None:
+                ora = sp_pat((sp.convertDoubleToP32(float(val)) if n == 32
+                              else sp.convertDoubleToPX2(float(val), n)), n)
+                if ref != ora:
+                    print(f"  CONST MISMATCH {name} {w}: ref=0x{ref:x} sp=0x{ora:x}"); ok = False
+    print("constants: ref-encoder == SoftPosit at posit8/16/32:", ok)
+    return ok
+
+def check_arith():
+    if sp is None:
+        print("arith: SKIP (softposit not installed)"); return True
+    ok = True
+    for name, fn in (('add', add), ('sub', sub), ('mul', mul), ('div', div)):
+        bad = 0
+        for a in range(256):
+            for b in range(256):
+                if fn(a, b, 8) != sp_op(name, a, b, 8): bad += 1
+        print(f"  {name}: {65536 - bad}/65536 posit8 pairs match SoftPosit")
+        ok &= (bad == 0)
+    return ok
+
+def isqrt(x):
+    if x == 0: return 0
+    r = 1 << ((x.bit_length() + 1) // 2)
+    while True:
+        nr = (r + x // r) // 2
+        if nr >= r: break
+        r = nr
+    while r * r > x: r -= 1
+    return r
+
+def my_sqrt(p, n):
+    u = decode(p, n)
+    if u[0] == 'n': return 1 << (n - 1)
+    if u[0] == 'z': return 0
+    _, neg, e, a = u
+    if neg: return 1 << (n - 1)
+    if e & 1: a <<= 1; e -= 1
+    G = 2 * n; m = a << (2 * G); s = isqrt(m)
+    if s * s != m: s |= 1
+    return encode(False, e // 2 - G, s, n)
+
+def my_round(p, n):
+    u = decode(p, n)
+    if u[0] != 'p': return p
+    _, neg, e, a = u
+    if e >= 0: return p
+    sh = -e; hi = a >> sh; rem = a & ((1 << sh) - 1); half = 1 << (sh - 1)
+    if rem > half or (rem == half and (hi & 1)): hi += 1
+    if hi == 0: return 0
+    return encode(neg, 0, hi, n)
+
+def my_fma(a, b, c, n):
+    ua, ub, uc = decode(a, n), decode(b, n), decode(c, n)
+    if ua[0] == 'n' or ub[0] == 'n' or uc[0] == 'n': return 1 << (n - 1)
+    if ua[0] == 'z' or ub[0] == 'z': return c
+    _, sa, ea, aa = ua; _, sb, eb, ab = ub
+    ps, pe, pa = sa ^ sb, ea + eb, aa * ab
+    if uc[0] == 'z': return encode(ps, pe, pa, n)
+    _, sc2, ec, ac = uc
+    emin = min(pe, ec); s1 = pa << (pe - emin); s2 = ac << (ec - emin)
+    if ps == sc2: return encode(ps, emin, s1 + s2, n)
+    if s1 > s2: return encode(ps, emin, s1 - s2, n)
+    if s2 > s1: return encode(sc2, emin, s2 - s1, n)
+    return 0
+
+def my_from_i(v, n):
+    if v == 0: return 0
+    return encode(v < 0, 0, abs(v), n)
+
+def check_elementary():
+    if sp is None:
+        print("elementary: SKIP (softposit not installed)"); return True
+    def mk(pat, n):
+        o = sp.convertDoubleToPX2(0.0, n); o.v = pat << (32 - n); return o
+    def pt(p, n): return p.v >> (32 - n)
+    n = 8; ok = True
+    bad = sum(1 for p in range(256) if my_sqrt(p, n) != pt(sp.pX2_sqrt(mk(p, n), n), n))
+    print(f"  sqrt: {256 - bad}/256 match"); ok &= (bad == 0)
+    # roundToInt: skip p=0x81 (-maxPos), a SoftPosit sign-flip bug at the extreme
+    bad = sum(1 for p in range(256)
+              if p != 0x81 and my_round(p, n) != pt(sp.pX2_roundToInt(mk(p, n), n), n))
+    print(f"  roundToInt: {255 - bad}/255 match (0x81 excluded: SoftPosit bug)")
+    ok &= (bad == 0)
+    bad = sum(1 for v in range(-300, 301) if my_from_i(v, n) != pt(sp.i32_to_pX2(v, n), n))
+    print(f"  i32->posit: {601 - bad}/601 match"); ok &= (bad == 0)
+    import random as _r; _r.seed(7); bad = 0
+    for _ in range(20000):
+        a, b, c = _r.randrange(256), _r.randrange(256), _r.randrange(256)
+        if my_fma(a, b, c, n) != pt(sp.pX2_mulAdd(mk(a, n), mk(b, n), mk(c, n), n), n): bad += 1
+    print(f"  fma: {20000 - bad}/20000 sampled match"); ok &= (bad == 0)
+    return ok
+
+def my_fdp(av, bv, n):
+    acc = 0; sc = 8 * n - 16
+    for a, b in zip(av, bv):
+        ua, ub = decode(a, n), decode(b, n)
+        if ua[0] == 'n' or ub[0] == 'n': return 1 << (n - 1)
+        if ua[0] == 'z' or ub[0] == 'z': continue
+        _, sa, ea, aa = ua; _, sb, eb, ab = ub
+        qc = (aa * ab) << (ea + eb + sc)
+        acc += -qc if (sa ^ sb) else qc
+    return ref_value_encode(Fraction(acc, 1 << sc), n)
+
+def check_quire():
+    if sp is None:
+        print("quire: SKIP (softposit not installed)"); return True
+    def mk(pat, n):
+        o = sp.convertDoubleToPX2(0.0, n); o.v = pat << (32 - n); return o
+    def pt(p, n): return p.v >> (32 - n)
+    import random as _r; _r.seed(11); n = 8; bad = 0; T = 3000
+    for _ in range(T):
+        L = _r.randrange(1, 6)
+        av = [_r.randrange(256) for _ in range(L)]
+        bv = [_r.randrange(256) for _ in range(L)]
+        q = sp.qX2Clr()
+        for a, b in zip(av, bv): q = sp.qX2_fdp_add(q, mk(a, n), mk(b, n))
+        if my_fdp(av, bv, n) != pt(sp.qX2_to_pX2(q, n), n): bad += 1
+    print(f"  fdp: {T - bad}/{T} random vectors match")
+    return bad == 0
+
+def check_arith_wide():
+    # add/sub/mul/div sampled at posit16 and posit32 vs SoftPosit (all exact).
+    if sp is None:
+        print("  wide arith: SKIP"); return True
+    import random as _r
+    def mk(p, n):
+        o = sp.convertDoubleToPX2(0.0, n); o.v = p << (32 - n); return o
+    def pt(p, n): return p.v >> (32 - n)
+    fns = {'add': add, 'sub': sub, 'mul': mul, 'div': div}
+    spf = {'add': sp.pX2_add, 'sub': sp.pX2_sub, 'mul': sp.pX2_mul, 'div': sp.pX2_div}
+    ok = True
+    for n in (16, 32):
+        _r.seed(1); bad = {}
+        for _ in range(100000):
+            a = _r.randrange(1 << n); b = _r.randrange(1 << n)
+            for k in fns:
+                if fns[k](a, b, n) != pt(spf[k](mk(a, n), mk(b, n), n), n):
+                    bad[k] = bad.get(k, 0) + 1
+        print(f"  posit{n}: {bad or 'all add/sub/mul/div match'}")
+        ok &= (not bad)
+    return ok
+
+if __name__ == '__main__':
+    c = check_consts(); a = check_arith()
+    print("elementary:"); el = check_elementary()
+    print("quire:"); q = check_quire()
+    print("wide arith (posit16/32 sampled):"); w = check_arith_wide()
+    print("ALL PASS:", c and a and el and q and w)