From 9f79dabb8205ee9fe116173bb19939939e5b3730 Mon Sep 17 00:00:00 2001 From: Brandon Schneider Date: Tue, 26 May 2026 22:52:52 -0500 Subject: [PATCH] feat(skills): extend lean-proof skill with anti-drift rules MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds 6 new sections addressing concrete drift patterns found by auditing the Compiler surface: 1. ofFloat leakage — Compiler-surface modules (RRC.*, AVMIsa.*, ReceiptCore) must have zero ofFloat calls in any compute path; undocumented magic integers are a bug. 2. #eval witness contract — every #eval must carry a '-- expect:' comment with a hand-computed expected value; treat divergence as a failing test. 3. Namespace/closing discipline — namespace X must close with 'end X' as the last non-blank line; no file-level open leakage; BEq RRCShape pitfall documented. 4. Lakefile/Compiler surface discipline — Compiler roots are frozen; job-count decrease after a change is an error signal. 5. Schema and claim_boundary strings — versioned, named, must not be renamed; table of current schemas added; vague strings forbidden. 6. Promotion gate invariant — promotion=not_promoted is a hard invariant; Promotion.candidate in any new code requires user approval. Also adds: axiom/unsafe/native_decide prohibition, canonical Python shim BOUNDARY comment format (exact format, PARTIAL BOUNDARY for mixed files). Generated with [Devin](https://cli.devin.ai/docs) Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com> --- .devin/skills/lean-proof/SKILL.md | 120 ++++++++++++++++++++++++++---- 1 file changed, 106 insertions(+), 14 deletions(-) diff --git a/.devin/skills/lean-proof/SKILL.md b/.devin/skills/lean-proof/SKILL.md index 72071611..4eaed95a 100644 --- a/.devin/skills/lean-proof/SKILL.md +++ b/.devin/skills/lean-proof/SKILL.md @@ -113,24 +113,115 @@ Proofs that are justified: - **No `Float` in compute paths.** `ofFloat` is only permitted at the external boundary (parsing JSON, reading sensor data) and must be immediately bracketed. + In particular: Compiler-surface modules (`Semantics.RRC.*`, `Semantics.AVMIsa.*`, + `Semantics.ReceiptCore`) must contain zero `ofFloat` calls in any definition + that feeds into a receipt, score, or gate decision. - Use `Q16_16.ofRatio num den` for rational constants. -- Use `Q16_16.ofRawInt` when the raw integer encoding is documented with its - float equivalent in a comment (e.g., `Q16_16.ofRawInt 53739 -- 0.82`). -- Arithmetic: `Q16_16.add`, `.sub`, `.mul`, `.div` — never native `+` on `Int` - unless building a raw value for `ofRawInt`. +- Use `Q16_16.ofRawInt` only when the raw integer is documented with its float + equivalent in a comment on the same line: + `Q16_16.ofRawInt 53739 -- 0.82 * 65536` + An undocumented magic integer is a bug. +- Arithmetic inside `def` bodies: accumulate in raw `Int`, then call `Q16_16.ofRawInt` + once at the end. Never use native `+` / `*` on two `Q16_16` values without going + through `Q16_16.mul` / `Q16_16.add`. -## Namespace and Import Conventions +## #eval Witness Contract -- Modules under `Semantics/RRC/` import `Semantics.RRC.Emit` for `RRCShape`, - `WitnessStatus`, `AlignmentStatus`, and `FixtureRow`. -- To use `RRCShape` constructors with dot notation, add: +Every `#eval` in a Compiler-surface module **must** carry a `-- expect:` comment +on the same or preceding line stating the expected output: + +```lean +#eval determineAlignment fixtureClf -- expect: alignedExact +#eval (emitFixture.totalRows, emitFixture.candidateRows) -- expect: (6, 3) +``` + +- The expected value must be hand-computed or derived from first principles, not + copy-pasted from a previous build output. +- After each build, manually confirm the `info:` lines from `lake build` match + the `-- expect:` comments. If they diverge, treat it as a failing test. +- `#eval` blocks without `-- expect:` comments are **not acceptable** in new code. + Existing ones without comments should be annotated when the file is next touched. + +## Namespace and Closing Discipline + +- Every module must open with `namespace Semantics.X.Y` and close with + `end Semantics.X.Y` (exact match, including case). +- The closing `end` must be the last non-blank line of the file. +- `open` statements are scoped to the namespace block only; do not `open` at file + level outside a namespace (causes leakage into downstream imports). +- To use `RRCShape` constructors with dot notation, add inside the namespace: `open Semantics.RRCLogogramProjection` -- `DecidableEq RRCShape` is derived but may not resolve via `==`; use exhaustive - `match` or `if decEq s t then` with the instance made explicit if needed. -- The blessed Compiler surface roots are: +- `DecidableEq RRCShape` is derived but `BEq RRCShape` is not automatically + synthesized. Use exhaustive `match` for shape comparisons, not `==`. + +## Lakefile / Compiler Surface Discipline + +- The blessed Compiler target roots are fixed: `Semantics.RRC.Emit`, `Semantics.AVMIsa.Emit`, `Semantics.RRC.Corpus278` - Do not add these as imports in new files unless intentional — importing them - is fine, but do not change their content without a build verification pass. +- **Do not add new roots to `[[lean_lib]] name = "Compiler"`** without explicit + user approval. New modules under `Semantics/RRC/` are imported by existing roots, + not added as independent Compiler roots. +- After any change to `lakefile.toml`, run `lake build Compiler` and verify the + job count matches the baseline in `0-Core-Formalism/lean/Semantics/AGENTS.md`. + A job-count decrease means a module was silently dropped — investigate before + committing. + +## Schema and Claim Boundary Strings + +Receipt JSON schemas are versioned strings. Existing values must not be renamed: + +| Module | Schema string | +|---|---| +| `Semantics.RRC.Emit` | `"rrc_emit_fixture_v1"` | +| `Semantics.AVMIsa.Emit` | `"avm_canary_emit_v1"` / `"avm_rrc_corpus278_v1"` | +| `Semantics.RRC.ReceiptDensity` | `"receipt-density-scoring-only; not-a-proof; promotion=not_promoted"` | + +- To add a new schema, use the next version suffix (e.g. `_v2`) and document the + change in `ARCHITECTURE.md` §7.1. +- `claim_boundary` strings must end with `"admissibility-and-routing-pass-only"` + or an equivalent explicit limitation. Never use vague strings like `"ok"` or `"verified"`. + +## Promotion Gate Invariant + +`promotion = not_promoted` is a hard invariant at this stage of the pipeline. +No Lean definition, theorem, or `#eval` block may set `Promotion.candidate` on +any row without explicit user approval and a corresponding update to `TODO_MAP.md`. + +Violation pattern to reject: +```lean +-- Forbidden: silently promoting a row +promotion := .candidate +``` + +## Axiom / Unsafe / native_decide Prohibition + +The following are **forbidden** in all Compiler-surface modules without explicit +sign-off: +- `axiom` (introducing an unproven assumption) +- `unsafe` (bypassing the type system) +- `native_decide` (compiles to native code, bypasses kernel — allowed in test + harnesses only, never in blessed Compiler modules) + +If you believe one of these is necessary, stop, document the reason in a comment, +and flag it to the user before proceeding. + +## Python Shim BOUNDARY Comment Format + +When a Python shim's logic has been ported to Lean, the shim file must be updated +with a BOUNDARY block in this **exact format**, immediately after the docstring: + +```python +# BOUNDARY: Python thin IO shim; logic in . +# - python_function_name → Lean.Module.Name.leanDefinitionName +# - ... +``` + +- One entry per ported function. +- Lean module name must be fully qualified. +- The comment must appear **before** any `import` statements that are not part of + the original shim header. +- If a file still contains un-ported logic, the BOUNDARY comment must say + `# PARTIAL BOUNDARY` and list both what is ported and what remains. ## Reference Files @@ -141,4 +232,5 @@ Proofs that are justified: - RRC alignment gate: `Semantics/RRC/Emit.lean` - Receipt density scoring: `Semantics/RRC/ReceiptDensity.lean` - Logogram projection types: `Semantics/RRCLogogramProjection.lean` -- Sorry/TODO audit: `TODO_MAP.md` (project root) +- Sorry/TODO audit and porting queue: `TODO_MAP.md` (project root) +- Architecture and output boundary: `ARCHITECTURE.md` §7.1