Agent rules + predict-audit: de-stale to static-floor knockout; add evidence-backed rules

Scope: Predict cluster only (no deepbook-core changes); docs/skill files only, no Move source.

Rule files:
- move.md: rewrite Predict-Economics to static-floor knockout (drop terminal_floor_index /
  floor_index / time-varying-floor / opened_at_ms-in-id; static F, quantity - floor_shares,
  exact NAV = Sum qty*P - Sum min(qty*P,F), knock-out level, lambda buffer) -- verified at HEAD.
  Add: Open-Closed/irreversibility, loop-hoist preservation, guard-preservation across
  extraction, unbounded-permissionless-state-in-aggregation, owner-auth fallback for terminal
  exits, defer-and-carry; return-struct default + Data-Clump (2-3, not 4+); trust-boundary
  carve-out to non-redundancy; two-sided + recoverable safety bounds.
- code-review.md: add loop-hoist regression check.
- unit-tests.md: Rule 4 -> reachable-only + testability-as-design; Rule 15 -> fix dangling
  .redesign/BUGS_FOUND.md path to .claude/predict-review/OPEN-ITEMS.md.
- CLAUDE.md: re-aim the Predict-economics gate at the current settled list; flag the journal as
  historical; separate NAV-supersession from the still-live D030 backing axis; state knockout.

predict-audit skill (kept Predict-scoped):
- SKILL.md/primer.md: fix scope to the 4 Predict-cluster packages (not deepbook core);
  migration out of scope.
- primer.md/lens 01/defi-invariant-classes.md: reframe live-backing / aggregate-NAV to static
  Q-F + lambda / knock-out-level.
- ownership-rules.md: R2 drops opened_at_ms; R5 adds the trust-boundary carve-out.
- move-sui-audit-checklist.md: add Refactor & API-surface safety section.
- rule-sweep.workflow.js: recalibrate test-coverage family (reachable-only + testability;
  drop stale .move.disabled note).

Verified at HEAD: terminal_floor_index/floor_index = 0 occurrences, backing_buffer_lambda exists,
0 .move.disabled files. (The matching ROUNDING_POLICY.md R1-scope edit stays local --
.claude/predict-design/ is gitignored.)

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: 0xaslan

.claude/rules/code-review.md

@@ -21,6 +21,7 @@ Read this manual-trigger file when the user asks for a code review. It is routed
 - Intuitive behavior: check whether names, public APIs, events, and state transitions match what a protocol integrator or maintainer would expect.
 - Ownership and responsibility boundaries for modules/functions: verify state is mutated by its owner, helpers do not absorb parent responsibilities, and callers do not duplicate leaf invariants without a sequencing reason.
 - Producer-side policy: flag cross-module returns that pre-apply a consumer's policy — especially lossy transforms (clamp at zero, saturating subtraction, `min`/`max`, rounding) that a downstream consumer then corrects for or re-derives. Bug signatures: the same economic quantity clamped at two altitudes, stance-named returns (`*_optimistic`, `net_*`), or tests that must invert a producer's step to state expectations.
+- Non-functional regressions in "behavior-preserving" changes: before approving a hot-path/loop refactor, confirm a deliberate loop-invariant hoist wasn't traded away for a cleaner signature — recomputing a per-iteration value previously sampled once is a gas regression even if outputs are identical (D020/D021).
 
 ## Comments and Documentation
 

.claude/rules/move.md

