C5 storage flip (étapes 3-4) + inventaire des chantiers en cours — récap de session 2026-08-13

[Th0rgal]

Récapitulatif de l'état au moment de la clôture de la session du 2026-08-13, couvrant la lane C5 (ContractState ≠ storage EVM), la lane forEach/refactor, et les lots orphelins à arbitrer.

---

Lane C5 — un seul map avec layout Solidity, lenses comme seule API

Fait (mergé)

• Étape 1 (feat(core): storage-lens API freeze — C5 step 1 #2323) : gel de l'API — gate à cliquet scripts/check_storage_lens_freeze.py dans make check (tout nouveau site brut échoue ; baseline par fichier qui ne peut que décroître).
• Étape 2 (feat(core): storage lenses off default simp — C5 step 2 #2326) : les lenses ne sont plus @[simp] global ; storage_simps reste laws-only (survivra au flip) ; ~25 fichiers de preuves réparés, zéro énoncé changé.
• Étape 2.5 (PR feat(core): storage-lens burn-down — C5 step 2.5 (pre-flip) #2329, ⚠️ à merger après CI verte — validation locale complète interrompue par la clôture, tous les modules touchés verts individuellement) : burn-down 304 → 63 sites bruts. Nouvelles lenses : bulk (writeSlots/modifySlots/writeTransientSlots/modifyTransientSlots/writeAddrSlots), withStorageChannel, ContractState.ofChannels. Baseline restante justifiée : Core (39, implémentations), Denote (6, faux positifs + bras find?), Owned/Basic (8, lane composition concurrente), TypedIRTests (3, faux positifs IRState), SourceSemantics (7, writers =-guardés dont le re-guard reshaperait GenericInduction).

Reste — Étape 3 (flip de représentation)

Design arrêté (informé par une recon complète de la dérivation de slots — voir ci-dessous) :

• StorageKey inductif injectif (| slot n | contractSlot c n | transient n | addr n | map n key | mapUint n k | map2 n k1 k2), DecidableEq ; ContractState.storageWords : StorageKey → Uint256 remplace les 7 champs de canaux. Le layout Solidity vit dans la structure de la clé ; l'effondrement keccak vers Nat reste côté compilateur — c'est ce qui préserve les lois storage_simps inconditionnellement (l'injectivité keccak n'est PAS prouvable et le repo la remplace déjà par des certificats non-alias finis).
• Les lectures restent stables : accesseurs def storage/storageAddr/storageMap/... aux anciens noms (dot-notation intacte) ⇒ les specs _meets_spec ne changent pas de forme, comme promis par le plan.
• storageArray (List, pas un mot) et knownAddresses (bookkeeping de preuve) restent des champs ce round.
• Séquence : flip dans Core + réimplémentation des lenses + repreuve des lois par injectivité de constructeurs → vague de réparation (résidus baseline + les ~60 sites simp [ContractState.writeX] explicites de l'étape 2, greppables) → baseline réduite à Core seul.
• Prérequis restants avant flip : migrer les writers =-guardés de SourceSemantics (impact GenericInduction), le bras find? de Denote, et statuer sur les 8 sites Owned (lane concurrente).

Reste — Étape 4 (correspondance lens-slot = slot CompilationModel/Yul)

Recon faite (résultats clés à réutiliser) :

• La dérivation canonique est Compiler.Proofs.abstractMappingSlot (= solidityMappingSlot, keccak kernel-computable, MappingSlot.lean:57) ∘ wordNormalize, + wordOffset pour struct members ; double mapping = composition ; chaînes = foldl.
• Les mappings sont déjà comparés dans le canal plat à des slots keccak (sourceResultMatchesIRResult ne compare que finalStorage ; finalMappings est une projection dérivée). Les canaux storageMap* sont des ombres write-only — encodeStorageAt ne les lit jamais.
• Le vrai trou : aucune cohérence prouvée entre les canaux ombre (ce que lisent readMap/les specs) et le canal plat aux slots dérivés. Livrable étape 4 : storageKeySlot : List Field → StorageKey → Option (Channel × Nat) + invariant MappingCoherent (ombre = plat au slot dérivé) + preuve que les write-helpers le préservent + lecture lens = encodeStorageAt sous cohérence.
• ⚠️ Divergence connue à trancher : les éléments de dynamic array utilisent solidityMappingSlot base idx dans le modèle source (findDynamicArrayElementAtSlot) mais keccak(slot)+i (layout Solidity réel) côté Yul/StructArrayStorage.
• Déjà prouvé et réutilisable : compiledMappingSlotPointer_eq_sourceMappingSlotRead (SolidityStorage.lean:92), les lemmes encodeStorageAt_write*_singleton_eq_written (GenericInduction/Storage.lean), les ponts packed/struct/array de StructArrayStorage.lean.
• Toucher la surface layout du compilateur ⇒ coordonner avec la lane forEach (Compile.lean/SupportedFragment.lean).

---

Lane refactor/forEach (session concurrente)

Arc admission forEach (design complet en mémoire de session) :

1. PR-A en cours de ship : CompiledNameDiscipline.lean (toolkit préfixes + loopFreeCheck/soundness + gate décidable forEachCompiledBodyChecks). Reste : forEach_loop_coupling (induction sur N−k ; corps via exec_compileStmtList_generic_sizeOf_extraFuel [Helpers.lean:3210], fuel via execIRStmt_boundedFor_stable [feat(proofs): fuel stability for literal-bound forEach loops #2328], shrink de scope via bindingsExactlyMatchIRVarsOnScope_of_included) + compiledStmtStep_forEach_literal (généralise Loops.lean:949/992).
2. PR-B : constructeur forEachLiteralBounded .literal 0 → .literal n (SupportedFragment.lean:373) + 7 sites consommateurs (Helpers.lean:1718/1866/2204, SupportedSpec.lean:3902/4096/6171/6296, EndToEnd/Base) + prédicat de surface (SupportedSpec.lean:1491) + enregistrement du checker.
3. PR-C optionnelle : lemme générique de discipline de noms (35 constructeurs SupportedStmtList) pour éliminer le decide du gate.
4. Limitation documentée : corps loop-free uniquement (les for_ imbriqués sont rejetés par varUntouchedCheck/LoopFree) — extension nested = chantier ultérieur.

Items de rotation restants : 7 (réduction allowlist proof-length, ~15 entrées), 8 (#2000 stores binding-aware pour payloads d'événements dynamiques), 9 (#1987 doc-sync — attention lane invisible active), 11 (identité Yul #2058/#2059), 3 (éclatement IRExecResult.outOfFuel, ~727 usages — à faire en dernier, décision actée), 5 (retrait lock-free erasure — uniquement sur décision explicite).

---

Lane événements / Lido (contexte)

• Journal d'appels + externalCall + checked arithmetic + préservation guarded des events : mergés (feat(proofs): guarded whole-contract event preservation + checked arithmetic completion #2321, feat(core): storage lenses off default simp — C5 step 2 #2326-era). Côté Lido : bump du pin, remplacer la CalleeInterface par AdversaryModel/journal.
• Lane feat(Events): broaden source-shaped emit surface (dynamic/struct event args) #2000 restante : events dynamiques/non-scalaires, emit imbriqué, events dans les fonctions lockées ; notModeledEventEmission conservé sciemment (ne couvre que rawLog, borne documentée dans TRUST_ASSUMPTIONS §Event Emission).

---

Lots orphelins / à arbitrer

• Une session « invisible » (hors ListAgents) travaille dans le même arbre : lane Ownable/OwnedCounterComposed/Specs.Composition/modifiers Macro + refactor owner.slot. Ses fichiers étaient non commités à la clôture.
• Patches sauvegardés dans le scratchpad de session (orphan-lanes/) : laneA-owned-slot-composition.patch (+ Composition.lean, Smoke-Include.lean), laneC-macro-modifiers.patch (883 lignes).
• ⚠️ Perte assumée : le lot docsync non commité (docs-site/*.mdx, ROADMAP, VERIFICATION_STATUS, docsync.py) a été écrasé par un checkout groupé dont la sauvegarde avait échoué en silence — en grande partie régénérable par les scripts generate_*.

Ordre suggéré à la reprise

1. Merger feat(core): storage-lens burn-down — C5 step 2.5 (pre-flip) #2329 (CI verte) puis la PR-A forEach de la lane concurrente.
2. C5 étape 3 (flip StorageKey) — le plus gros morceau restant, prérequis listés ci-dessus.
3. C5 étape 4 (cohérence ombre↔plat + storageKeySlot), coordonnée avec la surface layout.
4. Rotation : items 7/8/11, puis 3 en dernier.

[Th0rgal]

Précision post-clôture : la PR #2329 attend sa CI (validation locale rendue impossible par une session concurrente ayant reverté des fichiers de la PR dans le working tree partagé — sa branche feat/verity-mixin-include, commit afd65016, adapte déjà ses propres fichiers au flip C5). À la reprise : merger #2329 sur CI verte AVANT toute reprise de l'étape 3, et synchroniser la lane mixin/include avec l'état lens-migré de main.

[Th0rgal]

Session close status (forEach/refactor lane):

• feat(proofs): decidable admission gates for literal-bound forEach bodies #2331 merged — PR-A first slice: decidable admission gates (loopFreeCheck+soundness, prefix-discrimination toolkit, forEachCompiledBodyChecks) + main unbreak: feat(edsl): verifiable mixin include for proof reuse #2327 had landed four TypedIRCompilerCorrectness proofs relying on the pre-feat(core): storage lenses off default simp — C5 step 2 #2326 lens simp set; fixed by unfolding writeSlot at the four affected sites. Main is green again.
• feat(core): storage-lens burn-down — C5 step 2.5 (pre-flip) #2329: left unmerged — conflicts with feat(edsl): verifiable mixin include for proof reuse #2327 on GitHub and on rebase (its burn-down migrates the same files feat(edsl): verifiable mixin include for proof reuse #2327 re-added raw). Needs a rebase by its author or Thomas's arbitration; main no longer depends on it for green.
• Remainder of PR-A (forEach_loop_coupling + compiledStmtStep_forEach_literal) and PR-B/PR-C: fully designed, insertion points and eliminator signatures recorded in this issue's inventory above.

[Th0rgal]

Addendum final : l'agent de migration TypedIRTests a terminé après le commit de #2329 — la migration lens (79→3 sites) est DANS la PR, mais ses adaptations tardives aux APIs fraîchement mergées sur main (nouvel arg adtTypes de compileStmt, IRStorageWord.toNat/retypage flatStorage, retrait des annotations d'univers TExecState.{0}, 2 chaînes d'erreur packed-storage mises à jour) sont postérieures au commit. Elles sont sauvegardées en patch (149 lignes, typedirtests-post-commit-api-adaptations.patch dans le scratchpad de session, à côté des lots orphelins) : à appliquer lors du rebase de #2329 sur main — ce sont exactement les correctifs que la CI réclamera pour ce fichier.

[Th0rgal]

Reconciliation vs current main (c8f7a770, 2026-08-16)

The 2026-08-13 recap and later comments are no longer live truth for merged work.

Now on main (executable, merged)

• feat(core): storage-lens burn-down — C5 step 2.5 (pre-flip) #2329, feat(proofs): decidable admission gates for literal-bound forEach bodies #2331, feat(edsl): journal linked external calls in the executable plane #2334 already landed before this comment. Do not treat them as pending.
• fix(ci): give checks a monitored timeout budget #2336 (76c58a10, certified head 92630ce7): checks timeout 10 → 20 with verify-sync alignment. Local make check + 81 focused unit tests.
• feat(core): canonical StorageKey backing for ContractState #2335 (c8f7a770, certified head f8bd096a): C5 step 3 representation flip. ContractState.storageWords : StorageKey → Uint256, lens laws by constructor injectivity, freeze baseline 24 sites / 2 files (Verity/Core.lean + Contracts/TypedIRTests.lean). Full local lake build (2471 jobs) + make check. Zero new axioms.

Still open (do not mark complete)

• C5 step 4: storageKeySlot / shadow-vs-flat MappingCoherent is not done. Step 3 only flipped the source representation.
• forEach remainder (forEach_loop_coupling, PR-B forEachLiteralBounded), L2 widening, dynamic events (feat(Events): broaden source-shaped emit surface (dynamic/struct event args) #2000), etc.

This issue stays open until step 4 has executable evidence.

[Th0rgal]

C5 step 4 first slice is in #2337 (storageKeySlot + address-keyed MappingCoherent + aligned writeMap+writeSlot laws). It does not close this issue: field-list layout and global preservation under non-alias certificates remain.

[Th0rgal]

C5 step 4 slice 2 is in #2338 (MappingCoherentUint / MappingCoherentMap2 + aligned writeMapUint/writeMap2+writeSlot laws). It does not close this issue: field-list storageKeySlot and global preservation under finite non-alias certificates remain.

[Th0rgal]

C5 step 4 field-list first slice is in #2339 (FieldStorageKey: named CompilationModel field → root/map/mapUint/map2 StorageKey → storageKeySlot). It does not close this issue: remaining field-list cases (bytes32 keys, struct members, alias slots) and global preservation under finite non-alias certificates remain.

[Th0rgal]

C5 step 4 finite-set address preservation is in #2340 (MappingCoherentOn under DerivedAddrSlotsDistinct). It does not close this issue: global (all-keys) preservation, uint/map2 finite-set, and remaining field-list cases stay open.

[Th0rgal]

C5 step 4 finite-set uint/map2 preservation is in #2341 (MappingCoherentUintOn / MappingCoherentMap2On). It does not close this issue: global (all-keys) preservation and remaining field-list cases (bytes32 keys, struct members, alias slots) stay open.

[Th0rgal]

C5 step 4 mappingStruct member slots are in #2342 (fieldStructMemberSlot / fieldStructMember2Slot). It does not close this issue: global (all-keys) preservation, bytes32 keys, packed bit-ranges, and alias slots stay open.

[Th0rgal]

C5 step 4 alias-slot collapse is in #2343 (findFieldWriteSlots = resolved slot cons aliasSlots; persistent storageKeySlot is the head). It does not close this issue: global (all-keys) preservation, bytes32 keys, and packed bit-ranges stay open.

[Th0rgal]

C5 step 4 cross-channel finite-set preservation is in #2344 (aligned write on one mapping channel preserves another channel's *On list under an explicit derived-slot inequality). It does not close this issue: global (all-keys) preservation, bytes32 keys, and packed bit-ranges stay open.

[Th0rgal]

C5 step 4 bytes32 mapping compiler-slot collapse is in #2345 (fieldMapBytes32Slot / fieldStructMemberBytes32Slot). It does not close this issue: packed bit-ranges, mixed-key nestings, and global (all-keys) preservation stay open.