lightdp

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()
+}

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;

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!

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!