SC-7b : ERC-20 + Lean — vérification formelle de l’invariant Σ balances = totalSupply

Navigation : << Précédent : SC-7 (ERC-20 Token Standards) | Retour au sommaire SmartContracts | Suivant : SC-8 (DeFi Primitives) >>

Pourquoi ce notebook

Le notebook précédent [SC-07-Token-Standards-Python.ipynb](./SC-07-Token-Standards-Python.ipynb) déployait un jeton ERC-20 complet sur anvil et démontrait son cycle transfer / approve / transferFrom. Chaque test Foundry y vérifiait que les soldes réagissent aux opérations comme attendu — sur un scénario. La question qui restait : ce contrat peut-il un jour violer l’invariant Σ balances = totalSupply, sur un scénario qu’on n’a pas testé ?

Le notebook ../../Lean/Lean-23-ERC20-Invariant-Companion.ipynb, lui, ne se contente pas d’observer : il prouve qu’aucune séquence arbitraire d’opérations mint/burn/transfer (sur l’espace d’états fini d’ERC20.State) ne peut violer cet invariant. C’est une propriété vérifiée mécaniquement par Lean 4 + Mathlib dans le lac erc20_lean.

Ce notebook-ci est le pont narratif entre les deux : il prend le contrat Solidity déployé par SC-7, observe l’invariant sur des traces réelles, puis confronte ces observations à la garantie formelle du lac Lean. Aucune connaissance du vérifieur n’est requise pour suivre ; la profondeur technique est volontairement modeste.

Prérequis

  • Le notebook SC-07-Token-Standards-Python.ipynb (contrat déployé sur anvil).
  • Notions de ERC-20 (cf. SC-7, section 1).
  • Aucune connaissance préalable de Lean 4 (les références au lac servent d’illustration, pas d’outil).

Durée estimée : 25 minutes

1. L’invariant, vu côté Solidity

Côté Solidity (SC-7), on encode les soldes par un mapping(address => uint256) et l’offre totale par un uint256 _totalSupply. L’invariant attendu :

assert(totalSupply() == sum(balanceOf(a) for a in holders));

n’est pas encodé dans le contrat : SimpleERC20 n’a pas de fonction invariant_ok() qui le vérifie à chaque transition. C’est le test Foundry qui observe les comptes après chaque opération et constate que Σ balances = totalSupply (cf. les print de SC-7).

Autrement dit : côté Solidity, l’invariant est observé empiriquement, sur un nombre fini de cas. Il est vrai sur tous les cas qu’on a essayés, mais on n’a pas exclu qu’un cas futur le brise. C’est le défaut classique du testing par rapport aux méthodes formelles.

# Code 1.1 - Vérification empirique de l'invariant sur un mini-état ERC-20
#
# On rejoue ici la meme trace que dans Lean-24 (mint 100 / mint 50 / transfer
# 30 / burn 20), mais en Python -- sans deploiement. C'est l'ombre Pure Python
# du contrat Solidity, et le pivot est le meme : `Σ balances = totalSupply` a
# chaque etape. La difference : ici on sait qu'on l'a verifie, la-bas on sait
# qu'on ne peut PAS le violer.

def initial_state(n_holders=5, supply=0):
    return {
        "balances": {i: 0 for i in range(n_holders)},
        "totalSupply": supply,
    }


def assert_invariant(s, tag=""):
    s_sum = sum(s["balances"].values())
    ok = s_sum == s["totalSupply"]
    print(f"  [{tag}] Σ balances = {s_sum}, totalSupply = {s['totalSupply']}, invariant = {ok}")
    return ok


def mint(s, dst, amount):
    s_new = {"balances": dict(s["balances"]), "totalSupply": s["totalSupply"]}
    s_new["balances"][dst] += amount
    s_new["totalSupply"] += amount
    return s_new


def burn(s, src, amount):
    assert s["balances"][src] >= amount, "solde src insuffisant (garde burn)"
    s_new = {"balances": dict(s["balances"]), "totalSupply": s["totalSupply"]}
    s_new["balances"][src] -= amount
    s_new["totalSupply"] -= amount
    return s_new


def transfer(s, src, dst, amount):
    assert s["balances"][src] >= amount, "solde src insuffisant (garde transfer)"
    assert src != dst, "src != dst (garde transfer)"
    s_new = {"balances": dict(s["balances"]), "totalSupply": s["totalSupply"]}
    s_new["balances"][src] -= amount
    s_new["balances"][dst] += amount
    # totalSupply INCHANGE
    return s_new


# Trace jouet alignee sur Lean-24 code 1.1
s = initial_state(n_holders=5)
print("Trace jouet (5 ops) :")
assert_invariant(s, "t0 init")
s = mint(s, 0, 100); assert_invariant(s, "t1 mint Alice 100")
s = mint(s, 1, 50); assert_invariant(s, "t2 mint Bob 50")
s = transfer(s, 0, 1, 30); assert_invariant(s, "t3 Alice -> Bob 30, supply INCHANGE")
s = burn(s, 0, 20); assert_invariant(s, "t4 burn Alice 20")
Trace jouet (5 ops) :
  [t0 init] Σ balances = 0, totalSupply = 0, invariant = True
  [t1 mint Alice 100] Σ balances = 100, totalSupply = 100, invariant = True
  [t2 mint Bob 50] Σ balances = 150, totalSupply = 150, invariant = True
  [t3 Alice -> Bob 30, supply INCHANGE] Σ balances = 150, totalSupply = 150, invariant = True
  [t4 burn Alice 20] Σ balances = 130, totalSupply = 130, invariant = True
True

Lecture de la sortie. L’invariant tient à chaque étape, et le transfer (t3) est le pivot : totalSupply reste à 150 alors que les soldes d’Alice et de Bob ont bougé de 30 unités. C’est ce double comptage (ce que chaque adresse possède vs ce que le contrat dit détenir au total) qui sert de signature à un jeton ERC-20 et qu’on voit dans SC-7 comme une simple mapping mise à jour à chaque transition.

Côté Solidity (cf. SC-7 cellule 3) : - transfer : _balances[from] -= amount ; _balances[to] += amount ; (offre non touchée). - mint : _balances[to] += amount ; _totalSupply += amount ; (offre et soldes en parallèle). - burn (pattern OpenZeppelin) : _balances[from] -= amount ; _totalSupply -= amount ; (idem, symétrique).

Ces trois règles métier (offre inchangée pour transfer / symétrique pour mint et burn) sont identiques aux définitions Lean du lac erc20_lean – mais Solidity les exécute sans vérification automatique de leur effet cumulé.

2. L’invariant, vu côté Lean

Le lac erc20_lean (dans MyIA.AI.Notebooks/SymbolicAI/SmartContracts/erc20_lean/) encode le même invariant Σ balances = totalSupply comme un prédicat sur un type State n :

def supplyInvariant (s : State n) : Prop :=
  ∑ a : Address n, s.balances a = s.totalSupply

Et il prouve – via 5 théorèmes dans Invariant.lean – que les trois transitions (mint, burn, transfer) préservent ce prédicat, et par induction que toute trace Reachable le préserve aussi. C’est la garantie « sur tous les cas » : pour chaque combinaison possible de (s : State n, op : Op n, ...) atteignable depuis un état initial valide, l’invariant tient à l’état résultant.

Source de vérité Vérification Portée
Spec ERC-20 EIP-20 (Vogelsteller / Buterin, 2015) Standard Ethereum
Comportement runtime (SC-7) Tests Foundry / web3py Sur les cas déroulés
Garantie formelle (lac erc20_lean) Lean 4 + Mathlib Sur tous les cas possibles 
# Code 2.1 - Comparaison directe des signatures Solidity et Lean sur les 3 ops
#
# On aligne les noms ERC-20 (`from`/`to`, mots-cles Solidity) avec les noms
# du lac (`src`/`dst`, pour eviter les mots-cles reserves Lean 4) et on montre
# que la STRUCTURE des transitions est la meme -- la verification formelle
# porte donc exactement sur ce que SC-7 deploye.

print("=" * 72)
print("TRANSFER  (offre totale INCHANGE)")
print("=" * 72)
print("Solidity (SC-7 SimpleERC20) :")
print("  require(_balances[from] >= amount, 'ERC20: insufficient balance');")
print("  _balances[from] -= amount;")
print("  _balances[to]   += amount;       # +amount a to, -amount a from, supply !=")
print()
print("Lean (erc20_lean/ERC20/Ops.lean) :")
print("  def transfer (s src dst amount) : State n :=")
print("    { balances := fun a =>")
print("        if a = src then s.balances a - amount")
print("        else if a = dst then s.balances a + amount")
print("        else s.balances a,")
print("      totalSupply := s.totalSupply }    # <- INCHANGE, pivot de l'invariant")
print()

print("=" * 72)
print("MINT  (offre et soldes en parallele)")
print("=" * 72)
print("Solidity (SC-7 SimpleERC20) :")
print("  _totalSupply += amount;")
print("  _balances[to] += amount;")
print()
print("Lean (erc20_lean/ERC20/Ops.lean) :")
print("  def mint (s dst amount) : State n :=")
print("    { balances := fun a => if a = dst then s.balances a + amount else s.balances a,")
print("      totalSupply := s.totalSupply + amount }    # <- +amount ici ET la")
print()

print("=" * 72)
print("BURN  (offre et soldes en parallele, garde solde >= amount)")
print("=" * 72)
print("Solidity (SC-7 SimpleERC20) :")
print("  require(_balances[from] >= amount, 'ERC20: insufficient balance');")
print("  _totalSupply -= amount;")
print("  _balances[from] -= amount;")
print()
print("Lean (erc20_lean/ERC20/Ops.lean) :")
print("  def burn (s src amount) : State n :=")
print("    { balances := fun a => if a = src then s.balances a - amount else s.balances a,")
print("      totalSupply := s.totalSupply - amount }    # <- -amount ici ET la")
========================================================================
TRANSFER  (offre totale INCHANGE)
========================================================================
Solidity (SC-7 SimpleERC20) :
  require(_balances[from] >= amount, 'ERC20: insufficient balance');
  _balances[from] -= amount;
  _balances[to]   += amount;       # +amount a to, -amount a from, supply !=

Lean (erc20_lean/ERC20/Ops.lean) :
  def transfer (s src dst amount) : State n :=
    { balances := fun a =>
        if a = src then s.balances a - amount
        else if a = dst then s.balances a + amount
        else s.balances a,
      totalSupply := s.totalSupply }    # <- INCHANGE, pivot de l'invariant

========================================================================
MINT  (offre et soldes en parallele)
========================================================================
Solidity (SC-7 SimpleERC20) :
  _totalSupply += amount;
  _balances[to] += amount;

Lean (erc20_lean/ERC20/Ops.lean) :
  def mint (s dst amount) : State n :=
    { balances := fun a => if a = dst then s.balances a + amount else s.balances a,
      totalSupply := s.totalSupply + amount }    # <- +amount ici ET la

========================================================================
BURN  (offre et soldes en parallele, garde solde >= amount)
========================================================================
Solidity (SC-7 SimpleERC20) :
  require(_balances[from] >= amount, 'ERC20: insufficient balance');
  _totalSupply -= amount;
  _balances[from] -= amount;

Lean (erc20_lean/ERC20/Ops.lean) :
  def burn (s src amount) : State n :=
    { balances := fun a => if a = src then s.balances a - amount else s.balances a,
      totalSupply := s.totalSupply - amount }    # <- -amount ici ET la

Lecture des codes. Les trois transitions ont la même structure dans les deux langages : - transfer : from -= amount ET to += amount, offre inchangée. - mint : to += amount ET totalSupply += amount (parallèle). - burn : from -= amount ET totalSupply -= amount (parallèle, garde from >= amount).

C’est précisément cette simétrie entre soldes et offre qui fait marcher l’invariant. Le lac Lean ne se contente pas de croire cette symétrie : il la vérifie par des preuves non-triviales (l’extraction additive sum_univ_split joue un rôle clé pour transfer_preserves_supply, détaillé dans Lean-23 section 2.1).

Différence de garde-fou : - Solidity : la garde require(balance >= amount, "...") revert sur sous-flow. Sans le test Foundry, un cas extrême pourrait passer inaperçu. - Lean : la garde s.balances src ≥ amount est une hypothèse du théorème transfer_preserves_supply, et le théorème transfer_no_underflow la démontre comme une conséquence : pas besoin de la tester, elle sort de la preuve.

Autrement dit, Lean transforme « est-ce que mon test couvre tous les cas » en « est-ce que la preuve couvre tous les cas » – la question est devenue mécanique, plus affaire de pari sur la qualité du test.

3. Et la garantie formelle, concrètement ?

L’idée du lac erc20_lean est de remplacer « on observe l’invariant sur 10 000 cas Foundry » par « on prouve l’invariant pour les 2^N × M^L cas possibles, par induction sur la trace ». Voici la chaîne complète :

  1. Modèle – Address n := Fin n (un nombre fini d’adresses), State n (soldes + offre totale), supplyInvariant (le prédicat Σ balances = totalSupply).
  2. Transitions – mint, burn, transfer (les mêmes 3 opérations que SC-7, encodées en Lean).
  3. Préservation immédiate – 3 théorèmes dans Invariant.lean :
    • mint_preserves_supply : si s porte l’invariant, alors mint s dst amount aussi.
    • burn_preserves_supply : même chose avec garde balance ≥ amount.
    • transfer_preserves_supply : même chose avec gardes balance ≥ amount ET src ≠ dst.
  4. Induction sur la trace – le type Reachable (état atteignable par clôture réflexive-transitive de Op), et le théorème reachable_preserves_invariant : pour toute trace, l’invariant tient à l’état final.

Le dernier maillon – l’induction – est ce qui transforme le testing par cas en garantie universelle : peu importe le nombre d’opérations, peu importe l’ordre choisi, l’invariant survivra.

Note technique (pas requise pour la compréhension du notebook) : la preuve de transfer_preserves_supply repose sur l’extraction additive d’un point d’une somme finie (sum_univ_split dans Invariant.lean), parce que la soustraction ∑ f - ∑ g est fausse sur ℕ en général – l’extraction évite cette piège en sortant l’adresse src (puis dst) de la somme avant l’arithmétique ℕ. C’est une preuve pour chaque théorème, mais pour des valeurs critiques de cette complexité, c’est ce qui distingue « la preuve marche sur le papier » de « la preuve est solide en présence de cas-limites d’arithmétique ℕ ».

# Code 3.1 - Monte-Carlo : "empirique" vs "formel" sur le MEME scenario
#
# On rejoue 5 000 transitions aleatoires sur le mini-contrat Python, on
# observe l'invariant a chaque etape, et on rapporte le nombre de violations.
# C'est la version "empirique" de la garantie formelle : on cherche une seule
# violation sur 5 000 cas. La garantie du lac dit : "0 violation sur TOUS les
# cas (infini denombrable)". Si on n'en trouve pas en 5 000, ce n'est pas une
# preuve ; c'est juste un faisceau d'indices confortant la these.

import random


def mc_traces(n_trials=200, ops_per_trial=50, seed=42):
    rng = random.Random(seed)
    violations = 0
    worst_solde = 0
    worst_ecart = 0
    for _ in range(n_trials):
        s = initial_state(n_holders=5)
        for _ in range(ops_per_trial):
            op = rng.choices(["mint", "burn", "transfer", "transfer"], # transferrees plus frequentes
                              weights=[1, 1, 4, 4])[0]
            try:
                if op == "mint":
                    dst = rng.randrange(5)
                    amt = rng.randrange(1, 50)
                    s = mint(s, dst, amt)
                elif op == "burn":
                    non_zero = [a for a, v in s["balances"].items() if v > 0]
                    if not non_zero:
                        continue
                    src = rng.choice(non_zero)
                    amt = rng.randrange(1, s["balances"][src] + 1)
                    s = burn(s, src, amt)
                else:  # transfer
                    non_zero = [a for a, v in s["balances"].items() if v > 0]
                    if not non_zero:
                        continue
                    src = rng.choice(non_zero)
                    dst = rng.randrange(5)
                    if dst == src:
                        continue
                    amt = rng.randrange(1, s["balances"][src] + 1)
                    s = transfer(s, src, dst, amt)
            except AssertionError:
                # Revert silencieux (garde non satisfaite) -- pas une violation d'invariant
                continue
            total = sum(s["balances"].values())
            ecart = abs(total - s["totalSupply"])
            if ecart > worst_ecart:
                worst_ecart = ecart
            if ecart > 0:
                violations += 1
            for v in s["balances"].values():
                if v < worst_solde:
                    worst_solde = v
    return {
        "n_trials": n_trials,
        "ops_per_trial": ops_per_trial,
        "total_ops": n_trials * ops_per_trial,
        "violations_invariant": violations,
        "pire_solde": worst_solde,
        "pire_ecart_totalSupply": worst_ecart,
    }


result = mc_traces(n_trials=200, ops_per_trial=50)
print("Monte-Carlo : 200 traces x 50 ops, seed=42")
print()
for k, v in result.items():
    print(f"  {k} = {v}")
print()
if result["violations_invariant"] == 0 and result["pire_solde"] >= 0 and result["pire_ecart_totalSupply"] == 0:
    print("Aucune violation observee sur 10 000 transitions.")
    print("C'est CONFORTANT, mais PAS une preuve : un cas non couvert par le RNG")
    print("peut exister (e.g. une trace dedoublee sur 2^1000 transitions).")
    print("La GARANTIE formelle du lac erc20_lean, elle, est mecanique et exhaustive.")
else:
    print("ATTENTION : un cas pathologique a ete observe -- voir `pire_solde` ci-dessus.")
Monte-Carlo : 200 traces x 50 ops, seed=42

  n_trials = 200
  ops_per_trial = 50
  total_ops = 10000
  violations_invariant = 0
  pire_solde = 0
  pire_ecart_totalSupply = 0

Aucune violation observee sur 10 000 transitions.
C'est CONFORTANT, mais PAS une preuve : un cas non couvert par le RNG
peut exister (e.g. une trace dedoublee sur 2^1000 transitions).
La GARANTIE formelle du lac erc20_lean, elle, est mecanique et exhaustive.

Lecture de la simulation. Sur 10 000 transitions (200 traces × 50 ops), aucune violation de l’invariant n’a été observée – ce qui est cohérent avec la garantie formelle du lac. Mais c’est aussi attendu : la structure des transitions (les 3 règles métier alignées) réalise l’invariant par construction ; pour qu’il y ait violation, il faudrait qu’un mint/burn/transfer rompe la symétrie. Aucune ne le peut.

C’est précisément le point que la preuve Lean formalise : non pas que nous croyons la symétrie correcte, mais que le compilateur l’a vérifiée pour nous, sur les 2^N cas que n = Fin n permet.

Différence pratique entre Monte-Carlo et preuve Lean : - Monte-Carlo = « j’ai observé 10 000 cas cohérents » → crédence subjective, jamais une preuve. - Lean = « le compilateur a vérifié tous les cas pour n = Fin n » → garantie mécanique, reproductible, auditable.

Pour ERC-20 spécifiquement, le gap entre « testing » et « preuve formelle » n’est pas critique (les bugs ERC-20 viennent plutôt de la sémantique d’exécution : réentrance, gas, etc., pas de l’invariant de conservation). Mais pour des invariants plus subtils (e.g. « pas d’approve redondant », « pas de mint après renounceOwnership »), l’écart devient décisif. Le pattern formel du lac s’applique indépendamment de la complexité du prédicat.

4. Résumé

Ce notebook a confronté deux points de vue sur le même invariant ERC-20 Σ balances = totalSupply :

Registre Outil Réponse Limite
Observé Tests Foundry (SC-7) + simulation Monte-Carlo (code 3.1) Tient sur 10 000 transitions Pas une preuve (cas futurs possibles)
Prouvé Lean 4 + Mathlib (MyIA.AI.Notebooks/SymbolicAI/SmartContracts/erc20_lean/) Tient sur toutes les transitions possibles, par induction sur la trace Reachable Exige un encodage formel du contrat

Les deux se complètent : - Solidity (SC-7) montre le comportement sur anvil : c’est ce que l’utilisateur voit et ce qui s’exécute réellement. - Lean (lac erc20_lean) montre la garantie sur la spécification : c’est ce que la propriété restera vraie quel que soit le futur.

Pour ERC-20 spécifiquement, l’invariant de conservation est simple (3 règles symétriques), ce qui rend la preuve essentiellement triviale. Mais le pattern – modéliser en Lean, prouver par induction, confronter au runtime Solidity – s’applique à des invariants arbitrairement subtils sur des contrats arbitrairement complexes. Le présent notebook en est le cas d’école.

5. Pour aller plus loin

  • Le lac erc20_lean : MyIA.AI.Notebooks/SymbolicAI/SmartContracts/erc20_lean/. Voir README.md (modèle et théorèmes), ERC20/Invariant.lean (les 5 théorèmes de préservation + l’induction).
  • Le notebook noyau : Lean-23-ERC20-Invariant-Companion.ipynb – qui interroge directement le lac via #check et #print axioms.
  • Le contrat Solidity : MyIA.AI.Notebooks/SymbolicAI/SmartContracts/erc20_lean/ – le pendant déployable (et déployé par SC-7).
  • Le notebook SC-7 : [SC-07-Token-Standards-Python.ipynb](./SC-07-Token-Standards-Python.ipynb) – la base runtime, sans laquelle la garantie formelle n’aurait pas de scène.

Exercices

Les exercices portent sur la confrontation runtime ↔︎ formel : les trois registres couvrent les structures Solidity (équivalence Python), la garantie Lean (ce qui reste vrai même quand Solidity ne le garantit pas), et la rédaction de tests Foundry ciblés sur les invariants (le pont pratique entre les deux).

Exercice 1 : contre-exemple Solidity qui LEAN exclut par construction

Construisez un contrat BrokenERC20 qui brise l’invariant Σ balances = totalSupply au moins une fois (par exemple, un transfer qui oublie de mettre à jour totalSupply, ou un mint qui crédite le destinataire sans ajuster l’offre). Expliquez ensuite pourquoi la garantie formelle du lac erc20_lean exclut par construction cette classe de bug (la définition Lean de transfer modifie balances mais laisse totalSupply := s.totalSupply – aucune chance d’oublier).

Indice 1 (Solidity) : héritez de IERC20 (cf. SC-7 cellule 2) et remplacez transfer par une version buggy : _balances[from] -= amount; _balances[to] += amount; mais _totalSupply -= 1; (ou += 1). L’invariant sera violé après un seul transfer.

