diff --git a/random/src/lib.rs b/random/src/lib.rs
index 8042e80..3f8c5f7 100644
--- a/random/src/lib.rs
+++ b/random/src/lib.rs
@@ -79,3 +79,31 @@ pub fn ibig_neg(n: IBig) -> IBig {
 pub fn ibig_is_zero(n: &IBig) -> bool {
     *n == IBig::ZERO
 }
+
+pub fn ibig_zero() -> IBig {
+    IBig::ZERO
+}
+
+pub fn ibig_from_i64(n: i64) -> IBig {
+    IBig::from(n)
+}
+
+pub fn ibig_add(a: &IBig, b: &IBig) -> IBig {
+    a.clone() + b.clone()
+}
+
+pub fn ibig_sub(a: &IBig, b: &IBig) -> IBig {
+    a.clone() - b.clone()
+}
+
+pub fn ibig_ge(a: &IBig, b: &IBig) -> bool {
+    a >= b
+}
+
+pub fn ibig_lt(a: &IBig, b: &IBig) -> bool {
+    a < b
+}
+
+pub fn ibig_clone(n: &IBig) -> IBig {
+    n.clone()
+}
diff --git a/ub/dp/mod.rs b/ub/dp/mod.rs
new file mode 100644
index 0000000..c73cd5e
--- /dev/null
+++ b/ub/dp/mod.rs
@@ -0,0 +1,9 @@
+// DP module — LightDP-style value-dependent types on top of
+// multiplicative error credits. NumD encodes `num(d)`; its `laplace`
+// method is the T-LAPLACE coupling axiom.
+
+pub mod mult_credit;
+pub mod num_d;
+pub mod smart_sum;
+pub mod sparse_vector;
+pub mod num_sparse_vector;
diff --git a/ub/dp/mult_credit.rs b/ub/dp/mult_credit.rs
new file mode 100644
index 0000000..a91cc54
--- /dev/null
+++ b/ub/dp/mult_credit.rs
@@ -0,0 +1,136 @@
+use vstd::pcm::*;
+use vstd::prelude::*;
+
+verus! {
+
+#[allow(non_snake_case)]
+pub uninterp spec fn MULT_EC_GLOBAL_LOC() -> int;
+
+pub enum MultCreditCarrier {
+    Value { car: real },
+    Empty,
+    Invalid,
+}
+
+impl MultCreditCarrier {
+    pub closed spec fn zero() -> Self {
+        MultCreditCarrier::Value { car: 0real }
+    }
+
+    pub open spec fn value(self) -> Option<real> {
+        match self {
+            MultCreditCarrier::Value { car } => Some(car),
+            _ => None,
+        }
+    }
+}
+
+impl PCM for MultCreditCarrier {
+    closed spec fn valid(self) -> bool {
+        match self {
+            MultCreditCarrier::Value { car } => 0real <= car,
+            MultCreditCarrier::Empty => true,
+            MultCreditCarrier::Invalid => false,
+        }
+    }
+
+    closed spec fn op(self, other: Self) -> Self {
+        match (self, other) {
+            (MultCreditCarrier::Value { car: c1 }, MultCreditCarrier::Value { car: c2 }) => {
+                if c1 < 0real || c2 < 0real {
+                    MultCreditCarrier::Invalid
+                } else {
+                    MultCreditCarrier::Value { car: c1 + c2 }
+                }
+            },
+            (MultCreditCarrier::Empty, x) | (x, MultCreditCarrier::Empty) => x,
+            _ => MultCreditCarrier::Invalid,
+        }
+    }
+
+    closed spec fn unit() -> Self {
+        MultCreditCarrier::Empty
+    }
+
+    proof fn closed_under_incl(a: Self, b: Self) {
+    }
+
+    proof fn commutative(a: Self, b: Self) {
+    }
+
+    proof fn associative(a: Self, b: Self, c: Self) {
+    }
+
+    proof fn op_unit(a: Self) {
+    }
+
+    proof fn unit_valid() {
+    }
+}
+
+pub struct MultCreditResource {
+    r: Resource<MultCreditCarrier>,
+}
+
+impl MultCreditResource {
+    #[verifier::type_invariant]
+    closed spec fn wf(self) -> bool {
+        self.r.loc() == MULT_EC_GLOBAL_LOC()
+    }
+
+    pub closed spec fn view(self) -> MultCreditCarrier {
+        self.r.value()
+    }
+
+    pub proof fn valid(tracked &self)
+        ensures
+            self.view().valid(),
+    {
+        self.r.validate();
+    }
+}
+
+/// Combine two multiplicative credits additively
+pub proof fn mc_combine(
+    tracked c1: MultCreditResource,
+    tracked c2: MultCreditResource,
+    v1: real,
+    v2: real,
+) -> (tracked out: MultCreditResource)
+    requires
+        c1.view() =~= (MultCreditCarrier::Value { car: v1 }),
+        c2.view() =~= (MultCreditCarrier::Value { car: v2 }),
+        v1 >= 0real,
+        v2 >= 0real,
+    ensures
+        out.view() =~= (MultCreditCarrier::Value { car: v1 + v2 }),
+{
+    use_type_invariant(&c1);
+    use_type_invariant(&c2);
+    let tracked joined = c1.r.join(c2.r);
+    MultCreditResource { r: joined }
+}
+
+/// Split one credit into two.
+pub proof fn mc_split(
+    tracked c: MultCreditResource,
+    v1: real,
+    v2: real,
+) -> (tracked out: (MultCreditResource, MultCreditResource))
+    requires
+        c.view() =~= (MultCreditCarrier::Value { car: v1 + v2 }),
+        v1 >= 0real,
+        v2 >= 0real,
+    ensures
+        out.0.view() =~= (MultCreditCarrier::Value { car: v1 }),
+        out.1.view() =~= (MultCreditCarrier::Value { car: v2 }),
+{
+    use_type_invariant(&c);
+    let tracked (r1, r2) = c.r.split(
+        MultCreditCarrier::Value { car: v1 },
+        MultCreditCarrier::Value { car: v2 },
+    );
+    (MultCreditResource { r: r1 }, MultCreditResource { r: r2 })
+}
+
+} // verus!
diff --git a/ub/dp/num_d.rs b/ub/dp/num_d.rs
new file mode 100644
index 0000000..1db756e
--- /dev/null
+++ b/ub/dp/num_d.rs
@@ -0,0 +1,172 @@
+// NumD — a concrete integer value with a ghost "distance" annotation,
+// encoding LightDP's `num(d)` type.
+//
+// Intuition: we imagine two adjacent worlds (adjacent databases).
+// `val()` is the value in world 1; `val() + dist()` is the value in
+// world 2. `dist()` is ghost.
+//
+// the `d` field is PRIVATE to this module, so external code cannot 
+// fabricate a NumD with a chosen distance. Distances are only
+// produced by:
+//   • `lit`, `from_ibig`  — always distance 0 (safe)
+//   • `add`, `clone`       — derived from existing NumD distances
+//   • `laplace`            — #[verus::trusted] Laplace-shift axiom
+//                            paired with a credit payment
+//
+// Distance rules (LightDP T-OPLUS):   ^(e1 + e2) = ^e1 + ^e2
+// Comparison  (LightDP T-ODOT)    :   (e1 < e2) == (e1+d1 < e2+d2)
+
+use vstd::prelude::*;
+use random::{IBig, ibig_from_i64, ibig_add, ibig_ge, ibig_lt, ibig_clone};
+
+verus! {
+
+use crate::dp::mult_credit::*;
+use crate::extern_spec::{ExIBig, ibig_view};
+
+pub open spec fn abs_int(x: int) -> int {
+    if x >= 0 { x } else { -x }
+}
+
+pub open spec fn abs_real(x: real) -> real {
+    if x >= 0real { x } else { -x }
+}
+
+/// A numeric value with a ghost distance annotation.
+pub struct NumD {
+    v: IBig,
+    d: Ghost<int>,
+}
+
+impl NumD {
+    /// Ghost projection of the distance. Opaque.
+    pub closed spec fn dist(&self) -> int { self.d@ }
+
+    /// World-1 value. Opaque projection through `ibig_view`.
+    pub closed spec fn val(&self) -> int { ibig_view(&self.v) }
+
+    /// World-2 value.
+    pub open spec fn shifted(&self) -> int { self.val() + self.dist() }
+
+    /// Integer literal — distance 0.
+    #[inline]
+    pub fn lit(x: i64) -> (r: NumD)
+        ensures r.val() == x as int, r.dist() == 0int,
+    {
+        NumD { v: ibig_from_i64(x), d: Ghost(0int) }
+    }
+
+    /// Wrap an existing IBig with distance 0.
+    #[inline]
+    pub fn from_ibig(v: IBig) -> (r: NumD)
+        ensures r.val() == ibig_view(&v), r.dist() == 0int,
+    {
+        NumD { v, d: Ghost(0int) }
+    }
+
+    /// T-OPLUS
+    #[inline]
+    pub fn add(&self, other: &NumD) -> (r: NumD)
+        ensures
+            r.val() == self.val() + other.val(),
+            r.dist() == self.dist() + other.dist(),
+    {
+        NumD {
+            v: ibig_add(&self.v, &other.v),
+            d: Ghost(self.d@ + other.d@),
+        }
+    }
+
+    #[inline]
+    pub fn clone(&self) -> (r: NumD)
+        ensures r.val() == self.val(), r.dist() == self.dist(),
+    {
+        NumD { v: ibig_clone(&self.v), d: self.d }
+    }
+
+    /// T-ODOT aligned ≥. Caller proves the boolean agrees across worlds;
+    /// the returned bool is therefore identical in both worlds.
+    #[inline]
+    pub fn ge_aligned(&self, other: &NumD) -> (r: bool)
+        requires
+            (self.val() >= other.val()) == (self.shifted() >= other.shifted()),
+        ensures
+            r == (self.val() >= other.val()),
+            r == (self.shifted() >= other.shifted()),
+    {
+        ibig_ge(&self.v, &other.v)
+    }
+
+    /// T-ODOT aligned <.
+    #[inline]
+    pub fn lt_aligned(&self, other: &NumD) -> (r: bool)
+        requires
+            (self.val() < other.val()) == (self.shifted() < other.shifted()),
+        ensures
+            r == (self.val() < other.val()),
+            r == (self.shifted() < other.shifted()),
+    {
+        ibig_lt(&self.v, &other.v)
+    }
+
+    /// Laplace-shift axiom — T-LAPLACE.
+    ///
+    ///   {↯× ε}  η := Lap r  {η : num(d(v)),  ↯× (ε − |d(v)|/r)}
+    ///
+    /// Operationally this samples η from the verified discrete Laplace
+    /// at scale `r = scale_num / scale_den`, then attributes a ghost
+    /// "distance" equal to `d_chooser(v)` — the imagined world-2 value
+    /// will be `v + d_chooser(v)`. The distance commitment is the
+    /// Clutch-DP Laplace coupling: for any ghost `d` we can choose,
+    /// we pay `|d|/r` credits and the shifted distribution is
+    /// statistically indistinguishable from the original.
+    ///
+    /// Since the caller cannot know the drawn value `v` before the call, 
+    /// so we can't charge `|d_chooser(v)|/r`, we need to introduce a `d_bound`
+    /// that upper-bounds `d_chooser(v)` for any `v``. You can get back the credit
+    /// 
+    /// The refund is what lets SparseVector stay tight: η₂ has
+    /// `d_bound = 2` (so every iteration reserves ε/(2N)), but on the
+    /// False branch the chooser returns 0 and the residual charge is 0.
+    /// Only the True branches actually spend, capped at N of them.
+    ///
+    /// For fixed-distance callers (SmartSum) `d_chooser` is the constant
+    /// `|_| d`, so `d_bound = |d|` and there's no gap between reservation
+    /// and actual charge.
+    ///
+    /// TRUSTED AXIOM
+    #[verus::trusted]
+    #[verifier::external_body]
+    pub fn laplace(
+        scale_num: u64,
+        scale_den: u64,
+        Ghost(d_chooser): Ghost<spec_fn(int) -> int>,
+        Ghost(d_bound): Ghost<int>,
+        Ghost(eps_in): Ghost<real>,
+        Tracked(input_credit): Tracked<MultCreditResource>,
+    ) -> (ret: (NumD, Tracked<MultCreditResource>))
+        requires
+            scale_num > 0,
+            scale_den > 0,
+            d_bound >= 0,
+            forall |v: int| abs_int(#[trigger] d_chooser(v)) <= d_bound,
+            input_credit.view() =~= (MultCreditCarrier::Value { car: eps_in }),
+            eps_in >= (d_bound as real) * (scale_den as real) / (scale_num as real),
+        ensures
+            ret.0.dist() == d_chooser(ret.0.val()),
+            ret.1@.view() =~= (MultCreditCarrier::Value {
+                car: eps_in
+                    - (abs_int(d_chooser(ret.0.val())) as real)
+                        * (scale_den as real) / (scale_num as real),
+            }),
+    {
+        let v = crate::discrete_laplace::discrete_laplace::sample_discrete_laplace_entry(
+            scale_num,
+            scale_den,
+        );
+        let ghost d = d_chooser(ibig_view(&v));
+        (NumD { v, d: Ghost(d) }, Tracked::assume_new())
+    }
+}
+
+} // verus!
diff --git a/ub/dp/num_sparse_vector.rs b/ub/dp/num_sparse_vector.rs
new file mode 100644
index 0000000..16260c8
--- /dev/null
+++ b/ub/dp/num_sparse_vector.rs
@@ -0,0 +1,261 @@
+// NumSparseVector (LightDP, Figure 11 / §6.1).
+//
+// Numeric variant of SparseVector. Three independent noise sources:
+//   η₁ : num(1)                         — threshold noise, scale 3/ε
+//   η₂ : num(2 if q[i]+η₂ ≥ T else 0)  — comparison noise, scale 6N/ε
+//   η₃ : num(−^q[i])                    — release noise, scale 3N/ε
+//
+// η₂ decides the branch exactly as in SparseVector. In the TRUE branch we
+// sample a *fresh* η₃ whose distance cancels ^q[i], so the released value
+// q[i]+η₃ has distance 0 (LightDP `num(0)`, safe to release).
+//
+// No adjacency assumption needed. Per-iter η₃ cost ≤ 1·ε/(3N), summing
+// to ≤ N·(ε/(3N)) = ε/3 over N TRUE branches.
+//
+// Budget accounting (total ε):
+//   η₁:  1 / (3/ε)         = ε/3
+//   η₂:  per TRUE 2 / (6N/ε) = ε/(3N); N TRUEs       ⇒ ε/3
+//   η₃:  per TRUE |^q[i]| / (3N/ε) ≤ ε/(3N); N TRUEs ⇒ ε/3
+
+use vstd::prelude::*;
+use random::IBig;
+
+verus! {
+
+use crate::dp::mult_credit::*;
+use crate::dp::num_d::{NumD, abs_int};
+use crate::extern_spec::ExIBig;
+
+pub fn num_sparse_vector(
+    epsilon: u64,
+    big_n: u64,
+    big_t: IBig,
+    q: &Vec<NumD>,
+    Tracked(credit): Tracked<MultCreditResource>,
+    Ghost(eps_budget): Ghost<real>,
+) -> (ret: (Vec<NumD>, Tracked<MultCreditResource>))
+    requires
+        epsilon > 0,
+        big_n > 0,
+        big_n <= u64::MAX / 6,
+        q.len() < u64::MAX,
+        forall |i: int| 0 <= i < q.len() as int ==>
+            abs_int(#[trigger] q@[i].dist()) <= 1,
+        credit.view() =~= (MultCreditCarrier::Value { car: eps_budget }),
+        // LightDP Fig. 11: total budget ε.
+        eps_budget >= (epsilon as real),
+    ensures
+        ret.0.len() <= q.len(),
+        // Privacy: every released value has distance 0 (LightDP `num(0)`).
+        forall |k: int| 0 <= k < ret.0.len() as int ==>
+            (#[trigger] ret.0@[k].dist()) == 0int,
+        // Total DP cost ≤ ε.
+        exists |r: real|
+            ret.1@.view() =~= (MultCreditCarrier::Value { car: r })
+            && r >= eps_budget - (epsilon as real),
+{
+    let mut out: Vec<NumD> = Vec::new();
+    let tracked mut cred = credit;
+    let ghost mut spent: real = 0real;
+    let ghost mut eta3_cum: real = 0real;   // cumulative η₃ cost so far
+
+    // ─── η₁ : scale 3/ε, distance 1, cost ε/3 ─────────────────────────
+    let (eta_1, Tracked(cred1)) = NumD::laplace(
+        3, epsilon, Ghost(|_v: int| 1int), Ghost(1int),
+        Ghost(eps_budget), Tracked(cred),
+    );
+    proof {
+        cred = cred1;
+        spent = (epsilon as real) / 3real;
+        assert((abs_int(1int) as real) * (epsilon as real) / (3 as real)
+               == (epsilon as real) / 3real) by(nonlinear_arith);
+        assert(spent == (epsilon as real) / 3real
+               + (0 as real) * (epsilon as real) / (3real * (big_n as real))
+               + (0 as real))
+        by(nonlinear_arith)
+            requires spent == (epsilon as real) / 3real, big_n > 0;
+    }
+
+    // T_threshold = T + η₁ → distance 1.
+    let t_threshold: NumD = NumD::from_ibig(big_t).add(&eta_1);
+
+    let mut c1: u64 = 0;
+    let mut i: u64 = 0;
+
+    while c1 < big_n && (i as usize) < q.len()
+        invariant
+            big_n > 0,
+            big_n <= u64::MAX / 6,
+            epsilon > 0,
+            eps_budget >= (epsilon as real),
+            0 <= c1 as int <= big_n as int,
+            0 <= i as int <= q.len() as int,
+            q.len() < u64::MAX,
+            out.len() <= i as int,
+            out.len() <= c1 as int,
+            t_threshold.dist() == 1int,
+            cred.view() =~= (MultCreditCarrier::Value { car: eps_budget - spent }),
+            forall |k: int| 0 <= k < q.len() as int ==>
+                abs_int(#[trigger] q@[k].dist()) <= 1,
+            // Budget decomposition:
+            //   spent = ε/3  +  c1·ε/(3N)       [η₁ + η₂ cumulative]
+            //                +  eta3_cum         [η₃ cumulative]
+            //   with 0 ≤ eta3_cum ≤ c1 · ε/(3N).
+            spent == (epsilon as real) / 3real
+                   + (c1 as real) * (epsilon as real) / (3real * (big_n as real))
+                   + eta3_cum,
+            0real <= eta3_cum,
+            eta3_cum <= (c1 as real) * (epsilon as real) / (3real * (big_n as real)),
+            spent >= 0real,
+            spent <= (epsilon as real),
+            // Privacy of outputs.
+            forall |k: int| 0 <= k < out.len() as int ==>
+                (#[trigger] out@[k].dist()) == 0int,
+        decreases q.len() as int - i as int,
+    {
+        let qi: &NumD = &q[i as usize];
+        let ghost qi_d = qi.dist();
+
+        let ghost qi_v = qi.val();
+        let ghost t_v = t_threshold.val();
+        let ghost chooser2: spec_fn(int) -> int = |v: int|
+            if qi_v + v >= t_v { 2int } else { 0int };
+
+        // Pre-call reservation: credit ≥ 2 · ε / (6N) = ε/(3N).
+        proof {
+            assert(eps_budget - spent
+                   >= (2int as real) * (epsilon as real) / ((6 * big_n) as real))
+            by(nonlinear_arith)
+                requires
+                    eps_budget >= (epsilon as real),
+                    spent == (epsilon as real) / 3real
+                           + (c1 as real) * (epsilon as real) / (3real * (big_n as real))
+                           + eta3_cum,
+                    eta3_cum <= (c1 as real) * (epsilon as real) / (3real * (big_n as real)),
+                    (c1 as real) + 1real <= big_n as real,
+                    big_n > 0;
+        }
+
+        let (eta_2, Tracked(cred2)) = NumD::laplace(
+            6 * big_n, epsilon, Ghost(chooser2), Ghost(2int),
+            Ghost(eps_budget - spent), Tracked(cred),
+        );
+        proof { cred = cred2; }
+
+        let lhs: NumD = qi.add(&eta_2);
+
+        // T-ODOT for the comparison (same as SparseVector).
+        let is_above: bool = lhs.ge_aligned(&t_threshold);
+
+        if is_above {
+            // η₂ contributed ε/(3N); update spent.
+            proof {
+                let prev_spent = spent;
+                spent = spent + (epsilon as real) / (3real * (big_n as real));
+                assert((abs_int(chooser2(eta_2.val())) as real) * (epsilon as real)
+                       / ((6 * big_n) as real)
+                       == (epsilon as real) / (3real * (big_n as real)))
+                by(nonlinear_arith)
+                    requires
+                        chooser2(eta_2.val()) == 2int,
+                        big_n > 0;
+                // New formula: spent = ε/3 + (c1+1)·ε/(3N) + eta3_cum.
+                assert(spent == (epsilon as real) / 3real
+                       + ((c1 + 1) as real) * (epsilon as real) / (3real * (big_n as real))
+                       + eta3_cum)
+                by(nonlinear_arith)
+                    requires
+                        spent == prev_spent + (epsilon as real) / (3real * (big_n as real)),
+                        prev_spent == (epsilon as real) / 3real
+                            + (c1 as real) * (epsilon as real) / (3real * (big_n as real))
+                            + eta3_cum,
+                        epsilon > 0, big_n > 0;
+            }
+
+            // ─── η₃ : scale 3N/ε, distance −^q[i]. ──────────────────
+            // Per-TRUE cost ≤ 1·ε/(3N). Over N TRUEs, η₃_cum ≤ ε/3.
+            let ghost chooser3: spec_fn(int) -> int = |_v: int| -qi_d;
+
+            // Pre-call reservation: credit ≥ 1 · ε / (3N) = ε/(3N).
+            proof {
+                assert(eps_budget - spent
+                       >= (1int as real) * (epsilon as real) / ((3 * big_n) as real))
+                by(nonlinear_arith)
+                    requires
+                        eps_budget >= (epsilon as real),
+                        spent == (epsilon as real) / 3real
+                               + ((c1 + 1) as real)
+                                 * (epsilon as real) / (3real * (big_n as real))
+                               + eta3_cum,
+                        eta3_cum <= (c1 as real)
+                                    * (epsilon as real) / (3real * (big_n as real)),
+                        (c1 as int + 1) <= big_n as int,
+                        epsilon > 0, big_n > 0;
+            }
+
+            let (eta_3, Tracked(cred3)) = NumD::laplace(
+                3 * big_n, epsilon, Ghost(chooser3), Ghost(1int),
+                Ghost(eps_budget - spent), Tracked(cred),
+            );
+            proof {
+                let prev_eta3_cum = eta3_cum;
+                // η₃ actual cost = |−qi_d|·ε/(3N) ≤ ε/(3N).
+                eta3_cum = eta3_cum + (abs_int(-qi_d) as real)
+                                      * (epsilon as real) / (3real * (big_n as real));
+                spent = spent + (abs_int(-qi_d) as real)
+                                 * (epsilon as real) / (3real * (big_n as real));
+                cred = cred3;
+                // eta3_cum ≤ (c1+1)·ε/(3N).
+                assert(eta3_cum <= ((c1 + 1) as real)
+                                  * (epsilon as real) / (3real * (big_n as real)))
+                by(nonlinear_arith)
+                    requires
+                        eta3_cum == prev_eta3_cum + (abs_int(-qi_d) as real)
+                                    * (epsilon as real) / (3real * (big_n as real)),
+                        prev_eta3_cum <= (c1 as real)
+                                         * (epsilon as real) / (3real * (big_n as real)),
+                        abs_int(-qi_d) <= 1,
+                        big_n > 0;
+                // eta3_cum ≥ 0.
+                assert(eta3_cum >= 0real) by(nonlinear_arith)
+                    requires
+                        eta3_cum == prev_eta3_cum + (abs_int(-qi_d) as real)
+                                    * (epsilon as real) / (3real * (big_n as real)),
+                        prev_eta3_cum >= 0real,
+                        big_n > 0;
+            }
+
+            // q[i] + η₃: distance 0 (^q[i] + (−^q[i]) = 0), safe to release.
+            let value: NumD = qi.add(&eta_3);
+            out.push(value);
+            c1 = c1 + 1;
+
+            proof {
+                // Re-establish spent ≤ ε at loop-invariant level.
+                assert(spent <= (epsilon as real)) by(nonlinear_arith)
+                    requires
+                        spent == (epsilon as real) / 3real
+                               + (c1 as real) * (epsilon as real) / (3real * (big_n as real))
+                               + eta3_cum,
+                        eta3_cum <= (c1 as real)
+                                    * (epsilon as real) / (3real * (big_n as real)),
+                        (c1 as int) <= big_n as int,
+                        big_n > 0;
+            }
+        } else {
+            // FALSE branch: chooser2 returns 0, so η₂'s actual cost is 0
+            // and cred2.view() = eps_budget − spent already.
+            proof {
+                assert((abs_int(chooser2(eta_2.val())) as real) * (epsilon as real)
+                       / ((6 * big_n) as real) == 0real) by(nonlinear_arith)
+                    requires chooser2(eta_2.val()) == 0int, big_n > 0;
+            }
+        }
+
+        i = i + 1;
+    }
+
+    (out, Tracked(cred))
+}
+
+} // verus!
diff --git a/ub/dp/smart_sum.rs b/ub/dp/smart_sum.rs
new file mode 100644
index 0000000..2b3bc9a
--- /dev/null
+++ b/ub/dp/smart_sum.rs
@@ -0,0 +1,301 @@
+// SmartSum (LightDP, Figure 12)
+//
+//   precondition: only one entry of q may have nonzero distance
+//   epsilon, M: num(0); (note: i don't know why LightDP introduced this T thing...)
+//   q : list num(*); 
+//   out : list num(0);
+//   next, n, i : num(0);
+//   sum : num(*);
+//   eta_1 : num(-^sum-^q[i]); 
+//   eta_2 : num(-^q[i])
+//
+// LightDP-style guarantee (Fig. 12):
+//   • Privacy: every released value has distance 0.
+//   • Budget:  total cost ≤ 2·ε under the adjacency assumption
+//              (at most one q[i] has nonzero distance).
+//
+// Each q[j] shows up in at most two cost events:
+//   1. Its own iteration i = j contributes |^q[j]| · ε.
+//   2. The window-close that covers j (if j wasn't itself closed)
+//      contributes another |^q[j]| · ε via the accumulated ^sum.
+// Under adjacency only one j has |^q[j]| > 0, so total ≤ 2|^q[j]|·ε ≤ 2·ε.
+
+use vstd::prelude::*;
+use random::IBig;
+
+verus! {
+
+use crate::dp::mult_credit::*;
+use crate::dp::num_d::{NumD, abs_int};
+
+/// Sum of `q[j].dist()` for j ∈ [lo, hi).
+pub open spec fn dsum(q: Seq<NumD>, lo: int, hi: int) -> int
+    decreases hi - lo when lo <= hi
+{
+    if lo >= hi { 0int } else { q[lo].dist() + dsum(q, lo + 1, hi) }
+}
+
+/// `dx` witnesses adjacency: every other index has zero distance.
+pub open spec fn is_adjacency_witness(q: Seq<NumD>, dx: int) -> bool {
+    0 <= dx < q.len()
+    && (forall |i: int| 0 <= i < q.len() && i != dx ==>
+            #[trigger] q[i].dist() == 0int)
+}
+
+proof fn lemma_dsum_extend(q: Seq<NumD>, lo: int, hi: int)
+    requires lo <= hi,
+    ensures dsum(q, lo, hi + 1) == dsum(q, lo, hi) + q[hi].dist(),
+    decreases hi - lo,
+{
+    if lo == hi {
+        assert(dsum(q, lo + 1, lo + 1) == 0int);
+    } else {
+        lemma_dsum_extend(q, lo + 1, hi);
+    }
+}
+
+/// Under the adjacency assumption (only `d_idx` has nonzero distance),
+/// the window sum equals `^q[d_idx]` when d_idx is in [lo, hi), else 0.
+proof fn lemma_dsum_adjacency(q: Seq<NumD>, lo: int, hi: int, d_idx: int)
+    requires
+        0 <= lo <= hi <= q.len(),
+        0 <= d_idx < q.len(),
+        forall |j: int| #![auto] 0 <= j < q.len() && j != d_idx ==> q[j].dist() == 0int,
+    ensures
+        lo <= d_idx < hi ==> dsum(q, lo, hi) == q[d_idx].dist(),
+        !(lo <= d_idx < hi) ==> dsum(q, lo, hi) == 0int,
+    decreases hi - lo,
+{
+    if lo >= hi {
+        return;
+    }
+    lemma_dsum_adjacency(q, lo + 1, hi, d_idx);
+}
+
+pub fn smart_sum(
+    epsilon: u64,
+    big_m: u64,
+    q: &Vec<NumD>,
+    Tracked(credit): Tracked<MultCreditResource>,
+    Ghost(eps_budget): Ghost<real>,
+) -> (ret: (Vec<NumD>, Tracked<MultCreditResource>))
+    requires
+        epsilon > 0,
+        big_m > 0,
+        q.len() < u64::MAX,
+        forall |i: int| 0 <= i < q.len() as int ==>
+            abs_int(#[trigger] q@[i].dist()) <= 1,
+        // Adjacency: at most one index may have nonzero distance.
+        exists |dx: int| #[trigger] is_adjacency_witness(q@, dx),
+        credit.view() =~= (MultCreditCarrier::Value { car: eps_budget }),
+        eps_budget >= 2real * (epsilon as real),
+    ensures
+        ret.0.len() == q.len(),
+        // Privacy: every released value has distance 0.
+        forall |k: int| 0 <= k < ret.0.len() as int ==>
+            (#[trigger] ret.0@[k].dist()) == 0int,
+        // Budget: total credits spent ≤ 2·ε.
+        exists |r: real|
+            ret.1@.view() =~= (MultCreditCarrier::Value { car: r })
+            && r >= eps_budget - 2real * (epsilon as real),
+{
+    // Extract the differing index from the existential precondition.
+    let ghost d_idx: int = choose |dx: int| is_adjacency_witness(q@, dx);
+
+    let mut out: Vec<NumD> = Vec::new();
+    let mut next: NumD = NumD::lit(0);
+    let mut n:    NumD = NumD::lit(0);
+    let mut sum:  NumD = NumD::lit(0);
+    let ghost mut last_reset: int = 0;
+    let ghost mut paid_d: nat = 0;   // # times d_idx has been charged (≤ 2)
+    let mut i: u64 = 0;
+    let tracked mut cred = credit;
+    let ghost mut spent: real = 0real;
+
+    while i < q.len() as u64
+        invariant
+            0 <= i as int <= q.len() as int,
+            0 <= last_reset <= i as int,
+            out.len() == i as int,
+            last_reset % (big_m as int) == 0,
+            (i as int) - last_reset <= (big_m as int) - 1,
+            sum.dist() == dsum(q@, last_reset, i as int),
+            next.dist() == 0,
+            n.dist() == 0,
+            // Adjacency carried through.
+            0 <= d_idx < q.len() as int,
+            abs_int(q@[d_idx].dist()) <= 1,
+            forall |j: int| 0 <= j < q.len() as int && j != d_idx ==>
+                #[trigger] q@[j].dist() == 0int,
+            // LightDP accounting: d_idx contributes at most twice.
+            // Position-indexed bound on paid_d:
+            //   i ≤ d_idx                  ⇒ paid_d = 0
+            //   i > d_idx, last_reset ≤ d_idx ⇒ paid_d ≤ 1  (own-iter paid, window open)
+            //   last_reset > d_idx          ⇒ paid_d ≤ 2  (window closed)
+            (i as int) <= d_idx ==> paid_d == 0,
+            (i as int) > d_idx && last_reset <= d_idx ==> paid_d <= 1,
+            paid_d <= 2,
+            spent >= 0real,
+            spent <= (paid_d as real)
+                     * (abs_int(q@[d_idx].dist()) as real) * (epsilon as real),
+            cred.view() =~= (MultCreditCarrier::Value { car: eps_budget - spent }),
+            q.len() < u64::MAX,
+            big_m > 0,
+            epsilon > 0,
+            eps_budget >= 2real * (epsilon as real),
+            forall |k: int| 0 <= k < out.len() as int ==>
+                (#[trigger] out@[k].dist()) == 0int,
+        decreases q.len() as int - i as int,
+    {
+        let ghost prev_spent = spent;
+        let ghost prev_paid = paid_d;
+        let ghost prev_sum_d = sum.dist();
+        let ghost qi_d = q@[i as int].dist();
+        let ghost qd_d = q@[d_idx].dist(); // also ^q[d_idx]
+
+        // Under adjacency, |sum.dist()| ≤ |^q[d_idx]| (= 0 unless d_idx is in
+        // the current open window). qi_d = 0 unless i == d_idx.
+        proof {
+            lemma_dsum_adjacency(q@, last_reset, i as int, d_idx);
+        }
+
+        let ghost j = (i as int) - last_reset;
+        if (i + 1) % big_m == 0 {
+            // Window close: η₁ has distance −(^sum + ^q[i]).
+            let ghost d1: int = -(prev_sum_d + qi_d);
+            // |d1| ≤ |qi_d|: sum and qi_d can't both be nonzero
+
+            proof {
+                // Pre-call reservation: |d1|·ε ≤ |qd_d|·ε ≤ ε, and
+                // eps_budget − spent ≥ 2·ε − paid_d·|qd_d|·ε ≥ |qd_d|·ε
+                // (since paid_d ≤ 2 − 1 = 1 whenever |d1| > 0, by the
+                // positional invariants).
+                assert((abs_int(d1) as real) * (epsilon as real)
+                       <= eps_budget - spent) by(nonlinear_arith)
+                    requires
+                        abs_int(d1) <= abs_int(qd_d),
+                        prev_paid == 2nat ==> abs_int(d1) == 0,
+                        eps_budget >= 2real * (epsilon as real),
+                        spent <= (prev_paid as real)
+                                 * (abs_int(qd_d) as real) * (epsilon as real),
+                        prev_paid <= 2, abs_int(qd_d) <= 1,
+                        epsilon > 0;
+            }
+
+            let (eta1, Tracked(cred2)) = NumD::laplace(
+                1, epsilon, Ghost(|_v: int| d1), Ghost(abs_int(d1)),
+                Ghost(eps_budget - spent), Tracked(cred),
+            );
+            proof {
+                cred = cred2;
+                assert((abs_int(d1) as real) * (epsilon as real) >= 0real) by(nonlinear_arith)
+                    requires abs_int(d1) >= 0, epsilon > 0;
+                spent = spent + (abs_int(d1) as real) * (epsilon as real);
+                // Bump paid_d iff the actual cost came from d_idx.
+                if last_reset <= d_idx && d_idx <= (i as int) {
+                    paid_d = paid_d + 1;
+                }
+            }
+
+            let qi: &NumD = &q[i as usize];
+            n = n.add(&sum).add(qi).add(&eta1);
+            assert(n.dist() == 0);
+            next = n.clone();
+            sum = NumD::lit(0);
+            out.push(next.clone());
+
+            proof {
+                last_reset = i as int + 1;
+                assert(spent <= (paid_d as real)
+                             * (abs_int(qd_d) as real) * (epsilon as real))
+                by(nonlinear_arith)
+                    requires
+                        spent == prev_spent + (abs_int(d1) as real) * (epsilon as real),
+                        prev_spent <= (prev_paid as real)
+                                      * (abs_int(qd_d) as real) * (epsilon as real),
+                        abs_int(d1) <= abs_int(qd_d),
+                        (paid_d == prev_paid + 1) || (paid_d == prev_paid && abs_int(d1) == 0),
+                        epsilon > 0;
+            }
+        } else {
+            // Intra-window. Force j < big_m − 1 (else j+1 == big_m and
+            // (i+1) % big_m would be 0, contradicting the branch).
+            proof {
+                if j == (big_m as int) - 1 {
+                    assert((i as int + 1) % (big_m as int) == 0) by(nonlinear_arith)
+                        requires
+                            last_reset % (big_m as int) == 0,
+                            (i as int + 1) == last_reset + (big_m as int),
+                            big_m > 0;
+                }
+            }
+
+            let ghost d2: int = -qi_d;
+
+            // Pre-call reservation: |d2| ≤ |^q[d_idx]|, with d2 = 0 if i ≠ d_idx.
+            proof {
+                assert((abs_int(d2) as real) * (epsilon as real)
+                       <= eps_budget - spent) by(nonlinear_arith)
+                    requires
+                        abs_int(d2) <= abs_int(qd_d),
+                        (i as int) != d_idx ==> abs_int(d2) == 0,
+                        eps_budget >= 2real * (epsilon as real),
+                        spent <= (prev_paid as real)
+                                 * (abs_int(qd_d) as real) * (epsilon as real),
+                        (i as int) == d_idx ==> prev_paid == 0nat,
+                        prev_paid <= 2, abs_int(qd_d) <= 1,
+                        epsilon > 0;
+            }
+
+            let (eta2, Tracked(cred2)) = NumD::laplace(
+                1, epsilon, Ghost(|_v: int| d2), Ghost(abs_int(d2)),
+                Ghost(eps_budget - spent), Tracked(cred),
+            );
+            proof {
+                cred = cred2;
+                assert((abs_int(d2) as real) * (epsilon as real) >= 0real) by(nonlinear_arith)
+                    requires abs_int(d2) >= 0, epsilon > 0;
+                spent = spent + (abs_int(d2) as real) * (epsilon as real);
+                if (i as int) == d_idx {
+                    paid_d = paid_d + 1;
+                }
+            }
+
+            let qi: &NumD = &q[i as usize];
+            next = next.add(qi).add(&eta2);
+            sum = sum.add(qi);
+            out.push(next.clone());
+
+            proof {
+                lemma_dsum_extend(q@, last_reset, i as int);
+                assert(spent <= (paid_d as real)
+                             * (abs_int(qd_d) as real) * (epsilon as real))
+                by(nonlinear_arith)
+                    requires
+                        spent == prev_spent + (abs_int(d2) as real) * (epsilon as real),
+                        prev_spent <= (prev_paid as real)
+                                      * (abs_int(qd_d) as real) * (epsilon as real),
+                        abs_int(d2) <= abs_int(qd_d),
+                        (paid_d == prev_paid + 1) || (paid_d == prev_paid && abs_int(d2) == 0),
+                        epsilon > 0;
+            }
+        }
+
+        i = i + 1;
+    }
+
+    // Bound paid_d · |qd_d| · ε ≤ 2 · ε. So spent ≤ 2·ε, hence residual ≥ eps_budget − 2·ε.
+    proof {
+        assert(spent <= 2real * (epsilon as real)) by(nonlinear_arith)
+            requires
+                spent <= (paid_d as real)
+                         * (abs_int(q@[d_idx].dist()) as real) * (epsilon as real),
+                paid_d <= 2,
+                abs_int(q@[d_idx].dist()) <= 1,
+                epsilon > 0;
+    }
+
+    (out, Tracked(cred))
+}
+
+} // verus!
diff --git a/ub/dp/sparse_vector.rs b/ub/dp/sparse_vector.rs
new file mode 100644
index 0000000..89ed483
--- /dev/null
+++ b/ub/dp/sparse_vector.rs
@@ -0,0 +1,179 @@
+// SparseVector (LightDP, Figure 1).
+//
+//   precondition : forall i (-1 <= ^q[i] <= 1);
+//   T, N, len, epsilon : num(0);  
+//   q : list num(*);  
+//   out : list bool_0;
+//   c1, c2, i : num(0); 
+//   T_threshold, eta_1 : num(1);
+//   eta_2 : num(2 if q[i] + eta_2 >= T_threshold else 0)
+//
+// Budget (multiplicative credits, tight actual-cost residual):
+//   η₁       d = 1, scale 2/ε    ⇒ cost ε/2
+//   η₂ True  d = 2, scale 4N/ε   ⇒ cost ε/(2N)
+//   η₂ False d = 0               ⇒ cost 0
+// At most N True branches ⇒ total ≤ ε/2 + N · ε/(2N) = ε.
+
+use vstd::prelude::*;
+use random::IBig;
+
+verus! {
+
+use crate::dp::mult_credit::*;
+use crate::dp::num_d::{NumD, abs_int};
+use crate::extern_spec::ExIBig;
+
+pub fn sparse_vector(
+    epsilon: u64,
+    big_n: u64,
+    big_t: IBig,
+    q: &Vec<NumD>,
+    Tracked(credit): Tracked<MultCreditResource>,
+    Ghost(eps_budget): Ghost<real>,
+) -> (ret: (Vec<bool>, Tracked<MultCreditResource>))
+    requires
+        epsilon > 0,
+        big_n > 0,
+        big_n <= u64::MAX / 4,
+        q.len() < u64::MAX,
+        forall |i: int| 0 <= i < q.len() as int ==>
+            abs_int(#[trigger] q@[i].dist()) <= 1,
+        credit.view() =~= (MultCreditCarrier::Value { car: eps_budget }),
+        eps_budget >= (epsilon as real),
+    ensures
+        ret.0.len() <= q.len(),
+        exists |r: real|
+            ret.1@.view() =~= (MultCreditCarrier::Value { car: r })
+            && r >= eps_budget - (epsilon as real),
+{
+    let mut out: Vec<bool> = Vec::new();
+    let tracked mut cred = credit;
+    let ghost mut spent: real = 0real;
+
+    // η₁ : fixed d = 1, scale 2/ε → pay ε/2.
+    let (eta_1, Tracked(cred1)) = NumD::laplace(
+        2, epsilon, Ghost(|_v: int| 1int), Ghost(1int),
+        Ghost(eps_budget), Tracked(cred),
+    );
+    // ε/2 + c₁ · ε/(2N) at c₁ = 0.
+    proof {
+        cred = cred1;
+        spent = (epsilon as real) / 2real;
+        assert((abs_int(1int) as real) * (epsilon as real) / (2 as real)
+               == (epsilon as real) / 2real) by(nonlinear_arith);
+        assert(spent == (epsilon as real) / 2real
+            + (0 as real) * (epsilon as real) / (2real * (big_n as real)))
+        by(nonlinear_arith)
+            requires spent == (epsilon as real) / 2real, epsilon > 0, big_n > 0;
+    }
+
+    // T_threshold = T + η₁ → distance 1.
+    let t_threshold: NumD = NumD::from_ibig(big_t).add(&eta_1);
+
+    let mut c1: u64 = 0;
+    let mut c2: u64 = 0;
+    let mut i: u64 = 0;
+
+    while c1 < big_n && (i as usize) < q.len()
+        // TODO comment: lightdp doesn't really have this i < q.len() check...
+        invariant
+            big_n > 0,
+            big_n <= u64::MAX / 4,
+            epsilon > 0,
+            eps_budget >= (epsilon as real),
+            0 <= c1 as int <= big_n as int,
+            0 <= c2 as int <= q.len() as int,
+            c1 as int + c2 as int == i as int,
+            0 <= i as int <= q.len() as int,
+            q.len() < u64::MAX,
+            out.len() == i as int,
+            t_threshold.dist() == 1int,
+            cred.view() =~= (MultCreditCarrier::Value { car: eps_budget - spent }),
+            spent == (epsilon as real) / 2real
+                + (c1 as real) * (epsilon as real) / (2real * (big_n as real)),
+            spent <= (epsilon as real),
+            forall |k: int| 0 <= k < q.len() as int ==>
+                abs_int(#[trigger] q@[k].dist()) <= 1,
+        decreases q.len() as int - i as int,
+    {
+        let qi: &NumD = &q[i as usize];
+        let ghost qi_v = qi.val();
+        let ghost t_v = t_threshold.val();
+
+        // d(v) = 2 if q[i] + v ≥ T else 0.
+        let ghost chooser: spec_fn(int) -> int = |v: int|
+            if qi_v + v >= t_v { 2int } else { 0int };
+
+        // Pre-call reservation: credit ≥ 2 · ε / (4N) = ε/(2N).
+        proof {
+            assert(eps_budget - spent
+                   >= (2int as real) * (epsilon as real) / ((4 * big_n) as real))
+            by(nonlinear_arith)
+                requires
+                    eps_budget >= (epsilon as real),
+                    spent == (epsilon as real) / 2real
+                        + (c1 as real) * (epsilon as real) / (2real * (big_n as real)),
+                    (c1 as real) + 1real <= big_n as real,
+                    epsilon > 0, big_n > 0;
+        }
+
+        let (eta_2, Tracked(cred2)) = NumD::laplace(
+            4 * big_n, epsilon, Ghost(chooser), Ghost(2int),
+            Ghost(eps_budget - spent), Tracked(cred),
+        );
+        // Thread residual credit. The actual charge (|d|/r) gets
+        // added to `spent` below, once we know the branch outcome.
+        proof { cred = cred2; }
+
+        // T-ODOT: the ≥ comparison agrees between adjacent worlds because
+        //   True  (d=2): shifted diff = (lhs.v − t.v) + (^q[i] + 1) ≥ 0
+        //   False (d=0): shifted diff = (lhs.v − t.v) + (^q[i] − 1) ≤ 0
+        // given |^q[i]| ≤ 1. `ge_aligned`'s precondition discharges the
+        // alignment proof, so the returned bool is identical in both worlds —
+        // that's the ε-DP output witness.
+        let is_above: bool = qi.add(&eta_2).ge_aligned(&t_threshold);
+
+        if is_above {
+            // chooser = 2 ⇒ cost ε/(2N). Re-establish loop invariant's
+            // spent formula with c₁ incremented.
+            proof {
+                let prev_spent = spent;
+                spent = spent + (epsilon as real) / (2real * (big_n as real));
+                assert((abs_int(chooser(eta_2.val())) as real) * (epsilon as real)
+                       / ((4 * big_n) as real)
+                       == (epsilon as real) / (2real * (big_n as real)))
+                by(nonlinear_arith)
+                    requires
+                        chooser(eta_2.val()) == 2int,
+                        big_n > 0;
+                assert(spent == (epsilon as real) / 2real
+                    + ((c1 + 1) as real) * (epsilon as real) / (2real * (big_n as real))
+                    && spent <= (epsilon as real)) by(nonlinear_arith)
+                    requires
+                        spent == prev_spent + (epsilon as real) / (2real * (big_n as real)),
+                        prev_spent == (epsilon as real) / 2real
+                            + (c1 as real) * (epsilon as real) / (2real * (big_n as real)),
+                        (c1 as int + 1) <= big_n as int,
+                        epsilon > 0, big_n > 0;
+            }
+            out.push(is_above);  // value is `true`, aligned
+            c1 = c1 + 1;
+        } else {
+            // chooser = 0 ⇒ actual cost is 0, so `spent` doesn't change.
+            // We just need to show the laplace residual matches the
+            // invariant (|0| · ε / (4N) simplifies to 0).
+            proof {
+                assert((abs_int(chooser(eta_2.val())) as real) * (epsilon as real)
+                       / ((4 * big_n) as real) == 0real) by(nonlinear_arith)
+                    requires chooser(eta_2.val()) == 0int, (4 * big_n) as real > 0real;
+            }
+            out.push(is_above);  // value is `false`, aligned
+            c2 = c2 + 1;
+        }
+
+        i = i + 1;
+    }
+    (out, Tracked(cred))
+}
+
+} // verus!
diff --git a/ub/extern_spec.rs b/ub/extern_spec.rs
index a3aab8a..60a7deb 100644
--- a/ub/extern_spec.rs
+++ b/ub/extern_spec.rs
@@ -5,7 +5,7 @@
 
 use vstd::prelude::*;
 
-use random::{UBig, ubig_zero, ubig_succ, ubig_pred, ubig_is_zero, ubig_add, ubig_mul, ubig_mul_u64, ubig_from_u64, ubig_is_odd, ubig_div_u64, ubig_add_u64, IBig, ibig_from_ubig, ibig_neg, ibig_is_zero};
+use random::{UBig, ubig_zero, ubig_succ, ubig_pred, ubig_is_zero, ubig_add, ubig_mul, ubig_mul_u64, ubig_from_u64, ubig_is_odd, ubig_div_u64, ubig_add_u64, IBig, ibig_from_ubig, ibig_neg, ibig_is_zero, ibig_from_i64, ibig_add, ibig_ge, ibig_lt, ibig_clone};
 
 verus! {
 
@@ -81,4 +81,19 @@ pub assume_specification[ random::ibig_neg ](n: IBig) -> (ret: IBig)
 pub assume_specification[ random::ibig_is_zero ](n: &IBig) -> (ret: bool)
     ensures ret == (ibig_view(n) == 0int);
 
+pub assume_specification[ random::ibig_from_i64 ](n: i64) -> (ret: IBig)
+    ensures ibig_view(&ret) == n as int;
+
+pub assume_specification[ random::ibig_add ](a: &IBig, b: &IBig) -> (ret: IBig)
+    ensures ibig_view(&ret) == ibig_view(a) + ibig_view(b);
+
+pub assume_specification[ random::ibig_ge ](a: &IBig, b: &IBig) -> (ret: bool)
+    ensures ret == (ibig_view(a) >= ibig_view(b));
+
+pub assume_specification[ random::ibig_lt ](a: &IBig, b: &IBig) -> (ret: bool)
+    ensures ret == (ibig_view(a) < ibig_view(b));
+
+pub assume_specification[ random::ibig_clone ](n: &IBig) -> (ret: IBig)
+    ensures ibig_view(&ret) == ibig_view(n);
+
 } // verus!
diff --git a/ub/lib.rs b/ub/lib.rs
index e8259b4..f2df486 100644
--- a/ub/lib.rs
+++ b/ub/lib.rs
@@ -9,6 +9,7 @@ pub mod geo_dist;
 pub mod ho_rej_samp;
 pub mod discrete_laplace;
 pub mod random_walk;
+pub mod dp;
 
 // `fn main` is outside of `verus!`, so it is not checked
 fn main() {