mirror of
https://github.com/zooai/proofs.git
synced 2026-10-30 14:49:47 +00:00
zeekayandHanzo Dev
638fba4c90
Bylines, paper authorship, correspondence addresses and the founder blurb under each post named an individual. They name the organisation that published the work instead: the brand on posts and pages, the research byline on papers, and research@ in place of a personal address. Both are what these repositories already used elsewhere — nothing new was coined. Co-authors are untouched. Where a paper named someone else alongside, they stay named; only the one byline changed. Bibliography entries, running heads, PDF metadata and affiliations move with it, so a citation still resolves to whoever the cited paper names. Sample and fixture data uses the placeholder name these tests already use elsewhere, so no assertion changed meaning. Co-authored-by: Hanzo Dev <[email protected]>
182 lines
6.7 KiB
Lean4
182 lines
6.7 KiB
Lean4
/-
|
||
Authors: Antje Worring, Zoo Labs Foundation Research
|
||
|
||
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: Zoo Labs Foundation Research
|
||
-/
|
||
|
||
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
|