Skip to content

[ADC-691] Prove complete IMEX-AMR lowering and rollback - #639

Draft
wolf75222 wants to merge 5 commits into
masterfrom
codex/adc691-imex-amr-proof-20260730
Draft

[ADC-691] Prove complete IMEX-AMR lowering and rollback#639
wolf75222 wants to merge 5 commits into
masterfrom
codex/adc691-imex-amr-proof-20260730

Conversation

@wolf75222

@wolf75222 wolf75222 commented Jul 30, 2026

Copy link
Copy Markdown
Owner

Résultat

Réaduit ADC-691 contre origin/master@de3f6b56 et ferme quatre écarts source de l’exemple final IMEX + AMR :

  • le LoweringCoverageReport global contient les autorités AMR résolues (hiérarchie, regrid, graphe et prédicats de tagging, conflit, transferts, subcycling et bootstrap) avec des cibles runtime explicites ;
  • l’exemple force un solve implicite singulier, consomme le SolveOutcome via RejectAttempt et compare le snapshot complet avant/après le rejet avant toute publication ;
  • l’hystérésis AMR est désormais réellement persistante (min_cycles=2) et son lowering nomme la route AmrProgramAcceptedState ;
  • le rejet, le restart strict et la parité Program manuel / pops.lib.time.IMEX comparent les octets opaques de l’image Program acceptée, sans réimplémenter son codec en Python.

La seule voie d’exécution reste :

Model -> Case -> validate -> resolve(AMR) -> compile -> bind -> pops.run

Aucun ProgramContext, AmrProgramContext, SystemStepper, accès _executor ou transaction manuelle n’est utilisé dans l’exemple.

Historique conservé

  1. codegen: include AMR authorities in lowering coverage
  2. examples: exercise fail-closed IMEX rollback
  3. tests: prove AMR coverage and rejected IMEX isolation
  4. merge explicite de origin/master (aucun rebase/squash/amend/force)
  5. examples: persist IMEX AMR tagging state

Validation locale source/Python

  • Ruff ciblé sur les 3 fichiers Python modifiés : OK
  • 2 tests ADC-691 source/résolution : 2 passed
  • couverture + résolution AMR persistante : 10 passed, 31 deselected
  • python docs/check_docs.py : OK, avec 1 avertissement de fraîcheur documentaire préexistant
  • git diff --check : OK

Preuves encore requises avant de déclarer les critères runtime fermés

  • aucun build natif n’a été lancé dans cette tranche : la lane native est réservée au gate ADC-687 ;
  • l’exécution directe du script, le rejet natif, HDF5/NPZ/ParaView, le restart strict et la continuation MPI doivent être prouvés sur le head 81f879af par la matrice native/installée ;
  • la CI du head rafraîchi est requise ; les anciens résultats de la PR ne prouvent pas ce head.

La PR reste volontairement en draft jusqu’à ces preuves.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant