Skip to content

docs: reorganize README/DESIGN, drop phased-plan framing - #36

Merged
leonardoalt merged 1 commit into
mainfrom
docs/cleanup-status
Jul 15, 2026
Merged

docs: reorganize README/DESIGN, drop phased-plan framing#36
leonardoalt merged 1 commit into
mainfrom
docs/cleanup-status

Conversation

@leonardoalt

Copy link
Copy Markdown
Member

Cleans up all documentation now that the semantics is essentially complete and the phased build plan no longer applies.

What changed

  • Removed the phased framing — the "Build plan (phases)" section and every Phase N / Option D / Sketch / skeleton / first cut label across README.md, DESIGN.md, and the module docstrings (Basic, Ast, Dialect, Equiv, Rewrites, Dialect/EVM).
  • README reorganized into: What is implemented · What is not (yet) done, and why · Tests · meta-theory scope note · worked example.
  • DESIGN reorganized into design decisions → language model → EVM dialect (calls/creates/selfdestruct/gas/static/observation) → What is provenWhat is not done, and why → toward-compiler-correctness → program logic. Fixed the stale statement that adequacy is "the pending proof" (it is proven and EVM.run_adequacy is instantiated).
  • Docs now reflect the recently landed work: open-world call/create boundary, gas() oracle, static write protection, selfdestruct schedule bit, CREATE failure rollback, extcodehash consistency, and frame-boundary observation (committedState/RunCommitted/deadStore_revert_obs_eq).

Not code

Documentation and docstrings only — no semantic changes. lake build green (8576 jobs); lake exe runLinter YulSemantics clean.

🤖 Generated with Claude Code

The phased build plan is obsolete now that the semantics is essentially
complete. Rework the docs to describe the current state directly:

- Remove the "Build plan (phases)" section and all `Phase N` / `Option D` /
  `Sketch` / `skeleton` / `first cut` planning labels from README.md, DESIGN.md,
  and the module docstrings (Basic/Ast/Dialect/Equiv/Rewrites/EVM).
- README: reorganize into "What is implemented", "What is not (yet) done, and
  why", "Tests", and the meta-theory scope note.
- DESIGN: fix the stale claim that adequacy is "the pending proof" (it is
  proven); split status into "What is proven" and "What is not done, and why";
  keep the accurate calls/creates/selfdestruct/static/gas/observation sections.
- Reflect the recently landed work: open-world call/create boundary, gas()
  oracle, static write protection, selfdestruct schedule bit, CREATE failure
  rollback, extcodehash consistency, and frame-boundary observation.

No code changes. lake build green (8576 jobs); runLinter clean.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@leonardoalt
leonardoalt marked this pull request as ready for review July 15, 2026 14:42
@leonardoalt
leonardoalt merged commit 5cfcdc8 into main Jul 15, 2026
1 check passed
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