@@ -82,7 +82,7 @@ fun deposit_adds_funds() {
 
 ### 4. Cover every abort code with an `expected_failure` test
 
-For every `const E*` error constant in a source module, there must be at least one test that triggers it. Untested abort codes are untested error paths.
+For every *reachable* `const E*` error constant in a source module, there must be at least one test that triggers it; untested abort codes are untested error paths. Coverage applies regardless of visibility: if a guard behind a `public(package)` helper can't be triggered as-is, that is a signal to make it independently testable — extract the pure precondition into a `public(package)` checker taking only its scalar inputs (e.g. `assert_plp_price_in_bounds(pool_nav, total_supply)`) and test that directly. "The guard is package-internal" is never a reason to ship an untested abort code; add the root-free unit test or ledger it as a tracked deploy-gate. For a code that is genuinely structurally-unreachable in production, document why instead of contriving a bypass test (Rule 12 forbids bypassing production validation just to reach a code).
 
 ```move
 #[test, expected_failure(abort_code = predict::EOracleSettled)]
@@ -277,8 +277,8 @@ contract (and the expected value was derived independently per Rule 1):
 - **Never** re-express the bug as an `expected_failure` of the buggy behavior.
 - **Never** "fix" the contract to make the test pass (that is a separate effort).
 
-Instead: add an entry to the bug ledger (e.g. `.redesign/BUGS_FOUND.md`), tag the
-test `// KNOWN-FAILING: BUG-NNN`, and leave it RED. The ledger is the authoritative
+Instead: add an entry to the live audit tracker (`.claude/predict-review/OPEN-ITEMS.md`), tag the
+test `// KNOWN-FAILING: <id>`, and leave it RED. The tracker is the authoritative
 manifest of expected-failing tests, so a *new* red (a regression) is distinguishable
 from a *known* red. A green-on-first-write suite is suspect; tests are supposed to
 be able to break.

.claude/rules/unit-tests.md

@@ -17,7 +17,7 @@ Invoking, reading, explaining, or editing this skill never needs the gate — **
 
 A self-driving harness for a deep, adversarial, **smart-contract-only** audit of DeepBook "Predict" — a leveraged binary prediction market on Sui — and its three split-out sibling packages. The goal is to **find real bugs**: solvency/fund-loss, liveness/abort (a bricked flow), griefing/DoS, mispricing, broken invariants, and authorization holes — plus, via a dedicated lens, architecture/cohesion/readability issues (overgrown "god" modules, coupling, decomposition). Findings are reasoned from the code AND, where it matters, **empirically reproduced** on localnet or in Python.
 
-This is a *code-audit* skill (security/correctness + maintainability). It does NOT do testnet-readiness/deploy/ops checks (Move.toml hygiene, post-deploy admin steps, indexer parity, runbooks). If asked for those, say so and scope them separately.
+This is a *code-audit* skill (security/correctness + maintainability). It does NOT do testnet-readiness/deploy/ops checks (Move.toml hygiene, post-deploy admin steps, indexer parity, runbooks). If asked for those, say so and scope them separately. Scope is FIXED to the four Predict-cluster packages (predict + propbook + block_scholes_oracle + account); do NOT broaden it to deepbook core or other repo packages. Upgrade / object-layout migration correctness is also out of scope (matches `move.md` pre-deploy) — revisit only when nearing deploy.
 
 ## When to use
 - "Audit Predict" / "deep audit of the predict contracts" / "find bugs in Predict before testnet."

.claude/skills/predict-audit/SKILL.md

@@ -39,10 +39,10 @@ Produce:
 **Focus areas (scope, not conclusions):**
 - The cash-backing invariant (`expiry_cash`) and whether it is re-checked after every cash mutation
   (mint, redeem, liquidation, settlement, compaction, flush rebalance).
-- The relationship between the conservative pre-settlement live backing (max-live payout) and the exact
+- The relationship between the pre-settlement live backing (the exact `quantity - floor_shares` plus the aggregate λ buffer, D030) and the exact
   settled liability — what guarantees the former bounds the latter for every order.
 - The exact `current_nav` mark (payout-tree `walk_linear` − leveraged `correction_value`, floored) and the
-  precondition it rests on (every active leveraged order individually above its floor before valuation — the
+  precondition it rests on (every order whose gross value crossed its knock-out level (`floor_amount / liquidation_ltv`) has been liquidated before valuation — the
   aggregate-floor precondition; see move.md NAV rules + the C3 note in ROUNDING_POLICY).
 - PLP share-pricing symmetry: supply and withdraw priced at the SAME frozen `current_nav` in `finish_flush` /
   `drain_lp_requests`; confirm `supply_NAV = TRUE = withdraw_NAV` at the valuation boundary (no over/under-count).

.claude/skills/predict-audit/lenses/01-invariants.md

@@ -19,7 +19,7 @@ operator-pushed Block-Scholes spot/forward/SVI surface data — both now served
 `propbook` package, which `predict` consumes but does not own.
 
 ## Scope (read-only)
-- Audit the Move **source** of four packages: `packages/{predict,propbook,block_scholes_oracle,account}/sources/**`.
+- Audit the Move **source** of four packages: `packages/{predict,propbook,block_scholes_oracle,account}/sources/**`. Scope is FIXED to these four — do NOT broaden to deepbook core or other repo packages. Upgrade / object-layout migration correctness is out of scope (pre-deploy).
 - IGNORE every `packages/*/build/**` (generated copies). Treat `tests/**` as reference (and as coverage
   evidence) unless your lens says otherwise.
 - Never modify source. You may read dependency source (`deepbook`, `dusdc`, `pyth_lazer`, `fixed_math`)
@@ -88,7 +88,7 @@ donatable incentive), SUI (donatable incentive), PLP (LP vault share token).
 `market_manager` cadence config → `create_expiry_market` (reads no live spot; absolute ticks snapshotted from cadence) → seed propbook Pyth + BS data for the emitted expiry → `mint` → live trade/redeem (partial or full close) → permissionless passive liquidation (budgeted, folded into mint/redeem/supply/withdraw) → **passive settlement** (terminal spot = the exact post-expiry Pyth print from propbook minute history; if absent, the market stays unsettled and live valuation aborts) → settled redeem → compaction (free storage). Full-pool valuation: a transaction-local `PoolValuation` snapshots active expiries, values each once under the valuation lock; the **privileged** flush prices PLP supply AND withdraw at one exact `current_nav` mark.
 
 ## Glossary (neutral)
-absolute tick = strike unit; `raw = tick * tick_size`. `pos_inf_tick`/`neg_inf` = open-ended-range sentinels. floor_shares = the **static** deterministic floor `F` of a leveraged position (the LP-funded leverage portion); winner payout = `Q − F`. terminal vs live (backing) payout = settled value vs conservative pre-settlement upper bound. payout_liability / settled_payout_liability = cash the market must back. rebate_reserve = reserve from collected-but-unresolved trading fees for loss rebates. EWMA penalty = gas-congestion fee surcharge. basis = forward/spot from BS pushes. SVI = volatility-surface parameterization for the binary tail. NAV = pool value pricing PLP shares; the flush mark is the **exact** `current_nav` (tree `walk_linear` − leveraged `correction_value`, floored), no conservative band. float_scaling = 1e9 fixed-point.
+absolute tick = strike unit; `raw = tick * tick_size`. `pos_inf_tick`/`neg_inf` = open-ended-range sentinels. floor_shares = the **static** deterministic floor `F` of a leveraged position (the LP-funded leverage portion); winner payout = `Q − F`. terminal vs live (backing) payout: under the static floor the winner's `Q - F` is exact at settlement, and the only pre-settlement conservatism is the aggregate disjoint-backing λ buffer (D030). payout_liability / settled_payout_liability = cash the market must back. rebate_reserve = reserve from collected-but-unresolved trading fees for loss rebates. EWMA penalty = gas-congestion fee surcharge. basis = forward/spot from BS pushes. SVI = volatility-surface parameterization for the binary tail. NAV = pool value pricing PLP shares; the flush mark is the **exact** `current_nav` (tree `walk_linear` − leveraged `correction_value`, floored), no conservative band. float_scaling = 1e9 fixed-point.
 
 ## Prior-awareness (mandatory)
 Before raising anything, consult the settled-decision ledger and respect it:

.claude/skills/predict-audit/primer.md

@@ -6,7 +6,7 @@ Recon-style invariant testing), mapped to Predict surfaces. Lens 01 builds the l
 ## 1. Solvency / conservation
 The protocol must always be able to pay what it owes; value is conserved across parties.
 - `expiry_cash`: `cash_balance >= payout_liability + rebate_reserve` after EVERY cash mutation.
