State

#[weld::state] on a struct defines a fixed-capacity Poseidon2 tree (depth 8, 256 leaves) with typed accessors. Leaf 0 is a hidden salt the framework refreshes on every transition, so successive public state roots are unlinkable and a low-entropy state cannot be brute-forced. State<S> supports get(key), set(key, value), and root().

The generated main accepts state_in == 0 as the canonical empty state (all leaves zero, fresh salt) and otherwise welds state_in == old.root(); it always publishes new.root() as state_out. The chain of state roots for an FI is therefore a verified sequence of transitions from the empty tree, which is what makes cumulative rules sound.

#[weld::state]
struct Ledger { spent_today: u128, day: Field }
 
impl StatefulRule<Params, Ledger> for Velocity {
    fn on_initiate(p: Params, ctx: Ctx<Initiate>, s: State<Ledger>) -> (State<Ledger>, Verdict, Attest) {
        let day = ctx.time_bucket() / 288;                  // 5-min buckets → days
        let base = if s.day() == day { s.spent_today() } else { 0 };
        let total = base + ctx.recipient_note().amount;
        let v = Verdict::require(total <= p.daily_cap, "velocity/over-daily-cap");
        (s.with_spent_today(total).with_day(day), v, Attest::none())
    }
}

Keyed state (per counterparty, per day) is deferred to v2 and will use a sparse Merkle subtree with an insert-with-non-membership gadget. When keys are monotonic (day buckets, hold positions) the FI can freeze the prefix below a threshold to cold storage and keep only a frontier plus recent keys, so active state stays small regardless of lifetime activity.