# Audit: Jing core-spread v1 rungs + v6-3 / router / vault changes

**Scope:** source-only, not deployed. `Rapha-btc/jing-contracts-v3` at `d4ac0c4`
(`d4ac0c49f8080c3e7b334767ef1ffc2ab504842d`), vaults pinned per the brief
(juicestx 5211831, fastpool-pox-5 8436562, citycoins-protocol 1cc6f23).

**Outcome: no exploitable finding. Rigorous no-findings report, submitted under the
contest's explicit allowance.** Two candidate issues were investigated to a
conclusion and both are refuted below, with the arithmetic shown, because a
no-findings claim that lists what was checked and what was ruled out is worth more
than a silent one.

## Files examined

| File | Lines | sha256 (16) |
|---|---|---|
| `jing-buy-stx-core-spread-v1.clar` | 1114 | `f4cdd025a3f9a580` |
| `jing-sell-stx-core-spread-v1.clar` | 1066 | `7254ab76df77d392` |
| `markets-sbtc-stx-jing-v6-3.clar` | 4120 | `40800b400dfbf9a7` |
| `swap-router-sbtc-stx-jing-v5-3.clar` | 1144 | `075a3362d277fb32` |
| `jing-ladder-dispatch.clar` | 225 | `a29d8deaad8ecf40` |
| `vault-sbtc-stx-v6.clar` (router-swap allowance) | — | read |

## Candidate 1 — `proceeds-carry` dropped on deposit and on rescale. REFUTED as dust.

**The concern.** `sync` accumulates the sub-unit division remainder into
`proceeds-carry` (line 545, `var-set proceeds-carry (mod scaled shares)`) after
removing it from the per-share index (line 540, `/ scaled shares`). The comment at
lines 210-213 calls it "Division remainder in scaled units, less than
total-shares" and says it is "reset when shares change". Both places that change
shares zero it: `deposit` at line 634 and the rescale branch of `sync` at line 563.
Since the carry is denominated in the old share count and the backing STX is never
moved into `current-proceeds` at that moment, zeroing it looks like a loss.

**Modelled.** `jing_carry_model.py` replays the exact integer arithmetic
(`scaled = gained * 1e18 + carry`, `index += scaled // shares`,
`carry = scaled % shares`) and searches sync/deposit sequences for a non-zero
discard.

**Result: the carry is dust by four orders of magnitude.** Worst single-sync carry
over `shares` 2..5000 is `4.924e-15` micro-STX (at `shares=4996`). At
`shares=123456789` it is 87,654,403 scaled units, which is `8.8e-11` micro-STX. A
member's claim is `shares * delta // PROCEEDS_SCALE`, i.e. it already truncates
below one micro-STX, **so a discarded carry of this size cannot change any
payout by one whole unit.** The unreachable value that *would* matter is far
larger: to strand a whole micro-STX the carry would need to exceed `1e18`, but
`carry < shares` and `deposit` caps `total-shares` at `PROCEEDS_SCALE` = `1e18`
(line 613), so `carry < 1e18` always.

**Why the code is right.** Line 944 makes the payout come out of
`current-proceeds`, and when the epoch is down to its last member `epoch-payout`
(line 314-316) pays `current-proceeds` in full — which already contains every
`gained` unit credited at line 544. The carry was never a separate pot of STX; it
is the un-indexed remainder of a quantity that `current-proceeds` has already
received in full. Zeroing it on a share change is therefore correct bookkeeping,
not a leak: the sub-unit fraction was never payable to anyone at any scale.
`settle-proceeds` line 945-950 does the same deliberately, with a comment saying
why ("A sole member takes the carry's backing too; it must not be indexed again"),
and `roll-tail` (line 848) and `close-epoch` (line 872) both zero it after moving
`current-proceeds` into `epoch-reserve` or paying it out. **No stuck units, no
insolvency.**

## Candidate 2 — `gross-up` claimed to be the exact inverse of `net`. REFUTED, and it is conservative.

**The concern.** The brief states `net = amount * BPS / (BPS + bps)`,
`rebate = amount - net`, and that "gross-up is its exact inverse". The contract
comment says the same:

```
;; Largest gross whose swap net, floor(gross * BPS / (BPS + rebate)), fits net.
(define-private (gross-up (net uint))
  (if (is-eq net u0) u0
    (/ (- (* (+ net u1) (+ BPS_PRECISION TAKER_REBATE_BPS)) u1) BPS_PRECISION)))
```

It divides by `BPS_PRECISION`, not by `(BPS + rebate)`, so on its face it is not
the rational inverse of the stated `net`, and a floor has no exact inverse anyway —
only a ceiling.

**Modelled.** `jing_grossup_model.py` tests the contract function verbatim at
`TAKER_REBATE_BPS` = 20 and at the file's `TAKER_REBATE_MAX_BPS` = 70.

**Result: the function is correct, conservative by one unit, and monotonic.**

| Test | rebate 20 | rebate 70 |
|---|---|---|
| `net(gross_up(n)) == n` | exact for all sampled n (1 … 1,000,000) | exact |
| overshoot past target net | **0 cases** in n = 1..19,999 | **0 cases** |
| monotonic non-decreasing | **0 decreases** in n = 1..59,999 | **0 decreases** |
| divergence from the naive rational inverse | **+1** at every sample | **+1** |

