clutch.gen_diffpriv.examples.randomized_response

A LOCAL differential-privacy example on the GENERIC language: RANDOMISED RESPONSE releases a private bit ε-differentially-privately. This is the canonical coin-based local-DP mechanism, and the VALIDATING example for the RR_coin foundation (previously only canary-tested in lib/coin.v / lib/randomized_response.v). The mechanism is RR_release(x) := x XOR c, c ~ RR_coin(num, den), i.e. it XOR-perturbs the input bit x with a noisy coin c that is true with probability exp(ε)/(exp(ε)+1), ε = num/den. Equivalently it reports x truthfully with probability p = exp(ε)/(exp(ε)+1) and flips with probability 1 − p; the ratio between the two output probabilities is p/(1−p) = exp(ε), so releasing the bit is ε-DP with ZERO additive δ (a purely MULTIPLICATIVE guarantee) on the discrete bit metric dbool. All the per-distribution machinery (the RR notation, the wp_couple_RR coupling rules, their soundness) lives in the reusable library gen_diffpriv.lib.randomized_response. A client "enables" RR for its development by declaring a signature containing RR_coin and providing a one-line SampleIn RR_coin _ instance; after that the section needs nothing but Context `{!diffprivGS Srr Σ}.

The randomised-response release program: XOR the private input bit with a noisy RR_coin draw at privacy rate ε = num/den.

The RR MECHANISM is ε-DP on the bit metric: releasing a private bit via randomised response is (ε, 0)-differentially-private, ε = num/den ≥ 0. For adjacent inputs (bits at distance 1) the spec coin flips — costing the full ε — so that the two XOR-released bits agree; for identical inputs the release is coupled exactly at zero cost. This is the canonical local-DP guarantee, validating the coin foundation on a real DP proof.