Lean-23b — ERC-20 natif : l’invariant de conservation évalué sous le kernel Lean

Compagnon natif du lake erc20_lean (MyIA.AI.Notebooks/SymbolicAI/SmartContracts/erc20_lean), exécuté sous le kernel lean4-wsl. Il vient à côté du compagnon Python Lean-23-ERC20-Invariant-Companion.ipynb, qui lit les mêmes sources en statique — les deux formes coexistent par design.

La différence de fond : ici, chaque déclaration du lake est évaluée par le compilateur (#check, #print axioms, example réels), pas citée en prose ni extraite par regex. Le kernel est le garant : si un nom n’existe pas, si une preuve repose sur sorryAx, ou si un calcul de transition échoue, la cellule échoue.

Le lake formalise l’invariant fondateur d’un jeton ERC-20 fongible : la somme des soldes de toutes les adresses égale l’offre totale, et cet invariant est préservé par chaque opération standard (mint, burn, transfer), puis par toute trace atteignable (induction). C’est le port formel de l’issue #4047 ; l’arc pédagogique complet (traces jouets, Monte-Carlo, pont Solidity) vit dans le compagnon Python.

1. Import des modules du lake erc20_lean

Le kernel lean4-wsl lance le REPL Lean directement avec le LEAN_PATH du lake : les modules compilés (ERC20.State, ERC20.Ops, ERC20.Invariant) sont résolus depuis .lake/build/lib. Convention du kernel (cf. Lean-21b) : les import se font seuls, en tête de la première cellule code — le REPL les traite comme l’en-tête d’un fichier source, ce qui charge réellement les oleans (le chargement de la fermeture Mathlib complète prend de l’ordre de la minute).

On importe les modules du lake plutôt que la racine ERC20 : le lakefile.lean ne liste que .submodules ERC20 et ERC20_en dans ses globs — le module racine français n’est pas un target de build (asymétrie signalée, les sous-modules couvrent les déclarations).

import ERC20.State
import ERC20.Ops
import ERC20.Invariant
import ERC20.State
import ERC20.Ops
import ERC20.Invariant
--% env 0
Raw input {"cmd": "import ERC20.State\nimport ERC20.Ops\nimport ERC20.Invariant"}
Raw output {"env": 0}

Les imports sont passés silencieusement — c’est la signature du succès : le REPL ne produit aucun message quand un bloc d’import en tête de fichier charge. La cellule suivante vérifie que le sysroot standard est intact (Nat : Type) et que le namespace du lake est peuplé : tout ce qui suit s’exécute dans le même environnement Lean que le lake, les noms qualifiés ERC20.* sont ceux des sources, sans transcription.

open ERC20

#check Nat
open ERC20
 Nat : Type
--% env 1
Raw input {"cmd": "open ERC20\n\n#check Nat", "env": 0}
Raw output {"messages": [{"severity": "info", "pos": {"line": 3, "column": 0}, "endPos": {"line": 3, "column": 6}, "data": "Nat : Type"}], "env": 1}

Lecture du protocole REPL : ce que révèle #check Nat

Cette cellule anodine est la plus informative du notebook : elle expose le contrat du kernel lean4_jupyter. Le #check Nat renvoie ──────▶ Nat : Type — la flèche épaisse est la convention d’alectryon : à gauche la commande soumise, à droite la réponse du noyau. En dessous, --% env 1 et les blocs Raw input / Raw output montrent la mécanique : chaque cellule envoie un JSON {"cmd": ..., "env": 0} et reçoit des messages plus un nouvel identifiant d’environnement ("env": 1) — les définitions d’une cellule persistent dans les suivantes via ce chaînage, exactement comme une session REPL. La réponse du noyau est classée severity: "info" avec sa position (line: 3) : le type-checking réussit sans warning. Pourquoi Nat ? Parce que c’est le type des soldes ERC-20 de ce companion (Address n := Fin n, offres et transferts en Nat) : vérifier que Nat : Type répond, c’est vérifier que l’environnement ERC20 importé à la cellule précédente est vivant — l’équivalent d’un ping avant la démonstration.

Ce protocole a une conséquence pratique pour la suite : l’ordre des cellules de ce notebook est significatif — les example évalués plus bas réutilisent l’état accumulé ici (open ERC20, chaque cellule montant un env nouveau). Redémarrer le kernel replie tout env à zéro : la cellule d’imports devra être relancée avant toute autre.

2. Le module ERC20.State — la machine à états

Trois déclarations fondent le modèle : l’adresse (Fin n, un nombre fini de détenteurs potentiels), l’état (soldes + offre totale), et l’invariant de conservation.

#check @ERC20.Address
#check @ERC20.State
#check @ERC20.supplyInvariant
 Address : ℕ → Type
 State : ℕ → Type
 @supplyInvariant : {n : ℕ} → State n → Prop
--% env 2
Raw input {"cmd": "#check @ERC20.Address\n#check @ERC20.State\n#check @ERC20.supplyInvariant", "env": 1}
Raw output {"messages": [{"severity": "info", "pos": {"line": 1, "column": 0}, "endPos": {"line": 1, "column": 6}, "data": "Address : ℕ → Type"}, {"severity": "info", "pos": {"line": 2, "column": 0}, "endPos": {"line": 2, "column": 6}, "data": "State : ℕ → Type"}, {"severity": "info", "pos": {"line": 3, "column": 0}, "endPos": {"line": 3, "column": 6}, "data": "@supplyInvariant : {n : ℕ} → State n → Prop"}], "env": 2}

Lecture des énoncés. Address n := Fin n (définition abbrev) ; State n est une structure à deux champs (balances : Address n → ℕ, totalSupply : ℕ) ; supplyInvariant s est la proposition ∑ a : Address n, s.balances a = s.totalSupply — la somme finie est bien définie parce que Fin n est un type fini.

2.1 L’invariant évalué sur un état concret

Un état à trois détenteurs (soldes 1, 2, 3 ; offre 6). Le kernel vérifie l’invariant par calcul (unfold puis decide — l’énoncé est un def, opaque à la synthèse d’instances ; une fois la somme exposée, le kernel tranche), et vérifie aussi sa négation sur un état corrompu (offre 7) : les deux sens sont exécutés, pas affirmés.

open ERC20
-- Un état à trois détenteurs : soldes 1, 2, 3 -- offre totale 6.
def s0 : State 3 := ⟨![1, 2, 3], 6⟩

-- L'invariant tient : 1 + 2 + 3 = 6, vérifié par le kernel.
-- (unfold d'abord : `supplyInvariant` est un `def` opaque pour la synthèse
-- d'instances — une fois la somme exposée, `decide` évalue par le kernel.)
example : supplyInvariant s0 := by
  unfold supplyInvariant
  decide

-- ... et échoue si l'offre ne matche pas la somme : 1 + 2 + 3 ≠ 7.
example : ¬ supplyInvariant (⟨![1, 2, 3], 7⟩ : State 3) := by
  unfold supplyInvariant
  decide
open ERC20
-- Un état à trois détenteurs : soldes 1, 2, 3 -- offre totale 6.
def s0 : State 3 := ⟨![1, 2, 3], 6⟩
-- L'invariant tient : 1 + 2 + 3 = 6, vérifié par le kernel.
-- (unfold d'abord : `supplyInvariant` est un `def` opaque pour la synthèse
-- d'instances — une fois la somme exposée, `decide` évalue par le kernel.)
example : supplyInvariant s0 := by
  unfold supplyInvariant
  decide
-- ... et échoue si l'offre ne matche pas la somme : 1 + 2 + 3 ≠ 7.
example : ¬ supplyInvariant (⟨![1, 2, 3], 7⟩ : State 3) := by
  unfold supplyInvariant
  decide
--% env 3
Raw input {"cmd": "open ERC20\n-- Un \u00e9tat \u00e0 trois d\u00e9tenteurs : soldes 1, 2, 3 -- offre totale 6.\ndef s0 : State 3 := \u27e8![1, 2, 3], 6\u27e9\n\n-- L'invariant tient : 1 + 2 + 3 = 6, v\u00e9rifi\u00e9 par le kernel.\n-- (unfold d'abord : `supplyInvariant` est un `def` opaque pour la synth\u00e8se\n-- d'instances \u2014 une fois la somme expos\u00e9e, `decide` \u00e9value par le kernel.)\nexample : supplyInvariant s0 := by\n unfold supplyInvariant\n decide\n\n-- ... et \u00e9choue si l'offre ne matche pas la somme : 1 + 2 + 3 \u2260 7.\nexample : \u00ac supplyInvariant (\u27e8![1, 2, 3], 7\u27e9 : State 3) := by\n unfold supplyInvariant\n decide", "env": 2}
Raw output {"env": 3}

Ce que montre la sortie. Le decide a réduit la somme finie ∑ a : Fin 3, ![1, 2, 3] a vers le littéral 6 puis tranché l’égalité par Nat.decEq. L’invariant n’est pas une prose : c’est un calcul que le kernel a exécuté dans les deux polarités.

3. Le module ERC20.Ops — les transitions gardées

Les trois opérations standard, vues comme des transitions de l’état : mint (frapper), burn (brûler, garde implicite de solde suffisant via la soustraction tronquée de ℕ), transfer (déplacer, offre inchangée).

#check @ERC20.mint
#check @ERC20.burn
#check @ERC20.transfer
 @mint : {n : ℕ} → State n → Address n → ℕ → State n
 @burn : {n : ℕ} → State n → Address n → ℕ → State n
 @transfer : {n : ℕ} → State n → Address n → Address n → ℕ → State n
--% env 4
Raw input {"cmd": "#check @ERC20.mint\n#check @ERC20.burn\n#check @ERC20.transfer", "env": 3}
Raw output {"messages": [{"severity": "info", "pos": {"line": 1, "column": 0}, "endPos": {"line": 1, "column": 6}, "data": "@mint : {n : ℕ} → State n → Address n → ℕ → State n"}, {"severity": "info", "pos": {"line": 2, "column": 0}, "endPos": {"line": 2, "column": 6}, "data": "@burn : {n : ℕ} → State n → Address n → ℕ → State n"}, {"severity": "info", "pos": {"line": 3, "column": 0}, "endPos": {"line": 3, "column": 6}, "data": "@transfer : {n : ℕ} → State n → Address n → Address n → ℕ → State n"}], "env": 4}

Lecture des énoncés. Chaque opération consomme un State n et produit un State n. Les gardes (solde suffisant pour burn/transfer) ne sont pas dans la signature : elles sont des hypothèses des théorèmes du module Invariant — c’est le modèle des transitions gardées.

3.1 Les transitions évaluées sur l’état concret

Le kernel exécute les trois opérations comme du code : frapper 4 tokens au détenteur 0, brûler 1 token, transférer 1 token du détenteur 2 vers le détenteur 0. Chaque ligne est une égalité calculée, pas une citation.

open ERC20

-- mint : crédit +4 au détenteur 0, offre +4.
example : (mint s0 0 4).balances 0 = 5 := by decide
example : (mint s0 0 4).totalSupply = 10 := by decide

-- burn : débit -1 au détenteur 0, offre -1.
example : (burn s0 0 1).balances 0 = 0 := by decide
example : (burn s0 0 1).totalSupply = 5 := by decide

-- transfer : -1 au détenteur 2, +1 au détenteur 0, offre inchangée.
example : (transfer s0 2 0 1).balances 0 = 2 := by decide
example : (transfer s0 2 0 1).balances 2 = 2 := by decide
example : (transfer s0 2 0 1).totalSupply = 6 := by decide
open ERC20
-- mint : crédit +4 au détenteur 0, offre +4.
example : (mint s0 0 4).balances 0 = 5 := by decide
example : (mint s0 0 4).totalSupply = 10 := by decide
-- burn : débit -1 au détenteur 0, offre -1.
example : (burn s0 0 1).balances 0 = 0 := by decide
example : (burn s0 0 1).totalSupply = 5 := by decide
-- transfer : -1 au détenteur 2, +1 au détenteur 0, offre inchangée.
example : (transfer s0 2 0 1).balances 0 = 2 := by decide
example : (transfer s0 2 0 1).balances 2 = 2 := by decide
example : (transfer s0 2 0 1).totalSupply = 6 := by decide
--% env 5
Raw input {"cmd": "open ERC20\n\n-- mint : cr\u00e9dit +4 au d\u00e9tenteur 0, offre +4.\nexample : (mint s0 0 4).balances 0 = 5 := by decide\nexample : (mint s0 0 4).totalSupply = 10 := by decide\n\n-- burn : d\u00e9bit -1 au d\u00e9tenteur 0, offre -1.\nexample : (burn s0 0 1).balances 0 = 0 := by decide\nexample : (burn s0 0 1).totalSupply = 5 := by decide\n\n-- transfer : -1 au d\u00e9tenteur 2, +1 au d\u00e9tenteur 0, offre inchang\u00e9e.\nexample : (transfer s0 2 0 1).balances 0 = 2 := by decide\nexample : (transfer s0 2 0 1).balances 2 = 2 := by decide\nexample : (transfer s0 2 0 1).totalSupply = 6 := by decide", "env": 4}
Raw output {"env": 5}

Ce que montre la sortie. Les if a = dst / if a = src des définitions ont été évalués sur Fin 3 par le kernel. La colonne d’arrivée de transfer (offre inchangée à 6) est déjà visible au niveau des calculs — le module suivant en fait un théorème.

4. Le module ERC20.Invariant — la préservation prouvée

On #check les déclarations du module, en commençant par les inductive (Op, Reachable) : un extracteur à la main qui n’attrape que theorem|lemma|def|abbrev en sous-compte — le piège mesuré sur le compagnon Python. Ici c’est le kernel qui résout les noms : la couverture ne peut pas mentir.

#check @ERC20.Op
#check @ERC20.Reachable
#check @ERC20.sum_split_mem
#check @ERC20.sum_univ_split
#check @ERC20.balance_le_totalSupply
#check @ERC20.mint_preserves_supply
#check @ERC20.burn_preserves_supply
#check @ERC20.transfer_preserves_supply
#check @ERC20.transfer_no_underflow
#check @ERC20.op_preserves_invariant
#check @ERC20.reachable_preserves_invariant
 Op : (n : ℕ) → State n → State n → Prop
 Reachable : (n : ℕ) → State n → State n → Prop
 @sum_split_mem : ∀ {n : ℕ} (f : Address n → ℕ) (s : Finset (Address n)),
  ∀ a ∈ s, ∑ x ∈ s, f x = f a + ∑ x ∈ s.erase a, f x
 @sum_univ_split : ∀ {n : ℕ} (f : Address n → ℕ) (a : Address n), ∑ x, f x = f a + ∑ x ∈ Finset.univ.erase a, f x
 @balance_le_totalSupply : ∀ {n : ℕ} (s : State n) (a : Address n), supplyInvariant s → s.balances a ≤ s.totalSupply
 @mint_preserves_supply : ∀ {n : ℕ} (s : State n) (dst : Address n) (amount : ℕ),
  supplyInvariant s → supplyInvariant (mint s dst amount)
 @burn_preserves_supply : ∀ {n : ℕ} (s : State n) (src : Address n) (amount : ℕ),
  s.balances src ≥ amount → supplyInvariant s → supplyInvariant (burn s src amount)
 @transfer_preserves_supply : ∀ {n : ℕ} (s : State n) (src dst : Address n) (amount : ℕ),
  s.balances src ≥ amount → src ≠ dst → supplyInvariant s → supplyInvariant (transfer s src dst amount)
 @transfer_no_underflow : ∀ {n : ℕ} (s : State n) (src dst : Address n) (amount : ℕ),
  s.balances src ≥ amount →
    (transfer s src dst amount).balances src = s.balances src - amount ∧
      s.balances src - amount + amount = s.balances src
 @op_preserves_invariant : ∀ {n : ℕ} (s s' : State n), Op n s s' → supplyInvariant s → supplyInvariant s'
 @reachable_preserves_invariant : ∀ {n : ℕ} (s s' : State n), supplyInvariant s → Reachable n s s' → supplyInvariant s'
--% env 6
Raw input {"cmd": "#check @ERC20.Op\n#check @ERC20.Reachable\n#check @ERC20.sum_split_mem\n#check @ERC20.sum_univ_split\n#check @ERC20.balance_le_totalSupply\n#check @ERC20.mint_preserves_supply\n#check @ERC20.burn_preserves_supply\n#check @ERC20.transfer_preserves_supply\n#check @ERC20.transfer_no_underflow\n#check @ERC20.op_preserves_invariant\n#check @ERC20.reachable_preserves_invariant", "env": 5}
Raw output {"messages": [{"severity": "info", "pos": {"line": 1, "column": 0}, "endPos": {"line": 1, "column": 6}, "data": "Op : (n : ℕ) → State n → State n → Prop"}, {"severity": "info", "pos": {"line": 2, "column": 0}, "endPos": {"line": 2, "column": 6}, "data": "Reachable : (n : ℕ) → State n → State n → Prop"}, {"severity": "info", "pos": {"line": 3, "column": 0}, "endPos": {"line": 3, "column": 6}, "data": "@sum_split_mem : ∀ {n : ℕ} (f : Address n → ℕ) (s : Finset (Address n)),\n ∀ a ∈ s, ∑ x ∈ s, f x = f a + ∑ x ∈ s.erase a, f x"}, {"severity": "info", "pos": {"line": 4, "column": 0}, "endPos": {"line": 4, "column": 6}, "data": "@sum_univ_split : ∀ {n : ℕ} (f : Address n → ℕ) (a : Address n), ∑ x, f x = f a + ∑ x ∈ Finset.univ.erase a, f x"}, {"severity": "info", "pos": {"line": 5, "column": 0}, "endPos": {"line": 5, "column": 6}, "data": "@balance_le_totalSupply : ∀ {n : ℕ} (s : State n) (a : Address n), supplyInvariant s → s.balances a ≤ s.totalSupply"}, {"severity": "info", "pos": {"line": 6, "column": 0}, "endPos": {"line": 6, "column": 6}, "data": "@mint_preserves_supply : ∀ {n : ℕ} (s : State n) (dst : Address n) (amount : ℕ),\n supplyInvariant s → supplyInvariant (mint s dst amount)"}, {"severity": "info", "pos": {"line": 7, "column": 0}, "endPos": {"line": 7, "column": 6}, "data": "@burn_preserves_supply : ∀ {n : ℕ} (s : State n) (src : Address n) (amount : ℕ),\n s.balances src ≥ amount → supplyInvariant s → supplyInvariant (burn s src amount)"}, {"severity": "info", "pos": {"line": 8, "column": 0}, "endPos": {"line": 8, "column": 6}, "data": "@transfer_preserves_supply : ∀ {n : ℕ} (s : State n) (src dst : Address n) (amount : ℕ),\n s.balances src ≥ amount → src ≠ dst → supplyInvariant s → supplyInvariant (transfer s src dst amount)"}, {"severity": "info", "pos": {"line": 9, "column": 0}, "endPos": {"line": 9, "column": 6}, "data": "@transfer_no_underflow : ∀ {n : ℕ} (s : State n) (src dst : Address n) (amount : ℕ),\n s.balances src ≥ amount →\n (transfer s src dst amount).balances src = s.balances src - amount ∧\n s.balances src - amount + amount = s.balances src"}, {"severity": "info", "pos": {"line": 10, "column": 0}, "endPos": {"line": 10, "column": 6}, "data": "@op_preserves_invariant : ∀ {n : ℕ} (s s' : State n), Op n s s' → supplyInvariant s → supplyInvariant s'"}, {"severity": "info", "pos": {"line": 11, "column": 0}, "endPos": {"line": 11, "column": 6}, "data": "@reachable_preserves_invariant : ∀ {n : ℕ} (s s' : State n), supplyInvariant s → Reachable n s s' → supplyInvariant s'"}], "env": 6}

Lecture des énoncés. Op n s s' est la relation d’opération légale (un constructeur par opération, chacun portant ses gardes : solde suffisant, adresses distinctes, invariant à l’entrée). Reachable n s s' est sa clôture réflexive-transitive — la trace. Les trois théorèmes *_preserves_supply prouvent la conservation opération par opération ; op_preserves_invariant factorise le cas-par-cas ; reachable_preserves_invariant conclut par induction sur la trace.

4.1 Propreté axiomatique — #print axioms natif

Le compagnon Python vérifie l’absence de sorry par lecture statique des blocs de preuve. Ici on demande au compilateur lui-même sur quels axiomes repose chaque théorème phare : la réponse canonique de Mathlib est [propext, Classical.choice, Quot.sound] — tout sauf sorryAx.

open ERC20
#print axioms mint_preserves_supply
#print axioms burn_preserves_supply
#print axioms transfer_preserves_supply
#print axioms transfer_no_underflow
#print axioms reachable_preserves_invariant
open ERC20
 'ERC20.mint_preserves_supply' depends on axioms: [propext, Classical.choice, Quot.sound]
 'ERC20.burn_preserves_supply' depends on axioms: [propext, Classical.choice, Quot.sound]
 'ERC20.transfer_preserves_supply' depends on axioms: [propext, Classical.choice, Quot.sound]
 'ERC20.transfer_no_underflow' depends on axioms: [propext]
 'ERC20.reachable_preserves_invariant' depends on axioms: [propext, Classical.choice, Quot.sound]
--% env 7
Raw input {"cmd": "open ERC20\n#print axioms mint_preserves_supply\n#print axioms burn_preserves_supply\n#print axioms transfer_preserves_supply\n#print axioms transfer_no_underflow\n#print axioms reachable_preserves_invariant", "env": 6}
Raw output {"messages": [{"severity": "info", "pos": {"line": 2, "column": 0}, "endPos": {"line": 2, "column": 6}, "data": "'ERC20.mint_preserves_supply' depends on axioms: [propext, Classical.choice, Quot.sound]"}, {"severity": "info", "pos": {"line": 3, "column": 0}, "endPos": {"line": 3, "column": 6}, "data": "'ERC20.burn_preserves_supply' depends on axioms: [propext, Classical.choice, Quot.sound]"}, {"severity": "info", "pos": {"line": 4, "column": 0}, "endPos": {"line": 4, "column": 6}, "data": "'ERC20.transfer_preserves_supply' depends on axioms: [propext, Classical.choice, Quot.sound]"}, {"severity": "info", "pos": {"line": 5, "column": 0}, "endPos": {"line": 5, "column": 6}, "data": "'ERC20.transfer_no_underflow' depends on axioms: [propext]"}, {"severity": "info", "pos": {"line": 6, "column": 0}, "endPos": {"line": 6, "column": 6}, "data": "'ERC20.reachable_preserves_invariant' depends on axioms: [propext, Classical.choice, Quot.sound]"}], "env": 7}

Ce que montre la sortie. Les cinq théorèmes reposent uniquement sur les axiomes standard de Mathlib (extensionnalité propositionnelle, choix classique, quotients) — aucune preuve trouée. C’est la garantie #print axioms demandée par l’acceptance, exécutée par le kernel plutôt que déduite d’une lecture.

4.2 La pyramide complète évaluée : op → trace → invariant

Le morceau de bravoure natif : depuis s0, une trace à deux pas (frappe puis transfert). Chaque pas est reconnu comme Op (gardes arithmétiques par decide, garde d’invariant par unfold + decide), la trace comme Reachable, et le théorème du lake reachable_preserves_invariant conclut que l’état final porte encore l’invariant — l’application entière est type-checkée par le kernel, gardes comprises.

open ERC20

-- Une trace à deux pas depuis s0 : frappe de 4 tokens, puis transfert de 2.
def s1 : State 3 := mint s0 0 4
def s2 : State 3 := transfer s1 0 2 2

-- Chaque pas est une opération légale : gardes arithmétiques par decide,
-- garde d'invariant par unfold+decide (le `def` est opaque aux instances).
example : Op 3 s0 s1 := .mint s0 0 4 (by unfold supplyInvariant; decide)
example : Op 3 s1 s2 := .transfer s1 0 2 2 (by decide) (by decide)
  (by unfold supplyInvariant; decide)

-- La pyramide complète : la trace est Reachable, et le théorème du lake conclut.
example : Reachable 3 s0 s2 :=
  .step s0 s1 s2 (Op.mint s0 0 4 (by unfold supplyInvariant; decide))
    (.step s1 s2 s2 (Op.transfer s1 0 2 2 (by decide) (by decide)
      (by unfold supplyInvariant; decide))
      (.refl s2))

example : supplyInvariant s2 :=
  reachable_preserves_invariant s0 s2 (by unfold supplyInvariant; decide)
    (.step s0 s1 s2 (Op.mint s0 0 4 (by unfold supplyInvariant; decide))
      (.step s1 s2 s2 (Op.transfer s1 0 2 2 (by decide) (by decide)
        (by unfold supplyInvariant; decide))
        (.refl s2)))
open ERC20
-- Une trace à deux pas depuis s0 : frappe de 4 tokens, puis transfert de 2.
def s1 : State 3 := mint s0 0 4
def s2 : State 3 := transfer s1 0 2 2
-- Chaque pas est une opération légale : gardes arithmétiques par decide,
-- garde d'invariant par unfold+decide (le `def` est opaque aux instances).
example : Op 3 s0 s1 := .mint s0 0 4 (by unfold supplyInvariant; decide)
example : Op 3 s1 s2 := .transfer s1 0 2 2 (by decide) (by decide)
  (by unfold supplyInvariant; decide)
-- La pyramide complète : la trace est Reachable, et le théorème du lake conclut.
example : Reachable 3 s0 s2 :=
  .step s0 s1 s2 (Op.mint s0 0 4 (by unfold supplyInvariant; decide))
    (.step s1 s2 s2 (Op.transfer s1 0 2 2 (by decide) (by decide)
      (by unfold supplyInvariant; decide))
      (.refl s2))
example : supplyInvariant s2 :=
  reachable_preserves_invariant s0 s2 (by unfold supplyInvariant; decide)
    (.step s0 s1 s2 (Op.mint s0 0 4 (by unfold supplyInvariant; decide))
      (.step s1 s2 s2 (Op.transfer s1 0 2 2 (by decide) (by decide)
        (by unfold supplyInvariant; decide))
        (.refl s2)))
--% env 8
Raw input {"cmd": "open ERC20\n\n-- Une trace \u00e0 deux pas depuis s0 : frappe de 4 tokens, puis transfert de 2.\ndef s1 : State 3 := mint s0 0 4\ndef s2 : State 3 := transfer s1 0 2 2\n\n-- Chaque pas est une op\u00e9ration l\u00e9gale : gardes arithm\u00e9tiques par decide,\n-- garde d'invariant par unfold+decide (le `def` est opaque aux instances).\nexample : Op 3 s0 s1 := .mint s0 0 4 (by unfold supplyInvariant; decide)\nexample : Op 3 s1 s2 := .transfer s1 0 2 2 (by decide) (by decide)\n (by unfold supplyInvariant; decide)\n\n-- La pyramide compl\u00e8te : la trace est Reachable, et le th\u00e9or\u00e8me du lake conclut.\nexample : Reachable 3 s0 s2 :=\n .step s0 s1 s2 (Op.mint s0 0 4 (by unfold supplyInvariant; decide))\n (.step s1 s2 s2 (Op.transfer s1 0 2 2 (by decide) (by decide)\n (by unfold supplyInvariant; decide))\n (.refl s2))\n\nexample : supplyInvariant s2 :=\n reachable_preserves_invariant s0 s2 (by unfold supplyInvariant; decide)\n (.step s0 s1 s2 (Op.mint s0 0 4 (by unfold supplyInvariant; decide))\n (.step s1 s2 s2 (Op.transfer s1 0 2 2 (by decide) (by decide)\n (by unfold supplyInvariant; decide))\n (.refl s2)))", "env": 7}
Raw output {"env": 8}

Ce que montre la sortie. Le kernel a accepté s2 comme état final d’une trace Reachable légale et en a déduit supplyInvariant s2 via le théorème du lake — pas par un calcul ad hoc. C’est la différence entre un compagnon qui montre le théorème et un loader qui le cite.

5. Exercices

Exercice 1 — une trace à trois pas

Depuis s0, construire la trace mint 1 2 puis burn 2 1 puis transfer 0 1 3 : définir t1, t2, t3, prouver chaque pas Op 3 _ _ par .mint/.burn/.transfer (gardes arithmétiques par decide, invariant d’entrée par unfold supplyInvariant; decide), puis conclure supplyInvariant t3 par reachable_preserves_invariant. Attention à la garde de burn : le solde du détenteur 2 après la frappe doit couvrir le montant brûlé.

-- def t1 : State 3 := mint s0 1 2
-- def t2 : State 3 := burn t1 2 1
-- def t3 : State 3 := transfer t2 0 1 3
-- example : supplyInvariant t3 := reachable_preserves_invariant s0 t3 (by decide) <trace>

Exercice 2 — casser l’invariant, prouver la casse

Un état où supplyInvariant est faux (par exemple soldes ![4, 4, 4], offre 11). Le prouver par ¬ supplyInvariant _ := by decide, puis vérifier qu’aucune opération légale ne peut être lancée depuis cet état sans hypothèse d’invariant d’entrée — relire les constructeurs de Op : chacun exige supplyInvariant s. C’est exactement le rôle des gardes : un état corrompu est hors du modèle atteignable.

-- example : ¬ supplyInvariant (⟨![4, 4, 4], 11⟩ : State 3) := by decide

Conclusion

Compagnon Python (Lean-23) Ce compagnon natif (Lean-23b)
Accès aux déclarations lecture statique des .lean (regex) #check résolu par le kernel
Propreté axiomatique absence de sorry par lecture de bloc #print axioms exécuté
L’invariant traces jouets en Python example ... := by decide sous Lean
La trace simulation Python Op/Reachable/théorème type-checkés

Les déclarations du lake sont couvertes : chaque nom cité ci-dessus a été résolu par le kernel dans les cellules code 4–18. Les deux compagnons coexistent — la préférence de forme est « idéalement on veut les deux » (#11703) : le Python pour l’arc pédagogique et le Monte-Carlo, le natif pour la garantie du compilateur.

Références

  • Lake : SymbolicAI/SmartContracts/erc20_lean — State.lean, Ops.lean, Invariant.lean (Mathlib v4.33.0)
  • Issue #4047 (roadmap #4038) : l’invariant de conservation ERC-20 formalisé
  • Compagnon Python : Lean-23-ERC20-Invariant-Companion.ipynb (#11710)
  • Préférence de forme « notebook sous kernel Lean à côté du Python » : #11703 ; grain de suivi : #11721
  • Le standard ERC-20 (EIP-20) : transfer/transferFrom/approve/allowance
Retour au sommet