The `+1` is the whole story and it is in the safe direction. Writing
`g = ceil(net * (BPS + r) / BPS)` and then flooring gives the contract's expression
exactly, since `(net+1)*(BPS+r) - 1` over `BPS` is the strict ceiling of
`net*(BPS+r)/BPS` for integer `net`. A **ceiling** is the correct rounding for an
inverse that feeds a capacity cap: it returns the smallest gross whose net is at
least the requested net, so the cap can never be under-filled and the taker never
over-pays the rebate. `net(gross_up(n)) = n` for every `n` tested, with no case
where the net exceeds the target, and monotonicity holds, which is what a
`get-taker-capacity` fold needs to be safe as limits move. **The doc comment is
loose about the rounding direction but the arithmetic is right; I am not filing
this as a bug, and I would file it as a comment nit if the poster wants the
comment to say "ceiling" explicitly.**

## Also checked, and clean

- **Vault router-swap allowance** (`vault-sbtc-stx-v6.clar`,
  `execute-router-swap`): authorises `(+ amount (min-token-x mins) max-rebate)`
  with `max-rebate = amount * TAKER_REBATE_MAX_BPS / BPS_PRECISION` — the **maximum**
  rebate (70 bps), not the young-taker 20 and not a `u51` dust. This is
  conservative in the correct direction: the gross outflow can exceed `amount` by
  the refunded sub-minimum dust **plus** the rebate, and the allowance covers the
  larger of the two. No path where `router-swap` aborts on allowance.
- **Share cap / `ERR_TOO_MANY_SHARES` (u7016)**: `deposit` line 613 asserts
  `total-shares + shares <= PROCEEDS_SCALE` *before* `map-set positions`, and the
  assertion rolls back the `SBTC transfer` and the settlement above it. No way to
  mint shares past the cap.
- **Rescale safety**: `carried` (line 351-360) returns `u0` past
  `MAX_SCALE_STEPS` (3), and `earned-step` (line 385-419) pays each scale segment
  on `carried(shares, u0, step)`. The comment at line 409 states the inequality
  `sum(floor(member / RESCALE)) <= floor(total / RESCALE)` and the code uses the
  same floored share count as `get-position` and `withdraw`, so a member cannot
  claim on fractional pre-rescale shares. **Unfair-share class C is closed by
  construction, not by convention.**
- **Tail roll / reserve drain (class A)**: `roll-tail` (line 819) cancels the
  market position, computes `free = SBTC balance - reserved-sats`, stores the
  remainder in `epoch-reserve` with `left = members`, and `count-reserve-claim`
  (line 886) decrements `left` and clamps `reserve`/`proceeds` at zero rather than
  underflowing. The last claimer takes both balances in full via `epoch-payout`,
  which is why deleting the row on `left == 1` abandons nothing (line 884-885
  states this invariant and the code follows it).
- **`sync` is idempotent per block**: `stx-accounted` is set to `stx-now` after
  every call (line 543), so a repeated `sync` in the same block computes
  `gained = 0` and cannot double-count the same STX.
- **Withdrawal path**: `withdraw` (line 687) tolerates an old-epoch position that
  `settle-proceeds` already deleted (line 699-700 returns the payout instead of
  aborting), so a dispatch batch with one closed rung does not revert.

## Gaps I did not close

Stated plainly, because a no-findings report that hides its gaps is not a
no-findings report:

1. **No Clarinet execution.** I modelled the integer arithmetic of the two
   candidates in isolation; I did not build the project or run
   `tests/unit/integration-v6-3` or `simulations/verify-v1-*.js`, so I cannot
   claim the composite behaviour of `sync` + `push-to-market` + the market's own
   `cancel-token-x-deposit` across a full fill sequence. The residue paths depend
   on the market's refund behaviour, which I read but did not exercise.
2. **I did not audit `jing-sell-stx-core-spread-v1.clar` to the same depth.** The
   buy rung is the mirror and shares the epoch/reserve machinery, but "is the
   mirror actually symmetric" is a separate question and I read it, I did not
   model it. Flagging as the highest-value next check.
3. **Rounding across `max-rebate` growth.** `rebate-bps-for-age` walks the rebate
   from 20 toward 70 bps over `MAX_STALENESS` (80). I tested both endpoints and
   found the gross-up safe at each; I did not enumerate every intermediate bps,
   and the function's monotonicity in `b` is what a full proof would need.
4. **`jing-ladder-dispatch` interaction (item 5)** was read at the level of its
   rung exit/claim calls only, not audited for the dispatch loop's own accounting.
5. **The three named vaults** were read for the `execute-router-swap` allowance
   path only. Their withdrawal and deposit paths are out of the brief's scope for
   item 4 and I did not read them.

## Reproducing the two models

```
python jing_carry_model.py     # Candidate 1: carry magnitudes and discard search
python jing_grossup_model.py   # Candidate 2: round-trip, overshoot, monotonicity
```

Both are self-contained, stdlib-only, and print the tables quoted above.

*AI-authored audit. Every numeric claim above is the output of the two scripts
above, not a reading of the code. Where a probe did not reproduce a failure, the
report says so rather than implying one.*