proofs/lean/DeFi/CarbonCredits.lean

/-
  Authors: Antje Worring, Zach Kelling

  Carbon Credit Conservation — Token Integrity

  Formal proofs about carbon credit tokens used in conservation finance.
  Credits are issued for verified carbon sequestration, traded freely,
  and retired (burned) when used to offset emissions. Key invariants
  prevent double-counting and ensure retirement is irreversible.

  Maps to:
  - Zoo Labs Foundation's conservation tokenomics
  - zoo/papers/zoo-experience-ledger.tex: verification infrastructure

  Key results:
  - No double counting: each credit has a unique ID and is counted once
  - Retirement is irreversible: retired credits cannot be re-activated
  - Issuance is bounded by verified sequestration

  Author: Zach Kelling
-/

import Mathlib.Data.Nat.Defs
import Mathlib.Data.Finset.Basic
import Mathlib.Tactic

namespace DeFi.CarbonCredits

/-! ## Core Structures -/

/-- A carbon credit token. -/
structure CarbonCredit where
  /-- Unique credit identifier -/
  creditId : Nat
  /-- Amount of CO2 sequestered (kg) -/
  sequestrationKg : Nat
  /-- Verification attestation hash -/
  attestationHash : Nat
  /-- Current owner -/
  owner : Nat
  /-- Whether the credit has been retired (used for offset) -/
  retired : Bool
  deriving DecidableEq, Repr

/-- The carbon credit registry state. -/
structure Registry where
  /-- All issued credits -/
  credits : List CarbonCredit
  /-- Set of credit IDs that have been issued -/
  issuedIds : Finset Nat
  /-- Total verified sequestration available for issuance (kg) -/
  verifiedSequestration : Nat
  /-- Total credits issued (sum of sequestrationKg across all credits) -/
  totalIssued : Nat

/-- A sequestration verification attestation. -/
structure SequestrationAttestation where
  /-- Amount of CO2 verified as sequestered (kg) -/
  amountKg : Nat
  /-- Verifier's TEE signature -/
  teeSignature : Nat
  /-- The project/site that performed sequestration -/
  projectId : Nat
  hValid : teeSignature ≠ 0

/-! ## Theorem 1: No Double Counting -/

/-- Each credit has a unique ID in the registry. -/
def noDuplicateIds (reg : Registry) : Prop :=
  ∀ i j : Fin reg.credits.length,
    reg.credits[i].creditId = reg.credits[j].creditId → i = j

/-- Issue a new credit. Returns none if the ID already exists
    or if issuance would exceed verified sequestration. -/
def issueCredit (reg : Registry) (credit : CarbonCredit)
    (att : SequestrationAttestation)
    (h_amount : credit.sequestrationKg ≤ att.amountKg) : Option Registry :=
  if credit.creditId ∈ reg.issuedIds then none  -- duplicate ID
  else if reg.totalIssued + credit.sequestrationKg > reg.verifiedSequestration then none
  else some {
    credits := credit :: reg.credits
    issuedIds := reg.issuedIds ∪ {credit.creditId}
    verifiedSequestration := reg.verifiedSequestration
    totalIssued := reg.totalIssued + credit.sequestrationKg }

/-- No double counting: attempting to issue a credit with an existing ID fails. -/
theorem no_double_count (reg : Registry) (credit : CarbonCredit)
    (att : SequestrationAttestation)
    (h_amount : credit.sequestrationKg ≤ att.amountKg)
    (h_exists : credit.creditId ∈ reg.issuedIds) :
    issueCredit reg credit att h_amount = none := by
  simp [issueCredit, h_exists]

/-- After successful issuance, the new ID is recorded. -/
theorem issue_records_id (reg : Registry) (credit : CarbonCredit)
    (att : SequestrationAttestation) (h_amount : credit.sequestrationKg ≤ att.amountKg)
    (reg' : Registry)
    (h_ok : issueCredit reg credit att h_amount = some reg') :
    credit.creditId ∈ reg'.issuedIds := by
  unfold issueCredit at h_ok
  split at h_ok
  · exact absurd h_ok (by simp)
  · split at h_ok
    · exact absurd h_ok (by simp)
    · -- some-branch: reg'.issuedIds = reg.issuedIds ∪ {credit.creditId}
      injection h_ok with h_eq
      subst h_eq
      simp [Finset.mem_union]

/-! ## Theorem 2: Retirement Irreversible -/

/-- Retire a credit: mark it as retired (burned for offset). -/
def retireCredit (credit : CarbonCredit) : CarbonCredit :=
  { credit with retired := true }

/-- Retirement is irreversible: once a credit is retired, the retired flag
    is true and there is no operation to set it back to false.
    (The retireCredit function is the only state transition, and it only
    sets retired := true.) -/
theorem retirement_irreversible (credit : CarbonCredit) :
    (retireCredit credit).retired = true := by
  simp [retireCredit]

/-- Retiring preserves the credit identity. -/
theorem retire_preserves_id (credit : CarbonCredit) :
    (retireCredit credit).creditId = credit.creditId := by
  simp [retireCredit]

/-- Retiring preserves the sequestration amount. -/
theorem retire_preserves_amount (credit : CarbonCredit) :
    (retireCredit credit).sequestrationKg = credit.sequestrationKg := by
  simp [retireCredit]

/-- An already-retired credit is unchanged by another retirement. -/
theorem double_retire_idempotent (credit : CarbonCredit) :
    retireCredit (retireCredit credit) = retireCredit credit := by
  simp [retireCredit]

/-! ## Theorem 3: Issuance Bounded -/

/-- Total issued credits never exceed verified sequestration.
    This is enforced by the issueCredit function which checks
    totalIssued + newAmount <= verifiedSequestration. -/
theorem issuance_bounded (reg : Registry) (credit : CarbonCredit)
    (att : SequestrationAttestation) (h_amount : credit.sequestrationKg ≤ att.amountKg)
    (reg' : Registry)
    (h_ok : issueCredit reg credit att h_amount = some reg')
    (h_inv : reg.totalIssued ≤ reg.verifiedSequestration) :
    reg'.totalIssued ≤ reg'.verifiedSequestration := by
  unfold issueCredit at h_ok
  split at h_ok
  · exact absurd h_ok (by simp)
  · split at h_ok
    · exact absurd h_ok (by simp)
    · -- the second guard is false: ¬(totalIssued + amount > verifiedSequestration)
      rename_i h_guard
      injection h_ok with h_eq
      subst h_eq
      -- goal: reg.totalIssued + credit.sequestrationKg ≤ reg.verifiedSequestration
      simp only [gt_iff_lt, not_lt] at h_guard
      exact h_guard

/-- Issuance increases total by exactly the credit's sequestration amount. -/
theorem issuance_amount_exact (reg : Registry) (credit : CarbonCredit)
    (att : SequestrationAttestation) (h_amount : credit.sequestrationKg ≤ att.amountKg)
    (reg' : Registry)
    (h_ok : issueCredit reg credit att h_amount = some reg') :
    reg'.totalIssued = reg.totalIssued + credit.sequestrationKg := by
  unfold issueCredit at h_ok
  split at h_ok
  · exact absurd h_ok (by simp)
  · split at h_ok
    · exact absurd h_ok (by simp)
    · injection h_ok with h_eq
      subst h_eq
      rfl

/-- An empty registry has zero issuance. -/
theorem empty_zero_issued : (⟨[], ∅, 0, 0⟩ : Registry).totalIssued = 0 := rfl

end DeFi.CarbonCredits