Skip to main content

Crate nucleus_mechanism_vcg

Crate nucleus_mechanism_vcg 

Source
Expand description

§nucleus-mechanism-vcg — Pigouvian-VCG lifter for the substrate

Implements the Economic projection functor from nucleus_substrate_core specialized to Pigouvian-VCG auctions. Lifts a cleared auction (single-good Vickrey or knapsack-VCG) into the typed body of a Projection::Economic variant.

§Two variants, one wire shape

Both Vickrey and knapsack-VCG share the {auction, bids, outcome} skeleton. Only the outcome field differs:

{"kind":"economic","body":{
   "version": 1,
   "mechanism": "vickrey",
   "auction": { ... PostedAuction ... },
   "bids":    [ ... AgentBids ... ],
   "outcome": { "winner_spiffe_id": "...", "clearing_price_micro_usd": 250000 }
}}

For knapsack-VCG:

{"kind":"economic","body":{
   "version": 1,
   "mechanism": "vcg_knapsack",
   "auction": { ... },
   "bids":    [ ... ],
   "outcome": { "winners": [["spiffe://...", 750000], ...] }
}}

§Verifier invariants

verify_economic_projection_shape checks structural well-formedness only. The cryptographic check (signature over canonical bytes) lives on the parent Receipt. The shape invariants:

  1. Body version matches ECONOMIC_BODY_VERSION (1).
  2. mechanism is one of the two stable strings.
  3. For Vickrey: if winner_spiffe_id.is_some(), the winner must appear in bids as an agent_spiffe_id.
  4. For VCG: every entry in outcome.winners must reference a SPIFFE id that appears in bids.

Truthfulness (the mechanism property) is proven once, in Lean (formal/Nucleus/Auctions/VcgPigouTruthful.lean). The Aeneas parity proptest binds the kernel to the extracted Rust impl. This crate doesn’t re-prove either — it provides the wire shape that lets a receipt carry the outcome.

Structs§

ExternalityProfile
One agent’s claims about the externalities they would impose if awarded a given auction. Each claim is signed by a trusted oracle; the hub verifies signatures before the VCG path consumes them.
OpaqueSignedClaim
A signed externality claim, opaque from the SDK’s perspective. The hub deserializes the inner signed_bytes against the oracle’s verifying key; SDK consumers pass through whatever bytes they received from their oracle.
ReExportedAgentBid
ReExportedMatchResult
ReExportedPostedAuction
ReExportedVcgMatchResult
VcgKnapsackBody
Body of a knapsack-VCG-cleared auction’s Economic projection.
VcgKnapsackOutcome
VickreyBody
Body of a single-good Vickrey-cleared auction’s Economic projection.
VickreyOutcome
VickreyPayload
Wire payload of the Economic projection variant when a single-good Vickrey match has cleared. Roughly mirrors the hub’s /match response plus the bid set that produced it.

Enums§

EconomicBody
Discriminated union of the two body shapes — what verify_economic_projection_shape parses out of a Projection::Economic’s body Value.
EconomicVerifyError
ResourceDim
One axis of externality the auction internalizes. Each variant captures a measurable externality and an oracle that signs claims about it.

Constants§

ECONOMIC_BODY_VERSION
MECHANISM_VCG_KNAPSACK
MECHANISM_VICKREY
Stable wire tag for the mechanism variant.

Functions§

vcg_knapsack_projection
Pack a cleared knapsack-VCG auction into a Projection::Economic body.
verify_economic_projection_shape
Verify structural well-formedness of an Economic projection body. Returns the parsed typed body on success. Cryptographic signature verification happens on the parent Receipt.
vickrey_projection
Pack a cleared single-good Vickrey auction into a Projection::Economic body.