Skip to content

feat(lean): MacroCell quadtree + Hashlife algorithm + Lean-14 update (Epic #1647)#1989

Closed
jsboige wants to merge 3 commits into
mainfrom
feat/conway-hashlife-macrocell
Closed

feat(lean): MacroCell quadtree + Hashlife algorithm + Lean-14 update (Epic #1647)#1989
jsboige wants to merge 3 commits into
mainfrom
feat/conway-hashlife-macrocell

Conversation

@jsboige
Copy link
Copy Markdown
Owner

@jsboige jsboige commented May 31, 2026

Summary

Phase 3a of Conway Game-of-Life Epic #1647.

New modules

Module Lines sorry Description
Conway.Life.MacroCell 265 0 Quadtree data structure with toGrid/buildFromGrid round-trip
Conway.Life.Hashlife 339 0 Gosper's Hashlife algorithm (evolveHashlife top-level API)

Hashlife algorithm details

  • step4x4: level-2 base case (4x4 grid → centered 2x2, one generation via direct B3/S23)
  • hashlifeResult (partial def): recursive case — level-k → level-(k-1), advances 2^(k-2) generations
  • centerInLevelPlus2, hashlifeStep1, hashlifeStep: single-generation wrappers
  • hashlifeFastForward: k iterations of hashlifeStep1
  • evolveHashlife: top-level Grid → Grid API

Lean-14 notebook update

  • Section 9 rewritten: List/Bool design (not Finset/Prop)
  • Stats now cover all Life modules (Life + Spaceships + Oscillators + MacroCell + Hashlife)
  • lake build Conway (full, 3331 jobs)
  • grep -c sorry = 0 on all Life files
  • Roadmap updated: Phase 5 FAIT, Phase 3a/3b "En cours"

Verification (lean-merge-discipline HARD gate)

lake build Conway.Life.MacroCell Conway.Life.Hashlife → SUCCESS (3318 jobs)
grep -c sorry MacroCell.lean = 0
grep -c sorry Hashlife.lean = 0
All 15 #eval checks return expected values

Follow-up to #1975 (Spaceships + Oscillators, already merged).

Co-Authored-By: Claude Opus 4.8 noreply@anthropic.com

@github-actions
Copy link
Copy Markdown

github-actions Bot commented May 31, 2026

Notebook PR Validation: PASS

  • Notebooks checked: 1
  • Code cells validated: 8
  • Result: All passed

Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns)
Non-Python kernels (.NET/Lean): C.1 + errors only (execution_count advisory)
QuantConnect notebooks: C.1 + errors only (require QC Cloud for execution)

@jsboige jsboige mentioned this pull request Jun 1, 2026
Merged
clusterManager-Myia
clusterManager-Myia reviewed Jun 1, 2026
View reviewed changes
Copy link
Copy Markdown
Collaborator

@clusterManager-Myia clusterManager-Myia left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

[Hermes] — COMMENT_WITH_CONCERNS

Feature ambitieuse : MacroCell quadtree + Hashlife recursif + MacroCell.lean (265 LOC) + Hashlife.lean (339 LOC). CI green, gitleaks clean.

Concerns :

  1. Second reviewer souhaitable : 604 LOC Lean formelles avec algorithme recursif memoize. Règle cluster : PR > 200 LOC → 2 reviewers.
  2. Validation invariants Hashlife : step4x4 compute via applyB3S23 sur 4x4 sub-grids — verifier que la canonicalization (horizontal/vertical result caching) ne peut pas produire de faux resultats pour les macrocells border.
  3. centerInLevelPlus2 padding strategy : conversion Grid→MacroCell puis retour. S'assurer que le padding ne perd pas de cellules aux bords pour les patterns non-centres.

Code qualitatif, strategy List pour native_decide bien argumentee. Roadmap mise a jour proprement. Approvable post second review.

@jsboige jsboige force-pushed the feat/conway-hashlife-macrocell branch from 3199fba to ba3fb70 Compare June 1, 2026 02:54
clusterManager-Myia
clusterManager-Myia reviewed Jun 1, 2026
View reviewed changes
Copy link
Copy Markdown
Collaborator

@clusterManager-Myia clusterManager-Myia left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

[Hermes] — COMMENT_WITH_CONCERNS (re-review, SHA changed since 3199fba)

Security scan: CLEAN. CI: 5/5 green. Deux nouveaux commits depuis la precedente review :

ba3fb70 — fix(security): auto-detect Lean project path, strip absolute paths from output
60bbba8 — chore: regenerate catalog markers (fix drift CI)

Points resolus depuis la precedente review :

  • Path hardcode supprime : find_conway_lean_project() auto-detect, win_to_wsl() convertit dynamiquement. Output affiche .../conway_lean au lieu du chemin absolu. Concern #4 de la review precedente resolu.

Concerns persistants :

  1. Second reviewer obligatoire (regle cluster : > 200 LOC Lean formelles). MacroCell.lean (265 LOC) + Hashlife.lean (339 LOC) = 604 LOC avec algorithme recursif memoize. Approvable post second review.

  2. sorry=1 dans Conway.lean root. Concern #1 de la review precedente toujours pertinent : le build passe (3334 jobs) mais le sorry doit etre trace. Clarifier si preexistant ou introduit.

  3. Dependance PR #1975. Concern #3 toujours ouvert : le notebook reference Spaceships.lean et Oscillators.lean comme existants. Verifier que PR #1975 est mergee avant cette PR.

jsboige and others added 3 commits June 1, 2026 06:50
@jsboige @claude
feat(lean): MacroCell quadtree + Hashlife algorithm + Lean-14 noteboo…
481281e 
…k update (Epic #1647)

Phase 3a of Epic #1647: Hashlife implementation in Lean 4.

- Conway/Life/MacroCell.lean: quadtree data structure (265 lines)
  - inductive MacroCell (leaf | node nw ne sw se)
  - level, size, emptyOfLevel, isEmpty helpers
  - toGrid / buildFromGrid round-trip with sortDedup
  - gridFrame, gridToMacroCellWithOffset, gridToMacroCell helpers
  - 5 round-trip #eval checks (block, blinker_h, glider, beehive, toad)

- Conway/Life/Hashlife.lean: Gosper's Hashlife algorithm (339 lines)
  - step4x4: level-2 base case (4x4 -> centered 2x2, one generation)
  - hashlifeResult: recursive case (level-k -> level-(k-1), 2^(k-2) gens)
  - centerInLevelPlus2: padding for one-generation step
  - hashlifeStep1 / hashlifeStep: single-generation wrappers
  - hashlifeFastForward: k iterations of hashlifeStep1
  - evolveHashlife: top-level Grid -> Grid API
  - 10 round-trip #eval checks (all true)

- Conway.lean: added imports for MacroCell + Hashlife

- Lean-14-Conway-Tribute.ipynb: updated for PR #1975
  - Section 9 rewritten: List/Bool design (not Finset/Prop)
  - Stats now cover all 3 Life modules
  - lake build Conway (full, 3333 jobs)
  - sorry count on all Life files
  - Roadmap updated: Phase 5 done, Phase 3 in progress

Verification:
- lake build Conway SUCCESS (3333 jobs)
- grep -c sorry = 0 in MacroCell.lean and Hashlife.lean
- All #eval checks return true
- Papermill 26/26 cells, 0 errors (63s)

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@jsboige @claude
fix(security): auto-detect Lean project path in Lean-14 cell-2, strip…
08205cb 
… leaked paths

Cell 2 (subprocess-setup) hardcoded absolute paths:
- LEAN_PROJECT = '/mnt/c/dev/CoursIA/...' (machine-specific)
- WIN_LEAN_PROJECT = Path('C:/dev/CoursIA/...') (machine-specific)
- Outputs leaked both paths

Fix: auto-detect from notebook location via find_conway_lean_project()
+ generic drive-letter conversion via win_to_wsl(). Outputs show
relative paths only ('.../conway_lean') with drive letter indicator.

Also resolves rebase conflict in Conway.lean (RLE + MacroCell + Hashlife
imports merged correctly).

Re-executed via Papermill (3m34s). 8/8 code cells OK, 0 leaks, lake build
SUCCESS (3333 jobs), sorry=0 on Life modules.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@jsboige
chore: regenerate catalog markers (fix drift CI)
cd4991a
@jsboige jsboige force-pushed the feat/conway-hashlife-macrocell branch from 60bbba8 to cd4991a Compare June 1, 2026 04:50
@jsboige jsboige mentioned this pull request Jun 1, 2026
Merged
@jsboige
Copy link
Copy Markdown
Owner Author

jsboige commented Jun 1, 2026

Superseded by #2008 (merged). #2008 is a strict superset: it contains all files from this PR (Lean-14 notebook, MacroCell.lean, Hashlife.lean, Conway.lean imports, README) plus the new Computation.lean module (12 theorems, 0 sorry: Hashlife/reference consistency + eater1 still-life + glider/MacroCell round-trips) and the SymbolicAI/README update. ai-01 verified locally: lake build Conway SUCCESS (3335 jobs, exit 0), sorry-delta=0 vs origin/main, 0 path-leaks in source+outputs, C.2 8/8 cells with exec+outputs. No content lost. Merci po-2026 — le fix path-leak cell-2 (find_conway_lean_project auto-detect) est preserve dans #2008.

@jsboige jsboige closed this Jun 1, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@clusterManager-Myia clusterManager-Myia clusterManager-Myia left review comments

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@jsboige @clusterManager-Myia