Indice 2 (Lean) : regardez ERC20/Ops.lean ligne 38-43 (transfer) : totalSupply n’apparaît qu’une seule fois dans la définition, à droite du :=, et c’est s.totalSupply – la valeur avant. La garantie est « si l’invariant tient avant, il tient après » par construction syntaxique de la définition.

Exercice 2 : mesure du pire cas Monte-Carlo

Étendez le code 3.1 à n_trials=1000, ops_per_trial=200 (200 000 transitions au total). Vérifiez qu’aucune violation n’apparaît. Si une apparaît, c’est un bug de votre implémentation Python (pas du contrat Solidity), à investiguer :rivez une version corrigée.

Indice 1 (statistique) : sur 200 000 transitions, la borne supérieure de Hoeffding pour P(violation|transition) à 95 % de confiance avec 0 violation observée est P ≤ 3/200000 ≈ 1.5e-5. C’est très confortable, mais pas zéro.

Indice 2 (sanité) : result["pire_solde"] >= 0 (soldes jamais négatifs) et result["pire_ecart_totalSupply"] == 0 (offre toujours alignée aux soldes). Si pire_solde < 0, votre garde require(balance >= amount) côté Python a une fuite.

# Exercice 1 : contrat Solidity qui brise l'invariant Σ = totalSupply
# TODO etudiant : hereditez de IERC20, implementez un transfer buggy qui
# modifie totalSupply par erreur, deployez-le, montrez la violation en
# comparant balanceOf(deployer) + balanceOf(receiver) vs totalSupply().
#
# Indice : deployer un "BrokenERC20" sur anvil, transfer 100 tokens,
#          puis print(f"Σ balances = {deployer + receiver}, totalSupply = {broken.totalSupply()}")
#
# Indice 2 : en miroir, montrez pourquoi erc20_lean exclut cette classe
#            de bug par construction (transfer definit totalSupply := s.totalSupply,
#            AUCUNE mutation possible sur le supply).
#
# Etape 1 : ecrire le contrat dans une string (cf. SC-7 cellule 2 pour le pattern).
# Etape 2 : compile + deploy via forge_compile_and_deploy (cf. SC-7 cellule 10).
# Etape 3 : transfer, puis afficher Σ vs totalSupply pour montrer la violation.

print("Exercice a completer : contrat BrokenERC20 vs garantie formelle de erc20_lean")
Exercice a completer : contrat BrokenERC20 vs garantie formelle de erc20_lean
# Exercice 2 : Monte-Carlo 1000 traces x 200 ops (200 000 transitions)
# TODO etudiant : etendre mc_traces a n_trials=1000, ops_per_trial=200,
# et rapporter {"violations": ..., "pire_solde": ..., "pire_ecart": ...}.
#
# Indice 1 : la borne superieure de Hoeffding pour 0 violation sur 200 000
#            essais est P <= 3/N (approx 1.5e-5) -- pas zero, mais comfortable.
# Indice 2 : si pire_solde < 0, c'est un bug de votre garde Python, pas du contrat.

result = None  # TODO etudiant : {"violations": ..., "pire_solde": ..., "pire_ecart": ...}

print("Exercice a completer : Monte-Carlo etendu (1000 x 200)")
Exercice a completer : Monte-Carlo etendu (1000 x 200)

Exercice 3 : pinpoint du théorème clé qui protège l’invariant

Le théorème transfer_preserves_supply est le plus subtil des trois (mint et burn sont plus directs). En regardant la définition dans MyIA.AI.Notebooks/SymbolicAI/SmartContracts/erc20_lean/ERC20/Invariant.lean lignes 93-127, identifiez :

  1. L’hypothèse-clé de la preuve (la condition qui rend l’invariant non-trivialement préservé) ;
  2. Le lemme intermédiaire crucial – probablement sum_univ_split ou sum_split_mem (cf. lignes 30-38) ;
  3. L’endroit de la preuve où l’arithmétique ℕ est utilisée (et où une erreur sur ℕ aurait des conséquences).

