Greffe 4 (#13570) : le dépôt porte déjà, séparés, les trois organes d’une procédure de choix social argumentée — l’argumentation de Dung (ICT/Tweety), les règles de vote (SocialChoice), le comptage exécutable et falsifiable (SmartContracts : SC-17 vote vérifiable, SC-9 gouvernance DAO, SC-13 fuzz d’invariants). Cette greffe les branche ensemble : les positions votées viennent du graphe argumentatif, l’agrégation est une règle nommée et justifiée (Borda), l’exécution et l’audit sont sur chaîne, et la robustesse est falsifiée par fuzzing — y compris sur un contrat volontairement cassé.
Une greffe ne redémontre pas ce que les organes prouvent déjà : elle les consomme (principe #13564 — nommer l’organe natif plutôt que le réimplémenter). Ici : ict/argumentation.py (DungAF, sémantique grounded), les contrats BordaVote/BordaVoteBroken du projet Foundry greffe4-vote (compagnon de ce notebook), et l’outillage SC-12/SC-13 (forge, invariant fuzzing).
Statut épistémique — Sans verdict à ce jour : aucune ligne de la matrice de dissociations ne concerne ce notebook ; son statut épistémique sera porté par la matrice le cas échéant.
le débat : un graphe d’attaques dont la sémantique grounded produit une position (in / out / undec) par candidat
SocialContracts/greffe4-vote/src/BordaVote.sol (EVM, SC-17/SC-9 en lignée)
l’agrégation exécutable : comptage Borda on-chain, un vote par adresse, dépôt d’événements auditables
greffe4-vote/test/ + forge (SC-12/SC-13)
l’audit falsifiable : invariants I1/I2 fuzzés sur le contrat correct, et cassés par le fuzzer sur le contrat volontairement dégradé
La boucle : l’argumentation produit les raisons (positions), le choix social agrège (Borda), la chaîne exécute et prouve (comptage public + invariants). Chaque étape est testable séparément — c’est ce qui rend la greffe falsifiable.
Le débat : un AF de Dung sur trois propositions
Un collectif doit trancher entre trois propositions \(C_0\), \(C_1\), \(C_2\) (par ex. trois allocations du trésor d’une DAO). Le débat est un argumentation framework : 8 arguments, 5 attaques. Chaque candidat a un argument pro ; certains ont un argument contra non attaqué, d’autres une défense (un argument qui attaque l’attaquant).
La sémantique grounded (plus petit point fixe de la fonction caractéristique de Dung) labellise chaque argument : in (accepté), out (attaqué par un in), undec (les deux cas — cycles). La position d’un candidat se lit sur son argument pro : in = soutenu par le débat, out = réfuté, et l’ordre d’entrée dans le point fixe (le « round » de défense) distingue un soutenu immédiat d’un soutenu au terme d’une chaîne de défense.
# Le debat, construit sur l'organe natif ict.argumentation (aucune reimplementation)import sys, ossys.path.insert(0, os.path.abspath("."))from ict.argumentation import DungAF, grounded_labelingARGS =list(range(8))ATTACKS = [(1, 0), (4, 3), (5, 4), (6, 2), (7, 6)] # (attaquant, attaque)PRO = {0: "C0", 2: "C1", 3: "C2"} # arguments pro par candidatCONTRA = {1: "C0", 4: "C2", 6: "C1"} # arguments contra par candidatCANDS = ["C0", "C1", "C2"]debate = DungAF(ARGS, ATTACKS)labels_full = grounded_labeling(debate)print("Labeling grounded du debat complet :")for a in debate.arguments: role =f"pro-{PRO[a]}"if a in PRO else (f"contra-{CONTRA[a]}"if a in CONTRA else"defense")print(f" arg {a} ({role:<12}) : {labels_full[a]}")
Labeling grounded du debat complet :
arg 0 (pro-C0 ) : out
arg 1 (contra-C0 ) : in
arg 2 (pro-C1 ) : in
arg 3 (pro-C2 ) : in
arg 4 (contra-C2 ) : out
arg 5 (defense ) : in
arg 6 (contra-C1 ) : out
arg 7 (defense ) : in
Lecture du débat complet
\(q_0\) (contra-\(C_0\)), \(d_1\), \(d_2\) sont inattaqués → in dès le premier round. Conséquence : \(p_0\) est out (\(C_0\)réfuté — sa réfutation n’a pas de défense).
\(q_1\) et \(q_2\) sont attaqués par des in → out. Conséquence : \(p_1\) et \(p_2\) passent in au round suivant (\(C_1\) et \(C_2\)soutenus, mais au prix d’une défense).
Position du débat complet : \(C_0\) réfuté, \(C_1\) et \(C_2\) soutenus — à départager par la profondeur de défense (le round où l’argument pro entre dans le point fixe).
# Position avec rounds synchrones : extension fidele de grounded_labeling, validee contre l'organe.# L'organe rend le labeling final ; on ajoute uniquement le ROUND d'entree (l'ordre de defense),# puis on verifie que le labeling final de l'extension coincide EXACTEMENT avec celui de l'organe.def grounded_rounds(af):"""Rounds synchrones du point fixe grounded : {argument: round d'entree dans IN}.""" IN, rnd =set(), {} round_no =0whileTrue: OUT = {b for b in af.arguments if af.attackers(b) & IN} new =sorted(c for c in af.argumentsif c notin IN and (not af.attackers(c) or af.attackers(c) <= OUT))ifnot new:return rndfor c in new: IN.add(c) rnd[c] = round_no round_no +=1def position_rank(af):"""Ordre total des candidats derive du graphe : (label, round de defense, id en dernier recours). label : in=0 < undec=1 < out=2. Le tie-break par id est une convention discloree : le labeling grounded produit un ordre PARTIEL, Borda consomme un ordre total.""" lab = grounded_labeling(af) rnd = grounded_rounds(af) key = {}for c in CANDS: pros = [a for a in af.arguments if PRO.get(a) == c] pl = [lab[a] for a in pros]if"in"in pl: key[c] = (0, min(rnd[a] for a in pros if lab[a] =="in"))elif"undec"in pl: key[c] = (1, 99)else: key[c] = (2, 99) order =sorted(CANDS, key=lambda c: (key[c], c))return order, key, lab# --- Validation de l'extension contre l'organe (5 AFs : complet + 4 expositions) ---EXPOSURES = {"V1": ARGS, # debat complet"V2": [a for a in ARGS if a !=5], # a rate la defense d2"V3": [a for a in ARGS if a notin (1, 6, 7)], # a rate q0 et tout le fil contra de C1"V4": [a for a in ARGS if a !=7], # a rate la defense d1}for name, expo in EXPOSURES.items(): sub = DungAF(expo, ATTACKS) lab_organ = grounded_labeling(sub) rnd = grounded_rounds(sub)# l'organe et l'extension doivent designer les memes IN (rounds uniquement en plus) in_ext = {a for a in sub.arguments if a in rnd} in_organ = {a for a, l in lab_organ.items() if l =="in"}assert in_ext == in_organ, f"{name}: divergence extension/organe {in_ext} vs {in_organ}"print("Validation : l'extension a rounds coincide avec grounded_labeling (organe) sur les 5 AFs.")
Validation : l'extension a rounds coincide avec grounded_labeling (organe) sur les 5 AFs.
La machinerie est prête — et validée contre l’organe. Chaque électeur vote maintenant sur son propre sous-graphe : quatre expositions du même débat, quatre bulletins sincères.
# Les bulletins sinceres : chaque electeur calcule la position SUR SON sous-graphe.# Votants = expositions epistemiques distinctes du MEME debat (ce qu'on a lu du fil).sincere = {}for name, expo in EXPOSURES.items(): sub = DungAF(expo, ATTACKS) order, key, lab = position_rank(sub) sincere[name] = order detail =", ".join(f"{c}:{key[c]}"for c in order)print(f"{name} (a lu {sorted(expo)}) : bulletin = {order} [{detail}]")print()print("Profils sinceres (du graphe, pas saisis a la main) :")for v, b in sincere.items():print(f" {v} : {b[0]} > {b[1]} > {b[2]}")
Lecture — les positions viennent du graphe (critère 4 de #13570)
Les quatre bulletins sont dérivés, pas saisis : chaque électeur applique grounded_labeling à son sous-graphe du débat (son exposition épistémique — quels messages du fil il a lus). La seule chose choisie par l’expérimentateur est l’exposition, jamais le classement :
V1 (débat complet) : \(C_1\) et \(C_2\) soutenus au même round → convention d’id ; \(C_0\) réfuté → \([C_1, C_2, C_0]\).
V2 (a raté la défense \(d_2\)) : la réfutation de \(C_2\) reste sans réponse → \(C_2\) réfuté → \([C_1, C_0, C_2]\).
V3 (a raté \(q_0\) et tout le fil contra de \(C_1\)) : \(C_0\) et \(C_1\) soutenus d’emblée (tie id), \(C_2\) au round suivant → \([C_0, C_1, C_2]\).
V4 (a raté la défense \(d_1\)) : la réfutation de \(C_1\) reste sans réponse → \(C_1\) réfuté, \(C_2\) soutenu → \([C_2, C_0, C_1]\).
Un même débat, quatre lectures — quatre ordres de préférence sincères distincts. C’est l’hétérogénéité épistémique réelle d’un collectif (un forum n’est jamais lu entièrement par personne), et c’est elle qui alimente le choix social.
La règle d’agrégation : Borda — nommée et justifiée (critère 1)
Règle retenue : le score de Borda (m = 3 candidats, points 3-2-1 par bulletin, le non-classé recevant 0). Le choix n’est pas « un vote » ; il est motivé :
Ce que le graphe produit : la position grounded donne par électeur un ordre (faible, quasi total) — un bulletin de classement. Une règle positionnelle à score consomme exactement ce format. L’approbation (binaire) devrait inventer un seuil que le labeling in/undec/out ne fournit pas ; le vote quadratique modélise des intensités d’achat de voix, hors sujet ici.
Ce que la chaîne supporte : Borda est O(L) par bulletin (L ≤ m rangs), stockage mapping(candidat → score) — le compteur le plus simple à exécuter on-chain (cf. SC-9 : les propositions DAO réelles comptent des poids, pas des tournois). Une méthode de Condorcet exige la matrice pairwise \(O(m^2)\) on-chain et n’a aucun gagnant garanti (cycles — le tournoi de ce profil a justement un match nul décisif, cf. exercice 2).
Ce que la greffe veut démontrer : Borda est la règle manipulable canonique des manuels (elle n’est pas stratégiquement-proof : Gibbard–Satterthwaite interdit toute règle non dictatoriale à ≥ 3 alternatives de l’être). Prendre Borda, c’est prendre une règle dont la faiblesse est documentée et exposable — le critère 2 de #13570 devient la démonstration du manuel, pas un artefact de bricolage.
# Comptage Borda de reference (le meme que le contrat executera) : points m, m-1, ..., 1def borda_scores(profile):"""profile: {votant: [candidats par preference decroissante]} -> {candidat: score}.""" scores = {c: 0for c in CANDS} m =len(CANDS)for ballot in profile.values():for i, c inenumerate(ballot): scores[c] += m - i # rang 0 -> m points (3-2-1)return scoresdef winner(scores):returnmax(sorted(scores), key=lambda c: scores[c]) # tie-break id, meme convention que le contratsincere_scores = borda_scores(sincere)w_sincere = winner(sincere_scores)print("Scores Borda sinceres :")for c insorted(sincere_scores, key=lambda c: -sincere_scores[c]): bar ="#"* sincere_scores[c]print(f" {c} : {sincere_scores[c]:2d}{bar}")print(f"\nGagnant sincere : {w_sincere}")
La manipulation : un bulletin contredisant sa propre position (critère 2)
Sur chaîne, le dépôt de chaque bulletin est un événement public (SC-17/SC-9) : le décompte courant — donc la marge — est visible de tous, avant la fin du vote. V3, dont la position sincère (déduite de son graphe) classe \(C_0\) premier et \(C_1\) second, lit la marge : \(C_1\) mène \(C_0\) d’un point. Le contrat acceptant des bulletins partiels (1 à 3 candidats, le non-classé recevant 0), V3 dispose de deux mensonges sur sa position :
l’enterrage — classer \(C_1\) dernier bien que son débat le soutienne : \([C_0, C_2, C_1]\) ;
le vote-balle (bullet vote) — ne classer que son candidat de tête : \([C_0]\), en omettant le \(C_1\) que son propre graphe soutient.
Les deux contredisent le labeling de son sous-graphe. On calcule les deux.
# Les deux ballots strategiques de V3, contre le sincerestrategies = {"sincere [C0,C1,C2]": dict(sincere),"enterrage [C0,C2,C1]": {**sincere, "V3": ["C0", "C2", "C1"]},"bullet [C0]": {**sincere, "V3": ["C0"]},}print(f"{'strategie de V3':<24}{'C0':>5}{'C1':>5}{'C2':>5} gagnant")for name, prof in strategies.items(): s = borda_scores(prof)print(f"{name:<24}{s['C0']:>5}{s['C1']:>5}{s['C2']:>5}{winner(s)}")strategic_scores = borda_scores(strategies["bullet [C0]"])w_strategic = winner(strategic_scores)print(f"\nSincere : {w_sincere} gagne -> vote-balle de V3 : {w_strategic} gagne (ecart strict 8-7-6)")print("Bascule :", "OUI, un seul electeur change le gagnant"if w_sincere != w_strategic else"non")
strategie de V3 C0 C1 C2 gagnant
sincere [C0,C1,C2] 8 9 7 C1
enterrage [C0,C2,C1] 8 8 8 C0
bullet [C0] 8 7 6 C0
Sincere : C1 gagne -> vote-balle de V3 : C0 gagne (ecart strict 8-7-6)
Bascule : OUI, un seul electeur change le gagnant
Lecture — enterrage, vote-balle, et le mensonge épistémique
Enterrage\([C_0, C_2, C_1]\) : \(8\)-\(8\)-\(8\), triple égalité — le gagnant change (\(C_0\), par la convention d’égalité), mais c’est le maximum atteignable : à 3 candidats, un enterreur qui garde son favori en tête ne peut pas faire mieux qu’égaliser (le leader perd 1 point, le troisième en gagne 1). Petit lemme structurel, lisible sur la cellule.
Vote-balle\([C_0]\) : \(C_0 = 8\), \(C_1 = 7\), \(C_2 = 6\) → \(C_0\) gagne strictement. En omettant le \(C_1\) que son propre débat soutient, V3 retire 2 points au leader : l’omission est un mensonge plus rentable que l’inversion (l’incitation de Borda à tronquer, documentée dans la littérature).
Le mensonge est localisé avec précision : le bulletin stratégique contredit le labeling du sous-graphe de V3 (son débat soutient \(C_0\) ET \(C_1\) au round 0). La manipulation électorale est ici un mensonge épistémique — voter autrement que ce que les arguments qu’on a lus établissent.
C’est la leçon de Gibbard–Satterthwaite (1973) : aucune règle non dictatoriale à ≥ 3 alternatives n’est non-manipulable — Borda ne fait pas exception, elle est l’exemple canonique. Et la transparence de la chaîne, vertu du vote vérifiable (SC-17), fournit l’information (la marge d’un point) qui rend la stratégie rationnelle : un trade-off réel des DAO, pas un accident du prototype.
L’exécution et l’audit sur chaîne — SC-13 : fuzzing des invariants
Le comptage Borda vit dans le projet Foundry compagnon SymbolicAI/SmartContracts/greffe4-vote/ (forge 1.7, la chaîne d’outils des notebooks SC-12/SC-13). Deux contrats, deux rôles :
Contrat
Garde
Rôle
BordaVote.sol
un vote/adresse, bulletin non vide, ≤ maxRank candidats, unicité des candidats (le classement d’un même candidat deux fois est rejeté)
le compteur correct
BordaVoteBroken.sol
un vote/adresse, non vide — ni borne de longueur ni unicité
le compteur volontairement cassé (témoin)
Les invariants fuzzés (fonctions invariant_* de forge) :
I2 (borne Borda) : \(\text{scores}[c] \le \text{maxRank} \times \text{totalBallots}\) — un bulletin ne peut donner à un candidat plus que maxRank points.
I1 (conservation) : la somme des points distribués reste bornée par maxRank × totalRankedCandidates.
Le harnais de fuzz simule des électeurs distincts (le contrat limite à un vote par adresse) et mappe les entrées du fuzzer vers 4 candidats et des longueurs 1-3 : l’espace des bulletins est petit et dense, le fuzzer exerce toutes les formes — y compris les bulletins invalides, que le contrat correct rejette.
# Le fuzzer au travail sur le contrat CORRECT : 32 runs x profondeur 48 = >1500 bulletins adverses.# L'invariant doit TENIR (garde d'unicite + borne de longueur).import os, shutil, subprocess, globdef find_forge(): exe = shutil.which("forge")if exe:return exe cand = os.path.expanduser("~/.foundry/bin/forge") + (".exe"if os.name =="nt"else"")return cand if os.path.exists(cand) elseNonedef find_greffe_project(start): cur = os.path.abspath(start)for _ inrange(6): hit = os.path.join(cur, "SymbolicAI", "SmartContracts", "greffe4-vote", "foundry.toml")if os.path.exists(hit):return os.path.dirname(hit) cur = os.path.dirname(cur)returnNoneforge = find_forge()project = find_greffe_project(os.getcwd())ifnot forge ornot project:print("Foundry introuvable - installer (cf SC-12, regle F : reparer, jamais contourner).")print("forge =", forge, "| project =", project)else: r = subprocess.run([forge, "test", "--match-contract", "BordaInvariants"], cwd=project, capture_output=True, text=True, timeout=300) out ="\n".join(l for l in r.stdout.splitlines() if l.strip())print(out)print(f"\n[exit code = {r.returncode}] (0 = suite verte attendue)")
No files changed, compilation skipped
Ran 5 tests for test/BordaInv.t.sol:BordaInvariants
[PASS] invariant_pointsConserved() (runs: 32, calls: 1536, reverts: 0)
╭-----------------+----------+-------+---------+----------╮
| Contract | Selector | Calls | Reverts | Discards |
+=========================================================+
| BordaInvariants | cast | 1536 | 0 | 0 |
╰-----------------+----------+-------+---------+----------╯
[PASS] invariant_scoreNeverExceedsBound() (runs: 32, calls: 1536, reverts: 0)
╭-----------------+----------+-------+---------+----------╮
| Contract | Selector | Calls | Reverts | Discards |
+=========================================================+
| BordaInvariants | cast | 1536 | 0 | 0 |
╰-----------------+----------+-------+---------+----------╯
[PASS] test_bordaPointsByRank() (gas: 173686)
[PASS] test_brokenViolatesBound() (gas: 672796)
[PASS] test_correctRejectsDuplicateCandidate() (gas: 13046)
Suite result: ok. 5 passed; 0 failed; 0 skipped; finished in 388.68ms (709.91ms CPU time)
Ran 1 test suite in 389.75ms (388.68ms CPU time): 5 tests passed, 0 failed, 0 skipped (5 total tests)
[exit code = 0] (0 = suite verte attendue)
Lecture — la borne tient sous attaque aléatoire
Plus de 1500 bulletins adverses déposés par le fuzzer depuis des électeurs distincts : aucun candidat ne dépasse jamais maxRank × totalBallots. La raison est structurelle, pas statistique — tout bulletin qui tenterait de sur-attribuer (candidat dupliqué) est rejeté par la garde d’unicité (test_correctRejectsDuplicateCandidate en est le témoin déterministe).
# Le controle negatif EXIGE (critere 3) : les MEMES invariants, sur le contrat casse.# Le fuzzer doit y decouvrir un contre-exemple. L'exit code NON NUL est le RESULTAT ATTENDU :# un fuzzing toujours vert ne prouve pas la robustesse, il prouve que le fuzzer n'a rien cherche.ifnot forge ornot project:print("Foundry introuvable (cf cellule precedente).")else: r = subprocess.run([forge, "test", "--match-contract", "BrokenInvariants"], cwd=project, capture_output=True, text=True, timeout=300) out ="\n".join(l for l in r.stdout.splitlines() if l.strip())print(out)print(f"\n[exit code = {r.returncode}] (NON NUL attendu : l'invariant DOIT echouer sur le casse)")
No files changed, compilation skipped
Ran 1 test for test/BrokenFuzz.t.sol:BrokenInvariants
[FAIL: assertion failed: 5 > 3]
[Sequence] (original: 1, shrunk: 1)
sender=0x00000000000000000000000000000000477e292c addr=[test/BrokenFuzz.t.sol:BrokenInvariants]0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496 calldata=cast(uint8,uint8,uint8,uint8) args=[4, 36, 2, 4]
invariant_scoreNeverExceedsBound() (runs: 1, calls: 1, reverts: 1)
Suite result: FAILED. 0 passed; 1 failed; 0 skipped; finished in 335.80ms (335.17ms CPU time)
Ran 1 test suite in 336.84ms (335.80ms CPU time): 0 tests passed, 1 failed, 0 skipped (1 total tests)
Failing tests:
Encountered 1 failing test in test/BrokenFuzz.t.sol:BrokenInvariants
[FAIL: assertion failed: 5 > 3]
[Sequence] (original: 1, shrunk: 1)
sender=0x00000000000000000000000000000000477e292c addr=[test/BrokenFuzz.t.sol:BrokenInvariants]0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496 calldata=cast(uint8,uint8,uint8,uint8) args=[4, 36, 2, 4]
invariant_scoreNeverExceedsBound() (runs: 1, calls: 1, reverts: 1)
Encountered a total of 1 failing tests, 0 tests succeeded
Tip: Run `forge test --rerun` to retry only the 1 failed test
Fuzz seed: 0x1a2878a47ae32a0d3757dd98b1237e9e293dea703fc67b3463c7a6459a45fe7a (use `--fuzz-seed` to reproduce)
[exit code = 1] (NON NUL attendu : l'invariant DOIT echouer sur le casse)
Lecture — le contre-exemple du fuzzer, décodé
forge rapporte assertion failed: 5 > 3 et le contre-exemple rétréci à un seul appel — par ex. cast(a, b, c, n) produisant le bulletin [x, x] (le même candidat aux deux rangs). Décodage : sur le contrat cassé, ce bulletin passe (pas de garde d’unicité) et attribue à \(x\) les points 3 + 2 = 5, alors que la borne I2 exige \(\le 3 \times 1 = 3\).
Le même invariant, la même borne, le même fuzzer : vert sur le contrat correct, cassé par découverte d’un contre-exemple sur le contrat dégradé. C’est la paire qui prouve que le fuzzing de cette greffe cherchait quelque chose (la continuité exacte de SC-13 : moyenne naïve qui déborde vs moyenne corrigée).
Ce que la chaîne ajoute — et ce qu’elle ne résout pas
Ajoute : un comptage public et immuable (chaque bulletin est un événement, le score est lisible on-chain à tout instant — l’audit n’est pas un artefact de confiance mais un état de la machine) ; une exécution vérifiable par fuzzing (I1/I2) avec témoin négatif ; l’atomicité du dépôt (un vote par adresse, garanti par la machine, pas par la bienséance).
Ne résout pas : la sincérité. La manipulation de V3 survit à la chaîne — l’impossibilité de Gibbard–Satterthwaite porte sur la règle, pas sur le substrat d’exécution. Pire, la transparence (le décompte courant visible) équipe le manipulateur : la marge d’un point n’est connue de V3 que parce que le tally est public. La greffe ne referme pas la boucle normative ; elle la rend mesurable.
Limites honnêtes (prototype) : 4 électeurs jouets, 3 candidats ; la convention de tie-break par identifiant (le labeling grounded produit un ordre partiel, Borda consomme un ordre total) est disclosée ; les positions viennent de l’organe ict/argumentation.py (DungAF), le graphe AIF complet de #13567 reste séquencé — cette greffe le consommera tel quel quand il existera, sans changer une ligne du côté vote.
Exercices
Exercice 1 — La cinquième lecture du débat
Trouvez une exposition du débat (un sous-ensemble des 8 arguments — ni le classement, ni la règle ne doivent être modifiés) qui produise le bulletin sincère \([C_2, C_1, C_0]\). Indice : \(C_2\) doit être soutenu immédiatement et \(C_0\) réfuté — que faut-il ne pas avoir lu pour que la réfutation de \(C_2\) n’existe pas ?
# Exercice 1 a completer : definir EXPO5 (sous-ensemble de ARGS), verifier le bulletin derive.# Etape 1 : EXPO5 = [ ... ] # les arguments que V5 a lus# Etape 2 : sub5 = DungAF(EXPO5, ATTACKS) ; order, _, _ = position_rank(sub5)# Etape 3 : verifier order == ["C2", "C1", "C0"]EXPO5 =None# TODO etudiant : remplacer par une liste d'arguments lus par V5if EXPO5 isNone:print("Exercice a completer : EXPO5 (cf indice — quelle attaque faut-il ne pas avoir lue ?)")else: sub5 = DungAF(EXPO5, ATTACKS) order5, key5, _ = position_rank(sub5)print(f"V5 (a lu {sorted(EXPO5)}) : bulletin = {order5}")print("Attendu ['C2', 'C1', 'C0'] :", "OUI"if order5 == ["C2", "C1", "C0"] else"NON")
Exercice a completer : EXPO5 (cf indice — quelle attaque faut-il ne pas avoir lue ?)
Exercice 2 — Le tournoi majoritaire : pas de Condorcet ici
Construisez la matrice pairwise du profil sincère (pour chaque paire, combien d’électeurs préfèrent \(x\) à \(y\)). Montrez que aucun gagnant de Condorcet n’existe sur ce profil (le match \(C_1\) contre \(C_0\) se termine 2-2), et expliquez en une phrase ce que Borda exploite que le tournoi pairwise jette (l’information positionnelle des classements).
# Exercice 2 a completer : tournoi majoritaire du profil sincere.# Etape 1 : pour chaque paire (x, y), compter les votants preferant x a y (ballot.index(x) < ballot.index(y))# Etape 2 : chercher un candidat battant tous les autres a la majorite strictedef pairwise(profile): wins = {c: 0for c in CANDS}# TODO etudiant : remplir wins puis retourner la matrice des duelsreturn winswins = pairwise(sincere)ifall(v ==0for v in wins.values()):print("Exercice a completer : implementer pairwise (cf etapes).")else:for c insorted(CANDS, key=lambda c: -wins[c]):print(f" {c} : {wins[c]} duels gagnes")
Exercice a completer : implementer pairwise (cf etapes).
Exercice 3 — V4 ne peut PAS manipuler : l’opportunité est spécifique à l’électeur
-Énumérez les bulletins possibles de V4 — les 6 permutations et les bulletins partiels (\([C_2]\), \([C_2, C_0]\), \([C_2, C_1]\)… autorisés par le contrat : 1 à 3 candidats) — les trois autres votants restant sincères, et montrez qu’aucun n’élit \(C_2\), le candidat de tête de V4. Conclusion en une phrase : pourquoi la manipulation de V3 (énoncé plus haut) était-elle possible mais pas celle de V4 ?
# Exercice 3 a completer : enumeration des bulletins de V4 (perms + partiels), aucun n'elit C2.from itertools import permutationsBULLETINS_V4 = [] # TODO etudiant : les 6 permutations de CANDS + les partiels commencant par C2gagnants = [] # TODO etudiant : pour chaque bulletin, recompter borda_scores et noter winner(...)ifnot BULLETINS_V4 ornot gagnants:print("Exercice a completer : enumerer les bulletins de V4 (cf TODO) et verifier qu'aucun n'elit C2.")else:print("Gagnants atteints :", sorted(set(gagnants)))print("C2 elu par un ballot de V4 :", "OUI"if"C2"in gagnants else"NON")
Exercice a completer : enumerer les bulletins de V4 (cf TODO) et verifier qu'aucun n'elit C2.
Conclusion
La boucle est fermée : les raisons (un AF de Dung, sémantique grounded — organe ict/argumentation.py), l’agrégation (Borda, nommée et justifiée — 3-2-1 on-chain), l’exécution et l’audit (contrats Foundry, invariants I1/I2 fuzzés sur >1500 bulletins adverses, contre-exemple découvert par le fuzzer sur le contrat cassé). Les trois organes préexistaient, séparés, dans le dépôt ; la greffe les a branchés sans en réimplémenter aucun.
Deux résultats à retenir :
Positions dérivées, jamais saisies — quatre lectures du même débat donnent quatre bulletins sincères distincts (critère 4) ; l’hétérogénéité épistémique du collectif est le carburant du choix social.
La manipulation mesurée — un électeur, un vote-balle (\([C_0]\)) qui omet la moitié de sa propre position argumentative, un gagnant basculé strictement (critère 2) ; et la transparence de la chaîne, qui équipe le manipulateur, est le trade-off honnête de la greffe : la chaîne exécute et prouve le comptage, elle ne peut pas rendre les électeurs sincères (Gibbard–Satterthwaite).
Références
Issue #13570 — la greffe 4 : vote vérifiable et gouvernance DAO, branchés sur l’argumentation et le choix social.
#13567 — le graphe argumentatif AIF (séquencé) ; cette greffe consomme l’organe DungAF en attendant.
Dung (1995), On the Acceptability of Arguments and its Fundamental Role in Nonmonotonic Reasoning — la sémantique grounded.
Gibbard (1973) / Satterthwaite (1975) — le théorème d’impossibilité de la manipulation.
SC-13 — Fuzz & Invariants : la paire naïf/corrigé dont BordaVote/BordaVoteBroken est la continuation directe.