-- Live backing (max-live payout) must bound the exact settled liability for every order.
+- Live backing for a winning order is the exact `quantity - floor_shares` (= its settled payout under the static floor) plus the aggregate disjoint-backing λ buffer (D030) — not a time-varying max-live term.
 - DUSDC is conserved across trader / LP / protocol / builder — no path mints value from nothing or strands it.
 - LP NAV: the exact `current_nav` mark prices PLP supply AND withdraw identically (`supply_NAV == withdraw_NAV
   == TRUE`) at the valuation boundary — no over/under-count, so no dilution and no liveness clamp under-pays.
@@ -20,7 +20,7 @@ Only the intended actor can move value or change critical state (see the Move ch
 Under-collateralized / under-floor positions are removed correctly and cannot be blocked.
 - Passive liquidation of an under-floor leveraged order cannot be starved, skipped, double-applied, or griefed;
   paging cursors/watermarks cover all candidates under budgeted passes.
-- The aggregate-floor NAV precondition holds: every active leveraged order is individually above its floor
+- The aggregate-floor NAV precondition holds: every order whose gross value has crossed its knock-out level (`floor_amount / liquidation_ltv`) has been liquidated
   before valuation, else aggregate-floor subtraction overstates recoverable value.
 
 ## 4. Oracle integrity

.claude/skills/predict-audit/references/defi-invariant-classes.md

@@ -53,3 +53,9 @@ below.
 - On-chain landing time vs source-data time must be distinguishable in the field name (`*_timestamp_ms` vs
   `*_published_at_us`).
 - Cross-module returns are owned facts, not pre-applied consumer policy (no `*_optimistic`/clamp-at-two-altitudes).
+
+## Refactor & API-surface safety
+- Guard-preservation across extraction: a moved write path keeps every pre-split auth + value guard (cap, non-zero, in-range, freshness, whole-ms key), or the removal is a journaled decision with the new trust model. (Origin: the oracle split dropped the BS writer-cap + `EZeroForward`/`EZeroSpot` + whole-ms guards.)
+- Trust-boundary input validation is owned by the public entrypoint (fail-fast), independent of any leaf guard — a MISSING boundary check is a finding; a boundary check that duplicates a leaf is NOT.
+- Open–Closed / irreversibility: a shipped `public` signature, event field, packed-id layout, or error meaning is a permanent commitment — minimize the surface; design extension around a predicted axis of variation.
+- Two-sided safety bounds: a circuit breaker / pricing envelope / band bounds BOTH sides, has an admin recovery path (not a hard upgrade-only constant), and is `expected_failure`-tested at each boundary.

.claude/skills/predict-audit/references/move-sui-audit-checklist.md

@@ -54,7 +54,7 @@ never re-implemented per site.
   can write/assert it? Is a formula re-expressed at a second call site instead of calling the canonical
   evaluator? For aggregate insert/remove/recompute, do all sites call the SAME function?
 - **Signatures:** a helper chain that only shuttles a derived value; a formula duplicated across mint-insert
-  and settlement-recompute; a lossy repack of `quantity`/`floor_shares`/`opened_at_ms` through the packed
+  and settlement-recompute; a lossy repack of `quantity`/`floor_shares` through the packed
   order id.
 - **Input shape corollary:** signature shape is part of ownership. Pass a domain object when the callee needs
   that object's identity, authority, current state, invariants, or several facts owned by that object. Pass a
@@ -112,6 +112,10 @@ precondition just to avoid a later abort. *(ex-rule-auditor Agent 9, contextual
   leaf's exact guard with no added value? Is there a manual overflow/cast assert duplicating a VM abort?
 - **Intentional exceptions:** a caller guard with a semantically richer error for a different business
   precondition, or a strictly tighter bound; named semantic/solvency/auth/lifecycle/gas asserts (keep).
+- **Trust-boundary carve-out:** at the protocol's outer trust boundary (a public entrypoint taking
+  attacker-chosen primitives, external coins, or oracle payloads) input validation is owned by the boundary
+  regardless of any downstream leaf guard (fail-fast). Do NOT flag such a boundary check as a removable
+  defensive duplicate; R5 non-redundancy governs internal package composition only.
 
 ## R6 — Encapsulation (Move's grain)
 **Rule:** A public entrypoint that mutates a `Balance`/field lives in the module that **declares** that field

.claude/skills/predict-audit/references/ownership-rules.md

@@ -59,8 +59,8 @@ const RULE_FAMILIES = [
     rule: "Do not add explicit overflow/underflow/numeric-cast asserts solely to replace Move's primitive VM aborts (those are free atomic checks). KEEP named assertions for semantic domain bounds, division-by-zero with a meaningful named zero error, solvency/accounting invariants, authorization, lifecycle, gas-bounded iteration, and option/vector/balance assumptions.",
     focus: 'Math/pricing (fixed_math use, predict pricing), strike_payout_tree, expiry_cash, plp allocation math, propbook oracle normalization. Flag ONLY asserts that duplicate a VM overflow/cast abort. The leaf-self-consistency / redundant-caller-guard half of this rule is the ownership walk (R5) — do NOT report it here.' },
   { key: 'test-coverage-rules', scope: ALL,
-    rule: "Every source `const E*` error code has >=1 `expected_failure` test naming that abort code (with a trailing guard abort using a DISTINCT code like `abort 999`). Every non-failure test asserts an output value or state change. Every test calls the function it claims to test. Prefer `assert_eq!`, import constants instead of duplicating, avoid magic numbers.",
-    focus: 'All tests/ + every source error constant. Cross-check each `E*` against an `expected_failure`. NOTE: many predict flow tests are `.move.disabled` — flag uncovered `E*` but record the disabled-suite context so it is not mistaken for a regression.' },
+    rule: "Every REACHABLE source `const E*` error code has >=1 `expected_failure` test naming that abort code (with a trailing guard abort using a DISTINCT code like `abort 999`). A guard behind a `public(package)` helper must be made independently testable (extract the pure precondition into a `public(package)` checker taking scalar inputs and test it directly) — package-internal visibility is not a reason to leave it uncovered. A genuinely structurally-unreachable defense-in-depth code is documented, not given a contrived bypass test (Rule 12). Every non-failure test asserts an output value or state change. Every test calls the function it claims to test. Prefer `assert_eq!`, import constants instead of duplicating, avoid magic numbers.",
+    focus: 'All tests/ + every source error constant. Cross-check each REACHABLE `E*` against an `expected_failure`; a `public(package)` guard with no test is a finding (recommend extracting a testable checker), and a structurally-unreachable code with no test is a non-finding if documented. (The predict flow tests are no longer `.move.disabled` — they were re-enabled; do not assume a disabled suite.)' },
   { key: 'timestamp-semantics', scope: 'packages/predict/sources and packages/propbook/sources',
     rule: "Timestamp fields have clear semantics; do not bump a 'last price update' field on unrelated updates (an SVI-param change must not bump a spot timestamp). Distinguish on-chain landing time (`*_timestamp_ms` = `clock.timestamp_ms()`) from source-data time (`*_published_at_us` or similar) in field/getter/event names.",
     focus: 'propbook `pyth_feed` + the 3 BS feeds + oracle_lane, predict pricing freshness checks, events, getter names. (The old in-package `pyth_source`/`market_oracle` were extracted to propbook — check the current feeds.)' },