Indice 1 (hypothèses) : transfer_preserves_supply (s src dst amount) (hguard : s.balances src ≥ amount) (hne : src ≠ dst) (h : supplyInvariant s). C’est exactement 3 hypothèses : la garde solde suffisant, la non-égalité des adresses, et l’invariant sur l’état pré-transition.

Indice 2 (lemme intermédiaire) : sum_univ_split (f : Address n → ℕ) (a : Address n) : ∑ x : Address n, f x = f a + ∑ x ∈ (univ : ...).erase a, f x. C’est l’extraction additive d’un point – la brique qui permet d’extraire src puis dst de la somme des soldes successifs.

Indice 3 (omega) : la fin de la preuve (omega) est le moment où Lean ferme l’arithmétique ℕ – c’est l’étape où une éventuelle erreur de soustraction ℕ - ℕ ferait dérailler le raisonnement. omega couvre l’arithmétique linéaire sur les naturels, ce qui est suffisant ici parce que les sommes ont été décomposées additivement avant lui.

# Exercice 3 : pinpoint des hypotheses et lemmes cles de transfer_preserves_supply
# TODO etudiant : ouvrir le fichier ERC20/Invariant.lean et annoter les 3 reponses.
#
# Indice : lire le bloc ligne 93-127 ; c'est une preuve de 30 lignes en `omega`
# + `simp only` + `sum_univ_split` + `sum_split_mem`. Aucune magie, juste la
# decomposition de la somme en "part du src" + "part du dst" + "reste".

result = None  # TODO etudiant : {"hypothese_cle": "...", "lemme_intermediaire": "...", "arithm_Nat": "..."}

# Etape 1 : lire ERC20/Invariant.lean (MyIA.AI.Notebooks/SymbolicAI/SmartContracts/erc20_lean/).
# Etape 2 : identifier l'hypothese-cle (probablement hguard ou hne).
# Etape 3 : reperer sum_univ_split et le role additif (sortir src, puis dst).
# Etape 4 : reperer omega et expliquer pourquoi il suffit (somme deja decomposee).

print("Exercice a completer : pinpoint de la preuve de transfer_preserves_supply")
Exercice a completer : pinpoint de la preuve de transfer_preserves_supply

Références

  • Issue #4047 — Epic source du lac erc20_lean (phase 1 livrée : scaffolding, modèle, transitions gardées, préservation de l’invariant, absence de sorry).
  • EIP-20 (F. Vogelsteller, V. Buterin, 2015) — ERC-20 Token Standard, Ethereum.
  • K. Bhargavan et al., Formal Verification of Smart Contracts, WPCE 2016 — pionnier sur la vérification formelle Bitcoin/Ethereum ; citée dans le README.md du lac erc20_lean.
  • SC-07-Token-Standards-Python.ipynb (SmartContracts/02-Solidity-Advanced/) — le notebook précédent, qui déploie SimpleERC20 sur anvil et démontre les transitions ERC-20.
  • Le lac erc20_lean (MyIA.AI.Notebooks/SymbolicAI/SmartContracts/erc20_lean/) — la version Lean 4 + Mathlib, le « moteur formel » du présent notebook.
  • Le notebook compagnon Lean-23 — qui interroge directement le lac Lean pour ses #check réels.
  • EPIC #4980 — convention i18n Lean (sibling pair FR/EN dans ERC20.lean / ERC20_en.lean).
  • Notebooks associés : [SC-08-DeFi-Primitives-Python](./SC-08-DeFi-Primitives-Python.ipynb), [SC-11 (LLM-Assisted)](./SC-11-LLM-Assisted-Python.ipynb), [Lean-22 (Galois) >](../../Lean/Lean-22-Galois-Probleme-Inverse-M23.ipynb).
Retour au sommet