From 3a9bb307435675741e55ba778f236b5ae72fffb0 Mon Sep 17 00:00:00 2001 From: "Claude Sonnet 4.5" Date: Sat, 14 Feb 2026 23:42:34 +0000 Subject: [PATCH] docs: Add code comment conventions to CONTRIBUTING.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes #86 ### Summary Added comprehensive "Code Comment Conventions" section to CONTRIBUTING.md to prevent future documentation drift and establish clear standards. ### What's Included **Proof Status Conventions**: - Clear rules for when to use `sorry` vs no marker - Prohibition on TODO/STUB in proven theorems - Examples of good vs bad patterns **Module Documentation**: - Standard header format with Status/Dependencies - Clear status definitions (Complete/Partial/Draft) - Example template **Future Work Comments**: - Use `FUTURE:` instead of `TODO:` - Always link to tracking issue - Avoid FIXME/HACK **Implementation Notes**: - Use `NOTE:` for non-obvious design choices - Explain why, not just what - Reference related files **Axiom Documentation**: - Inline comment requirements - Link to AXIOMS.md - Consistent format **Property Test Tags**: - Must match Lean theorem names exactly - Standard tag format **What NOT to Include**: - Stale TODOs in completed code - Difficulty estimates after completion - Verbose explanations of obvious code - Inaccurate status claims ### Context Issue #86 identified stale TODO comments and inconsistent status claims. Recent refactoring commits (see #61, #62, #63) cleaned up the actual issues: - Removed 151 lines of stale planning comments - Deleted dead reentrancy wrappers - Fixed stale YulGeneration README - Removed 162 lines of stale/duplicate content This PR completes #86 by documenting conventions to prevent recurrence. ### Impact **Before**: - ❌ No documented comment conventions - ❌ Inconsistent status markers - ❌ TODOs in completed code - ❌ No guidance for contributors **After**: - ✅ Clear comment conventions documented - ✅ Standard status definitions - ✅ Examples of good/bad patterns - ✅ Prevents future documentation drift **For Contributors**: - Clear guidelines on code comments - Prevents misleading documentation - Consistent style across codebase - Easier code review ### Files Changed - `CONTRIBUTING.md`: Added 130-line "Code Comment Conventions" section ### Related Work Recent cleanup commits that addressed the actual issues: - #61: Delete dead reentrancy wrappers, clean stale proof comments - #62: Remove 151 lines of stale planning comments from proofs - #63: Simplify Compiler/Proofs/README.md from 324 to 109 lines Co-Authored-By: Claude Sonnet 4.5 --- CONTRIBUTING.md | 126 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 126 insertions(+) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 4f2b5763b..9a3fd0def 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -60,6 +60,132 @@ Co-Authored-By: Claude Sonnet 4.5 Types: `feat` `fix` `proof` `docs` `refactor` `test` `chore` +## Code Comment Conventions + +Follow these conventions to keep documentation accurate and maintainable. + +### Proof Status + +**For Theorems**: +- `sorry` - Incomplete proof (blocked by CI in proof files) +- No marker - Complete proof +- **DON'T** use TODO/STUB in proven theorems + +```lean +-- ✅ GOOD: Complete proof, no marker needed +theorem my_theorem : ... := by + unfold ... + simp [...] + +-- ❌ BAD: Complete proof but has misleading TODO +theorem my_theorem : ... := by + -- TODO: This actually works fine + unfold ... + simp [...] +``` + +**For Incomplete Proofs**: +```lean +-- Only in draft branches, NOT in main +theorem draft_theorem : ... := by + sorry -- Strategy: Use induction on List structure + -- See issue #123 for details +``` + +### Module Documentation + +**Module Headers** should reflect current status: + +```lean +/-! ## Module Name + +Brief description of what this module does. + +**Status**: Complete | Partial | Draft +**Dependencies**: List axioms/external dependencies +**Related**: Links to other relevant modules +-/ +``` + +**Status Definitions**: +- **Complete**: All theorems proven, no sorry +- **Partial**: Some proven, some sorry (specify which) +- **Draft**: Structural outline only + +**Example**: +```lean +/-! ## Layer 3: Statement-Level Equivalence + +Proves IR statement execution is equivalent to Yul statement execution +when states are aligned. + +**Status**: Complete - All statement types proven +**Dependencies**: Requires expression evaluation axioms (see AXIOMS.md) +-/ +``` + +### Future Work Comments + +For planned improvements or known limitations: + +```lean +-- FUTURE: Add support for delegatecall +-- See issue #123 for design discussion +def currentImplementation := ... +``` + +**DON'T** use: +- ~~`TODO:`~~ (implies incomplete current work) +- ~~`FIXME:`~~ (implies broken code) +- ~~`HACK:`~~ (use `NOTE:` with explanation instead) + +### Implementation Notes + +For non-obvious design choices: + +```lean +-- NOTE: We use fuel-based recursion here because Lean cannot prove +-- termination for mutually recursive functions with this structure. +-- See Equivalence.lean for the proof strategy this enables. +def execIRStmtFuel (fuel : Nat) : ... := ... +``` + +### Axiom Documentation + +All axioms **must** be documented inline **and** in AXIOMS.md: + +```lean +/-- AXIOM: Expression evaluation equivalence + +This is an axiom because both evalIRExpr and evalYulExpr are partial functions. +See AXIOMS.md for full soundness justification. +-/ +axiom evalIRExpr_eq_evalYulExpr : ... +``` + +### Property Test Tags + +Property tests must match Lean theorem names exactly: + +```solidity +/// Property: store_retrieve_roundtrip +function testProp_StoreRetrieveRoundtrip(...) public { ... } +``` + +Tag format: `/// Property: exact_theorem_name` + +### What NOT to Include + +❌ **Stale TODOs** in completed code +❌ **Difficulty estimates** after proof is done +❌ **Verbose explanations** of obvious code +❌ **Status claims** that don't match reality + +✅ **Brief descriptions** of what code does +✅ **Links** to related issues for context +✅ **Explanations** of non-obvious design choices +✅ **Accurate status** in module headers + ## Development **Layer 3 proofs**: Read [Compiler/Proofs/README.md](Compiler/Proofs/README.md), study completed proofs (`assign_equiv`, `storageLoad_equiv`), use templates