feat(lean): import 47 Lean 4 theorems — machine-checked auction core

.github/workflows/lean-build.yml

@@ -0,0 +1,44 @@
+name: Lean Build
+
+on:
+  push:
+    branches: [main]
+    paths:
+      - 'lean-verification/**'
+      - '.github/workflows/lean-build.yml'
+  pull_request:
+    paths:
+      - 'lean-verification/**'
+      - '.github/workflows/lean-build.yml'
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Install elan
+        run: |
+          curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      - name: Cache .lake
+        uses: actions/cache@v4
+        with:
+          path: lean-verification/.lake
+          key: lake-${{ runner.os }}-${{ hashFiles('lean-verification/lean-toolchain', 'lean-verification/lakefile.lean', 'lean-verification/lake-manifest.json') }}
+          restore-keys: lake-${{ runner.os }}-
+
+      - name: Build all theorems
+        working-directory: lean-verification
+        run: lake build
+
+      - name: Verify zero sorry/admit
+        working-directory: lean-verification
+        run: |
+          if grep -rEn '\bsorry\b|\badmit\b' --include='*.lean' NexbidVerify/; then
+            echo "::error::Found sorry or admit in proof code"
+            exit 1
+          fi
+          echo "PASS: zero sorry/admit confirmed"

lean-verification/.gitignore

@@ -0,0 +1,4 @@
+.lake/
+build/
+*.olean
+*.ilean

lean-verification/NexbidVerify.lean

@@ -0,0 +1,15 @@
+-- Nexbid Auction Engine — Formal Verification in Lean 4
+-- Full verification stack: Score, Normalization, Auction, Budget, Commerce, Wallet, EndToEnd
+
+import NexbidVerify.Types
+import NexbidVerify.RatHelpers
+import NexbidVerify.Score
+import NexbidVerify.Normalize
+import NexbidVerify.Auction
+import NexbidVerify.Budget
+import NexbidVerify.Wallet
+import NexbidVerify.Commerce.Policy
+import NexbidVerify.EndToEnd
+import NexbidVerify.Monotone
+import NexbidVerify.KanScore
+import NexbidVerify.Consistency

lean-verification/NexbidVerify/Auction.lean

@@ -0,0 +1,141 @@
+-- ─── T3-T6: Auction Logic — Formal Verification ──────────────────────
+-- Mirrors: runAuction() from packages/auction/src/engine.ts
+
+import NexbidVerify.Types
+import NexbidVerify.Score
+
+namespace Nexbid
+
+structure Participant where
+  campaignId : String
+  bidCents : Rat
+  qualityScore : UnitInterval
+  remainingBudgetCents : Rat
+  similarity : UnitInterval
+  contextRelevance : UnitInterval
+
+def isEligible (p : Participant) (floorPriceCents : Rat) : Prop :=
+  p.remainingBudgetCents ≥ p.bidCents ∧ p.bidCents ≥ floorPriceCents
+
+instance (p : Participant) (floor : Rat) : Decidable (isEligible p floor) := by
+  unfold isEligible; exact instDecidableAnd
+
+def filterEligible (ps : List Participant) (floor : Rat) : List Participant :=
+  ps.filter (fun p => decide (isEligible p floor))
+
+-- ─── T3 ──────────────────────────────────────────────────────────────
+
+/-- **Theorem T3:** Every filtered participant is eligible. -/
+theorem eligibility_correct (ps : List Participant) (floor : Rat) :
+    ∀ p ∈ filterEligible ps floor, isEligible p floor := by
+  intro p hp
+  unfold filterEligible at hp
+  simp [List.mem_filter] at hp
+  exact hp.2
+
+-- ─── Max selection ───────────────────────────────────────────────────
+
+def maxParticipant (f : Participant → Rat) : (l : List Participant) → l ≠ [] → Participant
+  | [x], _ => x
+  | x :: y :: ys, _ =>
+    let rest := maxParticipant f (y :: ys) (by simp)
+    if f x ≥ f rest then x else rest
+
+-- ─── L1: Tie-breaking uniqueness ────────────────────────────────────
+
+/-- **L1:** If two participants have equal scores, the one appearing first in the list wins.
+    maxParticipant uses ≥ in the if-branch, so when f x = f rest, the head x is returned. -/
+theorem maxParticipant_head_wins_tie (f : Participant → Rat) (x : Participant) (xs : List Participant)
+    (h : (x :: xs) ≠ []) (hx_in : xs ≠ [])
+    (h_tie : f x = f (maxParticipant f xs hx_in)) :
+    maxParticipant f (x :: xs) h = x := by
+  cases xs with
+  | nil => exact absurd rfl hx_in
+  | cons y ys =>
+    show (let rest := maxParticipant f (y :: ys) (by simp); if f x ≥ f rest then x else rest) = x
+    have h_eq : maxParticipant f (y :: ys) hx_in = maxParticipant f (y :: ys) (by simp) := by congr 1
+    rw [h_eq] at h_tie
+    have hge : f x ≥ f (maxParticipant f (y :: ys) (by simp)) := by
+      show f (maxParticipant f (y :: ys) (by simp)) ≤ f x
+      rw [← h_tie]  -- goal becomes f x ≤ f x
+      exact Rat.le_refl
+    simp [if_pos hge]
+
+-- ─── T4: maxParticipant returns the maximum ──────────────────────────
+
+/-- **Theorem T4:** maxParticipant returns element with highest f-value. -/
+theorem maxParticipant_is_max (f : Participant → Rat)
+    (l : List Participant) (h : l ≠ []) :
+    ∀ x ∈ l, f x ≤ f (maxParticipant f l h) := by
+  induction l with
+  | nil => exact absurd rfl h
+  | cons a as ih =>
+    intro x hx
+    cases as with
+    | nil =>
+      simp [maxParticipant]
+      have heq : x = a := by
+        cases List.mem_cons.mp hx with
+        | inl h => exact h
+        | inr h => exact absurd (List.not_mem_nil h) (by simp)
+      rw [heq]
+      exact Rat.le_refl
+    | cons b bs =>
+      simp only [maxParticipant]
+      split
+      · -- f a ≥ f rest
+        next hge =>
+        cases List.mem_cons.mp hx with
+        | inl heq => rw [heq]; exact Rat.le_refl
+        | inr hmem => exact Rat.le_trans (ih (by simp) x hmem) hge
+      · -- f a < f rest
+        next hlt =>
+        cases List.mem_cons.mp hx with
+        | inl heq =>
+          rw [heq]
+          simp [GE.ge, Rat.not_le] at hlt
+          exact Rat.le_of_lt hlt
+        | inr hmem => exact ih (by simp) x hmem
+
+/-- **T4b:** maxParticipant returns a member of the list. -/
+theorem maxParticipant_mem (f : Participant → Rat)
+    (l : List Participant) (h : l ≠ []) :
+    maxParticipant f l h ∈ l := by
+  induction l with
+  | nil => exact absurd rfl h
+  | cons a as ih =>
+    cases as with
+    | nil => simp [maxParticipant]
+    | cons b bs =>
+      simp only [maxParticipant]
+      split
+      · exact List.Mem.head _
+      · exact List.Mem.tail _ (ih (by simp))
+
+-- ─── T5: Winner is eligible ──────────────────────────────────────────
+
+/-- **Theorem T5:** Winner from filtered list is eligible. -/
+theorem winner_is_eligible (ps : List Participant) (floor : Rat)
+    (f : Participant → Rat) (h : filterEligible ps floor ≠ []) :
+    isEligible (maxParticipant f (filterEligible ps floor) h) floor :=
+  eligibility_correct ps floor _ (maxParticipant_mem f _ h)
+
+-- ─── T6: No winner ↔ no eligible ────────────────────────────────────
+
+/-- **T6a:** No eligible → no winner possible. -/
+theorem no_eligible_no_winner (ps : List Participant) (floor : Rat)
+    (h : filterEligible ps floor = []) :
+    ∀ p ∈ ps, ¬ isEligible p floor := by
+  intro p hp helig
+  have : p ∈ filterEligible ps floor := by
+    unfold filterEligible; simp [List.mem_filter]; exact ⟨hp, helig⟩
+  rw [h] at this; exact List.not_mem_nil this
+
+/-- **T6b:** Eligible → non-empty filtered list. -/
+theorem eligible_exists_nonempty (ps : List Participant) (floor : Rat)
+    (p : Participant) (hp : p ∈ ps) (helig : isEligible p floor) :
+    filterEligible ps floor ≠ [] := by
+  intro hempty
+  exact absurd helig (no_eligible_no_winner ps floor hempty p hp)
+
+end Nexbid

lean-verification/NexbidVerify/Budget.lean

@@ -0,0 +1,86 @@
+-- ─── T7: Atomic Budget Decrement — Formal Verification ───────────────
+-- Mirrors: atomicBudgetDecrement() from packages/auction/src/atomic-budget.ts
+
+namespace Nexbid
+
+structure BudgetState where
+  amountCents : Int
+  spentCents : Int
+  inv : spentCents ≤ amountCents
+  spent_nonneg : 0 ≤ spentCents
+
+theorem BudgetState.remaining_nonneg (b : BudgetState) :
+    0 ≤ b.amountCents - b.spentCents := by
+  have := b.inv; omega
+
+inductive DecrementResult where
+  | success (newState : BudgetState)
+  | insufficientBudget
+
+/-- Atomic budget decrement with WHERE guard. -/
+def atomicDecrement (state : BudgetState) (deductCents : Int)
+    (hdeduct : 0 ≤ deductCents) : DecrementResult :=
+  if h : state.amountCents - state.spentCents ≥ deductCents then
+    DecrementResult.success {
+      amountCents := state.amountCents
+      spentCents := state.spentCents + deductCents
+      inv := by have := state.inv; have := state.spent_nonneg; omega
+      spent_nonneg := by have := state.spent_nonneg; omega
+    }
+  else
+    DecrementResult.insufficientBudget
+
+-- ─── T7 theorems ────────────────────────────────────────────────────
+
+/-- **T7a:** Invariant preserved. -/
+theorem decrement_preserves_invariant (state : BudgetState) (deductCents : Int)
+    (hdeduct : 0 ≤ deductCents) (newState : BudgetState)
+    (_h : atomicDecrement state deductCents hdeduct = DecrementResult.success newState) :
+    newState.spentCents ≤ newState.amountCents :=
+  newState.inv
+
+/-- **T7b:** Spent increased exactly. -/
+theorem decrement_spent_exact (state : BudgetState) (deductCents : Int)
+    (hdeduct : 0 ≤ deductCents) (newState : BudgetState)
+    (h : atomicDecrement state deductCents hdeduct = DecrementResult.success newState) :
+    newState.spentCents = state.spentCents + deductCents := by
+  unfold atomicDecrement at h; split at h
+  · injection h with h; rw [← h]
+  · contradiction
+
+/-- **T7c:** Total unchanged. -/
+theorem decrement_total_unchanged (state : BudgetState) (deductCents : Int)
+    (hdeduct : 0 ≤ deductCents) (newState : BudgetState)
+    (h : atomicDecrement state deductCents hdeduct = DecrementResult.success newState) :
+    newState.amountCents = state.amountCents := by
+  unfold atomicDecrement at h; split at h
+  · injection h with h; rw [← h]
+  · contradiction
+
+/-- **T7d:** Failure means insufficient budget. -/
+theorem decrement_fail_means_insufficient (state : BudgetState) (deductCents : Int)
+    (hdeduct : 0 ≤ deductCents)
+    (h : atomicDecrement state deductCents hdeduct = DecrementResult.insufficientBudget) :
+    state.amountCents - state.spentCents < deductCents := by
+  unfold atomicDecrement at h; split at h
+  · contradiction
+  · next hn => omega
+
+/-- **T7e:** Spent monotone. -/
+theorem decrement_spent_monotone (state : BudgetState) (deductCents : Int)
+    (hdeduct : 0 ≤ deductCents) (newState : BudgetState)
+    (h : atomicDecrement state deductCents hdeduct = DecrementResult.success newState) :
+    state.spentCents ≤ newState.spentCents := by
+  have := decrement_spent_exact state deductCents hdeduct newState h; omega
+
+/-- **Theorem T7 (budget_never_overspent):** Main safety property.
+    Uses explicit unfolding to avoid match/simp issues. -/
+theorem budget_never_overspent (state : BudgetState) (deductCents : Int)
+    (hdeduct : 0 ≤ deductCents) :
+    ∀ newState : BudgetState,
+    atomicDecrement state deductCents hdeduct = DecrementResult.success newState →
+    newState.spentCents ≤ newState.amountCents := by
+  intro newState _h
+  exact newState.inv
+
+end Nexbid

lean-verification/NexbidVerify/Commerce/DSL.lean

@@ -0,0 +1,51 @@
+import NexbidVerify.Types
+
+namespace Commerce
+
+/-- A revenue split between two parties, guaranteed to sum to 1. -/
+structure RevenueShare where
+  publisherShare : Rat
+  platformShare : Rat
+  shares_nonneg : 0 ≤ publisherShare ∧ 0 ≤ platformShare
+  shares_sum_one : publisherShare + platformShare = 1
+
+/-- Default 70/30 revenue share. -/
+def defaultRevenueShare : RevenueShare := {
+  publisherShare := 7 / 10
+  platformShare := 3 / 10
+  shares_nonneg := ⟨by native_decide, by native_decide⟩
+  shares_sum_one := by native_decide
+}
+
+/-- Revenue computed from a bid and a revenue share. -/
+structure RevenueResult where
+  publisherRevenue : Rat
+  platformRevenue : Rat
+  totalRevenue : Rat
+
+/-- Compute revenue from a winning bid amount and share. -/
+def computeRevenue (bidAmountCents : Rat) (share : RevenueShare) : RevenueResult := {
+  publisherRevenue := bidAmountCents * share.publisherShare
+  platformRevenue := bidAmountCents * share.platformShare
+  totalRevenue := bidAmountCents
+}
+
+/-- A policy constraint that a bid must satisfy. -/
+structure PolicyConstraint where
+  maxBudgetCents : Rat
+  spentCents : Rat
+  floorCents : Rat
+  allowedCategories : List String
+  budget_nonneg : 0 ≤ maxBudgetCents
+  spent_nonneg : 0 ≤ spentCents
+  spent_le_budget : spentCents ≤ maxBudgetCents
+  floor_nonneg : 0 ≤ floorCents
+
+/-- Check if a bid satisfies a policy constraint. -/
+def policyCheck (bidCents : Rat) (category : String)
+    (policy : PolicyConstraint) : Bool :=
+  decide (bidCents ≤ policy.maxBudgetCents - policy.spentCents) &&
+  decide (policy.floorCents ≤ bidCents) &&
+  policy.allowedCategories.contains category
+
+end Commerce