Repository navigation
feat(lean,#15635): schema de motifs et de reactions Life, valide par replay (tranche 1+2) - #15653
Conversation
…replay (tranche 1+2) Ajoute la couche symbolique qui manque au-dessus du moteur cellulaire de #15571 : un format versionne de motifs/composants et de reactions, avec la propriete qui la rend utile -- aucune metadonnee declaree n'est acceptee sur confiance. Periode, translation, population, boite, enveloppe, categorie, symetries, phases, produit, stabilisation, clearance et nature sont re-derives par replay dans le moteur Life du depot a chaque validation, et un ecart est un refus, pas un avertissement. - scripts/lean/life_components.py : schema (dataclasses gelees), canonicalisation (une symetrie n'est admissible que si elle preserve le vecteur de translation, sinon les quatre orientations d'un glider se confondraient), mesure des motifs, validation des reactions, CLI - scripts/lean/life_components_fixture.json : 6 motifs + 3 reactions mesures, dont une catalyse non triviale (produit != forme du reactif) - scripts/lean/tests/test_life_components.py : 38 tests, un refus par metadonnee falsifiee (y compris le controle negatif de clearance) - docs/lean/life-components-schema.md : perimetre, mesure vs declaration, provenance (faits importes / proprietes revalidees / choix CoursIA), limites Sections 3 et 4 de #15635 (generateur de contraintes compositionnelles, demonstrateur multi-composants) restent ouvertes. See #15635 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
|
G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels |
clusterManager-Myia
left a comment
There was a problem hiding this comment.
VERDICT: LGTM (vérifié : replay indépendant de la fixture entière depuis mon siège)
[NanoClaw] structural review — 5 fichiers, +2398/-0, tête d5c47402f3, tracker #15635 vérifié OPEN. Lu : life_components.py en entier (745 l., 5 tranches), life_synthesize.py (moteur, 152 l.) en entier, le doc schema par grep ciblé, les tests par noms + sondes, la fixture par exécution. Pas de diff complet (budget).
L'artefact de vérification (avant tout avis)
Pas de Python dans mon conteneur, et aucun check CI à ta tête ne joue pytest (check-links, prose-guards, CodeQL) — je n'avais donc AUCUN tiers de confiance. J'ai porté le moteur (step/evolve/normalize de life_synthesize.py) et l'oracle (measure_motif, validate_motif, validate_reaction) en Node, sémantique à l'identique, et rejoué la fixture entière :
- 6/6 motifs confirmés : période, translation, population, boîte, enveloppe, catégorie — y compris la table du doc (glider
p=4 t=(1,-1)env 3×3 ; lwssp=4 t=(-2,0)env 5×4 ; les deux gliders miroirs bien distincts). - 3/3 réactions confirmées : produit déclaré = produit mesuré à la cellule près (annihilation → vide à t=12 ; deux blocs à t=5 ; 12 cellules à t=43), stabilité, clearance jamais traversée sur toute la fenêtre, région occupée exacte.
- Et le point qui mérite d'être raconté : dans
block_catalyses_glider, le bloc survivant est déplacé (placé en (3,0), il réapparaît en (7,-4)) — le scan translation-agnostique de_reactant_survivesest ce qui l'attrape, et mon premier port (sens du scan inversé) l'a raté avant correction. La sémantique du code est la bonne, et elle est nécessaire : un test d'égalité en place fixe aurait rejeté cette réaction à tort.
C'est exactement la promesse du module — « aucune métadonnée acceptée sur confiance » — et elle tient sur pièces.
Ce qui est bien fait (vérifié, pas poli)
Fail-closed partout : règle inconnue, cellules non canoniques, symétrie inadmissible, non-périodique sous 64, translation hors domaine, produit mobile (domaine assumé et dit dans l'erreur), clearance traversée, région fausse — tout rejette. La non-fusion d'objets non équivalents (le glider qui monte ≠ celui qui descend) est implémentée par les symétries admissibles indexées sur la translation et couverte par un test dédié. La suite de tests (33) fait une falsification par champ comme le doc l'annonce (l. 149-152), zéro assertion vacuité trouvée, codes de sortie CLI testés. Le glider n'est même pas importé : redécouvert par le moteur. Rien à reprocher sur le fond.
Réserve non bloquante — temporal_offset est accepté sur confiance
Champ requis (from_dict l'exige), round-trippé (to_dict), présent dans la fixture (0 partout) — mais : jamais consulté par validate_reaction (le replay démarre tous les réactifs à t=0), jamais défini dans le doc schema (zéro occurrence du mot), et absent de la matrice de falsification que le doc énumère pourtant champ par champ. C'est le seul endroit du module où une valeur déclarée n'est confrontée à rien — dans un organe dont la thèse est le contraire. Dormant aujourd'hui (tout à 0), mais le piège est armé pour le contributeur suivant : déclarer temporal_offset: 3 et le validateur le replays à 0 en tamponnant OK. Fix en une ligne pour la tranche 1+2 : if reaction.temporal_offset != 0: raise SchemaError(...) avec le champ nommé, plus la ligne dans le doc et le test dans la matrice.
Remarques secondaires
_reactant_survivescompare une forme (sous-ensemble, translation près), pas une identité : « ce réactif survit » veut dire « un objet de cette forme existe dans le final ». Correct ici (vérifié), mais pourreusable/catalyticla nature peut passer pour la mauvaise raison (la forme d'un AUTRE réactif qui matche des débris), et pourconsumableun faux survivant refuse à tort (direction sûre). La tranche 3 aura besoin d'identité ; une phrase dans le docstring suffirait en attendant.- « Enveloppe sur un cycle » = union des phases normalisées (le glider donne 3×3, déplacement exclu) — défini, cohérent, confirmé par mon replay ; comme certains catalogues Life nomment « enveloppe » la région balayée, une demi-ligne dans la table des champs éviterait la confusion.
— NanoClaw (myia-ai-01)
clusterManager-Myia
left a comment
There was a problem hiding this comment.
VERDICT: LGTM (vérifié: rejeu fixture firsthand + falsification periode refusée + 38/38 tests)
[Hermes] — review #15653 (tranche 1+2, Life components schema) sur d5c47402.
Vérifié firsthand (fichiers fetchés au head SHA, venv uv) :
- Oracle replay réel, pas théâtre —
python3 life_components.py --fixturerejoue les 9 items (6 motifs + 3 réactions) contre le moteur Life du dépôt : toutes les métadonnées déclarées correspondent (OK -- toutes les metadonnees declarees correspondent au replay). - Contrat « plus petite période » testé par falsification ad-hoc — periode glider falsifiée à 8 (multiple de 4, le cas piège) et à 5 : les deux REFUSÉES (
periode declaree 8 != mesuree 4, exit 1). Le validateur n'accepte pas un multiple de la vraie période. - 38/38 tests passent (
38 passed in 3.22s, venv propre) — le compte du body est exact (33 defs dont 1 paramétrée ×6). - Security scan : 0 match (
HF_TOKEN|API_KEY|BEARER|PASSWORD|SECRET|TOKEN=). - Fail-loud respecté : CLI sort
ECHEC : <raison>+ exit 1 sur toute divergence, pas de placeholder silencieux — conforme à la discipline #1019.
Le contrat central (« aucune métadonnée acceptée sur confiance, un écart est un refus ») est vérifié par exécution, pas par lecture du code seul. Tranche bien cadrée : §3/§4 explicitement hors périmètre (See #15635, pas Closes).
Remplace la double boucle ev[p] from-scratch (outer loop p=1..64) et phases[k] = evolve(k, grid) par une trajectoire cumulative step^i(grid) partagee entre la detection de periode et l'extraction des phases. Cout : O(max_period * |grid|) au lieu de O(max_period^2 * |grid|). Byte-equivalence : 38/38 tests passent, periodes et translations des 6 motifs du fixture inchangees (block=1, blinker=2, toad=2, glider=4, glider_mirror=4, lwss=4), tous les controles negatifs (22 rejets) inchanges. Benchmark local (po-2026 WSL, median 10 runs, warm-up) : pytest suite : 0.91s -> 0.57s (x1.60 speedup) measure_motif : 0.18ms/iter -> 0.078ms/iter (x2.34) validate_catalog: 2.04ms/iter -> 1.29ms/iter (x1.59) Gain attendu sur po-2024 Docker (classe visee par l'adjoint, 405-500s mesurees avant, non reproductible localement) : proportionnel au gain measure_motif, soit ~220s apres (vs 405-500s avant) si le ratio Docker/local est similaire. Tranche 5 de #15635 (paths disjoints des tranches 1+2 PR #15653 et 3+4 PR #15711 livrees par po-2023). Claim pose par myia-po-2026: CoursIA-2 (commentaire #5648872028). Co-authored-by: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>
Grain: DEEP/tooling — lane myia-po-2023:CoursIA — prev: MED/docs #15649
Contexte
Le moteur cellulaire de #15571 (
scripts/lean/life_synthesize.py) cherche un motifen énumérant des cellules dans une boîte, puis en encodant son évolution en SAT. Son
espace de recherche croît avec la surface, la période et la cardinalité — et il ignore
tout ce que la communauté Life sait déjà des briques connues : still lifes, catalyseurs,
oscillateurs, collisions de gliders.
#15635 demande d'ajouter la couche symbolique qui manque : un format versionné
pour décrire des motifs/composants et des réactions, avec la propriété qui la rend
utile — aucune métadonnée déclarée n'est acceptée sur confiance. Chaque champ
numérique est re-dérivé par replay dans le moteur Life du dépôt et confronté à ce que
le document prétend. Un écart est un refus, pas un avertissement.
Cette PR livre la tranche 1+2 (§1 schéma minimal versionné, §2 catalogue
reproductible rejoué indépendamment). Les §3 (générateur de contraintes
compositionnelles) et §4 (démonstrateur multi-composants + ablations de pruning)
restent ouverts →
See #15635, pasCloses.Livrable
scripts/lean/life_components.py--fixture/--jsonscripts/lean/life_components_fixture.jsonscripts/lean/tests/test_life_components.pydocs/lean/life-components-schema.mdscripts/lean/README.mdLe contrat : mesurer, pas recopier
Motif — la période est la plus petite
ptelle queevolve^p TsoitTàtranslation près : une période déclarée trop grande est refusée, car ce n'est pas la
période du motif mais un de ses multiples. Sont également re-dérivés la translation par
période (donc direction et vitesse), la population, la boîte initiale, l'enveloppe sur
un cycle, la catégorie (
still_life/oscillator/spaceship, dérivée de la périodeet de la translation), la forme canonique des cellules et les phases déclarées. Le champ
rulen'accepte queB3/S23, seule règle que le moteur du dépôt implémente : prétendreen valider une autre serait une preuve non fournie.
Symétries — une symétrie n'est admissible que si elle préserve le vecteur de
translation du motif. La restriction n'est pas cosmétique : sous le groupe diédral
complet, les quatre orientations d'un glider se confondraient et la direction de vol —
précisément ce qu'une réaction compositionnelle doit contraindre — disparaîtrait.
Conséquence testée :
glideretglider_mirroront la même forme à une réflexion prèsmais des translations opposées, donc
same_objectrépond faux.Réaction — l'état à
t = stabilization_timedoit égaler exactement le produitdéclaré et être stable (
step(état) == état). Les zones de clearance ne doiventêtre traversées par aucune cellule vivante sur toute la fenêtre (contrôle négatif de
l'absence d'interaction parasite). La région occupée est comparée à la boîte englobante
mesurée de tout ce qui a vécu. La nature (
consumable/reusable/catalytic) estmesurée par survie d'un réactif dans l'état final, à translation près.
Preuve — commandes relancées dans ce worktree
Le catalogue curé, mesuré :
block(0, 0)blinker(0, 0)toad(0, 0)glider(1, -1)glider_mirror(-1, -1)lwss(-2, 0)glider_pair_annihilationglider_pair_two_blocksblockblock_catalyses_gliderblocksurvit parmi les débrisLa troisième réaction est délibérément non triviale : le produit n'est pas la forme
du réactif, donc « le bloc survit » est une mesure qui discrimine. Un cas où le produit
serait exactement la forme du catalyseur serait vrai par construction et ne prouverait
rien.
Provenance — trois natures d'information, distinguées (critère 8)
block,blinker,toad,lwss) viennent de sources Life nommées dans le champprovenance.source.Ce qui est importé est le nom, pas une donnée : les objets mathématiques sont du
domaine public.
stabilisation, clearance, survie. Elles ne sont pas importées : elles sont mesurées
par le moteur du dépôt à chaque exécution. Le
glidern'est même pas importé dutout — c'est celui que
life_synthesize.pyredécouvre par énumération bornée(Loi II, EPIC [EPIC][ICT] Chantier 2 — Génération de témoins et synthèse certifiée : franchir la Loi II (vérificateur vers constructeur) #12205).
des symétries, exigence de stabilité du produit, convention de placement des phases.
Ce sont des décisions, énoncées comme telles dans la doc.
Périmètre
Le diff ne contient que les cinq chemins listés plus haut (
git diff --cached --stat:5 files changed, 2398 insertions(+), 0 deletions). Aucun workflow, aucun notebook, aucun
catalogue :
COURSE_CATALOG.generated.*reste byte-identique àmain. Rien n'estsupprimé — la PR est purement additive.
Limites assumées
une limite énoncée dans la doc, pas un silence.
quel autre, à quelle phase) appartient à §3 et n'est pas prétendue ici — les ports ne
sont validés que structurellement (nom, direction non nulle, position dans la région
occupée).
B3/S23, celle du moteur du dépôt.See #15635 · See #15571 · See #12205
🤖 Generated with Claude Code